mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

fixed logginf on return of Z3_compute_interpolant and added interpolation example to test_capi.c

Browse source
This commit is contained in:
Ken McMillan 2016-02-11 16:09:54 -08:00
parent 9ed7dadc02
commit 8b90bc9e91
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); 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 #define MAX_RETRACTABLE_ASSERTIONS 1024
/** /**
@ -2825,6 +2865,7 @@ int main() {
binary_tree_example(); binary_tree_example();
enum_example(); enum_example();
unsat_core_and_proof_example(); unsat_core_and_proof_example();
interpolation_example();
incremental_example1(); incremental_example1();
reference_counter_example(); reference_counter_example();
smt2parser_example(); smt2parser_example();

4
src/api/api_interp.cpp
View file

@ -289,7 +289,7 @@ extern "C" {
} }
catch (z3_exception & ex) { catch (z3_exception & ex) {
mk_c(c)->handle_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); *out_interp = of_ast_vector(v);
return status; RETURN_Z3_compute_interpolant status;
Z3_CATCH_RETURN(Z3_L_UNDEF); Z3_CATCH_RETURN(Z3_L_UNDEF);
} }