Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

.gitignore

@@ -48,4 +48,6 @@ src/api/dotnet/Native.cs
 src/api/python/z3consts.py
 src/api/python/z3core.py
 src/ast/pattern/database.h
-src/util/version.h
+src/util/version.h
+src/api/java/Z3Native.c
+src/api/java/Z3Native.java

doc/README

@@ -3,9 +3,20 @@ API documentation
 
 To generate the API documentation for the C, .NET and Python APIs, we must execute
 
-   python mk_doc.py
+   python mk_api_doc.py
 
 We must have doxygen installed in our system.
 
-The documentation will be stored in the subdirectory './html'.
-The main file is './html/index.html'
+The documentation will be stored in the subdirectory './api/html'.
+The main file is './api/html/index.html'
+
+Code documentation
+------------------
+
+To generate documentation for the Z3 code, we must execute
+
+   doxygen z3code.dox
+
+The documentation will be store in the subdirectory './code/html'.
+The main file is './code/html/index.html'
+

doc/mk_api_doc.py

@@ -21,7 +21,7 @@ def cleanup_API(inf, outf):
             _outf.write(line)
 
 try:
-    mk_dir('html')
+    mk_dir('api/html')
     cleanup_API('../src/api/z3_api.h', 'z3_api.h')
     print "Removed annotations from z3_api.h."
     DEVNULL = open(os.devnull, 'wb')
@@ -33,15 +33,15 @@ try:
     print "Generated C and .NET API documentation."
     os.remove('z3_api.h')
     print "Removed temporary file z3_api.h."
-    shutil.copy('z3.css', 'html/z3.css')
+    shutil.copy('z3.css', 'api/html/z3.css')
     print "Copied z3.css."
-    shutil.copy('z3.png', 'html/z3.png')
+    shutil.copy('z3.png', 'api/html/z3.png')
     print "Copied z3.png."
     sys.path.append('../src/api/python')
     pydoc.writedoc('z3')
-    shutil.move('z3.html', 'html/z3.html')
+    shutil.move('z3.html', 'api/html/z3.html')
     print "Generated Python documentation."
-    print "Documentation was successfully generated at subdirectory './html'."
+    print "Documentation was successfully generated at subdirectory './api/html'."
 except:
     print "ERROR: failed to generate documentation"
     exit(1)

doc/update_website.cmd

@@ -1,4 +1,4 @@
 REM Script for updating the website containing the Z3 API documentation.
 REM You must be inside the Microsoft network to execute this script, and 
 REM robocopy must be in your PATH.
-robocopy /S html \\research\root\web\external\en-us\UM\redmond\projects\z3
+robocopy /S api\html \\research\root\web\external\en-us\UM\redmond\projects\z3

doc/z3.dox

@@ -38,7 +38,7 @@ PROJECT_NUMBER         =
 # If a relative path is entered, it will be relative to the location
 # where doxygen was started. If left blank the current directory will be used.
 
-OUTPUT_DIRECTORY       = .
+OUTPUT_DIRECTORY       = api
 
 # If the CREATE_SUBDIRS tag is set to YES, then doxygen will create
 # 4096 sub-directories (in 2 levels) under the output directory of each output

scripts/update_api.py

@@ -252,11 +252,11 @@ def param2java(p):
     k = param_kind(p)
     if k == OUT:
         if param_type(p) == INT or param_type(p) == UINT:
-            return "IntPtr"
+            return "Integer"
         elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) >= FIRST_OBJ_ID:
-            return "LongPtr"
+            return "Long"
         elif param_type(p) == STRING:
-            return "StringPtr"
+            return "String"
         else:
             print "ERROR: unreachable code"
             assert(False)
@@ -496,14 +496,17 @@ def mk_java():
     if not is_java_enabled():
         return
     java_dir      = get_component('java').src_dir
-    java_nativef  = '%s/Z3Native.java' % java_dir
-    java_wrapperf = '%s/Z3Native.c' % java_dir 
+    try:
+        os.mkdir('%s/com/Microsoft/Z3/' % java_dir)
+    except:
+        pass # OK if it exists already.
+    java_nativef  = '%s/com/Microsoft/Z3/Native.java' % java_dir
+    java_wrapperf = '%s/com/Microsoft/Z3/Native.c' % java_dir 
     java_native   = open(java_nativef, 'w')
     java_native.write('// Automatically generated file\n')
-    java_native.write('public final class Z3Native {\n')
-    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('package com.Microsoft.Z3;\n')
+    java_native.write('public final class Native {\n')
+
     if is_windows():
         java_native.write('  static { System.loadLibrary("%s"); }\n' % get_component('java'))
     else:
@@ -521,9 +524,9 @@ def mk_java():
             i = i + 1
         java_native.write(');\n')
     java_native.write('  public static void main(String[] args) {\n')
-    java_native.write('     IntPtr major = new IntPtr(), minor = new IntPtr(), build = new IntPtr(), revision = new IntPtr();\n')
+    java_native.write('     Integer major = 0, minor = 0, build = 0, revision = 0;\n')
     java_native.write('     getVersion(major, minor, build, revision);\n')
-    java_native.write('     System.out.format("Z3 (for Java) %d.%d.%d%n", major.value, minor.value, build.value);\n')
+    java_native.write('     System.out.format("Z3 (for Java) %d.%d.%d%n", major, minor, build);\n')
     java_native.write('  }\n')
     java_native.write('}\n');
     java_wrapper = open(java_wrapperf, 'w')

src/api/api_arith.cpp

@@ -101,27 +101,14 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
-        if (mk_c(c)->fparams().m_pre_simplify_expr) {
-            // Do not use logging here... the function is implemented using API primitives
-            Z3_ast m1 = Z3_mk_int(c, -1, Z3_get_sort(c, args[0]));
-            Z3_ast args1[2] = { args[0], 0 };
-            for (unsigned i = 1; i < num_args; ++i) {
-                Z3_ast args2[3] = { m1, args[i] };
-                args1[1] = Z3_mk_mul(c, 2, args2);
-                args1[0] = Z3_mk_add(c, 2, args1);
-            }
-            RETURN_Z3(args1[0]);
-        }
-        else {
-            expr* r = to_expr(args[0]);
-            for (unsigned i = 1; i < num_args; ++i) {
-                expr* args1[2] = { r, to_expr(args[i]) };
-                r = mk_c(c)->m().mk_app(mk_c(c)->get_arith_fid(), OP_SUB, 0, 0, 2, args1);
-                check_sorts(c, r);
-            }
-            mk_c(c)->save_ast_trail(r);
-            RETURN_Z3(of_expr(r));
+        expr* r = to_expr(args[0]);
+        for (unsigned i = 1; i < num_args; ++i) {
+            expr* args1[2] = { r, to_expr(args[i]) };
+            r = mk_c(c)->m().mk_app(mk_c(c)->get_arith_fid(), OP_SUB, 0, 0, 2, args1);
+            check_sorts(c, r);
         }
+        mk_c(c)->save_ast_trail(r);
+        RETURN_Z3(of_expr(r));
         Z3_CATCH_RETURN(0);
     }
 
@@ -129,12 +116,6 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_unary_minus(c, n);
         RESET_ERROR_CODE();
-        if (mk_c(c)->fparams().m_pre_simplify_expr) {
-            Z3_ast m1 = Z3_mk_int(c, -1, Z3_get_sort(c, n));
-            Z3_ast args[2] = { m1, n };
-            Z3_ast r = Z3_mk_mul(c, 2, args);
-            RETURN_Z3(r);
-        }
         MK_UNARY_BODY(Z3_mk_unary_minus, mk_c(c)->get_arith_fid(), OP_UMINUS, SKIP);
         Z3_CATCH_RETURN(0);
     }

src/api/api_bv.cpp

@@ -280,12 +280,6 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) {                \
         Z3_TRY;
         LOG_Z3_mk_bvsub(c, n1, n2);
         RESET_ERROR_CODE();
-        // TODO: Do we really need this pre_simplifier hack?
-        if (mk_c(c)->fparams().m_pre_simplify_expr) {
-            Z3_ast m1 = Z3_mk_int(c, -1, Z3_get_sort(c, n2));
-            Z3_ast r = Z3_mk_bvadd(c, n1, Z3_mk_bvmul(c, m1, n2));
-            RETURN_Z3(r);
-        }
         MK_BINARY_BODY(Z3_mk_bvsub, mk_c(c)->get_bv_fid(), OP_BSUB, SKIP);
         Z3_CATCH_RETURN(0);
     }
@@ -294,12 +288,6 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) {                \
         Z3_TRY;
         LOG_Z3_mk_bvneg(c, n);
         RESET_ERROR_CODE();
-        // TODO: Do we really need this pre_simplifier hack? 
-        if (mk_c(c)->fparams().m_pre_simplify_expr) {
-            Z3_ast m1 = Z3_mk_int(c, -1, Z3_get_sort(c, n));
-            Z3_ast r  = Z3_mk_bvmul(c, m1, n);
-            RETURN_Z3(r);
-        }
         MK_UNARY_BODY(Z3_mk_bvneg, mk_c(c)->get_bv_fid(), OP_BNEG, SKIP);
         Z3_CATCH_RETURN(0);
     }

src/api/dotnet/ASTVector.cs

@@ -51,7 +51,7 @@ namespace Microsoft.Z3
             }
             set
             {
-                Contract.Requires(value!= null);
+                Contract.Requires(value != null);
 
                 Native.Z3_ast_vector_set(Context.nCtx, NativeObject, i, value.NativeObject);
             }

src/api/dotnet/Version.cs

@@ -22,77 +22,77 @@ using System.Diagnostics.Contracts;
 
 namespace Microsoft.Z3
 {
-  /// <summary>
-  /// Version information.
-  /// </summary>
-  /// <remarks>Note that this class is static.</remarks>
+    /// <summary>
+    /// Version information.
+    /// </summary>
+    /// <remarks>Note that this class is static.</remarks>
     [ContractVerification(true)]
     public static class Version
-  {
-    static Version() { }
-
-    /// <summary>
-    /// The major version
-    /// </summary>
-    public static uint Major
     {
-      get
-      {
-        uint major = 0, minor = 0, build = 0, revision = 0;
-        Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
-        return major;
-      }
-    }
+        static Version() { }
 
-    /// <summary>
-    /// The minor version
-    /// </summary>
-    public static uint Minor
-    {
-      get
-      {
-        uint major = 0, minor = 0, build = 0, revision = 0;
-        Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
-        return minor;
-      }
-    }
+        /// <summary>
+        /// The major version
+        /// </summary>
+        public static uint Major
+        {
+            get
+            {
+                uint major = 0, minor = 0, build = 0, revision = 0;
+                Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
+                return major;
+            }
+        }
 
-    /// <summary>
-    /// The build version
-    /// </summary>
-    public static uint Build
-    {
-      get
-      {
-        uint major = 0, minor = 0, build = 0, revision = 0;
-        Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
-        return build;
-      }
-    }
+        /// <summary>
+        /// The minor version
+        /// </summary>
+        public static uint Minor
+        {
+            get
+            {
+                uint major = 0, minor = 0, build = 0, revision = 0;
+                Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
+                return minor;
+            }
+        }
 
-    /// <summary>
-    /// The revision
-    /// </summary>
-    public static uint Revision
-    {
-      get
-      {
-        uint major = 0, minor = 0, build = 0, revision = 0;
-        Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
-        return revision;
-      }
-    }
+        /// <summary>
+        /// The build version
+        /// </summary>
+        public static uint Build
+        {
+            get
+            {
+                uint major = 0, minor = 0, build = 0, revision = 0;
+                Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
+                return build;
+            }
+        }
 
-    /// <summary>
-    /// A string representation of the version information.
-    /// </summary>
-    new public static string ToString()
-    {
-        Contract.Ensures(Contract.Result<string>() != null);
+        /// <summary>
+        /// The revision
+        /// </summary>
+        public static uint Revision
+        {
+            get
+            {
+                uint major = 0, minor = 0, build = 0, revision = 0;
+                Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
+                return revision;
+            }
+        }
 
-      uint major = 0, minor = 0, build = 0, revision = 0;
-      Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
-      return major.ToString() + "." + minor.ToString() + "." + build.ToString() + "." + revision.ToString();
+        /// <summary>
+        /// A string representation of the version information.
+        /// </summary>
+        new public static string ToString()
+        {
+            Contract.Ensures(Contract.Result<string>() != null);
+
+            uint major = 0, minor = 0, build = 0, revision = 0;
+            Native.Z3_get_version(ref major, ref minor, ref build, ref revision);
+            return major.ToString() + "." + minor.ToString() + "." + build.ToString() + "." + revision.ToString();
+        }
     }
-  }
 }

src/api/java/com/Microsoft/Z3/AST.java

@@ -0,0 +1,209 @@
+/**
+ * This file was automatically generated from AST.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+/* using System.Collections; */
+/* using System.Collections.Generic; */
+
+    /**
+     * The abstract syntax tree (AST) class. 
+     **/
+    public class AST extends Z3Object
+    {
+        /**
+         * Comparison operator.
+         * <param name="a">An AST</param>
+         * <param name="b">An AST</param>
+         * @return True if <paramref name="a"/> and <paramref name="b"/> are from the same context 
+         * and represent the same sort; false otherwise.
+         **/
+         /* Overloaded operators are not translated. */
+
+        /**
+         * Comparison operator.
+         * <param name="a">An AST</param>
+         * <param name="b">An AST</param>
+         * @return True if <paramref name="a"/> and <paramref name="b"/> are not from the same context 
+         * or represent different sorts; false otherwise.
+         **/
+         /* Overloaded operators are not translated. */
+
+        /**
+         * Object comparison.
+         **/
+        public boolean Equals(object o)
+        {
+            AST casted = (AST) o;
+            if (casted == null) return false;
+            return this == casted;
+        }
+
+        /**
+         * Object Comparison.
+         * <param name="other">Another AST</param>
+         * @return Negative if the object should be sorted before <paramref name="other"/>, positive if after else zero.
+         **/
+        public int CompareTo(object other)
+        {
+            if (other == null) return 1;
+            AST oAST = (AST) other;
+            if (oAST == null)
+                return 1;
+            else
+            {
+                if (Id < oAST.Id)
+                    return -1;
+                else if (Id > oAST.Id)
+                    return +1;
+                else
+                    return 0;
+            }
+        }
+
+        /**
+         * The AST's hash code.
+         * @return A hash code
+         **/
+        public int GetHashCode()
+        {
+            return (int)Native.getAstHash(Context.nCtx, NativeObject);
+        }
+
+        /**
+         * A unique identifier for the AST (unique among all ASTs).
+         **/
+        public Integer Id()  { return Native.getAstId(Context.nCtx, NativeObject); }
+
+        /**
+         * Translates (copies) the AST to the Context <paramref name="ctx"/>.
+         * <param name="ctx">A context</param>
+         * @return A copy of the AST which is associated with <paramref name="ctx"/>
+         **/
+        public AST Translate(Context ctx)
+        {
+            
+            
+
+            if (ReferenceEquals(Context, ctx))
+                return this;
+            else
+                return new AST(ctx, Native.translate(Context.nCtx, NativeObject, ctx.nCtx));
+        }
+
+        /**
+         * The kind of the AST.
+         **/
+        public Z3_ast_kind ASTKind()  { return (Z3AstKind)Native.getAstKind(Context.nCtx, NativeObject); }
+
+        /**
+         * Indicates whether the AST is an Expr
+         **/
+        public boolean IsExpr() 
+            {
+                switch (ASTKind)
+                {
+                    case Z3AstKind.Z3APPAST:
+                    case Z3AstKind.Z3NUMERALAST:
+                    case Z3AstKind.Z3QUANTIFIERAST:
+                    case Z3AstKind.Z3VARAST: return true;
+                    default: return false;
+            }
+        }
+
+        /**
+         * Indicates whether the AST is a BoundVariable
+         **/
+        public boolean IsVar()  { return this.ASTKind == Z3AstKind.Z3VARAST; }
+
+        /**
+         * Indicates whether the AST is a Quantifier
+         **/
+        public boolean IsQuantifier()  { return this.ASTKind == Z3AstKind.Z3QUANTIFIERAST; }
+
+        /**
+         * Indicates whether the AST is a Sort
+         **/
+        public boolean IsSort()  { return this.ASTKind == Z3AstKind.Z3SORTAST; }
+
+        /**
+         * Indicates whether the AST is a FunctionDeclaration
+         **/
+        public boolean IsFuncDecl()  { return this.ASTKind == Z3AstKind.Z3FUNCDECLAST; }
+
+        /**
+         * A string representation of the AST.
+         **/
+        public String toString()
+        {
+            return Native.asttoString(Context.nCtx, NativeObject);
+        }
+
+        /**
+         * A string representation of the AST in s-expression notation.
+         **/
+        public String SExpr()
+        {
+            
+
+            return Native.asttoString(Context.nCtx, NativeObject);
+        }
+
+        AST(Context ctx) { super(ctx);  }
+        AST(Context ctx, IntPtr obj) { super(ctx, obj);  }
+
+        class DecRefQueue extends Z3.DecRefQueue
+        {
+            public void IncRef(Context ctx, IntPtr obj)
+            {
+                Native.incRef(ctx.nCtx, obj);
+            }
+
+            public void DecRef(Context ctx, IntPtr obj)
+            {
+                Native.decRef(ctx.nCtx, obj);
+            }
+        };        
+
+        void IncRef(IntPtr o)
+        {            
+            // Console.WriteLine("AST IncRef()");
+            if (Context == null)
+                throw new Z3Exception("inc() called on null context");
+            if (o == IntPtr.Zero)
+                throw new Z3Exception("inc() called on null AST");
+            Context.ASTDRQ.IncAndClear(Context, o);
+            super.IncRef(o);
+        }
+
+        void DecRef(IntPtr o)
+        {
+            // Console.WriteLine("AST DecRef()");
+            if (Context == null)
+                throw new Z3Exception("dec() called on null context");
+            if (o == IntPtr.Zero)
+                throw new Z3Exception("dec() called on null AST");
+            Context.ASTDRQ.Add(o);
+            super.DecRef(o);
+        }
+
+        static AST Create(Context ctx, IntPtr obj)
+        {
+            
+            
+
+            switch ((Z3AstKind)Native.getAstKind(ctx.nCtx, obj))
+            {
+                case Z3AstKind.Z3FUNCDECLAST: return new FuncDecl(ctx, obj);
+                case Z3AstKind.Z3QUANTIFIERAST: return new Quantifier(ctx, obj);
+                case Z3AstKind.Z3SORTAST: return Sort.Create(ctx, obj);
+                case Z3AstKind.Z3APPAST:
+                case Z3AstKind.Z3NUMERALAST:
+                case Z3AstKind.Z3VARAST: return Expr.Create(ctx, obj);
+                default:
+                    throw new Z3Exception("Unknown AST kind");
+            }
+        }
+    }

src/api/java/com/Microsoft/Z3/ASTMap.java

@@ -0,0 +1,127 @@
+/**
+ * This file was automatically generated from ASTMap.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * Map from AST to AST
+     **/
+    class ASTMap extends Z3Object
+    {
+        /**
+         * Checks whether the map contains the key <paramref name="k"/>.
+         * <param name="k">An AST</param>
+         * @return True if <paramref name="k"/> is a key in the map, false otherwise.
+         **/
+        public boolean Contains(AST k)
+        {
+            
+
+            return Native.astMapContains(Context.nCtx, NativeObject, k.NativeObject) != 0;
+        }
+
+        /**
+         * Finds the value associated with the key <paramref name="k"/>.
+         * <remarks>
+         * This function signs an error when <paramref name="k"/> is not a key in the map.
+         * </remarks>
+         * <param name="k">An AST</param>    
+         **/
+        public AST Find(AST k)
+        {
+            
+            
+
+            return new AST(Context, Native.astMapFind(Context.nCtx, NativeObject, k.NativeObject));
+        }
+
+        /**
+         * Stores or replaces a new key/value pair in the map.
+         * <param name="k">The key AST</param>
+         * <param name="v">The value AST</param>
+         **/
+        public void Insert(AST k, AST v)
+        {
+            
+            
+
+            Native.astMapInsert(Context.nCtx, NativeObject, k.NativeObject, v.NativeObject);
+        }
+
+        /**
+         * Erases the key <paramref name="k"/> from the map.
+         * <param name="k">An AST</param>
+         **/
+        public void Erase(AST k)
+        {
+            
+
+            Native.astMapErase(Context.nCtx, NativeObject, k.NativeObject);
+        }
+
+        /**
+         * Removes all keys from the map.
+         **/
+        public void Reset()
+        {
+            Native.astMapReset(Context.nCtx, NativeObject);
+        }
+
+        /**
+         * The size of the map
+         **/
+        public Integer Size()  { return Native.astMapSize(Context.nCtx, NativeObject); }
+
+        /**
+         * The keys stored in the map.
+         **/
+        public ASTVector Keys() 
+            {
+                return new ASTVector(Context, Native.astMapKeys(Context.nCtx, NativeObject));
+        }
+
+        /**
+         * Retrieves a string representation of the map. 
+         **/
+        public String toString()
+        {
+            return Native.astMaptoString(Context.nCtx, NativeObject);
+        }
+
+        ASTMap(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+        ASTMap(Context ctx)
+            { super(ctx, Native.mkAstMap(ctx.nCtx));
+            
+        }
+
+        class DecRefQueue extends Z3.DecRefQueue
+        {
+            public void IncRef(Context ctx, IntPtr obj)
+            {
+                Native.astMapIncRef(ctx.nCtx, obj);
+            }
+
+            public void DecRef(Context ctx, IntPtr obj)
+            {
+                Native.astMapDecRef(ctx.nCtx, obj);
+            }
+        };
+
+        void IncRef(IntPtr o)
+        {
+            Context.ASTMapDRQ.IncAndClear(Context, o);
+            super.IncRef(o);
+        }
+
+        void DecRef(IntPtr o)
+        {
+            Context.ASTMapDRQ.Add(o);
+            super.DecRef(o);
+        }
+    }

src/api/java/com/Microsoft/Z3/ASTVector.java

@@ -0,0 +1,107 @@
+/**
+ * This file was automatically generated from ASTVector.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * Vectors of ASTs.
+     **/
+    class ASTVector extends Z3Object
+    {
+        /**
+         * The size of the vector
+         **/
+        public Integer Size()  { return Native.astVectorSize(Context.nCtx, NativeObject); }
+
+        /**
+         * Retrieves the i-th object in the vector.
+         * <remarks>May throw an IndexOutOfBoundsException when <paramref name="i"/> is out of range.</remarks>
+         * <param name="i">Index</param>
+         * @return An AST
+         **/
+        public AST this[Integer i]() 
+            {
+                
+
+                return new AST(Context, Native.astVectorGet(Context.nCtx, NativeObject, i));
+            set
+            {
+                
+
+                Native.astVectorSet(Context.nCtx, NativeObject, i, value.NativeObject);
+            }
+        }
+
+        /**
+         * Resize the vector to <paramref name="newSize"/>.
+         * <param name="newSize">The new size of the vector.</param>
+         **/
+        public void Resize(Integer newSize)
+        {
+            Native.astVectorResize(Context.nCtx, NativeObject, newSize);
+        }
+
+        /**
+         * Add the AST <paramref name="a"/> to the back of the vector. The size
+         * is increased by 1.
+         * <param name="a">An AST</param>
+         **/
+        public void Push(AST a)
+        {
+            
+
+            Native.astVectorPush(Context.nCtx, NativeObject, a.NativeObject);
+        }
+
+        /**
+         * Translates all ASTs in the vector to <paramref name="ctx"/>.
+         * <param name="ctx">A context</param>
+         * @return A new ASTVector
+         **/
+        public ASTVector Translate(Context ctx)
+        {
+            
+            
+
+            return new ASTVector(Context, Native.astVectorTranslate(Context.nCtx, NativeObject, ctx.nCtx));
+        }
+
+        /**
+         * Retrieves a string representation of the vector. 
+         **/
+        public String toString()
+        {
+            return Native.astVectortoString(Context.nCtx, NativeObject);
+        }
+
+        ASTVector(Context ctx, IntPtr obj) { super(ctx, obj);  }
+        ASTVector(Context ctx) { super(ctx, Native.mkAstVector(ctx.nCtx));  }
+
+        class DecRefQueue extends Z3.DecRefQueue
+        {
+            public void IncRef(Context ctx, IntPtr obj)
+            {
+                Native.astVectorIncRef(ctx.nCtx, obj);
+            }
+
+            public void DecRef(Context ctx, IntPtr obj)
+            {
+                Native.astVectorDecRef(ctx.nCtx, obj);
+            }
+        };
+
+        void IncRef(IntPtr o)
+        {
+            Context.ASTVectorDRQ.IncAndClear(Context, o);
+            super.IncRef(o);
+        }
+
+        void DecRef(IntPtr o)
+        {
+            Context.ASTVectorDRQ.Add(o);
+            super.DecRef(o);
+        }
+    }

src/api/java/com/Microsoft/Z3/ApplyResult.java

@@ -0,0 +1,84 @@
+/**
+ * This file was automatically generated from ApplyResult.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * ApplyResult objects represent the result of an application of a 
+     * tactic to a goal. It contains the subgoals that were produced.
+     **/
+    public class ApplyResult extends Z3Object
+    {
+        /**
+         * The number of Subgoals.
+         **/
+        public Integer NumSubgoals()  { return Native.applyResultGetNumSubgoals(Context.nCtx, NativeObject); }
+
+        /**
+         * Retrieves the subgoals from the ApplyResult.
+         **/
+        public Goal[] Subgoals() 
+            {
+              
+              
+
+                Integer n = NumSubgoals;
+                Goal[] res = new Goal[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = new Goal(Context, Native.applyResultGetSubgoal(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        /**
+         * Convert a model for the subgoal <paramref name="i"/> into a model for the original 
+         * goal <code>g</code>, that the ApplyResult was obtained from. 
+         * @return A model for <code>g</code>
+         **/
+        public Model ConvertModel(Integer i, Model m)
+        {
+            
+            
+
+            return new Model(Context, Native.applyResultConvertModel(Context.nCtx, NativeObject, i, m.NativeObject));
+        }
+
+        /**
+         * A string representation of the ApplyResult.
+         **/
+        public String toString()
+        {
+            return Native.applyResulttoString(Context.nCtx, NativeObject);
+        }
+
+        ApplyResult(Context ctx, IntPtr obj) { super(ctx, obj); 
+            
+        }
+
+        class DecRefQueue extends Z3.DecRefQueue
+        {
+            public void IncRef(Context ctx, IntPtr obj)
+            {
+                Native.applyResultIncRef(ctx.nCtx, obj);
+            }
+
+            public void DecRef(Context ctx, IntPtr obj)
+            {
+                Native.applyResultDecRef(ctx.nCtx, obj);
+            }
+        };        
+
+        void IncRef(IntPtr o)
+        {
+            Context.ApplyResultDRQ.IncAndClear(Context, o);
+            super.IncRef(o);
+        }
+
+        void DecRef(IntPtr o)
+        {
+            Context.ApplyResultDRQ.Add(o);
+            super.DecRef(o);
+        }
+    }

src/api/java/com/Microsoft/Z3/Constructor.java

@@ -0,0 +1,130 @@
+/**
+ * This file was automatically generated from Constructor.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * Constructors are used for datatype sorts.
+     **/
+    public class Constructor extends Z3Object
+    {
+        /**
+         * The number of fields of the constructor.
+         **/
+        public Integer NumFields()  { init();  return n; }
+
+        /**
+         * The function declaration of the constructor.
+         **/
+        public FuncDecl ConstructorDecl()  {
+                
+                init();  return mConstructorDecl; }
+
+        /**
+         * The function declaration of the tester.
+         **/
+        public FuncDecl TesterDecl()  {
+                
+                init();  return mTesterDecl; }
+
+        /**
+         * The function declarations of the accessors
+         **/
+        public FuncDecl[] AccessorDecls()  {
+                
+                init();  return mAccessorDecls; }
+
+        /**
+         * Destructor.
+         **/
+        protected void finalize()
+        {
+            Native.delConstructor(Context.nCtx, NativeObject);
+        }
+
+
+        private void ObjectInvariant()
+        {
+            
+            
+        }
+        
+
+        private Integer n = 0;
+        private FuncDecl mTesterDecl = null;
+        private FuncDecl mConstructorDecl = null;
+        private FuncDecl[] mAccessorDecls = null;
+
+        Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames,
+                             Sort[] sorts, Integer[] sortRefs)
+            { super(ctx);
+            
+            
+            
+
+            n = AST.ArrayLength(fieldNames);
+
+            if (n != AST.ArrayLength(sorts))
+                throw new Z3Exception("Number of field names does not match number of sorts");
+            if (sortRefs != null && sortRefs.Length != n)
+                throw new Z3Exception("Number of field names does not match number of sort refs");
+            
+            if (sortRefs == null) sortRefs = new Integer[n];
+
+            NativeObject = Native.mkConstructor(ctx.nCtx, name.NativeObject, recognizer.NativeObject,
+                                                    n,
+                                                    Symbol.ArrayToNative(fieldNames),
+                                                    Sort.ArrayToNative(sorts),
+                                                    sortRefs);
+
+        }
+
+        private void init() 
+        {
+            
+            
+            
+
+            if (mTesterDecl != null) return;
+            IntPtr constructor = IntPtr.Zero;
+            IntPtr tester = IntPtr.Zero;
+            IntPtr[] accessors = new IntPtr[n];
+            Native.queryConstructor(Context.nCtx, NativeObject, n, constructor, tester, accessors);
+            mConstructorDecl = new FuncDecl(Context, constructor);
+            mTesterDecl = new FuncDecl(Context, tester);
+            mAccessorDecls = new FuncDecl[n];
+            for (Integer i = 0; i < n; i++)
+                mAccessorDecls[i] = new FuncDecl(Context, accessors[i]);
+        }
+
+    }
+
+    /**
+     * Lists of constructors
+     **/
+    public class ConstructorList extends Z3Object
+    {
+        /**
+         * Destructor.
+         **/
+        protected void finalize()
+        {         
+            Native.delConstructorList(Context.nCtx, NativeObject);
+        }
+
+        ConstructorList(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+
+        ConstructorList(Context ctx, Constructor[] constructors)
+            { super(ctx);
+            
+            
+
+            NativeObject = Native.mkConstructorList(Context.nCtx, (Integer)constructors.Length, Constructor.ArrayToNative(constructors));
+        }        
+    }

src/api/java/com/Microsoft/Z3/DecRefQUeue.java

@@ -0,0 +1,50 @@
+/**
+ * This file was automatically generated from DecRefQUeue.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+/* using System.Collections; */
+/* using System.Collections.Generic; */
+/* using System.Threading; */
+
+    abstract class DecRefQueue
+
+        private void ObjectInvariant()
+            
+        
+
+        readonly protected Object mLock = new Object();
+        readonly protected List<IntPtr> mQueue = new List<IntPtr>();
+        const Integer mMoveLimit = 1024;
+
+        public abstract void IncRef(Context ctx, IntPtr obj);
+        public abstract void DecRef(Context ctx, IntPtr obj);
+
+        public void IncAndClear(Context ctx, IntPtr o)
+            
+
+            IncRef(ctx, o);
+            if (mQueue.Count >= mMoveLimit) Clear(ctx);
+
+        public void Add(IntPtr o)
+            if (o == IntPtr.Zero) return;
+
+            lock (mLock)
+                mQueue.Add(o);
+
+        public void Clear(Context ctx)
+            
+
+            lock (mLock)
+                for (IntPtr.Iterator o = mQueue.iterator(); o.hasNext(); )
+                    DecRef(ctx, o);
+                mQueue.Clear();
+
+    abstract class DecRefQueueContracts : DecRefQueue
+        public void IncRef(Context ctx, IntPtr obj)
+            
+
+        public void DecRef(Context ctx, IntPtr obj)
+            

src/api/java/com/Microsoft/Z3/Expr.java

@@ -0,0 +1,428 @@
+/**
+ * This file was automatically generated from Expr.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * Expressions are terms.     
+     **/
+    public class Expr extends AST
+    {
+        /**
+         * Returns a simplified version of the expression.
+         * <param name="p">A set of parameters to configure the simplifier</param>
+         * <seealso cref="Context.SimplifyHelp"/>
+         **/
+        public Expr Simplify(Params p)
+        {
+            
+
+            if (p == null)
+                return Expr.Create(Context, Native.simplify(Context.nCtx, NativeObject));
+            else
+                return Expr.Create(Context, Native.simplifyEx(Context.nCtx, NativeObject, p.NativeObject));
+        }
+
+        /**
+         * The function declaration of the function that is applied in this expression.
+         **/
+        public FuncDecl FuncDecl()  {
+                
+                return new FuncDecl(Context, Native.getAppDecl(Context.nCtx, NativeObject)); }
+
+        /**
+         * Indicates whether the expression is the true or false expression
+         * or something else (Z3_L_UNDEF).
+         **/
+        public Z3_lboolean BoolValue()  { return (Z3Lboolean)Native.getBooleanValue(Context.nCtx, NativeObject); }
+
+        /**
+         * The number of arguments of the expression.
+         **/
+        public Integer NumArgs()  { return Native.getAppNumArgs(Context.nCtx, NativeObject); }
+
+        /**
+         * The arguments of the expression.
+         **/
+        public Expr[] Args() 
+            {
+                
+
+                Integer n = NumArgs;
+                Expr[] res = new Expr[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = Expr.Create(Context, Native.getAppArg(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        /**
+         * Update the arguments of the expression using the arguments <paramref name="args"/>
+         * The number of new arguments should coincide with the current number of arguments.
+         **/
+        public void Update(Expr[] args)
+        {
+            
+            
+
+            Context.CheckContextMatch(args);
+            if (args.Length != NumArgs)
+                throw new Z3Exception("Number of arguments does not match");
+            NativeObject = Native.updateTerm(Context.nCtx, NativeObject, (Integer)args.Length, Expr.ArrayToNative(args));
+        }
+
+        /**
+         * Substitute every occurrence of <code>from[i]</code> in the expression with <code>to[i]</code>, for <code>i</code> smaller than <code>num_exprs</code>.
+         * <remarks>
+         * The result is the new expression. The arrays <code>from</code> and <code>to</code> must have size <code>num_exprs</code>.
+         * For every <code>i</code> smaller than <code>num_exprs</code>, we must have that 
+         * sort of <code>from[i]</code> must be equal to sort of <code>to[i]</code>.
+         * </remarks>    
+         **/
+        public Expr Substitute(Expr[] from, Expr[] to)
+        {
+            
+            
+            
+            
+            
+
+            Context.CheckContextMatch(from);
+            Context.CheckContextMatch(to);
+            if (from.Length != to.Length)
+                throw new Z3Exception("Argument sizes do not match");
+            return Expr.Create(Context, Native.substitute(Context.nCtx, NativeObject, (Integer)from.Length, Expr.ArrayToNative(from), Expr.ArrayToNative(to)));
+        }
+
+        /**
+         * Substitute every occurrence of <code>from</code> in the expression with <code>to</code>.
+         * <seealso cref="Substitute(Expr[],Expr[])"/>
+         **/
+        public Expr Substitute(Expr from, Expr to)
+        {
+            
+            
+            
+
+            return Substitute(new Expr[] { from }, new Expr[] { to });
+        }
+
+        /**
+         * Substitute the free variables in the expression with the expressions in <paramref name="to"/>
+         * <remarks>
+         * For every <code>i</code> smaller than <code>num_exprs</code>, the variable with de-Bruijn index <code>i</code> is replaced with term <code>to[i]</code>.
+         * </remarks>
+         **/
+        public Expr SubstituteVars(Expr[] to)
+        {
+            
+            
+            
+
+            Context.CheckContextMatch(to);
+            return Expr.Create(Context, Native.substituteVars(Context.nCtx, NativeObject, (Integer)to.Length, Expr.ArrayToNative(to)));
+        }
+
+        /**
+         * Translates (copies) the term to the Context <paramref name="ctx"/>.
+         * <param name="ctx">A context</param>
+         * @return A copy of the term which is associated with <paramref name="ctx"/>
+         **/
+        public Expr Translate(Context ctx)
+        {
+            
+            
+
+            if (ReferenceEquals(Context, ctx))
+                return this;
+            else
+                return Expr.Create(ctx, Native.translate(Context.nCtx, NativeObject, ctx.nCtx));
+        }
+
+        /**
+         * Returns a string representation of the expression.
+         **/
+        public String toString()
+        {
+            return super.toString();
+        }        
+
+        /**
+         * Indicates whether the term is a numeral
+         **/
+        public boolean IsNumeral()  { return Native.isNumeralAst(Context.nCtx, NativeObject) != 0; }
+
+        /**
+         * Indicates whether the term is well-sorted.
+         * @return True if the term is well-sorted, false otherwise.
+         **/
+        public boolean IsWellSorted()  { return Native.isWellSorted(Context.nCtx, NativeObject) != 0; }
+
+        /**
+         * The Sort of the term.
+         **/
+        public Sort Sort()  {
+                
+                return Sort.Create(Context, Native.getSort(Context.nCtx, NativeObject)); }
+
+        /**
+         * Indicates whether the term represents a constant.
+         **/
+        public boolean IsConst()  { return IsExpr && NumArgs == 0 && FuncDecl.DomainSize == 0; }
+
+        /**
+         * Indicates whether the term is an integer numeral.
+         **/
+        public boolean IsIntNum()  { return IsNumeral && IsInt; }
+
+        /**
+         * Indicates whether the term is a real numeral.
+         **/
+        public boolean IsRatNum()  { return IsNumeral && IsReal; }
+
+        /**
+         * Indicates whether the term is an algebraic number
+         **/
+        public boolean IsAlgebraicNumber()  { return Native.isAlgebraicNumber(Context.nCtx, NativeObject) != 0; }
+
+
+        /**
+         * Indicates whether the term has Boolean sort.
+         **/
+        public boolean IsBool() 
+            {
+                return (IsExpr &&
+                        Native.isEqSort(Context.nCtx,
+                                              Native.mkBooleanSort(Context.nCtx),
+                                              Native.getSort(Context.nCtx, NativeObject)) != 0);
+        }
+
+        /**
+         * Indicates whether the term is the constant true.
+         **/
+         /* Overloaded operators are not translated. */
+        }
+
+        /**
+         * Indicates whether the term is of sort real.
+         **/
+        public boolean IsReal()  { return Native.getSortKind(Context.nCtx, Native.getSort(Context.nCtx, NativeObject)) == (Integer)Z3SortKind.Z3REALSORT; }
+
+        /**
+         * Indicates whether the term is an arithmetic numeral.
+         **/
+         /* Overloaded operators are not translated. */
+        }
+
+        /**
+         * Indicates whether the term is an array store. 
+         * <remarks>It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). 
+         * Array store takes at least 3 arguments. </remarks>
+         **/
+         /* Overloaded operators are not translated. */
+
+        /**
+         * Indicates whether the term is a bit-vector numeral
+         **/
+         /* Overloaded operators are not translated. */
+        }
+
+        /**
+         * Indicates whether the term is an relation store
+         * <remarks>
+         * Insert a record into a relation.
+         * The function takes <code>n+1</code> arguments, where the first argument is the relation and the remaining <code>n</code> elements 
+         * correspond to the <code>n</code> columns of the relation.
+         * </remarks>
+         **/
+         /* Overloaded operators are not translated. */
+        }
+
+        /**
+         * Indicates whether the term is a less than predicate over a finite domain.
+         **/
+         /* Overloaded operators are not translated. */
+        }
+
+        /** Constructor for Expr </summary>
+         **/
+        protected Expr(Context ctx) { super(ctx);  }
+        /** Constructor for Expr </summary>
+         **/
+        protected Expr(Context ctx, IntPtr obj) { super(ctx, obj);  }
+
+        void CheckNativeObject(IntPtr obj)
+        {
+            if (Native.isApp(Context.nCtx, obj) == 0 &&
+                (Z3AstKind)Native.getAstKind(Context.nCtx, obj) != Z3AstKind.Z3VARAST &&
+                (Z3AstKind)Native.getAstKind(Context.nCtx, obj) != Z3AstKind.Z3QUANTIFIERAST)
+                throw new Z3Exception("Underlying object is not a term");
+            super.CheckNativeObject(obj);
+        }
+
+        static Expr Create(Context ctx, FuncDecl f, params Expr[] arguments)
+        {
+            
+            
+            
+
+            IntPtr obj = Native.mkApp(ctx.nCtx, f.NativeObject, 
+                                          AST.ArrayLength(arguments), 
+                                          AST.ArrayToNative(arguments));
+            return Create(ctx, obj);
+        }        
+
+        new static Expr Create(Context ctx, IntPtr obj)
+        {
+            
+            
+
+            Z3AstKind k = (Z3AstKind)Native.getAstKind(ctx.nCtx, obj);
+            if (k == Z3AstKind.Z3QUANTIFIERAST)
+                return new Quantifier(ctx, obj);
+            IntPtr s = Native.getSort(ctx.nCtx, obj);
+            Z3SortKind sk = (Z3SortKind)Native.getSortKind(ctx.nCtx, s);
+
+            if (Native.isAlgebraicNumber(ctx.nCtx, obj) != 0) // is this a numeral ast?
+                return new AlgebraicNum(ctx, obj);
+
+            if (Native.isNumeralAst(ctx.nCtx, obj) != 0)
+            {
+                switch (sk)
+                {
+                    case Z3SortKind.Z3INTSORT: return new IntNum(ctx, obj);
+                    case Z3SortKind.Z3REALSORT: return new RatNum(ctx, obj);
+                    case Z3SortKind.Z3BVSORT: return new BitVecNum(ctx, obj);
+                }
+            }
+
+            switch (sk)
+            {
+                case Z3SortKind.Z3BOOLSORT: return new BoolExpr(ctx, obj);
+                case Z3SortKind.Z3INTSORT: return new IntExpr(ctx, obj);
+                case Z3SortKind.Z3REALSORT: return new RealExpr(ctx, obj);
+                case Z3SortKind.Z3BVSORT: return new BitVecExpr(ctx, obj);
+                case Z3SortKind.Z3ARRAYSORT: return new ArrayExpr(ctx, obj);
+                case Z3SortKind.Z3DATATYPESORT: return new DatatypeExpr(ctx, obj);
+            }
+
+            return new Expr(ctx, obj);
+        }
+    }
+
+    /**
+     * Boolean expressions
+     **/
+    public class BoolExpr extends Expr
+    {
+        /** Constructor for BoolExpr </summary>
+     **/
+        protected BoolExpr(Context ctx) { super(ctx);  }
+        /** Constructor for BoolExpr </summary>
+     **/
+        BoolExpr(Context ctx, IntPtr obj) { super(ctx, obj);  }
+    }
+
+    /**
+     * Arithmetic expressions (int/real)
+     **/
+    public class ArithExpr extends Expr
+    {
+        /** Constructor for ArithExpr </summary>
+     **/
+        protected ArithExpr(Context ctx)
+            { super(ctx);
+            
+        }
+        ArithExpr(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+    }
+
+    /**
+     * Int expressions
+     **/
+    public class IntExpr extends ArithExpr
+    {
+        /** Constructor for IntExpr </summary>
+     **/
+        protected IntExpr(Context ctx)
+            { super(ctx);
+            
+        }
+        IntExpr(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+    }
+
+    /**
+     * Real expressions
+     **/
+    public class RealExpr extends ArithExpr
+    {
+        /** Constructor for RealExpr </summary>
+     **/
+        protected RealExpr(Context ctx)
+            { super(ctx);
+            
+        }
+        RealExpr(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+    }
+
+    /**
+     * Bit-vector expressions
+     **/
+    public class BitVecExpr extends Expr
+    {
+
+        /**
+         * The size of the sort of a bit-vector term.
+         **/
+        public Integer SortSize()  { return ((BitVecSort)Sort).Size; }
+
+        /** Constructor for BitVecExpr </summary>
+         **/
+        protected BitVecExpr(Context ctx) { super(ctx);  }
+        BitVecExpr(Context ctx, IntPtr obj) { super(ctx, obj);  }
+    }
+
+    /**
+     * Array expressions
+     **/
+    public class ArrayExpr extends Expr
+    {
+        /** Constructor for ArrayExpr </summary>
+     **/
+        protected ArrayExpr(Context ctx)
+            { super(ctx);
+            
+        }
+        ArrayExpr(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+    }
+
+    /**
+     * Datatype expressions
+     **/
+    public class DatatypeExpr extends Expr
+    {
+        /** Constructor for DatatypeExpr </summary>
+     **/
+        protected DatatypeExpr(Context ctx)
+            { super(ctx);
+            
+        }
+        DatatypeExpr(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+    }

src/api/java/com/Microsoft/Z3/Fixedpoint.java

@@ -0,0 +1,300 @@
+/**
+ * This file was automatically generated from Fixedpoint.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * Object for managing fixedpoints
+     **/
+    public class Fixedpoint extends Z3Object
+    {
+
+        /**
+         * A string that describes all available fixedpoint solver parameters.
+         **/
+        public String Help() 
+            {
+                
+                return Native.fixedpointGetHelp(Context.nCtx, NativeObject);
+        }
+
+        /**
+         * Sets the fixedpoint solver parameters.
+         **/
+        public void setParameters(Params value) 
+            {
+                
+                Context.CheckContextMatch(value);
+                Native.fixedpointSetParams(Context.nCtx, NativeObject, value.NativeObject);
+        }
+
+        /**
+         * Retrieves parameter descriptions for Fixedpoint solver.
+         **/
+        public ParamDescrs ParameterDescriptions()  { return new ParamDescrs(Context, Native.fixedpointGetParamDescrs(Context.nCtx, NativeObject)); }
+
+
+        /**
+         * Assert a constraint (or multiple) into the fixedpoint solver.
+         **/
+        public void Assert(BoolExpr[] constraints)
+        {
+            
+            
+
+            Context.CheckContextMatch(constraints);
+            for (BoolExpr.Iterator a = constraints.iterator(); a.hasNext(); )
+            {
+                Native.fixedpointAssert(Context.nCtx, NativeObject, a.NativeObject);
+            }
+        }
+
+        /**
+         * Register predicate as recursive relation.
+         **/
+        public void RegisterRelation(FuncDecl f)
+        {
+            
+
+            Context.CheckContextMatch(f);
+            Native.fixedpointRegisterRelation(Context.nCtx, NativeObject, f.NativeObject);
+        }
+
+        /**
+         * Add rule into the fixedpoint solver.
+         **/
+        public void AddRule(BoolExpr rule, Symbol name)
+        {
+            
+
+            Context.CheckContextMatch(rule);
+            Native.fixedpointAddRule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name));
+        }
+
+        /**
+         * Add table fact to the fixedpoint solver.
+         **/
+        public void AddFact(FuncDecl pred, Integer[] args)
+        {
+            
+            
+
+            Context.CheckContextMatch(pred);
+            Native.fixedpointAddFact(Context.nCtx, NativeObject, pred.NativeObject, (Integer)args.Length, args);
+        }
+
+        /**
+         * Query the fixedpoint solver.
+         * A query is a conjunction of constraints. The constraints may include the recursively defined relations.
+         * The query is satisfiable if there is an instance of the query variables and a derivation for it.
+         * The query is unsatisfiable if there are no derivations satisfying the query variables. 
+         **/
+        public Status Query(BoolExpr query)
+        {
+            
+
+            Context.CheckContextMatch(query);
+            Z3Lboolean r = (Z3Lboolean)Native.fixedpointQuery(Context.nCtx, NativeObject, query.NativeObject);
+            switch (r)
+            {
+                case Z3Lboolean.Z3LTRUE: return Status.SATISFIABLE;
+                case Z3Lboolean.Z3LFALSE: return Status.UNSATISFIABLE;
+                default: return Status.UNKNOWN;
+            }
+        }
+
+        /**
+         * Query the fixedpoint solver.
+         * A query is an array of relations.
+         * The query is satisfiable if there is an instance of some relation that is non-empty.
+         * The query is unsatisfiable if there are no derivations satisfying any of the relations.
+         **/
+        public Status Query(FuncDecl[] relations)
+        {
+            
+            
+
+            Context.CheckContextMatch(relations);
+            Z3Lboolean r = (Z3Lboolean)Native.fixedpointQueryRelations(Context.nCtx, NativeObject,
+                                   AST.ArrayLength(relations), AST.ArrayToNative(relations));
+            switch (r)
+            {
+                case Z3Lboolean.Z3LTRUE: return Status.SATISFIABLE;
+                case Z3Lboolean.Z3LFALSE: return Status.UNSATISFIABLE;
+                default: return Status.UNKNOWN;
+            }
+        }
+
+        /**
+         * Creates a backtracking point.
+         * <seealso cref="Pop"/>
+         **/
+        public void Push()
+        {
+            Native.fixedpointPush(Context.nCtx, NativeObject);
+        }
+
+        /**
+         * Backtrack one backtracking point.
+         * <remarks>Note that an exception is thrown if Pop is called without a corresponding <code>Push</code></remarks>
+         * <seealso cref="Push"/>
+         **/
+        public void Pop()
+        {
+            Native.fixedpointPop(Context.nCtx, NativeObject);
+        }
+
+
+        /**
+         * Update named rule into in the fixedpoint solver.
+         **/
+        public void UpdateRule(BoolExpr rule, Symbol name)
+        {
+            
+
+            Context.CheckContextMatch(rule);
+            Native.fixedpointUpdateRule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name));
+        }
+
+        /**
+         * Retrieve satisfying instance or instances of solver, 
+         * or definitions for the recursive predicates that show unsatisfiability.
+         **/
+        public Expr GetAnswer()
+        {
+            IntPtr ans = Native.fixedpointGetAnswer(Context.nCtx, NativeObject);
+            return (ans == IntPtr.Zero) ? null : Expr.Create(Context, ans);
+        }
+
+        /**
+         * Retrieve explanation why fixedpoint engine returned status Unknown.
+         **/
+        public String GetReasonUnknown()
+        {
+            
+
+            return Native.fixedpointGetReasonUnknown(Context.nCtx, NativeObject);
+        }
+
+        /**
+         * Retrieve the number of levels explored for a given predicate.
+         **/
+        public Integer GetNumLevels(FuncDecl predicate)
+        {
+            return Native.fixedpointGetNumLevels(Context.nCtx, NativeObject, predicate.NativeObject);
+        }
+
+        /**
+         * Retrieve the cover of a predicate.
+         **/
+        public Expr GetCoverDelta(int level, FuncDecl predicate)
+        {
+            IntPtr res = Native.fixedpointGetCoverDelta(Context.nCtx, NativeObject, level, predicate.NativeObject);
+            return (res == IntPtr.Zero) ? null : Expr.Create(Context, res);
+        }
+
+        /**
+         * Add <tt>property</tt> about the <tt>predicate</tt>.
+         * The property is added at <tt>level</tt>.
+         **/
+        public void AddCover(int level, FuncDecl predicate, Expr property)
+        {
+            Native.fixedpointAddCover(Context.nCtx, NativeObject, level, predicate.NativeObject, property.NativeObject);
+        }
+
+        /**
+         * Retrieve internal string representation of fixedpoint object.
+         **/
+        public String toString()
+        {
+            return Native.fixedpointtoString(Context.nCtx, NativeObject, 0, null);
+        }
+
+        /**
+         * Instrument the Datalog engine on which table representation to use for recursive predicate.
+         **/
+        public void SetPredicateRepresentation(FuncDecl f, Symbol[] kinds)
+        {
+            
+
+            Native.fixedpointSetPredicateRepresentation(Context.nCtx, NativeObject,
+                               f.NativeObject, AST.ArrayLength(kinds), Symbol.ArrayToNative(kinds));
+
+        }
+
+        /**
+         * Convert benchmark given as set of axioms, rules and queries to a string.
+         **/
+        public String toString(BoolExpr[] queries)
+        {
+
+            return Native.fixedpointtoString(Context.nCtx, NativeObject,
+                             AST.ArrayLength(queries), AST.ArrayToNative(queries));
+        }
+
+        /**
+         * Retrieve set of rules added to fixedpoint context.
+         **/
+        public BoolExpr[] Rules {() 
+                
+
+                ASTVector v = new ASTVector(Context, Native.fixedpointGetRules(Context.nCtx, NativeObject));
+                Integer n = v.Size;
+                BoolExpr[] res = new BoolExpr[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = new BoolExpr(Context, v[i].NativeObject);
+                return res;
+        }
+
+        /**
+         * Retrieve set of assertions added to fixedpoint context.
+         **/
+        public BoolExpr[] Assertions {() 
+                
+
+                ASTVector v = new ASTVector(Context, Native.fixedpointGetAssertions(Context.nCtx, NativeObject));
+                Integer n = v.Size;
+                BoolExpr[] res = new BoolExpr[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = new BoolExpr(Context, v[i].NativeObject);
+                return res;
+        }
+
+
+        Fixedpoint(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+        Fixedpoint(Context ctx)
+            { super(ctx, Native.mkFixedpoint(ctx.nCtx));
+            
+        }
+
+        class DecRefQueue extends Z3.DecRefQueue
+        {
+            public void IncRef(Context ctx, IntPtr obj)
+            {
+                Native.fixedpointIncRef(ctx.nCtx, obj);
+            }
+
+            public void DecRef(Context ctx, IntPtr obj)
+            {
+                Native.fixedpointDecRef(ctx.nCtx, obj);
+            }
+        };
+
+        void IncRef(IntPtr o)
+        {
+            Context.FixedpointDRQ.IncAndClear(Context, o);
+            super.IncRef(o);
+        }
+
+        void DecRef(IntPtr o)
+        {
+            Context.FixedpointDRQ.Add(o);
+            super.DecRef(o);
+        }
+    }

src/api/java/com/Microsoft/Z3/FuncDecl.java

@@ -0,0 +1,257 @@
+/**
+ * This file was automatically generated from FuncDecl.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * Function declarations. 
+     **/
+    public class FuncDecl extends AST
+    {
+        /**
+         * Comparison operator.
+         * @return True if <paramref name="a"/> and <paramref name="b"/> share the same context and are equal, false otherwise.
+         **/
+         /* Overloaded operators are not translated. */
+
+        /**
+         * Comparison operator.
+         * @return True if <paramref name="a"/> and <paramref name="b"/> do not share the same context or are not equal, false otherwise.
+         **/
+         /* Overloaded operators are not translated. */
+
+        /**
+         * Object comparison.
+         **/
+        public boolean Equals(object o)
+        {
+            FuncDecl casted = o as FuncDecl;
+            if (casted == null) return false;
+            return this == casted;
+        }
+
+        /**
+         * A hash code.
+         **/
+        public int GetHashCode()
+        {
+            return super.GetHashCode();
+        }
+
+        /**
+         * A string representations of the function declaration.
+         **/
+        public String toString()
+        {
+            return Native.funcDecltoString(Context.nCtx, NativeObject);
+        }
+
+        /**
+         * Returns a unique identifier for the function declaration.
+         **/
+        new public Integer Id()  { return Native.getFuncDeclId(Context.nCtx, NativeObject); }
+
+        /**
+         * The arity of the function declaration
+         **/
+        public Integer Arity()  { return Native.getArity(Context.nCtx, NativeObject); }
+
+        /**
+         * The size of the domain of the function declaration
+         * <seealso cref="Arity"/>
+         **/
+        public Integer DomainSize()  { return Native.getDomainSize(Context.nCtx, NativeObject); }
+
+        /**
+         * The domain of the function declaration
+         **/
+        public Sort[] Domain() 
+            {
+                
+
+                var n = DomainSize;
+
+                Sort[] res = new Sort[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = Sort.Create(Context, Native.getDomain(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        /**
+         * The range of the function declaration
+         **/
+        public Sort Range()  {
+                
+                return Sort.Create(Context, Native.getRange(Context.nCtx, NativeObject)); }
+
+        /**
+         * The kind of the function declaration.
+         **/
+        public Z3_decl_kind DeclKind()  { return (Z3DeclKind)Native.getDeclKind(Context.nCtx, NativeObject); }
+
+        /**
+         * The name of the function declaration
+         **/
+        public Symbol Name()  {
+                
+                return Symbol.Create(Context, Native.getDeclName(Context.nCtx, NativeObject)); }
+
+        /**
+         * The number of parameters of the function declaration
+         **/
+        public Integer NumParameters()  { return Native.getDeclNumParameters(Context.nCtx, NativeObject); }
+
+        /**
+         * The parameters of the function declaration
+         **/
+        public Parameter[] Parameters() 
+            {
+                
+
+                Integer num = NumParameters;
+                Parameter[] res = new Parameter[num];
+                for (Integer i = 0; i < num; i++)
+                {
+                    Z3ParameterKind k = (Z3ParameterKind)Native.getDeclParameterKind(Context.nCtx, NativeObject, i);
+                    switch (k)
+                    {
+                        case Z3ParameterKind.Z3PARAMETERINT:
+                            res[i] = new Parameter(k, Native.getDeclIntParameter(Context.nCtx, NativeObject, i));
+                            break;
+                        case Z3ParameterKind.Z3PARAMETERDOUBLE:
+                            res[i] = new Parameter(k, Native.getDeclDoubleParameter(Context.nCtx, NativeObject, i));
+                            break;
+                        case Z3ParameterKind.Z3PARAMETERSYMBOL:
+                            res[i] = new Parameter(k, Symbol.Create(Context, Native.getDeclSymbolParameter(Context.nCtx, NativeObject, i)));
+                            break;
+                        case Z3ParameterKind.Z3PARAMETERSORT:
+                            res[i] = new Parameter(k, Sort.Create(Context, Native.getDeclSortParameter(Context.nCtx, NativeObject, i)));
+                            break;
+                        case Z3ParameterKind.Z3PARAMETERAST:
+                            res[i] = new Parameter(k, new AST(Context, Native.getDeclAstParameter(Context.nCtx, NativeObject, i)));
+                            break;
+                        case Z3ParameterKind.Z3PARAMETERFUNCDECL:
+                            res[i] = new Parameter(k, new FuncDecl(Context, Native.getDeclFuncDeclParameter(Context.nCtx, NativeObject, i)));
+                            break;
+                        case Z3ParameterKind.Z3PARAMETERRATIONAL:
+                            res[i] = new Parameter(k, Native.getDeclRationalParameter(Context.nCtx, NativeObject, i));
+                            break;
+                        default:
+                            throw new Z3Exception("Unknown function declaration parameter kind encountered");
+                }
+                return res;
+            }
+        }
+
+        /**
+         * Function declarations can have Parameters associated with them. 
+         **/
+        public class Parameter
+        {
+            private Z3ParameterKind kind;
+            private int i;
+            private double d;
+            private Symbol sym;
+            private Sort srt;
+            private AST ast;
+            private FuncDecl fd;
+            private String r;
+
+            /**The int value of the parameter.</summary>
+         **/
+             /* Overloaded operators are not translated. */
+
+            Parameter(Z3ParameterKind k, double d)
+            {
+                this.kind = k;
+                this.d = d;
+            }
+
+            Parameter(Z3ParameterKind k, Symbol s)
+            {
+                this.kind = k;
+                this.sym = s;
+            }
+
+            Parameter(Z3ParameterKind k, Sort s)
+            {
+                this.kind = k;
+                this.srt = s;
+            }
+
+            Parameter(Z3ParameterKind k, AST a)
+            {
+                this.kind = k;
+                this.ast = a;
+            }
+
+            Parameter(Z3ParameterKind k, FuncDecl fd)
+            {
+                this.kind = k;
+                this.fd = fd;
+            }
+
+            Parameter(Z3ParameterKind k, String r)
+            {
+                this.kind = k;
+                this.r = r;
+            }
+        }
+
+        FuncDecl(Context ctx, IntPtr obj) { super(ctx, obj); 
+             
+        }
+
+        FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
+            : base(ctx, Native.mkFuncDecl(ctx.nCtx, name.NativeObject,
+                                             AST.ArrayLength(domain), AST.ArrayToNative(domain),
+                                             range.NativeObject))
+            
+            
+            
+        }        
+
+        FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range)
+            : base(ctx, Native.mkFreshFuncDecl(ctx.nCtx, prefix,
+                                             AST.ArrayLength(domain), AST.ArrayToNative(domain),
+                                             range.NativeObject))
+            
+            
+        }
+
+        void CheckNativeObject(IntPtr obj)
+        {
+            if (Native.getAstKind(Context.nCtx, obj) != (Integer)Z3AstKind.Z3FUNCDECLAST)
+                throw new Z3Exception("Underlying object is not a function declaration");
+            super.CheckNativeObject(obj);
+        }
+
+        /**
+         * Create expression that applies function to arguments.
+         * <param name="args"></param>
+         * @return 
+         **/
+        public Expr this[params() lic Expr this[params Expr[] args] 
+        public Expr this[params()  {
+                
+
+                return Apply(args); 
+        }
+
+        /**
+         * Create expression that applies function to arguments.
+         * <param name="args"></param>
+         * @return 
+         **/
+        public Expr Apply(Expr[] args)
+        {
+            
+
+            Context.CheckContextMatch(args);
+            return Expr.Create(Context, this, args);
+        }
+
+    }

src/api/java/com/Microsoft/Z3/FuncInterp.java

@@ -0,0 +1,177 @@
+/**
+ * This file was automatically generated from FuncInterp.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     *  A function interpretation is represented as a finite map and an 'else' value.
+     *  Each entry in the finite map represents the value of a function given a set of arguments.  
+     **/
+    public class FuncInterp extends Z3Object
+    {
+        /**
+         * An Entry object represents an element in the finite map used to encode
+         * a function interpretation.
+         **/
+        public class Entry extends Z3Object
+        {
+            /**
+             * Return the (symbolic) value of this entry.
+             **/
+            public Expr Value()  {
+                    
+                    return Expr.Create(Context, Native.funcEntryGetValue(Context.nCtx, NativeObject)); }
+
+            /**
+             * The number of arguments of the entry.
+             **/
+            public Integer NumArgs()  { return Native.funcEntryGetNumArgs(Context.nCtx, NativeObject); }
+
+            /**
+             * The arguments of the function entry.
+             **/
+            public Expr[] Args() 
+                {
+                    
+                    
+
+                    Integer n = NumArgs;
+                    Expr[] res = new Expr[n];
+                    for (Integer i = 0; i < n; i++)
+                        res[i] = Expr.Create(Context, Native.funcEntryGetArg(Context.nCtx, NativeObject, i));
+                    return res;
+            }
+
+            /**
+             * A string representation of the function entry.
+             **/
+            public String toString()
+            {
+                Integer n = NumArgs;
+                String res = "[";
+                Expr[] args = Args;
+                for (Integer i = 0; i < n; i++)
+                    res += args[i] + ", ";
+                return res + Value + "]";
+            }
+
+            Entry(Context ctx, IntPtr obj) { super(ctx, obj);  }
+
+            class DecRefQueue extends Z3.DecRefQueue
+            {
+                public void IncRef(Context ctx, IntPtr obj)
+                {
+                    Native.funcEntryIncRef(ctx.nCtx, obj);
+                }
+
+                public void DecRef(Context ctx, IntPtr obj)
+                {
+                    Native.funcEntryDecRef(ctx.nCtx, obj);
+                }
+            };
+
+            void IncRef(IntPtr o)
+            {
+                Context.FuncEntryDRQ.IncAndClear(Context, o);
+                super.IncRef(o);
+            }
+
+            void DecRef(IntPtr o)
+            {
+                Context.FuncEntryDRQ.Add(o);
+                super.DecRef(o);
+            }
+        };
+
+        /**
+         * The number of entries in the function interpretation.
+         **/
+        public Integer NumEntries()  { return Native.funcInterpGetNumEntries(Context.nCtx, NativeObject); }
+
+        /**
+         * The entries in the function interpretation
+         **/
+        public Entry[] Entries() 
+            {
+                
+                Contract.Ensures(Contract.ForAll(0, Contract.Result<Entry[]>().Length, 
+                    j => Contract.Result<Entry[]>()[j] != null));
+
+                Integer n = NumEntries;
+                Entry[] res = new Entry[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = new Entry(Context, Native.funcInterpGetEntry(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        /**
+         * The (symbolic) `else' value of the function interpretation.
+         **/
+        public Expr Else()  {
+                
+
+                return Expr.Create(Context, Native.funcInterpGetElse(Context.nCtx, NativeObject)); }
+
+        /**
+         * The arity of the function interpretation
+         **/
+        public Integer Arity()  { return Native.funcInterpGetArity(Context.nCtx, NativeObject); }
+
+        /**
+         * A string representation of the function interpretation.
+         **/
+        public String toString()
+        {
+            String res = "";
+            res += "[";
+            for (Entry.Iterator e = Entries.iterator(); e.hasNext(); )
+            {
+                Integer n = e.NumArgs;                
+                if (n > 1) res += "[";
+                Expr[] args = e.Args;
+                for (Integer i = 0; i < n; i++)
+                {
+                    if (i != 0) res += ", ";
+                    res += args[i];
+                }
+                if (n > 1) res += "]";
+                res += " -> " + e.Value + ", ";
+            }
+            res += "else -> " + Else;
+            res += "]";
+            return res;
+        }
+
+        FuncInterp(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+
+        class DecRefQueue extends Z3.DecRefQueue
+        {
+            public void IncRef(Context ctx, IntPtr obj)
+            {
+                Native.funcInterpIncRef(ctx.nCtx, obj);
+            }
+
+            public void DecRef(Context ctx, IntPtr obj)
+            {
+                Native.funcInterpDecRef(ctx.nCtx, obj);
+            }
+        };        
+
+        void IncRef(IntPtr o)
+        {
+            Context.FuncInterpDRQ.IncAndClear(Context, o);
+            super.IncRef(o);
+        }
+
+        void DecRef(IntPtr o)
+        {
+            Context.FuncInterpDRQ.Add(o);
+            super.DecRef(o);
+        }
+    }

src/api/java/com/Microsoft/Z3/Goal.java

@@ -0,0 +1,182 @@
+/**
+ * This file was automatically generated from Goal.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * A goal (aka problem). A goal is essentially a set
+     * of formulas, that can be solved and/or transformed using
+     * tactics and solvers.
+     **/
+    public class Goal extends Z3Object
+    {
+        /**
+         * The precision of the goal. 
+         * <remarks>
+         * Goals can be transformed using over and under approximations.
+         * An under approximation is applied when the objective is to find a model for a given goal.
+         * An over approximation is applied when the objective is to find a proof for a given goal.
+         * </remarks>
+         **/
+        public Z3_goal_prec Precision()  { return (Z3GoalPrec)Native.goalPrecision(Context.nCtx, NativeObject); }
+
+        /**
+         * Indicates whether the goal is precise.
+         **/
+        public boolean IsPrecise()  { return Precision == Z3GoalPrec.Z3GOALPRECISE; }
+        /**
+         * Indicates whether the goal is an under-approximation.
+         **/
+        public boolean IsUnderApproximation()  { return Precision == Z3GoalPrec.Z3GOALUNDER; }
+
+        /**
+         * Indicates whether the goal is an over-approximation.
+         **/
+        public boolean IsOverApproximation()  { return Precision == Z3GoalPrec.Z3GOALOVER; }
+
+        /**
+         * Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).
+         **/
+        public boolean IsGarbage()  { return Precision == Z3GoalPrec.Z3GOALUNDEROVER; }
+
+        /**
+         * Adds the <paramref name="constraints"/> to the given goal. 
+         **/
+        public void Assert(BoolExpr[] constraints)
+        {
+            
+            
+
+            Context.CheckContextMatch(constraints);
+            for (BoolExpr.Iterator c = constraints.iterator(); c.hasNext(); )
+            {
+                 // It was an assume, now made an assert just to be sure we do not regress
+                Native.goalAssert(Context.nCtx, NativeObject, c.NativeObject);
+            }
+        }
+
+        /**
+         * Indicates whether the goal contains `false'.
+         **/
+        public boolean Inconsistent()  { return Native.goalInconsistent(Context.nCtx, NativeObject) != 0; }
+
+        /**
+         * The depth of the goal.
+         * <remarks>
+         * This tracks how many transformations were applied to it.
+         * </remarks>
+         **/
+        public Integer Depth()  { return Native.goalDepth(Context.nCtx, NativeObject); }
+
+        /**
+         * Erases all formulas from the given goal.
+         **/
+        public void Reset()
+        {
+            Native.goalReset(Context.nCtx, NativeObject);
+        }
+
+        /**
+         * The number of formulas in the goal.
+         **/
+        public Integer Size()  { return Native.goalSize(Context.nCtx, NativeObject); }
+
+        /**
+         * The formulas in the goal.
+         **/
+        public BoolExpr[] Formulas() 
+            {
+                
+
+                Integer n = Size;
+                BoolExpr[] res = new BoolExpr[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = new BoolExpr(Context, Native.goalFormula(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        /**
+         * The number of formulas, subformulas and terms in the goal.
+         **/
+        public Integer NumExprs()  { return Native.goalNumExprs(Context.nCtx, NativeObject); }
+
+        /**
+         * Indicates whether the goal is empty, and it is precise or the product of an under approximation.
+         **/
+        public boolean IsDecidedSat()  { return Native.goalIsDecidedSat(Context.nCtx, NativeObject) != 0; }
+
+        /**
+         * Indicates whether the goal contains `false', and it is precise or the product of an over approximation.
+         **/
+        public boolean IsDecidedUnsat()  { return Native.goalIsDecidedUnsat(Context.nCtx, NativeObject) != 0; }
+
+        /**
+         * Translates (copies) the Goal to the target Context <paramref name="ctx"/>.
+         **/
+        public Goal Translate(Context ctx)
+        {
+            
+
+            return new Goal(ctx, Native.goalTranslate(Context.nCtx, NativeObject, ctx.nCtx));
+        }
+
+        /**
+         * Simplifies the goal.
+         * <remarks>Essentially invokes the `simplify' tactic on the goal.</remarks>
+         **/
+        public Goal Simplify(Params p)
+        {
+            Tactic t = Context.MkTactic("simplify");
+            ApplyResult res = t.Apply(this, p);
+            
+            if (res.NumSubgoals == 0)
+                return Context.MkGoal();
+            else        
+                return res.Subgoals[0];
+        }
+
+        /**
+         * Goal to string conversion.
+         * @return A string representation of the Goal.
+         **/
+        public String toString()
+        {
+            return Native.goaltoString(Context.nCtx, NativeObject);
+        }
+
+        Goal(Context ctx, IntPtr obj) { super(ctx, obj);  }
+
+        Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs)
+            { super(ctx, Native.mkGoal(ctx.nCtx, (models); ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0))
+            
+        }
+
+        class DecRefQueue extends Z3.DecRefQueue
+        {
+            public void IncRef(Context ctx, IntPtr obj)
+            {
+                Native.goalIncRef(ctx.nCtx, obj);
+            }
+
+            public void DecRef(Context ctx, IntPtr obj)
+            {
+                Native.goalDecRef(ctx.nCtx, obj);
+            }
+        };        
+
+        void IncRef(IntPtr o)
+        {
+            Context.GoalDRQ.IncAndClear(Context, o);
+            super.IncRef(o);
+        }
+
+        void DecRef(IntPtr o)
+        {
+            Context.GoalDRQ.Add(o);
+            super.DecRef(o);
+        }
+
+    }

src/api/java/com/Microsoft/Z3/IDisposable.java

@@ -0,0 +1,25 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    IDisposable.java
+
+Abstract:
+
+    Compatability interface (C# -> Java)
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-03-16
+
+Notes:
+    
+--*/
+
+package com.Microsoft.Z3;
+
+public class IDisposable
+{
+    public void Dispose() {}
+}

src/api/java/com/Microsoft/Z3/Log.java

@@ -0,0 +1,60 @@
+/**
+ * This file was automatically generated from Log.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * Interaction logging for Z3.
+     * <remarks>
+     * Note that this is a global, static log and if multiple Context 
+     * objects are created, it logs the interaction with all of them.
+     * </remarks>
+     **/
+    public final class Log
+    {
+        private  boolean mIsOpen = false;
+
+        /**
+         * Open an interaction log file.
+         * <param name="filename">the name of the file to open</param>
+         * @return True if opening the log file succeeds, false otherwise.
+         **/
+        public  boolean Open(String filename)
+        {
+            mIsOpen = true;
+            return Native.openLog(filename) == 1;
+        }
+
+        /**
+         * Closes the interaction log.
+         **/
+        public  void Close()
+        {
+            mIsOpen = false;
+            Native.closeLog();
+        }
+
+        /**
+         * Appends the user-provided string <paramref name="s"/> to the interaction log.
+         **/
+        public  void Append(String s)
+        {
+            
+
+            if (!mIsOpen)
+                throw new Z3Exception("Log cannot be closed.");
+            Native.appendLog(s);
+        }
+
+        /**
+         * Checks whether the interaction log is opened.
+         * @return True if the interaction log is open, false otherwise.
+         **/
+        public  boolean isOpen()
+        {
+            return mIsOpen;
+        }
+    }

src/api/java/com/Microsoft/Z3/Model.java

@@ -0,0 +1,279 @@
+/**
+ * This file was automatically generated from Model.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * A Model contains interpretations (assignments) of constants and functions. 
+     **/
+    public class Model extends Z3Object
+    {
+        /**
+         * Retrieves the interpretation (the assignment) of <paramref name="a"/> in the model. 
+         * <param name="a">A Constant</param>
+         * @return An expression if the constant has an interpretation in the model, null otherwise.
+         **/
+        public Expr ConstInterp(Expr a)
+        {
+            
+
+            Context.CheckContextMatch(a);
+            return ConstInterp(a.FuncDecl);
+        }
+
+        /**
+         * Retrieves the interpretation (the assignment) of <paramref name="f"/> in the model. 
+         * <param name="f">A function declaration of zero arity</param>
+         * @return An expression if the function has an interpretation in the model, null otherwise.    
+         **/
+        public Expr ConstInterp(FuncDecl f)
+        {
+            
+
+            Context.CheckContextMatch(f);
+            if (f.Arity != 0 ||
+                Native.getSortKind(Context.nCtx, Native.getRange(Context.nCtx, f.NativeObject)) == (Integer)Z3SortKind.Z3ARRAYSORT)
+                throw new Z3Exception("Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");
+
+            IntPtr n = Native.modelGetConstInterp(Context.nCtx, NativeObject, f.NativeObject);
+            if (n == IntPtr.Zero)
+                return null;
+            else
+                return Expr.Create(Context, n);
+        }
+
+        /**
+         * Retrieves the interpretation (the assignment) of a non-constant <paramref name="f"/> in the model. 
+         * <param name="f">A function declaration of non-zero arity</param>
+         * @return A FunctionInterpretation if the function has an interpretation in the model, null otherwise. 
+         **/
+        public FuncInterp FuncInterp(FuncDecl f)
+        {
+            
+
+            Context.CheckContextMatch(f);
+
+            Z3SortKind sk = (Z3SortKind)Native.getSortKind(Context.nCtx, Native.getRange(Context.nCtx, f.NativeObject));
+
+            if (f.Arity == 0)
+            {
+                IntPtr n = Native.modelGetConstInterp(Context.nCtx, NativeObject, f.NativeObject);
+
+                if (sk == Z3SortKind.Z3ARRAYSORT)
+                {
+                    if (n == IntPtr.Zero)
+                        return null;
+                    else
+                    {
+                        if (Native.isAsArray(Context.nCtx, n) == 0)
+                            throw new Z3Exception("Argument was not an array constant");
+                        IntPtr fd = Native.getAsArrayFuncDecl(Context.nCtx, n);
+                        return FuncInterp(new FuncDecl(Context, fd));
+                    }
+                }
+                else
+                {
+                    throw new Z3Exception("Constant functions do not have a function interpretation; use ConstInterp");
+                }
+            }
+            else
+            {
+                IntPtr n = Native.modelGetFuncInterp(Context.nCtx, NativeObject, f.NativeObject);
+                if (n == IntPtr.Zero)
+                    return null;
+                else
+                    return new FuncInterp(Context, n);
+            }
+        }
+
+        /**
+         * The number of constants that have an interpretation in the model.
+         **/
+        public Integer NumConsts()  { return Native.modelGetNumConsts(Context.nCtx, NativeObject); }
+
+        /**
+         * The function declarations of the constants in the model.
+         **/
+        public FuncDecl[] ConstDecls() 
+            {
+                
+
+                Integer n = NumConsts;
+                FuncDecl[] res = new FuncDecl[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = new FuncDecl(Context, Native.modelGetConstDecl(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        /**
+         * The number of function interpretations in the model.
+         **/
+        public Integer NumFuncs()  { return Native.modelGetNumFuncs(Context.nCtx, NativeObject); }
+
+        /**
+         * The function declarations of the function interpretations in the model.
+         **/
+        public FuncDecl[] FuncDecls() 
+            {
+                
+
+                Integer n = NumFuncs;
+                FuncDecl[] res = new FuncDecl[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = new FuncDecl(Context, Native.modelGetFuncDecl(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        /**
+         * All symbols that have an interpretation in the model.
+         **/
+        public FuncDecl[] Decls() 
+            {
+                
+
+                var nFuncs = NumFuncs;
+                var nConsts = NumConsts;
+                Integer n = nFuncs + nConsts;
+                FuncDecl[] res = new FuncDecl[n];
+                for (Integer i = 0; i < nConsts; i++)
+                    res[i] = new FuncDecl(Context, Native.modelGetConstDecl(Context.nCtx, NativeObject, i));
+                for (Integer i = 0; i < nFuncs; i++)
+                    res[nConsts + i] = new FuncDecl(Context, Native.modelGetFuncDecl(Context.nCtx, NativeObject, i));                
+                return res;
+        }
+
+        /**
+         * A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model.
+         **/
+        public class ModelEvaluationFailedException extends Z3Exception
+        {
+            /**
+             * An exception that is thrown when model evaluation fails.
+             **/
+            public ModelEvaluationFailedException() { super(); }
+        }
+
+        /**
+         * Evaluates the expression <paramref name="t"/> in the current model.
+         * <remarks>
+         * This function may fail if <paramref name="t"/> contains quantifiers, 
+         * is partial (MODEL_PARTIAL enabled), or if <paramref name="t"/> is not well-sorted.
+         * In this case a <code>ModelEvaluationFailedException</code> is thrown.
+         * </remarks>
+         * <param name="t">An expression</param>
+         * <param name="completion">
+         * When this flag is enabled, a model value will be assigned to any constant 
+         * or function that does not have an interpretation in the model.
+         * </param>
+         * @return The evaluation of <paramref name="t"/> in the model.        
+         **/
+        public Expr Eval(Expr t, boolean completion)
+        {
+            
+            
+
+            IntPtr v = IntPtr.Zero;
+            if (Native.modelEval(Context.nCtx, NativeObject, t.NativeObject, (completion) ? 1 : 0, v) == 0)
+                throw new ModelEvaluationFailedException();
+            else
+                return Expr.Create(Context, v);
+        }
+
+        /**
+         * Alias for <code>Eval</code>.
+         **/
+        public Expr Evaluate(Expr t, boolean completion)
+        {
+            
+            
+
+            return Eval(t, completion);
+        }
+
+        /**
+         * The number of uninterpreted sorts that the model has an interpretation for.
+         **/
+        public Integer NumSorts () { return Native.modelGetNumSorts(Context.nCtx, NativeObject); }
+
+        /**
+         * The uninterpreted sorts that the model has an interpretation for. 
+         * <remarks>
+         * Z3 also provides an intepretation for uninterpreted sorts used in a formula.
+         * The interpretation for a sort is a finite set of distinct values. We say this finite set is
+         * the "universe" of the sort.
+         * </remarks>
+         * <seealso cref="NumSorts"/>
+         * <seealso cref="SortUniverse"/>
+         **/
+        public Sort[] Sorts() 
+            {
+                
+
+                Integer n = NumSorts;
+                Sort[] res = new Sort[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = Sort.Create(Context, Native.modelGetSort(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        /**
+         * The finite set of distinct values that represent the interpretation for sort <paramref name="s"/>.
+         * <seealso cref="Sorts"/>
+         * <param name="s">An uninterpreted sort</param>
+         * @return An array of expressions, where each is an element of the universe of <paramref name="s"/>
+         **/
+        public Expr[] SortUniverse(Sort s)
+        {
+            
+            
+
+            ASTVector nUniv = new ASTVector(Context, Native.modelGetSortUniverse(Context.nCtx, NativeObject, s.NativeObject));
+            Integer n = nUniv.Size;
+            Expr[] res = new Expr[n];
+            for (Integer i = 0; i < n; i++)
+                res[i] = Expr.Create(Context, nUniv[i].NativeObject);
+            return res;
+        }
+
+        /**
+         * Conversion of models to strings. 
+         * @return A string representation of the model.
+         **/
+        public String toString()
+        {
+            return Native.modeltoString(Context.nCtx, NativeObject);
+        }
+
+        Model(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+
+        class DecRefQueue extends Z3.DecRefQueue
+        {
+            public void IncRef(Context ctx, IntPtr obj)
+            {
+                Native.modelIncRef(ctx.nCtx, obj);
+            }
+
+            public void DecRef(Context ctx, IntPtr obj)
+            {
+                Native.modelDecRef(ctx.nCtx, obj);
+            }
+        };        
+
+        void IncRef(IntPtr o)
+        {
+            Context.ModelDRQ.IncAndClear(Context, o);
+            super.IncRef(o);
+        }
+
+        void DecRef(IntPtr o)
+        {
+            Context.ModelDRQ.Add(o);
+            super.DecRef(o);
+        }
+    }

src/api/java/com/Microsoft/Z3/Native.java

@@ -0,0 +1,494 @@
+// Automatically generated file
+package com.Microsoft.Z3;
+public final class Native {
+  static { System.loadLibrary("<mk_util.JavaDLLComponent instance at 0x0240DCD8>"); }
+  public static native long mkConfig();
+  public static native void delConfig(long a0);
+  public static native void setParamValue(long a0, String a1, String a2);
+  public static native long mkContext(long a0);
+  public static native long mkContextRc(long a0);
+  public static native void delContext(long a0);
+  public static native void incRef(long a0, long a1);
+  public static native void decRef(long a0, long a1);
+  public static native void updateParamValue(long a0, String a1, String a2);
+  public static native boolean getParamValue(long a0, String a1, String a2);
+  public static native void interrupt(long a0);
+  public static native long mkParams(long a0);
+  public static native void paramsIncRef(long a0, long a1);
+  public static native void paramsDecRef(long a0, long a1);
+  public static native void paramsSetBool(long a0, long a1, long a2, boolean a3);
+  public static native void paramsSetUint(long a0, long a1, long a2, int a3);
+  public static native void paramsSetDouble(long a0, long a1, long a2, double a3);
+  public static native void paramsSetSymbol(long a0, long a1, long a2, long a3);
+  public static native String paramsToString(long a0, long a1);
+  public static native void paramsValidate(long a0, long a1, long a2);
+  public static native void paramDescrsIncRef(long a0, long a1);
+  public static native void paramDescrsDecRef(long a0, long a1);
+  public static native int paramDescrsGetKind(long a0, long a1, long a2);
+  public static native int paramDescrsSize(long a0, long a1);
+  public static native long paramDescrsGetName(long a0, long a1, int a2);
+  public static native String paramDescrsToString(long a0, long a1);
+  public static native long mkIntSymbol(long a0, int a1);
+  public static native long mkStringSymbol(long a0, String a1);
+  public static native long mkUninterpretedSort(long a0, long a1);
+  public static native long mkBoolSort(long a0);
+  public static native long mkIntSort(long a0);
+  public static native long mkRealSort(long a0);
+  public static native long mkBvSort(long a0, int a1);
+  public static native long mkFiniteDomainSort(long a0, long a1, long a2);
+  public static native long mkArraySort(long a0, long a1, long a2);
+  public static native long mkTupleSort(long a0, long a1, int a2, long[] a3, long[] a4, Long a5, long[] a6);
+  public static native long mkEnumerationSort(long a0, long a1, int a2, long[] a3, long[] a4, long[] a5);
+  public static native long mkListSort(long a0, long a1, long a2, Long a3, Long a4, Long a5, Long a6, Long a7, Long a8);
+  public static native long mkConstructor(long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6);
+  public static native void delConstructor(long a0, long a1);
+  public static native long mkDatatype(long a0, long a1, int a2, long[] a3);
+  public static native long mkConstructorList(long a0, int a1, long[] a2);
+  public static native void delConstructorList(long a0, long a1);
+  public static native void mkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4);
+  public static native void queryConstructor(long a0, long a1, int a2, Long a3, Long a4, long[] a5);
+  public static native long mkFuncDecl(long a0, long a1, int a2, long[] a3, long a4);
+  public static native long mkApp(long a0, long a1, int a2, long[] a3);
+  public static native long mkConst(long a0, long a1, long a2);
+  public static native long mkFreshFuncDecl(long a0, String a1, int a2, long[] a3, long a4);
+  public static native long mkFreshConst(long a0, String a1, long a2);
+  public static native long mkTrue(long a0);
+  public static native long mkFalse(long a0);
+  public static native long mkEq(long a0, long a1, long a2);
+  public static native long mkDistinct(long a0, int a1, long[] a2);
+  public static native long mkNot(long a0, long a1);
+  public static native long mkIte(long a0, long a1, long a2, long a3);
+  public static native long mkIff(long a0, long a1, long a2);
+  public static native long mkImplies(long a0, long a1, long a2);
+  public static native long mkXor(long a0, long a1, long a2);
+  public static native long mkAnd(long a0, int a1, long[] a2);
+  public static native long mkOr(long a0, int a1, long[] a2);
+  public static native long mkAdd(long a0, int a1, long[] a2);
+  public static native long mkMul(long a0, int a1, long[] a2);
+  public static native long mkSub(long a0, int a1, long[] a2);
+  public static native long mkUnaryMinus(long a0, long a1);
+  public static native long mkDiv(long a0, long a1, long a2);
+  public static native long mkMod(long a0, long a1, long a2);
+  public static native long mkRem(long a0, long a1, long a2);
+  public static native long mkPower(long a0, long a1, long a2);
+  public static native long mkLt(long a0, long a1, long a2);
+  public static native long mkLe(long a0, long a1, long a2);
+  public static native long mkGt(long a0, long a1, long a2);
+  public static native long mkGe(long a0, long a1, long a2);
+  public static native long mkInt2real(long a0, long a1);
+  public static native long mkReal2int(long a0, long a1);
+  public static native long mkIsInt(long a0, long a1);
+  public static native long mkBvnot(long a0, long a1);
+  public static native long mkBvredand(long a0, long a1);
+  public static native long mkBvredor(long a0, long a1);
+  public static native long mkBvand(long a0, long a1, long a2);
+  public static native long mkBvor(long a0, long a1, long a2);
+  public static native long mkBvxor(long a0, long a1, long a2);
+  public static native long mkBvnand(long a0, long a1, long a2);
+  public static native long mkBvnor(long a0, long a1, long a2);
+  public static native long mkBvxnor(long a0, long a1, long a2);
+  public static native long mkBvneg(long a0, long a1);
+  public static native long mkBvadd(long a0, long a1, long a2);
+  public static native long mkBvsub(long a0, long a1, long a2);
+  public static native long mkBvmul(long a0, long a1, long a2);
+  public static native long mkBvudiv(long a0, long a1, long a2);
+  public static native long mkBvsdiv(long a0, long a1, long a2);
+  public static native long mkBvurem(long a0, long a1, long a2);
+  public static native long mkBvsrem(long a0, long a1, long a2);
+  public static native long mkBvsmod(long a0, long a1, long a2);
+  public static native long mkBvult(long a0, long a1, long a2);
+  public static native long mkBvslt(long a0, long a1, long a2);
+  public static native long mkBvule(long a0, long a1, long a2);
+  public static native long mkBvsle(long a0, long a1, long a2);
+  public static native long mkBvuge(long a0, long a1, long a2);
+  public static native long mkBvsge(long a0, long a1, long a2);
+  public static native long mkBvugt(long a0, long a1, long a2);
+  public static native long mkBvsgt(long a0, long a1, long a2);
+  public static native long mkConcat(long a0, long a1, long a2);
+  public static native long mkExtract(long a0, int a1, int a2, long a3);
+  public static native long mkSignExt(long a0, int a1, long a2);
+  public static native long mkZeroExt(long a0, int a1, long a2);
+  public static native long mkRepeat(long a0, int a1, long a2);
+  public static native long mkBvshl(long a0, long a1, long a2);
+  public static native long mkBvlshr(long a0, long a1, long a2);
+  public static native long mkBvashr(long a0, long a1, long a2);
+  public static native long mkRotateLeft(long a0, int a1, long a2);
+  public static native long mkRotateRight(long a0, int a1, long a2);
+  public static native long mkExtRotateLeft(long a0, long a1, long a2);
+  public static native long mkExtRotateRight(long a0, long a1, long a2);
+  public static native long mkInt2bv(long a0, int a1, long a2);
+  public static native long mkBv2int(long a0, long a1, boolean a2);
+  public static native long mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3);
+  public static native long mkBvaddNoUnderflow(long a0, long a1, long a2);
+  public static native long mkBvsubNoOverflow(long a0, long a1, long a2);
+  public static native long mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3);
+  public static native long mkBvsdivNoOverflow(long a0, long a1, long a2);
+  public static native long mkBvnegNoOverflow(long a0, long a1);
+  public static native long mkBvmulNoOverflow(long a0, long a1, long a2, boolean a3);
+  public static native long mkBvmulNoUnderflow(long a0, long a1, long a2);
+  public static native long mkSelect(long a0, long a1, long a2);
+  public static native long mkStore(long a0, long a1, long a2, long a3);
+  public static native long mkConstArray(long a0, long a1, long a2);
+  public static native long mkMap(long a0, long a1, int a2, long[] a3);
+  public static native long mkArrayDefault(long a0, long a1);
+  public static native long mkSetSort(long a0, long a1);
+  public static native long mkEmptySet(long a0, long a1);
+  public static native long mkFullSet(long a0, long a1);
+  public static native long mkSetAdd(long a0, long a1, long a2);
+  public static native long mkSetDel(long a0, long a1, long a2);
+  public static native long mkSetUnion(long a0, int a1, long[] a2);
+  public static native long mkSetIntersect(long a0, int a1, long[] a2);
+  public static native long mkSetDifference(long a0, long a1, long a2);
+  public static native long mkSetComplement(long a0, long a1);
+  public static native long mkSetMember(long a0, long a1, long a2);
+  public static native long mkSetSubset(long a0, long a1, long a2);
+  public static native long mkNumeral(long a0, String a1, long a2);
+  public static native long mkReal(long a0, int a1, int a2);
+  public static native long mkInt(long a0, int a1, long a2);
+  public static native long mkUnsignedInt(long a0, int a1, long a2);
+  public static native long mkInt64(long a0, long a1, long a2);
+  public static native long mkUnsignedInt64(long a0, long a1, long a2);
+  public static native long mkPattern(long a0, int a1, long[] a2);
+  public static native long mkBound(long a0, int a1, long a2);
+  public static native long mkForall(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7);
+  public static native long mkExists(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7);
+  public static native long mkQuantifier(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long[] a7, long a8);
+  public static native long mkQuantifierEx(long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long[] a11, long a12);
+  public static native long mkForallConst(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6);
+  public static native long mkExistsConst(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6);
+  public static native long mkQuantifierConst(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long a7);
+  public static native long mkQuantifierConstEx(long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long a11);
+  public static native int getSymbolKind(long a0, long a1);
+  public static native int getSymbolInt(long a0, long a1);
+  public static native String getSymbolString(long a0, long a1);
+  public static native long getSortName(long a0, long a1);
+  public static native int getSortId(long a0, long a1);
+  public static native long sortToAst(long a0, long a1);
+  public static native boolean isEqSort(long a0, long a1, long a2);
+  public static native int getSortKind(long a0, long a1);
+  public static native int getBvSortSize(long a0, long a1);
+  public static native boolean getFiniteDomainSortSize(long a0, long a1, Long a2);
+  public static native long getArraySortDomain(long a0, long a1);
+  public static native long getArraySortRange(long a0, long a1);
+  public static native long getTupleSortMkDecl(long a0, long a1);
+  public static native int getTupleSortNumFields(long a0, long a1);
+  public static native long getTupleSortFieldDecl(long a0, long a1, int a2);
+  public static native int getDatatypeSortNumConstructors(long a0, long a1);
+  public static native long getDatatypeSortConstructor(long a0, long a1, int a2);
+  public static native long getDatatypeSortRecognizer(long a0, long a1, int a2);
+  public static native long getDatatypeSortConstructorAccessor(long a0, long a1, int a2, int a3);
+  public static native int getRelationArity(long a0, long a1);
+  public static native long getRelationColumn(long a0, long a1, int a2);
+  public static native long funcDeclToAst(long a0, long a1);
+  public static native boolean isEqFuncDecl(long a0, long a1, long a2);
+  public static native int getFuncDeclId(long a0, long a1);
+  public static native long getDeclName(long a0, long a1);
+  public static native int getDeclKind(long a0, long a1);
+  public static native int getDomainSize(long a0, long a1);
+  public static native int getArity(long a0, long a1);
+  public static native long getDomain(long a0, long a1, int a2);
+  public static native long getRange(long a0, long a1);
+  public static native int getDeclNumParameters(long a0, long a1);
+  public static native int getDeclParameterKind(long a0, long a1, int a2);
+  public static native int getDeclIntParameter(long a0, long a1, int a2);
+  public static native double getDeclDoubleParameter(long a0, long a1, int a2);
+  public static native long getDeclSymbolParameter(long a0, long a1, int a2);
+  public static native long getDeclSortParameter(long a0, long a1, int a2);
+  public static native long getDeclAstParameter(long a0, long a1, int a2);
+  public static native long getDeclFuncDeclParameter(long a0, long a1, int a2);
+  public static native String getDeclRationalParameter(long a0, long a1, int a2);
+  public static native long appToAst(long a0, long a1);
+  public static native long getAppDecl(long a0, long a1);
+  public static native int getAppNumArgs(long a0, long a1);
+  public static native long getAppArg(long a0, long a1, int a2);
+  public static native boolean isEqAst(long a0, long a1, long a2);
+  public static native int getAstId(long a0, long a1);
+  public static native int getAstHash(long a0, long a1);
+  public static native long getSort(long a0, long a1);
+  public static native boolean isWellSorted(long a0, long a1);
+  public static native int getBoolValue(long a0, long a1);
+  public static native int getAstKind(long a0, long a1);
+  public static native boolean isApp(long a0, long a1);
+  public static native boolean isNumeralAst(long a0, long a1);
+  public static native boolean isAlgebraicNumber(long a0, long a1);
+  public static native long toApp(long a0, long a1);
+  public static native long toFuncDecl(long a0, long a1);
+  public static native String getNumeralString(long a0, long a1);
+  public static native String getNumeralDecimalString(long a0, long a1, int a2);
+  public static native long getNumerator(long a0, long a1);
+  public static native long getDenominator(long a0, long a1);
+  public static native boolean getNumeralSmall(long a0, long a1, Long a2, Long a3);
+  public static native boolean getNumeralInt(long a0, long a1, Integer a2);
+  public static native boolean getNumeralUint(long a0, long a1, Integer a2);
+  public static native boolean getNumeralUint64(long a0, long a1, Long a2);
+  public static native boolean getNumeralInt64(long a0, long a1, Long a2);
+  public static native boolean getNumeralRationalInt64(long a0, long a1, Long a2, Long a3);
+  public static native long getAlgebraicNumberLower(long a0, long a1, int a2);
+  public static native long getAlgebraicNumberUpper(long a0, long a1, int a2);
+  public static native long patternToAst(long a0, long a1);
+  public static native int getPatternNumTerms(long a0, long a1);
+  public static native long getPattern(long a0, long a1, int a2);
+  public static native int getIndexValue(long a0, long a1);
+  public static native boolean isQuantifierForall(long a0, long a1);
+  public static native int getQuantifierWeight(long a0, long a1);
+  public static native int getQuantifierNumPatterns(long a0, long a1);
+  public static native long getQuantifierPatternAst(long a0, long a1, int a2);
+  public static native int getQuantifierNumNoPatterns(long a0, long a1);
+  public static native long getQuantifierNoPatternAst(long a0, long a1, int a2);
+  public static native int getQuantifierNumBound(long a0, long a1);
+  public static native long getQuantifierBoundName(long a0, long a1, int a2);
+  public static native long getQuantifierBoundSort(long a0, long a1, int a2);
+  public static native long getQuantifierBody(long a0, long a1);
+  public static native long simplify(long a0, long a1);
+  public static native long simplifyEx(long a0, long a1, long a2);
+  public static native String simplifyGetHelp(long a0);
+  public static native long simplifyGetParamDescrs(long a0);
+  public static native long updateTerm(long a0, long a1, int a2, long[] a3);
+  public static native long substitute(long a0, long a1, int a2, long[] a3, long[] a4);
+  public static native long substituteVars(long a0, long a1, int a2, long[] a3);
+  public static native long translate(long a0, long a1, long a2);
+  public static native void modelIncRef(long a0, long a1);
+  public static native void modelDecRef(long a0, long a1);
+  public static native boolean modelEval(long a0, long a1, long a2, boolean a3, Long a4);
+  public static native long modelGetConstInterp(long a0, long a1, long a2);
+  public static native long modelGetFuncInterp(long a0, long a1, long a2);
+  public static native int modelGetNumConsts(long a0, long a1);
+  public static native long modelGetConstDecl(long a0, long a1, int a2);
+  public static native int modelGetNumFuncs(long a0, long a1);
+  public static native long modelGetFuncDecl(long a0, long a1, int a2);
+  public static native int modelGetNumSorts(long a0, long a1);
+  public static native long modelGetSort(long a0, long a1, int a2);
+  public static native long modelGetSortUniverse(long a0, long a1, long a2);
+  public static native boolean isAsArray(long a0, long a1);
+  public static native long getAsArrayFuncDecl(long a0, long a1);
+  public static native void funcInterpIncRef(long a0, long a1);
+  public static native void funcInterpDecRef(long a0, long a1);
+  public static native int funcInterpGetNumEntries(long a0, long a1);
+  public static native long funcInterpGetEntry(long a0, long a1, int a2);
+  public static native long funcInterpGetElse(long a0, long a1);
+  public static native int funcInterpGetArity(long a0, long a1);
+  public static native void funcEntryIncRef(long a0, long a1);
+  public static native void funcEntryDecRef(long a0, long a1);
+  public static native long funcEntryGetValue(long a0, long a1);
+  public static native int funcEntryGetNumArgs(long a0, long a1);
+  public static native long funcEntryGetArg(long a0, long a1, int a2);
+  public static native int openLog(String a0);
+  public static native void appendLog(String a0);
+  public static native void closeLog();
+  public static native void toggleWarningMessages(boolean a0);
+  public static native void setAstPrintMode(long a0, int a1);
+  public static native String astToString(long a0, long a1);
+  public static native String patternToString(long a0, long a1);
+  public static native String sortToString(long a0, long a1);
+  public static native String funcDeclToString(long a0, long a1);
+  public static native String modelToString(long a0, long a1);
+  public static native String benchmarkToSmtlibString(long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7);
+  public static native long parseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7);
+  public static native long parseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7);
+  public static native void parseSmtlibString(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7);
+  public static native void parseSmtlibFile(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7);
+  public static native int getSmtlibNumFormulas(long a0);
+  public static native long getSmtlibFormula(long a0, int a1);
+  public static native int getSmtlibNumAssumptions(long a0);
+  public static native long getSmtlibAssumption(long a0, int a1);
+  public static native int getSmtlibNumDecls(long a0);
+  public static native long getSmtlibDecl(long a0, int a1);
+  public static native int getSmtlibNumSorts(long a0);
+  public static native long getSmtlibSort(long a0, int a1);
+  public static native String getSmtlibError(long a0);
+  public static native int getErrorCode(long a0);
+  public static native void setError(long a0, int a1);
+  public static native String getErrorMsg(int a0);
+  public static native String getErrorMsgEx(long a0, int a1);
+  public static native void getVersion(Integer a0, Integer a1, Integer a2, Integer a3);
+  public static native void enableTrace(String a0);
+  public static native void disableTrace(String a0);
+  public static native void resetMemory();
+  public static native long mkFixedpoint(long a0);
+  public static native void fixedpointIncRef(long a0, long a1);
+  public static native void fixedpointDecRef(long a0, long a1);
+  public static native void fixedpointAddRule(long a0, long a1, long a2, long a3);
+  public static native void fixedpointAddFact(long a0, long a1, long a2, int a3, int[] a4);
+  public static native void fixedpointAssert(long a0, long a1, long a2);
+  public static native int fixedpointQuery(long a0, long a1, long a2);
+  public static native int fixedpointQueryRelations(long a0, long a1, int a2, long[] a3);
+  public static native long fixedpointGetAnswer(long a0, long a1);
+  public static native String fixedpointGetReasonUnknown(long a0, long a1);
+  public static native void fixedpointUpdateRule(long a0, long a1, long a2, long a3);
+  public static native int fixedpointGetNumLevels(long a0, long a1, long a2);
+  public static native long fixedpointGetCoverDelta(long a0, long a1, int a2, long a3);
+  public static native void fixedpointAddCover(long a0, long a1, int a2, long a3, long a4);
+  public static native long fixedpointGetStatistics(long a0, long a1);
+  public static native void fixedpointRegisterRelation(long a0, long a1, long a2);
+  public static native void fixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4);
+  public static native long fixedpointGetRules(long a0, long a1);
+  public static native long fixedpointGetAssertions(long a0, long a1);
+  public static native void fixedpointSetParams(long a0, long a1, long a2);
+  public static native String fixedpointGetHelp(long a0, long a1);
+  public static native long fixedpointGetParamDescrs(long a0, long a1);
+  public static native String fixedpointToString(long a0, long a1, int a2, long[] a3);
+  public static native long fixedpointFromString(long a0, long a1, String a2);
+  public static native long fixedpointFromFile(long a0, long a1, String a2);
+  public static native void fixedpointPush(long a0, long a1);
+  public static native void fixedpointPop(long a0, long a1);
+  public static native long mkAstVector(long a0);
+  public static native void astVectorIncRef(long a0, long a1);
+  public static native void astVectorDecRef(long a0, long a1);
+  public static native int astVectorSize(long a0, long a1);
+  public static native long astVectorGet(long a0, long a1, int a2);
+  public static native void astVectorSet(long a0, long a1, int a2, long a3);
+  public static native void astVectorResize(long a0, long a1, int a2);
+  public static native void astVectorPush(long a0, long a1, long a2);
+  public static native long astVectorTranslate(long a0, long a1, long a2);
+  public static native String astVectorToString(long a0, long a1);
+  public static native long mkAstMap(long a0);
+  public static native void astMapIncRef(long a0, long a1);
+  public static native void astMapDecRef(long a0, long a1);
+  public static native boolean astMapContains(long a0, long a1, long a2);
+  public static native long astMapFind(long a0, long a1, long a2);
+  public static native void astMapInsert(long a0, long a1, long a2, long a3);
+  public static native void astMapErase(long a0, long a1, long a2);
+  public static native void astMapReset(long a0, long a1);
+  public static native int astMapSize(long a0, long a1);
+  public static native long astMapKeys(long a0, long a1);
+  public static native String astMapToString(long a0, long a1);
+  public static native long mkGoal(long a0, boolean a1, boolean a2, boolean a3);
+  public static native void goalIncRef(long a0, long a1);
+  public static native void goalDecRef(long a0, long a1);
+  public static native int goalPrecision(long a0, long a1);
+  public static native void goalAssert(long a0, long a1, long a2);
+  public static native boolean goalInconsistent(long a0, long a1);
+  public static native int goalDepth(long a0, long a1);
+  public static native void goalReset(long a0, long a1);
+  public static native int goalSize(long a0, long a1);
+  public static native long goalFormula(long a0, long a1, int a2);
+  public static native int goalNumExprs(long a0, long a1);
+  public static native boolean goalIsDecidedSat(long a0, long a1);
+  public static native boolean goalIsDecidedUnsat(long a0, long a1);
+  public static native long goalTranslate(long a0, long a1, long a2);
+  public static native String goalToString(long a0, long a1);
+  public static native long mkTactic(long a0, String a1);
+  public static native void tacticIncRef(long a0, long a1);
+  public static native void tacticDecRef(long a0, long a1);
+  public static native long mkProbe(long a0, String a1);
+  public static native void probeIncRef(long a0, long a1);
+  public static native void probeDecRef(long a0, long a1);
+  public static native long tacticAndThen(long a0, long a1, long a2);
+  public static native long tacticOrElse(long a0, long a1, long a2);
+  public static native long tacticParOr(long a0, int a1, long[] a2);
+  public static native long tacticParAndThen(long a0, long a1, long a2);
+  public static native long tacticTryFor(long a0, long a1, int a2);
+  public static native long tacticWhen(long a0, long a1, long a2);
+  public static native long tacticCond(long a0, long a1, long a2, long a3);
+  public static native long tacticRepeat(long a0, long a1, int a2);
+  public static native long tacticSkip(long a0);
+  public static native long tacticFail(long a0);
+  public static native long tacticFailIf(long a0, long a1);
+  public static native long tacticFailIfNotDecided(long a0);
+  public static native long tacticUsingParams(long a0, long a1, long a2);
+  public static native long probeConst(long a0, double a1);
+  public static native long probeLt(long a0, long a1, long a2);
+  public static native long probeGt(long a0, long a1, long a2);
+  public static native long probeLe(long a0, long a1, long a2);
+  public static native long probeGe(long a0, long a1, long a2);
+  public static native long probeEq(long a0, long a1, long a2);
+  public static native long probeAnd(long a0, long a1, long a2);
+  public static native long probeOr(long a0, long a1, long a2);
+  public static native long probeNot(long a0, long a1);
+  public static native int getNumTactics(long a0);
+  public static native String getTacticName(long a0, int a1);
+  public static native int getNumProbes(long a0);
+  public static native String getProbeName(long a0, int a1);
+  public static native String tacticGetHelp(long a0, long a1);
+  public static native long tacticGetParamDescrs(long a0, long a1);
+  public static native String tacticGetDescr(long a0, String a1);
+  public static native String probeGetDescr(long a0, String a1);
+  public static native double probeApply(long a0, long a1, long a2);
+  public static native long tacticApply(long a0, long a1, long a2);
+  public static native long tacticApplyEx(long a0, long a1, long a2, long a3);
+  public static native void applyResultIncRef(long a0, long a1);
+  public static native void applyResultDecRef(long a0, long a1);
+  public static native String applyResultToString(long a0, long a1);
+  public static native int applyResultGetNumSubgoals(long a0, long a1);
+  public static native long applyResultGetSubgoal(long a0, long a1, int a2);
+  public static native long applyResultConvertModel(long a0, long a1, int a2, long a3);
+  public static native long mkSolver(long a0);
+  public static native long mkSimpleSolver(long a0);
+  public static native long mkSolverForLogic(long a0, long a1);
+  public static native long mkSolverFromTactic(long a0, long a1);
+  public static native String solverGetHelp(long a0, long a1);
+  public static native long solverGetParamDescrs(long a0, long a1);
+  public static native void solverSetParams(long a0, long a1, long a2);
+  public static native void solverIncRef(long a0, long a1);
+  public static native void solverDecRef(long a0, long a1);
+  public static native void solverPush(long a0, long a1);
+  public static native void solverPop(long a0, long a1, int a2);
+  public static native void solverReset(long a0, long a1);
+  public static native int solverGetNumScopes(long a0, long a1);
+  public static native void solverAssert(long a0, long a1, long a2);
+  public static native void solverAssertAndTrack(long a0, long a1, long a2, long a3);
+  public static native long solverGetAssertions(long a0, long a1);
+  public static native int solverCheck(long a0, long a1);
+  public static native int solverCheckAssumptions(long a0, long a1, int a2, long[] a3);
+  public static native long solverGetModel(long a0, long a1);
+  public static native long solverGetProof(long a0, long a1);
+  public static native long solverGetUnsatCore(long a0, long a1);
+  public static native String solverGetReasonUnknown(long a0, long a1);
+  public static native long solverGetStatistics(long a0, long a1);
+  public static native String solverToString(long a0, long a1);
+  public static native String statsToString(long a0, long a1);
+  public static native void statsIncRef(long a0, long a1);
+  public static native void statsDecRef(long a0, long a1);
+  public static native int statsSize(long a0, long a1);
+  public static native String statsGetKey(long a0, long a1, int a2);
+  public static native boolean statsIsUint(long a0, long a1, int a2);
+  public static native boolean statsIsDouble(long a0, long a1, int a2);
+  public static native int statsGetUintValue(long a0, long a1, int a2);
+  public static native double statsGetDoubleValue(long a0, long a1, int a2);
+  public static native long mkInjectiveFunction(long a0, long a1, int a2, long[] a3, long a4);
+  public static native void setLogic(long a0, String a1);
+  public static native void push(long a0);
+  public static native void pop(long a0, int a1);
+  public static native int getNumScopes(long a0);
+  public static native void persistAst(long a0, long a1, int a2);
+  public static native void assertCnstr(long a0, long a1);
+  public static native int checkAndGetModel(long a0, Long a1);
+  public static native int check(long a0);
+  public static native int checkAssumptions(long a0, int a1, long[] a2, Long a3, Long a4, Integer a5, long[] a6);
+  public static native int getImpliedEqualities(long a0, int a1, long[] a2, int[] a3);
+  public static native void delModel(long a0, long a1);
+  public static native void softCheckCancel(long a0);
+  public static native int getSearchFailure(long a0);
+  public static native long mkLabel(long a0, long a1, boolean a2, long a3);
+  public static native long getRelevantLabels(long a0);
+  public static native long getRelevantLiterals(long a0);
+  public static native long getGuessedLiterals(long a0);
+  public static native void delLiterals(long a0, long a1);
+  public static native int getNumLiterals(long a0, long a1);
+  public static native long getLabelSymbol(long a0, long a1, int a2);
+  public static native long getLiteral(long a0, long a1, int a2);
+  public static native void disableLiteral(long a0, long a1, int a2);
+  public static native void blockLiterals(long a0, long a1);
+  public static native int getModelNumConstants(long a0, long a1);
+  public static native long getModelConstant(long a0, long a1, int a2);
+  public static native int getModelNumFuncs(long a0, long a1);
+  public static native long getModelFuncDecl(long a0, long a1, int a2);
+  public static native boolean evalFuncDecl(long a0, long a1, long a2, Long a3);
+  public static native boolean isArrayValue(long a0, long a1, long a2, Integer a3);
+  public static native void getArrayValue(long a0, long a1, long a2, int a3, long[] a4, long[] a5, Long a6);
+  public static native long getModelFuncElse(long a0, long a1, int a2);
+  public static native int getModelFuncNumEntries(long a0, long a1, int a2);
+  public static native int getModelFuncEntryNumArgs(long a0, long a1, int a2, int a3);
+  public static native long getModelFuncEntryArg(long a0, long a1, int a2, int a3, int a4);
+  public static native long getModelFuncEntryValue(long a0, long a1, int a2, int a3);
+  public static native boolean eval(long a0, long a1, long a2, Long a3);
+  public static native boolean evalDecl(long a0, long a1, long a2, int a3, long[] a4, Long a5);
+  public static native String contextToString(long a0);
+  public static native String statisticsToString(long a0);
+  public static native long getContextAssignment(long a0);
+  public static void main(String[] args) {
+     Integer major = 0, minor = 0, build = 0, revision = 0;
+     getVersion(major, minor, build, revision);
+     System.out.format("Z3 (for Java) %d.%d.%d%n", major, minor, build);
+  }
+}

src/api/java/com/Microsoft/Z3/Numeral.java

@@ -0,0 +1,262 @@
+/**
+ * This file was automatically generated from Numeral.cs 
+ **/
+
+package com.Microsoft.Z3;
+/* using System; */
+
+/* using System.Numerics; */
+
+    /**
+     * Integer Numerals
+     **/
+    public class IntNum extends IntExpr
+    {
+
+        IntNum(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+
+
+        /**
+         * Retrieve the 64-bit unsigned integer value.
+         **/
+        public UInt64 UInt64() 
+            {
+                UInt64 res = 0;
+                if (Native.getNumeralInteger64(Context.nCtx, NativeObject, res) == 0)
+                    throw new Z3Exception("Numeral is not a 64 bit unsigned");
+                return res;
+        }
+
+        /**
+         * Retrieve the int value.
+         **/
+        public int Int() 
+            {
+                int res = 0;
+                if (Native.getNumeralInt(Context.nCtx, NativeObject, res) == 0)
+                    throw new Z3Exception("Numeral is not an int");
+                return res;
+        }
+
+        /**
+         * Retrieve the 64-bit int value.
+         **/
+        public Int64 Int64() 
+            {
+                Int64 res = 0;
+                if (Native.getNumeralInt64(Context.nCtx, NativeObject, res) == 0)
+                    throw new Z3Exception("Numeral is not an int64");
+                return res;
+        }
+
+        /**
+         * Retrieve the int value.
+         **/
+        public Integer UInt() 
+            {
+                Integer res = 0;
+                if (Native.getNumeralInteger(Context.nCtx, NativeObject, res) == 0)
+                    throw new Z3Exception("Numeral is not a Integer");
+                return res;
+        }
+
+        /**
+         * Retrieve the BigInteger value.
+         **/
+        public BigInteger BigInteger() 
+            {  
+                return BigInteger.Parse(this.toString());
+        }
+
+        /**
+         * Returns a string representation of the numeral.
+         **/
+        public String toString()
+        {
+            return Native.getNumeralString(Context.nCtx, NativeObject);
+        }
+    }
+
+    /**
+     * Rational Numerals
+     **/
+    public class RatNum extends RealExpr
+    {
+        /**
+         * The numerator of a rational numeral.
+         **/
+        public IntNum Numerator()  {
+                
+
+                return new IntNum(Context, Native.getNumerator(Context.nCtx, NativeObject)); }
+
+        /**
+         * The denominator of a rational numeral.
+         **/
+        public IntNum Denominator()  {
+                
+
+                return new IntNum(Context, Native.getDenominator(Context.nCtx, NativeObject)); }
+
+        /**
+         * Converts the numerator of the rational to a BigInteger
+         **/
+        public BigInteger BigIntNumerator() 
+            {                
+                IntNum n = Numerator;
+                return BigInteger.Parse(n.toString());
+        }
+
+        /**
+         * Converts the denominator of the rational to a BigInteger
+         **/
+        public BigInteger BigIntDenominator() 
+            {
+                IntNum n = Denominator;
+                return BigInteger.Parse(n.toString());
+        }
+
+        /**
+         * Returns a string representation in decimal notation.
+         * <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>    
+         **/
+        public String ToDecimalString(Integer precision)
+        {
+            return Native.getNumeralDecimalString(Context.nCtx, NativeObject, precision);
+        }
+
+        /**
+         * Returns a string representation of the numeral.
+         **/
+        public String toString()
+        {
+            return Native.getNumeralString(Context.nCtx, NativeObject);
+        }
+
+        RatNum(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+    }
+
+
+    /**
+     * Bit-vector numerals
+     **/
+    public class BitVecNum extends BitVecExpr
+    {
+        /**
+         * Retrieve the 64-bit unsigned integer value.
+         **/
+        public UInt64 UInt64() 
+            {
+                UInt64 res = 0;
+                if (Native.getNumeralInteger64(Context.nCtx, NativeObject, res) == 0)
+                    throw new Z3Exception("Numeral is not a 64 bit unsigned");
+                return res;
+        }
+
+        /**
+         * Retrieve the int value.
+         **/
+        public int Int() 
+            {
+                int res = 0;
+                if (Native.getNumeralInt(Context.nCtx, NativeObject, res) == 0)
+                    throw new Z3Exception("Numeral is not an int");
+                return res;
+        }
+
+        /**
+         * Retrieve the 64-bit int value.
+         **/
+        public Int64 Int64() 
+            {
+                Int64 res = 0;
+                if (Native.getNumeralInt64(Context.nCtx, NativeObject, res) == 0)
+                    throw new Z3Exception("Numeral is not an int64");
+                return res;
+        }
+
+        /**
+         * Retrieve the int value.
+         **/
+        public Integer UInt() 
+            {
+                Integer res = 0;
+                if (Native.getNumeralInteger(Context.nCtx, NativeObject, res) == 0)
+                    throw new Z3Exception("Numeral is not a Integer");
+                return res;
+        }
+
+        /**
+         * Retrieve the BigInteger value.
+         **/
+        public BigInteger BigInteger() 
+            {
+                return BigInteger.Parse(this.toString());
+        }
+
+        /**
+         * Returns a string representation of the numeral.
+         **/
+        public String toString()
+        {
+            return Native.getNumeralString(Context.nCtx, NativeObject);
+        }
+
+        BitVecNum(Context ctx, IntPtr obj) { super(ctx, obj);  }
+    }
+
+    /**
+     * Algebraic numbers
+     **/
+    public class AlgebraicNum extends ArithExpr
+    {
+        /**
+         * Return a upper bound for a given real algebraic number. 
+         * The interval isolating the number is smaller than 1/10^<paramref name="precision"/>.    
+         * <seealso cref="Expr.IsAlgebraicNumber"/>   
+         * <param name="precision">the precision of the result</param>
+         * @return A numeral Expr of sort Real
+         **/
+        public RatNum ToUpper(Integer precision)
+        {
+            
+
+            return new RatNum(Context, Native.getAlgebraicNumberUpper(Context.nCtx, NativeObject, precision));
+        }
+
+        /**
+         * Return a lower bound for the given real algebraic number. 
+         * The interval isolating the number is smaller than 1/10^<paramref name="precision"/>.    
+         * <seealso cref="Expr.IsAlgebraicNumber"/>
+         * <param name="precision"></param>
+         * @return A numeral Expr of sort Real
+         **/
+        public RatNum ToLower(Integer precision)
+        {
+            
+
+            return new RatNum(Context, Native.getAlgebraicNumberLower(Context.nCtx, NativeObject, precision));
+        }
+
+        /**
+         * Returns a string representation in decimal notation.
+         * <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>    
+         **/
+        public String ToDecimal(Integer precision)
+        {
+            
+
+            return Native.getNumeralDecimalString(Context.nCtx, NativeObject, precision);
+        }
+
+        AlgebraicNum(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+    }

src/api/java/com/Microsoft/Z3/ParamDescrs.java

@@ -0,0 +1,87 @@
+/**
+ * This file was automatically generated from ParamDescrs.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * A ParamDescrs describes a set of parameters.
+     **/
+    public class ParamDescrs extends Z3Object
+    {
+        /**
+         * validate a set of parameters.
+         **/
+        public void Validate(Params p)
+        {
+            
+            Native.paramsValidate(Context.nCtx, p.NativeObject, NativeObject);
+        }
+
+        /**
+         * Retrieve kind of parameter.
+         **/
+        public Z3ParamKind GetKind(Symbol name)
+        {
+            
+            return (Z3ParamKind)Native.paramDescrsGetKind(Context.nCtx, NativeObject, name.NativeObject);
+        }
+
+        /**
+         * Retrieve all names of parameters.
+         **/
+        public Symbol[] Names() 
+            {
+                  Integer sz = Native.paramDescrsSize(Context.nCtx, NativeObject);
+                  Symbol[] names = new Symbol[sz];
+                  for (Integer i = 0; i < sz; ++i) {
+                      names[i] = Symbol.Create(Context, Native.paramDescrsGetName(Context.nCtx, NativeObject, i));
+                  return names;
+            }
+        }
+
+        /**
+         * The size of the ParamDescrs.
+         **/
+        public Integer Size()  { return Native.paramDescrsSize(Context.nCtx, NativeObject); }
+
+        /**
+         * Retrieves a string representation of the ParamDescrs. 
+         **/
+        public String toString()
+        {
+            return Native.paramDescrstoString(Context.nCtx, NativeObject); 
+        }
+
+        ParamDescrs(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+
+        class DecRefQueue extends Z3.DecRefQueue
+        {
+            public void IncRef(Context ctx, IntPtr obj)
+            {
+                Native.paramDescrsIncRef(ctx.nCtx, obj);
+            }
+
+            public void DecRef(Context ctx, IntPtr obj)
+            {
+                Native.paramDescrsDecRef(ctx.nCtx, obj);
+            }
+        };        
+
+        void IncRef(IntPtr o)
+        {
+            Context.ParamDescrsDRQ.IncAndClear(Context, o);
+            super.IncRef(o);
+        }
+
+        void DecRef(IntPtr o)
+        {
+            Context.ParamDescrsDRQ.Add(o);
+            super.DecRef(o);
+        }
+    }

src/api/java/com/Microsoft/Z3/Params.java

@@ -0,0 +1,126 @@
+/**
+ * This file was automatically generated from Params.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * A ParameterSet represents a configuration in the form of Symbol/value pairs.
+     **/
+    public class Params extends Z3Object
+    {
+        /**
+         * Adds a parameter setting.
+         **/
+        public void Add(Symbol name, boolean value)
+        {
+            
+
+            Native.paramsSetBoolean(Context.nCtx, NativeObject, name.NativeObject, (value) ? 1 : 0);
+        }
+
+        /**
+         * Adds a parameter setting.
+         **/
+        public void Add(Symbol name, Integer value)
+        {
+            
+
+            Native.paramsSetInteger(Context.nCtx, NativeObject, name.NativeObject, value);
+        }
+
+        /**
+         * Adds a parameter setting.
+         **/
+        public void Add(Symbol name, double value)
+        {
+            
+            
+            Native.paramsSetDouble(Context.nCtx, NativeObject, name.NativeObject, value);
+        }
+
+        /**
+         * Adds a parameter setting.
+         **/
+        public void Add(Symbol name, Symbol value)
+        {
+            
+            
+
+            Native.paramsSetSymbol(Context.nCtx, NativeObject, name.NativeObject, value.NativeObject);
+        }
+
+        /**
+         * Adds a parameter setting.
+         **/
+        public void Add(String name, boolean value)
+        {
+            Native.paramsSetBoolean(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value) ? 1 : 0);
+        }
+
+        /**
+         * Adds a parameter setting.
+         **/
+        public void Add(String name, Integer value)
+        {
+            Native.paramsSetInteger(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
+        }
+
+        /**
+         * Adds a parameter setting.
+         **/
+        public void Add(String name, double value)
+        {
+            Native.paramsSetDouble(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
+        }
+
+        /**
+         * Adds a parameter setting.
+         **/
+        public void Add(String name, Symbol value)
+        {
+            
+
+            Native.paramsSetSymbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value.NativeObject);
+        }
+
+        /**
+         * A string representation of the parameter set.
+         **/
+        public String toString()
+        {
+            return Native.paramstoString(Context.nCtx, NativeObject);
+        }
+
+        Params(Context ctx)
+            { super(ctx, Native.mkParams(ctx.nCtx));
+            
+        }
+
+        class DecRefQueue extends Z3.DecRefQueue
+        {
+            public void IncRef(Context ctx, IntPtr obj)
+            {
+                Native.paramsIncRef(ctx.nCtx, obj);
+            }
+
+            public void DecRef(Context ctx, IntPtr obj)
+            {
+                Native.paramsDecRef(ctx.nCtx, obj);
+            }
+        };        
+
+        void IncRef(IntPtr o)
+        {
+            Context.ParamsDRQ.IncAndClear(Context, o);
+            super.IncRef(o);
+        }
+
+        void DecRef(IntPtr o)
+        {
+            Context.ParamsDRQ.Add(o);
+            super.DecRef(o);
+        }
+    }

src/api/java/com/Microsoft/Z3/Pattern.java

@@ -0,0 +1,48 @@
+/**
+ * This file was automatically generated from Pattern.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+/* using System.Runtime.InteropServices; */
+
+    /**
+     * Patterns comprise a list of terms. The list should be
+     * non-empty.  If the list comprises of more than one term, it is
+     * also called a multi-pattern.
+     **/
+    public class Pattern extends AST
+    {
+        /**
+         * The number of terms in the pattern.
+         **/
+        public Integer NumTerms()  { return Native.getPatternNumTerms(Context.nCtx, NativeObject); }
+
+        /**
+         * The terms in the pattern.
+         **/
+        public Expr[] Terms() 
+            {
+                
+
+                Integer n = NumTerms;
+                Expr[] res = new Expr[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = Expr.Create(Context, Native.getPattern(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        /**
+         * A string representation of the pattern.
+         **/
+        public String toString()
+        {
+            return Native.patterntoString(Context.nCtx, NativeObject);
+        }
+
+        Pattern(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+    }

src/api/java/com/Microsoft/Z3/Probe.java

@@ -0,0 +1,72 @@
+/**
+ * This file was automatically generated from Probe.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+/* using System.Runtime.InteropServices; */
+
+    /**  
+     * Probes are used to inspect a goal (aka problem) and collect information that may be used to decide
+     * which solver and/or preprocessing step will be used.
+     * The complete list of probes may be obtained using the procedures <code>Context.NumProbes</code>
+     * and <code>Context.ProbeNames</code>.
+     * It may also be obtained using the command <code>(help-tactics)</code> in the SMT 2.0 front-end.
+     **/
+    public class Probe extends Z3Object
+    {
+        /**
+         * Execute the probe over the goal. 
+         * @return A probe always produce a double value.
+         * "Boolean" probes return 0.0 for false, and a value different from 0.0 for true.
+         **/
+        public double Apply(Goal g)
+        {
+            
+
+            Context.CheckContextMatch(g);
+            return Native.probeApply(Context.nCtx, NativeObject, g.NativeObject);
+        }
+
+        /**
+         * Apply the probe to a goal.
+         **/
+        public double this[Goal() 
+            
+
+            return Apply(g); } }
+
+        Probe(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        Probe(Context ctx, String name)
+            { super(ctx, Native.mkProbe(ctx.nCtx, name));
+            
+        }
+
+        class DecRefQueue extends Z3.DecRefQueue
+        {
+            public void IncRef(Context ctx, IntPtr obj)
+            {
+                Native.probeIncRef(ctx.nCtx, obj);
+            }
+
+            public void DecRef(Context ctx, IntPtr obj)
+            {
+                Native.probeDecRef(ctx.nCtx, obj);
+            }
+        };        
+
+        void IncRef(IntPtr o)
+        {
+            Context.ProbeDRQ.IncAndClear(Context, o);
+            super.IncRef(o);
+        }
+
+        void DecRef(IntPtr o)
+        {
+            Context.ProbeDRQ.Add(o);
+            super.DecRef(o);
+        }
+    }

src/api/java/com/Microsoft/Z3/Quantifier.java

@@ -0,0 +1,198 @@
+/**
+ * This file was automatically generated from Quantifier.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * Quantifier expressions.
+     **/
+    public class Quantifier extends BoolExpr
+    {
+        /**
+         * Indicates whether the quantifier is universal.
+         **/
+        public boolean IsUniversal()  { return Native.isQuantifierForall(Context.nCtx, NativeObject) != 0; }
+
+        /**
+         * Indicates whether the quantifier is existential.
+         **/
+        public boolean IsExistential()  { return !IsUniversal; }
+
+        /**
+         * The weight of the quantifier.
+         **/
+        public Integer Weight()  { return Native.getQuantifierWeight(Context.nCtx, NativeObject); }
+
+        /**
+         * The number of patterns.
+         **/
+        public Integer NumPatterns()  { return Native.getQuantifierNumPatterns(Context.nCtx, NativeObject); }
+
+        /**
+         * The patterns.
+         **/
+        public Pattern[] Patterns() 
+            {
+                
+
+                Integer n = NumPatterns;
+                Pattern[] res = new Pattern[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = new Pattern(Context, Native.getQuantifierPatternAst(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        /**
+         * The number of no-patterns.
+         **/
+        public Integer NumNoPatterns()  { return Native.getQuantifierNumNoPatterns(Context.nCtx, NativeObject); }
+
+        /**
+         * The no-patterns.
+         **/
+        public Pattern[] NoPatterns() 
+            {
+                
+
+                Integer n = NumNoPatterns;
+                Pattern[] res = new Pattern[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = new Pattern(Context, Native.getQuantifierNoPatternAst(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        /**
+         * The number of bound variables.
+         **/
+        public Integer NumBound()  { return Native.getQuantifierNumBound(Context.nCtx, NativeObject); }
+
+        /**
+         * The symbols for the bound variables.
+         **/
+        public Symbol[] BoundVariableNames() 
+            {
+                
+
+                Integer n = NumBound;
+                Symbol[] res = new Symbol[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = Symbol.Create(Context, Native.getQuantifierBoundName(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        /**
+         * The sorts of the bound variables.
+         **/
+        public Sort[] BoundVariableSorts() 
+            {
+                
+
+                Integer n = NumBound;
+                Sort[] res = new Sort[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = Sort.Create(Context, Native.getQuantifierBoundSort(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        /**
+         * The body of the quantifier.
+         **/
+        public BoolExpr Body()  {
+                
+                
+                return new BoolExpr(Context, Native.getQuantifierBody(Context.nCtx, NativeObject)); }
+
+        Quantifier(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body,
+                            Integer weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null,
+                            Symbol quantifierID = null, Symbol skolemID = null
+                            )
+            { super(ctx);
+            
+            
+            
+            
+            
+            
+            
+            
+            
+
+            Context.CheckContextMatch(patterns);
+            Context.CheckContextMatch(noPatterns);
+            Context.CheckContextMatch(sorts);
+            Context.CheckContextMatch(names);
+            Context.CheckContextMatch(body);
+
+            if (sorts.Length != names.Length)
+                throw new Z3Exception("Number of sorts does not match number of names");
+
+            IntPtr[] Patterns = AST.ArrayToNative(patterns);
+
+            if (noPatterns == null && quantifierID == null && skolemID == null)
+            {
+                NativeObject = Native.mkQuantifier(ctx.nCtx, (isForall) ? 1 : 0, weight,
+                                           AST.ArrayLength(patterns),  AST.ArrayToNative(patterns),
+                                           AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
+                                           Symbol.ArrayToNative(names),
+                                           body.NativeObject);
+            }
+            else
+            {
+                NativeObject = Native.mkQuantifierEx(ctx.nCtx, (isForall) ? 1 : 0, weight,
+                                  AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
+                                  AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
+                                  AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
+                                  AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
+                                  Symbol.ArrayToNative(names),
+                                  body.NativeObject);
+            }
+        }
+
+        Quantifier(Context ctx, boolean isForall, Expr[] bound, Expr body,
+                            Integer weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null,
+                            Symbol quantifierID = null, Symbol skolemID = null
+            )
+            { super(ctx);
+            
+            
+
+                   
+            
+            
+
+            Context.CheckContextMatch(noPatterns);
+            Context.CheckContextMatch(patterns);
+            //Context.CheckContextMatch(bound);
+            Context.CheckContextMatch(body);
+            
+            if (noPatterns == null && quantifierID == null && skolemID == null)
+            {
+                NativeObject = Native.mkQuantifierConst(ctx.nCtx, (isForall) ? 1 : 0, weight,
+                                                 AST.ArrayLength(bound), AST.ArrayToNative(bound),
+                                                 AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
+                                                 body.NativeObject);
+            }
+            else
+            {
+                NativeObject = Native.mkQuantifierConstEx(ctx.nCtx, (isForall) ? 1 : 0, weight,
+                                        AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
+                                        AST.ArrayLength(bound), AST.ArrayToNative(bound),
+                                        AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
+                                        AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
+                                        body.NativeObject);
+            }
+        }
+
+
+        Quantifier(Context ctx, IntPtr obj) { super(ctx, obj);  }
+
+        void CheckNativeObject(IntPtr obj)
+        {
+            if ((Z3AstKind)Native.getAstKind(Context.nCtx, obj) != Z3AstKind.Z3QUANTIFIERAST)
+                throw new Z3Exception("Underlying object is not a quantifier");
+            super.CheckNativeObject(obj);
+        }
+    }

src/api/java/com/Microsoft/Z3/Solver.java

@@ -0,0 +1,247 @@
+/**
+ * This file was automatically generated from Solver.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * Solvers.
+     **/
+    public class Solver extends Z3Object
+    {
+        /**
+         * A string that describes all available solver parameters.
+         **/
+        public String Help() 
+            {
+                
+
+                return Native.solverGetHelp(Context.nCtx, NativeObject);
+        }
+
+        /**
+         * Sets the solver parameters.
+         **/
+        public void setParameters(Params value) 
+            {
+                
+
+                Context.CheckContextMatch(value);
+                Native.solverSetParams(Context.nCtx, NativeObject, value.NativeObject);
+        }
+
+        /**
+         * Retrieves parameter descriptions for solver.
+         **/
+        public ParamDescrs ParameterDescriptions()  { return new ParamDescrs(Context, Native.solverGetParamDescrs(Context.nCtx, NativeObject)); }
+
+
+        /**
+         * The current number of backtracking points (scopes).
+         * <seealso cref="Pop"/>
+         * <seealso cref="Push"/>
+         **/
+        public Integer NumScopes()  { return Native.solverGetNumScopes(Context.nCtx, NativeObject); }
+
+        /**
+         * Creates a backtracking point.
+         * <seealso cref="Pop"/>
+         **/
+        public void Push()
+        {
+            Native.solverPush(Context.nCtx, NativeObject);
+        }
+
+        /**
+         * Backtracks <paramref name="n"/> backtracking points.
+         * <remarks>Note that an exception is thrown if <paramref name="n"/> is not smaller than <code>NumScopes</code></remarks>
+         * <seealso cref="Push"/>
+         **/
+        public void Pop(Integer n)
+        {
+            Native.solverPop(Context.nCtx, NativeObject, n);
+        }
+
+        /**
+         * Resets the Solver.
+         * <remarks>This removes all assertions from the solver.</remarks>
+         **/
+        public void Reset()
+        {
+            Native.solverReset(Context.nCtx, NativeObject);
+        }
+
+        /**
+         * Assert a constraint (or multiple) into the solver.
+         **/
+        public void Assert(BoolExpr[] constraints)
+        {
+            
+            
+
+            Context.CheckContextMatch(constraints);
+            for (BoolExpr.Iterator a = constraints.iterator(); a.hasNext(); )
+            {
+                Native.solverAssert(Context.nCtx, NativeObject, a.NativeObject);
+            }
+        }
+
+        /**
+         * The number of assertions in the solver.
+         **/
+        public Integer NumAssertions() 
+            {
+                ASTVector ass = new ASTVector(Context, Native.solverGetAssertions(Context.nCtx, NativeObject));
+                return ass.Size;
+        }
+
+        /**
+         * The set of asserted formulas.
+         **/
+        public BoolExpr[] Assertions() 
+            {
+                
+
+                ASTVector ass = new ASTVector(Context, Native.solverGetAssertions(Context.nCtx, NativeObject));
+                Integer n = ass.Size;
+                BoolExpr[] res = new BoolExpr[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = new BoolExpr(Context, ass[i].NativeObject);
+                return res;
+        }
+
+        /**
+         * Checks whether the assertions in the solver are consistent or not.
+         * <remarks>
+         * <seealso cref="Model"/>
+         * <seealso cref="UnsatCore"/>
+         * <seealso cref="Proof"/>    
+         * </remarks>    
+         **/
+        public Status Check(Expr[] assumptions)
+        {
+            Z3Lboolean r;
+            if (assumptions == null)
+                r = (Z3Lboolean)Native.solverCheck(Context.nCtx, NativeObject);
+            else
+                r = (Z3Lboolean)Native.solverCheckAssumptions(Context.nCtx, NativeObject, (Integer)assumptions.Length, AST.ArrayToNative(assumptions));
+            switch (r)
+            {
+                case Z3Lboolean.Z3LTRUE: return Status.SATISFIABLE;
+                case Z3Lboolean.Z3LFALSE: return Status.UNSATISFIABLE;
+                default: return Status.UNKNOWN;
+            }
+        }
+
+        /**
+         * The model of the last <code>Check</code>.
+         * <remarks>
+         * The result is <code>null</code> if <code>Check</code> was not invoked before,
+         * if its results was not <code>SATISFIABLE</code>, or if model production is not enabled.
+         * </remarks>
+         **/
+        public Model Model() 
+            {
+                IntPtr x = Native.solverGetModel(Context.nCtx, NativeObject);
+                if (x == IntPtr.Zero)
+                    return null;
+                else
+                    return new Model(Context, x);
+        }
+
+        /**
+         * The proof of the last <code>Check</code>.
+         * <remarks>    
+         * The result is <code>null</code> if <code>Check</code> was not invoked before,
+         * if its results was not <code>UNSATISFIABLE</code>, or if proof production is disabled.
+         * </remarks>
+         **/
+        public Expr Proof() 
+            {
+                IntPtr x = Native.solverGetProof(Context.nCtx, NativeObject);
+                if (x == IntPtr.Zero)
+                    return null;
+                else
+                    return Expr.Create(Context, x);
+        }
+
+        /**
+         * The unsat core of the last <code>Check</code>.
+         * <remarks>
+         * The unsat core is a subset of <code>Assertions</code>
+         * The result is empty if <code>Check</code> was not invoked before,
+         * if its results was not <code>UNSATISFIABLE</code>, or if core production is disabled.
+         * </remarks>
+         **/
+        public Expr[] UnsatCore() 
+            {
+                
+
+                ASTVector core = new ASTVector(Context, Native.solverGetUnsatCore(Context.nCtx, NativeObject));
+                Integer n = core.Size;
+                Expr[] res = new Expr[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = Expr.Create(Context, core[i].NativeObject);
+                return res;
+        }
+
+        /**
+         * A brief justification of why the last call to <code>Check</code> returned <code>UNKNOWN</code>.
+         **/
+        public String ReasonUnknown() 
+            {
+                
+
+                return Native.solverGetReasonUnknown(Context.nCtx, NativeObject);
+        }
+
+        /**
+         * Solver statistics.
+         **/
+        public Statistics Statistics() 
+            {
+                
+
+                return new Statistics(Context, Native.solverGetStatistics(Context.nCtx, NativeObject));
+        }
+
+        /**
+         * A string representation of the solver.
+         **/
+        public String toString()
+        {
+            return Native.solvertoString(Context.nCtx, NativeObject);
+        }
+
+        Solver(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+
+        class DecRefQueue extends Z3.DecRefQueue
+        {
+            public void IncRef(Context ctx, IntPtr obj)
+            {
+                Native.solverIncRef(ctx.nCtx, obj);
+            }
+
+            public void DecRef(Context ctx, IntPtr obj)
+            {
+                Native.solverDecRef(ctx.nCtx, obj);
+            }
+        };
+
+        void IncRef(IntPtr o)
+        {
+            Context.SolverDRQ.IncAndClear(Context, o);
+            super.IncRef(o);
+        }
+
+        void DecRef(IntPtr o)
+        {
+            Context.SolverDRQ.Add(o);
+            super.DecRef(o);
+        }
+    }

src/api/java/com/Microsoft/Z3/Sort.java

@@ -0,0 +1,579 @@
+/**
+ * This file was automatically generated from Sort.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * The Sort class implements type information for ASTs.
+     **/
+    public class Sort extends AST
+    {
+        /**
+         * Comparison operator.
+         * <param name="a">A Sort</param>
+         * <param name="b">A Sort</param>
+         * @return True if <paramref name="a"/> and <paramref name="b"/> are from the same context 
+         * and represent the same sort; false otherwise.
+         **/
+         /* Overloaded operators are not translated. */
+
+        /**
+         * Comparison operator.
+         * <param name="a">A Sort</param>
+         * <param name="b">A Sort</param>
+         * @return True if <paramref name="a"/> and <paramref name="b"/> are not from the same context 
+         * or represent different sorts; false otherwise.
+         **/
+         /* Overloaded operators are not translated. */
+
+        /**
+         * Equality operator for objects of type Sort.
+         * <param name="o"></param>
+         * @return 
+         **/
+        public boolean Equals(object o)
+        {
+            Sort casted = o as Sort;
+            if (casted == null) return false;
+            return this == casted;
+        }
+
+        /**
+         * Hash code generation for Sorts
+         * @return A hash code
+         **/
+        public int GetHashCode()
+        {
+            return super.GetHashCode();
+        }
+
+        /**
+         * Returns a unique identifier for the sort.
+         **/
+        new public Integer Id()  { return Native.getSortId(Context.nCtx, NativeObject); }
+
+        /**
+         * The kind of the sort.
+         **/
+        public Z3_sort_kind SortKind()  { return (Z3SortKind)Native.getSortKind(Context.nCtx, NativeObject); }
+
+        /**
+         * The name of the sort
+         **/
+        public Symbol Name()  {
+                
+                return Symbol.Create(Context, Native.getSortName(Context.nCtx, NativeObject)); }
+
+        /**
+         * A string representation of the sort.
+         **/
+        public String toString()
+        {
+            return Native.sorttoString(Context.nCtx, NativeObject);
+        }
+
+        /**
+         * Sort constructor
+         **/
+        protected Sort(Context ctx) { super(ctx);  }
+        Sort(Context ctx, IntPtr obj) { super(ctx, obj);  }
+
+        void CheckNativeObject(IntPtr obj)
+        {
+            if (Native.getAstKind(Context.nCtx, obj) != (Integer)Z3AstKind.Z3SORTAST)
+                throw new Z3Exception("Underlying object is not a sort");
+            super.CheckNativeObject(obj);
+        }
+
+        new static Sort Create(Context ctx, IntPtr obj)
+        {
+            
+            
+
+            switch ((Z3SortKind)Native.getSortKind(ctx.nCtx, obj))
+            {
+                case Z3SortKind.Z3ARRAYSORT: return new ArraySort(ctx, obj);
+                case Z3SortKind.Z3BOOLSORT: return new BoolSort(ctx, obj);
+                case Z3SortKind.Z3BVSORT: return new BitVecSort(ctx, obj);
+                case Z3SortKind.Z3DATATYPESORT: return new DatatypeSort(ctx, obj);
+                case Z3SortKind.Z3INTSORT: return new IntSort(ctx, obj);
+                case Z3SortKind.Z3REALSORT: return new RealSort(ctx, obj);
+                case Z3SortKind.Z3UNINTERPRETEDSORT: return new UninterpretedSort(ctx, obj);
+                case Z3SortKind.Z3FINITEDOMAINSORT: return new FiniteDomainSort(ctx, obj);
+                case Z3SortKind.Z3RELATIONSORT: return new RelationSort(ctx, obj);
+                default:
+                    throw new Z3Exception("Unknown sort kind");
+            }
+        }
+    }
+
+    /**
+     * A Boolean sort.
+     **/
+    public class BoolSort extends Sort
+    {
+        BoolSort(Context ctx, IntPtr obj) { super(ctx, obj);  }
+        BoolSort(Context ctx) { super(ctx, Native.mkBooleanSort(ctx.nCtx));  }
+    };
+
+    /**
+     * An arithmetic sort, i.e., Int or Real.
+     **/
+    public class ArithSort extends Sort
+    {
+        ArithSort(Context ctx, IntPtr obj) { super(ctx, obj);  }
+    };
+
+    /**
+     *  An Integer sort
+     **/
+    public class IntSort extends ArithSort
+    {
+        IntSort(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+        IntSort(Context ctx)
+            { super(ctx, Native.mkIntSort(ctx.nCtx));
+            
+        }
+    }
+
+    /**
+     * A real sort
+     **/
+    public class RealSort extends ArithSort
+    {
+        RealSort(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+        RealSort(Context ctx)
+            { super(ctx, Native.mkRealSort(ctx.nCtx));
+            
+        }
+    }
+
+    /**
+     * Bit-vector sorts.
+     **/
+    public class BitVecSort extends Sort
+    {
+        /**
+         * The size of the bit-vector sort.
+         **/
+        public Integer Size()  { return Native.getBvSortSize(Context.nCtx, NativeObject); }
+
+        BitVecSort(Context ctx, IntPtr obj) { super(ctx, obj);  }
+        BitVecSort(Context ctx, Integer size) { super(ctx, Native.mkBvSort(ctx.nCtx, size));  }
+    };
+
+    /**
+     * Array sorts.
+     **/
+    public class ArraySort extends Sort
+    {
+        /**
+         * The domain of the array sort.
+         **/
+        public Sort Domain()  {
+                
+
+                return Sort.Create(Context, Native.getArraySortDomain(Context.nCtx, NativeObject)); }
+
+        /**
+         * The range of the array sort.
+         **/
+        public Sort Range()  {
+                
+
+                return Sort.Create(Context, Native.getArraySortRange(Context.nCtx, NativeObject)); }
+
+        ArraySort(Context ctx, IntPtr obj) { super(ctx, obj);  }
+        ArraySort(Context ctx, Sort domain, Sort range)
+            { super(ctx, Native.mkArraySort(ctx.nCtx, domain.NativeObject, range.NativeObject));
+            
+            
+            
+        }
+    };
+
+    /**
+     * Datatype sorts.
+     **/
+    public class DatatypeSort extends Sort
+    {
+        /**
+         * The number of constructors of the datatype sort.
+         **/
+        public Integer NumConstructors()  { return Native.getDatatypeSortNumConstructors(Context.nCtx, NativeObject); }
+
+        /**
+         * The constructors.
+         **/
+        public FuncDecl[] Constructors() 
+            {
+                
+
+                Integer n = NumConstructors;
+                FuncDecl[] res = new FuncDecl[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = new FuncDecl(Context, Native.getDatatypeSortConstructor(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        /**
+         * The recognizers.
+         **/
+        public FuncDecl[] Recognizers() 
+            {
+                
+
+                Integer n = NumConstructors;
+                FuncDecl[] res = new FuncDecl[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = new FuncDecl(Context, Native.getDatatypeSortRecognizer(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        /**
+         * The constructor accessors.
+         **/
+        public FuncDecl[][] Accessors() 
+            {
+                
+
+                Integer n = NumConstructors;
+                FuncDecl[][] res = new FuncDecl[n][];
+                for (Integer i = 0; i < n; i++)
+                {
+                    FuncDecl fd = new FuncDecl(Context, Native.getDatatypeSortConstructor(Context.nCtx, NativeObject, i));
+                    Integer ds = fd.DomainSize;
+                    FuncDecl[] tmp = new FuncDecl[ds];
+                    for (Integer j = 0; j < ds; j++)
+                        tmp[j] = new FuncDecl(Context, Native.getDatatypeSortConstructorAccessor(Context.nCtx, NativeObject, i, j));
+                    res[i] = tmp;
+                return res;
+            }
+        }
+
+        DatatypeSort(Context ctx, IntPtr obj) { super(ctx, obj);  }
+
+        DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
+            { super(ctx, Native.mkDatatype(ctx.nCtx, name.NativeObject, (Integer)constructors.Length, ArrayToNative(constructors)));
+            
+            
+            
+        }
+    };
+
+    /**
+     * Uninterpreted Sorts
+     **/
+    public class UninterpretedSort extends Sort
+    {
+        UninterpretedSort(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+        UninterpretedSort(Context ctx, Symbol s)
+            { super(ctx, Native.mkUninterpretedSort(ctx.nCtx, s.NativeObject));
+            
+            
+        }
+    }
+
+    /**
+     * Tuple sorts.
+     **/
+    public class TupleSort extends Sort
+    {
+        /**
+         * The constructor function of the tuple.
+         **/
+        public FuncDecl MkDecl()  {
+                
+
+                return new FuncDecl(Context, Native.getTupleSortMkDecl(Context.nCtx, NativeObject)); }
+
+        /**
+         * The number of fields in the tuple.
+         **/
+        public Integer NumFields()  { return Native.getTupleSortNumFields(Context.nCtx, NativeObject); }
+
+        /**
+         * The field declarations.
+         **/
+        public FuncDecl[] FieldDecls() 
+            {
+                
+
+                Integer n = NumFields;
+                FuncDecl[] res = new FuncDecl[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = new FuncDecl(Context, Native.getTupleSortFieldDecl(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        TupleSort(Context ctx, Symbol name, Integer numFields, Symbol[] fieldNames, Sort[] fieldSorts)
+            { super(ctx);
+            
+            
+
+            IntPtr t = IntPtr.Zero;
+            NativeObject = Native.mkTupleSort(ctx.nCtx, name.NativeObject, numFields,
+                                                   Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
+                                                   t, new IntPtr[numFields]);
+        }
+    };
+
+    /**
+     * Enumeration sorts.
+     **/
+    public class EnumSort extends Sort
+    {
+        /**
+         * The function declarations of the constants in the enumeration.
+         **/
+        public FuncDecl[] ConstDecls()  {
+                
+
+                return Constdecls; }
+
+        /**
+         * The constants in the enumeration.
+         **/
+        public Expr[] Consts()  {
+                
+
+                return Consts; }
+
+        /**
+         * The test predicates for the constants in the enumeration.
+         **/
+        public FuncDecl[] TesterDecls()  {
+                
+                
+                return Testerdecls;
+        }
+
+
+        private void ObjectInvariant()
+        {
+            
+            
+            
+        }
+
+        
+
+        private FuncDecl[] Constdecls = null, Testerdecls = null;
+        private Expr[] Consts = null;
+
+        EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
+            { super(ctx);
+            
+            
+            
+
+            int n = enumNames.Length;
+            IntPtr[] nConstdecls = new IntPtr[n];
+            IntPtr[] nTesters = new IntPtr[n];
+            NativeObject = Native.mkEnumerationSort(ctx.nCtx, name.NativeObject, (Integer)n,
+                                                         Symbol.ArrayToNative(enumNames), nConstdecls, nTesters);
+            Constdecls = new FuncDecl[n];            
+            for (Integer i = 0; i < n; i++)            
+                Constdecls[i] = new FuncDecl(ctx, nConstdecls[i]);
+            Testerdecls = new FuncDecl[n];
+            for (Integer i = 0; i < n; i++)
+                Testerdecls[i] = new FuncDecl(ctx, nTesters[i]);
+            Consts = new Expr[n];
+            for (Integer i = 0; i < n; i++)
+                Consts[i] = ctx.MkApp(Constdecls[i]);
+        }
+    };
+
+    /**
+     * List sorts.
+     **/
+    public class ListSort extends Sort
+    {
+        /**
+         * The declaration of the nil function of this list sort.
+         **/
+        public FuncDecl NilDecl() 
+            
+            return nilDecl; } }
+
+        /**
+         * The empty list.
+         **/
+        public Expr Nil() 
+            {
+                
+                return nilConst;
+        }
+
+        /**
+         * The declaration of the isNil function of this list sort.
+         **/
+        public FuncDecl IsNilDecl() 
+            {
+                
+                return isNilDecl;
+        }
+
+        /**
+         * The declaration of the cons function of this list sort.
+         **/
+        public FuncDecl ConsDecl() 
+            {
+                
+                return consDecl;
+        }
+
+        /**
+         * The declaration of the isCons function of this list sort.
+         * 
+         **/
+        public FuncDecl IsConsDecl() 
+            {
+                
+                return isConsDecl;
+        }
+
+        /**
+         * The declaration of the head function of this list sort.
+         **/
+        public FuncDecl HeadDecl() 
+            {
+                
+                return headDecl;
+        }
+
+        /**
+         * The declaration of the tail function of this list sort.
+         **/
+        public FuncDecl TailDecl() 
+            {
+                
+                return tailDecl;
+        }
+
+
+        private void ObjectInvariant()
+        {
+            
+            
+            
+            
+            
+            
+            
+        }
+
+        
+
+        private FuncDecl nilDecl, isNilDecl, consDecl, isConsDecl, headDecl, tailDecl;
+        private Expr nilConst;
+
+        ListSort(Context ctx, Symbol name, Sort elemSort)
+            { super(ctx);
+            
+            
+            
+
+            IntPtr inil = IntPtr.Zero,
+                   iisnil = IntPtr.Zero,
+                   icons = IntPtr.Zero,
+                   iiscons = IntPtr.Zero,
+                   ihead = IntPtr.Zero,
+                   itail = IntPtr.Zero;
+
+            NativeObject = Native.mkListSort(ctx.nCtx, name.NativeObject, elemSort.NativeObject,
+                                                  inil, iisnil, icons, iiscons, ihead, itail);
+            nilDecl = new FuncDecl(ctx, inil);
+            isNilDecl = new FuncDecl(ctx, iisnil);
+            consDecl = new FuncDecl(ctx, icons);
+            isConsDecl = new FuncDecl(ctx, iiscons);
+            headDecl = new FuncDecl(ctx, ihead);
+            tailDecl = new FuncDecl(ctx, itail);
+            nilConst = ctx.MkConst(nilDecl);
+        }
+    };
+
+    /**
+     * Relation sorts.
+     **/
+    public class RelationSort extends Sort
+    {
+        /**
+         * The arity of the relation sort.
+         **/
+        public Integer Arity()  { return Native.getRelationArity(Context.nCtx, NativeObject); }
+
+        /**
+         * The sorts of the columns of the relation sort.
+         **/
+        public Sort[] ColumnSorts() 
+            {
+                
+
+                if (mColumnSorts != null)
+                    return mColumnSorts;
+
+                Integer n = Arity;
+                Sort[] res = new Sort[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = Sort.Create(Context, Native.getRelationColumn(Context.nCtx, NativeObject, i));
+                return res;
+        }
+
+        private Sort[] mColumnSorts = null;
+
+        RelationSort(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }        
+    }
+
+    /**
+     * Finite domain sorts.
+     **/
+    public class FiniteDomainSort extends Sort
+    {
+        /**
+         * The size of the finite domain sort.
+         **/
+        public ulong Size()  { ulong res = 0; Native.getFiniteDomainSortSize(Context.nCtx, NativeObject, ref res); return res; }
+
+        FiniteDomainSort(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+        FiniteDomainSort(Context ctx, Symbol name, ulong size)
+            { super(ctx, Native.mkFiniteDomainSort(ctx.nCtx, name.NativeObject, size));
+            
+            
+
+        }
+    }
+
+    /**
+     * Set sorts.
+     **/
+    public class SetSort extends Sort
+    {
+        SetSort(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+        SetSort(Context ctx, Sort ty)
+            { super(ctx, Native.mkSetSort(ctx.nCtx, ty.NativeObject));
+            
+            
+        }
+    }

src/api/java/com/Microsoft/Z3/Statistics.java

@@ -0,0 +1,167 @@
+/**
+ * This file was automatically generated from Statistics.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * Objects of this class track statistical information about solvers. 
+     **/
+    public class Statistics extends Z3Object
+    {
+        /**
+         * Statistical data is organized into pairs of [Key, Entry], where every
+         * Entry is either a <code>DoubleEntry</code> or a <code>UIntEntry</code>
+         **/
+        public class Entry
+        {
+            /**
+             * The key of the entry.
+             **/
+            /**
+             * The uint-value of the entry.
+             **/
+            public Integer UIntValue() { return mInteger; } 
+            /**
+             * The double-value of the entry.
+             **/
+            public double DoubleValue() { return mDouble; } 
+            /**
+             * True if the entry is uint-valued.
+             **/
+            public boolean IsUInt() { return mIsInteger; } 
+            /**
+             * True if the entry is double-valued.
+             **/
+            public boolean IsDouble() { return mIsDouble; } 
+
+            /**
+             * The string representation of the the entry's value.
+             **/
+            public String Value() 
+                {
+                    
+
+                    if (IsUInt)
+                        return mInteger.toString();
+                    else if (IsDouble)
+                        return mDouble.toString();
+                    else
+                        throw new Z3Exception("Unknown statistical entry type");
+            }
+
+            /**
+             * The string representation of the Entry.
+             **/
+            public String toString()
+            {
+                return Key + ": " + Value;
+            }
+
+            private boolean mIsInteger = false;
+            private boolean mIsDouble = false;
+            private Integer mInteger = 0;
+            private double mDouble = 0.0;
+            Entry(String k, Integer v) { Key = k; mIsInteger = true; mInteger = v; }
+            Entry(String k, double v) { Key = k; mIsDouble = true; mDouble = v; }
+        }
+
+        /**
+         * A string representation of the statistical data.
+         **/
+        public String toString()
+        {
+            return Native.statstoString(Context.nCtx, NativeObject);
+        }
+
+        /**
+         * The number of statistical data.
+         **/
+        public Integer Size()  { return Native.statsSize(Context.nCtx, NativeObject); }
+
+        /**
+         * The data entries.
+         **/
+        public Entry[] Entries() 
+            {
+                
+                
+                
+
+                Integer n = Size;
+                Entry[] res = new Entry[n];
+                for (Integer i = 0; i < n; i++)
+                {
+                    Entry e;
+                    String k = Native.statsGetKey(Context.nCtx, NativeObject, i);
+                    if (Native.statsIsInteger(Context.nCtx, NativeObject, i) != 0)
+                        e = new Entry(k, Native.statsGetIntegerValue(Context.nCtx, NativeObject, i));
+                    else if (Native.statsIsDouble(Context.nCtx, NativeObject, i) != 0)
+                        e = new Entry(k, Native.statsGetDoubleValue(Context.nCtx, NativeObject, i));
+                    else
+                        throw new Z3Exception("Unknown data entry value");
+                    res[i] = e;
+                return res;
+            }
+        }
+
+        /**
+         * The statistical counters.
+         **/
+        public String[] Keys() 
+            {
+                
+
+                Integer n = Size;
+                String[] res = new String[n];
+                for (Integer i = 0; i < n; i++)
+                    res[i] = Native.statsGetKey(Context.nCtx, NativeObject, i);
+                return res;
+        }
+
+        /**
+         * The value of a particular statistical counter.
+         * <remarks>Returns null if the key is unknown.</remarks>
+         **/
+        public Entry this[String key]() 
+            {
+                Integer n = Size;
+                Entry[] es = Entries;
+                for (Integer i = 0; i < n; i++)
+                    if (es[i].Key == key)
+                        return es[i];
+                return null;
+        }
+
+        Statistics(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+
+        class DecRefQueue extends Z3.DecRefQueue
+        {
+            public void IncRef(Context ctx, IntPtr obj)
+            {
+                Native.statsIncRef(ctx.nCtx, obj);
+            }
+
+            public void DecRef(Context ctx, IntPtr obj)
+            {
+                Native.statsDecRef(ctx.nCtx, obj);
+            }
+        };
+
+        void IncRef(IntPtr o)
+        {
+            Context.StatisticsDRQ.IncAndClear(Context, o);
+            super.IncRef(o);
+        }
+
+        void DecRef(IntPtr o)
+        {
+            Context.StatisticsDRQ.Add(o);
+            super.DecRef(o);
+        }
+    }

src/api/java/com/Microsoft/Z3/Status.java

@@ -0,0 +1,26 @@
+/**
+ * This file was automatically generated from Status.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+  /**
+   * Status values.
+   **/
+    /**
+     * Used to signify an unsatisfiable status.
+     **/
+    UNSATISFIABLE = -1,
+
+    /**
+     * Used to signify an unknown status.
+     **/
+    UNKNOWN = 0,
+
+    /**
+     * Used to signify a satisfiable status.
+     **/
+    SATISFIABLE = 1
+

src/api/java/com/Microsoft/Z3/Symbol.java

@@ -0,0 +1,140 @@
+/**
+ * This file was automatically generated from Symbol.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+/* using System.Runtime.InteropServices; */
+
+    /**
+     * Symbols are used to name several term and type constructors.
+     **/
+    public class Symbol extends Z3Object
+    {
+        /**
+         * The kind of the symbol (int or string)
+         **/
+        protected Z3SymbolKind Kind
+        {
+            get { return (Z3SymbolKind)Native.getSymbolKind(Context.nCtx, NativeObject); }
+        }
+
+        /**
+         * Indicates whether the symbol is of Int kind
+         **/
+        public boolean IsIntSymbol()
+        {
+            return Kind == Z3SymbolKind.Z3INTSYMBOL;
+        }
+
+        /**
+         * Indicates whether the symbol is of string kind.
+         **/
+        public boolean IsStringSymbol()
+        {
+            return Kind == Z3SymbolKind.Z3STRINGSYMBOL;
+        }
+
+        /**
+         * A string representation of the symbol.
+         **/
+        public String toString()
+        {
+            if (IsIntSymbol())
+                return ((IntSymbol)this).Int.toString();
+            else if (IsStringSymbol())
+                return ((StringSymbol)this).String;
+            else
+                throw new Z3Exception("Unknown symbol kind encountered");
+        }
+
+        /**
+         * Symbol constructor
+         **/
+        protected Symbol(Context ctx, IntPtr obj) { super(ctx, obj); 
+            
+        }
+
+        static Symbol Create(Context ctx, IntPtr obj)
+        {
+            
+            
+
+            switch ((Z3SymbolKind)Native.getSymbolKind(ctx.nCtx, obj))
+            {
+                case Z3SymbolKind.Z3INTSYMBOL: return new IntSymbol(ctx, obj);
+                case Z3SymbolKind.Z3STRINGSYMBOL: return new StringSymbol(ctx, obj);
+                default:
+                    throw new Z3Exception("Unknown symbol kind encountered");
+            }
+        }
+    }
+
+    /**
+     * Numbered symbols
+     **/
+    public class IntSymbol extends Symbol
+    {
+        /**
+         * The int value of the symbol.
+         * <remarks>Throws an exception if the symbol is not of int kind. </remarks>
+         **/
+        public int Int() 
+            {
+                if (!IsIntSymbol())
+                    throw new Z3Exception("Int requested from non-Int symbol");
+                return Native.getSymbolInt(Context.nCtx, NativeObject);
+        }
+
+        IntSymbol(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+        IntSymbol(Context ctx, int i)
+            { super(ctx, Native.mkIntSymbol(ctx.nCtx, i));
+            
+        }
+
+        void CheckNativeObject(IntPtr obj)
+        {
+            if ((Z3SymbolKind)Native.getSymbolKind(Context.nCtx, obj) != Z3SymbolKind.Z3INTSYMBOL)
+                throw new Z3Exception("Symbol is not of integer kind");
+            super.CheckNativeObject(obj);
+        }
+    }
+
+    /**
+     * Named symbols
+     **/
+    public class StringSymbol extends Symbol
+    {
+        /**
+         * The string value of the symbol.
+         * <remarks>Throws an exception if the symbol is not of string kind.</remarks>
+         **/
+        public String String() 
+            {
+                
+
+                if (!IsStringSymbol())
+                    throw new Z3Exception("String requested from non-String symbol");
+                return Native.getSymbolString(Context.nCtx, NativeObject);                
+        }
+
+        StringSymbol(Context ctx, IntPtr obj) { super(ctx, obj); 
+            
+        }
+
+        StringSymbol(Context ctx, String s) { super(ctx, Native.mkStringSymbol(ctx.nCtx, s)); 
+            
+        }
+
+        void CheckNativeObject(IntPtr obj)
+        {
+            if ((Z3SymbolKind)Native.getSymbolKind(Context.nCtx, obj) != Z3SymbolKind.Z3STRINGSYMBOL)
+                throw new Z3Exception("Symbol is not of String kind");
+
+            super.CheckNativeObject(obj);
+        }
+    }

src/api/java/com/Microsoft/Z3/Tactic.java

@@ -0,0 +1,107 @@
+/**
+ * This file was automatically generated from Tactic.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * Tactics are the basic building block for creating custom solvers for specific problem domains.
+     * The complete list of tactics may be obtained using <code>Context.NumTactics</code> 
+     * and <code>Context.TacticNames</code>.
+     * It may also be obtained using the command <code>(help-tactics)</code> in the SMT 2.0 front-end.
+     **/
+    public class Tactic extends Z3Object
+    {
+        /**
+         * A string containing a description of parameters accepted by the tactic.
+         **/
+        public String Help() 
+            {
+                
+
+                return Native.tacticGetHelp(Context.nCtx, NativeObject);
+        }
+
+
+        /**
+         * Retrieves parameter descriptions for Tactics.
+         **/
+        public ParamDescrs ParameterDescriptions()  { return new ParamDescrs(Context, Native.tacticGetParamDescrs(Context.nCtx, NativeObject)); }
+
+
+        /**
+         * Execute the tactic over the goal. 
+         **/
+        public ApplyResult Apply(Goal g, Params p)
+        {
+            
+            
+
+            Context.CheckContextMatch(g);
+            if (p == null)
+                return new ApplyResult(Context, Native.tacticApply(Context.nCtx, NativeObject, g.NativeObject));
+            else
+            {
+                Context.CheckContextMatch(p);
+                return new ApplyResult(Context, Native.tacticApplyEx(Context.nCtx, NativeObject, g.NativeObject, p.NativeObject));
+            }
+        }
+
+        /**
+         * Apply the tactic to a goal.
+         **/
+        public ApplyResult this[Goal g]() 
+            {
+                
+                
+
+                return Apply(g);
+        }
+
+        /**
+         * Creates a solver that is implemented using the given tactic.
+         * <seealso cref="Context.MkSolver(Tactic)"/>
+         **/
+        public Solver Solver() 
+            {
+                
+
+                return Context.MkSolver(this);
+        }
+
+        Tactic(Context ctx, IntPtr obj)
+            { super(ctx, obj);
+            
+        }
+        Tactic(Context ctx, String name)
+            { super(ctx, Native.mkTactic(ctx.nCtx, name));
+            
+        }
+
+        class DecRefQueue extends Z3.DecRefQueue
+        {
+            public void IncRef(Context ctx, IntPtr obj)
+            {
+                Native.tacticIncRef(ctx.nCtx, obj);
+            }
+
+            public void DecRef(Context ctx, IntPtr obj)
+            {
+                Native.tacticDecRef(ctx.nCtx, obj);
+            }
+        };
+
+        void IncRef(IntPtr o)
+        {
+            Context.TacticDRQ.IncAndClear(Context, o);
+            super.IncRef(o);
+        }
+
+        void DecRef(IntPtr o)
+        {
+            Context.TacticDRQ.Add(o);
+            super.DecRef(o);
+        }
+    }

src/api/java/com/Microsoft/Z3/Version.java

@@ -0,0 +1,68 @@
+/**
+ * This file was automatically generated from Version.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * Version information.
+     * <remarks>Note that this class is static.</remarks>
+     **/
+    public final class Version
+    {
+         Version() { }
+
+        /**
+         * The major version
+         **/
+        public  Integer Major() 
+            {
+                Integer major = 0, minor = 0, build = 0, revision = 0;
+                Native.getVersion(major, minor, build, revision);
+                return major;
+        }
+
+        /**
+         * The minor version
+         **/
+        public  Integer Minor() 
+            {
+                Integer major = 0, minor = 0, build = 0, revision = 0;
+                Native.getVersion(major, minor, build, revision);
+                return minor;
+        }
+
+        /**
+         * The build version
+         **/
+        public  Integer Build() 
+            {
+                Integer major = 0, minor = 0, build = 0, revision = 0;
+                Native.getVersion(major, minor, build, revision);
+                return build;
+        }
+
+        /**
+         * The revision
+         **/
+        public  Integer Revision() 
+            {
+                Integer major = 0, minor = 0, build = 0, revision = 0;
+                Native.getVersion(major, minor, build, revision);
+                return revision;
+        }
+
+        /**
+         * A string representation of the version information.
+         **/
+        public  String toString()
+        {
+            
+
+            Integer major = 0, minor = 0, build = 0, revision = 0;
+            Native.getVersion(major, minor, build, revision);
+            return major.toString() + "." + minor.toString() + "." + build.toString() + "." + revision.toString();
+        }
+    }

src/api/java/com/Microsoft/Z3/Z3Exception.java

@@ -0,0 +1,28 @@
+/**
+ * This file was automatically generated from Z3Exception.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+  /**
+   * The exception base class for error reporting from Z3
+   **/
+  public class Z3Exception extends Exception
+  {
+    /**
+     * Constructor.
+     **/
+    public Z3Exception() { super(); }
+
+    /**
+     * Constructor.
+     **/
+    public Z3Exception(String message) { super(message); }
+
+    /**
+     * Constructor.
+     **/
+    public Z3Exception(String message, System.Exception inner) { super(message, inner); }
+  }

src/api/java/com/Microsoft/Z3/Z3Object.java

@@ -0,0 +1,120 @@
+/**
+ * This file was automatically generated from Z3Object.cs 
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+    /**
+     * Internal base class for interfacing with native Z3 objects.
+     * Should not be used externally.
+     **/
+    public class Z3Object extends IDisposable
+    {
+        /**
+         * Finalizer.
+         **/
+        protected void finalize()
+        {
+            Dispose();            
+        }
+
+        /**
+         * Disposes of the underlying native Z3 object.
+         **/
+        public void Dispose()
+        {
+            if (mNObj != IntPtr.Zero)
+            {
+                DecRef(mNObj);
+                mNObj = IntPtr.Zero;                
+            }
+
+            if (mCtx != null)
+            {
+                mCtx.refCount--;
+                if (mCtx.refCount == 0)
+                    GC.ReRegisterForFinalize(mCtx);
+                mCtx = null;
+            }
+
+            GC.SuppressFinalize(this);
+        }
+
+        
+        private void ObjectInvariant()
+        {
+            
+        }
+
+
+        private Context mCtx = null;
+        private IntPtr mNObj = IntPtr.Zero;
+
+        Z3Object(Context ctx)
+        {
+            
+
+            ctx.refCount++;
+            mCtx = ctx;
+        }
+
+        Z3Object(Context ctx, IntPtr obj)
+        {
+            
+
+            ctx.refCount++;
+            mCtx = ctx;
+            IncRef(obj);
+            mNObj = obj;
+        }
+
+        void IncRef(IntPtr o) { }
+        void DecRef(IntPtr o) { }
+
+        void CheckNativeObject(IntPtr obj) { }
+
+        IntPtr NativeObject
+        {
+            get { return mNObj; }
+            set
+            {
+                if (value != IntPtr.Zero) { CheckNativeObject(value); IncRef(value); }
+                if (mNObj != IntPtr.Zero) { DecRef(mNObj); }
+                mNObj = value;
+            }
+        }
+
+        static IntPtr GetNativeObject(Z3Object s)
+        {
+            if (s == null) return new IntPtr();
+            return s.NativeObject;
+        }
+
+        Context Context
+        {
+            get 
+            {
+                
+                return mCtx; 
+            }            
+        }
+
+        static IntPtr[] ArrayToNative(Z3Object[] a)
+        {
+            
+            
+
+            if (a == null) return null;
+            IntPtr[] an = new IntPtr[a.Length];
+            for (Integer i = 0; i < a.Length; i++)
+                if (a[i] != null) an[i] = a[i].NativeObject;
+            return an;
+        }
+
+        static Integer ArrayLength(Z3Object[] a)
+        {
+            return (a == null)?0:(Integer)a.Length;
+        }
+    }

src/api/java/mk_java.py

@@ -0,0 +1,233 @@
+############################################
+# Copyright (c) 2012 Microsoft Corporation
+# 
+# Auxiliary scripts for generating Java bindings
+# from the managed API.
+#
+# Author: Christoph M. Wintersteiger (cwinter)
+############################################
+
+CS="../dotnet/"
+EXT=".cs"
+EXCLUDE=["Enumerations.cs", "Native.cs", "AssemblyInfo.cs"]
+OUTDIR="com/Microsoft/Z3/"
+
+import os
+import fileinput
+import string
+import re
+
+def mk_java_bindings():
+    print "Generating Java bindings (from C# bindings in " + CS + ")."
+    for root, dirs, files in os.walk(CS):
+        for fn in files:
+            if not fn in EXCLUDE and fn.endswith(EXT):
+                translate(fn)
+
+def subst_getters(s, getters):
+    for g in getters:
+        s = s.replace(g, g + "()")
+
+def type_replace(s):
+    s = s.replace("bool", "boolean")
+    s = s.replace("uint", "Integer")
+    s = s.replace("string", "String")
+    return s
+
+def rename_native(s):
+    a = re.sub("Native.Z3_(?P<id>\w+)", "Native.\g<id>", s)
+    lc_callback = lambda pat: pat.group("id").upper()
+    return re.sub("_(?P<id>\w)", lc_callback, a)
+
+
+def translate(filename):
+    tgtfn = OUTDIR + filename.replace(EXT, ".java")
+    print "Translating " + filename + " to " + tgtfn
+    tgt = open(tgtfn, "w")
+    in_header = 0
+    in_class = 0
+    in_static_class = 0
+    in_javadoc = 0
+    lastindent = 0
+    skip_brace = 0
+    in_getter = ""
+    in_getter_type = ""
+    in_unsupported = 0
+    getters = []
+    for line in fileinput.input(os.path.join(CS, filename)):
+        s = string.rstrip(string.lstrip(line))
+        if in_javadoc:
+            if s.startswith("///"):
+                lastindent = line.find(s);
+                if s.startswith("/// </summary>"):
+                    pass
+                else: 
+                    a = line
+                    a = a.replace("<c>", "<code>")
+                    a = a.replace("</c>", "</code>")
+                    a = a.replace("///"," *")
+                    a = a.replace("<returns>","@return ")
+                    a = a.replace("</returns>","")
+                    tgt.write(a)
+            else:
+                t = ""
+                for i in range(0, lastindent):
+                    t += " "
+                tgt.write(t + " **/\n")
+                in_javadoc = 0
+
+        if in_unsupported:
+            if s == "}":
+                in_unsupported = 0                
+        elif not in_javadoc:
+            if not in_header and s.find("/*++") != -1:
+                in_header = 1
+                tgt.write("/**\n")
+            elif in_header and s.startswith("--*/"):
+                in_header = 0
+                tgt.write(" * This file was automatically generated from " + filename + " \n")
+                tgt.write(" **/\n")
+                tgt.write("\npackage com.Microsoft.Z3;\n")
+
+            elif in_header == 1:
+                # tgt.write(" * " + line.replace(filename, tgtfn))
+                pass
+            elif s.startswith("using"):
+                if s.find("System.Diagnostics.Contracts") == -1:
+                    tgt.write("/* " + s + " */\n")
+            elif s.startswith("namespace"):
+                pass
+            elif s.startswith("public") and s.find("operator") and (s.find("==") != -1 or s.find("!=") != -1):
+                t = ""
+                for i in range(0, line.find(s)+1):
+                    t += " "                    
+                tgt.write(t + "/* Overloaded operators are not translated. */\n")
+                in_unsupported = 1;
+            elif s.startswith("public class") or s.startswith("internal class"):
+                a = line.replace(":", "extends").replace("internal ", "")
+                a = a.replace(", IComparable", "")
+                tgt.write(a)
+                in_class = 1
+                in_static_class = 0
+            elif s.startswith("public static class"):
+                tgt.write(line.replace(":", "extends").replace("static", "final"))
+                in_class = 1
+                in_static_class = 1
+            elif s.startswith("/// <summary>"):
+                tgt.write(line.replace("/// <summary>", "/**"))
+                in_javadoc = 1
+            elif skip_brace and s == "{":
+                skip_brace = 0
+            elif s.find("public") != -1 and s.find("class") == -1 and s.find("event") == -1 and s.find("(") == -1:
+                tokens = s.split(" ")
+                print "# TOKENS: " + str(len(tokens))
+                if len(tokens) == 3:
+                    in_getter = tokens[2]
+                    in_getter_type = type_replace((tokens[0] + " " + tokens[1]))
+                    if in_static_class:
+                        in_getter_type = in_getter_type.replace("static", "")                        
+                    lastindent = line.find(s)
+                    skip_brace = 1
+                elif len(tokens) == 4:
+                    in_getter = tokens[3]
+                    in_getter_type = type_replace(tokens[0] + " " + tokens[1] + " " + tokens[2])
+                    if in_static_class:
+                        in_getter_type = in_getter_type.replace("static", "")
+                    lastindent = line.find(s)
+                    skip_brace = 1                
+                else:
+                    in_getter = tokens[2]
+                    in_getter_type = type_replace(tokens[0] + " " + tokens[1])
+                    if in_static_class:
+                        in_getter_type = in_getter_type.replace("static", "")                        
+                    rest = s[s.find("get ") + 4:-1]
+                    subst_getters(rest, getters)
+                    rest = type_replace(rest)
+                    rest = rename_native(rest)
+                    t = ""
+                    for i in range(0, lastindent):
+                        t += " "
+                    tgt.write(t + in_getter_type + " " + in_getter + "() " + rest + "\n")
+                getters.append(in_getter)
+                print "ACC: " + s + " --> " + in_getter
+            elif s.find("{ get {") != -1:
+                line = type_replace(line)
+                line = line.replace("internal ", "")
+                d = line[0:line.find("{ get")]
+                rest = line[line.find("{ get")+5:]
+                rest = rest.replace("} }", "}")
+                subst_getters(rest, getters)
+                rest = rename_native(rest)
+                tgt.write(d + "()" + rest)
+                print "ACC: " + s + " --> " + in_getter
+            elif in_getter != "" and s.startswith("get"):
+                t = ""
+                for i in range(0, lastindent):
+                    t += " "
+                if len(s) > 3: rest = s[3:]
+                else: rest = ""
+                subst_getters(rest, getters)
+                rest = type_replace(rest)
+                rest = rename_native(rest)
+                tgt.write(t + in_getter_type + " " + in_getter + "() " + rest + "\n")
+            elif in_getter != "" and s.startswith("set"):
+                t = ""
+                for i in range(0, lastindent):
+                    t += " "
+                if len(s) > 3: rest = type_replace(s[3:])
+                else: rest = ""
+                subst_getters(rest, getters)
+                rest = rest.replace("(Integer)value", "Integer(value)")
+                rest = type_replace(rest)
+                rest = rename_native(rest)
+                ac_acc = in_getter_type[:in_getter_type.find(' ')]
+                ac_type = in_getter_type[in_getter_type.find(' ')+1:]
+                tgt.write(t + ac_acc + " void set" + in_getter + "(" + ac_type + " value) " + rest + "\n")
+            elif in_getter != "" and s == "}":
+                in_getter = ""
+                in_getter_type == ""
+                skip_brace = 0
+            elif s.startswith("uint ") and s.find("=") == -1:
+                line = line.replace("uint", "Integer", line)
+                line = re.sub("(?P<n>\w+)(?P<c>[,;])", "\g<n>\g<c>", line)
+                tgt.write(line);
+            elif (not in_class and (s.startswith("{") or s.startswith("}"))) or s.startswith("[") or s.startswith("#"):
+                # print "Skipping: " + s;
+                pass
+            elif line == "}\n":
+                pass
+            else:
+                # indent = line.find(s)
+                if line.find(": base") != -1:
+                    line = re.sub(": base\((?P<p>[\w,.\(\) ]*)\)", "{ super(\g<p>);", line)
+                    if line.find("; {") != -1:
+                        line = line.replace("; {", ";")
+                    else:
+                        skip_brace = 1                        
+                if s.startswith("public"):
+                    line = re.sub(" = [\w.]+(?P<d>[,;\)])", "\g<d>", line)
+                    line = re.sub("(?P<d>[\(, ])params ", "\g<d>", line)
+                line = line.replace("base.", "super.")
+                a = type_replace(line)
+                a = re.sub("Contract.\w+\([\s\S]*\);", "", a)
+                a = rename_native(a)
+                a = re.sub("~\w+\(\)", "protected void finalize()", a)
+                a = re.sub("foreach\s*\((?P<t>[\w <>,]+)\s+(?P<i>\w+)\s+in\s+(?P<w>\w+)\)",
+                           "for (\g<t>.Iterator \g<i> = \g<w>.iterator(); \g<i>.hasNext(); )", a)
+                a = a.replace("readonly private", "private")
+                a = a.replace("new public", "public")
+                a = a.replace("ToString", "toString")
+                a = a.replace("internal ", "")
+                a = a.replace("override ", "")
+                a = a.replace("virtual ", "")
+                a = a.replace("o as AST", "(AST) o")
+                a = a.replace("other as AST", "(AST) other")
+                if in_static_class:
+                    a = a.replace("static", "")
+                a = re.sub("ref (?P<id>\w+)", "\g<id>", a)
+                subst_getters(a, getters)
+                tgt.write(a)
+                
+    tgt.close()
+
+mk_java_bindings()

src/ast/rewriter/bit_blaster/eager_bit_blaster.cpp

@@ -1,436 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    eager_bit_blaster.cpp
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-10-02.
-
-Revision History:
-
---*/
-
-#include"ast_ll_pp.h"
-#include"eager_bit_blaster.h"
-
-eager_bit_blaster::basic_plugin::basic_plugin(ast_manager & m, eager_bit_blaster::bv_plugin & p, basic_simplifier_plugin & s):
-    simplifier_plugin(symbol("basic"), m),
-    m_main(p),
-    m_s(s) {
-}
-
-eager_bit_blaster::basic_plugin::~basic_plugin() {
-}
-
-bool eager_bit_blaster::basic_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
-    if (f->get_decl_kind() == OP_ITE) {
-        SASSERT(num_args == 3);
-        return m_main.reduce_ite(args[0], args[1], args[2], result);
-    }
-    else if (f->get_decl_kind() == OP_NOT) {
-        // the internalizer assumes there is not double negation (not (not x))
-        SASSERT(num_args == 1);
-        m_s.mk_not(args[0], result);
-        return true;
-    }
-    return false;
-}
-
-eager_bit_blaster::bv_plugin::bv_plugin(ast_manager & m, bit_blaster_params const & p):
-    simplifier_plugin(symbol("bv"), m),
-    m_util(m), 
-    m_bb(m, p),
-    m_s(m) {
-}
-    
-eager_bit_blaster::bv_plugin::~bv_plugin() {
-}
-
-void eager_bit_blaster::bv_plugin::get_bits(expr * n, expr_ref_vector & out_bits) {
-    rational val;
-    unsigned bv_size;
-    if (m_util.is_numeral(n, val, bv_size)) {
-        TRACE("eager_bb_bug", tout << "bv_size: " << bv_size << "\n";);
-        m_bb.num2bits(val, bv_size, out_bits);
-        SASSERT(out_bits.size() == bv_size);
-    }
-    else if (m_util.is_mkbv(n)) {
-        out_bits.append(to_app(n)->get_num_args(), to_app(n)->get_args());
-    }
-    else {
-        unsigned bv_size = m_util.get_bv_size(n);
-        for (unsigned i = 0; i < bv_size; i++) {
-            parameter p(i);
-            out_bits.push_back(m_manager.mk_app(get_family_id(), OP_BIT2BOOL, 1, &p, 1, &n));
-        }
-        SASSERT(bv_size == out_bits.size());
-    }
-}
-
-inline app * eager_bit_blaster::bv_plugin::mk_mkbv(expr_ref_vector const & bits) {
-#ifdef Z3DEBUG
-    for (unsigned i = 0; i < bits.size(); i++) {
-        expr * b = bits.get(i);
-        SASSERT(!m_manager.is_not(b) || !m_manager.is_not(to_app(b)->get_arg(0)));
-    }
-#endif
-    return m_manager.mk_app(get_family_id(), OP_MKBV, bits.size(), bits.c_ptr());
-}
-
-#define MK_UNARY_REDUCE(OP, BB_OP)                                      \
-void eager_bit_blaster::bv_plugin::OP(expr * arg, expr_ref & result) {  \
-    expr_ref_vector bits(m_manager);                                    \
-    get_bits(arg, bits);                                                \
-    expr_ref_vector out_bits(m_manager);                                \
-    m_bb.BB_OP(bits.size(), bits.c_ptr(), out_bits);                    \
-    result = mk_mkbv(out_bits);                                         \
-}
-
-#define MK_BIN_REDUCE(OP, BB_OP)                                                        \
-void eager_bit_blaster::bv_plugin::OP(expr * arg1, expr * arg2, expr_ref & result) {    \
-    expr_ref_vector bits1(m_manager);                                                   \
-    expr_ref_vector bits2(m_manager);                                                   \
-    get_bits(arg1, bits1);                                                              \
-    get_bits(arg2, bits2);                                                              \
-    expr_ref_vector out_bits(m_manager);                                                \
-    m_bb.BB_OP(bits1.size(), bits1.c_ptr(), bits2.c_ptr(), out_bits);                   \
-    result = mk_mkbv(out_bits);                                                         \
-}
-
-#define MK_BIN_AC_FLAT_REDUCE(OP, BIN_OP, S_OP, BB_OP)                                                  \
-MK_BIN_REDUCE(BIN_OP, BB_OP);                                                                           \
-void eager_bit_blaster::bv_plugin::OP(unsigned num_args, expr * const * args, expr_ref & result) {      \
-    SASSERT(num_args > 0);                                                                              \
-    if (num_args == 2) {                                                                                \
-        BIN_OP(args[0], args[1], result);                                                               \
-        return;                                                                                         \
-    }                                                                                                   \
-                                                                                                        \
-    ptr_buffer<expr_ref_vector> args_bits;                                                              \
-    for (unsigned i = 0; i < num_args; i++) {                                                           \
-        expr_ref_vector * bits = alloc(expr_ref_vector, m_manager);                                     \
-        get_bits(args[i], *bits);                                                                       \
-        args_bits.push_back(bits);                                                                      \
-    }                                                                                                   \
-                                                                                                        \
-    unsigned bv_size = m_util.get_bv_size(args[0]);                                                     \
-    expr_ref_vector new_bits(m_manager);                                                                \
-    for (unsigned i = 0; i < bv_size; i++) {                                                            \
-        expr_ref_vector arg_bits(m_manager);                                                            \
-        for (unsigned j = 0; j < num_args; j++)                                                         \
-            arg_bits.push_back(args_bits[j]->get(i));                                                   \
-        expr_ref new_bit(m_manager);                                                                    \
-        m_s.S_OP(arg_bits.size(), arg_bits.c_ptr(), new_bit);                                           \
-        new_bits.push_back(new_bit);                                                                    \
-    }                                                                                                   \
-    result = mk_mkbv(new_bits);                                                                         \
-    std::for_each(args_bits.begin(), args_bits.end(), delete_proc<expr_ref_vector>());                  \
-}
-
-#define MK_BIN_AC_REDUCE(OP, BIN_OP, BB_OP)                                                             \
-MK_BIN_REDUCE(BIN_OP, BB_OP);                                                                           \
-void eager_bit_blaster::bv_plugin::OP(unsigned num_args, expr * const * args, expr_ref & result) {      \
-    SASSERT(num_args > 0);                                                                              \
-    result = args[0];                                                                                   \
-    for (unsigned i = 1; i < num_args; i++) {                                                           \
-        expr_ref new_result(m_manager);                                                                 \
-        BIN_OP(result.get(), args[i], new_result);                                                      \
-        result = new_result;                                                                            \
-    }                                                                                                   \
-}
-
-#define MK_BIN_PRED_REDUCE(OP, BB_OP)                                                   \
-void eager_bit_blaster::bv_plugin::OP(expr * arg1, expr * arg2, expr_ref & result) {    \
-    expr_ref_vector bits1(m_manager);                                                   \
-    expr_ref_vector bits2(m_manager);                                                   \
-    get_bits(arg1, bits1);                                                              \
-    get_bits(arg2, bits2);                                                              \
-    m_bb.BB_OP(bits1.size(), bits1.c_ptr(), bits2.c_ptr(), result);                     \
-}
-
-#define MK_PARAMETRIC_UNARY_REDUCE(OP, BB_OP)                                           \
-void eager_bit_blaster::bv_plugin::OP(expr * arg, unsigned n, expr_ref & result) {      \
-    expr_ref_vector bits(m_manager);                                                    \
-    get_bits(arg, bits);                                                                \
-    expr_ref_vector out_bits(m_manager);                                                \
-    m_bb.BB_OP(bits.size(), bits.c_ptr(), n, out_bits);                                 \
-    result = mk_mkbv(out_bits);                                                         \
-}
-
-MK_UNARY_REDUCE(reduce_not, mk_not);
-MK_BIN_AC_FLAT_REDUCE(reduce_or, reduce_bin_or, mk_or, mk_or);
-MK_BIN_AC_FLAT_REDUCE(reduce_and, reduce_bin_and, mk_and, mk_and);
-MK_BIN_AC_FLAT_REDUCE(reduce_nor, reduce_bin_nor, mk_nor, mk_nor);
-MK_BIN_AC_FLAT_REDUCE(reduce_nand, reduce_bin_nand, mk_nand, mk_nand);
-MK_BIN_REDUCE(reduce_xor,  mk_xor);
-MK_BIN_REDUCE(reduce_xnor, mk_xnor);
-MK_UNARY_REDUCE(reduce_neg, mk_neg);
-MK_BIN_AC_REDUCE(reduce_add, reduce_bin_add, mk_adder);
-MK_BIN_AC_REDUCE(reduce_mul, reduce_bin_mul, mk_multiplier);
-MK_BIN_PRED_REDUCE(reduce_sle, mk_sle);
-MK_BIN_PRED_REDUCE(reduce_ule, mk_ule);
-MK_PARAMETRIC_UNARY_REDUCE(reduce_rotate_left, mk_rotate_left);
-MK_PARAMETRIC_UNARY_REDUCE(reduce_rotate_right, mk_rotate_right);
-MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
-MK_PARAMETRIC_UNARY_REDUCE(reduce_zero_extend, mk_zero_extend);
-MK_UNARY_REDUCE(reduce_redor, mk_redor);
-MK_UNARY_REDUCE(reduce_redand, mk_redand);
-MK_BIN_REDUCE(reduce_shl, mk_shl);
-MK_BIN_REDUCE(reduce_ashr, mk_ashr);
-MK_BIN_REDUCE(reduce_lshr, mk_lshr);
-MK_BIN_REDUCE(reduce_comp, mk_comp);
-MK_BIN_REDUCE(reduce_udiv, mk_udiv);
-MK_BIN_REDUCE(reduce_urem, mk_urem);
-MK_BIN_REDUCE(reduce_sdiv, mk_sdiv);
-MK_BIN_REDUCE(reduce_srem, mk_srem);
-MK_BIN_REDUCE(reduce_smod, mk_smod);
-
-void eager_bit_blaster::bv_plugin::reduce_extract(unsigned start, unsigned end, expr * arg, expr_ref & result) {
-    expr_ref_vector bits(m_manager);
-    get_bits(arg, bits);
-    expr_ref_vector out_bits(m_manager);
-    for (unsigned i = start; i <= end; ++i)
-        out_bits.push_back(bits.get(i));
-    result = mk_mkbv(out_bits);
-}
-
-void eager_bit_blaster::bv_plugin::reduce_concat(unsigned num_args, expr * const * args, expr_ref & result) {
-    expr_ref_vector out_bits(m_manager);
-    unsigned i = num_args;
-    while (i > 0) {
-        i--;
-        expr_ref_vector bits(m_manager);
-        get_bits(args[i], bits);
-        out_bits.append(bits.size(), bits.c_ptr());
-    }
-    result = mk_mkbv(out_bits);
-}
-
-bool eager_bit_blaster::bv_plugin::reduce_ite(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
-    sort * s = m_manager.get_sort(arg2);
-    if (!m_util.is_bv_sort(s))
-        return false;
-    expr_ref_vector bits1(m_manager);
-    expr_ref_vector bits2(m_manager);
-    get_bits(arg2, bits1);
-    get_bits(arg3, bits2);
-    SASSERT(bits1.size() == bits2.size());
-    expr_ref_vector out_bits(m_manager);
-    unsigned bv_size = bits1.size();
-    for (unsigned i = 0; i < bv_size; i++) {
-        expr_ref new_bit(m_manager);
-        m_s.mk_ite(arg1, bits1.get(i), bits2.get(i), new_bit);
-        out_bits.push_back(new_bit);
-    }
-    result = mk_mkbv(out_bits);
-    return true;
-}
-
-bool eager_bit_blaster::bv_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
-    bv_op_kind k = static_cast<bv_op_kind>(f->get_decl_kind());
-    switch (k) {
-    case OP_BNOT:
-        SASSERT(num_args == 1);
-        reduce_not(args[0], result);
-        return true;
-    case OP_BOR:
-        reduce_or(num_args, args, result);
-        return true;
-    case OP_BAND:
-        reduce_and(num_args, args, result);
-        return true;
-    case OP_BNOR:
-        reduce_nor(num_args, args, result);
-        return true;
-    case OP_BNAND:
-        reduce_nand(num_args, args, result);
-        return true;
-    case OP_BXOR:
-        SASSERT(num_args == 2);
-        reduce_xor(args[0], args[1], result);
-        return true;
-    case OP_BXNOR:
-        SASSERT(num_args == 2);
-        reduce_xnor(args[0], args[1], result);
-        return true;
-    case OP_BNEG:
-        SASSERT(num_args == 1);
-        reduce_neg(args[0], result);
-        return true;
-    case OP_BADD:
-        reduce_add(num_args, args, result);
-        return true;
-    case OP_BMUL:
-        reduce_mul(num_args, args, result);
-        return true;
-    case OP_BIT1:
-    case OP_BIT0:
-    case OP_BSUB:
-        // I'm assuming the expressions were simplified before invoking this method.
-        UNREACHABLE();
-        return false;
-    case OP_BSDIV:
-    case OP_BUDIV:
-    case OP_BSREM:
-    case OP_BUREM:
-    case OP_BSMOD:
-        // I'm assuming the expressions were simplified before invoking this method.
-        UNREACHABLE();
-        return false;
-    case OP_BSDIV0:
-    case OP_BUDIV0:
-    case OP_BSREM0:
-    case OP_BUREM0:
-    case OP_BSMOD0:
-        // do nothing... these are uninterpreted
-        return true;
-    case OP_BSDIV_I:
-        SASSERT(num_args == 2);
-        reduce_sdiv(args[0], args[1], result);
-        return true;
-    case OP_BUDIV_I:
-        SASSERT(num_args == 2);
-        reduce_udiv(args[0], args[1], result);
-        return true;
-    case OP_BSREM_I:
-        SASSERT(num_args == 2);
-        reduce_srem(args[0], args[1], result);
-        return true;
-    case OP_BUREM_I:
-        SASSERT(num_args == 2);
-        reduce_urem(args[0], args[1], result);
-        return true;
-    case OP_BSMOD_I:
-        SASSERT(num_args == 2);
-        reduce_smod(args[0], args[1], result);
-        return true;
-    case OP_ULEQ:
-        SASSERT(num_args == 2);
-        reduce_ule(args[0], args[1], result);
-        return true;
-    case OP_SLEQ:
-        SASSERT(num_args == 2);
-        reduce_sle(args[0], args[1], result);
-        return true;
-    case OP_UGEQ:
-    case OP_SGEQ:
-    case OP_ULT:
-    case OP_SLT:
-    case OP_UGT:
-    case OP_SGT:
-        // I'm assuming the expressions were simplified before invoking this method.
-        UNREACHABLE();
-        return false;
-    case OP_EXTRACT:
-        SASSERT(num_args == 1);
-        reduce_extract(f->get_parameter(1).get_int(), f->get_parameter(0).get_int(), args[0], result);
-        return true;
-    case OP_CONCAT:
-        reduce_concat(num_args, args, result);
-        return true;
-    case OP_SIGN_EXT:
-        SASSERT(num_args == 1);
-        reduce_sign_extend(args[0], f->get_parameter(0).get_int(), result);
-        return true;
-    case OP_ZERO_EXT:
-        SASSERT(num_args == 1);
-        reduce_zero_extend(args[0], f->get_parameter(0).get_int(), result);
-        return true;
-    case OP_REPEAT:
-        UNREACHABLE();
-        return false;
-    case OP_BREDOR:
-        SASSERT(num_args == 1);
-        reduce_redor(args[0], result);
-        return true;
-    case OP_BREDAND:
-        SASSERT(num_args == 1);
-        reduce_redand(args[0], result);
-        return true;
-    case OP_BCOMP:
-        SASSERT(num_args == 2);
-        reduce_comp(args[0], args[1], result);
-        return true;
-    case OP_BSHL:
-        SASSERT(num_args == 2);
-        reduce_shl(args[0], args[1], result);
-        return true;
-    case OP_BLSHR:
-        SASSERT(num_args == 2);
-        reduce_lshr(args[0], args[1], result);
-        return true;
-    case OP_BASHR:
-        SASSERT(num_args == 2);
-        reduce_ashr(args[0], args[1], result);
-        return true;
-    case OP_ROTATE_LEFT:
-        SASSERT(num_args == 1);
-        reduce_rotate_left(args[0], f->get_parameter(0).get_int(), result);
-        return true;
-    case OP_ROTATE_RIGHT:
-        SASSERT(num_args == 1);
-        reduce_rotate_right(args[0], f->get_parameter(0).get_int(), result);
-        return true;
-    default:
-        return false;
-    }
-}
-
-bool eager_bit_blaster::bv_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
-    TRACE("eager_bb_eq", tout << mk_ll_pp(lhs, m_manager) << "\n" << mk_ll_pp(rhs, m_manager) << "\n";);
-    SASSERT(m_util.get_bv_size(lhs) == m_util.get_bv_size(rhs));
-    expr_ref_vector bits1(m_manager);                                                   
-    expr_ref_vector bits2(m_manager);                                                   
-    get_bits(lhs, bits1);                                                              
-    get_bits(rhs, bits2); 
-    SASSERT(bits1.size() == bits2.size());
-    m_bb.mk_eq(bits1.size(), bits1.c_ptr(), bits2.c_ptr(), result);
-    return true;
-}
-
-bool eager_bit_blaster::bv_plugin::reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result) {
-    if (num_args <= 1) {
-        result = m_manager.mk_true();
-    }
-    if (num_args == 2) {
-        expr_ref tmp(m_manager);
-        reduce_eq(args[0], args[1], tmp);
-        m_s.mk_not(tmp, result);
-    }
-    else {
-        expr_ref_vector new_args(m_manager);
-        for (unsigned i = 0; i < num_args - 1; i++) {
-            expr * a1 = args[i];
-            for (unsigned j = i + 1; j < num_args; j++) {
-                expr * a2 = args[j];
-                expr_ref tmp1(m_manager);
-                reduce_eq(a1, a2, tmp1);
-                expr_ref tmp2(m_manager);
-                m_s.mk_not(tmp1, tmp2);
-                new_args.push_back(tmp2);
-            }
-        }
-        m_s.mk_and(new_args.size(), new_args.c_ptr(), result);
-    }
-    return true;
-}
-
-eager_bit_blaster::eager_bit_blaster(ast_manager & m, bit_blaster_params const & p):
-    m_simplifier(m) {
-    m_simplifier.enable_ac_support(false);
-    bv_plugin * bv_p = alloc(bv_plugin, m, p);
-    m_simplifier.register_plugin(bv_p);
-    m_simplifier.register_plugin(alloc(basic_plugin, m, *bv_p, bv_p->get_basic_simplifier()));
-}
-
-void eager_bit_blaster::operator()(expr * s, expr_ref & r, proof_ref & p) {
-    m_simplifier.operator()(s, r, p);
-}
-

src/ast/rewriter/bit_blaster/eager_bit_blaster.h

@@ -1,107 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    eager_bit_blaster.h
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-10-02.
-
-Revision History:
-
---*/
-#ifndef _EAGER_BIT_BLASTER_H_
-#define _EAGER_BIT_BLASTER_H_
-
-#include"bv_decl_plugin.h"
-#include"bit_blaster.h"
-#include"simplifier.h"
-#include"basic_simplifier_plugin.h"
-
-class eager_bit_blaster {
-
-    class bv_plugin : public simplifier_plugin {
-        bv_util                 m_util;
-        bit_blaster             m_bb;
-        basic_simplifier_plugin m_s;
-
-        void get_bits(expr * n, expr_ref_vector & out_bits);
-        app * mk_mkbv(expr_ref_vector const & bits);
-            
-        void reduce_not(expr * arg, expr_ref & result);
-        void reduce_bin_or(expr * arg1, expr * arg2, expr_ref & result);
-        void reduce_or(unsigned num_args, expr * const * args, expr_ref & result);
-        void reduce_bin_and(expr * arg1, expr * arg2, expr_ref & result);
-        void reduce_and(unsigned num_args, expr * const * args, expr_ref & result);
-        void reduce_bin_nor(expr * arg1, expr * arg2, expr_ref & result);
-        void reduce_nor(unsigned num_args, expr * const * args, expr_ref & result);
-        void reduce_bin_nand(expr * arg1, expr * arg2, expr_ref & result);
-        void reduce_nand(unsigned num_args, expr * const * args, expr_ref & result);
-        void reduce_xor(expr * arg1, expr * arg2, expr_ref & result);
-        void reduce_xnor(expr * arg1, expr * arg2, expr_ref & result);
-
-        void reduce_neg(expr * arg, expr_ref & result);
-        void reduce_bin_add(expr * arg1, expr * arg2, expr_ref & result);
-        void reduce_add(unsigned num_args, expr * const * args, expr_ref & result);
-        void reduce_bin_mul(expr * arg1, expr * arg2, expr_ref & result);
-        void reduce_mul(unsigned num_args, expr * const * args, expr_ref & result);
-        void reduce_sdiv(expr * arg1, expr * arg2, expr_ref & result);
-        void reduce_udiv(expr * arg1, expr * arg2, expr_ref & result);
-        void reduce_srem(expr * arg1, expr * arg2, expr_ref & result);
-        void reduce_urem(expr * arg1, expr * arg2, expr_ref & result);
-        void reduce_smod(expr * arg1, expr * arg2, expr_ref & result);
-        void reduce_sle(expr * arg1, expr * arg2, expr_ref & result);
-        void reduce_ule(expr * arg1, expr * arg2, expr_ref & result);
-
-        void reduce_concat(unsigned num_args, expr * const * args, expr_ref & result);
-        void reduce_extract(unsigned start, unsigned end, expr * arg, expr_ref & result);
-
-        void reduce_redor(expr * arg, expr_ref & result);
-        void reduce_redand(expr * arg, expr_ref & result);
-
-        void reduce_comp(expr * arg1, expr * arg2, expr_ref & result);
-        void reduce_shl(expr * arg1, expr * arg2, expr_ref & result);
-        void reduce_ashr(expr * arg1, expr * arg2, expr_ref & result);
-        void reduce_lshr(expr * arg1, expr * arg2, expr_ref & result);
-
-        void reduce_rotate_left(expr * arg, unsigned n, expr_ref & result);
-        void reduce_rotate_right(expr * arg, unsigned n, expr_ref & result);
-        void reduce_sign_extend(expr * arg, unsigned n, expr_ref & result);
-        void reduce_zero_extend(expr * arg, unsigned n, expr_ref & result);
-
-    public:
-        bv_plugin(ast_manager & m, bit_blaster_params const & p);
-        virtual ~bv_plugin();
-        virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
-        virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result);
-        virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result);
-        basic_simplifier_plugin & get_basic_simplifier() { return m_s; }
-        bool reduce_ite(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
-    };
-
-    /**
-       \brief Plugin for handling the term-ite.
-    */
-    class basic_plugin : public simplifier_plugin {
-        bv_plugin &               m_main;
-        basic_simplifier_plugin & m_s;
-    public:
-        basic_plugin(ast_manager & m, bv_plugin & p, basic_simplifier_plugin & s);
-        virtual ~basic_plugin();
-        virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
-    };
-
-    simplifier  m_simplifier;
-public:
-    eager_bit_blaster(ast_manager & m, bit_blaster_params const & p);
-    void operator()(expr * s, expr_ref & r, proof_ref & p);
-};
-
-#endif /* _EAGER_BIT_BLASTER_H_ */
-

src/front_end_params/bit_blaster_params.h

@@ -22,16 +22,13 @@ Revision History:
 #include"ini_file.h"
 
 struct bit_blaster_params {
-    bool  m_bb_eager;
     bool  m_bb_ext_gates;
     bool  m_bb_quantifiers;
     bit_blaster_params():
-        m_bb_eager(false),
         m_bb_ext_gates(false),
         m_bb_quantifiers(false) {
     }
     void register_params(ini_params & p) {
-        p.register_bool_param("BB_EAGER", m_bb_eager, "eager bit blasting");
         p.register_bool_param("BB_EXT_GATES", m_bb_ext_gates, "use extended gates during bit-blasting");
         p.register_bool_param("BB_QUANTIFIERS", m_bb_quantifiers, "convert bit-vectors to Booleans in quantifiers");
     }

src/front_end_params/front_end_params.cpp

@@ -21,12 +21,9 @@ Revision History:
 void front_end_params::register_params(ini_params & p) {
     p.register_param_vector(m_param_vector.get());
     preprocessor_params::register_params(p);
-    spc_params::register_params(p);
     smt_params::register_params(p);
     parser_params::register_params(p);
     arith_simplifier_params::register_params(p);
-    p.register_int_param("ENGINE", 0, 2, reinterpret_cast<int&>(m_engine), "0: SMT solver, 1: Superposition prover, 2: EPR solver, true");
-    z3_solver_params::register_params(p);
     model_params::register_params(p);
     p.register_unsigned_param("MAX_COUNTEREXAMPLES", m_max_num_cex, 
                               "set the maximum number of counterexamples when using Simplify front end");
@@ -45,7 +42,6 @@ void front_end_params::register_params(ini_params & p) {
     p.register_int_param("PROOF_MODE", 0, 2, reinterpret_cast<int&>(m_proof_mode), "select proof generation mode: 0 - disabled, 1 - coarse grain, 2 - fine grain");
     p.register_bool_param("TRACE", m_trace, "enable tracing for the Axiom Profiler tool");
     p.register_string_param("TRACE_FILE_NAME", m_trace_file_name, "tracing file name");
-    p.register_bool_param("IGNORE_SETPARAMETER", m_ignore_setparameter, "ignore (SETPARAMETER ...) commands in Simplify format input");
     p.register_bool_param("ASYNC_COMMANDS", m_async_commands, "enable/disable support for asynchronous commands in the Simplify front-end.");
     p.register_bool_param("DISPLAY_CONFIG", m_display_config, "display configuration used by Z3");
 

src/front_end_params/front_end_params.h

@@ -22,25 +22,16 @@ Revision History:
 #include"ini_file.h"
 #include"ast.h"
 #include"preprocessor_params.h"
-#include"spc_params.h"
 #include"smt_params.h"
 #include"pp_params.h"
 #include"parser_params.h"
 #include"arith_simplifier_params.h"
-#include"z3_solver_params.h"
 #include"model_params.h"
 
-enum engine {
-    ENG_SMT,
-    ENG_SPC,
-    ENG_EPR
-};
-
-struct front_end_params : public preprocessor_params, public spc_params, public smt_params, public parser_params, 
-                          public arith_simplifier_params, public z3_solver_params, public model_params
+struct front_end_params : public preprocessor_params, public smt_params, public parser_params, 
+                          public arith_simplifier_params, public model_params
                            {
     ref<param_vector>   m_param_vector;
-    engine              m_engine;
     unsigned            m_max_num_cex; // maximum number of counterexamples
     bool                m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
     bool                m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.
@@ -66,7 +57,6 @@ struct front_end_params : public preprocessor_params, public spc_params, public
     bool                m_trace;
     std::string         m_trace_file_name;
     std::fstream*       m_trace_stream;
-    bool                m_ignore_setparameter;
     bool                m_async_commands;
     bool                m_display_config;
     bool                m_user_theory_preprocess_axioms;
@@ -75,7 +65,6 @@ struct front_end_params : public preprocessor_params, public spc_params, public
 
     front_end_params():
         m_param_vector(alloc(param_vector, this)),
-        m_engine(ENG_SMT),
         m_max_num_cex(1),
         m_at_labels_cex(false),
         m_check_at_labels(false),
@@ -109,7 +98,6 @@ struct front_end_params : public preprocessor_params, public spc_params, public
         m_trace(false),
         m_trace_file_name("z3.log"),
         m_trace_stream(NULL),
-        m_ignore_setparameter(false),
         m_async_commands(true),
         m_display_config(false),
         m_user_theory_preprocess_axioms(false),

src/front_end_params/order_params.cpp

@@ -1,27 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    order_params.cpp
-
-Abstract:
-
-    Term ordering parameters.
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-01-28.
-
-Revision History:
-
---*/
-#include"order_params.h"
-
-void order_params::register_params(ini_params & p) {
-    p.register_symbol_list_param("PRECEDENCE", m_order_precedence, "describe a (partial) precedence for the term ordering used in the Superposition Calculus module. The precedence is lists of function symbols. Example: PRECEDENCE=\"(f, g, h)\"");
-    p.register_symbol_list_param("PRECEDENCE_GEN", m_order_precedence_gen, "describe how a total precedence order is generated. The generator is a sequence of simple (partial) orders with an optional '-' (indicating the next (partial) order should be inverted). The available simple (partial) orders are: user (the order specified by precedence); arity; interpreted (interpreted function symbols are considered smaller); definition (defined function symbols are considered bigger); frequency; arbitrary (total arbitrary order generated by Z3). Example: PRECEDENCE_GEN=\"user interpreted - arity arbitraty\"");
-    p.register_symbol_nat_list_param("ORDER_WEIGHTS", m_order_weights, "describe a (partial) assignment of weights to function symbols for term orderings (e.g., KBO). The assigment is a list of pairs of the form f:n where f is a string and n is a natural. Example: WEIGHTS=\"(f:1, g:2, h:3)\"");
-    p.register_unsigned_param("ORDER_VAR_WEIGHT", m_order_var_weight, "weight of variables in term orderings (e.g., KBO)");
-    p.register_int_param("ORDER", 0, 1, reinterpret_cast<int&>(m_order_kind), "Term ordering: 0 - KBO, 1 - LPO");
-}

src/front_end_params/order_params.h

@@ -1,44 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    order_params.h
-
-Abstract:
-
-    Term ordering parameters.
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-01-28.
-
-Revision History:
-
---*/
-#ifndef _ORDER_PARAMS_H_
-#define _ORDER_PARAMS_H_
-
-#include"ini_file.h"
-
-enum order_kind {
-    ORD_KBO,
-    ORD_LPO
-};
-
-struct order_params {
-    svector<symbol>          m_order_precedence;
-    svector<symbol>          m_order_precedence_gen;
-    svector<symbol_nat_pair> m_order_weights;
-    unsigned                 m_order_var_weight;
-    order_kind               m_order_kind;
-    
-    order_params():
-        m_order_var_weight(1),
-        m_order_kind(ORD_KBO) {
-    }
-
-    void register_params(ini_params & p);
-};
-
-#endif /* _ORDER_PARAMS_H_ */

src/front_end_params/spc_params.cpp

@@ -1,37 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    spc_params.cpp
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-02-08.
-
-Revision History:
-
---*/
-#include"spc_params.h"
-
-void spc_params::register_params(ini_params & p) {
-    order_params::register_params(p);
-    p.register_unsigned_param("SPC_MIN_FUNC_FREQ_SUBSUMPTION_INDEX",m_min_func_freq_subsumption_index,
-                              "minimal number of occurrences (in clauses) for a function symbol to be considered for subsumption indexing.");
-    p.register_unsigned_param("SPC_MAX_SUBSUMPTION_INDEX_FEATURES", m_max_subsumption_index_features,
-                              "maximum number of features to be used for subsumption index.");
-    p.register_unsigned_param("SPC_INITIAL_SUBSUMPTION_INDEX_OPT", m_initial_subsumption_index_opt,
-                              "after how many processed clauses the subsumption index is optimized.");
-    p.register_double_param("SPC_FACTOR_SUBSUMPTION_INDEX_OPT", m_factor_subsumption_index_opt,
-                            "after each optimization the threshold for optimization is increased by this factor. See INITIAL_SUBSUMPTION_INDEX_OPT.");
-    p.register_bool_param("SPC_BS", m_backward_subsumption, "Enable/disable backward subsumption in the superposition engine");
-    p.register_bool_param("SPC_ES", m_equality_subsumption, "Enable/disable equality resolution in the superposition engine");
-    p.register_unsigned_param("SPC_NUM_ITERATIONS", m_spc_num_iterations);
-    p.register_bool_param("SPC_TRACE", m_spc_trace);
-}
-
-

src/front_end_params/spc_params.h

@@ -1,49 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    spc_params.h
-
-Abstract:
-
-    Parameters for the Superposition Calculus Engine
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-02-08.
-
-Revision History:
-
---*/
-#ifndef _SPC_PARAMS_H_
-#define _SPC_PARAMS_H_
-
-#include"order_params.h"
-
-struct spc_params : public order_params {
-    unsigned m_min_func_freq_subsumption_index;
-    unsigned m_max_subsumption_index_features;
-    unsigned m_initial_subsumption_index_opt; 
-    double   m_factor_subsumption_index_opt;
-    bool     m_backward_subsumption;
-    bool     m_equality_subsumption;
-    unsigned m_spc_num_iterations;
-    bool     m_spc_trace;
-
-    spc_params():
-        m_min_func_freq_subsumption_index(100),
-        m_max_subsumption_index_features(32),
-        m_initial_subsumption_index_opt(1000),
-        m_factor_subsumption_index_opt(1.5),
-        m_backward_subsumption(true),
-        m_equality_subsumption(true),
-        m_spc_num_iterations(1000),
-        m_spc_trace(false) {
-    }
-    
-    void register_params(ini_params & p);
-};
-
-#endif /* _SPC_PARAMS_H_ */
-

src/front_end_params/z3_solver_params.cpp

@@ -1,30 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    z3_solver_params.cpp
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2007-06-11.
-
-Revision History:
-
---*/
-
-#include"z3_solver_params.h"
-
-void z3_solver_params::register_params(ini_params & p) {
-    p.register_bool_param("Z3_SOLVER_LL_PP", m_ast_ll_pp, "pretty print asserted constraints using low-level printer (Z3 input format specific)");
-    p.register_bool_param("Z3_SOLVER_SMT_PP", m_ast_smt_pp, "pretty print asserted constraints using SMT printer (Z3 input format specific)");
-    p.register_bool_param("PRE_SIMPLIFY_EXPR", m_pre_simplify_expr, "pre-simplify expressions when created over the API (example: -x -> (* -1 x))");
-    p.register_string_param("SMTLIB_TRACE_PATH", m_smtlib_trace_path, "path for converting Z3 formulas to SMTLIB benchmarks");
-    p.register_string_param("SMTLIB_SOURCE_INFO", m_smtlib_source_info, "additional source info to add to SMTLIB benchmark");
-    p.register_string_param("SMTLIB_CATEGORY", m_smtlib_category, "additional category info to add to SMTLIB benchmark");
-}
-

src/front_end_params/z3_solver_params.h

@@ -1,44 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    z3_solver_params.h
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2007-06-11.
-
-Revision History:
-
---*/
-#ifndef _Z3_SOLVER_PARAMS_H_
-#define _Z3_SOLVER_PARAMS_H_
-
-#include"ini_file.h"
-
-struct z3_solver_params {
-    bool     m_ast_ll_pp;
-    bool     m_ast_smt_pp;
-    bool     m_pre_simplify_expr;
-    std::string m_smtlib_trace_path;
-    std::string m_smtlib_source_info;
-    std::string m_smtlib_category;
-
-    z3_solver_params():
-        m_ast_ll_pp(false),
-        m_ast_smt_pp(false),
-        m_pre_simplify_expr(false),
-        m_smtlib_trace_path(""),
-        m_smtlib_source_info(""),
-        m_smtlib_category("")
-    {}
-    void register_params(ini_params & p);
-};
-
-#endif /* _Z3_SOLVER_PARAMS_H_ */
-

src/smt/asserted_formulas.cpp

@@ -40,7 +40,6 @@ Revision History:
 #include"der.h"
 #include"elim_bounds.h"
 #include"warning.h"
-#include"eager_bit_blaster.h"
 #include"bit2int.h"
 #include"distribute_forall.h"
 #include"quasi_macros.h"
@@ -340,13 +339,9 @@ void asserted_formulas::reduce() {
     INVOKE(m_params.m_quasi_macros && has_quantifiers(), apply_quasi_macros());    
     INVOKE(m_params.m_simplify_bit2int, apply_bit2int());
     INVOKE(m_params.m_eliminate_bounds && has_quantifiers(), cheap_quant_fourier_motzkin());
-    INVOKE(!m_params.m_bb_eager && has_quantifiers() && m_params.m_ematching, infer_patterns());
     INVOKE(m_params.m_max_bv_sharing && has_bv(), max_bv_sharing());
     INVOKE(m_params.m_bb_quantifiers, elim_bvs_from_quantifiers());
-    INVOKE(m_params.m_bb_eager, apply_eager_bit_blaster());                     
-    INVOKE(m_params.m_bb_eager && m_params.m_nnf_cnf, nnf_cnf());   // bit-blaster destroys CNF
     INVOKE(m_params.m_bb_quantifiers && m_params.m_der && has_quantifiers(), apply_der()); // bit-vector elimination + bit-blasting creates new opportunities for der.
-    INVOKE(m_params.m_bb_eager && has_quantifiers() && m_params.m_ematching, infer_patterns());
     // temporary HACK: make sure that arith & bv are list-assoc 
     // this may destroy some simplification steps such as max_bv_sharing
     reduce_asserted_formulas(); 
@@ -1434,8 +1429,6 @@ bool asserted_formulas::quant_elim() {
     return false;
 }
 
-MK_SIMPLIFIER(apply_eager_bit_blaster, eager_bit_blaster functor(m_manager, m_params), "eager_bb", "eager bit blasting", false);
-
 MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m_manager), "bv_elim", "eliminate bit-vectors from quantifiers", true);
 
 #define LIFT_ITE(NAME, FUNCTOR, MSG)                                                                                            \

src/smt/asserted_formulas.h

@@ -94,7 +94,6 @@ class asserted_formulas {
     void apply_demodulators();
     void apply_quasi_macros();
     void nnf_cnf();
-    bool apply_eager_bit_blaster();
     void infer_patterns();
     void eliminate_term_ite();
     void reduce_and_solve();