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

optimizations to bv-solver and euf-egraph (#4698)

Browse source 
* additional bit-vector propagators

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

* rename restrict (not a keyword, but well) #4694, tune euf

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

* merge

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

* add pb rewriting to pb2bv #4697

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-20 06:47:27 -07:00 • committed by GitHub
parent ed44a44579
commit 6f63f8761c
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
24 changed files with 206 additions and 116 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_asymm_branch.cpp
View file

@ -171,6 +171,7 @@ namespace sat {
TRACE("asymm_branch_detail", s.display(tout););
report rpt(*this);
bool_vector saved_phase(s.m_phase);
flet<bool> _is_probing(s.m_is_probing, true);
bool change = true;
unsigned counter = 0;

2
src/sat/sat_probing.cpp
View file

@ -237,7 +237,7 @@ namespace sat {
if (m_probing_cache && memory::get_allocation_size() > m_probing_cache_limit)
m_cached_bins.finalize();
flet<bool> _probing(m_active, true);
flet<bool> _is_probing(s.m_is_probing, true);
report rpt(*this);
bool r = true;
m_counter = 0;

2
src/sat/sat_probing.h
View file

@ -31,7 +31,6 @@ namespace sat {
unsigned m_stopped_at; // where did it stop
literal_set m_assigned; // literals assigned in the first branch
literal_vector m_to_assert;
bool m_active { false };
// counters
int m_counter; // track cost
@ -78,7 +77,6 @@ namespace sat {
void collect_statistics(statistics & st) const;
void reset_statistics();
bool active() const { return m_active; }
// return the literals implied by l.
// return 0, if the cache is not available

7
src/sat/sat_solver.cpp
View file

@ -955,9 +955,11 @@ namespace sat {
m_assigned_since_gc[v] = true;
m_trail.push_back(l);
if (m_ext && m_external[v])
if (m_ext && m_external[v] && (!is_probing() || at_base_lvl()))
m_ext->asserted(l);
// else
// std::cout << "assert " << l << "\n";
switch (m_config.m_branching_heuristic) {
case BH_VSIDS:
break;
@ -1339,6 +1341,7 @@ namespace sat {
m_conflicts_since_restart = 0;
m_restart_threshold = m_config.m_restart_initial;
}
log_stats();
lbool is_sat = l_undef;
while (is_sat == l_undef && !should_cancel()) {
if (inconsistent()) is_sat = resolve_conflict_core();

4
src/sat/sat_solver.h
View file

@ -103,6 +103,7 @@ namespace sat {
scc m_scc;
asymm_branch m_asymm_branch;
probing m_probing;
bool m_is_probing { false };
mus m_mus; // MUS for minimal core extraction
binspr m_binspr;
bool m_inconsistent;
@ -350,6 +351,7 @@ namespace sat {
bool was_eliminated(bool_var v) const { return m_eliminated[v]; }
void set_eliminated(bool_var v, bool f) override;
bool was_eliminated(literal l) const { return was_eliminated(l.var()); }
void set_phase(literal l) override { m_phase[l.var()] = !l.sign(); }
unsigned scope_lvl() const { return m_scope_lvl; }
unsigned search_lvl() const { return m_search_lvl; }
bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; }
@ -662,7 +664,7 @@ namespace sat {
public:
void set_should_simplify() { m_next_simplify = m_conflicts_since_init; }
bool_var_vector const& get_vars_to_reinit() const { return m_vars_to_reinit; }
bool is_probing() const { return m_probing.active(); }
bool is_probing() const { return m_is_probing; }
public:
void user_push() override;

1
src/sat/sat_solver_core.h
View file

@ -81,6 +81,7 @@ namespace sat {
virtual void set_external(bool_var v) {}
virtual void set_non_external(bool_var v) {}
virtual void set_eliminated(bool_var v, bool f) {}
virtual void set_phase(literal l) { }
// optional support for user-scopes. Not relevant for sat_tactic integration.
// it is only relevant for incremental mode SAT, which isn't wrapped (yet)

2
src/sat/smt/bv_internalize.cpp
View file

@ -597,7 +597,7 @@ namespace bv {
if (a) {
if (!a->is_fresh())
ctx.push(add_eq_occurs_trail(a));
a->m_eqs = new (get_region()) eq_occurs(idx, v1, v2, n, a->m_eqs);
a->m_eqs = new (get_region()) eq_occurs(idx, v1, v2, expr2literal(n->get_expr()), n, a->m_eqs);
}
}

30
src/sat/smt/bv_solver.cpp
View file

@ -152,7 +152,7 @@ namespace bv {
SASSERT(m_bits[v1][idx] == ~m_bits[v2][idx]);
TRACE("bv", tout << "found new diseq axiom\n" << pp(v1) << pp(v2););
m_stats.m_num_diseq_static++;
expr_ref eq(m.mk_eq(var2expr(v1), var2expr(v2)), m);
expr_ref eq = mk_var_eq(v1, v2);
add_unit(~ctx.internalize(eq, false, false, m_is_redundant));
}
@ -252,7 +252,7 @@ namespace bv {
force_push();
assert_ackerman(v1, v2);
}
else
else
m_ackerman.used_diseq_eh(v1, v2);
}
@ -410,7 +410,7 @@ namespace bv {
}
void solver::propagate_eq_occurs(eq_occurs const& occ) {
auto lit = expr2literal(occ.m_node->get_expr());
auto lit = occ.m_literal;
if (s().value(lit) != l_undef)
return;
lbool val1 = s().value(m_bits[occ.m_v1][occ.m_idx]);
@ -438,16 +438,24 @@ namespace bv {
if (val == l_false)
bit1.neg();
for (theory_var v2 = m_find.next(v1); v2 != v1 && !s().inconsistent(); v2 = m_find.next(v2)) {
unsigned num_bits = 0, num_assigned = 0;
for (theory_var v2 = m_find.next(v1); v2 != v1; v2 = m_find.next(v2)) {
literal bit2 = m_bits[v2][idx];
SASSERT(m_bits[v1][idx] != ~m_bits[v2][idx]);
TRACE("bv", tout << "propagating #" << var2enode(v2)->get_expr_id() << "[" << idx << "] = " << s().value(bit2) << "\n";);
if (val == l_false)
bit2.neg();
if (l_true != s().value(bit2))
assign_bit(bit2, v1, v2, idx, bit1, false);
++num_bits;
if (num_bits > 4 && num_assigned == 0)
break;
if (s().value(bit2) == l_true)
continue;
++num_assigned;
if (!assign_bit(bit2, v1, v2, idx, bit1, false))
break;
}
// std::cout << num_bits << " " << num_assigned << "\n";
}
sat::check_result solver::check() {
@ -718,7 +726,9 @@ namespace bv {
return sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index());
}
void solver::assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc) {
bool solver::assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc) {
m_stats.m_num_bit2core++;
SASSERT(ctx.s().value(antecedent) == l_true);
SASSERT(m_bits[v2][idx].var() == consequent.var());
@ -727,10 +737,11 @@ namespace bv {
if (s().value(consequent) == l_false) {
m_stats.m_num_conflicts++;
SASSERT(s().inconsistent());
return false;
}
else {
if (false && get_config().m_bv_eq_axioms) {
expr_ref eq(m.mk_eq(var2expr(v1), var2expr(v2)), m);
expr_ref eq = mk_var_eq(v1, v2);
flet<bool> _is_redundant(m_is_redundant, true);
literal eq_lit = ctx.internalize(eq, false, false, m_is_redundant);
add_clause(~antecedent, ~eq_lit, consequent);
@ -744,7 +755,8 @@ namespace bv {
if (a && a->is_bit())
for (auto curr : a->to_bit())
if (propagate_eqc || find(curr.first) != find(v2) || curr.second != idx)
m_prop_queue.push_back(propagation_item(curr));
m_prop_queue.push_back(propagation_item(curr));
return true;
}
}

7
src/sat/smt/bv_solver.h
View file

@ -137,10 +137,11 @@ namespace bv {
unsigned m_idx;
theory_var m_v1;
theory_var m_v2;
sat::literal m_literal;
euf::enode* m_node;
eq_occurs* m_next;
eq_occurs(unsigned idx, theory_var v1, theory_var v2, euf::enode* n, eq_occurs* next = nullptr):
m_idx(idx), m_v1(v1), m_v2(v2), m_node(n), m_next(next) {}
eq_occurs(unsigned idx, theory_var v1, theory_var v2, sat::literal lit, euf::enode* n, eq_occurs* next = nullptr):
m_idx(idx), m_v1(v1), m_v2(v2), m_literal(lit), m_node(n), m_next(next) {}
};
class eq_occurs_it {
@ -278,7 +279,7 @@ namespace bv {
void add_fixed_eq(theory_var v1, theory_var v2);
svector<theory_var> m_merge_aux[2]; //!< auxiliary vector used in merge_zero_one_bits
bool merge_zero_one_bits(theory_var r1, theory_var r2);
void assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc);
bool assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc);
void propagate_bits(var_pos entry);
void propagate_eq_occurs(eq_occurs const& occ);
numeral const& power2(unsigned i) const;

26
src/sat/smt/euf_internalize.cpp
View file

@ -82,10 +82,11 @@ namespace euf {
void solver::attach_node(euf::enode* n) {
expr* e = n->get_expr();
sat::literal lit;
if (!m.is_bool(e))
drat_log_node(e);
else
attach_lit(literal(si.add_bool_var(e), false), e);
lit = attach_lit(literal(si.add_bool_var(e), false), e);
if (!m.is_bool(e) && m.get_sort(e)->get_family_id() != null_family_id) {
auto* e_ext = expr2solver(e);
@ -93,7 +94,7 @@ namespace euf {
if (s_ext && s_ext != e_ext)
s_ext->apply_sort_cnstr(n, m.get_sort(e));
}
expr* a = nullptr, * b = nullptr;
expr* a = nullptr, * b = nullptr;
if (m.is_eq(e, a, b) && m.get_sort(a)->get_family_id() != null_family_id) {
auto* s_ext = sort2solver(m.get_sort(a));
if (s_ext)
@ -121,10 +122,12 @@ namespace euf {
return lit;
m_var2expr[v] = e;
m_var_trail.push_back(v);
if (!m_egraph.find(e)) {
enode* n = m_egraph.mk(e, 0, nullptr);
enode* n = m_egraph.find(e);
if (!n)
n = m_egraph.mk(e, 0, nullptr);
m_egraph.set_bool_var(n, v);
if (!m.is_true(e) && !m.is_false(e))
m_egraph.set_merge_enabled(n, false);
}
return lit;
}
@ -262,6 +265,19 @@ namespace euf {
s().add_clause(2, lits1, st);
s().add_clause(2, lits2, st);
}
else if (m.is_eq(e, th, el) && !m.is_iff(e)) {
sat::literal lit1 = expr2literal(e);
s().set_phase(lit1);
expr_ref e2(m.mk_eq(el, th), m);
enode* n2 = m_egraph.find(e2);
if (n2) {
sat::literal lit2 = expr2literal(e2);
sat::literal lits1[2] = { ~lit1, lit2 };
sat::literal lits2[2] = { lit1, ~lit2 };
s().add_clause(2, lits1, st);
s().add_clause(2, lits2, st);
}
}
}

40
src/sat/smt/euf_solver.cpp
View file

@ -45,12 +45,7 @@ namespace euf {
[&](std::ostream& out, void* j) {
display_justification_ptr(out, reinterpret_cast<size_t*>(j));
};
std::function<lbool(enode* n)> eval = [&](enode* n) {
sat::literal lit = expr2literal(n->get_expr());
return (lit == sat::null_literal) ? l_undef : s().value(lit);
};
m_egraph.set_display_justification(disp);
m_egraph.set_eval(eval);
}
void solver::updt_params(params_ref const& p) {
@ -197,7 +192,7 @@ namespace euf {
e = m_var2expr[l.var()];
n = m_egraph.find(e);
SASSERT(n);
SASSERT(m_egraph.is_equality(n));
SASSERT(n->is_equality());
SASSERT(!l.sign());
m_egraph.explain_eq<size_t>(m_explain, n->get_arg(0), n->get_arg(1));
break;
@ -219,28 +214,32 @@ namespace euf {
if (!e)
return;
bool sign = l.sign();
TRACE("euf", tout << "asserted: " << mk_bounded_pp(e, m) << " := " << l << "@" << s().scope_lvl() << "\n";);
euf::enode* n = m_egraph.find(e);
TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << "\n";);
if (!n)
return;
for (auto th : enode_th_vars(n))
bool sign = l.sign();
m_egraph.set_value(n, sign ? l_false : l_true);
auto const & j = s().get_justification(l);
for (auto th : enode_th_vars(n))
m_id2solver[th.get_id()]->asserted(l);
if (!n->merge_enabled())
return;
size_t* c = to_ptr(l);
SASSERT(is_literal(c));
SASSERT(l == get_literal(c));
if (m.is_eq(e) && n->num_args() == 2 && !sign) {
SASSERT(!m.is_iff(e));
euf::enode* na = n->get_arg(0);
euf::enode* nb = n->get_arg(1);
m_egraph.merge(na, nb, c);
}
else {
else if (n->merge_enabled()) {
euf::enode* nb = sign ? mk_false() : mk_true();
m_egraph.merge(n, nb, c);
}
else if (m.is_eq(e) && n->num_args() == 2 && sign) {
m_egraph.new_diseq(n);
}
}
@ -278,7 +277,7 @@ namespace euf {
bool is_eq = p.second;
expr* e = n->get_expr();
expr* a = nullptr, *b = nullptr;
bool_var v = si.to_bool_var(e);
bool_var v = n->bool_var();
SASSERT(m.is_bool(e));
size_t cnstr;
literal lit;
@ -288,10 +287,12 @@ namespace euf {
lit = literal(v, false);
}
else {
a = e, b = n->get_root()->get_expr();
SASSERT(m.is_true(b) || m.is_false(b));
lbool val = n->get_root()->value();
a = e;
b = (val == l_true) ? m.mk_true() : m.mk_false();
SASSERT(val != l_undef);
cnstr = lit_constraint().to_index();
lit = literal(v, m.is_false(b));
lit = literal(v, val == l_false);
}
unsigned lvl = s().scope_lvl();
@ -457,10 +458,7 @@ namespace euf {
auto* ext = bool_var2solver(v);
if (ext)
return ext->get_phase(v);
expr* e = bool_var2expr(v);
if (e && m.is_eq(e))
return l_true;
return l_undef;
return l_undef;
}
bool solver::set_root(literal l, literal r) {

4
src/sat/smt/sat_th.cpp
View file

@ -135,7 +135,9 @@ namespace euf {
return !is_true(a, b, c, d) && (ctx.s().add_clause(4, lits, sat::status::th(m_is_redundant, get_id())), true);
}
bool th_euf_solver::is_true(sat::literal lit) { return ctx.s().value(lit) == l_true; }
bool th_euf_solver::is_true(sat::literal lit) {
return ctx.s().value(lit) == l_true;
}
euf::enode* th_euf_solver::mk_enode(expr* e, bool suppress_args) {
m_args.reset();

11
src/sat/tactic/goal2sat.cpp
View file

@ -136,7 +136,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
void mk_root_clause(sat::literal l) {
TRACE("goal2sat", tout << "mk_clause: " << l << "\n";);
m_solver.add_clause(1, &l, m_is_redundant ? mk_status() : sat::status::input());
m_solver.add_clause(1, &l, m_is_redundant ? mk_status() : sat::status::input());
}
void mk_root_clause(sat::literal l1, sat::literal l2) {
@ -191,9 +191,12 @@ struct goal2sat::imp : public sat::sat_internalizer {
sat::bool_var to_bool_var(expr* e) override {
sat::literal l;
sat::bool_var v = m_map.to_bool_var(e);
if (v != sat::null_bool_var)
return v;
if (is_app(e) && m_cache.find(to_app(e), l) && !l.sign())
return l.var();
return m_map.to_bool_var(e);
return sat::null_bool_var;
}
@ -399,6 +402,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
if (m_aig)
m_aig->add_or(l, num, aig_lits.c_ptr());
m_solver.set_phase(~l);
m_result_stack.shrink(old_sz);
if (sign)
l.neg();
@ -450,7 +454,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
mk_clause(num+1, lits);
if (m_aig) {
m_aig->add_and(l, num, aig_lits.c_ptr());
}
}
m_solver.set_phase(l);
if (sign)
l.neg();