Proof-logging in the updated solver.

1 files changed, 9 insertions, 21 deletions

diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 1c9e9dbb..cde37116 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -85,13 +85,13 @@ struct varinfo_t
 {
     unsigned val    :  2;  // variable value 
     unsigned pol    :  1;  // last polarity
-    unsigned glo    :  1;  // global variable
+    unsigned partA  :  1;  // partA variable
     unsigned tag    :  4;  // conflict analysis tags
     unsigned lev    : 24;  // variable level
 };
 
-int    var_is_global (sat_solver2* s, int v)            { return s->vi[v].glo; }
-void   var_set_global(sat_solver2* s, int v, int glo)   { s->vi[v].glo = glo; if (glo) veci_push(&s->glob_vars, v); }
+int    var_is_partA (sat_solver2* s, int v)              { return s->vi[v].partA;  }
+void   var_set_partA(sat_solver2* s, int v, int partA)   { s->vi[v].partA = partA; }
 
 static inline int     var_value     (sat_solver2* s, int v)            { return s->vi[v].val; }
 static inline int     var_polar     (sat_solver2* s, int v)            { return s->vi[v].pol; }
@@ -145,7 +145,7 @@ static inline void    solver2_clear_marks(sat_solver2* s)              {
 static inline satset* clause_read   (sat_solver2* s, cla h)      { return satset_read( &s->clauses, h );    }
 static inline cla     clause_handle (sat_solver2* s, satset* c)  { return satset_handle( &s->clauses, c );  }
 static inline int     clause_check  (sat_solver2* s, satset* c)  { return satset_check( &s->clauses, c );   }
-static inline int     clause_proofid(sat_solver2* s, satset* c)  { return c->learnt ? veci_begin(&s->claProofs)[c->Id]<<1 : (clause_handle(s,c)<<1) | 1;                   }
+static inline int     clause_proofid(sat_solver2* s, satset* c, int partA)  { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (clause_handle(s,c)<<2) | 1; }
 
 //static inline int     var_reason    (sat_solver2* s, int v)      { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1;                   } 
 //static inline int     lit_reason    (sat_solver2* s, int l)      { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; } 
@@ -180,10 +180,7 @@ static inline void proof_chain_start( sat_solver2* s, satset* c )
         s->iStartChain = veci_size(&s->proof_clas);
         veci_push(&s->proof_clas, 0);
         veci_push(&s->proof_clas, 0);
-        veci_push(&s->proof_clas, clause_proofid(s, c) );
-        veci_push(&s->proof_vars, 0);
-        veci_push(&s->proof_vars, 0);
-        veci_push(&s->proof_vars, 0);
+        veci_push(&s->proof_clas, clause_proofid(s, c, 0) );
     }
 }
 
@@ -192,8 +189,7 @@ static inline void proof_chain_resolve( sat_solver2* s, satset* cls, int Var )
     if ( s->fProofLogging )
     {
         satset* c = cls ? cls : var_unit_clause( s, Var );
-        veci_push(&s->proof_clas, clause_proofid(s, c) );
-        veci_push(&s->proof_vars, Var);
+        veci_push(&s->proof_clas, clause_proofid(s, c, var_is_partA(s,Var)) );
 //        printf( "%d %d  ", clause_proofid(s, c), Var );
     }
 }
@@ -1225,9 +1221,7 @@ sat_solver2* sat_solver2_new(void)
     veci_new(&s->mark_levels);
     veci_new(&s->min_lit_order); 
     veci_new(&s->min_step_order);
-    veci_new(&s->glob_vars);
     veci_new(&s->proof_clas); veci_push(&s->proof_clas, -1);
-    veci_new(&s->proof_vars); veci_push(&s->proof_vars, -1);
     veci_new(&s->claActs);    veci_push(&s->claActs,    -1);
     veci_new(&s->claProofs);  veci_push(&s->claProofs,  -1);
 
@@ -1256,8 +1250,6 @@ sat_solver2* sat_solver2_new(void)
     {
         s->proof_clas.cap = (1 << 20);
         s->proof_clas.ptr = ABC_REALLOC( int, s->proof_clas.ptr, s->proof_clas.cap );
-        s->proof_vars.cap = (1 << 20);
-        s->proof_vars.ptr = ABC_REALLOC( int, s->proof_vars.ptr, s->proof_clas.cap );
     }
     return s;
 }
@@ -1306,16 +1298,14 @@ void sat_solver2_delete(sat_solver2* s)
 {
     satset * c = clause_read(s, s->iLearntLast);
     // report statistics
-    assert( veci_size(&s->proof_clas) == veci_size(&s->proof_vars) );
-    printf( "Used %6.2f Mb for proof-logging.   Unit clauses = %d.\n", 8.0 * veci_size(&s->proof_clas) / (1<<20), s->nUnits );
+    printf( "Used %6.2f Mb for proof-logging.   Unit clauses = %d.\n", 2.0 * veci_size(&s->proof_clas) / (1<<20), s->nUnits );
 
     Sat_ProofTest( 
         &s->clauses,      // clauses
         &s->proof_clas,   // proof clauses
-        &s->proof_vars,   // proof variables
         NULL,             // proof roots
-        veci_begin(&s->claProofs)[c->Id],  // one root
-        &s->glob_vars );  // global variables (for interpolation)
+        veci_begin(&s->claProofs)[c->Id]  // one root
+         );  
 
     // delete vectors
     veci_delete(&s->order);
@@ -1328,9 +1318,7 @@ void sat_solver2_delete(sat_solver2* s)
     veci_delete(&s->mark_levels);
     veci_delete(&s->min_lit_order);
     veci_delete(&s->min_step_order);
-    veci_delete(&s->glob_vars);
     veci_delete(&s->proof_clas);
-    veci_delete(&s->proof_vars);
     veci_delete(&s->claActs);
     veci_delete(&s->claProofs);
     veci_delete(&s->clauses);