Experiments with SAT sweeping.

3 files changed, 13 insertions, 11 deletions

diff --git a/src/sat/bmc/bmcGen.c b/src/sat/bmc/bmcGen.c
index 5d84ce87..460c9fec 100644
--- a/src/sat/bmc/bmcGen.c
+++ b/src/sat/bmc/bmcGen.c
@@ -46,13 +46,13 @@ ABC_NAMESPACE_IMPL_START
 ***********************************************************************/
 static inline word * Gia_ManMoObj( Gia_Man_t * p, int iObj )
 {
-    return Vec_WrdEntryP( p->vSims, iObj * p->iPatsPi );
+    return Vec_WrdEntryP( p->vSims, iObj * p->nSimWords );
 }
 static inline void Gia_ManMoSetCi( Gia_Man_t * p, int iObj )
 {
     int w;
     word * pSims = Gia_ManMoObj( p, iObj );
-    for ( w = 0; w < p->iPatsPi; w++ )
+    for ( w = 0; w < p->nSimWords; w++ )
         pSims[w] = Gia_ManRandomW( 0 );
 }
 static inline void Gia_ManMoSimAnd( Gia_Man_t * p, int iObj )
@@ -65,19 +65,19 @@ static inline void Gia_ManMoSimAnd( Gia_Man_t * p, int iObj )
     if ( Gia_ObjFaninC0(pObj) )
     {
         if (  Gia_ObjFaninC1(pObj) )
-            for ( w = 0; w < p->iPatsPi; w++ )
+            for ( w = 0; w < p->nSimWords; w++ )
                 pSims[w] = ~(pSims0[w] | pSims1[w]);
         else 
-            for ( w = 0; w < p->iPatsPi; w++ )
+            for ( w = 0; w < p->nSimWords; w++ )
                 pSims[w] = ~pSims0[w] & pSims1[w];
     }
     else 
     {
         if (  Gia_ObjFaninC1(pObj) )
-            for ( w = 0; w < p->iPatsPi; w++ )
+            for ( w = 0; w < p->nSimWords; w++ )
                 pSims[w] = pSims0[w] & ~pSims1[w];
         else 
-            for ( w = 0; w < p->iPatsPi; w++ )
+            for ( w = 0; w < p->nSimWords; w++ )
                 pSims[w] = pSims0[w] & pSims1[w];
     }
 }
@@ -89,12 +89,12 @@ static inline void Gia_ManMoSetCo( Gia_Man_t * p, int iObj )
     word * pSims0 = Gia_ManMoObj( p, Gia_ObjFaninId0(pObj, iObj) );
     if ( Gia_ObjFaninC0(pObj) )
     {
-        for ( w = 0; w < p->iPatsPi; w++ )
+        for ( w = 0; w < p->nSimWords; w++ )
             pSims[w] = ~pSims0[w];
     }
     else 
     {
-        for ( w = 0; w < p->iPatsPi; w++ )
+        for ( w = 0; w < p->nSimWords; w++ )
             pSims[w] = pSims0[w];
     }
 }
@@ -102,7 +102,7 @@ void Gia_ManMoFindSimulate( Gia_Man_t * p, int nWords )
 {
     int i, iObj;
     Gia_ManRandomW( 1 );
-    p->iPatsPi = nWords;
+    p->nSimWords = nWords;
     if ( p->vSims )
         Vec_WrdFill( p->vSims, nWords * Gia_ManObjNum(p), 0 );
     else
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h
index 88070eac..7c2f3720 100644
--- a/src/sat/satoko/satoko.h
+++ b/src/sat/satoko/satoko.h
@@ -83,7 +83,7 @@ extern void satoko_destroy(satoko_t *);
 extern void satoko_default_opts(satoko_opts_t *);
 extern void satoko_configure(satoko_t *, satoko_opts_t *);
 extern int  satoko_parse_dimacs(char *, satoko_t **);
-extern void satoko_add_variable(satoko_t *, char);
+extern int  satoko_add_variable(satoko_t *, char);
 extern int  satoko_add_clause(satoko_t *, unsigned *, unsigned);
 extern void satoko_assump_push(satoko_t *s, unsigned);
 extern void satoko_assump_pop(satoko_t *s);
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index 9cad0a14..e03cc084 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -216,7 +216,7 @@ int satoko_simplify(solver_t * s)
     return SATOKO_OK;
 }
 
-void satoko_add_variable(solver_t *s, char sign)
+int satoko_add_variable(solver_t *s, char sign)
 {
     unsigned var = vec_act_size(s->activity);
     vec_wl_push(s->watches);
@@ -231,6 +231,7 @@ void satoko_add_variable(solver_t *s, char sign)
     heap_insert(s->var_order, var);
     if (s->marks)
         vec_char_push_back(s->marks, 0);
+    return var;
 }
 
 int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size)
@@ -351,6 +352,7 @@ void satoko_rollback(satoko_t *s)
         clause_unwatch(s, cdb_cref(s->all_clauses, (unsigned *)cl_to_remove[i]));
         cl_to_remove[i]->f_mark = 1;
     }
+    satoko_free(cl_to_remove);
     vec_uint_shrink(s->originals, s->book_cl_orig);
     vec_uint_shrink(s->learnts, s->book_cl_lrnt);
     /* Shrink variable related vectors */