diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-03-01 13:59:23 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-03-01 13:59:23 -0800 |
| commit | bd9b7d64e1131f45699a5a4b20b4bf44795da857 (patch) | |
| tree | 3e6a6b9f243519bf31635e3efb9bf85bf450b201 /src/sat/bmc | |
| parent | b71d2ab2ba4dd1da265845a94439c36a38e9d8d3 (diff) | |
| download | abc-bd9b7d64e1131f45699a5a4b20b4bf44795da857.tar.gz abc-bd9b7d64e1131f45699a5a4b20b4bf44795da857.tar.bz2 abc-bd9b7d64e1131f45699a5a4b20b4bf44795da857.zip | |
Adding efficient procedure to minimize the set of assumptions.
Diffstat (limited to 'src/sat/bmc')
| -rw-r--r-- | src/sat/bmc/bmcClp.c | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c index cfc608b1..2ac94da5 100644 --- a/src/sat/bmc/bmcClp.c +++ b/src/sat/bmc/bmcClp.c @@ -353,11 +353,37 @@ int Bmc_CollapseIrredundantFull( Vec_Str_t * vSop, int nCubes, int nVars ) SeeAlso [] ***********************************************************************/ +int Bmc_CollapseExpandRound2( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTemp, int nBTLimit, int fOnOffSetLit ) +{ + // put into new array + int i, iLit, nLits; + Vec_IntClear( vTemp ); + Vec_IntForEachEntry( vLits, iLit, i ) + if ( iLit != -1 ) + Vec_IntPush( vTemp, iLit ); + assert( Vec_IntSize(vTemp) > 0 ); + // assume condition literal + if ( fOnOffSetLit >= 0 ) + sat_solver_push( pSat, fOnOffSetLit ); + // minimize + nLits = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vTemp), Vec_IntSize(vTemp), nBTLimit ); + Vec_IntShrink( vTemp, nLits ); + // assume conditional literal + if ( fOnOffSetLit >= 0 ) + sat_solver_pop( pSat ); + // modify output literas + Vec_IntForEachEntry( vLits, iLit, i ) + if ( iLit != -1 && Vec_IntFind(vTemp, iLit) == -1 ) + Vec_IntWriteEntry( vLits, i, -1 ); + return 0; +} + int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon, int fOnOffSetLit ) { int fProfile = 0; int k, n, iLit, status; abctime clk; + //return Bmc_CollapseExpandRound2( pSat, vLits, vTemp, nBTLimit, fOnOffSetLit ); // try removing one literal at a time for ( k = Vec_IntSize(vLits) - 1; k >= 0; k-- ) { |