move mk_fresh to inside files that include smt_context.h directly to address build problem reported in #297

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/theory_array_full.cpp

@@ -35,6 +35,10 @@ namespace smt {
         m_var_data_full.reset();
     }
 
+    theory* theory_array_full::mk_fresh(context* new_ctx) { 
+        return alloc(theory_array_full, new_ctx->get_manager(), m_params); 
+    }
+
     void theory_array_full::add_map(theory_var v, enode* s) {
         if (m_params.m_array_cg && !s->is_cgr()) {
             return;

src/smt/theory_array_full.h

@@ -91,7 +91,7 @@ namespace smt {
         theory_array_full(ast_manager & m, theory_array_params & params);
         virtual ~theory_array_full();
 
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array_full, new_ctx->get_manager(), m_params); }
+        virtual theory * mk_fresh(context * new_ctx);
 
         virtual void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var);
         virtual void display_var(std::ostream & out, theory_var v) const;

src/smt/theory_datatype.cpp

@@ -36,6 +36,11 @@ namespace smt {
         virtual theory_id get_from_theory() const { return null_theory_id; } 
     };
 
+
+    theory* theory_datatype::mk_fresh(context* new_ctx) { 
+        return alloc(theory_datatype, new_ctx->get_manager(), m_params); 
+    }
+
     /**
        \brief Assert the axiom (antecedent => lhs = rhs)
        antecedent may be null_literal

src/smt/theory_datatype.h

@@ -101,7 +101,7 @@ namespace smt {
     public:
         theory_datatype(ast_manager & m, theory_datatype_params & p);
         virtual ~theory_datatype();
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_datatype, new_ctx->get_manager(), m_params); }
+        virtual theory * mk_fresh(context * new_ctx);
         virtual void display(std::ostream & out) const;
         virtual void collect_statistics(::statistics & st) const;        
         virtual void init_model(model_generator & m);

src/smt/theory_dense_diff_logic.h

@@ -282,7 +282,7 @@ namespace smt {
         theory_dense_diff_logic(ast_manager & m, theory_arith_params & p);
         virtual ~theory_dense_diff_logic() { reset_eh(); }
         
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_dense_diff_logic, new_ctx->get_manager(), m_params); }
+        virtual theory * mk_fresh(context * new_ctx);
 
         virtual char const * get_name() const { return "difference-logic"; }
 

src/smt/theory_dense_diff_logic_def.h

@@ -39,6 +39,11 @@ namespace smt {
         m_edges.push_back(edge());
     }
 
+    template<typename Ext>
+    theory* theory_dense_diff_logic<Ext>::mk_fresh(context * new_ctx) { 
+        return alloc(theory_dense_diff_logic<Ext>, new_ctx->get_manager(), m_params); 
+    }
+
     template<typename Ext>
     inline app * theory_dense_diff_logic<Ext>::mk_zero_for(expr * n) {
         return m_autil.mk_numeral(rational(0), get_manager().get_sort(n));

src/smt/theory_diff_logic.h

@@ -243,7 +243,7 @@ namespace smt {
             reset_eh();
         }
 
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_diff_logic, new_ctx->get_manager(), m_params); }
+        virtual theory * mk_fresh(context * new_ctx);
 
         virtual char const * get_name() const { return "difference-logic"; }
 

src/smt/theory_diff_logic_def.h

@@ -1384,5 +1384,11 @@ bool theory_diff_logic<Ext>::internalize_objective(expr * n, rational const& m,
     return true;
 }
 
+template<typename Ext>
+theory* theory_diff_logic<Ext>::mk_fresh(context* new_ctx) {
+    return alloc(theory_diff_logic<Ext>, new_ctx->get_manager(), m_params); 
+}
+
+
 #endif /* THEORY_DIFF_LOGIC_DEF_H_ */
 

src/smt/theory_fpa.cpp

@@ -716,6 +716,10 @@ namespace smt {
         return;
     }
 
+    theory* theory_fpa::mk_fresh(context* new_ctx) { 
+        return alloc(theory_fpa, new_ctx->get_manager()); 
+    }
+
     void theory_fpa::push_scope_eh() {
         theory::push_scope_eh();
         m_trail_stack.push_scope();

src/smt/theory_fpa.h

@@ -158,7 +158,7 @@ namespace smt {
         virtual void push_scope_eh();
         virtual void pop_scope_eh(unsigned num_scopes);
         virtual void reset_eh();
-        virtual theory* mk_fresh(context* new_ctx) { return alloc(theory_fpa, new_ctx->get_manager()); }
+        virtual theory* mk_fresh(context* new_ctx);
         virtual char const * get_name() const { return "fpa"; }
 
         virtual model_value_proc * mk_value(enode * n, model_generator & mg);

src/smt/theory_utvpi.h

@@ -183,7 +183,7 @@ namespace smt {
 
         virtual ~theory_utvpi();
 
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_utvpi, new_ctx->get_manager()); }
+        virtual theory * mk_fresh(context * new_ctx);
 
         virtual char const * get_name() const { return "utvpi-logic"; }
 

src/smt/theory_utvpi_def.h

@@ -942,6 +942,10 @@ namespace smt {
         }
     }
 
+    template<typename Ext>
+    theory* theory_utvpi<Ext>::mk_fresh(context* new_ctx) { 
+        return alloc(theory_utvpi<Ext>, new_ctx->get_manager()); 
+    }
 
 
 };