From 3a692fe33c2992576ad381d050836a3b0913c996 Mon Sep 17 00:00:00 2001
From: "KangJing Huang (Chaserhkj)" <huangkangjing@gmail.com>
Date: Tue, 13 Jun 2017 00:25:36 -0400
Subject: [PATCH 1/2] Add translate method for FuncDecl in java api

---
 src/api/java/FuncDecl.java | 32 +++++++++++++++++++++++++-------
 1 file changed, 25 insertions(+), 7 deletions(-)

diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java
index 273e853c0..5909540b4 100644
--- a/src/api/java/FuncDecl.java
+++ b/src/api/java/FuncDecl.java
@@ -1,6 +1,6 @@
 /**
 Copyright (c) 2012-2014 Microsoft Corporation
-   
+
 Module Name:
 
     FuncDecl.java
@@ -12,8 +12,8 @@ Author:
     @author Christoph Wintersteiger (cwinter) 2012-03-15
 
 Notes:
-    
-**/ 
+
+**/
 
 package com.microsoft.z3;
 
@@ -59,6 +59,24 @@ public class FuncDecl extends AST
         return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
     }
 
+    /**
+     * Translates (copies) the AST to the Context {@code ctx}.
+     * @param ctx A context
+     *
+     * @return A copy of the AST which is associated with {@code ctx}
+     * @throws Z3Exception on error
+     **/
+    public FuncDecl translate(Context ctx)
+    {
+
+        if (getContext() == ctx) {
+            return this;
+        } else {
+            return new FuncDecl(ctx, Native.translate(getContext().nCtx(),
+                getNativeObject(), ctx.nCtx()));
+        }
+    }
+
     /**
      * The arity of the function declaration
      **/
@@ -68,7 +86,7 @@ public class FuncDecl extends AST
     }
 
     /**
-     * The size of the domain of the function declaration 
+     * The size of the domain of the function declaration
      * @see #getArity
      **/
     public int getDomainSize()
@@ -324,7 +342,7 @@ public class FuncDecl extends AST
     }
 
     FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
-           
+
     {
         super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(),
                 AST.arrayLength(domain), AST.arrayToNative(domain),
@@ -333,7 +351,7 @@ public class FuncDecl extends AST
     }
 
     FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range)
-           
+
     {
         super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix,
                 AST.arrayLength(domain), AST.arrayToNative(domain),
@@ -351,7 +369,7 @@ public class FuncDecl extends AST
     }
 
     /**
-     * Create expression that applies function to arguments. 
+     * Create expression that applies function to arguments.
      **/
     public Expr apply(Expr ... args)
     {

From 5799947183980eb440cfff243ca794e14872ce0b Mon Sep 17 00:00:00 2001
From: "KangJing Huang (Chaserhkj)" <huangkangjing@gmail.com>
Date: Tue, 13 Jun 2017 02:37:41 -0400
Subject: [PATCH 2/2] Fix docstrings for FuncDecl.translate

---
 src/api/java/FuncDecl.java | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java
index 5909540b4..8b1ad4b44 100644
--- a/src/api/java/FuncDecl.java
+++ b/src/api/java/FuncDecl.java
@@ -60,10 +60,10 @@ public class FuncDecl extends AST
     }
 
     /**
-     * Translates (copies) the AST to the Context {@code ctx}.
+     * Translates (copies) the function declaration to the Context {@code ctx}.
      * @param ctx A context
      *
-     * @return A copy of the AST which is associated with {@code ctx}
+     * @return A copy of the function declaration which is associated with {@code ctx}
      * @throws Z3Exception on error
      **/
     public FuncDecl translate(Context ctx)