diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-03-05 23:00:30 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-03-05 23:00:30 -0800 |
| commit | 6da21b8b884632c901ae10955e23c0c8206e7e58 (patch) | |
| tree | 29e14c72c7e6e2bf2780268a7ed9390f88b56a5d /src/sat/bmc/bmcEco.c | |
| parent | ddc522a0c03ead1f84e45e515105a750f84ff265 (diff) | |
| download | abc-6da21b8b884632c901ae10955e23c0c8206e7e58.tar.gz abc-6da21b8b884632c901ae10955e23c0c8206e7e58.tar.bz2 abc-6da21b8b884632c901ae10955e23c0c8206e7e58.zip | |
Experiments with SAT-based cube enumeration.
Diffstat (limited to 'src/sat/bmc/bmcEco.c')
| -rw-r--r-- | src/sat/bmc/bmcEco.c | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/sat/bmc/bmcEco.c b/src/sat/bmc/bmcEco.c index c4fc3ba8..07fdd704 100644 --- a/src/sat/bmc/bmcEco.c +++ b/src/sat/bmc/bmcEco.c @@ -138,7 +138,6 @@ static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p ) int Bmc_EcoSolve( sat_solver * pSat, int Root, Vec_Int_t * vVars ) { int nBTLimit = 1000000; - Vec_Int_t * vValues = Vec_IntAlloc( Vec_IntSize(vVars) ); Vec_Int_t * vLits = Vec_IntAlloc( Vec_IntSize(vVars) ); int status, i, Div, iVar, nFinal, * pFinal, nIter = 0, RetValue = 0; int pLits[2], nVars = sat_solver_nvars( pSat ); @@ -154,10 +153,6 @@ int Bmc_EcoSolve( sat_solver * pSat, int Root, Vec_Int_t * vVars ) if ( status == l_False ) { RetValue = 1; break; } assert( status == l_True ); - // remember variable values - Vec_IntClear( vValues ); - Vec_IntForEachEntry( vVars, iVar, i ) - Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) ); // collect divisor literals Vec_IntClear( vLits ); Vec_IntPush( vLits, Abc_LitNot(pLits[0]) ); // F = 0 @@ -189,7 +184,6 @@ int Bmc_EcoSolve( sat_solver * pSat, int Root, Vec_Int_t * vVars ) nIter++; } // assert( status == l_True ); - Vec_IntFree( vValues ); Vec_IntFree( vLits ); return RetValue; } |