diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-08-02 20:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-08-02 20:01:00 -0700 |
| commit | b8dea8ff0510ee7be465f5fe50994ecb58b9b30a (patch) | |
| tree | bfa6f6d88e01d51a9b1224a03e199c0efd199898 /src/aig/dch/dchSat.c | |
| parent | cbb7ff8642236fbc21576dec7b57b9e4cb7e60ef (diff) | |
| download | abc-b8dea8ff0510ee7be465f5fe50994ecb58b9b30a.tar.gz abc-b8dea8ff0510ee7be465f5fe50994ecb58b9b30a.tar.bz2 abc-b8dea8ff0510ee7be465f5fe50994ecb58b9b30a.zip | |
Version abc80802_2
Diffstat (limited to 'src/aig/dch/dchSat.c')
| -rw-r--r-- | src/aig/dch/dchSat.c | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/src/aig/dch/dchSat.c b/src/aig/dch/dchSat.c index 19aaffee..e0a446f8 100644 --- a/src/aig/dch/dchSat.c +++ b/src/aig/dch/dchSat.c @@ -51,7 +51,10 @@ int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) assert( pNew != pOld ); // check if SAT solver needs recycling - if ( p->pSat == NULL || (p->pPars->nSatVarMax && p->nSatVars > p->pPars->nSatVarMax) ) + if ( p->pSat == NULL || + (p->pPars->nSatVarMax && + p->nSatVars > p->pPars->nSatVarMax && + ++p->nCallsSince > p->pPars->nCallsRecycle) ) Dch_ManSatSolverRecycle( p ); // if the nodes do not have SAT variables, allocate them @@ -70,6 +73,11 @@ int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) // A = 1; B = 0 OR A = 1; B = 1 pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 0 ); pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase ); + if ( p->pPars->fPolarFlip ) + { + if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] ); + } //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); clk = clock(); RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, @@ -108,6 +116,11 @@ p->timeSatUndec += clock() - clk; // A = 0; B = 1 OR A = 0; B = 0 pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 1 ); pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase ); + if ( p->pPars->fPolarFlip ) + { + if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); + if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] ); + } clk = clock(); RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); |