From 4d9aadde351bb57c62db68e19f1d686a07260d0a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 31 Aug 2016 16:15:36 +0800 Subject: [PATCH] updated consequence finder to fix bug in processing enumeration types Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 1 + src/smt/smt_consequences.cpp | 147 ++++++++++++++++++++--------------- src/smt/smt_context.h | 1 + src/smt/theory_seq.cpp | 26 ++++++- src/smt/theory_seq.h | 2 + 5 files changed, 112 insertions(+), 65 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 418ccc58c..b6c3384e7 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -415,6 +415,7 @@ extern "C" { return; } mk_c(c)->m().dec_ref(to_ast(a)); + Z3_CATCH; } diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 922156d46..e71abf39d 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "smt_context.h" #include "ast_util.h" +#include "datatype_decl_plugin.h" namespace smt { @@ -31,74 +32,85 @@ namespace smt { return mk_and(premises); } - void context::extract_fixed_consequences(unsigned start, obj_map& vars, uint_set const& assumptions, expr_ref_vector& conseq) { + void context::extract_fixed_consequences(literal lit, obj_map& vars, uint_set const& assumptions, expr_ref_vector& conseq) { ast_manager& m = m_manager; + datatype_util dt(m); + expr* e1, *e2; + expr_ref fml(m); + if (lit == true_literal) return; + expr* e = bool_var2expr(lit.var()); + uint_set s; + if (assumptions.contains(lit.var())) { + s.insert(lit.var()); + } + else { + b_justification js = get_justification(lit.var()); + switch (js.get_kind()) { + case b_justification::CLAUSE: { + clause * cls = js.get_clause(); + unsigned num_lits = cls->get_num_literals(); + for (unsigned j = 0; j < num_lits; ++j) { + literal lit2 = cls->get_literal(j); + if (lit2.var() != lit.var()) { + s |= m_antecedents.find(lit2.var()); + } + } + break; + } + case b_justification::BIN_CLAUSE: { + s |= m_antecedents.find(js.get_literal().var()); + break; + } + case b_justification::AXIOM: { + break; + } + case b_justification::JUSTIFICATION: { + literal_vector literals; + m_conflict_resolution->justification2literals(js.get_justification(), literals); + for (unsigned j = 0; j < literals.size(); ++j) { + s |= m_antecedents.find(literals[j].var()); + } + break; + } + } + } + m_antecedents.insert(lit.var(), s); + TRACE("context", display_literal_verbose(tout, lit); tout << " " << s << "\n";); + bool found = false; + if (vars.contains(e)) { + found = true; + fml = lit.sign() ? m.mk_not(e) : e; + vars.erase(e); + } + else if (!lit.sign() && m.is_eq(e, e1, e2)) { + if (vars.contains(e2)) { + std::swap(e1, e2); + } + if (vars.contains(e1) && m.is_value(e2)) { + found = true; + fml = e; + vars.erase(e1); + } + } + else if (!lit.sign() && is_app(e) && dt.is_recognizer(to_app(e)->get_decl())) { + if (vars.contains(to_app(e)->get_arg(0))) { + found = true; + fml = m.mk_eq(to_app(e)->get_arg(0), m.mk_const(dt.get_recognizer_constructor(to_app(e)->get_decl()))); + vars.erase(to_app(e)->get_arg(0)); + } + } + if (found) { + fml = m.mk_implies(antecedent2fml(s), fml); + conseq.push_back(fml); + } + } + + void context::extract_fixed_consequences(unsigned start, obj_map& vars, uint_set const& assumptions, expr_ref_vector& conseq) { pop_to_search_lvl(); literal_vector const& lits = assigned_literals(); unsigned sz = lits.size(); - expr* e1, *e2; - expr_ref fml(m); for (unsigned i = start; i < sz; ++i) { - literal lit = lits[i]; - if (lit == true_literal) continue; - expr* e = bool_var2expr(lit.var()); - uint_set s; - if (assumptions.contains(lit.var())) { - s.insert(lit.var()); - } - else { - b_justification js = get_justification(lit.var()); - switch (js.get_kind()) { - case b_justification::CLAUSE: { - clause * cls = js.get_clause(); - unsigned num_lits = cls->get_num_literals(); - for (unsigned j = 0; j < num_lits; ++j) { - literal lit2 = cls->get_literal(j); - if (lit2.var() != lit.var()) { - s |= m_antecedents.find(lit2.var()); - } - } - break; - } - case b_justification::BIN_CLAUSE: { - s |= m_antecedents.find(js.get_literal().var()); - break; - } - case b_justification::AXIOM: { - break; - } - case b_justification::JUSTIFICATION: { - literal_vector literals; - m_conflict_resolution->justification2literals(js.get_justification(), literals); - for (unsigned j = 0; j < literals.size(); ++j) { - s |= m_antecedents.find(literals[j].var()); - } - break; - } - } - } - m_antecedents.insert(lit.var(), s); - TRACE("context", display_literal_verbose(tout, lit); tout << " " << s << "\n";); - bool found = false; - if (vars.contains(e)) { - found = true; - fml = lit.sign()?m.mk_not(e):e; - vars.erase(e); - } - else if (!lit.sign() && m.is_eq(e, e1, e2)) { - if (vars.contains(e2)) { - std::swap(e1, e2); - } - if (vars.contains(e1) && m.is_value(e2)) { - found = true; - fml = e; - vars.erase(e1); - } - } - if (found) { - fml = m.mk_implies(antecedent2fml(s), fml); - conseq.push_back(fml); - } + extract_fixed_consequences(lits[i], vars, assumptions, conseq); } } @@ -240,6 +252,7 @@ namespace smt { lit = literal(get_bool_var(e), m.is_true(val)); } else { + TRACE("context", tout << mk_pp(e, m) << " " << mk_pp(val, m) << "\n";); eq = mk_eq_atom(e, val); internalize_formula(eq, false); lit = literal(get_bool_var(eq), true); @@ -259,9 +272,10 @@ namespace smt { } break; } - if (get_assignment(lit) == l_true) { + if (is_sat == l_true && get_assignment(lit) == l_true) { var2val.erase(e); unfixed.push_back(e); + TRACE("context", tout << mk_pp(e, m) << " is unfixed\n";); } else if (get_assign_level(lit) > get_search_level()) { TRACE("context", tout << "Retry fixing: " << mk_pp(e, m) << "\n";); @@ -305,10 +319,15 @@ namespace smt { << " unfixed-deleted: " << num_unfixed << ")\n";); } + TRACE("context", tout << "finishing " << mk_pp(e, m) << "\n";); if (var2val.contains(e)) { TRACE("context", tout << "Fixed value to " << mk_pp(e, m) << " was not processed\n";); expr_ref fml(m); fml = m.mk_eq(e, var2val.find(e)); + if (!m_antecedents.contains(lit.var())) + { + extract_fixed_consequences(lit, var2val, _assumptions, conseq); + } fml = m.mk_implies(antecedent2fml(m_antecedents[lit.var()]), fml); conseq.push_back(fml); var2val.erase(e); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 48f6004e9..1a5952305 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1345,6 +1345,7 @@ namespace smt { vector b2v, ast_translation& tr); u_map m_antecedents; + void extract_fixed_consequences(literal lit, obj_map& var2val, uint_set const& assumptions, expr_ref_vector& conseq); void extract_fixed_consequences(unsigned idx, obj_map& var2val, uint_set const& assumptions, expr_ref_vector& conseq); unsigned delete_unfixed(obj_map& var2val, expr_ref_vector& unfixed); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 6a2208ad4..5b862b2d1 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -249,6 +249,7 @@ final_check_status theory_seq::final_check_eh() { } m_new_propagation = false; TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n");); + TRACE("seq_verbose", get_context().display(tout);); if (simplify_and_solve_eqs()) { ++m_stats.m_solve_eqs; TRACE("seq", tout << ">>solve_eqs\n";); @@ -1009,6 +1010,17 @@ bool theory_seq::is_nth(expr* e) const { return is_skolem(m_nth, e); } +bool theory_seq::is_nth(expr* e, expr*& e1, expr*& e2) const { + if (is_nth(e)) { + e1 = to_app(e)->get_arg(0); + e2 = to_app(e)->get_arg(1); + return true; + } + else { + return false; + } +} + bool theory_seq::is_tail(expr* e, expr*& s, unsigned& idx) const { rational r; return @@ -1038,6 +1050,10 @@ expr_ref theory_seq::mk_nth(expr* s, expr* idx) { return mk_skolem(m_nth, s, idx, 0, char_sort); } +expr_ref theory_seq::mk_sk_ite(expr* c, expr* t, expr* e) { + return mk_skolem(symbol("seq.if"), c, t, e, m.get_sort(t)); +} + expr_ref theory_seq::mk_last(expr* s) { zstring str; if (m_util.str.is_string(s, str) && str.length() > 0) { @@ -1133,7 +1149,7 @@ bool theory_seq::check_extensionality() { continue; } TRACE("seq", tout << m_lhs << " = " << m_rhs << "\n";); - ctx.assume_eq(n1, n2); + ctx.assume_eq(n1, n2); return false; } } @@ -2668,6 +2684,13 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) { } else if (m.is_ite(e, e1, e2, e3)) { literal lit(mk_literal(e1)); +#if 0 + expr_ref sk_ite = mk_sk_ite(e1, e2, e3); + add_axiom(~lit, mk_eq(e2, sk_ite, false)); + add_axiom( lit, mk_eq(e3, sk_ite, false)); + result = sk_ite; + +#else switch (ctx.get_assignment(lit)) { case l_true: deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit))); @@ -2684,6 +2707,7 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) { tout << lit << "@ level: " << ctx.get_scope_level() << "\n";); break; } +#endif } else if (m_util.str.is_itos(e, e1)) { rational val; diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 187573623..21955bf30 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -449,10 +449,12 @@ namespace smt { bool is_var(expr* b); bool add_solution(expr* l, expr* r, dependency* dep); bool is_nth(expr* a) const; + bool is_nth(expr* a, expr*& e1, expr*& e2) const; bool is_tail(expr* a, expr*& s, unsigned& idx) const; bool is_eq(expr* e, expr*& a, expr*& b) const; bool is_pre(expr* e, expr*& s, expr*& i); bool is_post(expr* e, expr*& s, expr*& i); + expr_ref mk_sk_ite(expr* c, expr* t, expr* f); expr_ref mk_nth(expr* s, expr* idx); expr_ref mk_last(expr* e); expr_ref mk_first(expr* e);