mirror of
https://github.com/Z3Prover/z3
synced 2026-07-15 03:25:43 +00:00
Details in original PR: https://github.com/Z3Prover/z3/pull/10007 --------- --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: Can Cebeci <can.cebeci99@gmail.com> Co-authored-by: Can Cebeci <t-cancebeci@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
GitHub
parent
c56b2cbaa4
commit
3f6a57e8a8
12 changed files with 267 additions and 115 deletions
|
|
@ -215,7 +215,6 @@ namespace {
|
|||
unsigned short m_num_args;
|
||||
unsigned m_ireg;
|
||||
unsigned m_oreg;
|
||||
unsigned m_curr_max_generation = 0;
|
||||
};
|
||||
|
||||
struct get_cgr : public instruction {
|
||||
|
|
@ -1881,47 +1880,33 @@ namespace {
|
|||
m_pool.recycle(v);
|
||||
}
|
||||
|
||||
void update_max_generation(enode * n, enode * prev, enode * min_gen_match=nullptr) {
|
||||
unsigned new_gen = min_gen_match ? min_gen_match->get_generation() : n->get_generation();
|
||||
|
||||
m_max_generation = std::max(m_max_generation, new_gen);
|
||||
void update_max_generation(enode * n, enode * prev) {
|
||||
m_max_generation = std::max(m_max_generation, m_context.get_generation(n));
|
||||
|
||||
if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality))
|
||||
m_used_enodes.push_back(std::make_tuple(prev, n));
|
||||
}
|
||||
|
||||
void get_f_app(func_decl* lbl, unsigned num_expected_args, enode* curr, enode*& matching_cgr, enode*& min_gen_match) {
|
||||
if (curr->get_decl() == lbl && curr->get_num_args() == num_expected_args) {
|
||||
if (curr->is_cgr() && !matching_cgr)
|
||||
matching_cgr = curr;
|
||||
|
||||
if (!min_gen_match || min_gen_match->get_generation() > curr->get_generation()) {
|
||||
min_gen_match = curr;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// We have to provide the number of expected arguments because we have flat-assoc applications such as +.
|
||||
// Flat-assoc applications may have arbitrary number of arguments.
|
||||
enode * get_first_f_app(func_decl * lbl, unsigned num_expected_args, enode * curr) {
|
||||
enode * first = curr;
|
||||
enode *matching_cgr = nullptr, *min_gen_match = nullptr;
|
||||
do {
|
||||
get_f_app(lbl, num_expected_args, curr, matching_cgr, min_gen_match);
|
||||
if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
|
||||
update_max_generation(curr, first);
|
||||
return curr;
|
||||
}
|
||||
curr = curr->get_next();
|
||||
}
|
||||
while (curr != first);
|
||||
if (matching_cgr)
|
||||
update_max_generation(matching_cgr, first, min_gen_match);
|
||||
return matching_cgr;
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
enode * get_next_f_app(func_decl * lbl, unsigned num_expected_args, enode * first, enode * curr) {
|
||||
curr = curr->get_next();
|
||||
while (curr != first) {
|
||||
if (curr->get_decl() == lbl && curr->get_num_args() == num_expected_args && curr->is_cgr()) {
|
||||
if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality))
|
||||
m_used_enodes.push_back(std::make_tuple(first, curr));
|
||||
if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
|
||||
update_max_generation(curr, first);
|
||||
return curr;
|
||||
}
|
||||
curr = curr->get_next();
|
||||
|
|
@ -2065,7 +2050,7 @@ namespace {
|
|||
void get_min_max_top_generation(unsigned& min, unsigned& max) {
|
||||
SASSERT(!m_pattern_instances.empty());
|
||||
if (m_min_top_generation.empty()) {
|
||||
min = max = m_pattern_instances[0]->get_generation();
|
||||
min = max = m_context.get_generation(m_pattern_instances[0]);
|
||||
m_min_top_generation.push_back(min);
|
||||
m_max_top_generation.push_back(max);
|
||||
}
|
||||
|
|
@ -2074,7 +2059,7 @@ namespace {
|
|||
max = m_max_top_generation.back();
|
||||
}
|
||||
for (unsigned i = m_min_top_generation.size(); i < m_pattern_instances.size(); ++i) {
|
||||
unsigned curr = m_pattern_instances[i]->get_generation();
|
||||
unsigned curr = m_context.get_generation(m_pattern_instances[i]);
|
||||
min = std::min(min, curr);
|
||||
m_min_top_generation.push_back(min);
|
||||
max = std::max(max, curr);
|
||||
|
|
@ -2315,7 +2300,8 @@ namespace {
|
|||
m_min_top_generation.reset();
|
||||
m_max_top_generation.reset();
|
||||
m_pattern_instances.push_back(n);
|
||||
m_max_generation = n->get_generation();
|
||||
|
||||
m_max_generation = m_context.get_generation(n);
|
||||
|
||||
if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality)) {
|
||||
m_used_enodes.reset();
|
||||
|
|
@ -2492,7 +2478,6 @@ namespace {
|
|||
m_backtrack_stack[m_top].m_old_max_generation = m_curr_max_generation; \
|
||||
m_backtrack_stack[m_top].m_old_used_enodes_size = m_curr_used_enodes_size; \
|
||||
m_backtrack_stack[m_top].m_curr = m_app; \
|
||||
const_cast<bind*>(static_cast<const bind*>(m_pc))->m_curr_max_generation = m_max_generation; \
|
||||
m_top++;
|
||||
|
||||
BIND_COMMON();
|
||||
|
|
@ -2556,7 +2541,7 @@ namespace {
|
|||
case YIELD1:
|
||||
m_bindings[0] = m_registers[static_cast<const yield *>(m_pc)->m_bindings[0]];
|
||||
#define ON_MATCH(NUM) \
|
||||
m_max_generation = std::max(m_max_generation, get_max_generation(NUM, m_bindings.begin())); \
|
||||
m_max_generation = std::max(m_max_generation, m_context.get_max_generation(NUM, m_bindings.begin())); \
|
||||
if (m_context.get_cancel_flag()) { \
|
||||
return false; \
|
||||
} \
|
||||
|
|
@ -2760,7 +2745,6 @@ namespace {
|
|||
#define BBIND_COMMON() m_b = static_cast<const bind*>(bp.m_instr); \
|
||||
m_n1 = m_registers[m_b->m_ireg]; \
|
||||
m_app = get_next_f_app(m_b->m_label, m_b->m_num_args, m_n1, bp.m_curr); \
|
||||
m_max_generation = m_b->m_curr_max_generation; \
|
||||
if (!m_app) { \
|
||||
m_top--; \
|
||||
goto backtrack; \
|
||||
|
|
@ -3972,10 +3956,6 @@ namespace {
|
|||
}
|
||||
return;
|
||||
}
|
||||
DEBUG_CODE(
|
||||
for (unsigned i = 0; i < num_bindings; ++i) {
|
||||
SASSERT(bindings[i]->get_generation() <= max_generation);
|
||||
});
|
||||
|
||||
#endif
|
||||
unsigned min_gen = 0, max_gen = 0;
|
||||
|
|
|
|||
|
|
@ -1012,7 +1012,7 @@ namespace {
|
|||
stack.pop_back();
|
||||
|
||||
if (m_context.e_internalized(curr)) {
|
||||
gen = m_context.get_enode(curr)->get_generation();
|
||||
gen = m_context.get_generation(m_context.get_enode(curr));
|
||||
if (gen > maxgen)
|
||||
maxgen = gen;
|
||||
if (gen < mingen)
|
||||
|
|
@ -1046,7 +1046,7 @@ namespace {
|
|||
void operator()(expr * e) {
|
||||
if (m_context.e_internalized(e)) {
|
||||
enode * n = m_context.get_enode(e);
|
||||
n->set_generation(&m_context, m_generation);
|
||||
m_context.set_generation(n, m_generation);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
|
@ -1069,7 +1069,8 @@ namespace {
|
|||
stack.pop_back();
|
||||
|
||||
if (m_context.e_internalized(curr)) {
|
||||
unsigned curr_gen = m_context.get_enode(curr)->get_generation();
|
||||
enode * n = m_context.get_enode(curr);
|
||||
unsigned curr_gen = m_context.get_generation(n);
|
||||
if (curr_gen > gen) {
|
||||
// Lower it.
|
||||
set_generation_rec(e, gen);
|
||||
|
|
|
|||
|
|
@ -537,7 +537,8 @@ namespace smt {
|
|||
mark_as_relevant(r1);
|
||||
}
|
||||
|
||||
push_trail(add_eq_trail(*this, r1, n1, r2->get_num_parents()));
|
||||
|
||||
unsigned r2_num_parents = r2->get_num_parents();
|
||||
|
||||
m_qmanager->add_eq_eh(r1, r2);
|
||||
|
||||
|
|
@ -567,6 +568,10 @@ namespace smt {
|
|||
|
||||
SASSERT(r1->get_root() == r2);
|
||||
reinsert_parents_into_cg_table(r1, r2, n1, n2, js);
|
||||
|
||||
// We push the add_eq_trail after reinsert_parents_into_cg_table because the latter may push merge_cgc_generations trails,
|
||||
// and we want add_eq to be undone before merge_cgc_generations is undone.
|
||||
push_trail(add_eq_trail(*this, r1, n1, r2_num_parents));
|
||||
|
||||
if (n2->is_bool())
|
||||
propagate_bool_enode_assignment(r1, r2, n1, n2);
|
||||
|
|
@ -594,6 +599,8 @@ namespace smt {
|
|||
must be removed from the congruence table since their hash code will change.
|
||||
*/
|
||||
void context::remove_parents_from_cg_table(enode * r1) {
|
||||
SASSERT(m_r1_parent_generations.empty());
|
||||
|
||||
// Remove parents from the congruence table
|
||||
for (enode * parent : enode::parents(r1)) {
|
||||
CTRACE(add_eq, !parent->is_marked() && parent->is_cgc_enabled() && parent->is_true_eq() && m_cg_table.contains_ptr(parent), tout << parent->get_owner_id() << "\n";);
|
||||
|
|
@ -603,7 +610,8 @@ namespace smt {
|
|||
tout << "\n";
|
||||
tout << "contains: " << m_cg_table.contains(parent) << "\n";
|
||||
if (m_cg_table.contains(parent)) {
|
||||
tout << "owner: " << m_cg_table.find(parent)->get_owner_id() << "\n";
|
||||
enode* owner = m_cg_table.find(parent);
|
||||
tout << "owner: " << owner->get_owner_id() << "\n";
|
||||
}
|
||||
m_cg_table.display(tout);
|
||||
);
|
||||
|
|
@ -614,6 +622,8 @@ namespace smt {
|
|||
SASSERT(!parent->is_cgc_enabled() || m_cg_table.contains_ptr(parent));
|
||||
parent->set_mark();
|
||||
if (parent->is_cgc_enabled()) {
|
||||
if (!parent->is_eq()) // we don't track generations of equalities.
|
||||
m_r1_parent_generations.push_back(std::make_pair(parent, get_generation(parent)));
|
||||
m_cg_table.erase(parent);
|
||||
SASSERT(!m_cg_table.contains_ptr(parent));
|
||||
}
|
||||
|
|
@ -621,6 +631,20 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
// Sticky update to the generation number of the congruence class
|
||||
// Goes out of scope when n is garbage collected.
|
||||
void context::set_generation_sticky(enode * n, unsigned generation) {
|
||||
SASSERT(n->uses_cg_table());
|
||||
SASSERT(!n->is_eq());
|
||||
|
||||
// Callers are responsible for this. Sticky updates are too expensive to accommodate no-ops.
|
||||
SASSERT(generation < get_generation(n));
|
||||
|
||||
set_generation(n, generation);
|
||||
m_sticky_generation_updates.insert(n, generation);
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
\brief Reinsert the parents of r1 that were removed from the
|
||||
cg_table at remove_parents_from_cg_table. Some of these parents will
|
||||
|
|
@ -638,6 +662,7 @@ namespace smt {
|
|||
enode_vector & r2_parents = r2->m_parents;
|
||||
enode_vector & r1_parents = r1->m_parents;
|
||||
unsigned num_r1_parents = r1_parents.size();
|
||||
unsigned generation_cache_idx = 0;
|
||||
for (unsigned i = 0; i < num_r1_parents; ++i) {
|
||||
enode* parent = r1_parents[i];
|
||||
if (!parent->is_marked())
|
||||
|
|
@ -659,25 +684,39 @@ namespace smt {
|
|||
assign(literal(v), mk_justification(eq_propagation_justification(lhs, rhs)));
|
||||
}
|
||||
// It is not necessary to reinsert the equality to the congruence table
|
||||
// (because the only congruence propagations that could lead to are already handled by the assign() here).
|
||||
continue;
|
||||
}
|
||||
}
|
||||
if (parent->is_cgc_enabled()) {
|
||||
// Look up the generation cache
|
||||
unsigned parent_generation = 0; // Just use generation 0 for equalities
|
||||
if (!parent->is_eq()) {
|
||||
auto [p, g] = m_r1_parent_generations[generation_cache_idx++];
|
||||
SASSERT(p == parent);
|
||||
parent_generation = g;
|
||||
}
|
||||
|
||||
auto [parent_prime, used_commutativity] = m_cg_table.insert(parent);
|
||||
if (parent_prime == parent) {
|
||||
SASSERT(parent);
|
||||
SASSERT(parent->is_cgr());
|
||||
SASSERT(parent->is_cgr());
|
||||
SASSERT(m_cg_table.contains_ptr(parent));
|
||||
parent->m_generation = parent_generation;
|
||||
|
||||
r2_parents.push_back(parent);
|
||||
continue;
|
||||
}
|
||||
|
||||
parent->m_cg = parent_prime;
|
||||
SASSERT(!m_cg_table.contains_ptr(parent));
|
||||
merge_cgc_generations(parent, parent_generation, parent_prime);
|
||||
|
||||
if (parent_prime->m_root != parent->m_root) {
|
||||
TRACE(cg, tout << "found new congruence: #" << parent->get_owner_id() << " = #" << parent_prime->get_owner_id()
|
||||
<< " used_commutativity: " << used_commutativity << "\n";);
|
||||
push_new_congruence(parent, parent_prime, used_commutativity);
|
||||
}
|
||||
|
||||
}
|
||||
else {
|
||||
// If congruence closure is not enabled for parent, then I just copy it
|
||||
|
|
@ -685,6 +724,7 @@ namespace smt {
|
|||
r2_parents.push_back(parent);
|
||||
}
|
||||
}
|
||||
m_r1_parent_generations.reset();
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -940,6 +980,8 @@ namespace smt {
|
|||
// unmerge "equivalence" classes
|
||||
std::swap(r1->m_next, r2->m_next);
|
||||
|
||||
SASSERT(m_r1_parent_generations.empty());
|
||||
|
||||
// remove the parents of r1 that remained as congruence roots
|
||||
enode_vector::iterator it = r2->begin_parents();
|
||||
enode_vector::iterator end = r2->end_parents();
|
||||
|
|
@ -956,6 +998,8 @@ namespace smt {
|
|||
display(tout << "\n"););
|
||||
SASSERT(parent->is_cgr());
|
||||
SASSERT(m_cg_table.contains_ptr(parent));
|
||||
if (!parent->is_eq())
|
||||
m_r1_parent_generations.push_back(std::make_pair(parent, get_generation(parent)));
|
||||
m_cg_table.erase(parent);
|
||||
}
|
||||
}
|
||||
|
|
@ -970,22 +1014,52 @@ namespace smt {
|
|||
// restore parents of r2
|
||||
r2->m_parents.shrink(r2_num_parents);
|
||||
|
||||
unsigned generation_cache_idx = 0;
|
||||
|
||||
// try to reinsert parents of r1 that are not cgr
|
||||
for (enode * parent : enode::parents(r1)) {
|
||||
TRACE(add_eq_parents, tout << "visiting: #" << parent->get_owner_id() << "\n";);
|
||||
if (parent->is_cgc_enabled()) {
|
||||
|
||||
enode * cg = parent->m_cg;
|
||||
if (!parent->is_true_eq() &&
|
||||
(parent == cg || // parent was root of the congruence class before and after the merge
|
||||
!congruent(parent, cg) // parent was root of the congruence class before but not after the merge
|
||||
)) {
|
||||
(parent == cg || // parent was root of the congruence class before and after the merge
|
||||
!congruent(parent, cg)) // parent was root of the congruence class before but not after the merge
|
||||
) {
|
||||
|
||||
unsigned gen;
|
||||
if (parent->is_eq()) {
|
||||
gen = 0;
|
||||
} else if (parent == cg) {
|
||||
enode *p = nullptr;
|
||||
unsigned parent_generation;
|
||||
if (generation_cache_idx < m_r1_parent_generations.size()) {
|
||||
std::tie(p, parent_generation) = m_r1_parent_generations[generation_cache_idx];
|
||||
}
|
||||
if (p == parent) {
|
||||
generation_cache_idx++;
|
||||
gen = parent_generation;
|
||||
} else {
|
||||
SASSERT(m_cg_table.contains_ptr(parent));
|
||||
continue;
|
||||
}
|
||||
} else {
|
||||
// Insert at some dummy generation here. An undo_merge_cgr will immediately follow to set the generation.
|
||||
unsigned dummy_generation = 100000; // NOT UINT_MAX. In case this goes badly overflows would be hell to debug.
|
||||
gen = dummy_generation;
|
||||
}
|
||||
|
||||
auto [parent_cg, used_commutativity] = m_cg_table.insert(parent);
|
||||
(void)used_commutativity;
|
||||
parent->m_cg = parent_cg;
|
||||
if (parent_cg == parent)
|
||||
// parent is (again) the congruence root: restore its generation.
|
||||
parent->m_generation = gen;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
m_r1_parent_generations.reset();
|
||||
|
||||
// restore theory vars
|
||||
if (r2->m_th_var_list.get_next() == nullptr) {
|
||||
// common case: r2 has at most one variable
|
||||
|
|
@ -1020,6 +1094,28 @@ namespace smt {
|
|||
CASSERT("add_eq", check_invariant());
|
||||
}
|
||||
|
||||
void context::undo_merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2, unsigned e2_generation) {
|
||||
// TODO: optimization: don't bother unrolling e1 if e1 is an enode about to be garbage collected.
|
||||
set_generation(e1, e1_generation);
|
||||
set_generation(e2, e2_generation);
|
||||
|
||||
apply_sticky_updates(e1, e1_generation, e2, e2_generation);
|
||||
}
|
||||
|
||||
void context::apply_sticky_updates(enode * e1, unsigned e1_generation, enode * e2, unsigned e2_generation) {
|
||||
SASSERT(e1->uses_cg_table());
|
||||
SASSERT(e2->uses_cg_table());
|
||||
// optimization opportunity: we actually just need to look at updates above the current decision level.
|
||||
// Then we wouldn't have to check for minimum either.
|
||||
for (auto const& [t, generation] : m_sticky_generation_updates) {
|
||||
if (generation < e1_generation && congruent(t, e1)) {
|
||||
set_generation(e1, generation);
|
||||
} else if (generation < e2_generation && congruent(t, e2)) {
|
||||
set_generation(e2, generation);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Auxiliary method for undo_add_eq.
|
||||
It restores the theory variables of a given root enode.
|
||||
|
|
@ -1283,7 +1379,7 @@ namespace smt {
|
|||
*/
|
||||
enode * context::get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args) {
|
||||
enode * tmp = m_tmp_enode.set(f, num_args, args);
|
||||
enode * r = m_cg_table.find(tmp);
|
||||
enode * r = m_cg_table.find(tmp);
|
||||
#ifdef Z3DEBUG
|
||||
if (r != nullptr) {
|
||||
SASSERT(r->get_decl() == f);
|
||||
|
|
@ -2246,8 +2342,9 @@ namespace smt {
|
|||
unsigned ilvl = e->get_iscope_lvl();
|
||||
if (ilvl <= new_scope_lvl)
|
||||
continue; // node and its children will not be recreated during backtracking
|
||||
TRACE(cached_generation, tout << "caching: #" << n->get_id() << " " << e->get_generation() << "\n";);
|
||||
m_cached_generation.insert(n, e->get_generation());
|
||||
unsigned generation = get_generation(e);
|
||||
TRACE(cached_generation, tout << "caching: #" << n->get_id() << " " << generation << "\n";);
|
||||
m_cached_generation.insert(n, generation);
|
||||
}
|
||||
for (expr * arg : *to_app(n)) {
|
||||
if (is_app(arg) || is_quantifier(arg))
|
||||
|
|
|
|||
|
|
@ -46,6 +46,7 @@ Revision History:
|
|||
#include "util/ref.h"
|
||||
#include "util/timer.h"
|
||||
#include "util/statistics.h"
|
||||
#include "util/map.h"
|
||||
#include "smt/fingerprints.h"
|
||||
#include "smt/proto_model/proto_model.h"
|
||||
#include "smt/theory_user_propagator.h"
|
||||
|
|
@ -66,6 +67,9 @@ namespace smt {
|
|||
class context;
|
||||
class kernel;
|
||||
|
||||
// Hash table for storing enode -> generation mappings
|
||||
typedef ptr_addr_map<enode, unsigned> enode_generation_table;
|
||||
|
||||
struct oom_exception : public z3_error {
|
||||
oom_exception() : z3_error(ERR_MEMOUT) {}
|
||||
};
|
||||
|
|
@ -156,7 +160,8 @@ namespace smt {
|
|||
vector<enode_vector> m_decl2enodes; // decl -> enode (for decls with arity > 0)
|
||||
enode_vector m_empty_vector;
|
||||
cg_table m_cg_table;
|
||||
|
||||
enode_generation_table m_sticky_generation_updates;
|
||||
vector<std::pair<enode*, unsigned>> m_r1_parent_generations; // temporary field used to cache generations between remove_parents_from_cg_table and reinsert_parents_into_cg_table
|
||||
struct new_eq {
|
||||
enode * m_lhs;
|
||||
enode * m_rhs;
|
||||
|
|
@ -615,6 +620,26 @@ namespace smt {
|
|||
return m_qmanager->get_generation(q);
|
||||
}
|
||||
|
||||
unsigned get_generation(enode * e) const {
|
||||
// We don't support patterns with equality so there is no need to track generations for them.
|
||||
if (e->is_eq())
|
||||
return 0;
|
||||
|
||||
return get_cg_root(e)->m_generation;
|
||||
}
|
||||
|
||||
unsigned get_max_generation(unsigned num_enodes, enode * const * enodes) {
|
||||
unsigned max = 0;
|
||||
for (unsigned i = 0; i < num_enodes; ++i) {
|
||||
unsigned curr = get_generation(enodes[i]);
|
||||
if (curr > max)
|
||||
max = curr;
|
||||
}
|
||||
return max;
|
||||
}
|
||||
|
||||
void set_generation(enode * e, unsigned generation);
|
||||
|
||||
/**
|
||||
\brief Return true if the logical context internalized universal quantifiers.
|
||||
*/
|
||||
|
|
@ -1131,12 +1156,16 @@ namespace smt {
|
|||
void push_new_th_diseq(theory_id th, theory_var lhs, theory_var rhs);
|
||||
|
||||
friend class add_eq_trail;
|
||||
|
||||
friend class merge_cgc_generations_trail;
|
||||
|
||||
void remove_parents_from_cg_table(enode * r1);
|
||||
|
||||
void reinsert_parents_into_cg_table(enode * r1, enode * r2, enode * n1, enode * n2, eq_justification js);
|
||||
|
||||
void merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2);
|
||||
|
||||
void set_generation_sticky(enode * e, unsigned generation);
|
||||
|
||||
void invert_trans(enode * n);
|
||||
|
||||
theory_var get_closest_var(enode * n, theory_id th_id);
|
||||
|
|
@ -1147,6 +1176,10 @@ namespace smt {
|
|||
|
||||
void propagate_bool_enode_assignment_core(enode * source, enode * target);
|
||||
|
||||
void undo_merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2, unsigned e2_generation);
|
||||
|
||||
void apply_sticky_updates(enode * e1, unsigned e1_generation, enode * e2, unsigned e2_generation);
|
||||
|
||||
void undo_add_eq(enode * r1, enode * n1, unsigned r2_num_parents);
|
||||
|
||||
void restore_theory_vars(enode * r2, enode * r1);
|
||||
|
|
@ -1193,6 +1226,18 @@ namespace smt {
|
|||
|
||||
static bool is_eq(enode const * n1, enode const * n2) { return n1->get_root() == n2->get_root(); }
|
||||
|
||||
enode * get_cg_root(enode * n) const {
|
||||
if (!n->uses_cg_table())
|
||||
return n;
|
||||
// Fast path: if e is already the congruence root, avoid table lookup.
|
||||
// This is important for performance, since get_cg_root is called on every generation lookup.
|
||||
if (n->is_cgr())
|
||||
return n;
|
||||
auto r = m_cg_table.find(n);
|
||||
SASSERT(r != nullptr);
|
||||
return r;
|
||||
}
|
||||
|
||||
bool is_diseq(enode * n1, enode * n2) const;
|
||||
|
||||
bool is_diseq_slow(enode * n1, enode * n2) const;
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@ Revision History:
|
|||
#include "smt/smt_enode.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
||||
/**
|
||||
\brief Initialize an enode in the given memory position.
|
||||
*/
|
||||
|
|
@ -65,8 +65,8 @@ namespace smt {
|
|||
}
|
||||
|
||||
enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner,
|
||||
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
|
||||
bool cgc_enabled, bool update_children_parent) {
|
||||
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
|
||||
bool cgc_enabled, bool update_children_parent) {
|
||||
SASSERT(m.is_bool(owner) || !merge_tf);
|
||||
unsigned sz = get_enode_size(suppress_args || !::is_app(owner) ? 0 : to_app(owner)->get_num_args());
|
||||
void * mem = r.allocate(sz);
|
||||
|
|
@ -131,20 +131,6 @@ namespace smt {
|
|||
m_th_var_list.del_var(id);
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
\brief Push old value of generation on the context trail stack
|
||||
and update the generation.
|
||||
*/
|
||||
void enode::set_generation(context * ctx, unsigned generation) {
|
||||
if (m_generation == generation)
|
||||
return;
|
||||
if (ctx)
|
||||
ctx->push_trail(value_trail<unsigned>(m_generation));
|
||||
m_generation = generation;
|
||||
}
|
||||
|
||||
|
||||
void enode::set_lbl_hash(context & ctx) {
|
||||
SASSERT(m_lbl_hash == -1);
|
||||
// m_lbl_hash should be different from -1, if and only if,
|
||||
|
|
@ -161,16 +147,17 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
enode * enode::get_eq_enode_with_min_gen() {
|
||||
if (m_generation == 0)
|
||||
return this;
|
||||
enode * enode::get_eq_enode_with_min_gen(context * ctx) {
|
||||
enode * r = this;
|
||||
enode * curr = this;
|
||||
unsigned r_gen = ctx->get_generation(r);
|
||||
do {
|
||||
if (curr->m_generation < r->m_generation) {
|
||||
unsigned curr_gen = ctx->get_generation(curr);
|
||||
if (curr_gen == 0)
|
||||
return curr;
|
||||
if (curr_gen < r_gen) {
|
||||
r = curr;
|
||||
if (r->m_generation == 0)
|
||||
return r;
|
||||
r_gen = curr_gen;
|
||||
}
|
||||
curr = curr->m_next;
|
||||
}
|
||||
|
|
@ -307,16 +294,6 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
unsigned get_max_generation(unsigned num_enodes, enode * const * enodes) {
|
||||
unsigned max = 0;
|
||||
for (unsigned i = 0; i < num_enodes; ++i) {
|
||||
unsigned curr = enodes[i]->get_generation();
|
||||
if (curr > max)
|
||||
max = curr;
|
||||
}
|
||||
return max;
|
||||
}
|
||||
|
||||
void unmark_enodes(unsigned num_enodes, enode * const * enodes) {
|
||||
for (unsigned i = 0; i < num_enodes; ++i)
|
||||
enodes[i]->unset_mark();
|
||||
|
|
|
|||
|
|
@ -64,7 +64,7 @@ namespace smt {
|
|||
enode * m_next; //!< Next element in the equivalence class.
|
||||
enode * m_cg;
|
||||
unsigned m_class_size; //!< Size of the equivalence class if the enode is the root.
|
||||
unsigned m_generation; //!< Tracks how many quantifier instantiation rounds were needed to generate this enode.
|
||||
unsigned m_generation; //!< Cached generation of the congruence class. Valid when is_cgr(), or when the enode does not use the cg_table (constants/leaves/true-eq nodes), where it directly stores the enode's generation.
|
||||
|
||||
unsigned m_func_decl_id; //!< Id generated by the congruence table for fast indexing.
|
||||
|
||||
|
|
@ -102,7 +102,7 @@ namespace smt {
|
|||
approx_set m_lbls;
|
||||
approx_set m_plbls;
|
||||
enode * m_args[0]; //!< Cached args
|
||||
|
||||
|
||||
friend class context;
|
||||
friend class conflict_resolution;
|
||||
friend class quantifier_manager;
|
||||
|
|
@ -142,8 +142,8 @@ namespace smt {
|
|||
}
|
||||
|
||||
static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner,
|
||||
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
|
||||
bool cgc_enabled, bool update_children_parent);
|
||||
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
|
||||
bool cgc_enabled, bool update_children_parent);
|
||||
|
||||
static enode * mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner);
|
||||
|
||||
|
|
@ -314,6 +314,10 @@ namespace smt {
|
|||
return m_cg;
|
||||
}
|
||||
|
||||
bool uses_cg_table() const {
|
||||
return get_num_args() > 0 && is_cgc_enabled() && !is_true_eq();
|
||||
}
|
||||
|
||||
bool is_cgc_enabled() const {
|
||||
return m_cgc_enabled;
|
||||
}
|
||||
|
|
@ -393,18 +397,12 @@ namespace smt {
|
|||
trans_justification get_trans_justification() {
|
||||
return m_trans;
|
||||
}
|
||||
|
||||
unsigned get_generation() const {
|
||||
return m_generation;
|
||||
}
|
||||
|
||||
void set_generation(context * ctx, unsigned generation);
|
||||
|
||||
/**
|
||||
\brief Return the enode n that is in the eqc of *this, and has the minimal generation.
|
||||
That is, there is no other enode with smaller generation.
|
||||
*/
|
||||
enode * get_eq_enode_with_min_gen();
|
||||
enode * get_eq_enode_with_min_gen(context * ctx);
|
||||
|
||||
unsigned get_iscope_lvl() const {
|
||||
return m_iscope_lvl;
|
||||
|
|
@ -459,8 +457,6 @@ namespace smt {
|
|||
bool aux;
|
||||
return congruent(n1, n2, aux);
|
||||
}
|
||||
|
||||
unsigned get_max_generation(unsigned num_enodes, enode * const * enodes);
|
||||
|
||||
void unmark_enodes(unsigned num_enodes, enode * const * enodes);
|
||||
|
||||
|
|
|
|||
|
|
@ -102,8 +102,60 @@ namespace smt {
|
|||
}
|
||||
|
||||
void context::update_generation(enode * e) {
|
||||
if (0 < m_generation && m_generation < e->get_generation())
|
||||
e->set_generation(nullptr, m_generation);
|
||||
// We don't support patterns with equality so there is no need to track generations for them.
|
||||
if (e->is_eq())
|
||||
return;
|
||||
|
||||
if (0 < m_generation && m_generation < get_generation(e)) {
|
||||
if (e->uses_cg_table())
|
||||
set_generation_sticky(e, m_generation);
|
||||
else
|
||||
set_generation(e, m_generation);
|
||||
}
|
||||
}
|
||||
|
||||
void context::set_generation(enode * e, unsigned generation) {
|
||||
// We don't support patterns with equality so there is no need to track generations for them.
|
||||
if (e->is_eq())
|
||||
return;
|
||||
|
||||
// The class generation is stored in the congruence root's m_generation field.
|
||||
enode * cgr = get_cg_root(e);
|
||||
cgr->m_generation = generation;
|
||||
}
|
||||
|
||||
class merge_cgc_generations_trail : public trail {
|
||||
context& ctx;
|
||||
enode* m_e1;
|
||||
unsigned m_e1_generation;
|
||||
enode* m_e2;
|
||||
unsigned m_e2_generation;
|
||||
public:
|
||||
merge_cgc_generations_trail(context& ctx, enode* e1, unsigned e1_generation, enode* e2, unsigned e2_generation):
|
||||
ctx(ctx),
|
||||
m_e1(e1),
|
||||
m_e1_generation(e1_generation),
|
||||
m_e2(e2),
|
||||
m_e2_generation(e2_generation) {
|
||||
}
|
||||
|
||||
void undo() override {
|
||||
ctx.undo_merge_cgc_generations(m_e1, m_e1_generation, m_e2, m_e2_generation);
|
||||
}
|
||||
};
|
||||
|
||||
void context::merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2) {
|
||||
SASSERT(e2->is_cgr());
|
||||
SASSERT(!m_cg_table.contains_ptr(e1));
|
||||
SASSERT(m_cg_table.contains_ptr(e2));
|
||||
|
||||
// Push trail even if we have a no-op. Otherwise we can't restore e1's generation after unmerging.
|
||||
push_trail(merge_cgc_generations_trail(*this, e1, e1_generation, e2, e2->m_generation));
|
||||
|
||||
if (e1_generation >= e2->m_generation)
|
||||
return; // no-op
|
||||
|
||||
e2->m_generation = e1_generation;
|
||||
}
|
||||
|
||||
void context::ts_visit_child(expr * n, bool gate_ctx, svector<expr_bool_pair> & todo, bool & visited) {
|
||||
|
|
@ -1025,6 +1077,9 @@ namespace smt {
|
|||
auto [e_prime, used_commutativity] = m_cg_table.insert(e);
|
||||
if (e != e_prime) {
|
||||
e->m_cg = e_prime;
|
||||
// We don't support patterns with equality so there is no need to track generations for them.
|
||||
if (!e->is_eq())
|
||||
merge_cgc_generations(e, generation, e_prime);
|
||||
push_new_congruence(e, e_prime, used_commutativity);
|
||||
}
|
||||
else {
|
||||
|
|
@ -1042,6 +1097,7 @@ namespace smt {
|
|||
m_decl2enodes[decl_id].push_back(e);
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(e_internalized(n));
|
||||
m_stats.m_num_mk_enode++;
|
||||
TRACE(mk_enode, tout << "created enode: #" << e->get_owner_id() << " for:\n" << mk_pp(n, m) << "\n";
|
||||
|
|
@ -1066,10 +1122,11 @@ namespace smt {
|
|||
unsigned n_id = n->get_id();
|
||||
enode * e = m_app2enode[n_id];
|
||||
m_app2enode[n_id] = nullptr;
|
||||
if (e->is_cgr() && !e->is_true_eq() && e->is_cgc_enabled()) {
|
||||
if (e->is_cgr() && e->uses_cg_table()) {
|
||||
SASSERT(m_cg_table.contains_ptr(e));
|
||||
m_cg_table.erase(e);
|
||||
}
|
||||
SASSERT(!(e->get_num_args() > 0 && m_cg_table.contains_ptr(e)));
|
||||
if (e->get_num_args() > 0 && !e->is_eq()) {
|
||||
unsigned decl_id = e->get_decl_id();
|
||||
SASSERT(decl_id < m_decl2enodes.size());
|
||||
|
|
@ -1080,6 +1137,7 @@ namespace smt {
|
|||
SASSERT(m_e_internalized_stack.size() == m_enodes.size());
|
||||
m_enodes.pop_back();
|
||||
m_e_internalized_stack.pop_back();
|
||||
m_sticky_generation_updates.erase(e);
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
|
|||
|
|
@ -109,7 +109,7 @@ namespace smt {
|
|||
for (auto const& kv : *m_root2value) {
|
||||
enode * n = kv.m_key;
|
||||
expr * val = kv.m_value;
|
||||
n = n->get_eq_enode_with_min_gen();
|
||||
n = n->get_eq_enode_with_min_gen(m_context);
|
||||
expr* e = n->get_expr();
|
||||
if (!m.is_value(e))
|
||||
m_value2expr.insert(val, e);
|
||||
|
|
|
|||
|
|
@ -1238,7 +1238,7 @@ namespace smt {
|
|||
// a necessary instantiation.
|
||||
enode* e_arg = n->get_arg(m_arg_i);
|
||||
expr* arg = e_arg->get_expr();
|
||||
A_f_i->insert(arg, e_arg->get_generation());
|
||||
A_f_i->insert(arg, ctx->get_generation(e_arg));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1256,7 +1256,7 @@ namespace smt {
|
|||
if (ctx->is_relevant(n)) {
|
||||
enode* e_arg = n->get_arg(m_arg_i);
|
||||
expr* arg = e_arg->get_expr();
|
||||
s->insert(arg, e_arg->get_generation());
|
||||
s->insert(arg, ctx->get_generation(e_arg));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1312,7 +1312,7 @@ namespace smt {
|
|||
bv_rw.mk_sub(arg, m_offset, arg_minus_k);
|
||||
else
|
||||
arith_rw.mk_sub(arg, m_offset, arg_minus_k);
|
||||
S_j->insert(arg_minus_k, e_arg->get_generation());
|
||||
S_j->insert(arg_minus_k, ctx->get_generation(e_arg));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1434,7 +1434,7 @@ namespace smt {
|
|||
auto e = n->get_expr();
|
||||
if (srt == n->get_sort()) {
|
||||
TRACE(model_finder, tout << "inserting " << mk_pp(e, m) << " into inst set\n");
|
||||
S->insert(e, n->get_generation());
|
||||
S->insert(e, ctx->get_generation(n));
|
||||
}
|
||||
else if (!use_term_enum)
|
||||
continue;
|
||||
|
|
@ -1573,7 +1573,7 @@ namespace smt {
|
|||
if (ctx->is_relevant(p) && p->get_decl() == m_select->get_decl()) {
|
||||
SASSERT(m_arg_i < p->get_num_args());
|
||||
enode* e_arg = p->get_arg(m_arg_i);
|
||||
A_f_i->insert(e_arg->get_expr(), e_arg->get_generation());
|
||||
A_f_i->insert(e_arg->get_expr(), ctx->get_generation(e_arg));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1702,7 +1702,7 @@ namespace smt {
|
|||
node* S_q_i = slv.get_uvar(q, m_var_i);
|
||||
for (enode* n : ctx->enodes()) {
|
||||
if (ctx->is_relevant(n) && n->get_expr()->get_sort() == s) {
|
||||
S_q_i->insert(n->get_expr(), n->get_generation());
|
||||
S_q_i->insert(n->get_expr(), ctx->get_generation(n));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -249,9 +249,7 @@ namespace smt {
|
|||
trace_stream() << "\n";
|
||||
} else {
|
||||
std::ostream & out = trace_stream();
|
||||
|
||||
obj_hashtable<enode> already_visited;
|
||||
|
||||
// In the term produced by the quantifier instantiation the root of the equivalence class of the terms bound to the quantified variables
|
||||
// is used. We need to make sure that all of these equalities appear in the log.
|
||||
for (unsigned i = 0; i < num_bindings; ++i) {
|
||||
|
|
@ -264,7 +262,6 @@ namespace smt {
|
|||
log_justification_to_root(out, substituted, already_visited, m_context, m());
|
||||
}
|
||||
}
|
||||
|
||||
// At this point all relevant equalities for the match are logged.
|
||||
out << "[new-match] " << f->get_data_hash() << " #" << q->get_id() << " #" << pat->get_id();
|
||||
for (unsigned i = 0; i < num_bindings; ++i) {
|
||||
|
|
@ -285,7 +282,7 @@ namespace smt {
|
|||
out << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
bool add_instance(quantifier * q, app * pat,
|
||||
unsigned num_bindings,
|
||||
enode * const * bindings,
|
||||
|
|
@ -724,8 +721,9 @@ namespace smt {
|
|||
}
|
||||
enode* n = m_context->get_enode(e);
|
||||
new_bindings.push_back(n);
|
||||
if (n->get_generation() > max_gen)
|
||||
max_gen = n->get_generation();
|
||||
unsigned gen = m_context->get_generation(n);
|
||||
if (gen > max_gen)
|
||||
max_gen = gen;
|
||||
}
|
||||
|
||||
TRACE(ho_matching,
|
||||
|
|
|
|||
|
|
@ -235,8 +235,8 @@ namespace smt {
|
|||
TRACE(quick_checker, tout << "found new candidate\n";);
|
||||
TRACE(quick_checker_sizes, tout << "found new candidate\n";
|
||||
for (unsigned i = 0; i < m_num_bindings; ++i) tout << "#" << m_bindings[i]->get_owner_id() << " "; tout << "\n";);
|
||||
unsigned max_generation = get_max_generation(m_num_bindings, m_bindings.data());
|
||||
if (m_context.add_instance(q, nullptr /* no pattern was used */, m_num_bindings, m_bindings.data(),
|
||||
unsigned max_generation = m_context.get_max_generation(m_num_bindings, m_bindings.data());
|
||||
if (m_context.add_instance(q, nullptr /* no pattern was used */, m_num_bindings, m_bindings.data(),
|
||||
max_generation,
|
||||
0, // min_top_generation is only available for instances created by the MAM
|
||||
0, // max_top_generation is only available for instances created by the MAM
|
||||
|
|
|
|||
|
|
@ -484,7 +484,7 @@ public:
|
|||
unsigned idx = h & mask;
|
||||
cell * c = m_table + idx;
|
||||
if (c->is_free())
|
||||
return;
|
||||
return;
|
||||
cell * prev = nullptr;
|
||||
do {
|
||||
if (equals(c->m_data, d)) {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue