From b002477d1af3e9dba06c9a113730f57555a3769c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Mar 2018 18:10:57 -0700 Subject: [PATCH] fix java API Signed-off-by: Nikolaj Bjorner --- src/api/java/InterpolationContext.java | 45 ++++++++++---------------- 1 file changed, 17 insertions(+), 28 deletions(-) diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index b285fe654..bce789807 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -178,34 +178,23 @@ public class InterpolationContext extends Context /// well documented. public ReadInterpolationProblemResult ReadInterpolationProblem(String filename) { - ReadInterpolationProblemResult res = new ReadInterpolationProblemResult(); - - -// 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; + ReadInterpolationProblemResult res = new ReadInterpolationProblemResult(); + 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(); + Native.IntPtr n_num = new Native.IntPtr(); + res.return_value = Native.readInterpolationProblem(nCtx(), _cnsts.getNativeObject(), n_num, + n_parents, filename, n_err_str, _theory.getNativeObject()); + res.error = n_err_str.value; + res.theory = _theory.ToExprArray(); + res.cnsts = _cnsts.ToExprArray(); + int num = n_num.value; + res.parents = new int[num]; + for (int i = 0; i < num; i++) { + res.parents[i] = n_parents.value[i]; + } + return res; } ///