mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

fix java

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-19 15:49:28 -07:00
parent af96e42724
commit 9598045435
1 changed files with 27 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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();
// TBD: update to AstVector based API
Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr();
ASTVector _cnsts = new ASTVector(this);
ASTVector _theory = new ASTVector(this);
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.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]);
// 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;
}