From f59cf2452d9a335785bd1691dbf04b93973193d1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 5 Oct 2017 22:20:31 +0100
Subject: [PATCH] #1284 build problems

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/core/CMakeLists.txt          |  2 +
 src/tactic/core/dom_simplify_tactic.cpp |  1 +
 src/tactic/core/dom_simplify_tactic.h   | 53 +++++++++++++------------
 3 files changed, 31 insertions(+), 25 deletions(-)

diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt
index f192b4fa6..16778d8dd 100644
--- a/src/tactic/core/CMakeLists.txt
+++ b/src/tactic/core/CMakeLists.txt
@@ -7,6 +7,7 @@ z3_add_component(core_tactics
     ctx_simplify_tactic.cpp
     der_tactic.cpp
     distribute_forall_tactic.cpp
+    dom_simplify_tactic.cpp
     elim_term_ite_tactic.cpp
     elim_uncnstr_tactic.cpp
     injectivity_tactic.cpp
@@ -32,6 +33,7 @@ z3_add_component(core_tactics
     ctx_simplify_tactic.h
     der_tactic.h
     distribute_forall_tactic.h
+    dom_simplify_tactic.h
     elim_term_ite_tactic.h
     elim_uncnstr_tactic.h
     injectivity_tactic.h
diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index 85b7fd9d6..bba27cf46 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -188,6 +188,7 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
                 simplify(child);
             }
         }
+
         pop(scope_level() - old_lvl);
         expr_ref new_t = simplify(t);
         if (!assert_expr(new_c, true)) {
diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h
index 9fe59de23..825a173bf 100644
--- a/src/tactic/core/dom_simplify_tactic.h
+++ b/src/tactic/core/dom_simplify_tactic.h
@@ -58,32 +58,35 @@ public:
     
 };
 
+class dom_simplifier {
+ public:
+    dom_simplifier() {}
+    
+    virtual ~dom_simplifier() {}
+    /**
+       \brief assert_expr performs an implicit push
+    */
+    virtual bool assert_expr(expr * t, bool sign) = 0;
+    
+    /**
+       \brief apply simplification.
+    */
+    virtual void operator()(expr_ref& r) = 0;
+    
+    /**
+       \brief pop scopes accumulated from assertions.
+    */
+    virtual void pop(unsigned num_scopes) = 0;
+    
+    virtual dom_simplifier * translate(ast_manager & m) = 0;
+    
+};
+
 class dom_simplify_tactic : public tactic {
 public:
-    class simplifier {
-    public:
-        virtual ~simplifier() {}
-        /**
-           \brief assert_expr performs an implicit push
-         */
-        virtual bool assert_expr(expr * t, bool sign) = 0;
-
-        /**
-           \brief apply simplification.
-        */
-        virtual void operator()(expr_ref& r) = 0;
-
-        /**
-           \brief pop scopes accumulated from assertions.
-         */
-        virtual void pop(unsigned num_scopes) = 0;
-
-        virtual simplifier * translate(ast_manager & m);
-
-    };
 private:
     ast_manager&         m;
-    simplifier*          m_simplifier;
+    dom_simplifier*      m_simplifier;
     params_ref           m_params;
     expr_ref_vector      m_trail, m_args, m_args2;
     obj_map<expr, expr*> m_result;
@@ -115,7 +118,7 @@ private:
     void init(goal& g);
 
 public:
-    dom_simplify_tactic(ast_manager & m, simplifier* s, params_ref const & p = params_ref()):
+    dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()):
         m(m), m_simplifier(s), m_params(p), 
         m_trail(m), m_args(m), m_args2(m), 
         m_dominators(m), 
@@ -138,7 +141,7 @@ public:
     virtual void cleanup();
 };
 
-class expr_substitution_simplifier : public dom_simplify_tactic::simplifier {
+class expr_substitution_simplifier : public dom_simplifier {
     ast_manager&             m;
     expr_substitution        m_subst;
     scoped_expr_substitution m_scoped_substitution;
@@ -160,7 +163,7 @@ public:
     
     virtual void pop(unsigned num_scopes) { m_scoped_substitution.pop(num_scopes); }
     
-    virtual simplifier * translate(ast_manager & m) {
+    virtual dom_simplifier * translate(ast_manager & m) {
         SASSERT(m_subst.empty());
         return alloc(expr_substitution_simplifier, m);
     }