From 1e0c1cefd6e60d81dccaf4a222b2d8580cacbca9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Nov 2019 18:24:22 +0100 Subject: [PATCH] add definitions for under-specified cases of arithmetic operators #2663 #2676 #2679 Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 10 +++++++--- src/ast/arith_decl_plugin.h | 8 ++++++++ src/ast/ast_smt_pp.cpp | 2 +- src/model/model_evaluator.cpp | 3 +-- src/muz/base/dl_context.cpp | 10 +++++++++- src/muz/fp/dl_cmds.cpp | 1 - src/muz/spacer/spacer_context.cpp | 2 +- src/smt/params/theory_array_params.cpp | 2 +- src/smt/smt_context.cpp | 1 + src/smt/smt_context.h | 5 +++-- src/smt/smt_enode.h | 4 ++++ src/smt/theory_arith_core.h | 22 ++++++++++++++-------- src/tactic/arith/purify_arith_tactic.cpp | 9 +++++++++ 13 files changed, 59 insertions(+), 20 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 75aa96717..41cdc0658 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -362,7 +362,7 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) { case OP_IDIVIDES: UNREACHABLE(); case OP_REM: return m_i_rem_decl; case OP_MOD: return m_i_mod_decl; - case OP_DIV0: return m_manager->mk_func_decl(symbol("div0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_DIV0)); + case OP_DIV0: return m_manager->mk_func_decl(symbol("/0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_DIV0)); case OP_IDIV0: return m_manager->mk_func_decl(symbol("idiv0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_IDIV0)); case OP_REM0: return m_manager->mk_func_decl(symbol("rem0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_REM0)); case OP_MOD0: return m_manager->mk_func_decl(symbol("mod0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_MOD0)); @@ -788,8 +788,7 @@ expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) { bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out) { rational r; if (is_decl_of(f, m_afid, OP_DIV) && is_numeral(args[1], r) && r.is_zero()) { - sort* rs[2] = { mk_real(), mk_real() }; - f_out = m_manager.mk_func_decl(m_afid, OP_DIV0, 0, nullptr, 2, rs, mk_real()); + f_out = mk_div0(); return true; } if (is_decl_of(f, m_afid, OP_IDIV) && is_numeral(args[1], r) && r.is_zero()) { @@ -814,3 +813,8 @@ bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* con } return plugin().is_considered_uninterpreted(f); } + +func_decl* arith_util::mk_div0() { + sort* rs[2] = { mk_real(), mk_real() }; + return m_manager.mk_func_decl(m_afid, OP_DIV0, 0, nullptr, 2, rs, mk_real()); +} diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 92ea35b0b..0bc572feb 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -213,6 +213,11 @@ public: case OP_NEG_ROOT: case OP_U_ASIN: case OP_U_ACOS: + case OP_DIV0: + case OP_IDIV0: + case OP_REM0: + case OP_MOD0: + case OP_POWER0: return true; default: return false; @@ -362,6 +367,9 @@ public: sort * mk_int() { return m_manager.mk_sort(m_afid, INT_SORT); } sort * mk_real() { return m_manager.mk_sort(m_afid, REAL_SORT); } + func_decl* mk_div0(); + + app * mk_numeral(rational const & val, bool is_int) const { return plugin().mk_numeral(val, is_int); } diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 2785eb1fa..c0c62c379 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -841,7 +841,7 @@ public: else { m_out << "(declare-sort "; visit_sort(s); - m_out << ")"; + m_out << " 0)"; newline(); } mark.mark(s, true); diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 708a136af..3764089a9 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -334,11 +334,10 @@ struct evaluator_cfg : public default_rewriter_cfg { func_interp * fi = m_model.get_func_interp(f); - func_decl_ref f_ui(m); if (!fi && m_au.is_considered_uninterpreted(f, num, args, f_ui)) { if (f_ui) { - fi = m_model.get_func_interp(f); + fi = m_model.get_func_interp(f_ui); } if (!fi) { result = m_au.mk_numeral(rational(0), f->get_range()); diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index ccbed6b70..35fc9d2f1 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -765,10 +765,15 @@ namespace datalog { ast_manager& m; arith_util a; datatype_util dt; + bv_util bv; DL_ENGINE m_engine_type; + bool is_large_bv(sort* s) { + return false; + } + public: - engine_type_proc(ast_manager& m): m(m), a(m), dt(m), m_engine_type(DATALOG_ENGINE) {} + engine_type_proc(ast_manager& m): m(m), a(m), dt(m), bv(m), m_engine_type(DATALOG_ENGINE) {} DL_ENGINE get_engine() const { return m_engine_type; } @@ -782,6 +787,9 @@ namespace datalog { else if (dt.is_datatype(m.get_sort(e))) { m_engine_type = SPACER_ENGINE; } + else if (is_large_bv(m.get_sort(e))) { + m_engine_type = SPACER_ENGINE; + } } }; diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index 651509bd8..707417279 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -305,7 +305,6 @@ public: case datalog::OK: (void)query_exn; - SASSERT(query_exn); break; case datalog::CANCELED: diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 772f58ed3..7a964b8a8 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -3800,6 +3800,7 @@ bool context::create_children(pob& n, datalog::rule const& r, void context::collect_statistics(statistics& st) const { + // m_params is not necessarily live when collect_statistics is called. m_pool0->collect_statistics(st); m_pool1->collect_statistics(st); m_pool2->collect_statistics(st); @@ -3841,7 +3842,6 @@ void context::collect_statistics(statistics& st) const // -- time in creating new predecessors st.update ("time.spacer.solve.reach.children", m_create_children_watch.get_seconds ()); - st.update("spacer.random_seed", m_params.spacer_random_seed()); st.update("spacer.lemmas_imported", m_stats.m_num_lemmas_imported); st.update("spacer.lemmas_discarded", m_stats.m_num_lemmas_discarded); diff --git a/src/smt/params/theory_array_params.cpp b/src/smt/params/theory_array_params.cpp index 9a9e5aa7b..892edb4ad 100644 --- a/src/smt/params/theory_array_params.cpp +++ b/src/smt/params/theory_array_params.cpp @@ -37,4 +37,4 @@ void theory_array_params::display(std::ostream & out) const { DISPLAY_PARAM(m_array_always_prop_upward); DISPLAY_PARAM(m_array_lazy_ieq); DISPLAY_PARAM(m_array_lazy_ieq_delay); -} \ No newline at end of file +} diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index d47e8dde3..bdd847598 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3318,6 +3318,7 @@ namespace smt { \brief Execute some finalization code after performing the search. */ lbool context::check_finalize(lbool r) { + if (r == l_undef) std::cout << m_unknown << "\n"; TRACE("after_search", display(tout << "result: " << r << "\n");); display_profile(verbose_stream()); if (r == l_true && get_cancel_flag()) { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index c651e933d..e0bd2b876 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -74,7 +74,7 @@ namespace smt { std::ostream& display_last_failure(std::ostream& out) const; std::string last_failure_as_string() const; - void set_reason_unknown(char const* msg) { m_unknown = msg; } + void set_reason_unknown(char const* msg) { m_unknown = msg; std::cout << m_unknown << "\n"; } void set_progress_callback(progress_callback *callback); @@ -1009,6 +1009,8 @@ namespace smt { } #endif + void add_eq(enode * n1, enode * n2, eq_justification js); + protected: void push_new_th_eq(theory_id th, theory_var lhs, theory_var rhs); @@ -1016,7 +1018,6 @@ namespace smt { friend class add_eq_trail; - void add_eq(enode * n1, enode * n2, eq_justification js); void remove_parents_from_cg_table(enode * r1); diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index f7dfda83b..58b14c811 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -201,6 +201,10 @@ namespace smt { return m_root; } + void set_root(enode* r) { + m_root = r; + } + enode * get_next() const { return m_next; } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 0fe92e325..a7f5db33d 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -19,12 +19,12 @@ Revision History: #ifndef THEORY_ARITH_CORE_H_ #define THEORY_ARITH_CORE_H_ -#include "smt/smt_context.h" -#include "smt/theory_arith.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" -#include "smt/smt_model_generator.h" #include "ast/ast_smt2_pp.h" +#include "smt/smt_context.h" +#include "smt/theory_arith.h" +#include "smt/smt_model_generator.h" namespace smt { @@ -3266,6 +3266,7 @@ namespace smt { template void theory_arith::init_model(model_generator & m) { TRACE("theory_arith", tout << "init model invoked...\n";); + context& ctx = get_context(); m_factory = alloc(arith_factory, get_manager()); m.register_factory(m_factory); compute_epsilon(); @@ -3273,20 +3274,25 @@ namespace smt { refine_epsilon(); } for (app* n : m_underspecified_ops) { + enode* e = nullptr; if (m_util.is_div(n)) { - mk_enode(m_util.mk_div0(n->get_arg(0), n->get_arg(1))); + e = mk_enode(m_util.mk_div0(n->get_arg(0), n->get_arg(1))); } else if (m_util.is_idiv(n)) { - mk_enode(m_util.mk_idiv0(n->get_arg(0), n->get_arg(1))); + e = mk_enode(m_util.mk_idiv0(n->get_arg(0), n->get_arg(1))); } else if (m_util.is_rem(n)) { - mk_enode(m_util.mk_rem0(n->get_arg(0), n->get_arg(1))); + e = mk_enode(m_util.mk_rem0(n->get_arg(0), n->get_arg(1))); } else if (m_util.is_mod(n)) { - mk_enode(m_util.mk_mod0(n->get_arg(0), n->get_arg(1))); + e = mk_enode(m_util.mk_mod0(n->get_arg(0), n->get_arg(1))); } else if (m_util.is_power(n)) { - mk_enode(m_util.mk_power0(n->get_arg(0), n->get_arg(1))); + e = mk_enode(m_util.mk_power0(n->get_arg(0), n->get_arg(1))); + } + if (e) { + ctx.mark_as_relevant(e); + ctx.add_eq(e, ctx.get_enode(n), eq_justification()); } } } diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 3d993392c..5bb26dfc7 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -795,6 +795,15 @@ struct purify_arith_proc { SASSERT(is_uninterp_const(v)); fmc->hide(v->get_decl()); } + if (!divs.empty()) { + expr_ref body(u().mk_real(0), m()); + expr_ref v0(m().mk_var(0, u().mk_real()), m()); + expr_ref v1(m().mk_var(1, u().mk_real()), m()); + for (auto const& p : divs) { + body = m().mk_ite(m().mk_and(m().mk_eq(v0, p.x), m().mk_eq(v1, p.y)), p.d, body); + } + fmc->add(u().mk_div0(), body); + } } if (produce_models && !m_sin_cos.empty()) { generic_model_converter* emc = alloc(generic_model_converter, m(), "purify_sin_cos");