3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00

reduce mem allocation in tactic API

This commit is contained in:
Nuno Lopes 2018-07-02 13:41:44 +01:00
parent fc8193828d
commit 8791f61aa7
7 changed files with 24 additions and 51 deletions

View file

@ -718,17 +718,11 @@ def mk_install_tactic_cpp_internal(h_files_full_path, path):
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')

View file

@ -32,14 +32,6 @@ Notes:
#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),

View file

@ -19,30 +19,28 @@ Notes:
#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);

View file

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

View file

@ -19,6 +19,7 @@ Author:
Notes:
--*/
#include "solver/tactic2solver.h"
#include "solver/solver_na2as.h"
#include "tactic/tactic.h"
#include "ast/ast_translation.h"
@ -31,6 +32,8 @@ Notes:
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 @@ public:
};
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);
}

View file

@ -23,12 +23,14 @@ Notes:
#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

View file

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