add definitions for under-specified cases of arithmetic operators #2663 #2676 #2679

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

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 = mk_div0();
-        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()) {
@@ -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());
+}

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

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

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

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

src/muz/fp/dl_cmds.cpp

@@ -305,7 +305,6 @@ public:
 
             case datalog::OK:
                 (void)query_exn;
-                SASSERT(query_exn);
                 break;
 
             case datalog::CANCELED:

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

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

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()) {

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

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

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<typename Ext>
     void theory_arith<Ext>::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());
             }
         }
     }

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