mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

ensure relevancy isn't increased between calls

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-11-23 15:41:07 -08:00
parent 61371b4abf
commit 5dfe4a4b48
11 changed files with 110 additions and 70 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

136
src/sat/sat_binspr.cpp
View file

@ -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;
}

5
src/sat/sat_binspr.h
View file

@ -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() {}

2
src/sat/sat_config.cpp
View file

@ -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();

5
src/sat/sat_solver.cpp
View file

@ -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)

5
src/sat/sat_solver.h
View file

@ -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

2
src/smt/smt_case_split_queue.cpp
View file

@ -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;

10
src/smt/smt_context.cpp
View file

@ -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();
}

9
src/smt/smt_context.h
View file

@ -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()];

2
src/smt/smt_internalizer.cpp
View file

@ -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;

2
src/smt/smt_model_generator.cpp
View file

@ -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();
}

2
src/smt/theory_seq.cpp
View file

@ -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]);
}