mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Java API: 32-bit issues and bugfixes.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2012-11-30 22:31:07 +00:00
parent 9b2236361c
commit 692593baaa
8 changed files with 119 additions and 71 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

50
examples/java/JavaExample.java
View file

@ -907,11 +907,10 @@ class JavaExample
// Error handling test. // Error handling test.
try try
{ {
IntExpr i = ctx.MkInt("0.5"); IntExpr i = ctx.MkInt("1/2");
throw new TestFailedException(); // unreachable throw new TestFailedException(); // unreachable
} catch (Z3Exception e) } catch (Z3Exception e)
{ {
System.out.println("GOT: " + e.getMessage());
} }
} }
@ -1001,19 +1000,38 @@ class JavaExample
} }
AST a = ctx.MkInt(42); AST a = ctx.MkInt(42);
Expr ae = (a.getClass() == Expr.class) ? ((Expr) a) : null;
if (ae == null) try
{
Expr.class.cast(a);
} catch (ClassCastException e)
{
throw new TestFailedException(); throw new TestFailedException();
ArithExpr aae = (a.getClass() == ArithExpr.class) ? ((ArithExpr) a) }
: null;
if (aae == null) try
{
ArithExpr.class.cast(a);
} catch (ClassCastException e)
{
throw new TestFailedException(); throw new TestFailedException();
IntExpr aie = (a.getClass() == IntExpr.class) ? ((IntExpr) a) : null; }
if (aie == null)
try
{
IntExpr.class.cast(a);
} catch (ClassCastException e)
{
throw new TestFailedException(); throw new TestFailedException();
IntNum ain = (a.getClass() == IntNum.class) ? ((IntNum) a) : null; }
if (ain == null)
try
{
IntNum.class.cast(a);
} catch (ClassCastException e)
{
throw new TestFailedException(); throw new TestFailedException();
}
Expr[][] earr = new Expr[2][]; Expr[][] earr = new Expr[2][];
earr[0] = new Expr[2]; earr[0] = new Expr[2];
@ -1585,7 +1603,7 @@ class JavaExample
Symbol name = ctx.MkSymbol("fruit"); Symbol name = ctx.MkSymbol("fruit");
EnumSort fruit = ctx.MkEnumSort(ctx.MkSymbol("fruit"), EnumSort fruit = ctx.MkEnumSort(name,
new Symbol[] { ctx.MkSymbol("apple"), ctx.MkSymbol("banana"), new Symbol[] { ctx.MkSymbol("apple"), ctx.MkSymbol("banana"),
ctx.MkSymbol("orange") }); ctx.MkSymbol("orange") });
@ -1974,7 +1992,7 @@ class JavaExample
{ {
int num_Exprs = to_minimize.length; int num_Exprs = to_minimize.length;
int[] upper = new int[num_Exprs]; int[] upper = new int[num_Exprs];
int[] lower = new int[num_Exprs]; int[] lower = new int[num_Exprs];
for (int i = 0; i < upper.length; ++i) for (int i = 0; i < upper.length; ++i)
{ {
upper[i] = Integer.MAX_VALUE; upper[i] = Integer.MAX_VALUE;
@ -2207,12 +2225,12 @@ class JavaExample
{ {
System.out.println("Z3 Managed Exception: " + ex.getMessage()); System.out.println("Z3 Managed Exception: " + ex.getMessage());
System.out.println("Stack trace: "); System.out.println("Stack trace: ");
ex.printStackTrace(System.out); ex.printStackTrace(System.out);
} catch (TestFailedException ex) } catch (TestFailedException ex)
{ {
System.out.println("TEST CASE FAILED: " + ex.getMessage()); System.out.println("TEST CASE FAILED: " + ex.getMessage());
System.out.println("Stack trace: "); System.out.println("Stack trace: ");
ex.printStackTrace(System.out); ex.printStackTrace(System.out);
} catch (Exception ex) } catch (Exception ex)
{ {
System.out.println("Unknown Exception: " + ex.getMessage()); System.out.println("Unknown Exception: " + ex.getMessage());

60
scripts/update_api.py
View file

@ -474,11 +474,6 @@ def java_array_element_type(p):
return 'jint' return 'jint'
else: else:
return 'jlong' return 'jlong'
def java_set_array_region(p):
if param_type(p) == INT or param_type(p) == UINT:
return 'SetIntArrayRegion'
else:
return 'SetLongArrayRegion'
def mk_java(): def mk_java():
if not is_java_enabled(): if not is_java_enabled():
@ -563,21 +558,43 @@ def mk_java():
java_wrapper.write('#endif\n\n') java_wrapper.write('#endif\n\n')
java_wrapper.write('#if defined(_M_X64) || defined(_AMD64_)\n\n') java_wrapper.write('#if defined(_M_X64) || defined(_AMD64_)\n\n')
java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n') java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n')
java_wrapper.write(' T * NEW = (T*) jenv->GetLongArrayElements(OLD, NULL); \n') java_wrapper.write(' T * NEW = (OLD == 0) ? 0 : (T*) jenv->GetLongArrayElements(OLD, NULL);\n')
java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n')
java_wrapper.write(' jenv->ReleaseLongArrayElements(OLD, (jlong *) NEW, JNI_ABORT); \n\n') java_wrapper.write(' if (OLD != 0) jenv->ReleaseLongArrayElements(OLD, (jlong *) NEW, JNI_ABORT); \n\n')
java_wrapper.write('#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \\\n')
java_wrapper.write(' jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)NEW); \n')
java_wrapper.write('#define SETLONGAREGION(OLD,Z,SZ,NEW) \\\n')
java_wrapper.write(' jenv->SetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)NEW) \n\n')
java_wrapper.write('#else\n\n') java_wrapper.write('#else\n\n')
java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n') java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n')
java_wrapper.write(' T * NEW = 0; { \\\n') java_wrapper.write(' T * NEW = 0; { \\\n')
java_wrapper.write(' jlong * temp = jenv->GetLongArrayElements(OLD, NULL); \\\n') java_wrapper.write(' jlong * temp = (OLD == 0) ? 0 : jenv->GetLongArrayElements(OLD, NULL); \\\n')
java_wrapper.write(' unsigned int size = jenv->GetArrayLength(OLD); \\\n') java_wrapper.write(' unsigned int size = (OLD == 0) ? 0 :jenv->GetArrayLength(OLD); \\\n')
java_wrapper.write(' NEW = (T*) (new int[size]); \\\n') java_wrapper.write(' if (OLD != 0) { \\\n')
java_wrapper.write(' for (unsigned i=0; i < size; i++) \\\n') java_wrapper.write(' NEW = (T*) (new int[size]); \\\n')
java_wrapper.write(' NEW[i] = reinterpret_cast<T>(temp[i]); \\\n') java_wrapper.write(' for (unsigned i=0; i < size; i++) \\\n')
java_wrapper.write(' jenv->ReleaseLongArrayElements(OLD, temp, JNI_ABORT); \\\n') java_wrapper.write(' NEW[i] = reinterpret_cast<T>(temp[i]); \\\n')
java_wrapper.write(' } \n\n') java_wrapper.write(' jenv->ReleaseLongArrayElements(OLD, temp, JNI_ABORT); \\\n')
java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') java_wrapper.write(' } \\\n')
java_wrapper.write(' } \n\n')
java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n')
java_wrapper.write(' delete [] NEW; \n\n') java_wrapper.write(' delete [] NEW; \n\n')
java_wrapper.write('#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \\\n')
java_wrapper.write(' { \\\n')
java_wrapper.write(' jlong * temp = new jlong[SZ]; \\\n')
java_wrapper.write(' jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)temp); \\\n')
java_wrapper.write(' for (int i = 0; i < (SZ); i++) \\\n')
java_wrapper.write(' NEW[i] = reinterpret_cast<T>(temp[i]); \\\n')
java_wrapper.write(' delete [] temp; \\\n')
java_wrapper.write(' }\n\n')
java_wrapper.write('#define SETLONGAREGION(OLD,Z,SZ,NEW) \\\n')
java_wrapper.write(' { \\\n')
java_wrapper.write(' jlong * temp = new jlong[SZ]; \\\n')
java_wrapper.write(' for (int i = 0; i < (SZ); i++) \\\n')
java_wrapper.write(' temp[i] = reinterpret_cast<jlong>(NEW[i]); \\\n')
java_wrapper.write(' jenv->SetLongArrayRegion(OLD,Z,(jsize)SZ,temp); \\\n')
java_wrapper.write(' delete [] temp; \\\n')
java_wrapper.write(' }\n\n')
java_wrapper.write('#endif\n\n') java_wrapper.write('#endif\n\n')
java_wrapper.write('void Z3JavaErrorHandler(Z3_context c, Z3_error_code e)\n') java_wrapper.write('void Z3JavaErrorHandler(Z3_context c, Z3_error_code e)\n')
java_wrapper.write('{\n') java_wrapper.write('{\n')
@ -615,6 +632,10 @@ def mk_java():
type2str(param_type(param)), type2str(param_type(param)),
param_array_capacity_pos(param), param_array_capacity_pos(param),
type2str(param_type(param)))) type2str(param_type(param))))
if param_type(param) == INT or param_type(param) == UINT:
java_wrapper.write(' jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
else:
java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i))
elif k == IN and param_type(param) == STRING: elif k == IN and param_type(param) == STRING:
java_wrapper.write(' Z3_string _a%s = (Z3_string) jenv->GetStringUTFChars(a%s, NULL);\n' % (i, i)) java_wrapper.write(' Z3_string _a%s = (Z3_string) jenv->GetStringUTFChars(a%s, NULL);\n' % (i, i))
i = i + 1 i = i + 1
@ -646,11 +667,10 @@ def mk_java():
for param in params: for param in params:
k = param_kind(param) k = param_kind(param)
if k == OUT_ARRAY: if k == OUT_ARRAY:
java_wrapper.write(' jenv->%s(a%s, 0, (jsize)a%s, (%s *) _a%s);\n' % (java_set_array_region(param), if param_type(param) == INT or param_type(param) == UINT:
i, java_wrapper.write(' jenv->SetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
param_array_capacity_pos(param), else:
java_array_element_type(param), java_wrapper.write(' SETLONGAREGION(a%s, 0, a%s, _a%s);\n' % (i, param_array_capacity_pos(param), i))
i))
java_wrapper.write(' free(_a%s);\n' % i) java_wrapper.write(' free(_a%s);\n' % i)
elif k == IN_ARRAY or k == OUT_ARRAY: elif k == IN_ARRAY or k == OUT_ARRAY:
if param_type(param) == INT or param_type(param) == UINT: if param_type(param) == INT or param_type(param) == UINT:

39
src/api/java/AST.java
View file

@ -37,10 +37,15 @@ public class AST extends Z3Object
**/ **/
public boolean equals(Object o) public boolean equals(Object o)
{ {
AST casted = (AST) o; AST casted = null;
if (casted == null)
return false; try {
return this == casted; casted = AST.class.cast(o);
} catch (ClassCastException e) {
return false;
}
return this.NativeObject() == casted.NativeObject();
} }
/** /**
@ -53,18 +58,20 @@ public class AST extends Z3Object
{ {
if (other == null) if (other == null)
return 1; return 1;
AST oAST = (AST) other;
if (oAST == null) AST oAST = null;
return 1; try {
else AST.class.cast(other);
{ } catch (ClassCastException e) {
if (Id() < oAST.Id()) return 1;
return -1; }
else if (Id() > oAST.Id())
return +1; if (Id() < oAST.Id())
else return -1;
return 0; else if (Id() > oAST.Id())
} return +1;
else
return 0;
} }
/** /**

2
src/api/java/Context.java
View file

@ -524,7 +524,7 @@ public class Context extends IDisposable
public Expr MkConst(FuncDecl f) throws Z3Exception public Expr MkConst(FuncDecl f) throws Z3Exception
{ {
return MkApp(f, (Expr) null); return MkApp(f, (Expr[]) null);
} }
/** /**

9
src/api/java/EnumSort.java
View file

@ -16,7 +16,6 @@ public class EnumSort extends Sort
**/ **/
public FuncDecl[] ConstDecls() public FuncDecl[] ConstDecls()
{ {
return _constdecls; return _constdecls;
} }
@ -25,7 +24,6 @@ public class EnumSort extends Sort
**/ **/
public Expr[] Consts() public Expr[] Consts()
{ {
return _consts; return _consts;
} }
@ -34,7 +32,6 @@ public class EnumSort extends Sort
**/ **/
public FuncDecl[] TesterDecls() public FuncDecl[] TesterDecls()
{ {
return _testerdecls; return _testerdecls;
} }
@ -53,12 +50,12 @@ public class EnumSort extends Sort
n_constdecls, n_testers)); 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]);
_testerdecls = new FuncDecl[n]; _testerdecls = new FuncDecl[n];
for (int i = 0; i < n; i++) for (int i = 0; i < n; i++)
_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], (Expr)null); _consts[i] = ctx.MkApp(_constdecls[i], (Expr[])null);
} }
}; };

15
src/api/java/Quantifier.java
View file

@ -159,13 +159,14 @@ public class Quantifier extends BoolExpr
.NativeObject())); .NativeObject()));
} else } else
{ {
setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), (isForall) ? true setNativeObject(Native.mkQuantifierEx(ctx.nCtx(),
: false, weight, AST.GetNativeObject(quantifierID), AST (isForall) ? true : false, weight, AST.GetNativeObject(quantifierID),
.GetNativeObject(skolemID), AST.ArrayLength(patterns), AST AST.GetNativeObject(skolemID),
.ArrayToNative(patterns), AST.ArrayLength(noPatterns), AST AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
.ArrayToNative(noPatterns), AST.ArrayLength(sorts), AST AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
.ArrayToNative(sorts), Symbol.ArrayToNative(names), body AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
.NativeObject())); Symbol.ArrayToNative(names),
body.NativeObject()));
} }
} }

13
src/api/java/Sort.java
View file

@ -39,10 +39,15 @@ public class Sort extends AST
**/ **/
public boolean equals(Object o) public boolean equals(Object o)
{ {
Sort casted = (Sort) o; Sort casted = null;
if (casted == null)
return false; try {
return this == casted; casted = Sort.class.cast(o);
} catch (ClassCastException e) {
return false;
}
return this.NativeObject() == casted.NativeObject();
} }
/** /**

2
src/api/java/Z3Object.java
View file

@ -104,7 +104,7 @@ public class Z3Object extends IDisposable
return null; return null;
long[] an = new long[a.length]; long[] an = new long[a.length];
for (int i = 0; i < a.length; i++) for (int i = 0; i < a.length; i++)
an[i] = a[i].NativeObject(); an[i] = (a[i] == null) ? 0 : a[i].NativeObject();
return an; return an;
} }