mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

Refactored iz3 example to avoid compiler warnings.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-10-29 13:03:19 +00:00
parent b47e9d74e9
commit bd5b455c46
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
examples/interp/iz3.cpp
View file

@ -104,7 +104,7 @@ int main(int argc, const char **argv) {
unsigned num_theory; unsigned num_theory;
Z3_ast *theory; Z3_ast *theory;
ok = Z3_read_interpolation_problem(ctx, &num, &constraints, tree_mode ? &parents : 0, filename, &error, &num_theory, &theory); ok = Z3_read_interpolation_problem(ctx, &num, &constraints, tree_mode ? &parents : 0, filename, &error, &num_theory, &theory) != 0;
/* If parse failed, print the error message */ /* If parse failed, print the error message */
@ -124,7 +124,7 @@ int main(int argc, const char **argv) {
std::cout << "Splitting formula into " << nconjs << " conjuncts...\n"; std::cout << "Splitting formula into " << nconjs << " conjuncts...\n";
num = nconjs; num = nconjs;
constraints = new Z3_ast[num]; constraints = new Z3_ast[num];
for(int k = 0; k < num; k++) for(unsigned k = 0; k < num; k++)
constraints[k] = Z3_get_app_arg(ctx,app,k); constraints[k] = Z3_get_app_arg(ctx,app,k);
} }
} }
@ -163,12 +163,12 @@ int main(int argc, const char **argv) {
std::vector<Z3_ast> asserted(num); std::vector<Z3_ast> asserted(num);
/* We start with nothing asserted. */ /* We start with nothing asserted. */
for(int i = 0; i < num; i++) for(unsigned i = 0; i < num; i++)
asserted[i] = Z3_mk_true(ctx); asserted[i] = Z3_mk_true(ctx);
/* Now we assert the constrints one at a time until UNSAT. */ /* Now we assert the constrints one at a time until UNSAT. */
for(int i = 0; i < num; i++){ for(unsigned i = 0; i < num; i++){
asserted[i] = constraints[i]; asserted[i] = constraints[i];
Z3_assert_cnstr(ctx,constraints[i]); // assert one constraint Z3_assert_cnstr(ctx,constraints[i]); // assert one constraint
result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, &asserted[0], parents, options, interpolants, &model, 0, true, 0, 0); result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, &asserted[0], parents, options, interpolants, &model, 0, true, 0, 0);
@ -190,7 +190,7 @@ int main(int argc, const char **argv) {
printf("unsat\n"); printf("unsat\n");
if(output_file.empty()){ if(output_file.empty()){
printf("interpolant:\n"); printf("interpolant:\n");
for(int i = 0; i < num-1; i++) for(unsigned i = 0; i < num-1; i++)
printf("%s\n", Z3_ast_to_string(ctx, interpolants[i])); printf("%s\n", Z3_ast_to_string(ctx, interpolants[i]));
} }
else { else {
@ -203,7 +203,7 @@ int main(int argc, const char **argv) {
if(check_mode){ if(check_mode){
std::cout << "Checking interpolant...\n"; std::cout << "Checking interpolant...\n";
bool chk; bool chk;
chk = Z3_check_interpolant(ctx,num,constraints,parents,interpolants,&error,num_theory,theory); chk = Z3_check_interpolant(ctx,num,constraints,parents,interpolants,&error,num_theory,theory) != 0;
if(chk) if(chk)
std::cout << "Interpolant is correct\n"; std::cout << "Interpolant is correct\n";
else { else {