abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bmcBmci.c File Reference
#include "bmc.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "aig/gia/giaAig.h"

Go to the source code of this file.

Functions

static
ABC_NAMESPACE_IMPL_START
Cnf_Dat_t
Cnf_DeriveGiaRemapped (Gia_Man_t *p)
 DECLARATIONS ///. More...
 
static void Cnf_DataLiftGia (Cnf_Dat_t *p, Gia_Man_t *pGia, int nVarsPlus)
 
void Bmc_BmciUnfold (Gia_Man_t *pNew, Gia_Man_t *p, Vec_Int_t *vFFLits, int fPiReuse)
 
int Bmc_BmciPart_rec (Gia_Man_t *pNew, Vec_Int_t *vSatMap, int iIdNew, Gia_Man_t *pPart, Vec_Int_t *vPartMap, Vec_Int_t *vCopies)
 
Gia_Man_tBmc_BmciPart (Gia_Man_t *pNew, Vec_Int_t *vSatMap, Vec_Int_t *vMiters, Vec_Int_t *vPartMap, Vec_Int_t *vCopies)
 
int Bmc_BmciPerform (Gia_Man_t *p, Vec_Int_t *vInit0, Vec_Int_t *vInit1, int nFrames, int nWords, int nTimeOut, int fVerbose)
 
int Gia_ManBmciTest (Gia_Man_t *p, Vec_Int_t *vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose)
 

Function Documentation

Gia_Man_t* Bmc_BmciPart ( Gia_Man_t pNew,
Vec_Int_t vSatMap,
Vec_Int_t vMiters,
Vec_Int_t vPartMap,
Vec_Int_t vCopies 
)

Definition at line 141 of file bmcBmci.c.

142 {
143  Gia_Man_t * pPart;
144  int i, iLit, iLitPart;
145  Vec_IntFill( vCopies, Gia_ManObjNum(pNew), 0 );
146  Vec_IntFillExtra( vSatMap, Gia_ManObjNum(pNew), -1 );
147  pPart = Gia_ManStart( 1000 );
148  pPart->pName = Abc_UtilStrsav( pNew->pName );
149  Vec_IntClear( vPartMap );
150  Vec_IntPush( vPartMap, 0 );
151  Vec_IntForEachEntry( vMiters, iLit, i )
152  {
153  if ( iLit == -1 )
154  continue;
155  assert( iLit >= 2 );
156  iLitPart = Bmc_BmciPart_rec( pNew, vSatMap, Abc_Lit2Var(iLit), pPart, vPartMap, vCopies );
157  Gia_ManAppendCo( pPart, Abc_LitNotCond(iLitPart, Abc_LitIsCompl(iLit)) );
158  Vec_IntPush( vPartMap, -1 );
159  }
160  assert( Gia_ManPoNum(pPart) > 0 );
161  assert( Vec_IntSize(vPartMap) == Gia_ManObjNum(pPart) );
162  return pPart;
163 }
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
static void Vec_IntFillExtra(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:376
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
char * pName
Definition: gia.h:97
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
int Bmc_BmciPart_rec(Gia_Man_t *pNew, Vec_Int_t *vSatMap, int iIdNew, Gia_Man_t *pPart, Vec_Int_t *vPartMap, Vec_Int_t *vCopies)
Definition: bmcBmci.c:118
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Definition: gia.h:95
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
int Bmc_BmciPart_rec ( Gia_Man_t pNew,
Vec_Int_t vSatMap,
int  iIdNew,
Gia_Man_t pPart,
Vec_Int_t vPartMap,
Vec_Int_t vCopies 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 118 of file bmcBmci.c.

119 {
120  Gia_Obj_t * pObj = Gia_ManObj( pNew, iIdNew );
121  int iLitPart0, iLitPart1, iRes;
122  if ( Vec_IntEntry(vCopies, iIdNew) )
123  return Vec_IntEntry(vCopies, iIdNew);
124  if ( Vec_IntEntry(vSatMap, iIdNew) >= 0 || Gia_ObjIsCi(pObj) )
125  {
126  Vec_IntPush( vPartMap, iIdNew );
127  iRes = Gia_ManAppendCi(pPart);
128  Vec_IntWriteEntry( vCopies, iIdNew, iRes );
129  return iRes;
130  }
131  assert( Gia_ObjIsAnd(pObj) );
132  iLitPart0 = Bmc_BmciPart_rec( pNew, vSatMap, Gia_ObjFaninId0(pObj, iIdNew), pPart, vPartMap, vCopies );
133  iLitPart1 = Bmc_BmciPart_rec( pNew, vSatMap, Gia_ObjFaninId1(pObj, iIdNew), pPart, vPartMap, vCopies );
134  iLitPart0 = Abc_LitNotCond( iLitPart0, Gia_ObjFaninC0(pObj) );
135  iLitPart1 = Abc_LitNotCond( iLitPart1, Gia_ObjFaninC1(pObj) );
136  Vec_IntPush( vPartMap, iIdNew );
137  iRes = Gia_ManAppendAnd( pPart, iLitPart0, iLitPart1 );
138  Vec_IntWriteEntry( vCopies, iIdNew, iRes );
139  return iRes;
140 }
static int Gia_ManAppendAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: gia.h:592
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Definition: gia.h:75
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
int Bmc_BmciPart_rec(Gia_Man_t *pNew, Vec_Int_t *vSatMap, int iIdNew, Gia_Man_t *pPart, Vec_Int_t *vPartMap, Vec_Int_t *vCopies)
Definition: bmcBmci.c:118
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
#define assert(ex)
Definition: util_old.h:213
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
int Bmc_BmciPerform ( Gia_Man_t p,
Vec_Int_t vInit0,
Vec_Int_t vInit1,
int  nFrames,
int  nWords,
int  nTimeOut,
int  fVerbose 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 176 of file bmcBmci.c.

177 {
178  int nSatVars = 1;
179  Vec_Int_t * vLits0, * vLits1, * vMiters, * vSatMap, * vPartMap, * vCopies;
180  Gia_Man_t * pNew, * pPart;
181  Gia_Obj_t * pObj;
182  Cnf_Dat_t * pCnf;
183  sat_solver * pSat;
184  int iVar0, iVar1, iLit, iLit0, iLit1;
185  int i, f, status, nChanges, nMiters, RetValue = 1;
186  assert( Vec_IntSize(vInit0) == Gia_ManRegNum(p) );
187  assert( Vec_IntSize(vInit1) == Gia_ManRegNum(p) );
188 
189  // start the SAT solver
190  pSat = sat_solver_new();
191  sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
192 
193  pNew = Gia_ManStart( 10000 );
194  pNew->pName = Abc_UtilStrsav( p->pName );
195  Gia_ManHashAlloc( pNew );
196  Gia_ManConst0(p)->Value = 0;
197 
198  vLits0 = Vec_IntAlloc( Gia_ManRegNum(p) );
199  Vec_IntForEachEntry( vInit0, iLit, i )
200  Vec_IntPush( vLits0, iLit < 2 ? iLit : Gia_ManAppendCi(pNew) );
201 
202  vLits1 = Vec_IntAlloc( Gia_ManRegNum(p) );
203  Vec_IntForEachEntry( vInit1, iLit, i )
204  Vec_IntPush( vLits1, iLit < 2 ? iLit : Gia_ManAppendCi(pNew) );
205 
206  vMiters = Vec_IntAlloc( 1000 );
207  vSatMap = Vec_IntAlloc( 1000 );
208  vPartMap = Vec_IntAlloc( 1000 );
209  vCopies = Vec_IntAlloc( 1000 );
210  for ( f = 0; f < nFrames; f++ )
211  {
212  abctime clk = Abc_Clock();
213  Bmc_BmciUnfold( pNew, p, vLits0, 0 );
214  Bmc_BmciUnfold( pNew, p, vLits1, 1 );
215  assert( Vec_IntSize(vLits0) == Vec_IntSize(vLits1) );
216  nMiters = 0;
217  Vec_IntClear( vMiters );
218  Vec_IntForEachEntryTwo( vLits0, vLits1, iLit0, iLit1, i )
219  if ( (iLit0 >= 2 || iLit1 >= 2) && iLit0 != iLit1 )
220  Vec_IntPush( vMiters, Gia_ManHashXor(pNew, iLit0, iLit1) ), nMiters++;
221  else
222  Vec_IntPush( vMiters, -1 );
223  assert( Vec_IntSize(vMiters) == Gia_ManRegNum(p) );
224  if ( Vec_IntSum(vMiters) + Vec_IntSize(vLits1) == 0 )
225  {
226  if ( fVerbose )
227  printf( "Reached a fixed point after %d frames. \n", f+1 );
228  break;
229  }
230  // create new part
231  pPart = Bmc_BmciPart( pNew, vSatMap, vMiters, vPartMap, vCopies );
232  pCnf = Cnf_DeriveGiaRemapped( pPart );
233  Cnf_DataLiftGia( pCnf, pPart, nSatVars );
234  nSatVars += pCnf->nVars;
235  sat_solver_setnvars( pSat, nSatVars );
236  for ( i = 0; i < pCnf->nClauses; i++ )
237  if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
238  assert( 0 );
239  // stitch the clauses
240  Gia_ManForEachPi( pPart, pObj, i )
241  {
242  iVar0 = pCnf->pVarNums[Gia_ObjId(pPart, pObj)];
243  iVar1 = Vec_IntEntry( vSatMap, Vec_IntEntry(vPartMap, Gia_ObjId(pPart, pObj)) );
244  if ( iVar1 == -1 )
245  continue;
246  sat_solver_add_buffer( pSat, iVar0, iVar1, 0 );
247  }
248  // transfer variables
249  Gia_ManForEachCand( pPart, pObj, i )
250  if ( pCnf->pVarNums[i] >= 0 )
251  {
252  assert( Gia_ObjIsCi(pObj) || Vec_IntEntry( vSatMap, Vec_IntEntry(vPartMap, i) ) == -1 );
253  Vec_IntWriteEntry( vSatMap, Vec_IntEntry(vPartMap, i), pCnf->pVarNums[i] );
254  }
255  Cnf_DataFree( pCnf );
256  Gia_ManStop( pPart );
257  // perform runs
258  nChanges = 0;
259  Vec_IntForEachEntry( vMiters, iLit, i )
260  {
261  if ( iLit == -1 )
262  continue;
263  assert( Vec_IntEntry(vSatMap, Abc_Lit2Var(iLit)) > 0 );
264  iLit = Abc_Lit2LitV( Vec_IntArray(vSatMap), iLit );
265  status = sat_solver_solve( pSat, &iLit, &iLit + 1, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
266  if ( status == l_True )
267  {
268  nChanges++;
269  continue;
270  }
271  if ( status == l_Undef )
272  {
273  printf( "Timeout reached after %d seconds. \n", nTimeOut );
274  RetValue = 0;
275  goto cleanup;
276  }
277  assert( status == l_False );
278  iLit0 = Vec_IntEntry( vLits0, i );
279  iLit1 = Vec_IntEntry( vLits1, i );
280  assert( (iLit0 >= 2 || iLit1 >= 2) && iLit0 != iLit1 );
281  if ( iLit1 >= 2 )
282  Vec_IntWriteEntry( vLits1, i, iLit0 );
283  else
284  Vec_IntWriteEntry( vLits0, i, iLit1 );
285  iLit0 = Vec_IntEntry( vLits0, i );
286  iLit1 = Vec_IntEntry( vLits1, i );
287  assert( iLit0 == iLit1 );
288  }
289  if ( fVerbose )
290  {
291  printf( "Frame %4d : ", f+1 );
292  printf( "Vars =%7d ", nSatVars );
293  printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
294  printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
295  printf( "AIG =%7d ", Gia_ManAndNum(pNew) );
296  printf( "Miters =%5d ", nMiters );
297  printf( "SAT =%5d ", nChanges );
298  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
299  }
300  if ( nChanges == 0 )
301  {
302  printf( "Reached a fixed point after %d frames. \n", f+1 );
303  break;
304  }
305  }
306 cleanup:
307 
308  sat_solver_delete( pSat );
309  Gia_ManStopP( &pNew );
310  Vec_IntFree( vLits0 );
311  Vec_IntFree( vLits1 );
312  Vec_IntFree( vMiters );
313  Vec_IntFree( vSatMap );
314  Vec_IntFree( vPartMap );
315  Vec_IntFree( vCopies );
316  return RetValue;
317 }
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
Gia_Man_t * Bmc_BmciPart(Gia_Man_t *pNew, Vec_Int_t *vSatMap, Vec_Int_t *vMiters, Vec_Int_t *vPartMap, Vec_Int_t *vCopies)
Definition: bmcBmci.c:141
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static int Abc_Lit2LitV(int *pMap, int Lit)
Definition: abc_global.h:269
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
int Gia_ManHashXor(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:658
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
#define l_Undef
Definition: SolverTypes.h:86
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
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
int nVars
Definition: cnf.h:59
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
int sat_solver_nconflicts(sat_solver *s)
Definition: satSolver.c:1908
int * pVarNums
Definition: cnf.h:63
#define l_True
Definition: SolverTypes.h:84
static abctime Abc_Clock()
Definition: abc_global.h:279
Definition: cnf.h:56
for(p=first;p->value< newval;p=p->next)
Definition: gia.h:75
static int sat_solver_add_buffer(sat_solver *pSat, int iVarA, int iVarB, int fCompl)
Definition: satSolver.h:288
void Gia_ManStopP(Gia_Man_t **p)
Definition: giaMan.c:177
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
void Bmc_BmciUnfold(Gia_Man_t *pNew, Gia_Man_t *p, Vec_Int_t *vFFLits, int fPiReuse)
Definition: bmcBmci.c:91
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
int ** pClauses
Definition: cnf.h:62
char * pName
Definition: gia.h:97
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
if(last==0)
Definition: sparse_int.h:34
else
Definition: sparse_int.h:55
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
#define Vec_IntForEachEntryTwo(vVec1, vVec2, Entry1, Entry2, i)
Definition: vecInt.h:64
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static ABC_NAMESPACE_IMPL_START Cnf_Dat_t * Cnf_DeriveGiaRemapped(Gia_Man_t *p)
DECLARATIONS ///.
Definition: bmcBmci.c:48
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
#define Gia_ManForEachCand(p, pObj, i)
Definition: gia.h:1008
int sat_solver_nclauses(sat_solver *s)
Definition: satSolver.c:1902
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static int Vec_IntSum(Vec_Int_t *p)
Definition: vecInt.h:1137
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
#define l_False
Definition: SolverTypes.h:85
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
static void Cnf_DataLiftGia(Cnf_Dat_t *p, Gia_Man_t *pGia, int nVarsPlus)
Definition: bmcBmci.c:69
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
ABC_INT64_T abctime
Definition: abc_global.h:278
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
void Bmc_BmciUnfold ( Gia_Man_t pNew,
Gia_Man_t p,
Vec_Int_t vFFLits,
int  fPiReuse 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 91 of file bmcBmci.c.

92 {
93  Gia_Obj_t * pObj;
94  int i;
95  assert( Gia_ManRegNum(p) == Vec_IntSize(vFFLits) );
96  Gia_ManConst0(p)->Value = 0;
97  Gia_ManForEachRo( p, pObj, i )
98  pObj->Value = Vec_IntEntry(vFFLits, i);
99  Gia_ManForEachPi( p, pObj, i )
100  pObj->Value = fPiReuse ? Gia_ObjToLit(pNew, Gia_ManPi(pNew, Gia_ManPiNum(pNew)-Gia_ManPiNum(p)+i)) : Gia_ManAppendCi(pNew);
101  Gia_ManForEachAnd( p, pObj, i )
102  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
103  Gia_ManForEachRi( p, pObj, i )
104  Vec_IntWriteEntry( vFFLits, i, Gia_ObjFanin0Copy(pObj) );
105 }
static int Gia_ObjToLit(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:497
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Definition: gia.h:75
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static Gia_Obj_t * Gia_ManPi(Gia_Man_t *p, int v)
Definition: gia.h:405
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
static void Cnf_DataLiftGia ( Cnf_Dat_t p,
Gia_Man_t pGia,
int  nVarsPlus 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 69 of file bmcBmci.c.

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 }
for(p=first;p->value< newval;p=p->next)
Definition: gia.h:75
if(last==0)
Definition: sparse_int.h:34
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
static ABC_NAMESPACE_IMPL_START Cnf_Dat_t* Cnf_DeriveGiaRemapped ( Gia_Man_t p)
inlinestatic

DECLARATIONS ///.

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

FileName [bmcBmci.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
bmcBmci.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file bmcBmci.c.

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 }
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
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
Definition: cnf.h:56
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
int Gia_ManBmciTest ( Gia_Man_t p,
Vec_Int_t vInit,
int  nFrames,
int  nWords,
int  nTimeOut,
int  fSim,
int  fVerbose 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 330 of file bmcBmci.c.

331 {
332  Vec_Int_t * vInit0 = Vec_IntStart( Gia_ManRegNum(p) );
333  Bmc_BmciPerform( p, vInit, vInit0, nFrames, nWords, nTimeOut, fVerbose );
334  Vec_IntFree( vInit0 );
335  return 1;
336 }
int Bmc_BmciPerform(Gia_Man_t *p, Vec_Int_t *vInit0, Vec_Int_t *vInit1, int nFrames, int nWords, int nTimeOut, int fVerbose)
Definition: bmcBmci.c:176
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
int nWords
Definition: abcNpn.c:127
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387