From 17993101554675c309df40f94d29b2a4885f0b62 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 26 Nov 2016 14:07:05 +0000 Subject: [PATCH 1/5] Fixed iterator invalidation bug in SAT probing. Relates to #798. --- src/sat/sat_probing.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index 0b5edb2c9..f54ee9f89 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -139,17 +139,17 @@ namespace sat { if (m_probing_binary) { watch_list & wlist = s.get_wlist(~l); - watch_list::iterator it = wlist.begin(); - watch_list::iterator end = wlist.end(); - for (; it != end ; ++it) { - if (!it->is_binary_clause()) + for (unsigned i = 0; i < wlist.size(); i++) { + watched & w = wlist[i]; + if (!w.is_binary_clause()) break; - literal l2 = it->get_literal(); + literal l2 = w.get_literal(); if (l.index() > l2.index()) continue; if (s.value(l2) != l_undef) continue; // verbose_stream() << "probing " << l << " " << l2 << " " << m_counter << "\n"; + // Note: that try_lit calls propagate, which may update the watch lists. if (!try_lit(l2, false)) return; if (s.inconsistent()) From 4452ac0d6d13001b95bba65ace9704b2857be5cc Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 28 Nov 2016 13:48:15 +0000 Subject: [PATCH 2/5] optimize pattern matching code generator for DAG patterns generated code now uses COMPARE instructions to compare subtrees instead of diving into both subtrees. Code is thus smaller and fails faster. --- src/smt/mam.cpp | 28 ++++++++++++++++++---------- 1 file changed, 18 insertions(+), 10 deletions(-) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index f5b3f34f7..62033c7b9 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -424,7 +424,7 @@ namespace smt { out << *curr; curr = curr->m_next; while (curr != 0 && curr->m_opcode != CHOOSE && curr->m_opcode != NOOP) { - out << " "; + out << "\n"; out << *curr; curr = curr->m_next; } @@ -796,6 +796,7 @@ namespace smt { unsigned m_num_choices; bool m_is_tmp_tree; svector m_mp_already_processed; + obj_map m_matched_exprs; struct pcheck_checked { func_decl * m_label; @@ -840,6 +841,7 @@ namespace smt { m_mp = mp; m_num_choices = 0; m_todo.reset(); + m_matched_exprs.reset(); m_registers.fill(0); app * p = to_app(mp->get_arg(first_idx)); @@ -951,7 +953,15 @@ namespace smt { set_check_mark(reg, NOT_CHECKED); // reset mark, register was fully processed. continue; } - + + unsigned matched_reg; + if (m_matched_exprs.find(p, matched_reg) && reg != matched_reg) { + m_seq.push_back(m_ct_manager.mk_compare(matched_reg, reg)); + set_check_mark(reg, NOT_CHECKED); // reset mark, register was fully processed. + continue; + } + m_matched_exprs.insert(p, reg); + if (m_use_filters && get_check_mark(reg) != CHECK_SINGLETON) { func_decl * lbl = to_app(p)->get_decl(); approx_set s(m_lbl_hasher(lbl)); @@ -1311,9 +1321,6 @@ namespace smt { unsigned reg2 = instr->m_reg2; return m_registers[reg1] != 0 && - m_registers[reg2] != 0 && - is_var(m_registers[reg1]) && - is_var(m_registers[reg2]) && m_registers[reg1] == m_registers[reg2]; } @@ -1571,12 +1578,13 @@ namespace smt { unsigned reg1 = static_cast(curr)->m_reg1; unsigned reg2 = static_cast(curr)->m_reg2; SASSERT(m_todo.contains(reg2)); - m_todo.erase(reg1); m_todo.erase(reg2); - SASSERT(is_var(m_registers[reg1])); - unsigned var_id = to_var(m_registers[reg1])->get_idx(); - if (m_vars[var_id] == -1) - m_vars[var_id] = reg1; + if (is_var(m_registers[reg1])) { + m_todo.erase(reg1); + unsigned var_id = to_var(m_registers[reg1])->get_idx(); + if (m_vars[var_id] == -1) + m_vars[var_id] = reg1; + } m_compatible.push_back(curr); } else { From 2babd192b8d1dd1645c28731cb331b2bdbf634b4 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 28 Nov 2016 14:43:47 +0000 Subject: [PATCH 3/5] small optimization in compilation of multi-patterns also make the path faster for single patterns --- src/smt/mam.cpp | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 62033c7b9..8c1eecb84 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -795,7 +795,7 @@ namespace smt { code_tree * m_tree; unsigned m_num_choices; bool m_is_tmp_tree; - svector m_mp_already_processed; + svector m_mp_already_processed; obj_map m_matched_exprs; struct pcheck_checked { @@ -1116,7 +1116,7 @@ namespace smt { unsigned best_j = 0; bool found_bounded_mp = false; 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; app * p = to_app(m_mp->get_arg(j)); bool has_unbound_vars = false; @@ -1133,7 +1133,7 @@ namespace smt { best_j = j; } } - m_mp_already_processed.push_back(best_j); + m_mp_already_processed[best_j] = true; SASSERT(best != 0); app * p = best; func_decl * lbl = p->get_decl(); @@ -1226,13 +1226,15 @@ namespace smt { */ void linearise(instruction * head, unsigned first_idx) { m_seq.reset(); - m_mp_already_processed.reset(); - m_mp_already_processed.push_back(first_idx); while (!m_todo.empty()) 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); + } #ifdef Z3DEBUG for (unsigned i = 0; i < m_qa->get_num_decls(); i++) { From 4b4365470d5000b14c7890f980d5b566571b52e1 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 28 Nov 2016 15:40:25 +0000 Subject: [PATCH 4/5] mam compiler: move reset of matched_exprs cache next to code reset --- src/smt/mam.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 8c1eecb84..60aed12e1 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -841,7 +841,6 @@ namespace smt { m_mp = mp; m_num_choices = 0; m_todo.reset(); - m_matched_exprs.reset(); m_registers.fill(0); app * p = to_app(mp->get_arg(first_idx)); @@ -1226,6 +1225,7 @@ namespace smt { */ void linearise(instruction * head, unsigned first_idx) { m_seq.reset(); + m_matched_exprs.reset(); while (!m_todo.empty()) linearise_core(); From d9227b95ea4e3894f63907c38c4b3a79e249c429 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 29 Nov 2016 15:45:23 -0800 Subject: [PATCH 5/5] blast distinct in incremental BV solver Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 682978287..e56abc50c 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -336,6 +336,7 @@ public: simp2_p.set_bool("flat", true); // required by som simp2_p.set_bool("hoist_mul", false); // required by som simp2_p.set_bool("elim_and", true); + simp2_p.set_bool("blast_distinct", true); m_preprocess = and_then(mk_card2bv_tactic(m, m_params), using_params(mk_simplify_tactic(m), simp2_p),