SAT sweeping under constraints.

src/aig/gia/gia.h

@@ -857,6 +857,7 @@ extern Gia_Man_t *         Gia_ManDupFlopClass( Gia_Man_t * p, int iClass );
 extern Gia_Man_t *         Gia_ManDupMarked( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTimes( Gia_Man_t * p, int nTimes );  
 extern Gia_Man_t *         Gia_ManDupDfs( Gia_Man_t * p );  
+extern Gia_Man_t *         Gia_ManDupDfsRehash( Gia_Man_t * p );  
 extern Gia_Man_t *         Gia_ManDupDfsSkip( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern Gia_Man_t *         Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits );

src/aig/gia/giaDup.c

@@ -974,10 +974,32 @@ void Gia_ManDupDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
     Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin1(pObj) );
     pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
 }
+Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    pNew->nConstrs = p->nConstrs;
+    if ( p->pCexSeq )
+        pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
+    return pNew;
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Duplicates AIG in the DFS order.]
+  Synopsis    [Duplicates the AIG in the DFS order while rehashing.]
 
   Description []
                
@@ -986,7 +1008,16 @@ void Gia_ManDupDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
+void Gia_ManDupDfsRehash_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( ~pObj->Value )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+Gia_Man_t * Gia_ManDupDfsRehash( Gia_Man_t * p )
 {
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj;
@@ -998,11 +1029,13 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManHashAlloc( pNew );
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
+        Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin0(pObj) );
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    pNew->nConstrs = p->nConstrs;
     if ( p->pCexSeq )
         pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
     return pNew;

src/base/abci/abc.c

@@ -22161,7 +22161,7 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( nConstrs > 0 )
     {
         if ( Abc_NtkIsComb(pNtk) )
-            Abc_Print( -1, "The network is combinational.\n" );
+            Abc_Print( 0, "The network is combinational.\n" );
         if ( Abc_NtkConstrNum(pNtk) > 0 )
         {
             Abc_Print( -1, "The network already has constraints.\n" );
@@ -22172,7 +22172,7 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_Print( -1, "The number of constraints specified (%d) should be less than POs (%d).\n", nConstrs, Abc_NtkPoNum(pNtk) );
             return 0;
         }
-        Abc_Print( 0, "Considering the last %d POs as constraint outputs.\n", nConstrs );
+        Abc_Print( 1, "Setting the last %d POs as constraint outputs.\n", nConstrs );
         pNtk->nConstrs = nConstrs;
         return 0;
     }

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) );

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 );
 

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 );
 }
 
 ////////////////////////////////////////////////////////////////////////

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;
 }