diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-11-09 08:33:56 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-11-09 08:33:56 -0800 |
| commit | 58c2584e2a667e8fa95e2fe093c2b6f7c491c139 (patch) | |
| tree | 48c1823c833b389385c8de765b202176e416e72d /src/sat | |
| parent | 236118c0b68f0c22123e1547c7a86c5c8ee2844f (diff) | |
| download | abc-58c2584e2a667e8fa95e2fe093c2b6f7c491c139.tar.gz abc-58c2584e2a667e8fa95e2fe093c2b6f7c491c139.tar.bz2 abc-58c2584e2a667e8fa95e2fe093c2b6f7c491c139.zip | |
Improvements to 'satclp'.
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bmc/bmcClp.c | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c index fbff7679..f7d43e60 100644 --- a/src/sat/bmc/bmcClp.c +++ b/src/sat/bmc/bmcClp.c @@ -1103,6 +1103,7 @@ Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat1, sat_solver * pSat2, int nV Vec_StrWriteEntry( vSop[n], Start + nVars + 2, '\n' ); Vec_StrWriteEntry( vSop[n], Start + nVars + 3, '\0' ); Vec_IntClear( vCube ); + Vec_IntPush( vCube, Abc_Var2Lit( iOOVars[n], 0 ) ); Vec_IntForEachEntry( vNums, iVar, v ) { int iLit = Vec_IntEntry( vLits, iVar ); @@ -1113,7 +1114,6 @@ Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat1, sat_solver * pSat2, int nV Vec_StrWriteEntry( vSop[n], Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) ); } // add cube - Vec_IntPush( vCube, Abc_Var2Lit( iOOVars[n], 0 ) ); // status = sat_solver_addclause( pSat, Vec_IntArray(vCube), Vec_IntLimit(vCube) ); status = sat_solver_addclause( pSat[n], Vec_IntArray(vCube), Vec_IntLimit(vCube) ); if ( status == 0 ) @@ -1230,8 +1230,8 @@ Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, int nVars, int nCubeLim, int if ( fVeryVerbose ) clk = Abc_Clock(); // get the assignment sat_solver_clean_polarity( pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) ); - pLits[0] = Abc_Var2Lit( iOOVars[n], 1 ); // enable clauses - pLits[1] = Abc_Var2Lit( iOutVar, n ); // set output + pLits[0] = Abc_Var2Lit( iOutVar, n ); // set output + pLits[1] = Abc_Var2Lit( iOOVars[n], 1 ); // enable clauses status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 ); if ( fVeryVerbose ) Time[n][0] += Abc_Clock() - clk; if ( status == l_Undef ) |