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