SAT sweeping under constraints.

10 files changed, 178 insertions, 6 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 41093a30..95700aaf 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1097,6 +1097,7 @@ extern void                Gia_ManInvertConstraints( Gia_Man_t * pAig );
 extern void                Gia_ManInvertPos( Gia_Man_t * pAig );
 extern int                 Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 );
 extern void                Gia_ManMarkFanoutDrivers( Gia_Man_t * p );
+extern void                Gia_ManSwapPos( Gia_Man_t * p, int i );
 
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index f3f60267..92248225 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -600,7 +600,7 @@ void Gia_ManDupAppendShare( Gia_Man_t * pNew, Gia_Man_t * pTwo )
     Gia_ManForEachObj1( pTwo, pObj, i )
     {
         if ( Gia_ObjIsAnd(pObj) )
-            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         else if ( Gia_ObjIsCi(pObj) )
             pObj->Value = Gia_Obj2Lit( pNew, Gia_ManCi( pNew, Gia_ObjCioId(pObj) ) );
         else if ( Gia_ObjIsCo(pObj) )
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index f4b5bcb6..dbad82c6 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -61,6 +61,7 @@ Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p )
     Gia_ManForEachCo( p, pObj, i )
         pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    pNew->nConstrs = p->nConstrs;
     assert( Gia_ManIsNormalized(pNew) );
     Gia_ManDupRemapEquiv( pNew, p );
     return pNew;
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 1d122112..8c1b6b12 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1338,6 +1338,31 @@ void Gia_ManMarkFanoutDrivers( Gia_Man_t * p )
         else if ( Gia_ObjIsCo(pObj) )
             Gia_ObjFanin0(pObj)->fMark0 = 1;
 }
+
+
+/**Function*************************************************************
+
+  Synopsis    [Swaps PO number 0 with PO number i.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSwapPos( Gia_Man_t * p, int i )
+{
+    int Lit0, LitI;
+    assert( i >= 0 && i < Gia_ManPoNum(p) );
+    if ( i == 0 )
+        return;
+    Lit0 = Gia_ObjFaninLit0p( p, Gia_ManPo(p, 0) );
+    LitI = Gia_ObjFaninLit0p( p, Gia_ManPo(p, i) );
+    Gia_ManPatchCoDriver( p, 0, LitI );
+    Gia_ManPatchCoDriver( p, i, Lit0 );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b15b5b04..0eba452d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27148,7 +27148,7 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     Ssc_Pars_t Pars, * pPars = &Pars;
     Ssc_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WCvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WCavh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -27174,6 +27174,9 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nBTLimit < 0 )
                 goto usage;
             break;
+        case 'a':
+            pPars->fAppend ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -27191,12 +27194,13 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &cfraig [-WC <num>] [-rmdwvh]\n" );
+    Abc_Print( -2, "usage: &cfraig [-WC <num>] [-avh]\n" );
     Abc_Print( -2, "\t         performs combinational SAT sweeping under constraints\n" );
     Abc_Print( -2, "\t         which are present in the AIG or set manually using \"constr\"\n" );
     Abc_Print( -2, "\t         (constraints are listed as last POs and true when they are 0)\n" );
     Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+    Abc_Print( -2, "\t-a     : toggle appending constraints to the result [default = %s]\n", pPars->fAppend? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -31513,7 +31517,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //     extern void Unr_ManTest( Gia_Man_t * pGia );
 //    extern void Mig_ManTest( Gia_Man_t * pGia );
 //    extern int Gia_ManVerify( Gia_Man_t * pGia );
-    extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose );
+//    extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose );
+    extern Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p );
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
@@ -31565,7 +31570,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Unr_ManTest( pAbc->pGia );
 //    Mig_ManTest( pAbc->pGia );
 //    Gia_ManVerifyWithBoxes( pAbc->pGia );
-    pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 );
+//    pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 );
+    pTemp = Gia_ManOptimizeRing( pAbc->pGia );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 usage:
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 60352a0f..5222ef53 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -888,6 +888,26 @@ static inline int Vec_IntRemove( Vec_Int_t * p, int Entry )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntDrop( Vec_Int_t * p, int i )
+{
+    int k;
+    assert( i >= 0 && i < Vec_IntSize(p) );
+    p->nSize--;
+    for ( k = i; k < p->nSize; k++ )
+        p->pArray[k] = p->pArray[k+1];
+}
+
+/**Function*************************************************************
+
   Synopsis    [Interts entry at the index iHere. Shifts other entries.]
 
   Description []
diff --git a/src/proof/ssc/ssc.h b/src/proof/ssc/ssc.h
index de32ffc1..1112719c 100644
--- a/src/proof/ssc/ssc.h
+++ b/src/proof/ssc/ssc.h
@@ -47,6 +47,7 @@ struct Ssc_Pars_t_
     int              nBTLimit;      // conflict limit at a node
     int              nSatVarMax;    // the max number of SAT variables
     int              nCallsRecycle; // calls to perform before recycling SAT solver
+    int              fAppend;       // append constraints to the resulting AIG
     int              fVerbose;      // verbose stats
 };
 
diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c
index 00491e31..b29a0193 100644
--- a/src/proof/ssc/sscCore.c
+++ b/src/proof/ssc/sscCore.c
@@ -313,6 +313,11 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
     pAig = Gia_ManDupLevelized( pResult = pAig );
     Gia_ManStop( pResult );
     pResult = Ssc_PerformSweeping( pAig, pCare, pPars );
+    if ( pPars->fAppend )
+    {
+        Gia_ManDupAppendShare( pResult, pCare );
+        pResult->nConstrs = Gia_ManPoNum(pCare);
+    }
     Gia_ManStop( pAig );
     Gia_ManStop( pCare );
     return pResult;
diff --git a/src/proof/ssc/sscSat.c b/src/proof/ssc/sscSat.c
index f6d5e9af..1de99c2e 100644
--- a/src/proof/ssc/sscSat.c
+++ b/src/proof/ssc/sscSat.c
@@ -260,7 +260,7 @@ p->timeCnfGen += clock() - clk;
 ***********************************************************************/
 void Ssc_ManStartSolver( Ssc_Man_t * p )
 {
-    Aig_Man_t * pMan = Gia_ManToAig( p->pFraig, 0 );
+    Aig_Man_t * pMan = Gia_ManToAigSimple( p->pFraig );
     Cnf_Dat_t * pDat = Cnf_Derive( pMan, 0 );
     Gia_Obj_t * pObj;
     sat_solver * pSat;
diff --git a/src/proof/ssc/sscUtil.c b/src/proof/ssc/sscUtil.c
index 21d78f85..c4edaba6 100644
--- a/src/proof/ssc/sscUtil.c
+++ b/src/proof/ssc/sscUtil.c
@@ -19,6 +19,8 @@
 ***********************************************************************/
 
 #include "sscInt.h"
+#include "sat/cnf/cnf.h"
+#include "aig/gia/giaAig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -42,6 +44,117 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+Gia_Man_t * Gia_ManDropContained( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Aig_Man_t * pMan = Gia_ManToAigSimple( p );
+    Cnf_Dat_t * pDat = Cnf_Derive( pMan, Gia_ManPoNum(p) );
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vLits, * vKeep;
+    sat_solver * pSat;
+    int i, status, Count = 0;
+    Aig_ManStop( pMan );
+
+    vLits = Vec_IntAlloc( Gia_ManPoNum(p) );
+    Gia_ManForEachPo( p, pObj, i )
+    {
+        int iObj = Gia_ObjId( p, pObj );
+        Vec_IntPush( vLits, Abc_Var2Lit(pDat->pVarNums[iObj], 1) );
+    }
+
+    // start the SAT solver
+    pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, pDat->nVars );
+    for ( i = 0; i < pDat->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pDat->pClauses[i], pDat->pClauses[i+1] ) )
+        {
+            Cnf_DataFree( pDat );
+            sat_solver_delete( pSat );
+            Vec_IntFree( vLits );
+            return NULL;
+        }
+    }
+    status = sat_solver_simplify( pSat );
+    if ( status == 0 )
+    {
+        Cnf_DataFree( pDat );
+        sat_solver_delete( pSat );
+        Vec_IntFree( vLits );
+        return NULL;
+    }
+
+    // iterate over POs
+    vKeep = Vec_IntAlloc( Gia_ManPoNum(p) );
+    Gia_ManForEachPo( p, pObj, i )
+    {
+        Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits,i)) );
+        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
+        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 );
+        return Gia_ManDup(p);
+    }
+    pNew = Gia_ManDupCones( p, Vec_IntArray(vKeep), Vec_IntSize(vKeep), 0 );
+    Vec_IntFree( vKeep );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p )
+{
+    Ssc_Pars_t Pars, * pPars = &Pars;
+    Gia_Man_t * pTemp, * pAux;
+    int i;
+    assert( p->nConstrs == 0 );
+    printf( "User AIG: " );
+    Gia_ManPrintStats( p, 0, 0, 0 );
+    pTemp = Gia_ManDropContained( p );
+    printf( "Drop AIG: " );
+    Gia_ManPrintStats( pTemp, 0, 0, 0 );
+//    return pTemp;
+    if ( Gia_ManPoNum(pTemp) == 1 )
+        return pTemp;
+    Ssc_ManSetDefaultParams( pPars );
+    pPars->fAppend  = 1;
+    pPars->fVerbose = 1;
+    pTemp->nConstrs = Gia_ManPoNum(pTemp) - 1;    
+    for ( i = 0; i < Gia_ManPoNum(pTemp); i++ )
+    {
+        Gia_ManSwapPos( pTemp, i );
+        pTemp = Ssc_PerformSweepingConstr( pAux = pTemp, pPars );
+        Gia_ManStop( pAux );
+        pTemp = Gia_ManDupNormalize( pAux = pTemp );
+        Gia_ManStop( pAux );
+        Gia_ManSwapPos( pTemp, i );
+        printf( "AIG%3d  : " );
+        Gia_ManPrintStats( pTemp, 0, 0, 0 );
+    }
+    return pTemp;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///