From 15a7621e27da45abf5392aa1411f63ca6452a8ae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Mar 2021 11:14:20 -0700 Subject: [PATCH] remove template dependency for trail objects --- src/math/lp/emonics.h | 6 +++--- src/math/lp/var_eqs.h | 6 +++--- src/muz/base/dl_context.cpp | 2 +- src/muz/base/dl_context.h | 2 +- src/muz/fp/dl_cmds.cpp | 4 ++-- src/sat/smt/bv_solver.cpp | 2 +- src/sat/smt/bv_solver.h | 2 +- src/sat/smt/euf_solver.cpp | 2 +- src/sat/smt/euf_solver.h | 5 ++--- src/sat/smt/q_mam.cpp | 2 -- src/sat/smt/sat_th.cpp | 2 +- src/sat/smt/sat_th.h | 2 +- src/smt/mam.cpp | 4 ++-- src/smt/smt_context.cpp | 2 +- src/smt/theory_array.cpp | 2 +- src/smt/theory_array.h | 5 ++--- src/smt/theory_bv.cpp | 2 +- src/smt/theory_bv.h | 5 ++--- src/smt/theory_datatype.cpp | 2 +- src/smt/theory_datatype.h | 5 ++--- src/smt/theory_fpa.cpp | 2 +- src/smt/theory_fpa.h | 3 +-- src/smt/theory_seq.cpp | 2 +- src/smt/theory_seq.h | 5 ++--- src/smt/theory_str.cpp | 4 ++-- src/smt/theory_str.h | 7 +++---- src/util/trail.h | 11 ++++------- src/util/union_find.h | 6 +++--- 28 files changed, 46 insertions(+), 58 deletions(-) diff --git a/src/math/lp/emonics.h b/src/math/lp/emonics.h index 243f65f1e..a72aa0fde 100644 --- a/src/math/lp/emonics.h +++ b/src/math/lp/emonics.h @@ -82,7 +82,7 @@ class emonics { }; union_find m_u_f; - trail_stack m_u_f_stack; + trail_stack m_u_f_stack; mutable svector m_find_key; // the key used when looking for a monic with the specific variables var_eqs& m_ve; mutable vector m_monics; // set of monics @@ -124,7 +124,7 @@ public: */ emonics(var_eqs& 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 & get_trail_stack() { return m_u_f_stack; } + trail_stack & get_trail_stack() { return m_u_f_stack; } /** \brief push/pop scopes. diff --git a/src/math/lp/var_eqs.h b/src/math/lp/var_eqs.h index 24e90673d..5a2eb5b5f 100644 --- a/src/math/lp/var_eqs.h +++ b/src/math/lp/var_eqs.h @@ -72,7 +72,7 @@ class var_eqs { m_trail; vector> m_eqs; // signed_var.index() -> the edges adjacent to signed_var.index() - trail_stack m_stack; + trail_stack m_stack; mutable svector 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 & 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) { diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index ed9183e1d..d3a79acb5 100644 --- a/src/muz/base/dl_context.cpp +++ b/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), diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 1425b43d9..754132f2a 100644 --- a/src/muz/base/dl_context.h +++ b/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 m_trail; + trail_stack m_trail; ast_ref_vector m_pinned; bind_variables m_bind_variables; sort_domain_map m_sorts; diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index 94efa5de2..7500674ad 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/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 m_context; - trail_stack 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; diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index c216530af..52a6be565 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/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& solver::get_trail_stack() { + trail_stack& solver::get_trail_stack() { return ctx.get_trail_stack(); } diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 17e199448..c92255d1b 100644 --- a/src/sat/smt/bv_solver.h +++ b/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& get_trail_stack(); + trail_stack& get_trail_stack(); // diagnostics std::ostream& display(std::ostream& out, theory_var v) const; diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 6155f6b20..89779f144 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/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), diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 379c21a90..0361e0735 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -73,7 +73,6 @@ namespace euf { struct scope { unsigned m_var_lim; }; - typedef trail_stack euf_trail_stack; size_t* to_ptr(sat::literal l) { return TAG(size_t*, reinterpret_cast((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; } diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index 42af24de8..d48613e19 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -71,8 +71,6 @@ namespace q { class mam_impl; - typedef trail_stack mam_trail_stack; - template class mam_value_trail : public value_trail { diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index bebe9ad5d..5e391533a 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -65,7 +65,7 @@ namespace euf { return ctx.get_region(); } - trail_stack& th_euf_solver::get_trail_stack() { + trail_stack& th_euf_solver::get_trail_stack() { return ctx.get_trail_stack(); } diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 3c1c369b9..d7865300d 100644 --- a/src/sat/smt/sat_th.h +++ b/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& 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++; } diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 14c7e048f..daa6f8e18 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -64,7 +64,7 @@ namespace { class mam_impl; - typedef trail_stack 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), diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 3a7ecab71..ff1478a0e 100644 --- a/src/smt/smt_context.cpp +++ b/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); } /** diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index 7c9b792ef..e27103757 100644 --- a/src/smt/theory_array.cpp +++ b/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; diff --git a/src/smt/theory_array.h b/src/smt/theory_array.h index 2b38aaa2d..67ae8a8a5 100644 --- a/src/smt/theory_array.h +++ b/src/smt/theory_array.h @@ -35,7 +35,6 @@ namespace smt { class theory_array : public theory_array_base { protected: - typedef trail_stack th_trail_stack; typedef union_find 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); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 468277cb3..4f59f9e7e 100644 --- a/src/smt/theory_bv.cpp +++ b/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)); diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index d01a9b1d4..931e3041a 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -37,7 +37,6 @@ namespace smt { class theory_bv : public theory { typedef rational numeral; - typedef trail_stack th_trail_stack; typedef union_find th_union_find; typedef std::pair 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 m_bits; // per var, the bits of a given variable. ptr_vector 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); diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index be16225b2..3e87894af 100644 --- a/src/smt/theory_datatype.cpp +++ b/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() { diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index a9168607a..d219b1f9d 100644 --- a/src/smt/theory_datatype.h +++ b/src/smt/theory_datatype.h @@ -27,7 +27,6 @@ Revision History: namespace smt { class theory_datatype : public theory { - typedef trail_stack th_trail_stack; typedef union_find th_union_find; struct var_data { @@ -49,7 +48,7 @@ namespace smt { array_util m_autil; ptr_vector 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); diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index cd5d2ad1e..5f8e35394 100644 --- a/src/smt/theory_fpa.cpp +++ b/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()), diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 59ce39e5c..9d5df855e 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -30,7 +30,6 @@ namespace smt { class theory_fpa : public theory { protected: - typedef trail_stack 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; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 506191c6b..cd3e48fae 100644 --- a/src/smt/theory_seq.cpp +++ b/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), diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 527df86a5..1041495af 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -49,7 +49,6 @@ namespace smt { typedef scoped_dependency_manager dependency_manager; typedef dependency_manager::dependency dependency; - typedef trail_stack 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 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) {} diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 4b27886c8..93ed5464e 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -85,8 +85,8 @@ namespace smt { cacheHitCount(0), cacheMissCount(0), m_fresh_id(0), - m_trail_stack(*this), - m_library_aware_trail_stack(*this), + m_trail_stack(), + m_library_aware_trail_stack(), m_find(*this), fixed_length_subterm_trail(m), fixed_length_assumptions(m) diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 8a7158d02..ccedcfc5c 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -332,7 +332,6 @@ class theory_str : public theory { } }; - typedef trail_stack th_trail_stack; typedef union_find th_union_find; typedef map, default_eq > rational_map; @@ -525,8 +524,8 @@ protected: // cache mapping each string S to Length(S) obj_map length_ast_map; - th_trail_stack m_trail_stack; - th_trail_stack m_library_aware_trail_stack; + trail_stack m_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) {} diff --git a/src/util/trail.h b/src/util/trail.h index 6450fc85a..2ef2bdbff 100644 --- a/src/util/trail.h +++ b/src/util/trail.h @@ -409,8 +409,7 @@ public: }; -template -void undo_trail_stack(Ctx & ctx, ptr_vector & s, unsigned old_size) { +inline void undo_trail_stack(ptr_vector & s, unsigned old_size) { SASSERT(old_size <= s.size()); typename ptr_vector::iterator begin = s.begin() + old_size; typename ptr_vector::iterator it = s.end(); @@ -421,14 +420,12 @@ void undo_trail_stack(Ctx & ctx, ptr_vector & s, unsigned old_size) { s.shrink(old_size); } -template class trail_stack { - Ctx & m_ctx; ptr_vector 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); } diff --git a/src/util/union_find.h b/src/util/union_find.h index e6ab80f8a..cd487a007 100644 --- a/src/util/union_find.h +++ b/src/util/union_find.h @@ -23,8 +23,8 @@ Revision History: class union_find_default_ctx { public: - typedef trail_stack _trail_stack; - union_find_default_ctx() : m_stack(*this) {} + typedef trail_stack _trail_stack; + union_find_default_ctx() : m_stack() {} void unmerge_eh(unsigned, unsigned) {} void merge_eh(unsigned, unsigned, unsigned, unsigned) {} @@ -39,7 +39,7 @@ private: template class union_find { Ctx & m_ctx; - trail_stack & m_trail_stack; + trail_stack & m_trail_stack; svector m_find; svector m_size; svector m_next;