fix some things for clause replay

src/smt/smt_context.cpp

@@ -82,8 +82,7 @@ namespace smt {
         m_mk_bool_var_trail(*this),
         m_mk_enode_trail(*this),
         m_mk_lambda_trail(*this),
-        m_lemma_visitor(m),
+        m_lemma_visitor(m) {
-        m_recorded_clauses(m) {
 
         SASSERT(m_scope_lvl == 0);
         SASSERT(m_base_lvl == 0);

src/smt/smt_context.h

@@ -137,7 +137,7 @@ namespace smt {
         scoped_ptr<base_dependent_expr_state> m_fmls;
 
         svector<double> m_lit_scores[2];
-        expr_ref_vector m_recorded_clauses;
+        vector<literal_vector> m_recorded_clauses;
 
 
         // -----------------------------------
@@ -1302,7 +1302,7 @@ namespace smt {
 
         void add_scores(unsigned n, literal const *lits);
 
-        void record_clause(clause const* cls);
+        void record_clause(unsigned n, literal const * lits);
 
 
         // -----------------------------------

src/smt/smt_internalizer.cpp

@@ -936,7 +936,6 @@ namespace smt {
         m_lit_scores[0].reserve(v + 1);
         m_lit_scores[1].reserve(v + 1);
         m_lit_scores[0][v] = m_lit_scores[1][v] = 0.0;
-        m_recorded_clauses.reserve(v + 1);
 
         literal l(v, false);
         literal not_l(v, true);
@@ -967,29 +966,23 @@ namespace smt {
     }
 
     // following the pattern of solver::persist_clause in src/sat/smt/user_solver.cpp
-    void context::record_clause(clause const* cls) {
+    void context::record_clause(unsigned num_lits, literal const *lits) {
-        expr_ref_vector clause(m);
+        literal_vector clause;
-        for (unsigned i = 0; i < cls->get_num_literals(); ++i) {
+        clause.append(num_lits, lits);
-            literal lit = cls->get_literal(i);
+        m_recorded_clauses.push_back(clause);
-            clause.push_back(literal2expr(~lit));
-        }
-        if (!clause.empty() && m.is_false(clause.back()))
-            clause.pop_back();
-        expr_ref disj(m.mk_or(clause.size(), clause.data()), m);
-        m_recorded_clauses.push_back(disj);
     }
 
     void context::add_scores(unsigned n, literal const *lits) {
         for (unsigned i = 0; i < n; ++i) {
             auto lit = lits[i];
-            unsigned v = lit.var();  // unique key per literal
+            unsigned v = lit.var();  // uniq0 / n;
-            m_lit_scores[lit.sign()][v] += 1.0 / n;
         }
     }
 
     
     void context::undo_mk_bool_var() {
-        SASSERT(!m_b_internalized_stack.empty());
+        SASSERT(!m_b_internalized_stack.empty(ue key per literal
+            m_lit_scores[lit.sign()][v] += 1.));
         m_stats.m_num_del_bool_var++;
         expr * n              = m_b_internalized_stack.back();
         unsigned n_id         = n->get_id();
@@ -1447,6 +1440,7 @@ namespace smt {
         case CLS_LEARNED:
             dump_lemma(num_lits, lits);
             add_scores(num_lits, lits);
+            record_clause(num_lits, lits);
             break;
         default:
             break;
@@ -1506,7 +1500,6 @@ namespace smt {
                 if (k == CLS_LEARNED) {
                     int w2_idx  = select_learned_watch_lit(cls);
                     cls->swap_lits(1, w2_idx);
-                    record_clause(cls);
                 }
                 else {
                     SASSERT(k == CLS_TH_LEMMA);

src/smt/smt_parallel.cpp

@@ -82,7 +82,26 @@ namespace smt {
 
     void parallel::param_generator::replay_proof_prefixes(unsigned max_conflicts_epsilon=200) {
         unsigned conflict_budget = m_max_prefix_conflicts + max_conflicts_epsilon;
+        // loop through m_param_probe_contexts
+        for (unsigned i = 0; i < m_param_probe_contexts.size(); ++i) {
+            IF_VERBOSE(1, verbose_stream() << " PARAM TUNER: replaying proof prefix in param probe context " << i << "\n");
+            context *probe_ctx = m_param_probe_contexts[i];
+            probe_ctx->get_fparams().m_max_conflicts = conflict_budget;
             
+            for (auto const& clause : probe_ctx->m_recorded_clauses) {
+                expr_ref_vector negated_lits(probe_ctx->m);
+                for (literal lit : clause) {
+                    expr* e = probe_ctx->bool_var2expr(lit.var());
+                    if (!e) continue;  // skip if var not yet mapped
+                    if (!lit.sign())
+                        e = probe_ctx->m.mk_not(e); // since bool_var2expr discards sign
+                    negated_lits.push_back(e);
+                }
+
+                // Replay the negated clause
+                lbool r = probe_ctx->check(negated_lits.size(), negated_lits.data());
+            }
+        }
     }
 
     void parallel::param_generator::protocol_iteration() {