SAT sweeping under constraints.

4 files changed, 64 insertions, 14 deletions

diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c
index b29a0193..55f0e140 100644
--- a/src/proof/ssc/sscCore.c
+++ b/src/proof/ssc/sscCore.c
@@ -83,8 +83,9 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar
     p->pPars  = pPars;
     p->pAig   = pAig;
     p->pCare  = pCare;
-    p->pFraig = Gia_ManDup( p->pCare );
-    Gia_ManHashStart( p->pFraig );
+    p->pFraig = Gia_ManDupDfs( p->pCare );
+    assert( p->pFraig->pHTable == NULL );
+    assert( !Gia_ManHasDangling(p->pFraig) );
     Gia_ManInvertPos( p->pFraig );
     Ssc_ManStartSolver( p );
     if ( p->pSat == NULL )
@@ -170,6 +171,8 @@ clk = clock();
     p = Ssc_ManStart( pAig, pCare, pPars );
     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 );
     // perform simulation 
     if ( Gia_ManAndNum(pCare) == 0 ) // no constraints
     {
@@ -189,6 +192,9 @@ p->timeSimInit += clock() - clk;
     Gia_ManConst0(pAig)->Value = 0;
     Gia_ManForEachCi( pAig, pObj, i )
         pObj->Value = Gia_Obj2Lit( p->pFraig, Gia_ManCi(p->pFraig, i) );
+//    Gia_ManLevelNum(pAig);
+    // prepare swept AIG (should be done after starting SAT solver in Ssc_ManStart)
+    Gia_ManHashStart( p->pFraig );
     // perform sweeping
     Ssc_GiaResetPiPattern( pAig, pPars->nWords );
     Ssc_GiaSavePiPattern( pAig, p->vPivot );
@@ -207,6 +213,7 @@ clk = clock();
             Ssc_GiaResetPiPattern( pAig, pPars->nWords );
             Ssc_GiaSavePiPattern( pAig, p->vPivot );
 p->timeSimSat += clock() - clk;
+//printf( "\n" );
         }
         if ( Gia_ObjIsAnd(pObj) )
             pObj->Value = Gia_ManHashAnd( p->pFraig, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
@@ -272,7 +279,6 @@ p->timeSimSat += clock() - clk;
     // count the number of representatives
     if ( pPars->fVerbose ) 
     {
-//        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) );
diff --git a/src/proof/ssc/sscInt.h b/src/proof/ssc/sscInt.h
index f0a556a6..1226f4ee 100644
--- a/src/proof/ssc/sscInt.h
+++ b/src/proof/ssc/sscInt.h
@@ -116,6 +116,7 @@ extern void          Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_
 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 );
+extern int           Ssc_GiaEstimateCare( Gia_Man_t * p, int nWords );
 /*=== sscUtil.c ===================================================*/
 extern Gia_Man_t *   Ssc_GenerateOneHot( int nVars );
 
diff --git a/src/proof/ssc/sscSim.c b/src/proof/ssc/sscSim.c
index 9a2c1033..d28db432 100644
--- a/src/proof/ssc/sscSim.c
+++ b/src/proof/ssc/sscSim.c
@@ -82,6 +82,24 @@ static inline int Ssc_SimFindBit( word * pSim, int nWords )
     return -1;
 }
 
+static inline int Ssc_SimCountBitsWord( word x )
+{
+    x = x - ((x >> 1) & ABC_CONST(0x5555555555555555));   
+    x = (x & ABC_CONST(0x3333333333333333)) + ((x >> 2) & ABC_CONST(0x3333333333333333));    
+    x = (x + (x >> 4)) & ABC_CONST(0x0F0F0F0F0F0F0F0F);    
+    x = x + (x >> 8);
+    x = x + (x >> 16);
+    x = x + (x >> 32); 
+    return (int)(x & 0xFF);
+}
+static inline int Ssc_SimCountBits( word * pSim, int nWords )
+{
+    int w, Counter = 0;
+    for ( w = 0; w < nWords; w++ )
+        Counter += Ssc_SimCountBitsWord(pSim[w]);
+    return Counter;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -245,6 +263,14 @@ Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p )
         Vec_IntPush( vInit, Abc_InfoHasBit((unsigned *)Gia_ObjSimObj(p, pObj), iBit) );
     return vInit;
 }
+Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p )
+{
+    Vec_Int_t * vInit;
+    Ssc_GiaRandomPiPattern( p, 1, NULL );
+    Ssc_GiaSimRound( p );
+    vInit = Ssc_GiaGetOneSim( p );
+    return vInit;
+}
 
 /**Function*************************************************************
 
@@ -257,13 +283,22 @@ Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p )
+int Ssc_GiaCountCaresSim( Gia_Man_t * p )
 {
-    Vec_Int_t * vInit;
-    Ssc_GiaRandomPiPattern( p, 1, NULL );
+    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 );
+    ABC_FREE( pRes );
+    return Count;
+}
+int Ssc_GiaEstimateCare( Gia_Man_t * p, int nWords )
+{
+    Ssc_GiaRandomPiPattern( p, nWords, NULL );
     Ssc_GiaSimRound( p );
-    vInit = Ssc_GiaGetOneSim( p );
-    return vInit;
+    return Ssc_GiaCountCaresSim( p );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/ssc/sscUtil.c b/src/proof/ssc/sscUtil.c
index 0ced578f..52aea52c 100644
--- a/src/proof/ssc/sscUtil.c
+++ b/src/proof/ssc/sscUtil.c
@@ -52,6 +52,7 @@ Gia_Man_t * Gia_ManDropContained( Gia_Man_t * p )
     Gia_Obj_t * pObj;
     Vec_Int_t * vLits, * vKeep;
     sat_solver * pSat;
+    int ConstLit = Abc_Var2Lit(pDat->pVarNums[0], 0);
     int i, status;//, Count = 0;
     Aig_ManStop( pMan );
 
@@ -75,10 +76,10 @@ Gia_Man_t * Gia_ManDropContained( Gia_Man_t * p )
             return NULL;
         }
     }
+    Cnf_DataFree( pDat );
     status = sat_solver_simplify( pSat );
     if ( status == 0 )
     {
-        Cnf_DataFree( pDat );
         sat_solver_delete( pSat );
         Vec_IntFree( vLits );
         return NULL;
@@ -92,17 +93,15 @@ Gia_Man_t * Gia_ManDropContained( Gia_Man_t * p )
         status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
         Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits,i)) );
         if ( status == l_False )
-            Vec_IntWriteEntry( vLits, i, Abc_Var2Lit(pDat->pVarNums[0], 0) ); // const1 SAT var is always true
+            Vec_IntWriteEntry( vLits, i, ConstLit ); // const1 SAT var is always true
         else 
         {
             assert( status = l_True );
             Vec_IntPush( vKeep, i );
         }
     }
-    Cnf_DataFree( pDat );
     sat_solver_delete( pSat );
     Vec_IntFree( vLits );
-
     if ( Vec_IntSize(vKeep) == Gia_ManPoNum(p) )
     {
         Vec_IntFree( vKeep );
@@ -140,19 +139,28 @@ Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p )
         return pTemp;
     Ssc_ManSetDefaultParams( pPars );
     pPars->fAppend  = 1;
-    pPars->fVerbose = 1;
+    pPars->fVerbose = 0;
     pTemp->nConstrs = Gia_ManPoNum(pTemp) - 1;    
     for ( i = 0; i < Gia_ManPoNum(pTemp); i++ )
     {
+        // move i-th PO forward
         Gia_ManSwapPos( pTemp, i );
+        pTemp = Gia_ManDupDfs( pAux = pTemp );
+        Gia_ManStop( pAux );
+        // minimize this PO
         pTemp = Ssc_PerformSweepingConstr( pAux = pTemp, pPars );
         Gia_ManStop( pAux );
-        pTemp = Gia_ManDupNormalize( pAux = pTemp );
+        pTemp = Gia_ManDupDfs( pAux = pTemp );
         Gia_ManStop( pAux );
+        // move i-th PO back
         Gia_ManSwapPos( pTemp, i );
+        pTemp = Gia_ManDupDfs( pAux = pTemp );
+        Gia_ManStop( pAux );
+        // report results
         printf( "AIG%3d  : ", i );
         Gia_ManPrintStats( pTemp, 0, 0, 0 );
     }
+    pTemp->nConstrs = 0;
     return pTemp;
 }