removing dead code

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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() {

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<expr> & result);
     bool empty() const { return m_asserted_formulas.empty(); }
     void collect_static_features();

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

src/smt/user_rewriter.cpp

@@ -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<user_rewriter>;

src/smt/user_rewriter.h

@@ -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<user_rewriter>     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