From d66211c0078424af64b79c05c69dd4e7db4f99a3 Mon Sep 17 00:00:00 2001
From: Kenneth McMillan <mcmillan@Kenneth-McMillans-MacBook-Pro.local>
Date: Mon, 4 Mar 2013 23:48:01 -0800
Subject: [PATCH] working on interpolation API
---
src/api/api_interp.cpp | 10 +++++-----
src/api/z3_api.h | 27 +++++++++++++--------------
2 files changed, 18 insertions(+), 19 deletions(-)
diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index 2768e97e3..d32bf8b4e 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -54,8 +54,8 @@ extern "C" {
Z3_ast proof,
int num,
Z3_ast *cnsts,
- int *parents,
- Z3_interpolation_options options,
+ unsigned *parents,
+ Z3_params options,
Z3_ast *interps,
int num_theory,
Z3_ast *theory
@@ -92,7 +92,7 @@ extern "C" {
pre_parents_vec,
interpolants,
theory_vec,
- (interpolation_options) options);
+ 0); // ignore params for now FIXME
// copy result back
for(unsigned i = 0; i < interpolants.size(); i++)
@@ -104,8 +104,8 @@ extern "C" {
Z3_lbool Z3_interpolate(Z3_context ctx,
int num,
Z3_ast *cnsts,
- int *parents,
- Z3_interpolation_options options,
+ unsigned *parents,
+ Z3_params options,
Z3_ast *interps,
Z3_model *model,
Z3_literals *labels,
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 12db470fd..975b45940 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -7750,24 +7750,23 @@ END_MLAPI_EXCLUDE
are considered to have global scope (i.e., may appear in any
interpolant formula).
- def_API('Z3_interpolate', LBOOL, (_in(CONTEXT),), (_in(INT),), (_in_ptr(AST),),
- (_in_ptr(INT),), (_in(PARAMS),), (_in_ptr(AST),),
- (_out(MODEL),), (_out(LITERALS),), (_in(BOOL),), (_in(INT),), (_in_ptr(AST,0),))
+ def_API('Z3_interpolate', INT, (_in(CONTEXT), _in(INT), _in_array(1,AST), _in_array(1,UINT), _in(PARAMS), _out_array(1,AST), _out(MODEL), _out(LITERALS), _in(BOOL), _in(INT), _in_array(9,AST),))
+
*/
- Z3_lbool Z3_API Z3_interpolate(Z3_context ctx,
- int num,
- Z3_ast *cnsts,
- int *parents,
- Z3_interpolation_options options,
- Z3_ast *interps,
- Z3_model *model = 0,
- Z3_literals *labels = 0,
- bool incremental = false,
- int num_theory = 0,
- Z3_ast *theory = 0);
+ Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx,
+ __in int num,
+ __in_ecount(num) Z3_ast *cnsts,
+ __in_ecount(num) unsigned *parents,
+ __in Z3_params options,
+ __out_ecount(num-1) Z3_ast *interps,
+ __out Z3_model *model = 0,
+ __out Z3_literals *labels = 0,
+ __in bool incremental = false,
+ __in int num_theory = 0,
+ __in_ecount(num_theory) Z3_ast *theory = 0);
/** Return a string summarizing cumulative time used for
interpolation. This string is purely for entertainment purposes