Interpolation API bugfixes

Added Interpolation to the Java API

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

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)

src/api/dotnet/InterpolationContext.cs

@@ -153,10 +153,10 @@ namespace Microsoft.Z3
         /// <remarks>For more information on interpolation please refer
         /// too the function Z3_write_interpolation_problem in the C/C++ API, which is 
         /// well documented.</remarks>
-        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));
         }
     }
 }

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;
+
+/** <summary>
+ *  The InterpolationContext is suitable for generation of interpolants.
+ * </summary>
+ * <remarks>For more information on interpolation please refer
+ * too the C/C++ API, which is well documented.</remarks> 
+ **/
+public class InterpolationContext extends Context
+{
+    /**
+     * Constructor.
+     **/
+    public InterpolationContext() throws Z3Exception
+    {
+        m_ctx = Native.mkInterpolationContext(0);
+        initContext(); 
+    }
+
+    /** 
+     * Constructor.
+     *
+     * <remarks><seealso cref="Context.Context(Dictionary&lt;string, string&gt;)"/></remarks>
+     **/
+    public InterpolationContext(Map<String, String> settings) throws Z3Exception
+    { 
+        long cfg = Native.mkConfig();
+        for (Map.Entry<String, String> 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.
+     * <remarks>For more information on interpolation please refer
+     * too the function Z3_get_interpolant in the C/C++ API, which is 
+     * well documented.</remarks>
+     * @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.   
+     * <remarks>For more information on interpolation please refer
+     * too the function Z3_compute_interpolant in the C/C++ API, which is 
+     * well documented.</remarks>
+     * @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);
+    }
+
+    /// <summary> 
+    /// Return a string summarizing cumulative time used for interpolation.
+    /// </summary>    
+    /// <remarks>For more information on interpolation please refer
+    /// too the function Z3_interpolation_profile in the C/C++ API, which is 
+    /// well documented.</remarks>
+    public String InterpolationProfile() throws Z3Exception
+    {
+        return Native.interpolationProfile(nCtx());
+    }
+
+    /// <summary> 
+    /// Checks the correctness of an interpolant.
+    /// </summary>    
+    /// <remarks>For more information on interpolation please refer
+    /// too the function Z3_check_interpolant in the C/C++ API, which is 
+    /// well documented.</remarks>
+    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;
+    }
+
+    /// <summary> 
+    /// Reads an interpolation problem from a file.
+    /// </summary>    
+    /// <remarks>For more information on interpolation please refer
+    /// too the function Z3_read_interpolation_problem in the C/C++ API, which is 
+    /// well documented.</remarks>
+    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;
+    }
+
+    /// <summary> 
+    /// Writes an interpolation problem to a file.
+    /// </summary>    
+    /// <remarks>For more information on interpolation please refer
+    /// too the function Z3_write_interpolation_problem in the C/C++ API, which is 
+    /// well documented.</remarks>
+    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));     
+    }
+}