From c9722a1313489bd355102ec242b39b904435946f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Nov 2012 12:21:14 -0700 Subject: [PATCH] removing dead code Signed-off-by: Leonardo de Moura --- src/smt/asserted_formulas.cpp | 5 --- src/smt/asserted_formulas.h | 5 --- src/smt/smt_context.h | 6 ---- src/smt/user_rewriter.cpp | 24 --------------- src/smt/user_rewriter.h | 58 ----------------------------------- 5 files changed, 98 deletions(-) delete mode 100644 src/smt/user_rewriter.cpp delete mode 100644 src/smt/user_rewriter.h diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 368889cdc..4a6cfd85d 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -60,7 +60,6 @@ asserted_formulas::asserted_formulas(ast_manager & m, front_end_params & p): m_macro_manager(m, m_simplifier), m_bit2int(m), m_bv_sharing(m), - m_user_rewriter(m), m_inconsistent(false), m_cancel_flag(false) { @@ -282,7 +281,6 @@ void asserted_formulas::reset() { } void asserted_formulas::set_cancel_flag(bool f) { - m_user_rewriter.set_cancel(f); m_cancel_flag = f; } @@ -341,7 +339,6 @@ void asserted_formulas::reduce() { TRACE("qbv_bug", tout << "after demod:\n"; display(tout);); INVOKE(m_params.m_quasi_macros && has_quantifiers(), apply_quasi_macros()); INVOKE(m_params.m_simplify_bit2int, apply_bit2int()); - INVOKE(m_user_rewriter.enabled(), apply_user_rewriter()); INVOKE(m_params.m_eliminate_bounds && has_quantifiers(), cheap_quant_fourier_motzkin()); INVOKE(!m_params.m_bb_eager && has_quantifiers() && m_params.m_ematching, infer_patterns()); INVOKE(m_params.m_max_bv_sharing && has_bv(), max_bv_sharing()); @@ -1414,8 +1411,6 @@ void asserted_formulas::refine_inj_axiom() { MK_SIMPLIFIER(apply_bit2int, bit2int& functor = m_bit2int, "bit2int", "propagate bit-vector over integers", true); -MK_SIMPLIFIER(apply_user_rewriter, user_rewriter& functor = m_user_rewriter, "user_rewriter", "apply user supplied rewriting", true); - MK_SIMPLIFIER(apply_der_core, der_star functor(m_manager), "der", "destructive equality resolution", true); void asserted_formulas::apply_der() { diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index b08ac90d3..94bb41682 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -30,7 +30,6 @@ Revision History: #include"maximise_ac_sharing.h" #include"bit2int.h" #include"statistics.h" -#include"user_rewriter.h" #include"pattern_inference.h" class arith_simplifier_plugin; @@ -66,8 +65,6 @@ class asserted_formulas { maximise_bv_sharing m_bv_sharing; - user_rewriter m_user_rewriter; - bool m_inconsistent; // qe::expr_quant_elim_star1 m_quant_elim; @@ -98,7 +95,6 @@ class asserted_formulas { void apply_quasi_macros(); void nnf_cnf(); bool apply_eager_bit_blaster(); - bool apply_user_rewriter(); void infer_patterns(); void eliminate_term_ite(); void reduce_and_solve(); @@ -157,7 +153,6 @@ public: void init(unsigned num_formulas, expr * const * formulas, proof * const * prs); void register_simplifier_plugin(simplifier_plugin * p) { m_simplifier.register_plugin(p); } simplifier & get_simplifier() { return m_simplifier; } - void set_user_rewriter(void* ctx, user_rewriter::fn* rw) { m_user_rewriter.set_rewriter(ctx, rw); } void get_assertions(ptr_vector & result); bool empty() const { return m_asserted_formulas.empty(); } void collect_static_features(); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 095bcff92..6137917f0 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -523,12 +523,6 @@ namespace smt { friend class set_var_theory_trail; void set_var_theory(bool_var v, theory_id tid); - /** - \brief set user-supplied rewriter. - */ - - void set_user_rewriter(void* ctx, user_rewriter::fn* rw) { m_asserted_formulas.set_user_rewriter(ctx, rw); } - // ----------------------------------- // // Backtracking support diff --git a/src/smt/user_rewriter.cpp b/src/smt/user_rewriter.cpp deleted file mode 100644 index 94c6c3858..000000000 --- a/src/smt/user_rewriter.cpp +++ /dev/null @@ -1,24 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - user_rewriter.cpp - -Abstract: - - Rewriter for applying user-defined rewrite routine. - -Author: - - Nikolaj (nbjorner) 2012-01-08 - -Notes: - ---*/ - -#include "rewriter_def.h" -#include "user_rewriter.h" - - -template class rewriter_tpl; diff --git a/src/smt/user_rewriter.h b/src/smt/user_rewriter.h deleted file mode 100644 index 870425f89..000000000 --- a/src/smt/user_rewriter.h +++ /dev/null @@ -1,58 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - user_rewriter.h - -Abstract: - - Rewriter for applying user-defined rewrite routine. - -Author: - - Nikolaj (nbjorner) 2012-01-08 - -Notes: - ---*/ -#ifndef _USER_REWRITER_H_ -#define _USER_REWRITER_H_ - -#include "ast.h" -#include "rewriter.h" - - -class user_rewriter : public default_rewriter_cfg { -public: - typedef bool fn(void* context, expr* expr_in, expr** expr_out, proof** proof_out); -private: - ast_manager& m; - rewriter_tpl m_rw; - void* m_ctx; - fn* m_rewriter; - bool m_rec; - -public: - user_rewriter(ast_manager & m): m(m), m_rw(m, m.proofs_enabled(), *this), m_rewriter(0), m_rec(false) {} - ~user_rewriter() {} - - void set_rewriter(void * ctx, fn* rw) { m_ctx = ctx; m_rewriter = rw; } - bool enabled() { return m_rewriter != 0; } - - void operator()(expr_ref& term) { expr_ref tmp(m); (*this)(tmp, term); } - void operator()(expr * t, expr_ref & result) { proof_ref pr(m); (*this)(t, result, pr); } - void operator()(expr * t, expr_ref & result, proof_ref & result_pr) { m_rw(t, result, result_pr); } - - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } - void set_cancel(bool f) { m_rw.set_cancel(f); } - void cleanup() { if (!m_rec) { m_rec = true; m_rw.cleanup(); m_rec = false; } } - void reset() { if (!m_rec) { m_rec = true; m_rw.reset(); m_rec = false; } } - - bool get_subst(expr* s, expr*& t, proof*& t_pr) { - return enabled() && m_rewriter(m_ctx, s, &t, &t_pr); - } -}; - -#endif