SAT sweeping under constraints.

6 files changed, 98 insertions, 39 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2f785a22..b15b5b04 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27186,14 +27186,15 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9CFraig(): There is no AIG.\n" );
         return 1;
     }
-    Abc_Print( 0, "Current AIG contains %d constraints.\n", pAbc->pGia->nConstrs );
     pTemp = Ssc_PerformSweepingConstr( pAbc->pGia, pPars );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
     Abc_Print( -2, "usage: &cfraig [-WC <num>] [-rmdwvh]\n" );
-    Abc_Print( -2, "\t         performs conditional combinational SAT sweeping\n" );
+    Abc_Print( -2, "\t         performs combinational SAT sweeping under constraints\n" );
+    Abc_Print( -2, "\t         which are present in the AIG or set manually using \"constr\"\n" );
+    Abc_Print( -2, "\t         (constraints are listed as last POs and true when they are 0)\n" );
     Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
diff --git a/src/proof/ssc/sscClass.c b/src/proof/ssc/sscClass.c
index 308fbada..a9904148 100644
--- a/src/proof/ssc/sscClass.c
+++ b/src/proof/ssc/sscClass.c
@@ -257,8 +257,8 @@ void Ssc_GiaClassesCheckPairs( Gia_Man_t * p, Vec_Int_t * vDisPairs )
     Vec_IntForEachEntryDouble( vDisPairs, iRepr, iObj, i )
         if ( iRepr == Gia_ObjRepr(p, iObj) )
             printf( "Pair (%d, %d) are still equivalent.\n", iRepr, iObj ), Result = 0;
-    if ( Result )
-        printf( "Classes are refined correctly.\n" );
+//    if ( Result )
+//        printf( "Classes are refined correctly.\n" );
 }
 
 
diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c
index 1aada663..00491e31 100644
--- a/src/proof/ssc/sscCore.c
+++ b/src/proof/ssc/sscCore.c
@@ -52,7 +52,6 @@ void Ssc_ManSetDefaultParams( Ssc_Pars_t * p )
     p->fVerbose       =     0;  // verbose stats
 }
 
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -104,7 +103,7 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar
         return NULL;
     }
     sat_solver_bookmark( p->pSat );
-    Vec_IntPrint( p->vPivot );
+//    Vec_IntPrint( p->vPivot );
     Gia_ManSetPhasePattern( p->pAig, p->vPivot );
     Gia_ManSetPhasePattern( p->pCare, p->vPivot );
     if ( Gia_ManCheckCoPhase(p->pCare) )
@@ -121,6 +120,26 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar
     Ssc_GiaClassesInit( pAig );
     return p;
 }
+void Ssc_ManPrintStats( Ssc_Man_t * p )
+{
+    Abc_Print( 1, "Parameters: SimWords = %d. SatConfs = %d. SatVarMax = %d. CallsRec = %d. Verbose = %d.\n",
+        p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax, p->pPars->nCallsRecycle, p->pPars->fVerbose );
+    Abc_Print( 1, "SAT calls : Total = %d. Proof = %d. Cex = %d. Undec = %d.\n",
+        p->nSatCalls, p->nSatCallsUnsat, p->nSatCallsSat, p->nSatCallsUndec );
+    Abc_Print( 1, "SAT solver: Vars = %d. Clauses = %d. Recycles = %d. Sim rounds = %d.\n",
+        sat_solver_nvars(p->pSat), sat_solver_nclauses(p->pSat), p->nRecycles, p->nSimRounds );
+
+    p->timeOther = p->timeTotal - p->timeSimInit - p->timeSimSat - p->timeCnfGen - p->timeSatSat - p->timeSatUnsat - p->timeSatUndec;
+    ABC_PRTP( "Initialization ", p->timeSimInit,            p->timeTotal );
+    ABC_PRTP( "SAT simulation ", p->timeSimSat,             p->timeTotal );
+    ABC_PRTP( "CNF generation ", p->timeSimSat,             p->timeTotal );
+    ABC_PRTP( "SAT solving    ", p->timeSat-p->timeCnfGen,  p->timeTotal );
+    ABC_PRTP( "  unsat        ", p->timeSatUnsat,           p->timeTotal );
+    ABC_PRTP( "  sat          ", p->timeSatSat,             p->timeTotal );
+    ABC_PRTP( "  undecided    ", p->timeSatUndec,           p->timeTotal );
+    ABC_PRTP( "Other          ", p->timeOther,              p->timeTotal );
+    ABC_PRTP( "TOTAL          ", p->timeTotal,              p->timeTotal );
+}
 
 /**Function*************************************************************
 
@@ -140,6 +159,7 @@ Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t
     Gia_Obj_t * pObj, * pRepr;
     clock_t clk, clkTotal = clock();
     int i, fCompl, status;
+clk = clock();
     assert( Gia_ManRegNum(pCare) == 0 );
     assert( Gia_ManCiNum(pAig) == Gia_ManCiNum(pCare) );
     assert( Gia_ManIsNormalized(pAig) );
@@ -151,14 +171,14 @@ Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t
     if ( p == NULL )
         return Gia_ManDup( pAig );
     // perform simulation 
-clk = clock();
     if ( Gia_ManAndNum(pCare) == 0 ) // no constraints
     {
         for ( i = 0; i < 16; i++ )
         {
             Ssc_GiaRandomPiPattern( pAig, 10, NULL );
             Ssc_GiaSimRound( pAig );
-            Ssc_GiaClassesRefine( pAig );
+            if ( pPars->fVerbose ) 
+                Ssc_GiaClassesRefine( pAig );
             Gia_ManEquivPrintClasses( pAig, 0, 0 );
         }
     }
@@ -176,63 +196,86 @@ p->timeSimInit += clock() - clk;
     {
         if ( pAig->iPatsPi == 64 * pPars->nWords )
         {
+clk = clock();
             Ssc_GiaSimRound( pAig );
             Ssc_GiaClassesRefine( pAig );
-            Gia_ManEquivPrintClasses( pAig, 0, 0 );
+            if ( pPars->fVerbose ) 
+                Gia_ManEquivPrintClasses( pAig, 0, 0 );
             Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs );
+            Vec_IntClear( p->vDisPairs );
+            // prepare next patterns
             Ssc_GiaResetPiPattern( pAig, pPars->nWords );
             Ssc_GiaSavePiPattern( pAig, p->vPivot );
-            Vec_IntClear( p->vDisPairs );
+p->timeSimSat += clock() - clk;
         }
         if ( Gia_ObjIsAnd(pObj) )
             pObj->Value = Gia_ManHashAnd( p->pFraig, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         if ( !Gia_ObjHasRepr(pAig, i) )
             continue;
         pRepr = Gia_ObjReprObj(pAig, i);
-        if ( pRepr->Value == pObj->Value )
+        if ( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase ) )
             continue;
         assert( Abc_Lit2Var(pRepr->Value) != Abc_Lit2Var(pObj->Value) );
         fCompl = pRepr->fPhase ^ pObj->fPhase ^ Abc_LitIsCompl(pRepr->Value) ^ Abc_LitIsCompl(pObj->Value);
 
         // perform SAT call
-        clk = clock();
+clk = clock();
         p->nSatCalls++;
         status = Ssc_ManCheckEquivalence( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl );
         if ( status == l_False )
         {
             p->nSatCallsUnsat++;
-            p->timeSatUnsat += clock() - clk;
             pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase );
         }
         else if ( status == l_True )
         {
             p->nSatCallsSat++;
-            p->timeSatSat += clock() - clk;
             Ssc_GiaSavePiPattern( pAig, p->vPattern );
             Vec_IntPush( p->vDisPairs, Gia_ObjRepr(p->pAig, i) );
             Vec_IntPush( p->vDisPairs, i );
+//            printf( "Try %2d and %2d: ", Gia_ObjRepr(p->pAig, i), i );
+//            Vec_IntPrint( p->vPattern );
         }
         else if ( status == l_Undef )
-        {
             p->nSatCallsUndec++;
-            p->timeSatUndec += clock() - clk;
-        }
         else assert( 0 );
+p->timeSat += clock() - clk;
+    }
+    if ( pAig->iPatsPi > 1 )
+    {
+clk = clock();
+        while ( pAig->iPatsPi < 64 * pPars->nWords )
+            Ssc_GiaSavePiPattern( pAig, p->vPivot );
+        Ssc_GiaSimRound( pAig );
+        Ssc_GiaClassesRefine( pAig );
+        if ( pPars->fVerbose ) 
+            Gia_ManEquivPrintClasses( pAig, 0, 0 );
+        Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs );
+        Vec_IntClear( p->vDisPairs );
+p->timeSimSat += clock() - clk;
     }
+//    Gia_ManEquivPrintClasses( pAig, 1, 0 );
 
-    // remember the resulting AIG
+    // generate the resulting AIG
     pResult = Gia_ManEquivReduce( pAig, 1, 0, 0 );
     if ( pResult == NULL )
     {
         printf( "There is no equivalences.\n" );
+        ABC_FREE( pAig->pReprs );
+        ABC_FREE( pAig->pNexts );
         pResult = Gia_ManDup( pAig );
     }
+    p->timeTotal = clock() - clkTotal;
+    if ( pPars->fVerbose )
+        Ssc_ManPrintStats( p );
     Ssc_ManStop( p );
     // count the number of representatives
     if ( pPars->fVerbose ) 
     {
-        Gia_ManEquivPrintClasses( pAig, 0, 0 );
-        Abc_Print( 1, "Reduction in AIG nodes:%8d  ->%8d.  ", Gia_ManAndNum(pAig), Gia_ManAndNum(pResult) );
+//        Gia_ManEquivPrintClasses( pAig, 0, 0 );
+        Abc_Print( 1, "Reduction in AIG nodes:%8d  ->%8d (%6.2f %%).  ", 
+            Gia_ManAndNum(pAig), Gia_ManAndNum(pResult), 
+            100.0 - 100.0 * Gia_ManAndNum(pResult) / Gia_ManAndNum(pAig) );
         Abc_PrintTime( 1, "Time", clock() - clkTotal );
     }
     return pResult;
@@ -241,6 +284,8 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
 {
     Gia_Man_t * pAig, * pCare, * pResult;
     int i;
+    if ( pPars->fVerbose )
+        Abc_Print( 0, "SAT sweeping AIG with %d constraints.\n", p->nConstrs );
     if ( p->nConstrs == 0 )
     {
         pAig = Gia_ManDup( p );
@@ -257,6 +302,14 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
         pCare = Gia_ManDupCones( p, Vec_IntArray(vOuts) + Gia_ManPoNum(p) - p->nConstrs, p->nConstrs, 0 );
         Vec_IntFree( vOuts );
     }
+    if ( pPars->fVerbose )
+    {
+        printf( "User AIG: " );
+        Gia_ManPrintStats( pAig, 0, 0, 0 );
+        printf( "Care AIG: " );
+        Gia_ManPrintStats( pCare, 0, 0, 0 );
+    }
+
     pAig = Gia_ManDupLevelized( pResult = pAig );
     Gia_ManStop( pResult );
     pResult = Ssc_PerformSweeping( pAig, pCare, pPars );
diff --git a/src/proof/ssc/sscInt.h b/src/proof/ssc/sscInt.h
index 7e710c19..f0a556a6 100644
--- a/src/proof/ssc/sscInt.h
+++ b/src/proof/ssc/sscInt.h
@@ -64,6 +64,7 @@ struct Ssc_Man_t_
     Vec_Int_t *      vPattern;       // counter-example
     Vec_Int_t *      vDisPairs;      // disproved pairs
     // SAT calls statistics
+    int              nSimRounds;     // the number of simulation rounds
     int              nRecycles;      // the number of times SAT solver was recycled
     int              nCallsSince;    // the number of calls since the last recycle
     int              nSatCalls;      // the number of SAT calls
@@ -74,6 +75,7 @@ struct Ssc_Man_t_
     clock_t          timeSimInit;    // simulation and class computation
     clock_t          timeSimSat;     // simulation of the counter-examples
     clock_t          timeCnfGen;     // generation of CNF
+    clock_t          timeSat;        // total SAT time
     clock_t          timeSatSat;     // sat
     clock_t          timeSatUnsat;   // unsat
     clock_t          timeSatUndec;   // undecided
diff --git a/src/proof/ssc/sscSat.c b/src/proof/ssc/sscSat.c
index ea9c599f..f6d5e9af 100644
--- a/src/proof/ssc/sscSat.c
+++ b/src/proof/ssc/sscSat.c
@@ -210,8 +210,9 @@ static void Ssc_ManCnfNodeAddToSolver( Ssc_Man_t * p, int NodeId )
     Gia_Obj_t * pNode;
     int i, k, Id, Lit;
     clock_t clk;
+    assert( NodeId > 0 );
     // quit if CNF is ready
-    if ( NodeId == 0 || Ssc_ObjSatVar(p, NodeId) )
+    if ( Ssc_ObjSatVar(p, NodeId) )
         return;
 clk = clock();
     // start the frontier
@@ -345,33 +346,24 @@ Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p )
 int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
 {
     int pLitsSat[2], RetValue;
+    clock_t clk;
+    assert( iRepr < iNode );
 //    if ( p->nTimeOut )
 //        sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + clock() );
 
     // create CNF
+    if ( iRepr )
     Ssc_ManCnfNodeAddToSolver( p, iRepr );
     Ssc_ManCnfNodeAddToSolver( p, iNode );
     sat_solver_compress( p->pSat );
 
     // order the literals
     pLitsSat[0] = Abc_Var2Lit( Ssc_ObjSatVar(p, iRepr), 0 );
-    pLitsSat[1] = Abc_Var2Lit( Ssc_ObjSatVar(p, iNode), 0 );
-    if ( pLitsSat[0] < pLitsSat[1] )
-        ABC_SWAP( int, pLitsSat[0], pLitsSat[1] );
-
-    // correct polarity
-    pLitsSat[1] = Abc_LitNotCond( pLitsSat[1], !fCompl ); // extra complement!
-    if ( !Abc_LitIsCompl(pLitsSat[1]) )
-    {
-        pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
-        pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
-    }
-    assert( pLitsSat[0] > pLitsSat[1] );
-    assert( Abc_LitIsCompl(pLitsSat[1]) );
-    assert( pLitsSat[1] != 0 );
+    pLitsSat[1] = Abc_Var2Lit( Ssc_ObjSatVar(p, iNode), fCompl ^ (int)(iRepr > 0) );
 
     // solve under assumptions
-    // A = 1; B = 0     OR     A = 1; B = 1 
+    // A = 1; B = 0
+    clk = clock();
     RetValue = sat_solver_solve( p->pSat, pLitsSat, pLitsSat + 2, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( RetValue == l_False )
     {
@@ -379,22 +371,27 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
         pLitsSat[1] = Abc_LitNot( pLitsSat[1] ); // compl
         RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
         assert( RetValue );
+        p->timeSatUnsat += clock() - clk;
     }
     else if ( RetValue == l_True )
     {
         Ssc_ManCollectSatPattern( p, p->vPattern );
+        p->timeSatSat += clock() - clk;
         return l_True;
     }
     else // if ( RetValue1 == l_Undef )
+    {
+        p->timeSatUndec += clock() - clk;
         return l_Undef;
+    }
 
     // if the old node was constant 0, we already know the answer
-    if ( pLitsSat[1] == 0 )
+    if ( iRepr == 0 )
         return l_False;
-    assert( pLitsSat[1] > 1 );
 
     // solve under assumptions
-    // A = 0; B = 1     OR     A = 0; B = 0 
+    // A = 0; B = 1
+    clk = clock();
     RetValue = sat_solver_solve( p->pSat, pLitsSat, pLitsSat + 2, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( RetValue == l_False )
     {
@@ -402,14 +399,19 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
         pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
         RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
         assert( RetValue );
+        p->timeSatUnsat += clock() - clk;
     }
     else if ( RetValue == l_True )
     {
         Ssc_ManCollectSatPattern( p, p->vPattern );
+        p->timeSatSat += clock() - clk;
         return l_True;
     }
     else // if ( RetValue1 == l_Undef )
+    {
+        p->timeSatUndec += clock() - clk;
         return l_Undef;
+    }
     return l_False;
 }
 
diff --git a/src/proof/ssc/sscSim.c b/src/proof/ssc/sscSim.c
index 89585ba6..9a2c1033 100644
--- a/src/proof/ssc/sscSim.c
+++ b/src/proof/ssc/sscSim.c
@@ -212,6 +212,7 @@ void Ssc_GiaSimRound( Gia_Man_t * p )
         assert( pSim == Gia_ObjSimObj( p, pObj ) );
         pSim0 = pSim - pObj->iDiff0 * nWords;
         Ssc_SimDup( pSim, pSim0, nWords, Gia_ObjFaninC0(pObj) );
+//        Extra_PrintBinary( stdout, pSim, 64 ), printf( "\n" );
         pSim += nWords;
     }
 }