adding div0

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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);

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 @@ public:
     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 @@ public:
     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 @@ public:
     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);
 
 };
 

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;
     }
 

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);
             }

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<app>         m_underspecified_ops;
         arith_eq_adapter        m_arith_eq_adapter;
         vector<row>             m_rows;
         svector<unsigned>       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);

src/smt/theory_arith_core.h

@@ -39,6 +39,8 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::found_underspecified_op(app * n) {
+        m_underspecified_ops.push_back(n);
+        get_context().push_trail(push_back_vector<context, ptr_vector<app>>(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<context, bool>(m_found_underspecified_op));
@@ -388,7 +390,6 @@ namespace smt {
     theory_var theory_arith<Ext>::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<typename Ext>
+    bool theory_arith<Ext>::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<typename Ext>
     model_value_proc * theory_arith<Ext>::mk_value(enode * n, model_generator & mg) {
         theory_var v = n->get_th_var(get_id());