abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
satProof.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [satProof.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [SAT solver.]
8 
9  Synopsis [Proof manipulation procedures.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: satProof.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 "misc/vec/vec.h"
27 #include "misc/vec/vecSet.h"
28 #include "aig/aig/aig.h"
29 #include "satTruth.h"
30 
31 ABC_NAMESPACE_IMPL_START
32 
33 /*
34  Proof is represented as a vector of records.
35  A resolution record is represented by a handle (an offset in this vector).
36  A resolution record entry is <size><label><ant1><ant2>...<antN>
37  Label is initialized to 0. Root clauses are given by their handles.
38  They are marked by bitshifting by 2 bits up and setting the LSB to 1
39 */
40 
41 typedef struct satset_t satset;
42 struct satset_t
43 {
44  unsigned learnt : 1;
45  unsigned mark : 1;
46  unsigned partA : 1;
47  unsigned nEnts : 29;
48  int Id;
49  int pEnts[0];
50 };
51 
52 ////////////////////////////////////////////////////////////////////////
53 /// DECLARATIONS ///
54 ////////////////////////////////////////////////////////////////////////
55 
56 //static inline satset* Proof_ClauseRead ( Vec_Int_t* p, int h ) { assert( h > 0 ); return satset_read( (veci *)p, h ); }
57 //static inline satset* Proof_ClauseRead ( Vec_Int_t* p, int h ) { assert( h > 0 ); return (satset *)Vec_IntEntryP( p, h );}
58 static inline satset* Proof_NodeRead ( Vec_Set_t* p, int h ) { assert( h > 0 ); return (satset*)Vec_SetEntry( p, h ); }
59 static inline int Proof_NodeWordNum ( int nEnts ) { assert( nEnts > 0 ); return 1 + ((nEnts + 1) >> 1); }
60 
61 void Proof_ClauseSetEnts( Vec_Set_t* p, int h, int nEnts ) { Proof_NodeRead(p, h)->nEnts = nEnts; }
62 
63 // iterating through nodes in the proof
64 #define Proof_ForeachClauseVec( pVec, p, pNode, i ) \
65  for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_ClauseRead(p, Vec_IntEntry(pVec,i))); i++ )
66 #define Proof_ForeachNodeVec( pVec, p, pNode, i ) \
67  for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ )
68 #define Proof_ForeachNodeVec1( pVec, p, pNode, i ) \
69  for ( i = 1; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ )
70 
71 // iterating through fanins of a proof node
72 #define Proof_NodeForeachFanin( pProof, pNode, pFanin, i ) \
73  for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)), 1); i++ )
74 /*
75 #define Proof_NodeForeachLeaf( pClauses, pNode, pLeaf, i ) \
76  for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ )
77 #define Proof_NodeForeachFaninLeaf( pProof, pClauses, pNode, pFanin, i ) \
78  for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_ClauseRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(pProof, pNode->pEnts[i] >> 2)); i++ )
79 */
80 
81 ////////////////////////////////////////////////////////////////////////
82 /// FUNCTION DEFINITIONS ///
83 ////////////////////////////////////////////////////////////////////////
84 
85 /**Function*************************************************************
86 
87  Synopsis [Cleans collected resultion nodes belonging to the proof.]
88 
89  Description []
90 
91  SideEffects []
92 
93  SeeAlso []
94 
95 ***********************************************************************/
96 void Proof_CleanCollected( Vec_Set_t * vProof, Vec_Int_t * vUsed )
97 {
98  satset * pNode;
99  int hNode;
100  Proof_ForeachNodeVec( vUsed, vProof, pNode, hNode )
101  pNode->Id = 0;
102 }
103 
104 /**Function*************************************************************
105 
106  Synopsis []
107 
108  Description []
109 
110  SideEffects []
111 
112  SeeAlso []
113 
114 ***********************************************************************/
115 void Proof_CollectUsed_iter( Vec_Set_t * vProof, int hNode, Vec_Int_t * vUsed, Vec_Int_t * vStack )
116 {
117  satset * pNext, * pNode = Proof_NodeRead( vProof, hNode );
118  int i;
119  if ( pNode->Id )
120  return;
121  // start with node
122  pNode->Id = 1;
123  Vec_IntPush( vStack, hNode << 1 );
124  // perform DFS search
125  while ( Vec_IntSize(vStack) )
126  {
127  hNode = Vec_IntPop( vStack );
128  if ( hNode & 1 ) // extracted second time
129  {
130  Vec_IntPush( vUsed, hNode >> 1 );
131  continue;
132  }
133  // extracted first time
134  Vec_IntPush( vStack, hNode ^ 1 ); // add second time
135  // add its anticedents ;
136  pNode = Proof_NodeRead( vProof, hNode >> 1 );
137  Proof_NodeForeachFanin( vProof, pNode, pNext, i )
138  if ( pNext && !pNext->Id )
139  {
140  pNext->Id = 1;
141  Vec_IntPush( vStack, (pNode->pEnts[i] >> 2) << 1 ); // add first time
142  }
143  }
144 }
145 Vec_Int_t * Proof_CollectUsedIter( Vec_Set_t * vProof, Vec_Int_t * vRoots, int fSort )
146 {
147  int fVerify = 0;
148  Vec_Int_t * vUsed, * vStack;
149  abctime clk = Abc_Clock();
150  int i, Entry, iPrev = 0;
151  vUsed = Vec_IntAlloc( 1000 );
152  vStack = Vec_IntAlloc( 1000 );
153  Vec_IntForEachEntry( vRoots, Entry, i )
154  if ( Entry >= 0 )
155  Proof_CollectUsed_iter( vProof, Entry, vUsed, vStack );
156  Vec_IntFree( vStack );
157 // Abc_PrintTime( 1, "Iterative clause collection time", Abc_Clock() - clk );
158  clk = Abc_Clock();
159  Abc_MergeSort( Vec_IntArray(vUsed), Vec_IntSize(vUsed) );
160 // Abc_PrintTime( 1, "Postprocessing with sorting time", Abc_Clock() - clk );
161  // verify topological order
162  if ( fVerify )
163  {
164  iPrev = 0;
165  Vec_IntForEachEntry( vUsed, Entry, i )
166  {
167  if ( iPrev >= Entry )
168  printf( "Out of topological order!!!\n" );
169  assert( iPrev < Entry );
170  iPrev = Entry;
171  }
172  }
173  return vUsed;
174 }
175 
176 /**Function*************************************************************
177 
178  Synopsis [Recursively collects useful proof nodes.]
179 
180  Description []
181 
182  SideEffects []
183 
184  SeeAlso []
185 
186 ***********************************************************************/
187 void Proof_CollectUsed_rec( Vec_Set_t * vProof, int hNode, Vec_Int_t * vUsed )
188 {
189  satset * pNext, * pNode = Proof_NodeRead( vProof, hNode );
190  int i;
191  if ( pNode->Id )
192  return;
193  pNode->Id = 1;
194  Proof_NodeForeachFanin( vProof, pNode, pNext, i )
195  if ( pNext && !pNext->Id )
196  Proof_CollectUsed_rec( vProof, pNode->pEnts[i] >> 2, vUsed );
197  Vec_IntPush( vUsed, hNode );
198 }
199 Vec_Int_t * Proof_CollectUsedRec( Vec_Set_t * vProof, Vec_Int_t * vRoots )
200 {
201  Vec_Int_t * vUsed;
202  int i, Entry;
203  vUsed = Vec_IntAlloc( 1000 );
204  Vec_IntForEachEntry( vRoots, Entry, i )
205  if ( Entry >= 0 )
206  Proof_CollectUsed_rec( vProof, Entry, vUsed );
207  return vUsed;
208 }
209 
210 /**Function*************************************************************
211 
212  Synopsis [Recursively visits useful proof nodes.]
213 
214  Description []
215 
216  SideEffects []
217 
218  SeeAlso []
219 
220 ***********************************************************************/
221 int Proof_MarkUsed_rec( Vec_Set_t * vProof, int hNode )
222 {
223  satset * pNext, * pNode = Proof_NodeRead( vProof, hNode );
224  int i, Counter = 1;
225  if ( pNode->Id )
226  return 0;
227  pNode->Id = 1;
228  Proof_NodeForeachFanin( vProof, pNode, pNext, i )
229  if ( pNext && !pNext->Id )
230  Counter += Proof_MarkUsed_rec( vProof, pNode->pEnts[i] >> 2 );
231  return Counter;
232 }
233 int Proof_MarkUsedRec( Vec_Set_t * vProof, Vec_Int_t * vRoots )
234 {
235  int i, Entry, Counter = 0;
236  Vec_IntForEachEntry( vRoots, Entry, i )
237  if ( Entry >= 0 )
238  Counter += Proof_MarkUsed_rec( vProof, Entry );
239  return Counter;
240 }
241 
242 
243 
244 
245 /**Function*************************************************************
246 
247  Synopsis [Checks the validity of the check point.]
248 
249  Description []
250 
251  SideEffects []
252 
253  SeeAlso []
254 
255 ***********************************************************************/
256 /*
257 void Sat_ProofReduceCheck_rec( Vec_Set_t * vProof, Vec_Int_t * vClauses, satset * pNode, int hClausePivot, Vec_Ptr_t * vVisited )
258 {
259  satset * pFanin;
260  int k;
261  if ( pNode->Id )
262  return;
263  pNode->Id = -1;
264  Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
265  if ( (pNode->pEnts[k] & 1) == 0 ) // proof node
266  Sat_ProofReduceCheck_rec( vProof, vClauses, pFanin, hClausePivot, vVisited );
267  else // problem clause
268  assert( (pNode->pEnts[k] >> 2) < hClausePivot );
269  Vec_PtrPush( vVisited, pNode );
270 }
271 void Sat_ProofReduceCheckOne( sat_solver2 * s, int iLearnt, Vec_Ptr_t * vVisited )
272 {
273  Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
274  Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
275  Vec_Int_t * vRoots = (Vec_Int_t *)&s->claProofs;
276  int hProofNode = Vec_IntEntry( vRoots, iLearnt );
277  satset * pNode = Proof_NodeRead( vProof, hProofNode );
278  Sat_ProofReduceCheck_rec( vProof, vClauses, pNode, s->hClausePivot, vVisited );
279 }
280 void Sat_ProofReduceCheck( sat_solver2 * s )
281 {
282  Vec_Ptr_t * vVisited;
283  satset * c;
284  int h, i = 1;
285  vVisited = Vec_PtrAlloc( 1000 );
286  sat_solver_foreach_learnt( s, c, h )
287  if ( h < s->hLearntPivot )
288  Sat_ProofReduceCheckOne( s, i++, vVisited );
289  Vec_PtrForEachEntry( satset *, vVisited, c, i )
290  c->Id = 0;
291  Vec_PtrFree( vVisited );
292 }
293 */
294 
295 /**Function*************************************************************
296 
297  Synopsis [Reduces the proof to contain only roots and their children.]
298 
299  Description [The result is updated proof and updated roots.]
300 
301  SideEffects []
302 
303  SeeAlso []
304 
305 ***********************************************************************/
306 /*
307 void Sat_ProofReduce2( sat_solver2 * s )
308 {
309  Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
310  Vec_Int_t * vRoots = (Vec_Int_t *)&s->claProofs;
311  Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
312 
313  int fVerbose = 0;
314  Vec_Int_t * vUsed;
315  satset * pNode, * pFanin, * pPivot;
316  int i, k, hTemp;
317  abctime clk = Abc_Clock();
318  static abctime TimeTotal = 0;
319 
320  // collect visited nodes
321  vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
322 
323  // relabel nodes to use smaller space
324  Vec_SetShrinkS( vProof, 2 );
325  Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
326  {
327  pNode->Id = Vec_SetAppendS( vProof, 2+pNode->nEnts );
328  Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
329  if ( (pNode->pEnts[k] & 1) == 0 ) // proof node
330  pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2);
331  else // problem clause
332  assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) );
333  }
334  // update roots
335  Proof_ForeachNodeVec1( vRoots, vProof, pNode, i )
336  Vec_IntWriteEntry( vRoots, i, pNode->Id );
337  // determine new pivot
338  assert( s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(vProof) );
339  pPivot = Proof_NodeRead( vProof, s->hProofPivot );
340  s->hProofPivot = Vec_SetHandCurrentS(vProof);
341  // compact the nodes
342  Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
343  {
344  hTemp = pNode->Id; pNode->Id = 0;
345  memmove( Vec_SetEntry(vProof, hTemp), pNode, sizeof(word)*Proof_NodeWordNum(pNode->nEnts) );
346  if ( pPivot && pPivot <= pNode )
347  {
348  s->hProofPivot = hTemp;
349  pPivot = NULL;
350  }
351  }
352  Vec_SetWriteEntryNum( vProof, Vec_IntSize(vUsed) );
353  Vec_IntFree( vUsed );
354 
355  // report the result
356  if ( fVerbose )
357  {
358  printf( "\n" );
359  printf( "The proof was reduced from %6.2f MB to %6.2f MB (by %6.2f %%) ",
360  1.0 * Vec_SetMemory(vProof) / (1<<20), 1.0 * Vec_SetMemoryS(vProof) / (1<<20),
361  100.0 * (Vec_SetMemory(vProof) - Vec_SetMemoryS(vProof)) / Vec_SetMemory(vProof) );
362  TimeTotal += Abc_Clock() - clk;
363  Abc_PrintTime( 1, "Time", TimeTotal );
364  }
365  Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) );
366 // Sat_ProofReduceCheck( s );
367 }
368 */
369 
370 
371 void Sat_ProofCheck0( Vec_Set_t * vProof )
372 {
373  satset * pNode, * pFanin;
374  int i, j, k, nSize;
375  Vec_SetForEachEntry( satset *, vProof, nSize, pNode, i, j )
376  {
377  nSize = Vec_SetWordNum( 2 + pNode->nEnts );
378  Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
379  assert( (pNode->pEnts[k] >> 2) );
380  }
381 }
382 
383 int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
384 {
385 // Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
386 // Vec_Int_t * vRoots = (Vec_Int_t *)&s->claProofs;
387  Vec_Int_t * vRoots = (Vec_Int_t *)pRoots;
388 // Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
389  int fVerbose = 0;
390  Vec_Ptr_t * vUsed;
391  satset * pNode, * pFanin, * pPivot;
392  int i, j, k, hTemp, nSize;
393  abctime clk = Abc_Clock();
394  static abctime TimeTotal = 0;
395  int RetValue;
396 //Sat_ProofCheck0( vProof );
397 
398  // collect visited nodes
399  nSize = Proof_MarkUsedRec( vProof, vRoots );
400  vUsed = Vec_PtrAlloc( nSize );
401 //Sat_ProofCheck0( vProof );
402 
403  // relabel nodes to use smaller space
404  Vec_SetShrinkS( vProof, 2 );
405  Vec_SetForEachEntry( satset *, vProof, nSize, pNode, i, j )
406  {
407  nSize = Vec_SetWordNum( 2 + pNode->nEnts );
408  if ( pNode->Id == 0 )
409  continue;
410  pNode->Id = Vec_SetAppendS( vProof, 2 + pNode->nEnts );
411  assert( pNode->Id > 0 );
412  Vec_PtrPush( vUsed, pNode );
413  // update fanins
414  Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
415  if ( (pNode->pEnts[k] & 1) == 0 ) // proof node
416  {
417  assert( pFanin->Id > 0 );
418  pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2);
419  }
420 // else // problem clause
421 // assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) );
422  }
423  // update roots
424  Proof_ForeachNodeVec1( vRoots, vProof, pNode, i )
425  Vec_IntWriteEntry( vRoots, i, pNode->Id );
426  // determine new pivot
427  assert( hProofPivot >= 1 && hProofPivot <= Vec_SetHandCurrent(vProof) );
428  pPivot = Proof_NodeRead( vProof, hProofPivot );
429  RetValue = Vec_SetHandCurrentS(vProof);
430  // compact the nodes
431  Vec_PtrForEachEntry( satset *, vUsed, pNode, i )
432  {
433  hTemp = pNode->Id; pNode->Id = 0;
434  memmove( Vec_SetEntry(vProof, hTemp), pNode, sizeof(word)*Proof_NodeWordNum(pNode->nEnts) );
435  if ( pPivot && pPivot <= pNode )
436  {
437  RetValue = hTemp;
438  pPivot = NULL;
439  }
440  }
441  Vec_SetWriteEntryNum( vProof, Vec_PtrSize(vUsed) );
442  Vec_PtrFree( vUsed );
443 
444  // report the result
445  if ( fVerbose )
446  {
447  printf( "\n" );
448  printf( "The proof was reduced from %6.2f MB to %6.2f MB (by %6.2f %%) ",
449  1.0 * Vec_SetMemory(vProof) / (1<<20), 1.0 * Vec_SetMemoryS(vProof) / (1<<20),
450  100.0 * (Vec_SetMemory(vProof) - Vec_SetMemoryS(vProof)) / Vec_SetMemory(vProof) );
451  TimeTotal += Abc_Clock() - clk;
452  Abc_PrintTime( 1, "Time", TimeTotal );
453  }
454  Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) );
455  Vec_SetShrinkLimits( vProof );
456 // Sat_ProofReduceCheck( s );
457 //Sat_ProofCheck0( vProof );
458 
459  return RetValue;
460 }
461 
462 #if 0
463 
464 /**Function*************************************************************
465 
466  Synopsis [Performs one resultion step.]
467 
468  Description [Returns ID of the resolvent if success, and -1 if failure.]
469 
470  SideEffects []
471 
472  SeeAlso []
473 
474 ***********************************************************************/
475 int Sat_ProofCheckResolveOne( Vec_Set_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp )
476 {
477  satset * c;
478  int h, i, k, Var = -1, Count = 0;
479  // find resolution variable
480  for ( i = 0; i < (int)c1->nEnts; i++ )
481  for ( k = 0; k < (int)c2->nEnts; k++ )
482  if ( (c1->pEnts[i] ^ c2->pEnts[k]) == 1 )
483  {
484  Var = (c1->pEnts[i] >> 1);
485  Count++;
486  }
487  if ( Count == 0 )
488  {
489  printf( "Cannot find resolution variable\n" );
490  return 0;
491  }
492  if ( Count > 1 )
493  {
494  printf( "Found more than 1 resolution variables\n" );
495  return 0;
496  }
497  // perform resolution
498  Vec_IntClear( vTemp );
499  Vec_IntPush( vTemp, 0 ); // placeholder
500  Vec_IntPush( vTemp, 0 );
501  for ( i = 0; i < (int)c1->nEnts; i++ )
502  if ( (c1->pEnts[i] >> 1) != Var )
503  Vec_IntPush( vTemp, c1->pEnts[i] );
504  for ( i = 0; i < (int)c2->nEnts; i++ )
505  if ( (c2->pEnts[i] >> 1) != Var )
506  Vec_IntPushUnique( vTemp, c2->pEnts[i] );
507  // create new resolution entry
508  h = Vec_SetAppend( p, Vec_IntArray(vTemp), Vec_IntSize(vTemp) );
509  // return the new entry
510  c = Proof_NodeRead( p, h );
511  c->nEnts = Vec_IntSize(vTemp)-2;
512  return h;
513 }
514 
515 /**Function*************************************************************
516 
517  Synopsis [Checks the proof for consitency.]
518 
519  Description []
520 
521  SideEffects []
522 
523  SeeAlso []
524 
525 ***********************************************************************/
526 satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Set_t * vProof, Vec_Set_t * vResolves, int iAnt )
527 {
528  satset * pAnt;
529  if ( iAnt & 1 )
530  return Proof_ClauseRead( vClauses, iAnt >> 2 );
531  assert( iAnt > 0 );
532  pAnt = Proof_NodeRead( vProof, iAnt >> 2 );
533  assert( pAnt->Id > 0 );
534  return Proof_NodeRead( vResolves, pAnt->Id );
535 }
536 
537 /**Function*************************************************************
538 
539  Synopsis [Checks the proof for consitency.]
540 
541  Description []
542 
543  SideEffects []
544 
545  SeeAlso []
546 
547 ***********************************************************************/
548 void Sat_ProofCheck( sat_solver2 * s )
549 {
550  Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
551  Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
552  Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots;
553  Vec_Set_t * vResolves;
554  Vec_Int_t * vUsed, * vTemp;
555  satset * pSet, * pSet0 = NULL, * pSet1;
556  int i, k, hRoot, Handle, Counter = 0;
557  abctime clk = Abc_Clock();
558  hRoot = s->hProofLast;
559  if ( hRoot == -1 )
560  return;
561  // collect visited clauses
562  vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
563  Proof_CleanCollected( vProof, vUsed );
564  // perform resolution steps
565  vTemp = Vec_IntAlloc( 1000 );
566  vResolves = Vec_SetAlloc( 20 );
567  Proof_ForeachNodeVec( vUsed, vProof, pSet, i )
568  {
569  Handle = -1;
570  pSet0 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] );
571  for ( k = 1; k < (int)pSet->nEnts; k++ )
572  {
573  pSet1 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] );
574  Handle = Sat_ProofCheckResolveOne( vResolves, pSet0, pSet1, vTemp );
575  pSet0 = Proof_NodeRead( vResolves, Handle );
576  }
577  pSet->Id = Handle;
578  Counter++;
579  }
580  Vec_IntFree( vTemp );
581  // clean the proof
582  Proof_CleanCollected( vProof, vUsed );
583  // compare the final clause
584  printf( "Used %6.2f MB for resolvents.\n", 1.0 * Vec_SetMemory(vResolves) / (1<<20) );
585  if ( pSet0->nEnts > 0 )
586  printf( "Derived clause with %d lits instead of the empty clause. ", pSet0->nEnts );
587  else
588  printf( "Proof verification successful. " );
589  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
590  // cleanup
591  Vec_SetFree( vResolves );
592  Vec_IntFree( vUsed );
593 }
594 #endif
595 
596 /**Function*************************************************************
597 
598  Synopsis [Collects nodes belonging to the UNSAT core.]
599 
600  Description [The resulting array contains 1-based IDs of root clauses.]
601 
602  SideEffects []
603 
604  SeeAlso []
605 
606 ***********************************************************************/
607 Vec_Int_t * Sat_ProofCollectCore( Vec_Set_t * vProof, Vec_Int_t * vUsed )
608 {
609  Vec_Int_t * vCore;
610  satset * pNode, * pFanin;
611  unsigned * pBitMap;
612  int i, k, MaxCla = 0;
613  // find the largest number
614  Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
615  Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
616  if ( pFanin == NULL )
617  MaxCla = Abc_MaxInt( MaxCla, pNode->pEnts[k] >> 2 );
618  // allocate bitmap
619  pBitMap = ABC_CALLOC( unsigned, Abc_BitWordNum(MaxCla) + 1 );
620  // collect leaves
621  vCore = Vec_IntAlloc( 1000 );
622  Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
623  Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
624  if ( pFanin == NULL )
625  {
626  int Entry = (pNode->pEnts[k] >> 2);
627  if ( Abc_InfoHasBit(pBitMap, Entry) )
628  continue;
629  Abc_InfoSetBit(pBitMap, Entry);
630  Vec_IntPush( vCore, Entry );
631  }
632  ABC_FREE( pBitMap );
633 // Vec_IntUniqify( vCore );
634  return vCore;
635 }
636 
637 #if 0
638 
639 /**Function*************************************************************
640 
641  Synopsis [Verifies that variables are labeled correctly.]
642 
643  Description []
644 
645  SideEffects []
646 
647  SeeAlso []
648 
649 ***********************************************************************/
650 void Sat_ProofInterpolantCheckVars( sat_solver2 * s, Vec_Int_t * vGloVars )
651 {
652  satset* c;
653  Vec_Int_t * vVarMap;
654  int i, k, Entry, * pMask;
655  int Counts[5] = {0};
656  // map variables into their type (A, B, or AB)
657  vVarMap = Vec_IntStart( s->size );
658  sat_solver_foreach_clause( s, c, i )
659  for ( k = 0; k < (int)c->nEnts; k++ )
660  *Vec_IntEntryP(vVarMap, lit_var(c->pEnts[k])) |= 2 - c->partA;
661  // analyze variables
662  Vec_IntForEachEntry( vGloVars, Entry, i )
663  {
664  pMask = Vec_IntEntryP(vVarMap, Entry);
665  assert( *pMask >= 0 && *pMask <= 3 );
666  Counts[(*pMask & 3)]++;
667  *pMask = 0;
668  }
669  // count the number of global variables not listed
670  Vec_IntForEachEntry( vVarMap, Entry, i )
671  if ( Entry == 3 )
672  Counts[4]++;
673  Vec_IntFree( vVarMap );
674  // report
675  if ( Counts[0] )
676  printf( "Warning: %6d variables listed as global do not appear in clauses (this is normal)\n", Counts[0] );
677  if ( Counts[1] )
678  printf( "Warning: %6d variables listed as global appear only in A-clauses (this is a BUG)\n", Counts[1] );
679  if ( Counts[2] )
680  printf( "Warning: %6d variables listed as global appear only in B-clauses (this is a BUG)\n", Counts[2] );
681  if ( Counts[3] )
682  printf( "Warning: %6d (out of %d) variables listed as global appear in both A- and B-clauses (this is normal)\n", Counts[3], Vec_IntSize(vGloVars) );
683  if ( Counts[4] )
684  printf( "Warning: %6d variables not listed as global appear in both A- and B-clauses (this is a BUG)\n", Counts[4] );
685 }
686 
687 /**Function*************************************************************
688 
689  Synopsis [Computes interpolant of the proof.]
690 
691  Description [Aassuming that vars/clause of partA are marked.]
692 
693  SideEffects []
694 
695  SeeAlso []
696 
697 ***********************************************************************/
698 void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
699 {
700  Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
701  Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
702  Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars;
703  Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots;
704  Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap;
705  satset * pNode, * pFanin;
706  Aig_Man_t * pAig;
707  Aig_Obj_t * pObj = NULL;
708  int i, k, iVar, Lit, Entry, hRoot;
709 // if ( s->hLearntLast < 0 )
710 // return NULL;
711 // hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
712  hRoot = s->hProofLast;
713  if ( hRoot == -1 )
714  return NULL;
715 
716  Sat_ProofInterpolantCheckVars( s, vGlobVars );
717 
718  // collect visited nodes
719  vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
720  // collect core clauses (cleans vUsed and vCore)
721  vCore = Sat_ProofCollectCore( vProof, vUsed );
722  // vCore arrived in terms of clause handles
723 
724  // map variables into their global numbers
725  vVarMap = Vec_IntStartFull( s->size );
726  Vec_IntForEachEntry( vGlobVars, Entry, i )
727  Vec_IntWriteEntry( vVarMap, Entry, i );
728 
729  // start the AIG
730  pAig = Aig_ManStart( 10000 );
731  pAig->pName = Abc_UtilStrsav( "interpol" );
732  for ( i = 0; i < Vec_IntSize(vGlobVars); i++ )
733  Aig_ObjCreateCi( pAig );
734 
735  // copy the numbers out and derive interpol for clause
736  vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) );
737  Proof_ForeachClauseVec( vCore, vClauses, pNode, i )
738  {
739  if ( pNode->partA )
740  {
741  pObj = Aig_ManConst0( pAig );
742  satset_foreach_lit( pNode, Lit, k, 0 )
743  if ( (iVar = Vec_IntEntry(vVarMap, lit_var(Lit))) >= 0 )
744  pObj = Aig_Or( pAig, pObj, Aig_NotCond(Aig_IthVar(pAig, iVar), lit_sign(Lit)) );
745  }
746  else
747  pObj = Aig_ManConst1( pAig );
748  // remember the interpolant
749  Vec_IntPush( vCoreNums, pNode->Id );
750  pNode->Id = Aig_ObjToLit(pObj);
751  }
752  Vec_IntFree( vVarMap );
753 
754  // copy the numbers out and derive interpol for resolvents
755  Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
756  {
757 // satset_print( pNode );
758  assert( pNode->nEnts > 1 );
759  Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
760  {
761  assert( pFanin->Id < 2*Aig_ManObjNumMax(pAig) );
762  if ( k == 0 )
763  pObj = Aig_ObjFromLit( pAig, pFanin->Id );
764  else if ( pNode->pEnts[k] & 2 ) // variable of A
765  pObj = Aig_Or( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) );
766  else
767  pObj = Aig_And( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) );
768  }
769  // remember the interpolant
770  pNode->Id = Aig_ObjToLit(pObj);
771  }
772  // save the result
773 // assert( Proof_NodeHandle(vProof, pNode) == hRoot );
774  Aig_ObjCreateCo( pAig, pObj );
775  Aig_ManCleanup( pAig );
776 
777  // move the results back
778  Proof_ForeachClauseVec( vCore, vClauses, pNode, i )
779  pNode->Id = Vec_IntEntry( vCoreNums, i );
780  Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
781  pNode->Id = 0;
782  // cleanup
783  Vec_IntFree( vCore );
784  Vec_IntFree( vUsed );
785  Vec_IntFree( vCoreNums );
786  return pAig;
787 }
788 
789 
790 /**Function*************************************************************
791 
792  Synopsis [Computes interpolant of the proof.]
793 
794  Description [Aassuming that vars/clause of partA are marked.]
795 
796  SideEffects []
797 
798  SeeAlso []
799 
800 ***********************************************************************/
801 word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
802 {
803  Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses;
804  Vec_Set_t * vProof = (Vec_Set_t *)&s->Proofs;
805  Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars;
806  Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots;
807  Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap;
808  satset * pNode, * pFanin;
809  Tru_Man_t * pTru;
810  int nVars = Vec_IntSize(vGlobVars);
811  int nWords = (nVars < 6) ? 1 : (1 << (nVars-6));
812  word * pRes = ABC_ALLOC( word, nWords );
813  int i, k, iVar, Lit, Entry, hRoot;
814  assert( nVars > 0 && nVars <= 16 );
815  hRoot = s->hProofLast;
816  if ( hRoot == -1 )
817  return NULL;
818 
819  Sat_ProofInterpolantCheckVars( s, vGlobVars );
820 
821  // collect visited nodes
822  vUsed = Proof_CollectUsedIter( vProof, vRoots, 1 );
823  // collect core clauses (cleans vUsed and vCore)
824  vCore = Sat_ProofCollectCore( vProof, vUsed, 0 );
825  // vCore arrived in terms of clause handles
826 
827  // map variables into their global numbers
828  vVarMap = Vec_IntStartFull( s->size );
829  Vec_IntForEachEntry( vGlobVars, Entry, i )
830  Vec_IntWriteEntry( vVarMap, Entry, i );
831 
832  // start the AIG
833  pTru = Tru_ManAlloc( nVars );
834 
835  // copy the numbers out and derive interpol for clause
836  vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) );
837  Proof_ForeachClauseVec( vCore, vClauses, pNode, i )
838  {
839  if ( pNode->partA )
840  {
841 // pObj = Aig_ManConst0( pAig );
842  Tru_ManClear( pRes, nWords );
843  satset_foreach_lit( pNode, Lit, k, 0 )
844  if ( (iVar = Vec_IntEntry(vVarMap, lit_var(Lit))) >= 0 )
845 // pObj = Aig_Or( pAig, pObj, Aig_NotCond(Aig_IthVar(pAig, iVar), lit_sign(Lit)) );
846  pRes = Tru_ManOrNotCond( pRes, Tru_ManVar(pTru, iVar), nWords, lit_sign(Lit) );
847  }
848  else
849 // pObj = Aig_ManConst1( pAig );
850  Tru_ManFill( pRes, nWords );
851  // remember the interpolant
852  Vec_IntPush( vCoreNums, pNode->Id );
853 // pNode->Id = Aig_ObjToLit(pObj);
854  pNode->Id = Tru_ManInsert( pTru, pRes );
855  }
856  Vec_IntFree( vVarMap );
857 
858  // copy the numbers out and derive interpol for resolvents
859  Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
860  {
861 // satset_print( pNode );
862  assert( pNode->nEnts > 1 );
863  Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
864  {
865 // assert( pFanin->Id < 2*Aig_ManObjNumMax(pAig) );
866 // assert( pFanin->Id <= Tru_ManHandleMax(pTru) );
867  if ( k == 0 )
868 // pObj = Aig_ObjFromLit( pAig, pFanin->Id );
869  pRes = Tru_ManCopyNotCond( pRes, Tru_ManFunc(pTru, pFanin->Id & ~1), nWords, pFanin->Id & 1 );
870  else if ( pNode->pEnts[k] & 2 ) // variable of A
871 // pObj = Aig_Or( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) );
872  pRes = Tru_ManOrNotCond( pRes, Tru_ManFunc(pTru, pFanin->Id & ~1), nWords, pFanin->Id & 1 );
873  else
874 // pObj = Aig_And( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) );
875  pRes = Tru_ManAndNotCond( pRes, Tru_ManFunc(pTru, pFanin->Id & ~1), nWords, pFanin->Id & 1 );
876  }
877  // remember the interpolant
878 // pNode->Id = Aig_ObjToLit(pObj);
879  pNode->Id = Tru_ManInsert( pTru, pRes );
880  }
881  // save the result
882 // assert( Proof_NodeHandle(vProof, pNode) == hRoot );
883 // Aig_ObjCreateCo( pAig, pObj );
884 // Aig_ManCleanup( pAig );
885 
886  // move the results back
887  Proof_ForeachClauseVec( vCore, vClauses, pNode, i )
888  pNode->Id = Vec_IntEntry( vCoreNums, i );
889  Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
890  pNode->Id = 0;
891  // cleanup
892  Vec_IntFree( vCore );
893  Vec_IntFree( vUsed );
894  Vec_IntFree( vCoreNums );
895  Tru_ManFree( pTru );
896 // ABC_FREE( pRes );
897  return pRes;
898 }
899 
900 #endif
901 
902 /**Function*************************************************************
903 
904  Synopsis [Computes UNSAT core.]
905 
906  Description [The result is the array of root clause indexes.]
907 
908  SideEffects []
909 
910  SeeAlso []
911 
912 ***********************************************************************/
913 void * Proof_DeriveCore( Vec_Set_t * vProof, int hRoot )
914 {
915  Vec_Int_t Roots = { 1, 1, &hRoot }, * vRoots = &Roots;
916  Vec_Int_t * vCore, * vUsed;
917  if ( hRoot == -1 )
918  return NULL;
919  // collect visited clauses
920  vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 );
921  // collect core clauses
922  vCore = Sat_ProofCollectCore( vProof, vUsed );
923  Vec_IntFree( vUsed );
924  Vec_IntSort( vCore, 1 );
925  return vCore;
926 }
927 
928 
929 ////////////////////////////////////////////////////////////////////////
930 /// END OF FILE ///
931 ////////////////////////////////////////////////////////////////////////
932 
933 ABC_NAMESPACE_IMPL_END
934 
Proof_CleanCollected
void Proof_CleanCollected(Vec_Set_t *vProof, Vec_Int_t *vUsed)
FUNCTION DEFINITIONS ///.
Definition: satProof.c:96
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
satset_t::pEnts
int pEnts[0]
Definition: satProof.c:49
satset_t
Definition: satProof.c:42
Vec_SetShrinkS
static void Vec_SetShrinkS(Vec_Set_t *p, int h)
Definition: vecSet.h:263
Tru_ManFree
void Tru_ManFree(Tru_Man_t *p)
Definition: satTruth.c:248
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Vec_SetAppendS
static int Vec_SetAppendS(Vec_Set_t *p, int nSize)
Definition: vecSet.h:236
satset_t::learnt
unsigned learnt
Definition: satProof.c:44
Vec_SetShrinkLimits
static void Vec_SetShrinkLimits(Vec_Set_t *p)
Definition: vecSet.h:270
sat_solver2_t::size
int size
Definition: satSolver2.h:92
Tru_ManAlloc
Tru_Man_t * Tru_ManAlloc(int nVars)
FUNCTION DECLARATIONS ///.
Definition: satTruth.c:198
Proof_CollectUsed_iter
void Proof_CollectUsed_iter(Vec_Set_t *vProof, int hNode, Vec_Int_t *vUsed, Vec_Int_t *vStack)
Definition: satProof.c:115
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Vec_SetFree
static void Vec_SetFree(Vec_Set_t *p)
Definition: vecSet.h:176
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Sat_ProofCheck
void Sat_ProofCheck(sat_solver2 *s)
sat_solver2_t::hProofLast
int hProofLast
Definition: satSolver2.h:165
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
satset_t::partA
unsigned partA
Definition: satProof.c:46
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Vec_SetForEachEntry
#define Vec_SetForEachEntry(Type, pVec, nSize, pSet, p, s)
Definition: vecSet.h:96
lit_var
static int lit_var(lit l)
Definition: satVec.h:145
Proof_DeriveCore
void * Proof_DeriveCore(Vec_Set_t *vProof, int hRoot)
Definition: satProof.c:913
Vec_SetWriteEntryNum
static void Vec_SetWriteEntryNum(Vec_Set_t *p, int i)
Definition: vecSet.h:72
sat_solver2_t
Definition: satSolver2.h:90
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Vec_SetAlloc
static Vec_Set_t * Vec_SetAlloc(int nPageSize)
Definition: vecSet.h:128
Vec_SetHandCurrent
static int Vec_SetHandCurrent(Vec_Set_t *p)
Definition: vecSet.h:83
Proof_CollectUsed_rec
void Proof_CollectUsed_rec(Vec_Set_t *vProof, int hNode, Vec_Int_t *vUsed)
Definition: satProof.c:187
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_ManConst0
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
Definition: aig.h:263
Tru_ManOrNotCond
static word * Tru_ManOrNotCond(word *pOut, word *pIn, int nWords, int fCompl)
Definition: satTruth.h:68
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Sat_ProofInterpolant
void * Sat_ProofInterpolant(sat_solver2 *s, void *pGloVars)
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Vec_SetEntry
static word * Vec_SetEntry(Vec_Set_t *p, int h)
Definition: vecSet.h:70
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Vec_SetAppend
static int Vec_SetAppend(Vec_Set_t *p, int *pArray, int nSize)
Definition: vecSet.h:213
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Proof_NodeRead
static satset * Proof_NodeRead(Vec_Set_t *p, int h)
DECLARATIONS ///.
Definition: satProof.c:58
Proof_CollectUsedRec
Vec_Int_t * Proof_CollectUsedRec(Vec_Set_t *vProof, Vec_Int_t *vRoots)
Definition: satProof.c:199
Vec_IntSort
static void Vec_IntSort(Vec_Int_t *p, int fReverse)
Definition: vecInt.h:1293
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
satset
typedefABC_NAMESPACE_IMPL_START struct satset_t satset
Definition: satProof.c:41
nWords
int nWords
Definition: abcNpn.c:127
Proof_ForeachNodeVec
#define Proof_ForeachNodeVec(pVec, p, pNode, i)
Definition: satProof.c:66
for
for(p=first;p->value< newval;p=p->next)
Tru_ManAndNotCond
static word * Tru_ManAndNotCond(word *pOut, word *pIn, int nWords, int fCompl)
Definition: satTruth.h:67
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
memmove
char * memmove()
Proof_MarkUsed_rec
int Proof_MarkUsed_rec(Vec_Set_t *vProof, int hNode)
Definition: satProof.c:221
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Vec_SetWordNum
static int Vec_SetWordNum(int nSize)
Definition: vecSet.h:67
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Abc_MergeSort
void Abc_MergeSort(int *pInput, int nSize)
Definition: utilSort.c:129
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Vec_SetShrink
static void Vec_SetShrink(Vec_Set_t *p, int h)
Definition: vecSet.h:257
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Proof_ClauseSetEnts
void Proof_ClauseSetEnts(Vec_Set_t *p, int h, int nEnts)
Definition: satProof.c:61
Aig_ObjFromLit
static Aig_Obj_t * Aig_ObjFromLit(Aig_Man_t *p, int iLit)
Definition: aig.h:322
Sat_ProofCheck0
void Sat_ProofCheck0(Vec_Set_t *vProof)
Definition: satProof.c:371
Aig_IthVar
Aig_Obj_t * Aig_IthVar(Aig_Man_t *p, int i)
FUNCTION DEFINITIONS ///.
Definition: aigOper.c:63
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
satset_t::nEnts
unsigned nEnts
Definition: satProof.c:47
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
if
if(last==0)
Definition: sparse_int.h:34
else
else
Definition: sparse_int.h:55
Vec_IntPop
static int Vec_IntPop(Vec_Int_t *p)
Definition: extraZddTrunc.c:110
Aig_Or
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:259
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Proof_ForeachClauseVec
#define Proof_ForeachClauseVec(pVec, p, pNode, i)
Definition: satProof.c:64
Counter
static int Counter
Definition: extraBddMisc.c:1877
Vec_SetMemory
static int Vec_SetMemory(Vec_Set_t *p)
Definition: vecSet.h:87
Tru_Man_t
typedefABC_NAMESPACE_HEADER_START struct Tru_Man_t_ Tru_Man_t
INCLUDES ///.
Definition: satTruth.h:44
Tru_ManFunc
word * Tru_ManFunc(Tru_Man_t *p, int h)
Definition: satTruth.c:285
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Tru_ManInsert
int Tru_ManInsert(Tru_Man_t *p, word *pTruth)
Definition: satTruth.c:158
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Proof_NodeForeachFanin
#define Proof_NodeForeachFanin(pProof, pNode, pFanin, i)
Definition: satProof.c:72
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Aig_ObjToLit
static int Aig_ObjToLit(Aig_Obj_t *pObj)
Definition: aig.h:321
Proof_NodeWordNum
static int Proof_NodeWordNum(int nEnts)
Definition: satProof.c:59
satset_t::mark
unsigned mark
Definition: satProof.c:45
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_SetHandCurrentS
static int Vec_SetHandCurrentS(Vec_Set_t *p)
Definition: vecSet.h:84
Vec_Set_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Set_t_ Vec_Set_t
INCLUDES ///.
Definition: vecSet.h:49
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
lit_sign
static int lit_sign(lit l)
Definition: satVec.h:146
satset_t::Id
int Id
Definition: satProof.c:48
Tru_ManClear
static word * Tru_ManClear(word *pOut, int nWords)
Definition: satTruth.h:58
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Proof_MarkUsedRec
int Proof_MarkUsedRec(Vec_Set_t *vProof, Vec_Int_t *vRoots)
Definition: satProof.c:233
Tru_ManCopyNotCond
static word * Tru_ManCopyNotCond(word *pOut, word *pIn, int nWords, int fCompl)
Definition: satTruth.h:66
Tru_ManFill
static word * Tru_ManFill(word *pOut, int nWords)
Definition: satTruth.h:59
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Minisat::Var
int Var
Definition: SolverTypes.h:42
Vec_SetMemoryS
static int Vec_SetMemoryS(Vec_Set_t *p)
Definition: vecSet.h:88
Proof_CollectUsedIter
Vec_Int_t * Proof_CollectUsedIter(Vec_Set_t *vProof, Vec_Int_t *vRoots, int fSort)
Definition: satProof.c:145
Abc_BitWordNum
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
Sat_ProofInterpolantTruth
word * Sat_ProofInterpolantTruth(sat_solver2 *s, void *pGloVars)
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntEntryP
static int * Vec_IntEntryP(Vec_Int_t *p, int i)
Definition: vecInt.h:417
Proof_ForeachNodeVec1
#define Proof_ForeachNodeVec1(pVec, p, pNode, i)
Definition: satProof.c:68
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Vec_IntPushUnique
static int Vec_IntPushUnique(Vec_Int_t *p, int Entry)
Definition: vecInt.h:832
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Sat_ProofReduce
int Sat_ProofReduce(Vec_Set_t *vProof, void *pRoots, int hProofPivot)
Definition: satProof.c:383
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Sat_ProofCollectCore
Vec_Int_t * Sat_ProofCollectCore(Vec_Set_t *vProof, Vec_Int_t *vUsed)
Definition: satProof.c:607
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Tru_ManVar
word * Tru_ManVar(Tru_Man_t *p, int v)
Definition: satTruth.c:268