SAT sweeping under constraints.

1 files changed, 104 insertions, 21 deletions

diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c
index f2cd810a..1aada663 100644
--- a/src/proof/ssc/sscCore.c
+++ b/src/proof/ssc/sscCore.c
@@ -45,13 +45,14 @@ ABC_NAMESPACE_IMPL_START
 void Ssc_ManSetDefaultParams( Ssc_Pars_t * p )
 {
     memset( p, 0, sizeof(Ssc_Pars_t) );
-    p->nWords         =     4;  // the number of simulation words
+    p->nWords         =     1;  // the number of simulation words
     p->nBTLimit       =  1000;  // conflict limit at a node
     p->nSatVarMax     =  5000;  // the max number of SAT variables
     p->nCallsRecycle  =   100;  // calls to perform before recycling SAT solver
     p->fVerbose       =     0;  // verbose stats
 }
 
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -65,11 +66,15 @@ void Ssc_ManSetDefaultParams( Ssc_Pars_t * p )
 ***********************************************************************/
 void Ssc_ManStop( Ssc_Man_t * p )
 {
-    if ( p->pSat )
-        sat_solver_delete( p->pSat );
-    Vec_IntFreeP( &p->vSatVars );
-    Gia_ManStopP( &p->pFraig );
+    Vec_IntFreeP( &p->vFront );
+    Vec_IntFreeP( &p->vFanins );
+    Vec_IntFreeP( &p->vPattern );
+    Vec_IntFreeP( &p->vDisPairs );
     Vec_IntFreeP( &p->vPivot );
+    Vec_IntFreeP( &p->vId2Var );
+    Vec_IntFreeP( &p->vVar2Id );
+    if ( p->pSat ) sat_solver_delete( p->pSat );
+    Gia_ManStopP( &p->pFraig );
     ABC_FREE( p );
 }
 Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars )
@@ -80,33 +85,48 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar
     p->pAig   = pAig;
     p->pCare  = pCare;
     p->pFraig = Gia_ManDup( p->pCare );
+    Gia_ManHashStart( p->pFraig );
     Gia_ManInvertPos( p->pFraig );
     Ssc_ManStartSolver( p );
     if ( p->pSat == NULL )
     {
-        printf( "Constraints are UNSAT after propagation.\n" );
+        printf( "Constraints are UNSAT after propagation (likely a bug!).\n" );
         Ssc_ManStop( p );
         return NULL;
     }
-    p->vPivot = Ssc_GiaFindPivotSim( p->pFraig );
+//    p->vPivot = Ssc_GiaFindPivotSim( p->pFraig );
 //    Vec_IntFreeP( &p->vPivot  );
-    if ( p->vPivot == NULL )
-        p->vPivot = Ssc_ManFindPivotSat( p );
+    p->vPivot = Ssc_ManFindPivotSat( p );
     if ( p->vPivot == NULL )
     {
         printf( "Constraints are UNSAT or conflict limit is too low.\n" );
         Ssc_ManStop( p );
         return NULL;
     }
+    sat_solver_bookmark( p->pSat );
     Vec_IntPrint( p->vPivot );
+    Gia_ManSetPhasePattern( p->pAig, p->vPivot );
+    Gia_ManSetPhasePattern( p->pCare, p->vPivot );
+    if ( Gia_ManCheckCoPhase(p->pCare) )
+    {
+        printf( "Computed reference pattern violates %d constraints (this is a bug!).\n", Gia_ManCheckCoPhase(p->pCare) );
+        Ssc_ManStop( p );
+        return NULL;
+    }
+    // other things
+    p->vDisPairs = Vec_IntAlloc( 100 );
+    p->vPattern = Vec_IntAlloc( 100 );
+    p->vFanins = Vec_IntAlloc( 100 );
+    p->vFront = Vec_IntAlloc( 100 );
+    Ssc_GiaClassesInit( pAig );
     return p;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Performs computation of AIGs with choices.]
+  Synopsis    []
 
-  Description [Takes several AIGs and performs choicing.]
+  Description []
                
   SideEffects []
 
@@ -117,10 +137,11 @@ Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t
 {
     Ssc_Man_t * p;
     Gia_Man_t * pResult;
+    Gia_Obj_t * pObj, * pRepr;
     clock_t clk, clkTotal = clock();
-    int i;
+    int i, fCompl, status;
     assert( Gia_ManRegNum(pCare) == 0 );
-    assert( Gia_ManPiNum(pAig) == Gia_ManPiNum(pCare) );
+    assert( Gia_ManCiNum(pAig) == Gia_ManCiNum(pCare) );
     assert( Gia_ManIsNormalized(pAig) );
     assert( Gia_ManIsNormalized(pCare) );
     // reset random numbers
@@ -131,14 +152,74 @@ Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t
         return Gia_ManDup( pAig );
     // perform simulation 
 clk = clock();
-    for ( i = 0; i < 16; i++ )
+    if ( Gia_ManAndNum(pCare) == 0 ) // no constraints
     {
-        Ssc_GiaRandomPiPattern( pAig, 10, NULL );
-        Ssc_GiaSimRound( pAig );
-        Ssc_GiaClassesRefine( pAig );
-        Gia_ManEquivPrintClasses( pAig, 0, 0 );
+        for ( i = 0; i < 16; i++ )
+        {
+            Ssc_GiaRandomPiPattern( pAig, 10, NULL );
+            Ssc_GiaSimRound( pAig );
+            Ssc_GiaClassesRefine( pAig );
+            Gia_ManEquivPrintClasses( pAig, 0, 0 );
+        }
     }
 p->timeSimInit += clock() - clk;
+
+    // prepare user's AIG
+    Gia_ManFillValue(pAig);
+    Gia_ManConst0(pAig)->Value = 0;
+    Gia_ManForEachCi( pAig, pObj, i )
+        pObj->Value = Gia_Obj2Lit( p->pFraig, Gia_ManCi(p->pFraig, i) );
+    // perform sweeping
+    Ssc_GiaResetPiPattern( pAig, pPars->nWords );
+    Ssc_GiaSavePiPattern( pAig, p->vPivot );
+    Gia_ManForEachCand( pAig, pObj, i )
+    {
+        if ( pAig->iPatsPi == 64 * pPars->nWords )
+        {
+            Ssc_GiaSimRound( pAig );
+            Ssc_GiaClassesRefine( pAig );
+            Gia_ManEquivPrintClasses( pAig, 0, 0 );
+            Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs );
+            Ssc_GiaResetPiPattern( pAig, pPars->nWords );
+            Ssc_GiaSavePiPattern( pAig, p->vPivot );
+            Vec_IntClear( p->vDisPairs );
+        }
+        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 )
+            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();
+        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 );
+        }
+        else if ( status == l_Undef )
+        {
+            p->nSatCallsUndec++;
+            p->timeSatUndec += clock() - clk;
+        }
+        else assert( 0 );
+    }
+
     // remember the resulting AIG
     pResult = Gia_ManEquivReduce( pAig, 1, 0, 0 );
     if ( pResult == NULL )
@@ -163,11 +244,11 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
     if ( p->nConstrs == 0 )
     {
         pAig = Gia_ManDup( p );
-        pCare = Gia_ManStart( Gia_ManPiNum(p) + 2 );
+        pCare = Gia_ManStart( Gia_ManCiNum(p) + 2 );
         pCare->pName = Abc_UtilStrsav( "care" );
-        for ( i = 0; i < Gia_ManPiNum(p); i++ )
+        for ( i = 0; i < Gia_ManCiNum(p); i++ )
             Gia_ManAppendCi( pCare );
-        Gia_ManAppendCo( pCare, 1 );
+        Gia_ManAppendCo( pCare, 0 );
     }
     else
     {
@@ -176,6 +257,8 @@ 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 );
     }
+    pAig = Gia_ManDupLevelized( pResult = pAig );
+    Gia_ManStop( pResult );
     pResult = Ssc_PerformSweeping( pAig, pCare, pPars );
     Gia_ManStop( pAig );
     Gia_ManStop( pCare );