Experiments with SAT-based simulation.

3 files changed, 42 insertions, 8 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index fcdb3941..20648b39 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1219,7 +1219,8 @@ extern Vec_Int_t *         Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_
 typedef struct Cbs_Man_t_  Cbs_Man_t;
 extern Cbs_Man_t *         Cbs_ManAlloc( Gia_Man_t * pGia );
 extern void                Cbs_ManStop( Cbs_Man_t * p );
-extern int                 Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
+extern int                 Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj );
+extern int                 Cbs_ManSolve2( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
 extern Vec_Int_t *         Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
 extern void                Cbs_ManSetConflictNum( Cbs_Man_t * p, int Num );
 extern Vec_Int_t *         Cbs_ReadModel( Cbs_Man_t * p );
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index 31f32e30..baf1b418 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -246,6 +246,15 @@ static inline void Cbs_ManSaveModel( Cbs_Man_t * p, Vec_Int_t * vCex )
 //            Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) );
             Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !Cbs_VarValue(pVar)) );
 } 
+static inline void Cbs_ManSaveModelAll( Cbs_Man_t * p, Vec_Int_t * vCex )
+{
+    Gia_Obj_t * pVar;
+    int i;
+    Vec_IntClear( vCex );
+    p->pProp.iHead = 0;
+    Cbs_QueForEachEntry( p->pProp, pVar, i )
+        Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) );
+} 
 
 /**Function*************************************************************
 
@@ -929,12 +938,35 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
   Returns 1 if unsatisfiable, 0 if satisfiable, and -1 if undecided.
   The node may be complemented. ]
                
-  SideEffects []
+  SideEffects [The two procedures differ in the CEX format.]
 
   SeeAlso     []
 
 ***********************************************************************/
-int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 )
+int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
+{
+    int RetValue = 0;
+    s_Counter = 0;
+    assert( !p->pProp.iHead && !p->pProp.iTail );
+    assert( !p->pJust.iHead && !p->pJust.iTail );
+    assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
+    p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
+    Cbs_ManAssign( p, pObj, 0, NULL, NULL );
+    if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) )
+        Cbs_ManSaveModel( p, p->vModel );
+    else
+        RetValue = 1;
+    Cbs_ManCancelUntil( p, 0 );
+    p->pJust.iHead = p->pJust.iTail = 0;
+    p->pClauses.iHead = p->pClauses.iTail = 1;
+    p->Pars.nBTTotal += p->Pars.nBTThis;
+    p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
+    if ( Cbs_ManCheckLimits( p ) )
+        RetValue = -1;
+//    printf( "%d ", s_Counter );
+    return RetValue;
+}
+int Cbs_ManSolve2( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 )
 {
     int RetValue = 0;
     s_Counter = 0;
@@ -946,7 +978,7 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 )
     if ( pObj2 ) 
     Cbs_ManAssign( p, pObj2, 0, NULL, NULL );
     if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) )
-        Cbs_ManSaveModel( p, p->vModel );
+        Cbs_ManSaveModelAll( p, p->vModel );
     else
         RetValue = 1;
     Cbs_ManCancelUntil( p, 0 );
@@ -956,7 +988,6 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 )
     p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
     if ( Cbs_ManCheckLimits( p ) )
         RetValue = -1;
-
 //    printf( "%d ", s_Counter );
     return RetValue;
 }
@@ -1052,14 +1083,14 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
         clk = Abc_Clock();
         p->Pars.fUseHighest = 1;
         p->Pars.fUseLowest  = 0;
-        status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot), NULL );
+        status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
 //        printf( "\n" );
 /*
         if ( status == -1 )
         {
             p->Pars.fUseHighest = 0;
             p->Pars.fUseLowest  = 1;
-            status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot), NULL );
+            status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
         }
 */
         Vec_StrPush( vStatus, (char)status );
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 228f6fb4..88e94156 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -1182,7 +1182,7 @@ void Gia_ManIncrSimSet( Gia_Man_t * p, Vec_Int_t * vObjLits )
         if ( Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(iLit))) )
             continue;
         //assert( Vec_IntEntry(p->vTimeStamps, Abc_Lit2Var(iLit)) == p->iTimeStamp-1 );
-        //Vec_IntWriteEntry(p->vTimeStamps, Abc_Lit2Var(iLit), p->iTimeStamp);
+        Vec_IntWriteEntry(p->vTimeStamps, Abc_Lit2Var(iLit), p->iTimeStamp);
         if ( Abc_TtGetBit(pSims, p->iPatsPi) == Abc_LitIsCompl(iLit) )
              Abc_TtXorBit(pSims, p->iPatsPi);
     }
@@ -1208,6 +1208,7 @@ int Gia_ManIncrSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 )
     Gia_ManIncrSimUpdate( p );
     Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit0) );
     Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit1) );
+//    return 0; // disable
     return Gia_ManBuiltInSimCheckOver( p, iLit0, iLit1 );
 }
 int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 )
@@ -1216,6 +1217,7 @@ int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 )
     Gia_ManIncrSimUpdate( p );
     Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit0) );
     Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit1) );
+//    return 1; // disable
     return Gia_ManBuiltInSimCheckEqual( p, iLit0, iLit1 );
 }