mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

#5324

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-04 16:15:09 -07:00
parent 39af2a188d
commit 08e7de3c09
1 changed files with 15 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -3030,6 +3030,7 @@ namespace q {
ptr_vector<code_tree> m_tmp_trees; ptr_vector<code_tree> m_tmp_trees;
ptr_vector<func_decl> m_tmp_trees_to_delete; ptr_vector<func_decl> m_tmp_trees_to_delete;
ptr_vector<code_tree> m_to_match; ptr_vector<code_tree> m_to_match;
unsigned m_to_match_head = 0;
typedef std::pair<quantifier *, app *> qp_pair; typedef std::pair<quantifier *, app *> qp_pair;
svector<qp_pair> m_new_patterns; // recently added patterns svector<qp_pair> m_new_patterns; // recently added patterns
@ -3059,16 +3060,14 @@ namespace q {
enode * m_other { nullptr }; // temp field enode * m_other { nullptr }; // temp field
bool m_check_missing_instances { false }; bool m_check_missing_instances { false };
class reset_to_match : public trail { class pop_to_match : public trail {
mam_impl& i; mam_impl& i;
public: public:
reset_to_match(mam_impl& i):i(i) {} pop_to_match(mam_impl& i):i(i) {}
void undo() override { void undo() override {
if (i.m_to_match.empty()) code_tree* t = i.m_to_match.back();
return; t->reset_candidates();
for (code_tree* t : i.m_to_match) i.m_to_match.pop_back();
t->reset_candidates();
i.m_to_match.reset();
} }
}; };
@ -3092,12 +3091,12 @@ namespace q {
} }
void add_candidate(code_tree * t, enode * app) { void add_candidate(code_tree * t, enode * app) {
if (t != nullptr) { if (t) {
TRACE("mam_candidate", tout << "adding candidate:\n" << mk_ll_pp(app->get_expr(), m);); TRACE("mam_candidate", tout << "adding candidate:\n" << mk_ll_pp(app->get_expr(), m););
if (m_to_match.empty()) if (!t->has_candidates()) {
ctx.push(reset_to_match(*this)); ctx.push(pop_to_match(*this));
if (!t->has_candidates())
m_to_match.push_back(t); m_to_match.push_back(t);
}
t->add_candidate(app); t->add_candidate(app);
} }
} }
@ -3755,7 +3754,6 @@ namespace q {
void reset() override { void reset() override {
m_trees.reset(); m_trees.reset();
m_to_match.reset();
m_new_patterns.reset(); m_new_patterns.reset();
m_is_plbl.reset(); m_is_plbl.reset();
m_is_clbl.reset(); m_is_clbl.reset();
@ -3773,12 +3771,15 @@ namespace q {
void propagate() override { void propagate() override {
TRACE("trigger_bug", tout << "match\n"; display(tout);); TRACE("trigger_bug", tout << "match\n"; display(tout););
for (code_tree* t : m_to_match) { if (m_to_match_head >= m_to_match.size())
return;
ctx.push(value_trail<unsigned>(m_to_match_head));
for (; m_to_match_head < m_to_match.size(); ++m_to_match_head) {
code_tree* t = m_to_match[m_to_match_head];
SASSERT(t->has_candidates()); SASSERT(t->has_candidates());
m_interpreter.execute(t); m_interpreter.execute(t);
t->reset_candidates(); t->reset_candidates();
} }
m_to_match.reset();
if (!m_new_patterns.empty()) { if (!m_new_patterns.empty()) {
match_new_patterns(); match_new_patterns();
m_new_patterns.reset(); m_new_patterns.reset();