mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

remove dependency on ARRAYSIZE for issue #1616

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-08-15 22:26:14 -07:00
parent 95963f71f4
commit 2b2f193f2b
11 changed files with 137 additions and 49 deletions
Download patch file Download diff file Expand all files Collapse all files

96
src/api/api_datalog.cpp
View file

@ -623,6 +623,100 @@ extern "C" {
to_fixedpoint_ref(d)->ctx().add_constraint(to_expr(e), lvl);
}
#include "api_datalog_spacer.inc"
Z3_lbool Z3_API Z3_fixedpoint_query_from_lvl (Z3_context c, Z3_fixedpoint d, Z3_ast q, unsigned lvl) {
Z3_TRY;
LOG_Z3_fixedpoint_query_from_lvl (c, d, q, lvl);
RESET_ERROR_CODE();
lbool r = l_undef;
unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
unsigned rlimit = to_fixedpoint(d)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
{
scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
cancel_eh<reslimit> eh(mk_c(c)->m().limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
scoped_timer timer(timeout, &eh);
try {
r = to_fixedpoint_ref(d)->ctx().query_from_lvl (to_expr(q), lvl);
}
catch (z3_exception& ex) {
mk_c(c)->handle_exception(ex);
r = l_undef;
}
to_fixedpoint_ref(d)->ctx().cleanup();
}
return of_lbool(r);
Z3_CATCH_RETURN(Z3_L_UNDEF);
}
Z3_ast Z3_API Z3_fixedpoint_get_ground_sat_answer(Z3_context c, Z3_fixedpoint d) {
Z3_TRY;
LOG_Z3_fixedpoint_get_ground_sat_answer(c, d);
RESET_ERROR_CODE();
expr* e = to_fixedpoint_ref(d)->ctx().get_ground_sat_answer();
mk_c(c)->save_ast_trail(e);
RETURN_Z3(of_expr(e));
Z3_CATCH_RETURN(nullptr);
}
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules_along_trace(
Z3_context c,
Z3_fixedpoint d)
{
Z3_TRY;
LOG_Z3_fixedpoint_get_rules_along_trace(c, d);
ast_manager& m = mk_c(c)->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);
svector<symbol> names;
to_fixedpoint_ref(d)->ctx().get_rules_along_trace_as_formulas(rules, names);
for (unsigned i = 0; i < rules.size(); ++i) {
v->m_ast_vector.push_back(rules[i].get());
}
RETURN_Z3(of_ast_vector(v));
Z3_CATCH_RETURN(nullptr);
}
Z3_symbol Z3_API Z3_fixedpoint_get_rule_names_along_trace(
Z3_context c,
Z3_fixedpoint d)
{
Z3_TRY;
LOG_Z3_fixedpoint_get_rule_names_along_trace(c, d);
ast_manager& m = mk_c(c)->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);
svector<symbol> names;
std::stringstream ss;
to_fixedpoint_ref(d)->ctx().get_rules_along_trace_as_formulas(rules, names);
for (unsigned i = 0; i < names.size(); ++i) {
ss << ";" << names[i].str();
}
RETURN_Z3(of_symbol(symbol(ss.str().substr(1).c_str())));
Z3_CATCH_RETURN(nullptr);
}
void Z3_API Z3_fixedpoint_add_invariant(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred, Z3_ast property) {
Z3_TRY;
LOG_Z3_fixedpoint_add_invariant(c, d, pred, property);
RESET_ERROR_CODE();
to_fixedpoint_ref(d)->ctx ().add_invariant(to_func_decl(pred), to_expr(property));
Z3_CATCH;
}
Z3_ast Z3_API Z3_fixedpoint_get_reachable(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred) {
Z3_TRY;
LOG_Z3_fixedpoint_get_reachable(c, d, pred);
RESET_ERROR_CODE();
expr_ref r = to_fixedpoint_ref(d)->ctx().get_reachable(to_func_decl(pred));
mk_c(c)->save_ast_trail(r);
RETURN_Z3(of_expr(r.get()));
Z3_CATCH_RETURN(nullptr);
}
};

40
src/api/api_qe.cpp
View file

@ -1,5 +1,5 @@
/*++
Copyright (c) 2017 Arie Gurfinkel
Copyright (c) Microsoft Corporation, Arive Gurfinkel 2017
Module Name:
@ -70,39 +70,39 @@ extern "C"
}
Z3_ast Z3_API Z3_qe_model_project_skolem (Z3_context c,
Z3_model m,
Z3_model mdl,
unsigned num_bounds,
Z3_app const bound[],
Z3_ast body,
Z3_ast_map map)
{
Z3_TRY;
LOG_Z3_qe_model_project_skolem (c, m, num_bounds, bound, body, map);
LOG_Z3_qe_model_project_skolem (c, mdl, num_bounds, bound, body, map);
RESET_ERROR_CODE();
ast_manager& man = mk_c(c)->m ();
app_ref_vector vars(man);
ast_manager& m = mk_c(c)->m();
app_ref_vector vars(m);
if (!to_apps(num_bounds, bound, vars)) {
RETURN_Z3(nullptr);
}
expr_ref result (mk_c(c)->m ());
expr_ref result (m);
result = to_expr (body);
model_ref model (to_model_ref (m));
expr_map emap (man);
model_ref model (to_model_ref (mdl));
expr_map emap (m);
spacer::qe_project (mk_c(c)->m (), vars, result, model, emap);
mk_c(c)->save_ast_trail (result.get ());
spacer::qe_project(m, vars, result, model, emap);
mk_c(c)->save_ast_trail(result);
obj_map<ast, ast*> &map_z3 = to_ast_map_ref(map);
for (expr_map::iterator it = emap.begin(), end = emap.end(); it != end; ++it){
man.inc_ref(&(it->get_key()));
man.inc_ref(it->get_value());
map_z3.insert(&(it->get_key()), it->get_value());
for (auto& kv : emap) {
m.inc_ref(kv.m_key);
m.inc_ref(kv.m_value);
map_z3.insert(kv.m_key, kv.m_value);
}
return of_expr (result.get ());
return of_expr (result);
Z3_CATCH_RETURN(nullptr);
}
@ -124,9 +124,9 @@ extern "C"
expr_ref result (mk_c(c)->m ());
result = mk_and (lits);
mk_c(c)->save_ast_trail (result.get ());
mk_c(c)->save_ast_trail (result);
return of_expr (result.get ());
return of_expr (result);
Z3_CATCH_RETURN(nullptr);
}
@ -138,8 +138,8 @@ extern "C"
ast_ref_vector &vVars = to_ast_vector_ref (vars);
app_ref_vector vApps (mk_c(c)->m());
for (unsigned i = 0; i < vVars.size (); ++i) {
app *a = to_app (vVars.get (i));
for (ast* v : vVars) {
app * a = to_app(v);
if (a->get_kind () != AST_APP) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
RETURN_Z3(nullptr);
@ -162,7 +162,7 @@ extern "C"
}
}
mk_c(c)->save_ast_trail (result.get ());
mk_c(c)->save_ast_trail (result);
return of_expr (result);
Z3_CATCH_RETURN(nullptr);
}