Transforming the solver to use different clause representation.

1 files changed, 388 insertions, 462 deletions

diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 4d851d0f..5a05e3b0 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -29,7 +29,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 ABC_NAMESPACE_IMPL_START
 
-//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
 #define SAT_USE_ANALYZE_FINAL
 
 //=================================================================================================
@@ -77,6 +76,62 @@ static inline int irand(double* seed, int size) {
 static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *));
 
 //=================================================================================================
+// Variable datatype + minor functions:
+
+static const int var0  = 1;
+static const int var1  = 0;
+static const int varX  = 3;
+
+struct varinfo_t
+{
+    unsigned val    :  2;  // variable value 
+    unsigned pol    :  1;  // last polarity
+    unsigned tag    :  1;  // conflict analysis tag
+    unsigned lev    : 28;  // variable level
+};
+
+static inline int     var_level     (sat_solver* s, int v)            { return s->levels[v]; }
+static inline int     var_value     (sat_solver* s, int v)            { return s->assigns[v]; }
+static inline int     var_polar     (sat_solver* s, int v)            { return s->polarity[v]; }
+
+static inline void    var_set_level (sat_solver* s, int v, int lev)   { s->levels[v] = lev;  }
+static inline void    var_set_value (sat_solver* s, int v, int val)   { s->assigns[v] = val;  }
+static inline void    var_set_polar (sat_solver* s, int v, int pol)   { s->polarity[v] = pol;  }
+
+// variable tags
+static inline int     var_tag       (sat_solver* s, int v)            { return s->tags[v]; }
+static inline void    var_set_tag   (sat_solver* s, int v, int tag)   { 
+    assert( tag > 0 && tag < 16 );
+    if ( s->tags[v] == 0 )
+        veci_push( &s->tagged, v );
+    s->tags[v] = tag;                           
+}
+static inline void    var_add_tag   (sat_solver* s, int v, int tag)   { 
+    assert( tag > 0 && tag < 16 );
+    if ( s->tags[v] == 0 )
+        veci_push( &s->tagged, v );
+    s->tags[v] |= tag;                           
+}
+static inline void    solver2_clear_tags(sat_solver* s, int start)    { 
+    int i, * tagged = veci_begin(&s->tagged);
+    for (i = start; i < veci_size(&s->tagged); i++)
+        s->tags[tagged[i]] = 0;
+    veci_resize(&s->tagged,start);
+}
+
+int sat_solver_get_var_value(sat_solver* s, int v)
+{
+    if ( var_value(s, v) == var0 )
+        return l_False;
+    if ( var_value(s, v) == var1 )
+        return l_True;
+    if ( var_value(s, v) == varX )
+        return l_Undef;
+    assert( 0 );
+    return 0;
+}
+
+//=================================================================================================
 // Clause datatype + minor functions:
 
 struct clause_t
@@ -85,7 +140,7 @@ struct clause_t
     lit lits[0];
 };
 
-static inline int      clause_size         (clause* c)             { return c->size_learnt >> 1;                       }
+static inline int      clause_nlits        (clause* c)             { return c->size_learnt >> 1;                       }
 static inline lit*     clause_begin        (clause* c)             { return c->lits;                                   }
 static inline int      clause_learnt       (clause* c)             { return c->size_learnt & 1;                        }
 static inline float    clause_activity     (clause* c)             { return *((float*)&c->lits[c->size_learnt>>1]);    }
@@ -95,23 +150,26 @@ static inline void     clause_setactivity2 (clause* c, unsigned a) { *((unsigned
 static inline void     clause_print        (clause* c)             { 
     int i;
     printf( "{ " );
-    for ( i = 0; i < clause_size(c); i++ )
+    for ( i = 0; i < clause_nlits(c); i++ )
         printf( "%d ", (clause_begin(c)[i] & 1)? -(clause_begin(c)[i] >> 1) : clause_begin(c)[i] >> 1 );
     printf( "}\n" );
 }
 
+static inline clause* clause_read( sat_solver* s, int h )          { return (clause *)Vec_RecEntryP(&s->Mem, h);       }
+static inline int     clause_size( int nLits, int fLearnt )        { int a = nLits + fLearnt + 1; return a + (a & 1);  }
+
 //=================================================================================================
 // Encode literals in clause pointers:
 
-static inline clause* clause_from_lit (lit l)     { return (clause*)((ABC_PTRUINT_T)l + (ABC_PTRUINT_T)l + 1);  }
-static inline int     clause_is_lit   (clause* c) { return ((ABC_PTRUINT_T)c & 1);                              }
-static inline lit     clause_read_lit (clause* c) { return (lit)((ABC_PTRUINT_T)c >> 1);                        }
+static inline int     clause_from_lit (lit l)       { return l + l + 1;                            }
+static inline int     clause_is_lit   (int h)       { return (h & 1);                              }
+static inline lit     clause_read_lit (int h)       { return (lit)(h >> 1);                        }
 
 //=================================================================================================
 // Simple helpers:
 
 static inline int     sat_solver_dl(sat_solver* s)                { return veci_size(&s->trail_lim); }
-static inline vecp*   sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l];            }
+static inline veci*   sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l];            }
 
 //=================================================================================================
 // Variable order functions:
@@ -153,49 +211,31 @@ static inline void order_unassigned(sat_solver* s, int v) // undoorder
 
 static inline int  order_select(sat_solver* s, float random_var_freq) // selectvar
 {
-    int*    heap;
-    int*    orderpos;
-
-    lbool* values = s->assigns;
-
+    int*      heap     = veci_begin(&s->order);
+    int*      orderpos = s->orderpos;
     // Random decision:
     if (drand(&s->random_seed) < random_var_freq){
         int next = irand(&s->random_seed,s->size);
         assert(next >= 0 && next < s->size);
-        if (values[next] == l_Undef)
+        if (var_value(s, next) == varX)
             return next;
     }
-
     // Activity based decision:
-
-    heap     = veci_begin(&s->order);
-    orderpos = s->orderpos;
-
-
     while (veci_size(&s->order) > 0){
         int    next  = heap[0];
         int    size  = veci_size(&s->order)-1;
         int    x     = heap[size];
-
         veci_resize(&s->order,size);
-
         orderpos[next] = -1;
-
         if (size > 0){
-
             int    i     = 0;
             int    child = 1;
-
-
             while (child < size){
                 if (child+1 < size && s->activity[heap[child]] < s->activity[heap[child+1]])
                     child++;
-
                 assert(child < size);
-
                 if (s->activity[x] >= s->activity[heap[child]])
                     break;
-
                 heap[i]           = heap[child];
                 orderpos[heap[i]] = i;
                 i                 = child;
@@ -204,12 +244,9 @@ static inline int  order_select(sat_solver* s, float random_var_freq) // selectv
             heap[i]           = x;
             orderpos[heap[i]] = i;
         }
-
-//printf( "-%d ", next );
-        if (values[next] == l_Undef)
+        if (var_value(s, next) == varX)
             return next;
     }
-
     return var_Undef;
 }
 
@@ -227,9 +264,9 @@ static inline void act_var_rescale(sat_solver* s)  {
 }
 static inline void act_clause_rescale(sat_solver* s) {
     static int Total = 0;
-    clause** cs = (clause**)vecp_begin(&s->learnts);
+    clause** cs = (clause**)veci_begin(&s->learnts);
     int i, clk = clock();
-    for (i = 0; i < vecp_size(&s->learnts); i++){
+    for (i = 0; i < veci_size(&s->learnts); i++){
         float a = clause_activity(cs[i]);
         clause_setactivity(cs[i], a * (float)1e-20);
     }
@@ -247,6 +284,8 @@ static inline void act_var_bump(sat_solver* s, int v) {
         order_update(s,v);
 }
 static inline void act_var_bump_global(sat_solver* s, int v) {
+    if ( !s->pGlobalVars )
+        return;
     s->activity[v] += (s->var_inc * 3.0 * s->pGlobalVars[v]);
     if (s->activity[v] > 1e100)
         act_var_rescale(s);
@@ -254,6 +293,8 @@ static inline void act_var_bump_global(sat_solver* s, int v) {
         order_update(s,v);
 }
 static inline void act_var_bump_factor(sat_solver* s, int v) {
+    if ( !s->factors )
+        return;
     s->activity[v] += (s->var_inc * s->factors[v]);
     if (s->activity[v] > 1e100)
         act_var_rescale(s);
@@ -278,6 +319,7 @@ static inline void act_var_rescale(sat_solver* s) {
     s->var_inc >>= 19;
     s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
 }
+/*
 static inline void act_clause_rescale(sat_solver* s) {
     static int Total = 0;
     clause** cs = (clause**)vecp_begin(&s->learnts);
@@ -293,6 +335,7 @@ static inline void act_clause_rescale(sat_solver* s) {
 //    printf( "Rescaling...   Cla inc = %5d  Conf = %10d   ", s->cla_inc,  s->stats.conflicts );
 //    Abc_PrintTime( 1, "Time", Total );
 }
+*/
 static inline void act_var_bump(sat_solver* s, int v) {
     s->activity[v] += s->var_inc;
     if (s->activity[v] & 0x80000000)
@@ -300,30 +343,100 @@ static inline void act_var_bump(sat_solver* s, int v) {
     if (s->orderpos[v] != -1)
         order_update(s,v);
 }
-static inline void act_var_bump_global(sat_solver* s, int v) {}
-static inline void act_var_bump_factor(sat_solver* s, int v) {}
+static inline void act_var_bump_global(sat_solver* s, int v) {
+    if ( !s->pGlobalVars )
+        return;
+    s->activity[v] += (int)(s->var_inc * 3 * s->pGlobalVars[v]);
+    if (s->activity[v] & 0x80000000)
+        act_var_rescale(s);
+    if (s->orderpos[v] != -1)
+        order_update(s,v);
+}
+static inline void act_var_bump_factor(sat_solver* s, int v) {
+    if ( !s->factors )
+        return;
+    s->activity[v] += (int)(s->var_inc * s->factors[v]);
+    if (s->activity[v] & 0x80000000)
+        act_var_rescale(s);
+    if (s->orderpos[v] != -1)
+        order_update(s,v);
+}
+/*
 static inline void act_clause_bump(sat_solver* s, clause*c) {
     unsigned a = clause_activity2(c) + s->cla_inc;
     clause_setactivity2(c,a);
     if (a & 0x80000000) 
         act_clause_rescale(s);
 }
+*/
 static inline void act_var_decay(sat_solver* s)    { s->var_inc += (s->var_inc >>  4); }
-static inline void act_clause_decay(sat_solver* s) { s->cla_inc += (s->cla_inc >> 10); }
+//static inline void act_clause_decay(sat_solver* s) { s->cla_inc += (s->cla_inc >> 10); }
 
 #endif
 
 
 //=================================================================================================
+// Sorting functions (sigh):
+
+static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
+{
+    int     i, j, best_i;
+    void*   tmp;
+
+    for (i = 0; i < size-1; i++){
+        best_i = i;
+        for (j = i+1; j < size; j++){
+            if (comp(array[j], array[best_i]) < 0)
+                best_i = j;
+        }
+        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
+    }
+}
+
+static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
+{
+    if (size <= 15)
+        selectionsort(array, size, comp);
+
+    else{
+        void*       pivot = array[irand(seed, size)];
+        void*       tmp;
+        int         i = -1;
+        int         j = size;
+
+        for(;;){
+            do i++; while(comp(array[i], pivot)<0);
+            do j--; while(comp(pivot, array[j])<0);
+
+            if (i >= j) break;
+
+            tmp = array[i]; array[i] = array[j]; array[j] = tmp;
+        }
+
+        sortrnd(array    , i     , comp, seed);
+        sortrnd(&array[i], size-i, comp, seed);
+    }
+}
+
+void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *))
+{
+//    int i;
+    double seed = 91648253;
+    sortrnd(array,size,comp,&seed);
+//    for ( i = 1; i < size; i++ )
+//        assert(comp(array[i-1], array[i])<0);
+}
+
+//=================================================================================================
 // Clause functions:
 
 /* pre: size > 1 && no variable occurs twice
  */
-static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
+static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
 {
     int size;
     clause* c;
-    int i;
+    int h, i;
 
     assert(end - begin > 1);
     assert(learnt >= 0 && learnt < 2);
@@ -332,23 +445,20 @@ static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt
     // do not allocate memory for the two-literal problem clause
     if ( size == 2 && !learnt )
     {
-        vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(clause_from_lit(begin[1])));
-        vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(clause_from_lit(begin[0])));
-        return NULL;
+        veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(clause_from_lit(begin[1])));
+        veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(clause_from_lit(begin[0])));
+        return 0;
     }
 
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
-#else
-    c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
-#endif
-
+    // create new clause
+    h = Vec_RecAppend( &s->Mem, clause_size(size, learnt) );
+    c = clause_read( s, h );
+    assert( !(h & 1) );
+    if ( s->hLearnts == -1 && learnt )
+        s->hLearnts = h;
     c->size_learnt = (size << 1) | learnt;
-    assert(((ABC_PTRUINT_T)c & 1) == 0);
-
     for (i = 0; i < size; i++)
         c->lits[i] = begin[i];
-
     if (learnt)
         *((float*)&c->lits[size]) = 0.0;
 
@@ -360,44 +470,35 @@ static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt
     assert(lit_neg(begin[0]) < s->size*2);
     assert(lit_neg(begin[1]) < s->size*2);
 
-    //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
-    //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
-
-    vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
-    vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
+    //veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),c);
+    //veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),c);
+    veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(size > 2 ? h : clause_from_lit(begin[1])));
+    veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(size > 2 ? h : clause_from_lit(begin[0])));
 
-    return c;
+    return h;
 }
 
 
 //=================================================================================================
 // Minor (solver) functions:
 
-static inline int sat_solver_enqueue(sat_solver* s, lit l, clause* from)
+static inline int sat_solver_enqueue(sat_solver* s, lit l, int from)
 {
-    lbool* values = s->assigns;
-    int    v      = lit_var(l);
-    lbool  val    = values[v];
-    lbool  sig;
+    int v  = lit_var(l);
 #ifdef VERBOSEDEBUG
     printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
 #endif
-
-    sig = !lit_sign(l); sig += sig - 1;
-    if (val != l_Undef){
-        return val == sig;
-    }else{
-        int*     levels  = s->levels;
-        clause** reasons = s->reasons;
+    if (var_value(s, v) != varX)
+        return var_value(s, v) == lit_sign(l);
+    else{
         // New fact -- store it.
 #ifdef VERBOSEDEBUG
         printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
 #endif
-        values [v] = sig;
-        levels [v] = sat_solver_dl(s);
-        reasons[v] = from;
+        var_set_value(s, v, lit_sign(l));
+        var_set_level(s, v, sat_solver_dl(s));
+        s->reasons[v] = from;
         s->trail[s->qtail++] = l;
-
         order_assigned(s, v);
         return true;
     }
@@ -406,20 +507,17 @@ static inline int sat_solver_enqueue(sat_solver* s, lit l, clause* from)
 
 static inline int sat_solver_assume(sat_solver* s, lit l){
     assert(s->qtail == s->qhead);
-    assert(s->assigns[lit_var(l)] == l_Undef);
+    assert(var_value(s, lit_var(l)) == varX);
 #ifdef VERBOSEDEBUG
     printf(L_IND"assume("L_LIT")  ", L_ind, L_lit(l));
     printf( "act = %.20f\n", s->activity[lit_var(l)] );
 #endif
     veci_push(&s->trail_lim,s->qtail);
-    return sat_solver_enqueue(s,l,(clause*)0);
+    return sat_solver_enqueue(s,l,0);
 }
 
 
 static void sat_solver_canceluntil(sat_solver* s, int level) {
-    lit*     trail;   
-    lbool*   values;  
-    clause** reasons; 
     int      bound;
     int      lastLev;
     int      c;
@@ -427,9 +525,6 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
     if (sat_solver_dl(s) <= level)
         return;
 
-    trail   = s->trail;
-    values  = s->assigns;
-    reasons = s->reasons;
     bound   = (veci_begin(&s->trail_lim))[level];
     lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1];
 
@@ -440,15 +535,15 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
     ////////////////////////////////////////
 
     for (c = s->qtail-1; c >= bound; c--) {
-        int     x  = lit_var(trail[c]);
-        values [x] = l_Undef;
-        reasons[x] = (clause*)0;
+        int     x  = lit_var(s->trail[c]);
+        var_set_value(s, x, varX);
+        s->reasons[x] = 0;
         if ( c < lastLev )
-            s->polarity[x] = !lit_sign(trail[c]);
+            var_set_polar( s, x, !lit_sign(s->trail[c]) );
     }
 
     for (c = s->qhead-1; c >= bound; c--)
-        order_unassigned(s,lit_var(trail[c]));
+        order_unassigned(s,lit_var(s->trail[c]));
 
     s->qhead = s->qtail = bound;
     veci_resize(&s->trail_lim,level);
@@ -458,8 +553,8 @@ static void sat_solver_record(sat_solver* s, veci* cls)
 {
     lit*    begin = veci_begin(cls);
     lit*    end   = begin + veci_size(cls);
-    clause* c     = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : (clause*)0;
-    sat_solver_enqueue(s,*begin,c);
+    int     h     = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : 0;
+    sat_solver_enqueue(s,*begin,h);
 
     ///////////////////////////////////
     // add clause to internal storage
@@ -472,9 +567,9 @@ static void sat_solver_record(sat_solver* s, veci* cls)
 
     assert(veci_size(cls) > 0);
 
-    if (c != 0) {
-        vecp_push(&s->learnts,c);
-        act_clause_bump(s,c);
+    if (h != 0) {
+//        veci_push(&s->learnts,c);
+//        act_clause_bump(s,c);
         s->stats.learnts++;
         s->stats.learnts_literals += veci_size(cls);
     }
@@ -483,82 +578,59 @@ static void sat_solver_record(sat_solver* s, veci* cls)
 
 static double sat_solver_progress(sat_solver* s)
 {
-    lbool*  values = s->assigns;
-    int*    levels = s->levels;
     int     i;
-
     double  progress = 0;
     double  F        = 1.0 / s->size;
     for (i = 0; i < s->size; i++)
-        if (values[i] != l_Undef)
-            progress += pow(F, levels[i]);
+        if (var_value(s, i) != varX)
+            progress += pow(F, var_level(s, i));
     return progress / s->size;
 }
 
 //=================================================================================================
 // Major methods:
 
-static int sat_solver_lit_removable(sat_solver* s, lit l, int minl)
+static int sat_solver_lit_removable(sat_solver* s, int x, int minl)
 {
-    lbool*   tags    = s->tags;
-    clause** reasons = s->reasons;
-    int*     levels  = s->levels;
     int      top     = veci_size(&s->tagged);
 
-    assert(lit_var(l) >= 0 && lit_var(l) < s->size);
-    assert(reasons[lit_var(l)] != 0);
+    assert(s->reasons[x] != 0);
     veci_resize(&s->stack,0);
-    veci_push(&s->stack,lit_var(l));
-
-    while (veci_size(&s->stack) > 0){
-        clause* c;
-        int v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
-        assert(v >= 0 && v < s->size);
-        veci_resize(&s->stack,veci_size(&s->stack)-1);
-        assert(reasons[v] != 0);
-        c    = reasons[v];
-
-        if (clause_is_lit(c)){
-            int v = lit_var(clause_read_lit(c));
-            if (tags[v] == l_Undef && levels[v] != 0){
-                if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+    veci_push(&s->stack,x);
+
+    while (veci_size(&s->stack)){
+        int v = veci_pop(&s->stack);
+        assert(s->reasons[v] != 0);
+        if (clause_is_lit(s->reasons[v])){
+            v = lit_var(clause_read_lit(s->reasons[v]));
+            if (!var_tag(s,v) && var_level(s, v)){
+                if (s->reasons[v] != 0 && ((1 << (var_level(s, v) & 31)) & minl)){
                     veci_push(&s->stack,v);
-                    tags[v] = l_True;
-                    veci_push(&s->tagged,v);
+                    var_set_tag(s, v, 1);
                 }else{
-                    int* tagged = veci_begin(&s->tagged);
-                    int j;
-                    for (j = top; j < veci_size(&s->tagged); j++)
-                        tags[tagged[j]] = l_Undef;
-                    veci_resize(&s->tagged,top);
-                    return false;
+                    solver2_clear_tags(s, top);
+                    return 0;
                 }
             }
         }else{
-            lit*    lits = clause_begin(c);
-            int     i, j;
-
-            for (i = 1; i < clause_size(c); i++){
+            clause* c = clause_read(s, s->reasons[v]);
+            lit* lits = clause_begin(c);
+            int  i;
+            for (i = 1; i < clause_nlits(c); i++){
                 int v = lit_var(lits[i]);
-                if (tags[v] == l_Undef && levels[v] != 0){
-                    if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
-
+                if (!var_tag(s,v) && var_level(s, v)){
+                    if (s->reasons[v] != 0 && ((1 << (var_level(s, v) & 31)) & minl)){
                         veci_push(&s->stack,lit_var(lits[i]));
-                        tags[v] = l_True;
-                        veci_push(&s->tagged,v);
+                        var_set_tag(s, v, 1);
                     }else{
-                        int* tagged = veci_begin(&s->tagged);
-                        for (j = top; j < veci_size(&s->tagged); j++)
-                            tags[tagged[j]] = l_Undef;
-                        veci_resize(&s->tagged,top);
-                        return false;
+                        solver2_clear_tags(s, top);
+                        return 0;
                     }
                 }
             }
         }
     }
-
-    return true;
+    return 1;
 }
 
 
@@ -613,8 +685,9 @@ void Solver::analyzeFinal(Clause* confl, bool skip_first)
 
 #ifdef SAT_USE_ANALYZE_FINAL
 
-static void sat_solver_analyze_final(sat_solver* s, clause* conf, int skip_first)
+static void sat_solver_analyze_final(sat_solver* s, int hConf, int skip_first)
 {
+    clause* conf = clause_read(s, hConf);
     int i, j, start;
     veci_resize(&s->conf_final,0);
     if ( s->root_level == 0 )
@@ -622,110 +695,87 @@ static void sat_solver_analyze_final(sat_solver* s, clause* conf, int skip_first
     assert( veci_size(&s->tagged) == 0 );
 //    assert( s->tags[lit_var(p)] == l_Undef );
 //    s->tags[lit_var(p)] = l_True;
-    for (i = skip_first ? 1 : 0; i < clause_size(conf); i++)
+    for (i = skip_first ? 1 : 0; i < clause_nlits(conf); i++)
     {
         int x = lit_var(clause_begin(conf)[i]);
-        if (s->levels[x] > 0)
-        {
-            s->tags[x] = l_True;
-            veci_push(&s->tagged,x);
-        }
+        if (var_level(s, x) > 0)
+            var_set_tag(s, x, 1);
     }
 
     start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level];
     for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){
         int x = lit_var(s->trail[i]);
-        if (s->tags[x] == l_True){
-            if (s->reasons[x] == NULL){
-                assert(s->levels[x] > 0);
+        if (var_tag(s,x)){
+            if (s->reasons[x] == 0){
+                assert(var_level(s, x) > 0);
                 veci_push(&s->conf_final,lit_neg(s->trail[i]));
             }else{
-                clause* c = s->reasons[x];
-                if (clause_is_lit(c)){
-                    lit q = clause_read_lit(c);
+                if (clause_is_lit(s->reasons[x])){
+                    lit q = clause_read_lit(s->reasons[x]);
                     assert(lit_var(q) >= 0 && lit_var(q) < s->size);
-                    if (s->levels[lit_var(q)] > 0)
-                    {
-                        s->tags[lit_var(q)] = l_True;
-                        veci_push(&s->tagged,lit_var(q));
-                    }
+                    if (var_level(s, lit_var(q)) > 0)
+                        var_set_tag(s, lit_var(q), 1);
                 }
                 else{
+                    clause* c = clause_read(s, s->reasons[x]);
                     int* lits = clause_begin(c);
-                    for (j = 1; j < clause_size(c); j++)
-                        if (s->levels[lit_var(lits[j])] > 0)
-                        {
-                            s->tags[lit_var(lits[j])] = l_True;
-                            veci_push(&s->tagged,lit_var(lits[j]));
-                        }
+                    for (j = 1; j < clause_nlits(c); j++)
+                        if (var_level(s, lit_var(lits[j])) > 0)
+                            var_set_tag(s, lit_var(lits[j]), 1);
                 }
             }
         }
     }
-    for (i = 0; i < veci_size(&s->tagged); i++)
-        s->tags[veci_begin(&s->tagged)[i]] = l_Undef;
-    veci_resize(&s->tagged,0);
+    solver2_clear_tags(s,0);
 }
 
 #endif
 
 
-static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
+static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
 {
     lit*     trail   = s->trail;
-    lbool*   tags    = s->tags;
-    clause** reasons = s->reasons;
-    int*     levels  = s->levels;
     int      cnt     = 0;
     lit      p       = lit_Undef;
     int      ind     = s->qtail-1;
     lit*     lits;
     int      i, j, minl;
-    int*     tagged;
-
     veci_push(learnt,lit_Undef);
-
     do{
-        assert(c != 0);
-
-        if (clause_is_lit(c)){
-            lit q = clause_read_lit(c);
-            assert(lit_var(q) >= 0 && lit_var(q) < s->size);
-            if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
-                tags[lit_var(q)] = l_True;
-                veci_push(&s->tagged,lit_var(q));
-                act_var_bump(s,lit_var(q));
-                if (levels[lit_var(q)] == sat_solver_dl(s))
+        assert(h != 0);
+        if (clause_is_lit(h)){
+            int x = lit_var(clause_read_lit(h));
+            if (var_tag(s, x) == 0 && var_level(s, x) > 0){
+                var_set_tag(s, x, 1);
+                act_var_bump(s,x);
+                if (var_level(s, x) == sat_solver_dl(s))
                     cnt++;
                 else
-                    veci_push(learnt,q);
+                    veci_push(learnt,clause_read_lit(h));
             }
         }else{
-
-            if (clause_learnt(c))
-                act_clause_bump(s,c);
-
+            clause* c = clause_read(s, h);
+//            if (clause_learnt(c))
+//                act_clause_bump(s,c);
             lits = clause_begin(c);
-            //printlits(lits,lits+clause_size(c)); printf("\n");
-            for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
-                lit q = lits[j];
-                assert(lit_var(q) >= 0 && lit_var(q) < s->size);
-                if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
-                    tags[lit_var(q)] = l_True;
-                    veci_push(&s->tagged,lit_var(q));
-                    act_var_bump(s,lit_var(q));
-                    if (levels[lit_var(q)] == sat_solver_dl(s))
+            //printlits(lits,lits+clause_nlits(c)); printf("\n");
+            for (j = (p == lit_Undef ? 0 : 1); j < clause_nlits(c); j++){
+                int x = lit_var(lits[j]);
+                if (var_tag(s, x) == 0 && var_level(s, x) > 0){
+                    var_set_tag(s, x, 1);
+                    act_var_bump(s,x);
+                    if (var_level(s,x) == sat_solver_dl(s))
                         cnt++;
                     else
-                        veci_push(learnt,q);
+                        veci_push(learnt,lits[j]);
                 }
             }
         }
 
-        while (tags[lit_var(trail[ind--])] == l_Undef);
+        while ( !var_tag(s, lit_var(trail[ind--])) );
 
         p = trail[ind+1];
-        c = reasons[lit_var(p)];
+        h = s->reasons[lit_var(p)];
         cnt--;
 
     }while (cnt > 0);
@@ -735,13 +785,13 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
     lits = veci_begin(learnt);
     minl = 0;
     for (i = 1; i < veci_size(learnt); i++){
-        int lev = levels[lit_var(lits[i])];
+        int lev = var_level(s, lit_var(lits[i]));
         minl    |= 1 << (lev & 31);
     }
 
     // simplify (full)
     for (i = j = 1; i < veci_size(learnt); i++){
-        if (reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lits[i],minl))
+        if (s->reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lit_var(lits[i]),minl))
             lits[j++] = lits[i];
     }
 
@@ -750,14 +800,11 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
     s->stats.tot_literals += j;
 
     // clear tags
-    tagged = veci_begin(&s->tagged);
-    for (i = 0; i < veci_size(&s->tagged); i++)
-        tags[tagged[i]] = l_Undef;
-    veci_resize(&s->tagged,0);
+    solver2_clear_tags(s,0);
 
 #ifdef DEBUG
     for (i = 0; i < s->size; i++)
-        assert(tags[i] == l_Undef);
+        assert(!var_tag(s, i));
 #endif
 
 #ifdef VERBOSEDEBUG
@@ -766,12 +813,12 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
 #endif
     if (veci_size(learnt) > 1){
         int max_i = 1;
-        int max   = levels[lit_var(lits[1])];
+        int max   = var_level(s, lit_var(lits[1]));
         lit tmp;
 
         for (i = 2; i < veci_size(learnt); i++)
-            if (levels[lit_var(lits[i])] > max){
-                max   = levels[lit_var(lits[i])];
+            if (var_level(s, lit_var(lits[i])) > max){
+                max   = var_level(s, lit_var(lits[i]));
                 max_i = i;
             }
 
@@ -781,28 +828,26 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
     }
 #ifdef VERBOSEDEBUG
     {
-        int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
+        int lev = veci_size(learnt) > 1 ? var_level(s, lit_var(lits[1])) : 0;
         printf(" } at level %d\n", lev);
     }
 #endif
 }
 
 
-clause* sat_solver_propagate(sat_solver* s)
+int sat_solver_propagate(sat_solver* s)
 {
-    lbool*  values = s->assigns;
-    clause* confl  = (clause*)0;
+    int     hConfl = 0;
     lit*    lits;
     lit false_lit;
-    lbool sig;
 
     //printf("sat_solver_propagate\n");
-    while (confl == 0 && s->qtail - s->qhead > 0){
-        lit  p  = s->trail[s->qhead++];
-        vecp* ws = sat_solver_read_wlist(s,p);
-        clause **begin = (clause**)vecp_begin(ws);
-        clause **end   = begin + vecp_size(ws);
-        clause **i, **j;
+    while (hConfl == 0 && s->qtail - s->qhead > 0){
+        lit   p     = s->trail[s->qhead++];
+        veci* ws    = sat_solver_read_wlist(s,p);
+        int*  begin = veci_begin(ws);
+        int*  end   = begin + veci_size(ws);
+        int*i, *j;
 
         s->stats.propagations++;
         s->simpdb_props--;
@@ -812,24 +857,24 @@ clause* sat_solver_propagate(sat_solver* s)
             if (clause_is_lit(*i)){
 
                 int Lit = clause_read_lit(*i);
-                sig = !lit_sign(Lit); sig += sig - 1;
-                if (values[lit_var(Lit)] == sig){
+                if (var_value(s, lit_var(Lit)) == lit_sign(Lit)){
                     *j++ = *i++;
                     continue;
                 }
 
                 *j++ = *i;
                 if (!sat_solver_enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
-                    confl = s->binary;
-                    (clause_begin(confl))[1] = lit_neg(p);
-                    (clause_begin(confl))[0] = clause_read_lit(*i++);
+                    hConfl = s->hBinary;
+                    (clause_begin(s->binary))[1] = lit_neg(p);
+                    (clause_begin(s->binary))[0] = clause_read_lit(*i++);
                     // Copy the remaining watches:
                     while (i < end)
                         *j++ = *i++;
                 }
             }else{
 
-                lits = clause_begin(*i);
+                clause* c = clause_read(s,*i);
+                lits = clause_begin(c);
 
                 // Make sure the false literal is data[1]:
                 false_lit = lit_neg(p);
@@ -838,29 +883,26 @@ clause* sat_solver_propagate(sat_solver* s)
                     lits[1] = false_lit;
                 }
                 assert(lits[1] == false_lit);
-                //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
 
                 // If 0th watch is true, then clause is already satisfied.
-                sig = !lit_sign(lits[0]); sig += sig - 1;
-                if (values[lit_var(lits[0])] == sig){
+                if (var_value(s, lit_var(lits[0])) == lit_sign(lits[0]))
                     *j++ = *i;
-                }else{
+                else{
                     // Look for new watch:
-                    lit* stop = lits + clause_size(*i);
+                    lit* stop = lits + clause_nlits(c);
                     lit* k;
                     for (k = lits + 2; k < stop; k++){
-                        lbool sig = lit_sign(*k); sig += sig - 1;
-                        if (values[lit_var(*k)] != sig){
+                        if (var_value(s, lit_var(*k)) != !lit_sign(*k)){
                             lits[1] = *k;
                             *k = false_lit;
-                            vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
+                            veci_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
                             goto next; }
                     }
 
                     *j++ = *i;
                     // Clause is unit under assignment:
                     if (!sat_solver_enqueue(s,lits[0], *i)){
-                        confl = *i++;
+                        hConfl = *i++;
                         // Copy the remaining watches:
                         while (i < end)
                             *j++ = *i++;
@@ -871,11 +913,11 @@ clause* sat_solver_propagate(sat_solver* s)
             i++;
         }
 
-        s->stats.inspects += j - (clause**)vecp_begin(ws);
-        vecp_resize(ws,j - (clause**)vecp_begin(ws));
+        s->stats.inspects += j - veci_begin(ws);
+        veci_resize(ws,j - veci_begin(ws));
     }
 
-    return confl;
+    return hConfl;
 }
 
 //=================================================================================================
@@ -883,12 +925,15 @@ clause* sat_solver_propagate(sat_solver* s)
 
 sat_solver* sat_solver_new(void)
 {
-    sat_solver* s = (sat_solver*)ABC_ALLOC( char, sizeof(sat_solver));
-    memset( s, 0, sizeof(sat_solver) );
+    sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver));
+
+    Vec_RecAlloc_(&s->Mem);
+    s->hLearnts = -1;
+    s->hBinary = Vec_RecAppend( &s->Mem, clause_size(2, 0) );
+    s->binary = clause_read( s, s->hBinary );
+    s->binary->size_learnt = (2 << 1);
 
     // initialize vectors
-    vecp_new(&s->clauses);
-    vecp_new(&s->learnts);
     veci_new(&s->order);
     veci_new(&s->trail_lim);
     veci_new(&s->tagged);
@@ -901,15 +946,10 @@ sat_solver* sat_solver_new(void)
     // initialize arrays
     s->wlists    = 0;
     s->activity  = 0;
-    s->factors   = 0;
-    s->assigns   = 0;
     s->orderpos  = 0;
     s->reasons   = 0;
-    s->levels    = 0;
-    s->tags      = 0;
     s->trail     = 0;
 
-
     // initialize other vars
     s->size                   = 0;
     s->cap                    = 0;
@@ -929,8 +969,8 @@ sat_solver* sat_solver_new(void)
     s->simpdb_props           = 0;
     s->random_seed            = 91648253;
     s->progress_estimate      = 0;
-    s->binary                 = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
-    s->binary->size_learnt    = (2 << 1);
+//    s->binary                 = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
+//    s->binary->size_learnt    = (2 << 1);
     s->verbosity              = 0;
 
     s->stats.starts           = 0;
@@ -943,12 +983,6 @@ sat_solver* sat_solver_new(void)
     s->stats.learnts          = 0;
     s->stats.learnts_literals = 0;
     s->stats.tot_literals     = 0;
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    s->pMem = NULL;
-#else
-    s->pMem = Sat_MmStepStart( 10 );
-#endif
     return s;
 }
 
@@ -960,42 +994,46 @@ void sat_solver_setnvars(sat_solver* s,int n)
         int old_cap = s->cap;
         while (s->cap < n) s->cap = s->cap*2+1;
 
-        s->wlists    = ABC_REALLOC(vecp,   s->wlists,   s->cap*2);
+        s->wlists    = ABC_REALLOC(veci,   s->wlists,   s->cap*2);
+//        s->vi        = ABC_REALLOC(varinfo,s->vi,       s->cap);
+        s->levels    = ABC_REALLOC(int,    s->levels,   s->cap);
+        s->assigns   = ABC_REALLOC(char,   s->assigns,  s->cap);
+        s->polarity  = ABC_REALLOC(char,   s->polarity, s->cap);
+        s->tags      = ABC_REALLOC(char,   s->tags,     s->cap);
 #ifdef USE_FLOAT_ACTIVITY
         s->activity  = ABC_REALLOC(double,   s->activity, s->cap);
 #else
         s->activity  = ABC_REALLOC(unsigned, s->activity, s->cap);
 #endif
+        if ( s->factors )
         s->factors   = ABC_REALLOC(double, s->factors,  s->cap);
-        s->assigns   = ABC_REALLOC(lbool,  s->assigns,  s->cap);
         s->orderpos  = ABC_REALLOC(int,    s->orderpos, s->cap);
-        s->reasons   = ABC_REALLOC(clause*,s->reasons,  s->cap);
-        s->levels    = ABC_REALLOC(int,    s->levels,   s->cap);
-        s->tags      = ABC_REALLOC(lbool,  s->tags,     s->cap);
+        s->reasons   = ABC_REALLOC(int,    s->reasons,  s->cap);
         s->trail     = ABC_REALLOC(lit,    s->trail,    s->cap);
-        s->polarity  = ABC_REALLOC(char,   s->polarity, s->cap);
-        memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) );
-    }
+        memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(veci) );
+    } 
 
     for (var = s->size; var < n; var++){
         assert(!s->wlists[2*var].size);
         assert(!s->wlists[2*var+1].size);
         if ( s->wlists[2*var].ptr == NULL )
-            vecp_new(&s->wlists[2*var]);
+            veci_new(&s->wlists[2*var]);
         if ( s->wlists[2*var+1].ptr == NULL )
-            vecp_new(&s->wlists[2*var+1]);
+            veci_new(&s->wlists[2*var+1]);
 #ifdef USE_FLOAT_ACTIVITY
         s->activity[var] = 0;
 #else
         s->activity[var] = (1<<10);
 #endif
-        s->factors  [var] = 0;
-        s->assigns  [var] = l_Undef;
-        s->orderpos [var] = veci_size(&s->order);
-        s->reasons  [var] = (clause*)0;
-        s->levels   [var] = 0;
-        s->tags     [var] = l_Undef;
-        s->polarity [var] = 0;
+        if ( s->factors )
+        s->factors [var] = 0;
+//        *((int*)s->vi + var) = 0; s->vi[var].val = varX;
+        s->levels  [var] = 0;
+        s->assigns [var] = varX;
+        s->polarity[var] = 0;
+        s->tags    [var] = 0;
+        s->orderpos[var] = veci_size(&s->order);
+        s->reasons [var] = 0;
         
         /* does not hold because variables enqueued at top level will not be reinserted in the heap
            assert(veci_size(&s->order) == var); 
@@ -1009,20 +1047,9 @@ void sat_solver_setnvars(sat_solver* s,int n)
 
 void sat_solver_delete(sat_solver* s)
 {
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    int i;
-    for (i = 0; i < vecp_size(&s->clauses); i++)
-        ABC_FREE(vecp_begin(&s->clauses)[i]);
-    for (i = 0; i < vecp_size(&s->learnts); i++)
-        ABC_FREE(vecp_begin(&s->learnts)[i]);
-#else
-    Sat_MmStepStop( s->pMem, 0 );
-#endif
+    Vec_RecFree_( &s->Mem );
 
     // delete vectors
-    vecp_delete(&s->clauses);
-    vecp_delete(&s->learnts);
     veci_delete(&s->order);
     veci_delete(&s->trail_lim);
     veci_delete(&s->tagged);
@@ -1031,23 +1058,23 @@ void sat_solver_delete(sat_solver* s)
     veci_delete(&s->act_vars);
     veci_delete(&s->temp_clause);
     veci_delete(&s->conf_final);
-    ABC_FREE(s->binary);
 
     // delete arrays
-    if (s->wlists != 0){
+    if (s->reasons != 0){
         int i;
         for (i = 0; i < s->cap*2; i++)
-            vecp_delete(&s->wlists[i]);
+            veci_delete(&s->wlists[i]);
         ABC_FREE(s->wlists   );
+//        ABC_FREE(s->vi       );
+        ABC_FREE(s->levels   );
+        ABC_FREE(s->assigns  );
+        ABC_FREE(s->polarity );
+        ABC_FREE(s->tags     );
         ABC_FREE(s->activity );
         ABC_FREE(s->factors  );
-        ABC_FREE(s->assigns  );
         ABC_FREE(s->orderpos );
         ABC_FREE(s->reasons  );
-        ABC_FREE(s->levels   );
         ABC_FREE(s->trail    );
-        ABC_FREE(s->tags     );
-        ABC_FREE(s->polarity );
     }
 
     sat_solver_store_free(s);
@@ -1057,16 +1084,13 @@ void sat_solver_delete(sat_solver* s)
 void sat_solver_rollback( sat_solver* s )
 {
     int i;
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    for (i = 0; i < vecp_size(&s->clauses); i++)
-        ABC_FREE(vecp_begin(&s->clauses)[i]);
-    for (i = 0; i < vecp_size(&s->learnts); i++)
-        ABC_FREE(vecp_begin(&s->learnts)[i]);
-#else
-    Sat_MmStepRestart( s->pMem );
-#endif
-    vecp_resize(&s->clauses, 0);
-    vecp_resize(&s->learnts, 0);
+    Vec_RecRestart( &s->Mem );
+
+    s->hLearnts = -1;
+    s->hBinary = Vec_RecAppend( &s->Mem, clause_size(2, 0) );
+    s->binary = clause_read( s, s->hBinary );
+    s->binary->size_learnt = (2 << 1);
+
     veci_resize(&s->trail_lim, 0);
     veci_resize(&s->order, 0);
     for ( i = 0; i < s->size*2; i++ )
@@ -1105,56 +1129,49 @@ void sat_solver_rollback( sat_solver* s )
     s->stats.tot_literals     = 0;
 }
 
-
+/*
 static void clause_remove(sat_solver* s, clause* c)
 {
     lit* lits = clause_begin(c);
     assert(lit_neg(lits[0]) < s->size*2);
     assert(lit_neg(lits[1]) < s->size*2);
 
-    //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
-    //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
+    //veci_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
+    //veci_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
 
     assert(lits[0] < s->size*2);
-    vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
-    vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
+    veci_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(clause_nlits(c) > 2 ? c : clause_from_lit(lits[1])));
+    veci_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(clause_nlits(c) > 2 ? c : clause_from_lit(lits[0])));
 
     if (clause_learnt(c)){
         s->stats.learnts--;
-        s->stats.learnts_literals -= clause_size(c);
+        s->stats.learnts_literals -= clause_nlits(c);
     }else{
         s->stats.clauses--;
-        s->stats.clauses_literals -= clause_size(c);
+        s->stats.clauses_literals -= clause_nlits(c);
     }
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    ABC_FREE(c);
-#else
-    Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
-#endif
 }
 
 static lbool clause_simplify(sat_solver* s, clause* c)
 {
     lit*   lits   = clause_begin(c);
-    lbool* values = s->assigns;
     int i;
 
     assert(sat_solver_dl(s) == 0);
 
-    for (i = 0; i < clause_size(c); i++){
+    for (i = 0; i < clause_nlits(c); i++){
         lbool sig = !lit_sign(lits[i]); sig += sig - 1;
-        if (values[lit_var(lits[i])] == sig)
+        if (s->assignss[lit_var(lits[i])] == sig)
             return l_True;
     }
     return l_False;
 }
+*/
 
 int sat_solver_simplify(sat_solver* s)
 {
-    clause** reasons;
-    int type;
-
+//    clause** reasons;
+//    int type;
     assert(sat_solver_dl(s) == 0);
 
     if (sat_solver_propagate(s) != 0)
@@ -1162,7 +1179,7 @@ int sat_solver_simplify(sat_solver* s)
 
     if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
         return true;
-
+/*
     reasons = s->reasons;
     for (type = 0; type < 2; type++){
         vecp*    cs  = type ? &s->learnts : &s->clauses;
@@ -1178,53 +1195,48 @@ int sat_solver_simplify(sat_solver* s)
         }
         vecp_resize(cs,j);
     }
-
+*/
     s->simpdb_assigns = s->qhead;
     // (shouldn't depend on 'stats' really, but it will do for now)
     s->simpdb_props   = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
-
     return true;
 }
 
 
+/*
 static int clause_cmp (const void* x, const void* y) {
-    return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
-
+    return clause_nlits((clause*)x) > 2 && (clause_nlits((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
 void sat_solver_reducedb(sat_solver* s)
 {
     int      i, j;
-    double   extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
-    clause** learnts = (clause**)vecp_begin(&s->learnts);
+    double   extra_lim = s->cla_inc / veci_size(&s->learnts); // Remove any clause below this activity
+    clause** learnts = (clause**)veci_begin(&s->learnts);
     clause** reasons = s->reasons;
 
-    sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
+    sat_solver_sort(veci_begin(&s->learnts), veci_size(&s->learnts), &clause_cmp);
 
-    for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
-        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
+    for (i = j = 0; i < veci_size(&s->learnts) / 2; i++){
+        if (clause_nlits(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
             clause_remove(s,learnts[i]);
         else
             learnts[j++] = learnts[i];
     }
-    for (; i < vecp_size(&s->learnts); i++){
-        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
+    for (; i < veci_size(&s->learnts); i++){
+        if (clause_nlits(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
             clause_remove(s,learnts[i]);
         else
             learnts[j++] = learnts[i];
     }
-
-    //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);
-
-
-    vecp_resize(&s->learnts,j);
+    veci_resize(&s->learnts,j);
 }
+*/
 
 int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
 {
-    clause * c;
     lit *i,*j;
     int maxvar;
-    lbool* values;
     lit last;
+    assert( begin < end );
 
     veci_resize( &s->temp_clause, 0 );
     for ( i = begin; i < end; i++ )
@@ -1232,10 +1244,6 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
     begin = veci_begin( &s->temp_clause );
     end = begin + veci_size( &s->temp_clause );
 
-    if (begin == end) 
-        return false;
-
-    //printlits(begin,end); printf("\n");
     // insertion sort
     maxvar = lit_var(*begin);
     for (i = begin + 1; i < end; i++){
@@ -1246,7 +1254,6 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
         *j = l;
     }
     sat_solver_setnvars(s,maxvar+1);
-//    sat_solver_setnvars(s, lit_var(*(end-1))+1 );
 
     ///////////////////////////////////
     // add clause to internal storage
@@ -1257,17 +1264,13 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
     }
     ///////////////////////////////////
 
-    //printlits(begin,end); printf("\n");
-    values = s->assigns;
-
     // delete duplicates
     last = lit_Undef;
     for (i = j = begin; i < end; i++){
-        //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
-        lbool sig = !lit_sign(*i); sig += sig - 1;
-        if (*i == lit_neg(last) || sig == values[lit_var(*i)])
+        //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]));
+        if (*i == lit_neg(last) || var_value(s, lit_var(*i)) == lit_sign(*i))
             return true;   // tautology
-        else if (*i != last && values[lit_var(*i)] == l_Undef)
+        else if (*i != last && var_value(s, lit_var(*i)) == varX)
             last = *j++ = *i;
     }
 //    j = i;
@@ -1276,17 +1279,13 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
         return false;
 
     if (j - begin == 1) // unit clause
-        return sat_solver_enqueue(s,*begin,(clause*)0);
+        return sat_solver_enqueue(s,*begin,0);
 
     // create new clause
-    c = clause_create_new(s,begin,j,0);
-    if ( c )
-        vecp_push(&s->clauses,c);
-
+    clause_create_new(s,begin,j,0);
 
     s->stats.clauses++;
     s->stats.clauses_literals += j - begin;
-
     return true;
 }
 
@@ -1313,7 +1312,6 @@ void luby_test()
 
 static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT64_T nof_learnts)
 {
-    int*    levels          = s->levels;
     double  var_decay       = 0.95;
     double  clause_decay    = 0.999;
     double  random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
@@ -1343,8 +1341,8 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
             act_var_bump_global(s, s->act_vars.ptr[i]);
 
     for (;;){
-        clause* confl = sat_solver_propagate(s);
-        if (confl != 0){
+        int hConfl = sat_solver_propagate(s);
+        if (hConfl != 0){
             // CONFLICT
             int blevel;
 
@@ -1354,24 +1352,25 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
             s->stats.conflicts++; conflictC++;
             if (sat_solver_dl(s) == s->root_level){
 #ifdef SAT_USE_ANALYZE_FINAL
-                sat_solver_analyze_final(s, confl, 0);
+                sat_solver_analyze_final(s, hConfl, 0);
 #endif
                 veci_delete(&learnt_clause);
                 return l_False;
             }
 
             veci_resize(&learnt_clause,0);
-            sat_solver_analyze(s, confl, &learnt_clause);
-            blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
+            sat_solver_analyze(s, hConfl, &learnt_clause);
+            blevel = veci_size(&learnt_clause) > 1 ? var_level(s, lit_var(veci_begin(&learnt_clause)[1])) : s->root_level;
             blevel = s->root_level > blevel ? s->root_level : blevel;
             sat_solver_canceluntil(s,blevel);
             sat_solver_record(s,&learnt_clause);
 #ifdef SAT_USE_ANALYZE_FINAL
 //            if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0;    // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions)
-            if ( learnt_clause.size == 1 ) s->levels[lit_var(learnt_clause.ptr[0])] = 0;
+            if ( learnt_clause.size == 1 ) 
+                var_set_level(s, lit_var(learnt_clause.ptr[0]), 0);
 #endif
             act_var_decay(s);
-            act_clause_decay(s);
+//            act_clause_decay(s);
 
         }else{
             // NO CONFLICT
@@ -1385,7 +1384,6 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
                 return l_Undef; }
 
             if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
-//                 (s->nInsLimit  && s->stats.inspects  > s->nInsLimit) )
                  (s->nInsLimit  && s->stats.propagations > s->nInsLimit) )
             {
                 // Reached bound on number of conflicts:
@@ -1399,7 +1397,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
                 // Simplify the set of problem clauses:
                 sat_solver_simplify(s);
 
-//            if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
+//            if (nof_learnts >= 0 && veci_size(&s->learnts) - s->qtail >= nof_learnts)
                 // Reduce the set of learnt clauses:
 //                sat_solver_reducedb(s);
 
@@ -1409,11 +1407,10 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
 
             if (next == var_Undef){
                 // Model found:
-                lbool* values = s->assigns;
                 int i;
                 veci_resize(&s->model, 0);
                 for (i = 0; i < s->size; i++) 
-                    veci_push(&s->model,(int)values[i]);
+                    veci_push( &s->model, var_value(s,i)==var1 ? l_True : l_False );
                 sat_solver_canceluntil(s,s->root_level);
                 veci_delete(&learnt_clause);
 
@@ -1428,7 +1425,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
                 return l_True;
             }
 
-            if ( s->polarity[next] ) // positive polarity
+            if ( var_polar(s, next) ) // positive polarity
                 sat_solver_assume(s,toLit(next));
             else
                 sat_solver_assume(s,lit_neg(toLit(next)));
@@ -1444,7 +1441,6 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
     ABC_INT64_T  nof_conflicts;
     ABC_INT64_T  nof_learnts   = sat_solver_nclauses(s) / 3;
     lbool   status        = l_Undef;
-    lbool*  values        = s->assigns;
     lit*    i;
 
     ////////////////////////////////////////////////
@@ -1478,15 +1474,16 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
 
     //printf("solve: "); printlits(begin, end); printf("\n");
     for (i = begin; i < end; i++){
-        switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
-        case 1: // l_True: 
+//        switch (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]){
+        switch (var_value(s, *i)) {
+        case var1: // l_True: 
             break;
-        case 0: // l_Undef
+        case varX: // l_Undef
             sat_solver_assume(s, *i);
-            if (sat_solver_propagate(s) == NULL)
+            if (sat_solver_propagate(s) == 0)
                 break;
             // fallthrough
-        case -1: // l_False 
+        case var0: // l_False 
             sat_solver_canceluntil(s, 0);
             return l_False;
         }
@@ -1535,21 +1532,18 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
         lit p = *i;
         assert(lit_var(p) < s->size);
         veci_push(&s->trail_lim,s->qtail);
-        if (!sat_solver_enqueue(s,p,(clause*)0))
+        if (!sat_solver_enqueue(s,p,0))
         {
-            clause * r = s->reasons[lit_var(p)];
-            if (r != NULL)
+            int h = s->reasons[lit_var(p)];
+            if (h)
             {
-                clause* confl;
-                if (clause_is_lit(r))
+                if (clause_is_lit(h))
                 {
-                    confl = s->binary;
-                    (clause_begin(confl))[1] = lit_neg(p);
-                    (clause_begin(confl))[0] = clause_read_lit(r);
+                    (clause_begin(s->binary))[1] = lit_neg(p);
+                    (clause_begin(s->binary))[0] = clause_read_lit(h);
+                    h = s->hBinary;
                 }
-                else
-                    confl = r;
-                sat_solver_analyze_final(s, confl, 1);
+                sat_solver_analyze_final(s, h, 1);
                 veci_push(&s->conf_final, lit_neg(p));
             }
             else
@@ -1557,7 +1551,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
                 veci_resize(&s->conf_final,0);
                 veci_push(&s->conf_final, lit_neg(p));
                 // the two lines below are a bug fix by Siert Wieringa 
-                if (s->levels[lit_var(p)] > 0)
+                if (var_level(s, lit_var(p)) > 0)
                     veci_push(&s->conf_final, p);
             }
             sat_solver_canceluntil(s, 0);
@@ -1565,9 +1559,9 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
         }
         else
         {
-            clause* confl = sat_solver_propagate(s);
-            if (confl != NULL){
-                sat_solver_analyze_final(s, confl, 0);
+            int fConfl = sat_solver_propagate(s);
+            if (fConfl){
+                sat_solver_analyze_final(s, fConfl, 0);
                 assert(s->conf_final.size > 0);
                 sat_solver_canceluntil(s, 0);
                 return l_False; }
@@ -1586,12 +1580,10 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
     }
 
     while (status == l_Undef){
-//        int nConfs = 0;
         double Ratio = (s->stats.learnts == 0)? 0.0 :
             s->stats.learnts_literals / (double)s->stats.learnts;
         if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
             break;
-
         if (s->verbosity >= 1)
         {
             printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", 
@@ -1606,31 +1598,16 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
             fflush(stdout);
         }
         nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) );
-//printf( "%d ", (int)nof_conflicts );
-//        nConfs = s->stats.conflicts;
         status = sat_solver_search(s, nof_conflicts, nof_learnts);
-//        if ( status == l_True )
-//            printf( "%d ", s->stats.conflicts - nConfs );
-
-//        nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
         nof_learnts    = nof_learnts * 11 / 10; //*= 1.1;
-//printf( "%d ", s->stats.conflicts  );
         // quit the loop if reached an external limit
         if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
-        {
-//            printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
             break;
-        }
-//        if ( s->nInsLimit  && s->stats.inspects > s->nInsLimit )
         if ( s->nInsLimit  && s->stats.propagations > s->nInsLimit )
-        {
-//            printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
             break;
-        }
         if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
             break;
     }
-//printf( "\n" );
     if (s->verbosity >= 1)
         printf("==============================================================================\n");
 
@@ -1655,7 +1632,7 @@ int sat_solver_nvars(sat_solver* s)
 
 int sat_solver_nclauses(sat_solver* s)
 {
-    return vecp_size(&s->clauses);
+    return s->stats.clauses;
 }
 
 
@@ -1710,57 +1687,6 @@ void * sat_solver_store_release( sat_solver * s )
     return pTemp;
 }
 
-//=================================================================================================
-// Sorting functions (sigh):
-
-static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
-{
-    int     i, j, best_i;
-    void*   tmp;
-
-    for (i = 0; i < size-1; i++){
-        best_i = i;
-        for (j = i+1; j < size; j++){
-            if (comp(array[j], array[best_i]) < 0)
-                best_i = j;
-        }
-        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
-    }
-}
-
-
-static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
-{
-    if (size <= 15)
-        selectionsort(array, size, comp);
-
-    else{
-        void*       pivot = array[irand(seed, size)];
-        void*       tmp;
-        int         i = -1;
-        int         j = size;
-
-        for(;;){
-            do i++; while(comp(array[i], pivot)<0);
-            do j--; while(comp(pivot, array[j])<0);
-
-            if (i >= j) break;
-
-            tmp = array[i]; array[i] = array[j]; array[j] = tmp;
-        }
-
-        sortrnd(array    , i     , comp, seed);
-        sortrnd(&array[i], size-i, comp, seed);
-    }
-}
 
-void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *))
-{
-//    int i;
-    double seed = 91648253;
-    sortrnd(array,size,comp,&seed);
-//    for ( i = 1; i < size; i++ )
-//        assert(comp(array[i-1], array[i])<0);
-}
 ABC_NAMESPACE_IMPL_END