mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

garbage collect all api::object references when calling del_context. Request issue #679

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-07-13 22:26:21 -07:00
parent f30fb7639e
commit b080e3a216
25 changed files with 115 additions and 56 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_algebraic.cpp
View file

@ -378,7 +378,7 @@ extern "C" {
vector_var2anum v2a(as);
_am.isolate_roots(_p, v2a, roots);
}
Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, mk_c(c)->m());
Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(result);
for (unsigned i = 0; i < roots.size(); i++) {
result->m_ast_vector.push_back(au(c).mk_numeral(roots.get(i), false));

2
src/api/api_ast.cpp
View file

@ -721,7 +721,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_simplify_get_param_descrs(c);
RESET_ERROR_CODE();
Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref);
Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c));
mk_c(c)->save_object(d);
th_rewriter::get_param_descrs(d->m_descrs);
Z3_param_descrs r = of_param_descrs(d);

4
src/api/api_ast_map.cpp
View file

@ -34,7 +34,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_ast_map(c);
RESET_ERROR_CODE();
Z3_ast_map_ref * m = alloc(Z3_ast_map_ref, mk_c(c)->m());
Z3_ast_map_ref * m = alloc(Z3_ast_map_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(m);
Z3_ast_map r = of_ast_map(m);
RETURN_Z3(r);
@ -137,7 +137,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_ast_map_keys(c, m);
RESET_ERROR_CODE();
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, to_ast_map(m)->m);
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), to_ast_map(m)->m);
mk_c(c)->save_object(v);
obj_map<ast, ast*>::iterator it = to_ast_map_ref(m).begin();
obj_map<ast, ast*>::iterator end = to_ast_map_ref(m).end();

2
src/api/api_ast_map.h
View file

@ -24,7 +24,7 @@ Revision History:
struct Z3_ast_map_ref : public api::object {
ast_manager & m;
obj_map<ast, ast*> m_map;
Z3_ast_map_ref(ast_manager & _m):m(_m) {}
Z3_ast_map_ref(api::context& c, ast_manager & _m): api::object(c), m(_m) {}
virtual ~Z3_ast_map_ref();
};

4
src/api/api_ast_vector.cpp
View file

@ -29,7 +29,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_ast_vector(c);
RESET_ERROR_CODE();
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(v);
Z3_ast_vector r = of_ast_vector(v);
RETURN_Z3(r);
@ -111,7 +111,7 @@ extern "C" {
RETURN_Z3(0);
}
ast_translation translator(mk_c(c)->m(), mk_c(t)->m());
Z3_ast_vector_ref * new_v = alloc(Z3_ast_vector_ref, mk_c(t)->m());
Z3_ast_vector_ref * new_v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(t)->m());
mk_c(t)->save_object(new_v);
unsigned sz = to_ast_vector_ref(v).size();
for (unsigned i = 0; i < sz; i++) {

6
src/api/api_ast_vector.h
View file

@ -20,9 +20,13 @@ Revision History:
#include"api_util.h"
namespace api {
class context;
};
struct Z3_ast_vector_ref : public api::object {
ast_ref_vector m_ast_vector;
Z3_ast_vector_ref(ast_manager & m):m_ast_vector(m) {}
Z3_ast_vector_ref(api::context& c, ast_manager & m): api::object(c), m_ast_vector(m) {}
virtual ~Z3_ast_vector_ref() {}
};

30
src/api/api_context.cpp
View file

@ -32,6 +32,28 @@ void install_tactics(tactic_manager & ctx);
namespace api {
object::object(context& c): m_ref_count(0), m_context(c) { this->m_id = m_context.add_object(this); }
void object::inc_ref() { m_ref_count++; }
void object::dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) m_context.del_object(this); }
unsigned context::add_object(api::object* o) {
unsigned id = m_allocated_objects.size();
if (!m_free_object_ids.empty()) {
id = m_free_object_ids.back();
m_free_object_ids.pop_back();
}
m_allocated_objects.insert(id, o);
return id;
}
void context::del_object(api::object* o) {
m_free_object_ids.push_back(o->id());
m_allocated_objects.remove(o->id());
dealloc(o);
}
static void default_error_handler(Z3_context ctx, Z3_error_code c) {
printf("Error: %s\n", Z3_get_error_msg(ctx, c));
exit(1);
@ -106,6 +128,14 @@ namespace api {
context::~context() {
reset_parser();
m_last_obj = 0;
u_map<api::object*>::iterator it = m_allocated_objects.begin();
while (it != m_allocated_objects.end()) {
//warning_msg("Junk: %d", it->m_key);
m_allocated_objects.remove(it->m_key);
dealloc(it->m_value);
it = m_allocated_objects.begin();
}
}
void context::interrupt() {

6
src/api/api_context.h
View file

@ -35,6 +35,7 @@ Revision History:
#include"tactic_manager.h"
#include"context_params.h"
#include"api_polynomial.h"
#include"hashtable.h"
namespace smtlib {
class parser;
@ -69,6 +70,8 @@ namespace api {
ast_ref_vector m_ast_trail; //!< used when m_user_ref_count == false
ref<api::object> m_last_obj; //!< reference to the last API object returned by the APIs
u_map<api::object*> m_allocated_objects; // !< table containing current set of allocated API objects
unsigned_vector m_free_object_ids; // !< free list of identifiers available for allocated objects.
family_id m_basic_fid;
family_id m_array_fid;
@ -141,6 +144,9 @@ namespace api {
// Sign an error if solver is searching
void check_searching();
unsigned add_object(api::object* o);
void del_object(api::object* o);
Z3_ast_print_mode get_print_mode() const { return m_print_mode; }
void set_print_mode(Z3_ast_print_mode m) { m_print_mode = m; }

12
src/api/api_datalog.cpp
View file

@ -223,7 +223,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_fixedpoint(c);
RESET_ERROR_CODE();
Z3_fixedpoint_ref * d = alloc(Z3_fixedpoint_ref);
Z3_fixedpoint_ref * d = alloc(Z3_fixedpoint_ref, *mk_c(c));
d->m_datalog = alloc(api::fixedpoint_context, mk_c(c)->m(), mk_c(c)->fparams());
mk_c(c)->save_object(d);
Z3_fixedpoint r = of_datalog(d);
@ -369,7 +369,7 @@ extern "C" {
return 0;
}
Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m);
mk_c(c)->save_object(v);
for (unsigned i = 0; i < coll.m_queries.size(); ++i) {
v->m_ast_vector.push_back(coll.m_queries[i].get());
@ -421,7 +421,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_fixedpoint_get_statistics(c, d);
RESET_ERROR_CODE();
Z3_stats_ref * st = alloc(Z3_stats_ref);
Z3_stats_ref * st = alloc(Z3_stats_ref, (*mk_c(c)));
to_fixedpoint_ref(d)->ctx().collect_statistics(st->m_stats);
mk_c(c)->save_object(st);
Z3_stats r = of_stats(st);
@ -460,7 +460,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_fixedpoint_get_rules(c, d);
ast_manager& m = mk_c(c)->m();
Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m);
mk_c(c)->save_object(v);
expr_ref_vector rules(m), queries(m);
svector<symbol> names;
@ -483,7 +483,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_fixedpoint_get_assertions(c, d);
ast_manager& m = mk_c(c)->m();
Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m);
mk_c(c)->save_object(v);
unsigned num_asserts = to_fixedpoint_ref(d)->ctx().get_num_assertions();
for (unsigned i = 0; i < num_asserts; ++i) {
@ -568,7 +568,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_fixedpoint_get_param_descrs(c, f);
RESET_ERROR_CODE();
Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref);
Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c));
mk_c(c)->save_object(d);
to_fixedpoint_ref(f)->collect_param_descrs(d->m_descrs);
Z3_param_descrs r = of_param_descrs(d);

3
src/api/api_datalog.h
View file

@ -30,13 +30,14 @@ typedef void (*reduce_assign_callback_fptr)(void*, func_decl*, unsigned, expr*co
namespace api {
class fixedpoint_context;
class context;
};
struct Z3_fixedpoint_ref : public api::object {
api::fixedpoint_context * m_datalog;
params_ref m_params;
Z3_fixedpoint_ref():m_datalog(0) {}
Z3_fixedpoint_ref(api::context& c): api::object(c), m_datalog(0) {}
virtual ~Z3_fixedpoint_ref() { dealloc(m_datalog); }
};

4
src/api/api_goal.cpp
View file

@ -32,7 +32,7 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
Z3_goal_ref * g = alloc(Z3_goal_ref);
Z3_goal_ref * g = alloc(Z3_goal_ref, *mk_c(c));
g->m_goal = alloc(goal, mk_c(c)->m(), proofs != 0, models != 0, unsat_cores != 0);
mk_c(c)->save_object(g);
Z3_goal r = of_goal(g);
@ -156,7 +156,7 @@ extern "C" {
LOG_Z3_goal_translate(c, g, target);
RESET_ERROR_CODE();
ast_translation translator(mk_c(c)->m(), mk_c(target)->m());
Z3_goal_ref * _r = alloc(Z3_goal_ref);
Z3_goal_ref * _r = alloc(Z3_goal_ref, *mk_c(c));
_r->m_goal = to_goal_ref(g)->translate(translator);
mk_c(target)->save_object(_r);
Z3_goal r = of_goal(_r);

1
src/api/api_goal.h
View file

@ -23,6 +23,7 @@ Revision History:
struct Z3_goal_ref : public api::object {
goal_ref m_goal;
Z3_goal_ref(api::context& c) : api::object(c) {}
virtual ~Z3_goal_ref() {}
};

6
src/api/api_interp.cpp
View file

@ -212,7 +212,7 @@ extern "C" {
LOG_Z3_get_interpolant(c, pf, pat, p);
RESET_ERROR_CODE();
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(v);
ast *_pf = to_ast(pf);
@ -303,7 +303,7 @@ extern "C" {
if (_status == l_false){
// copy result back
v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(v);
for (unsigned i = 0; i < interp.size(); i++){
v->m_ast_vector.push_back(interp[i]);
@ -314,7 +314,7 @@ extern "C" {
model_ref mr;
m_solver.get()->get_model(mr);
if(mr.get()){
Z3_model_ref *tmp_val = alloc(Z3_model_ref);
Z3_model_ref *tmp_val = alloc(Z3_model_ref, *mk_c(c));
tmp_val->m_model = mr.get();
mk_c(c)->save_object(tmp_val);
*model = of_model(tmp_val);

6
src/api/api_model.cpp
View file

@ -86,7 +86,7 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
Z3_func_interp_ref * fi = alloc(Z3_func_interp_ref, to_model_ref(m));
Z3_func_interp_ref * fi = alloc(Z3_func_interp_ref, *mk_c(c), to_model_ref(m));
fi->m_func_interp = _fi;
mk_c(c)->save_object(fi);
RETURN_Z3(of_func_interp(fi));
@ -192,7 +192,7 @@ extern "C" {
RETURN_Z3(0);
}
ptr_vector<expr> const & universe = to_model_ref(m)->get_universe(to_sort(s));
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(v);
unsigned sz = universe.size();
for (unsigned i = 0; i < sz; i++) {
@ -262,7 +262,7 @@ extern "C" {
SET_ERROR_CODE(Z3_IOB);
RETURN_Z3(0);
}
Z3_func_entry_ref * e = alloc(Z3_func_entry_ref, to_func_interp(f)->m_model.get());
Z3_func_entry_ref * e = alloc(Z3_func_entry_ref, *mk_c(c), to_func_interp(f)->m_model.get());
e->m_func_interp = to_func_interp_ref(f);
e->m_func_entry = to_func_interp_ref(f)->get_entry(i);
mk_c(c)->save_object(e);

6
src/api/api_model.h
View file

@ -23,7 +23,7 @@ Revision History:
struct Z3_model_ref : public api::object {
model_ref m_model;
Z3_model_ref() {}
Z3_model_ref(api::context& c): api::object(c) {}
virtual ~Z3_model_ref() {}
};
@ -34,7 +34,7 @@ inline model * to_model_ref(Z3_model s) { return to_model(s)->m_model.get(); }
struct Z3_func_interp_ref : public api::object {
model_ref m_model; // must have it to prevent reference to m_func_interp to be killed.
func_interp * m_func_interp;
Z3_func_interp_ref(model * m):m_model(m), m_func_interp(0) {}
Z3_func_interp_ref(api::context& c, model * m): api::object(c), m_model(m), m_func_interp(0) {}
virtual ~Z3_func_interp_ref() {}
};
@ -46,7 +46,7 @@ struct Z3_func_entry_ref : public api::object {
model_ref m_model; // must have it to prevent reference to m_func_entry to be killed.
func_interp * m_func_interp;
func_entry const * m_func_entry;
Z3_func_entry_ref(model * m):m_model(m), m_func_interp(0), m_func_entry(0) {}
Z3_func_entry_ref(api::context& c, model * m):api::object(c), m_model(m), m_func_interp(0), m_func_entry(0) {}
virtual ~Z3_func_entry_ref() {}
};

10
src/api/api_opt.cpp
View file

@ -31,7 +31,7 @@ extern "C" {
struct Z3_optimize_ref : public api::object {
opt::context* m_opt;
Z3_optimize_ref():m_opt(0) {}
Z3_optimize_ref(api::context& c): api::object(c), m_opt(0) {}
virtual ~Z3_optimize_ref() { dealloc(m_opt); }
};
inline Z3_optimize_ref * to_optimize(Z3_optimize o) { return reinterpret_cast<Z3_optimize_ref *>(o); }
@ -42,7 +42,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_optimize(c);
RESET_ERROR_CODE();
Z3_optimize_ref * o = alloc(Z3_optimize_ref);
Z3_optimize_ref * o = alloc(Z3_optimize_ref, *mk_c(c));
o->m_opt = alloc(opt::context,mk_c(c)->m());
mk_c(c)->save_object(o);
RETURN_Z3(of_optimize(o));
@ -158,7 +158,7 @@ extern "C" {
RESET_ERROR_CODE();
model_ref _m;
to_optimize_ptr(o)->get_model(_m);
Z3_model_ref * m_ref = alloc(Z3_model_ref);
Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c));
if (_m) {
m_ref->m_model = _m;
}
@ -186,7 +186,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_optimize_get_param_descrs(c, o);
RESET_ERROR_CODE();
Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref);
Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c));
mk_c(c)->save_object(d);
to_optimize_ptr(o)->collect_param_descrs(d->m_descrs);
Z3_param_descrs r = of_param_descrs(d);
@ -240,7 +240,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_optimize_get_statistics(c, d);
RESET_ERROR_CODE();
Z3_stats_ref * st = alloc(Z3_stats_ref);
Z3_stats_ref * st = alloc(Z3_stats_ref, *mk_c(c));
to_optimize_ptr(d)->collect_statistics(st->m_stats);
mk_c(c)->save_object(st);
Z3_stats r = of_stats(st);

2
src/api/api_params.cpp
View file

@ -30,7 +30,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_params(c);
RESET_ERROR_CODE();
Z3_params_ref * p = alloc(Z3_params_ref);
Z3_params_ref * p = alloc(Z3_params_ref, *mk_c(c));
mk_c(c)->save_object(p);
Z3_params r = of_params(p);
RETURN_Z3(r);

2
src/api/api_polynomial.cpp
View file

@ -53,7 +53,7 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, mk_c(c)->m());
Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(result);
if (converter.is_var(to_expr(x))) {
expr2var const & mapping = converter.get_mapping();

20
src/api/api_solver.cpp
View file

@ -58,7 +58,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_simple_solver(c);
RESET_ERROR_CODE();
Z3_solver_ref * s = alloc(Z3_solver_ref, mk_smt_solver_factory());
Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_solver_factory());
mk_c(c)->save_object(s);
Z3_solver r = of_solver(s);
RETURN_Z3(r);
@ -69,7 +69,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_solver(c);
RESET_ERROR_CODE();
Z3_solver_ref * s = alloc(Z3_solver_ref, mk_smt_strategic_solver_factory());
Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_strategic_solver_factory());
mk_c(c)->save_object(s);
Z3_solver r = of_solver(s);
RETURN_Z3(r);
@ -80,7 +80,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_solver_for_logic(c, logic);
RESET_ERROR_CODE();
Z3_solver_ref * s = alloc(Z3_solver_ref, mk_smt_strategic_solver_factory(to_symbol(logic)));
Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_strategic_solver_factory(to_symbol(logic)));
mk_c(c)->save_object(s);
Z3_solver r = of_solver(s);
RETURN_Z3(r);
@ -91,7 +91,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_solver_from_tactic(c, t);
RESET_ERROR_CODE();
Z3_solver_ref * s = alloc(Z3_solver_ref, mk_tactic2solver_factory(to_tactic_ref(t)));
Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_tactic2solver_factory(to_tactic_ref(t)));
mk_c(c)->save_object(s);
Z3_solver r = of_solver(s);
RETURN_Z3(r);
@ -103,7 +103,7 @@ extern "C" {
LOG_Z3_solver_translate(c, s, target);
RESET_ERROR_CODE();
params_ref const& p = to_solver(s)->m_params;
Z3_solver_ref * sr = alloc(Z3_solver_ref, 0);
Z3_solver_ref * sr = alloc(Z3_solver_ref, *mk_c(c), 0);
init_solver(c, s);
sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p);
mk_c(target)->save_object(sr);
@ -134,7 +134,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_get_param_descrs(c, s);
RESET_ERROR_CODE();
Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref);
Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c));
mk_c(c)->save_object(d);
bool initialized = to_solver(s)->m_solver.get() != 0;
if (!initialized)
@ -255,7 +255,7 @@ extern "C" {
LOG_Z3_solver_get_assertions(c, s);
RESET_ERROR_CODE();
init_solver(c, s);
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(v);
unsigned sz = to_solver_ref(s)->get_num_assertions();
for (unsigned i = 0; i < sz; i++) {
@ -323,7 +323,7 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_USAGE);
RETURN_Z3(0);
}
Z3_model_ref * m_ref = alloc(Z3_model_ref);
Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c));
m_ref->m_model = _m;
mk_c(c)->save_object(m_ref);
RETURN_Z3(of_model(m_ref));
@ -352,7 +352,7 @@ extern "C" {
init_solver(c, s);
ptr_vector<expr> core;
to_solver_ref(s)->get_unsat_core(core);
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(v);
for (unsigned i = 0; i < core.size(); i++) {
v->m_ast_vector.push_back(core[i]);
@ -375,7 +375,7 @@ extern "C" {
LOG_Z3_solver_get_statistics(c, s);
RESET_ERROR_CODE();
init_solver(c, s);
Z3_stats_ref * st = alloc(Z3_stats_ref);
Z3_stats_ref * st = alloc(Z3_stats_ref, *mk_c(c));
to_solver_ref(s)->collect_statistics(st->m_stats);
get_memory_statistics(st->m_stats);
get_rlimit_statistics(mk_c(c)->m().limit(), st->m_stats);

2
src/api/api_solver.h
View file

@ -26,7 +26,7 @@ struct Z3_solver_ref : public api::object {
ref<solver> m_solver;
params_ref m_params;
symbol m_logic;
Z3_solver_ref(solver_factory * f):m_solver_factory(f), m_solver(0), m_logic(symbol::null) {}
Z3_solver_ref(api::context& c, solver_factory * f): api::object(c), m_solver_factory(f), m_solver(0), m_logic(symbol::null) {}
virtual ~Z3_solver_ref() {}
};

1
src/api/api_stats.h
View file

@ -23,6 +23,7 @@ Revision History:
struct Z3_stats_ref : public api::object {
statistics m_stats;
Z3_stats_ref(api::context& c): api::object(c) {}
virtual ~Z3_stats_ref() {}
};

14
src/api/api_tactic.cpp
View file

@ -25,13 +25,13 @@ Revision History:
#include"cancel_eh.h"
#include"scoped_timer.h"
Z3_apply_result_ref::Z3_apply_result_ref(ast_manager & m):m_core(m) {
Z3_apply_result_ref::Z3_apply_result_ref(api::context& c, ast_manager & m): api::object(c), m_core(m) {
}
extern "C" {
#define RETURN_TACTIC(_t_) { \
Z3_tactic_ref * _ref_ = alloc(Z3_tactic_ref); \
Z3_tactic_ref * _ref_ = alloc(Z3_tactic_ref, *mk_c(c)); \
_ref_->m_tactic = _t_; \
mk_c(c)->save_object(_ref_); \
Z3_tactic _result_ = of_tactic(_ref_); \
@ -39,7 +39,7 @@ extern "C" {
}
#define RETURN_PROBE(_t_) { \
Z3_probe_ref * _ref_ = alloc(Z3_probe_ref); \
Z3_probe_ref * _ref_ = alloc(Z3_probe_ref, *mk_c(c)); \
_ref_->m_probe = _t_; \
mk_c(c)->save_object(_ref_); \
Z3_probe _result_ = of_probe(_ref_); \
@ -367,7 +367,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_tactic_get_param_descrs(c, t);
RESET_ERROR_CODE();
Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref);
Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c));
mk_c(c)->save_object(d);
to_tactic_ref(t)->collect_param_descrs(d->m_descrs);
Z3_param_descrs r = of_param_descrs(d);
@ -404,7 +404,7 @@ extern "C" {
static Z3_apply_result _tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g, params_ref p) {
goal_ref new_goal;
new_goal = alloc(goal, *to_goal_ref(g));
Z3_apply_result_ref * ref = alloc(Z3_apply_result_ref, mk_c(c)->m());
Z3_apply_result_ref * ref = alloc(Z3_apply_result_ref, (*mk_c(c)), mk_c(c)->m());
mk_c(c)->save_object(ref);
unsigned timeout = p.get_uint("timeout", UINT_MAX);
@ -505,7 +505,7 @@ extern "C" {
SET_ERROR_CODE(Z3_IOB);
RETURN_Z3(0);
}
Z3_goal_ref * g = alloc(Z3_goal_ref);
Z3_goal_ref * g = alloc(Z3_goal_ref, *mk_c(c));
g->m_goal = to_apply_result(r)->m_subgoals[i];
mk_c(c)->save_object(g);
Z3_goal result = of_goal(g);
@ -524,7 +524,7 @@ extern "C" {
model_ref new_m = to_model_ref(m)->copy();
if (to_apply_result(r)->m_mc)
to_apply_result(r)->m_mc->operator()(new_m, i);
Z3_model_ref * m_ref = alloc(Z3_model_ref);
Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c));
m_ref->m_model = new_m;
mk_c(c)->save_object(m_ref);
RETURN_Z3(of_model(m_ref));

9
src/api/api_tactic.h
View file

@ -21,13 +21,20 @@ Revision History:
#include"api_goal.h"
#include"tactical.h"
namespace api {
class context;
}
struct Z3_tactic_ref : public api::object {
tactic_ref m_tactic;
Z3_tactic_ref(api::context& c): api::object(c) {}
virtual ~Z3_tactic_ref() {}
};
struct Z3_probe_ref : public api::object {
probe_ref m_probe;
Z3_probe_ref(api::context& c):api::object(c) {}
virtual ~Z3_probe_ref() {}
};
@ -44,7 +51,7 @@ struct Z3_apply_result_ref : public api::object {
model_converter_ref m_mc;
proof_converter_ref m_pc;
expr_dependency_ref m_core;
Z3_apply_result_ref(ast_manager & m);
Z3_apply_result_ref(api::context& c, ast_manager & m);
virtual ~Z3_apply_result_ref() {}
};

13
src/api/api_util.h
View file

@ -31,15 +31,20 @@ Revision History:
#define CHECK_REF_COUNT(a) (reinterpret_cast<ast const*>(a)->get_ref_count() > 0)
namespace api {
class context;
// Generic wrapper for ref-count objects exposed by the API
class object {
unsigned m_ref_count;
unsigned m_id;
context& m_context;
public:
object():m_ref_count(0) {}
object(context& c);
virtual ~object() {}
unsigned ref_count() const { return m_ref_count; }
void inc_ref() { m_ref_count++; }
void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); }
unsigned id() const { return m_id; }
void inc_ref();
void dec_ref();
};
};
@ -82,6 +87,7 @@ inline lbool to_lbool(Z3_lbool b) { return static_cast<lbool>(b); }
struct Z3_params_ref : public api::object {
params_ref m_params;
Z3_params_ref(api::context& c): api::object(c) {}
virtual ~Z3_params_ref() {}
};
@ -91,6 +97,7 @@ inline params_ref to_param_ref(Z3_params p) { return p == 0 ? params_ref() : to_
struct Z3_param_descrs_ref : public api::object {
param_descrs m_descrs;
Z3_param_descrs_ref(api::context& c): api::object(c) {}
virtual ~Z3_param_descrs_ref() {}
};

4
src/util/hashtable.h
View file

@ -645,7 +645,6 @@ public:
ptr_addr_hashtable(unsigned initial_capacity = DEFAULT_HASHTABLE_INITIAL_CAPACITY):
core_hashtable<ptr_addr_hash_entry<T>, ptr_hash<T>, ptr_eq<T> >(initial_capacity) {}
// Using iterators to traverse the elements of this kind of hashtable will produce non-determinism.
iterator begin() const {
UNREACHABLE();
}
@ -653,6 +652,9 @@ public:
iterator end() const {
UNREACHABLE();
}
// NB. Using iterators to traverse the elements of this kind of hashtable will produce non-determinism.
};
/**