mirror of
https://github.com/Z3Prover/z3
synced 2025-08-14 23:05:26 +00:00
updates to ac-plugin
fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop.
This commit is contained in:
Nikolaj Bjorner
parent
07613942da
commit
67695b4cd6
5 changed files with 263 additions and 195 deletions
|
|
@ -136,15 +136,13 @@ namespace euf {
|
|||
|
||||
// unit -> {}
|
||||
void ac_plugin::add_unit(enode* u) {
|
||||
m_units.push_back(u);
|
||||
mk_node(u);
|
||||
auto m_id = to_monomial(u, {});
|
||||
init_equation(eq(to_monomial(u), m_id, justification::axiom(get_id())));
|
||||
push_equation(u, nullptr);
|
||||
}
|
||||
|
||||
// zero x -> zero
|
||||
void ac_plugin::add_zero(enode* z) {
|
||||
mk_node(z)->is_zero = true;
|
||||
// zeros persist
|
||||
}
|
||||
|
||||
void ac_plugin::register_shared(enode* n) {
|
||||
|
|
@ -165,12 +163,16 @@ namespace euf {
|
|||
push_undo(is_register_shared);
|
||||
}
|
||||
|
||||
void ac_plugin::push_scope_eh() {
|
||||
push_undo(is_push_scope);
|
||||
}
|
||||
|
||||
void ac_plugin::undo() {
|
||||
auto k = m_undo.back();
|
||||
m_undo.pop_back();
|
||||
switch (k) {
|
||||
case is_add_eq: {
|
||||
m_active.pop_back();
|
||||
case is_queue_eq: {
|
||||
m_queued.pop_back();
|
||||
break;
|
||||
}
|
||||
case is_add_node: {
|
||||
|
|
@ -180,14 +182,15 @@ namespace euf {
|
|||
n->~node();
|
||||
break;
|
||||
}
|
||||
case is_add_monomial: {
|
||||
m_monomials.pop_back();
|
||||
case is_push_scope: {
|
||||
m_active.reset();
|
||||
m_passive.reset();
|
||||
m_units.reset();
|
||||
m_queue_head = 0;
|
||||
break;
|
||||
}
|
||||
case is_update_eq: {
|
||||
auto const& [idx, eq] = m_update_eq_trail.back();
|
||||
m_active[idx] = eq;
|
||||
m_update_eq_trail.pop_back();
|
||||
case is_add_monomial: {
|
||||
m_monomials.pop_back();
|
||||
break;
|
||||
}
|
||||
case is_add_shared_index: {
|
||||
|
|
@ -316,14 +319,24 @@ namespace euf {
|
|||
}
|
||||
|
||||
void ac_plugin::merge_eh(enode* l, enode* r) {
|
||||
if (l == r)
|
||||
return;
|
||||
push_equation(l, r);
|
||||
}
|
||||
|
||||
void ac_plugin::pop_equation(enode* l, enode* r) {
|
||||
m_fuel += m_fuel_inc;
|
||||
if (!r) {
|
||||
m_units.push_back(l);
|
||||
mk_node(l);
|
||||
auto m_id = to_monomial(l, {});
|
||||
init_equation(eq(to_monomial(l), m_id, justification::axiom(get_id())), true);
|
||||
}
|
||||
else {
|
||||
auto j = justification::equality(l, r);
|
||||
auto m1 = to_monomial(l);
|
||||
auto m2 = to_monomial(r);
|
||||
TRACE(plugin, tout << "merge: " << m_name << " " << g.bpp(l) << " == " << g.bpp(r) << " " << m_pp_ll(*this, monomial(m1)) << " == " << m_pp_ll(*this, monomial(m2)) << "\n");
|
||||
init_equation(eq(m1, m2, j));
|
||||
init_equation(eq(m1, m2, j), true);
|
||||
}
|
||||
}
|
||||
|
||||
void ac_plugin::diseq_eh(enode* eq) {
|
||||
|
|
@ -336,12 +349,35 @@ namespace euf {
|
|||
register_shared(b);
|
||||
}
|
||||
|
||||
bool ac_plugin::init_equation(eq const& e) {
|
||||
m_active.push_back(e);
|
||||
auto& eq = m_active.back();
|
||||
deduplicate(monomial(eq.l).m_nodes, monomial(eq.r).m_nodes);
|
||||
void ac_plugin::push_equation(enode* l, enode* r) {
|
||||
if (l == r)
|
||||
return;
|
||||
m_queued.push_back({ l, r });
|
||||
push_undo(is_queue_eq);
|
||||
}
|
||||
|
||||
if (orient_equation(eq)) {
|
||||
bool ac_plugin::init_equation(eq eq, bool is_active) {
|
||||
deduplicate(monomial(eq.l), monomial(eq.r));
|
||||
if (!orient_equation(eq))
|
||||
return false;
|
||||
|
||||
#if 0
|
||||
if (is_reducing(eq))
|
||||
is_active = true;
|
||||
#endif
|
||||
|
||||
is_active = true; // set to active because forward reduction is not implemented yet.
|
||||
// we will have to forward reduce a passive equation before it can be activated.
|
||||
// this means that we have to iterate over all overlaps of variables in equation with
|
||||
// reducing eqations. Otherwise, we will not have the invariant that reducing variables
|
||||
// are eliminated from all equations.
|
||||
|
||||
if (!is_active) {
|
||||
m_passive.push_back(eq);
|
||||
return true;
|
||||
}
|
||||
|
||||
m_active.push_back(eq);
|
||||
auto& ml = monomial(eq.l);
|
||||
auto& mr = monomial(eq.r);
|
||||
|
||||
|
|
@ -388,11 +424,7 @@ namespace euf {
|
|||
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
m_active.pop_back();
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
bool ac_plugin::orient_equation(eq& e) {
|
||||
auto& ml = monomial(e.l);
|
||||
|
|
@ -455,8 +487,14 @@ namespace euf {
|
|||
|
||||
uint64_t ac_plugin::filter(monomial_t& m) {
|
||||
auto& bloom = m.m_bloom;
|
||||
if (bloom.m_tick == m_tick)
|
||||
|
||||
if (bloom.m_tick == m_tick) {
|
||||
uint64_t f = 0;
|
||||
for (auto n : m)
|
||||
f |= (1ull << (n->id() % 64ull));
|
||||
SASSERT(f == bloom.m_filter);
|
||||
return bloom.m_filter;
|
||||
}
|
||||
bloom.m_filter = 0;
|
||||
for (auto n : m)
|
||||
bloom.m_filter |= (1ull << (n->id() % 64ull));
|
||||
|
|
@ -562,6 +600,10 @@ namespace euf {
|
|||
}
|
||||
|
||||
void ac_plugin::propagate() {
|
||||
while (m_queue_head < m_queued.size()) {
|
||||
auto [l, r] = m_queued[m_queue_head++];
|
||||
pop_equation(l, r);
|
||||
}
|
||||
while (true) {
|
||||
loop_start:
|
||||
if (m_fuel == 0)
|
||||
|
|
@ -583,7 +625,7 @@ namespace euf {
|
|||
goto loop_start;
|
||||
|
||||
auto& eq = m_active[eq_id];
|
||||
deduplicate(monomial(eq.l).m_nodes, monomial(eq.r).m_nodes);
|
||||
deduplicate(monomial(eq.l), monomial(eq.r));
|
||||
if (monomial(eq.l).size() == 0) {
|
||||
set_status(eq_id, eq_status::is_dead_eq);
|
||||
continue;
|
||||
|
|
@ -623,12 +665,20 @@ namespace euf {
|
|||
}
|
||||
|
||||
unsigned ac_plugin::pick_next_eq() {
|
||||
init_pick:
|
||||
while (!m_to_simplify_todo.empty()) {
|
||||
unsigned id = *m_to_simplify_todo.begin();
|
||||
if (id < m_active.size() && is_to_simplify(id))
|
||||
return id;
|
||||
m_to_simplify_todo.remove(id);
|
||||
}
|
||||
if (!m_passive.empty()) {
|
||||
auto eq = m_passive.back();
|
||||
verbose_stream() << "pick passive " << eq_pp_ll(*this, eq) << "\n";
|
||||
m_passive.pop_back();
|
||||
init_equation(eq, true);
|
||||
goto init_pick;
|
||||
}
|
||||
return UINT_MAX;
|
||||
}
|
||||
|
||||
|
|
@ -640,11 +690,7 @@ namespace euf {
|
|||
if (are_equal(monomial(eq.l), monomial(eq.r)))
|
||||
s = eq_status::is_dead_eq;
|
||||
|
||||
if (eq.status != s) {
|
||||
m_update_eq_trail.push_back({ id, eq });
|
||||
eq.status = s;
|
||||
push_undo(is_update_eq);
|
||||
}
|
||||
switch (s) {
|
||||
case eq_status::is_processed_eq:
|
||||
case eq_status::is_reducing_eq:
|
||||
|
|
@ -673,7 +719,7 @@ namespace euf {
|
|||
}
|
||||
|
||||
//
|
||||
// backward iterator allows simplification of eq
|
||||
// forward iterator allows simplification of eq
|
||||
// The rhs of eq is a super-set of lhs of other eq.
|
||||
//
|
||||
unsigned_vector const& ac_plugin::forward_iterator(unsigned eq_id) {
|
||||
|
|
@ -749,7 +795,7 @@ namespace euf {
|
|||
}
|
||||
|
||||
//
|
||||
// forward iterator simplifies other eqs where their rhs is a superset of lhs of eq
|
||||
// backward iterator simplifies other eqs where their rhs is a superset of lhs of eq
|
||||
//
|
||||
unsigned_vector const& ac_plugin::backward_iterator(unsigned eq_id) {
|
||||
auto& eq = m_active[eq_id];
|
||||
|
|
@ -843,10 +889,8 @@ namespace euf {
|
|||
reduce(m_src_r, j);
|
||||
auto new_r = to_monomial(m_src_r);
|
||||
index_new_r(dst_eq, monomial(m_active[dst_eq].r), monomial(new_r));
|
||||
m_update_eq_trail.push_back({ dst_eq, m_active[dst_eq] });
|
||||
m_active[dst_eq].r = new_r;
|
||||
m_active[dst_eq].j = j;
|
||||
push_undo(is_update_eq);
|
||||
m_src_r.reset();
|
||||
m_src_r.append(monomial(src.r).m_nodes);
|
||||
TRACE(plugin_verbose, tout << "rewritten to " << m_pp_ll(*this, monomial(new_r)) << "\n");
|
||||
|
|
@ -862,7 +906,7 @@ namespace euf {
|
|||
//
|
||||
// dst_ids, dst_count contain rhs of dst_eq
|
||||
//
|
||||
TRACE(plugin, tout << "backward simplify " << eq_pp_ll(*this, src) << " " << eq_pp_ll(*this, dst) << " can-be-subset: " << can_be_subset(monomial(src.l), monomial(dst.r)) << "\n");
|
||||
TRACE(plugin, tout << "forward simplify " << eq_pp_ll(*this, src) << " " << eq_pp_ll(*this, dst) << " can-be-subset: " << can_be_subset(monomial(src.l), monomial(dst.r)) << "\n");
|
||||
|
||||
if (forward_subsumes(src_eq, dst_eq)) {
|
||||
set_status(dst_eq, eq_status::is_dead_eq);
|
||||
|
|
@ -891,11 +935,9 @@ namespace euf {
|
|||
reduce(m, j);
|
||||
auto new_r = to_monomial(m);
|
||||
index_new_r(dst_eq, monomial(m_active[dst_eq].r), monomial(new_r));
|
||||
m_update_eq_trail.push_back({ dst_eq, m_active[dst_eq] });
|
||||
m_active[dst_eq].r = new_r;
|
||||
m_active[dst_eq].j = j;
|
||||
TRACE(plugin, tout << "rewritten to " << m_pp(*this, monomial(new_r)) << "\n");
|
||||
push_undo(is_update_eq);
|
||||
|
||||
return true;
|
||||
}
|
||||
|
|
@ -975,7 +1017,9 @@ namespace euf {
|
|||
SASSERT(!are_equal(m_active[src_eq], m_active[dst_eq]));
|
||||
return false;
|
||||
}
|
||||
return all_of(monomial(dst.r), [&](node* n) { unsigned id = n->id(); return m_src_r_counts[id] == m_dst_r_counts[id]; });
|
||||
bool r = all_of(monomial(dst.r), [&](node* n) { unsigned id = n->id(); return m_src_r_counts[id] == m_dst_r_counts[id]; });
|
||||
SASSERT(r || !are_equal(m_active[src_eq], m_active[dst_eq]));
|
||||
return r;
|
||||
}
|
||||
|
||||
// src_l_counts, src_r_counts are initialized for src.l, src.r
|
||||
|
|
@ -1079,8 +1123,7 @@ namespace euf {
|
|||
goto init_loop;
|
||||
}
|
||||
}
|
||||
}
|
||||
while (false);
|
||||
} while (false);
|
||||
VERIFY(sz >= m.size());
|
||||
return change;
|
||||
}
|
||||
|
|
@ -1177,7 +1220,7 @@ namespace euf {
|
|||
unsigned max_left_new = std::max(m_src_r.size(), m_dst_r.size());
|
||||
unsigned min_right_new = std::min(m_src_r.size(), m_dst_r.size());
|
||||
if (max_left_new <= max_left && min_right_new <= min_right)
|
||||
added_eq = init_equation(eq(to_monomial(m_src_r), to_monomial(m_dst_r), j));
|
||||
added_eq = init_equation(eq(to_monomial(m_src_r), to_monomial(m_dst_r), j), false);
|
||||
|
||||
CTRACE(plugin, added_eq,
|
||||
tout << "superpose: " << m_name << " " << eq_pp_ll(*this, src) << " " << eq_pp_ll(*this, dst) << " --> ";
|
||||
|
|
@ -1204,21 +1247,24 @@ namespace euf {
|
|||
}
|
||||
}
|
||||
|
||||
// TODO: this is destructive. It breaks reversibility.
|
||||
// TODO: also need justifications from eq if there is a change.
|
||||
void ac_plugin::backward_reduce(eq const& eq, unsigned other_eq_id) {
|
||||
auto& other_eq = m_active[other_eq_id];
|
||||
TRACE(plugin_verbose,
|
||||
tout << "backward reduce " << eq_pp_ll(*this, eq) << " " << eq_pp_ll(*this, other_eq) << "\n");
|
||||
bool change = false;
|
||||
if (backward_reduce_monomial(eq, monomial(other_eq.l)))
|
||||
if (backward_reduce_monomial(eq, other_eq, monomial(other_eq.l)))
|
||||
change = true;
|
||||
if (backward_reduce_monomial(eq, monomial(other_eq.r)))
|
||||
if (backward_reduce_monomial(eq, other_eq, monomial(other_eq.r)))
|
||||
change = true;
|
||||
if (change)
|
||||
CTRACE(plugin, change,
|
||||
tout << "backward reduce " << eq_pp_ll(*this, eq) << " " << eq_pp_ll(*this, other_eq) << "\n");
|
||||
if (change) {
|
||||
set_status(other_eq_id, eq_status::is_to_simplify_eq);
|
||||
}
|
||||
}
|
||||
|
||||
bool ac_plugin::backward_reduce_monomial(eq const& eq, monomial_t& m) {
|
||||
auto const& r = monomial(eq.r);
|
||||
bool ac_plugin::backward_reduce_monomial(eq const& src, eq& dst, monomial_t& m) {
|
||||
auto const& r = monomial(src.r);
|
||||
unsigned j = 0;
|
||||
bool change = false;
|
||||
for (auto n : m) {
|
||||
|
|
@ -1241,6 +1287,10 @@ namespace euf {
|
|||
m.m_nodes[j++] = r[0];
|
||||
}
|
||||
m.m_nodes.shrink(j);
|
||||
if (change) {
|
||||
m.m_bloom.m_tick = 0;
|
||||
dst.j = join(dst.j, src);
|
||||
}
|
||||
return change;
|
||||
}
|
||||
|
||||
|
|
@ -1277,8 +1327,17 @@ namespace euf {
|
|||
return true;
|
||||
}
|
||||
|
||||
|
||||
void ac_plugin::deduplicate(monomial_t& a, monomial_t& b) {
|
||||
unsigned sza = a.size(), szb = b.size();
|
||||
deduplicate(a.m_nodes, b.m_nodes);
|
||||
if (sza != a.size())
|
||||
a.m_bloom.m_tick = 0;
|
||||
if (szb != b.size())
|
||||
b.m_bloom.m_tick = 0;
|
||||
}
|
||||
|
||||
void ac_plugin::deduplicate(ptr_vector<node>& a, ptr_vector<node>& b) {
|
||||
{
|
||||
for (auto n : a) {
|
||||
if (n->is_zero) {
|
||||
a[0] = n;
|
||||
|
|
@ -1293,7 +1352,6 @@ namespace euf {
|
|||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if (!m_is_injective)
|
||||
return;
|
||||
|
|
@ -1385,9 +1443,7 @@ namespace euf {
|
|||
push_undo(is_update_shared);
|
||||
m_shared[idx].m = new_m;
|
||||
m_shared[idx].j = j;
|
||||
|
||||
TRACE(plugin_verbose, tout << "shared simplified to " << m_pp_ll(*this, monomial(new_m)) << "\n");
|
||||
|
||||
push_merge(old_n, new_n, j);
|
||||
}
|
||||
|
||||
|
|
@ -1397,19 +1453,15 @@ namespace euf {
|
|||
}
|
||||
|
||||
justification::dependency* ac_plugin::justify_equation(unsigned eq) {
|
||||
auto const& e = m_active[eq];
|
||||
auto* j = m_dep_manager.mk_leaf(e.j);
|
||||
j = justify_monomial(j, monomial(e.l));
|
||||
j = justify_monomial(j, monomial(e.r));
|
||||
return j;
|
||||
}
|
||||
|
||||
justification::dependency* ac_plugin::justify_monomial(justification::dependency* j, monomial_t const& m) {
|
||||
return j;
|
||||
return m_dep_manager.mk_leaf(m_active[eq].j);
|
||||
}
|
||||
|
||||
justification ac_plugin::join(justification j, unsigned eq) {
|
||||
return justification::dependent(m_dep_manager.mk_join(m_dep_manager.mk_leaf(j), justify_equation(eq)));
|
||||
}
|
||||
|
||||
justification ac_plugin::join(justification j, eq const& eq) {
|
||||
return justification::dependent(m_dep_manager.mk_join(m_dep_manager.mk_leaf(j), m_dep_manager.mk_leaf(eq.j)));
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -123,6 +123,7 @@ namespace euf {
|
|||
func_decl* m_decl = nullptr;
|
||||
bool m_is_injective = false;
|
||||
vector<eq> m_active, m_passive;
|
||||
enode_pair_vector m_queued;
|
||||
ptr_vector<node> m_nodes;
|
||||
bool_vector m_shared_nodes;
|
||||
vector<monomial_t> m_monomials;
|
||||
|
|
@ -146,21 +147,21 @@ namespace euf {
|
|||
|
||||
// backtrackable state
|
||||
enum undo_kind {
|
||||
is_add_eq,
|
||||
is_queue_eq,
|
||||
is_add_monomial,
|
||||
is_add_node,
|
||||
is_update_eq,
|
||||
is_add_shared_index,
|
||||
is_add_eq_index,
|
||||
is_register_shared,
|
||||
is_update_shared
|
||||
is_update_shared,
|
||||
is_push_scope
|
||||
};
|
||||
svector<undo_kind> m_undo;
|
||||
ptr_vector<node> m_node_trail;
|
||||
unsigned m_queue_head = 0;
|
||||
|
||||
svector<std::pair<unsigned, shared>> m_update_shared_trail;
|
||||
svector<std::tuple<node*, unsigned, unsigned>> m_merge_trail;
|
||||
svector<std::pair<unsigned, eq>> m_update_eq_trail;
|
||||
|
||||
|
||||
|
||||
|
|
@ -191,8 +192,8 @@ namespace euf {
|
|||
bool well_formed(eq const& e) const;
|
||||
bool is_reducing(eq const& e) const;
|
||||
void backward_reduce(unsigned eq_id);
|
||||
void backward_reduce(eq const& src, unsigned dst);
|
||||
bool backward_reduce_monomial(eq const& eq, monomial_t& m);
|
||||
void backward_reduce(eq const& eq, unsigned dst);
|
||||
bool backward_reduce_monomial(eq const& src, eq & dst, monomial_t& m);
|
||||
void forward_subsume_new_eqs();
|
||||
bool is_forward_subsumed(unsigned dst_eq);
|
||||
bool forward_subsumes(unsigned src_eq, unsigned dst_eq);
|
||||
|
|
@ -208,7 +209,9 @@ namespace euf {
|
|||
return nullptr;
|
||||
}
|
||||
|
||||
bool init_equation(eq const& e);
|
||||
bool init_equation(eq e, bool is_active);
|
||||
void push_equation(enode* l, enode* r);
|
||||
void pop_equation(enode* l, enode* r);
|
||||
bool orient_equation(eq& e);
|
||||
void set_status(unsigned eq_id, eq_status s);
|
||||
unsigned pick_next_eq();
|
||||
|
|
@ -217,6 +220,7 @@ namespace euf {
|
|||
void backward_simplify(unsigned eq_id, unsigned using_eq);
|
||||
bool forward_simplify(unsigned eq_id, unsigned using_eq);
|
||||
bool superpose(unsigned src_eq, unsigned dst_eq);
|
||||
void deduplicate(monomial_t& a, monomial_t& b);
|
||||
void deduplicate(ptr_vector<node>& a, ptr_vector<node>& b);
|
||||
|
||||
ptr_vector<node> m_src_r, m_src_l, m_dst_r, m_dst_l;
|
||||
|
|
@ -260,8 +264,8 @@ namespace euf {
|
|||
|
||||
justification justify_rewrite(unsigned eq1, unsigned eq2);
|
||||
justification::dependency* justify_equation(unsigned eq);
|
||||
justification::dependency* justify_monomial(justification::dependency* d, monomial_t const& m);
|
||||
justification join(justification j1, unsigned eq);
|
||||
justification join(justification j1, eq const& eq);
|
||||
|
||||
bool is_correct_ref_count(monomial_t const& m, ref_counts const& counts) const;
|
||||
bool is_correct_ref_count(ptr_vector<node> const& m, ref_counts const& counts) const;
|
||||
|
|
@ -301,6 +305,8 @@ namespace euf {
|
|||
|
||||
void undo() override;
|
||||
|
||||
void push_scope_eh() override;
|
||||
|
||||
void propagate() override;
|
||||
|
||||
std::ostream& display(std::ostream& out) const override;
|
||||
|
|
|
|||
|
|
@ -43,6 +43,11 @@ namespace euf {
|
|||
|
||||
void undo() override;
|
||||
|
||||
void push_scope_eh() override {
|
||||
m_add.push_scope_eh();
|
||||
m_mul.push_scope_eh();
|
||||
}
|
||||
|
||||
void propagate() override;
|
||||
|
||||
std::ostream& display(std::ostream& out) const override;
|
||||
|
|
|
|||
|
|
@ -103,6 +103,9 @@ namespace euf {
|
|||
m_scopes.push_back(m_updates.size());
|
||||
m_region.push_scope();
|
||||
m_updates.push_back(update_record(m_new_th_eqs_qhead, update_record::new_th_eq_qhead()));
|
||||
for (auto p : m_plugins)
|
||||
if (p)
|
||||
p->push_scope_eh();
|
||||
}
|
||||
SASSERT(m_new_th_eqs_qhead <= m_new_th_eqs.size());
|
||||
}
|
||||
|
|
|
|||
|
|
@ -53,6 +53,8 @@ namespace euf {
|
|||
|
||||
virtual void undo() = 0;
|
||||
|
||||
virtual void push_scope_eh() {}
|
||||
|
||||
virtual std::ostream& display(std::ostream& out) const = 0;
|
||||
|
||||
virtual void collect_statistics(statistics& st) const {}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue