mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-21 10:41:35 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-11-30 09:52:15 -08:00
commit 7ebc660b6d
3 changed files with 32 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/sat/sat_probing.cpp
View file

@ -139,17 +139,17 @@ namespace sat {
if (m_probing_binary) { if (m_probing_binary) {
watch_list & wlist = s.get_wlist(~l); watch_list & wlist = s.get_wlist(~l);
watch_list::iterator it = wlist.begin(); for (unsigned i = 0; i < wlist.size(); i++) {
watch_list::iterator end = wlist.end(); watched & w = wlist[i];
for (; it != end ; ++it) { if (!w.is_binary_clause())
if (!it->is_binary_clause())
break; break;
literal l2 = it->get_literal(); literal l2 = w.get_literal();
if (l.index() > l2.index()) if (l.index() > l2.index())
continue; continue;
if (s.value(l2) != l_undef) if (s.value(l2) != l_undef)
continue; continue;
// verbose_stream() << "probing " << l << " " << l2 << " " << m_counter << "\n"; // 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)) if (!try_lit(l2, false))
return; return;
if (s.inconsistent()) if (s.inconsistent())

1
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -336,6 +336,7 @@ public:
simp2_p.set_bool("flat", true); // required by som simp2_p.set_bool("flat", true); // required by som
simp2_p.set_bool("hoist_mul", false); // required by som simp2_p.set_bool("hoist_mul", false); // required by som
simp2_p.set_bool("elim_and", true); simp2_p.set_bool("elim_and", true);
simp2_p.set_bool("blast_distinct", true);
m_preprocess = m_preprocess =
and_then(mk_card2bv_tactic(m, m_params), and_then(mk_card2bv_tactic(m, m_params),
using_params(mk_simplify_tactic(m), simp2_p), using_params(mk_simplify_tactic(m), simp2_p),

40
src/smt/mam.cpp
View file

@ -424,7 +424,7 @@ namespace smt {
out << *curr; out << *curr;
curr = curr->m_next; curr = curr->m_next;
while (curr != 0 && curr->m_opcode != CHOOSE && curr->m_opcode != NOOP) { while (curr != 0 && curr->m_opcode != CHOOSE && curr->m_opcode != NOOP) {
out << " "; out << "\n";
out << *curr; out << *curr;
curr = curr->m_next; curr = curr->m_next;
} }
@ -795,7 +795,8 @@ 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;
struct pcheck_checked { struct pcheck_checked {
func_decl * m_label; func_decl * m_label;
@ -952,6 +953,14 @@ namespace smt {
continue; 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) { if (m_use_filters && get_check_mark(reg) != CHECK_SINGLETON) {
func_decl * lbl = to_app(p)->get_decl(); func_decl * lbl = to_app(p)->get_decl();
approx_set s(m_lbl_hasher(lbl)); approx_set s(m_lbl_hasher(lbl));
@ -1106,7 +1115,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;
@ -1123,7 +1132,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();
@ -1216,13 +1225,16 @@ 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_matched_exprs.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++) {
@ -1311,9 +1323,6 @@ namespace smt {
unsigned reg2 = instr->m_reg2; unsigned reg2 = instr->m_reg2;
return return
m_registers[reg1] != 0 && m_registers[reg1] != 0 &&
m_registers[reg2] != 0 &&
is_var(m_registers[reg1]) &&
is_var(m_registers[reg2]) &&
m_registers[reg1] == m_registers[reg2]; m_registers[reg1] == m_registers[reg2];
} }
@ -1571,12 +1580,13 @@ namespace smt {
unsigned reg1 = static_cast<compare*>(curr)->m_reg1; unsigned reg1 = static_cast<compare*>(curr)->m_reg1;
unsigned reg2 = static_cast<compare*>(curr)->m_reg2; unsigned reg2 = static_cast<compare*>(curr)->m_reg2;
SASSERT(m_todo.contains(reg2)); SASSERT(m_todo.contains(reg2));
m_todo.erase(reg1);
m_todo.erase(reg2); m_todo.erase(reg2);
SASSERT(is_var(m_registers[reg1])); if (is_var(m_registers[reg1])) {
unsigned var_id = to_var(m_registers[reg1])->get_idx(); m_todo.erase(reg1);
if (m_vars[var_id] == -1) unsigned var_id = to_var(m_registers[reg1])->get_idx();
m_vars[var_id] = reg1; if (m_vars[var_id] == -1)
m_vars[var_id] = reg1;
}
m_compatible.push_back(curr); m_compatible.push_back(curr);
} }
else { else {