From 1ec977930a534b83a40d658991b42ca35617021e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Apr 2020 10:10:07 -0700 Subject: [PATCH] fix #3972 regression from changing the way assumptions are initialized Signed-off-by: Nikolaj Bjorner --- src/smt/expr_context_simplifier.cpp | 32 +++++++---------------------- src/smt/smt_context.cpp | 31 ++++++++++++++++------------ src/smt/theory_seq.cpp | 15 +++++++------- src/smt/theory_seq.h | 3 +-- 4 files changed, 33 insertions(+), 48 deletions(-) diff --git a/src/smt/expr_context_simplifier.cpp b/src/smt/expr_context_simplifier.cpp index 9efae9b89..fe733f897 100644 --- a/src/smt/expr_context_simplifier.cpp +++ b/src/smt/expr_context_simplifier.cpp @@ -81,29 +81,11 @@ void expr_context_simplifier::reduce_rec(expr * m, expr_ref & result) { void expr_context_simplifier::reduce_rec(quantifier* q, expr_ref & result) { result = q; - -#if 0 - // - // The context assumes that asserted expressions are in NNF with - // respect to the quantifier occurrences. - // This can be disabled if the strong context simplifier - // is called from the API over the Z3_simplify method. - // - expr_context_simplifier nested(m_manager); - expr_ref body_r(m_manager); - nested.reduce(q->get_expr(), body_r); - if (body_r.get() != q->get_expr()) { - result = m_manager.update_quantifier(q, body_r.get()); - } - else { - result = q; - } -#endif } void expr_context_simplifier::reduce_rec(app * a, expr_ref & result) { if (m_manager.get_basic_family_id() == a->get_family_id()) { - switch(a->get_decl_kind()) { + switch (a->get_decl_kind()) { case OP_AND: reduce_and(a->get_num_args(), a->get_args(), result); return; @@ -168,18 +150,18 @@ void expr_context_simplifier::reduce_rec(app * a, expr_ref & result) { } expr_ref_vector args(m_manager); - for (unsigned i = 0; i < a->get_num_args(); ++i) { + for (expr* arg : *a) { expr_ref tmp(m_manager); - reduce_rec(a->get_arg(i), tmp); + reduce_rec(arg, tmp); args.push_back(tmp.get()); } - result = m_manager.mk_app(a->get_decl(), args.size(), args.c_ptr()); + result = m_manager.mk_app(a->get_decl(), args); } void expr_context_simplifier::clean_trail(unsigned old_lim) { for (unsigned i = m_trail.size(); i > old_lim; ) { --i; - m_context.erase(m_trail[i].get()); + m_context.erase(m_trail.get(i)); } m_trail.resize(old_lim); } @@ -436,7 +418,7 @@ void expr_strong_context_simplifier::simplify_basic(expr* fml, expr_ref& result) args.push_back(arg); } } - r = m.mk_app(a->get_decl(), args.size(), args.c_ptr()); + r = m.mk_app(a->get_decl(), args); trail.push_back(r); if (n2) { m_solver.push(); @@ -712,7 +694,7 @@ void expr_strong_context_simplifier::simplify_model_based(expr* fml, expr_ref& r args.push_back(arg); } } - r = m.mk_app(a->get_decl(), args.size(), args.c_ptr()); + r = m.mk_app(a->get_decl(), args); trail.push_back(r); if (n2) { m_solver.push(); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index c94300387..b8e1ab721 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3025,17 +3025,21 @@ namespace smt { } } - static bool is_valid_assumption(ast_manager & m, expr * assumption) { + static bool is_valid_assumption(ast_manager & m, expr * a) { expr* arg; - if (!m.is_bool(assumption)) + if (!m.is_bool(a)) return false; - if (is_uninterp_const(assumption)) + if (is_uninterp_const(a)) return true; - if (m.is_not(assumption, arg) && is_uninterp_const(arg)) + if (m.is_not(a, arg) && is_uninterp_const(arg)) return true; - if (!is_app(assumption)) + if (!is_app(a)) return false; - if (m.is_true(assumption) || m.is_false(assumption)) + if (m.is_true(a) || m.is_false(a)) + return true; + if (is_app(a) && to_app(a)->get_family_id() == m.get_basic_family_id()) + return false; + if (is_app(a) && to_app(a)->get_num_args() == 0) return true; return false; } @@ -3192,6 +3196,8 @@ namespace smt { vector> asm2proxy; internalize_proxies(asms, asm2proxy); for (auto const& p: asm2proxy) { + if (inconsistent()) + break; expr_ref curr_assumption = p.second; expr* orig_assumption = p.first; if (m.is_true(curr_assumption)) continue; @@ -3199,17 +3205,16 @@ namespace smt { proof * pr = m.mk_asserted(curr_assumption); internalize_assertion(curr_assumption, pr, 0); literal l = get_literal(curr_assumption); - if (l == true_literal) + SASSERT(get_assignment(l) != l_undef); + SASSERT(l != false_literal || inconsistent()); + if (l == true_literal || l == false_literal) { continue; - if (inconsistent()) - break; - SASSERT(get_assignment(l) == l_true); + } m_literal2assumption.insert(l.index(), orig_assumption); - // internalize_assertion marked l as relevant. - SASSERT(is_relevant(l)); - TRACE("assumptions", tout << l << ":" << curr_assumption << " " << mk_pp(orig_assumption, m) << "\n";); m_assumptions.push_back(l); get_bdata(l.var()).m_assumption = true; + SASSERT(is_relevant(l)); + TRACE("assumptions", tout << l << ":" << curr_assumption << " " << mk_pp(orig_assumption, m) << "\n";); } } m_search_lvl = m_scope_lvl; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 44bb74dea..0aab00b23 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -4610,7 +4610,7 @@ expr_ref theory_seq::elim_skolem(expr* e) { } todo.pop_back(); - result = m.mk_app(to_app(a)->get_decl(), args.size(), args.c_ptr()); + result = m.mk_app(to_app(a)->get_decl(), args); trail.push_back(result); cache.insert(a, result); } @@ -4618,7 +4618,6 @@ expr_ref theory_seq::elim_skolem(expr* e) { } void theory_seq::validate_axiom(literal_vector const& lits) { - return; if (get_context().get_fparams().m_seq_validate) { enode_pair_vector eqs; literal_vector _lits; @@ -4744,7 +4743,7 @@ bool theory_seq::canonize(expr* e, expr_ref_vector& es, dependency*& eqs, bool& return false; } change |= e4 != e3; - m_util.str.get_concat_units(e4, es); + m_util.str.get_concat(e4, es); break; } } @@ -4793,9 +4792,12 @@ expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){ } bool theory_seq::expand1(expr* e0, dependency*& eqs, expr_ref& result) { result = try_expand(e0, eqs); - if (result) return true; + if (result) { + return true; + } dependency* deps = nullptr; expr* e = m_rep.find(e0, deps); + expr* e1, *e2, *e3; expr_ref arg1(m), arg2(m); context& ctx = get_context(); @@ -4870,9 +4872,6 @@ bool theory_seq::expand1(expr* e0, dependency*& eqs, expr_ref& result) { return false; } } - else if (m_util.str.is_itos(e, e1)) { - result = e; - } else { result = e; } @@ -5905,7 +5904,7 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2, expr* e3, expr*e4, sort* range) { expr* es[4] = { e1, e2, e3, e4 }; - unsigned len = e4?4:(e3?3:(e2?2:1)); + unsigned len = e4?4:(e3?3:(e2?2:(e1?1:0))); if (!range) { range = m.get_sort(e1); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 793a228dc..4427c9a92 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -696,8 +696,7 @@ namespace smt { bool is_step(expr* e) const; bool is_max_unfolding(expr* e) const { return is_skolem(symbol("seq.max_unfolding_depth"), e); } expr_ref mk_max_unfolding_depth() { - return mk_skolem(symbol("seq.max_unfolding_depth"), - m_autil.mk_int(m_max_unfolding_depth), + return mk_skolem(symbol("seq.max_unfolding_depth"), m_autil.mk_int(m_max_unfolding_depth), nullptr, nullptr, nullptr, m.mk_bool_sort()); } void propagate_not_prefix(expr* e);