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                                ///