merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/sat_elim_vars.cpp

@@ -87,7 +87,7 @@ namespace sat{
         simp.m_neg_cls.reset();
         simp.collect_clauses(pos_l, simp.m_pos_cls);
         simp.collect_clauses(neg_l, simp.m_neg_cls);
-        VERIFY(!s.is_external(v));
+        VERIFY(!simp.is_external(v));
         model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
         simp.save_clauses(mc_entry, simp.m_pos_cls);
         simp.save_clauses(mc_entry, simp.m_neg_cls);

src/sat/sat_scc.h

@@ -63,7 +63,9 @@ namespace sat {
         literal get_parent(literal l) const { return m_big.get_parent(l); }
         literal get_root(literal l) const { return m_big.get_root(l); }
         bool reaches(literal u, literal v) const { return m_big.reaches(u, v); }        
-        bool connected(literal u, literal v) const { return m_big.connected(u, v); }
+        bool connected(literal u, literal v) const {
+            return m_big.connected(u, v); 
+        }
     };
 };
 

src/sat/sat_solver.cpp

@@ -1341,7 +1341,6 @@ namespace sat {
         m_assumption_set.insert(lit);
         m_assumptions.push_back(lit);
         set_external(lit.var());
-        VERIFY(is_external(lit.var()));
     }
 
     void solver::pop_assumption() {
@@ -1457,13 +1456,11 @@ namespace sat {
             CASSERT("sat_missed_prop", check_missed_propagation());
             CASSERT("sat_simplify_bug", check_invariant());
         }
-		si.check_watches();
         if (m_config.m_lookahead_simplify) {
             lookahead lh(*this);
             lh.simplify();
             lh.collect_statistics(m_aux_stats);
         }
-		si.check_watches();
         sort_watch_lits();
         CASSERT("sat_simplify_bug", check_invariant());
 

src/sat/sat_solver/inc_sat_solver.cpp

@@ -36,6 +36,7 @@ Notes:
 #include "ast/ast_util.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "sat/sat_params.hpp"
+#include "sat/sat_simplifier_params.hpp"
 
 // incremental SAT solver.
 class inc_sat_solver : public solver {
@@ -88,7 +89,17 @@ public:
         m_internalized_fmls(m) {
         updt_params(p);
         init_preprocess();
-        m_solver.set_incremental(incremental_mode);
+        m_solver.set_incremental(incremental_mode && !override_incremental());
+    }
+
+    bool override_incremental() const {
+        sat_simplifier_params p(m_params);
+        std::cout << "override: " << p.override_incremental() << "\n";
+        return p.override_incremental();
+    }
+
+    bool is_incremental() const {
+        return m_solver.get_config().m_incremental;
     }
 
     virtual ~inc_sat_solver() {}
@@ -99,7 +110,7 @@ public:
         }
         ast_translation tr(m, dst_m);
         m_solver.pop_to_base_level();
-        inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p, m_solver.get_config().m_incremental);
+        inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p, is_incremental());
         result->m_solver.copy(m_solver);
         result->m_fmls_head = m_fmls_head;
         for (expr* f : m_fmls) result->m_fmls.push_back(tr(f));
@@ -272,6 +283,7 @@ public:
         m_params.set_bool("pb_totalizer", m_solver.get_config().m_pb_solver == sat::PB_TOTALIZER);
         m_params.set_bool("xor_solver", p1.xor_solver());
         m_solver.updt_params(m_params);
+        m_solver.set_incremental(is_incremental() && !override_incremental());
 
     }
     virtual void collect_statistics(statistics & st) const {
@@ -517,7 +529,7 @@ private:
         m_pc = g->pc();
         m_mc = g->mc();
         TRACE("sat", g->display_with_dependencies(tout););
-        m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, m_solver.get_config().m_incremental, is_lemma);
+        m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, is_incremental(), is_lemma);
         m_goal2sat.get_interpreted_atoms(atoms);
         if (!atoms.empty()) {
             std::stringstream strm;