mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 13:51:23 +00:00
Code Activity

take conflicts during restart into account. reported by Arie Gurfinkel

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-02-21 02:08:00 -08:00
parent 911ffc370a
commit 49483fdc28
3 changed files with 31 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/ast/simplifier/array_simplifier_plugin.cpp
View file

@ -327,16 +327,20 @@ void array_simplifier_plugin::get_stores(expr* n, unsigned& arity, expr*& m, ptr
} }
lbool array_simplifier_plugin::eq_default(expr* def, unsigned arity, unsigned num_st, expr*const* const* st) { lbool array_simplifier_plugin::eq_default(expr* def, unsigned arity, unsigned num_st, expr*const* const* st) {
bool all_diseq = m_manager.is_unique_value(def) && num_st > 0;
bool all_eq = true;
for (unsigned i = 0; i < num_st; ++i) { for (unsigned i = 0; i < num_st; ++i) {
if (st[i][arity] == def) { all_eq &= (st[i][arity] == def);
continue; all_diseq &= m_manager.is_unique_value(st[i][arity]) && (st[i][arity] != def);
} TRACE("array_simplifier", tout << m_manager.is_unique_value(st[i][arity]) << " " << mk_pp(st[i][arity], m_manager) << "\n";);
if (m_manager.is_unique_value(st[i][arity]) && m_manager.is_unique_value(def)) {
return l_false;
}
return l_undef;
} }
return l_true; if (all_eq) {
return l_true;
}
if (all_diseq) {
return l_false;
}
return l_undef;
} }
bool array_simplifier_plugin::insert_table(expr* def, unsigned arity, unsigned num_st, expr*const* const* st, arg_table& table) { bool array_simplifier_plugin::insert_table(expr* def, unsigned arity, unsigned num_st, expr*const* const* st, arg_table& table) {
@ -346,6 +350,12 @@ bool array_simplifier_plugin::insert_table(expr* def, unsigned arity, unsigned n
return false; return false;
} }
} }
TRACE("array_simplifier", tout << "inserting: ";
for (unsigned j = 0; j < arity; ++j) {
tout << mk_pp(st[i][j], m_manager) << " ";
}
tout << " |-> " << mk_pp(def, m_manager) << "\n";
);
args_entry e(arity, st[i]); args_entry e(arity, st[i]);
table.insert_if_not_there(e); table.insert_if_not_there(e);
} }
@ -419,7 +429,8 @@ bool array_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & resul
lbool eq = eq_stores(c1, arity, st1.size(), st1.c_ptr(), st2.size(), st2.c_ptr()); lbool eq = eq_stores(c1, arity, st1.size(), st1.c_ptr(), st2.size(), st2.c_ptr());
TRACE("array_simplifier", TRACE("array_simplifier",
tout << mk_pp(lhs, m_manager) << " = " tout << mk_pp(lhs, m_manager) << " = "
<< mk_pp(rhs, m_manager) << " := " << eq << "\n";); << mk_pp(rhs, m_manager) << " := " << eq << "\n";
tout << "arity: " << arity << "\n";);
switch(eq) { switch(eq) {
case l_false: case l_false:
result = m_manager.mk_false(); result = m_manager.mk_false();

3
src/smt/arith_eq_adapter.cpp
View file

@ -287,12 +287,13 @@ namespace smt {
} }
void arith_eq_adapter::restart_eh() { void arith_eq_adapter::restart_eh() {
context & ctx = get_context();
TRACE("arith_eq_adapter", tout << "restart\n";); TRACE("arith_eq_adapter", tout << "restart\n";);
svector<enode_pair> tmp(m_restart_pairs); svector<enode_pair> tmp(m_restart_pairs);
svector<enode_pair>::iterator it = tmp.begin(); svector<enode_pair>::iterator it = tmp.begin();
svector<enode_pair>::iterator end = tmp.end(); svector<enode_pair>::iterator end = tmp.end();
m_restart_pairs.reset(); m_restart_pairs.reset();
for (; it != end; ++it) { for (; it != end && !ctx.inconsistent(); ++it) {
TRACE("arith_eq_adapter", tout << "creating arith_eq_adapter axioms at the base level #" << it->first->get_owner_id() << " #" << TRACE("arith_eq_adapter", tout << "creating arith_eq_adapter axioms at the base level #" << it->first->get_owner_id() << " #" <<
it->second->get_owner_id() << "\n";); it->second->get_owner_id() << "\n";);
mk_axioms(it->first, it->second); mk_axioms(it->first, it->second);

11
src/smt/smt_context.cpp
View file

@ -3236,10 +3236,17 @@ namespace smt {
} }
ptr_vector<theory>::iterator it = m_theory_set.begin(); ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end(); ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) for (; it != end && !inconsistent(); ++it)
(*it)->restart_eh(); (*it)->restart_eh();
TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";); TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";);
m_qmanager->restart_eh(); if (!inconsistent()) {
m_qmanager->restart_eh();
}
if (inconsistent()) {
VERIFY(!resolve_conflict());
status = l_false;
break;
}
} }
if (m_fparams.m_simplify_clauses) if (m_fparams.m_simplify_clauses)
simplify_clauses(); simplify_clauses();