From f20e95184ee6532d7a538886c46cf6ad02ee9733 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 28 Aug 2017 13:29:51 -0700 Subject: [PATCH] remove old_simplify dependencies Signed-off-by: Nikolaj Bjorner --- src/CMakeLists.txt | 3 - src/ast/simplifier/CMakeLists.txt | 9 +- src/ast/simplifier/array_simplifier_params.h | 6 +- src/ast/simplifier/bv_simplifier_params.cpp | 2 +- src/ast/simplifier/maximise_ac_sharing.cpp | 192 ------------------- src/ast/simplifier/maximise_ac_sharing.h | 124 ------------ src/smt/params/CMakeLists.txt | 1 - src/smt/params/preprocessor_params.cpp | 4 - src/smt/params/preprocessor_params.h | 6 +- src/smt/params/theory_arith_params.cpp | 2 + src/smt/params/theory_arith_params.h | 4 + src/smt/params/theory_array_params.h | 8 +- src/smt/params/theory_bv_params.cpp | 6 +- src/smt/params/theory_bv_params.h | 2 + 14 files changed, 26 insertions(+), 343 deletions(-) delete mode 100644 src/ast/simplifier/maximise_ac_sharing.cpp delete mode 100644 src/ast/simplifier/maximise_ac_sharing.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3df33aac9..277335ce9 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -68,9 +68,6 @@ add_subdirectory(cmd_context) add_subdirectory(cmd_context/extra_cmds) add_subdirectory(parsers/smt2) add_subdirectory(ast/proof_checker) -## Simplifier module will be deleted in the future. -## It has been replaced with rewriter component. -add_subdirectory(ast/simplifier) add_subdirectory(ast/fpa) add_subdirectory(ast/macros) add_subdirectory(ast/pattern) diff --git a/src/ast/simplifier/CMakeLists.txt b/src/ast/simplifier/CMakeLists.txt index 649c0486e..37d96b1a5 100644 --- a/src/ast/simplifier/CMakeLists.txt +++ b/src/ast/simplifier/CMakeLists.txt @@ -2,11 +2,11 @@ z3_add_component(simplifier SOURCES arith_simplifier_params.cpp # arith_simplifier_plugin.cpp - array_simplifier_params.cpp +# array_simplifier_params.cpp # array_simplifier_plugin.cpp # basic_simplifier_plugin.cpp # bv_elim.cpp - bv_simplifier_params.cpp +# bv_simplifier_params.cpp # bv_simplifier_plugin.cpp # datatype_simplifier_plugin.cpp # elim_bounds.cpp @@ -18,8 +18,5 @@ z3_add_component(simplifier # simplifier_plugin.cpp COMPONENT_DEPENDENCIES rewriter - PYG_FILES - arith_simplifier_params_helper.pyg - array_simplifier_params_helper.pyg - bv_simplifier_params_helper.pyg + ) diff --git a/src/ast/simplifier/array_simplifier_params.h b/src/ast/simplifier/array_simplifier_params.h index 559e3de54..07ead5fd6 100644 --- a/src/ast/simplifier/array_simplifier_params.h +++ b/src/ast/simplifier/array_simplifier_params.h @@ -21,11 +21,9 @@ Revision History: #include "util/params.h" -struct array_simplifier_params { - bool m_array_canonize_simplify; - bool m_array_simplify; // temporary hack for disabling array simplifier plugin. +struct array_simplifier_params1 { - array_simplifier_params(params_ref const & p = params_ref()) { + array_simplifier_params1(params_ref const & p = params_ref()) { updt_params(p); } diff --git a/src/ast/simplifier/bv_simplifier_params.cpp b/src/ast/simplifier/bv_simplifier_params.cpp index 4c6b4a5fa..07f854179 100644 --- a/src/ast/simplifier/bv_simplifier_params.cpp +++ b/src/ast/simplifier/bv_simplifier_params.cpp @@ -33,4 +33,4 @@ void bv_simplifier_params::updt_params(params_ref const & _p) { void bv_simplifier_params::display(std::ostream & out) const { DISPLAY_PARAM(m_hi_div0); DISPLAY_PARAM(m_bv2int_distribute); -} \ No newline at end of file +} diff --git a/src/ast/simplifier/maximise_ac_sharing.cpp b/src/ast/simplifier/maximise_ac_sharing.cpp deleted file mode 100644 index 93e5a43f0..000000000 --- a/src/ast/simplifier/maximise_ac_sharing.cpp +++ /dev/null @@ -1,192 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - maximise_ac_sharing.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-10-22. - -Revision History: - ---*/ - -#include "ast/simplifier/maximise_ac_sharing.h" -#include "ast/ast_pp.h" -#include "ast/simplifier/basic_simplifier_plugin.h" - -maximise_ac_sharing::ac_plugin::ac_plugin(symbol const & fname, ast_manager & m, maximise_ac_sharing & owner): - simplifier_plugin(fname, m), - m_owner(owner) { -} - -void maximise_ac_sharing::ac_plugin::register_kind(decl_kind k) { - m_kinds.push_back(k); -} - -maximise_ac_sharing::ac_plugin::~ac_plugin() { -} - -bool maximise_ac_sharing::ac_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - decl_kind k = f->get_kind(); - if (!f->is_associative()) - return false; - if (num_args <= 2) - return false; - if (std::find(m_kinds.begin(), m_kinds.end(), k) == m_kinds.end()) - return false; - ptr_buffer _args; - expr * numeral = 0; - if (m_owner.is_numeral(args[0])) { - numeral = args[0]; - for (unsigned i = 1; i < num_args; i++) - _args.push_back(args[i]); - num_args--; - } - else { - _args.append(num_args, args); - } - - TRACE("ac_sharing_detail", tout << "before-reuse: num_args: " << num_args << "\n";); - -#define MAX_NUM_ARGS_FOR_OPT 128 - - // Try to reuse already created circuits. - TRACE("ac_sharing_detail", tout << "args: "; for (unsigned i = 0; i < num_args; i++) tout << mk_pp(_args[i], m_manager) << "\n";); - try_to_reuse: - if (num_args > 1 && num_args < MAX_NUM_ARGS_FOR_OPT) { - for (unsigned i = 0; i < num_args - 1; i++) { - for (unsigned j = i + 1; j < num_args; j++) { - if (m_owner.contains(f, _args[i], _args[j])) { - TRACE("ac_sharing_detail", tout << "reusing args: " << i << " " << j << "\n";); - _args[i] = m_manager.mk_app(f, _args[i], _args[j]); - SASSERT(num_args > 1); - for (unsigned w = j; w < num_args - 1; w++) { - _args[w] = _args[w+1]; - } - num_args--; - goto try_to_reuse; - } - } - } - } - - - // Create "tree-like circuit" - while (true) { - TRACE("ac_sharing_detail", tout << "tree-loop: num_args: " << num_args << "\n";); - unsigned j = 0; - for (unsigned i = 0; i < num_args; i += 2, j++) { - if (i == num_args - 1) { - _args[j] = _args[i]; - } - else { - m_owner.insert(f, _args[i], _args[i+1]); - _args[j] = m_manager.mk_app(f, _args[i], _args[i+1]); - } - } - num_args = j; - if (num_args == 1) { - if (numeral == 0) { - result = _args[0]; - } - else { - result = m_manager.mk_app(f, numeral, _args[0]); - } - TRACE("ac_sharing_detail", tout << "result: " << mk_pp(result, m_manager) << "\n";); - return true; - } - } - - UNREACHABLE(); - return false; -} - -bool maximise_ac_sharing::contains(func_decl * f, expr * arg1, expr * arg2) { - entry e(f, arg1, arg2); - return m_cache.contains(&e); -} - -void maximise_ac_sharing::insert(func_decl * f, expr * arg1, expr * arg2) { - entry * e = new (m_region) entry(f, arg1, arg2); - m_entries.push_back(e); - m_cache.insert(e); - m_manager.inc_ref(arg1); - m_manager.inc_ref(arg2); -} - -maximise_ac_sharing::maximise_ac_sharing(ast_manager & m): - m_manager(m), - m_simplifier(m), - m_init(false) { - basic_simplifier_plugin* basic_simp = alloc(basic_simplifier_plugin,m); - m_simplifier.register_plugin(basic_simp); -} - -maximise_ac_sharing::~maximise_ac_sharing() { - restore_entries(0); -} - -void maximise_ac_sharing::operator()(expr * s, expr_ref & r, proof_ref & p) { - init(); - m_simplifier.operator()(s, r, p); -} - -void maximise_ac_sharing::push_scope() { - init(); - m_scopes.push_back(m_entries.size()); - m_region.push_scope(); -} - -void maximise_ac_sharing::pop_scope(unsigned num_scopes) { - SASSERT(num_scopes <= m_scopes.size()); - unsigned new_lvl = m_scopes.size() - num_scopes; - unsigned old_lim = m_scopes[new_lvl]; - restore_entries(old_lim); - m_region.pop_scope(num_scopes); - m_scopes.shrink(new_lvl); -} - -void maximise_ac_sharing::restore_entries(unsigned old_lim) { - unsigned i = m_entries.size(); - while (i != old_lim) { - --i; - entry * e = m_entries[i]; - m_manager.dec_ref(e->m_arg1); - m_manager.dec_ref(e->m_arg2); - } - m_entries.shrink(old_lim); -} - -void maximise_ac_sharing::reset() { - restore_entries(0); - m_entries.reset(); - m_cache.reset(); - m_simplifier.reset(); - m_region.reset(); - m_scopes.reset(); -} - -void maximise_bv_sharing::init_core() { - maximise_ac_sharing::ac_plugin * p = alloc(maximise_ac_sharing::ac_plugin, symbol("bv"), get_manager(), *this); - p->register_kind(OP_BADD); - p->register_kind(OP_BMUL); - p->register_kind(OP_BOR); - p->register_kind(OP_BAND); - register_plugin(p); -} - -bool maximise_bv_sharing::is_numeral(expr * n) const { - return m_util.is_numeral(n); -} - -maximise_bv_sharing::maximise_bv_sharing(ast_manager & m): - maximise_ac_sharing(m), - m_util(m) { -} diff --git a/src/ast/simplifier/maximise_ac_sharing.h b/src/ast/simplifier/maximise_ac_sharing.h deleted file mode 100644 index cf488e20d..000000000 --- a/src/ast/simplifier/maximise_ac_sharing.h +++ /dev/null @@ -1,124 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - maximise_ac_sharing.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-10-22. - -Revision History: - ---*/ -#ifndef MAXIMISE_AC_SHARING_H_ -#define MAXIMISE_AC_SHARING_H_ - -#include "ast/simplifier/simplifier.h" -#include "util/hashtable.h" -#include "ast/bv_decl_plugin.h" -#include "util/region.h" - -/** - \brief Functor used to maximise the amount of shared terms in an expression. - The idea is to rewrite AC terms to maximise sharing. - Example: - - (f (bvadd a (bvadd b c)) (bvadd a (bvadd b d))) - - is rewritten to: - - (f (bvadd (bvadd a b) c) (bvadd (bvadd a b) d)) - - \warning This class uses an opportunistic heuristic to maximise sharing. - There is no guarantee that the optimal expression will be produced. -*/ -class maximise_ac_sharing { - - struct entry { - func_decl * m_decl; - expr * m_arg1; - expr * m_arg2; - - entry(func_decl * d = 0, expr * arg1 = 0, expr * arg2 = 0):m_decl(d), m_arg1(arg1), m_arg2(arg2) { - SASSERT((d == 0 && arg1 == 0 && arg2 == 0) || (d != 0 && arg1 != 0 && arg2 != 0)); - if (arg1->get_id() > arg2->get_id()) - std::swap(m_arg1, m_arg2); - } - - unsigned hash() const { - unsigned a = m_decl->get_id(); - unsigned b = m_arg1->get_id(); - unsigned c = m_arg2->get_id(); - mix(a,b,c); - return c; - } - - bool operator==(entry const & e) const { - return m_decl == e.m_decl && m_arg1 == e.m_arg1 && m_arg2 == e.m_arg2; - } - }; - - typedef ptr_hashtable, deref_eq > cache; - -protected: - class ac_plugin : public simplifier_plugin { - maximise_ac_sharing & m_owner; - svector m_kinds; //!< kinds to be processed - public: - ac_plugin(symbol const & fname, ast_manager & m, maximise_ac_sharing & owner); - void register_kind(decl_kind k); - virtual ~ac_plugin(); - virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); - }; - - friend class ac_plugin; - -private: - ast_manager & m_manager; - simplifier m_simplifier; - bool m_init; - region m_region; - cache m_cache; - ptr_vector m_entries; - unsigned_vector m_scopes; - - bool contains(func_decl * f, expr * arg1, expr * arg2); - void insert(func_decl * f, expr * arg1, expr * arg2); - void restore_entries(unsigned old_lim); - void init() { - if (!m_init) { - init_core(); - m_init = true; - } - } -protected: - virtual void init_core() = 0; - virtual bool is_numeral(expr * n) const = 0; - void register_plugin(ac_plugin * p) { m_simplifier.register_plugin(p); } -public: - maximise_ac_sharing(ast_manager & m); - virtual ~maximise_ac_sharing(); - void operator()(expr * s, expr_ref & r, proof_ref & p); - void push_scope(); - void pop_scope(unsigned num_scopes); - void reset(); - ast_manager & get_manager() { return m_manager; } -}; - -class maximise_bv_sharing : public maximise_ac_sharing { - bv_util m_util; -protected: - virtual void init_core(); - virtual bool is_numeral(expr * n) const; -public: - maximise_bv_sharing(ast_manager & m); -}; - -#endif /* MAXIMISE_AC_SHARING_H_ */ - diff --git a/src/smt/params/CMakeLists.txt b/src/smt/params/CMakeLists.txt index 500423dcc..c965f0a62 100644 --- a/src/smt/params/CMakeLists.txt +++ b/src/smt/params/CMakeLists.txt @@ -13,7 +13,6 @@ z3_add_component(smt_params ast bit_blaster pattern - simplifier PYG_FILES smt_params_helper.pyg ) diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp index afca0196a..93ea794fa 100644 --- a/src/smt/params/preprocessor_params.cpp +++ b/src/smt/params/preprocessor_params.cpp @@ -30,8 +30,6 @@ void preprocessor_params::updt_local_params(params_ref const & _p) { void preprocessor_params::updt_params(params_ref const & p) { pattern_inference_params::updt_params(p); - bv_simplifier_params::updt_params(p); - arith_simplifier_params::updt_params(p); updt_local_params(p); } @@ -40,8 +38,6 @@ void preprocessor_params::updt_params(params_ref const & p) { void preprocessor_params::display(std::ostream & out) const { pattern_inference_params::display(out); bit_blaster_params::display(out); - bv_simplifier_params::display(out); - arith_simplifier_params::display(out); DISPLAY_PARAM(m_lift_ite); DISPLAY_PARAM(m_ng_lift_ite); diff --git a/src/smt/params/preprocessor_params.h b/src/smt/params/preprocessor_params.h index 6f763c0e1..dc16d6244 100644 --- a/src/smt/params/preprocessor_params.h +++ b/src/smt/params/preprocessor_params.h @@ -21,8 +21,6 @@ Revision History: #include "ast/pattern/pattern_inference_params.h" #include "ast/rewriter/bit_blaster/bit_blaster_params.h" -#include "ast/simplifier/bv_simplifier_params.h" -#include "ast/simplifier/arith_simplifier_params.h" enum lift_ite_kind { LI_NONE, @@ -31,9 +29,7 @@ enum lift_ite_kind { }; struct preprocessor_params : public pattern_inference_params, - public bit_blaster_params, - public bv_simplifier_params, - public arith_simplifier_params { + public bit_blaster_params { lift_ite_kind m_lift_ite; lift_ite_kind m_ng_lift_ite; // lift ite for non ground terms bool m_pull_cheap_ite_trees; diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index 2b5a14493..ab80f0c67 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -42,6 +42,8 @@ void theory_arith_params::updt_params(params_ref const & _p) { #define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; void theory_arith_params::display(std::ostream & out) const { + DISPLAY_PARAM(m_arith_expand_eqs); + DISPLAY_PARAM(m_arith_process_all_eqs); DISPLAY_PARAM(m_arith_mode); DISPLAY_PARAM(m_arith_auto_config_simplex); //!< force simplex solver in auto_config DISPLAY_PARAM(m_arith_blands_rule_threshold); diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index d73a67985..89c4fe46c 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -49,6 +49,8 @@ enum arith_pivot_strategy { }; struct theory_arith_params { + bool m_arith_expand_eqs; + bool m_arith_process_all_eqs; arith_solver_id m_arith_mode; bool m_arith_auto_config_simplex; //!< force simplex solver in auto_config unsigned m_arith_blands_rule_threshold; @@ -108,6 +110,8 @@ struct theory_arith_params { theory_arith_params(params_ref const & p = params_ref()): + m_arith_expand_eqs(false), + m_arith_process_all_eqs(false), m_arith_mode(AS_ARITH), m_arith_auto_config_simplex(false), m_arith_blands_rule_threshold(1000), diff --git a/src/smt/params/theory_array_params.h b/src/smt/params/theory_array_params.h index af3fdebeb..edda4d7cf 100644 --- a/src/smt/params/theory_array_params.h +++ b/src/smt/params/theory_array_params.h @@ -19,7 +19,7 @@ Revision History: #ifndef THEORY_ARRAY_PARAMS_H_ #define THEORY_ARRAY_PARAMS_H_ -#include "ast/simplifier/array_simplifier_params.h" +#include "util/params.h" enum array_solver_id { AR_NO_ARRAY, @@ -28,7 +28,9 @@ enum array_solver_id { AR_FULL }; -struct theory_array_params : public array_simplifier_params { +struct theory_array_params { + bool m_array_canonize_simplify; + bool m_array_simplify; // temporary hack for disabling array simplifier plugin. array_solver_id m_array_mode; bool m_array_weak; bool m_array_extensional; @@ -40,6 +42,8 @@ struct theory_array_params : public array_simplifier_params { unsigned m_array_lazy_ieq_delay; theory_array_params(): + m_array_canonize_simplify(false), + m_array_simplify(true), m_array_mode(AR_FULL), m_array_weak(false), m_array_extensional(true), diff --git a/src/smt/params/theory_bv_params.cpp b/src/smt/params/theory_bv_params.cpp index 4b4808a1f..156fda592 100644 --- a/src/smt/params/theory_bv_params.cpp +++ b/src/smt/params/theory_bv_params.cpp @@ -18,9 +18,12 @@ Revision History: --*/ #include "smt/params/theory_bv_params.h" #include "smt/params/smt_params_helper.hpp" +#include "ast/rewriter/bv_rewriter_params.hpp" void theory_bv_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); + bv_rewriter_params rp(_p); + m_hi_div0 = rp.hi_div0(); m_bv_reflect = p.bv_reflect(); m_bv_enable_int2bv2int = p.bv_enable_int2bv(); } @@ -29,9 +32,10 @@ void theory_bv_params::updt_params(params_ref const & _p) { void theory_bv_params::display(std::ostream & out) const { DISPLAY_PARAM(m_bv_mode); + DISPLAY_PARAM(m_hi_div0); DISPLAY_PARAM(m_bv_reflect); DISPLAY_PARAM(m_bv_lazy_le); DISPLAY_PARAM(m_bv_cc); DISPLAY_PARAM(m_bv_blast_max_size); DISPLAY_PARAM(m_bv_enable_int2bv2int); -} \ No newline at end of file +} diff --git a/src/smt/params/theory_bv_params.h b/src/smt/params/theory_bv_params.h index 52aaa4c9c..e0bff3f17 100644 --- a/src/smt/params/theory_bv_params.h +++ b/src/smt/params/theory_bv_params.h @@ -28,6 +28,7 @@ enum bv_solver_id { struct theory_bv_params { bv_solver_id m_bv_mode; + bool m_hi_div0; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted. bool m_bv_reflect; bool m_bv_lazy_le; bool m_bv_cc; @@ -35,6 +36,7 @@ struct theory_bv_params { bool m_bv_enable_int2bv2int; theory_bv_params(params_ref const & p = params_ref()): m_bv_mode(BS_BLASTER), + m_hi_div0(false), m_bv_reflect(true), m_bv_lazy_le(false), m_bv_cc(false),