1 /**CFile****************************************************************
2 
3   FileName    [satInter.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [SAT sat_solver.]
8 
9   Synopsis    [Interpolation package.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - June 20, 2005.]
16 
17   Revision    [$Id: satInter.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
18 
19 ***********************************************************************/
20 
21 #include <stdio.h>
22 #include <stdlib.h>
23 #include <string.h>
24 #include <assert.h>
25 
26 #include "satStore.h"
27 
28 ABC_NAMESPACE_IMPL_START
29 
30 
31 ////////////////////////////////////////////////////////////////////////
32 ///                        DECLARATIONS                              ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 // variable assignments
36 static const lit    LIT_UNDEF = 0xffffffff;
37 
38 // interpolation manager
39 struct Int_Man_t_
40 {
41     // clauses of the problems
42     Sto_Man_t *     pCnf;         // the set of CNF clauses for A and B
43     int             pGloVars[16]; // global variables
44     int             nGloVars;     // the number of global variables
45     // various parameters
46     int             fVerbose;     // verbosiness flag
47     int             fProofVerif;  // verifies the proof
48     int             fProofWrite;  // writes the proof file
49     int             nVarsAlloc;   // the allocated size of var arrays
50     int             nClosAlloc;   // the allocated size of clause arrays
51     // internal BCP
52     int             nRootSize;    // the number of root level assignments
53     int             nTrailSize;   // the number of assignments made
54     lit *           pTrail;       // chronological order of assignments (size nVars)
55     lit *           pAssigns;     // assignments by variable (size nVars)
56     char *          pSeens;       // temporary mark (size nVars)
57     Sto_Cls_t **    pReasons;     // reasons for each assignment (size nVars)
58     Sto_Cls_t **    pWatches;     // watched clauses for each literal (size 2*nVars)
59     // interpolation data
60     int             nVarsAB;      // the number of global variables
61     int *           pVarTypes;    // variable type (size nVars) [1=A, 0=B, <0=AB]
62     unsigned *      pInters;      // storage for interpolants as truth tables (size nClauses)
63     int             nIntersAlloc; // the allocated size of truth table array
64     int             nWords;       // the number of words in the truth table
65     // proof recording
66     int             Counter;      // counter of resolved clauses
67     int *           pProofNums;   // the proof numbers for each clause (size nClauses)
68     FILE *          pFile;        // the file for proof recording
69     // internal verification
70     lit *           pResLits;     // the literals of the resolvent
71     int             nResLits;     // the number of literals of the resolvent
72     int             nResLitsAlloc;// the number of literals of the resolvent
73     // runtime stats
74     abctime         timeBcp;      // the runtime for BCP
75     abctime         timeTrace;    // the runtime of trace construction
76     abctime         timeTotal;    // the total runtime of interpolation
77 };
78 
79 // procedure to get hold of the clauses' truth table
Int_ManTruthRead(Int_Man_t * p,Sto_Cls_t * pCls)80 static inline unsigned * Int_ManTruthRead( Int_Man_t * p, Sto_Cls_t * pCls )          { return p->pInters + pCls->Id * p->nWords;                 }
Int_ManTruthClear(unsigned * p,int nWords)81 static inline void       Int_ManTruthClear( unsigned * p, int nWords )                { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i]  =  0;    }
Int_ManTruthFill(unsigned * p,int nWords)82 static inline void       Int_ManTruthFill( unsigned * p, int nWords )                 { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i]  = ~0;    }
Int_ManTruthCopy(unsigned * p,unsigned * q,int nWords)83 static inline void       Int_ManTruthCopy( unsigned * p, unsigned * q, int nWords )   { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i]  =  q[i]; }
Int_ManTruthAnd(unsigned * p,unsigned * q,int nWords)84 static inline void       Int_ManTruthAnd( unsigned * p, unsigned * q, int nWords )    { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &=  q[i]; }
Int_ManTruthOr(unsigned * p,unsigned * q,int nWords)85 static inline void       Int_ManTruthOr( unsigned * p, unsigned * q, int nWords )     { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |=  q[i]; }
Int_ManTruthOrNot(unsigned * p,unsigned * q,int nWords)86 static inline void       Int_ManTruthOrNot( unsigned * p, unsigned * q, int nWords )  { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= ~q[i]; }
87 
88 // reading/writing the proof for a clause
Int_ManProofGet(Int_Man_t * p,Sto_Cls_t * pCls)89 static inline int        Int_ManProofGet( Int_Man_t * p, Sto_Cls_t * pCls )           { return p->pProofNums[pCls->Id];  }
Int_ManProofSet(Int_Man_t * p,Sto_Cls_t * pCls,int n)90 static inline void       Int_ManProofSet( Int_Man_t * p, Sto_Cls_t * pCls, int n )    { p->pProofNums[pCls->Id] = n;     }
91 
92 ////////////////////////////////////////////////////////////////////////
93 ///                     FUNCTION DEFINITIONS                         ///
94 ////////////////////////////////////////////////////////////////////////
95 
96 /**Function*************************************************************
97 
98   Synopsis    [Allocate proof manager.]
99 
100   Description []
101 
102   SideEffects []
103 
104   SeeAlso     []
105 
106 ***********************************************************************/
Int_ManAlloc()107 Int_Man_t * Int_ManAlloc()
108 {
109     Int_Man_t * p;
110     // allocate the manager
111     p = (Int_Man_t *)ABC_ALLOC( char, sizeof(Int_Man_t) );
112     memset( p, 0, sizeof(Int_Man_t) );
113     // verification
114     p->nResLitsAlloc = (1<<16);
115     p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc );
116     // parameters
117     p->fProofWrite = 0;
118     p->fProofVerif = 1;
119     return p;
120 }
121 
122 /**Function*************************************************************
123 
124   Synopsis    [Allocate proof manager.]
125 
126   Description []
127 
128   SideEffects []
129 
130   SeeAlso     []
131 
132 ***********************************************************************/
Int_ManSetGlobalVars(Int_Man_t * p,int nGloVars)133 int * Int_ManSetGlobalVars( Int_Man_t * p, int nGloVars )
134 {
135     p->nGloVars = nGloVars;
136     return p->pGloVars;
137 }
138 
139 /**Function*************************************************************
140 
141   Synopsis    [Count common variables in the clauses of A and B.]
142 
143   Description []
144 
145   SideEffects []
146 
147   SeeAlso     []
148 
149 ***********************************************************************/
Int_ManGlobalVars(Int_Man_t * p)150 int Int_ManGlobalVars( Int_Man_t * p )
151 {
152     Sto_Cls_t * pClause;
153     int Var, nVarsAB, v;
154 
155     // mark the variable encountered in the clauses of A
156     Sto_ManForEachClauseRoot( p->pCnf, pClause )
157     {
158         if ( !pClause->fA )
159             break;
160         for ( v = 0; v < (int)pClause->nLits; v++ )
161             p->pVarTypes[lit_var(pClause->pLits[v])] = 1;
162     }
163 
164     if ( p->nGloVars )
165     {
166         for ( v = 0; v < p->nGloVars; v++ )
167             p->pVarTypes[ p->pGloVars[v] ] = - v - 1;
168         return p->nGloVars;
169     }
170 
171     // check variables that appear in clauses of B
172     nVarsAB = 0;
173     Sto_ManForEachClauseRoot( p->pCnf, pClause )
174     {
175         if ( pClause->fA )
176             continue;
177         for ( v = 0; v < (int)pClause->nLits; v++ )
178         {
179             Var = lit_var(pClause->pLits[v]);
180             if ( p->pVarTypes[Var] == 1 ) // var of A
181             {
182                 // change it into a global variable
183                 nVarsAB++;
184                 p->pVarTypes[Var] = -1;
185             }
186         }
187     }
188 
189     // order global variables
190     nVarsAB = 0;
191     for ( v = 0; v < p->pCnf->nVars; v++ )
192         if ( p->pVarTypes[v] == -1 )
193             p->pVarTypes[v] -= nVarsAB++;
194 //printf( "There are %d global variables.\n", nVarsAB );
195     return nVarsAB;
196 }
197 
198 /**Function*************************************************************
199 
200   Synopsis    [Resize proof manager.]
201 
202   Description []
203 
204   SideEffects []
205 
206   SeeAlso     []
207 
208 ***********************************************************************/
Int_ManResize(Int_Man_t * p)209 void Int_ManResize( Int_Man_t * p )
210 {
211     // check if resizing is needed
212     if ( p->nVarsAlloc < p->pCnf->nVars )
213     {
214         // find the new size
215         if ( p->nVarsAlloc == 0 )
216             p->nVarsAlloc = 1;
217         while ( p->nVarsAlloc < p->pCnf->nVars )
218             p->nVarsAlloc *= 2;
219         // resize the arrays
220         p->pTrail    = ABC_REALLOC(lit,         p->pTrail,    p->nVarsAlloc );
221         p->pAssigns  = ABC_REALLOC(lit,         p->pAssigns,  p->nVarsAlloc );
222         p->pSeens    = ABC_REALLOC(char,        p->pSeens,    p->nVarsAlloc );
223         p->pVarTypes = ABC_REALLOC(int,         p->pVarTypes, p->nVarsAlloc );
224         p->pReasons  = ABC_REALLOC(Sto_Cls_t *, p->pReasons,  p->nVarsAlloc );
225         p->pWatches  = ABC_REALLOC(Sto_Cls_t *, p->pWatches,  p->nVarsAlloc*2 );
226     }
227 
228     // clean the free space
229     memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars );
230     memset( p->pSeens   , 0,    sizeof(char) * p->pCnf->nVars );
231     memset( p->pVarTypes, 0,    sizeof(int) * p->pCnf->nVars );
232     memset( p->pReasons , 0,    sizeof(Sto_Cls_t *) * p->pCnf->nVars );
233     memset( p->pWatches , 0,    sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 );
234 
235     // compute the number of common variables
236     p->nVarsAB = Int_ManGlobalVars( p );
237     // compute the number of words in the truth table
238     p->nWords = (p->nVarsAB <= 5 ? 1 : (1 << (p->nVarsAB - 5)));
239 
240     // check if resizing of clauses is needed
241     if ( p->nClosAlloc < p->pCnf->nClauses )
242     {
243         // find the new size
244         if ( p->nClosAlloc == 0 )
245             p->nClosAlloc = 1;
246         while ( p->nClosAlloc < p->pCnf->nClauses )
247             p->nClosAlloc *= 2;
248         // resize the arrays
249         p->pProofNums = ABC_REALLOC(int, p->pProofNums,  p->nClosAlloc );
250     }
251     memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses );
252 
253     // check if resizing of truth tables is needed
254     if ( p->nIntersAlloc < p->nWords * p->pCnf->nClauses )
255     {
256         p->nIntersAlloc = p->nWords * p->pCnf->nClauses;
257         p->pInters = ABC_REALLOC(unsigned, p->pInters, p->nIntersAlloc );
258     }
259 //    memset( p->pInters, 0, sizeof(unsigned) * p->nWords * p->pCnf->nClauses );
260 }
261 
262 /**Function*************************************************************
263 
264   Synopsis    [Deallocate proof manager.]
265 
266   Description []
267 
268   SideEffects []
269 
270   SeeAlso     []
271 
272 ***********************************************************************/
Int_ManFree(Int_Man_t * p)273 void Int_ManFree( Int_Man_t * p )
274 {
275 /*
276     printf( "Runtime stats:\n" );
277 ABC_PRT( "BCP     ", p->timeBcp   );
278 ABC_PRT( "Trace   ", p->timeTrace );
279 ABC_PRT( "TOTAL   ", p->timeTotal );
280 */
281     ABC_FREE( p->pInters );
282     ABC_FREE( p->pProofNums );
283     ABC_FREE( p->pTrail );
284     ABC_FREE( p->pAssigns );
285     ABC_FREE( p->pSeens );
286     ABC_FREE( p->pVarTypes );
287     ABC_FREE( p->pReasons );
288     ABC_FREE( p->pWatches );
289     ABC_FREE( p->pResLits );
290     ABC_FREE( p );
291 }
292 
293 
294 
295 
296 /**Function*************************************************************
297 
298   Synopsis    [Prints the clause.]
299 
300   Description []
301 
302   SideEffects []
303 
304   SeeAlso     []
305 
306 ***********************************************************************/
Int_ManPrintClause(Int_Man_t * p,Sto_Cls_t * pClause)307 void Int_ManPrintClause( Int_Man_t * p, Sto_Cls_t * pClause )
308 {
309     int i;
310     printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Int_ManProofGet(p, pClause) );
311     for ( i = 0; i < (int)pClause->nLits; i++ )
312         printf( " %d", pClause->pLits[i] );
313     printf( " }\n" );
314 }
315 
316 /**Function*************************************************************
317 
318   Synopsis    [Prints the resolvent.]
319 
320   Description []
321 
322   SideEffects []
323 
324   SeeAlso     []
325 
326 ***********************************************************************/
Int_ManPrintResolvent(lit * pResLits,int nResLits)327 void Int_ManPrintResolvent( lit * pResLits, int nResLits )
328 {
329     int i;
330     printf( "Resolvent: {" );
331     for ( i = 0; i < nResLits; i++ )
332         printf( " %d", pResLits[i] );
333     printf( " }\n" );
334 }
335 
336 /**Function*************************************************************
337 
338   Synopsis    [Records the proof.]
339 
340   Description []
341 
342   SideEffects []
343 
344   SeeAlso     []
345 
346 ***********************************************************************/
Extra_PrintBinary__(FILE * pFile,unsigned Sign[],int nBits)347 void Extra_PrintBinary__( FILE * pFile, unsigned Sign[], int nBits )
348 {
349     int Remainder, nWords;
350     int w, i;
351 
352     Remainder = (nBits%(sizeof(unsigned)*8));
353     nWords    = (nBits/(sizeof(unsigned)*8)) + (Remainder>0);
354 
355     for ( w = nWords-1; w >= 0; w-- )
356         for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- )
357             fprintf( pFile, "%c", '0' + (int)((Sign[w] & (1<<i)) > 0) );
358 }
359 
360 /**Function*************************************************************
361 
362   Synopsis    [Prints the interpolant for one clause.]
363 
364   Description []
365 
366   SideEffects []
367 
368   SeeAlso     []
369 
370 ***********************************************************************/
Int_ManPrintInterOne(Int_Man_t * p,Sto_Cls_t * pClause)371 void Int_ManPrintInterOne( Int_Man_t * p, Sto_Cls_t * pClause )
372 {
373     printf( "Clause %2d :  ", pClause->Id );
374     Extra_PrintBinary__( stdout, Int_ManTruthRead(p, pClause), (1 << p->nVarsAB) );
375     printf( "\n" );
376 }
377 
378 
379 
380 /**Function*************************************************************
381 
382   Synopsis    [Adds one clause to the watcher list.]
383 
384   Description []
385 
386   SideEffects []
387 
388   SeeAlso     []
389 
390 ***********************************************************************/
Int_ManWatchClause(Int_Man_t * p,Sto_Cls_t * pClause,lit Lit)391 static inline void Int_ManWatchClause( Int_Man_t * p, Sto_Cls_t * pClause, lit Lit )
392 {
393     assert( lit_check(Lit, p->pCnf->nVars) );
394     if ( pClause->pLits[0] == Lit )
395         pClause->pNext0 = p->pWatches[lit_neg(Lit)];
396     else
397     {
398         assert( pClause->pLits[1] == Lit );
399         pClause->pNext1 = p->pWatches[lit_neg(Lit)];
400     }
401     p->pWatches[lit_neg(Lit)] = pClause;
402 }
403 
404 
405 /**Function*************************************************************
406 
407   Synopsis    [Records implication.]
408 
409   Description []
410 
411   SideEffects []
412 
413   SeeAlso     []
414 
415 ***********************************************************************/
Int_ManEnqueue(Int_Man_t * p,lit Lit,Sto_Cls_t * pReason)416 static inline int Int_ManEnqueue( Int_Man_t * p, lit Lit, Sto_Cls_t * pReason )
417 {
418     int Var = lit_var(Lit);
419     if ( p->pAssigns[Var] != LIT_UNDEF )
420         return p->pAssigns[Var] == Lit;
421     p->pAssigns[Var] = Lit;
422     p->pReasons[Var] = pReason;
423     p->pTrail[p->nTrailSize++] = Lit;
424 //printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) );
425     return 1;
426 }
427 
428 /**Function*************************************************************
429 
430   Synopsis    [Records implication.]
431 
432   Description []
433 
434   SideEffects []
435 
436   SeeAlso     []
437 
438 ***********************************************************************/
Int_ManCancelUntil(Int_Man_t * p,int Level)439 static inline void Int_ManCancelUntil( Int_Man_t * p, int Level )
440 {
441     lit Lit;
442     int i, Var;
443     for ( i = p->nTrailSize - 1; i >= Level; i-- )
444     {
445         Lit = p->pTrail[i];
446         Var = lit_var( Lit );
447         p->pReasons[Var] = NULL;
448         p->pAssigns[Var] = LIT_UNDEF;
449 //printf( "cancelling var %d\n", Var );
450     }
451     p->nTrailSize = Level;
452 }
453 
454 /**Function*************************************************************
455 
456   Synopsis    [Propagate one assignment.]
457 
458   Description []
459 
460   SideEffects []
461 
462   SeeAlso     []
463 
464 ***********************************************************************/
Int_ManPropagateOne(Int_Man_t * p,lit Lit)465 static inline Sto_Cls_t * Int_ManPropagateOne( Int_Man_t * p, lit Lit )
466 {
467     Sto_Cls_t ** ppPrev, * pCur, * pTemp;
468     lit LitF = lit_neg(Lit);
469     int i;
470     // iterate through the literals
471     ppPrev = p->pWatches + Lit;
472     for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev )
473     {
474         // make sure the false literal is in the second literal of the clause
475         if ( pCur->pLits[0] == LitF )
476         {
477             pCur->pLits[0] = pCur->pLits[1];
478             pCur->pLits[1] = LitF;
479             pTemp = pCur->pNext0;
480             pCur->pNext0 = pCur->pNext1;
481             pCur->pNext1 = pTemp;
482         }
483         assert( pCur->pLits[1] == LitF );
484 
485         // if the first literal is true, the clause is satisfied
486         if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] )
487         {
488             ppPrev = &pCur->pNext1;
489             continue;
490         }
491 
492         // look for a new literal to watch
493         for ( i = 2; i < (int)pCur->nLits; i++ )
494         {
495             // skip the case when the literal is false
496             if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] )
497                 continue;
498             // the literal is either true or unassigned - watch it
499             pCur->pLits[1] = pCur->pLits[i];
500             pCur->pLits[i] = LitF;
501             // remove this clause from the watch list of Lit
502             *ppPrev = pCur->pNext1;
503             // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1])
504             Int_ManWatchClause( p, pCur, pCur->pLits[1] );
505             break;
506         }
507         if ( i < (int)pCur->nLits ) // found new watch
508             continue;
509 
510         // clause is unit - enqueue new implication
511         if ( Int_ManEnqueue(p, pCur->pLits[0], pCur) )
512         {
513             ppPrev = &pCur->pNext1;
514             continue;
515         }
516 
517         // conflict detected - return the conflict clause
518         return pCur;
519     }
520     return NULL;
521 }
522 
523 /**Function*************************************************************
524 
525   Synopsis    [Propagate the current assignments.]
526 
527   Description []
528 
529   SideEffects []
530 
531   SeeAlso     []
532 
533 ***********************************************************************/
Int_ManPropagate(Int_Man_t * p,int Start)534 Sto_Cls_t * Int_ManPropagate( Int_Man_t * p, int Start )
535 {
536     Sto_Cls_t * pClause;
537     int i;
538     abctime clk = Abc_Clock();
539     for ( i = Start; i < p->nTrailSize; i++ )
540     {
541         pClause = Int_ManPropagateOne( p, p->pTrail[i] );
542         if ( pClause )
543         {
544 p->timeBcp += Abc_Clock() - clk;
545             return pClause;
546         }
547     }
548 p->timeBcp += Abc_Clock() - clk;
549     return NULL;
550 }
551 
552 
553 /**Function*************************************************************
554 
555   Synopsis    [Writes one root clause into a file.]
556 
557   Description []
558 
559   SideEffects []
560 
561   SeeAlso     []
562 
563 ***********************************************************************/
Int_ManProofWriteOne(Int_Man_t * p,Sto_Cls_t * pClause)564 void Int_ManProofWriteOne( Int_Man_t * p, Sto_Cls_t * pClause )
565 {
566     Int_ManProofSet( p, pClause, ++p->Counter );
567 
568     if ( p->fProofWrite )
569     {
570         int v;
571         fprintf( p->pFile, "%d", Int_ManProofGet(p, pClause) );
572         for ( v = 0; v < (int)pClause->nLits; v++ )
573             fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) );
574         fprintf( p->pFile, " 0 0\n" );
575     }
576 }
577 
578 /**Function*************************************************************
579 
580   Synopsis    [Traces the proof for one clause.]
581 
582   Description []
583 
584   SideEffects []
585 
586   SeeAlso     []
587 
588 ***********************************************************************/
Int_ManProofTraceOne(Int_Man_t * p,Sto_Cls_t * pConflict,Sto_Cls_t * pFinal)589 int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFinal )
590 {
591     Sto_Cls_t * pReason;
592     int i, v, Var, PrevId;
593     int fPrint = 0;
594     abctime clk = Abc_Clock();
595 
596     // collect resolvent literals
597     if ( p->fProofVerif )
598     {
599         assert( (int)pConflict->nLits <= p->nResLitsAlloc );
600         memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits );
601         p->nResLits = pConflict->nLits;
602     }
603 
604     // mark all the variables in the conflict as seen
605     for ( v = 0; v < (int)pConflict->nLits; v++ )
606         p->pSeens[lit_var(pConflict->pLits[v])] = 1;
607 
608     // start the anticedents
609 //    pFinal->pAntis = Vec_PtrAlloc( 32 );
610 //    Vec_PtrPush( pFinal->pAntis, pConflict );
611 
612     if ( p->pCnf->nClausesA )
613         Int_ManTruthCopy( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pConflict), p->nWords );
614 
615     // follow the trail backwards
616     PrevId = Int_ManProofGet(p, pConflict);
617     for ( i = p->nTrailSize - 1; i >= 0; i-- )
618     {
619         // skip literals that are not involved
620         Var = lit_var(p->pTrail[i]);
621         if ( !p->pSeens[Var] )
622             continue;
623         p->pSeens[Var] = 0;
624 
625         // skip literals of the resulting clause
626         pReason = p->pReasons[Var];
627         if ( pReason == NULL )
628             continue;
629         assert( p->pTrail[i] == pReason->pLits[0] );
630 
631         // add the variables to seen
632         for ( v = 1; v < (int)pReason->nLits; v++ )
633             p->pSeens[lit_var(pReason->pLits[v])] = 1;
634 
635 
636         // record the reason clause
637         assert( Int_ManProofGet(p, pReason) > 0 );
638         p->Counter++;
639         if ( p->fProofWrite )
640             fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Int_ManProofGet(p, pReason) );
641         PrevId = p->Counter;
642 
643         if ( p->pCnf->nClausesA )
644         {
645             if ( p->pVarTypes[Var] == 1 ) // var of A
646                 Int_ManTruthOr( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pReason), p->nWords );
647             else
648                 Int_ManTruthAnd( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pReason), p->nWords );
649         }
650 
651         // resolve the temporary resolvent with the reason clause
652         if ( p->fProofVerif )
653         {
654             int v1, v2;
655             if ( fPrint )
656                 Int_ManPrintResolvent( p->pResLits, p->nResLits );
657             // check that the var is present in the resolvent
658             for ( v1 = 0; v1 < p->nResLits; v1++ )
659                 if ( lit_var(p->pResLits[v1]) == Var )
660                     break;
661             if ( v1 == p->nResLits )
662                 printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var );
663             if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) )
664                 printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var );
665             // remove this variable from the resolvent
666             assert( lit_var(p->pResLits[v1]) == Var );
667             p->nResLits--;
668             for ( ; v1 < p->nResLits; v1++ )
669                 p->pResLits[v1] = p->pResLits[v1+1];
670             // add variables of the reason clause
671             for ( v2 = 1; v2 < (int)pReason->nLits; v2++ )
672             {
673                 for ( v1 = 0; v1 < p->nResLits; v1++ )
674                     if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) )
675                         break;
676                 // if it is a new variable, add it to the resolvent
677                 if ( v1 == p->nResLits )
678                 {
679                     if ( p->nResLits == p->nResLitsAlloc )
680                         printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n", pFinal->Id );
681                     p->pResLits[ p->nResLits++ ] = pReason->pLits[v2];
682                     continue;
683                 }
684                 // if the variable is the same, the literal should be the same too
685                 if ( p->pResLits[v1] == pReason->pLits[v2] )
686                     continue;
687                 // the literal is different
688                 printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id );
689             }
690         }
691 
692 //        Vec_PtrPush( pFinal->pAntis, pReason );
693     }
694 
695     // unmark all seen variables
696 //    for ( i = p->nTrailSize - 1; i >= 0; i-- )
697 //        p->pSeens[lit_var(p->pTrail[i])] = 0;
698     // check that the literals are unmarked
699 //    for ( i = p->nTrailSize - 1; i >= 0; i-- )
700 //        assert( p->pSeens[lit_var(p->pTrail[i])] == 0 );
701 
702     // use the resulting clause to check the correctness of resolution
703     if ( p->fProofVerif )
704     {
705         int v1, v2;
706         if ( fPrint )
707             Int_ManPrintResolvent( p->pResLits, p->nResLits );
708         for ( v1 = 0; v1 < p->nResLits; v1++ )
709         {
710             for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ )
711                 if ( pFinal->pLits[v2] == p->pResLits[v1] )
712                     break;
713             if ( v2 < (int)pFinal->nLits )
714                 continue;
715             break;
716         }
717         if ( v1 < p->nResLits )
718         {
719             printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id );
720             Int_ManPrintClause( p, pConflict );
721             Int_ManPrintResolvent( p->pResLits, p->nResLits );
722             Int_ManPrintClause( p, pFinal );
723         }
724 
725         // if there are literals in the clause that are not in the resolvent
726         // it means that the derived resolvent is stronger than the clause
727         // we can replace the clause with the resolvent by removing these literals
728         if ( p->nResLits != (int)pFinal->nLits )
729         {
730             for ( v1 = 0; v1 < (int)pFinal->nLits; v1++ )
731             {
732                 for ( v2 = 0; v2 < p->nResLits; v2++ )
733                     if ( pFinal->pLits[v1] == p->pResLits[v2] )
734                         break;
735                 if ( v2 < p->nResLits )
736                     continue;
737                 // remove literal v1 from the final clause
738                 pFinal->nLits--;
739                 for ( v2 = v1; v2 < (int)pFinal->nLits; v2++ )
740                     pFinal->pLits[v2] = pFinal->pLits[v2+1];
741                 v1--;
742             }
743             assert( p->nResLits == (int)pFinal->nLits );
744         }
745     }
746 p->timeTrace += Abc_Clock() - clk;
747 
748     // return the proof pointer
749     if ( p->pCnf->nClausesA )
750     {
751 //        Int_ManPrintInterOne( p, pFinal );
752     }
753     Int_ManProofSet( p, pFinal, p->Counter );
754     // make sure the same proof ID is not asssigned to two consecutive clauses
755     assert( p->pProofNums[pFinal->Id-1] != p->Counter );
756     return p->Counter;
757 }
758 
759 /**Function*************************************************************
760 
761   Synopsis    [Records the proof for one clause.]
762 
763   Description []
764 
765   SideEffects []
766 
767   SeeAlso     []
768 
769 ***********************************************************************/
Int_ManProofRecordOne(Int_Man_t * p,Sto_Cls_t * pClause)770 int Int_ManProofRecordOne( Int_Man_t * p, Sto_Cls_t * pClause )
771 {
772     Sto_Cls_t * pConflict;
773     int i;
774 
775     // empty clause never ends up there
776     assert( pClause->nLits > 0 );
777     if ( pClause->nLits == 0 )
778         printf( "Error: Empty clause is attempted.\n" );
779 
780     // add assumptions to the trail
781     assert( !pClause->fRoot );
782     assert( p->nTrailSize == p->nRootSize );
783 
784     // if any of the clause literals are already assumed
785     // it means that the clause is redundant and can be skipped
786     for ( i = 0; i < (int)pClause->nLits; i++ )
787         if ( p->pAssigns[lit_var(pClause->pLits[i])] == pClause->pLits[i] )
788             return 1;
789 
790     for ( i = 0; i < (int)pClause->nLits; i++ )
791         if ( !Int_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
792         {
793             assert( 0 ); // impossible
794             return 0;
795         }
796 
797     // propagate the assumptions
798     pConflict = Int_ManPropagate( p, p->nRootSize );
799     if ( pConflict == NULL )
800     {
801         assert( 0 ); // cannot prove
802         return 0;
803     }
804 
805     // skip the clause if it is weaker or the same as the conflict clause
806     if ( pClause->nLits >= pConflict->nLits )
807     {
808         // check if every literal of conflict clause can be found in the given clause
809         int j;
810         for ( i = 0; i < (int)pConflict->nLits; i++ )
811         {
812             for ( j = 0; j < (int)pClause->nLits; j++ )
813                 if ( pConflict->pLits[i] == pClause->pLits[j] )
814                     break;
815             if ( j == (int)pClause->nLits ) // literal pConflict->pLits[i] is not found
816                 break;
817         }
818         if ( i == (int)pConflict->nLits ) // all lits are found
819         {
820             // undo to the root level
821             Int_ManCancelUntil( p, p->nRootSize );
822             return 1;
823         }
824     }
825 
826     // construct the proof
827     Int_ManProofTraceOne( p, pConflict, pClause );
828 
829     // undo to the root level
830     Int_ManCancelUntil( p, p->nRootSize );
831 
832     // add large clauses to the watched lists
833     if ( pClause->nLits > 1 )
834     {
835         Int_ManWatchClause( p, pClause, pClause->pLits[0] );
836         Int_ManWatchClause( p, pClause, pClause->pLits[1] );
837         return 1;
838     }
839     assert( pClause->nLits == 1 );
840 
841     // if the clause proved is unit, add it and propagate
842     if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) )
843     {
844         assert( 0 ); // impossible
845         return 0;
846     }
847 
848     // propagate the assumption
849     pConflict = Int_ManPropagate( p, p->nRootSize );
850     if ( pConflict )
851     {
852         // construct the proof
853         Int_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty );
854         if ( p->fVerbose )
855             printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id );
856         return 0;
857     }
858 
859     // update the root level
860     p->nRootSize = p->nTrailSize;
861     return 1;
862 }
863 
864 /**Function*************************************************************
865 
866   Synopsis    [Propagate the root clauses.]
867 
868   Description []
869 
870   SideEffects []
871 
872   SeeAlso     []
873 
874 ***********************************************************************/
Int_ManProcessRoots(Int_Man_t * p)875 int Int_ManProcessRoots( Int_Man_t * p )
876 {
877     Sto_Cls_t * pClause;
878     int Counter;
879 
880     // make sure the root clauses are preceeding the learnt clauses
881     Counter = 0;
882     Sto_ManForEachClause( p->pCnf, pClause )
883     {
884         assert( (int)pClause->fA    == (Counter < (int)p->pCnf->nClausesA) );
885         assert( (int)pClause->fRoot == (Counter < (int)p->pCnf->nRoots)    );
886         Counter++;
887     }
888     assert( p->pCnf->nClauses == Counter );
889 
890     // make sure the last clause if empty
891     assert( p->pCnf->pTail->nLits == 0 );
892 
893     // go through the root unit clauses
894     p->nTrailSize = 0;
895     Sto_ManForEachClauseRoot( p->pCnf, pClause )
896     {
897         // create watcher lists for the root clauses
898         if ( pClause->nLits > 1 )
899         {
900             Int_ManWatchClause( p, pClause, pClause->pLits[0] );
901             Int_ManWatchClause( p, pClause, pClause->pLits[1] );
902         }
903         // empty clause and large clauses
904         if ( pClause->nLits != 1 )
905             continue;
906         // unit clause
907         assert( lit_check(pClause->pLits[0], p->pCnf->nVars) );
908         if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) )
909         {
910             // detected root level conflict
911 //            printf( "Error in Int_ManProcessRoots(): Detected a root-level conflict too early!\n" );
912 //            assert( 0 );
913             // detected root level conflict
914             Int_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
915             if ( p->fVerbose )
916                 printf( "Found root level conflict!\n" );
917             return 0;
918         }
919     }
920 
921     // propagate the root unit clauses
922     pClause = Int_ManPropagate( p, 0 );
923     if ( pClause )
924     {
925         // detected root level conflict
926         Int_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
927         if ( p->fVerbose )
928             printf( "Found root level conflict!\n" );
929         return 0;
930     }
931 
932     // set the root level
933     p->nRootSize = p->nTrailSize;
934     return 1;
935 }
936 
937 /**Function*************************************************************
938 
939   Synopsis    [Records the proof.]
940 
941   Description []
942 
943   SideEffects []
944 
945   SeeAlso     []
946 
947 ***********************************************************************/
Int_ManPrepareInter(Int_Man_t * p)948 void Int_ManPrepareInter( Int_Man_t * p )
949 {
950     // elementary truth tables
951     unsigned uTruths[8][8] = {
952         { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
953         { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
954         { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
955         { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
956         { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 },
957         { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF },
958         { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF },
959         { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF }
960     };
961     Sto_Cls_t * pClause;
962     int Var, VarAB, v;
963     assert( p->nVarsAB <= 8 );
964 
965     // set interpolants for root clauses
966     Sto_ManForEachClauseRoot( p->pCnf, pClause )
967     {
968         if ( !pClause->fA ) // clause of B
969         {
970             Int_ManTruthFill( Int_ManTruthRead(p, pClause), p->nWords );
971 //            Int_ManPrintInterOne( p, pClause );
972             continue;
973         }
974         // clause of A
975         Int_ManTruthClear( Int_ManTruthRead(p, pClause), p->nWords );
976         for ( v = 0; v < (int)pClause->nLits; v++ )
977         {
978             Var = lit_var(pClause->pLits[v]);
979             if ( p->pVarTypes[Var] < 0 ) // global var
980             {
981                 VarAB = -p->pVarTypes[Var]-1;
982                 assert( VarAB >= 0 && VarAB < p->nVarsAB );
983                 if ( lit_sign(pClause->pLits[v]) ) // negative var
984                     Int_ManTruthOrNot( Int_ManTruthRead(p, pClause), uTruths[VarAB], p->nWords );
985                 else
986                     Int_ManTruthOr( Int_ManTruthRead(p, pClause), uTruths[VarAB], p->nWords );
987             }
988         }
989 //        Int_ManPrintInterOne( p, pClause );
990     }
991 }
992 
993 /**Function*************************************************************
994 
995   Synopsis    [Computes interpolant for the given CNF.]
996 
997   Description [Returns the number of common variable found and interpolant.
998   Returns 0, if something did not work.]
999 
1000   SideEffects []
1001 
1002   SeeAlso     []
1003 
1004 ***********************************************************************/
Int_ManInterpolate(Int_Man_t * p,Sto_Man_t * pCnf,int fVerbose,unsigned ** ppResult)1005 int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult )
1006 {
1007     Sto_Cls_t * pClause;
1008     int RetValue = 1;
1009     abctime clkTotal = Abc_Clock();
1010 
1011     // check that the CNF makes sense
1012     assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
1013     p->pCnf = pCnf;
1014     p->fVerbose = fVerbose;
1015     *ppResult = NULL;
1016 
1017     // adjust the manager
1018     Int_ManResize( p );
1019 
1020     // prepare the interpolant computation
1021     Int_ManPrepareInter( p );
1022 
1023     // construct proof for each clause
1024     // start the proof
1025     if ( p->fProofWrite )
1026     {
1027         p->pFile = fopen( "proof.cnf_", "w" );
1028         p->Counter = 0;
1029     }
1030 
1031     // write the root clauses
1032     Sto_ManForEachClauseRoot( p->pCnf, pClause )
1033         Int_ManProofWriteOne( p, pClause );
1034 
1035     // propagate root level assignments
1036     if ( Int_ManProcessRoots( p ) )
1037     {
1038         // if there is no conflict, consider learned clauses
1039         Sto_ManForEachClause( p->pCnf, pClause )
1040         {
1041             if ( pClause->fRoot )
1042                 continue;
1043             if ( !Int_ManProofRecordOne( p, pClause ) )
1044             {
1045                 RetValue = 0;
1046                 break;
1047             }
1048         }
1049     }
1050 
1051     // stop the proof
1052     if ( p->fProofWrite )
1053     {
1054         fclose( p->pFile );
1055         p->pFile = NULL;
1056     }
1057 
1058     if ( fVerbose )
1059     {
1060     printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f MB\n",
1061         p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,
1062         1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),
1063         1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
1064 p->timeTotal += Abc_Clock() - clkTotal;
1065     }
1066 
1067     *ppResult = Int_ManTruthRead( p, p->pCnf->pTail );
1068     return p->nVarsAB;
1069 }
1070 
1071 ////////////////////////////////////////////////////////////////////////
1072 ///                       END OF FILE                                ///
1073 ////////////////////////////////////////////////////////////////////////
1074 
1075 
1076 ABC_NAMESPACE_IMPL_END
1077 
1078