diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index ae10d6740..2ff414f78 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -493,6 +493,9 @@ def get_c_files(path):
def get_cs_files(path):
return filter(lambda f: f.endswith('.cs'), os.listdir(path))
+def get_java_files(path):
+ return filter(lambda f: f.endswith('.java'), os.listdir(path))
+
def find_all_deps(name, deps):
new_deps = []
for dep in deps:
@@ -932,19 +935,21 @@ class JavaDLLComponent(Component):
def mk_makefile(self, out):
if is_java_enabled():
dllfile = '%s$(SO_EXT)' % self.dll_name
- out.write('%s: %s/Z3Native.java %s$(SO_EXT)\n' % (dllfile, self.to_src_dir, get_component('api_dll').dll_name))
- if IS_WINDOWS:
- out.write('\tcd %s && %s Z3Native.java\n' % (unix_path2dos(self.to_src_dir), JAVAC))
- out.write('\tmove %s\\*.class .\n' % unix_path2dos(self.to_src_dir))
- out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)Z3Native$(OBJ_EXT) -I"%s/include" -I"%s/include/win32" -I%s %s/Z3Native.c\n' % (JAVA_HOME, JAVA_HOME, get_component('api').to_src_dir, self.to_src_dir))
- out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) Z3Native$(OBJ_EXT) libz3.lib\n' % dllfile)
- else:
- out.write('\tcd %s; %s Z3Native.java\n' % (self.to_src_dir, JAVAC))
- out.write('\tmv %s/*.class .\n' % self.to_src_dir)
- out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)Z3Native$(OBJ_EXT) -I"%s/include" -I%s %s/Z3Native.c\n' % (JAVA_HOME, get_component('api').to_src_dir, self.to_src_dir))
- out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) -L. Z3Native$(OBJ_EXT) -lz3\n' % dllfile)
- out.write('%s: %s\n\n' % (self.name, dllfile))
- # TODO: Compile and package all the .class files.
+ subdir = self.package_name.replace(".","/")
+ out.write('libz3java$(SO_EXT): libz3$(SO_EXT) ../src/api/java/Native.cpp\n')
+ out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)Native$(OBJ_EXT) -I"%s/include" -I"%s/include/win32" -I%s %s/Native.cpp\n' % (JAVA_HOME, JAVA_HOME, get_component('api').to_src_dir, self.to_src_dir))
+ out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) Native$(OBJ_EXT) libz3.lib\n')
+ out.write('%s.jar: libz3java$(SO_EXT) ' % self.package_name)
+ # for java_file in get_java_files(self.src_dir):
+ # out.write('%s ' % java_file)
+ # for java_file in get_java_files((self.src_dir + "/%s/Enumerations") % subdir):
+ # out.write('%s ' % java_file)
+ out.write('\n')
+ src_wsub = self.to_src_dir + "/" + subdir;
+ out.write(('\tjavac %s/Enumerations/*.java -d api/java\n' % (src_wsub)).replace("/","\\"))
+ out.write(('\tjavac -cp api/java %s/*.java -d api/java\n' % (src_wsub)).replace("/","\\"))
+ out.write('\tjar cf %s.jar api/java/\n' % self.package_name)
+ out.write('java: %s.jar\n\n' % self.package_name)
def main_component(self):
return is_java_enabled()
@@ -1847,7 +1852,7 @@ def mk_z3consts_java(api_files):
if name not in DeprecatedEnums:
efile = open('%s/%s.java' % (gendir, name), 'w')
efile.write('/**\n * Automatically generated file\n **/\n\n')
- efile.write('package %s;\n\n' % java.package_name);
+ efile.write('package %s.Enumerations;\n\n' % java.package_name);
efile.write('/**\n')
efile.write(' * %s\n' % name)
diff --git a/scripts/update_api.py b/scripts/update_api.py
index 1eef11705..10849aede 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -501,7 +501,7 @@ def mk_java():
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_wrapperf = '%s/Native.cpp' % java_dir
java_native = open(java_nativef, 'w')
java_native.write('// Automatically generated file\n')
java_native.write('package com.Microsoft.Z3;\n')
diff --git a/src/api/java/com/Microsoft/Z3/Native.c b/src/api/java/Native.cpp
similarity index 100%
rename from src/api/java/com/Microsoft/Z3/Native.c
rename to src/api/java/Native.cpp
diff --git a/src/api/java/com/Microsoft/Z3/AST.java b/src/api/java/com/Microsoft/Z3/AST.java
index 069c07a4c..45e631694 100644
--- a/src/api/java/com/Microsoft/Z3/AST.java
+++ b/src/api/java/com/Microsoft/Z3/AST.java
@@ -87,7 +87,7 @@ import com.Microsoft.Z3.Enumerations.*;
* A context
* @return A copy of the AST which is associated with
**/
- public AST Translate(Context ctx)
+ public AST Translate(Context ctx) throws Z3Exception
{
@@ -157,7 +157,7 @@ import com.Microsoft.Z3.Enumerations.*;
}
AST(Context ctx) { super(ctx); { }}
- AST(Context ctx, long obj) { super(ctx, obj); { }}
+ AST(Context ctx, long obj) throws Z3Exception { super(ctx, obj); { }}
class DecRefQueue extends IDecRefQueue
{
@@ -172,7 +172,7 @@ import com.Microsoft.Z3.Enumerations.*;
}
};
- void IncRef(long o)
+ void IncRef(long o) throws Z3Exception
{
// Console.WriteLine("AST IncRef()");
if (Context() == null)
@@ -183,7 +183,7 @@ import com.Microsoft.Z3.Enumerations.*;
super.IncRef(o);
}
- void DecRef(long o)
+ void DecRef(long o) throws Z3Exception
{
// Console.WriteLine("AST DecRef()");
if (Context() == null)
@@ -194,7 +194,7 @@ import com.Microsoft.Z3.Enumerations.*;
super.DecRef(o);
}
- static AST Create(Context ctx, long obj)
+ static AST Create(Context ctx, long obj) throws Z3Exception
{
diff --git a/src/api/java/com/Microsoft/Z3/AlgebraicNum.java b/src/api/java/com/Microsoft/Z3/AlgebraicNum.java
index b9f5766ce..f98ccbce4 100644
--- a/src/api/java/com/Microsoft/Z3/AlgebraicNum.java
+++ b/src/api/java/com/Microsoft/Z3/AlgebraicNum.java
@@ -24,7 +24,7 @@ import com.Microsoft.Z3.Enumerations.*;
* the precision of the result
* @return A numeral Expr of sort Real
**/
- public RatNum ToUpper(int precision)
+ public RatNum ToUpper(int precision) throws Z3Exception
{
@@ -38,7 +38,7 @@ import com.Microsoft.Z3.Enumerations.*;
*
* @return A numeral Expr of sort Real
**/
- public RatNum ToLower(int precision)
+ public RatNum ToLower(int precision) throws Z3Exception
{
@@ -49,14 +49,14 @@ import com.Microsoft.Z3.Enumerations.*;
* Returns a string representation in decimal notation.
* The result has at most decimal places.
**/
- public String ToDecimal(int precision)
+ public String ToDecimal(int precision) throws Z3Exception
{
return Native.getNumeralDecimalString(Context().nCtx(), NativeObject(), precision);
}
- AlgebraicNum(Context ctx, long obj)
+ AlgebraicNum(Context ctx, long obj) throws Z3Exception
{ super(ctx, obj);
}
diff --git a/src/api/java/com/Microsoft/Z3/ArithExpr.java b/src/api/java/com/Microsoft/Z3/ArithExpr.java
index 8df3bb0a5..fa87bf2f1 100644
--- a/src/api/java/com/Microsoft/Z3/ArithExpr.java
+++ b/src/api/java/com/Microsoft/Z3/ArithExpr.java
@@ -25,7 +25,7 @@ import com.Microsoft.Z3.Enumerations.*;
{ super(ctx);
}
- ArithExpr(Context ctx, long obj)
+ ArithExpr(Context ctx, long obj) throws Z3Exception
{ super(ctx, obj);
}
diff --git a/src/api/java/com/Microsoft/Z3/BitVecExpr.java b/src/api/java/com/Microsoft/Z3/BitVecExpr.java
index bbb13a873..d7c43918e 100644
--- a/src/api/java/com/Microsoft/Z3/BitVecExpr.java
+++ b/src/api/java/com/Microsoft/Z3/BitVecExpr.java
@@ -23,7 +23,7 @@ import com.Microsoft.Z3.Enumerations.*;
/**
* The size of the sort of a bit-vector term.
**/
- public int SortSize() { return ((BitVecSort)Sort).Size; }
+ public int SortSize() { return ((BitVecSort)Sort()).Size(); }
/** Constructor for BitVecExpr
**/
diff --git a/src/api/java/com/Microsoft/Z3/Constructor.java b/src/api/java/com/Microsoft/Z3/Constructor.java
index d7d534873..bcf5654a4 100644
--- a/src/api/java/com/Microsoft/Z3/Constructor.java
+++ b/src/api/java/com/Microsoft/Z3/Constructor.java
@@ -92,11 +92,11 @@ import com.Microsoft.Z3.Enumerations.*;
if (sortRefs == null) sortRefs = new int[n];
- NativeObject() = Native.mkConstructor(ctx.nCtx(), name.NativeObject(), recognizer.NativeObject(),
- n,
- Symbol.ArrayToNative(fieldNames),
- Sort.ArrayToNative(sorts),
- sortRefs);
+ setNativeObject(Native.mkConstructor(ctx.nCtx(), name.NativeObject(), recognizer.NativeObject(),
+ n,
+ Symbol.ArrayToNative(fieldNames),
+ Sort.ArrayToNative(sorts),
+ sortRefs));
}
diff --git a/src/api/java/com/Microsoft/Z3/Context.java b/src/api/java/com/Microsoft/Z3/Context.java
index 079bcaf43..8b83271a1 100644
--- a/src/api/java/com/Microsoft/Z3/Context.java
+++ b/src/api/java/com/Microsoft/Z3/Context.java
@@ -42,6 +42,12 @@ import com.Microsoft.Z3.Enumerations.*;
InitContext();
}
+ private Context(long ctx)
+ {
+ super();
+ this.m_ctx = ctx;
+ }
+
/**
* Creates a new symbol using an integer.
*
@@ -591,7 +597,7 @@ import com.Microsoft.Z3.Enumerations.*;
- return MkApp(f);
+ return MkApp(f, null);
}
/**
@@ -2205,15 +2211,6 @@ import com.Microsoft.Z3.Enumerations.*;
return Expr.Create(this, Native.mkInt(nCtx(), v, ty.NativeObject()));
}
- /**
- * Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
- * It is slightly faster than MakeNumeral since it is not necessary to parse a string.
- * Value of the numeral
- * Sort of the numeral
- * @return A Term with value and type
- **/
- /* Not translated because it would translate to a function with clashing types. */
-
/**
* Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
* It is slightly faster than MakeNumeral since it is not necessary to parse a string.
@@ -2230,15 +2227,6 @@ import com.Microsoft.Z3.Enumerations.*;
return Expr.Create(this, Native.mkInt64(nCtx(), v, ty.NativeObject()));
}
- /**
- * Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
- * It is slightly faster than MakeNumeral since it is not necessary to parse a string.
- * Value of the numeral
- * Sort of the numeral
- * @return A Term with value and type
- **/
- /* Not translated because it would translate to a function with clashing types. */
-
/**
* Create a real from a fraction.
* numerator of rational.
@@ -2281,13 +2269,6 @@ import com.Microsoft.Z3.Enumerations.*;
return new RatNum(this, Native.mkInt(nCtx(), v, RealSort().NativeObject()));
}
- /**
- * Create a real numeral.
- * value of the numeral.
- * @return A Term with value and sort Real
- **/
- /* Not translated because it would translate to a function with clashing types. */
-
/**
* Create a real numeral.
* value of the numeral.
@@ -2300,13 +2281,6 @@ import com.Microsoft.Z3.Enumerations.*;
return new RatNum(this, Native.mkInt64(nCtx(), v, RealSort().NativeObject()));
}
- /**
- * Create a real numeral.
- * value of the numeral.
- * @return A Term with value and sort Real
- **/
- /* Not translated because it would translate to a function with clashing types. */
-
/**
* Create an integer numeral.
* A string representing the Term value in decimal notation.
@@ -2330,13 +2304,6 @@ import com.Microsoft.Z3.Enumerations.*;
return new IntNum(this, Native.mkInt(nCtx(), v, IntSort().NativeObject()));
}
- /**
- * Create an integer numeral.
- * value of the numeral.
- * @return A Term with value and sort Integer
- **/
- /* Not translated because it would translate to a function with clashing types. */
-
/**
* Create an integer numeral.
* value of the numeral.
@@ -2349,13 +2316,6 @@ import com.Microsoft.Z3.Enumerations.*;
return new IntNum(this, Native.mkInt64(nCtx(), v, IntSort().NativeObject()));
}
- /**
- * Create an integer numeral.
- * value of the numeral.
- * @return A Term with value and sort Integer
- **/
- /* Not translated because it would translate to a function with clashing types. */
-
/**
* Create a bit-vector numeral.
* A string representing the value in decimal notation.
@@ -2380,13 +2340,6 @@ import com.Microsoft.Z3.Enumerations.*;
return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
}
- /**
- * Create a bit-vector numeral.
- * value of the numeral.
- * the size of the bit-vector
- **/
- /* Not translated because it would translate to a function with clashing types. */
-
/**
* Create a bit-vector numeral.
* value of the numeral.
@@ -2399,13 +2352,6 @@ import com.Microsoft.Z3.Enumerations.*;
return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
}
- /**
- * Create a bit-vector numeral.
- * value of the numeral.
- * the size of the bit-vector
- **/
- /* Not translated because it would translate to a function with clashing types. */
-
/**
* Create a universal Quantifier.
@@ -2551,7 +2497,7 @@ import com.Microsoft.Z3.Enumerations.*;
*
*
**/
- public void setPrintMode(Z3_ast_print_mode value) { Native.setAstPrintMode(nCtx(), (int)value); }
+ public void setPrintMode(Z3_ast_print_mode value) { Native.setAstPrintMode(nCtx(), value.toInt()); }
/**
* Convert a benchmark into an SMT-LIB formatted string.
@@ -3356,12 +3302,12 @@ import com.Microsoft.Z3.Enumerations.*;
**/
public String GetParamValue(String id)
{
- long res = 0;
- int r = Native.getParamValue(nCtx(), id, res);
- if (r == Z3_lbool.Z3_L_FALSE.toInt())
+ String res = new String();
+ boolean r = Native.getParamValue(nCtx(), id, res);
+ if (!r)
return null;
else
- return Marshal.PtrToStringAnsi(res);
+ return res;
}
@@ -3376,7 +3322,7 @@ import com.Microsoft.Z3.Enumerations.*;
void InitContext()
{
- PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
+ setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT);
m_n_err_handler = new Native.errorHandler(NativeErrorHandler); // keep reference so it doesn't get collected.
Native.setErrorHandler(m_ctx, m_n_err_handler);
@@ -3386,7 +3332,7 @@ import com.Microsoft.Z3.Enumerations.*;
{
- if (!ReferenceEquals(this, other.Context))
+ if (this == other.Context())
throw new Z3Exception("Context mismatch");
}
@@ -3402,25 +3348,6 @@ import com.Microsoft.Z3.Enumerations.*;
CheckContextMatch(a);
}
}
- }
-
- private void ObjectInvariant()
- {
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
}
private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue();
@@ -3473,7 +3400,8 @@ import com.Microsoft.Z3.Enumerations.*;
m_ctx = 0;
}
else
- GC.ReRegisterForFinalize(this);
+ /* re-queue the finalizer */
+ new Context(m_ctx);
}
/**
diff --git a/src/api/java/com/Microsoft/Z3/DatatypeSort.java b/src/api/java/com/Microsoft/Z3/DatatypeSort.java
index 4d2dd8992..536bfa8bb 100644
--- a/src/api/java/com/Microsoft/Z3/DatatypeSort.java
+++ b/src/api/java/com/Microsoft/Z3/DatatypeSort.java
@@ -61,7 +61,7 @@ import com.Microsoft.Z3.Enumerations.*;
for (int i = 0; i < n; i++)
{
FuncDecl fd = new FuncDecl(Context(), Native.getDatatypeSortConstructor(Context().nCtx(), NativeObject(), i));
- int ds = fd.DomainSize;
+ int ds = fd.DomainSize();
FuncDecl[] tmp = new FuncDecl[ds];
for (int j = 0; j < ds; j++)
tmp[j] = new FuncDecl(Context(), Native.getDatatypeSortConstructorAccessor(Context().nCtx(), NativeObject(), i, j));
diff --git a/src/api/java/com/Microsoft/Z3/EnumSort.java b/src/api/java/com/Microsoft/Z3/EnumSort.java
index cfb9d099a..ab0620003 100644
--- a/src/api/java/com/Microsoft/Z3/EnumSort.java
+++ b/src/api/java/com/Microsoft/Z3/EnumSort.java
@@ -68,8 +68,8 @@ import com.Microsoft.Z3.Enumerations.*;
int n = enumNames.length;
long[] n_constdecls = new long[n];
long[] n_testers = new long[n];
- NativeObject() = Native.mkEnumerationSort(ctx.nCtx(), name.NativeObject(), (int)n,
- Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
+ setNativeObject(Native.mkEnumerationSort(ctx.nCtx(), name.NativeObject(), (int)n,
+ Symbol.ArrayToNative(enumNames), n_constdecls, n_testers));
_constdecls = new FuncDecl[n];
for (int i = 0; i < n; i++)
_constdecls[i] = new FuncDecl(ctx, n_constdecls[i]);
@@ -78,6 +78,6 @@ import com.Microsoft.Z3.Enumerations.*;
_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]);
+ _consts[i] = ctx.MkApp(_constdecls[i], null);
}
};
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java
index 66841c073..931d70f62 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java
@@ -2,7 +2,7 @@
* Automatically generated file
**/
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
/**
* Z3_ast_kind
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java
index bfbbadd96..37da961d7 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java
@@ -2,7 +2,7 @@
* Automatically generated file
**/
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
/**
* Z3_ast_print_mode
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java
index c9ae9aa35..dd701c1e1 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java
@@ -2,7 +2,7 @@
* Automatically generated file
**/
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
/**
* Z3_decl_kind
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java
index 0c1c22870..2672c9325 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java
@@ -2,7 +2,7 @@
* Automatically generated file
**/
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
/**
* Z3_error_code
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java
index 2d96c6e76..f16fe51ec 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java
@@ -2,7 +2,7 @@
* Automatically generated file
**/
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
/**
* Z3_goal_prec
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java
index d31f5c238..55d5d7e17 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java
@@ -2,7 +2,7 @@
* Automatically generated file
**/
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
/**
* Z3_lbool
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java
index 81b8ef7bd..086622e95 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java
@@ -2,7 +2,7 @@
* Automatically generated file
**/
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
/**
* Z3_param_kind
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java
index c009104ba..021157183 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java
@@ -2,7 +2,7 @@
* Automatically generated file
**/
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
/**
* Z3_parameter_kind
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java
index 43f5b2f14..91559a58a 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java
@@ -2,7 +2,7 @@
* Automatically generated file
**/
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
/**
* Z3_sort_kind
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java
index 2f08236de..0866dc786 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java
@@ -2,7 +2,7 @@
* Automatically generated file
**/
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
/**
* Z3_symbol_kind
diff --git a/src/api/java/com/Microsoft/Z3/Expr.java b/src/api/java/com/Microsoft/Z3/Expr.java
index 0851acf70..9cf25ed11 100644
--- a/src/api/java/com/Microsoft/Z3/Expr.java
+++ b/src/api/java/com/Microsoft/Z3/Expr.java
@@ -21,7 +21,7 @@ import com.Microsoft.Z3.Enumerations.*;
* A set of parameters to configure the simplifier
*
**/
- public Expr Simplify(Params p)
+ public Expr Simplify(Params p) throws Z3Exception
{
@@ -54,7 +54,7 @@ import com.Microsoft.Z3.Enumerations.*;
/**
* The arguments of the expression.
**/
- public Expr[] Args()
+ public Expr[] Args() throws Z3Exception
{
@@ -69,7 +69,7 @@ import com.Microsoft.Z3.Enumerations.*;
* Update the arguments of the expression using the arguments
* The number of new arguments should coincide with the current number of arguments.
**/
- public void Update(Expr[] args)
+ public void Update(Expr[] args) throws Z3Exception
{
@@ -88,7 +88,7 @@ import com.Microsoft.Z3.Enumerations.*;
* sort of from[i] must be equal to sort of to[i].
*
**/
- public Expr Substitute(Expr[] from, Expr[] to)
+ public Expr Substitute(Expr[] from, Expr[] to) throws Z3Exception
{
@@ -107,7 +107,7 @@ import com.Microsoft.Z3.Enumerations.*;
* Substitute every occurrence of from in the expression with to.
*
**/
- public Expr Substitute(Expr from, Expr to)
+ public Expr Substitute(Expr from, Expr to) throws Z3Exception
{
@@ -122,7 +122,7 @@ import com.Microsoft.Z3.Enumerations.*;
* For every i smaller than num_exprs, the variable with de-Bruijn index i is replaced with term to[i].
*
**/
- public Expr SubstituteVars(Expr[] to)
+ public Expr SubstituteVars(Expr[] to) throws Z3Exception
{
@@ -137,7 +137,7 @@ import com.Microsoft.Z3.Enumerations.*;
* A context
* @return A copy of the term which is associated with
**/
- public Expr Translate(Context ctx)
+ public Expr Translate(Context ctx) throws Z3Exception
{
@@ -1367,7 +1367,7 @@ import com.Microsoft.Z3.Enumerations.*;
* index.
*
**/
- public int Index()
+ public int Index() throws Z3Exception
{
if (!IsVar())
throw new Z3Exception("Term is not a bound variable.");
@@ -1384,9 +1384,9 @@ import com.Microsoft.Z3.Enumerations.*;
/**
* Constructor for Expr
**/
- protected Expr(Context ctx, long obj) { super(ctx, obj); { }}
+ protected Expr(Context ctx, long obj) throws Z3Exception { super(ctx, obj); { }}
- void CheckNativeObject(long obj)
+ void CheckNativeObject(long obj) throws Z3Exception
{
if (Native.isApp(Context().nCtx(), obj) ^ true &&
Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() &&
@@ -1395,7 +1395,7 @@ import com.Microsoft.Z3.Enumerations.*;
super.CheckNativeObject(obj);
}
- static Expr Create(Context ctx, FuncDecl f, Expr[] arguments)
+ static Expr Create(Context ctx, FuncDecl f, Expr[] arguments) throws Z3Exception
{
@@ -1407,7 +1407,7 @@ import com.Microsoft.Z3.Enumerations.*;
return Create(ctx, obj);
}
- static Expr Create(Context ctx, long obj)
+ static Expr Create(Context ctx, long obj) throws Z3Exception
{
diff --git a/src/api/java/com/Microsoft/Z3/Fixedpoint.java b/src/api/java/com/Microsoft/Z3/Fixedpoint.java
index 104fd354c..e2cc2a1e9 100644
--- a/src/api/java/com/Microsoft/Z3/Fixedpoint.java
+++ b/src/api/java/com/Microsoft/Z3/Fixedpoint.java
@@ -123,8 +123,8 @@ import com.Microsoft.Z3.Enumerations.*;
Context().CheckContextMatch(relations);
- Z3_lbool r = (Z3_lbool)Native.fixedpointQueryRelations(Context().nCtx(), NativeObject(),
- AST.ArrayLength(relations), AST.ArrayToNative(relations));
+ Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQueryRelations(Context().nCtx(), NativeObject(),
+ AST.ArrayLength(relations), AST.ArrayToNative(relations)));
switch (r)
{
case Z3_L_TRUE: return Status.SATISFIABLE;
@@ -248,10 +248,10 @@ import com.Microsoft.Z3.Enumerations.*;
ASTVector v = new ASTVector(Context(), Native.fixedpointGetRules(Context().nCtx(), NativeObject()));
- int n = v.Size;
+ int n = v.Size();
BoolExpr[] res = new BoolExpr[n];
for (int i = 0; i < n; i++)
- res[i] = new BoolExpr(Context(), v[i].NativeObject());
+ res[i] = new BoolExpr(Context(), v.get(i).NativeObject());
return res;
}
@@ -263,10 +263,10 @@ import com.Microsoft.Z3.Enumerations.*;
ASTVector v = new ASTVector(Context(), Native.fixedpointGetAssertions(Context().nCtx(), NativeObject()));
- int n = v.Size;
+ int n = v.Size();
BoolExpr[] res = new BoolExpr[n];
for (int i = 0; i < n; i++)
- res[i] = new BoolExpr(Context(), v[i].NativeObject());
+ res[i] = new BoolExpr(Context(), v.get(i).NativeObject());
return res;
}
diff --git a/src/api/java/com/Microsoft/Z3/FuncDecl.java b/src/api/java/com/Microsoft/Z3/FuncDecl.java
index aa716c028..82cccc36f 100644
--- a/src/api/java/com/Microsoft/Z3/FuncDecl.java
+++ b/src/api/java/com/Microsoft/Z3/FuncDecl.java
@@ -77,7 +77,7 @@ import com.Microsoft.Z3.Enumerations.*;
{
- var n = DomainSize;
+ int n = DomainSize();
Sort[] res = new Sort[n];
for (int i = 0; i < n; i++)
@@ -171,25 +171,25 @@ import com.Microsoft.Z3.Enumerations.*;
/**The int value of the parameter.
**/
- public int Int () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_INT) throw new Z3Exception("parameter is not an int"); return i; }
+ public int Int () { if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_INT) throw new Z3Exception("parameter is not an int"); return i; }
/**The double value of the parameter.
**/
- public double Double () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_DOUBLE) throw new Z3Exception("parameter is not a double "); return d; }
+ public double Double () { if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_DOUBLE) throw new Z3Exception("parameter is not a double "); return d; }
/**The Symbol value of the parameter.
**/
- public Symbol Symbol () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_SYMBOL) throw new Z3Exception("parameter is not a Symbol"); return sym; }
+ public Symbol Symbol () { if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SYMBOL) throw new Z3Exception("parameter is not a Symbol"); return sym; }
/**The Sort value of the parameter.
**/
- public Sort Sort () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_SORT) throw new Z3Exception("parameter is not a Sort"); return srt; }
+ public Sort Sort () { if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SORT) throw new Z3Exception("parameter is not a Sort"); return srt; }
/**The AST value of the parameter.
**/
- public AST AST () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_AST) throw new Z3Exception("parameter is not an AST"); return ast; }
+ public AST AST () { if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_AST) throw new Z3Exception("parameter is not an AST"); return ast; }
/**The FunctionDeclaration value of the parameter.
**/
- public FuncDecl FuncDecl () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL) throw new Z3Exception("parameter is not a function declaration"); return fd; }
+ public FuncDecl FuncDecl () { if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL) throw new Z3Exception("parameter is not a function declaration"); return fd; }
/**The rational string value of the parameter.
**/
- public String Rational () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_RATIONAL) throw new Z3Exception("parameter is not a rational String"); return r; }
+ public String Rational () { if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_RATIONAL) throw new Z3Exception("parameter is not a rational String"); return r; }
/**
* The kind of the parameter.
diff --git a/src/api/java/com/Microsoft/Z3/FuncInterp.java b/src/api/java/com/Microsoft/Z3/FuncInterp.java
index 341b82ec5..17ff7d6bd 100644
--- a/src/api/java/com/Microsoft/Z3/FuncInterp.java
+++ b/src/api/java/com/Microsoft/Z3/FuncInterp.java
@@ -59,10 +59,10 @@ import com.Microsoft.Z3.Enumerations.*;
{
int n = NumArgs();
String res = "[";
- Expr[] args = Args;
+ Expr[] args = Args();
for (int i = 0; i < n; i++)
res += args[i] + ", ";
- return res + Value + "]";
+ return res + Value() + "]";
}
Entry(Context ctx, long obj) { super(ctx, obj); { }}
@@ -135,20 +135,20 @@ import com.Microsoft.Z3.Enumerations.*;
{
String res = "";
res += "[";
- for (Entry e: Entries)
+ for (Entry e: Entries())
{
- int n = e.NumArgs;
+ int n = e.NumArgs();
if (n > 1) res += "[";
- Expr[] args = e.Args;
+ Expr[] args = e.Args();
for (int i = 0; i < n; i++)
{
if (i != 0) res += ", ";
res += args[i];
}
if (n > 1) res += "]";
- res += " -> " + e.Value + ", ";
+ res += " -> " + e.Value() + ", ";
}
- res += "else -> " + Else;
+ res += "else -> " + Else();
res += "]";
return res;
}
diff --git a/src/api/java/com/Microsoft/Z3/Goal.java b/src/api/java/com/Microsoft/Z3/Goal.java
index 9f522a768..9ca138140 100644
--- a/src/api/java/com/Microsoft/Z3/Goal.java
+++ b/src/api/java/com/Microsoft/Z3/Goal.java
@@ -31,21 +31,21 @@ import com.Microsoft.Z3.Enumerations.*;
/**
* Indicates whether the goal is precise.
**/
- public boolean IsPrecise() { return Precision == Z3_goal_prec.Z3_GOAL_PRECISE; }
+ public boolean IsPrecise() { return Precision() == Z3_goal_prec.Z3_GOAL_PRECISE; }
/**
* Indicates whether the goal is an under-approximation.
**/
- public boolean IsUnderApproximation() { return Precision == Z3_goal_prec.Z3_GOAL_UNDER; }
+ public boolean IsUnderApproximation() { return Precision() == Z3_goal_prec.Z3_GOAL_UNDER; }
/**
* Indicates whether the goal is an over-approximation.
**/
- public boolean IsOverApproximation() { return Precision == Z3_goal_prec.Z3_GOAL_OVER; }
+ public boolean IsOverApproximation() { return Precision() == Z3_goal_prec.Z3_GOAL_OVER; }
/**
* Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).
**/
- public boolean IsGarbage() { return Precision == Z3_goal_prec.Z3_GOAL_UNDER_OVER; }
+ public boolean IsGarbage() { return Precision() == Z3_goal_prec.Z3_GOAL_UNDER_OVER; }
/**
* Adds the to the given goal.
@@ -96,7 +96,7 @@ import com.Microsoft.Z3.Enumerations.*;
{
- int n = Size;
+ int n = Size();
BoolExpr[] res = new BoolExpr[n];
for (int i = 0; i < n; i++)
res[i] = new BoolExpr(Context(), Native.goalFormula(Context().nCtx(), NativeObject(), i));
@@ -132,15 +132,15 @@ import com.Microsoft.Z3.Enumerations.*;
* Simplifies the goal.
* Essentially invokes the `simplify' tactic on the goal.
**/
- public Goal Simplify(Params p)
+ public Goal Simplify(Params p) throws Z3Exception
{
Tactic t = Context().MkTactic("simplify");
ApplyResult res = t.Apply(this, p);
- if (res.NumSubgoals == 0)
- return Context().MkGoal();
+ if (res.NumSubgoals() == 0)
+ throw new Z3Exception("No subgoals");
else
- return res.Subgoals[0];
+ return res.Subgoals()[0];
}
/**
@@ -152,11 +152,11 @@ import com.Microsoft.Z3.Enumerations.*;
return Native.goalToString(Context().nCtx(), NativeObject());
}
- Goal(Context ctx, long obj) { super(ctx, obj); { }}
+ Goal(Context ctx, long obj) { super(ctx, obj); { }}
Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs)
- { super(ctx, Native.mkGoal(ctx.nCtx(), (models) ? true : false, (unsatCores) ? true : false, (proofs) ? true : false));
-
+ {
+ super(ctx, Native.mkGoal(ctx.nCtx(), (models) ? true : false, (unsatCores) ? true : false, (proofs) ? true : false));
}
class DecRefQueue extends IDecRefQueue
diff --git a/src/api/java/com/Microsoft/Z3/IDisposable.java b/src/api/java/com/Microsoft/Z3/IDisposable.java
index 03885d1e7..e0cbb84f0 100644
--- a/src/api/java/com/Microsoft/Z3/IDisposable.java
+++ b/src/api/java/com/Microsoft/Z3/IDisposable.java
@@ -21,5 +21,5 @@ package com.Microsoft.Z3;
public class IDisposable
{
- public void Dispose() {}
+ public void Dispose() throws Z3Exception {}
}
diff --git a/src/api/java/com/Microsoft/Z3/IntSymbol.java b/src/api/java/com/Microsoft/Z3/IntSymbol.java
index 1750d87e6..7b917c11d 100644
--- a/src/api/java/com/Microsoft/Z3/IntSymbol.java
+++ b/src/api/java/com/Microsoft/Z3/IntSymbol.java
@@ -39,7 +39,7 @@ import com.Microsoft.Z3.Enumerations.*;
void CheckNativeObject(long obj)
{
- if ((Z3_symbol_kind)Native.getSymbolKind(Context().nCtx(), obj) != Z3_symbol_kind.Z3_INT_SYMBOL)
+ if (Native.getSymbolKind(Context().nCtx(), obj) != Z3_symbol_kind.Z3_INT_SYMBOL.toInt())
throw new Z3Exception("Symbol is not of integer kind");
super.CheckNativeObject(obj);
}
diff --git a/src/api/java/com/Microsoft/Z3/ListSort.java b/src/api/java/com/Microsoft/Z3/ListSort.java
index 4efee3783..7e7b03f79 100644
--- a/src/api/java/com/Microsoft/Z3/ListSort.java
+++ b/src/api/java/com/Microsoft/Z3/ListSort.java
@@ -110,8 +110,8 @@ import com.Microsoft.Z3.Enumerations.*;
ihead = 0,
itail = 0;
- NativeObject() = Native.mkListSort(ctx.nCtx(), name.NativeObject(), elemSort.NativeObject(),
- inil, iisnil, icons, iiscons, ihead, itail);
+ setNativeObject(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);
diff --git a/src/api/java/com/Microsoft/Z3/Model.java b/src/api/java/com/Microsoft/Z3/Model.java
index c0c0e2852..f17dc1956 100644
--- a/src/api/java/com/Microsoft/Z3/Model.java
+++ b/src/api/java/com/Microsoft/Z3/Model.java
@@ -26,7 +26,7 @@ import com.Microsoft.Z3.Enumerations.*;
Context().CheckContextMatch(a);
- return ConstInterp(a.FuncDecl);
+ return ConstInterp(a.FuncDecl());
}
/**
@@ -39,7 +39,7 @@ import com.Microsoft.Z3.Enumerations.*;
Context().CheckContextMatch(f);
- if (f.Arity != 0 ||
+ if (f.Arity() != 0 ||
Native.getSortKind(Context().nCtx(), Native.getRange(Context().nCtx(), f.NativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT.toInt())
throw new Z3Exception("Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");
@@ -63,7 +63,7 @@ import com.Microsoft.Z3.Enumerations.*;
Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(Context().nCtx(), Native.getRange(Context().nCtx(), f.NativeObject())));
- if (f.Arity == 0)
+ if (f.Arity() == 0)
{
long n = Native.modelGetConstInterp(Context().nCtx(), NativeObject(), f.NativeObject());
@@ -139,8 +139,8 @@ import com.Microsoft.Z3.Enumerations.*;
{
- var nFuncs = NumFuncs();
- var nConsts = NumConsts();
+ int nFuncs = NumFuncs();
+ int nConsts = NumConsts();
int n = nFuncs + nConsts;
FuncDecl[] res = new FuncDecl[n];
for (int i = 0; i < nConsts; i++)
@@ -236,10 +236,10 @@ import com.Microsoft.Z3.Enumerations.*;
ASTVector nUniv = new ASTVector(Context(), Native.modelGetSortUniverse(Context().nCtx(), NativeObject(), s.NativeObject()));
- int n = nUniv.Size;
+ int n = nUniv.Size();
Expr[] res = new Expr[n];
for (int i = 0; i < n; i++)
- res[i] = Expr.Create(Context(), nUniv[i].NativeObject());
+ res[i] = Expr.Create(Context(), nUniv.get(i).NativeObject());
return res;
}
diff --git a/src/api/java/com/Microsoft/Z3/Native.java b/src/api/java/com/Microsoft/Z3/Native.java
index e42d8b7ba..8acf96cbf 100644
--- a/src/api/java/com/Microsoft/Z3/Native.java
+++ b/src/api/java/com/Microsoft/Z3/Native.java
@@ -5,7 +5,7 @@ public final class Native {
public static class LongPtr { public long value; }
public static class StringPtr { public String value; }
public static class errorHandler { public long ptr; }
- static { System.loadLibrary(""); }
+ static { System.loadLibrary(""); }
public static native long mkConfig();
public static native void delConfig(long a0);
public static native void setParamValue(long a0, String a1, String a2);
diff --git a/src/api/java/com/Microsoft/Z3/Params.java b/src/api/java/com/Microsoft/Z3/Params.java
index 1107a80ee..ab6401833 100644
--- a/src/api/java/com/Microsoft/Z3/Params.java
+++ b/src/api/java/com/Microsoft/Z3/Params.java
@@ -26,16 +26,6 @@ import com.Microsoft.Z3.Enumerations.*;
Native.paramsSetBool(Context().nCtx(), NativeObject(), name.NativeObject(), (value) ? true : false);
}
- /**
- * Adds a parameter setting.
- **/
- public void Add(Symbol name, int value)
- {
-
-
- Native.paramsSetInt(Context().nCtx(), NativeObject(), name.NativeObject(), value);
- }
-
/**
* Adds a parameter setting.
**/
@@ -70,7 +60,7 @@ import com.Microsoft.Z3.Enumerations.*;
**/
public void Add(String name, int value)
{
- Native.paramsSetInt(Context().nCtx(), NativeObject(), Context().MkSymbol(name).NativeObject(), value);
+ Native.paramsSetUint(Context().nCtx(), NativeObject(), Context().MkSymbol(name).NativeObject(), value);
}
/**
diff --git a/src/api/java/com/Microsoft/Z3/Quantifier.java b/src/api/java/com/Microsoft/Z3/Quantifier.java
index ad05c544b..b841623c2 100644
--- a/src/api/java/com/Microsoft/Z3/Quantifier.java
+++ b/src/api/java/com/Microsoft/Z3/Quantifier.java
@@ -24,7 +24,7 @@ import com.Microsoft.Z3.Enumerations.*;
/**
* Indicates whether the quantifier is existential.
**/
- public boolean IsExistential() { return !IsUniversal; }
+ public boolean IsExistential() { return !IsUniversal(); }
/**
* The weight of the quantifier.
@@ -137,21 +137,21 @@ import com.Microsoft.Z3.Enumerations.*;
if (noPatterns == null && quantifierID == null && skolemID == null)
{
- NativeObject() = Native.mkQuantifier(ctx.nCtx(), (isForall) ? true : false, weight,
- AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
- AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
- Symbol.ArrayToNative(names),
- body.NativeObject());
+ setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall) ? true : false, 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) ? true : false, 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());
+ setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), (isForall) ? true : false, 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()));
}
}
@@ -171,19 +171,19 @@ import com.Microsoft.Z3.Enumerations.*;
if (noPatterns == null && quantifierID == null && skolemID == null)
{
- NativeObject() = Native.mkQuantifierConst(ctx.nCtx(), (isForall) ? true : false, weight,
- AST.ArrayLength(bound), AST.ArrayToNative(bound),
- AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
- body.NativeObject());
+ setNativeObject(Native.mkQuantifierConst(ctx.nCtx(), (isForall) ? true : false, weight,
+ AST.ArrayLength(bound), AST.ArrayToNative(bound),
+ AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
+ body.NativeObject()));
}
else
{
- NativeObject() = Native.mkQuantifierConstEx(ctx.nCtx(), (isForall) ? true : false, 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());
+ setNativeObject(Native.mkQuantifierConstEx(ctx.nCtx(), (isForall) ? true : false, 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()));
}
}
@@ -192,7 +192,7 @@ import com.Microsoft.Z3.Enumerations.*;
void CheckNativeObject(long obj)
{
- if ((Z3_ast_kind)Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST)
+ if (Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt())
throw new Z3Exception("Underlying object is not a quantifier");
super.CheckNativeObject(obj);
}
diff --git a/src/api/java/com/Microsoft/Z3/RatNum.java b/src/api/java/com/Microsoft/Z3/RatNum.java
index ad0982a95..ff0b3d18a 100644
--- a/src/api/java/com/Microsoft/Z3/RatNum.java
+++ b/src/api/java/com/Microsoft/Z3/RatNum.java
@@ -72,7 +72,7 @@ import com.Microsoft.Z3.Enumerations.*;
return Native.getNumeralString(Context().nCtx(), NativeObject());
}
- RatNum(Context ctx, long obj)
+ RatNum(Context ctx, long obj) throws Z3Exception
{ super(ctx, obj);
}
diff --git a/src/api/java/com/Microsoft/Z3/RealExpr.java b/src/api/java/com/Microsoft/Z3/RealExpr.java
index 2f06e4643..907148c2a 100644
--- a/src/api/java/com/Microsoft/Z3/RealExpr.java
+++ b/src/api/java/com/Microsoft/Z3/RealExpr.java
@@ -19,13 +19,15 @@ import com.Microsoft.Z3.Enumerations.*;
**/
public class RealExpr extends ArithExpr
{
- /** Constructor for RealExpr
- **/
+ /**
+ * Constructor for RealExpr
+ **/
protected RealExpr(Context ctx)
{ super(ctx);
}
- RealExpr(Context ctx, long obj)
+
+ RealExpr(Context ctx, long obj) throws Z3Exception
{ super(ctx, obj);
}
diff --git a/src/api/java/com/Microsoft/Z3/RelationSort.java b/src/api/java/com/Microsoft/Z3/RelationSort.java
index 85f083b57..564c66eaf 100644
--- a/src/api/java/com/Microsoft/Z3/RelationSort.java
+++ b/src/api/java/com/Microsoft/Z3/RelationSort.java
@@ -31,7 +31,7 @@ import com.Microsoft.Z3.Enumerations.*;
if (m_columnSorts != null)
return m_columnSorts;
- int n = Arity;
+ int n = Arity();
Sort[] res = new Sort[n];
for (int i = 0; i < n; i++)
res[i] = Sort.Create(Context(), Native.getRelationColumn(Context().nCtx(), NativeObject(), i));
diff --git a/src/api/java/com/Microsoft/Z3/Solver.java b/src/api/java/com/Microsoft/Z3/Solver.java
index 5fda96bb1..1f6f099b3 100644
--- a/src/api/java/com/Microsoft/Z3/Solver.java
+++ b/src/api/java/com/Microsoft/Z3/Solver.java
@@ -99,7 +99,7 @@ import com.Microsoft.Z3.Enumerations.*;
public int NumAssertions()
{
ASTVector ass = new ASTVector(Context(), Native.solverGetAssertions(Context().nCtx(), NativeObject()));
- return ass.Size;
+ return ass.Size();
}
/**
@@ -110,10 +110,10 @@ import com.Microsoft.Z3.Enumerations.*;
ASTVector ass = new ASTVector(Context(), Native.solverGetAssertions(Context().nCtx(), NativeObject()));
- int n = ass.Size;
+ int n = ass.Size();
BoolExpr[] res = new BoolExpr[n];
for (int i = 0; i < n; i++)
- res[i] = new BoolExpr(Context(), ass[i].NativeObject());
+ res[i] = new BoolExpr(Context(), ass.get(i).NativeObject());
return res;
}
@@ -185,10 +185,10 @@ import com.Microsoft.Z3.Enumerations.*;
ASTVector core = new ASTVector(Context(), Native.solverGetUnsatCore(Context().nCtx(), NativeObject()));
- int n = core.Size;
+ int n = core.Size();
Expr[] res = new Expr[n];
for (int i = 0; i < n; i++)
- res[i] = Expr.Create(Context(), core[i].NativeObject());
+ res[i] = Expr.Create(Context(), core.get(i).NativeObject());
return res;
}
diff --git a/src/api/java/com/Microsoft/Z3/Statistics.java b/src/api/java/com/Microsoft/Z3/Statistics.java
index ec64ee0b3..93cd6e706 100644
--- a/src/api/java/com/Microsoft/Z3/Statistics.java
+++ b/src/api/java/com/Microsoft/Z3/Statistics.java
@@ -25,6 +25,8 @@ import com.Microsoft.Z3.Enumerations.*;
/**
* The key of the entry.
**/
+ public String Key;
+
/**
* The uint-value of the entry.
**/
@@ -49,10 +51,10 @@ import com.Microsoft.Z3.Enumerations.*;
{
- if (IsUInt)
- return m_int.toString();
- else if (IsDouble)
- return m_double.toString();
+ if (IsUInt())
+ return Integer.toString(m_int);
+ else if (IsDouble())
+ return Double.toString(m_double);
else
throw new Z3Exception("Unknown statistical entry type");
}
@@ -62,7 +64,7 @@ import com.Microsoft.Z3.Enumerations.*;
**/
public String toString()
{
- return Key + ": " + Value;
+ return Key + ": " + Value();
}
private boolean m_is_int = false;
@@ -71,13 +73,13 @@ import com.Microsoft.Z3.Enumerations.*;
private double m_double = 0.0;
Entry(String k, int v)
{
- Key = k;
+ Key = k;
m_is_int = true;
m_int = v;
}
Entry(String k, double v)
{
- Key = k;
+ Key = k;
m_is_double = true;
m_double = v;
}
@@ -105,14 +107,14 @@ import com.Microsoft.Z3.Enumerations.*;
- int n = Size;
+ int n = Size();
Entry[] res = new Entry[n];
for (int i = 0; i < n; i++)
{
Entry e;
String k = Native.statsGetKey(Context().nCtx(), NativeObject(), i);
- if (Native.statsIsInt(Context().nCtx(), NativeObject(), i) )
- e = new Entry(k, Native.statsGetIntValue(Context().nCtx(), NativeObject(), i));
+ if (Native.statsIsUint(Context().nCtx(), NativeObject(), i) )
+ e = new Entry(k, Native.statsGetUintValue(Context().nCtx(), NativeObject(), i));
else if (Native.statsIsDouble(Context().nCtx(), NativeObject(), i) )
e = new Entry(k, Native.statsGetDoubleValue(Context().nCtx(), NativeObject(), i));
else
@@ -129,7 +131,7 @@ import com.Microsoft.Z3.Enumerations.*;
{
- int n = Size;
+ int n = Size();
String[] res = new String[n];
for (int i = 0; i < n; i++)
res[i] = Native.statsGetKey(Context().nCtx(), NativeObject(), i);
@@ -142,8 +144,8 @@ import com.Microsoft.Z3.Enumerations.*;
**/
public Entry get(String key)
{
- int n = Size;
- Entry[] es = Entries;
+ int n = Size();
+ Entry[] es = Entries();
for (int i = 0; i < n; i++)
if (es[i].Key == key)
return es[i];
diff --git a/src/api/java/com/Microsoft/Z3/Status.java b/src/api/java/com/Microsoft/Z3/Status.java
index 64bd9f767..fdccb7376 100644
--- a/src/api/java/com/Microsoft/Z3/Status.java
+++ b/src/api/java/com/Microsoft/Z3/Status.java
@@ -14,21 +14,29 @@ import com.Microsoft.Z3.Enumerations.*;
/**
* Status values.
**/
- public class Status
+ public enum Status
{
- ///
/// Used to signify an unsatisfiable status.
- ///
-public static final int UNSATISFIABLE = 1;
+ UNSATISFIABLE (1),
- ///
/// Used to signify an unknown status.
- ///
-public static final int UNKNOWN = 0;
+ UNKNOWN (0),
- ///
/// Used to signify a satisfiable status.
- ///
-public static final int SATISFIABLE = 1;
+ SATISFIABLE (1);
+
+ private final int intValue;
+
+ Status (int v) {
+ this.intValue = v;
+ }
+
+ public static final Status fromInt(int v) {
+ for (Status k: values())
+ if (k.intValue == v) return k;
+ return values()[0];
+ }
+
+ public final int toInt() { return this.intValue; }
}
diff --git a/src/api/java/com/Microsoft/Z3/StringSymbol.java b/src/api/java/com/Microsoft/Z3/StringSymbol.java
index 1ff869002..5788c0944 100644
--- a/src/api/java/com/Microsoft/Z3/StringSymbol.java
+++ b/src/api/java/com/Microsoft/Z3/StringSymbol.java
@@ -43,7 +43,7 @@ import com.Microsoft.Z3.Enumerations.*;
void CheckNativeObject(long obj)
{
- if ((Z3_symbol_kind)Native.getSymbolKind(Context().nCtx(), obj) != Z3_symbol_kind.Z3_STRING_SYMBOL)
+ if (Native.getSymbolKind(Context().nCtx(), obj) != Z3_symbol_kind.Z3_STRING_SYMBOL.toInt())
throw new Z3Exception("Symbol is not of String kind");
super.CheckNativeObject(obj);
diff --git a/src/api/java/com/Microsoft/Z3/Symbol.java b/src/api/java/com/Microsoft/Z3/Symbol.java
index b7653414d..0cd0632de 100644
--- a/src/api/java/com/Microsoft/Z3/Symbol.java
+++ b/src/api/java/com/Microsoft/Z3/Symbol.java
@@ -27,7 +27,7 @@ import com.Microsoft.Z3.Enumerations.*;
**/
public boolean IsIntSymbol()
{
- return Kind == Z3_symbol_kind.Z3_INT_SYMBOL;
+ return Kind() == Z3_symbol_kind.Z3_INT_SYMBOL;
}
/**
@@ -35,7 +35,7 @@ import com.Microsoft.Z3.Enumerations.*;
**/
public boolean IsStringSymbol()
{
- return Kind == Z3_symbol_kind.Z3_STRING_SYMBOL;
+ return Kind() == Z3_symbol_kind.Z3_STRING_SYMBOL;
}
/**
@@ -44,9 +44,9 @@ import com.Microsoft.Z3.Enumerations.*;
public String toString()
{
if (IsIntSymbol())
- return ((IntSymbol)this).Int.toString();
+ return Integer.toString(((IntSymbol)this).Int());
else if (IsStringSymbol())
- return ((StringSymbol)this).String;
+ return ((StringSymbol)this).String();
else
throw new Z3Exception("Unknown symbol kind encountered");
}
@@ -54,8 +54,8 @@ import com.Microsoft.Z3.Enumerations.*;
/**
* Symbol constructor
**/
- protected Symbol(Context ctx, long obj) { super(ctx, obj);
-
+ protected Symbol(Context ctx, long obj) {
+ super(ctx, obj);
}
static Symbol Create(Context ctx, long obj)
diff --git a/src/api/java/com/Microsoft/Z3/Tactic.java b/src/api/java/com/Microsoft/Z3/Tactic.java
index fd560847a..3ef1ab645 100644
--- a/src/api/java/com/Microsoft/Z3/Tactic.java
+++ b/src/api/java/com/Microsoft/Z3/Tactic.java
@@ -62,7 +62,7 @@ import com.Microsoft.Z3.Enumerations.*;
- return Apply(g);
+ return Apply(g, null);
}
/**
diff --git a/src/api/java/com/Microsoft/Z3/TupleSort.java b/src/api/java/com/Microsoft/Z3/TupleSort.java
index 0ac03bb88..76a92f6c9 100644
--- a/src/api/java/com/Microsoft/Z3/TupleSort.java
+++ b/src/api/java/com/Microsoft/Z3/TupleSort.java
@@ -51,8 +51,8 @@ import com.Microsoft.Z3.Enumerations.*;
long t = 0;
- NativeObject() = Native.mkTupleSort(ctx.nCtx(), name.NativeObject(), numFields,
- Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
- t, new long[numFields]);
+ setNativeObject(Native.mkTupleSort(ctx.nCtx(), name.NativeObject(), numFields,
+ Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
+ t, new long[numFields]));
}
};
diff --git a/src/api/java/com/Microsoft/Z3/Version.java b/src/api/java/com/Microsoft/Z3/Version.java
index c3fc4268d..e9f883aaa 100644
--- a/src/api/java/com/Microsoft/Z3/Version.java
+++ b/src/api/java/com/Microsoft/Z3/Version.java
@@ -68,6 +68,6 @@ import com.Microsoft.Z3.Enumerations.*;
int major = 0, minor = 0, build = 0, revision = 0;
Native.getVersion(major, minor, build, revision);
- return major.toString() + "." + minor.toString() + "." + build.toString() + "." + revision.toString();
+ return Integer.toString(major) + "." + Integer.toString(minor) + "." + Integer.toString(build) + "." + Integer.toString(revision);
}
}
diff --git a/src/api/java/com/Microsoft/Z3/Z3Object.java b/src/api/java/com/Microsoft/Z3/Z3Object.java
index d4bdf08f7..1bbdbab8b 100644
--- a/src/api/java/com/Microsoft/Z3/Z3Object.java
+++ b/src/api/java/com/Microsoft/Z3/Z3Object.java
@@ -20,7 +20,7 @@ import com.Microsoft.Z3.Enumerations.*;
/**
* Finalizer.
**/
- protected void finalize()
+ protected void finalize() throws Z3Exception
{
Dispose();
}
@@ -28,7 +28,7 @@ import com.Microsoft.Z3.Enumerations.*;
/**
* Disposes of the underlying native Z3 object.
**/
- public void Dispose()
+ public void Dispose() throws Z3Exception
{
if (m_n_obj != 0)
{
@@ -65,7 +65,7 @@ import com.Microsoft.Z3.Enumerations.*;
m_ctx = ctx;
}
- Z3Object(Context ctx, long obj)
+ Z3Object(Context ctx, long obj) throws Z3Exception
{
@@ -75,13 +75,13 @@ import com.Microsoft.Z3.Enumerations.*;
m_n_obj = obj;
}
- void IncRef(long o) { }
- void DecRef(long o) { }
+ void IncRef(long o) throws Z3Exception { }
+ void DecRef(long o) throws Z3Exception { }
- void CheckNativeObject(long obj) { }
+ void CheckNativeObject(long obj) throws Z3Exception { }
- long NativeObject() { return m_n_obj; }
- void setNativeObject(long value)
+ long NativeObject() { return m_n_obj; }
+ void setNativeObject(long value) throws Z3Exception
{
if (value != 0) { CheckNativeObject(value); IncRef(value); }
if (m_n_obj != 0) { DecRef(m_n_obj); }
diff --git a/src/api/java/mk_java.py b/src/api/java/mk_java.py
index fe7f50a25..1c59fc957 100644
--- a/src/api/java/mk_java.py
+++ b/src/api/java/mk_java.py
@@ -163,11 +163,11 @@ def translate(filename):
tgt.write(t + " **/\n")
in_javadoc = 0
- for i in range(0, len(EXCLUDE_METHODS)):
- if filename == EXCLUDE_METHODS[i][0] and s.startswith(EXCLUDE_METHODS[i][1]):
- tgt.write(t + "/* Not translated because it would translate to a function with clashing types. */\n")
- in_unsupported = 1
- break
+ # for i in range(0, len(EXCLUDE_METHODS)):
+ # if filename == EXCLUDE_METHODS[i][0] and s.startswith(EXCLUDE_METHODS[i][1]):
+ # tgt.write(t + "/* Not translated because it would translate to a function with clashing types. */\n")
+ # in_unsupported = 1
+ # break
if in_unsupported: