From eb8c53c16431ddb6f3f07b5f102eab2a1a50769b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 5 Dec 2022 14:07:57 +0000 Subject: [PATCH] simplify factory of dependent_expr_state_tactic And as a side-effect, remove heap allocations for factories --- src/ast/simplifiers/dependent_expr_state.h | 18 ------------------ src/qe/lite/qe_lite.cpp | 10 ++-------- src/tactic/arith/card2bv_tactic.h | 13 ++----------- src/tactic/bv/bv_slice_tactic.cpp | 11 ++--------- src/tactic/bv/max_bv_sharing_tactic.h | 9 +-------- src/tactic/core/demodulator_tactic.h | 13 ++----------- src/tactic/core/elim_uncnstr2_tactic.h | 13 ++----------- src/tactic/core/eliminate_predicates_tactic.h | 13 ++----------- src/tactic/core/euf_completion_tactic.cpp | 10 ++-------- src/tactic/core/propagate_values2_tactic.h | 14 ++------------ src/tactic/core/solve_eqs_tactic.h | 13 ++----------- src/tactic/dependent_expr_state_tactic.h | 12 +++++++----- 12 files changed, 26 insertions(+), 123 deletions(-) diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h index d7aa1d6ebd1..212bc99a4a3 100644 --- a/src/ast/simplifiers/dependent_expr_state.h +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -149,21 +149,3 @@ class dependent_expr_simplifier { ast_manager& get_manager() { return m; } dependent_expr_state& get_fmls() { return m_fmls; } }; - -/** - Factory interface for creating simplifiers. - The use of a factory allows delaying the creation of the dependent_expr_state - argument until the point where the expression simplifier is created. - This is used in tactics where the dependent_expr_state is a reference to the - new tactic. - - Alternatively have a clone method on dependent_expr_simplifier. - */ -class dependent_expr_simplifier_factory { - unsigned m_ref = 0; -public: - virtual dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) = 0; - virtual ~dependent_expr_simplifier_factory() {} - void inc_ref() { ++m_ref; } - void dec_ref() { if (--m_ref == 0) dealloc(this); } -}; diff --git a/src/qe/lite/qe_lite.cpp b/src/qe/lite/qe_lite.cpp index 2ea11b6b960..d3d45bd4b1e 100644 --- a/src/qe/lite/qe_lite.cpp +++ b/src/qe/lite/qe_lite.cpp @@ -2440,17 +2440,11 @@ namespace { } } }; - - class qe_lite_tactic_factory : public dependent_expr_simplifier_factory { - public: - dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override { - return alloc(qe_lite_simplifier, m, p, s); - } - }; } tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p) { - return alloc(dependent_expr_state_tactic, m, p, alloc(qe_lite_tactic_factory)); + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(qe_lite_simplifier, m, p, s); }); } dependent_expr_simplifier* mk_qe_lite_simplifer(ast_manager& m, params_ref const& p, dependent_expr_state& st) { diff --git a/src/tactic/arith/card2bv_tactic.h b/src/tactic/arith/card2bv_tactic.h index 63cb021d706..d7ad76e7d30 100644 --- a/src/tactic/arith/card2bv_tactic.h +++ b/src/tactic/arith/card2bv_tactic.h @@ -16,25 +16,16 @@ Module Name: --*/ #pragma once - #include "util/params.h" #include "tactic/tactic.h" #include "tactic/dependent_expr_state_tactic.h" #include "ast/simplifiers/card2bv.h" -class card2bv_tactic_factory : public dependent_expr_simplifier_factory { -public: - dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override { - return alloc(card2bv, m, p, s); - } -}; - inline tactic* mk_card2bv_tactic(ast_manager& m, params_ref const& p = params_ref()) { - return alloc(dependent_expr_state_tactic, m, p, alloc(card2bv_tactic_factory)); + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(card2bv, m, p, s); }); } /* ADD_TACTIC("card2bv", "convert pseudo-boolean constraints to bit-vectors.", "mk_card2bv_tactic(m, p)") */ - - diff --git a/src/tactic/bv/bv_slice_tactic.cpp b/src/tactic/bv/bv_slice_tactic.cpp index 17d69c7b147..d470f6e7275 100644 --- a/src/tactic/bv/bv_slice_tactic.cpp +++ b/src/tactic/bv/bv_slice_tactic.cpp @@ -20,14 +20,7 @@ Module Name: #include "tactic/dependent_expr_state_tactic.h" #include "tactic/bv/bv_slice_tactic.h" - -class bv_slice_factory : public dependent_expr_simplifier_factory { -public: - dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override { - return alloc(bv::slice, m, s); - } -}; - tactic* mk_bv_slice_tactic(ast_manager& m, params_ref const& p) { - return alloc(dependent_expr_state_tactic, m, p, alloc(bv_slice_factory)); + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(bv::slice, m, s); }); } diff --git a/src/tactic/bv/max_bv_sharing_tactic.h b/src/tactic/bv/max_bv_sharing_tactic.h index 3521b4a041e..bf14e9f14e7 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.h +++ b/src/tactic/bv/max_bv_sharing_tactic.h @@ -24,15 +24,8 @@ Revision History: #include "ast/simplifiers/max_bv_sharing.h" #include "tactic/dependent_expr_state_tactic.h" -class max_bv_sharing_tactic_factory : public dependent_expr_simplifier_factory { -public: - dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override { - return mk_max_bv_sharing(m, p, s); - } -}; - inline tactic* mk_max_bv_sharing_tactic(ast_manager& m, params_ref const& p = params_ref()) { - return alloc(dependent_expr_state_tactic, m, p, alloc(max_bv_sharing_tactic_factory)); + return alloc(dependent_expr_state_tactic, m, p, mk_max_bv_sharing); } /* diff --git a/src/tactic/core/demodulator_tactic.h b/src/tactic/core/demodulator_tactic.h index 2583e902eb0..b278392c929 100644 --- a/src/tactic/core/demodulator_tactic.h +++ b/src/tactic/core/demodulator_tactic.h @@ -21,20 +21,11 @@ Module Name: #include "tactic/dependent_expr_state_tactic.h" #include "ast/simplifiers/demodulator_simplifier.h" - -class demodulator_tactic_factory : public dependent_expr_simplifier_factory { -public: - dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override { - return alloc(demodulator_simplifier, m, p, s); - } -}; - inline tactic * mk_demodulator_tactic(ast_manager& m, params_ref const& p = params_ref()) { - return alloc(dependent_expr_state_tactic, m, p, alloc(demodulator_tactic_factory)); + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(demodulator_simplifier, m, p, s); }); } /* ADD_TACTIC("demodulator", "solve for variables.", "mk_demodulator_tactic(m, p)") */ - - diff --git a/src/tactic/core/elim_uncnstr2_tactic.h b/src/tactic/core/elim_uncnstr2_tactic.h index e7226a8f0af..61e3bbb5a75 100644 --- a/src/tactic/core/elim_uncnstr2_tactic.h +++ b/src/tactic/core/elim_uncnstr2_tactic.h @@ -21,20 +21,11 @@ Module Name: #include "tactic/dependent_expr_state_tactic.h" #include "ast/simplifiers/elim_unconstrained.h" -class elim_uncnstr2_tactic_factory : public dependent_expr_simplifier_factory { -public: - dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override { - return alloc(elim_unconstrained, m, s); - } -}; - inline tactic * mk_elim_uncnstr2_tactic(ast_manager & m, params_ref const & p = params_ref()) { - return alloc(dependent_expr_state_tactic, m, p, alloc(elim_uncnstr2_tactic_factory)); + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(elim_unconstrained, m, s); }); } - /* ADD_TACTIC("elim-uncnstr2", "eliminate unconstrained variables.", "mk_elim_uncnstr2_tactic(m, p)") */ - - diff --git a/src/tactic/core/eliminate_predicates_tactic.h b/src/tactic/core/eliminate_predicates_tactic.h index de2291260b7..d89f369dc00 100644 --- a/src/tactic/core/eliminate_predicates_tactic.h +++ b/src/tactic/core/eliminate_predicates_tactic.h @@ -21,20 +21,11 @@ Module Name: #include "tactic/tactic.h" #include "tactic/dependent_expr_state_tactic.h" - -class eliminate_predicates_tactic_factory : public dependent_expr_simplifier_factory { -public: - dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override { - return alloc(eliminate_predicates, m, s); - } -}; - inline tactic * mk_eliminate_predicates_tactic(ast_manager& m, params_ref const& p = params_ref()) { - return alloc(dependent_expr_state_tactic, m, p, alloc(eliminate_predicates_tactic_factory)); + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(eliminate_predicates, m, s); }); } /* ADD_TACTIC("elim-predicates", "eliminate predicates.", "mk_eliminate_predicates_tactic(m, p)") */ - - diff --git a/src/tactic/core/euf_completion_tactic.cpp b/src/tactic/core/euf_completion_tactic.cpp index d229df62f74..ec440878299 100644 --- a/src/tactic/core/euf_completion_tactic.cpp +++ b/src/tactic/core/euf_completion_tactic.cpp @@ -20,13 +20,7 @@ Module Name: #include "ast/simplifiers/euf_completion.h" #include "tactic/core/euf_completion_tactic.h" -class euf_completion_tactic_factory : public dependent_expr_simplifier_factory { -public: - dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override { - return alloc(euf::completion, m, s); - } -}; - tactic * mk_euf_completion_tactic(ast_manager& m, params_ref const& p) { - return alloc(dependent_expr_state_tactic, m, p, alloc(euf_completion_tactic_factory)); + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(euf::completion, m, s); }); } diff --git a/src/tactic/core/propagate_values2_tactic.h b/src/tactic/core/propagate_values2_tactic.h index 834e8bebd48..4c89fae9766 100644 --- a/src/tactic/core/propagate_values2_tactic.h +++ b/src/tactic/core/propagate_values2_tactic.h @@ -14,8 +14,6 @@ Module Name: Nikolaj Bjorner (nbjorner) 2022-11-24 --*/ - -#include "util/params.h" #pragma once #include "util/params.h" @@ -23,19 +21,11 @@ Module Name: #include "tactic/dependent_expr_state_tactic.h" #include "ast/simplifiers/propagate_values.h" -class propagate_values2_tactic_factory : public dependent_expr_simplifier_factory { -public: - dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override { - return alloc(propagate_values, m, p, s); - } -}; - inline tactic * mk_propagate_values2_tactic(ast_manager & m, params_ref const & p = params_ref()) { - return alloc(dependent_expr_state_tactic, m, p, alloc(propagate_values2_tactic_factory)); + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(propagate_values, m, p, s); }); } - /* ADD_TACTIC("propagate-values2", "propagate constants.", "mk_propagate_values2_tactic(m, p)") */ - diff --git a/src/tactic/core/solve_eqs_tactic.h b/src/tactic/core/solve_eqs_tactic.h index 76a73866004..a0fd3b63bef 100644 --- a/src/tactic/core/solve_eqs_tactic.h +++ b/src/tactic/core/solve_eqs_tactic.h @@ -21,20 +21,11 @@ Module Name: #include "tactic/dependent_expr_state_tactic.h" #include "ast/simplifiers/solve_eqs.h" - -class solve_eqs_tactic_factory : public dependent_expr_simplifier_factory { -public: - dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override { - return alloc(euf::solve_eqs, m, s); - } -}; - inline tactic * mk_solve_eqs_tactic(ast_manager& m, params_ref const& p = params_ref()) { - return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs_tactic_factory)); + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(euf::solve_eqs, m, s); }); } /* ADD_TACTIC("solve-eqs", "solve for variables.", "mk_solve_eqs_tactic(m, p)") */ - - diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h index 3afc0fc9fe7..f2d53236840 100644 --- a/src/tactic/dependent_expr_state_tactic.h +++ b/src/tactic/dependent_expr_state_tactic.h @@ -20,19 +20,22 @@ Module Name: #include "ast/simplifiers/dependent_expr_state.h" class dependent_expr_state_tactic : public tactic, public dependent_expr_state { +public: + using factoryTy = dependent_expr_simplifier(*(*)(ast_manager& m, params_ref const& p, dependent_expr_state& s)); +private: ast_manager& m; params_ref m_params; trail_stack m_trail; goal_ref m_goal; dependent_expr m_dep; statistics m_st; - ref m_factory; + factoryTy m_factory; scoped_ptr m_simp; scoped_ptr m_model_trail; void init() { if (!m_simp) { - m_simp = m_factory->mk(m, m_params, *this); + m_simp = m_factory(m, m_params, *this); m_st.reset(); } if (!m_model_trail) @@ -41,12 +44,11 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state { public: - dependent_expr_state_tactic(ast_manager& m, params_ref const& p, dependent_expr_simplifier_factory* f): + dependent_expr_state_tactic(ast_manager& m, params_ref const& p, factoryTy f): dependent_expr_state(m), m(m), m_params(p), m_factory(f), - m_simp(nullptr), m_dep(m, m.mk_true(), nullptr) {} @@ -96,7 +98,7 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state { } tactic * translate(ast_manager & m) override { - return alloc(dependent_expr_state_tactic, m, m_params, m_factory.get()); + return alloc(dependent_expr_state_tactic, m, m_params, m_factory); } void operator()(goal_ref const & in,