diff options
Diffstat (limited to 'src/aig/dch/dchSat.c')
-rw-r--r-- | src/aig/dch/dchSat.c | 101 |
1 files changed, 100 insertions, 1 deletions
diff --git a/src/aig/dch/dchSat.c b/src/aig/dch/dchSat.c index 0d81991f..19aaffee 100644 --- a/src/aig/dch/dchSat.c +++ b/src/aig/dch/dchSat.c @@ -30,7 +30,7 @@ /**Function************************************************************* - Synopsis [] + Synopsis [Runs equivalence test for the two nodes.] Description [] @@ -39,6 +39,105 @@ SeeAlso [] ***********************************************************************/ +int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) +{ + int nBTLimit = p->pPars->nBTLimit; + int pLits[2], RetValue, RetValue1, status, clk; + p->nSatCalls++; + + // sanity checks + assert( !Aig_IsComplement(pNew) ); + assert( !Aig_IsComplement(pOld) ); + assert( pNew != pOld ); + + // check if SAT solver needs recycling + if ( p->pSat == NULL || (p->pPars->nSatVarMax && p->nSatVars > p->pPars->nSatVarMax) ) + Dch_ManSatSolverRecycle( p ); + + // if the nodes do not have SAT variables, allocate them + Dch_CnfNodeAddToSolver( p, pOld ); + Dch_CnfNodeAddToSolver( p, pNew ); + + // propage unit clauses + if ( p->pSat->qtail != p->pSat->qhead ) + { + status = sat_solver_simplify(p->pSat); + assert( status != 0 ); + assert( p->pSat->qtail == p->pSat->qhead ); + } + + // solve under assumptions + // 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 ); +//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); +clk = clock(); + RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, + (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); +p->timeSat += clock() - clk; + if ( RetValue1 == l_False ) + { +p->timeSatUnsat += clock() - clk; + pLits[0] = lit_neg( pLits[0] ); + pLits[1] = lit_neg( pLits[1] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + p->nSatCallsUnsat++; + } + else if ( RetValue1 == l_True ) + { +p->timeSatSat += clock() - clk; + p->nSatCallsSat++; + return 0; + } + else // if ( RetValue1 == l_Undef ) + { +p->timeSatUndec += clock() - clk; + p->nSatFailsReal++; + return -1; + } + + // if the old node was constant 0, we already know the answer + if ( pOld == Aig_ManConst1(p->pAigFraig) ) + { + p->nSatProof++; + return 1; + } + + // solve under assumptions + // 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 ); +clk = clock(); + RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, + (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); +p->timeSat += clock() - clk; + if ( RetValue1 == l_False ) + { +p->timeSatUnsat += clock() - clk; + pLits[0] = lit_neg( pLits[0] ); + pLits[1] = lit_neg( pLits[1] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + p->nSatCallsUnsat++; + } + else if ( RetValue1 == l_True ) + { +p->timeSatSat += clock() - clk; + p->nSatCallsSat++; + return 0; + } + else // if ( RetValue1 == l_Undef ) + { +p->timeSatUndec += clock() - clk; + p->nSatFailsReal++; + return -1; + } + // return SAT proof + p->nSatProof++; + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |