From d940516df3c60ca01c69e1569dcfbb3e950f52ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 27 Aug 2017 11:01:45 -0700 Subject: [PATCH] fixes Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 22 +--------------------- src/ast/arith_decl_plugin.h | 24 ------------------------ src/muz/spacer/spacer_sym_mux.cpp | 1 + src/smt/qi_queue.cpp | 5 ++--- src/smt/smt_quick_checker.cpp | 3 +-- src/smt/smt_quick_checker.h | 1 - src/smt/theory_arith_core.h | 5 ++--- src/smt/theory_fpa.cpp | 3 +-- src/tactic/arith/purify_arith_tactic.cpp | 7 ++++--- src/test/ext_numeral.cpp | 6 +++--- 10 files changed, 15 insertions(+), 62 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 0719ebdfa..03ee77458 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/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()); diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 0238df3ae..4b24ea5e6 100644 --- a/src/ast/arith_decl_plugin.h +++ b/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 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); } diff --git a/src/muz/spacer/spacer_sym_mux.cpp b/src/muz/spacer/spacer_sym_mux.cpp index c311d9990..ee1d3726d 100644 --- a/src/muz/spacer/spacer_sym_mux.cpp +++ b/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; } diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index 8f8e3df7b..f77fde29a 100644 --- a/src/smt/qi_queue.cpp +++ b/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(); - simp(instance, s_instance, pr); - TRACE("qi_queue_bug", tout << "new instance after simplification:\n" << mk_pp(s_instance, m_manager) << "\n";); + m_context.get_rewriter()(instance, s_instance, pr); + TRACE("qi_queue_bug", tout << "new instance after simplification:\n" << s_instance << "\n";); if (m_manager.is_true(s_instance)) { TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m_manager);); diff --git a/src/smt/smt_quick_checker.cpp b/src/smt/smt_quick_checker.cpp index 773768944..72c28fd7d 100644 --- a/src/smt/smt_quick_checker.cpp +++ b/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; diff --git a/src/smt/smt_quick_checker.h b/src/smt/smt_quick_checker.h index d07e10921..21a570c3c 100644 --- a/src/smt/smt_quick_checker.h +++ b/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 m_candidate_vectors; diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 16a49961e..13aba9686 100644 --- a/src/smt/theory_arith_core.h +++ b/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; diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 3f246b2c7..dfd295220 100644 --- a/src/smt/theory_fpa.cpp +++ b/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(); diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 17a69f93e..7e89794ce 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/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); - - if (complete()) { + rational r; + 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); diff --git a/src/test/ext_numeral.cpp b/src/test/ext_numeral.cpp index 4c82617c9..003aa272f 100644 --- a/src/test/ext_numeral.cpp +++ b/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)); \ } \ }