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