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

#5454

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-10 14:47:26 -07:00
parent 081cdbd762
commit 7ab7b8646b
2 changed files with 11 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/q_ematch.cpp
View file

@ -490,6 +490,10 @@ namespace q {
TRACE("q", tout << "add " << mk_pp(_q, m) << "\n";); TRACE("q", tout << "add " << mk_pp(_q, m) << "\n";);
clause* c = clausify(_q); clause* c = clausify(_q);
quantifier* q = c->q(); quantifier* q = c->q();
if (m_q2clauses.contains(q)) {
dealloc(c);
return;
}
ensure_ground_enodes(*c); ensure_ground_enodes(*c);
m_clauses.push_back(c); m_clauses.push_back(c);
m_q2clauses.insert(q, c->index()); m_q2clauses.insert(q, c->index());

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

@ -414,7 +414,7 @@ namespace q {
enode_vector m_candidates; enode_vector m_candidates;
#ifdef Z3DEBUG #ifdef Z3DEBUG
egraph * m_egraph; egraph * m_egraph;
ptr_vector<app> m_patterns; svector<std::pair<quantifier*, app*>> m_patterns;
#endif #endif
#ifdef _PROFILE_MAM #ifdef _PROFILE_MAM
stopwatch m_watch; stopwatch m_watch;
@ -568,7 +568,7 @@ namespace q {
m_egraph = ctx; m_egraph = ctx;
} }
ptr_vector<app> & get_patterns() { svector<std::pair<quantifier*, app*>> & get_patterns() {
return m_patterns; return m_patterns;
} }
#endif #endif
@ -578,8 +578,8 @@ namespace q {
if (m_egraph) { if (m_egraph) {
ast_manager & m = m_egraph->get_manager(); ast_manager & m = m_egraph->get_manager();
out << "patterns:\n"; out << "patterns:\n";
for (app* a : m_patterns) for (auto [q, a] : m_patterns)
out << mk_pp(a, m) << "\n"; out << mk_pp(q, m) << " " << mk_pp(a, m) << "\n";
} }
#endif #endif
out << "function: " << m_root_lbl->get_name(); out << "function: " << m_root_lbl->get_name();
@ -2862,12 +2862,11 @@ namespace q {
// The E-matching engine that was built when all + and * applications were binary. // The E-matching engine that was built when all + and * applications were binary.
// We ignore the pattern if it does not have the expected number of arguments. // We ignore the pattern if it does not have the expected number of arguments.
// This is not the ideal solution, but it avoids possible crashes. // This is not the ideal solution, but it avoids possible crashes.
if (tree->expected_num_args() == p->get_num_args()) { if (tree->expected_num_args() == p->get_num_args())
m_compiler.insert(tree, qa, mp, first_idx, false); m_compiler.insert(tree, qa, mp, first_idx, false);
}
} }
DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(mp); DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(std::make_pair(qa, mp));
ctx.push(push_back_trail<app*, false>(m_trees[lbl_id]->get_patterns()));); ctx.push(push_back_trail<std::pair<quantifier*,app*>, false>(m_trees[lbl_id]->get_patterns())););
TRACE("trigger_bug", tout << "after add_pattern, first_idx: " << first_idx << "\n"; m_trees[lbl_id]->display(tout);); TRACE("trigger_bug", tout << "after add_pattern, first_idx: " << first_idx << "\n"; m_trees[lbl_id]->display(tout););
} }