mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

bv fixes and tuning (#4703)

Browse source 
* heap size information

* bv tuning

* fix #4701

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

* throw on set-has-size #4700

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-21 19:54:53 -07:00 committed by GitHub
parent ba5c9c3883
commit b7ec4489a6
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
21 changed files with 339 additions and 169 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/array_decl_plugin.cpp
View file

@ -460,6 +460,7 @@ func_decl * array_decl_plugin::mk_set_has_size(unsigned arity, sort * const* dom
m_manager->raise_exception("set-has-size takes two arguments");
return nullptr;
}
m_manager->raise_exception("set-has-size is not supported");
// domain[0] is a Boolean array,
// domain[1] is Int
arith_util arith(*m_manager);

26
src/ast/euf/euf_egraph.cpp
View file

@ -22,6 +22,7 @@ Author:
namespace euf {
void egraph::undo_eq(enode* r1, enode* n1, unsigned r2_num_parents) {
enode* r2 = r1->get_root();
r2->dec_class_size(r1->class_size());
@ -113,6 +114,7 @@ namespace euf {
egraph::egraph(ast_manager& m) : m(m), m_table(m), m_exprs(m) {
m_tmp_eq = enode::mk_tmp(m_region, 2);
// m_updates.reserve(10000, update_record(nullptr));
}
egraph::~egraph() {
@ -143,14 +145,15 @@ namespace euf {
if (is_eq) ++m_stats.m_num_eqs; else ++m_stats.m_num_lits;
}
void egraph::new_diseq(enode* n1) {
SASSERT(n1->is_equality());
enode* arg1 = n1->get_arg(0), * arg2 = n1->get_arg(1);
void egraph::new_diseq(enode* n) {
SASSERT(n->is_equality());
SASSERT(n->value() == l_false);
enode* arg1 = n->get_arg(0), * arg2 = n->get_arg(1);
enode* r1 = arg1->get_root();
enode* r2 = arg2->get_root();
TRACE("euf", tout << "new-diseq: " << mk_pp(r1->get_expr(), m) << " " << mk_pp(r2->get_expr(), m) << ": " << r1->has_th_vars() << " " << r2->has_th_vars() << "\n";);
if (r1 == r2) {
add_literal(n1, true);
add_literal(n, true);
return;
}
if (!r1->has_th_vars())
@ -163,7 +166,7 @@ namespace euf {
return;
theory_var v1 = arg1->get_closest_th_var(id);
theory_var v2 = arg2->get_closest_th_var(id);
add_th_diseq(id, v1, v2, n1->get_expr());
add_th_diseq(id, v1, v2, n->get_expr());
return;
}
for (auto p : euf::enode_th_vars(r1)) {
@ -171,7 +174,7 @@ namespace euf {
continue;
for (auto q : euf::enode_th_vars(r2))
if (p.get_id() == q.get_id())
add_th_diseq(p.get_id(), p.get_var(), q.get_var(), n1->get_expr());
add_th_diseq(p.get_id(), p.get_var(), q.get_var(), n->get_expr());
}
}
@ -250,9 +253,9 @@ namespace euf {
}
}
void egraph::set_value(enode* n, lbool value) {
void egraph::set_value(enode* n, lbool value) {
force_push();
VERIFY(n->value() == l_undef);
SASSERT(n->value() == l_undef);
n->set_value(value);
m_updates.push_back(update_record(n, update_record::value_assignment()));
}
@ -331,9 +334,8 @@ namespace euf {
}
void egraph::merge(enode* n1, enode* n2, justification j) {
if (!n1->merge_enabled() && !n2->merge_enabled()) {
return;
}
if (!n1->merge_enabled() && !n2->merge_enabled())
return;
SASSERT(m.get_sort(n1->get_expr()) == m.get_sort(n2->get_expr()));
enode* r1 = n1->get_root();
enode* r2 = n2->get_root();
@ -357,7 +359,7 @@ namespace euf {
if (j.is_congruence() && (m.is_false(r2->get_expr()) || m.is_true(r2->get_expr()))) {
add_literal(n1, false);
}
if (n1->is_equality() && r2->value() == l_false)
if (n1->is_equality() && n1->value() == l_false)
new_diseq(n1);
unsigned num_merge = 0, num_eqs = 0;
for (enode* p : enode_parents(n1)) {

2
src/ast/euf/euf_egraph.h
View file

@ -207,7 +207,7 @@ namespace euf {
\brief merge nodes, all effects are deferred to the propagation step.
*/
void merge(enode* n1, enode* n2, void* reason) { merge(n1, n2, justification::external(reason)); }
void new_diseq(enode* n1);
void new_diseq(enode* n);
/**

12
src/cmd_context/cmd_context.cpp
View file

@ -285,7 +285,8 @@ bool cmd_context::contains_func_decl(symbol const& s, unsigned n, sort* const* d
}
bool cmd_context::contains_macro(symbol const& s) const {
return m_macros.contains(s);
macro_decls decls;
return m_macros.find(s, decls) && !decls.empty();
}
bool cmd_context::contains_macro(symbol const& s, func_decl* f) const {
@ -851,6 +852,7 @@ void cmd_context::insert(symbol const & s, unsigned arity, sort *const* domain,
insert_macro(s, arity, domain, t);
if (!m_global_decls) {
m_macros_stack.push_back(s);
}
}
@ -890,6 +892,8 @@ void cmd_context::model_add(symbol const & s, unsigned arity, sort *const* domai
fs.insert(m(), fn);
VERIFY(fn->get_range() == m().get_sort(t));
m_mc0->add(fn, t);
if (!m_global_decls)
m_func_decls_stack.push_back(sf_pair(s, fn));
}
void cmd_context::model_del(func_decl* f) {
@ -1424,10 +1428,8 @@ void cmd_context::restore_macros(unsigned old_sz) {
SASSERT(old_sz <= m_macros_stack.size());
svector<symbol>::iterator it = m_macros_stack.begin() + old_sz;
svector<symbol>::iterator end = m_macros_stack.end();
for (; it != end; ++it) {
symbol const & s = *it;
erase_macro(s);
}
for (; it != end; ++it)
erase_macro(*it);
m_macros_stack.shrink(old_sz);
}

1
src/cmd_context/cmd_context.h
View file

@ -81,6 +81,7 @@ public:
macro_decls() { m_decls = nullptr; }
void finalize(ast_manager& m);
bool insert(ast_manager& m, unsigned arity, sort *const* domain, expr* body);
bool empty() const { return !m_decls || m_decls->empty(); }
expr* find(unsigned arity, sort *const* domain) const;
void erase_last(ast_manager& m);
vector<macro_decl>::iterator begin() const { return m_decls->begin(); }

2
src/sat/sat_elim_eqs.cpp
View file

@ -218,10 +218,12 @@ namespace sat {
void elim_eqs::save_elim(literal_vector const & roots, bool_var_vector const & to_elim) {
model_converter & mc = m_solver.m_mc;
for (bool_var v : to_elim) {
literal l(v, false);
literal r = roots[v];
SASSERT(v != r.var());
if (m_solver.m_cut_simplifier) m_solver.m_cut_simplifier->set_root(v, r);
bool set_root = m_solver.set_root(l, r);
bool root_ok = !m_solver.is_external(v) || set_root;

1
src/sat/sat_scc.cpp
View file

@ -203,6 +203,7 @@ namespace sat {
in_s[l2_idx] = false;
literal l2 = to_literal(l2_idx);
bool_var v2 = l2.var();
if (roots[v2] == null_literal) {
if (l2.sign()) {
roots[v2] = ~r;

9
src/sat/sat_simplifier.cpp
View file

@ -995,6 +995,7 @@ namespace sat {
literal next() { SASSERT(!empty()); return to_literal(m_queue.erase_min()); }
bool empty() const { return m_queue.empty(); }
void reset() { m_queue.reset(); }
unsigned size() const { return m_queue.size(); }
};
simplifier & s;
@ -1589,9 +1590,8 @@ namespace sat {
SASSERT(!s.is_external(l));
model_converter::entry& new_entry = m_mc.mk(k, l.var());
for (literal lit : c) {
if (lit != l && process_var(lit.var())) {
m_queue.decreased(~lit);
}
if (lit != l && process_var(lit.var()))
m_queue.decreased(~lit);
}
m_mc.insert(new_entry, m_covered_clause);
m_mc.set_clause(new_entry, c);
@ -1605,7 +1605,8 @@ namespace sat {
s.set_learned(l1, l2);
m_mc.insert(new_entry, m_covered_clause);
m_mc.set_clause(new_entry, l1, l2);
m_queue.decreased(~l2);
if (process_var(l2.var()))
m_queue.decreased(~l2);
}
void bca() {

47
src/sat/sat_solver.cpp
View file

@ -318,24 +318,7 @@ namespace sat {
}
void solver::set_external(bool_var v) {
if (m_external[v]) return;
m_external[v] = true;
if (!m_ext) return;
lbool val = value(v);
switch (val) {
case l_true: {
m_ext->asserted(literal(v, false));
break;
}
case l_false: {
m_ext->asserted(literal(v, true));
break;
}
default:
break;
}
}
void solver::set_eliminated(bool_var v, bool f) {
@ -347,10 +330,13 @@ namespace sat {
clause* solver::mk_clause(unsigned num_lits, literal * lits, sat::status st) {
m_model_is_current = false;
for (unsigned i = 0; i < num_lits; i++)
VERIFY(!was_eliminated(lits[i]));
DEBUG_CODE({
for (unsigned i = 0; i < num_lits; i++) {
CTRACE("sat", m_eliminated[lits[i].var()], tout << lits[i] << " was eliminated\n";);
SASSERT(m_eliminated[lits[i].var()] == false);
CTRACE("sat", was_eliminated(lits[i]), tout << lits[i] << " was eliminated\n";);
SASSERT(!was_eliminated(lits[i]));
}
});
@ -587,7 +573,7 @@ namespace sat {
m_stats.m_mk_clause++;
clause * r = alloc_clause(num_lits, lits, st.is_redundant());
SASSERT(!st.is_redundant() || r->is_learned());
bool reinit = attach_nary_clause(*r);
bool reinit = attach_nary_clause(*r, st.is_sat() && st.is_redundant());
if (reinit || has_variables_to_reinit(*r)) push_reinit_stack(*r);
if (st.is_redundant()) {
m_learned.push_back(r);
@ -604,11 +590,11 @@ namespace sat {
return r;
}
bool solver::attach_nary_clause(clause & c) {
bool solver::attach_nary_clause(clause & c, bool is_asserting) {
bool reinit = false;
clause_offset cls_off = cls_allocator().get_offset(&c);
if (!at_base_lvl()) {
if (c.is_learned() && !c.on_reinit_stack()) {
if (is_asserting) {
unsigned w2_idx = select_learned_watch_lit(c);
std::swap(c[1], c[w2_idx]);
}
@ -626,7 +612,7 @@ namespace sat {
level = std::max(level, lvl(c[i]));
}
assign(c[1], justification(level, cls_off));
reinit = !c.is_learned();
reinit |= !c.is_learned();
}
else if (value(c[1]) == l_false) {
m_stats.m_propagate++;
@ -635,7 +621,7 @@ namespace sat {
level = std::max(level, lvl(c[i]));
}
assign(c[0], justification(level, cls_off));
reinit = !c.is_learned();
reinit |= !c.is_learned();
}
}
unsigned some_idx = c.size() >> 1;
@ -655,7 +641,7 @@ namespace sat {
if (ENABLE_TERNARY && c.size() == 3)
reinit = attach_ter_clause(c, c.is_learned() ? sat::status::redundant() : sat::status::asserted());
else
reinit = attach_nary_clause(c);
reinit = attach_nary_clause(c, c.is_learned() && !c.on_reinit_stack());
}
void solver::set_learned(clause& c, bool redundant) {
@ -1332,16 +1318,18 @@ namespace sat {
return l_undef;
}
if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) {
log_stats();
if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) {
m_restart_threshold = m_config.m_burst_search;
lbool r = bounded_search();
if (r != l_undef)
log_stats();
if (r != l_undef)
return r;
pop_reinit(scope_lvl());
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();
@ -1353,6 +1341,7 @@ namespace sat {
else if (should_simplify()) do_simplify();
else if (!decide()) is_sat = final_check();
}
log_stats();
return is_sat;
}
catch (const abort_solver &) {
@ -3588,8 +3577,6 @@ namespace sat {
if (!m_replay_assign.empty()) IF_VERBOSE(20, verbose_stream() << "replay assign: " << m_replay_assign.size() << "\n");
for (unsigned i = m_replay_assign.size(); i-- > 0; ) {
literal lit = m_replay_assign[i];
if (m_ext && m_external[lit.var()])
m_ext->asserted(lit);
m_trail.push_back(lit);
}

2
src/sat/sat_solver.h
View file

@ -290,7 +290,7 @@ namespace sat {
clause * mk_nary_clause(unsigned num_lits, literal * lits, status st);
bool has_variables_to_reinit(clause const& c) const;
bool has_variables_to_reinit(literal l1, literal l2) const;
bool attach_nary_clause(clause & c);
bool attach_nary_clause(clause & c, bool is_asserting);
void attach_clause(clause & c, bool & reinit);
void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); }
void set_learned(clause& c, bool learned);

20
src/sat/smt/bv_ackerman.cpp
View file

@ -41,18 +41,22 @@ namespace bv {
if (v1 > v2)
std::swap(v1, v2);
vv* n = m_tmp_vv;
n->v1 = v1;
n->v2 = v2;
n->set_var(v1, v2);
vv* other = m_table.insert_if_not_there(n);
other->m_count++;
update_glue(*other);
if (other->m_count > m_propagate_high_watermark || other->m_glue == 0)
s.s().set_should_simplify();
vv::push_to_front(m_queue, other);
if (other == n) {
new_tmp();
gc();
}
if (other->m_glue == 0) {
remove(other);
add_cc(v1, v2);
}
else if (other->m_count > m_propagate_high_watermark)
s.s().set_should_simplify();
}
void ackerman::used_diseq_eh(euf::theory_var v1, euf::theory_var v2) {
@ -61,17 +65,17 @@ namespace bv {
if (v1 > v2)
std::swap(v1, v2);
vv* n = m_tmp_vv;
n->v1 = v1;
n->v2 = v2;
n->set_var(v1, v2);
vv* other = m_table.insert_if_not_there(n);
other->m_count++;
if (other->m_count > m_propagate_high_watermark || other->m_glue == 0)
s.s().set_should_simplify();
vv::push_to_front(m_queue, other);
if (other == n) {
new_tmp();
gc();
}
if (other->m_count > m_propagate_high_watermark)
s.s().set_should_simplify();
}
void ackerman::update_glue(vv& v) {

1
src/sat/smt/bv_ackerman.h
View file

@ -32,6 +32,7 @@ namespace bv {
unsigned m_glue{ UINT_MAX };
vv():v1(euf::null_theory_var), v2(euf::null_theory_var) {}
vv(euf::theory_var v1, euf::theory_var v2):v1(v1), v2(v2) {}
void set_var(euf::theory_var x, euf::theory_var y) { v1 = x; v2 = y; m_count = 0; m_glue = UINT_MAX; }
};
struct vv_eq {

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

@ -29,9 +29,15 @@ namespace bv {
solver::def_atom& solver::atom::to_def() {
SASSERT(!is_bit());
SASSERT(!is_eq());
return dynamic_cast<def_atom&>(*this);
}
solver::eq_atom& solver::atom::to_eq() {
SASSERT(is_eq());
return dynamic_cast<eq_atom&>(*this);
}
class solver::add_var_pos_trail : public trail<euf::solver> {
solver::bit_atom* m_atom;
public:
@ -43,15 +49,43 @@ namespace bv {
};
class solver::add_eq_occurs_trail : public trail<euf::solver> {
solver::bit_atom* m_atom;
bit_atom* m_atom;
public:
add_eq_occurs_trail(solver::bit_atom* a) :m_atom(a) {}
add_eq_occurs_trail(bit_atom* a) :m_atom(a) {}
void undo(euf::solver& euf) override {
SASSERT(m_atom->m_eqs);
m_atom->m_eqs = m_atom->m_eqs->m_next;
if (m_atom->m_eqs)
m_atom->m_eqs->m_prev = nullptr;
}
};
class solver::del_eq_occurs_trail : public trail<euf::solver> {
bit_atom* m_atom;
eq_occurs* m_node;
public:
del_eq_occurs_trail(bit_atom* a, eq_occurs* n) : m_atom(a), m_node(n) {}
void undo(euf::solver& euf) override {
if (m_node->m_next)
m_node->m_next->m_prev = m_node;
if (m_node->m_prev)
m_node->m_prev->m_next = m_node;
else
m_atom->m_eqs = m_node;
}
};
void solver::del_eq_occurs(bit_atom* a, eq_occurs* occ) {
eq_occurs* prev = occ->m_prev;
if (prev)
prev->m_next = occ->m_next;
else
a->m_eqs = occ->m_next;
if (occ->m_next)
occ->m_next->m_prev = prev;
ctx.push(del_eq_occurs_trail(a, occ));
}
class solver::mk_atom_trail : public trail<euf::solver> {
solver& th;
sat::bool_var m_var;
@ -263,11 +297,24 @@ namespace bv {
}
}
solver::eq_atom* solver::mk_eq_atom(sat::bool_var bv) {
atom* a = get_bv2a(bv);
if (a)
return a->is_eq() ? &a->to_eq() : nullptr;
else {
eq_atom* b = new (get_region()) eq_atom();
insert_bv2a(bv, b);
ctx.push(mk_atom_trail(bv, *this));
return b;
}
}
void solver::set_bit_eh(theory_var v, literal l, unsigned idx) {
SASSERT(m_bits[v][idx] == l);
if (s().value(l) != l_undef && s().lvl(l) == 0)
register_true_false_bit(v, idx);
else {
else if (m_bits[v].size() > 1) {
bit_atom* b = mk_bit_atom(l.var());
if (b) {
if (b->m_occs)
@ -551,15 +598,18 @@ namespace bv {
mk_var(argn);
}
theory_var v_arg = argn->get_th_var(get_id());
SASSERT(idx < get_bv_size(v_arg));
unsigned arg_sz = get_bv_size(v_arg);
SASSERT(idx < arg_sz);
sat::literal lit = expr2literal(n);
sat::literal lit0 = m_bits[v_arg][idx];
if (lit0 == sat::null_literal) {
m_bits[v_arg][idx] = lit;
bit_atom* a = new (get_region()) bit_atom();
a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
insert_bv2a(lit.var(), a);
ctx.push(mk_atom_trail(lit.var(), *this));
if (arg_sz > 1) {
bit_atom* a = new (get_region()) bit_atom();
a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
insert_bv2a(lit.var(), a);
ctx.push(mk_atom_trail(lit.var(), *this));
}
}
else if (lit != lit0) {
add_clause(lit0, ~lit);
@ -581,24 +631,60 @@ namespace bv {
void solver::eq_internalized(euf::enode* n) {
SASSERT(m.is_eq(n->get_expr()));
sat::literal lit = literal(n->bool_var(), false);
theory_var v1 = n->get_arg(0)->get_th_var(get_id());
theory_var v2 = n->get_arg(1)->get_th_var(get_id());
SASSERT(v1 != euf::null_theory_var);
SASSERT(v2 != euf::null_theory_var);
#if 0
if (!n->is_attached_to(get_id()))
mk_var(n);
#endif
unsigned sz = m_bits[v1].size();
if (sz == 1) {
literal bit1 = m_bits[v1][0];
literal bit2 = m_bits[v2][0];
add_clause(~lit, ~bit1, bit2);
add_clause(~lit, ~bit2, bit1);
add_clause(~bit1, ~bit2, lit);
add_clause(bit2, bit1, lit);
return;
}
for (unsigned i = 0; i < sz; ++i) {
eq_internalized(m_bits[v1][i].var(), i, v1, v2, n);
eq_internalized(m_bits[v2][i].var(), i, v2, v1, n);
literal bit1 = m_bits[v1][i];
literal bit2 = m_bits[v2][i];
lbool val1 = s().value(bit1);
lbool val2 = s().value(bit2);
if (val1 != l_undef)
eq_internalized(bit2.var(), bit1.var(), i, v2, v1, lit, n);
else if (val2 != l_undef)
eq_internalized(bit1.var(), bit2.var(), i, v1, v2, lit, n);
else if ((s().rand()() % 2) == 0)
eq_internalized(bit2.var(), bit1.var(), i, v2, v1, lit, n);
else
eq_internalized(bit1.var(), bit2.var(), i, v1, v2, lit, n);
}
}
void solver::eq_internalized(sat::bool_var b, unsigned idx, theory_var v1, theory_var v2, euf::enode* n) {
bit_atom* a = mk_bit_atom(b);
void solver::eq_internalized(sat::bool_var b1, sat::bool_var b2, unsigned idx, theory_var v1, theory_var v2, literal lit, euf::enode* n) {
bit_atom* a = mk_bit_atom(b1);
// eq_atom* b = mk_eq_atom(lit.var());
if (a) {
if (!a->is_fresh())
ctx.push(add_eq_occurs_trail(a));
a->m_eqs = new (get_region()) eq_occurs(idx, v1, v2, expr2literal(n->get_expr()), n, a->m_eqs);
}
ctx.push(add_eq_occurs_trail(a));
auto* next = a->m_eqs;
a->m_eqs = new (get_region()) eq_occurs(b1, b2, idx, v1, v2, lit, n, next);
if (next)
next->m_prev = a->m_eqs;
#if 0
if (b) {
b->m_eqs.push_back(std::make_pair(a, a->m_eqs));
ctx.push(push_back_vector<euf::solver, svector<std::pair<bit_atom*,eq_occurs*>>>(b->m_eqs));
}
#endif
}
}
void solver::assert_ackerman(theory_var v1, theory_var v2) {

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

@ -77,7 +77,7 @@ namespace bv {
else if (var2enode(v1)->get_root() != var2enode(v2)->get_root()) {
SASSERT(get_bv_size(v1) == get_bv_size(v2));
TRACE("bv", tout << "detected equality: v" << v1 << " = v" << v2 << "\n" << pp(v1) << pp(v2););
m_stats.m_num_th2core_eq++;
m_stats.m_num_bit2eq++;
add_fixed_eq(v1, v2);
ctx.propagate(var2enode(v1), var2enode(v2), mk_bit2eq_justification(v1, v2));
}
@ -146,9 +146,6 @@ namespace bv {
\brief v1[idx] = ~v2[idx], then v1 /= v2 is a theory axiom.
*/
void solver::mk_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx) {
if (!get_config().m_bv_eq_axioms)
return;
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++;
@ -194,8 +191,10 @@ namespace bv {
void solver::new_eq_eh(euf::th_eq const& eq) {
force_push();
TRACE("bv", tout << "new eq " << mk_bounded_pp(var2expr(eq.v1()), m) << " == " << mk_bounded_pp(var2expr(eq.v2()), m) << "\n";);
if (is_bv(eq.v1()))
if (is_bv(eq.v1())) {
m_find.merge(eq.v1(), eq.v2());
VERIFY(eq.is_eq());
}
}
void solver::new_diseq_eh(euf::th_eq const& ne) {
@ -207,6 +206,8 @@ namespace bv {
TRACE("bv", tout << "diff: " << v1 << " != " << v2 << " @" << s().scope_lvl() << "\n";);
unsigned sz = m_bits[v1].size();
if (sz == 1)
return;
unsigned num_undef = 0;
int undef_idx = 0;
for (unsigned i = 0; i < sz; ++i) {
@ -245,7 +246,7 @@ namespace bv {
SASSERT(s().value(b) != l_undef);
if (s().value(b) == l_true)
consequent.neg();
++m_stats.m_num_nbit2core;
++m_stats.m_num_ne2bit;
s().assign(consequent, mk_ne2bit_justification(undef_idx, v1, v2, consequent, antecedent));
}
else if (s().at_search_lvl()) {
@ -387,6 +388,11 @@ namespace bv {
force_push();
m_prop_queue.push_back(propagation_item(&a->to_bit()));
}
else if (a && a->is_eq()) {
for (auto p : a->to_eq().m_eqs) {
del_eq_occurs(p.first, p.second);
}
}
}
bool solver::unit_propagate() {
@ -397,10 +403,21 @@ namespace bv {
for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head) {
auto const p = m_prop_queue[m_prop_queue_head];
if (p.m_atom) {
for (auto vp : *p.m_atom)
propagate_bits(vp);
for (auto const& eq : p.m_atom->eqs())
propagate_eq_occurs(eq);
unsigned num_atoms = 0, num_eqs = 0, num_assigned = 0, num_eq_assigned = 0, num_lit_assigned = 0;
for (auto vp : *p.m_atom) {
if (propagate_bits(vp))
++num_assigned;
++num_atoms;
}
for (auto const& eq : p.m_atom->eqs()) {
++num_eqs;
if (s().value(eq.m_literal) != l_undef)
++num_lit_assigned;
if (propagate_eq_occurs(eq)) {
++num_eq_assigned;
}
}
IF_VERBOSE(20, verbose_stream() << "atoms: " << num_atoms << " eqs: " << num_eqs << " atoms-assigned:" << num_assigned << " eqs-assigned: " << num_eq_assigned << " lits: " << num_lit_assigned << "\n");
}
else
propagate_bits(p.m_vp);
@ -409,20 +426,35 @@ namespace bv {
return true;
}
void solver::propagate_eq_occurs(eq_occurs const& occ) {
bool solver::propagate_eq_occurs(eq_occurs const& occ) {
auto lit = occ.m_literal;
if (s().value(lit) != l_undef)
return;
lbool val1 = s().value(m_bits[occ.m_v1][occ.m_idx]);
lbool val2 = s().value(m_bits[occ.m_v2][occ.m_idx]);
if (s().value(lit) != l_undef) {
IF_VERBOSE(20, verbose_stream() << "assigned " << lit << " " << s().value(lit) << "\n");
return false;
}
literal bit1 = m_bits[occ.m_v1][occ.m_idx];
literal bit2 = m_bits[occ.m_v2][occ.m_idx];
lbool val2 = s().value(bit2);
if (val2 == l_undef) {
IF_VERBOSE(20, verbose_stream() << "add " << occ.m_bv2 << " " << occ.m_v2 << "\n");
eq_internalized(occ.m_bv2, occ.m_bv1, occ.m_idx, occ.m_v2, occ.m_v1, occ.m_literal, occ.m_node);
return false;
}
lbool val1 = s().value(bit1);
SASSERT(val1 != l_undef);
if (val1 != val2 && val2 != l_undef) {
++m_stats.m_num_th2core_diseq;
++m_stats.m_num_bit2ne;
IF_VERBOSE(20, verbose_stream() << "assign " << ~lit << "\n");
s().assign(~lit, mk_bit2ne_justification(occ.m_idx, ~lit));
return true;
}
IF_VERBOSE(20, verbose_stream() << "eq " << lit << "\n");
return false;
}
void solver::propagate_bits(var_pos entry) {
bool solver::propagate_bits(var_pos entry) {
theory_var v1 = entry.first;
unsigned idx = entry.second;
SASSERT(idx < m_bits[v1].size());
@ -433,7 +465,7 @@ namespace bv {
lbool val = s().value(bit1);
TRACE("bv", tout << "propagating v" << v1 << " #" << var2enode(v1)->get_expr_id() << "[" << idx << "] = " << val << "\n";);
if (val == l_undef)
return;
return false;
if (val == l_false)
bit1.neg();
@ -447,7 +479,7 @@ namespace bv {
if (val == l_false)
bit2.neg();
++num_bits;
if (num_bits > 4 && num_assigned == 0)
if (num_bits > 3 && num_assigned == 0)
break;
if (s().value(bit2) == l_true)
continue;
@ -455,7 +487,7 @@ namespace bv {
if (!assign_bit(bit2, v1, v2, idx, bit1, false))
break;
}
// std::cout << num_bits << " " << num_assigned << "\n";
return num_assigned > 0;
}
sat::check_result solver::check() {
@ -590,10 +622,10 @@ namespace bv {
st.update("bv conflicts", m_stats.m_num_conflicts);
st.update("bv diseqs", m_stats.m_num_diseq_static);
st.update("bv dynamic diseqs", m_stats.m_num_diseq_dynamic);
st.update("bv eq2bit", m_stats.m_num_bit2core);
st.update("bv ne2bit", m_stats.m_num_nbit2core);
st.update("bv bit2eq", m_stats.m_num_th2core_eq);
st.update("bv bit2ne", m_stats.m_num_th2core_diseq);
st.update("bv eq2bit", m_stats.m_num_eq2bit);
st.update("bv ne2bit", m_stats.m_num_ne2bit);
st.update("bv bit2eq", m_stats.m_num_bit2eq);
st.update("bv bit2ne", m_stats.m_num_bit2ne);
st.update("bv ackerman", m_stats.m_ackerman);
}
@ -625,6 +657,12 @@ namespace bv {
m_bool_var2atom.setx(i, new_a, nullptr);
for (auto vp : a->to_bit())
new_a->m_occs = new (result->get_region()) var_pos_occ(vp.first, vp.second, new_a->m_occs);
for (auto const& occ : a->to_bit().eqs()) {
expr* e = occ.m_node->get_expr();
expr_ref e2(tr(e), tr.to());
euf::enode* n = ctx.get_enode(e2);
new_a->m_eqs = new (result->get_region()) eq_occurs(occ.m_bv1, occ.m_bv2, occ.m_idx, occ.m_v1, occ.m_v2, occ.m_literal, n, new_a->m_eqs);
}
}
else {
def_atom* new_a = new (result->get_region()) def_atom(a->to_def().m_var, a->to_def().m_def);
@ -669,6 +707,7 @@ namespace bv {
}
void solver::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {
TRACE("bv", tout << "merging: v" << v1 << " #" << var2enode(v1)->get_expr_id() << " v" << v2 << " #" << var2enode(v2)->get_expr_id() << "\n";);
if (!merge_zero_one_bits(r1, r2)) {
TRACE("bv", tout << "conflict detected\n";);
@ -676,10 +715,16 @@ namespace bv {
}
SASSERT(m_bits[v1].size() == m_bits[v2].size());
unsigned sz = m_bits[v1].size();
if (sz == 1)
return;
for (unsigned idx = 0; !s().inconsistent() && idx < sz; idx++) {
literal bit1 = m_bits[v1][idx];
literal bit2 = m_bits[v2][idx];
CTRACE("bv", bit1 == ~bit2, tout << pp(v1) << pp(v2) << "idx: " << idx << "\n";);
if (bit1 == ~bit2) {
mk_new_diseq_axiom(v1, v2, idx);
return;
}
SASSERT(bit1 != ~bit2);
lbool val1 = s().value(bit1);
lbool val2 = s().value(bit2);
@ -729,7 +774,7 @@ namespace bv {
bool solver::assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc) {
m_stats.m_num_bit2core++;
m_stats.m_num_eq2bit++;
SASSERT(ctx.s().value(antecedent) == l_true);
SASSERT(m_bits[v2][idx].var() == consequent.var());
SASSERT(consequent.var() != antecedent.var());
@ -740,14 +785,6 @@ namespace bv {
return false;
}
else {
if (false && get_config().m_bv_eq_axioms) {
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);
add_clause(antecedent, ~eq_lit, ~consequent);
}
if (m_wpos[v2] == idx)
find_wpos(v2);
bool_var cv = consequent.var();

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

@ -44,7 +44,7 @@ namespace bv {
struct stats {
unsigned m_num_diseq_static, m_num_diseq_dynamic, m_num_conflicts;
unsigned m_num_bit2core, m_num_th2core_eq, m_num_th2core_diseq, m_num_nbit2core;
unsigned m_num_bit2eq, m_num_bit2ne, m_num_eq2bit, m_num_ne2bit;
unsigned m_ackerman;
void reset() { memset(this, 0, sizeof(stats)); }
stats() { reset(); }
@ -106,14 +106,53 @@ namespace bv {
typedef svector<zero_one_bit> zero_one_bits;
struct eq_occurs {
sat::bool_var m_bv1;
sat::bool_var m_bv2;
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* m_prev;
eq_occurs(sat::bool_var b1, sat::bool_var b2, unsigned idx, theory_var v1, theory_var v2, sat::literal lit, euf::enode* n, eq_occurs* next = nullptr) :
m_bv1(b1), m_bv2(b2), m_idx(idx), m_v1(v1), m_v2(v2), m_literal(lit), m_node(n), m_next(next), m_prev(nullptr) {}
};
class eq_occurs_it {
eq_occurs* m_first;
public:
eq_occurs_it(eq_occurs* c) : m_first(c) {}
eq_occurs operator*() { return *m_first; }
eq_occurs_it& operator++() { m_first = m_first->m_next; return *this; }
eq_occurs_it operator++(int) { eq_occurs_it tmp = *this; ++* this; return tmp; }
bool operator==(eq_occurs_it const& other) const { return m_first == other.m_first; }
bool operator!=(eq_occurs_it const& other) const { return !(*this == other); }
};
class eqs_iterator {
eq_occurs* o;
public:
eqs_iterator(eq_occurs* o) :o(o) {}
eq_occurs_it begin() const { return eq_occurs_it(o); }
eq_occurs_it end() const { return eq_occurs_it(nullptr); }
};
struct bit_atom;
struct def_atom;
struct eq_atom;
class atom {
public:
atom() {}
virtual ~atom() {}
virtual bool is_bit() const = 0;
virtual bool is_bit() const { return false; }
virtual bool is_eq() const { return false; }
bit_atom& to_bit();
def_atom& to_def();
eq_atom& to_eq();
};
struct var_pos_occ {
@ -133,47 +172,24 @@ namespace bv {
bool operator!=(var_pos_it const& other) const { return !(*this == other); }
};
struct eq_occurs {
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, 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 {
eq_occurs* m_first;
public:
eq_occurs_it(eq_occurs* c) : m_first(c) {}
eq_occurs operator*() { return *m_first; }
eq_occurs_it& operator++() { m_first = m_first->m_next; return *this; }
eq_occurs_it operator++(int) { eq_occurs_it tmp = *this; ++* this; return tmp; }
bool operator==(eq_occurs_it const& other) const { return m_first == other.m_first; }
bool operator!=(eq_occurs_it const& other) const { return !(*this == other); }
};
struct bit_atom : public atom {
eq_occurs* m_eqs;
var_pos_occ * m_occs;
eq_occurs * m_eqs;
bit_atom():m_occs(nullptr), m_eqs(nullptr) {}
bit_atom() :m_eqs(nullptr), m_occs(nullptr) {}
~bit_atom() override {}
bool is_bit() const override { return true; }
var_pos_it begin() const { return var_pos_it(m_occs); }
var_pos_it end() const { return var_pos_it(nullptr); }
bool is_fresh() const { return !m_occs && !m_eqs; }
class eqs_iterator {
bit_atom const& a;
public:
eqs_iterator(bit_atom const& a):a(a) {}
eq_occurs_it begin() const { return eq_occurs_it(a.m_eqs); }
eq_occurs_it end() const { return eq_occurs_it(nullptr); }
};
eqs_iterator eqs() const { return eqs_iterator(m_eqs); }
};
eqs_iterator eqs() const { return eqs_iterator(*this); }
struct eq_atom : public atom {
eq_atom(){}
~eq_atom() override { m_eqs.clear(); }
bool is_bit() const override { return false; }
bool is_eq() const override { return true; }
svector<std::pair<bit_atom*,eq_occurs*>> m_eqs;
};
struct def_atom : public atom {
@ -181,7 +197,6 @@ namespace bv {
literal m_def;
def_atom(literal v, literal d):m_var(v), m_def(d) {}
~def_atom() override {}
bool is_bit() const override { return false; }
};
struct propagation_item {
@ -195,6 +210,7 @@ namespace bv {
class bit_trail;
class add_var_pos_trail;
class add_eq_occurs_trail;
class del_eq_occurs_trail;
class mk_atom_trail;
class bit_occs_trail;
typedef ptr_vector<atom> bool_var2atom;
@ -242,8 +258,10 @@ namespace bv {
sat::status status() const { return sat::status::th(m_is_redundant, get_id()); }
void register_true_false_bit(theory_var v, unsigned i);
void add_bit(theory_var v, sat::literal lit);
bit_atom* mk_bit_atom(sat::bool_var bv);
void eq_internalized(sat::bool_var b, unsigned idx, theory_var v1, theory_var v2, euf::enode* n);
bit_atom* mk_bit_atom(sat::bool_var b);
eq_atom* mk_eq_atom(sat::bool_var b);
void eq_internalized(sat::bool_var b1, sat::bool_var b2, unsigned idx, theory_var v1, theory_var v2, sat::literal eq, euf::enode* n);
void del_eq_occurs(bit_atom* a, eq_occurs* occ);
void set_bit_eh(theory_var v, literal l, unsigned idx);
void init_bits(expr* e, expr_ref_vector const & bits);
@ -280,8 +298,8 @@ namespace bv {
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);
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);
bool propagate_bits(var_pos entry);
bool propagate_eq_occurs(eq_occurs const& occ);
numeral const& power2(unsigned i) const;
// invariants
@ -348,7 +366,7 @@ namespace bv {
void unmerge_eh(theory_var v1, theory_var v2);
trail_stack<euf::solver>& get_trail_stack();
// disagnostics
// diagnostics
std::ostream& display(std::ostream& out, theory_var v) const;
typedef std::pair<solver const*, theory_var> pp_var;
pp_var pp(theory_var v) const { return pp_var(this, v); }

9
src/sat/smt/euf_ackerman.cpp
View file

@ -74,8 +74,13 @@ namespace euf {
new_tmp();
}
other->m_count++;
if (other->m_count > m_high_watermark)
s.s().set_should_simplify();
if (other->m_count > m_high_watermark) {
if (other->is_cc)
add_cc(other->a, other->b);
else
add_eq(other->a, other->b, other->c);
other->m_count = 0;
}
inference::push_to_front(m_queue, other);
}

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

@ -31,6 +31,14 @@ namespace euf {
}
sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
euf::enode* n = m_egraph.find(e);
if (n) {
if (m.is_bool(e)) {
VERIFY(!s().was_eliminated(n->bool_var()));
return literal(n->bool_var(), sign);
}
return sat::null_literal;
}
if (si.is_bool_op(e))
return attach_lit(si.internalize(e, redundant), e);
if (auto* ext = expr2solver(e))
@ -117,9 +125,13 @@ namespace euf {
s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id()));
lit = lit2;
}
m_var2expr.reserve(v + 1, nullptr);
if (m_var2expr[v])
if (m_var2expr[v]) {
SASSERT(m_egraph.find(e));
SASSERT(m_egraph.find(e)->bool_var() == v);
return lit;
}
m_var2expr[v] = e;
m_var_trail.push_back(v);
enode* n = m_egraph.find(e);

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

@ -227,7 +227,7 @@ namespace euf {
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) {
if (!sign && n->is_equality()) {
SASSERT(!m.is_iff(e));
euf::enode* na = n->get_arg(0);
euf::enode* nb = n->get_arg(1);
@ -237,9 +237,8 @@ namespace euf {
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);
}
else if (sign && n->is_equality())
m_egraph.new_diseq(n);
}
@ -462,20 +461,23 @@ namespace euf {
}
bool solver::set_root(literal l, literal r) {
expr* e = bool_var2expr(l.var());
if (!e)
return true;
bool ok = true;
for (auto* s : m_solvers)
if (!s->set_root(l, r))
ok = false;
expr* e = bool_var2expr(l.var());
if (e) {
if (m.is_eq(e) && !m.is_iff(e))
ok = false;
euf::enode* n = get_enode(e);
if (n && n->merge_enabled())
ok = false;
}
if (m.is_eq(e) && !m.is_iff(e))
ok = false;
euf::enode* n = get_enode(e);
if (n && n->merge_enabled())
ok = false;
(void)ok;
TRACE("euf", tout << ok << " " << l << " -> " << r << "\n";);
return ok;
// roots cannot be eliminated as long as the egraph contains the expressions.
return false;
}
void solver::flush_roots() {

1
src/sat/smt/sat_th.h
View file

@ -157,6 +157,7 @@ namespace euf {
enode* var2enode(theory_var v) const { return m_var2enode[v]; }
expr* var2expr(theory_var v) const { return var2enode(v)->get_expr(); }
expr* bool_var2expr(sat::bool_var v) const;
enode* bool_var2enode(sat::bool_var v) const { expr* e = bool_var2expr(v); return e ? expr2enode(e) : nullptr; }
expr_ref literal2expr(sat::literal lit) const { expr* e = bool_var2expr(lit.var()); return lit.sign() ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); }
theory_var get_th_var(enode* n) const { return n->get_th_var(get_id()); }
theory_var get_th_var(expr* e) const;

9
src/smt/theory_arith_int.h
View file

@ -219,6 +219,7 @@ namespace smt {
{
std::function<expr*(void)> fn = [&]() { return m.mk_or(bound, m.mk_not(bound)); };
scoped_trace_stream _sts(*this, fn);
IF_VERBOSE(10, verbose_stream() << "branch " << bound << "\n");
TRACE("arith_int", tout << mk_bounded_pp(bound, m) << "\n";);
ctx.internalize(bound, true);
ctx.mark_as_relevant(bound.get());
@ -296,7 +297,7 @@ namespace smt {
continue;
}
if (!is_int(x)) {
TRACE("theory_arith_int", display_row(tout << "!int: ", r, true); );
TRACE("arith_int", display_row(tout << "!int: ", r, true); );
is_tight = false;
continue;
}
@ -324,7 +325,7 @@ namespace smt {
row[i] *= denom.to_rational();
}
}
TRACE("theory_arith_int",
TRACE("arith_int",
tout << "extracted row:\n";
for (unsigned i = 0; i < max_row; ++i) {
tout << row[i] << " ";
@ -365,7 +366,7 @@ namespace smt {
}
}
if (pol.empty()) {
TRACE("theory_arith_int", tout << "The witness is trivial\n";);
TRACE("arith_int", tout << "The witness is trivial\n";);
return false;
}
expr_ref p1(get_manager()), p2(get_manager());
@ -419,6 +420,7 @@ namespace smt {
scoped_trace_stream _sts(*this, fn);
ctx.internalize(bound, true);
}
IF_VERBOSE(10, verbose_stream() << "free " << bound << "\n");
ctx.mark_as_relevant(bound.get());
result = true;
}
@ -672,6 +674,7 @@ namespace smt {
ctx.internalize(bound, true);
}
l = ctx.get_literal(bound);
IF_VERBOSE(10, verbose_stream() << "cut " << bound << "\n");
ctx.mark_as_relevant(l);
dump_lemmas(l, ante);
auto js = ctx.mk_justification(

4
src/util/heap.h
View file

@ -158,6 +158,10 @@ public:
return m_value2indices.size();
}
unsigned size() const {
return m_value2indices.size();
}
void reserve(int s) {
CASSERT("heap", check_invariant());
if (s > static_cast<int>(m_value2indices.size()))