Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

additional bit-vector propagators #4695

Merged
merged 1 commit into from
Sep 18, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 13 additions & 13 deletions src/ast/euf/euf_egraph.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -573,30 +573,30 @@ namespace euf {

std::ostream& egraph::display(std::ostream& out, unsigned max_args, enode* n) const {
out << n->get_expr_id() << " := ";
if (!n->is_root())
out << "[" << n->get_root()->get_expr_id() << "] ";
expr* f = n->get_expr();
if (is_app(f))
out << mk_bounded_pp(f, m, 1);
out << mk_bounded_pp(f, m, 1) << " ";
else if (is_quantifier(f))
out << "q:" << f->get_id();
out << "q:" << f->get_id() << " ";
else
out << "v:" << f->get_id();
out << "\n";
out << "v:" << f->get_id() << " ";
if (!n->is_root())
out << "[r " << n->get_root()->get_expr_id() << "] ";
if (!n->m_parents.empty()) {
out << " parents ";
out << "[p";
for (enode* p : enode_parents(n))
out << p->get_expr_id() << " ";
out << "\n";
out << " " << p->get_expr_id();
out << "] ";
}
if (n->has_th_vars()) {
out << " theories ";
out << "[t";
for (auto v : enode_th_vars(n))
out << v.get_id() << ":" << v.get_var() << " ";
out << "\n";
out << " " << v.get_id() << ":" << v.get_var();
out << "] ";
}
if (n->m_target && m_display_justification)
n->m_justification.display(out << " = " << n->m_target->get_expr_id() << " j: ", m_display_justification) << "\n";
n->m_justification.display(out << "[j " << n->m_target->get_expr_id() << " ", m_display_justification) << "] ";
out << "\n";
return out;
}

Expand Down
1 change: 1 addition & 0 deletions src/sat/sat_probing.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -237,6 +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);
report rpt(*this);
bool r = true;
m_counter = 0;
Expand Down
3 changes: 2 additions & 1 deletion src/sat/sat_probing.h
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ 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

Expand Down Expand Up @@ -78,6 +78,7 @@ 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
Expand Down
21 changes: 16 additions & 5 deletions src/sat/sat_solver.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1934,12 +1934,24 @@ namespace sat {
}
log_stats();
m_simplifications++;
IF_VERBOSE(2, verbose_stream() << "(sat.simplify :simplifications " << m_simplifications << ")\n";);

TRACE("sat", tout << "simplify\n";);

pop(scope_lvl());

struct report {
solver& s;
stopwatch m_watch;
report(solver& s):s(s) {
m_watch.start();
s.log_stats();
IF_VERBOSE(2, verbose_stream() << "(sat.simplify :simplifications " << s.m_simplifications << ")\n";);
}
~report() {
m_watch.stop();
s.log_stats();
}
};
report _rprt(*this);
SASSERT(at_base_lvl());

m_cleaner(m_config.m_force_cleanup);
Expand Down Expand Up @@ -3943,9 +3955,8 @@ namespace sat {
break;
}
case justification::EXT_JUSTIFICATION:
if (m_ext) {
m_ext->display_justification(out << " ", js.get_ext_justification_idx());
}
if (m_ext)
m_ext->display_justification(out, js.get_ext_justification_idx());
break;
default:
break;
Expand Down
1 change: 1 addition & 0 deletions src/sat/sat_solver.h
Original file line number Diff line number Diff line change
Expand Up @@ -662,6 +662,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(); }

public:
void user_push() override;
Expand Down
2 changes: 1 addition & 1 deletion src/sat/smt/bv_ackerman.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,7 @@ namespace bv {
}

if (glue < max_glue)
v.m_glue = 2*glue <= sz ? 0 : glue;
v.m_glue = (sz > 6 && 2*glue <= sz) ? 0 : glue;
}

void ackerman::remove(vv* p) {
Expand Down
72 changes: 50 additions & 22 deletions src/sat/smt/bv_internalize.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,16 @@ namespace bv {
}
};

class solver::add_eq_occurs_trail : public trail<euf::solver> {
solver::bit_atom* m_atom;
public:
add_eq_occurs_trail(solver::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;
}
};

class solver::mk_atom_trail : public trail<euf::solver> {
solver& th;
sat::bool_var m_var;
Expand Down Expand Up @@ -242,31 +252,30 @@ namespace bv {
}

solver::bit_atom* solver::mk_bit_atom(sat::bool_var bv) {
bit_atom* b = new (get_region()) bit_atom();
insert_bv2a(bv, b);
ctx.push(mk_atom_trail(bv, *this));
return b;
atom* a = get_bv2a(bv);
if (a)
return a->is_bit() ? &a->to_bit() : nullptr;
else {
bit_atom* b = new (get_region()) bit_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 {
atom* a = get_bv2a(l.var());
if (a && !a->is_bit())
;
else if (a) {
bit_atom* b = &a->to_bit();
find_new_diseq_axioms(*b, v, idx);
ctx.push(add_var_pos_trail(b));
bit_atom* b = mk_bit_atom(l.var());
if (b) {
if (b->m_occs)
find_new_diseq_axioms(*b, v, idx);
if (!b->is_fresh())
ctx.push(add_var_pos_trail(b));
b->m_occs = new (get_region()) var_pos_occ(v, idx, b->m_occs);
}
else {
bit_atom* b = mk_bit_atom(l.var());
SASSERT(!b->m_occs);
b->m_occs = new (get_region()) var_pos_occ(v, idx);
}
}
}

Expand Down Expand Up @@ -570,12 +579,34 @@ namespace bv {
}
}

void solver::eq_internalized(euf::enode* n) {
SASSERT(m.is_eq(n->get_expr()));
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);
unsigned sz = m_bits[v1].size();
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);
}
}

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

void solver::assert_ackerman(theory_var v1, theory_var v2) {
if (v1 == v2)
return;
if (v1 > v2)
std::swap(v1, v2);
flet<bool> _red(m_is_redundant, true);
flet<bool> _red(m_is_redundant, true);
++m_stats.m_ackerman;
expr* o1 = var2expr(v1);
expr* o2 = var2expr(v2);
Expand All @@ -584,6 +615,7 @@ namespace bv {
unsigned sz = m_bits[v1].size();
TRACE("bv", tout << "ackerman-eq: " << s().scope_lvl() << " " << oe << "\n";);
literal_vector eqs;
eqs.push_back(oeq);
for (unsigned i = 0; i < sz; ++i) {
literal l1 = m_bits[v1][i];
literal l2 = m_bits[v2][i];
Expand All @@ -592,14 +624,10 @@ namespace bv {
e2 = bv.mk_bit2bool(o2, i);
expr_ref e = mk_eq(e1, e2);
literal eq = ctx.internalize(e, false, false, m_is_redundant);
add_clause(l1, ~l2, ~eq);
add_clause(~l1, l2, ~eq);
add_clause(l1, l2, eq);
add_clause(~l1, ~l2, eq);
add_clause(eq, ~oeq);
eqs.push_back(~eq);
}
eqs.push_back(oeq);
TRACE("bv", for (auto l : eqs) tout << mk_bounded_pp(literal2expr(l), m) << " "; tout << "\n";);
s().add_clause(eqs.size(), eqs.c_ptr(), sat::status::th(m_is_redundant, get_id()));
}
}
22 changes: 22 additions & 0 deletions src/sat/smt/bv_invariant.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ Module Name:
--*/

#include "sat/smt/bv_solver.h"
#include "sat/smt/euf_solver.h"

namespace bv {

Expand All @@ -32,6 +33,27 @@ namespace bv {
}
}

void solver::check_missing_propagation() const {
for (euf::enode* n : ctx.get_egraph().nodes()) {
expr* e = n->get_expr(), *a = nullptr, *b = nullptr;
if (m.is_eq(e, a, b) && bv.is_bv(a) && s().value(expr2literal(e)) == l_undef) {
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);
unsigned sz = m_bits[v1].size();
for (unsigned i = 0; i < sz; ++i) {
lbool val1 = s().value(m_bits[v1][i]);
lbool val2 = s().value(m_bits[v2][i]);
if (val1 != l_undef && val2 != l_undef && val1 != val2) {
IF_VERBOSE(0, verbose_stream() << "missing " << mk_bounded_pp(e, m) << "\n");
break;
}
}
}
}
}

/**
\brief Check whether m_zero_one_bits is an accurate summary of the bits in the
equivalence class rooted by v.
Expand Down
Loading