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

Merge pull request #449 from kenmcmil/issue243

Browse source 
fixed logging on return of Z3_compute_interpolant...
This commit is contained in:
Christoph M. Wintersteiger 2016-02-12 12:40:01 +00:00
parent 8d61d36c3f 8b90bc9e91
commit 9dbb8057ca
2 changed files with 43 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
examples/c/test_capi.c
View file

@ -2341,6 +2341,46 @@ void unsat_core_and_proof_example() {
Z3_del_context(ctx);
}
void interpolation_example() {
Z3_context ctx = mk_context();
Z3_ast pa = mk_bool_var(ctx, "PredA");
Z3_ast pb = mk_bool_var(ctx, "PredB");
Z3_ast pc = mk_bool_var(ctx, "PredC");
Z3_ast args1[2] = {pa,pb}, args2[2] = {Z3_mk_not(ctx,pb),pc};
Z3_ast args3[2] = {Z3_mk_interpolant(ctx,Z3_mk_and(ctx,2,args1)),Z3_mk_and(ctx,2,args2)};
Z3_ast f = Z3_mk_and(ctx,2,args3);
Z3_ast_vector interpolant = 0;
Z3_model m = 0;
printf("\ninterpolation_example\n");
LOG_MSG("interpolation_example");
Z3_lbool result = Z3_compute_interpolant(ctx,f,0,&interpolant,&m);
switch (result) {
case Z3_L_FALSE:
printf("unsat\n");
printf("interpolant: %s\n", Z3_ast_to_string(ctx, Z3_ast_vector_get(ctx, interpolant, 0)));
printf("\n");
break;
case Z3_L_UNDEF:
printf("unknown\n");
printf("potential model:\n");
if (m) Z3_model_inc_ref(ctx, m);
display_model(ctx, stdout, m);
break;
case Z3_L_TRUE:
printf("sat\n");
if (m) Z3_model_inc_ref(ctx, m);
display_model(ctx, stdout, m);
break;
}
/* delete logical context */
if (m) Z3_model_dec_ref(ctx, m);
Z3_del_context(ctx);
}
#define MAX_RETRACTABLE_ASSERTIONS 1024
/**
@ -2825,6 +2865,7 @@ int main() {
binary_tree_example();
enum_example();
unsat_core_and_proof_example();
interpolation_example();
incremental_example1();
reference_counter_example();
smt2parser_example();

4
src/api/api_interp.cpp
View file

@ -289,7 +289,7 @@ extern "C" {
}
catch (z3_exception & ex) {
mk_c(c)->handle_exception(ex);
return Z3_L_UNDEF;
RETURN_Z3_compute_interpolant Z3_L_UNDEF;
}
}
@ -323,7 +323,7 @@ extern "C" {
*out_interp = of_ast_vector(v);
return status;
RETURN_Z3_compute_interpolant status;
Z3_CATCH_RETURN(Z3_L_UNDEF);
}