From 2087ee3fb0535760f92d1bf9d737249746339b5d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 28 Jun 2018 11:59:01 -0700 Subject: [PATCH] restore some code that was removed during the rebase Signed-off-by: Lev Nachmanson --- src/ast/rewriter/arith_rewriter.cpp | 96 +++++++++++++++++++ src/ast/rewriter/arith_rewriter.h | 5 +- src/ast/simplifier/arith_simplifier_plugin.h | 97 -------------------- src/shell/main.cpp | 3 - src/smt/smt_setup.cpp | 2 +- 5 files changed, 101 insertions(+), 102 deletions(-) delete mode 100644 src/ast/simplifier/arith_simplifier_plugin.h diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 744c8a235..a194dc561 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -800,9 +800,105 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu result = m_util.mk_numeral(div(v1, v2), is_int); return BR_DONE; } + if (m_util.is_numeral(arg2, v2, is_int) && v2.is_one()) { + result = arg1; + return BR_DONE; + } + if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) { + return BR_FAILED; + } + if (arg1 == arg2) { + expr_ref zero(m_util.mk_int(0), m()); + result = m().mk_ite(m().mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1)); + return BR_REWRITE3; + } + if (divides(arg1, arg2, result)) { + return BR_REWRITE_FULL; + } return BR_FAILED; } + +// +// implement div ab ac = floor( ab / ac) = floor (b / c) = div b c +// +bool arith_rewriter::divides(expr* num, expr* den, expr_ref& result) { + expr_fast_mark1 mark; + rational num_r(1), den_r(1); + expr* num_e = nullptr, *den_e = nullptr; + ptr_buffer args1, args2; + flat_mul(num, args1); + flat_mul(den, args2); + for (expr * arg : args1) { + mark.mark(arg); + if (m_util.is_numeral(arg, num_r)) num_e = arg; + } + for (expr* arg : args2) { + if (mark.is_marked(arg)) { + result = remove_divisor(arg, num, den); + return true; + } + if (m_util.is_numeral(arg, den_r)) den_e = arg; + } + rational g = gcd(num_r, den_r); + if (!g.is_one()) { + SASSERT(g.is_pos()); + // replace num_e, den_e by their gcd reduction. + for (unsigned i = 0; i < args1.size(); ++i) { + if (args1[i] == num_e) { + args1[i] = m_util.mk_numeral(num_r / g, true); + break; + } + } + for (unsigned i = 0; i < args2.size(); ++i) { + if (args2[i] == den_e) { + args2[i] = m_util.mk_numeral(den_r / g, true); + break; + } + } + num = m_util.mk_mul(args1.size(), args1.c_ptr()); + den = m_util.mk_mul(args2.size(), args2.c_ptr()); + result = m_util.mk_idiv(num, den); + return true; + } + return false; +} +expr_ref arith_rewriter::remove_divisor(expr* arg, expr* num, expr* den) { + ptr_buffer args1, args2; + flat_mul(num, args1); + flat_mul(den, args2); + remove_divisor(arg, args1); + remove_divisor(arg, args2); + expr_ref zero(m_util.mk_int(0), m()); + num = args1.empty() ? m_util.mk_int(1) : m_util.mk_mul(args1.size(), args1.c_ptr()); + den = args2.empty() ? m_util.mk_int(1) : m_util.mk_mul(args2.size(), args2.c_ptr()); + return expr_ref(m().mk_ite(m().mk_eq(zero, arg), m_util.mk_idiv(zero, zero), m_util.mk_idiv(num, den)), m()); +} + +void arith_rewriter::flat_mul(expr* e, ptr_buffer& args) { + args.push_back(e); + for (unsigned i = 0; i < args.size(); ++i) { + e = args[i]; + if (m_util.is_mul(e)) { + args.append(to_app(e)->get_num_args(), to_app(e)->get_args()); + args[i] = args.back(); + args.shrink(args.size()-1); + --i; + } + } +} + +void arith_rewriter::remove_divisor(expr* d, ptr_buffer& args) { + for (unsigned i = 0; i < args.size(); ++i) { + if (args[i] == d) { + args[i] = args.back(); + args.shrink(args.size()-1); + return; + } + } + UNREACHABLE(); +} + br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) { set_curr_sort(m().get_sort(arg1)); numeral v1, v2; diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index 95668ea44..93b6e5ad5 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -95,7 +95,10 @@ class arith_rewriter : public poly_rewriter { expr_ref neg_monomial(expr * e) const; expr * mk_sin_value(rational const & k); app * mk_sqrt(rational const & k); - + bool divides(expr* d, expr* n, expr_ref& result); + expr_ref remove_divisor(expr* arg, expr* num, expr* den); + void flat_mul(expr* e, ptr_buffer& args); + void remove_divisor(expr* d, ptr_buffer& args); public: arith_rewriter(ast_manager & m, params_ref const & p = params_ref()): poly_rewriter(m, p) { diff --git a/src/ast/simplifier/arith_simplifier_plugin.h b/src/ast/simplifier/arith_simplifier_plugin.h deleted file mode 100644 index 045ee0e71..000000000 --- a/src/ast/simplifier/arith_simplifier_plugin.h +++ /dev/null @@ -1,97 +0,0 @@ -/*++ -Copyright (c) 2007 Microsoft Corporation - -Module Name: - - arith_simplifier_plugin.h - -Abstract: - - Simplifier for the arithmetic family. - -Author: - - Leonardo (leonardo) 2008-01-08 - ---*/ -#ifndef ARITH_SIMPLIFIER_PLUGIN_H_ -#define ARITH_SIMPLIFIER_PLUGIN_H_ - -#include"basic_simplifier_plugin.h" -#include"poly_simplifier_plugin.h" -#include"arith_decl_plugin.h" -#include"arith_simplifier_params.h" - -/** - \brief Simplifier for the arith family. -*/ -class arith_simplifier_plugin : public poly_simplifier_plugin { -public: - enum op_kind { - LE, GE, EQ - }; -protected: - arith_simplifier_params & m_params; - arith_util m_util; - basic_simplifier_plugin & m_bsimp; - expr_ref m_int_zero; - expr_ref m_real_zero; - - bool is_neg_poly(expr * t) const; - - template - void mk_le_ge_eq_core(expr * arg1, expr * arg2, expr_ref & result); - - void prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result); - - void gcd_reduce_monomial(expr_ref_vector& monomials, numeral& k); - - void div_monomial(expr_ref_vector& monomials, numeral const& g); - void get_monomial_gcd(expr_ref_vector& monomials, numeral& g); - bool divides(expr* d, expr* n, expr_ref& quot); - -public: - arith_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, arith_simplifier_params & p); - ~arith_simplifier_plugin(); - arith_util & get_arith_util() { return m_util; } - virtual numeral norm(const numeral & n) { return n; } - virtual bool is_numeral(expr * n, rational & val) const { bool f; return m_util.is_numeral(n, val, f); } - bool is_numeral(expr * n) const { return m_util.is_numeral(n); } - virtual bool is_minus_one(expr * n) const { numeral tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); } - virtual expr * get_zero(sort * s) const { return m_util.is_int(s) ? m_int_zero.get() : m_real_zero.get(); } - - virtual app * mk_numeral(numeral const & n) { return m_util.mk_numeral(n, m_curr_sort->get_decl_kind() == INT_SORT); } - app * mk_numeral(numeral const & n, bool is_int) { return m_util.mk_numeral(n, is_int); } - bool is_int_sort(sort const * s) const { return m_util.is_int(s); } - bool is_real_sort(sort const * s) const { return m_util.is_real(s); } - bool is_arith_sort(sort const * s) const { return is_int_sort(s) || is_real_sort(s); } - bool is_int(expr const * n) const { return m_util.is_int(n); } - bool is_le(expr const * n) const { return m_util.is_le(n); } - bool is_ge(expr const * n) const { return m_util.is_ge(n); } - - virtual bool is_le_ge(expr * n) const { return is_le(n) || is_ge(n); } - - void mk_le(expr * arg1, expr * arg2, expr_ref & result); - void mk_ge(expr * arg1, expr * arg2, expr_ref & result); - void mk_lt(expr * arg1, expr * arg2, expr_ref & result); - void mk_gt(expr * arg1, expr * arg2, expr_ref & result); - void mk_arith_eq(expr * arg1, expr * arg2, expr_ref & result); - void mk_div(expr * arg1, expr * arg2, expr_ref & result); - void mk_idiv(expr * arg1, expr * arg2, expr_ref & result); - void mk_mod(expr * arg1, expr * arg2, expr_ref & result); - void mk_rem(expr * arg1, expr * arg2, expr_ref & result); - void mk_to_real(expr * arg, expr_ref & result); - void mk_to_int(expr * arg, expr_ref & result); - void mk_is_int(expr * arg, expr_ref & result); - void mk_abs(expr * arg, expr_ref & result); - - virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); - virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result); - - bool is_arith_term(expr * n) const; - - void gcd_normalize(numeral & coeff, expr_ref& term); - -}; - -#endif /* ARITH_SIMPLIFIER_PLUGIN_H_ */ diff --git a/src/shell/main.cpp b/src/shell/main.cpp index a0444a919..d367b8ec6 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -296,9 +296,6 @@ void parse_cmd_line_args(int argc, char ** argv) { int STD_CALL main(int argc, char ** argv) { try{ - DEBUG_CODE( for (int i = 0; i < argc; i++) - std::cout << argv[i] << " "; - std::cout << std::endl;); unsigned return_value = 0; memory::initialize(0); memory::exit_when_out_of_memory(true, "ERROR: out of memory"); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 6a689c8d9..164c664d6 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -979,7 +979,7 @@ namespace smt { if (st.num_theories() == 2 && st.has_uf() && is_arith(st)) { if (!st.m_has_real) setup_QF_UFLIA(st); - else if (!st.m_has_int) + else if (!st.m_has_int && st.m_num_non_linear == 0) setup_QF_UFLRA(); else setup_unknown();