fixes

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

src/ast/arith_decl_plugin.cpp

@@ -178,7 +178,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
     MK_AC_OP(m_i_mul_decl, "*", OP_MUL, i);
     MK_LEFT_ASSOC_OP(m_i_div_decl, "div", OP_IDIV, i);
     MK_OP(m_i_rem_decl, "rem", OP_REM, i);
-    //MK_OP(m_i_mod_decl, "mod", OP_MOD, i);
+    MK_OP(m_i_mod_decl, "mod", OP_MOD, i);
     MK_UNARY(m_i_uminus_decl, "-", OP_UMINUS, i);
 
     m_to_real_decl = m->mk_func_decl(symbol("to_real"), i, r, func_decl_info(id, OP_TO_REAL));
@@ -215,18 +215,8 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
     m_e = m->mk_const(e_decl);
     m->inc_ref(m_e);
 
-    //func_decl * z_pw_z_int = m->mk_const_decl(symbol("0^0-int"), i, func_decl_info(id, OP_0_PW_0_INT));
-    //m_0_pw_0_int = m->mk_const(z_pw_z_int);
-    //m->inc_ref(m_0_pw_0_int);
-
-    //func_decl * z_pw_z_real = m->mk_const_decl(symbol("0^0-real"), r, func_decl_info(id, OP_0_PW_0_REAL));
-    //m_0_pw_0_real = m->mk_const(z_pw_z_real);
-    //m->inc_ref(m_0_pw_0_real);
 
     MK_OP(m_neg_root_decl, "neg-root", OP_NEG_ROOT, r);
-    //MK_UNARY(m_div_0_decl, "/0", OP_DIV_0, r);
-    //MK_UNARY(m_idiv_0_decl, "div0", OP_IDIV_0, i);
-    //MK_UNARY(m_mod_0_decl, "mod0", OP_MOD_0, i);
     MK_UNARY(m_u_asin_decl, "asin-u", OP_U_ASIN, r);
     MK_UNARY(m_u_acos_decl, "acos-u", OP_U_ACOS, r);
 }
@@ -279,12 +269,7 @@ arith_decl_plugin::arith_decl_plugin():
     m_atanh_decl(0),
     m_pi(0),
     m_e(0),
-    m_0_pw_0_int(0),
-    m_0_pw_0_real(0),
     m_neg_root_decl(0),
-    m_div_0_decl(0),
-    m_idiv_0_decl(0),
-    m_mod_0_decl(0),
     m_u_asin_decl(0),
     m_u_acos_decl(0),
     m_convert_int_numerals_to_real(false) {
@@ -339,12 +324,7 @@ void arith_decl_plugin::finalize() {
     DEC_REF(m_atanh_decl);
     DEC_REF(m_pi);
     DEC_REF(m_e);
-    DEC_REF(m_0_pw_0_int);
-    DEC_REF(m_0_pw_0_real);
     DEC_REF(m_neg_root_decl);
-    DEC_REF(m_div_0_decl);
-    DEC_REF(m_idiv_0_decl);
-    DEC_REF(m_mod_0_decl);
     DEC_REF(m_u_asin_decl);
     DEC_REF(m_u_acos_decl);
     m_manager->dec_array_ref(m_small_ints.size(), m_small_ints.c_ptr());

src/ast/arith_decl_plugin.h

@@ -70,12 +70,7 @@ enum arith_op_kind {
     OP_PI,
     OP_E,
     // under-specified symbols
-    //OP_0_PW_0_INT,    // 0^0 for integers
-    //OP_0_PW_0_REAL,   // 0^0 for reals
     OP_NEG_ROOT,      // x^n when n is even and x is negative
-    // OP_DIV_0,         // x/0
-    // OP_IDIV_0,        // x div 0
-    // OP_MOD_0,         // x mod 0
     OP_U_ASIN,        // asin(x) for x < -1 or x > 1
     OP_U_ACOS,        // acos(x) for x < -1 or x > 1
     LAST_ARITH_OP
@@ -141,12 +136,7 @@ protected:
     app       * m_pi;
     app       * m_e;
 
-    app       * m_0_pw_0_int;
-    app       * m_0_pw_0_real;
     func_decl * m_neg_root_decl;
-    func_decl * m_div_0_decl;
-    func_decl * m_idiv_0_decl;
-    func_decl * m_mod_0_decl;
     func_decl * m_u_asin_decl;
     func_decl * m_u_acos_decl;
     ptr_vector<app> m_small_ints;
@@ -207,10 +197,6 @@ public:
 
     app * mk_e() const { return m_e; }
 
-    app * mk_0_pw_0_int() const { return m_0_pw_0_int; }
-
-    app * mk_0_pw_0_real() const { return m_0_pw_0_real; }
-
     virtual expr * get_some_value(sort * s);
 
     virtual bool is_considered_uninterpreted(func_decl * f) {
@@ -218,12 +204,7 @@ public:
             return false;
         switch (f->get_decl_kind())
         {
-        //case OP_0_PW_0_INT:
-        //case OP_0_PW_0_REAL:
         case OP_NEG_ROOT:
-        //case OP_DIV_0:
-        //case OP_IDIV_0:
-        //case OP_MOD_0:
         case OP_U_ASIN:
         case OP_U_ACOS:
             return true;
@@ -425,11 +406,6 @@ public:
     app * mk_pi() { return plugin().mk_pi(); }
     app * mk_e()  { return plugin().mk_e(); }
 
- //   app * mk_0_pw_0_int() { return plugin().mk_0_pw_0_int(); }
- //   app * mk_0_pw_0_real() { return plugin().mk_0_pw_0_real(); }
- //   app * mk_div0(expr * arg) { return m_manager.mk_app(m_afid, OP_DIV_0, arg); }
- //   app * mk_idiv0(expr * arg) { return m_manager.mk_app(m_afid, OP_IDIV_0, arg); }
- //   app * mk_mod0(expr * arg) { return m_manager.mk_app(m_afid, OP_MOD_0, arg); }
     app * mk_neg_root(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_NEG_ROOT, arg1, arg2); }
     app * mk_u_asin(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ASIN, arg); }
     app * mk_u_acos(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ACOS, arg); }

src/muz/spacer/spacer_sym_mux.cpp

@@ -368,6 +368,7 @@ public:
         app * a = to_app(s);
         func_decl * sym = a->get_decl();
         if (!m_parent.has_index(sym, m_from_idx)) {
+            (void) m_homogenous;
             SASSERT(!m_homogenous || !m_parent.is_muxed(sym));
             return false;
         }

src/smt/qi_queue.cpp

@@ -227,9 +227,8 @@ namespace smt {
         TRACE("qi_queue_instance", tout << "new instance:\n" << mk_pp(instance, m_manager) << "\n";);
         expr_ref  s_instance(m_manager);
         proof_ref pr(m_manager);
-        th_rewriter & simp = m_context.get_rewriter();
+        m_context.get_rewriter()(instance, s_instance, pr);
-        simp(instance, s_instance, pr);
+        TRACE("qi_queue_bug", tout << "new instance after simplification:\n" << s_instance << "\n";);
-        TRACE("qi_queue_bug", tout << "new instance after simplification:\n" << mk_pp(s_instance, m_manager) << "\n";);
         if (m_manager.is_true(s_instance)) {
             TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m_manager););
 

src/smt/smt_quick_checker.cpp

@@ -164,7 +164,6 @@ namespace smt {
     quick_checker::quick_checker(context & c):
         m_context(c),
         m_manager(c.get_manager()),
-        m_simplifier(c.get_rewriter()),
         m_collector(c),
         m_new_exprs(m_manager) {
     }
@@ -411,7 +410,7 @@ namespace smt {
             }
         }
         expr_ref new_expr(m_manager);
-        new_expr = m_simplifier.mk_app(to_app(n)->get_decl(), num_args, new_args.c_ptr());
+        new_expr = m_context.get_rewriter().mk_app(to_app(n)->get_decl(), num_args, new_args.c_ptr());
         m_new_exprs.push_back(new_expr);
         m_canonize_cache.insert(n, new_expr);
         return new_expr;

src/smt/smt_quick_checker.h

@@ -77,7 +77,6 @@ namespace smt {
 
         context &            m_context;
         ast_manager &        m_manager;
-        th_rewriter &        m_simplifier;
         collector            m_collector;
         expr_ref_vector      m_new_exprs;
         vector<enode_vector> m_candidate_vectors; 

src/smt/theory_arith_core.h

@@ -449,9 +449,8 @@ namespace smt {
         expr_ref s_ante(m), s_conseq(m);
         expr* s_conseq_n, * s_ante_n;
         bool negated;
-        proof_ref pr(m);
 
-        s(ante, s_ante, pr);
+        s(ante, s_ante);
         if (ctx.get_cancel_flag()) return;
         negated = m.is_not(s_ante, s_ante_n);
         if (negated) s_ante = s_ante_n;
@@ -459,7 +458,7 @@ namespace smt {
         literal l_ante = ctx.get_literal(s_ante);
         if (negated) l_ante.neg();
 
-        s(conseq, s_conseq, pr);
+        s(conseq, s_conseq);
         if (ctx.get_cancel_flag()) return;
         negated = m.is_not(s_conseq, s_conseq_n);
         if (negated) s_conseq = s_conseq_n;

src/smt/theory_fpa.cpp

@@ -385,7 +385,6 @@ namespace smt {
     {
         ast_manager & m = get_manager();
         context & ctx = get_context();
-        th_rewriter & simp = ctx.get_rewriter();
 
         expr_ref res(m), t(m);
         proof_ref t_pr(m);
@@ -394,7 +393,7 @@ namespace smt {
         expr_ref_vector::iterator it = m_converter.m_extra_assertions.begin();
         expr_ref_vector::iterator end = m_converter.m_extra_assertions.end();
         for (; it != end; it++) {
-            simp(*it, t, t_pr);
+            ctx.get_rewriter()(*it, t, t_pr);
             res = m.mk_and(res, t);
         }
         m_converter.m_extra_assertions.reset();

src/tactic/arith/purify_arith_tactic.cpp

@@ -297,8 +297,8 @@ struct purify_arith_proc {
             push_cnstr(OR(EQ(y, mk_real_zero()),
                           EQ(u().mk_mul(y, k), x)));
             push_cnstr_pr(result_pr);
-
+            rational r;
-            if (complete()) {
+            if (complete() && (!u().is_numeral(y, r) || r.is_zero())) {
                 // y != 0 \/ k = div-0(x)
                 push_cnstr(OR(NOT(EQ(y, mk_real_zero())),
                               EQ(k, u().mk_div(x, mk_real_zero()))));
@@ -348,7 +348,8 @@ struct purify_arith_proc {
             push_cnstr(OR(u().mk_ge(y, zero), u().mk_lt(k2, u().mk_mul(u().mk_numeral(rational(-1), true), y))));
             push_cnstr_pr(mod_pr);
 
-            if (complete()) {
+            rational r;
+            if (complete() && (!u().is_numeral(y, r) || r.is_zero())) {
                 push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, u().mk_idiv(x, zero))));
                 push_cnstr_pr(result_pr);
 

src/test/ext_numeral.cpp

@@ -43,13 +43,13 @@ static void FUN_NAME(int a, ext_numeral_kind ak, int b, ext_numeral_kind bk, int
     scoped_mpq _a(m), _b(m), _c(m);                                     \
     m.set(_a, a);                                                       \
     m.set(_b, b);                                                       \
-    ext_numeral_kind ck;                                                \
+    ext_numeral_kind ck(EN_NUMERAL);                                    \
     OP_NAME(m, _a, ak, _b, bk, _c, ck);                                 \
-    ENSURE(ck == expected_ck);                                         \
+    ENSURE(ck == expected_ck);                                          \
     if (expected_ck == EN_NUMERAL) {                                    \
         scoped_mpq _expected_c(m);                                      \
         m.set(_expected_c, expected_c);                                 \
-        ENSURE(m.eq(_c, _expected_c));                                 \
+        ENSURE(m.eq(_c, _expected_c));                                  \
     }                                                                   \
 }