User-controlable SAT sweeper.

3 files changed, 90 insertions, 62 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index f99a2246..2a003ad0 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -995,6 +995,7 @@ extern Gia_Man_t *         Gia_ManFraigSweep( Gia_Man_t * p, void * pPars );
 /*=== giaSweeper.c ============================================================*/
 extern Gia_Man_t *         Gia_SweeperStart();
 extern void                Gia_SweeperStop( Gia_Man_t * p );
+extern void                Gia_SweeperPrintStats( Gia_Man_t * p );
 extern void                Gia_SweeperSetConflictLimit( Gia_Man_t * p, int nConfMax );
 extern void                Gia_SweeperSetRuntimeLimit( Gia_Man_t * p, int nSeconds );
 extern Vec_Int_t *         Gia_SweeperGetCex( Gia_Man_t * p );
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c
index e08f0ab9..2b27cdeb 100644
--- a/src/aig/gia/giaSweeper.c
+++ b/src/aig/gia/giaSweeper.c
@@ -66,7 +66,6 @@ struct Swp_Man_t_
     Vec_Int_t *    vLit2Prob;   // mapping of literal into its probe
 //    Vec_Int_t *    vFreeProb;   // recycled probe IDs
     Vec_Int_t *    vCondProbes; // conditions as probes
-    Vec_Int_t *    vCondLits;   // conditions as literals
     Vec_Int_t *    vCondAssump; // conditions as SAT solver literals
     // equivalence checking
     sat_solver *   pSat;        // SAT solver 
@@ -80,8 +79,11 @@ struct Swp_Man_t_
     int            nSatCalls;
     int            nSatCallsSat;
     int            nSatCallsUnsat;
-    int            nSatFails;
+    int            nSatCallsUndec;
     int            nSatProofs;
+    clock_t        timeStart;
+    clock_t        timeTotal;
+    clock_t        timeCnf;
     clock_t        timeSat;
     clock_t        timeSatSat;
     clock_t        timeSatUnsat;
@@ -89,8 +91,8 @@ struct Swp_Man_t_
 };
 
 static inline int  Swp_ManObj2Lit( Swp_Man_t * p, int Id )              { return Vec_IntGetEntry( p->vId2Lit, Id );              }
-static inline int  Swp_ManLit2Lit( Swp_Man_t * p, int Lit )             { return Abc_Lit2LitL( Vec_IntArray(p->vId2Lit), Lit );  }
-static inline void Swp_ManSetObj2Lit( Swp_Man_t * p, int Id, int Lit )  { Vec_IntSetEntry( p->vId2Lit, Id, Lit );                }
+static inline int  Swp_ManLit2Lit( Swp_Man_t * p, int Lit )             { assert( Vec_IntEntry(p->vId2Lit, Abc_Lit2Var(Lit)) ); return Abc_Lit2LitL( Vec_IntArray(p->vId2Lit), Lit );  }
+static inline void Swp_ManSetObj2Lit( Swp_Man_t * p, int Id, int Lit )  { assert( Lit > 0 ); Vec_IntSetEntry( p->vId2Lit, Id, Lit );                }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -118,7 +120,6 @@ static inline Swp_Man_t * Swp_ManStart( Gia_Man_t * pGia )
     p->vProbRefs    = Vec_IntAlloc( 100 );
     p->vLit2Prob    = Vec_IntStartFull( 10000 );
     p->vCondProbes  = Vec_IntAlloc( 100 );
-    p->vCondLits    = Vec_IntAlloc( 100 );
     p->vCondAssump  = Vec_IntAlloc( 100 );
     p->vId2Lit      = Vec_IntAlloc( 10000 );
     p->vFront       = Vec_IntAlloc( 100 );
@@ -130,6 +131,7 @@ static inline Swp_Man_t * Swp_ManStart( Gia_Man_t * pGia )
     Swp_ManSetObj2Lit( p, 0, (Lit = Abc_Var2Lit(p->nSatVars++, 0)) );
     Lit = Abc_LitNot(Lit);
     sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
+    p->timeStart    = clock();
     return p;
 }
 static inline void Swp_ManStop( Gia_Man_t * pGia )
@@ -144,7 +146,6 @@ static inline void Swp_ManStop( Gia_Man_t * pGia )
     Vec_IntFree( p->vProbRefs );
     Vec_IntFree( p->vLit2Prob );
     Vec_IntFree( p->vCondProbes );
-    Vec_IntFree( p->vCondLits );
     Vec_IntFree( p->vCondAssump );
     ABC_FREE( p );
     pGia->pData = NULL;
@@ -165,6 +166,48 @@ void Gia_SweeperStop( Gia_Man_t * pGia )
     Gia_ManHashStop( pGia );
     Gia_ManStop( pGia );
 }
+double Gia_SweeperMemUsage( Gia_Man_t * pGia )
+{
+    Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
+    double nMem = sizeof(Swp_Man_t);
+    nMem += Vec_IntCap(p->vProbes);
+    nMem += Vec_IntCap(p->vProbRefs);
+    nMem += Vec_IntCap(p->vLit2Prob);
+    nMem += Vec_IntCap(p->vCondProbes);
+    nMem += Vec_IntCap(p->vCondAssump);
+    nMem += Vec_IntCap(p->vId2Lit);
+    nMem += Vec_IntCap(p->vFront);
+    nMem += Vec_IntCap(p->vFanins);
+    nMem += Vec_IntCap(p->vCexSwp);
+    return 4.0 * nMem;
+}
+void Gia_SweeperPrintStats( Gia_Man_t * pGia )
+{
+    Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
+    double nMemSwp = Gia_SweeperMemUsage(pGia)/(1<<20);
+    double nMemGia = (double)Gia_ManObjNum(pGia)*(sizeof(Gia_Obj_t) + sizeof(int))/(1<<20);
+    double nMemSat = sat_solver_memory(p->pSat)/(1<<20);
+    double nMemTot = nMemSwp + nMemGia + nMemSat;
+    printf( "SAT sweeper statistics:\n" );
+    printf( "Memory usage:\n" );
+    ABC_PRMP( "Sweeper         ", nMemSwp, nMemTot );
+    ABC_PRMP( "AIG manager     ", nMemGia, nMemTot );
+    ABC_PRMP( "SAT solver      ", nMemSat, nMemTot );
+    ABC_PRMP( "TOTAL           ", nMemTot, nMemTot );
+    printf( "Runtime usage:\n" );
+    p->timeTotal = clock() - p->timeStart;
+    ABC_PRTP( "CNF construction", p->timeCnf,      p->timeTotal );
+    ABC_PRTP( "SAT solving     ", p->timeSat,      p->timeTotal );
+    ABC_PRTP( "    Sat         ", p->timeSatSat,   p->timeTotal );
+    ABC_PRTP( "    Unsat       ", p->timeSatUnsat, p->timeTotal );
+    ABC_PRTP( "    Undecided   ", p->timeSatUndec, p->timeTotal );
+    ABC_PRTP( "TOTAL RUNTIME   ", p->timeTotal,    p->timeTotal );
+    printf( "GIA: " );
+    Gia_ManPrintStats( pGia, 0, 0, 0 );
+    printf( "SAT calls = %d. Sat = %d. Unsat = %d. Undecided = %d.  Proofs = %d.\n", 
+        p->nSatCalls, p->nSatCallsSat, p->nSatCallsSat, p->nSatCallsUndec, p->nSatProofs );
+    Sat_SolverPrintStats( stdout, p->pSat );
+}
 
 /**Function*************************************************************
 
@@ -264,14 +307,11 @@ void Gia_SweeperCondPush( Gia_Man_t * p, int ProbeId )
 {
     Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
     Vec_IntPush( pSwp->vCondProbes, ProbeId );
-    Vec_IntPush( pSwp->vCondLits, Gia_SweeperProbeLit(p, ProbeId) );
 }
 int Gia_SweeperCondPop( Gia_Man_t * p )
 {
     Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
-    int ProbId = Vec_IntPop( pSwp->vCondProbes );
-    Vec_IntPop( pSwp->vCondLits );
-    return ProbId;
+    return Vec_IntPop( pSwp->vCondProbes );
 }
 
 
@@ -286,27 +326,6 @@ int Gia_SweeperCondPop( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline Vec_Ptr_t * Vec_PtrDupStr( Vec_Ptr_t * pVec )
-{
-    char * pName;
-    int i;
-    Vec_Ptr_t * p = Vec_PtrDup( pVec );
-    Vec_PtrForEachEntry( char *, p, pName, i )
-        Vec_PtrWriteEntry( p, i, Abc_UtilStrsav(pName) );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 static void Gia_ManExtract_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vObjIds )
 {
     if ( !Gia_ObjIsAnd(pObj) )
@@ -320,19 +339,11 @@ static void Gia_ManExtract_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vOb
 }
 Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vOutNames )
 {
+    Vec_Int_t * vObjIds, * vValues;
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
-    Vec_Int_t * vObjIds;
-    Vec_Int_t * vValues;
     int i, ProbeId;
     assert( Vec_IntSize(vProbeIds) == Vec_PtrSize(vOutNames) );
-    // save values
-    vValues = Vec_IntAlloc( Gia_ManObjNum(p) );
-    Gia_ManForEachObj( p, pObj, i )
-    {
-        Vec_IntPush( vValues, pObj->Value );
-        pObj->Value = ~0;
-    }
     // create new
     Gia_ManIncrementTravId( p );
     vObjIds = Vec_IntAlloc( 1000 );
@@ -342,7 +353,7 @@ Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, V
         Gia_ManExtract_rec( p, Gia_Regular(pObj), vObjIds );
     }
     // create new manager
-    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew = Gia_ManStart( 1 + Gia_ManPiNum(p) + Vec_IntSize(vObjIds) + Vec_IntSize(vProbeIds) + 100 );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
@@ -350,16 +361,26 @@ Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, V
         pObj->Value = Gia_ManAppendCi(pNew);
     // create internal nodes
     Gia_ManHashStart( pNew );
+    vValues = Vec_IntAlloc( Vec_IntSize(vObjIds) );
     Gia_ManForEachObjVec( vObjIds, p, pObj, i )
+    {
+        Vec_IntPush( vValues, pObj->Value );
         pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    }
     Gia_ManHashStop( pNew );
-    Vec_IntFree( vObjIds );
     // create outputs
     Vec_IntForEachEntry( vProbeIds, ProbeId, i )
     {
         pObj = Gia_Lit2Obj( p, Gia_SweeperProbeLit(p, ProbeId) );
         Gia_ManAppendCo( pNew, Gia_Regular(pObj)->Value ^ Gia_IsComplement(pObj) );
     }
+    // return the values back
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->Value = 0;
+    Gia_ManForEachObjVec( vObjIds, p, pObj, i )
+        pObj->Value = Vec_IntEntry( vValues, i );
+    Vec_IntFree( vObjIds );
+    Vec_IntFree( vValues );
     // duplicated if needed
     if ( Gia_ManHasDangling(pNew) )
     {
@@ -371,11 +392,6 @@ Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, V
         pNew->vNamesIn = Vec_PtrDupStr( p->vNamesIn );
     if ( vOutNames )
         pNew->vNamesOut = Vec_PtrDupStr( vOutNames );
-//Gia_ManPrintStats( pNew, 0, 0, 0 );
-    // reset values
-    Gia_ManForEachObj( p, pObj, i )
-        pObj->Value = Vec_IntEntry( vValues, i );
-    Vec_IntFree( vValues );
     return pNew;
 }
 
@@ -553,9 +569,11 @@ static void Gia_ManCnfNodeAddToSolver( Swp_Man_t * p, int NodeId )
 {
     Gia_Obj_t * pNode;
     int i, k, Id, Lit;
+    clock_t clk;
     // quit if CNF is ready
     if ( NodeId == 0 || Swp_ManObj2Lit(p, NodeId) )
         return;
+clk = clock();
     // start the frontier
     Vec_IntClear( p->vFront );
     Gia_ManObjAddToFrontier( p, NodeId, p->vFront );
@@ -584,6 +602,7 @@ static void Gia_ManCnfNodeAddToSolver( Swp_Man_t * p, int NodeId )
         }
         assert( Vec_IntSize(p->vFanins) > 1 );
     }
+p->timeCnf += clock() - clk;
 }
 
 
@@ -632,7 +651,7 @@ static Vec_Int_t * Gia_ManGetCex( Gia_Man_t * pGia, Vec_Int_t * vId2Lit, sat_sol
 int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
 {
     Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
-    int iLitOld, iLitNew, pLitsSat[2], RetValue, RetValue1, iLitAig, i;
+    int iLitOld, iLitNew, iLitAig, pLitsSat[2], RetValue, RetValue1, ProbeId, i;
     clock_t clk;
     p->nSatCalls++;
     assert( p->pSat != NULL );
@@ -647,7 +666,7 @@ int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
     // if the literals are opposites, the probes are not equivalent
     if ( Abc_LitRegular(iLitOld) == Abc_LitRegular(iLitNew) )
     {
-        Vec_IntFill( p->vCexSwp, Gia_ManPiNum(pGia), 0 );
+        Vec_IntFill( p->vCexSwp, Gia_ManPiNum(pGia), 2 );
         p->vCexUser = p->vCexSwp;
         return 0;
     }
@@ -656,10 +675,11 @@ int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
         ABC_SWAP( int, iLitOld, iLitNew );
     assert( iLitOld > iLitNew );
 
-    // if the nodes do not have SAT variables, allocate them
+    // create logic cones and the array of assumptions
     Vec_IntClear( p->vCondAssump );
-    Vec_IntForEachEntry( p->vCondLits, iLitAig, i )
+    Vec_IntForEachEntry( p->vCondProbes, ProbeId, i )
     {
+        iLitAig = Gia_SweeperProbeLit( pGia, ProbeId );
         Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitAig) );
         Vec_IntPush( p->vCondAssump, Swp_ManLit2Lit(p, iLitAig) );
     }
@@ -684,11 +704,9 @@ p->timeSat += clock() - clk;
     if ( RetValue1 == l_False )
     {
         pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
-        pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
         RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
         assert( RetValue );
         pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
-        pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
 p->timeSatUnsat += clock() - clk;
         p->nSatCallsUnsat++;
     }
@@ -702,7 +720,7 @@ p->timeSatSat += clock() - clk;
     else // if ( RetValue1 == l_Undef )
     {
 p->timeSatUndec += clock() - clk;
-        p->nSatFails++;
+        p->nSatCallsUndec++;
         return -1;
     }
 
@@ -725,11 +743,9 @@ clk = clock();
 p->timeSat += clock() - clk;
     if ( RetValue1 == l_False )
     {
-        pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
         pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
         RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
         assert( RetValue );
-        pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
         pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
 p->timeSatUnsat += clock() - clk;
         p->nSatCallsUnsat++;
@@ -744,7 +760,7 @@ p->timeSatSat += clock() - clk;
     else // if ( RetValue1 == l_Undef )
     {
 p->timeSatUndec += clock() - clk;
-        p->nSatFails++;
+        p->nSatCallsUndec++;
         return -1;
     }
     // return SAT proof
@@ -766,15 +782,17 @@ p->timeSatUndec += clock() - clk;
 int Gia_SweeperCondCheckUnsat( Gia_Man_t * pGia )
 {
     Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
-    int RetValue, iLitAig, i;
+    int RetValue, ProbeId, iLitAig, i;
     clock_t clk;
-    p->nSatCalls++;
     assert( p->pSat != NULL );
+    p->nSatCalls++;
     p->vCexUser = NULL;
 
+    // create logic cones and the array of assumptions
     Vec_IntClear( p->vCondAssump );
-    Vec_IntForEachEntry( p->vCondLits, iLitAig, i )
+    Vec_IntForEachEntry( p->vCondProbes, ProbeId, i )
     {
+        iLitAig = Gia_SweeperProbeLit( pGia, ProbeId );
         Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitAig) );
         Vec_IntPush( p->vCondAssump, Swp_ManLit2Lit(p, iLitAig) );
     }
@@ -786,9 +804,10 @@ clk = clock();
 p->timeSat += clock() - clk;
     if ( RetValue == l_False )
     {
-        assert( Vec_IntSize(p->vCondLits) > 0 );
+        assert( Vec_IntSize(p->vCondProbes) > 0 );
 p->timeSatUnsat += clock() - clk;
         p->nSatCallsUnsat++;
+        p->nSatProofs++;
         return 1;
     }
     else if ( RetValue == l_True )
@@ -801,7 +820,7 @@ p->timeSatSat += clock() - clk;
     else // if ( RetValue1 == l_Undef )
     {
 p->timeSatUndec += clock() - clk;
-        p->nSatFails++;
+        p->nSatCallsUndec++;
         return -1;
     }
 }
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 731cf9a1..ead6bd60 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -174,6 +174,14 @@ static inline Vec_Ptr_t * Vec_PtrDup( Vec_Ptr_t * pVec )
     memcpy( p->pArray, pVec->pArray, sizeof(void *) * pVec->nSize );
     return p;
 }
+static inline Vec_Ptr_t * Vec_PtrDupStr( Vec_Ptr_t * pVec )
+{
+    int i;
+    Vec_Ptr_t * p = Vec_PtrDup( pVec );
+    for ( i = 0; i < p->nSize; i++ )
+        p->pArray[i] = Abc_UtilStrsav( (char *)p->pArray[i] );
+    return p;
+}
 
 /**Function*************************************************************