mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

fix iz3parse for updated API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-06-04 16:05:14 -07:00
parent c33dce1161
commit 83635eb826
1 changed files with 23 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

46
src/api/api_interp.cpp
View file

@ -506,42 +506,39 @@ extern "C" {
static std::string read_msg; static std::string read_msg;
static std::vector<Z3_ast> read_theory; static std::vector<Z3_ast> read_theory;
static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, svector<Z3_ast> &assertions){ static Z3_ast_vector iZ3_parse(Z3_context ctx, const char *filename, const char ** error){
read_error.clear(); read_error.clear();
try { try {
std::string foo(filename); std::string foo(filename);
if (foo.size() >= 5 && foo.substr(foo.size() - 5) == ".smt2"){ if (foo.size() >= 5 && foo.substr(foo.size() - 5) == ".smt2"){
Z3_ast_vector assrts = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0); Z3_ast_vector assrts = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0);
Z3_ast_vector_inc_ref(ctx, assrts); Z3_ast_vector_inc_ref(ctx, assrts);
unsigned nconjs = Z3_ast_vector_size(ctx, assrts); return assrts;
assertions.resize(nconjs);
for (unsigned k = 0; k < nconjs; k++)
assertions[k] = Z3_ast_vector_get(ctx, assrts, k);
// Z3_ast_vector_dec_ref(ctx, assrts) is unsafe
} }
else { else {
Z3_parse_smtlib_file(ctx, filename, 0, 0, 0, 0, 0, 0); Z3_parse_smtlib_file(ctx, filename, 0, 0, 0, 0, 0, 0);
int numa = Z3_get_smtlib_num_assumptions(ctx); int numa = Z3_get_smtlib_num_assumptions(ctx);
int numf = Z3_get_smtlib_num_formulas(ctx); int numf = Z3_get_smtlib_num_formulas(ctx);
int num = numa + numf; Z3_ast_vector assrts = Z3_mk_ast_vector(ctx);
Z3_ast_vector_inc_ref(ctx, assrts);
assertions.resize(num); for (int j = 0; j < numa; j++){
for (int j = 0; j < num; j++){ Z3_ast_vector_push(ctx, assrts, Z3_get_smtlib_assumption(ctx, j));
if (j < numa)
assertions[j] = Z3_get_smtlib_assumption(ctx, j);
else
assertions[j] = Z3_get_smtlib_formula(ctx, j - numa);
} }
for (int j = 0; j < numf; j++){
Z3_ast_vector_push(ctx, assrts, Z3_get_smtlib_formula(ctx, j));
}
return assrts;
} }
} }
catch (...) { catch (...) {
read_error << "SMTLIB parse error: " << Z3_get_smtlib_error(ctx); read_error << "SMTLIB parse error: " << Z3_get_smtlib_error(ctx);
read_msg = read_error.str(); read_msg = read_error.str();
*error = read_msg.c_str(); *error = read_msg.c_str();
return false; return 0;
} }
Z3_set_error_handler(ctx, 0); Z3_set_error_handler(ctx, 0);
return true; return 0;
} }
@ -554,23 +551,23 @@ extern "C" {
if (file_params.find("THEORY") != file_params.end()) if (file_params.find("THEORY") != file_params.end())
num_theory = atoi(file_params["THEORY"].c_str()); num_theory = atoi(file_params["THEORY"].c_str());
svector<Z3_ast> assertions; Z3_ast_vector assertions = iZ3_parse(ctx, filename, error);
if (!iZ3_parse(ctx, filename, error, assertions)) if (assertions == 0)
return false; return false;
if (num_theory > assertions.size()) if (num_theory > Z3_ast_vector_size(ctx, assertions))
num_theory = assertions.size(); num_theory = Z3_ast_vector_size(ctx, assertions);
unsigned num = assertions.size() - num_theory; unsigned num = Z3_ast_vector_size(ctx, assertions) - num_theory;
read_cnsts.resize(num); read_cnsts.resize(num);
read_parents.resize(num); read_parents.resize(num);
read_theory.resize(num_theory); read_theory.resize(num_theory);
for (unsigned j = 0; j < num_theory; j++) for (unsigned j = 0; j < num_theory; j++)
read_theory[j] = assertions[j]; read_theory[j] = Z3_ast_vector_get(ctx, assertions, j);
for (unsigned j = 0; j < num; j++) for (unsigned j = 0; j < num; j++)
read_cnsts[j] = assertions[j + num_theory]; read_cnsts[j] = Z3_ast_vector_get(ctx, assertions, j + num_theory);
if (ret_num_theory) if (ret_num_theory)
*ret_num_theory = num_theory; *ret_num_theory = num_theory;
if (theory) if (theory)
@ -579,6 +576,7 @@ extern "C" {
if (!parents){ if (!parents){
*_num = num; *_num = num;
*cnsts = &read_cnsts[0]; *cnsts = &read_cnsts[0];
Z3_ast_vector_dec_ref(ctx, assertions);
return true; return true;
} }
@ -650,9 +648,11 @@ extern "C" {
*_num = num; *_num = num;
*cnsts = &read_cnsts[0]; *cnsts = &read_cnsts[0];
*parents = &read_parents[0]; *parents = &read_parents[0];
Z3_ast_vector_dec_ref(ctx, assertions);
return true; return true;
fail: fail:
Z3_ast_vector_dec_ref(ctx, assertions);
read_msg = read_error.str(); read_msg = read_error.str();
*error = read_msg.c_str(); *error = read_msg.c_str();
return false; return false;