From 5dfe4a4b4898fd823906ba951fcacf6db4eb2026 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 23 Nov 2019 15:41:07 -0800
Subject: [PATCH] ensure relevancy isn't increased between calls
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/sat_binspr.cpp | 136 ++++++++++++++++++-------------
src/sat/sat_binspr.h | 5 +-
src/sat/sat_config.cpp | 2 +-
src/sat/sat_solver.cpp | 5 ++
src/sat/sat_solver.h | 5 ++
src/smt/smt_case_split_queue.cpp | 2 +-
src/smt/smt_context.cpp | 10 ++-
src/smt/smt_context.h | 9 +-
src/smt/smt_internalizer.cpp | 2 +-
src/smt/smt_model_generator.cpp | 2 +-
src/smt/theory_seq.cpp | 2 +-
11 files changed, 110 insertions(+), 70 deletions(-)
diff --git a/src/sat/sat_binspr.cpp b/src/sat/sat_binspr.cpp
index 670e7dfd8..c73dab168 100644
--- a/src/sat/sat_binspr.cpp
+++ b/src/sat/sat_binspr.cpp
@@ -132,21 +132,43 @@ namespace sat {
};
void binspr::operator()() {
- unsigned num = s.num_vars();
+ s = alloc(solver, m_solver.params(), m_solver.rlimit());
+ m_solver.pop_to_base_level();
+ s->copy(m_solver, true);
+ unsigned num = s->num_vars();
m_bin_clauses = 0;
report _rep(*this);
m_use_list.reset();
- m_use_list.reserve(num*2);
- for (clause* c : s.m_clauses) {
+ m_use_list.reserve(num * 2);
+ for (clause* c : s->m_clauses) {
if (!c->frozen() && !c->was_removed()) {
for (literal lit : *c) {
m_use_list[lit.index()].push_back(c);
}
}
}
- TRACE("sat", s.display(tout););
+ TRACE("sat", s->display(tout););
algorithm2();
+ if (!s->inconsistent()) {
+ params_ref p;
+ p.set_uint("sat.max_conflicts", 10000);
+ p.set_bool("sat.binspr", false);
+ s->updt_params(p);
+ lbool r = s->check(0, nullptr);
+ }
+
+ if (s->inconsistent()) {
+ s->set_conflict();
+ }
+ else {
+ s->pop_to_base_level();
+ for (unsigned i = m_solver.init_trail_size(); i < s->init_trail_size(); ++i) {
+ literal lit = s->trail_literal(i);
+ m_solver.assign(lit, s->get_justification(lit));
+ }
+ TRACE("sat", tout << "added " << (s->init_trail_size() - m_solver.init_trail_size()) << " units\n";);
+ }
}
@@ -167,48 +189,48 @@ namespace sat {
void binspr::algorithm2() {
mk_masks();
- unsigned num_lits = 2 * s.num_vars();
- for (unsigned l_idx = 0; l_idx < num_lits && !s.inconsistent(); ++l_idx) {
- s.checkpoint();
+ unsigned num_lits = 2 * s->num_vars();
+ for (unsigned l_idx = 0; l_idx < num_lits && !s->inconsistent(); ++l_idx) {
+ s->checkpoint();
literal p = to_literal(l_idx);
- TRACE("sat", tout << "p " << p << " " << s.value(p) << "\n";);
- if (is_used(p) && s.value(p) == l_undef) {
- s.push();
- s.assign_scoped(p);
- unsigned sz_p = s.m_trail.size();
- s.propagate(false);
- if (s.inconsistent()) {
- s.pop(1);
- s.assign_unit(~p);
- s.propagate(false);
- TRACE("sat", s.display(tout << "unit\n"););
+ TRACE("sat", tout << "p " << p << " " << s->value(p) << "\n";);
+ if (is_used(p) && s->value(p) == l_undef) {
+ s->push();
+ s->assign_scoped(p);
+ unsigned sz_p = s->m_trail.size();
+ s->propagate(false);
+ if (s->inconsistent()) {
+ s->pop(1);
+ s->assign_unit(~p);
+ s->propagate(false);
+ TRACE("sat", s->display(tout << "unit\n"););
IF_VERBOSE(0, verbose_stream() << "unit " << (~p) << "\n");
continue;
}
- for (unsigned i = sz_p; !s.inconsistent() && i < s.m_trail.size(); ++i) {
- literal u = ~s.m_trail[i];
+ for (unsigned i = sz_p; !s->inconsistent() && i < s->m_trail.size(); ++i) {
+ literal u = ~s->m_trail[i];
TRACE("sat", tout << "p " << p << " u " << u << "\n";);
for (clause* cp : m_use_list[u.index()]) {
for (literal q : *cp) {
- if (s.inconsistent())
+ if (s->inconsistent())
break;
- if (s.value(q) != l_undef)
+ if (s->value(q) != l_undef)
continue;
- s.push();
- s.assign_scoped(q);
- unsigned sz_q = s.m_trail.size();
- s.propagate(false);
- if (s.inconsistent()) {
+ s->push();
+ s->assign_scoped(q);
+ unsigned sz_q = s->m_trail.size();
+ s->propagate(false);
+ if (s->inconsistent()) {
// learn ~p or ~q
- s.pop(1);
+ s->pop(1);
block_binary(p, q, true);
- s.propagate(false);
+ s->propagate(false);
continue;
}
bool found = false;
- for (unsigned j = sz_q; !found && j < s.m_trail.size(); ++j) {
- literal v = ~s.m_trail[j];
+ for (unsigned j = sz_q; !found && j < s->m_trail.size(); ++j) {
+ literal v = ~s->m_trail[j];
for (clause* cp2 : m_use_list[v.index()]) {
if (cp2->contains(p)) {
if (check_spr(p, q, u, v)) {
@@ -218,29 +240,29 @@ namespace sat {
}
}
}
- s.pop(1);
+ s->pop(1);
if (found) {
block_binary(p, q, false);
- s.propagate(false);
- TRACE("sat", s.display(tout););
+ s->propagate(false);
+ TRACE("sat", s->display(tout););
}
}
}
}
- s.pop(1);
+ s->pop(1);
}
}
}
bool binspr::is_used(literal lit) const {
- return !m_use_list[lit.index()].empty() || !s.get_wlist(~lit).empty();
+ return !m_use_list[lit.index()].empty() || !s->get_wlist(~lit).empty();
}
bool binspr::check_spr(literal p, literal q, literal u, literal v) {
- SASSERT(s.value(p) == l_true);
- SASSERT(s.value(q) == l_true);
- SASSERT(s.value(u) == l_false);
- SASSERT(s.value(v) == l_false);
+ SASSERT(s->value(p) == l_true);
+ SASSERT(s->value(q) == l_true);
+ SASSERT(s->value(u) == l_false);
+ SASSERT(s->value(v) == l_false);
init_g(p, q, u, v);
literal lits[4] = { p, q, ~u, ~v };
for (unsigned i = 0; g_is_sat() && i < 4; ++i) {
@@ -252,7 +274,7 @@ namespace sat {
}
void binspr::binary_are_unit_implied(literal p) {
- for (watched const& w : s.get_wlist(~p)) {
+ for (watched const& w : s->get_wlist(~p)) {
if (!g_is_sat()) {
break;
}
@@ -270,13 +292,13 @@ namespace sat {
continue;
}
- bool inconsistent = (s.value(lit) == l_true);
- if (s.value(lit) == l_undef) {
- s.push();
- s.assign_scoped(~lit);
- s.propagate(false);
- inconsistent = s.inconsistent();
- s.pop(1);
+ bool inconsistent = (s->value(lit) == l_true);
+ if (s->value(lit) == l_undef) {
+ s->push();
+ s->assign_scoped(~lit);
+ s->propagate(false);
+ inconsistent = s->inconsistent();
+ s->pop(1);
}
if (!inconsistent) {
@@ -295,23 +317,23 @@ namespace sat {
}
void binspr::clause_is_unit_implied(clause const& c) {
- s.push();
+ s->push();
clear_alpha();
for (literal lit : c) {
if (touch(lit)) {
continue;
}
- else if (s.value(lit) == l_true) {
- s.pop(1);
+ else if (s->value(lit) == l_true) {
+ s->pop(1);
return;
}
- else if (s.value(lit) != l_false) {
- s.assign_scoped(~lit);
+ else if (s->value(lit) != l_false) {
+ s->assign_scoped(~lit);
}
}
- s.propagate(false);
- bool inconsistent = s.inconsistent();
- s.pop(1);
+ s->propagate(false);
+ bool inconsistent = s->inconsistent();
+ s->pop(1);
if (!inconsistent) {
add_touched();
}
@@ -321,7 +343,7 @@ namespace sat {
void binspr::block_binary(literal lit1, literal lit2, bool learned) {
IF_VERBOSE(2, verbose_stream() << "SPR: " << learned << " " << ~lit1 << " " << ~lit2 << "\n");
TRACE("sat", tout << "SPR: " << learned << " " << ~lit1 << " " << ~lit2 << "\n";);
- s.mk_clause(~lit1, ~lit2, learned);
+ s->mk_clause(~lit1, ~lit2, learned);
++m_bin_clauses;
}
diff --git a/src/sat/sat_binspr.h b/src/sat/sat_binspr.h
index ddab19368..7531e592c 100644
--- a/src/sat/sat_binspr.h
+++ b/src/sat/sat_binspr.h
@@ -37,7 +37,8 @@ namespace sat {
not_pr = 0x0
};
- solver& s;
+ solver& m_solver;
+ scoped_ptr<solver> s;
unsigned m_bin_clauses;
unsigned m_stopped_at;
vector<clause_vector> m_use_list;
@@ -92,7 +93,7 @@ namespace sat {
public:
- binspr(solver& s, params_ref const& p): s(s), m_stopped_at(0), m_limit1(1000), m_limit2(300) {}
+ binspr(solver& s): m_solver(s), m_stopped_at(0), m_limit1(1000), m_limit2(300) {}
~binspr() {}
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index b93665430..832b58f6e 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -99,7 +99,7 @@ namespace sat {
m_local_search_dbg_flips = p.local_search_dbg_flips();
m_unit_walk = p.unit_walk();
m_unit_walk_threads = p.unit_walk_threads();
- m_binspr = false; // unsound :-( p.binspr();
+ m_binspr = p.binspr();
m_lookahead_simplify = p.lookahead_simplify();
m_lookahead_double = p.lookahead_double();
m_lookahead_simplify_bca = p.lookahead_simplify_bca();
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 4068adc08..860105583 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -53,6 +53,7 @@ namespace sat {
m_asymm_branch(*this, p),
m_probing(*this, p),
m_mus(*this),
+ m_binspr(*this),
m_inconsistent(false),
m_searching(false),
m_conflict(justification(0)),
@@ -1921,6 +1922,10 @@ namespace sat {
}
}
+ if (m_config.m_binspr && !inconsistent()) {
+ m_binspr();
+ }
+
#if 0
static unsigned file_no = 0;
#pragma omp critical (print_sat)
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index c5dc7c9d3..4fb587c7c 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -34,6 +34,7 @@ Revision History:
#include "sat/sat_iff3_finder.h"
#include "sat/sat_probing.h"
#include "sat/sat_mus.h"
+#include "sat/sat_binspr.h"
#include "sat/sat_drat.h"
#include "sat/sat_parallel.h"
#include "sat/sat_local_search.h"
@@ -102,6 +103,7 @@ namespace sat {
asymm_branch m_asymm_branch;
probing m_probing;
mus m_mus; // MUS for minimal core extraction
+ binspr m_binspr;
bool m_inconsistent;
bool m_searching;
// A conflict is usually a single justification. That is, a justification
@@ -323,6 +325,8 @@ namespace sat {
bool at_base_lvl() const override { return m_scope_lvl == 0; }
lbool value(literal l) const { return m_assignment[l.index()]; }
lbool value(bool_var v) const { return m_assignment[literal(v, false).index()]; }
+ justification get_justification(literal l) const { return m_justification[l.var()]; }
+ justification get_justification(bool_var v) const { return m_justification[v]; }
unsigned lvl(bool_var v) const { return m_justification[v].level(); }
unsigned lvl(literal l) const { return m_justification[l.var()].level(); }
unsigned init_trail_size() const override { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; }
@@ -612,6 +616,7 @@ namespace sat {
void pop_to_base_level() override;
unsigned num_user_scopes() const override { return m_user_scope_literals.size(); }
reslimit& rlimit() { return m_rlimit; }
+ params_ref const& params() { return m_params; }
// -----------------------
//
// Simplification
diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp
index e14b9434f..2c64772e0 100644
--- a/src/smt/smt_case_split_queue.cpp
+++ b/src/smt/smt_case_split_queue.cpp
@@ -1253,7 +1253,7 @@ namespace smt {
case_split_queue * mk_case_split_queue(context & ctx, smt_params & p) {
- if (p.m_relevancy_lvl < 2 && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY ||
+ if (ctx.relevancy_lvl() < 2 && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY ||
p.m_case_split_strategy == CS_RELEVANCY_GOAL)) {
warning_msg("relevancy must be enabled to use option CASE_SPLIT=3, 4 or 5");
p.m_case_split_strategy = CS_ACTIVITY;
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 1c64901c3..e554ce715 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -46,6 +46,7 @@ namespace smt {
m_fparams(p),
m_params(_p),
m_setup(*this, p),
+ m_relevancy_lvl(2),
m_asserted_formulas(m, p, _p),
m_rewriter(m),
m_qmanager(alloc(quantifier_manager, *this, p, _p)),
@@ -321,7 +322,7 @@ namespace smt {
TRACE("relevancy",
tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(l) << "\n";);
- if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(l)))
+ if (d.is_atom() && (m_relevancy_lvl == 0 || (m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(l)))
m_atom_propagation_queue.push_back(l);
if (m.has_trace_stream())
@@ -1582,7 +1583,7 @@ namespace smt {
SASSERT(relevancy());
// Quantifiers are only asserted when marked as relevant.
// Other atoms are only asserted when marked as relevant if m_relevancy_lvl >= 2
- if (d.is_atom() && (d.is_quantifier() || m_fparams.m_relevancy_lvl >= 2)) {
+ if (d.is_atom() && (d.is_quantifier() || m_relevancy_lvl >= 2)) {
lbool val = get_assignment(v);
if (val != l_undef)
m_atom_propagation_queue.push_back(literal(v, val == l_false));
@@ -3391,9 +3392,12 @@ namespace smt {
}
void context::setup_context(bool use_static_features) {
- if (m_setup.already_configured() || inconsistent())
+ if (m_setup.already_configured() || inconsistent()) {
+ m_relevancy_lvl = std::min(m_fparams.m_relevancy_lvl, m_relevancy_lvl);
return;
+ }
m_setup(get_config_mode(use_static_features));
+ m_relevancy_lvl = m_fparams.m_relevancy_lvl;
setup_components();
}
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 81e58d7ff..ff0c4609b 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -83,6 +83,7 @@ namespace smt {
smt_params & m_fparams;
params_ref m_params;
setup m_setup;
+ unsigned m_relevancy_lvl;
timer m_timer;
asserted_formulas m_asserted_formulas;
th_rewriter m_rewriter;
@@ -196,8 +197,8 @@ namespace smt {
literal_vector m_atom_propagation_queue;
- obj_map<expr, unsigned> m_cached_generation;
- obj_hashtable<expr> m_cache_generation_visited;
+ obj_map<expr, unsigned> m_cached_generation;
+ obj_hashtable<expr> m_cache_generation_visited;
dyn_ack_manager m_dyn_ack_manager;
// -----------------------------------
@@ -280,9 +281,11 @@ namespace smt {
}
bool relevancy() const {
- return m_fparams.m_relevancy_lvl > 0;
+ return m_relevancy_lvl > 0;
}
+ unsigned relevancy_lvl() const { return m_relevancy_lvl; }
+
enode * get_enode(expr const * n) const {
SASSERT(e_internalized(n));
return m_app2enode[n->get_id()];
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 0ee56069e..0f3dd2b5c 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1195,7 +1195,7 @@ namespace smt {
// Reason: when a learned clause becomes unit, it should mark the
// unit literal as relevant. When binary_clause_opt is used,
// it is not possible to distinguish between learned and non-learned clauses.
- if (lemma && m_fparams.m_relevancy_lvl >= 2)
+ if (lemma && m_relevancy_lvl >= 2)
return false;
if (m_base_lvl > 0)
return false;
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index 955327904..7b80c44af 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -497,7 +497,7 @@ namespace smt {
mk_func_interps();
finalize_theory_models();
register_macros();
- TRACE("model", model_v2_pp(tout, *m_model, true););
+ TRACE("model", model_v2_pp(tout, *m_model, true););
return m_model.get();
}
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 3a81f18ec..fd2acf42b 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3684,7 +3684,6 @@ bool theory_seq::internalize_term(app* term) {
return true;
}
for (auto arg : *term) {
- ensure_enodes(arg);
mk_var(ensure_enode(arg));
}
if (m.is_bool(term)) {
@@ -5135,6 +5134,7 @@ void theory_seq::ensure_enodes(expr* e) {
}
}
}
+ // TBD: std::stable_sort(m_ensure_todo.begin(), m_ensure_todo.end(), compare_depth);
for (unsigned i = m_ensure_todo.size(); i-- > 0; ) {
ensure_enode(m_ensure_todo[i]);
}