From 95980454359a7e2c8da1659fa3180e03f4259294 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Mar 2018 15:49:28 -0700 Subject: [PATCH] fix java Signed-off-by: Nikolaj Bjorner --- src/api/java/InterpolationContext.java | 49 ++++++++++++++------------ 1 file changed, 27 insertions(+), 22 deletions(-) diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 99a63821f..b285fe654 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -176,30 +176,35 @@ public class InterpolationContext extends Context /// Remarks: For more information on interpolation please refer /// too the function Z3_read_interpolation_problem in the C/C++ API, which is /// well documented. - public ReadInterpolationProblemResult ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) + public ReadInterpolationProblemResult ReadInterpolationProblem(String filename) { ReadInterpolationProblemResult res = new ReadInterpolationProblemResult(); - - Native.IntPtr n_num = new Native.IntPtr(); - Native.IntPtr n_num_theory = new Native.IntPtr(); - Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr(); - Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr(); - Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr(); - Native.StringPtr n_err_str = new Native.StringPtr(); - res.return_value = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory); - int num = n_num.value; - int num_theory = n_num_theory.value; - res.error = n_err_str.value; - res.cnsts = new Expr[num]; - res.parents = new int[num]; - theory = new Expr[num_theory]; - for (int i = 0; i < num; i++) - { - res.cnsts[i] = Expr.create(this, n_cnsts.value[i]); - res.parents[i] = n_parents.value[i]; - } - for (int i = 0; i < num_theory; i++) - res.theory[i] = Expr.create(this, n_theory.value[i]); + + +// TBD: update to AstVector based API + Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr(); + ASTVector _cnsts = new ASTVector(this); + ASTVector _theory = new ASTVector(this); + Native.StringPtr n_err_str = new Native.StringPtr(); + res.return_value = Native.readInterpolationProblem(nCtx(), _cnsts, n_parents, filename, n_err_str, _theory); + +// Native.IntPtr n_num = new Native.IntPtr(); +// Native.IntPtr n_num_theory = new Native.IntPtr(); +// Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr(); +// +// int num = n_num.value; +// int num_theory = _theory.n_num_theory.value; + res.error = n_err_str.value; +// res.cnsts = new Expr[num]; +// res.parents = new int[num]; +// theory = new Expr[num_theory]; +// for (int i = 0; i < num; i++) +// { +// res.cnsts[i] = Expr.create(this, n_cnsts.value[i]); +// res.parents[i] = n_parents.value[i]; +// } +// for (int i = 0; i < num_theory; i++) +// res.theory[i] = Expr.create(this, n_theory.value[i]); return res; }