Experiments with SAT-based cube enumeration.

3 files changed, 38 insertions, 5 deletions

diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 029d1599..81362276 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -426,6 +426,39 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+Gia_Man_t * Gia_ManDupOnsetOffset( 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_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+        pObj->Value = Gia_ManAppendCo( pNew, Abc_LitNot(Gia_ObjFanin0Copy(pObj)) );
+    }
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while putting first PIs, then nodes, then POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Gia_Man_t * Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis )
 {
     Gia_Man_t * pNew;
diff --git a/src/aig/gia/giaMf.c b/src/aig/gia/giaMf.c
index 03848f1e..b90e7bc9 100644
--- a/src/aig/gia/giaMf.c
+++ b/src/aig/gia/giaMf.c
@@ -346,9 +346,9 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla )
         Gia_ManForEachAndReverseId( p->pGia, Id )
             if ( Mf_ObjMapRefNum(p, Id) )
                 Vec_IntWriteEntry( vCnfIds, Id, Id ), iVar++;
+        Vec_IntWriteEntry( vCnfIds, 0, 0 );
         Gia_ManForEachCiId( p->pGia, Id, i )
             Vec_IntWriteEntry( vCnfIds, Id, Id );
-        Vec_IntWriteEntry( vCnfIds, 0, 0 );
         assert( iVar == nVars );
     }
     else
@@ -358,9 +358,9 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla )
         Gia_ManForEachAndReverseId( p->pGia, Id )
             if ( Mf_ObjMapRefNum(p, Id) )
                 Vec_IntWriteEntry( vCnfIds, Id, iVar++ );
+        Vec_IntWriteEntry( vCnfIds, 0, iVar++ );
         Gia_ManForEachCiId( p->pGia, Id, i )
             Vec_IntWriteEntry( vCnfIds, Id, iVar++ );
-        Vec_IntWriteEntry( vCnfIds, 0, iVar++ );
         assert( iVar == nVars );
     }
     // generate CNF
diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c
index a14ec443..b7d678b3 100644
--- a/src/aig/gia/giaQbf.c
+++ b/src/aig/gia/giaQbf.c
@@ -75,7 +75,7 @@ int Gia_ManSatEnum( Gia_Man_t * pGia, int nConfLimit, int nTimeOut, int fVerbose
     abctime clkStart = Abc_Clock();
     pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 );
     pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
-    iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 1;
+    iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1;
     Cnf_DataFree( pCnf );
     // iterate through the SAT assignment
     vLits = Vec_IntAlloc( Gia_ManPiNum(pGia) );
@@ -180,7 +180,7 @@ Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose )
     p->nPars      = nPars;
     p->nVars      = Gia_ManPiNum(pGia) - nPars;
     p->fVerbose   = fVerbose;
-    p->iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 1;
+    p->iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1;
     p->pSatVer    = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     p->pSatSyn    = sat_solver_new();
     p->vValues    = Vec_IntAlloc( Gia_ManPiNum(pGia) );
@@ -280,7 +280,7 @@ Gia_Man_t * Gia_QbfCofactor( Gia_Man_t * p, int nPars, Vec_Int_t * vValues, Vec_
 int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof )
 {
     Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 1, 0 );
-    int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) - 1;
+    int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof);// - 1;
     pCnf->pMan = NULL;
     Cnf_DataLift( pCnf, sat_solver_nvars(p->pSatSyn) );
     for ( i = 0; i < pCnf->nClauses; i++ )