From 5f0ea74e89e686a07240fb370ec56b301424a2ca Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 28 Jan 2016 11:14:01 +0000
Subject: [PATCH] Made ufbv-rewriter tactic public

---
 src/tactic/ufbv/ufbv_rewriter_tactic.cpp | 16 ++++++++--------
 src/tactic/ufbv/ufbv_rewriter_tactic.h   |  4 ++++
 2 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
index 5bcf5eae3..37ad9c73c 100644
--- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
+++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
@@ -75,7 +75,7 @@ class ufbv_rewriter_tactic : public tactic {
         void updt_params(params_ref const & p) {
         }
     };
-    
+
     imp *      m_imp;
     params_ref m_params;
 
@@ -88,7 +88,7 @@ public:
     virtual tactic * translate(ast_manager & m) {
         return alloc(ufbv_rewriter_tactic, m, m_params);
     }
-        
+
     virtual ~ufbv_rewriter_tactic() {
         dealloc(m_imp);
     }
@@ -103,19 +103,19 @@ public:
         insert_produce_models(r);
         insert_produce_proofs(r);
     }
-    
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            model_converter_ref & mc, 
+
+    virtual void operator()(goal_ref const & in,
+                            goal_ref_buffer & result,
+                            model_converter_ref & mc,
                             proof_converter_ref & pc,
                             expr_dependency_ref & core) {
         (*m_imp)(in, result, mc, pc, core);
     }
-    
+
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
         imp * d = alloc(imp, m, m_params);
-        std::swap(d, m_imp);        
+        std::swap(d, m_imp);
         dealloc(d);
     }
 
diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.h b/src/tactic/ufbv/ufbv_rewriter_tactic.h
index 85cffee54..78e34bae2 100644
--- a/src/tactic/ufbv/ufbv_rewriter_tactic.h
+++ b/src/tactic/ufbv/ufbv_rewriter_tactic.h
@@ -25,4 +25,8 @@ class tactic;
 
 tactic * mk_ufbv_rewriter_tactic(ast_manager & m, params_ref const & p = params_ref());
 
+/*
+  ADD_TACTIC("ufbv-rewriter",  "Applies UFBV-specific rewriting rules, mainly demodulation.", "mk_quasi_macros_tactic(m, p)")
+*/
+
 #endif