mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

Java API: Build system and Refactoring.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2012-11-27 00:39:23 +00:00
parent 8c32f6b015
commit 1e8b45e653
46 changed files with 218 additions and 283 deletions
Download patch file Download diff file Expand all files Collapse all files

33
scripts/mk_util.py
View file

@ -493,6 +493,9 @@ def get_c_files(path):
def get_cs_files(path): def get_cs_files(path):
return filter(lambda f: f.endswith('.cs'), os.listdir(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): def find_all_deps(name, deps):
new_deps = [] new_deps = []
for dep in deps: for dep in deps:
@ -932,19 +935,21 @@ class JavaDLLComponent(Component):
def mk_makefile(self, out): def mk_makefile(self, out):
if is_java_enabled(): if is_java_enabled():
dllfile = '%s$(SO_EXT)' % self.dll_name 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)) subdir = self.package_name.replace(".","/")
if IS_WINDOWS: out.write('libz3java$(SO_EXT): libz3$(SO_EXT) ../src/api/java/Native.cpp\n')
out.write('\tcd %s && %s Z3Native.java\n' % (unix_path2dos(self.to_src_dir), JAVAC)) 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('\tmove %s\\*.class .\n' % unix_path2dos(self.to_src_dir)) out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) Native$(OBJ_EXT) libz3.lib\n')
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('%s.jar: libz3java$(SO_EXT) ' % self.package_name)
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) Z3Native$(OBJ_EXT) libz3.lib\n' % dllfile) # for java_file in get_java_files(self.src_dir):
else: # out.write('%s ' % java_file)
out.write('\tcd %s; %s Z3Native.java\n' % (self.to_src_dir, JAVAC)) # for java_file in get_java_files((self.src_dir + "/%s/Enumerations") % subdir):
out.write('\tmv %s/*.class .\n' % self.to_src_dir) # out.write('%s ' % java_file)
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('\n')
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) -L. Z3Native$(OBJ_EXT) -lz3\n' % dllfile) src_wsub = self.to_src_dir + "/" + subdir;
out.write('%s: %s\n\n' % (self.name, dllfile)) out.write(('\tjavac %s/Enumerations/*.java -d api/java\n' % (src_wsub)).replace("/","\\"))
# TODO: Compile and package all the .class files. 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): def main_component(self):
return is_java_enabled() return is_java_enabled()
@ -1847,7 +1852,7 @@ def mk_z3consts_java(api_files):
if name not in DeprecatedEnums: if name not in DeprecatedEnums:
efile = open('%s/%s.java' % (gendir, name), 'w') efile = open('%s/%s.java' % (gendir, name), 'w')
efile.write('/**\n * Automatically generated file\n **/\n\n') 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('/**\n')
efile.write(' * %s\n' % name) efile.write(' * %s\n' % name)

2
scripts/update_api.py
View file

@ -501,7 +501,7 @@ def mk_java():
except: except:
pass # OK if it exists already. pass # OK if it exists already.
java_nativef = '%s/com/Microsoft/Z3/Native.java' % java_dir 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 = open(java_nativef, 'w')
java_native.write('// Automatically generated file\n') java_native.write('// Automatically generated file\n')
java_native.write('package com.Microsoft.Z3;\n') java_native.write('package com.Microsoft.Z3;\n')

0
src/api/java/com/Microsoft/Z3/Native.c → src/api/java/Native.cpp
View file

10
src/api/java/com/Microsoft/Z3/AST.java
View file

@ -87,7 +87,7 @@ import com.Microsoft.Z3.Enumerations.*;
* <param name="ctx">A context</param> * <param name="ctx">A context</param>
* @return A copy of the AST which is associated with <paramref name="ctx"/> * @return A copy of the AST which is associated with <paramref name="ctx"/>
**/ **/
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) { super(ctx); { }}
AST(Context ctx, long obj) { super(ctx, obj); { }} AST(Context ctx, long obj) throws Z3Exception { super(ctx, obj); { }}
class DecRefQueue extends IDecRefQueue 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()"); // Console.WriteLine("AST IncRef()");
if (Context() == null) if (Context() == null)
@ -183,7 +183,7 @@ import com.Microsoft.Z3.Enumerations.*;
super.IncRef(o); super.IncRef(o);
} }
void DecRef(long o) void DecRef(long o) throws Z3Exception
{ {
// Console.WriteLine("AST DecRef()"); // Console.WriteLine("AST DecRef()");
if (Context() == null) if (Context() == null)
@ -194,7 +194,7 @@ import com.Microsoft.Z3.Enumerations.*;
super.DecRef(o); super.DecRef(o);
} }
static AST Create(Context ctx, long obj) static AST Create(Context ctx, long obj) throws Z3Exception
{ {

8
src/api/java/com/Microsoft/Z3/AlgebraicNum.java
View file

@ -24,7 +24,7 @@ import com.Microsoft.Z3.Enumerations.*;
* <param name="precision">the precision of the result</param> * <param name="precision">the precision of the result</param>
* @return A numeral Expr of sort Real * @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.*;
* <param name="precision"></param> * <param name="precision"></param>
* @return A numeral Expr of sort Real * @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. * Returns a string representation in decimal notation.
* <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks> * <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>
**/ **/
public String ToDecimal(int precision) public String ToDecimal(int precision) throws Z3Exception
{ {
return Native.getNumeralDecimalString(Context().nCtx(), NativeObject(), precision); return Native.getNumeralDecimalString(Context().nCtx(), NativeObject(), precision);
} }
AlgebraicNum(Context ctx, long obj) AlgebraicNum(Context ctx, long obj) throws Z3Exception
{ super(ctx, obj); { super(ctx, obj);
} }

2
src/api/java/com/Microsoft/Z3/ArithExpr.java
View file

@ -25,7 +25,7 @@ import com.Microsoft.Z3.Enumerations.*;
{ super(ctx); { super(ctx);
} }
ArithExpr(Context ctx, long obj) ArithExpr(Context ctx, long obj) throws Z3Exception
{ super(ctx, obj); { super(ctx, obj);
} }

2
src/api/java/com/Microsoft/Z3/BitVecExpr.java
View file

@ -23,7 +23,7 @@ import com.Microsoft.Z3.Enumerations.*;
/** /**
* The size of the sort of a bit-vector term. * 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 </summary> /** Constructor for BitVecExpr </summary>
**/ **/

10
src/api/java/com/Microsoft/Z3/Constructor.java
View file

@ -92,11 +92,11 @@ import com.Microsoft.Z3.Enumerations.*;
if (sortRefs == null) sortRefs = new int[n]; if (sortRefs == null) sortRefs = new int[n];
NativeObject() = Native.mkConstructor(ctx.nCtx(), name.NativeObject(), recognizer.NativeObject(), setNativeObject(Native.mkConstructor(ctx.nCtx(), name.NativeObject(), recognizer.NativeObject(),
n, n,
Symbol.ArrayToNative(fieldNames), Symbol.ArrayToNative(fieldNames),
Sort.ArrayToNative(sorts), Sort.ArrayToNative(sorts),
sortRefs); sortRefs));
} }

104
src/api/java/com/Microsoft/Z3/Context.java
View file

@ -42,6 +42,12 @@ import com.Microsoft.Z3.Enumerations.*;
InitContext(); InitContext();
} }
private Context(long ctx)
{
super();
this.m_ctx = ctx;
}
/** /**
* Creates a new symbol using an integer. * Creates a new symbol using an integer.
* <remarks> * <remarks>
@ -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())); 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 <code>MakeNumeral</code> since it is not necessary to parse a string.
* <param name="v">Value of the numeral</param>
* <param name="ty">Sort of the numeral</param>
* @return A Term with value <paramref name="v"/> and type <paramref name="ty"/>
**/
/* 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. * 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 <code>MakeNumeral</code> since it is not necessary to parse a string. * It is slightly faster than <code>MakeNumeral</code> 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())); 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 <code>MakeNumeral</code> since it is not necessary to parse a string.
* <param name="v">Value of the numeral</param>
* <param name="ty">Sort of the numeral</param>
* @return A Term with value <paramref name="v"/> and type <paramref name="ty"/>
**/
/* Not translated because it would translate to a function with clashing types. */
/** /**
* Create a real from a fraction. * Create a real from a fraction.
* <param name="num">numerator of rational.</param> * <param name="num">numerator of rational.</param>
@ -2281,13 +2269,6 @@ import com.Microsoft.Z3.Enumerations.*;
return new RatNum(this, Native.mkInt(nCtx(), v, RealSort().NativeObject())); return new RatNum(this, Native.mkInt(nCtx(), v, RealSort().NativeObject()));
} }
/**
* Create a real numeral.
* <param name="v">value of the numeral.</param>
* @return A Term with value <paramref name="v"/> and sort Real
**/
/* Not translated because it would translate to a function with clashing types. */
/** /**
* Create a real numeral. * Create a real numeral.
* <param name="v">value of the numeral.</param> * <param name="v">value of the numeral.</param>
@ -2300,13 +2281,6 @@ import com.Microsoft.Z3.Enumerations.*;
return new RatNum(this, Native.mkInt64(nCtx(), v, RealSort().NativeObject())); return new RatNum(this, Native.mkInt64(nCtx(), v, RealSort().NativeObject()));
} }
/**
* Create a real numeral.
* <param name="v">value of the numeral.</param>
* @return A Term with value <paramref name="v"/> and sort Real
**/
/* Not translated because it would translate to a function with clashing types. */
/** /**
* Create an integer numeral. * Create an integer numeral.
* <param name="v">A string representing the Term value in decimal notation.</param> * <param name="v">A string representing the Term value in decimal notation.</param>
@ -2330,13 +2304,6 @@ import com.Microsoft.Z3.Enumerations.*;
return new IntNum(this, Native.mkInt(nCtx(), v, IntSort().NativeObject())); return new IntNum(this, Native.mkInt(nCtx(), v, IntSort().NativeObject()));
} }
/**
* Create an integer numeral.
* <param name="v">value of the numeral.</param>
* @return A Term with value <paramref name="v"/> and sort Integer
**/
/* Not translated because it would translate to a function with clashing types. */
/** /**
* Create an integer numeral. * Create an integer numeral.
* <param name="v">value of the numeral.</param> * <param name="v">value of the numeral.</param>
@ -2349,13 +2316,6 @@ import com.Microsoft.Z3.Enumerations.*;
return new IntNum(this, Native.mkInt64(nCtx(), v, IntSort().NativeObject())); return new IntNum(this, Native.mkInt64(nCtx(), v, IntSort().NativeObject()));
} }
/**
* Create an integer numeral.
* <param name="v">value of the numeral.</param>
* @return A Term with value <paramref name="v"/> and sort Integer
**/
/* Not translated because it would translate to a function with clashing types. */
/** /**
* Create a bit-vector numeral. * Create a bit-vector numeral.
* <param name="v">A string representing the value in decimal notation.</param> * <param name="v">A string representing the value in decimal notation.</param>
@ -2380,13 +2340,6 @@ import com.Microsoft.Z3.Enumerations.*;
return (BitVecNum)MkNumeral(v, MkBitVecSort(size)); return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
} }
/**
* Create a bit-vector numeral.
* <param name="v">value of the numeral.</param>
* <param name="size">the size of the bit-vector</param>
**/
/* Not translated because it would translate to a function with clashing types. */
/** /**
* Create a bit-vector numeral. * Create a bit-vector numeral.
* <param name="v">value of the numeral.</param> * <param name="v">value of the numeral.</param>
@ -2399,13 +2352,6 @@ import com.Microsoft.Z3.Enumerations.*;
return (BitVecNum)MkNumeral(v, MkBitVecSort(size)); return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
} }
/**
* Create a bit-vector numeral.
* <param name="v">value of the numeral.</param>
* <param name="size">the size of the bit-vector</param>
**/
/* Not translated because it would translate to a function with clashing types. */
/** /**
* Create a universal Quantifier. * Create a universal Quantifier.
@ -2551,7 +2497,7 @@ import com.Microsoft.Z3.Enumerations.*;
* <seealso cref="FuncDecl.ToString()"/> * <seealso cref="FuncDecl.ToString()"/>
* <seealso cref="Sort.ToString()"/> * <seealso cref="Sort.ToString()"/>
**/ **/
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. * Convert a benchmark into an SMT-LIB formatted string.
@ -3356,12 +3302,12 @@ import com.Microsoft.Z3.Enumerations.*;
**/ **/
public String GetParamValue(String id) public String GetParamValue(String id)
{ {
long res = 0; String res = new String();
int r = Native.getParamValue(nCtx(), id, res); boolean r = Native.getParamValue(nCtx(), id, res);
if (r == Z3_lbool.Z3_L_FALSE.toInt()) if (!r)
return null; return null;
else else
return Marshal.PtrToStringAnsi(res); return res;
} }
@ -3376,7 +3322,7 @@ import com.Microsoft.Z3.Enumerations.*;
void InitContext() 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. m_n_err_handler = new Native.errorHandler(NativeErrorHandler); // keep reference so it doesn't get collected.
Native.setErrorHandler(m_ctx, m_n_err_handler); 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"); throw new Z3Exception("Context mismatch");
} }
@ -3402,25 +3348,6 @@ import com.Microsoft.Z3.Enumerations.*;
CheckContextMatch(a); CheckContextMatch(a);
} }
} }
}
private void ObjectInvariant()
{
} }
private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue(); private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue();
@ -3473,7 +3400,8 @@ import com.Microsoft.Z3.Enumerations.*;
m_ctx = 0; m_ctx = 0;
} }
else else
GC.ReRegisterForFinalize(this); /* re-queue the finalizer */
new Context(m_ctx);
} }
/** /**

2
src/api/java/com/Microsoft/Z3/DatatypeSort.java
View file

@ -61,7 +61,7 @@ import com.Microsoft.Z3.Enumerations.*;
for (int i = 0; i < n; i++) for (int i = 0; i < n; i++)
{ {
FuncDecl fd = new FuncDecl(Context(), Native.getDatatypeSortConstructor(Context().nCtx(), NativeObject(), 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]; FuncDecl[] tmp = new FuncDecl[ds];
for (int j = 0; j < ds; j++) for (int j = 0; j < ds; j++)
tmp[j] = new FuncDecl(Context(), Native.getDatatypeSortConstructorAccessor(Context().nCtx(), NativeObject(), i, j)); tmp[j] = new FuncDecl(Context(), Native.getDatatypeSortConstructorAccessor(Context().nCtx(), NativeObject(), i, j));

6
src/api/java/com/Microsoft/Z3/EnumSort.java
View file

@ -68,8 +68,8 @@ import com.Microsoft.Z3.Enumerations.*;
int n = enumNames.length; int n = enumNames.length;
long[] n_constdecls = new long[n]; long[] n_constdecls = new long[n];
long[] n_testers = new long[n]; long[] n_testers = new long[n];
NativeObject() = Native.mkEnumerationSort(ctx.nCtx(), name.NativeObject(), (int)n, setNativeObject(Native.mkEnumerationSort(ctx.nCtx(), name.NativeObject(), (int)n,
Symbol.ArrayToNative(enumNames), n_constdecls, n_testers); Symbol.ArrayToNative(enumNames), n_constdecls, n_testers));
_constdecls = new FuncDecl[n]; _constdecls = new FuncDecl[n];
for (int i = 0; i < n; i++) for (int i = 0; i < n; i++)
_constdecls[i] = new FuncDecl(ctx, n_constdecls[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]); _testerdecls[i] = new FuncDecl(ctx, n_testers[i]);
_consts = new Expr[n]; _consts = new Expr[n];
for (int i = 0; i < n; i++) for (int i = 0; i < n; i++)
_consts[i] = ctx.MkApp(_constdecls[i]); _consts[i] = ctx.MkApp(_constdecls[i], null);
} }
}; };

2
src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java
View file

@ -2,7 +2,7 @@
* Automatically generated file * Automatically generated file
**/ **/
package com.Microsoft.Z3; package com.Microsoft.Z3.Enumerations;
/** /**
* Z3_ast_kind * Z3_ast_kind

2
src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java
View file

@ -2,7 +2,7 @@
* Automatically generated file * Automatically generated file
**/ **/
package com.Microsoft.Z3; package com.Microsoft.Z3.Enumerations;
/** /**
* Z3_ast_print_mode * Z3_ast_print_mode

2
src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java
View file

@ -2,7 +2,7 @@
* Automatically generated file * Automatically generated file
**/ **/
package com.Microsoft.Z3; package com.Microsoft.Z3.Enumerations;
/** /**
* Z3_decl_kind * Z3_decl_kind

2
src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java
View file

@ -2,7 +2,7 @@
* Automatically generated file * Automatically generated file
**/ **/
package com.Microsoft.Z3; package com.Microsoft.Z3.Enumerations;
/** /**
* Z3_error_code * Z3_error_code

2
src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java
View file

@ -2,7 +2,7 @@
* Automatically generated file * Automatically generated file
**/ **/
package com.Microsoft.Z3; package com.Microsoft.Z3.Enumerations;
/** /**
* Z3_goal_prec * Z3_goal_prec

2
src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java
View file

@ -2,7 +2,7 @@
* Automatically generated file * Automatically generated file
**/ **/
package com.Microsoft.Z3; package com.Microsoft.Z3.Enumerations;
/** /**
* Z3_lbool * Z3_lbool

2
src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java
View file

@ -2,7 +2,7 @@
* Automatically generated file * Automatically generated file
**/ **/
package com.Microsoft.Z3; package com.Microsoft.Z3.Enumerations;
/** /**
* Z3_param_kind * Z3_param_kind

2
src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java
View file

@ -2,7 +2,7 @@
* Automatically generated file * Automatically generated file
**/ **/
package com.Microsoft.Z3; package com.Microsoft.Z3.Enumerations;
/** /**
* Z3_parameter_kind * Z3_parameter_kind

2
src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java
View file

@ -2,7 +2,7 @@
* Automatically generated file * Automatically generated file
**/ **/
package com.Microsoft.Z3; package com.Microsoft.Z3.Enumerations;
/** /**
* Z3_sort_kind * Z3_sort_kind

2
src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java
View file

@ -2,7 +2,7 @@
* Automatically generated file * Automatically generated file
**/ **/
package com.Microsoft.Z3; package com.Microsoft.Z3.Enumerations;
/** /**
* Z3_symbol_kind * Z3_symbol_kind

24
src/api/java/com/Microsoft/Z3/Expr.java
View file

@ -21,7 +21,7 @@ import com.Microsoft.Z3.Enumerations.*;
* <param name="p">A set of parameters to configure the simplifier</param> * <param name="p">A set of parameters to configure the simplifier</param>
* <seealso cref="Context.SimplifyHelp"/> * <seealso cref="Context.SimplifyHelp"/>
**/ **/
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. * 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 <paramref name="args"/> * 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. * 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 <code>from[i]</code> must be equal to sort of <code>to[i]</code>. * sort of <code>from[i]</code> must be equal to sort of <code>to[i]</code>.
* </remarks> * </remarks>
**/ **/
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 <code>from</code> in the expression with <code>to</code>. * Substitute every occurrence of <code>from</code> in the expression with <code>to</code>.
* <seealso cref="Substitute(Expr[],Expr[])"/> * <seealso cref="Substitute(Expr[],Expr[])"/>
**/ **/
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 <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>. * 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> * </remarks>
**/ **/
public Expr SubstituteVars(Expr[] to) public Expr SubstituteVars(Expr[] to) throws Z3Exception
{ {
@ -137,7 +137,7 @@ import com.Microsoft.Z3.Enumerations.*;
* <param name="ctx">A context</param> * <param name="ctx">A context</param>
* @return A copy of the term which is associated with <paramref name="ctx"/> * @return A copy of the term which is associated with <paramref name="ctx"/>
**/ **/
public Expr Translate(Context ctx) public Expr Translate(Context ctx) throws Z3Exception
{ {
@ -1367,7 +1367,7 @@ import com.Microsoft.Z3.Enumerations.*;
* index. * index.
* </remarks> * </remarks>
**/ **/
public int Index() public int Index() throws Z3Exception
{ {
if (!IsVar()) if (!IsVar())
throw new Z3Exception("Term is not a bound variable."); throw new Z3Exception("Term is not a bound variable.");
@ -1384,9 +1384,9 @@ import com.Microsoft.Z3.Enumerations.*;
/** /**
* Constructor for Expr * 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 && if (Native.isApp(Context().nCtx(), obj) ^ true &&
Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() && Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() &&
@ -1395,7 +1395,7 @@ import com.Microsoft.Z3.Enumerations.*;
super.CheckNativeObject(obj); 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); return Create(ctx, obj);
} }
static Expr Create(Context ctx, long obj) static Expr Create(Context ctx, long obj) throws Z3Exception
{ {

12
src/api/java/com/Microsoft/Z3/Fixedpoint.java
View file

@ -123,8 +123,8 @@ import com.Microsoft.Z3.Enumerations.*;
Context().CheckContextMatch(relations); Context().CheckContextMatch(relations);
Z3_lbool r = (Z3_lbool)Native.fixedpointQueryRelations(Context().nCtx(), NativeObject(), Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQueryRelations(Context().nCtx(), NativeObject(),
AST.ArrayLength(relations), AST.ArrayToNative(relations)); AST.ArrayLength(relations), AST.ArrayToNative(relations)));
switch (r) switch (r)
{ {
case Z3_L_TRUE: return Status.SATISFIABLE; 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())); ASTVector v = new ASTVector(Context(), Native.fixedpointGetRules(Context().nCtx(), NativeObject()));
int n = v.Size; int n = v.Size();
BoolExpr[] res = new BoolExpr[n]; BoolExpr[] res = new BoolExpr[n];
for (int i = 0; i < n; i++) 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; return res;
} }
@ -263,10 +263,10 @@ import com.Microsoft.Z3.Enumerations.*;
ASTVector v = new ASTVector(Context(), Native.fixedpointGetAssertions(Context().nCtx(), NativeObject())); ASTVector v = new ASTVector(Context(), Native.fixedpointGetAssertions(Context().nCtx(), NativeObject()));
int n = v.Size; int n = v.Size();
BoolExpr[] res = new BoolExpr[n]; BoolExpr[] res = new BoolExpr[n];
for (int i = 0; i < n; i++) 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; return res;
} }

16
src/api/java/com/Microsoft/Z3/FuncDecl.java
View file

@ -77,7 +77,7 @@ import com.Microsoft.Z3.Enumerations.*;
{ {
var n = DomainSize; int n = DomainSize();
Sort[] res = new Sort[n]; Sort[] res = new Sort[n];
for (int i = 0; i < n; i++) for (int i = 0; i < n; i++)
@ -171,25 +171,25 @@ import com.Microsoft.Z3.Enumerations.*;
/**The int value of the parameter.</summary> /**The int value of the parameter.</summary>
**/ **/
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.</summary> /**The double value of the parameter.</summary>
**/ **/
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.</summary> /**The Symbol value of the parameter.</summary>
**/ **/
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.</summary> /**The Sort value of the parameter.</summary>
**/ **/
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.</summary> /**The AST value of the parameter.</summary>
**/ **/
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.</summary> /**The FunctionDeclaration value of the parameter.</summary>
**/ **/
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.</summary> /**The rational string value of the parameter.</summary>
**/ **/
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. * The kind of the parameter.

14
src/api/java/com/Microsoft/Z3/FuncInterp.java
View file

@ -59,10 +59,10 @@ import com.Microsoft.Z3.Enumerations.*;
{ {
int n = NumArgs(); int n = NumArgs();
String res = "["; String res = "[";
Expr[] args = Args; Expr[] args = Args();
for (int i = 0; i < n; i++) for (int i = 0; i < n; i++)
res += args[i] + ", "; res += args[i] + ", ";
return res + Value + "]"; return res + Value() + "]";
} }
Entry(Context ctx, long obj) { super(ctx, obj); { }} Entry(Context ctx, long obj) { super(ctx, obj); { }}
@ -135,20 +135,20 @@ import com.Microsoft.Z3.Enumerations.*;
{ {
String res = ""; String res = "";
res += "["; res += "[";
for (Entry e: Entries) for (Entry e: Entries())
{ {
int n = e.NumArgs; int n = e.NumArgs();
if (n > 1) res += "["; if (n > 1) res += "[";
Expr[] args = e.Args; Expr[] args = e.Args();
for (int i = 0; i < n; i++) for (int i = 0; i < n; i++)
{ {
if (i != 0) res += ", "; if (i != 0) res += ", ";
res += args[i]; res += args[i];
} }
if (n > 1) res += "]"; if (n > 1) res += "]";
res += " -> " + e.Value + ", "; res += " -> " + e.Value() + ", ";
} }
res += "else -> " + Else; res += "else -> " + Else();
res += "]"; res += "]";
return res; return res;
} }

24
src/api/java/com/Microsoft/Z3/Goal.java
View file

@ -31,21 +31,21 @@ import com.Microsoft.Z3.Enumerations.*;
/** /**
* Indicates whether the goal is precise. * 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. * 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. * 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). * 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 <paramref name="constraints"/> to the given goal. * Adds the <paramref name="constraints"/> to the given goal.
@ -96,7 +96,7 @@ import com.Microsoft.Z3.Enumerations.*;
{ {
int n = Size; int n = Size();
BoolExpr[] res = new BoolExpr[n]; BoolExpr[] res = new BoolExpr[n];
for (int i = 0; i < n; i++) for (int i = 0; i < n; i++)
res[i] = new BoolExpr(Context(), Native.goalFormula(Context().nCtx(), NativeObject(), i)); res[i] = new BoolExpr(Context(), Native.goalFormula(Context().nCtx(), NativeObject(), i));
@ -132,15 +132,15 @@ import com.Microsoft.Z3.Enumerations.*;
* Simplifies the goal. * Simplifies the goal.
* <remarks>Essentially invokes the `simplify' tactic on the goal.</remarks> * <remarks>Essentially invokes the `simplify' tactic on the goal.</remarks>
**/ **/
public Goal Simplify(Params p) public Goal Simplify(Params p) throws Z3Exception
{ {
Tactic t = Context().MkTactic("simplify"); Tactic t = Context().MkTactic("simplify");
ApplyResult res = t.Apply(this, p); ApplyResult res = t.Apply(this, p);
if (res.NumSubgoals == 0) if (res.NumSubgoals() == 0)
return Context().MkGoal(); throw new Z3Exception("No subgoals");
else else
return res.Subgoals[0]; return res.Subgoals()[0];
} }
/** /**
@ -152,11 +152,11 @@ import com.Microsoft.Z3.Enumerations.*;
return Native.goalToString(Context().nCtx(), NativeObject()); 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) 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 class DecRefQueue extends IDecRefQueue

2
src/api/java/com/Microsoft/Z3/IDisposable.java
View file

@ -21,5 +21,5 @@ package com.Microsoft.Z3;
public class IDisposable public class IDisposable
{ {
public void Dispose() {} public void Dispose() throws Z3Exception {}
} }

2
src/api/java/com/Microsoft/Z3/IntSymbol.java
View file

@ -39,7 +39,7 @@ import com.Microsoft.Z3.Enumerations.*;
void CheckNativeObject(long obj) 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"); throw new Z3Exception("Symbol is not of integer kind");
super.CheckNativeObject(obj); super.CheckNativeObject(obj);
} }

4
src/api/java/com/Microsoft/Z3/ListSort.java
View file

@ -110,8 +110,8 @@ import com.Microsoft.Z3.Enumerations.*;
ihead = 0, ihead = 0,
itail = 0; itail = 0;
NativeObject() = Native.mkListSort(ctx.nCtx(), name.NativeObject(), elemSort.NativeObject(), setNativeObject(Native.mkListSort(ctx.nCtx(), name.NativeObject(), elemSort.NativeObject(),
inil, iisnil, icons, iiscons, ihead, itail); inil, iisnil, icons, iiscons, ihead, itail));
nilDecl = new FuncDecl(ctx, inil); nilDecl = new FuncDecl(ctx, inil);
isNilDecl = new FuncDecl(ctx, iisnil); isNilDecl = new FuncDecl(ctx, iisnil);
consDecl = new FuncDecl(ctx, icons); consDecl = new FuncDecl(ctx, icons);

14
src/api/java/com/Microsoft/Z3/Model.java
View file

@ -26,7 +26,7 @@ import com.Microsoft.Z3.Enumerations.*;
Context().CheckContextMatch(a); Context().CheckContextMatch(a);
return ConstInterp(a.FuncDecl); return ConstInterp(a.FuncDecl());
} }
/** /**
@ -39,7 +39,7 @@ import com.Microsoft.Z3.Enumerations.*;
Context().CheckContextMatch(f); 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()) 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."); 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()))); 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()); long n = Native.modelGetConstInterp(Context().nCtx(), NativeObject(), f.NativeObject());
@ -139,8 +139,8 @@ import com.Microsoft.Z3.Enumerations.*;
{ {
var nFuncs = NumFuncs(); int nFuncs = NumFuncs();
var nConsts = NumConsts(); int nConsts = NumConsts();
int n = nFuncs + nConsts; int n = nFuncs + nConsts;
FuncDecl[] res = new FuncDecl[n]; FuncDecl[] res = new FuncDecl[n];
for (int i = 0; i < nConsts; i++) 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())); 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]; Expr[] res = new Expr[n];
for (int i = 0; i < n; i++) 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; return res;
} }

2
src/api/java/com/Microsoft/Z3/Native.java
View file

@ -5,7 +5,7 @@ public final class Native {
public static class LongPtr { public long value; } public static class LongPtr { public long value; }
public static class StringPtr { public String value; } public static class StringPtr { public String value; }
public static class errorHandler { public long ptr; } public static class errorHandler { public long ptr; }
static { System.loadLibrary("<mk_util.JavaDLLComponent instance at 0x0235B918>"); } static { System.loadLibrary("<mk_util.JavaDLLComponent instance at 0x0256D828>"); }
public static native long mkConfig(); public static native long mkConfig();
public static native void delConfig(long a0); public static native void delConfig(long a0);
public static native void setParamValue(long a0, String a1, String a2); public static native void setParamValue(long a0, String a1, String a2);

12
src/api/java/com/Microsoft/Z3/Params.java
View file

@ -26,16 +26,6 @@ import com.Microsoft.Z3.Enumerations.*;
Native.paramsSetBool(Context().nCtx(), NativeObject(), name.NativeObject(), (value) ? true : false); 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. * Adds a parameter setting.
**/ **/
@ -70,7 +60,7 @@ import com.Microsoft.Z3.Enumerations.*;
**/ **/
public void Add(String name, int value) 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);
} }
/** /**

48
src/api/java/com/Microsoft/Z3/Quantifier.java
View file

@ -24,7 +24,7 @@ import com.Microsoft.Z3.Enumerations.*;
/** /**
* Indicates whether the quantifier is existential. * Indicates whether the quantifier is existential.
**/ **/
public boolean IsExistential() { return !IsUniversal; } public boolean IsExistential() { return !IsUniversal(); }
/** /**
* The weight of the quantifier. * The weight of the quantifier.
@ -137,21 +137,21 @@ import com.Microsoft.Z3.Enumerations.*;
if (noPatterns == null && quantifierID == null && skolemID == null) if (noPatterns == null && quantifierID == null && skolemID == null)
{ {
NativeObject() = Native.mkQuantifier(ctx.nCtx(), (isForall) ? true : false, weight, setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall) ? true : false, weight,
AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
AST.ArrayLength(sorts), AST.ArrayToNative(sorts), AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
Symbol.ArrayToNative(names), Symbol.ArrayToNative(names),
body.NativeObject()); body.NativeObject()));
} }
else else
{ {
NativeObject() = Native.mkQuantifierEx(ctx.nCtx(), (isForall) ? true : false, weight, setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), (isForall) ? true : false, weight,
AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID), AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns), AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
AST.ArrayLength(sorts), AST.ArrayToNative(sorts), AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
Symbol.ArrayToNative(names), Symbol.ArrayToNative(names),
body.NativeObject()); body.NativeObject()));
} }
} }
@ -171,19 +171,19 @@ import com.Microsoft.Z3.Enumerations.*;
if (noPatterns == null && quantifierID == null && skolemID == null) if (noPatterns == null && quantifierID == null && skolemID == null)
{ {
NativeObject() = Native.mkQuantifierConst(ctx.nCtx(), (isForall) ? true : false, weight, setNativeObject(Native.mkQuantifierConst(ctx.nCtx(), (isForall) ? true : false, weight,
AST.ArrayLength(bound), AST.ArrayToNative(bound), AST.ArrayLength(bound), AST.ArrayToNative(bound),
AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
body.NativeObject()); body.NativeObject()));
} }
else else
{ {
NativeObject() = Native.mkQuantifierConstEx(ctx.nCtx(), (isForall) ? true : false, weight, setNativeObject(Native.mkQuantifierConstEx(ctx.nCtx(), (isForall) ? true : false, weight,
AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID), AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
AST.ArrayLength(bound), AST.ArrayToNative(bound), AST.ArrayLength(bound), AST.ArrayToNative(bound),
AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns), AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
body.NativeObject()); body.NativeObject()));
} }
} }
@ -192,7 +192,7 @@ import com.Microsoft.Z3.Enumerations.*;
void CheckNativeObject(long obj) 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"); throw new Z3Exception("Underlying object is not a quantifier");
super.CheckNativeObject(obj); super.CheckNativeObject(obj);
} }

2
src/api/java/com/Microsoft/Z3/RatNum.java
View file

@ -72,7 +72,7 @@ import com.Microsoft.Z3.Enumerations.*;
return Native.getNumeralString(Context().nCtx(), NativeObject()); return Native.getNumeralString(Context().nCtx(), NativeObject());
} }
RatNum(Context ctx, long obj) RatNum(Context ctx, long obj) throws Z3Exception
{ super(ctx, obj); { super(ctx, obj);
} }

8
src/api/java/com/Microsoft/Z3/RealExpr.java
View file

@ -19,13 +19,15 @@ import com.Microsoft.Z3.Enumerations.*;
**/ **/
public class RealExpr extends ArithExpr public class RealExpr extends ArithExpr
{ {
/** Constructor for RealExpr </summary> /**
**/ * Constructor for RealExpr </summary>
**/
protected RealExpr(Context ctx) protected RealExpr(Context ctx)
{ super(ctx); { super(ctx);
} }
RealExpr(Context ctx, long obj)
RealExpr(Context ctx, long obj) throws Z3Exception
{ super(ctx, obj); { super(ctx, obj);
} }

2
src/api/java/com/Microsoft/Z3/RelationSort.java
View file

@ -31,7 +31,7 @@ import com.Microsoft.Z3.Enumerations.*;
if (m_columnSorts != null) if (m_columnSorts != null)
return m_columnSorts; return m_columnSorts;
int n = Arity; int n = Arity();
Sort[] res = new Sort[n]; Sort[] res = new Sort[n];
for (int i = 0; i < n; i++) for (int i = 0; i < n; i++)
res[i] = Sort.Create(Context(), Native.getRelationColumn(Context().nCtx(), NativeObject(), i)); res[i] = Sort.Create(Context(), Native.getRelationColumn(Context().nCtx(), NativeObject(), i));

10
src/api/java/com/Microsoft/Z3/Solver.java
View file

@ -99,7 +99,7 @@ import com.Microsoft.Z3.Enumerations.*;
public int NumAssertions() public int NumAssertions()
{ {
ASTVector ass = new ASTVector(Context(), Native.solverGetAssertions(Context().nCtx(), NativeObject())); 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())); ASTVector ass = new ASTVector(Context(), Native.solverGetAssertions(Context().nCtx(), NativeObject()));
int n = ass.Size; int n = ass.Size();
BoolExpr[] res = new BoolExpr[n]; BoolExpr[] res = new BoolExpr[n];
for (int i = 0; i < n; i++) 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; return res;
} }
@ -185,10 +185,10 @@ import com.Microsoft.Z3.Enumerations.*;
ASTVector core = new ASTVector(Context(), Native.solverGetUnsatCore(Context().nCtx(), NativeObject())); ASTVector core = new ASTVector(Context(), Native.solverGetUnsatCore(Context().nCtx(), NativeObject()));
int n = core.Size; int n = core.Size();
Expr[] res = new Expr[n]; Expr[] res = new Expr[n];
for (int i = 0; i < n; i++) 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; return res;
} }

28
src/api/java/com/Microsoft/Z3/Statistics.java
View file

@ -25,6 +25,8 @@ import com.Microsoft.Z3.Enumerations.*;
/** /**
* The key of the entry. * The key of the entry.
**/ **/
public String Key;
/** /**
* The uint-value of the entry. * The uint-value of the entry.
**/ **/
@ -49,10 +51,10 @@ import com.Microsoft.Z3.Enumerations.*;
{ {
if (IsUInt) if (IsUInt())
return m_int.toString(); return Integer.toString(m_int);
else if (IsDouble) else if (IsDouble())
return m_double.toString(); return Double.toString(m_double);
else else
throw new Z3Exception("Unknown statistical entry type"); throw new Z3Exception("Unknown statistical entry type");
} }
@ -62,7 +64,7 @@ import com.Microsoft.Z3.Enumerations.*;
**/ **/
public String toString() public String toString()
{ {
return Key + ": " + Value; return Key + ": " + Value();
} }
private boolean m_is_int = false; private boolean m_is_int = false;
@ -71,13 +73,13 @@ import com.Microsoft.Z3.Enumerations.*;
private double m_double = 0.0; private double m_double = 0.0;
Entry(String k, int v) Entry(String k, int v)
{ {
Key = k; Key = k;
m_is_int = true; m_is_int = true;
m_int = v; m_int = v;
} }
Entry(String k, double v) Entry(String k, double v)
{ {
Key = k; Key = k;
m_is_double = true; m_is_double = true;
m_double = v; m_double = v;
} }
@ -105,14 +107,14 @@ import com.Microsoft.Z3.Enumerations.*;
int n = Size; int n = Size();
Entry[] res = new Entry[n]; Entry[] res = new Entry[n];
for (int i = 0; i < n; i++) for (int i = 0; i < n; i++)
{ {
Entry e; Entry e;
String k = Native.statsGetKey(Context().nCtx(), NativeObject(), i); String k = Native.statsGetKey(Context().nCtx(), NativeObject(), i);
if (Native.statsIsInt(Context().nCtx(), NativeObject(), i) ) if (Native.statsIsUint(Context().nCtx(), NativeObject(), i) )
e = new Entry(k, Native.statsGetIntValue(Context().nCtx(), NativeObject(), i)); e = new Entry(k, Native.statsGetUintValue(Context().nCtx(), NativeObject(), i));
else if (Native.statsIsDouble(Context().nCtx(), NativeObject(), i) ) else if (Native.statsIsDouble(Context().nCtx(), NativeObject(), i) )
e = new Entry(k, Native.statsGetDoubleValue(Context().nCtx(), NativeObject(), i)); e = new Entry(k, Native.statsGetDoubleValue(Context().nCtx(), NativeObject(), i));
else else
@ -129,7 +131,7 @@ import com.Microsoft.Z3.Enumerations.*;
{ {
int n = Size; int n = Size();
String[] res = new String[n]; String[] res = new String[n];
for (int i = 0; i < n; i++) for (int i = 0; i < n; i++)
res[i] = Native.statsGetKey(Context().nCtx(), NativeObject(), i); res[i] = Native.statsGetKey(Context().nCtx(), NativeObject(), i);
@ -142,8 +144,8 @@ import com.Microsoft.Z3.Enumerations.*;
**/ **/
public Entry get(String key) public Entry get(String key)
{ {
int n = Size; int n = Size();
Entry[] es = Entries; Entry[] es = Entries();
for (int i = 0; i < n; i++) for (int i = 0; i < n; i++)
if (es[i].Key == key) if (es[i].Key == key)
return es[i]; return es[i];

28
src/api/java/com/Microsoft/Z3/Status.java
View file

@ -14,21 +14,29 @@ import com.Microsoft.Z3.Enumerations.*;
/** /**
* Status values. * Status values.
**/ **/
public class Status public enum Status
{ {
/// <summary>
/// Used to signify an unsatisfiable status. /// Used to signify an unsatisfiable status.
/// </summary> UNSATISFIABLE (1),
public static final int UNSATISFIABLE = 1;
/// <summary>
/// Used to signify an unknown status. /// Used to signify an unknown status.
/// </summary> UNKNOWN (0),
public static final int UNKNOWN = 0;
/// <summary>
/// Used to signify a satisfiable status. /// Used to signify a satisfiable status.
/// </summary> SATISFIABLE (1);
public static final int 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; }
} }

2
src/api/java/com/Microsoft/Z3/StringSymbol.java
View file

@ -43,7 +43,7 @@ import com.Microsoft.Z3.Enumerations.*;
void CheckNativeObject(long obj) 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"); throw new Z3Exception("Symbol is not of String kind");
super.CheckNativeObject(obj); super.CheckNativeObject(obj);

12
src/api/java/com/Microsoft/Z3/Symbol.java
View file

@ -27,7 +27,7 @@ import com.Microsoft.Z3.Enumerations.*;
**/ **/
public boolean IsIntSymbol() 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() 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() public String toString()
{ {
if (IsIntSymbol()) if (IsIntSymbol())
return ((IntSymbol)this).Int.toString(); return Integer.toString(((IntSymbol)this).Int());
else if (IsStringSymbol()) else if (IsStringSymbol())
return ((StringSymbol)this).String; return ((StringSymbol)this).String();
else else
throw new Z3Exception("Unknown symbol kind encountered"); throw new Z3Exception("Unknown symbol kind encountered");
} }
@ -54,8 +54,8 @@ import com.Microsoft.Z3.Enumerations.*;
/** /**
* Symbol constructor * 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) static Symbol Create(Context ctx, long obj)

2
src/api/java/com/Microsoft/Z3/Tactic.java
View file

@ -62,7 +62,7 @@ import com.Microsoft.Z3.Enumerations.*;
return Apply(g); return Apply(g, null);
} }
/** /**

6
src/api/java/com/Microsoft/Z3/TupleSort.java
View file

@ -51,8 +51,8 @@ import com.Microsoft.Z3.Enumerations.*;
long t = 0; long t = 0;
NativeObject() = Native.mkTupleSort(ctx.nCtx(), name.NativeObject(), numFields, setNativeObject(Native.mkTupleSort(ctx.nCtx(), name.NativeObject(), numFields,
Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts), Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
t, new long[numFields]); t, new long[numFields]));
} }
}; };

2
src/api/java/com/Microsoft/Z3/Version.java
View file

@ -68,6 +68,6 @@ import com.Microsoft.Z3.Enumerations.*;
int major = 0, minor = 0, build = 0, revision = 0; int major = 0, minor = 0, build = 0, revision = 0;
Native.getVersion(major, minor, build, revision); 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);
} }
} }

16
src/api/java/com/Microsoft/Z3/Z3Object.java
View file

@ -20,7 +20,7 @@ import com.Microsoft.Z3.Enumerations.*;
/** /**
* Finalizer. * Finalizer.
**/ **/
protected void finalize() protected void finalize() throws Z3Exception
{ {
Dispose(); Dispose();
} }
@ -28,7 +28,7 @@ import com.Microsoft.Z3.Enumerations.*;
/** /**
* Disposes of the underlying native Z3 object. * Disposes of the underlying native Z3 object.
**/ **/
public void Dispose() public void Dispose() throws Z3Exception
{ {
if (m_n_obj != 0) if (m_n_obj != 0)
{ {
@ -65,7 +65,7 @@ import com.Microsoft.Z3.Enumerations.*;
m_ctx = ctx; 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; m_n_obj = obj;
} }
void IncRef(long o) { } void IncRef(long o) throws Z3Exception { }
void DecRef(long o) { } void DecRef(long o) throws Z3Exception { }
void CheckNativeObject(long obj) { } void CheckNativeObject(long obj) throws Z3Exception { }
long NativeObject() { return m_n_obj; } long NativeObject() { return m_n_obj; }
void setNativeObject(long value) void setNativeObject(long value) throws Z3Exception
{ {
if (value != 0) { CheckNativeObject(value); IncRef(value); } if (value != 0) { CheckNativeObject(value); IncRef(value); }
if (m_n_obj != 0) { DecRef(m_n_obj); } if (m_n_obj != 0) { DecRef(m_n_obj); }

10
src/api/java/mk_java.py
View file

@ -163,11 +163,11 @@ def translate(filename):
tgt.write(t + " **/\n") tgt.write(t + " **/\n")
in_javadoc = 0 in_javadoc = 0
for i in range(0, len(EXCLUDE_METHODS)): # for i in range(0, len(EXCLUDE_METHODS)):
if filename == EXCLUDE_METHODS[i][0] and s.startswith(EXCLUDE_METHODS[i][1]): # 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") # tgt.write(t + "/* Not translated because it would translate to a function with clashing types. */\n")
in_unsupported = 1 # in_unsupported = 1
break # break
if in_unsupported: if in_unsupported: