From 303157d3b725048d01bd9f2d6fec2bf37bd50495 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Nov 2017 15:00:52 -0800
Subject: [PATCH] allow incremental mode override
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/ba_solver.h | 2 +-
src/sat/sat_config.cpp | 1 +
src/sat/sat_config.h | 1 +
src/sat/sat_simplifier.cpp | 31 +++++++++++++++++-------
src/sat/sat_simplifier.h | 1 +
src/sat/sat_simplifier_params.pyg | 1 +
src/sat/sat_solver.h | 1 +
src/sat/sat_solver/inc_sat_solver.cpp | 12 +++------
src/tactic/portfolio/parallel_tactic.cpp | 3 ++-
9 files changed, 34 insertions(+), 19 deletions(-)
diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h
index 16c853423..4eb46609f 100644
--- a/src/sat/ba_solver.h
+++ b/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;
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 31304bab5..c1c4ff5f8 100644
--- a/src/sat/sat_config.cpp
+++ b/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);
}
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 2e1d8a145..e1e40e100 100644
--- a/src/sat/sat_config.h
+++ b/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;
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 5dccdd379..2cc5758d3 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/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() &&
- !m_learned_in_use_lists &&
- m_num_calls >= m_bce_delay &&
+ return
+ !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && 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::cce_enabled() const { return !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && (m_cce || acce_enabled()); }
- 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::elim_vars_bdd_enabled() const { return !s.tracking_assumptions() && m_elim_vars_bdd && m_num_calls >= m_elim_vars_bdd_delay && single_threaded(); }
- bool simplifier::elim_vars_enabled() const { return !s.tracking_assumptions() && m_elim_vars && single_threaded(); }
+ bool simplifier::acce_enabled() const {
+ return !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_acce;
+ }
+ bool simplifier::cce_enabled() const {
+ return !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && (m_cce || acce_enabled());
+ }
+ 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) {
diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h
index 98cae5398..0acb78ce1 100644
--- a/src/sat/sat_simplifier.h
+++ b/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;
diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg
index 6dd00ec83..a8f0db724 100644
--- a/src/sat/sat_simplifier_params.pyg
+++ b/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'),
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index e7dae93a2..43e36de46 100644
--- a/src/sat/sat_solver.h
+++ b/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);
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 3f97025e9..f922be580 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/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_incremental_mode(incremental_mode) {
+ m_internalized_fmls(m) {
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);
diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp
index 5762271ba..381a13a48 100644
--- a/src/tactic/portfolio/parallel_tactic.cpp
+++ b/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) {