From 0cf401c67bc980669bcb844be4e5008c8ed07154 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Mar 2020 17:27:10 -0700 Subject: [PATCH] fix #3458 Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.h | 29 ++++++++++++++++++++++------- src/cmd_context/cmd_context.cpp | 23 ++++++++++++++++------- src/solver/tactic2solver.cpp | 19 ++++++++++++++----- 3 files changed, 52 insertions(+), 19 deletions(-) diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 3e7cb58ab..20a474d8b 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -306,14 +306,29 @@ public: bool is_sin(expr const* n) const { return is_app_of(n, m_afid, OP_SIN); } bool is_cos(expr const* n) const { return is_app_of(n, m_afid, OP_COS); } bool is_tan(expr const* n) const { return is_app_of(n, m_afid, OP_TAN); } + bool is_tanh(expr const* n) const { return is_app_of(n, m_afid, OP_TANH); } bool is_asin(expr const* n) const { return is_app_of(n, m_afid, OP_ASIN); } bool is_acos(expr const* n) const { return is_app_of(n, m_afid, OP_ACOS); } bool is_atan(expr const* n) const { return is_app_of(n, m_afid, OP_ATAN); } bool is_asinh(expr const* n) const { return is_app_of(n, m_afid, OP_ASINH); } bool is_acosh(expr const* n) const { return is_app_of(n, m_afid, OP_ACOSH); } bool is_atanh(expr const* n) const { return is_app_of(n, m_afid, OP_ATANH); } - bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); } - bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); } + bool is_pi(expr const * arg) const { return is_app_of(arg, m_afid, OP_PI); } + bool is_e(expr const * arg) const { return is_app_of(arg, m_afid, OP_E); } + bool is_non_algebraic(expr const* n) const { + return is_sin(n) || + is_cos(n) || + is_tan(n) || + is_tanh(n) || + is_asin(n) || + is_acos(n) || + is_atan(n) || + is_asinh(n) || + is_acosh(n) || + is_atanh(n) || + is_e(n) || + is_pi(n); + } MATCH_UNARY(is_uminus); MATCH_UNARY(is_to_real); @@ -350,17 +365,17 @@ class arith_util : public arith_recognizers { void init_plugin(); +public: + arith_util(ast_manager & m); + + ast_manager & get_manager() const { return m_manager; } + arith_decl_plugin & plugin() const { if (!m_plugin) const_cast(this)->init_plugin(); SASSERT(m_plugin != 0); return *m_plugin; } -public: - arith_util(ast_manager & m); - - ast_manager & get_manager() const { return m_manager; } - algebraic_numbers::manager & am() { return plugin().am(); } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 787b7a8a2..32347638e 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1775,14 +1775,26 @@ struct contains_underspecified_op_proc { struct found {}; family_id m_array_fid; datatype_util m_dt; + arith_util m_arith; seq_util m_seq; family_id m_seq_id; - contains_underspecified_op_proc(ast_manager & m):m_array_fid(m.mk_family_id("array")), m_dt(m), m_seq(m), m_seq_id(m_seq.get_family_id()) {} + contains_underspecified_op_proc(ast_manager & m): + m_array_fid(m.mk_family_id("array")), + m_dt(m), + m_arith(m), + m_seq(m), + m_seq_id(m_seq.get_family_id()) {} void operator()(var * n) {} void operator()(app * n) { if (m_dt.is_accessor(n->get_decl())) throw found(); + if (n->get_family_id() == m_seq_id && m_seq.is_re(n)) + throw found(); + if (m_arith.plugin().is_considered_uninterpreted(n->get_decl())) + throw found(); + if (m_arith.is_non_algebraic(n)) + throw found(); if (n->get_family_id() == m_array_fid) { decl_kind k = n->get_decl_kind(); if (k == OP_AS_ARRAY || @@ -1791,9 +1803,6 @@ struct contains_underspecified_op_proc { k == OP_CONST_ARRAY) throw found(); } - if (n->get_family_id() == m_seq_id && m_seq.is_re(n)) { - throw found(); - } } void operator()(quantifier * n) {} }; @@ -1896,9 +1905,6 @@ void cmd_context::validate_model() { if (m().is_true(r)) continue; - analyze_failure(evaluator, a, true); - IF_VERBOSE(11, model_smt2_pp(verbose_stream(), *this, *md, 0);); - // The evaluator for array expressions is not complete // If r contains as_array/store/map/const expressions, then we do not generate the error. // TODO: improve evaluator for model expressions. @@ -1913,6 +1919,9 @@ void cmd_context::validate_model() { catch (const contains_underspecified_op_proc::found &) { continue; } + + analyze_failure(evaluator, a, true); + IF_VERBOSE(11, model_smt2_pp(verbose_stream(), *this, *md, 0);); TRACE("model_validate", model_smt2_pp(tout, *this, *md, 0);); invalid_model = true; } diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index c286c1224..041ae32cd 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -36,6 +36,8 @@ Notes: namespace { class tactic2solver : public solver_na2as { expr_ref_vector m_assertions; + expr_ref_vector m_last_assertions; + unsigned m_last_assertions_valid; unsigned_vector m_scopes; ref m_result; tactic_ref m_tactic; @@ -101,7 +103,9 @@ ast_manager& tactic2solver::get_manager() const { return m_assertions.get_manage tactic2solver::tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic): solver_na2as(m), - m_assertions(m) { + m_assertions(m), + m_last_assertions(m), + m_last_assertions_valid(false) { m_tactic = t; m_logic = logic; @@ -126,18 +130,21 @@ void tactic2solver::collect_param_descrs(param_descrs & r) { } void tactic2solver::assert_expr_core(expr * t) { + m_last_assertions_valid = false; m_assertions.push_back(t); m_result = nullptr; } void tactic2solver::push_core() { + m_last_assertions_valid = false; m_scopes.push_back(m_assertions.size()); m_result = nullptr; TRACE("pop", tout << m_scopes.size() << "\n";); } void tactic2solver::pop_core(unsigned n) { + m_last_assertions_valid = false; TRACE("pop", tout << m_scopes.size() << " " << n << "\n";); n = std::min(m_scopes.size(), n); unsigned new_lvl = m_scopes.size() - n; @@ -150,6 +157,7 @@ void tactic2solver::pop_core(unsigned n) { lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * assumptions) { if (m_tactic.get() == nullptr) return l_false; + m_last_assertions_valid = false; ast_manager & m = m_assertions.m(); m_result = alloc(simple_check_sat_result, m); m_tactic->cleanup(); @@ -185,8 +193,9 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as if (!reason_unknown.empty()) m_result->m_unknown = reason_unknown; if (num_assumptions == 0 && m_scopes.empty()) { - m_assertions.reset(); - g->get_formulas(m_assertions); + m_last_assertions.reset(); + g->get_formulas(m_last_assertions); + m_last_assertions_valid = true; } break; } @@ -278,11 +287,11 @@ void tactic2solver::set_reason_unknown(char const* msg) { } unsigned tactic2solver::get_num_assertions() const { - return m_assertions.size(); + return m_last_assertions_valid ? m_last_assertions.size() : m_assertions.size(); } expr * tactic2solver::get_assertion(unsigned idx) const { - return m_assertions.get(idx); + return m_last_assertions_valid ? m_last_assertions.get(idx) : m_assertions.get(idx); } }