diff --git a/scripts/update_api.py b/scripts/update_api.py index 2ffd95e3d..837c2e1f4 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -281,8 +281,13 @@ def param2java(p): print("ERROR: unreachable code") assert(False) exit(1) - if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: + elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: return "%s[]" % type2java(param_type(p)) + elif k == OUT_MANAGED_ARRAY: + if param_type(p) == UINT: + return "UIntArrayPtr" + else: + return "ObjArrayPtr" else: return type2java(param_type(p)) @@ -529,6 +534,8 @@ def mk_java(): java_native.write(' public static class IntPtr { public int value; }\n') java_native.write(' public static class LongPtr { public long value; }\n') java_native.write(' public static class StringPtr { public String value; }\n') + java_native.write(' public static class ObjArrayPtr { public long[] value; }\n') + java_native.write(' public static class UIntArrayPtr { public int[] value; }\n') java_native.write(' public static native void setInternalErrorHandler(long ctx);\n\n') if IS_WINDOWS or os.uname()[0]=="CYGWIN": java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name) diff --git a/src/api/dotnet/InterpolationContext.cs b/src/api/dotnet/InterpolationContext.cs index 8ba5fe773..b5ada1bbd 100644 --- a/src/api/dotnet/InterpolationContext.cs +++ b/src/api/dotnet/InterpolationContext.cs @@ -153,10 +153,10 @@ namespace Microsoft.Z3 /// For more information on interpolation please refer /// too the function Z3_write_interpolation_problem in the C/C++ API, which is /// well documented. - public void WriteInterpolationProblem(string filename, Expr[] cnsts, uint[] parents, string error, Expr[] theory) + public void WriteInterpolationProblem(string filename, Expr[] cnsts, uint[] parents, Expr[] theory) { Contract.Requires(cnsts.Length == parents.Length); - Native.Z3_write_interpolation_problem(nCtx, (uint)cnsts.Length, Expr.ArrayToNative(cnsts), parents, error, (uint)theory.Length, Expr.ArrayToNative(theory)); + Native.Z3_write_interpolation_problem(nCtx, (uint)cnsts.Length, Expr.ArrayToNative(cnsts), parents, filename, (uint)theory.Length, Expr.ArrayToNative(theory)); } } } diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java new file mode 100644 index 000000000..067871324 --- /dev/null +++ b/src/api/java/InterpolationContext.java @@ -0,0 +1,169 @@ +/** + * + */ +package com.microsoft.z3; + +import java.util.Map; +import java.lang.String; + +import com.microsoft.z3.Native.IntPtr; +import com.microsoft.z3.Native.UIntArrayPtr; +import com.microsoft.z3.enumerations.Z3_lbool; + +/** + * The InterpolationContext is suitable for generation of interpolants. + * + * For more information on interpolation please refer + * too the C/C++ API, which is well documented. + **/ +public class InterpolationContext extends Context +{ + /** + * Constructor. + **/ + public InterpolationContext() throws Z3Exception + { + m_ctx = Native.mkInterpolationContext(0); + initContext(); + } + + /** + * Constructor. + * + * + **/ + public InterpolationContext(Map settings) throws Z3Exception + { + long cfg = Native.mkConfig(); + for (Map.Entry kv : settings.entrySet()) + Native.setParamValue(cfg, kv.getKey(), kv.getValue()); + m_ctx = Native.mkInterpolationContext(cfg); + Native.delConfig(cfg); + initContext(); + } + + /** + * Create an expression that marks a formula position for interpolation. + * @throws Z3Exception + **/ + public BoolExpr MkInterpolant(BoolExpr a) throws Z3Exception + { + checkContextMatch(a); + return new BoolExpr(this, Native.mkInterpolant(nCtx(), a.getNativeObject())); + } + + /** + * Computes an interpolant. + * For more information on interpolation please refer + * too the function Z3_get_interpolant in the C/C++ API, which is + * well documented. + * @throws Z3Exception + **/ + Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception + { + checkContextMatch(pf); + checkContextMatch(pat); + checkContextMatch(p); + + ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject())); + int n = seq.size(); + Expr[] res = new Expr[n]; + for (int i = 0; i < n; i++) + res[i] = Expr.create(this, seq.get(i).getNativeObject()); + return res; + } + + /** + * Computes an interpolant. + * For more information on interpolation please refer + * too the function Z3_compute_interpolant in the C/C++ API, which is + * well documented. + * @throws Z3Exception + **/ + Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception + { + checkContextMatch(pat); + checkContextMatch(p); + + Native.LongPtr n_i = new Native.LongPtr(); + Native.LongPtr n_m = new Native.LongPtr(); + int r = Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m); + interp = new ASTVector(this, n_i.value); + model = new Model(this, n_m.value); + return Z3_lbool.fromInt(r); + } + + /// + /// Return a string summarizing cumulative time used for interpolation. + /// + /// For more information on interpolation please refer + /// too the function Z3_interpolation_profile in the C/C++ API, which is + /// well documented. + public String InterpolationProfile() throws Z3Exception + { + return Native.interpolationProfile(nCtx()); + } + + /// + /// Checks the correctness of an interpolant. + /// + /// For more information on interpolation please refer + /// too the function Z3_check_interpolant in the C/C++ API, which is + /// well documented. + public int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory) throws Z3Exception + { + Native.StringPtr n_err_str = new Native.StringPtr(); + int r = Native.checkInterpolant(nCtx(), + cnsts.length, + Expr.arrayToNative(cnsts), + parents, + Expr.arrayToNative(interps), + n_err_str, + theory.length, + Expr.arrayToNative(theory)); + error = n_err_str.value; + return r; + } + + /// + /// Reads an interpolation problem from a file. + /// + /// For more information on interpolation please refer + /// too the function Z3_read_interpolation_problem in the C/C++ API, which is + /// well documented. + public int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception + { + 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(); + int r = 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; + error = n_err_str.value; + cnsts = new Expr[num]; + parents = new int[num]; + theory = new Expr[num_theory]; + for (int i = 0; i < num; i++) + { + cnsts[i] = Expr.create(this, n_cnsts.value[i]); + parents[i] = n_parents.value[i]; + } + for (int i = 0; i < num_theory; i++) + theory[i] = Expr.create(this, n_theory.value[i]); + return r; + } + + /// + /// Writes an interpolation problem to a file. + /// + /// For more information on interpolation please refer + /// too the function Z3_write_interpolation_problem in the C/C++ API, which is + /// well documented. + public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception + { + Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory)); + } +}