SAT sweeping under constraints.

1 files changed, 77 insertions, 10 deletions

diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c
index 55f0e140..43d0e250 100644
--- a/src/proof/ssc/sscCore.c
+++ b/src/proof/ssc/sscCore.c
@@ -119,6 +119,7 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar
     p->vFanins = Vec_IntAlloc( 100 );
     p->vFront = Vec_IntAlloc( 100 );
     Ssc_GiaClassesInit( pAig );
+    // now it is ready for refinement using simulation 
     return p;
 }
 void Ssc_ManPrintStats( Ssc_Man_t * p )
@@ -144,6 +145,65 @@ void Ssc_ManPrintStats( Ssc_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Refine one class by resimulating one pattern.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssc_GiaSimulatePatternFraig_rec( Ssc_Man_t * p, int iFraigObj )
+{
+    Gia_Obj_t * pObj;
+    int Res0, Res1;
+    if ( Ssc_ObjSatVar(p, iFraigObj) )
+        return sat_solver_var_value( p->pSat, Ssc_ObjSatVar(p, iFraigObj) );
+    pObj = Gia_ManObj( p->pFraig, iFraigObj );
+    assert( Gia_ObjIsAnd(pObj) );
+    Res0 = Ssc_GiaSimulatePatternFraig_rec( p, Gia_ObjFaninId0(pObj, iFraigObj) );
+    Res1 = Ssc_GiaSimulatePatternFraig_rec( p, Gia_ObjFaninId1(pObj, iFraigObj) );
+    pObj->fMark0 = (Res0 ^ Gia_ObjFaninC0(pObj)) & (Res1 ^ Gia_ObjFaninC1(pObj));
+    return pObj->fMark0;
+}
+int Ssc_GiaSimulatePattern_rec( Ssc_Man_t * p, Gia_Obj_t * pObj )
+{
+    int Res0, Res1;
+    if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) )
+        return pObj->fMark0;
+    Gia_ObjSetTravIdCurrent(p->pAig, pObj);
+    if ( ~pObj->Value )  // mapping into FRAIG exists - simulate FRAIG
+    { 
+        Res0 = Ssc_GiaSimulatePatternFraig_rec( p, Abc_Lit2Var(pObj->Value) );
+        pObj->fMark0 = Res0 ^ Abc_LitIsCompl(pObj->Value);
+    }
+    else // mapping into FRAIG does not exist - simulate AIG
+    {
+        Res0 = Ssc_GiaSimulatePattern_rec( p, Gia_ObjFanin0(pObj) );
+        Res1 = Ssc_GiaSimulatePattern_rec( p, Gia_ObjFanin1(pObj) );
+        pObj->fMark0 = (Res0 ^ Gia_ObjFaninC0(pObj)) & (Res1 ^ Gia_ObjFaninC1(pObj));
+    }
+    return pObj->fMark0;
+}
+int Ssc_GiaResimulateOneClass( Ssc_Man_t * p, int iRepr, int iObj )
+{
+    int Ent, RetValue;
+    assert( iRepr == Gia_ObjRepr(p->pAig, iObj) );
+    assert( Gia_ObjIsHead( p->pAig, iRepr ) );
+    // set bit-values at the nodes according to the counter-example
+    Gia_ManIncrementTravId( p->pAig );
+    Gia_ClassForEachObj( p->pAig, iRepr, Ent )
+        Ssc_GiaSimulatePattern_rec( p, Gia_ManObj(p->pAig, Ent) );
+    // refine one class using these bit-values
+    RetValue = Ssc_GiaSimClassRefineOneBit( p->pAig, iRepr );
+    // check that the candidate equivalence is indeed refined
+    assert( iRepr != Gia_ObjRepr(p->pAig, iObj) );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -159,7 +219,7 @@ Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t
     Gia_Man_t * pResult;
     Gia_Obj_t * pObj, * pRepr;
     clock_t clk, clkTotal = clock();
-    int i, fCompl, status;
+    int i, fCompl, nRefined, status;
 clk = clock();
     assert( Gia_ManRegNum(pCare) == 0 );
     assert( Gia_ManCiNum(pAig) == Gia_ManCiNum(pCare) );
@@ -172,18 +232,23 @@ clk = clock();
     if ( p == NULL )
         return Gia_ManDup( pAig );
     if ( p->pPars->fVerbose )
-        printf( "Care set produced %d hits out of %d.\n", Ssc_GiaEstimateCare(p->pFraig, 10), 640 );
+        printf( "Care set produced %d hits out of %d.\n", Ssc_GiaEstimateCare(p->pFraig, 5), 640 );
     // perform simulation 
-    if ( Gia_ManAndNum(pCare) == 0 ) // no constraints
+    while ( 1 ) 
     {
-        for ( i = 0; i < 16; i++ )
-        {
-            Ssc_GiaRandomPiPattern( pAig, 10, NULL );
-            Ssc_GiaSimRound( pAig );
-            if ( pPars->fVerbose ) 
-                Ssc_GiaClassesRefine( pAig );
+        // simulate care set
+        Ssc_GiaRandomPiPattern( p->pFraig, 5, NULL );
+        Ssc_GiaSimRound( p->pFraig );
+        // transfer care patterns to user's AIG
+        if ( !Ssc_GiaTransferPiPattern( pAig, p->pFraig, p->vPivot ) )
+            break;
+        // simulate the main AIG
+        Ssc_GiaSimRound( pAig );
+        nRefined = Ssc_GiaClassesRefine( pAig );
+        if ( pPars->fVerbose ) 
             Gia_ManEquivPrintClasses( pAig, 0, 0 );
-        }
+        if ( nRefined <= Gia_ManCandNum(pAig) / 100 )
+            break;
     }
 p->timeSimInit += clock() - clk;
 
@@ -242,6 +307,8 @@ clk = clock();
             Vec_IntPush( p->vDisPairs, i );
 //            printf( "Try %2d and %2d: ", Gia_ObjRepr(p->pAig, i), i );
 //            Vec_IntPrint( p->vPattern );
+            if ( Gia_ObjRepr(p->pAig, i) > 0 )
+                Ssc_GiaResimulateOneClass( p, Gia_ObjRepr(p->pAig, i), i );
         }
         else if ( status == l_Undef )
             p->nSatCallsUndec++;