remove template dependency for trail objects

src/math/lp/emonics.h

@@ -82,7 +82,7 @@ class emonics {
     };
     
     union_find<emonics>          m_u_f;
-    trail_stack<emonics>         m_u_f_stack;
+    trail_stack                  m_u_f_stack;
     mutable svector<lpvar>       m_find_key; // the key used when looking for a monic with the specific variables
     var_eqs<emonics>&            m_ve;
     mutable vector<monic>        m_monics;     // set of monics
@@ -124,7 +124,7 @@ public:
     */
     emonics(var_eqs<emonics>& ve):
         m_u_f(*this),
-        m_u_f_stack(*this),
+        m_u_f_stack(),
         m_ve(ve), 
         m_visited(0), 
         m_cg_hash(*this),
@@ -141,7 +141,7 @@ public:
     void after_merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {}
 
     // this method is required by union_find
-    trail_stack<emonics> & get_trail_stack() { return m_u_f_stack; }
+    trail_stack & get_trail_stack() { return m_u_f_stack; }
 
     /**
        \brief push/pop scopes. 

src/math/lp/var_eqs.h

@@ -72,7 +72,7 @@ class var_eqs {
 	                                  m_trail;
     vector<svector<eq_edge>>          m_eqs;    // signed_var.index() -> the edges adjacent to signed_var.index()
 
-    trail_stack<var_eqs>              m_stack;
+    trail_stack                       m_stack;
     mutable svector<var_frame>        m_todo;
     mutable bool_vector             m_marked;
     mutable unsigned_vector           m_marked_trail;
@@ -80,7 +80,7 @@ class var_eqs {
         
     mutable stats m_stats;
 public:    
-    var_eqs(): m_merge_handler(nullptr), m_uf(*this), m_stack(*this) {}    
+    var_eqs(): m_merge_handler(nullptr), m_uf(*this), m_stack() {}    
     /**
        \brief push a scope    */
     void push() {
@@ -328,7 +328,7 @@ public:
     // union find event handlers
     void set_merge_handler(T* mh) { m_merge_handler = mh; }
     // this method is required by union_find
-    trail_stack<var_eqs> & get_trail_stack() { return m_stack; }
+    trail_stack & get_trail_stack() { return m_stack; }
 
     void unmerge_eh(unsigned i, unsigned j) { 
         if (m_merge_handler) {

src/muz/base/dl_context.cpp

@@ -210,7 +210,7 @@ namespace datalog {
         m_contains_p(*this),
         m_rule_properties(m, m_rule_manager, *this, m_contains_p),
         m_transf(*this),
-        m_trail(*this),
+        m_trail(),
         m_pinned(m),
         m_bind_variables(m),
         m_rule_set(*this),

src/muz/base/dl_context.h

@@ -176,7 +176,7 @@ namespace datalog {
         contains_pred      m_contains_p;
         rule_properties    m_rule_properties;
         rule_transformer   m_transf;
-        trail_stack<context> m_trail;
+        trail_stack        m_trail;
         ast_ref_vector     m_pinned;
         bind_variables     m_bind_variables;
         sort_domain_map    m_sorts;

src/muz/fp/dl_cmds.cpp

@@ -44,7 +44,7 @@ struct dl_context {
     unsigned                      m_ref_count;
     datalog::dl_decl_plugin*      m_decl_plugin;
     scoped_ptr<datalog::context>  m_context;
-    trail_stack<dl_context>       m_trail;
+    trail_stack                   m_trail;
 
     fp_params const& get_params() {
         init();
@@ -57,7 +57,7 @@ struct dl_context {
         m_collected_cmds(collected_cmds),
         m_ref_count(0),
         m_decl_plugin(nullptr),
-        m_trail(*this) {}
+        m_trail() {}
 
     void inc_ref() {
         ++m_ref_count;

src/sat/smt/bv_solver.cpp

@@ -716,7 +716,7 @@ namespace bv {
         values[n->get_root_id()] = bv.mk_numeral(val, m_bits[v].size());
     }
 
-    trail_stack<euf::solver>& solver::get_trail_stack() {
+    trail_stack& solver::get_trail_stack() {
         return ctx.get_trail_stack();
     }
 

src/sat/smt/bv_solver.h

@@ -359,7 +359,7 @@ namespace bv {
         void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2);
         void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { SASSERT(check_zero_one_bits(r1)); }
         void unmerge_eh(theory_var v1, theory_var v2);
-        trail_stack<euf::solver>& get_trail_stack();
+        trail_stack& get_trail_stack();
 
         // diagnostics
         std::ostream& display(std::ostream& out, theory_var v) const;        

src/sat/smt/euf_solver.cpp

@@ -42,7 +42,7 @@ namespace euf {
         m(m),
         si(si),
         m_egraph(m),
-        m_trail(*this),
+        m_trail(),
         m_rewriter(m),
         m_unhandled_functions(m),
         m_lookahead(nullptr),

src/sat/smt/euf_solver.h

@@ -73,7 +73,6 @@ namespace euf {
         struct scope {
             unsigned m_var_lim;
         };
-        typedef trail_stack<solver> euf_trail_stack;
 
 
         size_t* to_ptr(sat::literal l) { return TAG(size_t*, reinterpret_cast<size_t*>((size_t)(l.index() << 4)), 1); }
@@ -93,7 +92,7 @@ namespace euf {
         sat::sat_internalizer& si;
         smt_params             m_config;
         euf::egraph            m_egraph;
-        euf_trail_stack        m_trail;
+        trail_stack            m_trail;
         stats                  m_stats;
         th_rewriter            m_rewriter;
         func_decl_ref_vector   m_unhandled_functions;
@@ -265,7 +264,7 @@ namespace euf {
             vec.push_back(val);
             push(push_back_trail< V, false>(vec));
         }
-        euf_trail_stack& get_trail_stack() { return m_trail; }
+        trail_stack& get_trail_stack() { return m_trail; }
 
         void updt_params(params_ref const& p);
         void set_lookahead(sat::lookahead* s) override { m_lookahead = s; }

src/sat/smt/q_mam.cpp

@@ -71,8 +71,6 @@ namespace q {
 
     class mam_impl;
 
-    typedef trail_stack<mam_impl> mam_trail_stack;
-
 
     template<typename T>
     class mam_value_trail : public value_trail<T> {

src/sat/smt/sat_th.cpp

@@ -65,7 +65,7 @@ namespace euf {
         return ctx.get_region();
     }
 
-    trail_stack<euf::solver>& th_euf_solver::get_trail_stack() {
+    trail_stack& th_euf_solver::get_trail_stack() {
         return ctx.get_trail_stack();
     }
 

src/sat/smt/sat_th.h

@@ -182,7 +182,7 @@ namespace euf {
         sat::literal mk_literal(expr* e) const;
         theory_var get_th_var(enode* n) const { return n->get_th_var(get_id()); }
         theory_var get_th_var(expr* e) const;
-        trail_stack<euf::solver>& get_trail_stack();
+        trail_stack& get_trail_stack();
         bool is_attached_to_var(enode* n) const;
         bool is_root(theory_var v) const { return var2enode(v)->is_root(); }
         void push() override { m_num_scopes++; }

src/smt/mam.cpp

@@ -64,7 +64,7 @@ namespace {
 
     class mam_impl;
 
-    typedef trail_stack<mam_impl> mam_trail_stack;
+    typedef trail_stack mam_trail_stack;
 
     typedef trail mam_trail;
 
@@ -3816,7 +3816,7 @@ namespace {
             mam(ctx),
             m(ctx.get_manager()),
             m_use_filters(use_filters),
-            m_trail_stack(*this),
+            m_trail_stack(),
             m_ct_manager(m_lbl_hasher, m_trail_stack),
             m_compiler(ctx, m_ct_manager, m_lbl_hasher, use_filters),
             m_interpreter(ctx, *this, use_filters),

src/smt/smt_context.cpp

@@ -1941,7 +1941,7 @@ namespace smt {
        \brief Execute generic undo-objects.
     */
     void context::undo_trail_stack(unsigned old_size) {
-        ::undo_trail_stack(*this, m_trail_stack, old_size);
+        ::undo_trail_stack(m_trail_stack, old_size);
     }
 
     /**

src/smt/theory_array.cpp

@@ -28,7 +28,7 @@ namespace smt {
         theory_array_base(ctx), 
         m_params(ctx.get_fparams()),
         m_find(*this),
-        m_trail_stack(*this),
+        m_trail_stack(),
         m_final_check_idx(0) {
         if (!ctx.relevancy())
             m_params.m_array_laziness = 0;

src/smt/theory_array.h

@@ -35,7 +35,6 @@ namespace smt {
 
     class theory_array : public theory_array_base {
     protected:
-        typedef trail_stack<theory_array> th_trail_stack;
         typedef union_find<theory_array>  th_union_find;
 
         struct var_data {
@@ -51,7 +50,7 @@ namespace smt {
         theory_array_params&            m_params;
         theory_array_stats              m_stats;
         th_union_find                   m_find;
-        th_trail_stack                  m_trail_stack;
+        trail_stack                     m_trail_stack;
         unsigned                        m_final_check_idx;
 
         theory_var mk_var(enode * n) override;
@@ -104,7 +103,7 @@ namespace smt {
         virtual void display_var(std::ostream & out, theory_var v) const;
         void display(std::ostream & out) const override;
         void collect_statistics(::statistics & st) const override;
-        th_trail_stack & get_trail_stack() { return m_trail_stack; }
+        trail_stack & get_trail_stack() { return m_trail_stack; }
         virtual void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var);
         static void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}
         void unmerge_eh(theory_var v1, theory_var v2);

src/smt/theory_bv.cpp

@@ -1442,7 +1442,7 @@ namespace smt {
         m_util(ctx.get_manager()),
         m_autil(ctx.get_manager()),
         m_bb(ctx.get_manager(), ctx.get_fparams()),
-        m_trail_stack(*this),
+        m_trail_stack(),
         m_find(*this),
         m_approximates_large_bvs(false) {
         memset(m_eq_activity, 0, sizeof(m_eq_activity));

src/smt/theory_bv.h

@@ -37,7 +37,6 @@ namespace smt {
 
     class theory_bv : public theory {
         typedef rational numeral;
-        typedef trail_stack<theory_bv> th_trail_stack;
         typedef union_find<theory_bv>  th_union_find;
         typedef std::pair<theory_var, unsigned> var_pos;
 
@@ -108,7 +107,7 @@ namespace smt {
         bv_util                  m_util;
         arith_util               m_autil;
         bit_blaster              m_bb;
-        th_trail_stack           m_trail_stack;
+        trail_stack              m_trail_stack;
         th_union_find            m_find;
         vector<literal_vector>   m_bits;     // per var, the bits of a given variable.
         ptr_vector<expr>         m_bits_expr;
@@ -268,7 +267,7 @@ namespace smt {
 
         char const * get_name() const override { return "bit-vector"; }
 
-        th_trail_stack & get_trail_stack() { return m_trail_stack; }
+        trail_stack & get_trail_stack() { return m_trail_stack; }
         void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2);
         void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { SASSERT(check_zero_one_bits(r1)); }
         void unmerge_eh(theory_var v1, theory_var v2);

src/smt/theory_datatype.cpp

@@ -701,7 +701,7 @@ namespace smt {
         m_util(m),
         m_autil(m),
         m_find(*this),
-        m_trail_stack(*this) {
+        m_trail_stack() {
     }
 
     theory_datatype::~theory_datatype() {

src/smt/theory_datatype.h

@@ -27,7 +27,6 @@ Revision History:
 
 namespace smt {
     class theory_datatype : public theory {
-        typedef trail_stack<theory_datatype> th_trail_stack;
         typedef union_find<theory_datatype>  th_union_find;
 
         struct var_data {
@@ -49,7 +48,7 @@ namespace smt {
         array_util                m_autil;
         ptr_vector<var_data>      m_var_data;
         th_union_find             m_find;
-        th_trail_stack            m_trail_stack;
+        trail_stack               m_trail_stack;
         datatype_factory *        m_factory;
         stats                     m_stats;
 
@@ -137,7 +136,7 @@ namespace smt {
         void collect_statistics(::statistics & st) const override;
         void init_model(model_generator & m) override;
         model_value_proc * mk_value(enode * n, model_generator & m) override;
-        th_trail_stack & get_trail_stack() { return m_trail_stack; }
+        trail_stack & get_trail_stack() { return m_trail_stack; }
         virtual void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var);
         static void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}
         void unmerge_eh(theory_var v1, theory_var v2);

src/smt/theory_fpa.cpp

@@ -30,7 +30,7 @@ namespace smt {
         m_th_rw(ctx.get_manager()),
         m_converter(ctx.get_manager(), m_th_rw),
         m_rw(ctx.get_manager(), m_converter, params_ref()),
-        m_trail_stack(*this),
+        m_trail_stack(),
         m_fpa_util(m_converter.fu()),
         m_bv_util(m_converter.bu()),
         m_arith_util(m_converter.au()),

src/smt/theory_fpa.h

@@ -30,7 +30,6 @@ namespace smt {
 
     class theory_fpa : public theory {
     protected:
-        typedef trail_stack<theory_fpa> th_trail_stack;
 
 
         class fpa_value_proc : public model_value_proc {
@@ -84,7 +83,7 @@ namespace smt {
         th_rewriter               m_th_rw;
         fpa2bv_converter_wrapped  m_converter;
         fpa2bv_rewriter           m_rw;
-        th_trail_stack            m_trail_stack;
+        trail_stack               m_trail_stack;
         fpa_value_factory *       m_factory;
         fpa_util                & m_fpa_util;
         bv_util                 & m_bv_util;

src/smt/theory_seq.cpp

@@ -275,7 +275,7 @@ theory_seq::theory_seq(context& ctx):
     m_eq(m, *this, m_ax.ax()),
     m_regex(*this),
     m_arith_value(m),
-    m_trail_stack(*this),
+    m_trail_stack(),
     m_ls(m), m_rs(m),
     m_lhs(m), m_rhs(m),
     m_new_eqs(m),

src/smt/theory_seq.h

@@ -49,7 +49,6 @@ namespace smt {
         typedef scoped_dependency_manager<assumption> dependency_manager;
         typedef dependency_manager::dependency dependency;        
 
-        typedef trail_stack<theory_seq> th_trail_stack;
         struct expr_dep {
             expr* v;
             expr* e;
@@ -365,7 +364,7 @@ namespace smt {
         seq::eq_solver   m_eq;
         seq_regex        m_regex;
         arith_value      m_arith_value;
-        th_trail_stack   m_trail_stack;
+        trail_stack      m_trail_stack;
         stats            m_stats;
         ptr_vector<expr> m_todo, m_concat;
         expr_ref_vector  m_ls, m_rs, m_lhs, m_rhs;
@@ -622,7 +621,7 @@ namespace smt {
         // model building
         app* mk_value(app* a);
 
-        th_trail_stack& get_trail_stack() { return m_trail_stack; }
+        trail_stack& get_trail_stack() { return m_trail_stack; }
         void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2) {}
         void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { }
         void unmerge_eh(theory_var v1, theory_var v2) {}

src/smt/theory_str.cpp

@@ -85,8 +85,8 @@ namespace smt {
         cacheHitCount(0),
         cacheMissCount(0),
         m_fresh_id(0),
-        m_trail_stack(*this),
+        m_trail_stack(),
-        m_library_aware_trail_stack(*this),
+        m_library_aware_trail_stack(),
         m_find(*this),
         fixed_length_subterm_trail(m),
         fixed_length_assumptions(m)

src/smt/theory_str.h

@@ -332,7 +332,6 @@ class theory_str : public theory {
         }
     };
 
-    typedef trail_stack<theory_str> th_trail_stack;
     typedef union_find<theory_str> th_union_find;
 
     typedef map<rational, expr*, obj_hash<rational>, default_eq<rational> > rational_map;
@@ -525,8 +524,8 @@ protected:
     // cache mapping each string S to Length(S)
     obj_map<expr, app*> length_ast_map;
 
-    th_trail_stack m_trail_stack;
+    trail_stack m_trail_stack;
-    th_trail_stack m_library_aware_trail_stack;
+    trail_stack m_library_aware_trail_stack;
     th_union_find m_find;
     theory_var get_var(expr * n) const;
     expr * get_eqc_next(expr * n);
@@ -792,7 +791,7 @@ public:
 
     bool overlapping_variables_detected() const { return loopDetected; }
 
-    th_trail_stack& get_trail_stack() { return m_trail_stack; }
+    trail_stack& get_trail_stack() { return m_trail_stack; }
     void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2) {}
     void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { }
     void unmerge_eh(theory_var v1, theory_var v2) {}

src/util/trail.h

@@ -409,8 +409,7 @@ public:
 };
 
 
-template<typename Ctx>
+inline void undo_trail_stack(ptr_vector<trail> & s, unsigned old_size) {
-void undo_trail_stack(Ctx & ctx, ptr_vector<trail> & s, unsigned old_size) {
     SASSERT(old_size <= s.size());
     typename ptr_vector<trail >::iterator begin = s.begin() + old_size;
     typename ptr_vector<trail >::iterator it    = s.end();
@@ -421,14 +420,12 @@ void undo_trail_stack(Ctx & ctx, ptr_vector<trail> & s, unsigned old_size) {
     s.shrink(old_size);
 }
 
-template<typename Ctx>
 class trail_stack {
-    Ctx &                   m_ctx;
     ptr_vector<trail>       m_trail_stack;
     unsigned_vector         m_scopes;
     region                  m_region;
 public:
-    trail_stack(Ctx & c):m_ctx(c) {}
+    trail_stack() {}
 
     ~trail_stack() {}
 
@@ -437,7 +434,7 @@ public:
     void reset() {
         pop_scope(m_scopes.size());
         // Undo trail objects stored at lvl 0 (avoid memory leaks if lvl 0 contains new_obj_trail objects).
-        undo_trail_stack(m_ctx, m_trail_stack, 0);
+        undo_trail_stack(m_trail_stack, 0);
     }
 
     void push_ptr(trail * t) { m_trail_stack.push_back(t); }
@@ -455,7 +452,7 @@ public:
         SASSERT(num_scopes <= lvl);
         unsigned new_lvl  = lvl - num_scopes;
         unsigned old_size = m_scopes[new_lvl];
-        undo_trail_stack(m_ctx, m_trail_stack, old_size);
+        undo_trail_stack(m_trail_stack, old_size);
         m_scopes.shrink(new_lvl);
         m_region.pop_scope(num_scopes);
     }

src/util/union_find.h

@@ -23,8 +23,8 @@ Revision History:
 
 class union_find_default_ctx {
 public:
-    typedef trail_stack<union_find_default_ctx> _trail_stack;
+    typedef trail_stack _trail_stack;
-    union_find_default_ctx() : m_stack(*this) {}
+    union_find_default_ctx() : m_stack() {}
        
     void unmerge_eh(unsigned, unsigned) {}
     void merge_eh(unsigned, unsigned, unsigned, unsigned) {}
@@ -39,7 +39,7 @@ private:
 template<typename Ctx = union_find_default_ctx, typename StackCtx = Ctx>
 class union_find {
     Ctx &                         m_ctx;
-    trail_stack<StackCtx> &       m_trail_stack;
+    trail_stack &                 m_trail_stack;
     svector<unsigned>             m_find;
     svector<unsigned>             m_size;
     svector<unsigned>             m_next;