Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt

src/sat/ba_solver.h

@@ -370,7 +370,7 @@ namespace sat {
         inline void assign(literal l, justification j) { if (m_lookahead) m_lookahead->assign(l); else m_solver->assign(l, j); }
         inline void set_conflict(justification j, literal l) { if (m_lookahead) m_lookahead->set_conflict(); else m_solver->set_conflict(j, l); }
         inline config const& get_config() const { return m_lookahead ? m_lookahead->get_config() : m_solver->get_config(); }
-        inline void drat_add(literal_vector const& c, svector<drat::premise> const& premises) { m_solver->m_drat.add(c, premises); }
+        inline void drat_add(literal_vector const& c, svector<drat::premise> const& premises) { if (m_solver) m_solver->m_drat.add(c, premises); }
 
 
         mutable bool m_overflow;

src/sat/sat_config.cpp

@@ -42,6 +42,7 @@ namespace sat {
         m_lookahead_search = false;
         m_lookahead_simplify = false;
         m_elim_vars = false;
+        m_incremental = false;
         updt_params(p); 
     }
 

src/sat/sat_config.h

@@ -88,6 +88,7 @@ namespace sat {
         double             m_lookahead_cube_fraction;
         reward_t           m_lookahead_reward;
 
+        bool               m_incremental;
         unsigned           m_simplify_mult1;
         double             m_simplify_mult2;
         unsigned           m_simplify_max;

src/sat/sat_simplifier.cpp

@@ -93,17 +93,28 @@ namespace sat {
     bool simplifier::single_threaded() const { return s.m_config.m_num_threads == 1; }
 
     bool simplifier::bce_enabled() const { 
-        return !s.tracking_assumptions() && 
+        return 
-            !m_learned_in_use_lists && 
+            !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && 
-            m_num_calls >= m_bce_delay && 
             (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls || cce_enabled()); 
     }
-    bool simplifier::acce_enabled() const { return !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_acce; }
+    bool simplifier::acce_enabled() const { 
-    bool simplifier::cce_enabled()  const { return !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && (m_cce || acce_enabled()); }
+        return !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_acce; 
-    bool simplifier::abce_enabled() const { return !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_abce; }
+    }
-    bool simplifier::bca_enabled()  const { return !s.tracking_assumptions() && m_bca && m_learned_in_use_lists && single_threaded(); }
+    bool simplifier::cce_enabled()  const { 
-    bool simplifier::elim_vars_bdd_enabled() const { return !s.tracking_assumptions() && m_elim_vars_bdd && m_num_calls >= m_elim_vars_bdd_delay && single_threaded(); }
+        return !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && (m_cce || acce_enabled()); 
-    bool simplifier::elim_vars_enabled() const { return !s.tracking_assumptions() && m_elim_vars && single_threaded(); }    
+    }
+    bool simplifier::abce_enabled() const { 
+        return !m_incremental_mode && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_abce; 
+    }
+    bool simplifier::bca_enabled()  const { 
+        return !m_incremental_mode && !s.tracking_assumptions() && m_bca && m_learned_in_use_lists && single_threaded(); 
+    }
+    bool simplifier::elim_vars_bdd_enabled() const { 
+        return !m_incremental_mode && !s.tracking_assumptions() && m_elim_vars_bdd && m_num_calls >= m_elim_vars_bdd_delay && single_threaded(); 
+    }
+    bool simplifier::elim_vars_enabled() const { 
+        return !m_incremental_mode && !s.tracking_assumptions() && m_elim_vars && single_threaded(); 
+    }    
 
     void simplifier::register_clauses(clause_vector & cs) {
         std::stable_sort(cs.begin(), cs.end(), size_lt());
@@ -199,6 +210,7 @@ namespace sat {
     }
 
     void simplifier::operator()(bool learned) {
+
         if (s.inconsistent())
             return;
         if (!m_subsumption && !bce_enabled() && !bca_enabled() && !elim_vars_enabled())
@@ -1883,6 +1895,7 @@ namespace sat {
         m_elim_vars               = p.elim_vars();
         m_elim_vars_bdd           = p.elim_vars_bdd();
         m_elim_vars_bdd_delay     = p.elim_vars_bdd_delay();
+        m_incremental_mode        = s.get_config().m_incremental && !p.override_incremental();
     }
 
     void simplifier::collect_param_descrs(param_descrs & r) {

src/sat/sat_simplifier.h

@@ -80,6 +80,7 @@ namespace sat {
         unsigned               m_elim_blocked_clauses_at;
         bool                   m_retain_blocked_clauses;
         unsigned               m_blocked_clause_limit;
+        bool                   m_incremental_mode; 
         bool                   m_resolution;
         unsigned               m_res_limit;
         unsigned               m_res_occ_cutoff;

src/sat/sat_simplifier_params.pyg

@@ -10,6 +10,7 @@ def_module_params(module_name='sat',
 	                  ('bce_delay', UINT, 0, 'delay eliminate blocked clauses until simplification round'),
                           ('retain_blocked_clauses', BOOL, False, 'retain blocked clauses for propagation, hide them from variable elimination'),
                           ('blocked_clause_limit', UINT, 100000000, 'maximum number of literals visited during blocked clause elimination'),
+                          ('override_incremental', BOOL, False, 'override incemental safety gaps. Enable elimination of blocked clauses and variables even if solver is reused'),
                           ('resolution.limit', UINT, 500000000, 'approx. maximum number of literals visited during variable elimination'),
                           ('resolution.occ_cutoff', UINT, 10, 'first cutoff (on number of positive/negative occurrences) for Boolean variable elimination'),
                           ('resolution.occ_cutoff_range1', UINT, 8, 'second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses'),

src/sat/sat_solver.h

@@ -322,6 +322,7 @@ namespace sat {
         void set_par(parallel* p, unsigned id);
         bool canceled() { return !m_rlimit.inc(); }
         config const& get_config() const { return m_config; }
+        void set_incremental(bool b) { m_config.m_incremental = b; }
         extension* get_extension() const { return m_ext.get(); }
         void       set_extension(extension* e);
         bool       set_root(literal l, literal r);

src/sat/sat_solver/inc_sat_solver.cpp

@@ -70,7 +70,7 @@ class inc_sat_solver : public solver {
     bool                m_internalized;           // are formulas internalized?
     bool                m_internalized_converted; // have internalized formulas been converted back
     expr_ref_vector     m_internalized_fmls;      // formulas in internalized format
-    bool                m_incremental_mode;
+
 
     typedef obj_map<expr, sat::literal> dep2asm_t;
 public:
@@ -87,10 +87,10 @@ public:
         m_unknown("no reason given"),
         m_internalized(false), 
         m_internalized_converted(false), 
-        m_internalized_fmls(m),
+        m_internalized_fmls(m) {
-        m_incremental_mode(incremental_mode) {
         updt_params(p);
         init_preprocess();
+        m_solver.set_incremental(incremental_mode);
     }
 
     virtual ~inc_sat_solver() {}
@@ -101,7 +101,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_incremental_mode);
+        inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p, m_solver.get_config().m_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));
@@ -280,10 +280,6 @@ public:
     virtual void updt_params(params_ref const & p) {
         m_params.append(p);
         sat_params p1(p);
-        if (m_incremental_mode) {
-            m_params.set_bool("elim_vars", false);
-            m_params.set_uint("elim_blocked_clauses_at", UINT_MAX);
-        }
         m_params.set_bool("keep_cardinality_constraints", p1.cardinality_solver());
         m_params.set_bool("keep_pb_constraints", m_solver.get_config().m_pb_solver == sat::PB_SOLVER);
         m_params.set_bool("pb_num_system", m_solver.get_config().m_pb_solver == sat::PB_SORTING);

src/tactic/portfolio/parallel_tactic.cpp

@@ -339,6 +339,7 @@ private:
         m_allsat = false;
         m_num_unsat = 0;
         m_exn_code = 0;
+        m_params.set_bool("override_incremental", true);
     }
 
     void close_branch(solver_state& s, lbool status) {
@@ -538,7 +539,7 @@ public:
     parallel_tactic(ast_manager& m, params_ref const& p) :
         m_manager(m),
         m_params(p) {
-        init();
+        init();        
     }
 
     void operator ()(const goal_ref & g,goal_ref_buffer & result,model_converter_ref & mc,proof_converter_ref & pc,expr_dependency_ref & dep) {