Experiments with SAT-based simulation.

8 files changed, 59 insertions, 18 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 );
 }
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2259d3ff..0c2b72ec 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -13050,7 +13050,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //        Cba_PrsReadBlifTest();
     }
 //    Abc_NtkComputePaths( Abc_FrameReadNtk(pAbc) );
-//    Maj_ManExactSynthesisTest();
+//    Psl_FileTest();
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
diff --git a/src/proof/cec/cecSat.c b/src/proof/cec/cecSat.c
index 1d2ebd1d..5421e885 100644
--- a/src/proof/cec/cecSat.c
+++ b/src/proof/cec/cecSat.c
@@ -278,26 +278,28 @@ void Cec2_AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper,
   SeeAlso     []
 
 ***********************************************************************/
-void Cec2_CollectSuper_rec( Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
+void Cec2_CollectSuper_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
 {
+    //printf( "v%d ", Gia_ObjValue(pObj) );
     // if the new node is complemented or a PI, another gate begins
     if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) || 
-         (!fFirst && Gia_ObjValue(pObj) > 1) || 
+//         (!fFirst && Gia_ObjValue(pObj) > 1) || 
+         (!fFirst && (p->pRefs ? Gia_ObjRefNum(p, pObj) : Gia_ObjValue(pObj)) > 1) || 
          (fUseMuxes && pObj->fMark0) )
     {
         Vec_PtrPushUnique( vSuper, pObj );
         return;
     }
     // go through the branches
-    Cec2_CollectSuper_rec( Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes );
-    Cec2_CollectSuper_rec( Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes );
+    Cec2_CollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes );
+    Cec2_CollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes );
 }
-void Cec2_CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
+void Cec2_CollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
 {
     assert( !Gia_IsComplement(pObj) );
     assert( !Gia_ObjIsCi(pObj) );
     Vec_PtrClear( vSuper );
-    Cec2_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
+    Cec2_CollectSuper_rec( p, pObj, vSuper, 1, fUseMuxes );
 }
 void Cec2_ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, satoko_t * pSat )
 {
@@ -360,10 +362,11 @@ int Gia_ObjGetCnfVar( Gia_Man_t * pGia, int iObj, Vec_Ptr_t * vFrontier, Vec_Ptr
         }
         else
         {
-            Cec2_CollectSuper( pNode, fUseMuxes, vFanins );
+            Cec2_CollectSuper( pGia, pNode, fUseMuxes, vFanins );
             Vec_PtrForEachEntry( Gia_Obj_t *, vFanins, pFanin, k )
                 Cec2_ObjAddToFrontier( pGia, Gia_Regular(pFanin), vFrontier, pSat );
-            Cec2_AddClausesSuper( pGia, pNode, vFanins, pSat );
+            Cec2_AddClausesSuper( pGia, pNode, vFanins, pSat ); 
+            //printf( "%d ", Vec_PtrSize(vFanins) );
         }
         assert( Vec_PtrSize(vFanins) > 1 );
     }
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h
index 7ee8cd85..347bd187 100644
--- a/src/sat/satoko/satoko.h
+++ b/src/sat/satoko/satoko.h
@@ -76,6 +76,7 @@ struct satoko_stats {
 
     long n_decisions;
     long n_propagations;
+    long n_propagations_all;
     long n_inspects;
     long n_conflicts;
     long n_conflicts_all;
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index 6e58e8a5..6ea1a0b4 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -620,6 +620,7 @@ unsigned solver_propagate(solver_t *s)
         watch_list_shrink(ws, j - watch_list_array(ws));
     }
     s->stats.n_propagations += n_propagations;
+    s->stats.n_propagations_all += n_propagations;
     s->n_props_simplify -= n_propagations;
     return conf_cref;
 }
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index 79d48c3b..0193b1c3 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -45,9 +45,11 @@ static inline int clause_is_satisfied(solver_t *s, struct clause *clause)
 
 static inline void solver_clean_stats(solver_t *s)
 {
-    int n_conflicts_all = s->stats.n_conflicts_all;
+    long n_conflicts_all = s->stats.n_conflicts_all;
+    long n_propagations_all = s->stats.n_propagations_all;
     memset(&(s->stats), 0, sizeof(struct satoko_stats));
     s->stats.n_conflicts_all = n_conflicts_all;
+    s->stats.n_propagations_all = n_propagations_all;
 }
 
 static inline void print_opts(solver_t *s)