Java API: Bugfixes and Example.

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

examples/java/README

@@ -0,0 +1,10 @@
+### This is work-in-progress and does not work yet.
+
+Small example using the Z3 Java bindings.
+To build the example execute
+   make examples
+in the build directory.
+
+It will create JavaExample.class in the build directory,
+which can be run via
+   java -cp com.microsoft.z3.jar;. JavaExample

scripts/mk_project.py

@@ -79,6 +79,7 @@ def init_project_def():
     add_c_example('c_example', 'c')
     add_c_example('maxsat')
     add_dotnet_example('dotnet_example', 'dotnet')
+    add_java_example('java_example', 'java')
     add_z3py_example('py_example', 'python')
     return API_files
 

scripts/mk_util.py

@@ -1070,7 +1070,7 @@ class DotNetExampleComponent(ExampleComponent):
         if DOTNET_ENABLED:
             dll_name = get_component(DOTNET_COMPONENT).dll_name
             dll = '%s.dll' % dll_name
-            exefile = '%s.exe' % self.name
+            exefile = '%s$(EXE_EXT)' % self.name
             out.write('%s: %s' % (exefile, dll))
             for csfile in get_cs_files(self.ex_dir):
                 out.write(' ')
@@ -1089,6 +1089,28 @@ class DotNetExampleComponent(ExampleComponent):
             out.write('\n')
             out.write('_ex_%s: %s\n\n' % (self.name, exefile))
 
+class JavaExampleComponent(ExampleComponent):
+    def __init__(self, name, path):
+        ExampleComponent.__init__(self, name, path)
+
+    def is_example(self):
+        return True
+
+    def mk_makefile(self, out):
+        if JAVA_ENABLED:
+            pkg = get_component(JAVA_COMPONENT).package_name + '.jar'
+            out.write('_ex_%s: %s' % (self.name, pkg))
+            # for javafile in get_java_files(self.ex_dir):
+            #     out.write(' ')
+            #     out.write('%s/%s' % (self.to_ex_dir, javafile))
+            out.write('\n')
+            out.write('\t%s -cp %s ' % (JAVAC, pkg))
+            win_ex_dir = self.to_ex_dir
+            for javafile in get_java_files(self.ex_dir):
+                out.write(' ')
+                out.write('%s/%s' % (win_ex_dir, javafile))
+            out.write(' -d .\n\n')
+
 class PythonExampleComponent(ExampleComponent):
     def __init__(self, name, path):
         ExampleComponent.__init__(self, name, path)
@@ -1154,6 +1176,10 @@ def add_dotnet_example(name, path=None):
     c = DotNetExampleComponent(name, path)
     reg_component(name, c)
 
+def add_java_example(name, path=None):
+    c = JavaExampleComponent(name, path)
+    reg_component(name, c)
+
 def add_z3py_example(name, path=None):
     c = PythonExampleComponent(name, path)
     reg_component(name, c)

src/api/java/Context.java

@@ -525,7 +525,7 @@ public class Context extends IDisposable
 	public Expr MkConst(FuncDecl f) throws Z3Exception
 	{
 
-		return MkApp(f, null);
+	    return MkApp(f, (Expr)null);
 	}
 
 	/**
@@ -600,6 +600,17 @@ public class Context extends IDisposable
 		return (BitVecExpr) MkConst(name, MkBitVecSort(size));
 	}
 
+	/**
+	 * Create a new function application.
+	 **/
+	public Expr MkApp(FuncDecl f, Expr arg) throws Z3Exception
+	{
+	    CheckContextMatch(f);
+	    CheckContextMatch(arg);
+	    Expr[] args = { arg };
+	    return Expr.Create(this, f, args);
+	}
+
 	/**
 	 * Create a new function application.
 	 **/
@@ -2773,6 +2784,17 @@ public class Context extends IDisposable
 		return new Probe(this, Native.probeNot(nCtx(), p.NativeObject()));
 	}
 
+       /**
+	 * Creates a new (incremental) solver. <remarks> This solver also uses a set
+	 * of builtin tactics for handling the first check-sat command, and
+	 * check-sat commands that take more than a given number of milliseconds to
+	 * be solved. </remarks>
+	 **/
+	public Solver MkSolver() throws Z3Exception
+	{
+	    return MkSolver((Symbol)null);
+	}
+
 	/**
 	 * Creates a new (incremental) solver. <remarks> This solver also uses a set
 	 * of builtin tactics for handling the first check-sat command, and

src/api/java/EnumSort.java

@@ -59,6 +59,6 @@ public class EnumSort extends Sort
 			_testerdecls[i] = new FuncDecl(ctx, n_testers[i]);
 		_consts = new Expr[n];
 		for (int i = 0; i < n; i++)
-			_consts[i] = ctx.MkApp(_constdecls[i], null);
+		    _consts[i] = ctx.MkApp(_constdecls[i], (Expr)null);
 	}
 };

src/api/java/Expr.java

@@ -16,9 +16,18 @@ import com.microsoft.z3.enumerations.*;
 public class Expr extends AST
 {
 	/**
-	 * Returns a simplified version of the expression. <param name="p">A set of
+	 * Returns a simplified version of the expression
-	 * parameters to configure the simplifier</param> <seealso
+	 **/
-	 * cref="Context.SimplifyHelp"/>
+	public Expr Simplify() throws Z3Exception
+	{
+	    return Simplify(null);
+	}
+
+	/**
+	 * Returns a simplified version of the expression 
+	 * A set of
+	 * parameters <param name="p" /> to configure the simplifier 
+	 * <seealso cref="Context.SimplifyHelp"/>
 	 **/
 	public Expr Simplify(Params p) throws Z3Exception
 	{

src/api/java/FuncDecl.java

@@ -356,24 +356,36 @@ public class FuncDecl extends AST
 	}
 
 	/**
-	 * Create expression that applies function to arguments. <param
+	 * Create expression that applies function to arguments. 
-	 * name="args"></param>
+	 * <param name="args"></param>
 	 * 
 	 * @return
 	 **/
 	/* operator this[] not translated */
 
 	/**
-	 * Create expression that applies function to arguments. <param
+	 * Create expression that applies function to arguments.
-	 * name="args"></param>
+	 * <param name="args"></param>
 	 * 
 	 * @return
 	 **/
 	public Expr Apply(Expr[] args) throws Z3Exception
 	{
-
 		Context().CheckContextMatch(args);
 		return Expr.Create(Context(), this, args);
 	}
 
+	/**
+	 * Create expression that applies function to one argument.
+	 * <param name="arg"></param>
+	 * 
+	 * @return
+	 **/
+	public Expr Apply(Expr arg) throws Z3Exception
+	{
+		Context().CheckContextMatch(arg);
+		Expr[] a = { arg };
+		return Expr.Create(Context(), this, a);
+	}
+
 }

src/api/java/Goal.java

@@ -69,13 +69,22 @@ public class Goal extends Z3Object
 		Context().CheckContextMatch(constraints);
 		for (BoolExpr c : constraints)
 		{
-			// It was an assume, now made an assert just to be sure we do not
+		    Native.goalAssert(Context().nCtx(), NativeObject(),
-			// regress
+				      c.NativeObject());
-			Native.goalAssert(Context().nCtx(), NativeObject(),
-					c.NativeObject());
 		}
 	}
 
+        /**
+	 * Adds a <paramref name="constraint"/> to the given goal.
+	 * @throws Z3Exception 
+	 **/
+	public void Assert(BoolExpr constraint) throws Z3Exception
+	{
+	    Context().CheckContextMatch(constraint);		
+	    Native.goalAssert(Context().nCtx(), NativeObject(),
+			      constraint.NativeObject());
+	}
+
 	/**
 	 * Indicates whether the goal contains `false'.
 	 **/

src/api/java/Log.java

@@ -13,7 +13,7 @@ package com.microsoft.z3;
  **/
 public final class Log
 {
-    private boolean m_is_open = false;
+    private static boolean m_is_open = false;
 
     /**
      * Open an interaction log file. <param name="filename">the name of the file
@@ -21,7 +21,7 @@ public final class Log
      * 
      * @return True if opening the log file succeeds, false otherwise.
      **/
-    public boolean Open(String filename)
+    public static boolean Open(String filename)
     {
         m_is_open = true;
         return Native.openLog(filename) == 1;
@@ -30,7 +30,7 @@ public final class Log
     /**
      * Closes the interaction log.
      **/
-    public void Close()
+    public static void Close()
     {
         m_is_open = false;
         Native.closeLog();
@@ -41,7 +41,7 @@ public final class Log
      * log.
      * @throws Z3Exception 
      **/
-    public void Append(String s) throws Z3Exception
+    public static void Append(String s) throws Z3Exception
     {
         if (!m_is_open)
             throw new Z3Exception("Log cannot be closed.");
@@ -53,7 +53,7 @@ public final class Log
      * 
      * @return True if the interaction log is open, false otherwise.
      **/
-    public boolean isOpen()
+    public static boolean isOpen()
     {
         return m_is_open;
     }

src/api/java/Solver.java

@@ -59,6 +59,14 @@ public class Solver extends Z3Object
         Native.solverPush(Context().nCtx(), NativeObject());
     }
 
+    /**
+     * Backtracks one backtracking point. <remarks>.
+     **/
+    public void Pop()
+    {
+	Pop(1);
+    }
+
     /**
      * Backtracks <paramref name="n"/> backtracking points. <remarks>Note that
      * an exception is thrown if <paramref name="n"/> is not smaller than
@@ -79,7 +87,7 @@ public class Solver extends Z3Object
     }
 
     /**
-     * Assert a constraint (or multiple) into the solver.
+     * Assert a multiple constraints into the solver.
      * @throws Z3Exception 
      **/
     public void Assert(BoolExpr[] constraints) throws Z3Exception
@@ -92,6 +100,16 @@ public class Solver extends Z3Object
         }
     }
 
+    /**
+     * Assert one constraint into the solver.
+     * @throws Z3Exception 
+     **/
+    public void Assert(BoolExpr constraint) throws Z3Exception
+    {
+        Context().CheckContextMatch(constraint);
+	Native.solverAssert(Context().nCtx(), NativeObject(), constraint.NativeObject());
+    }
+
     /**
      * The number of assertions in the solver.
      * @throws Z3Exception 
@@ -144,6 +162,16 @@ public class Solver extends Z3Object
         }
     }
 
+    /**
+     * 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()
+    {
+	return Check(null);
+    }
+
     /**
      * 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

src/api/java/Tactic.java

@@ -33,6 +33,15 @@ public class Tactic extends Z3Object
                 .nCtx(), NativeObject()));
     }
 
+    /**
+     * Execute the tactic over the goal.
+     * @throws Z3Exception 
+     **/
+    public ApplyResult Apply(Goal g) throws Z3Exception
+    {	
+        return Apply(g, null);
+    }
+
     /**
      * Execute the tactic over the goal.
      * @throws Z3Exception 

src/api/java/Version.java

@@ -9,16 +9,12 @@ package com.microsoft.z3;
 /**
  * Version information. <remarks>Note that this class is static.</remarks>
  **/
-public final class Version
+public class Version
 {
-    Version()
-    {
-    }
-
     /**
      * The major version
      **/
-    public int Major()
+    public static int Major()
     {
         Native.IntPtr major = new Native.IntPtr(), minor = new Native.IntPtr(), build = new Native.IntPtr(), revision = new Native.IntPtr();
         Native.getVersion(major, minor, build, revision);
@@ -28,7 +24,7 @@ public final class Version
     /**
      * The minor version
      **/
-    public int Minor()
+    public static int Minor()
     {
         Native.IntPtr major = new Native.IntPtr(), minor = new Native.IntPtr(), build = new Native.IntPtr(), revision = new Native.IntPtr();
         Native.getVersion(major, minor, build, revision);
@@ -38,7 +34,7 @@ public final class Version
     /**
      * The build version
      **/
-    public int Build()
+    public static int Build()
     {
         Native.IntPtr major = new Native.IntPtr(), minor = new Native.IntPtr(), build = new Native.IntPtr(), revision = new Native.IntPtr();
         Native.getVersion(major, minor, build, revision);
@@ -48,7 +44,7 @@ public final class Version
     /**
      * The revision
      **/
-    public int Revision()
+    public static int Revision()
     {
         Native.IntPtr major = new Native.IntPtr(), minor = new Native.IntPtr(), build = new Native.IntPtr(), revision = new Native.IntPtr();
         Native.getVersion(major, minor, build, revision);
@@ -58,7 +54,7 @@ public final class Version
     /**
      * A string representation of the version information.
      **/
-    public String toString()
+    public static String getString()
     {
         Native.IntPtr major = new Native.IntPtr(), minor = new Native.IntPtr(), build = new Native.IntPtr(), revision = new Native.IntPtr();
         Native.getVersion(major, minor, build, revision);