From 13b19eb35120a59da2abd80112985174af031ea8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 7 Nov 2015 10:10:21 -0800
Subject: [PATCH] add translate facility to Java/C# APIs, request #209

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/dotnet/Solver.cs | 11 +++++++++++
 src/api/java/Solver.java |  8 ++++++++
 2 files changed, 19 insertions(+)

diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs
index 80ca7a0cd..c9e76e68e 100644
--- a/src/api/dotnet/Solver.cs
+++ b/src/api/dotnet/Solver.cs
@@ -290,6 +290,17 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Create a clone of the current solver with respect to <c>ctx</c>.
+        /// </summary>
+        public Solver Translate(Context ctx) 
+        {
+	     Contract.Requires(ctx != null);
+             Contract.Ensures(Contract.Result<Solver>() != null);
+             return new Solver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx));
+        }
+
+
         /// <summary>
         /// Solver statistics.
         /// </summary>
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index 4d2d9b641..f312da051 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -293,6 +293,14 @@ public class Solver extends Z3Object
                 getNativeObject());
     }
 
+    /**
+     * Create a clone of the current solver with respect to <c>ctx</c>.
+     */
+    public Solver translate(Context ctx) 
+    {
+	return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
+    }
+
     /**
      * Solver statistics.
      *