simplify factory of dependent_expr_state_tactic

And as a side-effect, remove heap allocations for factories

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); }
-};

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) {

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)")
 */
-
-

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); });
 }

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);
 }
 
 /*

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)")
 */
-
-

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)")
 */
-
-

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)")
 */
-
-

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); });
 }

src/tactic/core/propagate_values2_tactic.h

@@ -14,28 +14,18 @@ Module Name:
     Nikolaj Bjorner (nbjorner) 2022-11-24
 
 --*/
-
-#include "util/params.h"
 #pragma once
 
 #include "util/params.h"
 #include "tactic/tactic.h"
 #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)")
 */
-

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)")
 */
-
-

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<dependent_expr_simplifier_factory>  m_factory;
+    factoryTy       m_factory;
     scoped_ptr<dependent_expr_simplifier>   m_simp;
     scoped_ptr<model_reconstruction_trail>  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,