reduce mem allocation in tactic API

Z3Prover · Jul 2, 2018 · 8791f61 · 8791f61
1 parent fc81938
commit 8791f61
Show file tree

Hide file tree

Showing 7 changed files with 24 additions and 51 deletions.
diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py
@@ -718,17 +718,11 @@ def ADD_PROBE(name, descr, cmd):
                             fullname, line))
                         raise e
     # First pass will just generate the tactic factories
-    idx = 0
-    for data in ADD_TACTIC_DATA:
-        fout.write('MK_SIMPLE_TACTIC_FACTORY(__Z3_local_factory_%s, %s);\n' % (idx, data[2]))
-        idx = idx + 1
-    fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, FACTORY) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, alloc(FACTORY)))\n')
+    fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, CODE) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, [](ast_manager &m, const params_ref &p) { return CODE; }))\n')
     fout.write('#define ADD_PROBE(NAME, DESCR, PROBE) ctx.insert(alloc(probe_info, symbol(NAME), DESCR, PROBE))\n')
     fout.write('void install_tactics(tactic_manager & ctx) {\n')
-    idx = 0
     for data in ADD_TACTIC_DATA:
-        fout.write('  ADD_TACTIC_CMD("%s", "%s", __Z3_local_factory_%s);\n' % (data[0], data[1], idx))
-        idx = idx + 1
+        fout.write('  ADD_TACTIC_CMD("%s", "%s", %s);\n' % data)
     for data in ADD_PROBE_DATA:
         fout.write('  ADD_PROBE("%s", "%s", %s);\n' % data)
     fout.write('}\n')

diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
@@ -32,14 +32,6 @@ Module Name:
 #include "cmd_context/cmd_context_to_goal.h"
 #include "cmd_context/echo_tactic.h"
 
-tactic_cmd::~tactic_cmd() {
-    dealloc(m_factory);
-}
-
-tactic * tactic_cmd::mk(ast_manager & m) {
-    return (*m_factory)(m, params_ref());
-}
-
 probe_info::probe_info(symbol const & n, char const * d, probe * p):
     m_name(n),
     m_descr(d),

diff --git a/src/cmd_context/tactic_cmds.h b/src/cmd_context/tactic_cmds.h
@@ -19,30 +19,28 @@ Module Name:
 #define TACTIC_CMDS_H_
 
 #include "ast/ast.h"
+#include "util/params.h"
 #include "util/cmd_context_types.h"
 #include "util/ref.h"
 
 class tactic;
 class probe;
-class tactic_factory;
+
+typedef tactic* (*tactic_factory)(ast_manager&, const params_ref&);
 
 class tactic_cmd {
-    symbol           m_name;
-    char const *     m_descr;
-    tactic_factory * m_factory;
+    symbol         m_name;
+    char const *   m_descr;
+    tactic_factory m_factory;
 public:
-    tactic_cmd(symbol const & n, char const * d, tactic_factory * f):
-        m_name(n), m_descr(d), m_factory(f) {
-        SASSERT(m_factory);
-    }
-
-    ~tactic_cmd();
+    tactic_cmd(symbol const & n, char const * d, tactic_factory f):
+        m_name(n), m_descr(d), m_factory(f) {}
 
     symbol get_name() const { return m_name; }
 
     char const * get_descr() const { return m_descr; }
 
-    tactic * mk(ast_manager & m);
+    tactic * mk(ast_manager & m) { return m_factory(m, params_ref()); }
 };
 
 void install_core_tactic_cmds(cmd_context & ctx);

diff --git a/src/nlsat/tactic/qfnra_nlsat_tactic.h b/src/nlsat/tactic/qfnra_nlsat_tactic.h
@@ -25,8 +25,6 @@ class tactic;
 
 tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p = params_ref());
 
-MK_SIMPLE_TACTIC_FACTORY(qfnra_nlsat_fct, mk_qfnra_nlsat_tactic(m, p));
-
 /*
   ADD_TACTIC("qfnra-nlsat", "builtin strategy for solving QF_NRA problems using only nlsat.", "mk_qfnra_nlsat_tactic(m, p)")
 */

diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
@@ -19,6 +19,7 @@ Module Name:
 Notes:
 
 --*/
+#include "solver/tactic2solver.h"
 #include "solver/solver_na2as.h"
 #include "tactic/tactic.h"
 #include "ast/ast_translation.h"
@@ -31,6 +32,8 @@ Module Name:
    option for applications trying to solve many easy queries that a
    similar to each other.
 */
+
+namespace {
 class tactic2solver : public solver_na2as {
     expr_ref_vector              m_assertions;
     unsigned_vector              m_scopes;
@@ -258,6 +261,7 @@ unsigned tactic2solver::get_num_assertions() const {
 expr * tactic2solver::get_assertion(unsigned idx) const {
     return m_assertions.get(idx);
 }
+}
 
 
 solver * mk_tactic2solver(ast_manager & m, 
@@ -270,6 +274,7 @@ solver * mk_tactic2solver(ast_manager & m,
     return alloc(tactic2solver, m, t, p, produce_proofs, produce_models, produce_unsat_cores, logic);
 }
 
+namespace {
 class tactic2solver_factory : public solver_factory {
     ref<tactic> m_tactic;
 public:
@@ -284,24 +289,23 @@ class tactic2solver_factory : public solver_factory {
 };
 
 class tactic_factory2solver_factory : public solver_factory {
-    scoped_ptr<tactic_factory> m_factory;
+    tactic_factory m_factory;
 public:
-    tactic_factory2solver_factory(tactic_factory * f):m_factory(f) {
+    tactic_factory2solver_factory(tactic_factory f):m_factory(f) {
     }
 
-    ~tactic_factory2solver_factory() override {}
-
     solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override {
         tactic * t = (*m_factory)(m, p);
         return mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, logic);
     }
 };
+}
 
 solver_factory * mk_tactic2solver_factory(tactic * t) {
     return alloc(tactic2solver_factory, t);
 }
 
-solver_factory * mk_tactic_factory2solver_factory(tactic_factory * f) {
+solver_factory * mk_tactic_factory2solver_factory(tactic_factory f) {
     return alloc(tactic_factory2solver_factory, f);
 }
 

diff --git a/src/solver/tactic2solver.h b/src/solver/tactic2solver.h
@@ -23,12 +23,14 @@ Module Name:
 #define TACTIC2SOLVER_H_
 
 #include "util/params.h"
+
 class ast_manager;
 class tactic;
-class tactic_factory;
 class solver;
 class solver_factory;
 
+typedef tactic* (*tactic_factory)(ast_manager&, const params_ref&);
+
 solver * mk_tactic2solver(ast_manager & m, 
                           tactic * t = nullptr,
                           params_ref const & p = params_ref(), 
@@ -39,6 +41,6 @@ solver * mk_tactic2solver(ast_manager & m,
 
 
 solver_factory * mk_tactic2solver_factory(tactic * t);
-solver_factory * mk_tactic_factory2solver_factory(tactic_factory * f);
+solver_factory * mk_tactic_factory2solver_factory(tactic_factory f);
 
 #endif
diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
@@ -119,21 +119,6 @@ tactic * mk_fail_if_undecided_tactic();
 tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl);
 tactic * mk_trace_tactic(char const * tag);
 
-class tactic_factory {
-public:
-    virtual ~tactic_factory() {}
-    virtual tactic * operator()(ast_manager & m, params_ref const & p) = 0;
-};
-
-#define MK_TACTIC_FACTORY(NAME, CODE)                                           \
-class NAME : public tactic_factory {                                            \
-public:                                                                         \
-    virtual ~NAME() {}                                                          \
-    virtual tactic * operator()(ast_manager & m, params_ref const & p) { CODE } \
-};
-
-#define MK_SIMPLE_TACTIC_FACTORY(NAME, ST)  MK_TACTIC_FACTORY(NAME, return ST;)
-
 void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result);
 lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown);