Bug fix related to not properly resizing SAT solver's model array.

11 files changed, 45 insertions, 151 deletions

diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index 90659333..9548c166 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -1303,7 +1303,8 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
         if ( RetValue != l_False )
         {
 //            printf( "S- " );
-            Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model.ptr + p->nFrames * p->pCnf->nVars );
+//            Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model.ptr + p->nFrames * p->pCnf->nVars );
+            Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model + p->nFrames * p->pCnf->nVars );
 //            RetValue = Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg);
 //            assert( RetValue );
 
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 37620a16..8f912915 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -244,7 +244,8 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
     int i;
     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
     Aig_ManForEachPi( p->pManFraig, pObj, i )
-        if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
+//        if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
+        if ( sat_solver_var_value(p->pSat, Fra_ObjSatNum(pObj)) )
             Aig_InfoSetBit( p->pPatWords, i );
 
     if ( p->vCex )
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 48e09ae9..7cc00556 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -83,118 +83,6 @@ extern Vec_Int_t * Gia_VtaCollect( Gia_Man_t * p, Vec_Int_t ** pvFraLims, Vec_In
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark )
-{
-    lit Lits[1];
-    int Cid;
-    assert( iVar >= 0 );
-
-    Lits[0] = toLitCond( iVar, fCompl );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 1 );
-    if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
-    return 1;
-}
-static inline int sat_solver2_add_buffer( sat_solver2 * pSat, int iVarA, int iVarB, int fCompl, int fMark )
-{
-    lit Lits[2];
-    int Cid;
-    assert( iVarA >= 0 && iVarB >= 0 );
-
-    Lits[0] = toLitCond( iVarA, 0 );
-    Lits[1] = toLitCond( iVarB, !fCompl );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
-    if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
-
-    Lits[0] = toLitCond( iVarA, 1 );
-    Lits[1] = toLitCond( iVarB, fCompl );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
-    if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
-    return 2;
-}
-static inline int sat_solver2_add_and( sat_solver2 * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fMark )
-{
-    lit Lits[3];
-    int Cid;
-
-    Lits[0] = toLitCond( iVar, 1 );
-    Lits[1] = toLitCond( iVar0, fCompl0 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
-    if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
-
-    Lits[0] = toLitCond( iVar, 1 );
-    Lits[1] = toLitCond( iVar1, fCompl1 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
-    if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
-
-    Lits[0] = toLitCond( iVar, 0 );
-    Lits[1] = toLitCond( iVar0, !fCompl0 );
-    Lits[2] = toLitCond( iVar1, !fCompl1 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
-    if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
-    return 3;
-}
-static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB, int iVarC, int fCompl, int fMark )
-{
-    lit Lits[3];
-    int Cid;
-    assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
-
-    Lits[0] = toLitCond( iVarA, !fCompl );
-    Lits[1] = toLitCond( iVarB, 1 );
-    Lits[2] = toLitCond( iVarC, 1 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
-    if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
-
-    Lits[0] = toLitCond( iVarA, !fCompl );
-    Lits[1] = toLitCond( iVarB, 0 );
-    Lits[2] = toLitCond( iVarC, 0 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
-    if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
-
-    Lits[0] = toLitCond( iVarA, fCompl );
-    Lits[1] = toLitCond( iVarB, 1 );
-    Lits[2] = toLitCond( iVarC, 0 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
-    if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
-
-    Lits[0] = toLitCond( iVarA, fCompl );
-    Lits[1] = toLitCond( iVarB, 0 );
-    Lits[2] = toLitCond( iVarC, 1 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
-    if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
-    return 4;
-}
-static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int fCompl, int fMark )
-{
-    lit Lits[2];
-    int Cid;
-    assert( iVar >= 0 );
-
-    Lits[0] = toLitCond( iVar, fCompl );
-    Lits[1] = toLitCond( iVar+1, 0 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
-    if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
-
-    Lits[0] = toLitCond( iVar, fCompl );
-    Lits[1] = toLitCond( iVar+1, 1 );
-    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
-    if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
-    return 2;
-}
-
-
 
 /**Function*************************************************************
 
diff --git a/src/aig/int/intContain.c b/src/aig/int/intContain.c
index d4af0ae8..77b057a7 100644
--- a/src/aig/int/intContain.c
+++ b/src/aig/int/intContain.c
@@ -274,7 +274,12 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf
     int Counter;
     if ( nFrames == 1 )
         return 1;
-    if ( pSat->model.size == 0 )
+//    if ( pSat->model.size == 0 )
+    
+    // possible consequences here!!!
+    assert( 0 );
+
+    if ( sat_solver_nvars(pSat) == 0 )
         return 1;
 //    assert( Saig_ManPoNum(p) == 1 );
     assert( Aig_ManRegNum(p) > 0 );
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index f7c0743b..7cf97132 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -1518,7 +1518,8 @@ int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p )
     int i;
     pModel = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
     Ivy_ManForEachPi( p->pManFraig, pObj, i )
-        pModel[i] = ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True );
+//        pModel[i] = ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True );
+        pModel[i] = ( p->pSat->model[Ivy_ObjSatNum(pObj)] == l_True );
     return pModel;
 }
 
@@ -1540,7 +1541,8 @@ void Ivy_FraigSavePattern( Ivy_FraigMan_t * p )
     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
     Ivy_ManForEachPi( p->pManFraig, pObj, i )
 //    Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPiVars, pObj, i )
-        if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
+//        if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
+        if ( p->pSat->model[Ivy_ObjSatNum(pObj)] == l_True )
             Ivy_InfoSetBit( p->pPatWords, i );
 //            Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
 }
@@ -1563,7 +1565,8 @@ void Ivy_FraigSavePattern2( Ivy_FraigMan_t * p )
     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
 //    Ivy_ManForEachPi( p->pManFraig, pObj, i )
     Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPiVars, pObj, i )
-        if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
+//        if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
+        if ( p->pSat->model[Ivy_ObjSatNum(pObj)] == l_True )
 //            Ivy_InfoSetBit( p->pPatWords, i );
             Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
 }
@@ -1586,7 +1589,8 @@ void Ivy_FraigSavePattern3( Ivy_FraigMan_t * p )
     for ( i = 0; i < p->nPatWords; i++ )
         p->pPatWords[i] = Ivy_ObjRandomSim();
     Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPiVars, pObj, i )
-        if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ (p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True) )
+//        if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ (p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True) )
+        if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ sat_solver_var_value(p->pSat, Ivy_ObjSatNum(pObj)) )
             Ivy_InfoXorBit( p->pPatWords, pObj->Id - 1 );
 }
 
diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c
index a17f92fa..17f3d661 100644
--- a/src/opt/res/resSat.c
+++ b/src/opt/res/resSat.c
@@ -279,7 +279,8 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
             for ( i = 0; i < p->nTruePis; i++ )
             {
                 Var = (int)(ABC_PTRUINT_T)Abc_NtkPi(p->pAig,i)->pCopy;
-                value = (int)(pSat->model.ptr[Var] == l_True);
+//                value = (int)(pSat->model.ptr[Var] == l_True);
+                value = sat_solver_var_value(pSat, Var);
                 if ( value )
                     Abc_InfoSetBit( (unsigned *)Vec_PtrEntry(vPats, i), k );
                 Lit = toLitCond( Var, value );
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 5a05e3b0..a4bd29cd 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -938,7 +938,7 @@ sat_solver* sat_solver_new(void)
     veci_new(&s->trail_lim);
     veci_new(&s->tagged);
     veci_new(&s->stack);
-    veci_new(&s->model);
+//    veci_new(&s->model);
     veci_new(&s->act_vars);
     veci_new(&s->temp_clause);
     veci_new(&s->conf_final);
@@ -1010,6 +1010,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
         s->orderpos  = ABC_REALLOC(int,    s->orderpos, s->cap);
         s->reasons   = ABC_REALLOC(int,    s->reasons,  s->cap);
         s->trail     = ABC_REALLOC(lit,    s->trail,    s->cap);
+        s->model     = ABC_REALLOC(int,    s->model,    s->cap);
         memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(veci) );
     } 
 
@@ -1054,7 +1055,7 @@ void sat_solver_delete(sat_solver* s)
     veci_delete(&s->trail_lim);
     veci_delete(&s->tagged);
     veci_delete(&s->stack);
-    veci_delete(&s->model);
+//    veci_delete(&s->model);
     veci_delete(&s->act_vars);
     veci_delete(&s->temp_clause);
     veci_delete(&s->conf_final);
@@ -1075,6 +1076,7 @@ void sat_solver_delete(sat_solver* s)
         ABC_FREE(s->orderpos );
         ABC_FREE(s->reasons  );
         ABC_FREE(s->trail    );
+        ABC_FREE(s->model    );
     }
 
     sat_solver_store_free(s);
@@ -1326,7 +1328,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
     s->stats.starts++;
 //    s->var_decay = (float)(1 / var_decay   );  // move this to sat_solver_new()
 //    s->cla_decay = (float)(1 / clause_decay);  // move this to sat_solver_new()
-    veci_resize(&s->model,0);
+//    veci_resize(&s->model,0);
     veci_new(&learnt_clause);
 
     // use activity factors in every even restart
@@ -1408,9 +1410,8 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
             if (next == var_Undef){
                 // Model found:
                 int i;
-                veci_resize(&s->model, 0);
-                for (i = 0; i < s->size; i++) 
-                    veci_push( &s->model, var_value(s,i)==var1 ? l_True : l_False );
+                for (i = 0; i < s->size; i++)
+                    s->model[i] = (var_value(s,i)==var1 ? l_True : l_False);
                 sat_solver_canceluntil(s,s->root_level);
                 veci_delete(&learnt_clause);
 
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index ce597271..1437f5c1 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -125,7 +125,8 @@ struct sat_solver_t
 
     veci        order;         // Variable order. (heap) (contains: var)
     veci        trail_lim;     // Separator indices for different decision levels in 'trail'. (contains: int)
-    veci        model;         // If problem is solved, this vector contains the model (contains: lbool).
+//    veci        model;         // If problem is solved, this vector contains the model (contains: lbool).
+    int *       model;         // If problem is solved, this vector contains the model (contains: lbool).
     veci        conf_final;    // If problem is unsatisfiable (possibly under assumptions),
                                // this vector represent the final conflict clause expressed in the assumptions.
 
@@ -164,15 +165,15 @@ struct sat_solver_t
     veci        temp_clause;    // temporary storage for a CNF clause
 };
 
-static int sat_solver_var_value( sat_solver* s, int v ) 
+static int sat_solver_var_value( sat_solver* s, int v )
 {
-    assert( s->model.ptr != NULL && v < s->size );
-    return (int)(s->model.ptr[v] == l_True);
+    assert( v >= 0 && v < s->size );
+    return (int)(s->model[v] == l_True);
 }
-static int sat_solver_var_literal( sat_solver* s, int v ) 
+static int sat_solver_var_literal( sat_solver* s, int v )
 {
-    assert( s->model.ptr != NULL && v < s->size );
-    return toLitCond( v, s->model.ptr[v] != l_True );
+    assert( v >= 0 && v < s->size );
+    return toLitCond( v, s->model[v] != l_True );
 }
 static void sat_solver_act_var_clear(sat_solver* s) 
 {
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index a4166fef..0da59fda 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1087,7 +1087,6 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
     s->stats.starts++;
 //    s->var_decay = (float)(1 / 0.95   );
 //    s->cla_decay = (float)(1 / 0.999);
-    veci_resize(&s->model,0);
     veci_new(&learnt_clause);
 
     for (;;){
@@ -1158,9 +1157,8 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
             if (next == var_Undef){
                 // Model found:
                 int i;
-                veci_resize(&s->model, 0);
                 for (i = 0; i < s->size; i++) 
-                    veci_push( &s->model, var_value(s,i)==var1 ? l_True : l_False );
+                    s->model[i] = (var_value(s,i)==var1 ? l_True : l_False);
                 solver2_canceluntil(s,s->root_level);
                 veci_delete(&learnt_clause);
 
@@ -1197,7 +1195,6 @@ sat_solver2* sat_solver2_new(void)
     veci_new(&s->trail_lim);
     veci_new(&s->tagged);
     veci_new(&s->stack);
-    veci_new(&s->model);
     veci_new(&s->temp_clause);
     veci_new(&s->conf_final);
     veci_new(&s->mark_levels);
@@ -1276,6 +1273,7 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
 #else
         s->activity  = ABC_REALLOC(unsigned, s->activity, s->cap);
 #endif
+        s->model     = ABC_REALLOC(int,      s->model,    s->cap);
         memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) );
     }
 
@@ -1326,7 +1324,6 @@ void sat_solver2_delete(sat_solver2* s)
     veci_delete(&s->trail_lim);
     veci_delete(&s->tagged);
     veci_delete(&s->stack);
-    veci_delete(&s->model);
     veci_delete(&s->temp_clause);
     veci_delete(&s->conf_final);
     veci_delete(&s->mark_levels);
@@ -1354,6 +1351,7 @@ void sat_solver2_delete(sat_solver2* s)
         ABC_FREE(s->reasons  );
         ABC_FREE(s->units    );
         ABC_FREE(s->activity );
+        ABC_FREE(s->model    );
     }
     ABC_FREE(s);
 }
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index f3d70deb..4b26f55f 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -132,13 +132,13 @@ struct sat_solver2_t
     int*            orderpos;       // Index in variable order.
     cla*            reasons;        // reason clauses
     cla*            units;          // unit clauses
+    int*            model;          // If problem is solved, this vector contains the model (contains: lbool).
 
     veci            tagged;         // (contains: var)
     veci            stack;          // (contains: var)
     veci            order;          // Variable order. (heap) (contains: var)
     veci            trail_lim;      // Separator indices for different decision levels in 'trail'. (contains: int)
     veci            temp_clause;    // temporary storage for a CNF clause
-    veci            model;          // If problem is solved, this vector contains the model (contains: lbool).
     veci            conf_final;     // If problem is unsatisfiable (possibly under assumptions),
                                     // this vector represent the final conflict clause expressed in the assumptions.
     veci            mark_levels;    // temporary storage for labeled levels
@@ -213,13 +213,13 @@ static inline int sat_solver2_nconflicts(sat_solver2* s)
 
 static inline int sat_solver2_var_value( sat_solver2* s, int v ) 
 {
-    assert( s->model.ptr != NULL && v < s->size );
-    return (int)(s->model.ptr[v] == l_True);
+    assert( v >= 0 && v < s->size );
+    return (int)(s->model[v] == l_True);
 }
 static inline int sat_solver2_var_literal( sat_solver2* s, int v ) 
 {
-    assert( s->model.ptr != NULL && v < s->size );
-    return toLitCond( v, s->model.ptr[v] != l_True );
+    assert( v >= 0 && v < s->size );
+    return toLitCond( v, s->model[v] != l_True );
 }
 static inline void sat_solver2_act_var_clear(sat_solver2* s) 
 {
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 5e809172..70d09638 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -231,10 +231,7 @@ int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars )
     int i;
     pModel = ABC_CALLOC( int, nVars+1 );
     for ( i = 0; i < nVars; i++ )
-    {
-        assert( pVars[i] >= 0 && pVars[i] < p->size );
-        pModel[i] = (int)(p->model.ptr[pVars[i]] == l_True);
-    }
+        pModel[i] = sat_solver_var_value(p, pVars[i]);
     return pModel;    
 }
 
@@ -255,10 +252,7 @@ int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars )
     int i;
     pModel = ABC_CALLOC( int, nVars+1 );
     for ( i = 0; i < nVars; i++ )
-    {
-        assert( pVars[i] >= 0 && pVars[i] < p->size );
-        pModel[i] = (int)(p->model.ptr[pVars[i]] == l_True);
-    }
+        pModel[i] = sat_solver2_var_value(p, pVars[i]);
     return pModel;    
 }