Skip to content

A
abc
Commit 241b042f by Alan Mishchenko
Options

Experiments with SAT-based cube enumeration.

parent 1961f179
Showing with 1 additions and 1 deletions
src/sat/bmc/bmcFx.c
...@@ -558,7 +558,7 @@ int Bmc_FxCompute( Gia_Man_t * p ) ...@@ -558,7 +558,7 @@ int Bmc_FxCompute( Gia_Man_t * p )
int nOuts = Gia_ManCoNum(p); int nOuts = Gia_ManCoNum(p);
int nCiVars = Gia_ManCiNum(p), iCiVarBeg = pCnf->nVars - nCiVars;// - 1; int nCiVars = Gia_ManCiNum(p), iCiVarBeg = pCnf->nVars - nCiVars;// - 1;
int o, i, n, RetValue, nCounter, iAuxVarStart = sat_solver_nvars( pSat ); int o, i, n, RetValue, nCounter, iAuxVarStart = sat_solver_nvars( pSat );
int nCubes[2][2] = {0}; int nCubes[2][2] = {{0}};
// create variables // create variables
Vec_Int_t * vVars = Vec_IntAlloc( nCiVars ); Vec_Int_t * vVars = Vec_IntAlloc( nCiVars );
for ( n = 0; n < nCiVars; n++ ) for ( n = 0; n < nCiVars; n++ )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment