abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraCec.c File Reference
#include "fra.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver2.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START int Fra_FraigSat (Aig_Man_t *pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose)
 DECLARATIONS ///. More...
 
int Aig_ManCountXors (Aig_Man_t *p)
 
int Fra_FraigCec (Aig_Man_t **ppAig, int nConfLimit, int fVerbose)
 
int Fra_FraigCecPartitioned (Aig_Man_t *pMan1, Aig_Man_t *pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose)
 
int Fra_FraigCecTop (Aig_Man_t *pMan1, Aig_Man_t *pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose)
 

Function Documentation

int Aig_ManCountXors ( Aig_Man_t p)

Function*************************************************************

Synopsis [Recognizes what nodes are inputs of the EXOR.]

Description []

SideEffects []

SeeAlso []

Definition at line 298 of file fraCec.c.

299 {
300  Aig_Obj_t * pObj, * pFan0, * pFan1;
301  int i, Counter = 0;
302  Aig_ManForEachNode( p, pObj, i )
303  if ( Aig_ObjIsMuxType(pObj) && Aig_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
304  Counter++;
305  return Counter;
306 
307 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
if(last==0)
Definition: sparse_int.h:34
int Aig_ObjRecognizeExor(Aig_Obj_t *pObj, Aig_Obj_t **ppFan0, Aig_Obj_t **ppFan1)
Definition: aigUtil.c:343
Definition: aig.h:69
static int Counter
int Aig_ObjIsMuxType(Aig_Obj_t *pObj)
Definition: aigUtil.c:307
int Fra_FraigCec ( Aig_Man_t **  ppAig,
int  nConfLimit,
int  fVerbose 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 320 of file fraCec.c.

321 {
322  int nBTLimitStart = 300; // starting SAT run
323  int nBTLimitFirst = 2; // first fraiging iteration
324  int nBTLimitLast = nConfLimit; // the last-gasp SAT run
325 
326  Fra_Par_t Params, * pParams = &Params;
327  Aig_Man_t * pAig = *ppAig, * pTemp;
328  int i, RetValue;
329  abctime clk;
330 
331  // report the original miter
332  if ( fVerbose )
333  {
334  printf( "Original miter: Nodes = %6d.\n", Aig_ManNodeNum(pAig) );
335  }
336  RetValue = Fra_FraigMiterStatus( pAig );
337 // assert( RetValue == -1 );
338  if ( RetValue == 0 )
339  {
340  pAig->pData = ABC_ALLOC( int, Aig_ManCiNum(pAig) );
341  memset( pAig->pData, 0, sizeof(int) * Aig_ManCiNum(pAig) );
342  return RetValue;
343  }
344 
345  // if SAT only, solve without iteration
346 clk = Abc_Clock();
347  RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
348  if ( fVerbose )
349  {
350  printf( "Initial SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
351 ABC_PRT( "Time", Abc_Clock() - clk );
352  }
353  if ( RetValue >= 0 )
354  return RetValue;
355 
356  // duplicate the AIG
357 clk = Abc_Clock();
358  pAig = Dar_ManRwsat( pTemp = pAig, 1, 0 );
359  Aig_ManStop( pTemp );
360  if ( fVerbose )
361  {
362  printf( "Rewriting: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
363 ABC_PRT( "Time", Abc_Clock() - clk );
364  }
365 
366  // perform the loop
367  Fra_ParamsDefault( pParams );
368  pParams->nBTLimitNode = nBTLimitFirst;
369  pParams->nBTLimitMiter = nBTLimitStart;
370  pParams->fDontShowBar = 1;
371  pParams->fProve = 1;
372  for ( i = 0; i < 6; i++ )
373  {
374 //printf( "Running fraiging with %d BTnode and %d BTmiter.\n", pParams->nBTLimitNode, pParams->nBTLimitMiter );
375  // try XOR balancing
376  if ( Aig_ManCountXors(pAig) * 30 > Aig_ManNodeNum(pAig) + 300 )
377  {
378 clk = Abc_Clock();
379  pAig = Dar_ManBalanceXor( pTemp = pAig, 1, 0, 0 );
380  Aig_ManStop( pTemp );
381  if ( fVerbose )
382  {
383  printf( "Balance-X: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
384 ABC_PRT( "Time", Abc_Clock() - clk );
385  }
386  }
387 
388  // run fraiging
389 clk = Abc_Clock();
390  pAig = Fra_FraigPerform( pTemp = pAig, pParams );
391  Aig_ManStop( pTemp );
392  if ( fVerbose )
393  {
394  printf( "Fraiging (i=%d): Nodes = %6d. ", i+1, Aig_ManNodeNum(pAig) );
395 ABC_PRT( "Time", Abc_Clock() - clk );
396  }
397 
398  // check the miter status
399  RetValue = Fra_FraigMiterStatus( pAig );
400  if ( RetValue >= 0 )
401  break;
402 
403  // perform rewriting
404 clk = Abc_Clock();
405  pAig = Dar_ManRewriteDefault( pTemp = pAig );
406  Aig_ManStop( pTemp );
407  if ( fVerbose )
408  {
409  printf( "Rewriting: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
410 ABC_PRT( "Time", Abc_Clock() - clk );
411  }
412 
413  // check the miter status
414  RetValue = Fra_FraigMiterStatus( pAig );
415  if ( RetValue >= 0 )
416  break;
417  // try simulation
418 
419  // set the parameters for the next run
420  pParams->nBTLimitNode = 8 * pParams->nBTLimitNode;
421  pParams->nBTLimitMiter = 2 * pParams->nBTLimitMiter;
422  }
423 
424  // if still unsolved try last gasp
425  if ( RetValue == -1 )
426  {
427 clk = Abc_Clock();
428  RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
429  if ( fVerbose )
430  {
431  printf( "Final SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
432 ABC_PRT( "Time", Abc_Clock() - clk );
433  }
434  }
435 
436  *ppAig = pAig;
437  return RetValue;
438 }
char * memset()
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Aig_Man_t * Dar_ManBalanceXor(Aig_Man_t *pAig, int fExor, int fUpdateLevel, int fVerbose)
Definition: darBalance.c:687
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
int Aig_ManCountXors(Aig_Man_t *p)
Definition: fraCec.c:298
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
ABC_NAMESPACE_IMPL_START int Fra_FraigSat(Aig_Man_t *pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose)
DECLARATIONS ///.
Definition: fraCec.c:47
static abctime Abc_Clock()
Definition: abc_global.h:279
ABC_NAMESPACE_IMPL_START Aig_Man_t * Dar_ManRwsat(Aig_Man_t *pAig, int fBalance, int fVerbose)
DECLARATIONS ///.
Definition: darScript.c:71
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
void Fra_ParamsDefault(Fra_Par_t *pParams)
DECLARATIONS ///.
Definition: fraMan.c:45
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Aig_Man_t * Dar_ManRewriteDefault(Aig_Man_t *pAig)
DECLARATIONS ///.
Definition: darScript.c:48
typedefABC_NAMESPACE_HEADER_START struct Fra_Par_t_ Fra_Par_t
INCLUDES ///.
Definition: fra.h:53
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Aig_Man_t * Fra_FraigPerform(Aig_Man_t *pManAig, Fra_Par_t *pPars)
Definition: fraCore.c:375
int Fra_FraigMiterStatus(Aig_Man_t *p)
DECLARATIONS ///.
Definition: fraCore.c:62
ABC_INT64_T abctime
Definition: abc_global.h:278
int Fra_FraigCecPartitioned ( Aig_Man_t pMan1,
Aig_Man_t pMan2,
int  nConfLimit,
int  nPartSize,
int  fSmart,
int  fVerbose 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 451 of file fraCec.c.

452 {
453  Aig_Man_t * pAig;
454  Vec_Ptr_t * vParts;
455  int i, RetValue = 1, nOutputs;
456  // create partitions
457  vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize, fSmart );
458  // solve the partitions
459  nOutputs = -1;
460  Vec_PtrForEachEntry( Aig_Man_t *, vParts, pAig, i )
461  {
462  nOutputs++;
463  if ( fVerbose )
464  {
465  printf( "Verifying part %4d (out of %4d) PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r",
466  i+1, Vec_PtrSize(vParts), Aig_ManCiNum(pAig), Aig_ManCoNum(pAig),
467  Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
468  fflush( stdout );
469  }
470  RetValue = Fra_FraigMiterStatus( pAig );
471  if ( RetValue == 1 )
472  continue;
473  if ( RetValue == 0 )
474  break;
475  RetValue = Fra_FraigCec( &pAig, nConfLimit, 0 );
476  Vec_PtrWriteEntry( vParts, i, pAig );
477  if ( RetValue == 1 )
478  continue;
479  if ( RetValue == 0 )
480  break;
481  break;
482  }
483  // clear the result
484  if ( fVerbose )
485  {
486  printf( " \r" );
487  fflush( stdout );
488  }
489  // report the timeout
490  if ( RetValue == -1 )
491  {
492  printf( "Timed out after verifying %d partitions (out of %d).\n", nOutputs, Vec_PtrSize(vParts) );
493  fflush( stdout );
494  }
495  // free intermediate results
496  Vec_PtrForEachEntry( Aig_Man_t *, vParts, pAig, i )
497  Aig_ManStop( pAig );
498  Vec_PtrFree( vParts );
499  return RetValue;
500 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
int Fra_FraigCec(Aig_Man_t **ppAig, int nConfLimit, int fVerbose)
Definition: fraCec.c:320
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
int Aig_ManLevelNum(Aig_Man_t *p)
Definition: aigDfs.c:486
Vec_Ptr_t * Aig_ManMiterPartitioned(Aig_Man_t *p1, Aig_Man_t *p2, int nPartSize, int fSmart)
Definition: aigPart.c:1189
int Fra_FraigMiterStatus(Aig_Man_t *p)
DECLARATIONS ///.
Definition: fraCore.c:62
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
int Fra_FraigCecTop ( Aig_Man_t pMan1,
Aig_Man_t pMan2,
int  nConfLimit,
int  nPartSize,
int  fSmart,
int  fVerbose 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 513 of file fraCec.c.

514 {
515  Aig_Man_t * pTemp;
516  //Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose );
517  int RetValue;
518  abctime clkTotal = Abc_Clock();
519 
520  if ( Aig_ManCiNum(pMan1) != Aig_ManCiNum(pMan1) )
521  {
522  printf( "Abc_CommandAbc8Cec(): Miters have different number of PIs.\n" );
523  return 0;
524  }
525  if ( Aig_ManCoNum(pMan1) != Aig_ManCoNum(pMan1) )
526  {
527  printf( "Abc_CommandAbc8Cec(): Miters have different number of POs.\n" );
528  return 0;
529  }
530  assert( Aig_ManCiNum(pMan1) == Aig_ManCiNum(pMan1) );
531  assert( Aig_ManCoNum(pMan1) == Aig_ManCoNum(pMan1) );
532 
533  // make sure that the first miter has more nodes
534  if ( Aig_ManNodeNum(pMan1) < Aig_ManNodeNum(pMan2) )
535  {
536  pTemp = pMan1;
537  pMan1 = pMan2;
538  pMan2 = pTemp;
539  }
540  assert( Aig_ManNodeNum(pMan1) >= Aig_ManNodeNum(pMan2) );
541 
542  if ( nPartSize )
543  RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, nPartSize, fSmart, fVerbose );
544  else // no partitioning
545  RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, Aig_ManCoNum(pMan1), 0, fVerbose );
546 
547  // report the miter
548  if ( RetValue == 1 )
549  {
550  printf( "Networks are equivalent. " );
551 ABC_PRT( "Time", Abc_Clock() - clkTotal );
552  }
553  else if ( RetValue == 0 )
554  {
555  printf( "Networks are NOT EQUIVALENT. " );
556 ABC_PRT( "Time", Abc_Clock() - clkTotal );
557  }
558  else
559  {
560  printf( "Networks are UNDECIDED. " );
561 ABC_PRT( "Time", Abc_Clock() - clkTotal );
562  }
563  fflush( stdout );
564  return RetValue;
565 }
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
int Fra_FraigCecPartitioned(Aig_Man_t *pMan1, Aig_Man_t *pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose)
Definition: fraCec.c:451
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
#define ABC_PRT(a, t)
Definition: abc_global.h:220
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
ABC_NAMESPACE_IMPL_START int Fra_FraigSat ( Aig_Man_t pMan,
ABC_INT64_T  nConfLimit,
ABC_INT64_T  nInsLimit,
int  nLearnedStart,
int  nLearnedDelta,
int  nLearnedPerce,
int  fFlipBits,
int  fAndOuts,
int  fNewSolver,
int  fVerbose 
)

DECLARATIONS ///.

ITERATORS ///.

CFile****************************************************************

FileName [fraCec.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [CEC engined based on fraiging.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:
fraCec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file fraCec.c.

48 {
49  if ( fNewSolver )
50  {
51  extern void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit );
52  extern int Cnf_DataWriteOrClause2( void * pSat, Cnf_Dat_t * pCnf );
53 
54  sat_solver2 * pSat;
55  Cnf_Dat_t * pCnf;
56  int status, RetValue;
57  abctime clk = Abc_Clock();
58  Vec_Int_t * vCiIds;
59 
60  assert( Aig_ManRegNum(pMan) == 0 );
61  pMan->pData = NULL;
62 
63  // derive CNF
64  pCnf = Cnf_Derive( pMan, Aig_ManCoNum(pMan) );
65  // pCnf = Cnf_DeriveSimple( pMan, Aig_ManCoNum(pMan) );
66 
67  if ( fFlipBits )
68  Cnf_DataTranformPolarity( pCnf, 0 );
69 
70  if ( fVerbose )
71  {
72  printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
73  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
74  }
75 
76  // convert into SAT solver
77  pSat = (sat_solver2 *)Cnf_DataWriteIntoSolver2( pCnf, 1, 0 );
78  if ( pSat == NULL )
79  {
80  Cnf_DataFree( pCnf );
81  return 1;
82  }
83 
84  if ( fAndOuts )
85  {
86  // assert each output independently
87  if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) )
88  {
89  sat_solver2_delete( pSat );
90  Cnf_DataFree( pCnf );
91  return 1;
92  }
93  }
94  else
95  {
96  // add the OR clause for the outputs
97  if ( !Cnf_DataWriteOrClause2( pSat, pCnf ) )
98  {
99  sat_solver2_delete( pSat );
100  Cnf_DataFree( pCnf );
101  return 1;
102  }
103  }
104  vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
105  Cnf_DataFree( pCnf );
106 
107 
108  printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) );
109  ABC_PRT( "Time", Abc_Clock() - clk );
110 
111  // simplify the problem
112  clk = Abc_Clock();
113  status = sat_solver2_simplify(pSat);
114 // printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) );
115 // ABC_PRT( "Time", Abc_Clock() - clk );
116  if ( status == 0 )
117  {
118  Vec_IntFree( vCiIds );
119  sat_solver2_delete( pSat );
120  // printf( "The problem is UNSATISFIABLE after simplification.\n" );
121  return 1;
122  }
123 
124  // solve the miter
125  clk = Abc_Clock();
126  if ( fVerbose )
127  pSat->verbosity = 1;
128  status = sat_solver2_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
129  if ( status == l_Undef )
130  {
131  // printf( "The problem timed out.\n" );
132  RetValue = -1;
133  }
134  else if ( status == l_True )
135  {
136  // printf( "The problem is SATISFIABLE.\n" );
137  RetValue = 0;
138  }
139  else if ( status == l_False )
140  {
141  // printf( "The problem is UNSATISFIABLE.\n" );
142  RetValue = 1;
143  }
144  else
145  assert( 0 );
146 
147  // Abc_Print( 1, "The number of conflicts = %6d. ", (int)pSat->stats.conflicts );
148  // Abc_PrintTime( 1, "Solving time", Abc_Clock() - clk );
149 
150  // if the problem is SAT, get the counterexample
151  if ( status == l_True )
152  {
153  pMan->pData = Sat_Solver2GetModel( pSat, vCiIds->pArray, vCiIds->nSize );
154  }
155  // free the sat_solver2
156  if ( fVerbose )
157  Sat_Solver2PrintStats( stdout, pSat );
158  //sat_solver2_store_write( pSat, "trace.cnf" );
159  //sat_solver2_store_free( pSat );
160  sat_solver2_delete( pSat );
161  Vec_IntFree( vCiIds );
162  return RetValue;
163  }
164  else
165  {
166  sat_solver * pSat;
167  Cnf_Dat_t * pCnf;
168  int status, RetValue;
169  abctime clk = Abc_Clock();
170  Vec_Int_t * vCiIds;
171 
172  assert( Aig_ManRegNum(pMan) == 0 );
173  pMan->pData = NULL;
174 
175  // derive CNF
176  pCnf = Cnf_Derive( pMan, Aig_ManCoNum(pMan) );
177  // pCnf = Cnf_DeriveSimple( pMan, Aig_ManCoNum(pMan) );
178 
179  if ( fFlipBits )
180  Cnf_DataTranformPolarity( pCnf, 0 );
181 
182  if ( fVerbose )
183  {
184  printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
185  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
186  }
187 
188  // convert into SAT solver
189  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
190  if ( pSat == NULL )
191  {
192  Cnf_DataFree( pCnf );
193  return 1;
194  }
195 
196  if ( nLearnedStart )
197  pSat->nLearntStart = nLearnedStart;
198  if ( nLearnedDelta )
199  pSat->nLearntDelta = nLearnedDelta;
200  if ( nLearnedPerce )
201  pSat->nLearntRatio = nLearnedPerce;
202  if ( fVerbose )
203  pSat->fVerbose = fVerbose;
204 
205  if ( fAndOuts )
206  {
207  // assert each output independently
208  if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) )
209  {
210  sat_solver_delete( pSat );
211  Cnf_DataFree( pCnf );
212  return 1;
213  }
214  }
215  else
216  {
217  // add the OR clause for the outputs
218  if ( !Cnf_DataWriteOrClause( pSat, pCnf ) )
219  {
220  sat_solver_delete( pSat );
221  Cnf_DataFree( pCnf );
222  return 1;
223  }
224  }
225  vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
226  Cnf_DataFree( pCnf );
227 
228 
229  // printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
230  // ABC_PRT( "Time", Abc_Clock() - clk );
231 
232  // simplify the problem
233  clk = Abc_Clock();
234  status = sat_solver_simplify(pSat);
235  // printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
236  // ABC_PRT( "Time", Abc_Clock() - clk );
237  if ( status == 0 )
238  {
239  Vec_IntFree( vCiIds );
240  sat_solver_delete( pSat );
241  // printf( "The problem is UNSATISFIABLE after simplification.\n" );
242  return 1;
243  }
244 
245  // solve the miter
246  clk = Abc_Clock();
247 // if ( fVerbose )
248 // pSat->verbosity = 1;
249  status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
250  if ( status == l_Undef )
251  {
252  // printf( "The problem timed out.\n" );
253  RetValue = -1;
254  }
255  else if ( status == l_True )
256  {
257  // printf( "The problem is SATISFIABLE.\n" );
258  RetValue = 0;
259  }
260  else if ( status == l_False )
261  {
262  // printf( "The problem is UNSATISFIABLE.\n" );
263  RetValue = 1;
264  }
265  else
266  assert( 0 );
267 
268  // Abc_Print( 1, "The number of conflicts = %6d. ", (int)pSat->stats.conflicts );
269  // Abc_PrintTime( 1, "Solving time", Abc_Clock() - clk );
270 
271  // if the problem is SAT, get the counterexample
272  if ( status == l_True )
273  {
274  pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
275  }
276  // free the sat_solver
277  if ( fVerbose )
278  Sat_SolverPrintStats( stdout, pSat );
279  //sat_solver_store_write( pSat, "trace.cnf" );
280  //sat_solver_store_free( pSat );
281  sat_solver_delete( pSat );
282  Vec_IntFree( vCiIds );
283  return RetValue;
284  }
285 }
static int sat_solver2_nclauses(sat_solver2 *s)
Definition: satSolver2.h:195
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
#define l_Undef
Definition: SolverTypes.h:86
int Cnf_DataWriteOrClause(void *pSat, Cnf_Dat_t *pCnf)
Definition: cnfMan.c:571
int nClauses
Definition: cnf.h:61
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
void sat_solver2_delete(sat_solver2 *s)
Definition: satSolver2.c:1225
int nVars
Definition: cnf.h:59
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
void Cnf_DataTranformPolarity(Cnf_Dat_t *pCnf, int fTransformPos)
Definition: cnfMan.c:652
#define l_True
Definition: SolverTypes.h:84
void Sat_Solver2PrintStats(FILE *pFile, sat_solver2 *p)
Definition: satUtil.c:210
static abctime Abc_Clock()
Definition: abc_global.h:279
Definition: cnf.h:56
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
int nLearntDelta
Definition: satSolver.h:159
void * Cnf_DataWriteIntoSolver2(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:479
int sat_solver2_simplify(sat_solver2 *s)
Definition: satSolver2.c:996
Vec_Int_t * Cnf_DataCollectPiSatNums(Cnf_Dat_t *pCnf, Aig_Man_t *p)
Definition: cnfMan.c:104
int Cnf_DataWriteAndClauses(void *p, Cnf_Dat_t *pCnf)
Definition: cnfMan.c:627
int nLearntRatio
Definition: satSolver.h:160
int Cnf_DataWriteOrClause2(void *p, Cnf_Dat_t *pCnf)
Definition: cnfMan.c:599
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
int nLearntStart
Definition: satSolver.h:158
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
#define ABC_PRT(a, t)
Definition: abc_global.h:220
static int sat_solver2_nvars(sat_solver2 *s)
Definition: satSolver2.h:190
#define l_False
Definition: SolverTypes.h:85
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
int sat_solver2_solve(sat_solver2 *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver2.c:1835
int * Sat_Solver2GetModel(sat_solver2 *p, int *pVars, int nVars)
Definition: satUtil.c:287
#define assert(ex)
Definition: util_old.h:213
void Sat_SolverPrintStats(FILE *pFile, sat_solver *p)
Definition: satUtil.c:188
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
ABC_INT64_T abctime
Definition: abc_global.h:278
int nLiterals
Definition: cnf.h:60
int * Sat_SolverGetModel(sat_solver *p, int *pVars, int nVars)
Definition: satUtil.c:266