From cf87b6d622d8cb71b4dff4a3cbd034dccbaddcbf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 29 Aug 2017 09:22:27 -0700 Subject: [PATCH] remove simplifier files Signed-off-by: Nikolaj Bjorner --- src/ast/macros/macro_util.cpp | 2 - src/ast/simplifier/CMakeLists.txt | 22 - src/ast/simplifier/README | 2 - .../simplifier/arith_simplifier_params.cpp | 33 - src/ast/simplifier/arith_simplifier_params.h | 38 - .../arith_simplifier_params_helper.pyg | 7 - .../simplifier/arith_simplifier_plugin.cpp | 449 ---- src/ast/simplifier/arith_simplifier_plugin.h | 96 - .../simplifier/array_simplifier_params.cpp | 26 - src/ast/simplifier/array_simplifier_params.h | 34 - .../array_simplifier_params_helper.pyg | 6 - .../simplifier/array_simplifier_plugin.cpp | 877 ------- src/ast/simplifier/array_simplifier_plugin.h | 154 -- src/ast/simplifier/base_simplifier.h | 76 - .../simplifier/basic_simplifier_plugin.cpp | 147 -- src/ast/simplifier/basic_simplifier_plugin.h | 78 - src/ast/simplifier/bv_elim.cpp | 119 - src/ast/simplifier/bv_elim.h | 45 - src/ast/simplifier/bv_simplifier_params.cpp | 36 - src/ast/simplifier/bv_simplifier_params.h | 38 - .../bv_simplifier_params_helper.pyg | 4 - src/ast/simplifier/bv_simplifier_plugin.cpp | 2261 ----------------- src/ast/simplifier/bv_simplifier_plugin.h | 187 -- .../simplifier/datatype_simplifier_plugin.cpp | 115 - .../simplifier/datatype_simplifier_plugin.h | 42 - src/ast/simplifier/elim_bounds.cpp | 224 -- src/ast/simplifier/elim_bounds.h | 69 - src/ast/simplifier/fpa_simplifier_plugin.cpp | 39 - src/ast/simplifier/fpa_simplifier_plugin.h | 39 - src/ast/simplifier/poly_simplifier_plugin.cpp | 835 ------ src/ast/simplifier/poly_simplifier_plugin.h | 155 -- src/ast/simplifier/seq_simplifier_plugin.cpp | 39 - src/ast/simplifier/seq_simplifier_plugin.h | 39 - src/ast/simplifier/simplifier.cpp | 962 ------- src/ast/simplifier/simplifier.h | 232 -- src/ast/simplifier/simplifier_plugin.cpp | 46 - src/ast/simplifier/simplifier_plugin.h | 94 - src/muz/pdr/pdr_util.cpp | 27 +- src/muz/rel/dl_bound_relation.h | 1 - src/muz/rel/dl_interval_relation.h | 5 +- src/muz/spacer/spacer_legacy_mbp.cpp | 3 - src/smt/arith_eq_adapter.h | 1 - src/smt/theory_arith.h | 1 - src/smt/theory_arith_int.h | 7 +- 44 files changed, 17 insertions(+), 7695 deletions(-) delete mode 100644 src/ast/simplifier/CMakeLists.txt delete mode 100644 src/ast/simplifier/README delete mode 100644 src/ast/simplifier/arith_simplifier_params.cpp delete mode 100644 src/ast/simplifier/arith_simplifier_params.h delete mode 100644 src/ast/simplifier/arith_simplifier_params_helper.pyg delete mode 100644 src/ast/simplifier/arith_simplifier_plugin.cpp delete mode 100644 src/ast/simplifier/arith_simplifier_plugin.h delete mode 100644 src/ast/simplifier/array_simplifier_params.cpp delete mode 100644 src/ast/simplifier/array_simplifier_params.h delete mode 100644 src/ast/simplifier/array_simplifier_params_helper.pyg delete mode 100644 src/ast/simplifier/array_simplifier_plugin.cpp delete mode 100644 src/ast/simplifier/array_simplifier_plugin.h delete mode 100644 src/ast/simplifier/base_simplifier.h delete mode 100644 src/ast/simplifier/basic_simplifier_plugin.cpp delete mode 100644 src/ast/simplifier/basic_simplifier_plugin.h delete mode 100644 src/ast/simplifier/bv_elim.cpp delete mode 100644 src/ast/simplifier/bv_elim.h delete mode 100644 src/ast/simplifier/bv_simplifier_params.cpp delete mode 100644 src/ast/simplifier/bv_simplifier_params.h delete mode 100644 src/ast/simplifier/bv_simplifier_params_helper.pyg delete mode 100644 src/ast/simplifier/bv_simplifier_plugin.cpp delete mode 100644 src/ast/simplifier/bv_simplifier_plugin.h delete mode 100644 src/ast/simplifier/datatype_simplifier_plugin.cpp delete mode 100644 src/ast/simplifier/datatype_simplifier_plugin.h delete mode 100644 src/ast/simplifier/elim_bounds.cpp delete mode 100644 src/ast/simplifier/elim_bounds.h delete mode 100644 src/ast/simplifier/fpa_simplifier_plugin.cpp delete mode 100644 src/ast/simplifier/fpa_simplifier_plugin.h delete mode 100644 src/ast/simplifier/poly_simplifier_plugin.cpp delete mode 100644 src/ast/simplifier/poly_simplifier_plugin.h delete mode 100644 src/ast/simplifier/seq_simplifier_plugin.cpp delete mode 100644 src/ast/simplifier/seq_simplifier_plugin.h delete mode 100644 src/ast/simplifier/simplifier.cpp delete mode 100644 src/ast/simplifier/simplifier.h delete mode 100644 src/ast/simplifier/simplifier_plugin.cpp delete mode 100644 src/ast/simplifier/simplifier_plugin.h diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index 6bc1ee66e..55c5436e4 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -20,8 +20,6 @@ Revision History: #include "ast/macros/macro_util.h" #include "ast/occurs.h" #include "ast/ast_util.h" -#include "ast/simplifier/arith_simplifier_plugin.h" -#include "ast/simplifier/bv_simplifier_plugin.h" #include "ast/rewriter/var_subst.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" diff --git a/src/ast/simplifier/CMakeLists.txt b/src/ast/simplifier/CMakeLists.txt deleted file mode 100644 index 37d96b1a5..000000000 --- a/src/ast/simplifier/CMakeLists.txt +++ /dev/null @@ -1,22 +0,0 @@ -z3_add_component(simplifier - SOURCES - arith_simplifier_params.cpp -# arith_simplifier_plugin.cpp -# array_simplifier_params.cpp -# array_simplifier_plugin.cpp -# basic_simplifier_plugin.cpp -# bv_elim.cpp -# bv_simplifier_params.cpp -# bv_simplifier_plugin.cpp -# datatype_simplifier_plugin.cpp -# elim_bounds.cpp -# fpa_simplifier_plugin.cpp -# maximise_ac_sharing.cpp -# poly_simplifier_plugin.cpp -# seq_simplifier_plugin.cpp -# simplifier.cpp -# simplifier_plugin.cpp - COMPONENT_DEPENDENCIES - rewriter - -) diff --git a/src/ast/simplifier/README b/src/ast/simplifier/README deleted file mode 100644 index 4725d9de9..000000000 --- a/src/ast/simplifier/README +++ /dev/null @@ -1,2 +0,0 @@ -Simplifier module is now obsolete. -It is still being used in many places, but we will eventually replace all occurrences with the new rewriter module. diff --git a/src/ast/simplifier/arith_simplifier_params.cpp b/src/ast/simplifier/arith_simplifier_params.cpp deleted file mode 100644 index 73bbbaa1a..000000000 --- a/src/ast/simplifier/arith_simplifier_params.cpp +++ /dev/null @@ -1,33 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - arith_simplifier_params.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2012-12-02. - -Revision History: - ---*/ -#include "ast/simplifier/arith_simplifier_params.h" -#include "ast/simplifier/arith_simplifier_params_helper.hpp" - -void arith_simplifier_params::updt_params(params_ref const & _p) { - arith_simplifier_params_helper p(_p); - m_arith_expand_eqs = p.arith_expand_eqs(); - m_arith_process_all_eqs = p.arith_process_all_eqs(); -} - -#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; - -void arith_simplifier_params::display(std::ostream & out) const { - DISPLAY_PARAM(m_arith_expand_eqs); - DISPLAY_PARAM(m_arith_process_all_eqs); -} \ No newline at end of file diff --git a/src/ast/simplifier/arith_simplifier_params.h b/src/ast/simplifier/arith_simplifier_params.h deleted file mode 100644 index 8a4150099..000000000 --- a/src/ast/simplifier/arith_simplifier_params.h +++ /dev/null @@ -1,38 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - arith_simplifier_params.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-05-09. - -Revision History: - ---*/ -#ifndef ARITH_SIMPLIFIER_PARAMS_H_ -#define ARITH_SIMPLIFIER_PARAMS_H_ - -#include "util/params.h" - -struct arith_simplifier_params { - bool m_arith_expand_eqs; - bool m_arith_process_all_eqs; - - arith_simplifier_params(params_ref const & p = params_ref()) { - updt_params(p); - } - - void updt_params(params_ref const & _p); - - void display(std::ostream & out) const; -}; - -#endif /* ARITH_SIMPLIFIER_PARAMS_H_ */ - diff --git a/src/ast/simplifier/arith_simplifier_params_helper.pyg b/src/ast/simplifier/arith_simplifier_params_helper.pyg deleted file mode 100644 index 49a7cf3d2..000000000 --- a/src/ast/simplifier/arith_simplifier_params_helper.pyg +++ /dev/null @@ -1,7 +0,0 @@ -def_module_params(class_name='arith_simplifier_params_helper', - module_name="old_simplify", # Parameters will be in the old_simplify module - description="old simplification (stack) still used in the smt module", - export=True, - params=( - ('arith.expand_eqs', BOOL, False, 'expand equalities into two inequalities'), - ('arith.process_all_eqs', BOOL, False, 'put all equations in the form (= t c), where c is a numeral'))) diff --git a/src/ast/simplifier/arith_simplifier_plugin.cpp b/src/ast/simplifier/arith_simplifier_plugin.cpp deleted file mode 100644 index bfe72b232..000000000 --- a/src/ast/simplifier/arith_simplifier_plugin.cpp +++ /dev/null @@ -1,449 +0,0 @@ -/*++ -Copyright (c) 2007 Microsoft Corporation - -Module Name: - - arith_simplifier_plugin.cpp - -Abstract: - - Simplifier for the arithmetic family. - -Author: - - Leonardo (leonardo) 2008-01-08 - ---*/ -#include "ast/simplifier/arith_simplifier_plugin.h" -#include "ast/ast_pp.h" -#include "ast/ast_ll_pp.h" -#include "ast/ast_smt2_pp.h" - -arith_simplifier_plugin::~arith_simplifier_plugin() { -} - -arith_simplifier_plugin::arith_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, arith_simplifier_params & p): - poly_simplifier_plugin(symbol("arith"), m, OP_ADD, OP_MUL, OP_UMINUS, OP_SUB, OP_NUM), - m_params(p), - m_util(m), - m_bsimp(b), - m_int_zero(m), - m_real_zero(m) { - m_int_zero = m_util.mk_numeral(rational(0), true); - m_real_zero = m_util.mk_numeral(rational(0), false); -} - -/** - \brief Return true if the first monomial of t is negative. -*/ -bool arith_simplifier_plugin::is_neg_poly(expr * t) const { - if (m_util.is_add(t)) { - t = to_app(t)->get_arg(0); - } - if (m_util.is_mul(t)) { - t = to_app(t)->get_arg(0); - rational r; - if (is_numeral(t, r)) - return r.is_neg(); - } - return false; -} - -void arith_simplifier_plugin::get_monomial_gcd(expr_ref_vector& monomials, numeral& g) { - g = numeral::zero(); - numeral n; - for (unsigned i = 0; !g.is_one() && i < monomials.size(); ++i) { - expr* e = monomials[i].get(); - if (is_numeral(e, n)) { - g = gcd(abs(n), g); - } - else if (is_mul(e) && is_numeral(to_app(e)->get_arg(0), n)) { - g = gcd(abs(n), g); - } - else { - g = numeral::one(); - return; - } - } - if (g.is_zero()) { - g = numeral::one(); - } -} - -void arith_simplifier_plugin::div_monomial(expr_ref_vector& monomials, numeral const& g) { - numeral n; - for (unsigned i = 0; i < monomials.size(); ++i) { - expr* e = monomials[i].get(); - if (is_numeral(e, n)) { - SASSERT((n/g).is_int()); - monomials[i] = mk_numeral(n/g); - } - else if (is_mul(e) && is_numeral(to_app(e)->get_arg(0), n)) { - SASSERT((n/g).is_int()); - monomials[i] = mk_mul(n/g, to_app(e)->get_arg(1)); - } - else { - UNREACHABLE(); - } - } -} - -void arith_simplifier_plugin::gcd_reduce_monomial(expr_ref_vector& monomials, numeral& k) { - numeral g, n; - - get_monomial_gcd(monomials, g); - g = gcd(abs(k), g); - - if (g.is_one()) { - return; - } - SASSERT(g.is_pos()); - - k = k / g; - div_monomial(monomials, g); - -} - -template -void arith_simplifier_plugin::mk_le_ge_eq_core(expr * arg1, expr * arg2, expr_ref & result) { - set_curr_sort(arg1); - bool is_int = m_curr_sort->get_decl_kind() == INT_SORT; - expr_ref_vector monomials(m_manager); - rational k; - TRACE("arith_eq_bug", tout << mk_ismt2_pp(arg1, m_manager) << "\n" << mk_ismt2_pp(arg2, m_manager) << "\n";); - process_sum_of_monomials(false, arg1, monomials, k); - process_sum_of_monomials(true, arg2, monomials, k); - k.neg(); - if (is_int) { - numeral g; - get_monomial_gcd(monomials, g); - if (!g.is_one()) { - div_monomial(monomials, g); - switch(Kind) { - case LE: - // - // g*monmials' <= k - // <=> - // monomials' <= floor(k/g) - // - k = floor(k/g); - break; - case GE: - // - // g*monmials' >= k - // <=> - // monomials' >= ceil(k/g) - // - k = ceil(k/g); - break; - case EQ: - k = k/g; - if (!k.is_int()) { - result = m_manager.mk_false(); - return; - } - break; - } - } - } - expr_ref lhs(m_manager); - mk_sum_of_monomials(monomials, lhs); - if (m_util.is_numeral(lhs)) { - SASSERT(lhs == mk_zero()); - if (( Kind == LE && numeral::zero() <= k) || - ( Kind == GE && numeral::zero() >= k) || - ( Kind == EQ && numeral::zero() == k)) - result = m_manager.mk_true(); - else - result = m_manager.mk_false(); - } - else { - - if (is_neg_poly(lhs)) { - expr_ref neg_lhs(m_manager); - mk_uminus(lhs, neg_lhs); - lhs = neg_lhs; - k.neg(); - expr * rhs = m_util.mk_numeral(k, is_int); - switch (Kind) { - case LE: - result = m_util.mk_ge(lhs, rhs); - break; - case GE: - result = m_util.mk_le(lhs, rhs); - break; - case EQ: - result = m_manager.mk_eq(lhs, rhs); - break; - } - } - else { - expr * rhs = m_util.mk_numeral(k, is_int); - switch (Kind) { - case LE: - result = m_util.mk_le(lhs, rhs); - break; - case GE: - result = m_util.mk_ge(lhs, rhs); - break; - case EQ: - result = m_manager.mk_eq(lhs, rhs); - break; - } - } - } -} - -void arith_simplifier_plugin::mk_arith_eq(expr * arg1, expr * arg2, expr_ref & result) { - mk_le_ge_eq_core(arg1, arg2, result); -} - -void arith_simplifier_plugin::mk_le(expr * arg1, expr * arg2, expr_ref & result) { - mk_le_ge_eq_core(arg1, arg2, result); -} - -void arith_simplifier_plugin::mk_ge(expr * arg1, expr * arg2, expr_ref & result) { - mk_le_ge_eq_core(arg1, arg2, result); -} - -void arith_simplifier_plugin::mk_lt(expr * arg1, expr * arg2, expr_ref & result) { - expr_ref tmp(m_manager); - mk_le(arg2, arg1, tmp); - m_bsimp.mk_not(tmp, result); -} - -void arith_simplifier_plugin::mk_gt(expr * arg1, expr * arg2, expr_ref & result) { - expr_ref tmp(m_manager); - mk_le(arg1, arg2, tmp); - m_bsimp.mk_not(tmp, result); -} - -void arith_simplifier_plugin::gcd_normalize(numeral & coeff, expr_ref& term) { - if (!abs(coeff).is_one()) { - set_curr_sort(term); - SASSERT(m_curr_sort->get_decl_kind() == INT_SORT); - expr_ref_vector monomials(m_manager); - rational k; - monomials.push_back(mk_numeral(numeral(coeff), true)); - process_sum_of_monomials(false, term, monomials, k); - gcd_reduce_monomial(monomials, k); - numeral coeff1; - if (!is_numeral(monomials[0].get(), coeff1)) { - UNREACHABLE(); - } - if (coeff1 == coeff) { - return; - } - monomials[0] = mk_numeral(k, true); - coeff = coeff1; - mk_sum_of_monomials(monomials, term); - } -} - - -void arith_simplifier_plugin::mk_div(expr * arg1, expr * arg2, expr_ref & result) { - set_curr_sort(arg1); - numeral v1, v2; - bool is_int; - if (m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) { - SASSERT(!is_int); - if (m_util.is_numeral(arg1, v1, is_int)) - result = m_util.mk_numeral(v1/v2, false); - else { - numeral k(1); - k /= v2; - - expr_ref inv_arg2(m_util.mk_numeral(k, false), m_manager); - mk_mul(inv_arg2, arg1, result); - } - } - else - result = m_util.mk_div(arg1, arg2); -} - -void arith_simplifier_plugin::mk_idiv(expr * arg1, expr * arg2, expr_ref & result) { - set_curr_sort(arg1); - numeral v1, v2; - bool is_int; - if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) - result = m_util.mk_numeral(div(v1, v2), is_int); - else - result = m_util.mk_idiv(arg1, arg2); -} - -void arith_simplifier_plugin::prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result) { - SASSERT(m_util.is_int(e)); - SASSERT(k.is_int() && k.is_pos()); - numeral n; - bool is_int; - - if (depth == 0) { - result = e; - } - else if (is_add(e) || is_mul(e)) { - expr_ref_vector args(m_manager); - expr_ref tmp(m_manager); - app* a = to_app(e); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - prop_mod_const(a->get_arg(i), depth - 1, k, tmp); - args.push_back(tmp); - } - reduce(a->get_decl(), args.size(), args.c_ptr(), result); - } - else if (m_util.is_numeral(e, n, is_int) && is_int) { - result = mk_numeral(mod(n, k), true); - } - else { - result = e; - } -} - -void arith_simplifier_plugin::mk_mod(expr * arg1, expr * arg2, expr_ref & result) { - set_curr_sort(arg1); - numeral v1, v2; - bool is_int; - if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) { - result = m_util.mk_numeral(mod(v1, v2), is_int); - } - else if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_one()) { - result = m_util.mk_numeral(numeral(0), true); - } - else if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos()) { - expr_ref tmp(m_manager); - prop_mod_const(arg1, 5, v2, tmp); - result = m_util.mk_mod(tmp, arg2); - } - else { - result = m_util.mk_mod(arg1, arg2); - } -} - -void arith_simplifier_plugin::mk_rem(expr * arg1, expr * arg2, expr_ref & result) { - set_curr_sort(arg1); - numeral v1, v2; - bool is_int; - if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) { - numeral m = mod(v1, v2); - // - // rem(v1,v2) = if v2 >= 0 then mod(v1,v2) else -mod(v1,v2) - // - if (v2.is_neg()) { - m.neg(); - } - result = m_util.mk_numeral(m, is_int); - } - else if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_one()) { - result = m_util.mk_numeral(numeral(0), true); - } - else if (m_util.is_numeral(arg2, v2, is_int) && is_int && !v2.is_zero()) { - expr_ref tmp(m_manager); - prop_mod_const(arg1, 5, v2, tmp); - result = m_util.mk_mod(tmp, arg2); - if (v2.is_neg()) { - result = m_util.mk_uminus(result); - } - } - else { - result = m_util.mk_rem(arg1, arg2); - } -} - -void arith_simplifier_plugin::mk_to_real(expr * arg, expr_ref & result) { - numeral v; - if (m_util.is_numeral(arg, v)) - result = m_util.mk_numeral(v, false); - else - result = m_util.mk_to_real(arg); -} - -void arith_simplifier_plugin::mk_to_int(expr * arg, expr_ref & result) { - numeral v; - if (m_util.is_numeral(arg, v)) - result = m_util.mk_numeral(floor(v), true); - else if (m_util.is_to_real(arg)) - result = to_app(arg)->get_arg(0); - else - result = m_util.mk_to_int(arg); -} - -void arith_simplifier_plugin::mk_is_int(expr * arg, expr_ref & result) { - numeral v; - if (m_util.is_numeral(arg, v)) - result = v.is_int()?m_manager.mk_true():m_manager.mk_false(); - else if (m_util.is_to_real(arg)) - result = m_manager.mk_true(); - else - result = m_util.mk_is_int(arg); -} - -bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - set_reduce_invoked(); - SASSERT(f->get_family_id() == m_fid); - TRACE("arith_simplifier_plugin", tout << mk_pp(f, m_manager) << "\n"; - for (unsigned i = 0; i < num_args; i++) tout << mk_pp(args[i], m_manager) << "\n";); - arith_op_kind k = static_cast(f->get_decl_kind()); - switch (k) { - case OP_NUM: return false; - case OP_LE: if (m_presimp) return false; SASSERT(num_args == 2); mk_le(args[0], args[1], result); break; - case OP_GE: if (m_presimp) return false; SASSERT(num_args == 2); mk_ge(args[0], args[1], result); break; - case OP_LT: if (m_presimp) return false; SASSERT(num_args == 2); mk_lt(args[0], args[1], result); break; - case OP_GT: if (m_presimp) return false; SASSERT(num_args == 2); mk_gt(args[0], args[1], result); break; - case OP_ADD: mk_add(num_args, args, result); break; - case OP_SUB: mk_sub(num_args, args, result); break; - case OP_UMINUS: SASSERT(num_args == 1); mk_uminus(args[0], result); break; - case OP_MUL: - mk_mul(num_args, args, result); - TRACE("arith_simplifier_plugin", tout << mk_pp(result, m_manager) << "\n";); - break; - case OP_DIV: SASSERT(num_args == 2); mk_div(args[0], args[1], result); break; - case OP_IDIV: SASSERT(num_args == 2); mk_idiv(args[0], args[1], result); break; - case OP_REM: SASSERT(num_args == 2); mk_rem(args[0], args[1], result); break; - case OP_MOD: SASSERT(num_args == 2); mk_mod(args[0], args[1], result); break; - case OP_TO_REAL: SASSERT(num_args == 1); mk_to_real(args[0], result); break; - case OP_TO_INT: SASSERT(num_args == 1); mk_to_int(args[0], result); break; - case OP_IS_INT: SASSERT(num_args == 1); mk_is_int(args[0], result); break; - case OP_POWER: return false; - case OP_ABS: SASSERT(num_args == 1); mk_abs(args[0], result); break; - case OP_IRRATIONAL_ALGEBRAIC_NUM: return false; - default: - return false; - } - TRACE("arith_simplifier_plugin", tout << mk_pp(result.get(), m_manager) << "\n";); - return true; -} - -void arith_simplifier_plugin::mk_abs(expr * arg, expr_ref & result) { - expr_ref c(m_manager); - expr_ref m_arg(m_manager); - mk_uminus(arg, m_arg); - mk_ge(arg, m_util.mk_numeral(rational(0), m_util.is_int(arg)), c); - m_bsimp.mk_ite(c, arg, m_arg, result); -} - -bool arith_simplifier_plugin::is_arith_term(expr * n) const { - return n->get_kind() == AST_APP && to_app(n)->get_family_id() == m_fid; -} - -bool arith_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) { - TRACE("reduce_eq_bug", tout << mk_ismt2_pp(lhs, m_manager) << "\n" << mk_ismt2_pp(rhs, m_manager) << "\n";); - set_reduce_invoked(); - if (m_presimp) { - return false; - } - if (m_params.m_arith_expand_eqs) { - expr_ref le(m_manager), ge(m_manager); - mk_le_ge_eq_core(lhs, rhs, le); - mk_le_ge_eq_core(lhs, rhs, ge); - m_bsimp.mk_and(le, ge, result); - return true; - } - - if (m_params.m_arith_process_all_eqs || is_arith_term(lhs) || is_arith_term(rhs)) { - mk_arith_eq(lhs, rhs, result); - return true; - } - return false; -} - - - diff --git a/src/ast/simplifier/arith_simplifier_plugin.h b/src/ast/simplifier/arith_simplifier_plugin.h deleted file mode 100644 index 21ab8f6b4..000000000 --- a/src/ast/simplifier/arith_simplifier_plugin.h +++ /dev/null @@ -1,96 +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 "ast/simplifier/basic_simplifier_plugin.h" -#include "ast/simplifier/poly_simplifier_plugin.h" -#include "ast/arith_decl_plugin.h" -#include "ast/simplifier/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); - -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/ast/simplifier/array_simplifier_params.cpp b/src/ast/simplifier/array_simplifier_params.cpp deleted file mode 100644 index ff7dba25f..000000000 --- a/src/ast/simplifier/array_simplifier_params.cpp +++ /dev/null @@ -1,26 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - array_simplifier_params.cpp - -Abstract: - - This file was created during code reorg. - -Author: - - Leonardo de Moura (leonardo) 2012-12-02. - -Revision History: - ---*/ -#include "ast/simplifier/array_simplifier_params.h" -#include "ast/simplifier/array_simplifier_params_helper.hpp" - -void array_simplifier_params::updt_params(params_ref const & _p) { - array_simplifier_params_helper p(_p); - m_array_canonize_simplify = p.array_canonize(); - m_array_simplify = p.array_simplify(); -} diff --git a/src/ast/simplifier/array_simplifier_params.h b/src/ast/simplifier/array_simplifier_params.h deleted file mode 100644 index 07ead5fd6..000000000 --- a/src/ast/simplifier/array_simplifier_params.h +++ /dev/null @@ -1,34 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - array_simplifier_params.h - -Abstract: - - This file was created during code reorg. - -Author: - - Leonardo de Moura (leonardo) 2012-12-02. - -Revision History: - ---*/ -#ifndef ARRAY_SIMPLIFIER_PARAMS_H_ -#define ARRAY_SIMPLIFIER_PARAMS_H_ - -#include "util/params.h" - -struct array_simplifier_params1 { - - array_simplifier_params1(params_ref const & p = params_ref()) { - updt_params(p); - } - - void updt_params(params_ref const & _p); -}; - -#endif /* ARITH_SIMPLIFIER_PARAMS_H_ */ - diff --git a/src/ast/simplifier/array_simplifier_params_helper.pyg b/src/ast/simplifier/array_simplifier_params_helper.pyg deleted file mode 100644 index 93c184c23..000000000 --- a/src/ast/simplifier/array_simplifier_params_helper.pyg +++ /dev/null @@ -1,6 +0,0 @@ -def_module_params(class_name='array_simplifier_params_helper', - module_name="old_simplify", # Parameters will be in the old_simplify module - export=True, - params=( - ('array.canonize', BOOL, False, 'normalize array terms into normal form during simplification'), - ('array.simplify', BOOL, True, 'enable/disable array simplifications'))) diff --git a/src/ast/simplifier/array_simplifier_plugin.cpp b/src/ast/simplifier/array_simplifier_plugin.cpp deleted file mode 100644 index 754daab69..000000000 --- a/src/ast/simplifier/array_simplifier_plugin.cpp +++ /dev/null @@ -1,877 +0,0 @@ -/*++ -Copyright (c) 2008 Microsoft Corporation - -Module Name: - - array_simplifier_plugin.cpp - -Abstract: - - - -Author: - - Nikolaj Bjorner (nbjorner) 2008-05-05 - -Revision History: - -Notes TODO: - - Examine quadratic cost of simplification vs. model-based procedure. - - Parameterize cache replacement strategy. - Some parameters are hard-wired. - ---*/ - -#include "ast/simplifier/array_simplifier_plugin.h" -#include "ast/ast_ll_pp.h" -#include "ast/ast_pp.h" - - -array_simplifier_plugin::array_simplifier_plugin( - ast_manager & m, - basic_simplifier_plugin& s, - simplifier& simp, - array_simplifier_params const& p) : - simplifier_plugin(symbol("array"),m), - m_util(m), - m_simp(s), - m_simplifier(simp), - m_params(p), - m_store_cache_size(0) -{} - - -array_simplifier_plugin::~array_simplifier_plugin() { - - select_cache::iterator it = m_select_cache.begin(); - select_cache::iterator end = m_select_cache.end(); - for ( ; it != end; ++it) { - m_manager.dec_array_ref(it->m_key->size(), it->m_key->c_ptr()); - m_manager.dec_ref(it->m_value); - dealloc(it->m_key); - } - - store_cache::iterator it2 = m_store_cache.begin(); - store_cache::iterator end2 = m_store_cache.end(); - for (; it2 != end2; ++it2) { - m_manager.dec_ref(it->m_value); - dealloc(it->m_key); - } -} - - -bool array_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - if (!m_params.m_array_simplify) - return false; - set_reduce_invoked(); - if (m_presimp) - return false; -#if Z3DEBUG - for (unsigned i = 0; i < num_args && i < f->get_arity(); ++i) { - SASSERT(m_manager.get_sort(args[i]) == f->get_domain(i)); - } -#endif - TRACE("array_simplifier", { - tout << mk_pp(f, m_manager) << " "; - for (unsigned i = 0; i < num_args; ++i) { - tout << mk_pp(args[i], m_manager) << " "; - } - tout << "\n"; - } - ); - SASSERT(f->get_family_id() == m_fid); - switch(f->get_decl_kind()) { - case OP_SELECT: - mk_select(num_args, args, result); - break; - case OP_STORE: - mk_store(f, num_args, args, result); - break; - case OP_SET_UNION: { - sort* s = f->get_range(); - expr_ref empty(m_manager); - mk_empty_set(s, empty); - switch(num_args) { - case 0: - result = empty; - break; - case 1: - result = args[0]; - break; - default: { - result = args[0]; - func_decl* f_or = m_manager.mk_or_decl(); - for (unsigned i = 1; i < num_args; ++i) { - mk_map(f_or, result, args[i], result); - } - break; - } - } - break; - } - case OP_SET_INTERSECT: { - expr_ref full(m_manager); - mk_full_set(f->get_range(), full); - switch(num_args) { - case 0: - result = full; - break; - case 1: - result = args[0]; - break; - default: { - result = args[0]; - func_decl* f_and = m_manager.mk_and_decl(); - for (unsigned i = 1; i < num_args; ++i) { - mk_map(f_and, result, args[i], result); - } - break; - } - } - TRACE("array_simplifier", tout << "sort " << mk_pp(result.get(), m_manager) << "\n";); - break; - } - case OP_SET_SUBSET: { - SASSERT(num_args == 2); - expr_ref diff(m_manager), emp(m_manager); - mk_set_difference(num_args, args, diff); - mk_empty_set(m_manager.get_sort(args[0]), emp); - m_simp.mk_eq(diff.get(), emp.get(), result); - break; - } - case OP_SET_COMPLEMENT: { - SASSERT(num_args == 1); - func_decl* f_not = m_manager.mk_not_decl(); - mk_map(f_not, args[0], result); - break; - } - case OP_SET_DIFFERENCE: { - SASSERT(num_args == 2); - expr_ref r1(m_manager); - mk_map(m_manager.mk_not_decl(), args[1], r1); - mk_map(m_manager.mk_and_decl(), args[0], r1, result); - break; - } - case OP_ARRAY_MAP: { - SASSERT(f->get_num_parameters() == 1); - SASSERT(f->get_parameter(0).is_ast()); - SASSERT(is_func_decl(f->get_parameter(0).get_ast())); - // - // map_d (store a j v) = (store (map_f a) v (d v)) - // - if (num_args == 1 && is_store(args[0])) { - app* store_expr = to_app(args[0]); - unsigned num_args = store_expr->get_num_args(); - SASSERT(num_args >= 3); - parameter p = f->get_parameter(0); - func_decl* d = to_func_decl(p.get_ast()); - expr* a = store_expr->get_arg(0); - expr* v = store_expr->get_arg(num_args-1); - // expr*const* args = store_expr->get_args()+1; - expr_ref r1(m_manager), r2(m_manager); - ptr_vector new_args; - - reduce(f, 1, &a, r1); - m_simplifier.mk_app(d, 1, &v, r2); - new_args.push_back(r1); - for (unsigned i = 1; i + 1 < num_args; ++i) { - new_args.push_back(store_expr->get_arg(i)); - } - new_args.push_back(r2); - mk_store(store_expr->get_decl(), num_args, new_args.c_ptr(), result); - break; - } - - // - // map_d (store a j v) (store b j w) = (store (map_f a b) j (d v w)) - // - if (num_args > 1 && same_store(num_args, args)) { - app* store_expr1 = to_app(args[0]); - unsigned num_indices = store_expr1->get_num_args(); - SASSERT(num_indices >= 3); - parameter p = f->get_parameter(0); - func_decl* d = to_func_decl(p.get_ast()); - ptr_vector arrays; - ptr_vector values; - for (unsigned i = 0; i < num_args; ++i) { - arrays.push_back(to_app(args[i])->get_arg(0)); - values.push_back(to_app(args[i])->get_arg(num_indices-1)); - } - - expr_ref r1(m_manager), r2(m_manager); - reduce(f, arrays.size(), arrays.c_ptr(), r1); - m_simplifier.mk_app(d, values.size(), values.c_ptr(), r2); - ptr_vector new_args; - new_args.push_back(r1); - for (unsigned i = 1; i + 1 < num_indices; ++i) { - new_args.push_back(store_expr1->get_arg(i)); - } - new_args.push_back(r2); - mk_store(store_expr1->get_decl(), new_args.size(), new_args.c_ptr(), result); - break; - } - // - // map_d (const v) = (const (d v)) - // - if (num_args == 1 && is_const_array(args[0])) { - app* const_expr = to_app(args[0]); - SASSERT(const_expr->get_num_args() == 1); - parameter p = f->get_parameter(0); - func_decl* d = to_func_decl(p.get_ast()); - expr* v = const_expr->get_arg(0); - expr_ref r1(m_manager); - - m_simplifier.mk_app(d, 1, &v, r1); - expr* arg = r1.get(); - parameter param(f->get_range()); - result = m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, ¶m, 1, &arg); - break; - } - // - // map_d (const v) (const w) = (const (d v w)) - // - if (num_args > 1 && all_const_array(num_args, args)) { - parameter p = f->get_parameter(0); - func_decl* d = to_func_decl(p.get_ast()); - ptr_vector values; - for (unsigned i = 0; i < num_args; ++i) { - values.push_back(to_app(args[i])->get_arg(0)); - } - expr_ref r1(m_manager); - - m_simplifier.mk_app(d, values.size(), values.c_ptr(), r1); - expr* arg = r1.get(); - parameter param(f->get_range()); - result = m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, ¶m, 1, &arg); - break; - } - result = m_manager.mk_app(f, num_args, args); - - break; - } - default: - result = m_manager.mk_app(f, num_args, args); - break; - } - TRACE("array_simplifier", - tout << mk_pp(result.get(), m_manager) << "\n";); - - return true; -} - -bool array_simplifier_plugin::same_store(unsigned num_args, expr* const* args) const { - if (num_args == 0) { - return true; - } - if (!is_store(args[0])) { - return false; - } - SASSERT(to_app(args[0])->get_num_args() >= 3); - unsigned num_indices = to_app(args[0])->get_num_args() - 2; - for (unsigned i = 1; i < num_args; ++i) { - if (!is_store(args[i])) { - return false; - } - for (unsigned j = 1; j < num_indices + 1; ++j) { - if (to_app(args[0])->get_arg(j) != to_app(args[i])->get_arg(j)) { - return false; - } - } - } - return true; -} - -bool array_simplifier_plugin::all_const_array(unsigned num_args, expr* const* args) const { - bool is_const = true; - for (unsigned i = 0; is_const && i < num_args; ++i) { - is_const = is_const_array(args[i]); - } - return is_const; -} - -bool array_simplifier_plugin::all_values(unsigned num_args, expr* const* args) const { - for (unsigned i = 0; i < num_args; ++i) { - if (!m_manager.is_unique_value(args[i])) { - return false; - } - } - return true; -} - -bool array_simplifier_plugin::lex_lt(unsigned num_args, expr* const* args1, expr* const* args2) { - for (unsigned i = 0; i < num_args; ++i) { - TRACE("array_simplifier", - tout << mk_pp(args1[i], m_manager) << "\n"; - tout << mk_pp(args2[i], m_manager) << "\n"; - tout << args1[i]->get_id() << " " << args2[i]->get_id() << "\n"; - ); - - if (args1[i]->get_id() < args2[i]->get_id()) return true; - if (args1[i]->get_id() > args2[i]->get_id()) return false; - } - return false; -} - - -void array_simplifier_plugin::get_stores(expr* n, unsigned& arity, expr*& m, ptr_vector& stores) { - while (is_store(n)) { - app* a = to_app(n); - SASSERT(a->get_num_args() > 2); - arity = a->get_num_args()-2; - n = a->get_arg(0); - stores.push_back(a->get_args()+1); - } - m = n; -} - -lbool array_simplifier_plugin::eq_default(expr* def, unsigned arity, unsigned num_st, expr*const* const* st) { - bool all_diseq = m_manager.is_unique_value(def) && num_st > 0; - bool all_eq = true; - for (unsigned i = 0; i < num_st; ++i) { - all_eq &= (st[i][arity] == def); - all_diseq &= m_manager.is_unique_value(st[i][arity]) && (st[i][arity] != def); - TRACE("array_simplifier", tout << m_manager.is_unique_value(st[i][arity]) << " " << mk_pp(st[i][arity], m_manager) << "\n";); - } - if (all_eq) { - return l_true; - } - if (all_diseq) { - return l_false; - } - return l_undef; -} - - -bool array_simplifier_plugin::insert_table(expr* def, unsigned arity, unsigned num_st, expr*const* const* st, arg_table& table) { - for (unsigned i = 0; i < num_st; ++i ) { - for (unsigned j = 0; j < arity; ++j) { - if (!m_manager.is_unique_value(st[i][j])) { - return false; - } - } - TRACE("array_simplifier", tout << "inserting: "; - for (unsigned j = 0; j < arity; ++j) { - tout << mk_pp(st[i][j], m_manager) << " "; - } - tout << " |-> " << mk_pp(def, m_manager) << "\n"; - ); - args_entry e(arity, st[i]); - table.insert_if_not_there(e); - } - return true; -} - - -lbool array_simplifier_plugin::eq_stores(expr* def, unsigned arity, unsigned num_st1, expr*const* const* st1, unsigned num_st2, expr*const* const* st2) { - if (num_st1 == 0) { - return eq_default(def, arity, num_st2, st2); - } - if (num_st2 == 0) { - return eq_default(def, arity, num_st1, st1); - } - arg_table table1, table2; - if (!insert_table(def, arity, num_st1, st1, table1)) { - return l_undef; - } - if (!insert_table(def, arity, num_st2, st2, table2)) { - return l_undef; - } - - arg_table::iterator it = table1.begin(); - arg_table::iterator end = table1.end(); - for (; it != end; ++it) { - args_entry const & e1 = *it; - args_entry e2; - expr* v1 = e1.m_args[arity]; - if (table2.find(e1, e2)) { - expr* v2 = e2.m_args[arity]; - if (v1 == v2) { - table2.erase(e1); - continue; - } - if (m_manager.is_unique_value(v1) && m_manager.is_unique_value(v2)) { - return l_false; - } - return l_undef; - } - else if (m_manager.is_unique_value(v1) && m_manager.is_unique_value(def) && v1 != def) { - return l_false; - } - } - it = table2.begin(); - end = table2.end(); - for (; it != end; ++it) { - args_entry const & e = *it; - expr* v = e.m_args[arity]; - if (m_manager.is_unique_value(v) && m_manager.is_unique_value(def) && v != def) { - return l_false; - } - } - if (!table2.empty() || !table1.empty()) { - return l_undef; - } - return l_true; -} - - -bool array_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) { - set_reduce_invoked(); - expr* c1, *c2; - ptr_vector st1, st2; - unsigned arity1 = 0; - unsigned arity2 = 0; - get_stores(lhs, arity1, c1, st1); - get_stores(rhs, arity2, c2, st2); - if (arity1 == arity2 && is_const_array(c1) && is_const_array(c2)) { - c1 = to_app(c1)->get_arg(0); - c2 = to_app(c2)->get_arg(0); - if (c1 == c2) { - lbool eq = eq_stores(c1, arity2, st1.size(), st1.c_ptr(), st2.size(), st2.c_ptr()); - TRACE("array_simplifier", - tout << mk_pp(lhs, m_manager) << " = " - << mk_pp(rhs, m_manager) << " := " << eq << "\n"; - tout << "arity: " << arity1 << "\n";); - switch(eq) { - case l_false: - result = m_manager.mk_false(); - return true; - case l_true: - result = m_manager.mk_true(); - return true; - default: - return false; - } - } - else if (m_manager.is_unique_value(c1) && m_manager.is_unique_value(c2)) { - result = m_manager.mk_false(); - return true; - } - } - return false; -} - -bool array_simplifier_plugin::reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result) { - set_reduce_invoked(); - return false; -} - - -array_simplifier_plugin::const_select_result -array_simplifier_plugin::mk_select_const(expr* m, app* index, expr_ref& result) { - store_info* info = 0; - expr* r = 0, *a = 0; - if (!is_store(m)) { - return NOT_CACHED; - } - if (!m_store_cache.find(m, info)) { - return NOT_CACHED; - } - if (info->m_map.find(index, r)) { - result = r; - return FOUND_VALUE; - } - a = info->m_default.get(); - - // - // Unfold and cache the store while searching for value of index. - // - while (is_store(a) && m_manager.is_unique_value(to_app(a)->get_arg(1))) { - app* b = to_app(a); - app* c = to_app(b->get_arg(1)); - - if (!info->m_map.contains(c)) { - info->m_map.insert(c, b->get_arg(2)); - m_manager.inc_ref(b->get_arg(2)); - ++m_store_cache_size; - } - a = b->get_arg(0); - info->m_default = a; - - if (c == index) { - result = b->get_arg(2); - return FOUND_VALUE; - } - } - result = info->m_default.get(); - return FOUND_DEFAULT; -} - -void array_simplifier_plugin::cache_store(unsigned num_stores, expr* store_term) -{ - if (num_stores <= m_const_store_threshold) { - return; - } - prune_store_cache(); - if (!m_store_cache.contains(store_term)) { - store_info * info = alloc(store_info, m_manager, store_term); - m_manager.inc_ref(store_term); - m_store_cache.insert(store_term, info); - TRACE("cache_store", tout << m_store_cache.size() << "\n";); - ++m_store_cache_size; - } -} - -void array_simplifier_plugin::cache_select(unsigned num_args, expr * const * args, expr * result) { - ptr_vector * entry = alloc(ptr_vector); - entry->append(num_args, const_cast(args)); - const select_cache::key_data & kd = m_select_cache.insert_if_not_there(entry, result); - if (kd.m_key != entry) { - dealloc(entry); - return; - } - m_manager.inc_array_ref(num_args, args); - m_manager.inc_ref(result); - TRACE("cache_select", tout << m_select_cache.size() << "\n";); -} - - - -void array_simplifier_plugin::prune_select_cache() { - if (m_select_cache.size() > m_select_cache_max_size) { - flush_select_cache(); - } -} - -void array_simplifier_plugin::prune_store_cache() { - if (m_store_cache_size > m_store_cache_max_size) { - flush_store_cache(); - } -} - -void array_simplifier_plugin::flush_select_cache() { - select_cache::iterator it = m_select_cache.begin(); - select_cache::iterator end = m_select_cache.end(); - for (; it != end; ++it) { - ptr_vector * e = (*it).m_key; - m_manager.dec_array_ref(e->size(), e->begin()); - m_manager.dec_ref((*it).m_value); - dealloc(e); - } - m_select_cache.reset(); -} - -void array_simplifier_plugin::flush_store_cache() { - store_cache::iterator it = m_store_cache.begin(); - store_cache::iterator end = m_store_cache.end(); - for (; it != end; ++it) { - m_manager.dec_ref((*it).m_key); - const_map::iterator mit = (*it).m_value->m_map.begin(); - const_map::iterator mend = (*it).m_value->m_map.end(); - for (; mit != mend; ++mit) { - m_manager.dec_ref((*mit).m_value); - } - dealloc((*it).m_value); - } - m_store_cache.reset(); - m_store_cache_size = 0; -} - - -void array_simplifier_plugin::flush_caches() { - flush_select_cache(); - flush_store_cache(); -} - -void array_simplifier_plugin::mk_set_difference(unsigned num_args, expr * const * args, expr_ref & result) { - SASSERT(num_args == 2); - result = m_manager.mk_app(m_fid, OP_SET_DIFFERENCE, 0, 0, num_args, args); -} - -void array_simplifier_plugin::mk_empty_set(sort* ty, expr_ref & result) { - parameter param(ty); - expr* args[1] = { m_manager.mk_false() }; - result = m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, ¶m, 1, args); -} - -void array_simplifier_plugin::mk_full_set(sort* ty, expr_ref & result) { - parameter param(ty); - expr* args[1] = { m_manager.mk_true() }; - result = m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, ¶m, 1, args); -} - - -bool array_simplifier_plugin::same_args(unsigned num_args, expr * const * args1, expr * const * args2) { - for (unsigned i = 0; i < num_args; ++i) { - if (args1[i] != args2[i]) { - return false; - } - } - return true; -} - -void array_simplifier_plugin::mk_store(func_decl* f, unsigned num_args, expr * const * args, expr_ref & result) { - - SASSERT(num_args >= 3); - - expr* arg0 = args[0]; - expr* argn = args[num_args-1]; - - // - // store(store(a,i,v),i,w) = store(a,i,w) - // - if (is_store(arg0) && - same_args(num_args-2, args+1, to_app(arg0)->get_args()+1)) { - expr_ref_buffer new_args(m_manager); - new_args.push_back(to_app(arg0)->get_arg(0)); - for (unsigned i = 1; i < num_args; ++i) { - new_args.push_back(args[i]); - } - reduce(f, num_args, new_args.c_ptr(), result); - TRACE("array_simplifier", tout << mk_pp(result.get(), m_manager) << "\n";); - return; - } - - // - // store(const(v),i,v) = const(v) - // - if (is_const_array(arg0) && - to_app(arg0)->get_arg(0) == args[num_args-1]) { - result = arg0; - TRACE("array_simplifier", tout << mk_pp(result.get(), m_manager) << "\n";); - return; - } - - // - // store(a, i, select(a, i)) = a - // - if (is_select(argn) && - (to_app(argn)->get_num_args() == num_args - 1) && - same_args(num_args-1, args, to_app(argn)->get_args())) { - TRACE("dummy_store", tout << "dummy store simplified mk_store(\n"; - for (unsigned i = 0; i < num_args; i++) ast_ll_pp(tout, m_manager, args[i]); - tout << ") =====>\n"; - ast_ll_pp(tout, m_manager, arg0);); - result = arg0; - TRACE("array_simplifier", tout << mk_pp(result.get(), m_manager) << "\n";); - return; - } - - // - // store(store(a,i,v),j,w) -> store(store(a,j,w),i,v) - // if i, j are values, i->get_id() < j->get_id() - // - if (m_params.m_array_canonize_simplify && - is_store(arg0) && - all_values(num_args-2, args+1) && - all_values(num_args-2, to_app(arg0)->get_args()+1) && - lex_lt(num_args-2, args+1, to_app(arg0)->get_args()+1)) { - expr* const* args2 = to_app(arg0)->get_args(); - expr_ref_buffer new_args(m_manager); - new_args.push_back(args2[0]); - for (unsigned i = 1; i < num_args; ++i) { - new_args.push_back(args[i]); - } - reduce(f, num_args, new_args.c_ptr(), result); - new_args.reset(); - new_args.push_back(result); - for (unsigned i = 1; i < num_args; ++i) { - new_args.push_back(args2[i]); - } - result = m_manager.mk_app(m_fid, OP_STORE, num_args, new_args.c_ptr()); - TRACE("array_simplifier", tout << mk_pp(result.get(), m_manager) << "\n";); - return; - } - - - result = m_manager.mk_app(m_fid, OP_STORE, num_args, args); - TRACE("array_simplifier", tout << "default: " << mk_pp(result.get(), m_manager) << "\n";); - -} - -void array_simplifier_plugin::mk_select_as_array(unsigned num_args, expr * const * args, expr_ref & result) { - SASSERT(is_as_array(args[0])); - func_decl * f = get_as_array_func_decl(to_app(args[0])); - result = m_manager.mk_app(f, num_args - 1, args+1); -} - -void array_simplifier_plugin::mk_select_as_array_tree(unsigned num_args, expr * const * args, expr_ref & result) { - SASSERT(is_as_array_tree(args[0])); - SASSERT(m_manager.is_ite(args[0])); - ptr_buffer todo; - obj_map cache; - app_ref_buffer trail(m_manager); - todo.push_back(to_app(args[0])); - while (!todo.empty()) { - app * curr = todo.back(); - SASSERT(m_manager.is_ite(curr)); - expr * branches[2] = {0, 0}; - bool visited = true; - for (unsigned i = 0; i < 2; i++) { - expr * arg = curr->get_arg(i+1); - if (is_as_array(arg)) { - branches[i] = m_manager.mk_app(get_as_array_func_decl(to_app(arg)), num_args - 1, args+1); - } - else { - SASSERT(m_manager.is_ite(arg)); - app * new_arg = 0; - if (!cache.find(to_app(arg), new_arg)) { - todo.push_back(to_app(arg)); - visited = false; - } - else { - branches[i] = new_arg; - } - } - } - if (visited) { - todo.pop_back(); - app * new_curr = m_manager.mk_ite(curr->get_arg(0), branches[0], branches[1]); - trail.push_back(new_curr); - cache.insert(curr, new_curr); - } - } - SASSERT(cache.contains(to_app(args[0]))); - app * r = 0; - cache.find(to_app(args[0]), r); - result = r; -} - -void array_simplifier_plugin::mk_select(unsigned num_args, expr * const * args, expr_ref & result) { - expr * r = 0; - - if (is_as_array(args[0])) { - mk_select_as_array(num_args, args, result); - return; - } - - if (is_as_array_tree(args[0])) { - mk_select_as_array_tree(num_args, args, result); - return; - } - - bool is_const_select = num_args == 2 && m_manager.is_unique_value(args[1]); - app* const_index = is_const_select?to_app(args[1]):0; - unsigned num_const_stores = 0; - expr_ref tmp(m_manager); - expr* args2[2]; - if (is_const_select) { - switch(mk_select_const(args[0], const_index, tmp)) { - case NOT_CACHED: - break; - case FOUND_VALUE: - TRACE("mk_select", tout << "found value\n"; ast_ll_pp(tout, m_manager, tmp.get()); ); - result = tmp.get(); - // value of select is stored under result. - return; - case FOUND_DEFAULT: - args2[0] = tmp.get(); - args2[1] = args[1]; - args = args2; - is_const_select = false; - break; - } - } - - SASSERT(num_args > 0); - ptr_vector & entry = m_tmp2; - entry.reset(); - entry.append(num_args, args); - expr * entry0 = entry[0]; - SASSERT(m_todo.empty()); - m_todo.push_back(entry0); - while (!m_todo.empty()) { - expr * m = m_todo.back(); - TRACE("array_simplifier", tout << mk_bounded_pp(m, m_manager) << "\n";); - if (is_store(m)) { - expr * nested_array = to_app(m)->get_arg(0); - expr * else_branch = 0; - entry[0] = nested_array; - if (is_const_select) { - if (m_manager.is_unique_value(to_app(m)->get_arg(1))) { - app* const_index2 = to_app(to_app(m)->get_arg(1)); - // - // we found the value, all other stores are different. - // there is no need to recurse. - // - if (const_index == const_index2) { - result = to_app(m)->get_arg(2); - cache_store(num_const_stores, args[0]); - m_todo.reset(); - return; - } - ++num_const_stores; - } - else { - is_const_select = false; - } - } - if (m_select_cache.find(&entry, else_branch)) { - expr_ref_buffer eqs(m_manager); - for (unsigned i = 1; i < num_args ; ++i) { - expr * a = args[i]; - expr * b = to_app(m)->get_arg(i); - expr_ref eq(m_manager); - m_simp.mk_eq(a, b, eq); - eqs.push_back(eq.get()); - } - expr_ref cond(m_manager); - m_simp.mk_and(eqs.size(), eqs.c_ptr(), cond); - expr * then_branch = to_app(m)->get_arg(num_args); - if (m_manager.is_true(cond.get())) { - result = then_branch; - } - else if (m_manager.is_false(cond.get())) { - result = else_branch; - } - else { - m_simp.mk_ite(cond.get(), then_branch, else_branch, result); - } - entry[0] = m; - cache_select(entry.size(), entry.c_ptr(), result.get()); - m_todo.pop_back(); - } - else { - m_todo.push_back(nested_array); - } - } - else if (is_const_array(m)) { - entry[0] = m; - cache_select(entry.size(), entry.c_ptr(), to_app(m)->get_arg(0)); - m_todo.pop_back(); - } - else { - entry[0] = m; - TRACE("array_simplifier", { - for (unsigned i = 0; i < entry.size(); ++i) { - tout << mk_bounded_pp(entry[i], m_manager) << ": " - << mk_bounded_pp(m_manager.get_sort(entry[i]), m_manager) << "\n"; - }} - ); - r = m_manager.mk_app(m_fid, OP_SELECT, 0, 0, entry.size(), entry.c_ptr()); - cache_select(entry.size(), entry.c_ptr(), r); - m_todo.pop_back(); - } - } - cache_store(num_const_stores, args[0]); - entry[0] = entry0; -#ifdef Z3DEBUG - bool f = -#endif - m_select_cache.find(&entry, r); - SASSERT(f); - result = r; - prune_select_cache(); - prune_store_cache(); - TRACE("mk_select", - for (unsigned i = 0; i < num_args; i++) { - ast_ll_pp(tout, m_manager, args[i]); tout << "\n"; - }; - tout << "is_store: " << is_store(args[0]) << "\n"; - ast_ll_pp(tout, m_manager, r);); -} - - -void array_simplifier_plugin::mk_map(func_decl* f, expr* a, expr* b, expr_ref& result) { - expr* exprs[2] = { a, b }; - parameter param(f); - result = m_manager.mk_app(m_fid, OP_ARRAY_MAP, 1, ¶m, 2, exprs ); -} - -void array_simplifier_plugin::mk_map(func_decl* f, expr* a, expr_ref& result) { - parameter param(f); - result = m_manager.mk_app(m_fid, OP_ARRAY_MAP, 1, ¶m, 1, &a ); -} - - diff --git a/src/ast/simplifier/array_simplifier_plugin.h b/src/ast/simplifier/array_simplifier_plugin.h deleted file mode 100644 index 62eb5e5ff..000000000 --- a/src/ast/simplifier/array_simplifier_plugin.h +++ /dev/null @@ -1,154 +0,0 @@ -/*++ -Copyright (c) 2008 Microsoft Corporation - -Module Name: - - array_simplifier_plugin.h - -Abstract: - - - -Author: - - Nikolaj Bjorner (nbjorner) 2008-05-05 - -Revision History: - ---*/ -#ifndef ARRAY_SIMPLIFIER_PLUGIN_H_ -#define ARRAY_SIMPLIFIER_PLUGIN_H_ - -#include "ast/ast.h" -#include "util/map.h" -#include "ast/array_decl_plugin.h" -#include "ast/simplifier/simplifier_plugin.h" -#include "ast/simplifier/basic_simplifier_plugin.h" -#include "ast/simplifier/array_simplifier_params.h" -#include "ast/simplifier/simplifier.h" -#include "util/obj_hashtable.h" -#include "util/lbool.h" - -class array_simplifier_plugin : public simplifier_plugin { - - typedef ptr_vector entry; - - struct entry_hash_proc { - unsigned operator()(ptr_vector * entry) const { - return get_exprs_hash(entry->size(), entry->begin(), 0xbeef1010); - } - }; - - struct entry_eq_proc { - bool operator()(ptr_vector * entry1, ptr_vector * entry2) const { - if (entry1->size() != entry2->size()) return false; - return compare_arrays(entry1->begin(), entry2->begin(), entry1->size()); - } - }; - - typedef map select_cache; - - struct args_entry { - unsigned m_arity; - expr* const* m_args; - args_entry(unsigned a, expr* const* args) : m_arity(a), m_args(args) {} - args_entry() : m_arity(0), m_args(0) {} - }; - - struct args_entry_hash_proc { - unsigned operator()(args_entry const& e) const { - return get_exprs_hash(e.m_arity, e.m_args, 0xbeef1010); - } - }; - struct args_entry_eq_proc { - bool operator()(args_entry const& e1, args_entry const& e2) const { - if (e1.m_arity != e2.m_arity) return false; - return compare_arrays(e1.m_args, e2.m_args, e1.m_arity); - } - }; - typedef hashtable arg_table; - - array_util m_util; - basic_simplifier_plugin& m_simp; - simplifier& m_simplifier; - array_simplifier_params const& m_params; - select_cache m_select_cache; - ptr_vector m_tmp; - ptr_vector m_tmp2; - ptr_vector m_todo; - static const unsigned m_select_cache_max_size = 100000; - typedef obj_map const_map; - class store_info { - store_info(); - store_info(store_info const&); - public: - const_map m_map; - expr_ref m_default; - store_info(ast_manager& m, expr* d): m_default(d, m) {} - }; - - typedef obj_map store_cache; - store_cache m_store_cache; - unsigned m_store_cache_size; - static const unsigned m_store_cache_max_size = 10000; - static const unsigned m_const_store_threshold = 5; - enum const_select_result { - NOT_CACHED, - FOUND_DEFAULT, - FOUND_VALUE - }; - - -public: - array_simplifier_plugin(ast_manager & m, basic_simplifier_plugin& s, simplifier& simp, array_simplifier_params const& p); - virtual ~array_simplifier_plugin(); - - 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); - - virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result); - - virtual void flush_caches(); - -private: - bool is_select(expr* n) const { return m_util.is_select(n); } - bool is_store(expr * n) const { return m_util.is_store(n); } - bool is_const_array(expr * n) const { return m_util.is_const(n); } - bool is_as_array(expr * n) const { return m_util.is_as_array(n); } - bool is_as_array_tree(expr * n) { return m_util.is_as_array_tree(n); } - func_decl * get_as_array_func_decl(app * n) const { return m_util.get_as_array_func_decl(n); } - void mk_select_as_array(unsigned num_args, expr * const * args, expr_ref & result); - void mk_select_as_array_tree(unsigned num_args, expr * const * args, expr_ref & result); - bool is_enumerated(expr* n, expr_ref& c, ptr_vector& keys, ptr_vector& vals); - const_select_result mk_select_const(expr* m, app* index, expr_ref& result); - void cache_store(unsigned num_stores, expr* nested_store); - void cache_select(unsigned num_args, expr * const * args, expr * result); - void prune_select_cache(); - void prune_store_cache(); - void flush_select_cache(); - void flush_store_cache(); - void mk_set_difference(unsigned num_args, expr * const * args, expr_ref & result); - void mk_empty_set(sort* ty, expr_ref & result); - void mk_full_set(sort* ty, expr_ref & result); - void mk_select(unsigned num_args, expr * const * args, expr_ref & result); - void mk_store(func_decl* f, unsigned num_args, expr * const * args, expr_ref & result); - void mk_map(func_decl* f, expr* a, expr* b, expr_ref & result); - void mk_map(func_decl* f, expr* a, expr_ref & result); - bool same_args(unsigned num_args, expr * const * args1, expr * const * args2); - - void get_stores(expr* n, unsigned& arity, expr*& m, ptr_vector& stores); - lbool eq_default(expr* def, unsigned arity, unsigned num_st, expr*const* const* st); - bool insert_table(expr* def, unsigned arity, unsigned num_st, expr*const* const* st, arg_table& table); - lbool eq_stores(expr* def, unsigned arity, unsigned num_st1, expr*const* const* st1, unsigned num_st2, expr*const* const* st2); - - bool same_store(unsigned num_args, expr* const* args) const; - bool all_const_array(unsigned num_args, expr* const* args) const; - bool all_values(unsigned num_args, expr* const* args) const; - bool lex_lt(unsigned num_args, expr* const* args1, expr* const* args2); - -}; - - -#endif /* ARRAY_SIMPLIFIER_PLUGIN_H_ */ - diff --git a/src/ast/simplifier/base_simplifier.h b/src/ast/simplifier/base_simplifier.h deleted file mode 100644 index 73a04d605..000000000 --- a/src/ast/simplifier/base_simplifier.h +++ /dev/null @@ -1,76 +0,0 @@ -/*++ -Copyright (c) 2007 Microsoft Corporation - -Module Name: - - base_simplifier.h - -Abstract: - - Base class for expression simplifier functors. - -Author: - - Leonardo (leonardo) 2008-01-11 - -Notes: - ---*/ -#ifndef BASE_SIMPLIFIER_H_ -#define BASE_SIMPLIFIER_H_ - -#include "ast/expr_map.h" -#include "ast/ast_pp.h" - -/** - \brief Implements basic functionality used by expression simplifiers. -*/ -class base_simplifier { -protected: - ast_manager & m; - expr_map m_cache; - ptr_vector m_todo; - - void cache_result(expr * n, expr * r, proof * p) { - m_cache.insert(n, r, p); - CTRACE("simplifier", !is_rewrite_proof(n, r, p), - tout << mk_pp(n, m) << "\n"; - tout << mk_pp(r, m) << "\n"; - tout << mk_pp(p, m) << "\n";); - SASSERT(is_rewrite_proof(n, r, p)); - } - void reset_cache() { m_cache.reset(); } - void flush_cache() { m_cache.flush(); } - void get_cached(expr * n, expr * & r, proof * & p) const { m_cache.get(n, r, p); } - - void reinitialize() { m_cache.set_store_proofs(m.fine_grain_proofs()); } - - - void visit(expr * n, bool & visited) { - if (!is_cached(n)) { - m_todo.push_back(n); - visited = false; - } - } - -public: - base_simplifier(ast_manager & m): - m(m), - m_cache(m, m.fine_grain_proofs()) { - } - bool is_cached(expr * n) const { return m_cache.contains(n); } - ast_manager & get_manager() { return m; } - - bool is_rewrite_proof(expr* n, expr* r, proof* p) { - if (p && - !m.is_undef_proof(p) && - !(m.has_fact(p) && - (m.is_eq(m.get_fact(p)) || m.is_oeq(m.get_fact(p)) || m.is_iff(m.get_fact(p))) && - to_app(m.get_fact(p))->get_arg(0) == n && - to_app(m.get_fact(p))->get_arg(1) == r)) return false; - - return (!m.fine_grain_proofs() || p || (n == r)); - } -}; - -#endif /* BASE_SIMPLIFIER_H_ */ diff --git a/src/ast/simplifier/basic_simplifier_plugin.cpp b/src/ast/simplifier/basic_simplifier_plugin.cpp deleted file mode 100644 index be51bc291..000000000 --- a/src/ast/simplifier/basic_simplifier_plugin.cpp +++ /dev/null @@ -1,147 +0,0 @@ -/*++ -Copyright (c) 2007 Microsoft Corporation - -Module Name: - - basic_simplifier_plugin.cpp - -Abstract: - - Simplifier for the basic family. - -Author: - - Leonardo (leonardo) 2008-01-07 - ---*/ -#include "ast/simplifier/basic_simplifier_plugin.h" -#include "ast/ast_ll_pp.h" -#include "ast/rewriter/bool_rewriter.h" - -basic_simplifier_plugin::basic_simplifier_plugin(ast_manager & m): - simplifier_plugin(symbol("basic"), m), - m_rewriter(alloc(bool_rewriter, m)) { -} - -basic_simplifier_plugin::~basic_simplifier_plugin() { - dealloc(m_rewriter); -} - -bool basic_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - set_reduce_invoked(); - SASSERT(f->get_family_id() == m_manager.get_basic_family_id()); - basic_op_kind k = static_cast(f->get_decl_kind()); - switch (k) { - case OP_FALSE: - case OP_TRUE: - return false; - case OP_EQ: - SASSERT(num_args == 2); - mk_eq(args[0], args[1], result); - return true; - case OP_DISTINCT: - mk_distinct(num_args, args, result); - return true; - case OP_ITE: - SASSERT(num_args == 3); - mk_ite(args[0], args[1], args[2], result); - return true; - case OP_AND: - mk_and(num_args, args, result); - return true; - case OP_OR: - mk_or(num_args, args, result); - return true; - case OP_IMPLIES: - mk_implies(args[0], args[1], result); - return true; - case OP_IFF: - mk_iff(args[0], args[1], result); - return true; - case OP_XOR: - switch (num_args) { - case 0: result = m_manager.mk_true(); break; - case 1: result = args[0]; break; - case 2: mk_xor(args[0], args[1], result); break; - default: UNREACHABLE(); break; - } - return true; - case OP_NOT: - SASSERT(num_args == 1); - mk_not(args[0], result); - return true; - default: - UNREACHABLE(); - return false; - } -} - -/** - \brief Return true if \c rhs is of the form (ite c t1 t2) and are_distinct(lhs, t1) and are_distinct(lhs, t2). -*/ -static bool is_lhs_diseq_rhs_ite_branches(ast_manager & m, expr * lhs, expr * rhs) { - return m.is_ite(rhs) && m.are_distinct(lhs, to_app(rhs)->get_arg(1)) && m.are_distinct(lhs, to_app(rhs)->get_arg(2)); -} - -/** - \brief Return true if \c rhs is of the form (ite c t1 t2) and lhs = t1 && are_distinct(lhs, t2) -*/ -static bool is_lhs_eq_rhs_ite_then(ast_manager & m, expr * lhs, expr * rhs) { - return m.is_ite(rhs) && lhs == to_app(rhs)->get_arg(1) && m.are_distinct(lhs, to_app(rhs)->get_arg(2)); -} - -/** - \brief Return true if \c rhs is of the form (ite c t1 t2) and are_distinct(lhs,t1) && lhs = t2 -*/ -static bool is_lhs_eq_rhs_ite_else(ast_manager & m, expr * lhs, expr * rhs) { - return m.is_ite(rhs) && lhs == to_app(rhs)->get_arg(2) && m.are_distinct(lhs, to_app(rhs)->get_arg(1)); -} - -void basic_simplifier_plugin::mk_eq(expr * lhs, expr * rhs, expr_ref & result) { - // (= t1 (ite C t2 t3)) --> false if are_distinct(t1, t2) && are_distinct(t1, t3) - if (is_lhs_diseq_rhs_ite_branches(m_manager, lhs, rhs) || is_lhs_diseq_rhs_ite_branches(m_manager, rhs, lhs)) { - result = m_manager.mk_false(); - } - // (= t1 (ite C t2 t3)) --> C if t1 = t2 && are_distinct(t1, t3) - else if (is_lhs_eq_rhs_ite_then(m_manager, lhs, rhs)) { - result = to_app(rhs)->get_arg(0); - } - // (= t1 (ite C t2 t3)) --> C if t1 = t2 && are_distinct(t1, t3) - else if (is_lhs_eq_rhs_ite_then(m_manager, rhs, lhs)) { - result = to_app(lhs)->get_arg(0); - } - // (= t1 (ite C t2 t3)) --> (not C) if t1 = t3 && are_distinct(t1, t2) - else if (is_lhs_eq_rhs_ite_else(m_manager, lhs, rhs)) { - mk_not(to_app(rhs)->get_arg(0), result); - } - // (= t1 (ite C t2 t3)) --> (not C) if t1 = t3 && are_distinct(t1, t2) - else if (is_lhs_eq_rhs_ite_else(m_manager, rhs, lhs)) { - mk_not(to_app(lhs)->get_arg(0), result); - } - else { - m_rewriter->mk_eq(lhs, rhs, result); - } -} - -bool basic_simplifier_plugin::eliminate_and() const { return m_rewriter->elim_and(); } -void basic_simplifier_plugin::set_eliminate_and(bool f) { m_rewriter->set_elim_and(f); } -void basic_simplifier_plugin::mk_iff(expr * lhs, expr * rhs, expr_ref & result) { mk_eq(lhs, rhs, result); } -void basic_simplifier_plugin::mk_xor(expr * lhs, expr * rhs, expr_ref & result) { m_rewriter->mk_xor(lhs, rhs, result); } -void basic_simplifier_plugin::mk_implies(expr * lhs, expr * rhs, expr_ref & result) { m_rewriter->mk_implies(lhs, rhs, result); } -void basic_simplifier_plugin::mk_ite(expr * c, expr * t, expr * e, expr_ref & result) { m_rewriter->mk_ite(c, t, e, result); } -void basic_simplifier_plugin::mk_and(unsigned num_args, expr * const * args, expr_ref & result) { m_rewriter->mk_and(num_args, args, result); } -void basic_simplifier_plugin::mk_or(unsigned num_args, expr * const * args, expr_ref & result) { m_rewriter->mk_or(num_args, args, result); } -void basic_simplifier_plugin::mk_and(expr * arg1, expr * arg2, expr_ref & result) { m_rewriter->mk_and(arg1, arg2, result); } -void basic_simplifier_plugin::mk_or(expr * arg1, expr * arg2, expr_ref & result) { m_rewriter->mk_or(arg1, arg2, result); } -void basic_simplifier_plugin::mk_and(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { m_rewriter->mk_and(arg1, arg2, arg3, result); } -void basic_simplifier_plugin::mk_or(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { m_rewriter->mk_or(arg1, arg2, arg3, result); } -void basic_simplifier_plugin::mk_nand(unsigned num_args, expr * const * args, expr_ref & result) { m_rewriter->mk_nand(num_args, args, result); } -void basic_simplifier_plugin::mk_nor(unsigned num_args, expr * const * args, expr_ref & result) { m_rewriter->mk_nor(num_args, args, result); } -void basic_simplifier_plugin::mk_nand(expr * arg1, expr * arg2, expr_ref & result) { m_rewriter->mk_nand(arg1, arg2, result); } -void basic_simplifier_plugin::mk_nor(expr * arg1, expr * arg2, expr_ref & result) { m_rewriter->mk_nor(arg1, arg2, result); } -void basic_simplifier_plugin::mk_distinct(unsigned num_args, expr * const * args, expr_ref & result) { m_rewriter->mk_distinct(num_args, args, result); } -void basic_simplifier_plugin::mk_not(expr * n, expr_ref & result) { m_rewriter->mk_not(n, result); } - -void basic_simplifier_plugin::enable_ac_support(bool flag) { - m_rewriter->set_flat(flag); -} diff --git a/src/ast/simplifier/basic_simplifier_plugin.h b/src/ast/simplifier/basic_simplifier_plugin.h deleted file mode 100644 index f28a19b56..000000000 --- a/src/ast/simplifier/basic_simplifier_plugin.h +++ /dev/null @@ -1,78 +0,0 @@ -/*++ -Copyright (c) 2007 Microsoft Corporation - -Module Name: - - basic_simplifier_plugin.h - -Abstract: - - Simplifier for the basic family. - -Author: - - Leonardo (leonardo) 2008-01-07 - ---*/ -#ifndef BASIC_SIMPLIFIER_PLUGIN_H_ -#define BASIC_SIMPLIFIER_PLUGIN_H_ - -#include "ast/simplifier/simplifier_plugin.h" - -class bool_rewriter; - -/** - \brief Simplifier for the basic family. -*/ -class basic_simplifier_plugin : public simplifier_plugin { - bool_rewriter * m_rewriter; -public: - basic_simplifier_plugin(ast_manager & m); - virtual ~basic_simplifier_plugin(); - bool_rewriter & get_rewriter() { return *m_rewriter; } - bool eliminate_and() const; - void set_eliminate_and(bool f); - void mk_eq(expr * lhs, expr * rhs, expr_ref & result); - void mk_iff(expr * lhs, expr * rhs, expr_ref & result); - void mk_xor(expr * lhs, expr * rhs, expr_ref & result); - void mk_implies(expr * lhs, expr * rhs, expr_ref & result); - void mk_ite(expr * c, expr * t, expr * e, expr_ref & result); - void mk_and(unsigned num_args, expr * const * args, expr_ref & result); - void mk_or(unsigned num_args, expr * const * args, expr_ref & result); - void mk_and(expr * arg1, expr * arg2, expr_ref & result); - void mk_or(expr * arg1, expr * arg2, expr_ref & result); - void mk_and(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); - void mk_or(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); - void mk_nand(unsigned num_args, expr * const * args, expr_ref & result); - void mk_nor(unsigned num_args, expr * const * args, expr_ref & result); - void mk_nand(expr * arg1, expr * arg2, expr_ref & result); - void mk_nor(expr * arg1, expr * arg2, expr_ref & result); - void mk_distinct(unsigned num_args, expr * const * args, expr_ref & result); - void mk_not(expr * n, expr_ref & result); - virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); - virtual void enable_ac_support(bool flag); -}; - -/** - \brief Functor that compares expressions, but puts the expressions e and f(e) close to each other, where - f is in family m_fid, and has kind m_dkind; -*/ -struct expr_lt_proc { - family_id m_fid; - decl_kind m_dkind; - - expr_lt_proc(family_id fid = null_family_id, decl_kind k = null_decl_kind):m_fid(fid), m_dkind(k) {} - - unsigned get_id(expr * n) const { - if (m_fid != null_family_id && is_app_of(n, m_fid, m_dkind)) - return (to_app(n)->get_arg(0)->get_id() << 1) + 1; - else - return n->get_id() << 1; - } - - bool operator()(expr * n1, expr * n2) const { - return get_id(n1) < get_id(n2); - } -}; - -#endif /* BASIC_SIMPLIFIER_PLUGIN_H_ */ diff --git a/src/ast/simplifier/bv_elim.cpp b/src/ast/simplifier/bv_elim.cpp deleted file mode 100644 index 1c0048a07..000000000 --- a/src/ast/simplifier/bv_elim.cpp +++ /dev/null @@ -1,119 +0,0 @@ - -/*++ -Copyright (c) 2015 Microsoft Corporation - ---*/ - -#include "ast/simplifier/bv_elim.h" -#include "ast/bv_decl_plugin.h" -#include "ast/rewriter/var_subst.h" -#include - -void bv_elim::elim(quantifier* q, quantifier_ref& r) { - - svector names, _names; - sort_ref_buffer sorts(m), _sorts(m); - expr_ref_buffer pats(m); - expr_ref_buffer no_pats(m); - expr_ref_buffer subst_map(m), _subst_map(m); - var_subst subst(m); - bv_util bv(m); - expr_ref new_body(m); - expr* old_body = q->get_expr(); - unsigned num_decls = q->get_num_decls(); - family_id bfid = m.mk_family_id("bv"); - - // - // Traverse sequence of bound variables to eliminate - // bit-vecctor variables and replace them by - // Booleans. - // - unsigned var_idx = 0; - for (unsigned i = num_decls; i > 0; ) { - --i; - sort* s = q->get_decl_sort(i); - symbol nm = q->get_decl_name(i); - - if (bv.is_bv_sort(s)) { - // convert n-bit bit-vector variable into sequence of n-Booleans. - unsigned num_bits = bv.get_bv_size(s); - expr_ref_buffer args(m); - expr_ref bv(m); - for (unsigned j = 0; j < num_bits; ++j) { - std::ostringstream new_name; - new_name << nm.str(); - new_name << "_"; - new_name << j; - var* v = m.mk_var(var_idx++, m.mk_bool_sort()); - args.push_back(v); - _sorts.push_back(m.mk_bool_sort()); - _names.push_back(symbol(new_name.str().c_str())); - } - bv = m.mk_app(bfid, OP_MKBV, 0, 0, args.size(), args.c_ptr()); - _subst_map.push_back(bv.get()); - } - else { - _subst_map.push_back(m.mk_var(var_idx++, s)); - _sorts.push_back(s); - _names.push_back(nm); - } - } - // - // reverse the vectors. - // - SASSERT(_names.size() == _sorts.size()); - for (unsigned i = _names.size(); i > 0; ) { - --i; - names.push_back(_names[i]); - sorts.push_back(_sorts[i]); - } - for (unsigned i = _subst_map.size(); i > 0; ) { - --i; - subst_map.push_back(_subst_map[i]); - } - - expr* const* sub = subst_map.c_ptr(); - unsigned sub_size = subst_map.size(); - - subst(old_body, sub_size, sub, new_body); - - for (unsigned j = 0; j < q->get_num_patterns(); j++) { - expr_ref pat(m); - subst(q->get_pattern(j), sub_size, sub, pat); - pats.push_back(pat); - } - for (unsigned j = 0; j < q->get_num_no_patterns(); j++) { - expr_ref nopat(m); - subst(q->get_no_pattern(j), sub_size, sub, nopat); - no_pats.push_back(nopat); - } - - r = m.mk_quantifier(true, - names.size(), - sorts.c_ptr(), - names.c_ptr(), - new_body.get(), - q->get_weight(), - q->get_qid(), - q->get_skid(), - pats.size(), pats.c_ptr(), - no_pats.size(), no_pats.c_ptr()); -} - -bool bv_elim_star::visit_quantifier(quantifier* q) { - // behave like destructive resolution, do not recurse. - return true; -} - -void bv_elim_star::reduce1_quantifier(quantifier* q) { - quantifier_ref r(m); - proof_ref pr(m); - m_bv_elim.elim(q, r); - if (m.fine_grain_proofs()) { - pr = m.mk_rewrite(q, r.get()); - } - else { - pr = 0; - } - cache_result(q, r, pr); -} diff --git a/src/ast/simplifier/bv_elim.h b/src/ast/simplifier/bv_elim.h deleted file mode 100644 index c027b1a9e..000000000 --- a/src/ast/simplifier/bv_elim.h +++ /dev/null @@ -1,45 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - bv_elim.h - -Abstract: - - Eliminate bit-vectors variables from clauses, by - replacing them by bound Boolean variables. - -Author: - - Nikolaj Bjorner (nbjorner) 2008-12-16. - -Revision History: - ---*/ -#ifndef BV_ELIM_H_ -#define BV_ELIM_H_ - -#include "ast/ast.h" -#include "ast/simplifier/simplifier.h" - -class bv_elim { - ast_manager& m; -public: - bv_elim(ast_manager& m) : m(m) {}; - - void elim(quantifier* q, quantifier_ref& r); -}; - -class bv_elim_star : public simplifier { -protected: - bv_elim m_bv_elim; - virtual bool visit_quantifier(quantifier* q); - virtual void reduce1_quantifier(quantifier* q); -public: - bv_elim_star(ast_manager& m) : simplifier(m), m_bv_elim(m) { enable_ac_support(false); } - virtual ~bv_elim_star() {} -}; - -#endif /* BV_ELIM_H_ */ - diff --git a/src/ast/simplifier/bv_simplifier_params.cpp b/src/ast/simplifier/bv_simplifier_params.cpp deleted file mode 100644 index 07f854179..000000000 --- a/src/ast/simplifier/bv_simplifier_params.cpp +++ /dev/null @@ -1,36 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - bv_simplifier_params.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2012-12-02. - -Revision History: - ---*/ -#include "ast/simplifier/bv_simplifier_params.h" -#include "ast/simplifier/bv_simplifier_params_helper.hpp" -#include "ast/rewriter/bv_rewriter_params.hpp" - -void bv_simplifier_params::updt_params(params_ref const & _p) { - bv_simplifier_params_helper p(_p); - bv_rewriter_params rp(_p); - m_hi_div0 = rp.hi_div0(); - m_bv2int_distribute = p.bv_bv2int_distribute(); - -} - -#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; - -void bv_simplifier_params::display(std::ostream & out) const { - DISPLAY_PARAM(m_hi_div0); - DISPLAY_PARAM(m_bv2int_distribute); -} diff --git a/src/ast/simplifier/bv_simplifier_params.h b/src/ast/simplifier/bv_simplifier_params.h deleted file mode 100644 index 8c0792203..000000000 --- a/src/ast/simplifier/bv_simplifier_params.h +++ /dev/null @@ -1,38 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - bv_simplifier_params.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-10-10. - -Revision History: - ---*/ -#ifndef BV_SIMPLIFIER_PARAMS_H_ -#define BV_SIMPLIFIER_PARAMS_H_ - -#include "util/params.h" - -struct bv_simplifier_params { - bool m_hi_div0; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted. - bool m_bv2int_distribute; //!< if true allows downward propagation of bv2int. - - bv_simplifier_params(params_ref const & p = params_ref()) { - updt_params(p); - } - - void updt_params(params_ref const & _p); - - void display(std::ostream & out) const; -}; - -#endif /* BV_SIMPLIFIER_PARAMS_H_ */ - diff --git a/src/ast/simplifier/bv_simplifier_params_helper.pyg b/src/ast/simplifier/bv_simplifier_params_helper.pyg deleted file mode 100644 index 6bcf83207..000000000 --- a/src/ast/simplifier/bv_simplifier_params_helper.pyg +++ /dev/null @@ -1,4 +0,0 @@ -def_module_params(class_name='bv_simplifier_params_helper', - module_name="old_simplify", # Parameters will be in the old_simplify module - export=True, - params=(('bv.bv2int_distribute', BOOL, True, 'if true, then int2bv is distributed over arithmetical operators'),)) diff --git a/src/ast/simplifier/bv_simplifier_plugin.cpp b/src/ast/simplifier/bv_simplifier_plugin.cpp deleted file mode 100644 index c23d2e748..000000000 --- a/src/ast/simplifier/bv_simplifier_plugin.cpp +++ /dev/null @@ -1,2261 +0,0 @@ -/*++ -Copyright (c) 2007 Microsoft Corporation - -Module Name: - - bv_simplifier_plugin.cpp - -Abstract: - - Simplifier for the bv family. - -Author: - - Leonardo (leonardo) 2008-01-08 - Nikolaj Bjorner (nbjorner) 2008-01-05 - ---*/ -#include "ast/simplifier/bv_simplifier_plugin.h" -#include "ast/ast_ll_pp.h" -#include "ast/ast_pp.h" -#include "ast/arith_decl_plugin.h" -#include "util/obj_hashtable.h" -#include "ast/ast_util.h" - -bv_simplifier_plugin::~bv_simplifier_plugin() { - flush_caches(); -} - -bv_simplifier_plugin::bv_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, bv_simplifier_params & p): - poly_simplifier_plugin(symbol("bv"), m, OP_BADD, OP_BMUL, OP_BNEG, OP_BSUB, OP_BV_NUM), - m_manager(m), - m_util(m), - m_arith(m), - m_bsimp(b), - m_params(p), - m_zeros(m) { -} - -rational bv_simplifier_plugin::norm(const numeral & n) { - unsigned bv_size = get_bv_size(m_curr_sort); - return norm(n, bv_size, false); -} - - -bool bv_simplifier_plugin::is_numeral(expr * n, rational & val) const { - unsigned bv_size; - return m_util.is_numeral(n, val, bv_size); -} - -expr * bv_simplifier_plugin::get_zero(sort * s) const { - bv_simplifier_plugin * _this = const_cast(this); - unsigned bv_size = _this->get_bv_size(s); - if (bv_size >= m_zeros.size()) - _this->m_zeros.resize(bv_size+1); - if (m_zeros.get(bv_size) == 0) - _this->m_zeros.set(bv_size, _this->m_util.mk_numeral(rational(0), s)); - return m_zeros.get(bv_size); -} - -bool bv_simplifier_plugin::are_numerals(unsigned num_args, expr * const* args, unsigned& bv_size) { - numeral r; - if (num_args == 0) { - return false; - } - for (unsigned i = 0; i < num_args; ++i) { - if (!m_util.is_numeral(args[i], r, bv_size)) { - return false; - } - } - return true; -} - -app * bv_simplifier_plugin::mk_numeral(numeral const & n) { - unsigned bv_size = get_bv_size(m_curr_sort); - return mk_numeral(n, bv_size); -} - -app * bv_simplifier_plugin::mk_numeral(numeral const& n, unsigned bv_size) { - numeral r = mod(n, rational::power_of_two(bv_size)); - SASSERT(!r.is_neg()); - SASSERT(r < rational::power_of_two(bv_size)); - return m_util.mk_numeral(r, bv_size); -} - -bool bv_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - set_reduce_invoked(); - - SASSERT(f->get_family_id() == m_fid); - - bv_op_kind k = static_cast(f->get_decl_kind()); - switch (k) { - case OP_BV_NUM: SASSERT(num_args == 0); result = mk_numeral(f->get_parameter(0).get_rational(), f->get_parameter(1).get_int()); break; - case OP_BIT0: SASSERT(num_args == 0); result = mk_numeral(0, 1); break; - case OP_BIT1: SASSERT(num_args == 0); result = mk_numeral(1, 1); break; - case OP_BADD: SASSERT(num_args > 0); - mk_add(num_args, args, result); - TRACE("bv_add_bug", - for (unsigned i = 0; i < num_args; i++) tout << mk_bounded_pp(args[i], m_manager, 10) << "\n"; - tout << mk_bounded_pp(result, m_manager, 10) << "\n";); - mk_add_concat(result); - break; - case OP_BSUB: SASSERT(num_args > 0); mk_sub(num_args, args, result); break; - case OP_BNEG: SASSERT(num_args == 1); mk_uminus(args[0], result); break; - case OP_BMUL: SASSERT(num_args > 0); mk_mul(num_args, args, result); break; - case OP_ULEQ: if (m_presimp) return false; SASSERT(num_args == 2); mk_ule(args[0], args[1], result); break; - case OP_UGEQ: if (m_presimp) return false; SASSERT(num_args == 2); mk_ule(args[1], args[0], result); break; - case OP_ULT: if (m_presimp) return false; SASSERT(num_args == 2); mk_ult(args[0], args[1], result); break; - case OP_UGT: if (m_presimp) return false; SASSERT(num_args == 2); mk_ult(args[1], args[0], result); break; - case OP_SLEQ: if (m_presimp) return false; SASSERT(num_args == 2); mk_sle(args[0], args[1], result); break; - case OP_SGEQ: if (m_presimp) return false; SASSERT(num_args == 2); mk_sle(args[1], args[0], result); break; - case OP_SLT: if (m_presimp) return false; SASSERT(num_args == 2); mk_slt(args[0], args[1], result); break; - case OP_SGT: if (m_presimp) return false; SASSERT(num_args == 2); mk_slt(args[1], args[0], result); break; - case OP_BAND: SASSERT(num_args > 0); mk_bv_and(num_args, args, result); break; - case OP_BOR: SASSERT(num_args > 0); mk_bv_or(num_args, args, result); break; - case OP_BNOT: SASSERT(num_args == 1); mk_bv_not(args[0], result); break; - case OP_BXOR: SASSERT(num_args > 0); mk_bv_xor(num_args, args, result); break; - case OP_CONCAT: SASSERT(num_args > 0); mk_concat(num_args, args, result); break; - case OP_ZERO_EXT: - SASSERT(num_args == 1); SASSERT(f->get_num_parameters() == 1); - mk_zeroext(f->get_parameter(0).get_int(), args[0], result); - break; - case OP_EXTRACT: - SASSERT(num_args == 1); SASSERT(f->get_num_parameters() == 2); - mk_extract(f->get_parameter(0).get_int(), f->get_parameter(1).get_int(), args[0], result); - break; - case OP_REPEAT: - SASSERT(num_args == 1); SASSERT(f->get_num_parameters() == 1); - mk_repeat(f->get_parameter(0).get_int(), args[0], result); - break; - case OP_BUREM: - SASSERT(num_args == 2); - mk_bv_urem(args[0], args[1], result); - break; - case OP_SIGN_EXT: - SASSERT(num_args == 1); SASSERT(f->get_num_parameters() == 1); - mk_sign_extend(f->get_parameter(0).get_int(), args[0], result); - break; - case OP_BSHL: SASSERT(num_args == 2); mk_bv_shl(args[0], args[1], result); break; - case OP_BLSHR: SASSERT(num_args == 2); mk_bv_lshr(args[0], args[1], result); break; - case OP_INT2BV: SASSERT(num_args == 1); mk_int2bv(args[0], f->get_range(), result); break; - case OP_BV2INT: SASSERT(num_args == 1); mk_bv2int(args[0], f->get_range(), result); break; - case OP_BSDIV: SASSERT(num_args == 2); mk_bv_sdiv(args[0], args[1], result); break; - case OP_BUDIV: SASSERT(num_args == 2); mk_bv_udiv(args[0], args[1], result); break; - case OP_BSREM: SASSERT(num_args == 2); mk_bv_srem(args[0], args[1], result); break; - case OP_BSMOD: SASSERT(num_args == 2); mk_bv_smod(args[0], args[1], result); break; - case OP_BNAND: SASSERT(num_args > 0); mk_bv_nand(num_args, args, result); break; - case OP_BNOR: SASSERT(num_args > 0); mk_bv_nor(num_args, args, result); break; - case OP_BXNOR: SASSERT(num_args > 0); mk_bv_xnor(num_args, args, result); break; - case OP_ROTATE_LEFT: SASSERT(num_args == 1); mk_bv_rotate_left(f, args[0], result); break; - case OP_ROTATE_RIGHT: SASSERT(num_args == 1); mk_bv_rotate_right(f, args[0], result); break; - case OP_EXT_ROTATE_LEFT: SASSERT(num_args == 2); mk_bv_ext_rotate_left(args[0], args[1], result); break; - case OP_EXT_ROTATE_RIGHT: SASSERT(num_args == 2); mk_bv_ext_rotate_right(args[0], args[1], result); break; - case OP_BREDOR: SASSERT(num_args == 1); mk_bv_redor(args[0], result); break; - case OP_BREDAND: SASSERT(num_args == 1); mk_bv_redand(args[0], result); break; - case OP_BCOMP: SASSERT(num_args == 2); mk_bv_comp(args[0], args[1], result); break; - case OP_BASHR: SASSERT(num_args == 2); mk_bv_ashr(args[0], args[1], result); break; - case OP_BSDIV_I: SASSERT(num_args == 2); mk_bv_sdiv_i(args[0], args[1], result); break; - case OP_BUDIV_I: SASSERT(num_args == 2); mk_bv_udiv_i(args[0], args[1], result); break; - case OP_BSREM_I: SASSERT(num_args == 2); mk_bv_srem_i(args[0], args[1], result); break; - case OP_BUREM_I: SASSERT(num_args == 2); mk_bv_urem_i(args[0], args[1], result); break; - case OP_BSMOD_I: SASSERT(num_args == 2); mk_bv_smod_i(args[0], args[1], result); break; - case OP_BSDIV0: - case OP_BUDIV0: - case OP_BSREM0: - case OP_BUREM0: - case OP_BSMOD0: - case OP_BIT2BOOL: - case OP_CARRY: - case OP_XOR3: - case OP_MKBV: - case OP_BUMUL_NO_OVFL: - case OP_BSMUL_NO_OVFL: - case OP_BSMUL_NO_UDFL: - result = m_manager.mk_app(f, num_args, args); - break; - default: - UNREACHABLE(); - break; - } - SASSERT(result.get()); - - TRACE("bv_simplifier", - tout << mk_pp(f, m_manager) << "\n"; - for (unsigned i = 0; i < num_args; ++i) { - tout << mk_pp(args[i], m_manager) << " "; - } - tout << "\n"; - tout << mk_pp(result.get(), m_manager) << "\n"; - ); - - return true; -} - -bool bv_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) { - set_reduce_invoked(); - - if (m_presimp) - return false; - expr_ref tmp(m_manager); - tmp = m_manager.mk_eq(lhs,rhs); - mk_bv_eq(lhs, rhs, result); - return result.get() != tmp.get(); -} - -bool bv_simplifier_plugin::reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result) { - set_reduce_invoked(); - - return false; -} - -void bv_simplifier_plugin::flush_caches() { - TRACE("extract_cache", tout << "flushing extract cache...\n";); - extract_cache::iterator it = m_extract_cache.begin(); - extract_cache::iterator end = m_extract_cache.end(); - for (; it != end; ++it) { - extract_entry & e = (*it).m_key; - m_manager.dec_ref(e.m_arg); - m_manager.dec_ref((*it).m_value); - } - m_extract_cache.reset(); -} - - -inline uint64 bv_simplifier_plugin::to_uint64(const numeral & n, unsigned bv_size) { - SASSERT(bv_size <= 64); - numeral tmp = n; - if (tmp.is_neg()) { - tmp = mod(tmp, rational::power_of_two(bv_size)); - } - SASSERT(tmp.is_nonneg()); - SASSERT(tmp.is_uint64()); - return tmp.get_uint64(); -} - -#define MK_BV_OP(_oper_,_binop_) \ -rational bv_simplifier_plugin::mk_bv_ ## _oper_(numeral const& a0, numeral const& b0, unsigned sz) { \ - rational r(0), a(a0), b(b0); \ - numeral p64 = rational::power_of_two(64); \ - numeral mul(1); \ - while (sz > 0) { \ - numeral a1 = a % p64; \ - numeral b1 = b % p64; \ - uint64 u = a1.get_uint64() _binop_ b1.get_uint64(); \ - if (sz < 64) { \ - uint64 mask = shift_left(1ull,(uint64)sz) - 1ull; \ - u = mask & u; \ - } \ - r += mul*rational(u,rational::ui64()); \ - mul *= p64; \ - a = div(a, p64); \ - b = div(b, p64); \ - sz -= (sz<64)?sz:64; \ - } \ - return r; \ -} - -MK_BV_OP(and,&) -MK_BV_OP(or,|) -MK_BV_OP(xor,^) - -rational bv_simplifier_plugin::mk_bv_not(numeral const& a0, unsigned sz) { - rational r(0), a(a0), mul(1); - numeral p64 = rational::power_of_two(64); - while (sz > 0) { - numeral a1 = a % p64; - uint64 u = ~a1.get_uint64(); - if (sz < 64) { - uint64 mask = shift_left(1ull,(uint64)sz) - 1ull; - u = mask & u; - } - r += mul*rational(u,rational::ui64()); - mul *= p64; - a = div(a, p64); - sz -= (64get_num_args() == 2) { - // - // c <=_u (concat 0 a) <=> c[u:l] = 0 && c[l-1:0] <=_u a - // - app* app = to_app(arg2); - expr * arg2_1 = app->get_arg(0); - expr * arg2_2 = app->get_arg(1); - if (m_util.is_zero(arg2_1)) { - unsigned sz1 = get_bv_size(arg2_1); - unsigned sz2 = get_bv_size(arg2_2); - - expr_ref tmp1(m_manager); - expr_ref tmp2(m_manager); - mk_extract(sz2 + sz1 - 1, sz2, arg1, tmp1); - mk_extract(sz2 - 1, 0, arg1, tmp2); - - expr_ref eq(m_manager); - expr_ref zero(m_manager); - zero = mk_bv0(sz1); - mk_bv_eq(tmp1.get(), zero, eq); - - expr_ref ineq(m_manager); - ineq = m_util.mk_ule(tmp2.get(), arg2_2); - - m_bsimp.mk_and(eq.get(), ineq.get(), result); - return; - } - } - - // - // TODO: - // Others: - // - // k <=_s (concat 0 a) <=> (k[u:l] = 0 && k[l-1:0] <=_u a) || k[u:u] = bv1 - // - // (concat 0 a) <=_s k <=> k[u:u] = bv0 && (k[u:l] != 0 || a <=_u k[l-1:0]) - // - // (concat 0 a) <=_u k <=> k[u:l] != 0 || a <=_u k[l-1:0] - // - - result = m_manager.mk_app(m_fid, k, arg1, arg2); -} - -void bv_simplifier_plugin::mk_extract(unsigned high, unsigned low, expr* arg, expr_ref& result) { - - unsigned arg_sz = get_bv_size(arg); - unsigned sz = high - low + 1; - TRACE("bv_simplifier_plugin", tout << "mk_extract [" << high << ":" << low << "]\n"; - tout << "arg_sz: " << arg_sz << " sz: " << sz << "\n"; - tout << "arg:\n"; - ast_ll_pp(tout, m_manager, arg);); - - if (arg_sz == sz) { - result = arg; - } - else { - mk_extract_core(high, low, arg, result); - } - if (m_extract_cache.size() > (1 << 12)) { - flush_caches(); - } - - TRACE("bv_simplifier_plugin", tout << "mk_extract [" << high << ":" << low << "]\n"; - tout << "arg_sz: " << arg_sz << " sz: " << sz << "\n"; - tout << "arg:\n"; - ast_ll_pp(tout, m_manager, arg); - tout << "=====================>\n"; - ast_ll_pp(tout, m_manager, result.get());); -} - - -void bv_simplifier_plugin::cache_extract(unsigned h, unsigned l, expr * arg, expr * result) { - m_manager.inc_ref(arg); - m_manager.inc_ref(result); - m_extract_cache.insert(extract_entry(h, l, arg), result); -} - -expr* bv_simplifier_plugin::get_cached_extract(unsigned h, unsigned l, expr * arg) { - expr * result = 0; - if (m_extract_cache.find(extract_entry(h, l, arg), result)) { - return result; - } - return 0; -} - - -void bv_simplifier_plugin::mk_extract_core(unsigned high, unsigned low, expr * arg, expr_ref& result) { - - if (!lookup_mk_extract(high, low, arg, result)) { - while (!m_extract_args.empty()) { - unsigned low2 = m_lows.back(); - unsigned high2 = m_highs.back(); - expr* arg2 = m_extract_args.back(); - if (try_mk_extract(high2, low2, arg2, result)) { - if (!m_extract_cache.contains(extract_entry(high2, low2, arg2))) { - cache_extract(high2, low2, arg2, result.get()); - } - m_lows.pop_back(); - m_highs.pop_back(); - m_extract_args.pop_back(); - } - } - if (!lookup_mk_extract(high, low, arg, result)) { - UNREACHABLE(); - } - } -} - - -bool bv_simplifier_plugin::lookup_mk_extract(unsigned high, unsigned low, expr * arg, expr_ref& result) { - expr* cached_result = get_cached_extract(high, low, arg); - if (cached_result) { - result = cached_result; - return true; - } - - m_extract_args.push_back(arg); - m_lows.push_back(low); - m_highs.push_back(high); - return false; -} - - -bool bv_simplifier_plugin::try_mk_extract(unsigned high, unsigned low, expr * arg, expr_ref& result) { - - SASSERT(low <= high); - unsigned arg_sz = get_bv_size(arg); - unsigned sz = high - low + 1; - numeral r; - unsigned num_bits; - - if (arg_sz == sz) { - result = arg; - return true; - } - - expr* cached_result = get_cached_extract(high, low, arg); - if (cached_result) { - result = cached_result; - return true; - } - - if (!is_app(arg)) { - result = m_util.mk_extract(high, low, arg); - return true; - } - app* a = to_app(arg); - - if (m_util.is_numeral(a, r, num_bits)) { - if (r.is_neg()) { - r = mod(r, rational::power_of_two(sz)); - } - SASSERT(r.is_nonneg()); - if (r.is_uint64()) { - uint64 u = r.get_uint64(); - uint64 e = shift_right(u, low) & (shift_left(1ull, sz) - 1ull); - TRACE("mk_extract_bug", tout << u << "[" << high << ":" << low << "] " << e << " (u >> low): " << shift_right(u, low) << " (1ull << sz): " - << shift_left(1ull, sz) << " ((1ull << sz) - 1ull)" << (shift_left(1ull, sz) - 1ull) << "\n";); - result = mk_numeral(numeral(e, numeral::ui64()), sz); - return true; - } - result = mk_numeral(div(r, rational::power_of_two(low)), sz); - return true; - } - // (extract[high:low] (extract[high2:low2] x)) == (extract[high+low2 : low+low2] x) - else if (is_app_of(a, m_fid, OP_EXTRACT)) { - expr * x = a->get_arg(0); - unsigned low2 = a->get_decl()->get_parameter(1).get_int(); - return lookup_mk_extract(high + low2, low + low2, x, result); - } - // - // (extract[hi:lo] (bvXshr A c:bv[n])) -> (extract[hi+c:lo+c] A) - // if c < n, c <= lo <= hi < n - c - // - else if ((is_app_of(a, m_fid, OP_BASHR) || is_app_of(a, m_fid, OP_BLSHR)) && - is_numeral(a->get_arg(1), r) && r.is_unsigned()) { - unsigned c = r.get_unsigned(); - unsigned bv_size = get_bv_size(a); - if (c < bv_size && c <= low && high < bv_size - c) { - return lookup_mk_extract(high+c, low+c, a->get_arg(0), result); - } - } - // (concat a_0 ... a_{n-1}) - // Remark: the least significant bits are stored in a_{n-1} - else if (is_app_of(a, m_fid, OP_CONCAT)) { - expr_ref_buffer new_args(m_manager); - unsigned i = a->get_num_args(); - // look for first argument - while (i > 0) { - --i; - expr * a_i = a->get_arg(i); - unsigned a_sz = get_bv_size(a_i); - TRACE("extract_bug", tout << "FIRST a_sz: " << a_sz << " high: " << high << " low: " << low << "\n" << - mk_pp(a_i, m_manager) << "\n";); - if (a_sz <= low) { - low -= a_sz; - high -= a_sz; - } - else { - // found first argument - if (a_sz <= high) { - expr_ref new_arg(m_manager); - if (!lookup_mk_extract(a_sz - 1, low, a_i, new_arg)) { - return false; - } - new_args.push_back(new_arg.get()); - unsigned num_consumed_bytes = a_sz - low; - // I have to apply extract[sz - num_consumed_bytes - 1, 0] on the rest of concat - high = (sz - num_consumed_bytes - 1); - break; - } - else { - return lookup_mk_extract(high, low, a_i, result); - } - } - } - TRACE("extract_bug", tout << " high: " << high << " low: " << low << "\n";); - - // look for remaining arguments - while (i > 0) { - --i; - expr * a_i = a->get_arg(i); - unsigned a_sz = get_bv_size(a_i); - TRACE("extract_bug", tout << "SECOND a_sz: " << a_sz << " high: " << high << " " << - mk_pp( a_i, m_manager) << "\n";); - if (a_sz <= high) { - high -= a_sz; - new_args.push_back(a_i); - } - else { - // found last argument - expr_ref new_arg(m_manager); - if (!lookup_mk_extract(high, 0, a_i, new_arg)) { - return false; - } - new_args.push_back(new_arg.get()); - // The arguments in new_args are in reverse order. - ptr_buffer rev_new_args; - unsigned i = new_args.size(); - while (i > 0) { - --i; - rev_new_args.push_back(new_args[i]); - } - mk_concat(rev_new_args.size(), rev_new_args.c_ptr(), result); - return true; - } - } - UNREACHABLE(); - } - else if (is_app_of(a, m_fid, OP_SIGN_EXT)) { - SASSERT(a->get_num_args() == 1); - unsigned bv_size = get_bv_size(a->get_arg(0)); - if (high < bv_size) { - return lookup_mk_extract(high, low, a->get_arg(0), result); - } - } - else if (is_app_of(a, m_fid, OP_BAND) || - is_app_of(a, m_fid, OP_BOR) || - is_app_of(a, m_fid, OP_BXOR) || - is_app_of(a, m_fid, OP_BNOR) || - is_app_of(a, m_fid, OP_BNAND) || - is_app_of(a, m_fid, OP_BNOT) || - (low == 0 && is_app_of(a, m_fid, OP_BADD)) || - (low == 0 && is_app_of(a, m_fid, OP_BMUL)) || - (low == 0 && is_app_of(a, m_fid, OP_BSUB))) { - expr_ref_buffer new_args(m_manager); - bool all_found = true; - for (unsigned i = 0; i < a->get_num_args(); ++i) { - expr_ref new_arg(m_manager); - if (!lookup_mk_extract(high, low, a->get_arg(i), new_arg)) { - all_found = false; - } - new_args.push_back(new_arg.get()); - } - if (!all_found) { - return false; - } - // We should not use mk_app because it does not guarantee that the result would be in simplified form. - // result = m_manager.mk_app(m_fid, a->get_decl_kind(), new_args.size(), new_args.c_ptr()); - if (is_app_of(a, m_fid, OP_BAND)) - mk_bv_and(new_args.size(), new_args.c_ptr(), result); - else if (is_app_of(a, m_fid, OP_BOR)) - mk_bv_or(new_args.size(), new_args.c_ptr(), result); - else if (is_app_of(a, m_fid, OP_BXOR)) - mk_bv_xor(new_args.size(), new_args.c_ptr(), result); - else if (is_app_of(a, m_fid, OP_BNOR)) - mk_bv_nor(new_args.size(), new_args.c_ptr(), result); - else if (is_app_of(a, m_fid, OP_BNAND)) - mk_bv_nand(new_args.size(), new_args.c_ptr(), result); - else if (is_app_of(a, m_fid, OP_BNOT)) { - SASSERT(new_args.size() == 1); - mk_bv_not(new_args[0], result); - } - else if (is_app_of(a, m_fid, OP_BADD)) - mk_add(new_args.size(), new_args.c_ptr(), result); - else if (is_app_of(a, m_fid, OP_BMUL)) - mk_mul(new_args.size(), new_args.c_ptr(), result); - else if (is_app_of(a, m_fid, OP_BSUB)) - mk_sub(new_args.size(), new_args.c_ptr(), result); - else { - UNREACHABLE(); - } - return true; - } - else if (m_manager.is_ite(a)) { - expr_ref then_b(m_manager), else_b(m_manager); - bool ok = lookup_mk_extract(high, low, a->get_arg(1), then_b); - ok = lookup_mk_extract(high, low, a->get_arg(2), else_b) && ok; - if (ok) { - m_bsimp.mk_ite(a->get_arg(0), then_b.get(), else_b.get(), result); - } - return ok; - } - result = m_util.mk_extract(high, low, arg); - return true; -} - -/** - \brief Let f be the operator fid:k. Then, this function - store in result the flat args of n. If n is not an f application, then store n in result. - - Example: if n is (f (f a b) (f c (f d e))), then a b c d e are stored in result. -*/ -template -void get_assoc_args(family_id fid, decl_kind k, expr * n, T & result) { - ptr_buffer todo; - todo.push_back(n); - while (!todo.empty()) { - expr * n = todo.back(); - todo.pop_back(); - if (is_app_of(n, fid, k)) { - app * app = to_app(n); - unsigned i = app->get_num_args(); - while (i > 0) { - --i; - todo.push_back(app->get_arg(i)); - } - } - else { - result.push_back(n); - } - } -} - -/** - \brief Similar to get_assoc_args, but the arguments are stored in reverse - other in result. -*/ -template -void get_inv_assoc_args(family_id fid, decl_kind k, expr * n, T & result) { - ptr_buffer todo; - todo.push_back(n); - while (!todo.empty()) { - expr * n = todo.back(); - todo.pop_back(); - if (is_app_of(n, fid, k)) { - app * app = to_app(n); - unsigned num = app->get_num_args(); - for (unsigned i = 0; i < num; i++) - todo.push_back(app->get_arg(i)); - } - else { - result.push_back(n); - } - } -} - -void bv_simplifier_plugin::mk_bv_eq(expr* a1, expr* a2, expr_ref& result) { - - rational val1; - rational val2; - bool is_num1 = is_numeral(a1, val1); - bool is_num2 = is_numeral(a2, val2); - if (is_num1 && is_num2 && val1 != val2) { - result = m_manager.mk_false(); - return; - } - - if (!m_util.is_concat(a1) && !is_num1) { - mk_eq_core(a1, a2, result); - return; - } - if (!m_util.is_concat(a2) && !is_num2) { - mk_eq_core(a1, a2, result); - return; - } - - ptr_buffer args1, args2; - get_inv_assoc_args(m_fid, OP_CONCAT, a1, args1); - get_inv_assoc_args(m_fid, OP_CONCAT, a2, args2); - TRACE("mk_bv_eq_concat", tout << mk_ll_pp(a1, m_manager) << "\n" << mk_ll_pp(a2, m_manager) << "\n"; - tout << "args1:\n"; - for (unsigned i = 0; i < args1.size(); i++) tout << mk_ll_pp(args1[i], m_manager) << "\n"; - tout << "args2:\n"; - for (unsigned i = 0; i < args2.size(); i++) tout << mk_ll_pp(args2[i], m_manager) << "\n";); - - - - expr_ref lhs(m_manager), rhs(m_manager), eq(m_manager); - expr_ref_buffer eqs(m_manager); - unsigned low1 = 0, low2 = 0; - ptr_buffer::iterator it1 = args1.begin(); - ptr_buffer::iterator end1 = args1.end(); - ptr_buffer::iterator it2 = args2.begin(); - ptr_buffer::iterator end2 = args2.end(); - - while (it1 != end1 && it2 != end2) { - SASSERT(it1 != end1); - SASSERT(it2 != end2); - expr * arg1 = *it1; - expr * arg2 = *it2; - TRACE("expr_bv_util", tout << "low1: " << low1 << " low2: " << low2 << "\n"; - tout << mk_pp(arg1, m_manager) << "\n"; - tout << mk_pp(arg2, m_manager) << "\n";); - unsigned sz1 = get_bv_size(arg1); - unsigned sz2 = get_bv_size(arg2); - SASSERT(low1 < sz1 && low2 < sz2); - unsigned rsz1 = sz1 - low1; - unsigned rsz2 = sz2 - low2; - TRACE("expr_bv_util", tout << "rsz1: " << rsz1 << " rsz2: " << rsz2 << "\n"; - tout << mk_pp(arg1, m_manager) << "\n"; - tout << mk_pp(arg2, m_manager) << "\n";); - - if (rsz1 == rsz2) { - mk_extract(sz1 - 1, low1, arg1, lhs); - mk_extract(sz2 - 1, low2, arg2, rhs); - low1 = 0; - low2 = 0; - ++it1; - ++it2; - } - else if (rsz1 < rsz2) { - mk_extract(sz1 - 1, low1, arg1, lhs); - mk_extract(rsz1 + low2 - 1, low2, arg2, rhs); - low1 = 0; - low2 += rsz1; - ++it1; - } - else { - mk_extract(rsz2 + low1 - 1, low1, arg1, lhs); - mk_extract(sz2 - 1, low2, arg2, rhs); - low1 += rsz2; - low2 = 0; - ++it2; - } - mk_eq_core(lhs.get(), rhs.get(), eq); - eqs.push_back(eq.get()); - } - m_bsimp.mk_and(eqs.size(), eqs.c_ptr(), result); -} - -void bv_simplifier_plugin::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) { - TRACE("mk_eq_core", ast_ll_pp(tout, m_manager, arg1 ); ast_ll_pp(tout, m_manager, arg2);); - if (arg1 == arg2) { - result = m_manager.mk_true(); - return; - } - if ((m_util.is_bv_and(arg1) && m_util.is_allone(arg2)) || (m_util.is_bv_or(arg1) && m_util.is_zero(arg2))) { - mk_args_eq_numeral(to_app(arg1), arg2, result); - return; - } - if ((m_util.is_bv_and(arg2) && m_util.is_allone(arg1)) || (m_util.is_bv_or(arg2) && m_util.is_zero(arg1))) { - mk_args_eq_numeral(to_app(arg2), arg1, result); - return; - } - -#if 1 - rational r; - unsigned num_bits = 0; - if (m_util.is_numeral(arg2, r, num_bits)) { - std::swap(arg1, arg2); - } - - if (m_util.is_numeral(arg1, r, num_bits) && - (m_util.is_bv_and(arg2) || m_util.is_bv_or(arg2) || m_util.is_bv_not(arg2))) { - rational two(2); - expr_ref tmp(m_manager); - expr_ref_vector tmps(m_manager); - for (unsigned i = 0; i < num_bits; ++i) { - bool is_neg = (r % two).is_zero(); - bit2bool_simplify(i, arg2, tmp); - if (is_neg) { - expr_ref tmp2(m_manager); - m_bsimp.mk_not(tmp, tmp2); - tmp = tmp2; - } - tmps.push_back(tmp); - r = div(r, two); - } - m_bsimp.mk_and(tmps.size(), tmps.c_ptr(), result); - TRACE("mk_eq_bb", - tout << mk_pp(arg1, m_manager) << "\n"; - tout << mk_pp(arg2, m_manager) << "\n"; - tout << mk_pp(result, m_manager) << "\n";); - return; - } -#endif - - if (!m_util.is_bv_add(arg1) && !m_util.is_bv_add(arg2) && - !m_util.is_bv_mul(arg1) && !m_util.is_bv_mul(arg2)) { - m_bsimp.mk_eq(arg1, arg2, result); - return; - } - - set_curr_sort(arg1); - expr_ref_vector args1(m_manager); - expr_ref_vector args2(m_manager); - get_assoc_args(m_fid, OP_BADD, arg1, args1); - get_assoc_args(m_fid, OP_BADD, arg2, args2); - TRACE("mk_eq_core", - tout << mk_pp(arg1, m_manager) << "\n" << mk_pp(arg2, m_manager) << "\n"; - tout << args1.size() << " " << args2.size() << "\n";); - - unsigned idx2 = 0; - while (idx2 < args2.size()) { - expr * m2 = args2.get(idx2); - unsigned sz1 = args1.size(); - unsigned idx1 = 0; - for (; idx1 < sz1; ++idx1) { - expr * m1 = args1.get(idx1); - if (eq_monomials_modulo_k(m1, m2)) { - expr_ref tmp(m_manager); - if (merge_monomials(true, m1, m2, tmp)) { - args1.set(idx1, tmp.get()); - } - else { - // the monomial cancelled each other. - args1.erase(idx1); - } - break; - } - } - if (idx1 == sz1) { - ++idx2; - } - else { - args2.erase(idx2); - } - } - - expr_ref lhs(m_manager); - expr_ref rhs(m_manager); - mk_sum_of_monomials(args1, lhs); - mk_sum_of_monomials(args2, rhs); - m_bsimp.mk_eq(lhs.get(), rhs.get(), result); -} - -void bv_simplifier_plugin::mk_args_eq_numeral(app * app, expr * n, expr_ref & result) { - expr_ref_buffer eqs(m_manager); - expr_ref eq(m_manager); - unsigned num = app->get_num_args(); - for (unsigned i = 0; i < num; i++) { - mk_bv_eq(app->get_arg(i), n, eq); - eqs.push_back(eq.get()); - } - m_bsimp.mk_and(eqs.size(), eqs.c_ptr(), result); -} - -void bv_simplifier_plugin::mk_concat(unsigned num_args, expr * const * args, expr_ref & result) { - TRACE("bv_simplifier_plugin", tout << "mk_concat:\n"; - for (unsigned i = 0; i < num_args; i++) ast_ll_pp(tout, m_manager, args[i]);); - unsigned shift = 0; - numeral val(0), arg_val; - for (unsigned i = num_args; i > 0; ) { - --i; - expr * arg = args[i]; - if (is_numeral(arg, arg_val)) { - arg_val *= rational::power_of_two(shift); - val += arg_val; - shift += get_bv_size(arg); - TRACE("bv_simplifier_plugin", - tout << "val: " << val << " arg_val: " << arg_val << " shift: " << shift << "\n";); - } - else { - // one of the arguments is not a number - result = m_manager.mk_app(m_fid, OP_CONCAT, num_args, args); - return; - } - } - - // all arguments are numerals - result = mk_numeral(val, shift); -} - -void bv_simplifier_plugin::mk_bv_and(unsigned num_args, expr * const* args, expr_ref & result) { - ptr_buffer flat_args; - for (unsigned i = 0; i < num_args; ++i) { - flat_args.push_back(args[i]); - } - // expr_lt_proc is a total order on expressions. - std::sort(flat_args.begin(), flat_args.end(), expr_lt_proc(m_fid, OP_BNOT)); - SASSERT(num_args > 0); - - unsigned bv_size = get_bv_size(args[0]); - - numeral allone = mk_allone(bv_size); - numeral val; - - uint64 unit = bv_size <= 64 ? to_uint64(numeral(-1), bv_size) : 0; - numeral n_unit(allone); - - expr * prev = 0; - ptr_buffer::iterator it = flat_args.begin(); - ptr_buffer::iterator it2 = it; - ptr_buffer::iterator end = flat_args.end(); - for (; it != end; ++it) { - expr* n = *it; - if (prev && - ((is_app_of(n, m_fid, OP_BNOT) && to_app(n)->get_arg(0) == prev) || - (is_app_of(prev, m_fid, OP_BNOT) && to_app(prev)->get_arg(0) == n))) { - result = mk_bv0(bv_size); - return; - } - else if (bv_size <= 64 && is_numeral(n, val)) { - unit &= to_uint64(val, bv_size); - if (unit == 0) { - result = mk_bv0(bv_size); - return; - } - } - else if (bv_size > 64 && is_numeral(n, val)) { - n_unit = mk_bv_and(val, n_unit, bv_size); - if (n_unit.is_zero()) { - result = mk_bv0(bv_size); - return; - } - } - else if (!prev || prev != n) { - *it2 = n; - prev = *it2; - ++it2; - } - } - - if (bv_size <= 64) { - n_unit = numeral(unit, numeral::ui64()); - } - - flat_args.set_end(it2); - if (n_unit != allone) { - flat_args.push_back(mk_numeral(n_unit, bv_size)); - } - - unsigned sz = flat_args.size(); - switch(sz) { - case 0: - result = mk_numeral(n_unit, bv_size); - break; - case 1: - result = flat_args.back(); - break; - default: - result = mk_list_assoc_app(m_manager, m_fid, OP_BAND, sz, flat_args.c_ptr()); - break; - } -} - -void bv_simplifier_plugin::mk_bv_or(unsigned num_args, expr * const* args, expr_ref & result) { -#if 0 - // Transformations for SAGE - // (bvor (concat 0 x) (concat y 0)) ==> (concat y x) - // (bvor (concat x 0) (concat 0 y)) ==> (concat x y) - if (num_args == 2 && - m_util.is_concat(args[0]) && - m_util.is_concat(args[1]) && - to_app(args[0])->get_num_args() == 2 && - to_app(args[1])->get_num_args() == 2) { - expr * x1 = to_app(args[0])->get_arg(0); - expr * x2 = to_app(args[0])->get_arg(1); - expr * y1 = to_app(args[1])->get_arg(0); - expr * y2 = to_app(args[1])->get_arg(1); - if (get_bv_size(x1) == get_bv_size(y1) && - get_bv_size(x2) == get_bv_size(y2)) { - if (m_util.is_zero(x1) && m_util.is_zero(y2)) { - // (bvor (concat 0 x) (concat y 0)) ==> (concat y x) - mk_concat(y1, x2, result); - return; - } - if (m_util.is_zero(x2) && m_util.is_zero(y1)) { - // (bvor (concat x 0) (concat 0 y)) ==> (concat x y) - mk_concat(x1, y2, result); - return; - } - } - } - // Investigate why it did not work. -#endif - - ptr_buffer flat_args; - for (unsigned i = 0; i < num_args; ++i) { - flat_args.push_back(args[i]); - } - std::sort(flat_args.begin(), flat_args.end(), expr_lt_proc(m_fid, OP_BNOT)); - SASSERT(num_args > 0); - - unsigned bv_size = get_bv_size(args[0]), sz; - numeral allone = mk_allone(bv_size); - numeral val; - - uint64 unit = 0; - numeral n_unit(0); - - expr * prev = 0; - ptr_buffer::iterator it = flat_args.begin(); - ptr_buffer::iterator it2 = it; - ptr_buffer::iterator end = flat_args.end(); - for (; it != end; ++it) { - expr* n = *it; - if (prev && - ((is_app_of(n, m_fid, OP_BNOT) && to_app(n)->get_arg(0) == prev) || - (is_app_of(prev, m_fid, OP_BNOT) && to_app(prev)->get_arg(0) == n))) { - result = mk_numeral(allone, bv_size); - return; - } - else if (bv_size <= 64 && is_numeral(n, val)) { - unit |= to_uint64(val, bv_size); - } - else if (bv_size > 64 && is_numeral(n, val)) { - n_unit = mk_bv_or(val, n_unit, bv_size); - } - else if (!prev || prev != n) { - *it2 = n; - prev = *it2; - ++it2; - } - } - - if (bv_size <= 64) { - n_unit = numeral(unit, numeral::ui64()); - } - - if (allone == n_unit) { - result = mk_numeral(allone, bv_size); - return; - } - - flat_args.set_end(it2); - if (!n_unit.is_zero()) { - flat_args.push_back(mk_numeral(n_unit, bv_size)); - } - - sz = flat_args.size(); - switch(sz) { - case 0: - result = mk_numeral(n_unit, bv_size); - break; - case 1: - result = flat_args.back(); - break; - default: - result = mk_list_assoc_app(m_manager, m_fid, OP_BOR, sz, flat_args.c_ptr()); - break; - } -} - -void bv_simplifier_plugin::mk_bv_xor(unsigned num_args, expr * const * args, expr_ref & result) { - ptr_buffer flat_args; - for (unsigned i = 0; i < num_args; ++i) { - flat_args.push_back(args[i]); - } - std::sort(flat_args.begin(), flat_args.end(), expr_lt_proc()); - SASSERT(num_args > 0); - - unsigned bv_size = get_bv_size(args[0]); - numeral val; - - uint64 unit = 0; - numeral n_unit(0); - - expr * prev = 0; - ptr_buffer::iterator it = flat_args.begin(); - ptr_buffer::iterator it2 = it; - ptr_buffer::iterator end = flat_args.end(); - for (; it != end; ++it) { - if (bv_size <= 64 && is_numeral(*it, val)) { - uint64 u = to_uint64(val, bv_size); - unit = u ^ unit; - } - else if (bv_size > 64 && is_numeral(*it, val)) { - n_unit = mk_bv_xor(n_unit, val, bv_size); - } - else if (prev != 0 && prev == *it) { - --it2; // remove prev - prev = 0; - } - else { - *it2 = *it; - prev = *it2; - ++it2; - } - } - flat_args.set_end(it2); - - if (bv_size <= 64) { - n_unit = numeral(numeral(unit,numeral::ui64())); - } - - if (!n_unit.is_zero()) { - flat_args.push_back(mk_numeral(n_unit, bv_size)); - } - - unsigned sz = flat_args.size(); - switch(sz) { - case 0: - result = mk_numeral(n_unit, bv_size); - break; - case 1: - result = flat_args.back(); - break; - default: - result = mk_list_assoc_app(m_manager, m_fid, OP_BXOR, flat_args.size(), flat_args.c_ptr()); - break; - } -} - -void bv_simplifier_plugin::mk_bv_not(expr * arg, expr_ref & result) { - numeral val; - unsigned bv_size; - if (m_util.is_numeral(arg, val, bv_size)) { - if (bv_size <= 64) { - uint64 l = bv_size; - uint64 mask = shift_left(1ull,l) - 1ull; - uint64 u = val.get_uint64(); - u = mask & (~u); - result = mk_numeral(numeral(u, numeral::ui64()), bv_size); - TRACE("bv_not_bug", - tout << l << " " << mask << " " << u << "\n"; - tout << mk_pp(arg, m_manager) << "\n" << mk_pp(result, m_manager) << "\n";); - } - else { - numeral r = mk_bv_not(val, bv_size); - result = mk_numeral(r, bv_size); - TRACE("bv_not_bug", - tout << mk_pp(arg, m_manager) << "\n" << mk_pp(result, m_manager) << "\n";); - } - } - else if (is_app_of(arg, m_fid, OP_BNOT)) { - result = to_app(arg)->get_arg(0); - } - else { - result = m_manager.mk_app(m_fid, OP_BNOT, arg); - } -} - -void bv_simplifier_plugin::mk_zeroext(unsigned n, expr * arg, expr_ref & result) { - if (n == 0) { - result = arg; - } - else { - expr_ref zero(m_manager); - zero = mk_bv0(n); - mk_concat(zero.get(), arg, result); - } -} - -void bv_simplifier_plugin::mk_repeat(unsigned n, expr * arg, expr_ref & result) { - ptr_buffer args; - for (unsigned i = 0; i < n; i++) { - args.push_back(arg); - } - mk_concat(args.size(), args.c_ptr(), result); -} - -bool bv_simplifier_plugin::is_minus_one_core(expr * arg) const { - numeral r; - unsigned bv_size; - if (m_util.is_numeral(arg, r, bv_size)) { - numeral minus_one(-1); - minus_one = mod(minus_one, rational::power_of_two(bv_size)); - return r == minus_one; - } - return false; -} - -bool bv_simplifier_plugin::is_x_minus_one(expr * arg, expr * & x) { - if (is_add(arg) && to_app(arg)->get_num_args() == 2) { - if (is_minus_one_core(to_app(arg)->get_arg(0))) { - x = to_app(arg)->get_arg(1); - return true; - } - if (is_minus_one_core(to_app(arg)->get_arg(1))) { - x = to_app(arg)->get_arg(0); - return true; - } - } - return false; -} - -void bv_simplifier_plugin::mk_bv_urem(expr * arg1, expr * arg2, expr_ref & result) { - numeral r1, r2; - unsigned bv_size; - bool is_num1 = m_util.is_numeral(arg1, r1, bv_size); - bool is_num2 = m_util.is_numeral(arg2, r2, bv_size); - bv_size = get_bv_size(arg1); - - if (is_num2 && r2.is_zero() && !m_params.m_hi_div0) { - result = m_manager.mk_app(m_fid, OP_BUREM0, arg1); - return; - } - - if (is_num1 && is_num2 && !r2.is_zero()) { - SASSERT(r1.is_nonneg() && r2.is_pos()); - r1 %= r2; - result = mk_numeral(r1, bv_size); - return; - } - - if (!m_params.m_hi_div0) { - // TODO: implement the optimization in this branch for the case the hardware interpretation is used for (x urem 0) - // urem(0, x) ==> ite(x = 0, urem0(x), 0) - if (is_num1 && r1.is_zero()) { - expr * zero = arg1; - expr_ref urem0(m_manager), eq0(m_manager); - urem0 = m_manager.mk_app(m_fid, OP_BUREM0, 1, &zero); - m_bsimp.mk_eq(arg2, zero, eq0); - m_bsimp.mk_ite(eq0.get(), urem0.get(), zero, result); - TRACE("urem", - tout << "urem:\n"; - ast_ll_pp(tout, m_manager, arg1); ast_ll_pp(tout, m_manager, arg2); - tout << "result:\n"; ast_ll_pp(tout, m_manager, result.get());); - return; - } - - // urem(x - 1, x) ==> ite(x = 0, urem0(x-1), x - 1) ==> ite(x = 0, urem0(-1), x - 1) - expr * x; - if (is_x_minus_one(arg1, x) && x == arg2) { - expr * x_minus_1 = arg1; - expr_ref zero(m_manager); - zero = mk_bv0(bv_size); - expr_ref minus_one(m_manager), urem0(m_manager), eq0(m_manager); - minus_one = mk_numeral(numeral::minus_one(), bv_size); - expr * minus_1 = minus_one.get(); - urem0 = m_manager.mk_app(m_fid, OP_BUREM0, 1, &minus_1); - m_bsimp.mk_eq(arg2, zero.get(), eq0); - m_bsimp.mk_ite(eq0.get(), urem0.get(), x_minus_1, result); - TRACE("urem", - tout << "urem:\n"; - ast_ll_pp(tout, m_manager, arg1); ast_ll_pp(tout, m_manager, arg2); - tout << "result:\n"; ast_ll_pp(tout, m_manager, result.get());); - return; - } - } - - if (is_num2 || m_params.m_hi_div0) { - result = m_manager.mk_app(m_fid, OP_BUREM_I, arg1, arg2); - } - else { - bv_size = get_bv_size(arg2); - result = m_manager.mk_ite(m_manager.mk_eq(arg2, mk_numeral(0, bv_size)), - m_manager.mk_app(m_fid, OP_BUREM0, arg1), - m_manager.mk_app(m_fid, OP_BUREM_I, arg1, arg2)); - } -} - -void bv_simplifier_plugin::mk_sign_extend(unsigned n, expr * arg, expr_ref & result) { - numeral r; - unsigned bv_size; - if (m_util.is_numeral(arg, r, bv_size)) { - unsigned result_bv_size = bv_size + n; - r = norm(r, bv_size, true); - r = mod(r, rational::power_of_two(result_bv_size)); - result = mk_numeral(r, result_bv_size); - TRACE("mk_sign_extend", tout << "n: " << n << "\n"; - ast_ll_pp(tout, m_manager, arg); tout << "====>\n"; - ast_ll_pp(tout, m_manager, result.get());); - return; - } - parameter param(n); - result = m_manager.mk_app(m_fid, OP_SIGN_EXT, 1, ¶m, 1, &arg); -} - -/** - Implement the following reductions - - (bvashr (bvashr a n1) n2) ==> (bvashr a (+ n1 n2)) - (bvlshr (bvlshr a n1) n2) ==> (bvlshr a (+ n1 n2)) - (bvshl (bvshl a n1) n2) ==> (bvshl a (+ n1 n2)) - when n1 and n2 are numerals. - Remark if (+ n1 n2) is greater than bv_size, we set (+ n1 n2) to bv_size - - Return true if the transformation was applied and the result stored in 'result'. - Return false otherwise. -*/ -bool bv_simplifier_plugin::shift_shift(bv_op_kind k, expr* arg1, expr* arg2, expr_ref& result) { - SASSERT(k == OP_BASHR || k == OP_BSHL || k == OP_BLSHR); - if (!is_app_of(arg1, m_fid, k)) - return false; - expr * a = to_app(arg1)->get_arg(0); - expr * n1 = to_app(arg1)->get_arg(1); - expr * n2 = arg2; - numeral r1, r2; - unsigned bv_size = UINT_MAX; - bool is_num1 = m_util.is_numeral(n1, r1, bv_size); - bool is_num2 = m_util.is_numeral(n2, r2, bv_size); - if (!is_num1 || !is_num2) - return false; - SASSERT(bv_size != UINT_MAX); - numeral r = r1 + r2; - if (r > numeral(bv_size)) - r = numeral(bv_size); - switch (k) { - case OP_BASHR: - mk_bv_ashr(a, m_util.mk_numeral(r, bv_size), result); - break; - case OP_BLSHR: - mk_bv_lshr(a, m_util.mk_numeral(r, bv_size), result); - break; - default: - SASSERT(k == OP_BSHL); - mk_bv_shl(a, m_util.mk_numeral(r, bv_size), result); - break; - } - return true; -} - -void bv_simplifier_plugin::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) { - // x << 0 == x - numeral r1, r2; - unsigned bv_size = get_bv_size(arg1); - bool is_num1 = is_numeral(arg1, r1); - bool is_num2 = is_numeral(arg2, r2); - - if (is_num2 && r2.is_zero()) { - result = arg1; - } - else if (is_num2 && r2 >= rational(bv_size)) { - result = mk_numeral(0, bv_size); - } - else if (is_num2 && is_num1 && bv_size <= 64) { - SASSERT(r1.is_uint64() && r2.is_uint64()); - SASSERT(r2.get_uint64() < bv_size); - - uint64 r = shift_left(r1.get_uint64(), r2.get_uint64()); - result = mk_numeral(r, bv_size); - } - else if (is_num1 && is_num2) { - SASSERT(r2 < rational(bv_size)); - SASSERT(r2.is_unsigned()); - result = mk_numeral(r1 * rational::power_of_two(r2.get_unsigned()), bv_size); - } - - // - // (bvshl x k) -> (concat (extract [n-1-k:0] x) bv0:k) - // - else if (is_num2 && r2.is_pos() && r2 < numeral(bv_size)) { - SASSERT(r2.is_unsigned()); - unsigned r = r2.get_unsigned(); - expr_ref tmp1(m_manager); - mk_extract(bv_size - r - 1, 0, arg1, tmp1); - expr_ref zero(m_manager); - zero = mk_bv0(r); - expr* args[2] = { tmp1.get(), zero.get() }; - mk_concat(2, args, result); - } - else if (shift_shift(OP_BSHL, arg1, arg2, result)) { - // done - } - else { - result = m_manager.mk_app(m_fid, OP_BSHL, arg1, arg2); - } - TRACE("mk_bv_shl", - tout << mk_pp(arg1, m_manager) << " << " - << mk_pp(arg2, m_manager) << " = " - << mk_pp(result.get(), m_manager) << "\n";); -} - -void bv_simplifier_plugin::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) { - // x >> 0 == x - numeral r1, r2; - unsigned bv_size = get_bv_size(arg1); - bool is_num1 = is_numeral(arg1, r1); - bool is_num2 = is_numeral(arg2, r2); - - if (is_num2 && r2.is_zero()) { - result = arg1; - } - else if (is_num2 && r2 >= rational(bv_size)) { - result = mk_numeral(rational(0), bv_size); - } - else if (is_num1 && is_num2 && bv_size <= 64) { - SASSERT(r1.is_uint64()); - SASSERT(r2.is_uint64()); - uint64 r = shift_right(r1.get_uint64(), r2.get_uint64()); - result = mk_numeral(r, bv_size); - } - else if (is_num1 && is_num2) { - SASSERT(r2.is_unsigned()); - unsigned sh = r2.get_unsigned(); - r1 = div(r1, rational::power_of_two(sh)); - result = mk_numeral(r1, bv_size); - } - // - // (bvlshr x k) -> (concat bv0:k (extract [n-1:k] x)) - // - else if (is_num2 && r2.is_pos() && r2 < numeral(bv_size)) { - SASSERT(r2.is_unsigned()); - unsigned r = r2.get_unsigned(); - expr_ref tmp1(m_manager); - mk_extract(bv_size - 1, r, arg1, tmp1); - expr_ref zero(m_manager); - zero = mk_bv0(r); - expr* args[2] = { zero.get(), tmp1.get() }; - mk_concat(2, args, result); - } - else if (shift_shift(OP_BLSHR, arg1, arg2, result)) { - // done - } - else { - result = m_manager.mk_app(m_fid, OP_BLSHR, arg1, arg2); - } - TRACE("mk_bv_lshr", tout << mk_pp(arg1, m_manager) << " >> " << - mk_pp(arg2, m_manager) << " = " << mk_pp(result.get(), m_manager) << "\n";); - -} - - -void bv_simplifier_plugin::mk_int2bv(expr * arg, sort* range, expr_ref & result) { - numeral val; - bool is_int; - unsigned bv_size = get_bv_size(range); - - if (m_arith.is_numeral(arg, val, is_int)) { - result = mk_numeral(val, bv_size); - } - // (int2bv (bv2int x)) == x - else if (is_app_of(arg, m_fid, OP_BV2INT) && bv_size == get_bv_size(to_app(arg)->get_arg(0))) { - result = to_app(arg)->get_arg(0); - } - else { - parameter parameter(bv_size); - result = m_manager.mk_app(m_fid, OP_INT2BV, 1, ¶meter, 1, &arg); - SASSERT(result.get()); - } -} - -void bv_simplifier_plugin::mk_bv2int(expr * arg, sort* range, expr_ref & result) { - if (!m_params.m_bv2int_distribute) { - parameter parameter(range); - result = m_manager.mk_app(m_fid, OP_BV2INT, 1, ¶meter, 1, &arg); - return; - } - numeral v; - if (is_numeral(arg, v)) { - result = m_arith.mk_numeral(v, true); - } - else if (is_mul_no_overflow(arg)) { - expr_ref tmp1(m_manager), tmp2(m_manager); - mk_bv2int(to_app(arg)->get_arg(0), range, tmp1); - mk_bv2int(to_app(arg)->get_arg(1), range, tmp2); - result = m_arith.mk_mul(tmp1, tmp2); - } - else if (is_add_no_overflow(arg)) { - expr_ref tmp1(m_manager), tmp2(m_manager); - mk_bv2int(to_app(arg)->get_arg(0), range, tmp1); - mk_bv2int(to_app(arg)->get_arg(1), range, tmp2); - result = m_arith.mk_add(tmp1, tmp2); - } - // commented out to reproduce bug in reduction of int2bv/bv2int - else if (m_util.is_concat(arg) && to_app(arg)->get_num_args() > 0) { - expr_ref_vector args(m_manager); - unsigned num_args = to_app(arg)->get_num_args(); - for (unsigned i = 0; i < num_args; ++i) { - expr_ref tmp(m_manager); - mk_bv2int(to_app(arg)->get_arg(i), range, tmp); - args.push_back(tmp); - } - unsigned sz = get_bv_size(to_app(arg)->get_arg(num_args-1)); - for (unsigned i = num_args - 1; i > 0; ) { - expr_ref tmp(m_manager); - --i; - tmp = args[i].get(); - tmp = m_arith.mk_mul(m_arith.mk_numeral(power(numeral(2), sz), true), tmp); - args[i] = tmp; - sz += get_bv_size(to_app(arg)->get_arg(i)); - } - result = m_arith.mk_add(args.size(), args.c_ptr()); - } - else { - parameter parameter(range); - result = m_manager.mk_app(m_fid, OP_BV2INT, 1, ¶meter, 1, &arg); - } - SASSERT(m_arith.is_int(m_manager.get_sort(result.get()))); -} - -unsigned bv_simplifier_plugin::num_leading_zero_bits(expr* e) { - numeral v; - unsigned sz = get_bv_size(e); - if (is_numeral(e, v)) { - while (v.is_pos()) { - SASSERT(sz > 0); - --sz; - v = div(v, numeral(2)); - } - return sz; - } - else if (m_util.is_concat(e)) { - app* a = to_app(e); - unsigned sz1 = get_bv_size(a->get_arg(0)); - unsigned nb1 = num_leading_zero_bits(a->get_arg(0)); - if (sz1 == nb1) { - nb1 += num_leading_zero_bits(a->get_arg(1)); - } - return nb1; - } - return 0; -} - -bool bv_simplifier_plugin::is_mul_no_overflow(expr* e) { - if (!is_mul(e)) { - return false; - } - expr* e1 = to_app(e)->get_arg(0); - expr* e2 = to_app(e)->get_arg(1); - unsigned sz = get_bv_size(e1); - unsigned nb1 = num_leading_zero_bits(e1); - unsigned nb2 = num_leading_zero_bits(e2); - return nb1 + nb2 >= sz; -} - -bool bv_simplifier_plugin::is_add_no_overflow(expr* e) { - if (!is_add(e)) { - return false; - } - expr* e1 = to_app(e)->get_arg(0); - expr* e2 = to_app(e)->get_arg(1); - unsigned nb1 = num_leading_zero_bits(e1); - unsigned nb2 = num_leading_zero_bits(e2); - return nb1 > 0 && nb2 > 0; -} - - - -// Macro for generating mk_bv_sdiv_i, mk_bv_udiv_i, mk_bv_srem_i, mk_bv_urem_i and mk_bv_smod_i. -// These are essentially evaluators for the arg1 and arg2 are numerals. -// Q: Why do we need them? -// A: A constant may be eliminated using substitution. Its value is computed using the evaluator. -// Example: Suppose we have the top-level atom (= x (bvsrem_i a b)), and x is eliminated. -#define MK_FIXED_DIV_I(NAME, OP) \ -void bv_simplifier_plugin::NAME##_i(expr * arg1, expr * arg2, expr_ref & result) { \ - numeral r1, r2; \ - unsigned bv_size; \ - bool is_num1 = m_util.is_numeral(arg1, r1, bv_size); \ - bool is_num2 = m_util.is_numeral(arg2, r2, bv_size); \ - if (is_num1 && is_num2 && !r2.is_zero()) { \ - NAME(arg1, arg2, result); \ - } \ - else { \ - result = m_manager.mk_app(m_fid, OP, arg1, arg2); \ - } \ -} - -MK_FIXED_DIV_I(mk_bv_sdiv, OP_BSDIV_I) -MK_FIXED_DIV_I(mk_bv_udiv, OP_BUDIV_I) -MK_FIXED_DIV_I(mk_bv_srem, OP_BSREM_I) -MK_FIXED_DIV_I(mk_bv_urem, OP_BUREM_I) -MK_FIXED_DIV_I(mk_bv_smod, OP_BSMOD_I) - -void bv_simplifier_plugin::mk_bv_sdiv(expr* arg1, expr* arg2, expr_ref& result) { - numeral r1, r2; - unsigned bv_size; - bool is_num1 = m_util.is_numeral(arg1, r1, bv_size); - bool is_num2 = m_util.is_numeral(arg2, r2, bv_size); - - if (is_num2 && r2.is_zero() && !m_params.m_hi_div0) { - result = m_manager.mk_app(m_fid, OP_BSDIV0, arg1); - } - else if (is_num1 && is_num2 && !r2.is_zero()) { - r1 = norm(r1, bv_size, true); - r2 = norm(r2, bv_size, true); - result = mk_numeral(machine_div(r1, r2), bv_size); - } - else if (is_num2 || m_params.m_hi_div0) { - result = m_manager.mk_app(m_fid, OP_BSDIV_I, arg1, arg2); - } - else { - bv_size = get_bv_size(arg2); - result = m_manager.mk_ite(m_manager.mk_eq(arg2, mk_numeral(0, bv_size)), - m_manager.mk_app(m_fid, OP_BSDIV0, arg1), - m_manager.mk_app(m_fid, OP_BSDIV_I, arg1, arg2)); - } -} - -void bv_simplifier_plugin::mk_bv_udiv(expr* arg1, expr* arg2, expr_ref& result) { - numeral r1, r2; - unsigned bv_size; - bool is_num1 = m_util.is_numeral(arg1, r1, bv_size); - bool is_num2 = m_util.is_numeral(arg2, r2, bv_size); - - if (is_num2 && r2.is_zero() && !m_params.m_hi_div0) { - result = m_manager.mk_app(m_fid, OP_BUDIV0, arg1); - } - else if (is_num1 && is_num2 && !r2.is_zero()) { - SASSERT(r1.is_nonneg()); - SASSERT(r2.is_nonneg()); - result = mk_numeral(machine_div(r1, r2), bv_size); - } - else if (is_num2 || m_params.m_hi_div0) { - result = m_manager.mk_app(m_fid, OP_BUDIV_I, arg1, arg2); - } - else { - bv_size = get_bv_size(arg2); - result = m_manager.mk_ite(m_manager.mk_eq(arg2, mk_numeral(0, bv_size)), - m_manager.mk_app(m_fid, OP_BUDIV0, arg1), - m_manager.mk_app(m_fid, OP_BUDIV_I, arg1, arg2)); - } -} - -void bv_simplifier_plugin::mk_bv_srem(expr* arg1, expr* arg2, expr_ref& result) { - numeral r1, r2; - unsigned bv_size; - bool is_num1 = m_util.is_numeral(arg1, r1, bv_size); - bool is_num2 = m_util.is_numeral(arg2, r2, bv_size); - - if (is_num2 && r2.is_zero() && !m_params.m_hi_div0) { - result = m_manager.mk_app(m_fid, OP_BSREM0, arg1); - } - else if (is_num1 && is_num2 && !r2.is_zero()) { - r1 = norm(r1, bv_size, true); - r2 = norm(r2, bv_size, true); - result = mk_numeral(r1 % r2, bv_size); - } - else if (is_num2 || m_params.m_hi_div0) { - result = m_manager.mk_app(m_fid, OP_BSREM_I, arg1, arg2); - } - else { - bv_size = get_bv_size(arg2); - result = m_manager.mk_ite(m_manager.mk_eq(arg2, mk_numeral(0, bv_size)), - m_manager.mk_app(m_fid, OP_BSREM0, arg1), - m_manager.mk_app(m_fid, OP_BSREM_I, arg1, arg2)); - } -} - -void bv_simplifier_plugin::mk_bv_smod(expr* arg1, expr* arg2, expr_ref& result) { - numeral r1, r2; - unsigned bv_size; - bool is_num1 = m_util.is_numeral(arg1, r1, bv_size); - bool is_num2 = m_util.is_numeral(arg2, r2, bv_size); - - if (is_num1) - r1 = m_util.norm(r1, bv_size, true); - if (is_num2) - r2 = m_util.norm(r2, bv_size, true); - - TRACE("bv_simplifier", - tout << mk_pp(arg1, m_manager) << " smod " << mk_pp(arg2, m_manager) << "\n"; - ); - - - if (is_num2 && r2.is_zero()) { - if (!m_params.m_hi_div0) - result = m_manager.mk_app(m_fid, OP_BSMOD0, arg1); - else - result = arg1; - } - else if (is_num1 && is_num2) { - SASSERT(!r2.is_zero()); - numeral abs_r1 = m_util.norm(abs(r1), bv_size); - numeral abs_r2 = m_util.norm(abs(r2), bv_size); - numeral u = m_util.norm(abs_r1 % abs_r2, bv_size); - numeral r; - if (u.is_zero()) - r = u; - else if (r1.is_pos() && r2.is_pos()) - r = u; - else if (r1.is_neg() && r2.is_pos()) - r = m_util.norm(-u + r2, bv_size); - else if (r1.is_pos() && r2.is_neg()) - r = m_util.norm(u + r2, bv_size); - else - r = m_util.norm(-u, bv_size); - result = mk_numeral(r, bv_size); - } - else if (is_num2 || m_params.m_hi_div0) { - result = m_manager.mk_app(m_fid, OP_BSMOD_I, arg1, arg2); - } - else { - bv_size = get_bv_size(arg2); - result = m_manager.mk_ite(m_manager.mk_eq(arg2, mk_numeral(0, bv_size)), - m_manager.mk_app(m_fid, OP_BSMOD0, arg1), - m_manager.mk_app(m_fid, OP_BSMOD_I, arg1, arg2)); - } -} - -uint64 bv_simplifier_plugin::n64(expr* e) { - numeral r; - unsigned bv_size; - if (m_util.is_numeral(e, r, bv_size) && bv_size <= 64) { - return r.get_uint64(); - } - UNREACHABLE(); - return 0; -} - -rational bv_simplifier_plugin::num(expr* e) { - numeral r; - unsigned bv_size; - if (!m_util.is_numeral(e, r, bv_size)) { - UNREACHABLE(); - } - return r; - -} - -void bv_simplifier_plugin::mk_bv_nand(unsigned num_args, expr* const* args, expr_ref& result) { - unsigned bv_size; - if (are_numerals(num_args, args, bv_size)) { - if (bv_size <= 64) { - uint64 r = n64(args[0]); - for (unsigned i = 1; i < num_args; i++) { - r &= n64(args[i]); - } - result = mk_numeral(~r, bv_size); - } - else { - numeral r = num(args[0]); - for (unsigned i = 1; i < num_args; i++) { - r = mk_bv_and(r, num(args[i]), bv_size); - } - result = mk_numeral(mk_bv_not(r, bv_size), bv_size); - } - } - else { - result = m_manager.mk_app(m_fid, OP_BNAND, num_args, args); - } -} - -void bv_simplifier_plugin::mk_bv_nor(unsigned num_args, expr* const* args, expr_ref& result) { - unsigned bv_size; - if (are_numerals(num_args, args, bv_size)) { - if (bv_size <= 64) { - uint64 r = n64(args[0]); - for (unsigned i = 1; i < num_args; i++) { - r |= n64(args[i]); - } - result = mk_numeral(~r, bv_size); - } - else { - numeral r = num(args[0]); - for (unsigned i = 1; i < num_args; i++) { - r = mk_bv_or(r, num(args[i]), bv_size); - } - result = mk_numeral(mk_bv_not(r, bv_size), bv_size); - } - } - else { - result = m_manager.mk_app(m_fid, OP_BNOR, num_args, args); - } -} - -void bv_simplifier_plugin::mk_bv_xnor(unsigned num_args, expr* const* args, expr_ref& result) { - unsigned bv_size; - if (are_numerals(num_args, args, bv_size)) { - if (bv_size <= 64) { - uint64 r = n64(args[0]); - for (unsigned i = 1; i < num_args; i++) { - r ^= n64(args[i]); - } - result = mk_numeral(~r, bv_size); - } - else { - numeral r = num(args[0]); - for (unsigned i = 1; i < num_args; i++) { - r = mk_bv_xor(r, num(args[i]), bv_size); - } - result = mk_numeral(mk_bv_not(r, bv_size), bv_size); - } - } - else { - result = m_manager.mk_app(m_fid, OP_BXNOR, num_args, args); - } -} - -void bv_simplifier_plugin::mk_bv_rotate_left_core(unsigned shift, numeral r, unsigned bv_size, expr_ref& result) { - SASSERT(shift < bv_size); - if (bv_size <= 64) { - uint64 a = r.get_uint64(); - uint64 r = shift_left(a, shift) | shift_right(a, bv_size - shift); - result = mk_numeral(r, bv_size); - } - else { - rational r1 = div(r, rational::power_of_two(bv_size - shift)); // shift right - rational r2 = (r * rational::power_of_two(shift)) % rational::power_of_two(bv_size); // shift left - result = mk_numeral(r1 + r2, bv_size); - } -} - -void bv_simplifier_plugin::mk_bv_rotate_left(func_decl* f, expr* arg, expr_ref& result) { - numeral r; - unsigned bv_size; - SASSERT(f->get_decl_kind() == OP_ROTATE_LEFT); - if (m_util.is_numeral(arg, r, bv_size)) { - unsigned shift = f->get_parameter(0).get_int() % bv_size; - mk_bv_rotate_left_core(shift, r, bv_size, result); - } - else { - result = m_manager.mk_app(f, arg); - } -} - -void bv_simplifier_plugin::mk_bv_rotate_right_core(unsigned shift, numeral r, unsigned bv_size, expr_ref& result) { - SASSERT(shift < bv_size); - if (bv_size <= 64) { - uint64 a = r.get_uint64(); - uint64 r = shift_right(a, shift) | shift_left(a, bv_size - shift); - result = mk_numeral(r, bv_size); - } - else { - rational r1 = div(r, rational::power_of_two(shift)); // shift right - rational r2 = (r * rational::power_of_two(bv_size - shift)) % rational::power_of_two(bv_size); // shift left - result = mk_numeral(r1 + r2, bv_size); - } -} - -void bv_simplifier_plugin::mk_bv_rotate_right(func_decl* f, expr* arg, expr_ref& result) { - numeral r; - unsigned bv_size; - SASSERT(f->get_decl_kind() == OP_ROTATE_RIGHT); - if (m_util.is_numeral(arg, r, bv_size)) { - unsigned shift = f->get_parameter(0).get_int() % bv_size; - mk_bv_rotate_right_core(shift, r, bv_size, result); - } - else { - result = m_manager.mk_app(f, arg); - } -} - -void bv_simplifier_plugin::mk_bv_redor(expr* arg, expr_ref& result) { - if (is_numeral(arg)) { - result = m_util.is_zero(arg)?mk_numeral(0, 1):mk_numeral(1,1); - } - else { - result = m_manager.mk_app(m_fid, OP_BREDOR, arg); - } -} - -void bv_simplifier_plugin::mk_bv_redand(expr* arg, expr_ref& result) { - numeral r; - unsigned bv_size; - if (m_util.is_numeral(arg, r, bv_size)) { - numeral allone = mk_allone(bv_size); - result = mk_numeral((r == allone)?1:0, 1); - } - else { - result = m_manager.mk_app(m_fid, OP_BREDAND, arg); - } -} - -void bv_simplifier_plugin::mk_bv_comp(expr* arg1, expr* arg2, expr_ref& result) { - numeral r1, r2; - if (arg1 == arg2) { - result = mk_numeral(1,1); - } - else if (is_numeral(arg1, r1) && is_numeral(arg2, r2)) { - result = mk_numeral((r1 == r2)?1:0, 1); - } - else { - result = m_manager.mk_app(m_fid, OP_BCOMP, arg1, arg2); - } -} - -void bv_simplifier_plugin::mk_bv_ashr(expr* arg1, expr* arg2, expr_ref& result) { - numeral r1, r2; - unsigned bv_size = get_bv_size(arg1); - bool is_num1 = m_util.is_numeral(arg1, r1, bv_size); - bool is_num2 = m_util.is_numeral(arg2, r2, bv_size); - - if (bv_size == 0) { - result = mk_numeral(rational(0), bv_size); - } - else if (is_num2 && r2.is_zero()) { - result = arg1; - } - else if (bv_size <= 64 && is_num1 && is_num2) { - uint64 n1 = n64(arg1); - uint64 n2_orig = n64(arg2); - uint64 n2 = n2_orig % bv_size; - SASSERT(n2 < bv_size); - uint64 r = shift_right(n1, n2); - bool sign = (n1 & shift_left(1ull, bv_size - 1ull)) != 0; - if (n2_orig > n2) { - if (sign) { - r = shift_left(1ull, bv_size) - 1ull; - } - else { - r = 0; - } - } - else if (sign) { - uint64 allone = shift_left(1ull, bv_size) - 1ull; - uint64 mask = ~(shift_left(1ull, bv_size - n2) - 1ull); - mask &= allone; - r |= mask; - } - result = mk_numeral(r, bv_size); - TRACE("bv", tout << mk_pp(arg1, m_manager) << " >> " - << mk_pp(arg2, m_manager) << " = " - << mk_pp(result.get(), m_manager) << "\n"; - tout << n1 << " >> " << n2 << " = " << r << "\n"; - ); - } - else if (is_num1 && is_num2 && rational(bv_size) <= r2) { - if (has_sign_bit(r1, bv_size)) { - result = mk_numeral(mk_allone(bv_size), bv_size); - } - else { - result = mk_bv0(bv_size); - } - } - else if (is_num1 && is_num2) { - SASSERT(r2 < rational(bv_size)); - bool sign = has_sign_bit(r1, bv_size); - r1 = div(r1, rational::power_of_two(r2.get_unsigned())); - if (sign) { - // pad ones. - rational p(1); - for (unsigned i = 0; i < bv_size; ++i) { - if (r1 < p) { - r1 += p; - } - p *= rational(2); - } - } - result = mk_numeral(r1, bv_size); - - } - else if (shift_shift(OP_BASHR, arg1, arg2, result)) { - // done - } - else { - result = m_manager.mk_app(m_fid, OP_BASHR, arg1, arg2); - } -} - -void bv_simplifier_plugin::mk_bv_ext_rotate_right(expr* arg1, expr* arg2, expr_ref& result) { - numeral r2; - unsigned bv_size; - if (m_util.is_numeral(arg2, r2, bv_size)) { - unsigned shift = static_cast((r2 % numeral(bv_size)).get_uint64() % static_cast(bv_size)); - numeral r1; - if (is_numeral(arg1, r1)) { - mk_bv_rotate_right_core(shift, r1, bv_size, result); - } - else { - parameter p(shift); - result = m_manager.mk_app(m_fid, OP_ROTATE_RIGHT, 1, &p, 1, &arg1); - } - } - else { - result = m_manager.mk_app(m_fid, OP_EXT_ROTATE_RIGHT, arg1, arg2); - } -} - - -void bv_simplifier_plugin::mk_bv_ext_rotate_left(expr* arg1, expr* arg2, expr_ref& result) { - numeral r2; - unsigned bv_size; - if (m_util.is_numeral(arg2, r2, bv_size)) { - unsigned shift = static_cast((r2 % numeral(bv_size)).get_uint64() % static_cast(bv_size)); - numeral r1; - if (is_numeral(arg1, r1)) { - mk_bv_rotate_left_core(shift, r1, bv_size, result); - } - else { - parameter p(shift); - result = m_manager.mk_app(m_fid, OP_ROTATE_LEFT, 1, &p, 1, &arg1); - } - } - else { - result = m_manager.mk_app(m_fid, OP_EXT_ROTATE_LEFT, arg1, arg2); - } -} - -void bv_simplifier_plugin::bit2bool_simplify(unsigned idx, expr* e, expr_ref& result) { - - parameter p(idx); - - ptr_vector todo; - expr_ref_vector pinned(m_manager); - ptr_vector cache; - todo.push_back(e); - expr* e0 = e; - ptr_vector argv; - expr_ref tmp(m_manager); - while (!todo.empty()) { - e = todo.back(); - unsigned e_id = e->get_id(); - if (e_id >= cache.size()) { - cache.resize(e_id+1,0); - } - if (cache[e_id]) { - todo.pop_back(); - continue; - } - if (!m_util.is_numeral(e) && - !m_util.is_bv_and(e) && - !m_util.is_bv_or(e) && - !(is_app_of(e, m_fid, OP_BXOR) && to_app(e)->get_num_args() == 2) && - !m_manager.is_ite(e) && - !m_util.is_concat(e) && - !m_util.is_bv_not(e)) { - expr_ref extr(m_manager); - extr = m_util.mk_extract(idx, idx, e); - cache[e_id] = m_manager.mk_eq(m_util.mk_numeral(1, 1), extr); - pinned.push_back(cache[e_id]); - todo.pop_back(); - continue; - } - app* a = to_app(e); - unsigned sz = a->get_num_args(); - if (m_util.is_concat(e)) { - // look for first argument - unsigned idx1 = idx; - while (sz > 0) { - --sz; - expr * a_i = a->get_arg(sz); - unsigned a_sz = get_bv_size(a_i); - if (a_sz <= idx1) { - idx1 -= a_sz; - } - else { - // idx < a_sz; - bit2bool_simplify(idx1, a_i, tmp); - pinned.push_back(tmp); - cache[e_id] = to_app(tmp); - break; - } - } - todo.pop_back(); - continue; - } - argv.reset(); - for (unsigned i = 0; i < sz; ++i) { - expr* arg_i = a->get_arg(i); - if (i == 0 && m_manager.is_ite(e)) { - argv.push_back(arg_i); - } - else if (cache.size() > arg_i->get_id() && cache[arg_i->get_id()]) { - argv.push_back(cache[arg_i->get_id()]); - } - else { - todo.push_back(arg_i); - } - } - if (sz != argv.size()) { - continue; - } - todo.pop_back(); - rational val; - unsigned num_bits; - if (m_util.is_numeral(e, val, num_bits)) { - rational two(2); - for (unsigned i = 0; i < idx; ++i) { - val = div(val, two); - } - bool is_pos = !(val % two).is_zero(); - tmp = is_pos?m_manager.mk_true():m_manager.mk_false(); - } - else if (m_util.is_bv_and(e)) { - //tmp = m_manager.mk_and(sz, argv.c_ptr()); - m_bsimp.mk_and(sz, argv.c_ptr(), tmp); - pinned.push_back(tmp); - } - else if (m_util.is_bv_or(e)) { - //tmp = m_manager.mk_or(sz, argv.c_ptr()); - m_bsimp.mk_or(sz, argv.c_ptr(), tmp); - pinned.push_back(tmp); - } - else if (m_util.is_bv_not(e)) { - //tmp = m_manager.mk_not(argv[0]); - m_bsimp.mk_not(argv[0], tmp); - pinned.push_back(tmp); - } - else if (is_app_of(e, m_fid, OP_BXOR)) { - SASSERT(argv.size() == 2); - m_bsimp.mk_xor(argv[0], argv[1], tmp); - pinned.push_back(tmp); - } - else if (m_manager.is_ite(e)) { - //tmp = m_manager.mk_ite(argv[0], argv[1], argv[2]); - m_bsimp.mk_ite(argv[0], argv[1], argv[2], tmp); - pinned.push_back(tmp); - } - else { - UNREACHABLE(); - } - cache[e_id] = to_app(tmp); - } - result = cache[e0->get_id()]; -} - - -// replace addition by concatenation. -void bv_simplifier_plugin::mk_add_concat(expr_ref& result) { - if (!m_util.is_bv_add(result)) { - return; - } - app* a = to_app(result); - if (a->get_num_args() != 2) { - return; - } - expr* x = a->get_arg(0); - expr* y = a->get_arg(1); - if (!m_util.is_concat(x)) { - std::swap(x, y); - } - if (!m_util.is_concat(x)) { - return; - } - unsigned sz = m_util.get_bv_size(x); - -#if 0 - // optimzied version. Seems not worth it.. -#define UPDATE_CURR(_curr1, _idx1,_x,_is_num, _i) \ - if (_idx1 >= m_util.get_bv_size(_curr1)) { \ - _curr1 = _x; \ - _idx1 = _i; \ - _is_num = false; \ - } \ - while (m_util.is_concat(_curr1)) { \ - _is_num = false; \ - unsigned num_args = to_app(_curr1)->get_num_args(); \ - while (true) { \ - --num_args; \ - expr* c1 = to_app(_curr1)->get_arg(num_args); \ - unsigned sz1 = m_util.get_bv_size(c1); \ - if (sz1 < _idx1) { \ - _idx1 -= sz1; \ - } \ - else { \ - _curr1 = c1; \ - break; \ - } \ - } \ - } - - unsigned idx1 = 0, idx2 = 0; - expr* curr1 = x, *curr2 = y; - bool is_num1 = false, is_num2 = false; - rational val1, val2; - rational two(2); - for (unsigned i = 0; i < sz; ++i, ++idx1, ++idx2) { - UPDATE_CURR(curr1, idx1, x, is_num1, i); - UPDATE_CURR(curr2, idx2, y, is_num2, i); - if (idx1 == 0 && m_util.is_numeral(curr1, val1, bv_size)) { - is_num1 = true; - } - if (idx2 == 0 && m_util.is_numeral(curr2, val2, bv_size)) { - is_num2 = true; - } - if ((is_num1 && (val1 % two).is_zero()) || - (is_num2 && (val2 % two).is_zero())) { - val1 = div(val1, two); - val2 = div(val2, two); - continue; - } - return; - } - mk_bv_or(2, a->get_args(), result); -#endif - - for (unsigned i = 0; i < sz; ++i) { - if (!is_zero_bit(x,i) && !is_zero_bit(y,i)) { - return; - } - } - mk_bv_or(2, a->get_args(), result); -} - -bool bv_simplifier_plugin::is_zero_bit(expr* x, unsigned idx) { - rational val; - unsigned bv_size; - if (m_util.is_numeral(x, val, bv_size)) { - if (val.is_zero()) { - return true; - } - rational two(2); - while (idx > 0) { - val = div(val, two); - idx--; - } - return (val % two).is_zero(); - } - if (m_util.is_concat(x)) { - unsigned num_args = to_app(x)->get_num_args(); - while (num_args > 0) { - --num_args; - expr* y = to_app(x)->get_arg(num_args); - bv_size = m_util.get_bv_size(y); - if (bv_size <= idx) { - idx -= bv_size; - } - else { - return is_zero_bit(y, idx); - } - } - UNREACHABLE(); - } - - return false; -} diff --git a/src/ast/simplifier/bv_simplifier_plugin.h b/src/ast/simplifier/bv_simplifier_plugin.h deleted file mode 100644 index 7208b6dc8..000000000 --- a/src/ast/simplifier/bv_simplifier_plugin.h +++ /dev/null @@ -1,187 +0,0 @@ -/*++ -Copyright (c) 2007 Microsoft Corporation - -Module Name: - - bv_simplifier_plugin.h - -Abstract: - - Simplifier for the bv family. - -Author: - - Leonardo (leonardo) 2008-01-08 - ---*/ -#ifndef BV_SIMPLIFIER_PLUGIN_H_ -#define BV_SIMPLIFIER_PLUGIN_H_ - -#include "ast/simplifier/basic_simplifier_plugin.h" -#include "ast/simplifier/poly_simplifier_plugin.h" -#include "ast/bv_decl_plugin.h" -#include "util/map.h" -#include "ast/simplifier/bv_simplifier_params.h" -#include "ast/arith_decl_plugin.h" - -/** - \brief Simplifier for the bv family. -*/ -class bv_simplifier_plugin : public poly_simplifier_plugin { - - typedef rational numeral; - struct extract_entry { - unsigned m_high; - unsigned m_low; - expr * m_arg; - extract_entry():m_high(0), m_low(0), m_arg(0) {} - extract_entry(unsigned h, unsigned l, expr * n):m_high(h), m_low(l), m_arg(n) {} - unsigned hash() const { - unsigned a = m_high; - unsigned b = m_low; - unsigned c = m_arg->get_id(); - mix(a,b,c); - return c; - } - bool operator==(const extract_entry & e) const { - return m_high == e.m_high && m_low == e.m_low && m_arg == e.m_arg; - } - struct hash_proc { - unsigned operator()(extract_entry const& e) const { return e.hash(); } - }; - struct eq_proc { - bool operator()(extract_entry const& a, extract_entry const& b) const { return a == b; } - }; - }; - typedef map extract_cache; - -protected: - ast_manager& m_manager; - bv_util m_util; - arith_util m_arith; - basic_simplifier_plugin & m_bsimp; - bv_simplifier_params & m_params; - expr_ref_vector m_zeros; - extract_cache m_extract_cache; - - unsigned_vector m_lows, m_highs; - ptr_vector m_extract_args; - - rational mk_bv_and(numeral const& a0, numeral const& b0, unsigned sz); - rational mk_bv_or(numeral const& a0, numeral const& b0, unsigned sz); - rational mk_bv_xor(numeral const& a0, numeral const& b0, unsigned sz); - rational mk_bv_not(numeral const& a0, unsigned sz); - rational num(expr* e); - bool has_sign_bit(numeral const& n, unsigned bv_size) { return m_util.has_sign_bit(n, bv_size); } - - bool shift_shift(bv_op_kind k, expr* arg1, expr* arg2, expr_ref& result); - - void bit2bool_simplify(unsigned idx, expr* e, expr_ref& result); - - void mk_add_concat(expr_ref& result); - bool is_zero_bit(expr* x, unsigned idx); - - void mk_bv_rotate_left_core(unsigned shift, numeral r, unsigned bv_size, expr_ref& result); - void mk_bv_rotate_right_core(unsigned shift, numeral r, unsigned bv_size, expr_ref& result); - -public: - bv_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, bv_simplifier_params & p); - virtual ~bv_simplifier_plugin(); - - - // simplifier_plugin: - 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); - virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result); - virtual void flush_caches(); - - // poly_simplifier_plugin - virtual rational norm(const rational & n); - virtual bool is_numeral(expr * n, rational & val) const; - bool is_numeral(expr * n) const { return m_util.is_numeral(n); } - virtual bool is_minus_one(expr * n) const { return is_minus_one_core(n); } - virtual expr * get_zero(sort * s) const; - virtual app * mk_numeral(rational const & n); - - bool is_bv(expr * n) const { return m_util.is_bv(n); } - bool is_bv_sort(sort * s) const { return m_util.is_bv_sort(s); } - - bool is_le(expr * n) const { return m_util.is_bv_ule(n) || m_util.is_bv_sle(n); } - // REMARK: simplified bv expressions are never of the form a >= b. - virtual bool is_le_ge(expr * n) const { return is_le(n); } - - uint64 to_uint64(const numeral & n, unsigned bv_size); - rational norm(rational const& n, unsigned bv_size, bool is_signed) { return m_util.norm(n, bv_size, is_signed); } - unsigned get_bv_size(expr const * n) { return get_bv_size(m_manager.get_sort(n)); } - unsigned get_bv_size(sort const * s) { return m_util.get_bv_size(s); } - void mk_leq_core(bool is_signed, expr * arg1, expr * arg2, expr_ref & result); - void mk_ule(expr* a, expr* b, expr_ref& result); - void mk_ult(expr* a, expr* b, expr_ref& result); - void mk_sle(expr* a, expr* b, expr_ref& result); - void mk_slt(expr* a, expr* b, expr_ref& result); - void mk_bv_and(unsigned num_args, expr * const* args, expr_ref & result); - void mk_bv_or(unsigned num_args, expr * const* args, expr_ref & result); - void mk_bv_xor(unsigned num_args, expr * const* args, expr_ref & result); - void mk_bv_not(expr * arg, expr_ref & result); - void mk_extract(unsigned hi,unsigned lo, expr* bv, expr_ref& result); - void mk_extract_core(unsigned high, unsigned low, expr * arg, expr_ref& result); - void cache_extract(unsigned h, unsigned l, expr * arg, expr * result); - expr* get_cached_extract(unsigned h, unsigned l, expr * arg); - - bool lookup_mk_extract(unsigned high, unsigned low, expr * arg, expr_ref& result); - bool try_mk_extract(unsigned high, unsigned low, expr * arg, expr_ref& result); - - void mk_bv_eq(expr* a1, expr* a2, expr_ref& result); - void mk_eq_core(expr * arg1, expr * arg2, expr_ref & result); - void mk_args_eq_numeral(app * app, expr * n, expr_ref & result); - - void mk_concat(unsigned num_args, expr * const * args, expr_ref & result); - void mk_concat(expr * arg1, expr * arg2, expr_ref & result) { - expr * args[2] = { arg1, arg2 }; - mk_concat(2, args, result); - } - void mk_zeroext(unsigned n, expr * arg, expr_ref & result); - void mk_repeat(unsigned n, expr * arg, expr_ref & result); - void mk_sign_extend(unsigned n, expr * arg, expr_ref & result); - void mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result); - void mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result); - void mk_bv_ashr(expr* arg1, expr* arg2, expr_ref& result); - void mk_bv_smod(expr* arg1, expr* arg2, expr_ref& result); - void mk_bv_urem(expr * arg1, expr * arg2, expr_ref & result); - void mk_bv_srem(expr* arg1, expr* arg2, expr_ref& result); - void mk_bv_udiv(expr* arg1, expr* arg2, expr_ref& result); - void mk_bv_sdiv(expr* arg1, expr* arg2, expr_ref& result); - void mk_bv_smod_i(expr* arg1, expr* arg2, expr_ref& result); - void mk_bv_urem_i(expr * arg1, expr * arg2, expr_ref & result); - void mk_bv_srem_i(expr* arg1, expr* arg2, expr_ref& result); - void mk_bv_udiv_i(expr* arg1, expr* arg2, expr_ref& result); - void mk_bv_sdiv_i(expr* arg1, expr* arg2, expr_ref& result); - void mk_bv_nand(unsigned num_args, expr* const* args, expr_ref& result); - void mk_bv_nor(unsigned num_args, expr* const* args, expr_ref& result); - void mk_bv_xnor(unsigned num_args, expr* const* args, expr_ref& result); - void mk_bv_rotate_right(func_decl* f, expr* arg, expr_ref& result); - void mk_bv_rotate_left(func_decl* f, expr* arg, expr_ref& result); - void mk_bv_ext_rotate_right(expr* arg1, expr* arg2, expr_ref& result); - void mk_bv_ext_rotate_left(expr* arg1, expr* arg2, expr_ref& result); - - void mk_bv_redor(expr* arg, expr_ref& result); - void mk_bv_redand(expr* arg, expr_ref& result); - void mk_bv_comp(expr* arg1, expr* arg2, expr_ref& result); - - bool are_numerals(unsigned num_args, expr * const* args, unsigned& bv_size); - app * mk_numeral(rational const & n, unsigned bv_size); - app * mk_numeral(uint64 n, unsigned bv_size) { return mk_numeral(numeral(n, numeral::ui64()), bv_size); } - app* mk_bv0(unsigned bv_size) { return m_util.mk_numeral(numeral(0), bv_size); } - rational mk_allone(unsigned bv_size) { return rational::power_of_two(bv_size) - numeral(1); } - bool is_minus_one_core(expr * arg) const; - bool is_x_minus_one(expr * arg, expr * & x); - void mk_int2bv(expr * arg, sort* range, expr_ref & result); - void mk_bv2int(expr * arg, sort* range, expr_ref & result); - uint64 n64(expr* e); - bool is_mul_no_overflow(expr* e); - bool is_add_no_overflow(expr* e); - unsigned num_leading_zero_bits(expr* e); - -}; - -#endif /* BV_SIMPLIFIER_PLUGIN_H_ */ diff --git a/src/ast/simplifier/datatype_simplifier_plugin.cpp b/src/ast/simplifier/datatype_simplifier_plugin.cpp deleted file mode 100644 index b665ed101..000000000 --- a/src/ast/simplifier/datatype_simplifier_plugin.cpp +++ /dev/null @@ -1,115 +0,0 @@ -/*++ -Copyright (c) 2008 Microsoft Corporation - -Module Name: - - datatype_simplifier_plugin.cpp - -Abstract: - - Simplifier for algebraic datatypes. - -Author: - - nbjorner 2008-11-6 - ---*/ - -#include "ast/simplifier/datatype_simplifier_plugin.h" - -datatype_simplifier_plugin::datatype_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b): - simplifier_plugin(symbol("datatype"), m), - m_util(m), - m_bsimp(b) { -} - -datatype_simplifier_plugin::~datatype_simplifier_plugin() { -} - -bool datatype_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - set_reduce_invoked(); - - SASSERT(f->get_family_id() == get_family_id()); - switch(f->get_decl_kind()) { - case OP_DT_CONSTRUCTOR: { - return false; - } - case OP_DT_RECOGNISER: { - // - // simplify is_cons(cons(x,y)) -> true - // simplify is_cons(nil) -> false - // - SASSERT(num_args == 1); - - if (!is_app_of(args[0], get_family_id(), OP_DT_CONSTRUCTOR)) { - return false; - } - app* a = to_app(args[0]); - func_decl* f1 = a->get_decl(); - func_decl* f2 = m_util.get_recognizer_constructor(f); - if (f1 == f2) { - result = m_manager.mk_true(); - } - else { - result = m_manager.mk_false(); - } - return true; - } - case OP_DT_ACCESSOR: { - // - // simplify head(cons(x,y)) -> x - // - SASSERT(num_args == 1); - - if (!is_app_of(args[0], get_family_id(), OP_DT_CONSTRUCTOR)) { - return false; - } - app* a = to_app(args[0]); - func_decl* f1 = a->get_decl(); - func_decl* f2 = m_util.get_accessor_constructor(f); - if (f1 != f2) { - return false; - } - ptr_vector const* acc = m_util.get_constructor_accessors(f1); - SASSERT(acc && acc->size() == a->get_num_args()); - for (unsigned i = 0; i < acc->size(); ++i) { - if (f == (*acc)[i]) { - // found it. - result = a->get_arg(i); - return true; - } - } - UNREACHABLE(); - } - case OP_DT_UPDATE_FIELD: - return false; - default: - UNREACHABLE(); - } - - return false; -} - -bool datatype_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) { - set_reduce_invoked(); - if (is_app_of(lhs, get_family_id(), OP_DT_CONSTRUCTOR) && - is_app_of(rhs, get_family_id(), OP_DT_CONSTRUCTOR)) { - app* a = to_app(lhs); - app* b = to_app(rhs); - if (a->get_decl() != b->get_decl()) { - result = m_manager.mk_false(); - return true; - } - expr_ref_vector eqs(m_manager); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - m_bsimp.mk_eq(a->get_arg(i),b->get_arg(i), result); - eqs.push_back(result); - } - m_bsimp.mk_and(eqs.size(), eqs.c_ptr(), result); - return true; - } - // TBD: occurs check, constructor check. - - return false; -} - diff --git a/src/ast/simplifier/datatype_simplifier_plugin.h b/src/ast/simplifier/datatype_simplifier_plugin.h deleted file mode 100644 index e976beba7..000000000 --- a/src/ast/simplifier/datatype_simplifier_plugin.h +++ /dev/null @@ -1,42 +0,0 @@ -/*++ -Copyright (c) 2008 Microsoft Corporation - -Module Name: - - datatype_simplifier_plugin.h - -Abstract: - - Simplifier for algebraic datatypes. - -Author: - - nbjorner 2008-11-6 - ---*/ -#ifndef DATATYPE_SIMPLIFIER_PLUGIN_H_ -#define DATATYPE_SIMPLIFIER_PLUGIN_H_ - -#include "ast/simplifier/basic_simplifier_plugin.h" -#include "ast/datatype_decl_plugin.h" - -/** - \brief Simplifier for the arith family. -*/ -class datatype_simplifier_plugin : public simplifier_plugin { - datatype_util m_util; - basic_simplifier_plugin & m_bsimp; - - -public: - datatype_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b); - ~datatype_simplifier_plugin(); - - - 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); - -}; - -#endif /* DATATYPE_SIMPLIFIER_PLUGIN_H_ */ diff --git a/src/ast/simplifier/elim_bounds.cpp b/src/ast/simplifier/elim_bounds.cpp deleted file mode 100644 index 738fc3012..000000000 --- a/src/ast/simplifier/elim_bounds.cpp +++ /dev/null @@ -1,224 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - elim_bounds.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-06-28. - -Revision History: - ---*/ -#include "ast/simplifier/elim_bounds.h" -#include "ast/used_vars.h" -#include "util/obj_hashtable.h" -#include "ast/rewriter/var_subst.h" -#include "ast/ast_pp.h" - -elim_bounds::elim_bounds(ast_manager & m): - m_manager(m), - m_util(m) { -} - -/** - \brief Find bounds of the form - - (<= x k) - (<= (+ x (* -1 y)) k) - (<= (+ x (* -1 t)) k) - (<= (+ t (* -1 x)) k) - - x and y are a bound variables, t is a ground term and k is a numeral - - It also detects >=, and the atom can be negated. -*/ -bool elim_bounds::is_bound(expr * n, var * & lower, var * & upper) { - upper = 0; - lower = 0; - bool neg = false; - if (m_manager.is_not(n)) { - n = to_app(n)->get_arg(0); - neg = true; - } - - bool le = false; - if (m_util.is_le(n)) { - SASSERT(m_util.is_numeral(to_app(n)->get_arg(1))); - n = to_app(n)->get_arg(0); - le = true; - } - else if (m_util.is_ge(n)) { - SASSERT(m_util.is_numeral(to_app(n)->get_arg(1))); - n = to_app(n)->get_arg(0); - le = false; - } - else { - return false; - } - - if (neg) - le = !le; - - if (is_var(n)) { - upper = to_var(n); - } - else if (m_util.is_add(n) && to_app(n)->get_num_args() == 2) { - expr * arg1 = to_app(n)->get_arg(0); - expr * arg2 = to_app(n)->get_arg(1); - if (is_var(arg1)) - upper = to_var(arg1); - else if (!is_ground(arg1)) - return false; - rational k; - bool is_int; - if (m_util.is_mul(arg2) && m_util.is_numeral(to_app(arg2)->get_arg(0), k, is_int) && k.is_minus_one()) { - arg2 = to_app(arg2)->get_arg(1); - if (is_var(arg2)) - lower = to_var(arg2); - else if (!is_ground(arg2)) - return false; // not supported - } - else { - return false; // not supported - } - } - else { - return false; - } - - if (!le) - std::swap(upper, lower); - - return true; -} - -bool elim_bounds::is_bound(expr * n) { - var * lower, * upper; - return is_bound(n, lower, upper); -} - -void elim_bounds::operator()(quantifier * q, expr_ref & r) { - if (!q->is_forall()) { - r = q; - return; - } - expr * n = q->get_expr(); - unsigned num_vars = q->get_num_decls(); - ptr_buffer atoms; - if (m_manager.is_or(n)) - atoms.append(to_app(n)->get_num_args(), to_app(n)->get_args()); - else - atoms.push_back(n); - used_vars m_used_vars; - // collect non-candidates - unsigned sz = atoms.size(); - for (unsigned i = 0; i < sz; i++) { - expr * a = atoms[i]; - if (!is_bound(a)) - m_used_vars.process(a); - } - if (m_used_vars.uses_all_vars(q->get_num_decls())) { - r = q; - return; - } - // collect candidates - obj_hashtable m_lowers; - obj_hashtable m_uppers; - obj_hashtable m_candidate_set; - ptr_buffer m_candidates; -#define ADD_CANDIDATE(V) if (!m_lowers.contains(V) && !m_uppers.contains(V)) { m_candidate_set.insert(V); m_candidates.push_back(V); } - for (unsigned i = 0; i < sz; i++) { - expr * a = atoms[i]; - var * lower = 0; - var * upper = 0; - if (is_bound(a, lower, upper)) { - if (lower != 0 && !m_used_vars.contains(lower->get_idx()) && lower->get_idx() < num_vars) { - ADD_CANDIDATE(lower); - m_lowers.insert(lower); - } - if (upper != 0 && !m_used_vars.contains(upper->get_idx()) && upper->get_idx() < num_vars) { - ADD_CANDIDATE(upper); - m_uppers.insert(upper); - } - } - } - TRACE("elim_bounds", tout << "candidates:\n"; for (unsigned i = 0; i < m_candidates.size(); i++) tout << mk_pp(m_candidates[i], m_manager) << "\n";); - // remove candidates that have lower and upper bounds - for (unsigned i = 0; i < m_candidates.size(); i++) { - var * v = m_candidates[i]; - if (m_lowers.contains(v) && m_uppers.contains(v)) - m_candidate_set.erase(v); - } - TRACE("elim_bounds", tout << "candidates after filter:\n"; for (unsigned i = 0; i < m_candidates.size(); i++) tout << mk_pp(m_candidates[i], m_manager) << "\n";); - if (m_candidate_set.empty()) { - r = q; - return; - } - // remove bounds that contain variables in m_candidate_set - unsigned j = 0; - for (unsigned i = 0; i < sz; i++) { - expr * a = atoms[i]; - var * lower = 0; - var * upper = 0; - if (is_bound(a, lower, upper) && ((lower != 0 && m_candidate_set.contains(lower)) || (upper != 0 && m_candidate_set.contains(upper)))) - continue; - atoms[j] = a; - j++; - } - atoms.resize(j); - expr * new_body = 0; - switch (atoms.size()) { - case 0: - r = m_manager.mk_false(); - TRACE("elim_bounds", tout << mk_pp(q, m_manager) << "\n" << mk_pp(r, m_manager) << "\n";); - return; - case 1: - new_body = atoms[0]; - break; - default: - new_body = m_manager.mk_or(atoms.size(), atoms.c_ptr()); - break; - } - quantifier_ref new_q(m_manager); - new_q = m_manager.update_quantifier(q, new_body); - elim_unused_vars(m_manager, new_q, params_ref(), r); - TRACE("elim_bounds", tout << mk_pp(q, m_manager) << "\n" << mk_pp(r, m_manager) << "\n";); -} - -bool elim_bounds_star::visit_quantifier(quantifier * q) { - if (!q->is_forall() || q->get_num_patterns() != 0) - return true; - bool visited = true; - visit(q->get_expr(), visited); - return visited; -} - -void elim_bounds_star::reduce1_quantifier(quantifier * q) { - if (!q->is_forall() || q->get_num_patterns() != 0) { - cache_result(q, q, 0); - return; - } - quantifier_ref new_q(m); - expr * new_body = 0; - proof * new_pr; - get_cached(q->get_expr(), new_body, new_pr); - new_q = m.update_quantifier(q, new_body); - expr_ref r(m); - m_elim(new_q, r); - if (q == r.get()) { - cache_result(q, q, 0); - return; - } - proof_ref pr(m); - if (m.fine_grain_proofs()) - pr = m.mk_rewrite(q, r); // TODO: improve justification - cache_result(q, r, pr); -} - diff --git a/src/ast/simplifier/elim_bounds.h b/src/ast/simplifier/elim_bounds.h deleted file mode 100644 index d4da953a8..000000000 --- a/src/ast/simplifier/elim_bounds.h +++ /dev/null @@ -1,69 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - elim_bounds.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-06-28. - -Revision History: - ---*/ -#ifndef ELIM_BOUNDS_H_ -#define ELIM_BOUNDS_H_ - -#include "ast/ast.h" -#include "ast/arith_decl_plugin.h" -#include "ast/simplifier/simplifier.h" - -/** - \brief Functor for eliminating irrelevant bounds in quantified formulas. - - Example: - (forall (x Int) (y Int) (or (not (>= y x) (not (>= x 0)) (= (select a x) 1)))) - - The bound (>= y x) is irrelevant and can be eliminated. - - This can be easily proved by using Fourier-Motzkin elimination. - - Limitations & Assumptions: - - It assumes the input formula was already simplified. - - It can only handle bounds in the diff-logic fragment. - - \remark This operation is subsumed by Fourier-Motzkin elimination. -*/ -class elim_bounds { - ast_manager & m_manager; - arith_util m_util; - bool is_bound(expr * n, var * & lower, var * & upper); - bool is_bound(expr * n); -public: - elim_bounds(ast_manager & m); - void operator()(quantifier * q, expr_ref & r); -}; - -/** - \brief Functor for applying elim_bounds in all - universal quantifiers in an expression. - - Assumption: the formula was already skolemized. -*/ -class elim_bounds_star : public simplifier { -protected: - elim_bounds m_elim; - virtual bool visit_quantifier(quantifier * q); - virtual void reduce1_quantifier(quantifier * q); -public: - elim_bounds_star(ast_manager & m):simplifier(m), m_elim(m) { enable_ac_support(false); } - virtual ~elim_bounds_star() {} -}; - -#endif /* ELIM_BOUNDS_H_ */ - diff --git a/src/ast/simplifier/fpa_simplifier_plugin.cpp b/src/ast/simplifier/fpa_simplifier_plugin.cpp deleted file mode 100644 index 2d333c872..000000000 --- a/src/ast/simplifier/fpa_simplifier_plugin.cpp +++ /dev/null @@ -1,39 +0,0 @@ -/*++ -Copyright (c) 2015 Microsoft Corporation - -Module Name: - - fpa_simplifier_plugin.cpp - -Abstract: - - Simplifier for the floating-point theory - -Author: - - Christoph (cwinter) 2015-01-14 - ---*/ -#include "ast/simplifier/fpa_simplifier_plugin.h" - -fpa_simplifier_plugin::fpa_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b) : -simplifier_plugin(symbol("fpa"), m), -m_util(m), -m_rw(m) {} - -fpa_simplifier_plugin::~fpa_simplifier_plugin() {} - -bool fpa_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - set_reduce_invoked(); - - SASSERT(f->get_family_id() == get_family_id()); - - return m_rw.mk_app_core(f, num_args, args, result) != BR_FAILED; -} - -bool fpa_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) { - set_reduce_invoked(); - - return m_rw.mk_eq_core(lhs, rhs, result) != BR_FAILED; -} - diff --git a/src/ast/simplifier/fpa_simplifier_plugin.h b/src/ast/simplifier/fpa_simplifier_plugin.h deleted file mode 100644 index 8c9f8de4e..000000000 --- a/src/ast/simplifier/fpa_simplifier_plugin.h +++ /dev/null @@ -1,39 +0,0 @@ -/*++ -Copyright (c) 2015 Microsoft Corporation - -Module Name: - - fpa_simplifier_plugin.h - -Abstract: - - Simplifier for the floating-point theory - -Author: - - Christoph (cwinter) 2015-01-14 - ---*/ -#ifndef FPA_SIMPLIFIER_PLUGIN_H_ -#define FPA_SIMPLIFIER_PLUGIN_H_ - -#include "ast/simplifier/basic_simplifier_plugin.h" -#include "ast/fpa_decl_plugin.h" -#include "ast/rewriter/fpa_rewriter.h" - -class fpa_simplifier_plugin : public simplifier_plugin { - fpa_util m_util; - fpa_rewriter m_rw; - -public: - fpa_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b); - ~fpa_simplifier_plugin(); - - - 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); - -}; - -#endif /* FPA_SIMPLIFIER_PLUGIN_H_ */ diff --git a/src/ast/simplifier/poly_simplifier_plugin.cpp b/src/ast/simplifier/poly_simplifier_plugin.cpp deleted file mode 100644 index 88637d694..000000000 --- a/src/ast/simplifier/poly_simplifier_plugin.cpp +++ /dev/null @@ -1,835 +0,0 @@ -/*++ -Copyright (c) 2007 Microsoft Corporation - -Module Name: - - poly_simplifier_plugin.cpp - -Abstract: - - Abstract class for families that have polynomials. - -Author: - - Leonardo (leonardo) 2008-01-08 - ---*/ -#include "ast/simplifier/poly_simplifier_plugin.h" -#include "ast/ast_pp.h" -#include "ast/ast_util.h" -#include "ast/ast_smt2_pp.h" -#include "ast/ast_ll_pp.h" - -poly_simplifier_plugin::poly_simplifier_plugin(symbol const & fname, ast_manager & m, decl_kind add, decl_kind mul, decl_kind uminus, decl_kind sub, - decl_kind num): - simplifier_plugin(fname, m), - m_ADD(add), - m_MUL(mul), - m_SUB(sub), - m_UMINUS(uminus), - m_NUM(num), - m_curr_sort(0), - m_curr_sort_zero(0) { -} - -expr * poly_simplifier_plugin::mk_add(unsigned num_args, expr * const * args) { - SASSERT(num_args > 0); -#ifdef Z3DEBUG - // check for incorrect use of mk_add - for (unsigned i = 0; i < num_args; i++) { - SASSERT(!is_zero(args[i])); - } -#endif - if (num_args == 1) - return args[0]; - else - return m_manager.mk_app(m_fid, m_ADD, num_args, args); -} - -expr * poly_simplifier_plugin::mk_mul(unsigned num_args, expr * const * args) { - SASSERT(num_args > 0); -#ifdef Z3DEBUG - // check for incorrect use of mk_mul - set_curr_sort(args[0]); - SASSERT(!is_zero(args[0])); - numeral k; - for (unsigned i = 0; i < num_args; i++) { - SASSERT(!is_numeral(args[i], k) || !k.is_one()); - SASSERT(i == 0 || !is_numeral(args[i])); - } -#endif - if (num_args == 1) - return args[0]; - else if (num_args == 2) - return m_manager.mk_app(m_fid, m_MUL, args[0], args[1]); - else if (is_numeral(args[0])) - return m_manager.mk_app(m_fid, m_MUL, args[0], m_manager.mk_app(m_fid, m_MUL, num_args - 1, args+1)); - else - return m_manager.mk_app(m_fid, m_MUL, num_args, args); -} - -expr * poly_simplifier_plugin::mk_mul(numeral const & c, expr * body) { - numeral c_prime, d; - c_prime = norm(c); - if (c_prime.is_zero()) - return 0; - if (body == 0) - return mk_numeral(c_prime); - if (c_prime.is_one()) - return body; - if (is_numeral(body, d)) { - c_prime = norm(c_prime*d); - if (c_prime.is_zero()) - return 0; - return mk_numeral(c_prime); - } - set_curr_sort(body); - expr * args[2] = { mk_numeral(c_prime), body }; - return mk_mul(2, args); -} - -/** - \brief Traverse args, and copy the non-numeral exprs to result, and accumulate the - value of the numerals in k. -*/ -void poly_simplifier_plugin::process_monomial(unsigned num_args, expr * const * args, numeral & k, ptr_buffer & result) { - rational v; - for (unsigned i = 0; i < num_args; i++) { - expr * arg = args[i]; - if (is_numeral(arg, v)) - k *= v; - else - result.push_back(arg); - } -} - -#ifdef Z3DEBUG -/** - \brief Return true if m is a wellformed monomial. -*/ -bool poly_simplifier_plugin::wf_monomial(expr * m) const { - SASSERT(!is_add(m)); - if (is_mul(m)) { - app * curr = to_app(m); - expr * pp = 0; - if (is_numeral(curr->get_arg(0))) - pp = curr->get_arg(1); - else - pp = curr; - if (is_mul(pp)) { - for (unsigned i = 0; i < to_app(pp)->get_num_args(); i++) { - expr * arg = to_app(pp)->get_arg(i); - CTRACE("wf_monomial_bug", is_mul(arg), - tout << "m: " << mk_ismt2_pp(m, m_manager) << "\n"; - tout << "pp: " << mk_ismt2_pp(pp, m_manager) << "\n"; - tout << "arg: " << mk_ismt2_pp(arg, m_manager) << "\n"; - tout << "i: " << i << "\n"; - ); - SASSERT(!is_mul(arg)); - SASSERT(!is_numeral(arg)); - } - } - } - return true; -} - -/** - \brief Return true if m is a wellformed polynomial. -*/ -bool poly_simplifier_plugin::wf_polynomial(expr * m) const { - if (is_add(m)) { - for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { - expr * arg = to_app(m)->get_arg(i); - SASSERT(!is_add(arg)); - SASSERT(wf_monomial(arg)); - } - } - else if (is_mul(m)) { - SASSERT(wf_monomial(m)); - } - return true; -} -#endif - -/** - \brief Functor used to sort the elements of a monomial. - Force numeric constants to be in the beginning. -*/ -struct monomial_element_lt_proc { - poly_simplifier_plugin & m_plugin; - monomial_element_lt_proc(poly_simplifier_plugin & p):m_plugin(p) {} - bool operator()(expr * m1, expr * m2) const { - SASSERT(!m_plugin.is_numeral(m1) || !m_plugin.is_numeral(m2)); - if (m_plugin.is_numeral(m1)) - return true; - if (m_plugin.is_numeral(m2)) - return false; - return m1->get_id() < m2->get_id(); - } -}; - -/** - \brief Create a monomial (* args). -*/ -void poly_simplifier_plugin::mk_monomial(unsigned num_args, expr * * args, expr_ref & result) { - switch(num_args) { - case 0: - result = mk_one(); - break; - case 1: - result = args[0]; - break; - default: - std::stable_sort(args, args + num_args, monomial_element_lt_proc(*this)); - result = mk_mul(num_args, args); - SASSERT(wf_monomial(result)); - break; - } -} - -/** - \brief Return the body of the monomial. That is, the monomial without a coefficient. - Examples: (* 2 (* x y)) ==> (* x y) - (* x x) ==> (* x x) - x ==> x - 10 ==> 10 -*/ -expr * poly_simplifier_plugin::get_monomial_body(expr * m) { - TRACE("get_monomial_body_bug", tout << mk_pp(m, m_manager) << "\n";); - SASSERT(wf_monomial(m)); - if (!is_mul(m)) - return m; - if (is_numeral(to_app(m)->get_arg(0))) - return to_app(m)->get_arg(1); - return m; -} - -inline bool is_essentially_var(expr * n, family_id fid) { - SASSERT(is_var(n) || is_app(n)); - return is_var(n) || to_app(n)->get_family_id() != fid; -} - -/** - \brief Hack for ordering monomials. - We want an order << where - - (* c1 m1) << (* c2 m2) when m1->get_id() < m2->get_id(), and c1 and c2 are numerals. - - c << m when c is a numeral, and m is not. - - So, this method returns -1 for numerals, and the id of the body of the monomial -*/ -int poly_simplifier_plugin::get_monomial_body_order(expr * m) { - if (is_essentially_var(m, m_fid)) { - return m->get_id(); - } - else if (is_mul(m)) { - if (is_numeral(to_app(m)->get_arg(0))) - return to_app(m)->get_arg(1)->get_id(); - else - return m->get_id(); - } - else if (is_numeral(m)) { - return -1; - } - else { - return m->get_id(); - } -} - -void poly_simplifier_plugin::get_monomial_coeff(expr * m, numeral & result) { - SASSERT(!is_numeral(m)); - SASSERT(wf_monomial(m)); - if (!is_mul(m)) - result = numeral::one(); - else if (is_numeral(to_app(m)->get_arg(0), result)) - return; - else - result = numeral::one(); -} - -/** - \brief Return true if n1 and n2 can be written as k1 * t and k2 * t, where k1 and - k2 are numerals, or n1 and n2 are both numerals. -*/ -bool poly_simplifier_plugin::eq_monomials_modulo_k(expr * n1, expr * n2) { - bool is_num1 = is_numeral(n1); - bool is_num2 = is_numeral(n2); - if (is_num1 != is_num2) - return false; - if (is_num1 && is_num2) - return true; - return get_monomial_body(n1) == get_monomial_body(n2); -} - -/** - \brief Return (k1 + k2) * t (or (k1 - k2) * t when inv = true), where n1 = k1 * t, and n2 = k2 * t - Return false if the monomials cancel each other. -*/ -bool poly_simplifier_plugin::merge_monomials(bool inv, expr * n1, expr * n2, expr_ref & result) { - numeral k1; - numeral k2; - bool is_num1 = is_numeral(n1, k1); - bool is_num2 = is_numeral(n2, k2); - SASSERT(is_num1 == is_num2); - if (!is_num1 && !is_num2) { - get_monomial_coeff(n1, k1); - get_monomial_coeff(n2, k2); - SASSERT(eq_monomials_modulo_k(n1, n2)); - } - if (inv) - k1 -= k2; - else - k1 += k2; - if (k1.is_zero()) - return false; - if (is_num1 && is_num2) { - result = mk_numeral(k1); - } - else { - expr * b = get_monomial_body(n1); - if (k1.is_one()) - result = b; - else - result = m_manager.mk_app(m_fid, m_MUL, mk_numeral(k1), b); - } - TRACE("merge_monomials", tout << mk_pp(n1, m_manager) << "\n" << mk_pp(n2, m_manager) << "\n" << mk_pp(result, m_manager) << "\n";); - return true; -} - -/** - \brief Return a monomial equivalent to -n. -*/ -void poly_simplifier_plugin::inv_monomial(expr * n, expr_ref & result) { - set_curr_sort(n); - SASSERT(wf_monomial(n)); - rational v; - SASSERT(n != 0); - TRACE("inv_monomial_bug", tout << "n:\n" << mk_ismt2_pp(n, m_manager) << "\n";); - if (is_numeral(n, v)) { - TRACE("inv_monomial_bug", tout << "is numeral\n";); - v.neg(); - result = mk_numeral(v); - } - else { - TRACE("inv_monomial_bug", tout << "is not numeral\n";); - numeral k; - get_monomial_coeff(n, k); - expr * b = get_monomial_body(n); - k.neg(); - if (k.is_one()) - result = b; - else - result = m_manager.mk_app(m_fid, m_MUL, mk_numeral(k), b); - } -} - -/** - \brief Add a monomial n to result. -*/ -template -void poly_simplifier_plugin::add_monomial_core(expr * n, expr_ref_vector & result) { - if (is_zero(n)) - return; - if (Inv) { - expr_ref n_prime(m_manager); - inv_monomial(n, n_prime); - result.push_back(n_prime); - } - else { - result.push_back(n); - } -} - -void poly_simplifier_plugin::add_monomial(bool inv, expr * n, expr_ref_vector & result) { - if (inv) - add_monomial_core(n, result); - else - add_monomial_core(n, result); -} - -/** - \brief Copy the monomials in n to result. The monomials are inverted if inv is true. - Equivalent monomials are merged. -*/ -template -void poly_simplifier_plugin::process_sum_of_monomials_core(expr * n, expr_ref_vector & result) { - SASSERT(wf_polynomial(n)); - if (is_add(n)) { - for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) - add_monomial_core(to_app(n)->get_arg(i), result); - } - else { - add_monomial_core(n, result); - } -} - -void poly_simplifier_plugin::process_sum_of_monomials(bool inv, expr * n, expr_ref_vector & result) { - if (inv) - process_sum_of_monomials_core(n, result); - else - process_sum_of_monomials_core(n, result); -} - -/** - \brief Copy the (non-numeral) monomials in n to result. The monomials are inverted if inv is true. - Equivalent monomials are merged. The constant (numeral) monomials are accumulated in k. -*/ -void poly_simplifier_plugin::process_sum_of_monomials(bool inv, expr * n, expr_ref_vector & result, numeral & k) { - SASSERT(wf_polynomial(n)); - numeral val; - if (is_add(n)) { - for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) { - expr * arg = to_app(n)->get_arg(i); - if (is_numeral(arg, val)) { - k += inv ? -val : val; - } - else { - add_monomial(inv, arg, result); - } - } - } - else if (is_numeral(n, val)) { - k += inv ? -val : val; - } - else { - add_monomial(inv, n, result); - } -} - -/** - \brief Functor used to sort monomials. - Force numeric constants to be in the beginning of a polynomial. -*/ -struct monomial_lt_proc { - poly_simplifier_plugin & m_plugin; - monomial_lt_proc(poly_simplifier_plugin & p):m_plugin(p) {} - bool operator()(expr * m1, expr * m2) const { - return m_plugin.get_monomial_body_order(m1) < m_plugin.get_monomial_body_order(m2); - } -}; - -void poly_simplifier_plugin::mk_sum_of_monomials_core(unsigned sz, expr ** ms, expr_ref & result) { - switch (sz) { - case 0: - result = mk_zero(); - break; - case 1: - result = ms[0]; - break; - default: - result = mk_add(sz, ms); - break; - } -} - -/** - \brief Return true if m is essentially a variable, or is of the form (* c x), - where c is a numeral and x is essentially a variable. - Store the "variable" in x. -*/ -bool poly_simplifier_plugin::is_simple_monomial(expr * m, expr * & x) { - if (is_essentially_var(m, m_fid)) { - x = m; - return true; - } - if (is_app(m) && to_app(m)->get_num_args() == 2) { - expr * arg1 = to_app(m)->get_arg(0); - expr * arg2 = to_app(m)->get_arg(1); - if (is_numeral(arg1) && is_essentially_var(arg2, m_fid)) { - x = arg2; - return true; - } - } - return false; -} - -/** - \brief Return true if all monomials are simple, and each "variable" occurs only once. - The method assumes the monomials were sorted using monomial_lt_proc. -*/ -bool poly_simplifier_plugin::is_simple_sum_of_monomials(expr_ref_vector & monomials) { - expr * last_var = 0; - expr * curr_var = 0; - unsigned size = monomials.size(); - for (unsigned i = 0; i < size; i++) { - expr * m = monomials.get(i); - if (!is_simple_monomial(m, curr_var)) - return false; - if (curr_var == last_var) - return false; - last_var = curr_var; - } - return true; -} - -/** - \brief Store in result the sum of the given monomials. -*/ -void poly_simplifier_plugin::mk_sum_of_monomials(expr_ref_vector & monomials, expr_ref & result) { - switch (monomials.size()) { - case 0: - result = mk_zero(); - break; - case 1: - result = monomials.get(0); - break; - default: { - TRACE("mk_sum_sort", tout << "before\n"; for (unsigned i = 0; i < monomials.size(); i++) tout << mk_ll_pp(monomials.get(i), m_manager) << "\n";); - std::stable_sort(monomials.c_ptr(), monomials.c_ptr() + monomials.size(), monomial_lt_proc(*this)); - TRACE("mk_sum_sort", tout << "after\n"; for (unsigned i = 0; i < monomials.size(); i++) tout << mk_ll_pp(monomials.get(i), m_manager) << "\n";); - if (is_simple_sum_of_monomials(monomials)) { - mk_sum_of_monomials_core(monomials.size(), monomials.c_ptr(), result); - return; - } - ptr_buffer new_monomials; - expr * last_body = 0; - numeral last_coeff; - numeral coeff; - unsigned sz = monomials.size(); - for (unsigned i = 0; i < sz; i++) { - expr * m = monomials.get(i); - expr * body = 0; - if (!is_numeral(m, coeff)) { - body = get_monomial_body(m); - get_monomial_coeff(m, coeff); - } - if (last_body == body) { - last_coeff += coeff; - continue; - } - expr * new_m = mk_mul(last_coeff, last_body); - if (new_m) - new_monomials.push_back(new_m); - last_body = body; - last_coeff = coeff; - } - expr * new_m = mk_mul(last_coeff, last_body); - if (new_m) - new_monomials.push_back(new_m); - TRACE("mk_sum", for (unsigned i = 0; i < monomials.size(); i++) tout << mk_pp(monomials.get(i), m_manager) << "\n"; - tout << "======>\n"; - for (unsigned i = 0; i < new_monomials.size(); i++) tout << mk_pp(new_monomials.get(i), m_manager) << "\n";); - mk_sum_of_monomials_core(new_monomials.size(), new_monomials.c_ptr(), result); - break; - } } -} - -/** - \brief Auxiliary template for mk_add_core -*/ -template -void poly_simplifier_plugin::mk_add_core_core(unsigned num_args, expr * const * args, expr_ref & result) { - SASSERT(num_args >= 2); - expr_ref_vector monomials(m_manager); - process_sum_of_monomials_core(args[0], monomials); - for (unsigned i = 1; i < num_args; i++) { - process_sum_of_monomials_core(args[i], monomials); - } - TRACE("mk_add_core_bug", - for (unsigned i = 0; i < monomials.size(); i++) { - SASSERT(monomials.get(i) != 0); - tout << mk_ismt2_pp(monomials.get(i), m_manager) << "\n"; - }); - mk_sum_of_monomials(monomials, result); -} - -/** - \brief Return a sum of monomials. The method assume that each arg in args is a sum of monomials. - If inv is true, then all but the first argument in args are inverted. -*/ -void poly_simplifier_plugin::mk_add_core(bool inv, unsigned num_args, expr * const * args, expr_ref & result) { - TRACE("mk_add_core_bug", - for (unsigned i = 0; i < num_args; i++) { - SASSERT(args[i] != 0); - tout << mk_ismt2_pp(args[i], m_manager) << "\n"; - }); - switch (num_args) { - case 0: - result = mk_zero(); - break; - case 1: - result = args[0]; - break; - default: - if (inv) - mk_add_core_core(num_args, args, result); - else - mk_add_core_core(num_args, args, result); - break; - } -} - -void poly_simplifier_plugin::mk_add(unsigned num_args, expr * const * args, expr_ref & result) { - SASSERT(num_args > 0); - set_curr_sort(args[0]); - mk_add_core(false, num_args, args, result); -} - -void poly_simplifier_plugin::mk_add(expr * arg1, expr * arg2, expr_ref & result) { - expr * args[2] = { arg1, arg2 }; - mk_add(2, args, result); -} - -void poly_simplifier_plugin::mk_sub(unsigned num_args, expr * const * args, expr_ref & result) { - SASSERT(num_args > 0); - set_curr_sort(args[0]); - mk_add_core(true, num_args, args, result); -} - -void poly_simplifier_plugin::mk_sub(expr * arg1, expr * arg2, expr_ref & result) { - expr * args[2] = { arg1, arg2 }; - mk_sub(2, args, result); -} - -void poly_simplifier_plugin::mk_uminus(expr * arg, expr_ref & result) { - set_curr_sort(arg); - rational v; - if (is_numeral(arg, v)) { - v.neg(); - result = mk_numeral(v); - } - else { - expr_ref zero(mk_zero(), m_manager); - mk_sub(zero.get(), arg, result); - } -} - -/** - \brief Add monomial n to result, the coeff of n is stored in k. -*/ -void poly_simplifier_plugin::append_to_monomial(expr * n, numeral & k, ptr_buffer & result) { - SASSERT(wf_monomial(n)); - rational val; - if (is_numeral(n, val)) { - k *= val; - return; - } - get_monomial_coeff(n, val); - k *= val; - n = get_monomial_body(n); - - unsigned hd = result.size(); - result.push_back(n); - while (hd < result.size()) { - n = result[hd]; - if (is_mul(n)) { - result[hd] = result.back(); - result.pop_back(); - for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) { - result.push_back(to_app(n)->get_arg(i)); - } - } - else if (is_numeral(n, val)) { - k *= val; - result[hd] = result.back(); - result.pop_back(); - } - else { - ++hd; - } - } -} - -/** - \brief Return a sum of monomials that is equivalent to (* args[0] ... args[num_args-1]). - This method assumes that each arg[i] is a sum of monomials. -*/ -void poly_simplifier_plugin::mk_mul(unsigned num_args, expr * const * args, expr_ref & result) { - if (num_args == 1) { - result = args[0]; - return; - } - rational val; - if (num_args == 2 && is_numeral(args[0], val) && is_essentially_var(args[1], m_fid)) { - if (val.is_one()) - result = args[1]; - else if (val.is_zero()) - result = args[0]; - else - result = mk_mul(num_args, args); - return; - } - if (num_args == 2 && is_essentially_var(args[0], m_fid) && is_numeral(args[1], val)) { - if (val.is_one()) - result = args[0]; - else if (val.is_zero()) - result = args[1]; - else { - expr * inv_args[2] = { args[1], args[0] }; - result = mk_mul(2, inv_args); - } - return; - } - - TRACE("mk_mul_bug", - for (unsigned i = 0; i < num_args; i++) { - tout << mk_pp(args[i], m_manager) << "\n"; - }); - set_curr_sort(args[0]); - buffer szs; - buffer it; - vector > sums; - for (unsigned i = 0; i < num_args; i ++) { - it.push_back(0); - expr * arg = args[i]; - SASSERT(wf_polynomial(arg)); - sums.push_back(ptr_vector()); - ptr_vector & v = sums.back(); - if (is_add(arg)) { - v.append(to_app(arg)->get_num_args(), to_app(arg)->get_args()); - } - else { - v.push_back(arg); - } - szs.push_back(v.size()); - } - expr_ref_vector monomials(m_manager); - do { - rational k(1); - ptr_buffer m; - for (unsigned i = 0; i < num_args; i++) { - ptr_vector & v = sums[i]; - expr * arg = v[it[i]]; - TRACE("mk_mul_bug", tout << "k: " << k << " arg: " << mk_pp(arg, m_manager) << "\n";); - append_to_monomial(arg, k, m); - TRACE("mk_mul_bug", tout << "after k: " << k << "\n";); - } - expr_ref num(m_manager); - if (!k.is_zero() && !k.is_one()) { - num = mk_numeral(k); - m.push_back(num); - // bit-vectors can normalize - // to 1 during - // internalization. - if (is_numeral(num, k) && k.is_one()) { - m.pop_back(); - } - } - if (!k.is_zero()) { - expr_ref new_monomial(m_manager); - TRACE("mk_mul_bug", - for (unsigned i = 0; i < m.size(); i++) { - tout << mk_pp(m[i], m_manager) << "\n"; - }); - mk_monomial(m.size(), m.c_ptr(), new_monomial); - TRACE("mk_mul_bug", tout << "new_monomial:\n" << mk_pp(new_monomial, m_manager) << "\n";); - add_monomial_core(new_monomial, monomials); - } - } - while (product_iterator_next(szs.size(), szs.c_ptr(), it.c_ptr())); - mk_sum_of_monomials(monomials, result); -} - -void poly_simplifier_plugin::mk_mul(expr * arg1, expr * arg2, expr_ref & result) { - expr * args[2] = { arg1, arg2 }; - mk_mul(2, args, result); -} - -bool poly_simplifier_plugin::reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result) { - set_reduce_invoked(); - unsigned i = 0; - for (; i < num_args; i++) - if (!is_numeral(args[i])) - break; - if (i == num_args) { - // all arguments are numerals - // check if arguments are different... - ptr_buffer buffer; - buffer.append(num_args, args); - std::sort(buffer.begin(), buffer.end(), ast_lt_proc()); - for (unsigned i = 0; i < num_args; i++) { - if (i > 0 && buffer[i] == buffer[i-1]) { - result = m_manager.mk_false(); - return true; - } - } - result = m_manager.mk_true(); - return true; - } - return false; -} - -bool poly_simplifier_plugin::reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result) { - set_reduce_invoked(); - if (is_decl_of(f, m_fid, m_ADD)) { - SASSERT(num_args > 0); - set_curr_sort(args[0]); - expr_ref_buffer args1(m_manager); - for (unsigned i = 0; i < num_args; ++i) { - expr * arg = args[i]; - rational m = norm(mults[i]); - if (m.is_zero()) { - // skip - } - else if (m.is_one()) { - args1.push_back(arg); - } - else { - expr_ref k(m_manager); - k = mk_numeral(m); - expr_ref new_arg(m_manager); - mk_mul(k, args[i], new_arg); - args1.push_back(new_arg); - } - } - if (args1.empty()) { - result = mk_zero(); - } - else { - mk_add(args1.size(), args1.c_ptr(), result); - } - return true; - } - else { - return simplifier_plugin::reduce(f, num_args, mults, args, result); - } -} - -/** - \brief Return true if n is can be put into the form (+ v t) or (+ (- v) t) - \c inv = true will contain true if (- v) is found, and false otherwise. -*/ -bool poly_simplifier_plugin::is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) { - if (!is_add(n) || is_ground(n)) - return false; - - ptr_buffer args; - v = 0; - expr * curr = to_app(n); - bool stop = false; - inv = false; - while (!stop) { - expr * arg; - expr * neg_arg; - if (is_add(curr)) { - arg = to_app(curr)->get_arg(0); - curr = to_app(curr)->get_arg(1); - } - else { - arg = curr; - stop = true; - } - if (is_ground(arg)) { - TRACE("model_checker_bug", tout << "pushing:\n" << mk_pp(arg, m_manager) << "\n";); - args.push_back(arg); - } - else if (is_var(arg)) { - if (v != 0) - return false; // already found variable - v = to_var(arg); - } - else if (is_times_minus_one(arg, neg_arg) && is_var(neg_arg)) { - if (v != 0) - return false; // already found variable - v = to_var(neg_arg); - inv = true; - } - else { - return false; // non ground term. - } - } - if (v == 0) - return false; // did not find variable - SASSERT(!args.empty()); - mk_add(args.size(), args.c_ptr(), t); - return true; -} diff --git a/src/ast/simplifier/poly_simplifier_plugin.h b/src/ast/simplifier/poly_simplifier_plugin.h deleted file mode 100644 index fe5572b20..000000000 --- a/src/ast/simplifier/poly_simplifier_plugin.h +++ /dev/null @@ -1,155 +0,0 @@ -/*++ -Copyright (c) 2007 Microsoft Corporation - -Module Name: - - poly_simplifier_plugin.h - -Abstract: - - Abstract class for families that have polynomials. - -Author: - - Leonardo (leonardo) 2008-01-08 - ---*/ -#ifndef POLY_SIMPLIFIER_PLUGIN_H_ -#define POLY_SIMPLIFIER_PLUGIN_H_ - -#include "ast/simplifier/simplifier_plugin.h" - -/** - \brief Abstract class that provides simplification functions for polynomials. -*/ -class poly_simplifier_plugin : public simplifier_plugin { -protected: - typedef rational numeral; - decl_kind m_ADD; - decl_kind m_MUL; - decl_kind m_SUB; - decl_kind m_UMINUS; - decl_kind m_NUM; - sort * m_curr_sort; - expr * m_curr_sort_zero; - - expr * mk_add(unsigned num_args, expr * const * args); - expr * mk_add(expr * arg1, expr * arg2) { expr * args[2] = { arg1, arg2 }; return mk_add(2, args); } - expr * mk_mul(unsigned num_args, expr * const * args); - expr * mk_mul(expr * arg1, expr * arg2) { expr * args[2] = { arg1, arg2 }; return mk_mul(2, args); } - // expr * mk_sub(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_fid, m_SUB, num_args, args); } - expr * mk_uminus(expr * arg) { return m_manager.mk_app(m_fid, m_UMINUS, arg); } - - void process_monomial(unsigned num_args, expr * const * args, numeral & k, ptr_buffer & result); - void mk_monomial(unsigned num_args, expr * * args, expr_ref & result); - bool eq_monomials_modulo_k(expr * n1, expr * n2); - bool merge_monomials(bool inv, expr * n1, expr * n2, expr_ref & result); - template - void add_monomial_core(expr * n, expr_ref_vector & result); - void add_monomial(bool inv, expr * n, expr_ref_vector & result); - template - void process_sum_of_monomials_core(expr * n, expr_ref_vector & result); - void process_sum_of_monomials(bool inv, expr * n, expr_ref_vector & result); - void process_sum_of_monomials(bool inv, expr * n, expr_ref_vector & result, numeral & k); - void mk_sum_of_monomials(expr_ref_vector & monomials, expr_ref & result); - template - void mk_add_core_core(unsigned num_args, expr * const * args, expr_ref & result); - void mk_add_core(bool inv, unsigned num_args, expr * const * args, expr_ref & result); - void append_to_monomial(expr * n, numeral & k, ptr_buffer & result); - expr * mk_mul(numeral const & c, expr * body); - void mk_sum_of_monomials_core(unsigned sz, expr ** ms, expr_ref & result); - bool is_simple_sum_of_monomials(expr_ref_vector & monomials); - bool is_simple_monomial(expr * m, expr * & x); - -public: - poly_simplifier_plugin(symbol const & fname, ast_manager & m, decl_kind add, decl_kind mul, decl_kind uminus, decl_kind sub, decl_kind num); - virtual ~poly_simplifier_plugin() {} - - /** - \brief Return true if the given expression is a numeral, and store its value in \c val. - */ - virtual bool is_numeral(expr * n, numeral & val) const = 0; - bool is_numeral(expr * n) const { return is_app_of(n, m_fid, m_NUM); } - bool is_zero(expr * n) const { - SASSERT(m_curr_sort_zero != 0); - SASSERT(m_manager.get_sort(n) == m_manager.get_sort(m_curr_sort_zero)); - return n == m_curr_sort_zero; - } - bool is_zero_safe(expr * n) { - set_curr_sort(m_manager.get_sort(n)); - return is_zero(n); - } - virtual bool is_minus_one(expr * n) const = 0; - virtual expr * get_zero(sort * s) const = 0; - - - /** - \brief Return true if n is of the form (* -1 r) - */ - bool is_times_minus_one(expr * n, expr * & r) const { - if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) { - r = to_app(n)->get_arg(1); - return true; - } - return false; - } - - /** - \brief Return true if n is of the form: a <= b or a >= b. - */ - virtual bool is_le_ge(expr * n) const = 0; - - /** - \brief Return a constant representing the giving numeral and sort m_curr_sort. - */ - virtual app * mk_numeral(numeral const & n) = 0; - app * mk_zero() { return mk_numeral(numeral::zero()); } - app * mk_one() { return mk_numeral(numeral::one()); } - app * mk_minus_one() { return mk_numeral(numeral::minus_one()); } - - /** - \brief Normalize the given numeral with respect to m_curr_sort - */ - virtual numeral norm(numeral const & n) = 0; - - void set_curr_sort(sort * s) { - if (s != m_curr_sort) { - // avoid virtual function call - m_curr_sort = s; - m_curr_sort_zero = get_zero(m_curr_sort); - } - } - void set_curr_sort(expr * n) { set_curr_sort(m_manager.get_sort(n)); } - - bool is_add(expr const * n) const { return is_app_of(n, m_fid, m_ADD); } - bool is_mul(expr const * n) const { return is_app_of(n, m_fid, m_MUL); } - void mk_add(unsigned num_args, expr * const * args, expr_ref & result); - void mk_add(expr * arg1, expr * arg2, expr_ref & result); - void mk_sub(unsigned num_args, expr * const * args, expr_ref & result); - void mk_sub(expr * arg1, expr * arg2, expr_ref & result); - void mk_uminus(expr * arg, expr_ref & result); - void mk_mul(unsigned num_args, expr * const * args, expr_ref & result); - void mk_mul(expr * arg1, expr * arg2, expr_ref & result); - - virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result); - - virtual bool reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result); - virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - return simplifier_plugin::reduce(f, num_args, args, result); - } - - - expr * get_monomial_body(expr * m); - int get_monomial_body_order(expr * m); - void get_monomial_coeff(expr * m, numeral & result); - void inv_monomial(expr * n, expr_ref & result); - - bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t); - -#ifdef Z3DEBUG - bool wf_monomial(expr * m) const; - bool wf_polynomial(expr * m) const; -#endif -}; - -#endif /* POLY_SIMPLIFIER_PLUGIN_H_ */ diff --git a/src/ast/simplifier/seq_simplifier_plugin.cpp b/src/ast/simplifier/seq_simplifier_plugin.cpp deleted file mode 100644 index 2125c4f4c..000000000 --- a/src/ast/simplifier/seq_simplifier_plugin.cpp +++ /dev/null @@ -1,39 +0,0 @@ -/*++ -Copyright (c) 2016 Microsoft Corporation - -Module Name: - - seq_simplifier_plugin.cpp - -Abstract: - - Simplifier for the theory of sequences - -Author: - - Nikolaj Bjorner (nbjorner) 2016-02-05 - ---*/ -#include "ast/simplifier/seq_simplifier_plugin.h" - -seq_simplifier_plugin::seq_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b) : -simplifier_plugin(symbol("seq"), m), -m_util(m), -m_rw(m) {} - -seq_simplifier_plugin::~seq_simplifier_plugin() {} - -bool seq_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - set_reduce_invoked(); - - SASSERT(f->get_family_id() == get_family_id()); - - return m_rw.mk_app_core(f, num_args, args, result) != BR_FAILED; -} - -bool seq_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) { - set_reduce_invoked(); - - return m_rw.mk_eq_core(lhs, rhs, result) != BR_FAILED; -} - diff --git a/src/ast/simplifier/seq_simplifier_plugin.h b/src/ast/simplifier/seq_simplifier_plugin.h deleted file mode 100644 index a37a2209f..000000000 --- a/src/ast/simplifier/seq_simplifier_plugin.h +++ /dev/null @@ -1,39 +0,0 @@ -/*++ -Copyright (c) 2016 Microsoft Corporation - -Module Name: - - seq_simplifier_plugin.h - -Abstract: - - Simplifier for the sequence theory - -Author: - - Nikolaj Bjorner (nbjorner) 2016-02-05 - ---*/ -#ifndef SEQ_SIMPLIFIER_PLUGIN_H_ -#define SEQ_SIMPLIFIER_PLUGIN_H_ - -#include "ast/simplifier/basic_simplifier_plugin.h" -#include "ast/seq_decl_plugin.h" -#include "ast/rewriter/seq_rewriter.h" - -class seq_simplifier_plugin : public simplifier_plugin { - seq_util m_util; - seq_rewriter m_rw; - -public: - seq_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b); - ~seq_simplifier_plugin(); - - - 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); - -}; - -#endif /* SEQ_SIMPLIFIER_PLUGIN_H_ */ diff --git a/src/ast/simplifier/simplifier.cpp b/src/ast/simplifier/simplifier.cpp deleted file mode 100644 index c02753440..000000000 --- a/src/ast/simplifier/simplifier.cpp +++ /dev/null @@ -1,962 +0,0 @@ -/*++ -Copyright (c) 2007 Microsoft Corporation - -Module Name: - - simplifier.cpp - -Abstract: - - Expression simplifier. - -Author: - - Leonardo (leonardo) 2008-01-03 - -Notes: - ---*/ -#include "ast/simplifier/simplifier.h" -#include "ast/rewriter/var_subst.h" -#include "ast/ast_ll_pp.h" -#include "ast/ast_pp.h" -#include "ast/well_sorted.h" -#include "ast/ast_smt_pp.h" - -simplifier::simplifier(ast_manager & m): - base_simplifier(m), - m_proofs(m), - m_subst_proofs(m), - m_need_reset(false), - m_use_oeq(false), - m_visited_quantifier(false), - m_ac_support(true) { -} - -void simplifier::register_plugin(plugin * p) { - m_plugins.register_plugin(p); -} - -simplifier::~simplifier() { - flush_cache(); -} - -void simplifier::enable_ac_support(bool flag) { - m_ac_support = flag; - ptr_vector::const_iterator it = m_plugins.begin(); - ptr_vector::const_iterator end = m_plugins.end(); - for (; it != end; ++it) { - if (*it != 0) - (*it)->enable_ac_support(flag); - } -} - -/** - \brief External interface for the simplifier. - A client will invoke operator()(s, r, p) to simplify s. - The result is stored in r. - When proof generation is enabled, a proof for the equivalence (or equisatisfiability) - of s and r is stored in p. - When proof generation is disabled, this method stores the "undefined proof" object in p. -*/ -void simplifier::operator()(expr * s, expr_ref & r, proof_ref & p) { - m_need_reset = true; - reinitialize(); - expr * s_orig = s; - (void)s_orig; - expr * old_s; - expr * result; - proof * result_proof; - switch (m.proof_mode()) { - case PGM_DISABLED: // proof generation is disabled. - reduce_core(s); - // after executing reduce_core, the result of the simplification is in the cache - get_cached(s, result, result_proof); - r = result; - p = m.mk_undef_proof(); - break; - case PGM_COARSE: // coarse proofs... in this case, we do not produce a step by step (fine grain) proof to show the equivalence (or equisatisfiability) of s an r. - m_subst_proofs.reset(); // m_subst_proofs is an auxiliary vector that is used to justify substitutions. See comment on method get_subst. - reduce_core(s); - get_cached(s, result, result_proof); - r = result; - if (result == s) - p = m.mk_reflexivity(s); - else { - remove_duplicates(m_subst_proofs); - p = m.mk_rewrite_star(s, result, m_subst_proofs.size(), m_subst_proofs.c_ptr()); - } - break; - case PGM_FINE: // fine grain proofs... in this mode, every proof step (or most of them) is described. - m_proofs.reset(); - old_s = 0; - // keep simplyfing until no further simplifications are possible. - while (s != old_s) { - TRACE("simplifier", tout << "simplification pass... " << s->get_id() << "\n";); - TRACE("simplifier_loop", tout << mk_ll_pp(s, m) << "\n";); - reduce_core(s); - get_cached(s, result, result_proof); - SASSERT(is_rewrite_proof(s, result, result_proof)); - if (result_proof != 0) { - m_proofs.push_back(result_proof); - } - old_s = s; - s = result; - } - SASSERT(s != 0); - r = s; - p = m_proofs.empty() ? m.mk_reflexivity(s) : m.mk_transitivity(m_proofs.size(), m_proofs.c_ptr()); - SASSERT(is_rewrite_proof(s_orig, r, p)); - break; - default: - UNREACHABLE(); - } -} - -void simplifier::flush_cache() { - m_cache.flush(); - ptr_vector::const_iterator it = m_plugins.begin(); - ptr_vector::const_iterator end = m_plugins.end(); - for (; it != end; ++it) { - if (*it != 0) { - (*it)->flush_caches(); - } - } -} - -bool simplifier::get_subst(expr * n, expr_ref & r, proof_ref & p) { - return false; -} - -void simplifier::reduce_core(expr * n1) { - if (!is_cached(n1)) { - // We do not assume m_todo is empty... So, we store the current size of the todo-stack. - unsigned sz = m_todo.size(); - m_todo.push_back(n1); - while (m_todo.size() != sz) { - expr * n = m_todo.back(); - if (is_cached(n)) - m_todo.pop_back(); - else if (visit_children(n)) { - // if all children were already simplified, then remove n from the todo stack and apply a - // simplification step to it. - m_todo.pop_back(); - reduce1(n); - } - if (m.canceled()) { - cache_result(n1, n1, 0); - break; - } - } - } -} - -/** - \brief Return true if all children of n have been already simplified. -*/ -bool simplifier::visit_children(expr * n) { - switch(n->get_kind()) { - case AST_VAR: - return true; - case AST_APP: - // The simplifier has support for flattening AC (associative-commutative) operators. - // The method ast_manager::mk_app is used to create the flat version of an AC operator. - // In Z3 1.x, we used multi-ary operators. This creates problems for the superposition engine. - // So, starting at Z3 2.x, only boolean operators can be multi-ary. - // Example: - // (and (and a b) (and c d)) --> (and a b c d) - // (+ (+ a b) (+ c d)) --> (+ a (+ b (+ c d))) - // Remark: The flattening is only applied if m_ac_support is true. - if (m_ac_support && to_app(n)->get_decl()->is_associative() && to_app(n)->get_decl()->is_commutative()) - return visit_ac(to_app(n)); - else { - bool visited = true; - unsigned j = to_app(n)->get_num_args(); - while (j > 0) { - --j; - visit(to_app(n)->get_arg(j), visited); - } - return visited; - } - case AST_QUANTIFIER: - return visit_quantifier(to_quantifier(n)); - default: - UNREACHABLE(); - return true; - } -} - -/** - \brief Visit the children of n assuming it is an AC (associative-commutative) operator. - - For example, if n is of the form (+ (+ a b) (+ c d)), this method - will return true if the nodes a, b, c and d have been already simplified. - The nodes (+ a b) and (+ c d) are not really checked. -*/ -bool simplifier::visit_ac(app * n) { - bool visited = true; - func_decl * decl = n->get_decl(); - SASSERT(m_ac_support); - SASSERT(decl->is_associative()); - SASSERT(decl->is_commutative()); - m_ac_marked.reset(); - ptr_buffer todo; - todo.push_back(n); - while (!todo.empty()) { - app * n = todo.back(); - todo.pop_back(); - if (m_ac_mark.is_marked(n)) - continue; - m_ac_mark.mark(n, true); - m_ac_marked.push_back(n); - SASSERT(n->get_decl() == decl); - unsigned i = n->get_num_args(); - while (i > 0) { - --i; - expr * arg = n->get_arg(i); - if (is_app_of(arg, decl)) - todo.push_back(to_app(arg)); - else - visit(arg, visited); - } - } - ptr_vector::const_iterator it = m_ac_marked.begin(); - ptr_vector::const_iterator end = m_ac_marked.end(); - for (; it != end; ++it) - m_ac_mark.mark(*it, false); - return visited; -} - -bool simplifier::visit_quantifier(quantifier * n) { - m_visited_quantifier = true; - bool visited = true; - unsigned j = to_quantifier(n)->get_num_patterns(); - while (j > 0) { - --j; - visit(to_quantifier(n)->get_pattern(j), visited); - } - j = to_quantifier(n)->get_num_no_patterns(); - while (j > 0) { - --j; - visit(to_quantifier(n)->get_no_pattern(j), visited); - } - visit(to_quantifier(n)->get_expr(), visited); - return visited; -} - -/** - \brief Simplify n and store the result in the cache. -*/ -void simplifier::reduce1(expr * n) { - switch (n->get_kind()) { - case AST_VAR: - cache_result(n, n, 0); - break; - case AST_APP: - reduce1_app(to_app(n)); - break; - case AST_QUANTIFIER: - reduce1_quantifier(to_quantifier(n)); - break; - default: - UNREACHABLE(); - } -} - -/** - \brief Simplify the given application using the cached values, - associativity flattening, the given substitution, and family/theory - specific simplifications via plugins. -*/ -void simplifier::reduce1_app(app * n) { - expr_ref r(m); - proof_ref p(m); - TRACE("reduce", tout << "reducing...\n" << mk_pp(n, m) << "\n";); - if (get_subst(n, r, p)) { - TRACE("reduce", tout << "applying substitution...\n";); - cache_result(n, r, p); - return; - } - - func_decl * decl = n->get_decl(); - if (m_ac_support && decl->is_associative() && decl->is_commutative()) - reduce1_ac_app_core(n); - else - reduce1_app_core(n); -} - - -void simplifier::reduce1_app_core(app * n) { - m_args.reset(); - func_decl * decl = n->get_decl(); - proof_ref p1(m); - // Stores the new arguments of n in m_args. - // Let n be of the form - // (decl arg_0 ... arg_{n-1}) - // then - // m_args contains [arg_0', ..., arg_{n-1}'], - // where arg_i' is the simplification of arg_i - // and - // p1 is a proof for - // (decl arg_0 ... arg_{n-1}) is equivalente/equisatisfiable to (decl arg_0' ... arg_{n-1}') - // p1 is built using the congruence proof step and the proofs for arg_0' ... arg_{n-1}'. - // Of course, p1 is 0 if proofs are not enabled or coarse grain proofs are used. - bool has_new_args = get_args(n, m_args, p1); - // The following if implements a simple trick. - // If none of the arguments have been simplified, and n is not a theory symbol, - // Then no simplification is possible, and we can cache the result of the simplification of n as n. - if (has_new_args || decl->get_family_id() != null_family_id) { - expr_ref r(m); - TRACE("reduce", tout << "reduce1_app\n"; for(unsigned i = 0; i < m_args.size(); i++) tout << mk_ll_pp(m_args[i], m);); - // the method mk_app invokes get_subst and plugins to simplify - // (decl arg_0' ... arg_{n-1}') - mk_app(decl, m_args.size(), m_args.c_ptr(), r); - if (!m.fine_grain_proofs()) { - cache_result(n, r, 0); - } - else { - expr * s = m.mk_app(decl, m_args.size(), m_args.c_ptr()); - proof * p; - if (n == r) - p = 0; - else if (r != s) - // we use a "theory rewrite generic proof" to justify the step - // s = (decl arg_0' ... arg_{n-1}') --> r - p = m.mk_transitivity(p1, m.mk_rewrite(s, r)); - else - p = p1; - cache_result(n, r, p); - } - } - else { - cache_result(n, n, 0); - } -} - -bool is_ac_list(app * n, ptr_vector & args) { - args.reset(); - func_decl * f = n->get_decl(); - app * curr = n; - while (true) { - if (curr->get_num_args() != 2) - return false; - expr * arg1 = curr->get_arg(0); - if (is_app_of(arg1, f)) - return false; - args.push_back(arg1); - expr * arg2 = curr->get_arg(1); - if (!is_app_of(arg2, f)) { - args.push_back(arg2); - return true; - } - curr = to_app(arg2); - } -} - -bool is_ac_vector(app * n) { - func_decl * f = n->get_decl(); - unsigned num_args = n->get_num_args(); - for (unsigned i = 0; i < num_args; i++) { - if (is_app_of(n->get_arg(i), f)) - return false; - } - return true; -} - -void simplifier::reduce1_ac_app_core(app * n) { - app_ref n_c(m); - proof_ref p1(m); - mk_ac_congruent_term(n, n_c, p1); - TRACE("ac", tout << "expr:\n" << mk_pp(n, m) << "\ncongruent term:\n" << mk_pp(n_c, m) << "\n";); - expr_ref r(m); - func_decl * decl = n->get_decl(); - family_id fid = decl->get_family_id(); - plugin * p = get_plugin(fid); - if (is_ac_vector(n_c)) { - if (p != 0 && p->reduce(decl, n_c->get_num_args(), n_c->get_args(), r)) { - // done... - } - else { - r = n_c; - } - } - else if (is_ac_list(n_c, m_args)) { - // m_args contains the arguments... - if (p != 0 && p->reduce(decl, m_args.size(), m_args.c_ptr(), r)) { - // done... - } - else { - r = m.mk_app(decl, m_args.size(), m_args.c_ptr()); - } - } - else { - m_args.reset(); - m_mults.reset(); - get_ac_args(n_c, m_args, m_mults); - TRACE("ac", tout << "AC args:\n"; - for (unsigned i = 0; i < m_args.size(); i++) { - tout << mk_pp(m_args[i], m) << " * " << m_mults[i] << "\n"; - }); - if (p != 0 && p->reduce(decl, m_args.size(), m_mults.c_ptr(), m_args.c_ptr(), r)) { - // done... - } - else { - ptr_buffer new_args; - expand_args(m_args.size(), m_mults.c_ptr(), m_args.c_ptr(), new_args); - r = m.mk_app(decl, new_args.size(), new_args.c_ptr()); - } - } - TRACE("ac", tout << "AC result:\n" << mk_pp(r, m) << "\n";); - - if (!m.fine_grain_proofs()) { - cache_result(n, r, 0); - } - else { - proof * p; - if (n == r.get()) - p = 0; - else if (r.get() != n_c.get()) - p = m.mk_transitivity(p1, m.mk_rewrite(n_c, r)); - else - p = p1; - cache_result(n, r, p); - } -} - -static unsigned g_rewrite_lemma_id = 0; - -void simplifier::dump_rewrite_lemma(func_decl * decl, unsigned num_args, expr * const * args, expr* result) { - expr_ref arg(m); - arg = m.mk_app(decl, num_args, args); - if (arg.get() != result) { - char buffer[128]; -#ifdef _WINDOWS - sprintf_s(buffer, ARRAYSIZE(buffer), "lemma_%d.smt", g_rewrite_lemma_id); -#else - sprintf(buffer, "rewrite_lemma_%d.smt", g_rewrite_lemma_id); -#endif - ast_smt_pp pp(m); - pp.set_benchmark_name("rewrite_lemma"); - pp.set_status("unsat"); - expr_ref n(m); - n = m.mk_not(m.mk_eq(arg.get(), result)); - std::ofstream out(buffer); - pp.display(out, n); - out.close(); - ++g_rewrite_lemma_id; - } -} - -/** - \brief Return in \c result an expression \c e equivalent to (f args[0] ... args[num_args - 1]), and - store in \c pr a proof for (= (f args[0] ... args[num_args - 1]) e) - - If e is identical to (f args[0] ... args[num_args - 1]), then pr is set to 0. -*/ -void simplifier::mk_app(func_decl * decl, unsigned num_args, expr * const * args, expr_ref & result) { - m_need_reset = true; - if (m.is_eq(decl)) { - sort * s = m.get_sort(args[0]); - plugin * p = get_plugin(s->get_family_id()); - if (p != 0 && p->reduce_eq(args[0], args[1], result)) - return; - } - else if (m.is_distinct(decl)) { - sort * s = m.get_sort(args[0]); - plugin * p = get_plugin(s->get_family_id()); - if (p != 0 && p->reduce_distinct(num_args, args, result)) - return; - } - family_id fid = decl->get_family_id(); - plugin * p = get_plugin(fid); - if (p != 0 && p->reduce(decl, num_args, args, result)) { - //uncomment this line if you want to trace rewrites as lemmas: - //dump_rewrite_lemma(decl, num_args, args, result.get()); - return; - } - - result = m.mk_app(decl, num_args, args); -} - -/** - \brief Create a term congruence to n (f a[0] ... a[num_args-1]) using the - cached values for the a[i]'s. Store the result in r, and the proof for (= n r) in p. - If n and r are identical, then set p to 0. -*/ -void simplifier::mk_congruent_term(app * n, app_ref & r, proof_ref & p) { - bool has_new_args = false; - ptr_vector args; - ptr_vector proofs; - unsigned num = n->get_num_args(); - for (unsigned j = 0; j < num; j++) { - expr * arg = n->get_arg(j); - expr * new_arg; - proof * arg_proof; - get_cached(arg, new_arg, arg_proof); - - CTRACE("simplifier_bug", (arg != new_arg) != (arg_proof != 0), - tout << mk_ll_pp(arg, m) << "\n---->\n" << mk_ll_pp(new_arg, m) << "\n"; - tout << "#" << arg->get_id() << " #" << new_arg->get_id() << "\n"; - tout << arg << " " << new_arg << "\n";); - - - if (arg != new_arg) { - has_new_args = true; - proofs.push_back(arg_proof); - SASSERT(arg_proof); - } - else { - SASSERT(arg_proof == 0); - } - args.push_back(new_arg); - } - if (has_new_args) { - r = m.mk_app(n->get_decl(), args.size(), args.c_ptr()); - if (m_use_oeq) - p = m.mk_oeq_congruence(n, r, proofs.size(), proofs.c_ptr()); - else - p = m.mk_congruence(n, r, proofs.size(), proofs.c_ptr()); - } - else { - r = n; - p = 0; - } -} - -/** - \brief Store the new arguments of \c n in result. Store in p a proof for - (= n (f result[0] ... result[num_args - 1])), where f is the function symbol of n. - - If there are no new arguments or fine grain proofs are disabled, then p is set to 0. - - Return true there are new arguments. -*/ -bool simplifier::get_args(app * n, ptr_vector & result, proof_ref & p) { - bool has_new_args = false; - unsigned num = n->get_num_args(); - if (m.fine_grain_proofs()) { - app_ref r(m); - mk_congruent_term(n, r, p); - result.append(r->get_num_args(), r->get_args()); - SASSERT(n->get_num_args() == result.size()); - has_new_args = r != n; - } - else { - p = 0; - for (unsigned j = 0; j < num; j++) { - expr * arg = n->get_arg(j); - expr * new_arg; - proof * arg_proof; - get_cached(arg, new_arg, arg_proof); - if (arg != new_arg) { - has_new_args = true; - } - result.push_back(new_arg); - } - } - return has_new_args; -} - -/** - \brief Create a term congruence to n (where n is an expression such as: (f (f a_1 a_2) (f a_3 (f a_4 a_5))) using the - cached values for the a_i's. Store the result in r, and the proof for (= n r) in p. - If n and r are identical, then set p to 0. -*/ -void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) { - SASSERT(m_ac_support); - func_decl * f = n->get_decl(); - - m_ac_cache.reset(); - m_ac_pr_cache.reset(); - - ptr_buffer todo; - ptr_buffer new_args; - ptr_buffer new_arg_prs; - todo.push_back(n); - while (!todo.empty()) { - app * curr = todo.back(); - if (m_ac_cache.contains(curr)) { - todo.pop_back(); - continue; - } - bool visited = true; - bool has_new_arg = false; - new_args.reset(); - new_arg_prs.reset(); - unsigned num_args = curr->get_num_args(); - for (unsigned j = 0; j < num_args; j ++) { - expr * arg = curr->get_arg(j); - if (is_app_of(arg, f)) { - app * new_arg = 0; - if (m_ac_cache.find(to_app(arg), new_arg)) { - SASSERT(new_arg != 0); - new_args.push_back(new_arg); - if (arg != new_arg) - has_new_arg = true; - if (m.fine_grain_proofs()) { - proof * pr = 0; - m_ac_pr_cache.find(to_app(arg), pr); - if (pr != 0) - new_arg_prs.push_back(pr); - } - } - else { - visited = false; - todo.push_back(to_app(arg)); - } - } - else { - expr * new_arg = 0; - proof * pr; - get_cached(arg, new_arg, pr); - new_args.push_back(new_arg); - if (arg != new_arg) - has_new_arg = true; - if (m.fine_grain_proofs() && pr != 0) - new_arg_prs.push_back(pr); - } - } - if (visited) { - SASSERT(new_args.size() == curr->get_num_args()); - todo.pop_back(); - if (!has_new_arg) { - m_ac_cache.insert(curr, curr); - if (m.fine_grain_proofs()) - m_ac_pr_cache.insert(curr, 0); - } - else { - app * new_curr = m.mk_app(f, new_args.size(), new_args.c_ptr()); - m_ac_cache.insert(curr, new_curr); - if (m.fine_grain_proofs()) { - proof * p = m.mk_congruence(curr, new_curr, new_arg_prs.size(), new_arg_prs.c_ptr()); - m_ac_pr_cache.insert(curr, p); - } - } - } - } - - SASSERT(m_ac_cache.contains(n)); - app * new_n = 0; - m_ac_cache.find(n, new_n); - r = new_n; - if (m.fine_grain_proofs()) { - proof * new_pr = 0; - m_ac_pr_cache.find(n, new_pr); - p = new_pr; - } -} - -#define White 0 -#define Grey 1 -#define Black 2 - -#ifdef Z3DEBUG -static int get_color(obj_map & colors, expr * n) { - obj_map::obj_map_entry * entry = colors.insert_if_not_there2(n, White); - return entry->get_data().m_value; -} -#endif - -static bool visit_ac_children(func_decl * f, expr * n, obj_map & colors, ptr_buffer & todo, ptr_buffer & result) { - if (is_app_of(n, f)) { - unsigned num_args = to_app(n)->get_num_args(); - bool visited = true; - // Put the arguments in 'result' in reverse order. - // Reason: preserve the original order of the arguments in the final result. - // Remark: get_ac_args will traverse 'result' backwards. - for (unsigned i = 0; i < num_args; i++) { - expr * arg = to_app(n)->get_arg(i); - obj_map::obj_map_entry * entry = colors.insert_if_not_there2(arg, White); - if (entry->get_data().m_value == White) { - todo.push_back(arg); - visited = false; - } - } - return visited; - } - else { - return true; - } -} - -void simplifier::ac_top_sort(app * n, ptr_buffer & result) { - ptr_buffer todo; - func_decl * f = n->get_decl(); - obj_map & colors = m_colors; - colors.reset(); - todo.push_back(n); - while (!todo.empty()) { - expr * curr = todo.back(); - int color; - obj_map::obj_map_entry * entry = colors.insert_if_not_there2(curr, White); - SASSERT(entry); - color = entry->get_data().m_value; - switch (color) { - case White: - // Remark: entry becomes invalid if an element is inserted into the hashtable. - // So, I must set Grey before executing visit_ac_children. - entry->get_data().m_value = Grey; - SASSERT(get_color(colors, curr) == Grey); - if (visit_ac_children(f, curr, colors, todo, result)) { - // If visit_ac_children succeeded, then the hashtable was not modified, - // and entry is still valid. - SASSERT(todo.back() == curr); - entry->get_data().m_value = Black; - SASSERT(get_color(colors, curr) == Black); - result.push_back(curr); - todo.pop_back(); - } - break; - case Grey: - SASSERT(visit_ac_children(f, curr, colors, todo, result)); - SASSERT(entry); - entry->get_data().m_value = Black; - SASSERT(get_color(colors, curr) == Black); - result.push_back(curr); - SASSERT(todo.back() == curr); - todo.pop_back(); - break; - case Black: - todo.pop_back(); - break; - default: - UNREACHABLE(); - } - } -} - -void simplifier::get_ac_args(app * n, ptr_vector & args, vector & mults) { - SASSERT(m_ac_support); - ptr_buffer sorted_exprs; - ac_top_sort(n, sorted_exprs); - SASSERT(!sorted_exprs.empty()); - SASSERT(sorted_exprs[sorted_exprs.size()-1] == n); - - TRACE("ac", tout << mk_ll_pp(n, m, true, false) << "#" << n->get_id() << "\nsorted expressions...\n"; - for (unsigned i = 0; i < sorted_exprs.size(); i++) { - tout << "#" << sorted_exprs[i]->get_id() << " "; - } - tout << "\n";); - - m_ac_mults.reset(); - m_ac_mults.insert(n, rational(1)); - func_decl * decl = n->get_decl(); - unsigned j = sorted_exprs.size(); - while (j > 0) { - --j; - expr * curr = sorted_exprs[j]; - rational mult; - m_ac_mults.find(curr, mult); - SASSERT(!mult.is_zero()); - if (is_app_of(curr, decl)) { - unsigned num_args = to_app(curr)->get_num_args(); - for (unsigned i = 0; i < num_args; i++) { - expr * arg = to_app(curr)->get_arg(i); - rational zero; - obj_map::obj_map_entry * entry = m_ac_mults.insert_if_not_there2(arg, zero); - entry->get_data().m_value += mult; - } - } - else { - args.push_back(curr); - mults.push_back(mult); - } - } -} - -void simplifier::reduce1_quantifier(quantifier * q) { - expr * new_body; - proof * new_body_pr; - SASSERT(is_well_sorted(m, q)); - get_cached(q->get_expr(), new_body, new_body_pr); - - quantifier_ref q1(m); - proof * p1 = 0; - - if (is_quantifier(new_body) && - to_quantifier(new_body)->is_forall() == q->is_forall() && - !to_quantifier(q)->has_patterns() && - !to_quantifier(new_body)->has_patterns()) { - - quantifier * nested_q = to_quantifier(new_body); - - ptr_buffer sorts; - buffer names; - sorts.append(q->get_num_decls(), q->get_decl_sorts()); - names.append(q->get_num_decls(), q->get_decl_names()); - sorts.append(nested_q->get_num_decls(), nested_q->get_decl_sorts()); - names.append(nested_q->get_num_decls(), nested_q->get_decl_names()); - - q1 = m.mk_quantifier(q->is_forall(), - sorts.size(), - sorts.c_ptr(), - names.c_ptr(), - nested_q->get_expr(), - std::min(q->get_weight(), nested_q->get_weight()), - q->get_qid(), - q->get_skid(), - 0, 0, 0, 0); - SASSERT(is_well_sorted(m, q1)); - - if (m.fine_grain_proofs()) { - quantifier * q0 = m.update_quantifier(q, new_body); - proof * p0 = q == q0 ? 0 : m.mk_quant_intro(q, q0, new_body_pr); - p1 = m.mk_pull_quant(q0, q1); - p1 = m.mk_transitivity(p0, p1); - } - } - else { - ptr_buffer new_patterns; - ptr_buffer new_no_patterns; - expr * new_pattern; - proof * new_pattern_pr; - - // Remark: we can ignore the proofs for the patterns. - unsigned num = q->get_num_patterns(); - for (unsigned i = 0; i < num; i++) { - get_cached(q->get_pattern(i), new_pattern, new_pattern_pr); - if (m.is_pattern(new_pattern)) { - new_patterns.push_back(new_pattern); - } - } - num = q->get_num_no_patterns(); - for (unsigned i = 0; i < num; i++) { - get_cached(q->get_no_pattern(i), new_pattern, new_pattern_pr); - new_no_patterns.push_back(new_pattern); - } - - remove_duplicates(new_patterns); - remove_duplicates(new_no_patterns); - - q1 = m.mk_quantifier(q->is_forall(), - q->get_num_decls(), - q->get_decl_sorts(), - q->get_decl_names(), - new_body, - q->get_weight(), - q->get_qid(), - q->get_skid(), - new_patterns.size(), - new_patterns.c_ptr(), - new_no_patterns.size(), - new_no_patterns.c_ptr()); - SASSERT(is_well_sorted(m, q1)); - - TRACE("simplifier", tout << mk_pp(q, m) << "\n" << mk_pp(q1, m) << "\n";); - if (m.fine_grain_proofs()) { - if (q != q1 && !new_body_pr) { - new_body_pr = m.mk_rewrite(q->get_expr(), new_body); - } - p1 = q == q1 ? 0 : m.mk_quant_intro(q, q1, new_body_pr); - } - } - - expr_ref r(m); - elim_unused_vars(m, q1, params_ref(), r); - - proof * pr = 0; - if (m.fine_grain_proofs()) { - proof * p2 = 0; - if (q1.get() != r.get()) - p2 = m.mk_elim_unused_vars(q1, r); - pr = m.mk_transitivity(p1, p2); - } - - cache_result(q, r, pr); -} - -/** - \see release_plugins -*/ -void simplifier::borrow_plugins(simplifier const & s) { - ptr_vector::const_iterator it = s.begin_plugins(); - ptr_vector::const_iterator end = s.end_plugins(); - for (; it != end; ++it) - register_plugin(*it); -} - -/** - \brief Make the simplifier behave as a pre-simplifier: No AC, and plugins are marked in pre-simplification mode. -*/ -void simplifier::enable_presimp() { - enable_ac_support(false); - ptr_vector::const_iterator it = begin_plugins(); - ptr_vector::const_iterator end = end_plugins(); - for (; it != end; ++it) - (*it)->enable_presimp(true); -} - -/** - \brief This method should be invoked if the plugins of this simplifier were borrowed from a different simplifier. -*/ -void simplifier::release_plugins() { - m_plugins.release(); -} - -void subst_simplifier::set_subst_map(expr_map * s) { - flush_cache(); - m_subst_map = s; -} - -bool subst_simplifier::get_subst(expr * n, expr_ref & r, proof_ref & p) { - if (m_subst_map && m_subst_map->contains(n)) { - expr * _r; - proof * _p = 0; - m_subst_map->get(n, _r, _p); - r = _r; - p = _p; - if (m.coarse_grain_proofs()) - m_subst_proofs.push_back(p); - return true; - } - return false; -} - -static void push_core(ast_manager & m, expr * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs) { - SASSERT(pr == 0 || m.is_undef_proof(pr) || e == m.get_fact(pr)); - TRACE("preprocessor", - tout << mk_pp(e, m) << "\n"; - if (pr) tout << mk_ll_pp(pr, m) << "\n\n";); - if (m.is_true(e)) - return; - result.push_back(e); - if (m.proofs_enabled()) - result_prs.push_back(pr); -} - -static void push_and(ast_manager & m, app * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs) { - unsigned num = e->get_num_args(); - TRACE("push_and", tout << mk_pp(e, m) << "\n";); - for (unsigned i = 0; i < num; i++) - push_assertion(m, e->get_arg(i), m.mk_and_elim(pr, i), result, result_prs); -} - -static void push_not_or(ast_manager & m, app * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs) { - unsigned num = e->get_num_args(); - TRACE("push_not_or", tout << mk_pp(e, m) << "\n";); - for (unsigned i = 0; i < num; i++) { - expr * child = e->get_arg(i); - if (m.is_not(child)) { - expr * not_child = to_app(child)->get_arg(0); - push_assertion(m, not_child, m.mk_not_or_elim(pr, i), result, result_prs); - } - else { - expr_ref not_child(m); - not_child = m.mk_not(child); - push_assertion(m, not_child, m.mk_not_or_elim(pr, i), result, result_prs); - } - } -} - -void push_assertion(ast_manager & m, expr * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs) { - CTRACE("push_assertion", !(pr == 0 || m.is_undef_proof(pr) || m.get_fact(pr) == e), - tout << mk_pp(e, m) << "\n" << mk_pp(m.get_fact(pr), m) << "\n";); - SASSERT(pr == 0 || m.is_undef_proof(pr) || m.get_fact(pr) == e); - if (m.is_and(e)) - push_and(m, to_app(e), pr, result, result_prs); - else if (m.is_not(e) && m.is_or(to_app(e)->get_arg(0))) - push_not_or(m, to_app(to_app(e)->get_arg(0)), pr, result, result_prs); - else - push_core(m, e, pr, result, result_prs); -} - diff --git a/src/ast/simplifier/simplifier.h b/src/ast/simplifier/simplifier.h deleted file mode 100644 index 5148721f1..000000000 --- a/src/ast/simplifier/simplifier.h +++ /dev/null @@ -1,232 +0,0 @@ -/*++ -Copyright (c) 2007 Microsoft Corporation - -Module Name: - - simplifier.h - -Abstract: - - Generic expression simplifier with support for theory specific "plugins". - -Author: - - Leonardo (leonardo) 2008-01-03 - -Notes: - ---*/ -#ifndef SIMPLIFIER_H_ -#define SIMPLIFIER_H_ - -#include "ast/simplifier/base_simplifier.h" -#include "ast/simplifier/simplifier_plugin.h" -#include "util/plugin_manager.h" -#include "ast/ast_util.h" -#include "util/obj_hashtable.h" - -/** - \brief Local simplifier. - Proof production can be enabled/disabled. - - The simplifier can also apply substitutions during the - simplification. A substitution is a mapping from expression - to expression+proof, where for each entry e_1->(e_2,p) p is - a proof for (= e_1 e_2). - - The simplifier can also generate coarse grain proofs. In a coarse - proof, local rewrite steps are omitted, and only the substitutions - used are tracked. - - Example: - - Consider the expression (+ a b), and the substitution b->(0, p) - When fine grain proofs are enabled, the simplifier will produce the - following proof - - Assume the id of the proof object p is $0. Note that p is a proof for (= b 0). - - $1: [reflexivity] |- (= a a) - $2: [congruence] $1 $0 |- (= (+ a b) (+ a 0)) - $3: [plus-0] |- (= (+ a 0) a) - $4: [transitivity] $2 $3 |- (= (+ a b) a) - - When coarse grain proofs are enabled, the simplifier produces the following - proof: - - $1: [simplifier] $0 |- (= (+ a b) a) -*/ -class simplifier : public base_simplifier { -protected: - typedef simplifier_plugin plugin; - plugin_manager m_plugins; - ptr_vector m_args; - vector m_mults; - ptr_vector m_args2; - - proof_ref_vector m_proofs; // auxiliary vector for implementing exhaustive simplification. - proof_ref_vector m_subst_proofs; // in coarse grain proof generation mode, this vector tracks the justification for substitutions (see method get_subst). - - bool m_need_reset; - bool m_use_oeq; - - bool m_visited_quantifier; //!< true, if the simplifier found a quantifier - - bool m_ac_support; - - expr_mark m_ac_mark; - ptr_vector m_ac_marked; - obj_map m_ac_cache; // temporary cache for ac - obj_map m_ac_pr_cache; // temporary cache for ac - obj_map m_colors; // temporary cache for topological sort. - obj_map m_ac_mults; - - /* - Simplifier uses an idiom for rewriting ASTs without using recursive calls. - - - It uses a cache (field m_cache in base_simplifier) and a todo-stack (field m_todo in base_simplifier). - - - The cache is a mapping from AST to (AST + Proof). An entry [n -> (n',pr)] is used to store the fact - that n and n' are equivalent and pr is a proof for that. If proofs are disabled, then pr is 0. - We say n' is the result of the simplification of n. - Note: Some simplifications do not preserve equivalence, but equisatisfiability. - For saving space, we use pr = 0 also to represent the reflexivity proof [n -> (n, 0)]. - - - - The simplifier can be extended using plugin (subclasses of the class simplifier_plugin). - Each theory has a family ID. All operators (func_decls) and sorts from a given theory have - the same family_id. Given an application (object of the class app), we use the method - get_family_id() to obtain the family id of the operator in this application. - The simplifier uses plugin to apply theory specific simplifications. The basic idea is: - whenever an AST with family_id X is found, invoke the plugin for this family_id. - A simplifier_plugin implements the following API: - 1) bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) - This method is invoked when the simplifier is trying to reduce/simplify an application - of the form (f args[0] ... args[num_args - 1]), and f has a family_id associated with - the plugin. The plugin may return false to indicate it could not simplify this application. - If it returns true (success), the result should be stored in the argument result. - - 2) bool reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result); - This method is a similar to the previous one, and it is used to handle associative operators. - A plugin does not need to implement this method, the default implementation will use the previous one. - The arguments mults indicates the multiplicity of every argument in args. - For example, suppose this reduce is invoked with the arguments (f, 2, [3, 2], [a, b], result). - This represents the application (f a a a b b). - Some theory simplifiers may have efficient ways to encode this multiplicity. For example, - the arithmetic solver, if f is "+", the multiplicity can be encoded using "*". - This optimization is used because some benchmarks can create term that are very huge when - flattened. One "real" example (that motivated this optimization) is: - let a1 = x1 + x1 - let a2 = a1 + a1 - ... - let an = a{n-1} + a{n-1} - an - In this example, n was 32, so after AC flattening, we had an application - (+ x1 ... x1) with 2^32 arguments. Using the simple reduce would produce a stack overflow. - - This class uses a topological sort for computing the multiplicities efficiently. - So, the field m_colors is used to implement the topological sort. - - - 3) bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result) - This method is invoked when the sort of lhs and rhs has a family_id associated with the plugin. - This method allows theory specific simplifications such as: - (= (+ a b) b) --> (= a 0) - Assuming n1 is a reference to (+ a b) and n2 to b, the simplifier would invoke - reduce_eq(n1, n2, result) - Like reduce, false can be returned if a simplification could not be applied. - And if true is returned, then the result is stored in the argument result. - - 4) bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result) - It is similar to reduce_eq, but it used for theory specific simplifications for - (distinct args[0] ... args[num_args-1]) - Example: - (distinct 0 1 ... n) --> true - - - The idiom used in this class is implemented in the methdo reduce_core. - See reduce_core for more details. The basic idea is: - - 1) Get the next ast to be simplified from the todo-stack. - 2) If it is already cached, then do nothing. That is, this expression was already simplified. - 3) Otherwise, check whether all arguments already have been simplified (method visit_children). - 3a) The arguments that have not been simplified are added to the todo-stack by visit_children. - In this case visit_children will return false. - 3b) If all arguments have already been simplified, then invoke reduce1 to perform a reduction/simplification - step. The cache is updated with the result. - - - After invoking reduce_core(n), the cache contains an entry [n -> (n', pr)]. - - */ - - void flush_cache(); - - /** - \brief This method can be redefined in subclasses of simplifier to implement substitutions. - It returns true if n should be substituted by r, where the substitution is justified by the - proof p. The field m_subst_proofs is used to store these justifications when coarse proofs are used (PGM_COARSE). - This method is redefined in the class subst_simplifier. It is used in asserted_formulas - for implementing constant elimination. For example, if asserted_formulas contains the atoms - (= a (+ b 1)) (p a c), then the constant "a" can be eliminated. This is achieved by set (+ b 1) as - a substitution for "a". - */ - virtual bool get_subst(expr * n, expr_ref & r, proof_ref & p); - - void reduce_core(expr * n); - bool visit_children(expr * n); - bool visit_ac(app * n); - virtual bool visit_quantifier(quantifier * q); - void reduce1(expr * n); - void reduce1_app(app * n); - void reduce1_app_core(app * n); - void reduce1_ac_app_core(app * n); - void mk_congruent_term(app * n, app_ref & r, proof_ref & p); - void mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p); - bool get_args(app * n, ptr_vector & result, proof_ref & p); - void get_ac_args(app * n, ptr_vector & args, vector & mults); - virtual void reduce1_quantifier(quantifier * q); - void dump_rewrite_lemma(func_decl * decl, unsigned num_args, expr * const * args, expr* result); - void ac_top_sort(app * n, ptr_buffer & result); - -public: - simplifier(ast_manager & manager); - virtual ~simplifier(); - - void enable_ac_support(bool flag); - - /** - \brief Simplify the expression \c s. Store the result in \c r, and a proof that (= s r) in \c p. - */ - void operator()(expr * s, expr_ref & r, proof_ref & p); - void reset() { if (m_need_reset) { flush_cache(); m_need_reset = false; } } - - bool visited_quantifier() const { return m_visited_quantifier; } - - void mk_app(func_decl * decl, unsigned num_args, expr * const * args, expr_ref & r); - void cache_result(expr * n, expr * r, proof * p) { m_need_reset = true; base_simplifier::cache_result(n, r, p); } - - void register_plugin(plugin * p); - ptr_vector::const_iterator begin_plugins() const { return m_plugins.begin(); } - ptr_vector::const_iterator end_plugins() const { return m_plugins.end(); } - - plugin * get_plugin(family_id fid) const { return m_plugins.get_plugin(fid); } - - ast_manager & get_manager() { return m; } - - void borrow_plugins(simplifier const & s); - void release_plugins(); - - void enable_presimp(); -}; - -class subst_simplifier : public simplifier { -protected: - expr_map * m_subst_map; - virtual bool get_subst(expr * n, expr_ref & r, proof_ref & p); -public: - subst_simplifier(ast_manager & manager):simplifier(manager), m_subst_map(0) {} - void set_subst_map(expr_map * s); -}; - -void push_assertion(ast_manager & m, expr * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs); - -#endif diff --git a/src/ast/simplifier/simplifier_plugin.cpp b/src/ast/simplifier/simplifier_plugin.cpp deleted file mode 100644 index a62b15131..000000000 --- a/src/ast/simplifier/simplifier_plugin.cpp +++ /dev/null @@ -1,46 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - simplifier_plugin.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-12-29. - -Revision History: - ---*/ -#include "ast/simplifier/simplifier_plugin.h" - -/** - \brief Copy every args[i] mult[i] times to new_args. -*/ -void expand_args(unsigned num_args, rational const * mults, expr * const * args, ptr_buffer & new_args) { - for (unsigned i = 0; i < num_args; i++) { - rational const & c = mults[i]; - SASSERT(c.is_int()); - rational j(0); - while (j < c) { - new_args.push_back(args[i]); - j++; - } - } -} - -bool simplifier_plugin::reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result) { - set_reduce_invoked(); - if (f->is_idempotent()) { - return reduce(f, num_args, args, result); - } - else { - ptr_buffer new_args; - expand_args(num_args, mults, args, new_args); - return reduce(f, new_args.size(), new_args.c_ptr(), result); - } -} diff --git a/src/ast/simplifier/simplifier_plugin.h b/src/ast/simplifier/simplifier_plugin.h deleted file mode 100644 index 26b5bcd59..000000000 --- a/src/ast/simplifier/simplifier_plugin.h +++ /dev/null @@ -1,94 +0,0 @@ -/*++ -Copyright (c) 2007 Microsoft Corporation - -Module Name: - - simplifier_plugin.h - -Abstract: - - Expression simplifier plugin interface. - -Author: - - Leonardo (leonardo) 2008-01-03 - ---*/ - -#ifndef SIMPLIFIER_PLUGIN_H_ -#define SIMPLIFIER_PLUGIN_H_ - -#include "ast/ast.h" - -class simplifier; - -void expand_args(unsigned num_args, rational const * mults, expr * const * args, ptr_buffer & new_args); - -/** - \brief Abstract simplifier for the operators in a given family. -*/ -class simplifier_plugin { -protected: - ast_manager & m_manager; - family_id m_fid; - bool m_presimp; // true if simplifier is performing pre-simplification... - bool m_reduce_invoked; // true if one of the reduce methods were invoked. - - void set_reduce_invoked() { m_reduce_invoked = true; } - -public: - simplifier_plugin(symbol const & fname, ast_manager & m):m_manager(m), m_fid(m.mk_family_id(fname)), m_presimp(false), m_reduce_invoked(false) {} - - bool reduce_invoked() const { return m_reduce_invoked; } - - virtual ~simplifier_plugin() {} - - virtual simplifier_plugin * mk_fresh() { - UNREACHABLE(); - return 0; - } - - /** - \brief Return in \c result an expression \c e equivalent to (f args[0] ... args[num_args - 1]). - - Return true if succeeded. - */ - virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { set_reduce_invoked(); return false; } - - /** - \brief Return in \c result an expression \c e equivalent to (f args[0] ... args[0] ... args[num_args - 1]). - Where each args[i] occurs mults[i] times. - - Return true if succeeded. - */ - virtual bool reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result); - - /** - \brief Return in \c result an expression \c e equivalent to (= lhs rhs). - - Return true if succeeded. - */ - virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result) { set_reduce_invoked(); return false; } - - /** - \brief Return in \c result an expression \c e equivalent to (distinct args[0] ... args[num_args-1]). - - Return true if succeeded. - */ - virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result) { set_reduce_invoked(); return false; } - - family_id get_family_id() const { return m_fid; } - - /** - \brief Simplifiers may maintain local caches. These caches must be flushed when this method is invoked. - */ - virtual void flush_caches() { /* do nothing */ } - - ast_manager & get_manager() { return m_manager; } - - void enable_presimp(bool flag) { m_presimp = flag; } - - virtual void enable_ac_support(bool flag) {} -}; - -#endif diff --git a/src/muz/pdr/pdr_util.cpp b/src/muz/pdr/pdr_util.cpp index 42a57214a..19ffdeeec 100644 --- a/src/muz/pdr/pdr_util.cpp +++ b/src/muz/pdr/pdr_util.cpp @@ -22,29 +22,26 @@ Notes: --*/ #include -#include "ast/simplifier/arith_simplifier_plugin.h" +#include "util/util.h" +#include "util/ref_vector.h" #include "ast/array_decl_plugin.h" #include "ast/ast_pp.h" -#include "ast/simplifier/basic_simplifier_plugin.h" -#include "ast/simplifier/bv_simplifier_plugin.h" -#include "ast/rewriter/bool_rewriter.h" -#include "muz/base/dl_util.h" #include "ast/for_each_expr.h" -#include "smt/params/smt_params.h" -#include "model/model.h" -#include "util/ref_vector.h" -#include "ast/rewriter/rewriter.h" -#include "ast/rewriter/rewriter_def.h" -#include "util/util.h" -#include "muz/pdr/pdr_manager.h" -#include "muz/pdr/pdr_util.h" +#include "ast/scoped_proof.h" #include "ast/arith_decl_plugin.h" #include "ast/rewriter/expr_replacer.h" -#include "model/model_smt2_pp.h" +#include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/poly_rewriter.h" #include "ast/rewriter/poly_rewriter_def.h" #include "ast/rewriter/arith_rewriter.h" -#include "ast/scoped_proof.h" +#include "ast/rewriter/rewriter.h" +#include "ast/rewriter/rewriter_def.h" +#include "smt/params/smt_params.h" +#include "model/model.h" +#include "muz/base/dl_util.h" +#include "muz/pdr/pdr_manager.h" +#include "muz/pdr/pdr_util.h" +#include "model/model_smt2_pp.h" diff --git a/src/muz/rel/dl_bound_relation.h b/src/muz/rel/dl_bound_relation.h index 1678e23b8..3dec9d313 100644 --- a/src/muz/rel/dl_bound_relation.h +++ b/src/muz/rel/dl_bound_relation.h @@ -26,7 +26,6 @@ Revision History: #include "muz/rel/dl_vector_relation.h" #include "muz/rel/dl_interval_relation.h" #include "ast/arith_decl_plugin.h" -#include "ast/simplifier/basic_simplifier_plugin.h" #include "ast/rewriter/bool_rewriter.h" namespace datalog { diff --git a/src/muz/rel/dl_interval_relation.h b/src/muz/rel/dl_interval_relation.h index 05334624f..a9cce9802 100644 --- a/src/muz/rel/dl_interval_relation.h +++ b/src/muz/rel/dl_interval_relation.h @@ -20,13 +20,12 @@ Revision History: #define DL_INTERVAL_RELATION_H_ +#include "ast/arith_decl_plugin.h" +#include "smt/old_interval.h" #include "muz/base/dl_context.h" #include "muz/rel/dl_relation_manager.h" #include "muz/rel/dl_base.h" -#include "smt/old_interval.h" #include "muz/rel/dl_vector_relation.h" -#include "ast/arith_decl_plugin.h" -#include "ast/simplifier/basic_simplifier_plugin.h" namespace datalog { diff --git a/src/muz/spacer/spacer_legacy_mbp.cpp b/src/muz/spacer/spacer_legacy_mbp.cpp index fc2fd1fdd..9f03e6d2f 100644 --- a/src/muz/spacer/spacer_legacy_mbp.cpp +++ b/src/muz/spacer/spacer_legacy_mbp.cpp @@ -20,9 +20,6 @@ Notes: #include "ast/array_decl_plugin.h" #include "ast/ast_pp.h" -#include "ast/simplifier/arith_simplifier_plugin.h" -#include "ast/simplifier/basic_simplifier_plugin.h" -#include "ast/simplifier/bv_simplifier_plugin.h" #include "ast/rewriter/bool_rewriter.h" #include "muz/base/dl_util.h" #include "ast/for_each_expr.h" diff --git a/src/smt/arith_eq_adapter.h b/src/smt/arith_eq_adapter.h index f18b2999f..4a8a293e3 100644 --- a/src/smt/arith_eq_adapter.h +++ b/src/smt/arith_eq_adapter.h @@ -23,7 +23,6 @@ Revision History: #include "util/obj_pair_hashtable.h" #include "ast/arith_decl_plugin.h" #include "util/statistics.h" -#include "ast/simplifier/arith_simplifier_plugin.h" namespace smt { diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 26b970d30..5f4e58a1b 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -34,7 +34,6 @@ Revision History: #include "util/obj_pair_hashtable.h" #include "smt/old_interval.h" #include "math/grobner/grobner.h" -#include "ast/simplifier/arith_simplifier_plugin.h" #include "smt/arith_eq_solver.h" #include "smt/theory_opt.h" #include "util/uint_set.h" diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index fbcc9c11a..4f15a6156 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -19,12 +19,11 @@ Revision History: #ifndef THEORY_ARITH_INT_H_ #define THEORY_ARITH_INT_H_ -#include "ast/ast_ll_pp.h" -#include "ast/simplifier/arith_simplifier_plugin.h" -#include "ast/well_sorted.h" -#include "math/euclid/euclidean_solver.h" #include "util/numeral_buffer.h" +#include "ast/ast_ll_pp.h" +#include "ast/well_sorted.h" #include "ast/ast_smt2_pp.h" +#include "math/euclid/euclidean_solver.h" namespace smt {