abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
pr.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [pr.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Proof recording.]
8 
9  Synopsis [Core procedures of the 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: pr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include <stdio.h>
22 #include <stdlib.h>
23 #include <string.h>
24 #include <assert.h>
25 
26 #include "misc/util/abc_global.h"
27 #include "pr.h"
28 
29 ABC_NAMESPACE_IMPL_START
30 
31 
32 ////////////////////////////////////////////////////////////////////////
33 /// DECLARATIONS ///
34 ////////////////////////////////////////////////////////////////////////
35 
36 typedef unsigned lit;
37 
38 typedef struct Pr_Cls_t_ Pr_Cls_t;
39 struct Pr_Cls_t_
40 {
41  unsigned uTruth; // interpolant
42  void * pProof; // the proof node
43 // void * pAntis; // the anticedents
44  Pr_Cls_t * pNext; // the next clause
45  Pr_Cls_t * pNext0; // the next 0-watch
46  Pr_Cls_t * pNext1; // the next 0-watch
47  int Id; // the clause ID
48  unsigned fA : 1; // belongs to A
49  unsigned fRoot : 1; // original clause
50  unsigned fVisit : 1; // visited clause
51  unsigned nLits : 24; // the number of literals
52  lit pLits[0]; // literals of this clause
53 };
54 
55 struct Pr_Man_t_
56 {
57  // general data
58  int fProofWrite; // writes the proof file
59  int fProofVerif; // verifies the proof
60  int nVars; // the number of variables
61  int nVarsAB; // the number of global variables
62  int nRoots; // the number of root clauses
63  int nClauses; // the number of all clauses
64  int nClausesA; // the number of clauses of A
65  Pr_Cls_t * pHead; // the head clause
66  Pr_Cls_t * pTail; // the tail clause
67  Pr_Cls_t * pLearnt; // the tail clause
68  Pr_Cls_t * pEmpty; // the empty clause
69  // internal BCP
70  int nRootSize; // the number of root level assignments
71  int nTrailSize; // the number of assignments made
72  lit * pTrail; // chronological order of assignments (size nVars)
73  lit * pAssigns; // assignments by variable (size nVars)
74  char * pSeens; // temporary mark (size nVars)
75  char * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB]
76  Pr_Cls_t ** pReasons; // reasons for each assignment (size nVars)
77  Pr_Cls_t ** pWatches; // watched clauses for each literal (size 2*nVars)
78  int nVarsAlloc; // the allocated size of arrays
79  // proof recording
80  void * pManProof; // proof manager
81  int Counter; // counter of resolved clauses
82  // memory management
83  int nChunkSize; // the number of bytes in a chunk
84  int nChunkUsed; // the number of bytes used in the last chunk
85  char * pChunkLast; // the last memory chunk
86  // internal verification
87  lit * pResLits; // the literals of the resolvent
88  int nResLits; // the number of literals of the resolvent
89  int nResLitsAlloc;// the number of literals of the resolvent
90  // runtime stats
91  abctime timeBcp;
92  abctime timeTrace;
93  abctime timeRead;
94  abctime timeTotal;
95 };
96 
97 // variable assignments
98 static const lit LIT_UNDEF = 0xffffffff;
99 
100 // variable/literal conversions (taken from MiniSat)
101 static inline lit toLit (int v) { return v + v; }
102 static inline lit toLitCond(int v, int c) { return v + v + (c != 0); }
103 static inline lit lit_neg (lit l) { return l ^ 1; }
104 static inline int lit_var (lit l) { return l >> 1; }
105 static inline int lit_sign (lit l) { return l & 1; }
106 static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
107 static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
108 static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; }
109 
110 // iterators through the clauses
111 #define Pr_ManForEachClause( p, pCls ) for( pCls = p->pHead; pCls; pCls = pCls->pNext )
112 #define Pr_ManForEachClauseRoot( p, pCls ) for( pCls = p->pHead; pCls != p->pLearnt; pCls = pCls->pNext )
113 #define Pr_ManForEachClauseLearnt( p, pCls ) for( pCls = p->pLearnt; pCls; pCls = pCls->pNext )
114 
115 // static procedures
116 static char * Pr_ManMemoryFetch( Pr_Man_t * p, int nBytes );
117 static void Pr_ManMemoryStop( Pr_Man_t * p );
118 static void Pr_ManResize( Pr_Man_t * p, int nVarsNew );
119 
120 // exported procedures
121 extern Pr_Man_t * Pr_ManAlloc( int nVarsAlloc );
122 extern void Pr_ManFree( Pr_Man_t * p );
123 extern int Pr_ManAddClause( Pr_Man_t * p, lit * pBeg, lit * pEnd, int fRoot, int fClauseA );
124 extern int Pr_ManProofWrite( Pr_Man_t * p );
125 
126 ////////////////////////////////////////////////////////////////////////
127 /// FUNCTION DEFINITIONS ///
128 ////////////////////////////////////////////////////////////////////////
129 
130 /**Function*************************************************************
131 
132  Synopsis [Allocate proof manager.]
133 
134  Description []
135 
136  SideEffects []
137 
138  SeeAlso []
139 
140 ***********************************************************************/
141 Pr_Man_t * Pr_ManAlloc( int nVarsAlloc )
142 {
143  Pr_Man_t * p;
144  // allocate the manager
145  p = (Pr_Man_t *)ABC_ALLOC( char, sizeof(Pr_Man_t) );
146  memset( p, 0, sizeof(Pr_Man_t) );
147  // allocate internal arrays
148  Pr_ManResize( p, nVarsAlloc? nVarsAlloc : 256 );
149  // set the starting number of variables
150  p->nVars = 0;
151  // memory management
152  p->nChunkSize = (1<<16); // use 64K chunks
153  // verification
154  p->nResLitsAlloc = (1<<16);
155  p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc );
156  // parameters
157  p->fProofWrite = 0;
158  p->fProofVerif = 0;
159  return p;
160 }
161 
162 /**Function*************************************************************
163 
164  Synopsis [Resize proof manager.]
165 
166  Description []
167 
168  SideEffects []
169 
170  SeeAlso []
171 
172 ***********************************************************************/
173 void Pr_ManResize( Pr_Man_t * p, int nVarsNew )
174 {
175  // check if resizing is needed
176  if ( p->nVarsAlloc < nVarsNew )
177  {
178  int nVarsAllocOld = p->nVarsAlloc;
179  // find the new size
180  if ( p->nVarsAlloc == 0 )
181  p->nVarsAlloc = 1;
182  while ( p->nVarsAlloc < nVarsNew )
183  p->nVarsAlloc *= 2;
184  // resize the arrays
185  p->pTrail = ABC_REALLOC(lit, p->pTrail, p->nVarsAlloc );
186  p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc );
187  p->pSeens = ABC_REALLOC(char, p->pSeens, p->nVarsAlloc );
188  p->pVarTypes = ABC_REALLOC(char, p->pVarTypes, p->nVarsAlloc );
189  p->pReasons = ABC_REALLOC(Pr_Cls_t *, p->pReasons, p->nVarsAlloc );
190  p->pWatches = ABC_REALLOC(Pr_Cls_t *, p->pWatches, p->nVarsAlloc*2 );
191  // clean the free space
192  memset( p->pAssigns + nVarsAllocOld, 0xff, sizeof(lit) * (p->nVarsAlloc - nVarsAllocOld) );
193  memset( p->pSeens + nVarsAllocOld, 0, sizeof(char) * (p->nVarsAlloc - nVarsAllocOld) );
194  memset( p->pVarTypes + nVarsAllocOld, 0, sizeof(char) * (p->nVarsAlloc - nVarsAllocOld) );
195  memset( p->pReasons + nVarsAllocOld, 0, sizeof(Pr_Cls_t *) * (p->nVarsAlloc - nVarsAllocOld) );
196  memset( p->pWatches + nVarsAllocOld, 0, sizeof(Pr_Cls_t *) * (p->nVarsAlloc - nVarsAllocOld)*2 );
197  }
198  // adjust the number of variables
199  if ( p->nVars < nVarsNew )
200  p->nVars = nVarsNew;
201 }
202 
203 /**Function*************************************************************
204 
205  Synopsis [Deallocate proof manager.]
206 
207  Description []
208 
209  SideEffects []
210 
211  SeeAlso []
212 
213 ***********************************************************************/
214 void Pr_ManFree( Pr_Man_t * p )
215 {
216  printf( "Runtime stats:\n" );
217 ABC_PRT( "Reading ", p->timeRead );
218 ABC_PRT( "BCP ", p->timeBcp );
219 ABC_PRT( "Trace ", p->timeTrace );
220 ABC_PRT( "TOTAL ", p->timeTotal );
221 
222  Pr_ManMemoryStop( p );
223  ABC_FREE( p->pTrail );
224  ABC_FREE( p->pAssigns );
225  ABC_FREE( p->pSeens );
226  ABC_FREE( p->pVarTypes );
227  ABC_FREE( p->pReasons );
228  ABC_FREE( p->pWatches );
229  ABC_FREE( p->pResLits );
230  ABC_FREE( p );
231 }
232 
233 /**Function*************************************************************
234 
235  Synopsis [Adds one clause to the watcher list.]
236 
237  Description []
238 
239  SideEffects []
240 
241  SeeAlso []
242 
243 ***********************************************************************/
244 static inline void Pr_ManWatchClause( Pr_Man_t * p, Pr_Cls_t * pClause, lit Lit )
245 {
246  assert( lit_check(Lit, p->nVars) );
247  if ( pClause->pLits[0] == Lit )
248  pClause->pNext0 = p->pWatches[lit_neg(Lit)];
249  else
250  {
251  assert( pClause->pLits[1] == Lit );
252  pClause->pNext1 = p->pWatches[lit_neg(Lit)];
253  }
254  p->pWatches[lit_neg(Lit)] = pClause;
255 }
256 
257 /**Function*************************************************************
258 
259  Synopsis [Adds one clause to the manager.]
260 
261  Description []
262 
263  SideEffects []
264 
265  SeeAlso []
266 
267 ***********************************************************************/
268 int Pr_ManAddClause( Pr_Man_t * p, lit * pBeg, lit * pEnd, int fRoot, int fClauseA )
269 {
270  Pr_Cls_t * pClause;
271  lit Lit, * i, * j;
272  int nSize, VarMax;
273 
274  // process the literals
275  if ( pBeg < pEnd )
276  {
277  // insertion sort
278  VarMax = lit_var( *pBeg );
279  for ( i = pBeg + 1; i < pEnd; i++ )
280  {
281  Lit = *i;
282  VarMax = lit_var(Lit) > VarMax ? lit_var(Lit) : VarMax;
283  for ( j = i; j > pBeg && *(j-1) > Lit; j-- )
284  *j = *(j-1);
285  *j = Lit;
286  }
287  // make sure there is no duplicated variables
288  for ( i = pBeg + 1; i < pEnd; i++ )
289  assert( lit_var(*(i-1)) != lit_var(*i) );
290  // resize the manager
291  Pr_ManResize( p, VarMax+1 );
292  }
293 
294  // get memory for the clause
295  nSize = sizeof(Pr_Cls_t) + sizeof(lit) * (pEnd - pBeg);
296  pClause = (Pr_Cls_t *)Pr_ManMemoryFetch( p, nSize );
297  memset( pClause, 0, sizeof(Pr_Cls_t) );
298 
299  // assign the clause
300  assert( !fClauseA || fRoot ); // clause of A is always a root clause
301  p->nRoots += fRoot;
302  p->nClausesA += fClauseA;
303  pClause->Id = p->nClauses++;
304  pClause->fA = fClauseA;
305  pClause->fRoot = fRoot;
306  pClause->nLits = pEnd - pBeg;
307  memcpy( pClause->pLits, pBeg, sizeof(lit) * (pEnd - pBeg) );
308 
309  // add the clause to the list
310  if ( p->pHead == NULL )
311  p->pHead = pClause;
312  if ( p->pTail == NULL )
313  p->pTail = pClause;
314  else
315  {
316  p->pTail->pNext = pClause;
317  p->pTail = pClause;
318  }
319 
320  // mark the first learnt clause
321  if ( p->pLearnt == NULL && !pClause->fRoot )
322  p->pLearnt = pClause;
323 
324  // add the empty clause
325  if ( pClause->nLits == 0 )
326  {
327  if ( p->pEmpty )
328  printf( "More than one empty clause!\n" );
329  p->pEmpty = pClause;
330  }
331  return 1;
332 }
333 
334 /**Function*************************************************************
335 
336  Synopsis [Fetches memory.]
337 
338  Description []
339 
340  SideEffects []
341 
342  SeeAlso []
343 
344 ***********************************************************************/
345 char * Pr_ManMemoryFetch( Pr_Man_t * p, int nBytes )
346 {
347  char * pMem;
348  if ( p->pChunkLast == NULL || nBytes > p->nChunkSize - p->nChunkUsed )
349  {
350  pMem = (char *)ABC_ALLOC( char, p->nChunkSize );
351  *(char **)pMem = p->pChunkLast;
352  p->pChunkLast = pMem;
353  p->nChunkUsed = sizeof(char *);
354  }
355  pMem = p->pChunkLast + p->nChunkUsed;
356  p->nChunkUsed += nBytes;
357  return pMem;
358 }
359 
360 /**Function*************************************************************
361 
362  Synopsis [Frees memory manager.]
363 
364  Description []
365 
366  SideEffects []
367 
368  SeeAlso []
369 
370 ***********************************************************************/
371 void Pr_ManMemoryStop( Pr_Man_t * p )
372 {
373  char * pMem, * pNext;
374  if ( p->pChunkLast == NULL )
375  return;
376  for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext )
377  ABC_FREE( pMem );
378  ABC_FREE( pMem );
379 }
380 
381 /**Function*************************************************************
382 
383  Synopsis [Reports memory usage in bytes.]
384 
385  Description []
386 
387  SideEffects []
388 
389  SeeAlso []
390 
391 ***********************************************************************/
392 int Pr_ManMemoryReport( Pr_Man_t * p )
393 {
394  int Total;
395  char * pMem, * pNext;
396  if ( p->pChunkLast == NULL )
397  return 0;
398  Total = p->nChunkUsed;
399  for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext )
400  Total += p->nChunkSize;
401  return Total;
402 }
403 
404 /**Function*************************************************************
405 
406  Synopsis [Records the proof.]
407 
408  Description []
409 
410  SideEffects []
411 
412  SeeAlso []
413 
414 ***********************************************************************/
415 void Extra_PrintBinary_( FILE * pFile, unsigned Sign[], int nBits )
416 {
417  int Remainder, nWords;
418  int w, i;
419 
420  Remainder = (nBits%(sizeof(unsigned)*8));
421  nWords = (nBits/(sizeof(unsigned)*8)) + (Remainder>0);
422 
423  for ( w = nWords-1; w >= 0; w-- )
424  for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- )
425  fprintf( pFile, "%c", '0' + (int)((Sign[w] & (1<<i)) > 0) );
426 }
427 
428 /**Function*************************************************************
429 
430  Synopsis [Prints the interpolant for one clause.]
431 
432  Description []
433 
434  SideEffects []
435 
436  SeeAlso []
437 
438 ***********************************************************************/
439 void Pr_ManPrintInterOne( Pr_Man_t * p, Pr_Cls_t * pClause )
440 {
441  printf( "Clause %2d : ", pClause->Id );
442  Extra_PrintBinary_( stdout, &pClause->uTruth, (1 << p->nVarsAB) );
443  printf( "\n" );
444 }
445 
446 
447 
448 /**Function*************************************************************
449 
450  Synopsis [Records implication.]
451 
452  Description []
453 
454  SideEffects []
455 
456  SeeAlso []
457 
458 ***********************************************************************/
459 static inline int Pr_ManEnqueue( Pr_Man_t * p, lit Lit, Pr_Cls_t * pReason )
460 {
461  int Var = lit_var(Lit);
462  if ( p->pAssigns[Var] != LIT_UNDEF )
463  return p->pAssigns[Var] == Lit;
464  p->pAssigns[Var] = Lit;
465  p->pReasons[Var] = pReason;
466  p->pTrail[p->nTrailSize++] = Lit;
467 //printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) );
468  return 1;
469 }
470 
471 /**Function*************************************************************
472 
473  Synopsis [Records implication.]
474 
475  Description []
476 
477  SideEffects []
478 
479  SeeAlso []
480 
481 ***********************************************************************/
482 static inline void Pr_ManCancelUntil( Pr_Man_t * p, int Level )
483 {
484  lit Lit;
485  int i, Var;
486  for ( i = p->nTrailSize - 1; i >= Level; i-- )
487  {
488  Lit = p->pTrail[i];
489  Var = lit_var( Lit );
490  p->pReasons[Var] = NULL;
491  p->pAssigns[Var] = LIT_UNDEF;
492 //printf( "cancelling var %d\n", Var );
493  }
494  p->nTrailSize = Level;
495 }
496 
497 /**Function*************************************************************
498 
499  Synopsis [Propagate one assignment.]
500 
501  Description []
502 
503  SideEffects []
504 
505  SeeAlso []
506 
507 ***********************************************************************/
508 static inline Pr_Cls_t * Pr_ManPropagateOne( Pr_Man_t * p, lit Lit )
509 {
510  Pr_Cls_t ** ppPrev, * pCur, * pTemp;
511  lit LitF = lit_neg(Lit);
512  int i;
513  // iterate through the literals
514  ppPrev = p->pWatches + Lit;
515  for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev )
516  {
517  // make sure the false literal is in the second literal of the clause
518  if ( pCur->pLits[0] == LitF )
519  {
520  pCur->pLits[0] = pCur->pLits[1];
521  pCur->pLits[1] = LitF;
522  pTemp = pCur->pNext0;
523  pCur->pNext0 = pCur->pNext1;
524  pCur->pNext1 = pTemp;
525  }
526  assert( pCur->pLits[1] == LitF );
527 
528  // if the first literal is true, the clause is satisfied
529  if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] )
530  {
531  ppPrev = &pCur->pNext1;
532  continue;
533  }
534 
535  // look for a new literal to watch
536  for ( i = 2; i < (int)pCur->nLits; i++ )
537  {
538  // skip the case when the literal is false
539  if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] )
540  continue;
541  // the literal is either true or unassigned - watch it
542  pCur->pLits[1] = pCur->pLits[i];
543  pCur->pLits[i] = LitF;
544  // remove this clause from the watch list of Lit
545  *ppPrev = pCur->pNext1;
546  // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1])
547  Pr_ManWatchClause( p, pCur, pCur->pLits[1] );
548  break;
549  }
550  if ( i < (int)pCur->nLits ) // found new watch
551  continue;
552 
553  // clause is unit - enqueue new implication
554  if ( Pr_ManEnqueue(p, pCur->pLits[0], pCur) )
555  {
556  ppPrev = &pCur->pNext1;
557  continue;
558  }
559 
560  // conflict detected - return the conflict clause
561  return pCur;
562  }
563  return NULL;
564 }
565 
566 /**Function*************************************************************
567 
568  Synopsis [Propagate the current assignments.]
569 
570  Description []
571 
572  SideEffects []
573 
574  SeeAlso []
575 
576 ***********************************************************************/
577 Pr_Cls_t * Pr_ManPropagate( Pr_Man_t * p, int Start )
578 {
579  Pr_Cls_t * pClause;
580  int i;
581  abctime clk = Abc_Clock();
582  for ( i = Start; i < p->nTrailSize; i++ )
583  {
584  pClause = Pr_ManPropagateOne( p, p->pTrail[i] );
585  if ( pClause )
586  {
587 p->timeBcp += Abc_Clock() - clk;
588  return pClause;
589  }
590  }
591 p->timeBcp += Abc_Clock() - clk;
592  return NULL;
593 }
594 
595 
596 /**Function*************************************************************
597 
598  Synopsis [Prints the clause.]
599 
600  Description []
601 
602  SideEffects []
603 
604  SeeAlso []
605 
606 ***********************************************************************/
607 void Pr_ManPrintClause( Pr_Cls_t * pClause )
608 {
609  int i;
610  printf( "Clause ID = %d. Proof = %d. {", pClause->Id, (int)pClause->pProof );
611  for ( i = 0; i < (int)pClause->nLits; i++ )
612  printf( " %d", pClause->pLits[i] );
613  printf( " }\n" );
614 }
615 
616 /**Function*************************************************************
617 
618  Synopsis [Prints the resolvent.]
619 
620  Description []
621 
622  SideEffects []
623 
624  SeeAlso []
625 
626 ***********************************************************************/
627 void Pr_ManPrintResolvent( lit * pResLits, int nResLits )
628 {
629  int i;
630  printf( "Resolvent: {" );
631  for ( i = 0; i < nResLits; i++ )
632  printf( " %d", pResLits[i] );
633  printf( " }\n" );
634 }
635 
636 /**Function*************************************************************
637 
638  Synopsis [Writes one root clause into a file.]
639 
640  Description []
641 
642  SideEffects []
643 
644  SeeAlso []
645 
646 ***********************************************************************/
647 void Pr_ManProofWriteOne( Pr_Man_t * p, Pr_Cls_t * pClause )
648 {
649  pClause->pProof = (void *)++p->Counter;
650 
651  if ( p->fProofWrite )
652  {
653  int v;
654  fprintf( (FILE *)p->pManProof, "%d", (int)pClause->pProof );
655  for ( v = 0; v < (int)pClause->nLits; v++ )
656  fprintf( (FILE *)p->pManProof, " %d", lit_print(pClause->pLits[v]) );
657  fprintf( (FILE *)p->pManProof, " 0 0\n" );
658  }
659 }
660 
661 /**Function*************************************************************
662 
663  Synopsis [Traces the proof for one clause.]
664 
665  Description []
666 
667  SideEffects []
668 
669  SeeAlso []
670 
671 ***********************************************************************/
672 int Pr_ManProofTraceOne( Pr_Man_t * p, Pr_Cls_t * pConflict, Pr_Cls_t * pFinal )
673 {
674  Pr_Cls_t * pReason;
675  int i, v, Var, PrevId;
676  int fPrint = 0;
677  abctime clk = Abc_Clock();
678 
679  // collect resolvent literals
680  if ( p->fProofVerif )
681  {
682  assert( (int)pConflict->nLits <= p->nResLitsAlloc );
683  memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits );
684  p->nResLits = pConflict->nLits;
685  }
686 
687  // mark all the variables in the conflict as seen
688  for ( v = 0; v < (int)pConflict->nLits; v++ )
689  p->pSeens[lit_var(pConflict->pLits[v])] = 1;
690 
691  // start the anticedents
692 // pFinal->pAntis = Vec_PtrAlloc( 32 );
693 // Vec_PtrPush( pFinal->pAntis, pConflict );
694 
695  if ( p->nClausesA )
696  pFinal->uTruth = pConflict->uTruth;
697 
698  // follow the trail backwards
699  PrevId = (int)pConflict->pProof;
700  for ( i = p->nTrailSize - 1; i >= 0; i-- )
701  {
702  // skip literals that are not involved
703  Var = lit_var(p->pTrail[i]);
704  if ( !p->pSeens[Var] )
705  continue;
706  p->pSeens[Var] = 0;
707 
708  // skip literals of the resulting clause
709  pReason = p->pReasons[Var];
710  if ( pReason == NULL )
711  continue;
712  assert( p->pTrail[i] == pReason->pLits[0] );
713 
714  // add the variables to seen
715  for ( v = 1; v < (int)pReason->nLits; v++ )
716  p->pSeens[lit_var(pReason->pLits[v])] = 1;
717 
718 
719  // record the reason clause
720  assert( pReason->pProof > 0 );
721  p->Counter++;
722  if ( p->fProofWrite )
723  fprintf( (FILE *)p->pManProof, "%d * %d %d 0\n", p->Counter, PrevId, (int)pReason->pProof );
724  PrevId = p->Counter;
725 
726  if ( p->nClausesA )
727  {
728  if ( p->pVarTypes[Var] == 1 ) // var of A
729  pFinal->uTruth |= pReason->uTruth;
730  else
731  pFinal->uTruth &= pReason->uTruth;
732  }
733 
734  // resolve the temporary resolvent with the reason clause
735  if ( p->fProofVerif )
736  {
737  int v1, v2;
738  if ( fPrint )
739  Pr_ManPrintResolvent( p->pResLits, p->nResLits );
740  // check that the var is present in the resolvent
741  for ( v1 = 0; v1 < p->nResLits; v1++ )
742  if ( lit_var(p->pResLits[v1]) == Var )
743  break;
744  if ( v1 == p->nResLits )
745  printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var );
746  if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) )
747  printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var );
748  // remove this variable from the resolvent
749  assert( lit_var(p->pResLits[v1]) == Var );
750  p->nResLits--;
751  for ( ; v1 < p->nResLits; v1++ )
752  p->pResLits[v1] = p->pResLits[v1+1];
753  // add variables of the reason clause
754  for ( v2 = 1; v2 < (int)pReason->nLits; v2++ )
755  {
756  for ( v1 = 0; v1 < p->nResLits; v1++ )
757  if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) )
758  break;
759  // if it is a new variable, add it to the resolvent
760  if ( v1 == p->nResLits )
761  {
762  if ( p->nResLits == p->nResLitsAlloc )
763  printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n, pFinal->Id" );
764  p->pResLits[ p->nResLits++ ] = pReason->pLits[v2];
765  continue;
766  }
767  // if the variable is the same, the literal should be the same too
768  if ( p->pResLits[v1] == pReason->pLits[v2] )
769  continue;
770  // the literal is different
771  printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id );
772  }
773  }
774 
775 // Vec_PtrPush( pFinal->pAntis, pReason );
776  }
777 
778  // unmark all seen variables
779 // for ( i = p->nTrailSize - 1; i >= 0; i-- )
780 // p->pSeens[lit_var(p->pTrail[i])] = 0;
781  // check that the literals are unmarked
782 // for ( i = p->nTrailSize - 1; i >= 0; i-- )
783 // assert( p->pSeens[lit_var(p->pTrail[i])] == 0 );
784 
785  // use the resulting clause to check the correctness of resolution
786  if ( p->fProofVerif )
787  {
788  int v1, v2;
789  if ( fPrint )
790  Pr_ManPrintResolvent( p->pResLits, p->nResLits );
791  for ( v1 = 0; v1 < p->nResLits; v1++ )
792  {
793  for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ )
794  if ( pFinal->pLits[v2] == p->pResLits[v1] )
795  break;
796  if ( v2 < (int)pFinal->nLits )
797  continue;
798  break;
799  }
800  if ( v1 < p->nResLits )
801  {
802  printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id );
803  Pr_ManPrintClause( pConflict );
804  Pr_ManPrintResolvent( p->pResLits, p->nResLits );
805  Pr_ManPrintClause( pFinal );
806  }
807  }
808 p->timeTrace += Abc_Clock() - clk;
809 
810  // return the proof pointer
811  if ( p->nClausesA )
812  {
813  Pr_ManPrintInterOne( p, pFinal );
814  }
815  return p->Counter;
816 }
817 
818 /**Function*************************************************************
819 
820  Synopsis [Records the proof for one clause.]
821 
822  Description []
823 
824  SideEffects []
825 
826  SeeAlso []
827 
828 ***********************************************************************/
829 int Pr_ManProofRecordOne( Pr_Man_t * p, Pr_Cls_t * pClause )
830 {
831  Pr_Cls_t * pConflict;
832  int i;
833 
834  // empty clause never ends up there
835  assert( pClause->nLits > 0 );
836  if ( pClause->nLits == 0 )
837  printf( "Error: Empty clause is attempted.\n" );
838 
839  // add assumptions to the trail
840  assert( !pClause->fRoot );
841  assert( p->nTrailSize == p->nRootSize );
842  for ( i = 0; i < (int)pClause->nLits; i++ )
843  if ( !Pr_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
844  {
845  assert( 0 ); // impossible
846  return 0;
847  }
848 
849  // propagate the assumptions
850  pConflict = Pr_ManPropagate( p, p->nRootSize );
851  if ( pConflict == NULL )
852  {
853  assert( 0 ); // cannot prove
854  return 0;
855  }
856 
857  // construct the proof
858  pClause->pProof = (void *)Pr_ManProofTraceOne( p, pConflict, pClause );
859 
860  // undo to the root level
861  Pr_ManCancelUntil( p, p->nRootSize );
862 
863  // add large clauses to the watched lists
864  if ( pClause->nLits > 1 )
865  {
866  Pr_ManWatchClause( p, pClause, pClause->pLits[0] );
867  Pr_ManWatchClause( p, pClause, pClause->pLits[1] );
868  return 1;
869  }
870  assert( pClause->nLits == 1 );
871 
872  // if the clause proved is unit, add it and propagate
873  if ( !Pr_ManEnqueue( p, pClause->pLits[0], pClause ) )
874  {
875  assert( 0 ); // impossible
876  return 0;
877  }
878 
879  // propagate the assumption
880  pConflict = Pr_ManPropagate( p, p->nRootSize );
881  if ( pConflict )
882  {
883  // construct the proof
884  p->pEmpty->pProof = (void *)Pr_ManProofTraceOne( p, pConflict, p->pEmpty );
885  printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id );
886  return 0;
887  }
888 
889  // update the root level
890  p->nRootSize = p->nTrailSize;
891  return 1;
892 }
893 
894 /**Function*************************************************************
895 
896  Synopsis [Propagate the root clauses.]
897 
898  Description []
899 
900  SideEffects []
901 
902  SeeAlso []
903 
904 ***********************************************************************/
905 int Pr_ManProcessRoots( Pr_Man_t * p )
906 {
907  Pr_Cls_t * pClause;
908  int Counter;
909 
910  // make sure the root clauses are preceeding the learnt clauses
911  Counter = 0;
912  Pr_ManForEachClause( p, pClause )
913  {
914  assert( (int)pClause->fA == (Counter < (int)p->nClausesA) );
915  assert( (int)pClause->fRoot == (Counter < (int)p->nRoots) );
916  Counter++;
917  }
918  assert( p->nClauses == Counter );
919 
920  // make sure the last clause if empty
921  assert( p->pTail->nLits == 0 );
922 
923  // go through the root unit clauses
924  p->nTrailSize = 0;
925  Pr_ManForEachClauseRoot( p, pClause )
926  {
927  // create watcher lists for the root clauses
928  if ( pClause->nLits > 1 )
929  {
930  Pr_ManWatchClause( p, pClause, pClause->pLits[0] );
931  Pr_ManWatchClause( p, pClause, pClause->pLits[1] );
932  }
933  // empty clause and large clauses
934  if ( pClause->nLits != 1 )
935  continue;
936  // unit clause
937  assert( lit_check(pClause->pLits[0], p->nVars) );
938  if ( !Pr_ManEnqueue( p, pClause->pLits[0], pClause ) )
939  {
940  // detected root level conflict
941  printf( "Pr_ManProcessRoots(): Detected a root-level conflict\n" );
942  assert( 0 );
943  return 0;
944  }
945  }
946 
947  // propagate the root unit clauses
948  pClause = Pr_ManPropagate( p, 0 );
949  if ( pClause )
950  {
951  // detected root level conflict
952  printf( "Pr_ManProcessRoots(): Detected a root-level conflict\n" );
953  assert( 0 );
954  return 0;
955  }
956 
957  // set the root level
958  p->nRootSize = p->nTrailSize;
959  return 1;
960 }
961 
962 /**Function*************************************************************
963 
964  Synopsis [Records the proof.]
965 
966  Description []
967 
968  SideEffects []
969 
970  SeeAlso []
971 
972 ***********************************************************************/
973 void Pr_ManPrepareInter( Pr_Man_t * p )
974 {
975  unsigned uTruths[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
976  Pr_Cls_t * pClause;
977  int Var, v;
978 
979  // mark the variable encountered in the clauses of A
980  Pr_ManForEachClauseRoot( p, pClause )
981  {
982  if ( !pClause->fA )
983  break;
984  for ( v = 0; v < (int)pClause->nLits; v++ )
985  p->pVarTypes[lit_var(pClause->pLits[v])] = 1;
986  }
987 
988  // check variables that appear in clauses of B
989  p->nVarsAB = 0;
990  Pr_ManForEachClauseRoot( p, pClause )
991  {
992  if ( pClause->fA )
993  continue;
994  for ( v = 0; v < (int)pClause->nLits; v++ )
995  {
996  Var = lit_var(pClause->pLits[v]);
997  if ( p->pVarTypes[Var] == 1 ) // var of A
998  {
999  // change it into a global variable
1000  p->nVarsAB++;
1001  p->pVarTypes[Var] = -1;
1002  }
1003  }
1004  }
1005 
1006  // order global variables
1007  p->nVarsAB = 0;
1008  for ( v = 0; v < p->nVars; v++ )
1009  if ( p->pVarTypes[v] == -1 )
1010  p->pVarTypes[v] -= p->nVarsAB++;
1011 printf( "There are %d global variables.\n", p->nVarsAB );
1012 
1013  // set interpolants for root clauses
1014  Pr_ManForEachClauseRoot( p, pClause )
1015  {
1016  if ( !pClause->fA ) // clause of B
1017  {
1018  pClause->uTruth = ~0;
1019  Pr_ManPrintInterOne( p, pClause );
1020  continue;
1021  }
1022  // clause of A
1023  pClause->uTruth = 0;
1024  for ( v = 0; v < (int)pClause->nLits; v++ )
1025  {
1026  Var = lit_var(pClause->pLits[v]);
1027  if ( p->pVarTypes[Var] < 0 ) // global var
1028  {
1029  if ( lit_sign(pClause->pLits[v]) ) // negative var
1030  pClause->uTruth |= ~uTruths[ -p->pVarTypes[Var]-1 ];
1031  else
1032  pClause->uTruth |= uTruths[ -p->pVarTypes[Var]-1 ];
1033  }
1034  }
1035  Pr_ManPrintInterOne( p, pClause );
1036  }
1037 }
1038 
1039 /**Function*************************************************************
1040 
1041  Synopsis [Records the proof.]
1042 
1043  Description []
1044 
1045  SideEffects []
1046 
1047  SeeAlso []
1048 
1049 ***********************************************************************/
1050 int Pr_ManProofWrite( Pr_Man_t * p )
1051 {
1052  Pr_Cls_t * pClause;
1053  int RetValue = 1;
1054 
1055  // propagate root level assignments
1056  Pr_ManProcessRoots( p );
1057 
1058  // prepare the interpolant computation
1059  if ( p->nClausesA )
1060  Pr_ManPrepareInter( p );
1061 
1062  // construct proof for each clause
1063  // start the proof
1064  if ( p->fProofWrite )
1065  p->pManProof = fopen( "proof.cnf_", "w" );
1066  p->Counter = 0;
1067 
1068  // write the root clauses
1069  Pr_ManForEachClauseRoot( p, pClause )
1070  Pr_ManProofWriteOne( p, pClause );
1071 
1072  // consider each learned clause
1073  Pr_ManForEachClauseLearnt( p, pClause )
1074  {
1075  if ( !Pr_ManProofRecordOne( p, pClause ) )
1076  {
1077  RetValue = 0;
1078  break;
1079  }
1080  }
1081 
1082  if ( p->nClausesA )
1083  {
1084  printf( "Interpolant: " );
1085  }
1086 
1087 
1088  // stop the proof
1089  if ( p->fProofWrite )
1090  {
1091  fclose( (FILE *)p->pManProof );
1092  p->pManProof = NULL;
1093  }
1094  return RetValue;
1095 }
1096 
1097 /**Function*************************************************************
1098 
1099  Synopsis [Reads clauses from file.]
1100 
1101  Description []
1102 
1103  SideEffects []
1104 
1105  SeeAlso []
1106 
1107 ***********************************************************************/
1108 Pr_Man_t * Pr_ManProofRead( char * pFileName )
1109 {
1110  Pr_Man_t * p = NULL;
1111  char * pCur, * pBuffer = NULL;
1112  int * pArray = NULL;
1113  FILE * pFile;
1114  int RetValue, Counter, nNumbers, Temp;
1115  int nClauses, nClausesA, nRoots, nVars;
1116 
1117  // open the file
1118  pFile = fopen( pFileName, "r" );
1119  if ( pFile == NULL )
1120  {
1121  printf( "Count not open input file \"%s\".\n", pFileName );
1122  return NULL;
1123  }
1124 
1125  // read the file
1126  pBuffer = (char *)ABC_ALLOC( char, (1<<16) );
1127  for ( Counter = 0; fgets( pBuffer, (1<<16), pFile ); )
1128  {
1129  if ( pBuffer[0] == 'c' )
1130  continue;
1131  if ( pBuffer[0] == 'p' )
1132  {
1133  assert( p == NULL );
1134  nClausesA = 0;
1135  RetValue = sscanf( pBuffer + 1, "%d %d %d %d", &nVars, &nClauses, &nRoots, &nClausesA );
1136  if ( RetValue != 3 && RetValue != 4 )
1137  {
1138  printf( "Wrong input file format.\n" );
1139  }
1140  p = Pr_ManAlloc( nVars );
1141  pArray = (int *)ABC_ALLOC( char, sizeof(int) * (nVars + 10) );
1142  continue;
1143  }
1144  // skip empty lines
1145  for ( pCur = pBuffer; *pCur; pCur++ )
1146  if ( !(*pCur == ' ' || *pCur == '\t' || *pCur == '\r' || *pCur == '\n') )
1147  break;
1148  if ( *pCur == 0 )
1149  continue;
1150  // scan the numbers from file
1151  nNumbers = 0;
1152  pCur = pBuffer;
1153  while ( *pCur )
1154  {
1155  // skip spaces
1156  for ( ; *pCur && *pCur == ' '; pCur++ );
1157  // read next number
1158  Temp = 0;
1159  sscanf( pCur, "%d", &Temp );
1160  if ( Temp == 0 )
1161  break;
1162  pArray[ nNumbers++ ] = lit_read( Temp );
1163  // skip non-spaces
1164  for ( ; *pCur && *pCur != ' '; pCur++ );
1165  }
1166  // add the clause
1167  if ( !Pr_ManAddClause( p, (unsigned *)pArray, (unsigned *)pArray + nNumbers, Counter < nRoots, Counter < nClausesA ) )
1168  {
1169  printf( "Bad clause number %d.\n", Counter );
1170  return NULL;
1171  }
1172  // count the clauses
1173  Counter++;
1174  }
1175  // check the number of clauses
1176  if ( Counter != nClauses )
1177  printf( "Expected %d clauses but read %d.\n", nClauses, Counter );
1178 
1179  // finish
1180  if ( pArray ) ABC_FREE( pArray );
1181  if ( pBuffer ) ABC_FREE( pBuffer );
1182  fclose( pFile );
1183  return p;
1184 }
1185 
1186 /**Function*************************************************************
1187 
1188  Synopsis [Records the proof.]
1189 
1190  Description []
1191 
1192  SideEffects []
1193 
1194  SeeAlso []
1195 
1196 ***********************************************************************/
1197 /*
1198 int Pr_ManProofCount_rec( Pr_Cls_t * pClause )
1199 {
1200  Pr_Cls_t * pNext;
1201  int i, Counter;
1202  if ( pClause->fRoot )
1203  return 0;
1204  if ( pClause->fVisit )
1205  return 0;
1206  pClause->fVisit = 1;
1207  // count the number of visited clauses
1208  Counter = 1;
1209  Vec_PtrForEachEntry( Pr_Cls_t *, pClause->pAntis, pNext, i )
1210  Counter += Pr_ManProofCount_rec( pNext );
1211  return Counter;
1212 }
1213 */
1214 
1215 /**Function*************************************************************
1216 
1217  Synopsis [Records the proof.]
1218 
1219  Description []
1220 
1221  SideEffects []
1222 
1223  SeeAlso []
1224 
1225 ***********************************************************************/
1226 int Pr_ManProofTest( char * pFileName )
1227 {
1228  Pr_Man_t * p;
1229  abctime clk, clkTotal = Abc_Clock();
1230 
1231 clk = Abc_Clock();
1232  p = Pr_ManProofRead( pFileName );
1233 p->timeRead = Abc_Clock() - clk;
1234  if ( p == NULL )
1235  return 0;
1236 
1237  Pr_ManProofWrite( p );
1238 
1239  // print stats
1240 /*
1241  nUsed = Pr_ManProofCount_rec( p->pEmpty );
1242  printf( "Roots = %d. Learned = %d. Total = %d. Steps = %d. Ave = %.2f. Used = %d. Ratio = %.2f. \n",
1243  p->nRoots, p->nClauses-p->nRoots, p->nClauses, p->Counter,
1244  1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots),
1245  nUsed, 1.0*nUsed/(p->nClauses-p->nRoots) );
1246 */
1247  printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f MB\n",
1248  p->nVars, p->nRoots, p->nClauses-p->nRoots, p->Counter,
1249  1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots),
1250  1.0*Pr_ManMemoryReport(p)/(1<<20) );
1251 
1252 p->timeTotal = Abc_Clock() - clkTotal;
1253  Pr_ManFree( p );
1254  return 1;
1255 }
1256 
1257 
1258 ////////////////////////////////////////////////////////////////////////
1259 /// END OF FILE ///
1260 ////////////////////////////////////////////////////////////////////////
1261 
1262 
1263 ABC_NAMESPACE_IMPL_END
1264 
memset
char * memset()
Pr_Man_t_::fProofWrite
int fProofWrite
Definition: pr.c:58
Pr_Man_t_::nClauses
int nClauses
Definition: pr.c:63
Pr_Man_t_::nChunkSize
int nChunkSize
Definition: pr.c:83
Pr_Man_t_
Definition: pr.c:55
Pr_Man_t_::nResLitsAlloc
int nResLitsAlloc
Definition: pr.c:89
Pr_Man_t_::pAssigns
lit * pAssigns
Definition: pr.c:73
Pr_Cls_t_::pNext
Pr_Cls_t * pNext
Definition: pr.c:44
Pr_ManPrintResolvent
void Pr_ManPrintResolvent(lit *pResLits, int nResLits)
Definition: pr.c:627
Pr_ManProcessRoots
int Pr_ManProcessRoots(Pr_Man_t *p)
Definition: pr.c:905
Pr_ManForEachClauseLearnt
#define Pr_ManForEachClauseLearnt(p, pCls)
Definition: pr.c:113
Pr_ManPropagateOne
static Pr_Cls_t * Pr_ManPropagateOne(Pr_Man_t *p, lit Lit)
Definition: pr.c:508
Pr_Man_t_::timeTotal
abctime timeTotal
Definition: pr.c:94
Pr_ManFree
void Pr_ManFree(Pr_Man_t *p)
Definition: pr.c:214
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
lit_check
static int lit_check(lit l, int n)
Definition: pr.c:108
lit_var
static int lit_var(lit l)
Definition: pr.c:104
Pr_Cls_t_::fVisit
unsigned fVisit
Definition: pr.c:50
Pr_Man_t_::nRoots
int nRoots
Definition: pr.c:62
Pr_Cls_t_::Id
int Id
Definition: pr.c:47
Pr_Cls_t_
Definition: pr.c:39
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition: abc_global.h:233
Pr_ManForEachClauseRoot
#define Pr_ManForEachClauseRoot(p, pCls)
Definition: pr.c:112
Pr_ManProofTraceOne
int Pr_ManProofTraceOne(Pr_Man_t *p, Pr_Cls_t *pConflict, Pr_Cls_t *pFinal)
Definition: pr.c:672
Pr_Man_t_::timeTrace
abctime timeTrace
Definition: pr.c:92
Pr_ManResize
static void Pr_ManResize(Pr_Man_t *p, int nVarsNew)
Definition: pr.c:173
Pr_Man_t_::nResLits
int nResLits
Definition: pr.c:88
Pr_Man_t_::nVarsAB
int nVarsAB
Definition: pr.c:61
Pr_ManEnqueue
static int Pr_ManEnqueue(Pr_Man_t *p, lit Lit, Pr_Cls_t *pReason)
Definition: pr.c:459
lit_neg
static lit lit_neg(lit l)
Definition: pr.c:103
Pr_ManWatchClause
static void Pr_ManWatchClause(Pr_Man_t *p, Pr_Cls_t *pClause, lit Lit)
Definition: pr.c:244
Pr_Cls_t_::uTruth
unsigned uTruth
Definition: pr.c:41
Pr_Man_t_::nRootSize
int nRootSize
Definition: pr.c:70
memcpy
char * memcpy()
Pr_ManProofWrite
int Pr_ManProofWrite(Pr_Man_t *p)
Definition: pr.c:1050
Pr_Man_t_::pLearnt
Pr_Cls_t * pLearnt
Definition: pr.c:67
Pr_Man_t_::nVarsAlloc
int nVarsAlloc
Definition: pr.c:78
Pr_Man_t_::pManProof
void * pManProof
Definition: pr.c:80
Pr_ManPropagate
Pr_Cls_t * Pr_ManPropagate(Pr_Man_t *p, int Start)
Definition: pr.c:577
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Pr_Man_t_::pEmpty
Pr_Cls_t * pEmpty
Definition: pr.c:68
Pr_ManPrintClause
void Pr_ManPrintClause(Pr_Cls_t *pClause)
Definition: pr.c:607
Pr_ManMemoryReport
int Pr_ManMemoryReport(Pr_Man_t *p)
Definition: pr.c:392
Pr_Man_t_::fProofVerif
int fProofVerif
Definition: pr.c:59
Pr_Man_t_::pSeens
char * pSeens
Definition: pr.c:74
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Extra_PrintBinary_
void Extra_PrintBinary_(FILE *pFile, unsigned Sign[], int nBits)
Definition: pr.c:415
nWords
int nWords
Definition: abcNpn.c:127
for
for(p=first;p->value< newval;p=p->next)
toLit
static lit toLit(int v)
Definition: pr.c:101
lit
int lit
Definition: satVec.h:130
Pr_ManProofRecordOne
int Pr_ManProofRecordOne(Pr_Man_t *p, Pr_Cls_t *pClause)
Definition: pr.c:829
Pr_ManProofTest
int Pr_ManProofTest(char *pFileName)
Definition: pr.c:1226
Pr_Man_t_::nTrailSize
int nTrailSize
Definition: pr.c:71
Pr_Cls_t_::pLits
lit pLits[0]
Definition: pr.c:52
Pr_ManForEachClause
#define Pr_ManForEachClause(p, pCls)
Definition: pr.c:111
Pr_Cls_t_::fA
unsigned fA
Definition: pr.c:48
Pr_ManCancelUntil
static void Pr_ManCancelUntil(Pr_Man_t *p, int Level)
Definition: pr.c:482
Pr_ManProofWriteOne
void Pr_ManProofWriteOne(Pr_Man_t *p, Pr_Cls_t *pClause)
Definition: pr.c:647
Pr_Man_t_::nClausesA
int nClausesA
Definition: pr.c:64
Pr_ManPrintInterOne
void Pr_ManPrintInterOne(Pr_Man_t *p, Pr_Cls_t *pClause)
Definition: pr.c:439
Pr_ManPrepareInter
void Pr_ManPrepareInter(Pr_Man_t *p)
Definition: pr.c:973
Pr_Man_t_::timeRead
abctime timeRead
Definition: pr.c:93
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
if
if(last==0)
Definition: sparse_int.h:34
Pr_Cls_t_::nLits
unsigned nLits
Definition: pr.c:51
Pr_Man_t
typedefABC_NAMESPACE_HEADER_START struct Pr_Man_t_ Pr_Man_t
INCLUDES ///.
Definition: pr.h:46
Pr_Man_t_::pHead
Pr_Cls_t * pHead
Definition: pr.c:65
Pr_Man_t_::timeBcp
abctime timeBcp
Definition: pr.c:91
Counter
static int Counter
Definition: extraBddMisc.c:1877
Pr_Man_t_::nChunkUsed
int nChunkUsed
Definition: pr.c:84
Pr_ManAlloc
Pr_Man_t * Pr_ManAlloc(int nVarsAlloc)
FUNCTION DEFINITIONS ///.
Definition: pr.c:141
Pr_ManMemoryStop
static void Pr_ManMemoryStop(Pr_Man_t *p)
Definition: pr.c:371
Pr_Cls_t_::pNext0
Pr_Cls_t * pNext0
Definition: pr.c:45
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Pr_ManAddClause
int Pr_ManAddClause(Pr_Man_t *p, lit *pBeg, lit *pEnd, int fRoot, int fClauseA)
Definition: pr.c:268
Pr_Cls_t_::fRoot
unsigned fRoot
Definition: pr.c:49
lit_read
static lit lit_read(int s)
Definition: pr.c:107
Pr_Man_t_::pChunkLast
char * pChunkLast
Definition: pr.c:85
lit_sign
static int lit_sign(lit l)
Definition: pr.c:105
abc_global.h
lit_print
static int lit_print(lit l)
Definition: pr.c:106
Pr_Cls_t_::pNext1
Pr_Cls_t * pNext1
Definition: pr.c:46
Pr_Man_t_::pVarTypes
char * pVarTypes
Definition: pr.c:75
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Pr_Man_t_::pWatches
Pr_Cls_t ** pWatches
Definition: pr.c:77
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Pr_ManProofRead
Pr_Man_t * Pr_ManProofRead(char *pFileName)
Definition: pr.c:1108
LIT_UNDEF
static const lit LIT_UNDEF
Definition: pr.c:98
Minisat::Var
int Var
Definition: SolverTypes.h:42
Pr_Cls_t
struct Pr_Cls_t_ Pr_Cls_t
Definition: pr.c:38
Pr_Man_t_::pTail
Pr_Cls_t * pTail
Definition: pr.c:66
assert
#define assert(ex)
Definition: util_old.h:213
Pr_Man_t_::pResLits
lit * pResLits
Definition: pr.c:87
Pr_Man_t_::nVars
int nVars
Definition: pr.c:60
Pr_ManMemoryFetch
static char * Pr_ManMemoryFetch(Pr_Man_t *p, int nBytes)
Definition: pr.c:345
toLitCond
static lit toLitCond(int v, int c)
Definition: pr.c:102
Pr_Man_t_::pTrail
lit * pTrail
Definition: pr.c:72
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Pr_Man_t_::pReasons
Pr_Cls_t ** pReasons
Definition: pr.c:76
Pr_Man_t_::Counter
int Counter
Definition: pr.c:81
Pr_Cls_t_::pProof
void * pProof
Definition: pr.c:42
lit
ABC_NAMESPACE_IMPL_START typedef unsigned lit
DECLARATIONS ///.
Definition: pr.c:36