From b47851d7da0965e24e33c5c1d532776618e0698d Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 2 Apr 2015 16:51:30 +0100
Subject: [PATCH] Made GetInterpolant and ComputeInterpolant public in Java and
 .NET.

Fixes Codeplex discussion #616450
---
 src/api/dotnet/ASTVector.cs            | 2 +-
 src/api/dotnet/InterpolationContext.cs | 4 ++--
 src/api/java/ASTVector.java            | 2 +-
 src/api/java/InterpolationContext.java | 4 ++--
 4 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/api/dotnet/ASTVector.cs b/src/api/dotnet/ASTVector.cs
index 597b1decc..b70ff13b6 100644
--- a/src/api/dotnet/ASTVector.cs
+++ b/src/api/dotnet/ASTVector.cs
@@ -25,7 +25,7 @@ namespace Microsoft.Z3
     /// <summary>
     /// Vectors of ASTs.
     /// </summary>
-    internal class ASTVector : Z3Object
+    public class ASTVector : Z3Object
     {
         /// <summary>
         /// The size of the vector
diff --git a/src/api/dotnet/InterpolationContext.cs b/src/api/dotnet/InterpolationContext.cs
index 0f516c0b0..d54c8f634 100644
--- a/src/api/dotnet/InterpolationContext.cs
+++ b/src/api/dotnet/InterpolationContext.cs
@@ -47,7 +47,7 @@ namespace Microsoft.Z3
         /// <remarks>For more information on interpolation please refer
         /// too the function Z3_get_interpolant in the C/C++ API, which is 
         /// well documented.</remarks>
-        Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
+        public Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
         {
             Contract.Requires(pf != null);
             Contract.Requires(pat != null);
@@ -72,7 +72,7 @@ namespace Microsoft.Z3
         /// <remarks>For more information on interpolation please refer
         /// too the function Z3_compute_interpolant in the C/C++ API, which is 
         /// well documented.</remarks>
-        Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model)
+        public Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model)
         {
             Contract.Requires(pat != null);
             Contract.Requires(p != null);
diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java
index 48c079ecc..03e1b0a98 100644
--- a/src/api/java/ASTVector.java
+++ b/src/api/java/ASTVector.java
@@ -20,7 +20,7 @@ package com.microsoft.z3;
 /**
  * Vectors of ASTs.
  **/
-class ASTVector extends Z3Object
+public class ASTVector extends Z3Object
 {
     /**
      * The size of the vector
diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java
index 4c20ec6ae..91aac7f93 100644
--- a/src/api/java/InterpolationContext.java
+++ b/src/api/java/InterpolationContext.java
@@ -73,7 +73,7 @@ public class InterpolationContext extends Context
      * well documented.
      * @throws Z3Exception 
      **/
-    Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception
+    public Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception
     {
         checkContextMatch(pf);
         checkContextMatch(pat);
@@ -94,7 +94,7 @@ public class InterpolationContext extends Context
      * well documented.
      * @throws Z3Exception 
      **/
-    Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception
+    public Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception
     {
         checkContextMatch(pat);
         checkContextMatch(p);