mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

#5753

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-16 09:31:16 -08:00
parent bc9c6ad93d
commit cd56d55e34
3 changed files with 19 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/euf/euf_enode.h
View file

@ -45,6 +45,7 @@ namespace euf {
expr* m_expr = nullptr; expr* m_expr = nullptr;
bool m_mark1 = false; bool m_mark1 = false;
bool m_mark2 = false; bool m_mark2 = false;
bool m_mark3 = false;
bool m_commutative = false; bool m_commutative = false;
bool m_interpreted = false; bool m_interpreted = false;
bool m_merge_enabled = true; bool m_merge_enabled = true;
@ -173,6 +174,9 @@ namespace euf {
void mark2() { m_mark2 = true; } void mark2() { m_mark2 = true; }
void unmark2() { m_mark2 = false; } void unmark2() { m_mark2 = false; }
bool is_marked2() { return m_mark2; } bool is_marked2() { return m_mark2; }
void mark3() { m_mark3 = true; }
void unmark3() { m_mark3 = false; }
bool is_marked3() { return m_mark3; }
template<bool m> void mark1_targets() { template<bool m> void mark1_targets() {
enode* n = this; enode* n = this;

18
src/sat/smt/q_eval.cpp
View file

@ -230,13 +230,17 @@ namespace q {
if (!n) if (!n)
return nullptr; return nullptr;
for (unsigned i = args.size(); i-- > 0; ) { for (unsigned i = args.size(); i-- > 0; ) {
if (args[i] != n->get_arg(i)) { euf::enode* a = args[i], *b = n->get_arg(i);
// roots could be different when using commutativity if (a == b)
// instead of compensating for this, we just bail out continue;
if (args[i]->get_root() != n->get_arg(i)->get_root())
return nullptr; // roots could be different when using commutativity
evidence.push_back(euf::enode_pair(args[i], n->get_arg(i))); // instead of compensating for this, we just bail out
} if (a->get_root() != b->get_root())
return nullptr;
TRACE("q", tout << "evidence " << ctx.bpp(a) << " " << ctx.bpp(b) << "\n");
evidence.push_back(euf::enode_pair(a, b));
} }
m_indirect_nodes.push_back(n); m_indirect_nodes.push_back(n);
m_eval.setx(t->get_id(), n, nullptr); m_eval.setx(t->get_id(), n, nullptr);

8
src/sat/smt/q_mam.cpp
View file

@ -553,8 +553,8 @@ namespace q {
void unmark(unsigned head) { void unmark(unsigned head) {
for (unsigned i = m_candidates.size(); i-- > head; ) { for (unsigned i = m_candidates.size(); i-- > head; ) {
enode* app = m_candidates[i]; enode* app = m_candidates[i];
if (app->is_marked2()) if (app->is_marked3())
app->unmark2(); app->unmark3();
} }
} }
@ -2022,9 +2022,9 @@ namespace q {
code_tree::scoped_unmark _unmark(t); code_tree::scoped_unmark _unmark(t);
while ((app = t->next_candidate()) && !ctx.resource_limits_exceeded()) { while ((app = t->next_candidate()) && !ctx.resource_limits_exceeded()) {
TRACE("trigger_bug", tout << "candidate\n" << ctx.bpp(app) << "\n";); TRACE("trigger_bug", tout << "candidate\n" << ctx.bpp(app) << "\n";);
if (!app->is_marked2() && app->is_cgr()) { if (!app->is_marked3() && app->is_cgr()) {
execute_core(t, app); execute_core(t, app);
app->mark2(); app->mark3();
} }
} }
} }