mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

fix java API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-19 18:10:57 -07:00
parent ac2fe879ae
commit b002477d1a
1 changed files with 17 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

45
src/api/java/InterpolationContext.java
View file

@ -178,34 +178,23 @@ public class InterpolationContext extends Context
/// well documented. /// well documented.
public ReadInterpolationProblemResult ReadInterpolationProblem(String filename) public ReadInterpolationProblemResult ReadInterpolationProblem(String filename)
{ {
ReadInterpolationProblemResult res = new ReadInterpolationProblemResult(); ReadInterpolationProblemResult res = new ReadInterpolationProblemResult();
Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
ASTVector _cnsts = new ASTVector(this);
// TBD: update to AstVector based API ASTVector _theory = new ASTVector(this);
Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr(); Native.StringPtr n_err_str = new Native.StringPtr();
ASTVector _cnsts = new ASTVector(this); Native.IntPtr n_num = new Native.IntPtr();
ASTVector _theory = new ASTVector(this); res.return_value = Native.readInterpolationProblem(nCtx(), _cnsts.getNativeObject(), n_num,
Native.StringPtr n_err_str = new Native.StringPtr(); n_parents, filename, n_err_str, _theory.getNativeObject());
res.return_value = Native.readInterpolationProblem(nCtx(), _cnsts, n_parents, filename, n_err_str, _theory); res.error = n_err_str.value;
res.theory = _theory.ToExprArray();
// Native.IntPtr n_num = new Native.IntPtr(); res.cnsts = _cnsts.ToExprArray();
// Native.IntPtr n_num_theory = new Native.IntPtr(); int num = n_num.value;
// Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr(); res.parents = new int[num];
// for (int i = 0; i < num; i++) {
// int num = n_num.value; res.parents[i] = n_parents.value[i];
// int num_theory = _theory.n_num_theory.value; }
res.error = n_err_str.value; return res;
// 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;
} }
/// ///