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