From f062e170373b1e1c3e7344b0b2a6c0bf93c14097 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Aug 2017 12:30:33 -0700 Subject: [PATCH] remove simplifier dependencies from ufbv tactics Signed-off-by: Nikolaj Bjorner --- src/tactic/ufbv/macro_finder_tactic.cpp | 16 ---------------- src/tactic/ufbv/quasi_macros_tactic.cpp | 17 +---------------- src/tactic/ufbv/ufbv_rewriter.cpp | 13 ++++++++----- src/tactic/ufbv/ufbv_rewriter.h | 6 +++--- src/tactic/ufbv/ufbv_rewriter_tactic.cpp | 6 +----- 5 files changed, 13 insertions(+), 45 deletions(-) diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index b3f258ba7..3832339a8 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -17,10 +17,6 @@ Notes: --*/ #include "tactic/tactical.h" -#include "ast/simplifier/simplifier.h" -#include "ast/simplifier/basic_simplifier_plugin.h" -#include "ast/simplifier/arith_simplifier_plugin.h" -#include "ast/simplifier/bv_simplifier_plugin.h" #include "ast/macros/macro_manager.h" #include "ast/macros/macro_finder.h" #include "tactic/extension_model_converter.h" @@ -52,18 +48,6 @@ class macro_finder_tactic : public tactic { fail_if_unsat_core_generation("macro-finder", g); bool produce_proofs = g->proofs_enabled(); - - simplifier simp(m_manager); - basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager); - bsimp->set_eliminate_and(m_elim_and); - simp.register_plugin(bsimp); - arith_simplifier_params a_params; - arith_simplifier_plugin * asimp = alloc(arith_simplifier_plugin, m_manager, *bsimp, a_params); - simp.register_plugin(asimp); - bv_simplifier_params bv_params; - bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, bv_params); - simp.register_plugin(bvsimp); - macro_manager mm(m_manager); macro_finder mf(m_manager, mm); diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index 8a91bde61..8196dc664 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -17,10 +17,6 @@ Notes: --*/ #include "tactic/tactical.h" -#include "ast/simplifier/simplifier.h" -#include "ast/simplifier/basic_simplifier_plugin.h" -#include "ast/simplifier/arith_simplifier_plugin.h" -#include "ast/simplifier/bv_simplifier_plugin.h" #include "ast/macros/macro_manager.h" #include "ast/macros/macro_finder.h" #include "tactic/extension_model_converter.h" @@ -50,18 +46,7 @@ class quasi_macros_tactic : public tactic { fail_if_unsat_core_generation("quasi-macros", g); bool produce_proofs = g->proofs_enabled(); - - simplifier simp(m_manager); - basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager); - bsimp->set_eliminate_and(true); - simp.register_plugin(bsimp); - arith_simplifier_params a_params; - arith_simplifier_plugin * asimp = alloc(arith_simplifier_plugin, m_manager, *bsimp, a_params); - simp.register_plugin(asimp); - bv_simplifier_params bv_params; - bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, bv_params); - simp.register_plugin(bvsimp); - + macro_manager mm(m_manager); quasi_macros qm(m_manager, mm); bool more = true; diff --git a/src/tactic/ufbv/ufbv_rewriter.cpp b/src/tactic/ufbv/ufbv_rewriter.cpp index 4f0f5e548..446d1a49c 100644 --- a/src/tactic/ufbv/ufbv_rewriter.cpp +++ b/src/tactic/ufbv/ufbv_rewriter.cpp @@ -20,20 +20,23 @@ Revision History: --*/ +#include "util/uint_set.h" #include "ast/ast_pp.h" -#include "tactic/ufbv/ufbv_rewriter.h" #include "ast/for_each_expr.h" #include "ast/rewriter/var_subst.h" -#include "util/uint_set.h" +#include "tactic/ufbv/ufbv_rewriter.h" -ufbv_rewriter::ufbv_rewriter(ast_manager & m, basic_simplifier_plugin & p): +ufbv_rewriter::ufbv_rewriter(ast_manager & m): m_manager(m), m_match_subst(m), - m_bsimp(p), + m_bsimp(m), m_todo(m), m_rewrite_todo(m), m_rewrite_cache(m), m_new_exprs(m) { + params_ref p; + p.set_bool("elim_and", true); + m_bsimp.updt_params(p); } ufbv_rewriter::~ufbv_rewriter() { @@ -396,7 +399,7 @@ expr * ufbv_rewriter::rewrite(expr * n) { if (f->get_family_id() != m_manager.get_basic_family_id()) na = m_manager.mk_app(f, m_new_args.size(), m_new_args.c_ptr()); else - m_bsimp.reduce(f, m_new_args.size(), m_new_args.c_ptr(), na); + m_bsimp.mk_app(f, m_new_args.size(), m_new_args.c_ptr(), na); TRACE("demodulator_bug", tout << "e:\n" << mk_pp(e, m_manager) << "\nnew_args: \n"; for (unsigned i = 0; i < m_new_args.size(); i++) { tout << mk_pp(m_new_args[i], m_manager) << "\n"; } tout << "=====>\n"; diff --git a/src/tactic/ufbv/ufbv_rewriter.h b/src/tactic/ufbv/ufbv_rewriter.h index d11453836..1e13f4fa4 100644 --- a/src/tactic/ufbv/ufbv_rewriter.h +++ b/src/tactic/ufbv/ufbv_rewriter.h @@ -23,10 +23,10 @@ Revision History: #include "ast/ast.h" #include "ast/substitution/substitution.h" +#include "ast/rewriter/bool_rewriter.h" #include "util/obj_hashtable.h" #include "util/obj_pair_hashtable.h" #include "util/array_map.h" -#include "ast/simplifier/basic_simplifier_plugin.h" /** \brief Apply demodulators as a preprocessing technique. @@ -159,7 +159,7 @@ class ufbv_rewriter { ast_manager & m_manager; match_subst m_match_subst; - basic_simplifier_plugin & m_bsimp; + bool_rewriter m_bsimp; fwd_idx_map m_fwd_idx; back_idx_map m_back_idx; demodulator2lhs_rhs m_demodulator2lhs_rhs; @@ -194,7 +194,7 @@ protected: virtual int is_subset(expr * e1, expr * e2) const; public: - ufbv_rewriter(ast_manager & m, basic_simplifier_plugin & p); + ufbv_rewriter(ast_manager & m); virtual ~ufbv_rewriter(); void operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp index b4bfabf65..615593317 100644 --- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp +++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp @@ -17,8 +17,6 @@ Notes: --*/ #include "tactic/tactical.h" -#include "ast/simplifier/simplifier.h" -#include "ast/simplifier/basic_simplifier_plugin.h" #include "tactic/ufbv/ufbv_rewriter.h" #include "tactic/ufbv/ufbv_rewriter_tactic.h" @@ -45,9 +43,7 @@ class ufbv_rewriter_tactic : public tactic { bool produce_proofs = g->proofs_enabled(); - basic_simplifier_plugin bsimp(m_manager); - bsimp.set_eliminate_and(true); - ufbv_rewriter dem(m_manager, bsimp); + ufbv_rewriter dem(m_manager); expr_ref_vector forms(m_manager), new_forms(m_manager); proof_ref_vector proofs(m_manager), new_proofs(m_manager);