SAT sweeping under constraints.

4 files changed, 200 insertions, 22 deletions

diff --git a/src/proof/ssc/sscClass.c b/src/proof/ssc/sscClass.c
index a9904148..c6b96a90 100644
--- a/src/proof/ssc/sscClass.c
+++ b/src/proof/ssc/sscClass.c
@@ -107,6 +107,12 @@ static inline int Ssc_GiaSimAreEqual( Gia_Man_t * p, int iObj0, int iObj1 )
     }
     return 1;
 }
+static inline int Ssc_GiaSimAreEqualBit( Gia_Man_t * p, int iObj0, int iObj1 )
+{
+    Gia_Obj_t * pObj0 = Gia_ManObj( p, iObj0 );
+    Gia_Obj_t * pObj1 = Gia_ManObj( p, iObj1 );
+    return (pObj0->fPhase ^ pObj0->fMark0) == (pObj1->fPhase ^ pObj1->fMark0);
+}
 
 /**Function*************************************************************
 
@@ -141,10 +147,58 @@ void Ssc_GiaSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
     }
     Gia_ObjSetNext( p, EntPrev, 0 );
 }
+
+/**Function*************************************************************
+
+  Synopsis    [Refines one equivalence class using individual bit-pattern.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssc_GiaSimClassRefineOneBit( Gia_Man_t * p, int i )
+{
+    Gia_Obj_t * pObj;
+    int Ent;
+    assert( Gia_ObjIsHead( p, i ) );
+    Vec_IntClear( p->vClassOld );
+    Vec_IntClear( p->vClassNew );
+    Vec_IntPush( p->vClassOld, i );
+    pObj = Gia_ManObj(p, i);
+    Gia_ClassForEachObj1( p, i, Ent )
+    {
+        if ( Ssc_GiaSimAreEqualBit( p, i, Ent ) )
+            Vec_IntPush( p->vClassOld, Ent );
+        else
+            Vec_IntPush( p->vClassNew, Ent );
+    }
+    if ( Vec_IntSize( p->vClassNew ) == 0 )
+        return 0;
+    Ssc_GiaSimClassCreate( p, p->vClassOld );
+    Ssc_GiaSimClassCreate( p, p->vClassNew );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Refines one class using simulation patterns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Ssc_GiaSimClassRefineOne( Gia_Man_t * p, int i )
 {
     Gia_Obj_t * pObj;
     int Ent;
+    assert( Gia_ObjIsHead( p, i ) );
     Vec_IntClear( p->vClassOld );
     Vec_IntClear( p->vClassNew );
     Vec_IntPush( p->vClassOld, i );
@@ -226,17 +280,18 @@ int Ssc_GiaClassesRefine( Gia_Man_t * p )
 {
     Vec_Int_t * vRefinedC;
     Gia_Obj_t * pObj;
-    int i;
+    int i, Counter = 0;
     if ( p->pReprs != NULL );
     vRefinedC = Vec_IntAlloc( 100 );
     Gia_ManForEachCand( p, pObj, i )
         if ( Gia_ObjIsTail(p, i) )
-            Ssc_GiaSimClassRefineOne( p, Gia_ObjRepr(p, i) );
+            Counter += Ssc_GiaSimClassRefineOne( p, Gia_ObjRepr(p, i) );
         else if ( Gia_ObjIsConst(p, i) && !Ssc_GiaSimIsConst0(p, i) )
             Vec_IntPush( vRefinedC, i );
     Ssc_GiaSimProcessRefined( p, vRefinedC );
+    Counter += Vec_IntSize( vRefinedC );
     Vec_IntFree( vRefinedC );
-    return 0;
+    return Counter;
 }
 
 
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++;
diff --git a/src/proof/ssc/sscInt.h b/src/proof/ssc/sscInt.h
index 1226f4ee..0be25174 100644
--- a/src/proof/ssc/sscInt.h
+++ b/src/proof/ssc/sscInt.h
@@ -102,6 +102,7 @@ static inline void   Ssc_ObjSetFraig( Gia_Obj_t * pObj, int iNode )       { pObj
 extern void          Ssc_GiaClassesInit( Gia_Man_t * p );
 extern int           Ssc_GiaClassesRefine( Gia_Man_t * p );
 extern void          Ssc_GiaClassesCheckPairs( Gia_Man_t * p, Vec_Int_t * vDisPairs );
+extern int           Ssc_GiaSimClassRefineOneBit( Gia_Man_t * p, int i );
 /*=== sscCnf.c ===================================================*/
 extern void          Ssc_CnfNodeAddToSolver( Ssc_Man_t * p, Gia_Obj_t * pObj );
 /*=== sscCore.c ==================================================*/
@@ -113,6 +114,7 @@ extern int           Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iObj
 /*=== sscSim.c ===================================================*/
 extern void          Ssc_GiaResetPiPattern( Gia_Man_t * p, int nWords );
 extern void          Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot );
+extern int           Ssc_GiaTransferPiPattern( Gia_Man_t * pAig, Gia_Man_t * pCare, Vec_Int_t * vPivot );
 extern void          Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat );
 extern void          Ssc_GiaSimRound( Gia_Man_t * p );
 extern Vec_Int_t *   Ssc_GiaFindPivotSim( Gia_Man_t * p );
diff --git a/src/proof/ssc/sscSim.c b/src/proof/ssc/sscSim.c
index d28db432..ae9a3eec 100644
--- a/src/proof/ssc/sscSim.c
+++ b/src/proof/ssc/sscSim.c
@@ -175,6 +175,56 @@ void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot )
 //            Extra_PrintBinary( stdout, (unsigned *)pSimPi, 64 ), printf( "\n" );
     }
 }
+void Ssc_GiaPrintPiPatterns( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    word * pSimAig;
+    int i, nWords = Gia_ObjSimWords( p );
+    Gia_ManForEachCi( p, pObj, i )
+    {
+        pSimAig = Gia_ObjSimObj( p, pObj );
+//        Extra_PrintBinary( stdout, pSimAig, 64 * nWords );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfer the simulation pattern from pCare to pAig.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssc_GiaTransferPiPattern( Gia_Man_t * pAig, Gia_Man_t * pCare, Vec_Int_t * vPivot )
+{
+    extern word * Ssc_GiaGetCareMask( Gia_Man_t * p );
+    Gia_Obj_t * pObj;
+    int i, w, nWords = Gia_ObjSimWords( pCare );
+    word * pCareMask = Ssc_GiaGetCareMask( pCare );
+    int Count = Ssc_SimCountBits( pCareMask, nWords );
+    word * pSimPiCare, * pSimPiAig;
+    if ( Count == 0 )
+    {
+        ABC_FREE( pCareMask );
+        return 0;
+    }
+    Ssc_GiaResetPiPattern( pAig, nWords );
+    Gia_ManForEachCi( pCare, pObj, i )
+    {
+        pSimPiAig  = Gia_ObjSimPi( pAig, i );
+        pSimPiCare = Gia_ObjSimObj( pCare, pObj );
+        for ( w = 0; w < nWords; w++ )
+            if ( Vec_IntEntry(vPivot, i) )
+                pSimPiAig[w] = pSimPiCare[w] | ~pCareMask[w];
+            else
+                pSimPiAig[w] = pSimPiCare[w] & pCareMask[w];
+    }
+    ABC_FREE( pCareMask );
+    return Count;
+}
 
 /**Function*************************************************************
 
@@ -246,14 +296,21 @@ void Ssc_GiaSimRound( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p )
+word * Ssc_GiaGetCareMask( Gia_Man_t * p )
 {
-    Vec_Int_t * vInit;
     Gia_Obj_t * pObj;
-    int i, iBit, nWords = Gia_ObjSimWords( p );
+    int i, nWords = Gia_ObjSimWords( p );
     word * pRes = ABC_FALLOC( word, nWords );
     Gia_ManForEachPo( p, pObj, i )
         Ssc_SimAnd( pRes, pRes, Gia_ObjSimObj(p, pObj), nWords, 0, 0 );
+    return pRes;
+}
+Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p )
+{
+    Vec_Int_t * vInit;
+    Gia_Obj_t * pObj;
+    int i, iBit, nWords = Gia_ObjSimWords( p );
+    word * pRes = Ssc_GiaGetCareMask( p );
     iBit = Ssc_SimFindBit( pRes, nWords );
     ABC_FREE( pRes );
     if ( iBit == -1 )
@@ -285,12 +342,9 @@ Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p )
 ***********************************************************************/
 int Ssc_GiaCountCaresSim( Gia_Man_t * p )
 {
-    Gia_Obj_t * pObj;
-    int i, Count, nWords = Gia_ObjSimWords( p );
-    word * pRes = ABC_FALLOC( word, nWords );
-    Gia_ManForEachPo( p, pObj, i )
-        Ssc_SimAnd( pRes, pRes, Gia_ObjSimObj(p, pObj), nWords, 0, 0 );
-    Count = Ssc_SimCountBits( pRes, nWords );
+    word * pRes = Ssc_GiaGetCareMask( p );
+    int nWords = Gia_ObjSimWords( p );
+    int Count = Ssc_SimCountBits( pRes, nWords );
     ABC_FREE( pRes );
     return Count;
 }