abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraClaus.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [fraClaus.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [New FRAIG package.]
8 
9  Synopsis [Induction with clause strengthening.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 30, 2007.]
16 
17  Revision [$Id: fraClau.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "fra.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satSolver.h"
24 
25 ABC_NAMESPACE_IMPL_START
26 
27 
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 typedef struct Clu_Man_t_ Clu_Man_t;
33 struct Clu_Man_t_
34 {
35  // parameters
36  int nFrames; // the K of the K-step induction
37  int nPref; // the number of timeframes to skip
38  int nClausesMax; // the max number of 4-clauses to consider
39  int nLutSize; // the max cut size
40  int nLevels; // the number of levels for cut computation
41  int nCutsMax; // the maximum number of cuts to compute at a node
42  int nBatches; // the number of clause batches to use
43  int fStepUp; // increase cut size for each batch
44  int fTarget; // tries to prove the property
45  int fVerbose;
46  int fVeryVerbose;
47  // internal parameters
48  int nSimWords; // the number of simulation words
49  int nSimWordsPref; // the number of simulation words in the prefix
50  int nSimFrames; // the number of frames to simulate
51  int nBTLimit; // the largest number of backtracks (0 = infinite)
52  // the network
53  Aig_Man_t * pAig;
54  // SAT solvers
55  sat_solver * pSatMain;
56  sat_solver * pSatBmc;
57  // CNF for the test solver
58  Cnf_Dat_t * pCnf;
59  int fFail;
60  int fFiltering;
61  int fNothingNew;
62  // clauses
63  Vec_Int_t * vLits;
64  Vec_Int_t * vClauses;
65  Vec_Int_t * vCosts;
66  int nClauses;
67  int nCuts;
68  int nOneHots;
69  int nOneHotsProven;
70  // clauses proven
71  Vec_Int_t * vLitsProven;
72  Vec_Int_t * vClausesProven;
73  // counter-examples
74  Vec_Ptr_t * vCexes;
75  int nCexes;
76  int nCexesAlloc;
77 };
78 
79 ////////////////////////////////////////////////////////////////////////
80 /// FUNCTION DEFINITIONS ///
81 ////////////////////////////////////////////////////////////////////////
82 
83 /**Function*************************************************************
84 
85  Synopsis [Runs the SAT solver on the problem.]
86 
87  Description []
88 
89  SideEffects []
90 
91  SeeAlso []
92 
93 ***********************************************************************/
94 int Fra_ClausRunBmc( Clu_Man_t * p )
95 {
96  Aig_Obj_t * pObj;
97  int Lits[2], nLitsTot, RetValue, i;
98  // set the output literals
99  nLitsTot = 2 * p->pCnf->nVars;
100  pObj = Aig_ManCo(p->pAig, 0);
101  for ( i = 0; i < p->nPref + p->nFrames; i++ )
102  {
103  Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 0 );
104  RetValue = sat_solver_solve( p->pSatBmc, Lits, Lits + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
105  if ( RetValue != l_False )
106  return 0;
107  }
108  return 1;
109 }
110 
111 /**Function*************************************************************
112 
113  Synopsis [Runs the SAT solver on the problem.]
114 
115  Description []
116 
117  SideEffects []
118 
119  SeeAlso []
120 
121 ***********************************************************************/
122 int Fra_ClausRunSat( Clu_Man_t * p )
123 {
124  Aig_Obj_t * pObj;
125  int * pLits;
126  int i, RetValue;
127  pLits = ABC_ALLOC( int, p->nFrames + 1 );
128  // set the output literals
129  pObj = Aig_ManCo(p->pAig, 0);
130  for ( i = 0; i <= p->nFrames; i++ )
131  pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], i != p->nFrames );
132  // try to solve the problem
133  RetValue = sat_solver_solve( p->pSatMain, pLits, pLits + p->nFrames + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
134  ABC_FREE( pLits );
135  if ( RetValue == l_False )
136  return 1;
137  // get the counter-example
138  assert( RetValue == l_True );
139  return 0;
140 }
141 
142 /**Function*************************************************************
143 
144  Synopsis [Runs the SAT solver on the problem.]
145 
146  Description []
147 
148  SideEffects []
149 
150  SeeAlso []
151 
152 ***********************************************************************/
153 int Fra_ClausRunSat0( Clu_Man_t * p )
154 {
155  Aig_Obj_t * pObj;
156  int Lits[2], RetValue;
157  pObj = Aig_ManCo(p->pAig, 0);
158  Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 0 );
159  RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
160  if ( RetValue == l_False )
161  return 1;
162  return 0;
163 }
164 
165 /**Function*************************************************************
166 
167  Synopsis [Return combinations appearing in the cut.]
168 
169  Description [This procedure is taken from "Hacker's Delight" by H.S.Warren.]
170 
171  SideEffects []
172 
173  SeeAlso []
174 
175 ***********************************************************************/
176 void transpose32a( unsigned a[32] )
177 {
178  int j, k;
179  unsigned long m, t;
180  for ( j = 16, m = 0x0000FFFF; j; j >>= 1, m ^= m << j )
181  {
182  for ( k = 0; k < 32; k = ((k | j) + 1) & ~j )
183  {
184  t = (a[k] ^ (a[k|j] >> j)) & m;
185  a[k] ^= t;
186  a[k|j] ^= (t << j);
187  }
188  }
189 }
190 
191 /**Function*************************************************************
192 
193  Synopsis [Return combinations appearing in the cut.]
194 
195  Description []
196 
197  SideEffects []
198 
199  SeeAlso []
200 
201 ***********************************************************************/
202 int Fra_ClausProcessClausesCut( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * pCut, int * pScores )
203 {
204  unsigned Matrix[32];
205  unsigned * pSims[16], uWord;
206  int nSeries, i, k, j;
207  int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
208  // compute parameters
209  assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 );
210  assert( nWordsForSim % 8 == 0 );
211  // get parameters
212  for ( i = 0; i < (int)pCut->nLeaves; i++ )
213  pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] ) + p->nSimWordsPref;
214  // add combinational patterns
215  memset( pScores, 0, sizeof(int) * 16 );
216  nSeries = nWordsForSim / 8;
217  for ( i = 0; i < nSeries; i++ )
218  {
219  memset( Matrix, 0, sizeof(unsigned) * 32 );
220  for ( k = 0; k < 8; k++ )
221  for ( j = 0; j < (int)pCut->nLeaves; j++ )
222  Matrix[31-(k*4+j)] = pSims[j][i*8+k];
223  transpose32a( Matrix );
224  for ( k = 0; k < 32; k++ )
225  for ( j = 0, uWord = Matrix[k]; j < 8; j++, uWord >>= 4 )
226  pScores[uWord & 0xF]++;
227  }
228  // collect patterns
229  uWord = 0;
230  for ( i = 0; i < 16; i++ )
231  if ( pScores[i] )
232  uWord |= (1 << i);
233 // Extra_PrintBinary( stdout, &uWord, 16 ); printf( "\n" );
234  return (int)uWord;
235 }
236 
237 /**Function*************************************************************
238 
239  Synopsis [Return combinations appearing in the cut.]
240 
241  Description []
242 
243  SideEffects []
244 
245  SeeAlso []
246 
247 ***********************************************************************/
248 int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * pCut, int * pScores )
249 {
250  unsigned * pSims[16], uWord;
251  int iMint, i, k, b;
252  int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
253  // compute parameters
254  assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 );
255  assert( nWordsForSim % 8 == 0 );
256  // get parameters
257  for ( i = 0; i < (int)pCut->nLeaves; i++ )
258  pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] ) + p->nSimWordsPref;
259  // add combinational patterns
260  memset( pScores, 0, sizeof(int) * 16 );
261  for ( i = 0; i < nWordsForSim; i++ )
262  for ( k = 0; k < 32; k++ )
263  {
264  iMint = 0;
265  for ( b = 0; b < (int)pCut->nLeaves; b++ )
266  if ( pSims[b][i] & (1 << k) )
267  iMint |= (1 << b);
268  pScores[iMint]++;
269  }
270  // collect patterns
271  uWord = 0;
272  for ( i = 0; i < 16; i++ )
273  if ( pScores[i] )
274  uWord |= (1 << i);
275 // Extra_PrintBinary( stdout, &uWord, 16 ); printf( "\n" );
276  return (int)uWord;
277 }
278 
279 /**Function*************************************************************
280 
281  Synopsis [Return the number of combinations appearing in the cut.]
282 
283  Description []
284 
285  SideEffects []
286 
287  SeeAlso []
288 
289 ***********************************************************************/
290 void Fra_ClausProcessClausesCut3( Clu_Man_t * p, Fra_Sml_t * pSimMan, Aig_Cut_t * pCut, int * pScores )
291 {
292  unsigned Matrix[32];
293  unsigned * pSims[16], uWord;
294  int iMint, i, j, k, b, nMints, nSeries;
295  int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
296 
297  // compute parameters
298  assert( pCut->nFanins > 1 && pCut->nFanins < 17 );
299  assert( nWordsForSim % 8 == 0 );
300  // get parameters
301  for ( i = 0; i < (int)pCut->nFanins; i++ )
302  pSims[i] = Fra_ObjSim( pSimMan, pCut->pFanins[i] ) + p->nSimWordsPref;
303  // add combinational patterns
304  nMints = (1 << pCut->nFanins);
305  memset( pScores, 0, sizeof(int) * nMints );
306 
307  if ( pCut->nLeafMax == 4 )
308  {
309  // convert the simulation patterns
310  nSeries = nWordsForSim / 8;
311  for ( i = 0; i < nSeries; i++ )
312  {
313  memset( Matrix, 0, sizeof(unsigned) * 32 );
314  for ( k = 0; k < 8; k++ )
315  for ( j = 0; j < (int)pCut->nFanins; j++ )
316  Matrix[31-(k*4+j)] = pSims[j][i*8+k];
317  transpose32a( Matrix );
318  for ( k = 0; k < 32; k++ )
319  for ( j = 0, uWord = Matrix[k]; j < 8; j++, uWord >>= 4 )
320  pScores[uWord & 0xF]++;
321  }
322  }
323  else
324  {
325  // go through the simulation patterns
326  for ( i = 0; i < nWordsForSim; i++ )
327  for ( k = 0; k < 32; k++ )
328  {
329  iMint = 0;
330  for ( b = 0; b < (int)pCut->nFanins; b++ )
331  if ( pSims[b][i] & (1 << k) )
332  iMint |= (1 << b);
333  pScores[iMint]++;
334  }
335  }
336 }
337 
338 
339 /**Function*************************************************************
340 
341  Synopsis [Returns the cut-off cost.]
342 
343  Description []
344 
345  SideEffects []
346 
347  SeeAlso []
348 
349 ***********************************************************************/
350 int Fra_ClausSelectClauses( Clu_Man_t * p )
351 {
352  int * pCostCount, nClauCount, Cost, CostMax, i, c;
353  assert( Vec_IntSize(p->vClauses) > p->nClausesMax );
354  // count how many implications have each cost
355  CostMax = p->nSimWords * 32 + 1;
356  pCostCount = ABC_ALLOC( int, CostMax );
357  memset( pCostCount, 0, sizeof(int) * CostMax );
358  Vec_IntForEachEntry( p->vCosts, Cost, i )
359  {
360  if ( Cost == -1 )
361  continue;
362  assert( Cost < CostMax );
363  pCostCount[ Cost ]++;
364  }
365  assert( pCostCount[0] == 0 );
366  // select the bound on the cost (above this bound, implication will be included)
367  nClauCount = 0;
368  for ( c = CostMax - 1; c > 0; c-- )
369  {
370  assert( pCostCount[c] >= 0 );
371  nClauCount += pCostCount[c];
372  if ( nClauCount >= p->nClausesMax )
373  break;
374  }
375  // collect implications with the given costs
376  nClauCount = 0;
377  Vec_IntForEachEntry( p->vCosts, Cost, i )
378  {
379  if ( Cost >= c && nClauCount < p->nClausesMax )
380  {
381  nClauCount++;
382  continue;
383  }
384  Vec_IntWriteEntry( p->vCosts, i, -1 );
385  }
386  ABC_FREE( pCostCount );
387  p->nClauses = nClauCount;
388 if ( p->fVerbose )
389 printf( "Selected %d clauses. Cost range: [%d < %d < %d]\n", nClauCount, 1, c, CostMax );
390  return c;
391 }
392 
393 
394 /**Function*************************************************************
395 
396  Synopsis [Processes the clauses.]
397 
398  Description []
399 
400  SideEffects []
401 
402  SeeAlso []
403 
404 ***********************************************************************/
405 void Fra_ClausRecordClause( Clu_Man_t * p, Dar_Cut_t * pCut, int iMint, int Cost )
406 {
407  int i;
408  for ( i = 0; i < (int)pCut->nLeaves; i++ )
409  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pCut->pLeaves[i]], (iMint&(1<<i)) ) );
410  Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
411  Vec_IntPush( p->vCosts, Cost );
412 }
413 
414 /**Function*************************************************************
415 
416  Synopsis [Processes the clauses.]
417 
418  Description []
419 
420  SideEffects []
421 
422  SeeAlso []
423 
424 ***********************************************************************/
425 void Fra_ClausRecordClause2( Clu_Man_t * p, Aig_Cut_t * pCut, int iMint, int Cost )
426 {
427  int i;
428  for ( i = 0; i < (int)pCut->nFanins; i++ )
429  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pCut->pFanins[i]], (iMint&(1<<i)) ) );
430  Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
431  Vec_IntPush( p->vCosts, Cost );
432 }
433 
434 /**Function*************************************************************
435 
436  Synopsis [Returns 1 if simulation info is composed of all zeros.]
437 
438  Description []
439 
440  SideEffects []
441 
442  SeeAlso []
443 
444 ***********************************************************************/
445 int Fra_ClausSmlNodeIsConst( Fra_Sml_t * pSeq, Aig_Obj_t * pObj )
446 {
447  unsigned * pSims;
448  int i;
449  pSims = Fra_ObjSim(pSeq, pObj->Id);
450  for ( i = pSeq->nWordsPref; i < pSeq->nWordsTotal; i++ )
451  if ( pSims[i] )
452  return 0;
453  return 1;
454 }
455 
456 /**Function*************************************************************
457 
458  Synopsis [Returns 1 if implications holds.]
459 
460  Description []
461 
462  SideEffects []
463 
464  SeeAlso []
465 
466 ***********************************************************************/
467 int Fra_ClausSmlNodesAreImp( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
468 {
469  unsigned * pSimL, * pSimR;
470  int k;
471  pSimL = Fra_ObjSim(pSeq, pObj1->Id);
472  pSimR = Fra_ObjSim(pSeq, pObj2->Id);
473  for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
474  if ( pSimL[k] & ~pSimR[k] ) // !(Obj1 -> Obj2)
475  return 0;
476  return 1;
477 }
478 
479 /**Function*************************************************************
480 
481  Synopsis [Returns 1 if implications holds.]
482 
483  Description []
484 
485  SideEffects []
486 
487  SeeAlso []
488 
489 ***********************************************************************/
490 int Fra_ClausSmlNodesAreImpC( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
491 {
492  unsigned * pSimL, * pSimR;
493  int k;
494  pSimL = Fra_ObjSim(pSeq, pObj1->Id);
495  pSimR = Fra_ObjSim(pSeq, pObj2->Id);
496  for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
497  if ( pSimL[k] & pSimR[k] )
498  return 0;
499  return 1;
500 }
501 
502 /**Function*************************************************************
503 
504  Synopsis [Processes the clauses.]
505 
506  Description []
507 
508  SideEffects []
509 
510  SeeAlso []
511 
512 ***********************************************************************/
513 int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq )
514 {
515  Aig_Obj_t * pObj1, * pObj2;
516  unsigned * pSims1, * pSims2;
517  int CostMax, i, k, nCountConst, nCountImps;
518 
519  nCountConst = nCountImps = 0;
520  CostMax = p->nSimWords * 32;
521 /*
522  // add the property
523  {
524  Aig_Obj_t * pObj;
525  int Lits[1];
526  pObj = Aig_ManCo( p->pAig, 0 );
527  Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 1 );
528  Vec_IntPush( p->vLits, Lits[0] );
529  Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
530  Vec_IntPush( p->vCosts, CostMax );
531  nCountConst++;
532 // printf( "Added the target property to the set of clauses to be inductively checked.\n" );
533  }
534 */
535 
536  pSeq->nWordsPref = p->nSimWordsPref;
537  Aig_ManForEachLoSeq( p->pAig, pObj1, i )
538  {
539  pSims1 = Fra_ObjSim( pSeq, pObj1->Id );
540  if ( Fra_ClausSmlNodeIsConst( pSeq, pObj1 ) )
541  {
542  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
543  Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
544  Vec_IntPush( p->vCosts, CostMax );
545  nCountConst++;
546  continue;
547  }
548  Aig_ManForEachLoSeq( p->pAig, pObj2, k )
549  {
550  pSims2 = Fra_ObjSim( pSeq, pObj2->Id );
551  if ( Fra_ClausSmlNodesAreImp( pSeq, pObj1, pObj2 ) )
552  {
553  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
554  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 0 ) );
555  Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
556  Vec_IntPush( p->vCosts, CostMax );
557  nCountImps++;
558  continue;
559  }
560  if ( Fra_ClausSmlNodesAreImp( pSeq, pObj2, pObj1 ) )
561  {
562  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 ) );
563  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 0 ) );
564  Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
565  Vec_IntPush( p->vCosts, CostMax );
566  nCountImps++;
567  continue;
568  }
569  if ( Fra_ClausSmlNodesAreImpC( pSeq, pObj1, pObj2 ) )
570  {
571  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
572  Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 ) );
573  Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
574  Vec_IntPush( p->vCosts, CostMax );
575  nCountImps++;
576  continue;
577  }
578  }
579  if ( nCountConst + nCountImps > p->nClausesMax / 2 )
580  break;
581  }
582  pSeq->nWordsPref = 0;
583  if ( p->fVerbose )
584  printf( "Collected %d register constants and %d one-hotness implications.\n", nCountConst, nCountImps );
585  p->nOneHots = nCountConst + nCountImps;
586  p->nOneHotsProven = 0;
587  return 0;
588 }
589 
590 /**Function*************************************************************
591 
592  Synopsis [Processes the clauses.]
593 
594  Description []
595 
596  SideEffects []
597 
598  SeeAlso []
599 
600 ***********************************************************************/
601 int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
602 {
603  Aig_MmFixed_t * pMemCuts;
604 // Aig_ManCut_t * pManCut;
605  Fra_Sml_t * pComb, * pSeq;
606  Aig_Obj_t * pObj;
607  Dar_Cut_t * pCut;
608  int Scores[16], uScores, i, k, j, nCuts = 0;
609  abctime clk;
610 
611  // simulate the AIG
612 clk = Abc_Clock();
613 // srand( 0xAABBAABB );
614  Aig_ManRandom(1);
615  pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames, 1 );
616  if ( p->fTarget && pSeq->fNonConstOut )
617  {
618  printf( "Property failed after sequential simulation!\n" );
619  Fra_SmlStop( pSeq );
620  return 0;
621  }
622 if ( p->fVerbose )
623 {
624 ABC_PRT( "Sim-seq", Abc_Clock() - clk );
625 }
626 
627 
628 clk = Abc_Clock();
629  if ( fRefs )
630  {
631  Fra_ClausCollectLatchClauses( p, pSeq );
632 if ( p->fVerbose )
633 {
634 ABC_PRT( "Lat-cla", Abc_Clock() - clk );
635 }
636  }
637 
638 
639  // generate cuts for all nodes, assign cost, and find best cuts
640 clk = Abc_Clock();
641  pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 0, 1 );
642 // pManCut = Aig_ComputeCuts( p->pAig, 10, 4, 0, 1 );
643 if ( p->fVerbose )
644 {
645 ABC_PRT( "Cuts ", Abc_Clock() - clk );
646 }
647 
648  // collect sequential info for each cut
649 clk = Abc_Clock();
650  Aig_ManForEachNode( p->pAig, pObj, i )
651  Dar_ObjForEachCut( pObj, pCut, k )
652  if ( pCut->nLeaves > 1 )
653  {
654  pCut->uTruth = Fra_ClausProcessClausesCut( p, pSeq, pCut, Scores );
655 // uScores = Fra_ClausProcessClausesCut2( p, pSeq, pCut, Scores );
656 // if ( uScores != pCut->uTruth )
657 // {
658 // int x = 0;
659 // }
660  }
661 if ( p->fVerbose )
662 {
663 ABC_PRT( "Infoseq", Abc_Clock() - clk );
664 }
665  Fra_SmlStop( pSeq );
666 
667  // perform combinational simulation
668 clk = Abc_Clock();
669 // srand( 0xAABBAABB );
670  Aig_ManRandom(1);
671  pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref, 0 );
672 if ( p->fVerbose )
673 {
674 ABC_PRT( "Sim-cmb", Abc_Clock() - clk );
675 }
676 
677  // collect combinational info for each cut
678 clk = Abc_Clock();
679  Aig_ManForEachNode( p->pAig, pObj, i )
680  Dar_ObjForEachCut( pObj, pCut, k )
681  if ( pCut->nLeaves > 1 )
682  {
683  nCuts++;
684  uScores = Fra_ClausProcessClausesCut( p, pComb, pCut, Scores );
685  uScores &= ~pCut->uTruth; pCut->uTruth = 0;
686  if ( uScores == 0 )
687  continue;
688  // write the clauses
689  for ( j = 0; j < (1<<pCut->nLeaves); j++ )
690  if ( uScores & (1 << j) )
691  Fra_ClausRecordClause( p, pCut, j, Scores[j] );
692 
693  }
694  Fra_SmlStop( pComb );
695  Aig_MmFixedStop( pMemCuts, 0 );
696 // Aig_ManCutStop( pManCut );
697 if ( p->fVerbose )
698 {
699 ABC_PRT( "Infocmb", Abc_Clock() - clk );
700 }
701 
702  if ( p->fVerbose )
703  printf( "Node = %5d. Non-triv cuts = %7d. Clauses = %6d. Clause per cut = %6.2f.\n",
704  Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
705 
706  if ( Vec_IntSize(p->vClauses) > p->nClausesMax )
707  Fra_ClausSelectClauses( p );
708  else
709  p->nClauses = Vec_IntSize( p->vClauses );
710  return 1;
711 }
712 
713 /**Function*************************************************************
714 
715  Synopsis [Processes the clauses.]
716 
717  Description []
718 
719  SideEffects []
720 
721  SeeAlso []
722 
723 ***********************************************************************/
724 int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs )
725 {
726 // Aig_MmFixed_t * pMemCuts;
727  Aig_ManCut_t * pManCut;
728  Fra_Sml_t * pComb, * pSeq;
729  Aig_Obj_t * pObj;
730  Aig_Cut_t * pCut;
731  int i, k, j, nCuts = 0;
732  abctime clk;
733  int ScoresSeq[1<<12], ScoresComb[1<<12];
734  assert( p->nLutSize < 13 );
735 
736  // simulate the AIG
737 clk = Abc_Clock();
738 // srand( 0xAABBAABB );
739  Aig_ManRandom(1);
740  pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames, 1 );
741  if ( p->fTarget && pSeq->fNonConstOut )
742  {
743  printf( "Property failed after sequential simulation!\n" );
744  Fra_SmlStop( pSeq );
745  return 0;
746  }
747 if ( p->fVerbose )
748 {
749 //ABC_PRT( "Sim-seq", Abc_Clock() - clk );
750 }
751 
752  // perform combinational simulation
753 clk = Abc_Clock();
754 // srand( 0xAABBAABB );
755  Aig_ManRandom(1);
756  pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref, 0 );
757 if ( p->fVerbose )
758 {
759 //ABC_PRT( "Sim-cmb", Abc_Clock() - clk );
760 }
761 
762 
763 clk = Abc_Clock();
764  if ( fRefs )
765  {
766  Fra_ClausCollectLatchClauses( p, pSeq );
767 if ( p->fVerbose )
768 {
769 //ABC_PRT( "Lat-cla", Abc_Clock() - clk );
770 }
771  }
772 
773 
774  // generate cuts for all nodes, assign cost, and find best cuts
775 clk = Abc_Clock();
776 // pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 0, 1 );
777  pManCut = Aig_ComputeCuts( p->pAig, p->nCutsMax, p->nLutSize, 0, p->fVerbose );
778 if ( p->fVerbose )
779 {
780 //ABC_PRT( "Cuts ", Abc_Clock() - clk );
781 }
782 
783  // collect combinational info for each cut
784 clk = Abc_Clock();
785  Aig_ManForEachNode( p->pAig, pObj, i )
786  {
787  if ( pObj->Level > (unsigned)p->nLevels )
788  continue;
789  Aig_ObjForEachCut( pManCut, pObj, pCut, k )
790  if ( pCut->nFanins > 1 )
791  {
792  nCuts++;
793  Fra_ClausProcessClausesCut3( p, pSeq, pCut, ScoresSeq );
794  Fra_ClausProcessClausesCut3( p, pComb, pCut, ScoresComb );
795  // write the clauses
796  for ( j = 0; j < (1<<pCut->nFanins); j++ )
797  if ( ScoresComb[j] != 0 && ScoresSeq[j] == 0 )
798  Fra_ClausRecordClause2( p, pCut, j, ScoresComb[j] );
799 
800  }
801  }
802  Fra_SmlStop( pSeq );
803  Fra_SmlStop( pComb );
804  p->nCuts = nCuts;
805 // Aig_MmFixedStop( pMemCuts, 0 );
806  Aig_ManCutStop( pManCut );
807  p->pAig->pManCuts = NULL;
808 
809  if ( p->fVerbose )
810  {
811  printf( "Node = %5d. Cuts = %7d. Clauses = %6d. Clause/cut = %6.2f.\n",
812  Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
813  ABC_PRT( "Processing sim-info to find candidate clauses (unoptimized)", Abc_Clock() - clk );
814  }
815 
816  // filter out clauses that are contained in the already proven clauses
817  assert( p->nClauses == 0 );
818  p->nClauses = Vec_IntSize( p->vClauses );
819  if ( Vec_IntSize( p->vClausesProven ) > 0 )
820  {
821  int RetValue, k, Beg;
822  int End = -1; // Suppress "might be used uninitialized"
823  int * pStart;
824  // reset the solver
825  if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
826  p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
827  if ( p->pSatMain == NULL )
828  {
829  printf( "Error: Main solver is unsat.\n" );
830  return -1;
831  }
832 
833  // add the proven clauses
834  Beg = 0;
835  pStart = Vec_IntArray(p->vLitsProven);
836  Vec_IntForEachEntry( p->vClausesProven, End, i )
837  {
838  assert( End - Beg <= p->nLutSize );
839  // add the clause to all timeframes
840  RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
841  if ( RetValue == 0 )
842  {
843  printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
844  return -1;
845  }
846  Beg = End;
847  }
848  assert( End == Vec_IntSize(p->vLitsProven) );
849 
850  // check the clauses
851  Beg = 0;
852  pStart = Vec_IntArray(p->vLits);
853  Vec_IntForEachEntry( p->vClauses, End, i )
854  {
855  assert( Vec_IntEntry( p->vCosts, i ) >= 0 );
856  assert( End - Beg <= p->nLutSize );
857  // check the clause
858  for ( k = Beg; k < End; k++ )
859  pStart[k] = lit_neg( pStart[k] );
860  RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
861  for ( k = Beg; k < End; k++ )
862  pStart[k] = lit_neg( pStart[k] );
863  // the clause holds
864  if ( RetValue == l_False )
865  {
866  Vec_IntWriteEntry( p->vCosts, i, -1 );
867  p->nClauses--;
868  }
869  Beg = End;
870  }
871  assert( End == Vec_IntSize(p->vLits) );
872  if ( p->fVerbose )
873  printf( "Already proved clauses filtered out %d candidate clauses (out of %d).\n",
874  Vec_IntSize(p->vClauses) - p->nClauses, Vec_IntSize(p->vClauses) );
875  }
876 
877  p->fFiltering = 0;
878  if ( p->nClauses > p->nClausesMax )
879  {
880  Fra_ClausSelectClauses( p );
881  p->fFiltering = 1;
882  }
883  return 1;
884 }
885 
886 /**Function*************************************************************
887 
888  Synopsis [Converts AIG into the SAT solver.]
889 
890  Description []
891 
892  SideEffects []
893 
894  SeeAlso []
895 
896 ***********************************************************************/
897 int Fra_ClausBmcClauses( Clu_Man_t * p )
898 {
899  int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f;
900 /*
901  for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
902  printf( "%d ", p->vLits->pArray[i] );
903  printf( "\n" );
904 */
905  // add the clauses
906  Counter = 0;
907  // skip through the prefix variables
908  if ( p->nPref )
909  {
910  nLitsTot = p->nPref * 2 * p->pCnf->nVars;
911  for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
912  p->vLits->pArray[i] += nLitsTot;
913  }
914  // go through the timeframes
915  nLitsTot = 2 * p->pCnf->nVars;
916  pStart = Vec_IntArray(p->vLits);
917  for ( f = 0; f < p->nFrames; f++ )
918  {
919  Beg = 0;
920  Vec_IntForEachEntry( p->vClauses, End, i )
921  {
922  if ( Vec_IntEntry( p->vCosts, i ) == -1 )
923  {
924  Beg = End;
925  continue;
926  }
927  assert( Vec_IntEntry( p->vCosts, i ) > 0 );
928  assert( End - Beg <= p->nLutSize );
929 
930  for ( k = Beg; k < End; k++ )
931  pStart[k] = lit_neg( pStart[k] );
932  RetValue = sat_solver_solve( p->pSatBmc, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
933  for ( k = Beg; k < End; k++ )
934  pStart[k] = lit_neg( pStart[k] );
935 
936  if ( RetValue != l_False )
937  {
938  Beg = End;
939  Vec_IntWriteEntry( p->vCosts, i, -1 );
940  Counter++;
941  continue;
942  }
943 /*
944  // add the clause
945  RetValue = sat_solver_addclause( p->pSatBmc, pStart + Beg, pStart + End );
946  // assert( RetValue == 1 );
947  if ( RetValue == 0 )
948  {
949  printf( "Error: Solver is UNSAT after adding BMC clauses.\n" );
950  return -1;
951  }
952 */
953  Beg = End;
954 
955  // simplify the solver
956  if ( p->pSatBmc->qtail != p->pSatBmc->qhead )
957  {
958  RetValue = sat_solver_simplify(p->pSatBmc);
959  assert( RetValue != 0 );
960  assert( p->pSatBmc->qtail == p->pSatBmc->qhead );
961  }
962  }
963  // increment literals
964  for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
965  p->vLits->pArray[i] += nLitsTot;
966  }
967 
968  // return clauses back to normal
969  nLitsTot = (p->nPref + p->nFrames) * nLitsTot;
970  for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
971  p->vLits->pArray[i] -= nLitsTot;
972 /*
973  for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
974  printf( "%d ", p->vLits->pArray[i] );
975  printf( "\n" );
976 */
977  return Counter;
978 }
979 
980 /**Function*************************************************************
981 
982  Synopsis [Cleans simulation info.]
983 
984  Description []
985 
986  SideEffects []
987 
988  SeeAlso []
989 
990 ***********************************************************************/
991 void Fra_ClausSimInfoClean( Clu_Man_t * p )
992 {
993  assert( p->pCnf->nVars <= Vec_PtrSize(p->vCexes) );
994  Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 );
995  p->nCexes = 0;
996 }
997 
998 /**Function*************************************************************
999 
1000  Synopsis [Reallocs simulation info.]
1001 
1002  Description []
1003 
1004  SideEffects []
1005 
1006  SeeAlso []
1007 
1008 ***********************************************************************/
1009 void Fra_ClausSimInfoRealloc( Clu_Man_t * p )
1010 {
1011  assert( p->nCexes == p->nCexesAlloc );
1012  Vec_PtrReallocSimInfo( p->vCexes );
1013  Vec_PtrCleanSimInfo( p->vCexes, p->nCexesAlloc/32, 2 * p->nCexesAlloc/32 );
1014  p->nCexesAlloc *= 2;
1015 }
1016 
1017 /**Function*************************************************************
1018 
1019  Synopsis [Records simulation info.]
1020 
1021  Description []
1022 
1023  SideEffects []
1024 
1025  SeeAlso []
1026 
1027 ***********************************************************************/
1028 void Fra_ClausSimInfoRecord( Clu_Man_t * p, int * pModel )
1029 {
1030  int i;
1031  if ( p->nCexes == p->nCexesAlloc )
1032  Fra_ClausSimInfoRealloc( p );
1033  assert( p->nCexes < p->nCexesAlloc );
1034  for ( i = 0; i < p->pCnf->nVars; i++ )
1035  {
1036  if ( pModel[i] == l_True )
1037  {
1038  assert( Abc_InfoHasBit( (unsigned *)Vec_PtrEntry(p->vCexes, i), p->nCexes ) == 0 );
1039  Abc_InfoSetBit( (unsigned *)Vec_PtrEntry(p->vCexes, i), p->nCexes );
1040  }
1041  }
1042  p->nCexes++;
1043 }
1044 
1045 /**Function*************************************************************
1046 
1047  Synopsis [Uses the simulation info.]
1048 
1049  Description [Returns 1 if the simulation info disproved the clause.]
1050 
1051  SideEffects []
1052 
1053  SeeAlso []
1054 
1055 ***********************************************************************/
1056 int Fra_ClausSimInfoCheck( Clu_Man_t * p, int * pLits, int nLits )
1057 {
1058  unsigned * pSims[16], uWord;
1059  int nWords, iVar, i, w;
1060  for ( i = 0; i < nLits; i++ )
1061  {
1062  iVar = lit_var(pLits[i]) - p->nFrames * p->pCnf->nVars;
1063  assert( iVar > 0 && iVar < p->pCnf->nVars );
1064  pSims[i] = (unsigned *)Vec_PtrEntry( p->vCexes, iVar );
1065  }
1066  nWords = p->nCexes / 32;
1067  for ( w = 0; w < nWords; w++ )
1068  {
1069  uWord = ~(unsigned)0;
1070  for ( i = 0; i < nLits; i++ )
1071  uWord &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
1072  if ( uWord )
1073  return 1;
1074  }
1075  if ( p->nCexes % 32 )
1076  {
1077  uWord = ~(unsigned)0;
1078  for ( i = 0; i < nLits; i++ )
1079  uWord &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
1080  if ( uWord & Abc_InfoMask( p->nCexes % 32 ) )
1081  return 1;
1082  }
1083  return 0;
1084 }
1085 
1086 
1087 /**Function*************************************************************
1088 
1089  Synopsis [Converts AIG into the SAT solver.]
1090 
1091  Description []
1092 
1093  SideEffects []
1094 
1095  SeeAlso []
1096 
1097 ***********************************************************************/
1098 int Fra_ClausInductiveClauses( Clu_Man_t * p )
1099 {
1100 // Aig_Obj_t * pObjLi, * pObjLo;
1101  int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f, fFlag;//, Lits[2];
1102  p->fFail = 0;
1103 
1104  // reset the solver
1105  if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
1106  p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
1107  if ( p->pSatMain == NULL )
1108  {
1109  printf( "Error: Main solver is unsat.\n" );
1110  return -1;
1111  }
1112  Fra_ClausSimInfoClean( p );
1113 
1114 /*
1115  // check if the property holds
1116  if ( Fra_ClausRunSat0( p ) )
1117  printf( "Property holds without strengthening.\n" );
1118  else
1119  printf( "Property does not hold without strengthening.\n" );
1120 */
1121 /*
1122  // add constant registers
1123  Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
1124  if ( Aig_ObjFanin0(pObjLi) == Aig_ManConst1(p->pAig) )
1125  {
1126  for ( k = 0; k < p->nFrames; k++ )
1127  {
1128  Lits[0] = k * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObjLo->Id], Aig_ObjFaninC0(pObjLi) );
1129  RetValue = sat_solver_addclause( p->pSatMain, Lits, Lits + 1 );
1130  if ( RetValue == 0 )
1131  {
1132  printf( "Error: Solver is UNSAT after adding constant-register clauses.\n" );
1133  return -1;
1134  }
1135  }
1136  }
1137 */
1138 
1139 
1140  // add the proven clauses
1141  nLitsTot = 2 * p->pCnf->nVars;
1142  pStart = Vec_IntArray(p->vLitsProven);
1143  for ( f = 0; f < p->nFrames; f++ )
1144  {
1145  Beg = 0;
1146  Vec_IntForEachEntry( p->vClausesProven, End, i )
1147  {
1148  assert( End - Beg <= p->nLutSize );
1149  // add the clause to all timeframes
1150  RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
1151  if ( RetValue == 0 )
1152  {
1153  printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
1154  return -1;
1155  }
1156  Beg = End;
1157  }
1158  // increment literals
1159  for ( i = 0; i < Vec_IntSize(p->vLitsProven); i++ )
1160  p->vLitsProven->pArray[i] += nLitsTot;
1161  }
1162  // return clauses back to normal
1163  nLitsTot = (p->nFrames) * nLitsTot;
1164  for ( i = 0; i < Vec_IntSize(p->vLitsProven); i++ )
1165  p->vLitsProven->pArray[i] -= nLitsTot;
1166 
1167 /*
1168  // add the proven clauses
1169  nLitsTot = 2 * p->pCnf->nVars;
1170  pStart = Vec_IntArray(p->vLitsProven);
1171  Beg = 0;
1172  Vec_IntForEachEntry( p->vClausesProven, End, i )
1173  {
1174  assert( End - Beg <= p->nLutSize );
1175  // add the clause to all timeframes
1176  RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
1177  if ( RetValue == 0 )
1178  {
1179  printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
1180  return -1;
1181  }
1182  Beg = End;
1183  }
1184 */
1185 
1186  // add the clauses
1187  nLitsTot = 2 * p->pCnf->nVars;
1188  pStart = Vec_IntArray(p->vLits);
1189  for ( f = 0; f < p->nFrames; f++ )
1190  {
1191  Beg = 0;
1192  Vec_IntForEachEntry( p->vClauses, End, i )
1193  {
1194  if ( Vec_IntEntry( p->vCosts, i ) == -1 )
1195  {
1196  Beg = End;
1197  continue;
1198  }
1199  assert( Vec_IntEntry( p->vCosts, i ) > 0 );
1200  assert( End - Beg <= p->nLutSize );
1201  // add the clause to all timeframes
1202  RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
1203  if ( RetValue == 0 )
1204  {
1205  printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
1206  return -1;
1207  }
1208  Beg = End;
1209  }
1210  // increment literals
1211  for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
1212  p->vLits->pArray[i] += nLitsTot;
1213  }
1214 
1215  // simplify the solver
1216  if ( p->pSatMain->qtail != p->pSatMain->qhead )
1217  {
1218  RetValue = sat_solver_simplify(p->pSatMain);
1219  assert( RetValue != 0 );
1220  assert( p->pSatMain->qtail == p->pSatMain->qhead );
1221  }
1222 
1223  // check if the property holds
1224  if ( p->fTarget )
1225  {
1226  if ( Fra_ClausRunSat0( p ) )
1227  {
1228  if ( p->fVerbose )
1229  printf( " Property holds. " );
1230  }
1231  else
1232  {
1233  if ( p->fVerbose )
1234  printf( " Property fails. " );
1235  // return -2;
1236  p->fFail = 1;
1237  }
1238  }
1239 
1240 /*
1241  // add the property for the first K frames
1242  for ( i = 0; i < p->nFrames; i++ )
1243  {
1244  Aig_Obj_t * pObj;
1245  int Lits[2];
1246  // set the output literals
1247  pObj = Aig_ManCo(p->pAig, 0);
1248  Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 1 );
1249  // add the clause
1250  RetValue = sat_solver_addclause( p->pSatMain, Lits, Lits + 1 );
1251 // assert( RetValue == 1 );
1252  if ( RetValue == 0 )
1253  {
1254  printf( "Error: Solver is UNSAT after adding property for the first K frames.\n" );
1255  return -1;
1256  }
1257  }
1258 */
1259 
1260  // simplify the solver
1261  if ( p->pSatMain->qtail != p->pSatMain->qhead )
1262  {
1263  RetValue = sat_solver_simplify(p->pSatMain);
1264  assert( RetValue != 0 );
1265  assert( p->pSatMain->qtail == p->pSatMain->qhead );
1266  }
1267 
1268 
1269  // check the clause in the last timeframe
1270  Beg = 0;
1271  Counter = 0;
1272  Vec_IntForEachEntry( p->vClauses, End, i )
1273  {
1274  if ( Vec_IntEntry( p->vCosts, i ) == -1 )
1275  {
1276  Beg = End;
1277  continue;
1278  }
1279  assert( Vec_IntEntry( p->vCosts, i ) > 0 );
1280  assert( End - Beg <= p->nLutSize );
1281 
1282  if ( Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg) )
1283  {
1284  fFlag = 1;
1285 // printf( "s-" );
1286 
1287  Beg = End;
1288  Vec_IntWriteEntry( p->vCosts, i, -1 );
1289  Counter++;
1290  continue;
1291  }
1292  else
1293  {
1294  fFlag = 0;
1295 // printf( "s?" );
1296  }
1297 
1298  for ( k = Beg; k < End; k++ )
1299  pStart[k] = lit_neg( pStart[k] );
1300  RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1301  for ( k = Beg; k < End; k++ )
1302  pStart[k] = lit_neg( pStart[k] );
1303 
1304  // the problem is not solved
1305  if ( RetValue != l_False )
1306  {
1307 // printf( "S- " );
1308 // Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model.ptr + p->nFrames * p->pCnf->nVars );
1309  Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model + p->nFrames * p->pCnf->nVars );
1310 // RetValue = Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg);
1311 // assert( RetValue );
1312 
1313  Beg = End;
1314  Vec_IntWriteEntry( p->vCosts, i, -1 );
1315  Counter++;
1316  continue;
1317  }
1318 // printf( "S+ " );
1319 // assert( !fFlag );
1320 
1321 /*
1322  // add the clause
1323  RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
1324 // assert( RetValue == 1 );
1325  if ( RetValue == 0 )
1326  {
1327  printf( "Error: Solver is UNSAT after adding proved clauses.\n" );
1328  return -1;
1329  }
1330 */
1331  Beg = End;
1332 
1333  // simplify the solver
1334  if ( p->pSatMain->qtail != p->pSatMain->qhead )
1335  {
1336  RetValue = sat_solver_simplify(p->pSatMain);
1337  assert( RetValue != 0 );
1338  assert( p->pSatMain->qtail == p->pSatMain->qhead );
1339  }
1340  }
1341 
1342  // return clauses back to normal
1343  nLitsTot = p->nFrames * nLitsTot;
1344  for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
1345  p->vLits->pArray[i] -= nLitsTot;
1346 
1347 // if ( fFail )
1348 // return -2;
1349  return Counter;
1350 }
1351 
1352 
1353 
1354 /**Function*************************************************************
1355 
1356  Synopsis [Converts AIG into the SAT solver.]
1357 
1358  Description []
1359 
1360  SideEffects []
1361 
1362  SeeAlso []
1363 
1364 ***********************************************************************/
1365 Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fTarget, int fVerbose, int fVeryVerbose )
1366 {
1367  Clu_Man_t * p;
1368  p = ABC_ALLOC( Clu_Man_t, 1 );
1369  memset( p, 0, sizeof(Clu_Man_t) );
1370  p->pAig = pAig;
1371  p->nFrames = nFrames;
1372  p->nPref = nPref;
1373  p->nClausesMax = nClausesMax;
1374  p->nLutSize = nLutSize;
1375  p->nLevels = nLevels;
1376  p->nCutsMax = nCutsMax;
1377  p->nBatches = nBatches;
1378  p->fStepUp = fStepUp;
1379  p->fTarget = fTarget;
1380  p->fVerbose = fVerbose;
1381  p->fVeryVerbose = fVeryVerbose;
1382  p->nSimWords = 512;//1024;//64;
1383  p->nSimFrames = 32;//8;//32;
1384  p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
1385 
1386  p->vLits = Vec_IntAlloc( 1<<14 );
1387  p->vClauses = Vec_IntAlloc( 1<<12 );
1388  p->vCosts = Vec_IntAlloc( 1<<12 );
1389 
1390  p->vLitsProven = Vec_IntAlloc( 1<<14 );
1391  p->vClausesProven= Vec_IntAlloc( 1<<12 );
1392 
1393  p->nCexesAlloc = 1024;
1394  p->vCexes = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pAig)+1, p->nCexesAlloc/32 );
1395  Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 );
1396  return p;
1397 }
1398 
1399 /**Function*************************************************************
1400 
1401  Synopsis [Converts AIG into the SAT solver.]
1402 
1403  Description []
1404 
1405  SideEffects []
1406 
1407  SeeAlso []
1408 
1409 ***********************************************************************/
1410 void Fra_ClausFree( Clu_Man_t * p )
1411 {
1412  if ( p->vCexes ) Vec_PtrFree( p->vCexes );
1413  if ( p->vLits ) Vec_IntFree( p->vLits );
1414  if ( p->vClauses ) Vec_IntFree( p->vClauses );
1415  if ( p->vLitsProven ) Vec_IntFree( p->vLitsProven );
1416  if ( p->vClausesProven ) Vec_IntFree( p->vClausesProven );
1417  if ( p->vCosts ) Vec_IntFree( p->vCosts );
1418  if ( p->pCnf ) Cnf_DataFree( p->pCnf );
1419  if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
1420  if ( p->pSatBmc ) sat_solver_delete( p->pSatBmc );
1421  ABC_FREE( p );
1422 }
1423 
1424 
1425 /**Function*************************************************************
1426 
1427  Synopsis [Converts AIG into the SAT solver.]
1428 
1429  Description []
1430 
1431  SideEffects []
1432 
1433  SeeAlso []
1434 
1435 ***********************************************************************/
1436 void Fra_ClausAddToStorage( Clu_Man_t * p )
1437 {
1438  int * pStart;
1439  int Beg, End, Counter, i, k;
1440  Beg = 0;
1441  Counter = 0;
1442  pStart = Vec_IntArray( p->vLits );
1443  Vec_IntForEachEntry( p->vClauses, End, i )
1444  {
1445  if ( Vec_IntEntry( p->vCosts, i ) == -1 )
1446  {
1447  Beg = End;
1448  continue;
1449  }
1450  assert( Vec_IntEntry( p->vCosts, i ) > 0 );
1451  assert( End - Beg <= p->nLutSize );
1452  for ( k = Beg; k < End; k++ )
1453  Vec_IntPush( p->vLitsProven, pStart[k] );
1454  Vec_IntPush( p->vClausesProven, Vec_IntSize(p->vLitsProven) );
1455  Beg = End;
1456  Counter++;
1457 
1458  if ( i < p->nOneHots )
1459  p->nOneHotsProven++;
1460  }
1461  if ( p->fVerbose )
1462  printf( "Added to storage %d proved clauses (including %d one-hot clauses)\n", Counter, p->nOneHotsProven );
1463 
1464  Vec_IntClear( p->vClauses );
1465  Vec_IntClear( p->vLits );
1466  Vec_IntClear( p->vCosts );
1467  p->nClauses = 0;
1468 
1469  p->fNothingNew = (int)(Counter == 0);
1470 }
1471 
1472 /**Function*************************************************************
1473 
1474  Synopsis [Converts AIG into the SAT solver.]
1475 
1476  Description []
1477 
1478  SideEffects []
1479 
1480  SeeAlso []
1481 
1482 ***********************************************************************/
1483 void Fra_ClausPrintIndClauses( Clu_Man_t * p )
1484 {
1485  int Counters[9] = {0};
1486  int * pStart;
1487  int Beg, End, i;
1488  Beg = 0;
1489  pStart = Vec_IntArray( p->vLitsProven );
1490  Vec_IntForEachEntry( p->vClausesProven, End, i )
1491  {
1492  if ( End - Beg >= 8 )
1493  Counters[8]++;
1494  else
1495  Counters[End - Beg]++;
1496 //printf( "%d ", End-Beg );
1497  Beg = End;
1498  }
1499  printf( "SUMMARY: Total proved clauses = %d. ", Vec_IntSize(p->vClausesProven) );
1500  printf( "Clause per lit: " );
1501  for ( i = 0; i < 8; i++ )
1502  if ( Counters[i] )
1503  printf( "%d=%d ", i, Counters[i] );
1504  if ( Counters[8] )
1505  printf( ">7=%d ", Counters[8] );
1506  printf( "\n" );
1507 }
1508 
1509 /**Function*************************************************************
1510 
1511  Synopsis [Writes the clauses into an AIGER file.]
1512 
1513  Description []
1514 
1515  SideEffects []
1516 
1517  SeeAlso []
1518 
1519 ***********************************************************************/
1520 Aig_Obj_t * Fra_ClausGetLiteral( Clu_Man_t * p, int * pVar2Id, int Lit )
1521 {
1522  Aig_Obj_t * pLiteral;
1523  int NodeId = pVar2Id[ lit_var(Lit) ];
1524  assert( NodeId >= 0 );
1525  pLiteral = (Aig_Obj_t *)Aig_ManObj( p->pAig, NodeId )->pData;
1526  return Aig_NotCond( pLiteral, lit_sign(Lit) );
1527 }
1528 
1529 /**Function*************************************************************
1530 
1531  Synopsis [Writes the clauses into an AIGER file.]
1532 
1533  Description []
1534 
1535  SideEffects []
1536 
1537  SeeAlso []
1538 
1539 ***********************************************************************/
1540 void Fra_ClausWriteIndClauses( Clu_Man_t * p )
1541 {
1542  extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
1543  Aig_Man_t * pNew;
1544  Aig_Obj_t * pClause, * pLiteral;
1545  char * pName;
1546  int * pStart, * pVar2Id;
1547  int Beg, End, i, k;
1548  // create mapping from SAT vars to node IDs
1549  pVar2Id = ABC_ALLOC( int, p->pCnf->nVars );
1550  memset( pVar2Id, 0xFF, sizeof(int) * p->pCnf->nVars );
1551  for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
1552  if ( p->pCnf->pVarNums[i] >= 0 )
1553  {
1554  assert( p->pCnf->pVarNums[i] < p->pCnf->nVars );
1555  pVar2Id[ p->pCnf->pVarNums[i] ] = i;
1556  }
1557  // start the manager
1558  pNew = Aig_ManDupWithoutPos( p->pAig );
1559  // add the clauses
1560  Beg = 0;
1561  pStart = Vec_IntArray( p->vLitsProven );
1562  Vec_IntForEachEntry( p->vClausesProven, End, i )
1563  {
1564  pClause = Fra_ClausGetLiteral( p, pVar2Id, pStart[Beg] );
1565  for ( k = Beg + 1; k < End; k++ )
1566  {
1567  pLiteral = Fra_ClausGetLiteral( p, pVar2Id, pStart[k] );
1568  pClause = Aig_Or( pNew, pClause, pLiteral );
1569  }
1570  Aig_ObjCreateCo( pNew, pClause );
1571  Beg = End;
1572  }
1573  ABC_FREE( pVar2Id );
1574  Aig_ManCleanup( pNew );
1575  pName = Ioa_FileNameGenericAppend( p->pAig->pName, "_care.aig" );
1576  printf( "Care one-hotness clauses will be written into file \"%s\".\n", pName );
1577  Ioa_WriteAiger( pNew, pName, 0, 1 );
1578  Aig_ManStop( pNew );
1579 }
1580 
1581 /**Function*************************************************************
1582 
1583  Synopsis [Checks if the clause holds using the given simulation info.]
1584 
1585  Description []
1586 
1587  SideEffects []
1588 
1589  SeeAlso []
1590 
1591 ***********************************************************************/
1592 void Fra_ClausEstimateCoverageOne( Fra_Sml_t * pSim, int * pLits, int nLits, int * pVar2Id, unsigned * pResult )
1593 {
1594  unsigned * pSims[16];
1595  int iVar, i, w;
1596  for ( i = 0; i < nLits; i++ )
1597  {
1598  iVar = lit_var(pLits[i]);
1599  pSims[i] = Fra_ObjSim( pSim, pVar2Id[iVar] );
1600  }
1601  for ( w = 0; w < pSim->nWordsTotal; w++ )
1602  {
1603  pResult[w] = ~(unsigned)0;
1604  for ( i = 0; i < nLits; i++ )
1605  pResult[w] &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
1606  }
1607 }
1608 
1609 /**Function*************************************************************
1610 
1611  Synopsis [Estimates the coverage of state space by clauses.]
1612 
1613  Description []
1614 
1615  SideEffects []
1616 
1617  SeeAlso []
1618 
1619 ***********************************************************************/
1620 void Fra_ClausEstimateCoverage( Clu_Man_t * p )
1621 {
1622  int nCombSimWords = (1<<11);
1623  Fra_Sml_t * pComb;
1624  unsigned * pResultTot, * pResultOne;
1625  int nCovered, Beg, End, i, w;
1626  int * pStart, * pVar2Id;
1627  abctime clk = Abc_Clock();
1628  // simulate the circuit with nCombSimWords * 32 = 64K patterns
1629 // srand( 0xAABBAABB );
1630  Aig_ManRandom(1);
1631  pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords, 0 );
1632  // create mapping from SAT vars to node IDs
1633  pVar2Id = ABC_ALLOC( int, p->pCnf->nVars );
1634  memset( pVar2Id, 0, sizeof(int) * p->pCnf->nVars );
1635  for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
1636  if ( p->pCnf->pVarNums[i] >= 0 )
1637  {
1638  assert( p->pCnf->pVarNums[i] < p->pCnf->nVars );
1639  pVar2Id[ p->pCnf->pVarNums[i] ] = i;
1640  }
1641  // get storage for one assignment and all assignments
1642  assert( Aig_ManCoNum(p->pAig) > 2 );
1643  pResultOne = Fra_ObjSim( pComb, Aig_ManCo(p->pAig, 0)->Id );
1644  pResultTot = Fra_ObjSim( pComb, Aig_ManCo(p->pAig, 1)->Id );
1645  // start the OR of don't-cares
1646  for ( w = 0; w < nCombSimWords; w++ )
1647  pResultTot[w] = 0;
1648  // check clauses
1649  Beg = 0;
1650  pStart = Vec_IntArray( p->vLitsProven );
1651  Vec_IntForEachEntry( p->vClausesProven, End, i )
1652  {
1653  Fra_ClausEstimateCoverageOne( pComb, pStart + Beg, End-Beg, pVar2Id, pResultOne );
1654  Beg = End;
1655  for ( w = 0; w < nCombSimWords; w++ )
1656  pResultTot[w] |= pResultOne[w];
1657  }
1658  // count the total number of patterns contained in the don't-care
1659  nCovered = 0;
1660  for ( w = 0; w < nCombSimWords; w++ )
1661  nCovered += Aig_WordCountOnes( pResultTot[w] );
1662  Fra_SmlStop( pComb );
1663  ABC_FREE( pVar2Id );
1664  // print the result
1665  printf( "Care states ratio = %f. ", 1.0 * (nCombSimWords * 32 - nCovered) / (nCombSimWords * 32) );
1666  printf( "(%d out of %d patterns) ", nCombSimWords * 32 - nCovered, nCombSimWords * 32 );
1667  ABC_PRT( "Time", Abc_Clock() - clk );
1668 }
1669 
1670 
1671 /**Function*************************************************************
1672 
1673  Synopsis [Converts AIG into the SAT solver.]
1674 
1675  Description []
1676 
1677  SideEffects []
1678 
1679  SeeAlso []
1680 
1681 ***********************************************************************/
1682 int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose )
1683 {
1684  Clu_Man_t * p;
1685  abctime clk, clkTotal = Abc_Clock(), clkInd;
1686  int b, Iter, Counter, nPrefOld;
1687  int nClausesBeg = 0;
1688 
1689  // create the manager
1690  p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fTarget, fVerbose, fVeryVerbose );
1691 if ( p->fVerbose )
1692 {
1693  printf( "PARAMETERS: Frames = %d. Pref = %d. Clauses max = %d. Cut size = %d.\n", nFrames, nPref, nClausesMax, nLutSize );
1694  printf( "Level max = %d. Cuts max = %d. Batches = %d. Increment cut size = %s.\n", nLevels, nCutsMax, nBatches, fStepUp? "yes":"no" );
1695 //ABC_PRT( "Sim-seq", Abc_Clock() - clk );
1696 }
1697 
1698  assert( !p->fTarget || Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
1699 
1700 clk = Abc_Clock();
1701  // derive CNF
1702 // if ( p->fTarget )
1703 // p->pAig->nRegs++;
1704  p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManCoNum(p->pAig) );
1705 // if ( p->fTarget )
1706 // p->pAig->nRegs--;
1707 if ( fVerbose )
1708 {
1709 //ABC_PRT( "CNF ", Abc_Clock() - clk );
1710 }
1711 
1712  // check BMC
1713 clk = Abc_Clock();
1714  p->pSatBmc = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nPref + p->nFrames, 1 );
1715  if ( p->pSatBmc == NULL )
1716  {
1717  printf( "Error: BMC solver is unsat.\n" );
1718  Fra_ClausFree( p );
1719  return 1;
1720  }
1721  if ( p->fTarget && !Fra_ClausRunBmc( p ) )
1722  {
1723  printf( "Problem fails the base case after %d frame expansion.\n", p->nPref + p->nFrames );
1724  Fra_ClausFree( p );
1725  return 1;
1726  }
1727 if ( fVerbose )
1728 {
1729 //ABC_PRT( "SAT-bmc", Abc_Clock() - clk );
1730 }
1731 
1732  // start the SAT solver
1733 clk = Abc_Clock();
1734  p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
1735  if ( p->pSatMain == NULL )
1736  {
1737  printf( "Error: Main solver is unsat.\n" );
1738  Fra_ClausFree( p );
1739  return 1;
1740  }
1741 
1742 
1743  for ( b = 0; b < p->nBatches; b++ )
1744  {
1745 // if ( fVerbose )
1746  printf( "*** BATCH %d: ", b+1 );
1747  if ( b && p->nLutSize < 12 && (!p->fFiltering || p->fNothingNew || p->fStepUp) )
1748  p->nLutSize++;
1749  printf( "Using %d-cuts.\n", p->nLutSize );
1750 
1751  // try solving without additional clauses
1752  if ( p->fTarget && Fra_ClausRunSat( p ) )
1753  {
1754  printf( "Problem is inductive without strengthening.\n" );
1755  Fra_ClausFree( p );
1756  return 1;
1757  }
1758  if ( fVerbose )
1759  {
1760 // ABC_PRT( "SAT-ind", Abc_Clock() - clk );
1761  }
1762 
1763  // collect the candidate inductive clauses using 4-cuts
1764  clk = Abc_Clock();
1765  nPrefOld = p->nPref; p->nPref = 0; p->nSimWordsPref = 0;
1766  // Fra_ClausProcessClauses( p, fRefs );
1767  Fra_ClausProcessClauses2( p, fRefs );
1768  p->nPref = nPrefOld;
1769  p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
1770  nClausesBeg = p->nClauses;
1771 
1772  //ABC_PRT( "Clauses", Abc_Clock() - clk );
1773 
1774 
1775  // check clauses using BMC
1776  if ( fBmc )
1777  {
1778  clk = Abc_Clock();
1779  Counter = Fra_ClausBmcClauses( p );
1780  p->nClauses -= Counter;
1781  if ( fVerbose )
1782  {
1783  printf( "BMC disproved %d clauses. ", Counter );
1784  ABC_PRT( "Time", Abc_Clock() - clk );
1785  }
1786  }
1787 
1788 
1789  // prove clauses inductively
1790  clkInd = clk = Abc_Clock();
1791  Counter = 1;
1792  for ( Iter = 0; Counter > 0; Iter++ )
1793  {
1794  if ( fVerbose )
1795  printf( "Iter %3d : Begin = %5d. ", Iter, p->nClauses );
1796  Counter = Fra_ClausInductiveClauses( p );
1797  if ( Counter > 0 )
1798  p->nClauses -= Counter;
1799  if ( fVerbose )
1800  {
1801  printf( "End = %5d. Exs = %5d. ", p->nClauses, p->nCexes );
1802  // printf( "\n" );
1803  ABC_PRT( "Time", Abc_Clock() - clk );
1804  }
1805  clk = Abc_Clock();
1806  }
1807  // add proved clauses to storage
1808  Fra_ClausAddToStorage( p );
1809  // report the results
1810  if ( p->fTarget )
1811  {
1812  if ( Counter == -1 )
1813  printf( "Fra_Claus(): Internal error. " );
1814  else if ( p->fFail )
1815  printf( "Property FAILS during refinement. " );
1816  else
1817  printf( "Property HOLDS inductively after strengthening. " );
1818  ABC_PRT( "Time ", Abc_Clock() - clkTotal );
1819  if ( !p->fFail )
1820  break;
1821  }
1822  else
1823  {
1824  printf( "Finished proving inductive clauses. " );
1825  ABC_PRT( "Time ", Abc_Clock() - clkTotal );
1826  }
1827  }
1828 
1829  // verify the computed interpolant
1830  Fra_InvariantVerify( pAig, nFrames, p->vClausesProven, p->vLitsProven );
1831 // printf( "THIS COMMAND IS KNOWN TO HAVE A BUG!\n" );
1832 
1833 // if ( !p->fTarget && p->fVerbose )
1834  if ( p->fVerbose )
1835  {
1836  Fra_ClausPrintIndClauses( p );
1837  Fra_ClausEstimateCoverage( p );
1838  }
1839 
1840  if ( !p->fTarget )
1841  {
1842  Fra_ClausWriteIndClauses( p );
1843  }
1844 /*
1845  // print the statistic into a file
1846  {
1847  FILE * pTable;
1848  assert( p->nBatches == 1 );
1849  pTable = fopen( "stats.txt", "a+" );
1850  fprintf( pTable, "%s ", pAig->pName );
1851  fprintf( pTable, "%d ", Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig) );
1852  fprintf( pTable, "%d ", Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig) );
1853  fprintf( pTable, "%d ", Aig_ManRegNum(pAig) );
1854  fprintf( pTable, "%d ", Aig_ManNodeNum(pAig) );
1855  fprintf( pTable, "%d ", p->nCuts );
1856  fprintf( pTable, "%d ", nClausesBeg );
1857  fprintf( pTable, "%d ", p->nClauses );
1858  fprintf( pTable, "%d ", Iter );
1859  fprintf( pTable, "%.2f ", (float)(clkInd-clkTotal)/(float)(CLOCKS_PER_SEC) );
1860  fprintf( pTable, "%.2f ", (float)(Abc_Clock()-clkInd)/(float)(CLOCKS_PER_SEC) );
1861  fprintf( pTable, "%.2f ", (float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC) );
1862  fprintf( pTable, "\n" );
1863  fclose( pTable );
1864  }
1865 */
1866  // clean the manager
1867  Fra_ClausFree( p );
1868  return 1;
1869 }
1870 
1871 ////////////////////////////////////////////////////////////////////////
1872 /// END OF FILE ///
1873 ////////////////////////////////////////////////////////////////////////
1874 
1875 
1876 ABC_NAMESPACE_IMPL_END
1877 
memset
char * memset()
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Fra_Sml_t_::fNonConstOut
int fNonConstOut
Definition: fra.h:179
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Clu_Man_t_::nCexes
int nCexes
Definition: fraClaus.c:75
Fra_ClausAlloc
Clu_Man_t * Fra_ClausAlloc(Aig_Man_t *pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fTarget, int fVerbose, int fVeryVerbose)
Definition: fraClaus.c:1365
Abc_InfoMask
static unsigned Abc_InfoMask(int nVar)
Definition: abc_global.h:261
Clu_Man_t_::pAig
Aig_Man_t * pAig
Definition: fraClaus.c:53
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Aig_Obj_t_::Level
unsigned Level
Definition: aig.h:82
Clu_Man_t_::nBTLimit
int nBTLimit
Definition: fraClaus.c:51
Clu_Man_t_::fStepUp
int fStepUp
Definition: fraClaus.c:43
Clu_Man_t_::nOneHotsProven
int nOneHotsProven
Definition: fraClaus.c:69
Clu_Man_t_::nBatches
int nBatches
Definition: fraClaus.c:42
Clu_Man_t_::nCuts
int nCuts
Definition: fraClaus.c:67
Clu_Man_t_::nLutSize
int nLutSize
Definition: fraClaus.c:39
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Clu_Man_t_::nSimWordsPref
int nSimWordsPref
Definition: fraClaus.c:49
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Clu_Man_t_::vCexes
Vec_Ptr_t * vCexes
Definition: fraClaus.c:74
Clu_Man_t_::vClauses
Vec_Int_t * vClauses
Definition: fraClaus.c:64
Fra_ClausRunBmc
int Fra_ClausRunBmc(Clu_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: fraClaus.c:94
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Clu_Man_t_::fVerbose
int fVerbose
Definition: fraClaus.c:45
Fra_ClausProcessClauses
int Fra_ClausProcessClauses(Clu_Man_t *p, int fRefs)
Definition: fraClaus.c:601
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Fra_SmlSimulateSeq
Fra_Sml_t * Fra_SmlSimulateSeq(Aig_Man_t *pAig, int nPref, int nFrames, int nWords, int fCheckMiter)
Definition: fraSim.c:1021
Fra_ClausEstimateCoverage
void Fra_ClausEstimateCoverage(Clu_Man_t *p)
Definition: fraClaus.c:1620
Fra_ClausRecordClause
void Fra_ClausRecordClause(Clu_Man_t *p, Dar_Cut_t *pCut, int iMint, int Cost)
Definition: fraClaus.c:405
sat_solver_solve
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
lit_var
static int lit_var(lit l)
Definition: satVec.h:145
Dar_Cut_t_::uTruth
unsigned uTruth
Definition: darInt.h:58
Aig_MmFixedStop
void Aig_MmFixedStop(Aig_MmFixed_t *p, int fVerbose)
Definition: aigMem.c:132
Fra_ClausRunSat
int Fra_ClausRunSat(Clu_Man_t *p)
Definition: fraClaus.c:122
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Fra_ClausSimInfoCheck
int Fra_ClausSimInfoCheck(Clu_Man_t *p, int *pLits, int nLits)
Definition: fraClaus.c:1056
Fra_ClausFree
void Fra_ClausFree(Clu_Man_t *p)
Definition: fraClaus.c:1410
Clu_Man_t_::pCnf
Cnf_Dat_t * pCnf
Definition: fraClaus.c:58
Vec_PtrCleanSimInfo
static void Vec_PtrCleanSimInfo(Vec_Ptr_t *vInfo, int iWord, int nWords)
Definition: vecPtr.h:968
Clu_Man_t_::nCutsMax
int nCutsMax
Definition: fraClaus.c:41
Clu_Man_t_::vClausesProven
Vec_Int_t * vClausesProven
Definition: fraClaus.c:72
l_True
#define l_True
Definition: SolverTypes.h:84
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Aig_ManObj
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
Fra_Sml_t_::nWordsTotal
int nWordsTotal
Definition: fra.h:177
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Cnf_Dat_t_
Definition: cnf.h:56
Clu_Man_t_
Definition: fraClaus.c:33
nWords
int nWords
Definition: abcNpn.c:127
Aig_ManNodeNum
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Fra_ClausProcessClausesCut3
void Fra_ClausProcessClausesCut3(Clu_Man_t *p, Fra_Sml_t *pSimMan, Aig_Cut_t *pCut, int *pScores)
Definition: fraClaus.c:290
Fra_ClausSelectClauses
int Fra_ClausSelectClauses(Clu_Man_t *p)
Definition: fraClaus.c:350
Aig_MmFixed_t_
DECLARATIONS ///.
Definition: aigMem.c:30
Fra_ClausSmlNodesAreImp
int Fra_ClausSmlNodesAreImp(Fra_Sml_t *pSeq, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2)
Definition: fraClaus.c:467
Fra_ClausPrintIndClauses
void Fra_ClausPrintIndClauses(Clu_Man_t *p)
Definition: fraClaus.c:1483
Clu_Man_t_::nCexesAlloc
int nCexesAlloc
Definition: fraClaus.c:76
Aig_Cut_t_::nLeafMax
char nLeafMax
Definition: aig.h:186
Aig_ManCutStop
void Aig_ManCutStop(Aig_ManCut_t *p)
Definition: aigCuts.c:86
Fra_ObjSim
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
Dar_ManComputeCuts
Aig_MmFixed_t * Dar_ManComputeCuts(Aig_Man_t *pAig, int nCutsMax, int fSkipTtMin, int fVerbose)
Definition: darCore.c:287
Dar_ObjForEachCut
#define Dar_ObjForEachCut(pObj, pCut, i)
Definition: darInt.h:121
Fra_ClausSimInfoRecord
void Fra_ClausSimInfoRecord(Clu_Man_t *p, int *pModel)
Definition: fraClaus.c:1028
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
Ioa_FileNameGenericAppend
char * Ioa_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition: ioaUtil.c:93
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Clu_Man_t_::nOneHots
int nOneHots
Definition: fraClaus.c:68
Aig_WordCountOnes
static int Aig_WordCountOnes(unsigned uWord)
Definition: aig.h:229
Fra_Sml_t_
Definition: fra.h:171
Clu_Man_t_::fVeryVerbose
int fVeryVerbose
Definition: fraClaus.c:46
Dar_Cut_t_::pLeaves
int pLeaves[4]
Definition: darInt.h:63
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Fra_ClausRecordClause2
void Fra_ClausRecordClause2(Clu_Man_t *p, Aig_Cut_t *pCut, int iMint, int Cost)
Definition: fraClaus.c:425
Clu_Man_t_::nSimWords
int nSimWords
Definition: fraClaus.c:48
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
transpose32a
void transpose32a(unsigned a[32])
Definition: fraClaus.c:176
Clu_Man_t_::nLevels
int nLevels
Definition: fraClaus.c:40
Aig_ComputeCuts
Aig_ManCut_t * Aig_ComputeCuts(Aig_Man_t *pAig, int nCutsMax, int nLeafMax, int fTruth, int fVerbose)
Definition: aigCuts.c:631
Fra_ClausSimInfoClean
void Fra_ClausSimInfoClean(Clu_Man_t *p)
Definition: fraClaus.c:991
Clu_Man_t_::nSimFrames
int nSimFrames
Definition: fraClaus.c:50
Clu_Man_t_::fNothingNew
int fNothingNew
Definition: fraClaus.c:61
Fra_SmlSimulateComb
Fra_Sml_t * Fra_SmlSimulateComb(Aig_Man_t *pAig, int nWords, int fCheckMiter)
Definition: fraSim.c:856
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Fra_ClausProcessClausesCut
int Fra_ClausProcessClausesCut(Clu_Man_t *p, Fra_Sml_t *pSimMan, Dar_Cut_t *pCut, int *pScores)
Definition: fraClaus.c:202
Fra_ClausWriteIndClauses
void Fra_ClausWriteIndClauses(Clu_Man_t *p)
Definition: fraClaus.c:1540
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
Aig_Cut_t_::nFanins
char nFanins
Definition: aig.h:187
Counter
static int Counter
Definition: extraBddMisc.c:1877
Clu_Man_t_::fTarget
int fTarget
Definition: fraClaus.c:44
Dar_Cut_t_
Definition: darInt.h:55
Dar_Cut_t_::nLeaves
unsigned nLeaves
Definition: darInt.h:62
Ioa_WriteAiger
void Ioa_WriteAiger(Aig_Man_t *pMan, char *pFileName, int fWriteSymbols, int fCompact)
Definition: ioaWriteAig.c:446
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Clu_Man_t_::nFrames
int nFrames
Definition: fraClaus.c:36
Aig_Cut_t_::pFanins
int pFanins[0]
Definition: aig.h:188
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Clu_Man_t
typedefABC_NAMESPACE_IMPL_START struct Clu_Man_t_ Clu_Man_t
DECLARATIONS ///.
Definition: fraClaus.c:32
Aig_ManCut_t_
Definition: aig.h:192
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Aig_Cut_t_
Definition: aig.h:179
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
sat_solver_simplify
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
Fra_ClausGetLiteral
Aig_Obj_t * Fra_ClausGetLiteral(Clu_Man_t *p, int *pVar2Id, int Lit)
Definition: fraClaus.c:1520
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Cnf_DataWriteIntoSolver
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
Fra_ClausProcessClausesCut2
int Fra_ClausProcessClausesCut2(Clu_Man_t *p, Fra_Sml_t *pSimMan, Dar_Cut_t *pCut, int *pScores)
Definition: fraClaus.c:248
Fra_ClausSmlNodeIsConst
int Fra_ClausSmlNodeIsConst(Fra_Sml_t *pSeq, Aig_Obj_t *pObj)
Definition: fraClaus.c:445
Cnf_DeriveSimple
Cnf_Dat_t * Cnf_DeriveSimple(Aig_Man_t *p, int nOutputs)
Definition: cnfWrite.c:587
lit_sign
static int lit_sign(lit l)
Definition: satVec.h:146
Clu_Man_t_::pSatBmc
sat_solver * pSatBmc
Definition: fraClaus.c:56
Fra_ClausSmlNodesAreImpC
int Fra_ClausSmlNodesAreImpC(Fra_Sml_t *pSeq, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2)
Definition: fraClaus.c:490
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Clu_Man_t_::nPref
int nPref
Definition: fraClaus.c:37
Clu_Man_t_::vLits
Vec_Int_t * vLits
Definition: fraClaus.c:63
Clu_Man_t_::vCosts
Vec_Int_t * vCosts
Definition: fraClaus.c:65
Clu_Man_t_::vLitsProven
Vec_Int_t * vLitsProven
Definition: fraClaus.c:71
Aig_ManForEachLoSeq
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition: aig.h:441
l_False
#define l_False
Definition: SolverTypes.h:85
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
Fra_ClausRunSat0
int Fra_ClausRunSat0(Clu_Man_t *p)
Definition: fraClaus.c:153
Fra_ClausAddToStorage
void Fra_ClausAddToStorage(Clu_Man_t *p)
Definition: fraClaus.c:1436
Clu_Man_t_::pSatMain
sat_solver * pSatMain
Definition: fraClaus.c:55
Fra_ClausCollectLatchClauses
int Fra_ClausCollectLatchClauses(Clu_Man_t *p, Fra_Sml_t *pSeq)
Definition: fraClaus.c:513
Fra_ClausBmcClauses
int Fra_ClausBmcClauses(Clu_Man_t *p)
Definition: fraClaus.c:897
Vec_PtrReallocSimInfo
static void Vec_PtrReallocSimInfo(Vec_Ptr_t *vInfo)
Definition: vecPtr.h:1035
sat_solver_t
Definition: satSolver.h:91
assert
#define assert(ex)
Definition: util_old.h:213
Fra_ClausSimInfoRealloc
void Fra_ClausSimInfoRealloc(Clu_Man_t *p)
Definition: fraClaus.c:1009
Clu_Man_t_::fFail
int fFail
Definition: fraClaus.c:59
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
Fra_Sml_t_::nWordsPref
int nWordsPref
Definition: fra.h:178
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Fra_ClausEstimateCoverageOne
void Fra_ClausEstimateCoverageOne(Fra_Sml_t *pSim, int *pLits, int nLits, int *pVar2Id, unsigned *pResult)
Definition: fraClaus.c:1592
Aig_ManDupWithoutPos
Aig_Man_t * Aig_ManDupWithoutPos(Aig_Man_t *p)
Definition: aigDup.c:835
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Clu_Man_t_::nClausesMax
int nClausesMax
Definition: fraClaus.c:38
Aig_ObjForEachCut
#define Aig_ObjForEachCut(p, pObj, pCut, i)
Definition: aig.h:218
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Fra_ClausInductiveClauses
int Fra_ClausInductiveClauses(Clu_Man_t *p)
Definition: fraClaus.c:1098
Fra_InvariantVerify
int Fra_InvariantVerify(Aig_Man_t *p, int nFrames, Vec_Int_t *vClauses, Vec_Int_t *vLits)
DECLARATIONS ///.
Definition: fraIndVer.c:46
Fra_ClausProcessClauses2
int Fra_ClausProcessClauses2(Clu_Man_t *p, int fRefs)
Definition: fraClaus.c:724
Vec_PtrAllocSimInfo
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
Clu_Man_t_::nClauses
int nClauses
Definition: fraClaus.c:66
Fra_SmlStop
void Fra_SmlStop(Fra_Sml_t *p)
Definition: fraSim.c:839
Fra_Claus
int Fra_Claus(Aig_Man_t *pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose)
Definition: fraClaus.c:1682
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Clu_Man_t_::fFiltering
int fFiltering
Definition: fraClaus.c:60