abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bmcICheck.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [bmcICheck.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [SAT-based bounded model checking.]
8 
9  Synopsis [Performs specialized check.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: bmcICheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "bmc.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satStore.h"
24 #include "aig/gia/giaAig.h"
25 
26 ABC_NAMESPACE_IMPL_START
27 
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 ////////////////////////////////////////////////////////////////////////
34 /// FUNCTION DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36 
37 /**Function*************************************************************
38 
39  Synopsis []
40 
41  Description []
42 
43  SideEffects []
44 
45  SeeAlso []
46 
47 ***********************************************************************/
48 static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
49 {
50  Cnf_Dat_t * pCnf;
51  Aig_Man_t * pAig = Gia_ManToAigSimple( p );
52  pAig->nRegs = 0;
53  pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
54  Aig_ManStop( pAig );
55  return pCnf;
56 }
57 
58 /**Function*************************************************************
59 
60  Synopsis []
61 
62  Description []
63 
64  SideEffects []
65 
66  SeeAlso []
67 
68 ***********************************************************************/
69 static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPlus )
70 {
71  Gia_Obj_t * pObj;
72  int v;
73  Gia_ManForEachObj( pGia, pObj, v )
74  if ( p->pVarNums[Gia_ObjId(pGia, pObj)] >= 0 )
75  p->pVarNums[Gia_ObjId(pGia, pObj)] += nVarsPlus;
76  for ( v = 0; v < p->nLiterals; v++ )
77  p->pClauses[0][v] += 2*nVarsPlus;
78 }
79 
80 /**Function*************************************************************
81 
82  Synopsis []
83 
84  Description []
85 
86  SideEffects []
87 
88  SeeAlso []
89 
90 ***********************************************************************/
91 sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pCnf, int nFramesMax, int nTimeOut, int fVerbose )
92 {
93  sat_solver * pSat;
94  Vec_Int_t * vLits;
95  Gia_Obj_t * pObj, * pObj0, * pObj1;
96  int i, k, iVar0, iVar1, iVarOut;
97  int VarShift = 0;
98 
99  // start the SAT solver
100  pSat = sat_solver_new();
101  sat_solver_setnvars( pSat, Gia_ManRegNum(p) + Gia_ManCoNum(p) + pCnf->nVars * (nFramesMax + 1) );
102  sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
103 
104  // add one large OR clause
105  vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
106  Gia_ManForEachCo( p, pObj, i )
107  Vec_IntPush( vLits, Abc_Var2Lit(Gia_ManRegNum(p) + i, 0) );
108  sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
109 
110  // load the last timeframe
111  Cnf_DataLiftGia( pCnf, pMiter, Gia_ManRegNum(p) + Gia_ManCoNum(p) );
112  VarShift += Gia_ManRegNum(p) + Gia_ManCoNum(p);
113 
114  // add XOR clauses
115  Gia_ManForEachPo( p, pObj, i )
116  {
117  pObj0 = Gia_ManPo( pMiter, 2*i+0 );
118  pObj1 = Gia_ManPo( pMiter, 2*i+1 );
119  iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
120  iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
121  iVarOut = Gia_ManRegNum(p) + i;
122  sat_solver_add_xor( pSat, iVar0, iVar1, iVarOut, 0 );
123  }
124  Gia_ManForEachRi( p, pObj, i )
125  {
126  pObj0 = Gia_ManRi( pMiter, i );
127  pObj1 = Gia_ManRi( pMiter, i + Gia_ManRegNum(p) );
128  iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
129  iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
130  iVarOut = Gia_ManRegNum(p) + Gia_ManPoNum(p) + i;
131  sat_solver_add_xor_and( pSat, iVarOut, iVar0, iVar1, i );
132  }
133  // add timeframe clauses
134  for ( i = 0; i < pCnf->nClauses; i++ )
135  if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
136  assert( 0 );
137 
138  // add other timeframes
139  for ( k = 0; k < nFramesMax; k++ )
140  {
141  // collect variables of the RO nodes
142  Vec_IntClear( vLits );
143  Gia_ManForEachRo( pMiter, pObj, i )
144  Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pMiter, pObj)] );
145  // lift CNF again
146  Cnf_DataLiftGia( pCnf, pMiter, pCnf->nVars );
147  VarShift += pCnf->nVars;
148  // stitch the clauses
149  Gia_ManForEachRi( pMiter, pObj, i )
150  {
151  iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj)];
152  iVar1 = Vec_IntEntry( vLits, i );
153  if ( iVar1 == -1 )
154  continue;
155  sat_solver_add_buffer( pSat, iVar0, iVar1, 0 );
156  }
157  // add equality clauses for the COs
158  Gia_ManForEachPo( p, pObj, i )
159  {
160  pObj0 = Gia_ManPo( pMiter, 2*i+0 );
161  pObj1 = Gia_ManPo( pMiter, 2*i+1 );
162  iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
163  iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
164  sat_solver_add_buffer( pSat, iVar0, iVar1, 0 );
165  }
166  Gia_ManForEachRi( p, pObj, i )
167  {
168  pObj0 = Gia_ManRi( pMiter, i );
169  pObj1 = Gia_ManRi( pMiter, i + Gia_ManRegNum(p) );
170  iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
171  iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
172  sat_solver_add_buffer_enable( pSat, iVar0, iVar1, i, 0 );
173  }
174  // add timeframe clauses
175  for ( i = 0; i < pCnf->nClauses; i++ )
176  if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
177  assert( 0 );
178  }
179 // sat_solver_compress( pSat );
180  Cnf_DataLiftGia( pCnf, pMiter, -VarShift );
181  Vec_IntFree( vLits );
182  return pSat;
183 }
184 
185 /**Function*************************************************************
186 
187  Synopsis []
188 
189  Description []
190 
191  SideEffects []
192 
193  SeeAlso []
194 
195 ***********************************************************************/
196 void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose )
197 {
198  int fUseOldCnf = 0;
199  Gia_Man_t * pMiter, * pTemp;
200  Cnf_Dat_t * pCnf;
201  sat_solver * pSat;
202  Vec_Int_t * vLits, * vUsed;
203  int i, status, Lit;
204  int nLitsUsed, nLits, * pLits;
205  abctime clkStart = Abc_Clock();
206  assert( nFramesMax > 0 );
207  assert( Gia_ManRegNum(p) > 0 );
208 
209  if ( fVerbose )
210  printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n",
211  Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) );
212 
213  // create miter
214  pTemp = Gia_ManDup( p );
215  pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0, 0 );
216  Gia_ManStop( pTemp );
217  assert( Gia_ManPoNum(pMiter) == 2 * Gia_ManPoNum(p) );
218  assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );
219  // derive CNF
220  if ( fUseOldCnf )
221  pCnf = Cnf_DeriveGiaRemapped( pMiter );
222  else
223  {
224  pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
225  Gia_ManStop( pTemp );
226  pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
227  }
228 
229  // collect positive literals
230  vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
231  for ( i = 0; i < Gia_ManRegNum(p); i++ )
232  Vec_IntPush( vLits, Abc_Var2Lit(i, fEmpty) );
233 
234  // iteratively compute a minimal M-inductive set of next-state functions
235  nLitsUsed = fEmpty ? 0 : Vec_IntSize(vLits);
236  vUsed = Vec_IntAlloc( Vec_IntSize(vLits) );
237  while ( 1 )
238  {
239  int fChanges = 0;
240  // derive SAT solver
241  pSat = Bmc_DeriveSolver( p, pMiter, pCnf, nFramesMax, nTimeOut, fVerbose );
242 // sat_solver_bookmark( pSat );
243  status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
244  if ( status == l_Undef )
245  {
246  printf( "Timeout reached after %d seconds.\n", nTimeOut );
247  break;
248  }
249  if ( status == l_True )
250  {
251  printf( "The problem is satisfiable (the current set is not M-inductive).\n" );
252  break;
253  }
254  assert( status == l_False );
255  // call analize_final
256  nLits = sat_solver_final( pSat, &pLits );
257  // mark used literals
258  Vec_IntFill( vUsed, Vec_IntSize(vLits), 0 );
259  for ( i = 0; i < nLits; i++ )
260  Vec_IntWriteEntry( vUsed, Abc_Lit2Var(pLits[i]), 1 );
261 
262  // check if there are any positive unused
263  Vec_IntForEachEntry( vLits, Lit, i )
264  {
265  assert( i == Abc_Lit2Var(Lit) );
266  if ( Abc_LitIsCompl(Lit) )
267  continue;
268  if ( Vec_IntEntry(vUsed, i) )
269  continue;
270  // positive literal became unused
271  Vec_IntWriteEntry( vLits, i, Abc_LitNot(Lit) );
272  nLitsUsed--;
273  fChanges = 1;
274  }
275  // report the results
276  if ( fVerbose )
277  printf( "M =%4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ",
278  nFramesMax, (nFramesMax+1) * Gia_ManAndNum(pMiter),
279  Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat),
280  sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
281  if ( fVerbose )
282  Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
283  // count the number of negative literals
284  sat_solver_delete( pSat );
285  if ( !fChanges || fEmpty )
286  break;
287 // break;
288 // sat_solver_rollback( pSat );
289  }
290  Cnf_DataFree( pCnf );
291  Gia_ManStop( pMiter );
292  Vec_IntFree( vLits );
293  Vec_IntFree( vUsed );
294 }
295 
296 /**Function*************************************************************
297 
298  Synopsis []
299 
300  Description []
301 
302  SideEffects []
303 
304  SeeAlso []
305 
306 ***********************************************************************/
307 int Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fVerbose, Vec_Int_t * vLits )
308 {
309  int fUseOldCnf = 0;
310  Gia_Man_t * pMiter, * pTemp;
311  Cnf_Dat_t * pCnf;
312  sat_solver * pSat;
313 // Vec_Int_t * vLits;
314  int i, Iter, status;
315  int nLitsUsed, RetValue = 0;
316  abctime clkStart = Abc_Clock();
317  assert( nFramesMax > 0 );
318  assert( Gia_ManRegNum(p) > 0 );
319 
320  // create miter
321  pTemp = Gia_ManDup( p );
322  pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0, 0 );
323  Gia_ManStop( pTemp );
324  assert( Gia_ManPoNum(pMiter) == 2 * Gia_ManPoNum(p) );
325  assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );
326  // derive CNF
327  if ( fUseOldCnf )
328  pCnf = Cnf_DeriveGiaRemapped( pMiter );
329  else
330  {
331  pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
332  Gia_ManStop( pTemp );
333  pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
334  }
335 /*
336  // collect positive literals
337  vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
338  for ( i = 0; i < Gia_ManRegNum(p); i++ )
339  Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
340 */
341  // derive SAT solver
342  pSat = Bmc_DeriveSolver( p, pMiter, pCnf, nFramesMax, nTimeOut, fVerbose );
343  status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
344  if ( status == l_True )
345  {
346  printf( "I = %4d : ", nFramesMax );
347  printf( "Problem is satisfiable.\n" );
348  sat_solver_delete( pSat );
349  Cnf_DataFree( pCnf );
350  Gia_ManStop( pMiter );
351  return 1;
352  }
353  if ( status == l_Undef )
354  {
355  printf( "ICheck: Timeout reached after %d seconds. \n", nTimeOut );
356  RetValue = 1;
357  goto cleanup;
358  }
359  assert( status == l_False );
360 
361  // count the number of positive literals
362  nLitsUsed = 0;
363  for ( i = 0; i < Gia_ManRegNum(p); i++ )
364  if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
365  nLitsUsed++;
366 
367  // try removing variables
368  for ( Iter = 0; Iter < Gia_ManRegNum(p); Iter++ )
369  {
370  i = fReverse ? Gia_ManRegNum(p) - 1 - Iter : Iter;
371  if ( Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
372  continue;
373  Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits, i)) );
374  status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
375  if ( status == l_Undef )
376  {
377  printf( "ICheck: Timeout reached after %d seconds. \n", nTimeOut );
378  RetValue = 1;
379  goto cleanup;
380  }
381  if ( status == l_True )
382  Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits, i)) );
383  else if ( status == l_False )
384  nLitsUsed--;
385  else assert( 0 );
386  // report the results
387  //printf( "Round %d: ", o );
388  if ( fVerbose )
389  {
390  printf( "I = %4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ",
391  i, (nFramesMax+1) * Gia_ManAndNum(pMiter),
392  Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat),
393  sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
394  ABC_PRTr( "Time", Abc_Clock() - clkStart );
395  fflush( stdout );
396  }
397  }
398  // report the results
399  //printf( "Round %d: ", o );
400  if ( fVerbose )
401  {
402  printf( "M = %4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ",
403  nFramesMax, (nFramesMax+1) * Gia_ManAndNum(pMiter),
404  Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat),
405  sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
406  Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
407  fflush( stdout );
408  }
409 cleanup:
410  // cleanup
411  sat_solver_delete( pSat );
412  Cnf_DataFree( pCnf );
413  Gia_ManStop( pMiter );
414 // Vec_IntFree( vLits );
415  return RetValue;
416 }
417 Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose )
418 {
419  Vec_Int_t * vLits, * vFlops;
420  int i, f;
421  if ( fVerbose )
422  printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n",
423  Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) );
424  fflush( stdout );
425 
426  // collect positive literals
427  vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
428  for ( i = 0; i < Gia_ManRegNum(p); i++ )
429  Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
430 
431  for ( f = 1; f <= nFramesMax; f++ )
432  if ( Bmc_PerformISearchOne( p, f, nTimeOut, fReverse, fVerbose, vLits ) )
433  {
434  Vec_IntFree( vLits );
435  return NULL;
436  }
437 
438  // dump the numbers of the flops
439  if ( fDump )
440  {
441  int nLitsUsed = 0;
442  for ( i = 0; i < Gia_ManRegNum(p); i++ )
443  if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
444  nLitsUsed++;
445  printf( "The set contains %d (out of %d) next-state functions with 0-based numbers:\n", nLitsUsed, Gia_ManRegNum(p) );
446  for ( i = 0; i < Gia_ManRegNum(p); i++ )
447  if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
448  printf( "%d ", i );
449  printf( "\n" );
450  }
451  // save flop indexes
452  vFlops = Vec_IntAlloc( Gia_ManRegNum(p) );
453  for ( i = 0; i < Gia_ManRegNum(p); i++ )
454  if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
455  Vec_IntPush( vFlops, 1 );
456  else
457  Vec_IntPush( vFlops, 0 );
458  Vec_IntFree( vLits );
459  return vFlops;
460 }
461 
462 ////////////////////////////////////////////////////////////////////////
463 /// END OF FILE ///
464 ////////////////////////////////////////////////////////////////////////
465 
466 
467 ABC_NAMESPACE_IMPL_END
468 
sat_solver_set_runtime_limit
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition: giaDup.c:552
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Cnf_Derive
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
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
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Cnf_DeriveGiaRemapped
static ABC_NAMESPACE_IMPL_START Cnf_Dat_t * Cnf_DeriveGiaRemapped(Gia_Man_t *p)
DECLARATIONS ///.
Definition: bmcICheck.c:48
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
Gia_ManName
static char * Gia_ManName(Gia_Man_t *p)
Definition: gia.h:382
Cnf_Dat_t_::nClauses
int nClauses
Definition: cnf.h:61
Gia_ManPo
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
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
sat_solver_add_xor_and
static int sat_solver_add_xor_and(sat_solver *pSat, int iVarF, int iVarA, int iVarB, int iVarC)
Definition: satSolver.h:487
Cnf_Dat_t_::nVars
int nVars
Definition: cnf.h:59
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
sat_solver_nconflicts
int sat_solver_nconflicts(sat_solver *s)
Definition: satSolver.c:1908
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition: cnf.h:63
l_True
#define l_True
Definition: SolverTypes.h:84
sat_solver_add_xor
static int sat_solver_add_xor(sat_solver *pSat, int iVarA, int iVarB, int iVarC, int fCompl)
Definition: satSolver.h:346
Bmc_PerformISearchOne
int Bmc_PerformISearchOne(Gia_Man_t *p, int nFramesMax, int nTimeOut, int fReverse, int fVerbose, Vec_Int_t *vLits)
Definition: bmcICheck.c:307
Jf_ManDeriveCnf
Gia_Man_t * Jf_ManDeriveCnf(Gia_Man_t *p, int fCnfObjIds)
Definition: giaJf.c:1746
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Cnf_Dat_t_
Definition: cnf.h:56
Gia_Obj_t_
Definition: gia.h:75
sat_solver_add_buffer
static int sat_solver_add_buffer(sat_solver *pSat, int iVarA, int iVarB, int fCompl)
Definition: satSolver.h:288
sat_solver_final
static int sat_solver_final(sat_solver *s, int **ppArray)
Definition: satSolver.h:227
Bmc_DeriveSolver
sat_solver * Bmc_DeriveSolver(Gia_Man_t *p, Gia_Man_t *pMiter, Cnf_Dat_t *pCnf, int nFramesMax, int nTimeOut, int fVerbose)
Definition: bmcICheck.c:91
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Cnf_Dat_t_::pClauses
int ** pClauses
Definition: cnf.h:62
Bmc_PerformISearch
Vec_Int_t * Bmc_PerformISearch(Gia_Man_t *p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose)
Definition: bmcICheck.c:417
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
ABC_PRTr
#define ABC_PRTr(a, t)
Definition: abc_global.h:221
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Gia_Man_t_::pData
void * pData
Definition: gia.h:169
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Cnf_DataLiftGia
static void Cnf_DataLiftGia(Cnf_Dat_t *p, Gia_Man_t *pGia, int nVarsPlus)
Definition: bmcICheck.c:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Bmc_PerformICheck
void Bmc_PerformICheck(Gia_Man_t *p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose)
Definition: bmcICheck.c:196
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Gia_Man_t_
Definition: gia.h:95
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
l_False
#define l_False
Definition: SolverTypes.h:85
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
sat_solver_t
Definition: satSolver.h:91
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
sat_solver_add_buffer_enable
static int sat_solver_add_buffer_enable(sat_solver *pSat, int iVarA, int iVarB, int iVarEn, int fCompl)
Definition: satSolver.h:305
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Cnf_Dat_t_::nLiterals
int nLiterals
Definition: cnf.h:60
Gia_ManMiter
Gia_Man_t * Gia_ManMiter(Gia_Man_t *pAig0, Gia_Man_t *pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose)
Definition: giaDup.c:2128
Gia_ManRi
static Gia_Obj_t * Gia_ManRi(Gia_Man_t *p, int v)
Definition: gia.h:408
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387