From b8dea8ff0510ee7be465f5fe50994ecb58b9b30a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 2 Aug 2008 20:01:00 -0700 Subject: Version abc80802_2 --- src/aig/dch/dchSat.c | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) (limited to 'src/aig/dch/dchSat.c') 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 ); -- cgit v1.2.3