mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-29 23:43:15 +00:00
Code Activity

small optimization in compilation of multi-patterns

Browse source 
also make the path faster for single patterns
This commit is contained in:
Nuno Lopes 2016-11-28 14:43:47 +00:00
parent 4452ac0d6d
commit 2babd192b8
1 changed files with 8 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/smt/mam.cpp
View file

@ -795,7 +795,7 @@ namespace smt {
code_tree * m_tree; code_tree * m_tree;
unsigned m_num_choices; unsigned m_num_choices;
bool m_is_tmp_tree; bool m_is_tmp_tree;
svector<unsigned> m_mp_already_processed; svector<bool> m_mp_already_processed;
obj_map<expr, unsigned> m_matched_exprs; obj_map<expr, unsigned> m_matched_exprs;
struct pcheck_checked { struct pcheck_checked {
@ -1116,7 +1116,7 @@ namespace smt {
unsigned best_j = 0; unsigned best_j = 0;
bool found_bounded_mp = false; bool found_bounded_mp = false;
for (unsigned j = 0; j < m_mp->get_num_args(); j++) { for (unsigned j = 0; j < m_mp->get_num_args(); j++) {
if (std::find(m_mp_already_processed.begin(), m_mp_already_processed.end(), j) != m_mp_already_processed.end()) if (m_mp_already_processed[j])
continue; continue;
app * p = to_app(m_mp->get_arg(j)); app * p = to_app(m_mp->get_arg(j));
bool has_unbound_vars = false; bool has_unbound_vars = false;
@ -1133,7 +1133,7 @@ namespace smt {
best_j = j; best_j = j;
} }
} }
m_mp_already_processed.push_back(best_j); m_mp_already_processed[best_j] = true;
SASSERT(best != 0); SASSERT(best != 0);
app * p = best; app * p = best;
func_decl * lbl = p->get_decl(); func_decl * lbl = p->get_decl();
@ -1226,13 +1226,15 @@ namespace smt {
*/ */
void linearise(instruction * head, unsigned first_idx) { void linearise(instruction * head, unsigned first_idx) {
m_seq.reset(); m_seq.reset();
m_mp_already_processed.reset();
m_mp_already_processed.push_back(first_idx);
while (!m_todo.empty()) while (!m_todo.empty())
linearise_core(); linearise_core();
if (m_mp->get_num_args() > 1) if (m_mp->get_num_args() > 1) {
m_mp_already_processed.reset();
m_mp_already_processed.resize(m_mp->get_num_args());
m_mp_already_processed[first_idx] = true;
linearise_multi_pattern(first_idx); linearise_multi_pattern(first_idx);
}
#ifdef Z3DEBUG #ifdef Z3DEBUG
for (unsigned i = 0; i < m_qa->get_num_decls(); i++) { for (unsigned i = 0; i < m_qa->get_num_decls(); i++) {