diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index f372b9b6fe8..75aa96717de 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -362,6 +362,11 @@ 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_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)); + case OP_POWER0: return m_manager->mk_func_decl(symbol("power0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_POWER0)); case OP_TO_REAL: return m_to_real_decl; case OP_TO_INT: return m_to_int_decl; case OP_IS_INT: return m_is_int_decl; @@ -780,18 +785,31 @@ expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) { return result; } -bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, 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()); return true; } if (is_decl_of(f, m_afid, OP_IDIV) && 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_IDIV0, 0, nullptr, 2, rs, mk_real()); return true; } if (is_decl_of(f, m_afid, OP_MOD) && 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_MOD0, 0, nullptr, 2, rs, mk_real()); return true; } if (is_decl_of(f, m_afid, OP_REM) && 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_REM0, 0, nullptr, 2, rs, mk_real()); + return true; + } + if (is_decl_of(f, m_afid, OP_POWER) && is_numeral(args[1], r) && r.is_zero() && is_numeral(args[0], r) && r.is_zero()) { + sort* rs[2] = { mk_real(), mk_real() }; + f_out = m_manager.mk_func_decl(m_afid, OP_POWER0, 0, nullptr, 2, rs, mk_real()); return true; } return plugin().is_considered_uninterpreted(f); diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 64973f7d13d..92ea35b0b27 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -46,14 +46,19 @@ enum arith_op_kind { OP_MUL, OP_DIV, OP_IDIV, + OP_DIV0, + OP_IDIV0, OP_IDIVIDES, OP_REM, OP_MOD, + OP_REM0, + OP_MOD0, OP_TO_REAL, OP_TO_INT, OP_IS_INT, OP_ABS, OP_POWER, + OP_POWER0, // hyperbolic and trigonometric functions OP_SIN, OP_COS, @@ -260,14 +265,21 @@ class arith_recognizers { bool is_ge(func_decl const * n) const { return is_decl_of(n, m_afid, OP_GE); } bool is_lt(func_decl const * n) const { return is_decl_of(n, m_afid, OP_LT); } bool is_gt(func_decl const * n) const { return is_decl_of(n, m_afid, OP_GT); } + + bool is_div0(func_decl const * n) const { return is_decl_of(n, m_afid, OP_DIV0); } + bool is_idiv0(func_decl const * n) const { return is_decl_of(n, m_afid, OP_IDIV0); } + bool is_rem0(func_decl const * n) const { return is_decl_of(n, m_afid, OP_REM0); } + bool is_mod0(func_decl const * n) const { return is_decl_of(n, m_afid, OP_MOD0); } + bool is_power0(func_decl const * n) const { return is_decl_of(n, m_afid, OP_POWER0); } + bool is_add(expr const * n) const { return is_app_of(n, m_afid, OP_ADD); } bool is_sub(expr const * n) const { return is_app_of(n, m_afid, OP_SUB); } bool is_uminus(expr const * n) const { return is_app_of(n, m_afid, OP_UMINUS); } bool is_mul(expr const * n) const { return is_app_of(n, m_afid, OP_MUL); } bool is_div(expr const * n) const { return is_app_of(n, m_afid, OP_DIV); } - //bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV_0); } + bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV0); } bool is_idiv(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV); } - //bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV_0); } + bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV0); } bool is_mod(expr const * n) const { return is_app_of(n, m_afid, OP_MOD); } bool is_rem(expr const * n) const { return is_app_of(n, m_afid, OP_REM); } bool is_to_real(expr const * n) const { return is_app_of(n, m_afid, OP_TO_REAL); } @@ -395,10 +407,15 @@ class arith_util : public arith_recognizers { app * mk_idiv(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_IDIV, arg1, arg2); } app * mk_rem(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_REM, arg1, arg2); } app * mk_mod(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_MOD, arg1, arg2); } + app * mk_div0(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_DIV0, arg1, arg2); } + app * mk_idiv0(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_IDIV0, arg1, arg2); } + app * mk_rem0(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_REM0, arg1, arg2); } + app * mk_mod0(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_MOD0, arg1, arg2); } app * mk_to_real(expr * arg1) { return m_manager.mk_app(m_afid, OP_TO_REAL, arg1); } app * mk_to_int(expr * arg1) { return m_manager.mk_app(m_afid, OP_TO_INT, arg1); } app * mk_is_int(expr * arg1) { return m_manager.mk_app(m_afid, OP_IS_INT, arg1); } app * mk_power(expr* arg1, expr* arg2) { return m_manager.mk_app(m_afid, OP_POWER, arg1, arg2); } + app * mk_power0(expr* arg1, expr* arg2) { return m_manager.mk_app(m_afid, OP_POWER0, arg1, arg2); } app * mk_sin(expr * arg) { return m_manager.mk_app(m_afid, OP_SIN, arg); } app * mk_cos(expr * arg) { return m_manager.mk_app(m_afid, OP_COS, arg); } @@ -444,7 +461,7 @@ class arith_util : public arith_recognizers { expr_ref mk_add_simplify(expr_ref_vector const& args); expr_ref mk_add_simplify(unsigned sz, expr* const* args); - bool is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args); + bool is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out); }; diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 237a8c5a19e..708a136af5c 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -334,6 +334,21 @@ 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); + } + if (!fi) { + result = m_au.mk_numeral(rational(0), f->get_range()); + return BR_DONE; + } + } + else if (!fi && m_fpau.is_considered_uninterpreted(f, num, args)) { + result = m.get_some_value(f->get_range()); + return BR_DONE; + } if (fi) { if (fi->is_partial()) fi->set_else(m.get_some_value(f->get_range())); @@ -343,14 +358,6 @@ struct evaluator_cfg : public default_rewriter_cfg { return BR_REWRITE_FULL; } - if (m_au.is_considered_uninterpreted(f, num, args)) { - result = m_au.mk_numeral(rational(0), f->get_range()); - return BR_DONE; - } - else if (m_fpau.is_considered_uninterpreted(f, num, args)) { - result = m.get_some_value(f->get_range()); - return BR_DONE; - } return BR_FAILED; } diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index 53072d0b4fe..9e2f2397712 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -435,7 +435,6 @@ namespace datalog { Since the destructor is protected, we cannot use the \c dealloc macro. */ void destroy() { - SASSERT(this != nullptr); this->~base_ancestor(); memory::deallocate(this); } diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 15571aba093..9bdbf4fb5c0 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -440,6 +440,7 @@ namespace smt { arith_eq_solver m_arith_eq_solver; bool m_found_unsupported_op; bool m_found_underspecified_op; + ptr_vector m_underspecified_ops; arith_eq_adapter m_arith_eq_adapter; vector m_rows; svector m_dead_rows; @@ -1077,6 +1078,7 @@ namespace smt { // // ----------------------------------- bool get_value(enode * n, expr_ref & r) override; + bool include_func_interp(func_decl* f) override; bool get_lower(enode* n, expr_ref& r); bool get_upper(enode* n, expr_ref& r); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index c62dbc33691..0fe92e325ea 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -39,6 +39,8 @@ namespace smt { template void theory_arith::found_underspecified_op(app * n) { + m_underspecified_ops.push_back(n); + get_context().push_trail(push_back_vector>(m_underspecified_ops)); if (!m_found_underspecified_op) { TRACE("arith", tout << "found underspecified expression:\n" << mk_pp(n, get_manager()) << "\n";); get_context().push_trail(value_trail(m_found_underspecified_op)); @@ -388,7 +390,6 @@ namespace smt { theory_var theory_arith::internalize_div(app * n) { rational r(1); if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n); - found_underspecified_op(n); theory_var s = mk_binary_op(n); context & ctx = get_context(); if (!ctx.relevancy()) @@ -3271,8 +3272,36 @@ namespace smt { if (!m_model_depends_on_computed_epsilon) { refine_epsilon(); } + for (app* n : m_underspecified_ops) { + if (m_util.is_div(n)) { + 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))); + } + else if (m_util.is_rem(n)) { + 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))); + } + else if (m_util.is_power(n)) { + mk_enode(m_util.mk_power0(n->get_arg(0), n->get_arg(1))); + } + } } + template + bool theory_arith::include_func_interp(func_decl* f) { + return + m_util.is_div0(f) || + m_util.is_idiv0(f) || + m_util.is_power0(f) || + m_util.is_rem0(f) || + m_util.is_mod0(f); + } + + template model_value_proc * theory_arith::mk_value(enode * n, model_generator & mg) { theory_var v = n->get_th_var(get_id());