mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

Java API: more automatic translation from C#, but still unfinished.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2012-11-26 21:03:35 +00:00
parent 75b1278e97
commit 36d9a90d2a
80 changed files with 1439 additions and 1166 deletions
Download patch file Download diff file Expand all files Collapse all files

19
scripts/mk_util.py
View file

@ -1854,8 +1854,25 @@ def mk_z3consts_java(api_files):
efile.write(' **/\n') efile.write(' **/\n')
efile.write('public enum %s {\n' % name) efile.write('public enum %s {\n' % name)
efile.write efile.write
first = True
for k, i in decls.iteritems(): for k, i in decls.iteritems():
efile.write('%s (%s),\n' % (k, i)) if first:
first = False
else:
efile.write(',\n')
efile.write(' %s (%s)' % (k, i))
efile.write(";\n")
efile.write('\n private final int intValue;\n\n')
efile.write(' %s(int v) {\n' % name)
efile.write(' this.intValue = v;\n')
efile.write(' }\n\n')
efile.write(' public static final %s fromInt(int v) {\n' % name)
efile.write(' for (%s k: values()) \n' % name)
efile.write(' if (k.intValue == v) return k;\n')
efile.write(' return values()[0];\n')
efile.write(' }\n\n')
efile.write(' public final int toInt() { return this.intValue; }\n')
# efile.write(';\n %s(int v) {}\n' % name)
efile.write('}\n\n') efile.write('}\n\n')
efile.close() efile.close()
mode = SEARCHING mode = SEARCHING

1
scripts/update_api.py
View file

@ -509,6 +509,7 @@ def mk_java():
java_native.write(' public static class IntPtr { public int value; }\n') java_native.write(' public static class IntPtr { public int value; }\n')
java_native.write(' public static class LongPtr { public long value; }\n') java_native.write(' public static class LongPtr { public long value; }\n')
java_native.write(' public static class StringPtr { public String value; }\n') java_native.write(' public static class StringPtr { public String value; }\n')
java_native.write(' public static class errorHandler { public long ptr; }\n')
if is_windows(): if is_windows():
java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java')) java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java'))

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Collections; */ /* using System.Collections; */
@ -58,9 +59,9 @@ import java.lang.Exception;
return 1; return 1;
else else
{ {
if (Id < oAST.Id) if (Id() < oAST.Id())
return -1; return -1;
else if (Id > oAST.Id) else if (Id() > oAST.Id())
return +1; return +1;
else else
return 0; return 0;
@ -79,7 +80,7 @@ import java.lang.Exception;
/** /**
* A unique identifier for the AST (unique among all ASTs). * A unique identifier for the AST (unique among all ASTs).
**/ **/
public long Id() { return Native.getAstId(Context().nCtx(), NativeObject()); } public int Id() { return Native.getAstId(Context().nCtx(), NativeObject()); }
/** /**
* Translates (copies) the AST to the Context <paramref name="ctx"/>. * Translates (copies) the AST to the Context <paramref name="ctx"/>.
@ -91,7 +92,7 @@ import java.lang.Exception;
if (ReferenceEquals(Context, ctx)) if (Context() == ctx)
return this; return this;
else else
return new AST(ctx, Native.translate(Context().nCtx(), NativeObject(), ctx.nCtx())); return new AST(ctx, Native.translate(Context().nCtx(), NativeObject(), ctx.nCtx()));
@ -100,7 +101,7 @@ import java.lang.Exception;
/** /**
* The kind of the AST. * The kind of the AST.
**/ **/
public Z3_ast_kind ASTKind() { return (Z3_ast_kind)Native.getAstKind(Context().nCtx(), NativeObject()); } public Z3_ast_kind ASTKind() { return Z3_ast_kind.fromInt(Native.getAstKind(Context().nCtx(), NativeObject())); }
/** /**
* Indicates whether the AST is an Expr * Indicates whether the AST is an Expr
@ -109,10 +110,10 @@ import java.lang.Exception;
{ {
switch (ASTKind()) switch (ASTKind())
{ {
case Z3_ast_kind.Z3_APP_AST: case Z3_APP_AST:
case Z3_ast_kind.Z3_NUMERAL_AST: case Z3_NUMERAL_AST:
case Z3_ast_kind.Z3_QUANTIFIER_AST: case Z3_QUANTIFIER_AST:
case Z3_ast_kind.Z3_VAR_AST: return true; case Z3_VAR_AST: return true;
default: return false; default: return false;
} }
} }
@ -174,22 +175,22 @@ import java.lang.Exception;
void IncRef(long o) void IncRef(long o)
{ {
// Console.WriteLine("AST IncRef()"); // Console.WriteLine("AST IncRef()");
if (Context == null) if (Context() == null)
throw new Z3Exception("inc() called on null context"); throw new Z3Exception("inc() called on null context");
if (o == 0) if (o == 0)
throw new Z3Exception("inc() called on null AST"); throw new Z3Exception("inc() called on null AST");
Context.AST_DRQ.IncAndClear(Context, o); Context().AST_DRQ().IncAndClear(Context(), o);
super.IncRef(o); super.IncRef(o);
} }
void DecRef(long o) void DecRef(long o)
{ {
// Console.WriteLine("AST DecRef()"); // Console.WriteLine("AST DecRef()");
if (Context == null) if (Context() == null)
throw new Z3Exception("dec() called on null context"); throw new Z3Exception("dec() called on null context");
if (o == 0) if (o == 0)
throw new Z3Exception("dec() called on null AST"); throw new Z3Exception("dec() called on null AST");
Context.AST_DRQ.Add(o); Context().AST_DRQ().Add(o);
super.DecRef(o); super.DecRef(o);
} }
@ -198,14 +199,14 @@ import java.lang.Exception;
switch ((Z3_ast_kind)Native.getAstKind(ctx.nCtx(), obj)) switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)))
{ {
case Z3_ast_kind.Z3_FUNC_DECL_AST: return new FuncDecl(ctx, obj); case Z3_FUNC_DECL_AST: return new FuncDecl(ctx, obj);
case Z3_ast_kind.Z3_QUANTIFIER_AST: return new Quantifier(ctx, obj); case Z3_QUANTIFIER_AST: return new Quantifier(ctx, obj);
case Z3_ast_kind.Z3_SORT_AST: return Sort.Create(ctx, obj); case Z3_SORT_AST: return Sort.Create(ctx, obj);
case Z3_ast_kind.Z3_APP_AST: case Z3_APP_AST:
case Z3_ast_kind.Z3_NUMERAL_AST: case Z3_NUMERAL_AST:
case Z3_ast_kind.Z3_VAR_AST: return Expr.Create(ctx, obj); case Z3_VAR_AST: return Expr.Create(ctx, obj);
default: default:
throw new Z3Exception("Unknown AST kind"); throw new Z3Exception("Unknown AST kind");
} }

17
src/api/java/com/Microsoft/Z3/ASTMap.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -24,7 +25,7 @@ import java.lang.Exception;
{ {
return Native.astMapContains(Context().nCtx(), NativeObject(), k.NativeObject) != 0; return Native.astMapContains(Context().nCtx(), NativeObject(), k.NativeObject()) ;
} }
/** /**
@ -39,7 +40,7 @@ import java.lang.Exception;
return new AST(Context, Native.astMapFind(Context().nCtx(), NativeObject(), k.NativeObject)); return new AST(Context(), Native.astMapFind(Context().nCtx(), NativeObject(), k.NativeObject()));
} }
/** /**
@ -52,7 +53,7 @@ import java.lang.Exception;
Native.astMapInsert(Context().nCtx(), NativeObject(), k.NativeObject, v.NativeObject); Native.astMapInsert(Context().nCtx(), NativeObject(), k.NativeObject(), v.NativeObject());
} }
/** /**
@ -63,7 +64,7 @@ import java.lang.Exception;
{ {
Native.astMapErase(Context().nCtx(), NativeObject(), k.NativeObject); Native.astMapErase(Context().nCtx(), NativeObject(), k.NativeObject());
} }
/** /**
@ -77,14 +78,14 @@ import java.lang.Exception;
/** /**
* The size of the map * The size of the map
**/ **/
public long Size() { return Native.astMapSize(Context().nCtx(), NativeObject()); } public int Size() { return Native.astMapSize(Context().nCtx(), NativeObject()); }
/** /**
* The keys stored in the map. * The keys stored in the map.
**/ **/
public ASTVector Keys() public ASTVector Keys()
{ {
return new ASTVector(Context, Native.astMapKeys(Context().nCtx(), NativeObject())); return new ASTVector(Context(), Native.astMapKeys(Context().nCtx(), NativeObject()));
} }
/** /**
@ -119,13 +120,13 @@ import java.lang.Exception;
void IncRef(long o) void IncRef(long o)
{ {
Context.ASTMap_DRQ.IncAndClear(Context, o); Context().ASTMap_DRQ().IncAndClear(Context(), o);
super.IncRef(o); super.IncRef(o);
} }
void DecRef(long o) void DecRef(long o)
{ {
Context.ASTMap_DRQ.Add(o); Context().ASTMap_DRQ().Add(o);
super.DecRef(o); super.DecRef(o);
} }
} }

21
src/api/java/com/Microsoft/Z3/ASTVector.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -18,7 +19,7 @@ import java.lang.Exception;
/** /**
* The size of the vector * The size of the vector
**/ **/
public long Size() { return Native.astVectorSize(Context().nCtx(), NativeObject()); } public int Size() { return Native.astVectorSize(Context().nCtx(), NativeObject()); }
/** /**
* Retrieves the i-th object in the vector. * Retrieves the i-th object in the vector.
@ -26,24 +27,24 @@ import java.lang.Exception;
* <param name="i">Index</param> * <param name="i">Index</param>
* @return An AST * @return An AST
**/ **/
public AST get(long i) public AST get(int i)
{ {
return new AST(Context, Native.astVectorGet(Context().nCtx(), NativeObject(), i)); return new AST(Context(), Native.astVectorGet(Context().nCtx(), NativeObject(), i));
} }
public void set(long i, AST value) public void set(int i, AST value)
{ {
Native.astVectorSet(Context().nCtx(), NativeObject(), i, value.NativeObject); Native.astVectorSet(Context().nCtx(), NativeObject(), i, value.NativeObject());
} }
/** /**
* Resize the vector to <paramref name="newSize"/>. * Resize the vector to <paramref name="newSize"/>.
* <param name="newSize">The new size of the vector.</param> * <param name="newSize">The new size of the vector.</param>
**/ **/
public void Resize(long newSize) public void Resize(int newSize)
{ {
Native.astVectorResize(Context().nCtx(), NativeObject(), newSize); Native.astVectorResize(Context().nCtx(), NativeObject(), newSize);
} }
@ -57,7 +58,7 @@ import java.lang.Exception;
{ {
Native.astVectorPush(Context().nCtx(), NativeObject(), a.NativeObject); Native.astVectorPush(Context().nCtx(), NativeObject(), a.NativeObject());
} }
/** /**
@ -70,7 +71,7 @@ import java.lang.Exception;
return new ASTVector(Context, Native.astVectorTranslate(Context().nCtx(), NativeObject(), ctx.nCtx())); return new ASTVector(Context(), Native.astVectorTranslate(Context().nCtx(), NativeObject(), ctx.nCtx()));
} }
/** /**
@ -99,13 +100,13 @@ import java.lang.Exception;
void IncRef(long o) void IncRef(long o)
{ {
Context.ASTVector_DRQ.IncAndClear(Context, o); Context().ASTVector_DRQ().IncAndClear(Context(), o);
super.IncRef(o); super.IncRef(o);
} }
void DecRef(long o) void DecRef(long o)
{ {
Context.ASTVector_DRQ.Add(o); Context().ASTVector_DRQ().Add(o);
super.DecRef(o); super.DecRef(o);
} }
} }

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Numerics; */ /* using System.Numerics; */
@ -23,11 +24,11 @@ import java.lang.Exception;
* <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(long precision) public RatNum ToUpper(int precision)
{ {
return new RatNum(Context, Native.getAlgebraicNumberUpper(Context().nCtx(), NativeObject(), precision)); return new RatNum(Context(), Native.getAlgebraicNumberUpper(Context().nCtx(), NativeObject(), precision));
} }
/** /**
@ -37,18 +38,18 @@ import java.lang.Exception;
* <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(long precision) public RatNum ToLower(int precision)
{ {
return new RatNum(Context, Native.getAlgebraicNumberLower(Context().nCtx(), NativeObject(), precision)); return new RatNum(Context(), Native.getAlgebraicNumberLower(Context().nCtx(), NativeObject(), precision));
} }
/** /**
* 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(long precision) public String ToDecimal(int precision)
{ {

17
src/api/java/com/Microsoft/Z3/ApplyResult.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -19,7 +20,7 @@ import java.lang.Exception;
/** /**
* The number of Subgoals. * The number of Subgoals.
**/ **/
public long NumSubgoals() { return Native.applyResultGetNumSubgoals(Context().nCtx(), NativeObject()); } public int NumSubgoals() { return Native.applyResultGetNumSubgoals(Context().nCtx(), NativeObject()); }
/** /**
* Retrieves the subgoals from the ApplyResult. * Retrieves the subgoals from the ApplyResult.
@ -29,10 +30,10 @@ import java.lang.Exception;
long n = NumSubgoals; int n = NumSubgoals();
Goal[] res = new Goal[n]; Goal[] res = new Goal[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = new Goal(Context, Native.applyResultGetSubgoal(Context().nCtx(), NativeObject(), i)); res[i] = new Goal(Context(), Native.applyResultGetSubgoal(Context().nCtx(), NativeObject(), i));
return res; return res;
} }
@ -41,12 +42,12 @@ import java.lang.Exception;
* goal <code>g</code>, that the ApplyResult was obtained from. * goal <code>g</code>, that the ApplyResult was obtained from.
* @return A model for <code>g</code> * @return A model for <code>g</code>
**/ **/
public Model ConvertModel(long i, Model m) public Model ConvertModel(int i, Model m)
{ {
return new Model(Context, Native.applyResultConvertModel(Context().nCtx(), NativeObject(), i, m.NativeObject)); return new Model(Context(), Native.applyResultConvertModel(Context().nCtx(), NativeObject(), i, m.NativeObject()));
} }
/** /**
@ -77,13 +78,13 @@ import java.lang.Exception;
void IncRef(long o) void IncRef(long o)
{ {
Context.ApplyResult_DRQ.IncAndClear(Context, o); Context().ApplyResult_DRQ().IncAndClear(Context(), o);
super.IncRef(o); super.IncRef(o);
} }
void DecRef(long o) void DecRef(long o)
{ {
Context.ApplyResult_DRQ.Add(o); Context().ApplyResult_DRQ().Add(o);
super.DecRef(o); super.DecRef(o);
} }
} }

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Collections.Generic; */ /* using System.Collections.Generic; */
/* using System.Linq; */ /* using System.Linq; */

1
src/api/java/com/Microsoft/Z3/ArithSort.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */

1
src/api/java/com/Microsoft/Z3/ArrayExpr.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Collections.Generic; */ /* using System.Collections.Generic; */
/* using System.Linq; */ /* using System.Linq; */

7
src/api/java/com/Microsoft/Z3/ArraySort.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -22,7 +23,7 @@ import java.lang.Exception;
{ {
return Sort.Create(Context, Native.getArraySortDomain(Context().nCtx(), NativeObject())); return Sort.Create(Context(), Native.getArraySortDomain(Context().nCtx(), NativeObject()));
} }
/** /**
@ -32,12 +33,12 @@ import java.lang.Exception;
{ {
return Sort.Create(Context, Native.getArraySortRange(Context().nCtx(), NativeObject())); return Sort.Create(Context(), Native.getArraySortRange(Context().nCtx(), NativeObject()));
} }
ArraySort(Context ctx, long obj) { super(ctx, obj); { }} ArraySort(Context ctx, long obj) { super(ctx, obj); { }}
ArraySort(Context ctx, Sort domain, Sort range) ArraySort(Context ctx, Sort domain, Sort range)
{ super(ctx, Native.mkArraySort(ctx.nCtx(), domain.NativeObject, range.NativeObject)); { super(ctx, Native.mkArraySort(ctx.nCtx(), domain.NativeObject(), range.NativeObject()));

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Collections.Generic; */ /* using System.Collections.Generic; */
/* using System.Linq; */ /* using System.Linq; */
@ -22,7 +23,7 @@ import java.lang.Exception;
/** /**
* The size of the sort of a bit-vector term. * The size of the sort of a bit-vector term.
**/ **/
public long SortSize() { return ((BitVecSort)Sort).Size; } public int SortSize() { return ((BitVecSort)Sort).Size; }
/** Constructor for BitVecExpr </summary> /** Constructor for BitVecExpr </summary>
**/ **/

17
src/api/java/com/Microsoft/Z3/BitVecNum.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Numerics; */ /* using System.Numerics; */
@ -22,7 +23,7 @@ import java.lang.Exception;
public long UInt64() public long UInt64()
{ {
long res = 0; long res = 0;
if (Native.getNumeralLong64(Context().nCtx(), NativeObject(), res) == 0) if (Native.getNumeralInt64(Context().nCtx(), NativeObject(), res) ^ true)
throw new Z3Exception("Numeral is not a 64 bit unsigned"); throw new Z3Exception("Numeral is not a 64 bit unsigned");
return res; return res;
} }
@ -33,7 +34,7 @@ import java.lang.Exception;
public int Int() public int Int()
{ {
int res = 0; int res = 0;
if (Native.getNumeralInt(Context().nCtx(), NativeObject(), res) == 0) if (Native.getNumeralInt(Context().nCtx(), NativeObject(), res) ^ true)
throw new Z3Exception("Numeral is not an int"); throw new Z3Exception("Numeral is not an int");
return res; return res;
} }
@ -44,7 +45,7 @@ import java.lang.Exception;
public long Int64() public long Int64()
{ {
long res = 0; long res = 0;
if (Native.getNumeralInt64(Context().nCtx(), NativeObject(), res) == 0) if (Native.getNumeralInt64(Context().nCtx(), NativeObject(), res) ^ true)
throw new Z3Exception("Numeral is not an int64"); throw new Z3Exception("Numeral is not an int64");
return res; return res;
} }
@ -52,11 +53,11 @@ import java.lang.Exception;
/** /**
* Retrieve the int value. * Retrieve the int value.
**/ **/
public long UInt() public int UInt()
{ {
long res = 0; int res = 0;
if (Native.getNumeralLong(Context().nCtx(), NativeObject(), res) == 0) if (Native.getNumeralInt(Context().nCtx(), NativeObject(), res) ^ true)
throw new Z3Exception("Numeral is not a long"); throw new Z3Exception("Numeral is not a int");
return res; return res;
} }
@ -65,7 +66,7 @@ import java.lang.Exception;
**/ **/
public BigInteger BigInteger() public BigInteger BigInteger()
{ {
return BigInteger.Parse(this.ToString()); return new BigInteger(this.toString());
} }
/** /**

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -18,8 +19,7 @@ import java.lang.Exception;
/** /**
* The size of the bit-vector sort. * The size of the bit-vector sort.
**/ **/
public long Size() { return Native.getBvSortSize(Context().nCtx(), NativeObject()); } public int Size() { return Native.getBvSortSize(Context().nCtx(), NativeObject()); }
BitVecSort(Context ctx, long obj) { super(ctx, obj); { }} BitVecSort(Context ctx, long obj) { super(ctx, obj); { }}
BitVecSort(Context ctx, long size) { super(ctx, Native.mkBvSort(ctx.nCtx(), size)); { }}
}; };

1
src/api/java/com/Microsoft/Z3/BoolExpr.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Collections.Generic; */ /* using System.Collections.Generic; */
/* using System.Linq; */ /* using System.Linq; */

1
src/api/java/com/Microsoft/Z3/BoolSort.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -18,7 +19,7 @@ import java.lang.Exception;
/** /**
* The number of fields of the constructor. * The number of fields of the constructor.
**/ **/
public long NumFields() public int NumFields()
{ {
init(); init();
return n; return n;
@ -70,13 +71,13 @@ import java.lang.Exception;
} }
private long n = 0; private int n = 0;
private FuncDecl m_testerDecl = null; private FuncDecl m_testerDecl = null;
private FuncDecl m_constructorDecl = null; private FuncDecl m_constructorDecl = null;
private FuncDecl[] m_accessorDecls = null; private FuncDecl[] m_accessorDecls = null;
Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames, Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames,
Sort[] sorts, long[] sortRefs) Sort[] sorts, int[] sortRefs)
{ super(ctx); { super(ctx);
@ -86,12 +87,12 @@ import java.lang.Exception;
if (n != AST.ArrayLength(sorts)) if (n != AST.ArrayLength(sorts))
throw new Z3Exception("Number of field names does not match number of sorts"); throw new Z3Exception("Number of field names does not match number of sorts");
if (sortRefs != null && sortRefs.Length != n) if (sortRefs != null && sortRefs.length != n)
throw new Z3Exception("Number of field names does not match number of sort refs"); throw new Z3Exception("Number of field names does not match number of sort refs");
if (sortRefs == null) sortRefs = new long[n]; if (sortRefs == null) sortRefs = new int[n];
NativeObject() = Native.mkConstructor(ctx.nCtx(), name.NativeObject, recognizer.NativeObject, NativeObject() = Native.mkConstructor(ctx.nCtx(), name.NativeObject(), recognizer.NativeObject(),
n, n,
Symbol.ArrayToNative(fieldNames), Symbol.ArrayToNative(fieldNames),
Sort.ArrayToNative(sorts), Sort.ArrayToNative(sorts),
@ -110,11 +111,11 @@ import java.lang.Exception;
long tester = 0; long tester = 0;
long[] accessors = new long[n]; long[] accessors = new long[n];
Native.queryConstructor(Context().nCtx(), NativeObject(), n, constructor, tester, accessors); Native.queryConstructor(Context().nCtx(), NativeObject(), n, constructor, tester, accessors);
m_constructorDecl = new FuncDecl(Context, constructor); m_constructorDecl = new FuncDecl(Context(), constructor);
m_testerDecl = new FuncDecl(Context, tester); m_testerDecl = new FuncDecl(Context(), tester);
m_accessorDecls = new FuncDecl[n]; m_accessorDecls = new FuncDecl[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
m_accessorDecls[i] = new FuncDecl(Context, accessors[i]); m_accessorDecls[i] = new FuncDecl(Context(), accessors[i]);
} }
} }

3
src/api/java/com/Microsoft/Z3/ConstructorList.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Collections.Generic; */ /* using System.Collections.Generic; */
@ -37,6 +38,6 @@ import java.lang.Exception;
setNativeObject(Native.mkConstructorList(Context().nCtx(), (long)constructors.Length, Constructor.ArrayToNative(constructors))); setNativeObject(Native.mkConstructorList(Context().nCtx(), (int)constructors.length, Constructor.ArrayToNative(constructors)));
} }
} }

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

File diff suppressed because it is too large Load diff

1
src/api/java/com/Microsoft/Z3/DatatypeExpr.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Collections.Generic; */ /* using System.Collections.Generic; */
/* using System.Linq; */ /* using System.Linq; */

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -18,7 +19,7 @@ import java.lang.Exception;
/** /**
* The number of constructors of the datatype sort. * The number of constructors of the datatype sort.
**/ **/
public long NumConstructors() { return Native.getDatatypeSortNumConstructors(Context().nCtx(), NativeObject()); } public int NumConstructors() { return Native.getDatatypeSortNumConstructors(Context().nCtx(), NativeObject()); }
/** /**
* The constructors. * The constructors.
@ -27,10 +28,10 @@ import java.lang.Exception;
{ {
long n = NumConstructors; int n = NumConstructors();
FuncDecl[] res = new FuncDecl[n]; FuncDecl[] res = new FuncDecl[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.getDatatypeSortConstructor(Context().nCtx(), NativeObject(), i)); res[i] = new FuncDecl(Context(), Native.getDatatypeSortConstructor(Context().nCtx(), NativeObject(), i));
return res; return res;
} }
@ -41,10 +42,10 @@ import java.lang.Exception;
{ {
long n = NumConstructors; int n = NumConstructors();
FuncDecl[] res = new FuncDecl[n]; FuncDecl[] res = new FuncDecl[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.getDatatypeSortRecognizer(Context().nCtx(), NativeObject(), i)); res[i] = new FuncDecl(Context(), Native.getDatatypeSortRecognizer(Context().nCtx(), NativeObject(), i));
return res; return res;
} }
@ -55,15 +56,15 @@ import java.lang.Exception;
{ {
long n = NumConstructors; int n = NumConstructors();
FuncDecl[][] res = new FuncDecl[n][]; FuncDecl[][] res = new FuncDecl[n][];
for (long i; 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));
long ds = fd.DomainSize; int ds = fd.DomainSize;
FuncDecl[] tmp = new FuncDecl[ds]; FuncDecl[] tmp = new FuncDecl[ds];
for (long j; 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));
res[i] = tmp; res[i] = tmp;
} }
return res; return res;
@ -72,7 +73,7 @@ import java.lang.Exception;
DatatypeSort(Context ctx, long obj) { super(ctx, obj); { }} DatatypeSort(Context ctx, long obj) { super(ctx, obj); { }}
DatatypeSort(Context ctx, Symbol name, Constructor[] constructors) DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
{ super(ctx, Native.mkDatatype(ctx.nCtx(), name.NativeObject, (long)constructors.Length, ArrayToNative(constructors))); { super(ctx, Native.mkDatatype(ctx.nCtx(), name.NativeObject(), (int)constructors.length, ArrayToNative(constructors)));

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -64,19 +65,19 @@ import java.lang.Exception;
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, (long)n, NativeObject() = 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 (long i; 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 (long i; 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 (long i; i < n; i++) for (int i = 0; i < n; i++)
_consts[i] = ctx.MkApp(_constdecls[i]); _consts[i] = ctx.MkApp(_constdecls[i]);
} }
}; };

BIN
src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.class Normal file
View file

Binary file not shown.

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

@ -8,12 +8,26 @@ package com.Microsoft.Z3;
* Z3_ast_kind * Z3_ast_kind
**/ **/
public enum Z3_ast_kind { public enum Z3_ast_kind {
Z3_VAR_AST (2), Z3_VAR_AST (2),
Z3_SORT_AST (4), Z3_SORT_AST (4),
Z3_QUANTIFIER_AST (3), Z3_QUANTIFIER_AST (3),
Z3_UNKNOWN_AST (1000), Z3_UNKNOWN_AST (1000),
Z3_FUNC_DECL_AST (5), Z3_FUNC_DECL_AST (5),
Z3_NUMERAL_AST (0), Z3_NUMERAL_AST (0),
Z3_APP_AST (1), Z3_APP_AST (1);
private final int intValue;
Z3_ast_kind(int v) {
this.intValue = v;
}
public static final Z3_ast_kind fromInt(int v) {
for (Z3_ast_kind k: values())
if (k.intValue == v) return k;
return values()[0];
}
public final int toInt() { return this.intValue; }
} }

BIN
src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.class Normal file
View file

Binary file not shown.

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

@ -8,9 +8,23 @@ package com.Microsoft.Z3;
* Z3_ast_print_mode * Z3_ast_print_mode
**/ **/
public enum Z3_ast_print_mode { public enum Z3_ast_print_mode {
Z3_PRINT_SMTLIB2_COMPLIANT (3), Z3_PRINT_SMTLIB2_COMPLIANT (3),
Z3_PRINT_SMTLIB_COMPLIANT (2), Z3_PRINT_SMTLIB_COMPLIANT (2),
Z3_PRINT_SMTLIB_FULL (0), Z3_PRINT_SMTLIB_FULL (0),
Z3_PRINT_LOW_LEVEL (1), Z3_PRINT_LOW_LEVEL (1);
private final int intValue;
Z3_ast_print_mode(int v) {
this.intValue = v;
}
public static final Z3_ast_print_mode fromInt(int v) {
for (Z3_ast_print_mode k: values())
if (k.intValue == v) return k;
return values()[0];
}
public final int toInt() { return this.intValue; }
} }

BIN
src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.class Normal file
View file

Binary file not shown.

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

@ -8,157 +8,171 @@ package com.Microsoft.Z3;
* Z3_decl_kind * Z3_decl_kind
**/ **/
public enum Z3_decl_kind { public enum Z3_decl_kind {
Z3_OP_LABEL (1792), Z3_OP_LABEL (1792),
Z3_OP_PR_REWRITE (1294), Z3_OP_PR_REWRITE (1294),
Z3_OP_UNINTERPRETED (2051), Z3_OP_UNINTERPRETED (2051),
Z3_OP_SUB (519), Z3_OP_SUB (519),
Z3_OP_ZERO_EXT (1058), Z3_OP_ZERO_EXT (1058),
Z3_OP_ADD (518), Z3_OP_ADD (518),
Z3_OP_IS_INT (528), Z3_OP_IS_INT (528),
Z3_OP_BREDOR (1061), Z3_OP_BREDOR (1061),
Z3_OP_BNOT (1051), Z3_OP_BNOT (1051),
Z3_OP_BNOR (1054), Z3_OP_BNOR (1054),
Z3_OP_PR_CNF_STAR (1315), Z3_OP_PR_CNF_STAR (1315),
Z3_OP_RA_JOIN (1539), Z3_OP_RA_JOIN (1539),
Z3_OP_LE (514), Z3_OP_LE (514),
Z3_OP_SET_UNION (773), Z3_OP_SET_UNION (773),
Z3_OP_PR_UNDEF (1280), Z3_OP_PR_UNDEF (1280),
Z3_OP_BREDAND (1062), Z3_OP_BREDAND (1062),
Z3_OP_LT (516), Z3_OP_LT (516),
Z3_OP_RA_UNION (1540), Z3_OP_RA_UNION (1540),
Z3_OP_BADD (1028), Z3_OP_BADD (1028),
Z3_OP_BUREM0 (1039), Z3_OP_BUREM0 (1039),
Z3_OP_OEQ (267), Z3_OP_OEQ (267),
Z3_OP_PR_MODUS_PONENS (1284), Z3_OP_PR_MODUS_PONENS (1284),
Z3_OP_RA_CLONE (1548), Z3_OP_RA_CLONE (1548),
Z3_OP_REPEAT (1060), Z3_OP_REPEAT (1060),
Z3_OP_RA_NEGATION_FILTER (1544), Z3_OP_RA_NEGATION_FILTER (1544),
Z3_OP_BSMOD0 (1040), Z3_OP_BSMOD0 (1040),
Z3_OP_BLSHR (1065), Z3_OP_BLSHR (1065),
Z3_OP_BASHR (1066), Z3_OP_BASHR (1066),
Z3_OP_PR_UNIT_RESOLUTION (1304), Z3_OP_PR_UNIT_RESOLUTION (1304),
Z3_OP_ROTATE_RIGHT (1068), Z3_OP_ROTATE_RIGHT (1068),
Z3_OP_ARRAY_DEFAULT (772), Z3_OP_ARRAY_DEFAULT (772),
Z3_OP_PR_PULL_QUANT (1296), Z3_OP_PR_PULL_QUANT (1296),
Z3_OP_PR_APPLY_DEF (1310), Z3_OP_PR_APPLY_DEF (1310),
Z3_OP_PR_REWRITE_STAR (1295), Z3_OP_PR_REWRITE_STAR (1295),
Z3_OP_IDIV (523), Z3_OP_IDIV (523),
Z3_OP_PR_GOAL (1283), Z3_OP_PR_GOAL (1283),
Z3_OP_PR_IFF_TRUE (1305), Z3_OP_PR_IFF_TRUE (1305),
Z3_OP_LABEL_LIT (1793), Z3_OP_LABEL_LIT (1793),
Z3_OP_BOR (1050), Z3_OP_BOR (1050),
Z3_OP_PR_SYMMETRY (1286), Z3_OP_PR_SYMMETRY (1286),
Z3_OP_TRUE (256), Z3_OP_TRUE (256),
Z3_OP_SET_COMPLEMENT (776), Z3_OP_SET_COMPLEMENT (776),
Z3_OP_CONCAT (1056), Z3_OP_CONCAT (1056),
Z3_OP_PR_NOT_OR_ELIM (1293), Z3_OP_PR_NOT_OR_ELIM (1293),
Z3_OP_IFF (263), Z3_OP_IFF (263),
Z3_OP_BSHL (1064), Z3_OP_BSHL (1064),
Z3_OP_PR_TRANSITIVITY (1287), Z3_OP_PR_TRANSITIVITY (1287),
Z3_OP_SGT (1048), Z3_OP_SGT (1048),
Z3_OP_RA_WIDEN (1541), Z3_OP_RA_WIDEN (1541),
Z3_OP_PR_DEF_INTRO (1309), Z3_OP_PR_DEF_INTRO (1309),
Z3_OP_NOT (265), Z3_OP_NOT (265),
Z3_OP_PR_QUANT_INTRO (1290), Z3_OP_PR_QUANT_INTRO (1290),
Z3_OP_UGT (1047), Z3_OP_UGT (1047),
Z3_OP_DT_RECOGNISER (2049), Z3_OP_DT_RECOGNISER (2049),
Z3_OP_SET_INTERSECT (774), Z3_OP_SET_INTERSECT (774),
Z3_OP_BSREM (1033), Z3_OP_BSREM (1033),
Z3_OP_RA_STORE (1536), Z3_OP_RA_STORE (1536),
Z3_OP_SLT (1046), Z3_OP_SLT (1046),
Z3_OP_ROTATE_LEFT (1067), Z3_OP_ROTATE_LEFT (1067),
Z3_OP_PR_NNF_NEG (1313), Z3_OP_PR_NNF_NEG (1313),
Z3_OP_PR_REFLEXIVITY (1285), Z3_OP_PR_REFLEXIVITY (1285),
Z3_OP_ULEQ (1041), Z3_OP_ULEQ (1041),
Z3_OP_BIT1 (1025), Z3_OP_BIT1 (1025),
Z3_OP_BIT0 (1026), Z3_OP_BIT0 (1026),
Z3_OP_EQ (258), Z3_OP_EQ (258),
Z3_OP_BMUL (1030), Z3_OP_BMUL (1030),
Z3_OP_ARRAY_MAP (771), Z3_OP_ARRAY_MAP (771),
Z3_OP_STORE (768), Z3_OP_STORE (768),
Z3_OP_PR_HYPOTHESIS (1302), Z3_OP_PR_HYPOTHESIS (1302),
Z3_OP_RA_RENAME (1545), Z3_OP_RA_RENAME (1545),
Z3_OP_AND (261), Z3_OP_AND (261),
Z3_OP_TO_REAL (526), Z3_OP_TO_REAL (526),
Z3_OP_PR_NNF_POS (1312), Z3_OP_PR_NNF_POS (1312),
Z3_OP_PR_AND_ELIM (1292), Z3_OP_PR_AND_ELIM (1292),
Z3_OP_MOD (525), Z3_OP_MOD (525),
Z3_OP_BUDIV0 (1037), Z3_OP_BUDIV0 (1037),
Z3_OP_PR_TRUE (1281), Z3_OP_PR_TRUE (1281),
Z3_OP_BNAND (1053), Z3_OP_BNAND (1053),
Z3_OP_PR_ELIM_UNUSED_VARS (1299), Z3_OP_PR_ELIM_UNUSED_VARS (1299),
Z3_OP_RA_FILTER (1543), Z3_OP_RA_FILTER (1543),
Z3_OP_FD_LT (1549), Z3_OP_FD_LT (1549),
Z3_OP_RA_EMPTY (1537), Z3_OP_RA_EMPTY (1537),
Z3_OP_DIV (522), Z3_OP_DIV (522),
Z3_OP_ANUM (512), Z3_OP_ANUM (512),
Z3_OP_MUL (521), Z3_OP_MUL (521),
Z3_OP_UGEQ (1043), Z3_OP_UGEQ (1043),
Z3_OP_BSREM0 (1038), Z3_OP_BSREM0 (1038),
Z3_OP_PR_TH_LEMMA (1318), Z3_OP_PR_TH_LEMMA (1318),
Z3_OP_BXOR (1052), Z3_OP_BXOR (1052),
Z3_OP_DISTINCT (259), Z3_OP_DISTINCT (259),
Z3_OP_PR_IFF_FALSE (1306), Z3_OP_PR_IFF_FALSE (1306),
Z3_OP_BV2INT (1072), Z3_OP_BV2INT (1072),
Z3_OP_EXT_ROTATE_LEFT (1069), Z3_OP_EXT_ROTATE_LEFT (1069),
Z3_OP_PR_PULL_QUANT_STAR (1297), Z3_OP_PR_PULL_QUANT_STAR (1297),
Z3_OP_BSUB (1029), Z3_OP_BSUB (1029),
Z3_OP_PR_ASSERTED (1282), Z3_OP_PR_ASSERTED (1282),
Z3_OP_BXNOR (1055), Z3_OP_BXNOR (1055),
Z3_OP_EXTRACT (1059), Z3_OP_EXTRACT (1059),
Z3_OP_PR_DER (1300), Z3_OP_PR_DER (1300),
Z3_OP_DT_CONSTRUCTOR (2048), Z3_OP_DT_CONSTRUCTOR (2048),
Z3_OP_GT (517), Z3_OP_GT (517),
Z3_OP_BUREM (1034), Z3_OP_BUREM (1034),
Z3_OP_IMPLIES (266), Z3_OP_IMPLIES (266),
Z3_OP_SLEQ (1042), Z3_OP_SLEQ (1042),
Z3_OP_GE (515), Z3_OP_GE (515),
Z3_OP_BAND (1049), Z3_OP_BAND (1049),
Z3_OP_ITE (260), Z3_OP_ITE (260),
Z3_OP_AS_ARRAY (778), Z3_OP_AS_ARRAY (778),
Z3_OP_RA_SELECT (1547), Z3_OP_RA_SELECT (1547),
Z3_OP_CONST_ARRAY (770), Z3_OP_CONST_ARRAY (770),
Z3_OP_BSDIV (1031), Z3_OP_BSDIV (1031),
Z3_OP_OR (262), Z3_OP_OR (262),
Z3_OP_PR_HYPER_RESOLVE (1319), Z3_OP_PR_HYPER_RESOLVE (1319),
Z3_OP_AGNUM (513), Z3_OP_AGNUM (513),
Z3_OP_PR_PUSH_QUANT (1298), Z3_OP_PR_PUSH_QUANT (1298),
Z3_OP_BSMOD (1035), Z3_OP_BSMOD (1035),
Z3_OP_PR_IFF_OEQ (1311), Z3_OP_PR_IFF_OEQ (1311),
Z3_OP_PR_LEMMA (1303), Z3_OP_PR_LEMMA (1303),
Z3_OP_SET_SUBSET (777), Z3_OP_SET_SUBSET (777),
Z3_OP_SELECT (769), Z3_OP_SELECT (769),
Z3_OP_RA_PROJECT (1542), Z3_OP_RA_PROJECT (1542),
Z3_OP_BNEG (1027), Z3_OP_BNEG (1027),
Z3_OP_UMINUS (520), Z3_OP_UMINUS (520),
Z3_OP_REM (524), Z3_OP_REM (524),
Z3_OP_TO_INT (527), Z3_OP_TO_INT (527),
Z3_OP_PR_QUANT_INST (1301), Z3_OP_PR_QUANT_INST (1301),
Z3_OP_SGEQ (1044), Z3_OP_SGEQ (1044),
Z3_OP_POWER (529), Z3_OP_POWER (529),
Z3_OP_XOR3 (1074), Z3_OP_XOR3 (1074),
Z3_OP_RA_IS_EMPTY (1538), Z3_OP_RA_IS_EMPTY (1538),
Z3_OP_CARRY (1073), Z3_OP_CARRY (1073),
Z3_OP_DT_ACCESSOR (2050), Z3_OP_DT_ACCESSOR (2050),
Z3_OP_PR_TRANSITIVITY_STAR (1288), Z3_OP_PR_TRANSITIVITY_STAR (1288),
Z3_OP_PR_NNF_STAR (1314), Z3_OP_PR_NNF_STAR (1314),
Z3_OP_PR_COMMUTATIVITY (1307), Z3_OP_PR_COMMUTATIVITY (1307),
Z3_OP_ULT (1045), Z3_OP_ULT (1045),
Z3_OP_BSDIV0 (1036), Z3_OP_BSDIV0 (1036),
Z3_OP_SET_DIFFERENCE (775), Z3_OP_SET_DIFFERENCE (775),
Z3_OP_INT2BV (1071), Z3_OP_INT2BV (1071),
Z3_OP_XOR (264), Z3_OP_XOR (264),
Z3_OP_PR_MODUS_PONENS_OEQ (1317), Z3_OP_PR_MODUS_PONENS_OEQ (1317),
Z3_OP_BNUM (1024), Z3_OP_BNUM (1024),
Z3_OP_BUDIV (1032), Z3_OP_BUDIV (1032),
Z3_OP_PR_MONOTONICITY (1289), Z3_OP_PR_MONOTONICITY (1289),
Z3_OP_PR_DEF_AXIOM (1308), Z3_OP_PR_DEF_AXIOM (1308),
Z3_OP_FALSE (257), Z3_OP_FALSE (257),
Z3_OP_EXT_ROTATE_RIGHT (1070), Z3_OP_EXT_ROTATE_RIGHT (1070),
Z3_OP_PR_DISTRIBUTIVITY (1291), Z3_OP_PR_DISTRIBUTIVITY (1291),
Z3_OP_SIGN_EXT (1057), Z3_OP_SIGN_EXT (1057),
Z3_OP_PR_SKOLEMIZE (1316), Z3_OP_PR_SKOLEMIZE (1316),
Z3_OP_BCOMP (1063), Z3_OP_BCOMP (1063),
Z3_OP_RA_COMPLEMENT (1546), Z3_OP_RA_COMPLEMENT (1546);
private final int intValue;
Z3_decl_kind(int v) {
this.intValue = v;
}
public static final Z3_decl_kind fromInt(int v) {
for (Z3_decl_kind k: values())
if (k.intValue == v) return k;
return values()[0];
}
public final int toInt() { return this.intValue; }
} }

BIN
src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.class Normal file
View file

Binary file not shown.

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

@ -8,18 +8,32 @@ package com.Microsoft.Z3;
* Z3_error_code * Z3_error_code
**/ **/
public enum Z3_error_code { public enum Z3_error_code {
Z3_INVALID_PATTERN (6), Z3_INVALID_PATTERN (6),
Z3_MEMOUT_FAIL (7), Z3_MEMOUT_FAIL (7),
Z3_NO_PARSER (5), Z3_NO_PARSER (5),
Z3_OK (0), Z3_OK (0),
Z3_INVALID_ARG (3), Z3_INVALID_ARG (3),
Z3_EXCEPTION (12), Z3_EXCEPTION (12),
Z3_IOB (2), Z3_IOB (2),
Z3_INTERNAL_FATAL (9), Z3_INTERNAL_FATAL (9),
Z3_INVALID_USAGE (10), Z3_INVALID_USAGE (10),
Z3_FILE_ACCESS_ERROR (8), Z3_FILE_ACCESS_ERROR (8),
Z3_SORT_ERROR (1), Z3_SORT_ERROR (1),
Z3_PARSER_ERROR (4), Z3_PARSER_ERROR (4),
Z3_DEC_REF_ERROR (11), Z3_DEC_REF_ERROR (11);
private final int intValue;
Z3_error_code(int v) {
this.intValue = v;
}
public static final Z3_error_code fromInt(int v) {
for (Z3_error_code k: values())
if (k.intValue == v) return k;
return values()[0];
}
public final int toInt() { return this.intValue; }
} }

BIN
src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.class Normal file
View file

Binary file not shown.

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

@ -8,9 +8,23 @@ package com.Microsoft.Z3;
* Z3_goal_prec * Z3_goal_prec
**/ **/
public enum Z3_goal_prec { public enum Z3_goal_prec {
Z3_GOAL_UNDER (1), Z3_GOAL_UNDER (1),
Z3_GOAL_PRECISE (0), Z3_GOAL_PRECISE (0),
Z3_GOAL_UNDER_OVER (3), Z3_GOAL_UNDER_OVER (3),
Z3_GOAL_OVER (2), Z3_GOAL_OVER (2);
private final int intValue;
Z3_goal_prec(int v) {
this.intValue = v;
}
public static final Z3_goal_prec fromInt(int v) {
for (Z3_goal_prec k: values())
if (k.intValue == v) return k;
return values()[0];
}
public final int toInt() { return this.intValue; }
} }

BIN
src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.class Normal file
View file

Binary file not shown.

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

@ -8,8 +8,22 @@ package com.Microsoft.Z3;
* Z3_lbool * Z3_lbool
**/ **/
public enum Z3_lbool { public enum Z3_lbool {
Z3_L_TRUE (1), Z3_L_TRUE (1),
Z3_L_UNDEF (0), Z3_L_UNDEF (0),
Z3_L_FALSE (-1), Z3_L_FALSE (-1);
private final int intValue;
Z3_lbool(int v) {
this.intValue = v;
}
public static final Z3_lbool fromInt(int v) {
for (Z3_lbool k: values())
if (k.intValue == v) return k;
return values()[0];
}
public final int toInt() { return this.intValue; }
} }

BIN
src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.class Normal file
View file

Binary file not shown.

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

@ -8,12 +8,26 @@ package com.Microsoft.Z3;
* Z3_param_kind * Z3_param_kind
**/ **/
public enum Z3_param_kind { public enum Z3_param_kind {
Z3_PK_BOOL (1), Z3_PK_BOOL (1),
Z3_PK_SYMBOL (3), Z3_PK_SYMBOL (3),
Z3_PK_OTHER (5), Z3_PK_OTHER (5),
Z3_PK_INVALID (6), Z3_PK_INVALID (6),
Z3_PK_UINT (0), Z3_PK_UINT (0),
Z3_PK_STRING (4), Z3_PK_STRING (4),
Z3_PK_DOUBLE (2), Z3_PK_DOUBLE (2);
private final int intValue;
Z3_param_kind(int v) {
this.intValue = v;
}
public static final Z3_param_kind fromInt(int v) {
for (Z3_param_kind k: values())
if (k.intValue == v) return k;
return values()[0];
}
public final int toInt() { return this.intValue; }
} }

BIN
src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.class Normal file
View file

Binary file not shown.

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

@ -8,12 +8,26 @@ package com.Microsoft.Z3;
* Z3_parameter_kind * Z3_parameter_kind
**/ **/
public enum Z3_parameter_kind { public enum Z3_parameter_kind {
Z3_PARAMETER_FUNC_DECL (6), Z3_PARAMETER_FUNC_DECL (6),
Z3_PARAMETER_DOUBLE (1), Z3_PARAMETER_DOUBLE (1),
Z3_PARAMETER_SYMBOL (3), Z3_PARAMETER_SYMBOL (3),
Z3_PARAMETER_INT (0), Z3_PARAMETER_INT (0),
Z3_PARAMETER_AST (5), Z3_PARAMETER_AST (5),
Z3_PARAMETER_SORT (4), Z3_PARAMETER_SORT (4),
Z3_PARAMETER_RATIONAL (2), Z3_PARAMETER_RATIONAL (2);
private final int intValue;
Z3_parameter_kind(int v) {
this.intValue = v;
}
public static final Z3_parameter_kind fromInt(int v) {
for (Z3_parameter_kind k: values())
if (k.intValue == v) return k;
return values()[0];
}
public final int toInt() { return this.intValue; }
} }

BIN
src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.class Normal file
View file

Binary file not shown.

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

@ -8,15 +8,29 @@ package com.Microsoft.Z3;
* Z3_sort_kind * Z3_sort_kind
**/ **/
public enum Z3_sort_kind { public enum Z3_sort_kind {
Z3_BV_SORT (4), Z3_BV_SORT (4),
Z3_FINITE_DOMAIN_SORT (8), Z3_FINITE_DOMAIN_SORT (8),
Z3_ARRAY_SORT (5), Z3_ARRAY_SORT (5),
Z3_UNKNOWN_SORT (1000), Z3_UNKNOWN_SORT (1000),
Z3_RELATION_SORT (7), Z3_RELATION_SORT (7),
Z3_REAL_SORT (3), Z3_REAL_SORT (3),
Z3_INT_SORT (2), Z3_INT_SORT (2),
Z3_UNINTERPRETED_SORT (0), Z3_UNINTERPRETED_SORT (0),
Z3_BOOL_SORT (1), Z3_BOOL_SORT (1),
Z3_DATATYPE_SORT (6), Z3_DATATYPE_SORT (6);
private final int intValue;
Z3_sort_kind(int v) {
this.intValue = v;
}
public static final Z3_sort_kind fromInt(int v) {
for (Z3_sort_kind k: values())
if (k.intValue == v) return k;
return values()[0];
}
public final int toInt() { return this.intValue; }
} }

BIN
src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.class Normal file
View file

Binary file not shown.

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

@ -8,7 +8,21 @@ package com.Microsoft.Z3;
* Z3_symbol_kind * Z3_symbol_kind
**/ **/
public enum Z3_symbol_kind { public enum Z3_symbol_kind {
Z3_INT_SYMBOL (0), Z3_INT_SYMBOL (0),
Z3_STRING_SYMBOL (1), Z3_STRING_SYMBOL (1);
private final int intValue;
Z3_symbol_kind(int v) {
this.intValue = v;
}
public static final Z3_symbol_kind fromInt(int v) {
for (Z3_symbol_kind k: values())
if (k.intValue == v) return k;
return values()[0];
}
public final int toInt() { return this.intValue; }
} }

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

File diff suppressed because it is too large Load diff

3
src/api/java/com/Microsoft/Z3/FiniteDomainSort.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -30,7 +31,7 @@ import java.lang.Exception;
} }
FiniteDomainSort(Context ctx, Symbol name, long size) FiniteDomainSort(Context ctx, Symbol name, long size)
{ super(ctx, Native.mkFiniteDomainSort(ctx.nCtx(), name.NativeObject, size)); { super(ctx, Native.mkFiniteDomainSort(ctx.nCtx(), name.NativeObject(), size));

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -31,14 +32,14 @@ import java.lang.Exception;
public void setParameters(Params value) public void setParameters(Params value)
{ {
Context.CheckContextMatch(value); Context().CheckContextMatch(value);
Native.fixedpointSetParams(Context().nCtx(), NativeObject(), value.NativeObject); Native.fixedpointSetParams(Context().nCtx(), NativeObject(), value.NativeObject());
} }
/** /**
* Retrieves parameter descriptions for Fixedpoint solver. * Retrieves parameter descriptions for Fixedpoint solver.
**/ **/
public ParamDescrs ParameterDescriptions() { return new ParamDescrs(Context, Native.fixedpointGetParamDescrs(Context().nCtx(), NativeObject())); } public ParamDescrs ParameterDescriptions() { return new ParamDescrs(Context(), Native.fixedpointGetParamDescrs(Context().nCtx(), NativeObject())); }
/** /**
@ -49,10 +50,10 @@ import java.lang.Exception;
Context.CheckContextMatch(constraints); Context().CheckContextMatch(constraints);
for (Iterator a = constraints.iterator(); a.hasNext(); ) for (BoolExpr a: constraints)
{ {
Native.fixedpointAssert(Context().nCtx(), NativeObject(), a.NativeObject); Native.fixedpointAssert(Context().nCtx(), NativeObject(), a.NativeObject());
} }
} }
@ -63,8 +64,8 @@ import java.lang.Exception;
{ {
Context.CheckContextMatch(f); Context().CheckContextMatch(f);
Native.fixedpointRegisterRelation(Context().nCtx(), NativeObject(), f.NativeObject); Native.fixedpointRegisterRelation(Context().nCtx(), NativeObject(), f.NativeObject());
} }
/** /**
@ -74,20 +75,20 @@ import java.lang.Exception;
{ {
Context.CheckContextMatch(rule); Context().CheckContextMatch(rule);
Native.fixedpointAddRule(Context().nCtx(), NativeObject(), rule.NativeObject, AST.GetNativeObject(name)); Native.fixedpointAddRule(Context().nCtx(), NativeObject(), rule.NativeObject(), AST.GetNativeObject(name));
} }
/** /**
* Add table fact to the fixedpoint solver. * Add table fact to the fixedpoint solver.
**/ **/
public void AddFact(FuncDecl pred, long[] args) public void AddFact(FuncDecl pred, int[] args)
{ {
Context.CheckContextMatch(pred); Context().CheckContextMatch(pred);
Native.fixedpointAddFact(Context().nCtx(), NativeObject(), pred.NativeObject, (long)args.Length, args); Native.fixedpointAddFact(Context().nCtx(), NativeObject(), pred.NativeObject(), (int)args.length, args);
} }
/** /**
@ -100,12 +101,12 @@ import java.lang.Exception;
{ {
Context.CheckContextMatch(query); Context().CheckContextMatch(query);
Z3_lbool r = (Z3_lbool)Native.fixedpointQuery(Context().nCtx(), NativeObject(), query.NativeObject); Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(Context().nCtx(), NativeObject(), query.NativeObject()));
switch (r) switch (r)
{ {
case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE; case Z3_L_TRUE: return Status.SATISFIABLE;
case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE; case Z3_L_FALSE: return Status.UNSATISFIABLE;
default: return Status.UNKNOWN; default: return Status.UNKNOWN;
} }
} }
@ -121,13 +122,13 @@ import java.lang.Exception;
Context.CheckContextMatch(relations); Context().CheckContextMatch(relations);
Z3_lbool r = (Z3_lbool)Native.fixedpointQueryRelations(Context().nCtx(), NativeObject(), Z3_lbool r = (Z3_lbool)Native.fixedpointQueryRelations(Context().nCtx(), NativeObject(),
AST.ArrayLength(relations), AST.ArrayToNative(relations)); AST.ArrayLength(relations), AST.ArrayToNative(relations));
switch (r) switch (r)
{ {
case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE; case Z3_L_TRUE: return Status.SATISFIABLE;
case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE; case Z3_L_FALSE: return Status.UNSATISFIABLE;
default: return Status.UNKNOWN; default: return Status.UNKNOWN;
} }
} }
@ -159,8 +160,8 @@ import java.lang.Exception;
{ {
Context.CheckContextMatch(rule); Context().CheckContextMatch(rule);
Native.fixedpointUpdateRule(Context().nCtx(), NativeObject(), rule.NativeObject, AST.GetNativeObject(name)); Native.fixedpointUpdateRule(Context().nCtx(), NativeObject(), rule.NativeObject(), AST.GetNativeObject(name));
} }
/** /**
@ -170,7 +171,7 @@ import java.lang.Exception;
public Expr GetAnswer() public Expr GetAnswer()
{ {
long ans = Native.fixedpointGetAnswer(Context().nCtx(), NativeObject()); long ans = Native.fixedpointGetAnswer(Context().nCtx(), NativeObject());
return (ans == 0) ? null : Expr.Create(Context, ans); return (ans == 0) ? null : Expr.Create(Context(), ans);
} }
/** /**
@ -186,9 +187,9 @@ import java.lang.Exception;
/** /**
* Retrieve the number of levels explored for a given predicate. * Retrieve the number of levels explored for a given predicate.
**/ **/
public long GetNumLevels(FuncDecl predicate) public int GetNumLevels(FuncDecl predicate)
{ {
return Native.fixedpointGetNumLevels(Context().nCtx(), NativeObject(), predicate.NativeObject); return Native.fixedpointGetNumLevels(Context().nCtx(), NativeObject(), predicate.NativeObject());
} }
/** /**
@ -196,8 +197,8 @@ import java.lang.Exception;
**/ **/
public Expr GetCoverDelta(int level, FuncDecl predicate) public Expr GetCoverDelta(int level, FuncDecl predicate)
{ {
long res = Native.fixedpointGetCoverDelta(Context().nCtx(), NativeObject(), level, predicate.NativeObject); long res = Native.fixedpointGetCoverDelta(Context().nCtx(), NativeObject(), level, predicate.NativeObject());
return (res == 0) ? null : Expr.Create(Context, res); return (res == 0) ? null : Expr.Create(Context(), res);
} }
/** /**
@ -206,7 +207,7 @@ import java.lang.Exception;
**/ **/
public void AddCover(int level, FuncDecl predicate, Expr property) public void AddCover(int level, FuncDecl predicate, Expr property)
{ {
Native.fixedpointAddCover(Context().nCtx(), NativeObject(), level, predicate.NativeObject, property.NativeObject); Native.fixedpointAddCover(Context().nCtx(), NativeObject(), level, predicate.NativeObject(), property.NativeObject());
} }
/** /**
@ -225,7 +226,7 @@ import java.lang.Exception;
Native.fixedpointSetPredicateRepresentation(Context().nCtx(), NativeObject(), Native.fixedpointSetPredicateRepresentation(Context().nCtx(), NativeObject(),
f.NativeObject, AST.ArrayLength(kinds), Symbol.ArrayToNative(kinds)); f.NativeObject(), AST.ArrayLength(kinds), Symbol.ArrayToNative(kinds));
} }
@ -246,11 +247,11 @@ import java.lang.Exception;
{ {
ASTVector v = new ASTVector(Context, Native.fixedpointGetRules(Context().nCtx(), NativeObject())); ASTVector v = new ASTVector(Context(), Native.fixedpointGetRules(Context().nCtx(), NativeObject()));
long n = v.Size; int n = v.Size;
BoolExpr[] res = new BoolExpr[n]; BoolExpr[] res = new BoolExpr[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = new BoolExpr(Context, v[i].NativeObject); res[i] = new BoolExpr(Context(), v[i].NativeObject());
return res; return res;
} }
@ -261,11 +262,11 @@ import java.lang.Exception;
{ {
ASTVector v = new ASTVector(Context, Native.fixedpointGetAssertions(Context().nCtx(), NativeObject())); ASTVector v = new ASTVector(Context(), Native.fixedpointGetAssertions(Context().nCtx(), NativeObject()));
long n = v.Size; int n = v.Size;
BoolExpr[] res = new BoolExpr[n]; BoolExpr[] res = new BoolExpr[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = new BoolExpr(Context, v[i].NativeObject); res[i] = new BoolExpr(Context(), v[i].NativeObject());
return res; return res;
} }
@ -294,13 +295,13 @@ import java.lang.Exception;
void IncRef(long o) void IncRef(long o)
{ {
Context.Fixedpoint_DRQ.IncAndClear(Context, o); Context().Fixedpoint_DRQ().IncAndClear(Context(), o);
super.IncRef(o); super.IncRef(o);
} }
void DecRef(long o) void DecRef(long o)
{ {
Context.Fixedpoint_DRQ.Add(o); Context().Fixedpoint_DRQ().Add(o);
super.DecRef(o); super.DecRef(o);
} }
} }

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -56,18 +57,18 @@ import java.lang.Exception;
/** /**
* Returns a unique identifier for the function declaration. * Returns a unique identifier for the function declaration.
**/ **/
public long Id() { return Native.getFuncDeclId(Context().nCtx(), NativeObject()); } public int Id() { return Native.getFuncDeclId(Context().nCtx(), NativeObject()); }
/** /**
* The arity of the function declaration * The arity of the function declaration
**/ **/
public long Arity() { return Native.getArity(Context().nCtx(), NativeObject()); } public int Arity() { return Native.getArity(Context().nCtx(), NativeObject()); }
/** /**
* The size of the domain of the function declaration * The size of the domain of the function declaration
* <seealso cref="Arity"/> * <seealso cref="Arity"/>
**/ **/
public long DomainSize() { return Native.getDomainSize(Context().nCtx(), NativeObject()); } public int DomainSize() { return Native.getDomainSize(Context().nCtx(), NativeObject()); }
/** /**
* The domain of the function declaration * The domain of the function declaration
@ -79,8 +80,8 @@ import java.lang.Exception;
var n = DomainSize; var n = DomainSize;
Sort[] res = new Sort[n]; Sort[] res = new Sort[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = Sort.Create(Context, Native.getDomain(Context().nCtx(), NativeObject(), i)); res[i] = Sort.Create(Context(), Native.getDomain(Context().nCtx(), NativeObject(), i));
return res; return res;
} }
@ -90,13 +91,13 @@ import java.lang.Exception;
public Sort Range() public Sort Range()
{ {
return Sort.Create(Context, Native.getRange(Context().nCtx(), NativeObject())); return Sort.Create(Context(), Native.getRange(Context().nCtx(), NativeObject()));
} }
/** /**
* The kind of the function declaration. * The kind of the function declaration.
**/ **/
public Z3_decl_kind DeclKind() { return (Z3_decl_kind)Native.getDeclKind(Context().nCtx(), NativeObject()); } public Z3_decl_kind DeclKind() { return Z3_decl_kind.fromInt(Native.getDeclKind(Context().nCtx(), NativeObject())); }
/** /**
* The name of the function declaration * The name of the function declaration
@ -104,13 +105,13 @@ import java.lang.Exception;
public Symbol Name() public Symbol Name()
{ {
return Symbol.Create(Context, Native.getDeclName(Context().nCtx(), NativeObject())); return Symbol.Create(Context(), Native.getDeclName(Context().nCtx(), NativeObject()));
} }
/** /**
* The number of parameters of the function declaration * The number of parameters of the function declaration
**/ **/
public long NumParameters() { return Native.getDeclNumParameters(Context().nCtx(), NativeObject()); } public int NumParameters() { return Native.getDeclNumParameters(Context().nCtx(), NativeObject()); }
/** /**
* The parameters of the function declaration * The parameters of the function declaration
@ -119,32 +120,32 @@ import java.lang.Exception;
{ {
long num = NumParameters; int num = NumParameters();
Parameter[] res = new Parameter[num]; Parameter[] res = new Parameter[num];
for (long i; i < num; i++) for (int i = 0; i < num; i++)
{ {
Z3_parameter_kind k = (Z3_parameter_kind)Native.getDeclParameterKind(Context().nCtx(), NativeObject(), i); Z3_parameter_kind k = Z3_parameter_kind.fromInt(Native.getDeclParameterKind(Context().nCtx(), NativeObject(), i));
switch (k) switch (k)
{ {
case Z3_parameter_kind.Z3_PARAMETER_INT: case Z3_PARAMETER_INT:
res[i] = new Parameter(k, Native.getDeclIntParameter(Context().nCtx(), NativeObject(), i)); res[i] = new Parameter(k, Native.getDeclIntParameter(Context().nCtx(), NativeObject(), i));
break; break;
case Z3_parameter_kind.Z3_PARAMETER_DOUBLE: case Z3_PARAMETER_DOUBLE:
res[i] = new Parameter(k, Native.getDeclDoubleParameter(Context().nCtx(), NativeObject(), i)); res[i] = new Parameter(k, Native.getDeclDoubleParameter(Context().nCtx(), NativeObject(), i));
break; break;
case Z3_parameter_kind.Z3_PARAMETER_SYMBOL: case Z3_PARAMETER_SYMBOL:
res[i] = new Parameter(k, Symbol.Create(Context, Native.getDeclSymbolParameter(Context().nCtx(), NativeObject(), i))); res[i] = new Parameter(k, Symbol.Create(Context(), Native.getDeclSymbolParameter(Context().nCtx(), NativeObject(), i)));
break; break;
case Z3_parameter_kind.Z3_PARAMETER_SORT: case Z3_PARAMETER_SORT:
res[i] = new Parameter(k, Sort.Create(Context, Native.getDeclSortParameter(Context().nCtx(), NativeObject(), i))); res[i] = new Parameter(k, Sort.Create(Context(), Native.getDeclSortParameter(Context().nCtx(), NativeObject(), i)));
break; break;
case Z3_parameter_kind.Z3_PARAMETER_AST: case Z3_PARAMETER_AST:
res[i] = new Parameter(k, new AST(Context, Native.getDeclAstParameter(Context().nCtx(), NativeObject(), i))); res[i] = new Parameter(k, new AST(Context(), Native.getDeclAstParameter(Context().nCtx(), NativeObject(), i)));
break; break;
case Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL: case Z3_PARAMETER_FUNC_DECL:
res[i] = new Parameter(k, new FuncDecl(Context, Native.getDeclFuncDeclParameter(Context().nCtx(), NativeObject(), i))); res[i] = new Parameter(k, new FuncDecl(Context(), Native.getDeclFuncDeclParameter(Context().nCtx(), NativeObject(), i)));
break; break;
case Z3_parameter_kind.Z3_PARAMETER_RATIONAL: case Z3_PARAMETER_RATIONAL:
res[i] = new Parameter(k, Native.getDeclRationalParameter(Context().nCtx(), NativeObject(), i)); res[i] = new Parameter(k, Native.getDeclRationalParameter(Context().nCtx(), NativeObject(), i));
break; break;
default: default:
@ -244,21 +245,21 @@ import java.lang.Exception;
} }
FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range) FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
{ super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject)); { super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.NativeObject(), AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject()));
} }
FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range) FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range)
{ super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject)); { super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject()));
} }
void CheckNativeObject(long obj) void CheckNativeObject(long obj)
{ {
if (Native.getAstKind(Context().nCtx(), obj) != (long)Z3_ast_kind.Z3_FUNC_DECL_AST) if (Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_FUNC_DECL_AST.toInt())
throw new Z3Exception("Underlying object is not a function declaration"); throw new Z3Exception("Underlying object is not a function declaration");
super.CheckNativeObject(obj); super.CheckNativeObject(obj);
} }
@ -279,8 +280,8 @@ import java.lang.Exception;
{ {
Context.CheckContextMatch(args); Context().CheckContextMatch(args);
return Expr.Create(Context, this, args); return Expr.Create(Context(), this, args);
} }
} }

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -28,13 +29,13 @@ import java.lang.Exception;
public Expr Value() public Expr Value()
{ {
return Expr.Create(Context, Native.funcEntryGetValue(Context().nCtx(), NativeObject())); return Expr.Create(Context(), Native.funcEntryGetValue(Context().nCtx(), NativeObject()));
} }
/** /**
* The number of arguments of the entry. * The number of arguments of the entry.
**/ **/
public long NumArgs() { return Native.funcEntryGetNumArgs(Context().nCtx(), NativeObject()); } public int NumArgs() { return Native.funcEntryGetNumArgs(Context().nCtx(), NativeObject()); }
/** /**
* The arguments of the function entry. * The arguments of the function entry.
@ -44,10 +45,10 @@ import java.lang.Exception;
long n = NumArgs; int n = NumArgs();
Expr[] res = new Expr[n]; Expr[] res = new Expr[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = Expr.Create(Context, Native.funcEntryGetArg(Context().nCtx(), NativeObject(), i)); res[i] = Expr.Create(Context(), Native.funcEntryGetArg(Context().nCtx(), NativeObject(), i));
return res; return res;
} }
@ -56,10 +57,10 @@ import java.lang.Exception;
**/ **/
public String toString() public String toString()
{ {
long n = NumArgs; int n = NumArgs();
String res = "["; String res = "[";
Expr[] args = Args; Expr[] args = Args;
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res += args[i] + ", "; res += args[i] + ", ";
return res + Value + "]"; return res + Value + "]";
} }
@ -81,13 +82,13 @@ import java.lang.Exception;
void IncRef(long o) void IncRef(long o)
{ {
Context.FuncEntry_DRQ.IncAndClear(Context, o); Context().FuncEntry_DRQ().IncAndClear(Context(), o);
super.IncRef(o); super.IncRef(o);
} }
void DecRef(long o) void DecRef(long o)
{ {
Context.FuncEntry_DRQ.Add(o); Context().FuncEntry_DRQ().Add(o);
super.DecRef(o); super.DecRef(o);
} }
}; };
@ -95,7 +96,7 @@ import java.lang.Exception;
/** /**
* The number of entries in the function interpretation. * The number of entries in the function interpretation.
**/ **/
public long NumEntries() { return Native.funcInterpGetNumEntries(Context().nCtx(), NativeObject()); } public int NumEntries() { return Native.funcInterpGetNumEntries(Context().nCtx(), NativeObject()); }
/** /**
* The entries in the function interpretation * The entries in the function interpretation
@ -105,10 +106,10 @@ import java.lang.Exception;
long n = NumEntries; int n = NumEntries();
Entry[] res = new Entry[n]; Entry[] res = new Entry[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = new Entry(Context, Native.funcInterpGetEntry(Context().nCtx(), NativeObject(), i)); res[i] = new Entry(Context(), Native.funcInterpGetEntry(Context().nCtx(), NativeObject(), i));
return res; return res;
} }
@ -119,13 +120,13 @@ import java.lang.Exception;
{ {
return Expr.Create(Context, Native.funcInterpGetElse(Context().nCtx(), NativeObject())); return Expr.Create(Context(), Native.funcInterpGetElse(Context().nCtx(), NativeObject()));
} }
/** /**
* The arity of the function interpretation * The arity of the function interpretation
**/ **/
public long Arity() { return Native.funcInterpGetArity(Context().nCtx(), NativeObject()); } public int Arity() { return Native.funcInterpGetArity(Context().nCtx(), NativeObject()); }
/** /**
* A string representation of the function interpretation. * A string representation of the function interpretation.
@ -134,12 +135,12 @@ import java.lang.Exception;
{ {
String res = ""; String res = "";
res += "["; res += "[";
for (Iterator e = Entries.iterator(); e.hasNext(); ) for (Entry e: Entries)
{ {
long n = e.NumArgs; int n = e.NumArgs;
if (n > 1) res += "["; if (n > 1) res += "[";
Expr[] args = e.Args; Expr[] args = e.Args;
for (long i; i < n; i++) for (int i = 0; i < n; i++)
{ {
if (i != 0) res += ", "; if (i != 0) res += ", ";
res += args[i]; res += args[i];
@ -172,13 +173,13 @@ import java.lang.Exception;
void IncRef(long o) void IncRef(long o)
{ {
Context.FuncInterp_DRQ.IncAndClear(Context, o); Context().FuncInterp_DRQ().IncAndClear(Context(), o);
super.IncRef(o); super.IncRef(o);
} }
void DecRef(long o) void DecRef(long o)
{ {
Context.FuncInterp_DRQ.Add(o); Context().FuncInterp_DRQ().Add(o);
super.DecRef(o); super.DecRef(o);
} }
} }

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -25,7 +26,7 @@ import java.lang.Exception;
* An over approximation is applied when the objective is to find a proof for a given goal. * An over approximation is applied when the objective is to find a proof for a given goal.
* </remarks> * </remarks>
**/ **/
public Z3_goal_prec Precision() { return (Z3_goal_prec)Native.goalPrecision(Context().nCtx(), NativeObject()); } public Z3_goal_prec Precision() { return Z3_goal_prec.fromInt(Native.goalPrecision(Context().nCtx(), NativeObject())); }
/** /**
* Indicates whether the goal is precise. * Indicates whether the goal is precise.
@ -54,18 +55,18 @@ import java.lang.Exception;
Context.CheckContextMatch(constraints); Context().CheckContextMatch(constraints);
for (Iterator c = constraints.iterator(); c.hasNext(); ) for (BoolExpr c: constraints)
{ {
// It was an assume, now made an assert just to be sure we do not regress // It was an assume, now made an assert just to be sure we do not regress
Native.goalAssert(Context().nCtx(), NativeObject(), c.NativeObject); Native.goalAssert(Context().nCtx(), NativeObject(), c.NativeObject());
} }
} }
/** /**
* Indicates whether the goal contains `false'. * Indicates whether the goal contains `false'.
**/ **/
public boolean Inconsistent() { return Native.goalInconsistent(Context().nCtx(), NativeObject()) != 0; } public boolean Inconsistent() { return Native.goalInconsistent(Context().nCtx(), NativeObject()) ; }
/** /**
* The depth of the goal. * The depth of the goal.
@ -73,7 +74,7 @@ import java.lang.Exception;
* This tracks how many transformations were applied to it. * This tracks how many transformations were applied to it.
* </remarks> * </remarks>
**/ **/
public long Depth() { return Native.goalDepth(Context().nCtx(), NativeObject()); } public int Depth() { return Native.goalDepth(Context().nCtx(), NativeObject()); }
/** /**
* Erases all formulas from the given goal. * Erases all formulas from the given goal.
@ -86,7 +87,7 @@ import java.lang.Exception;
/** /**
* The number of formulas in the goal. * The number of formulas in the goal.
**/ **/
public long Size() { return Native.goalSize(Context().nCtx(), NativeObject()); } public int Size() { return Native.goalSize(Context().nCtx(), NativeObject()); }
/** /**
* The formulas in the goal. * The formulas in the goal.
@ -95,27 +96,27 @@ import java.lang.Exception;
{ {
long n = Size; int n = Size;
BoolExpr[] res = new BoolExpr[n]; BoolExpr[] res = new BoolExpr[n];
for (long i; 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));
return res; return res;
} }
/** /**
* The number of formulas, subformulas and terms in the goal. * The number of formulas, subformulas and terms in the goal.
**/ **/
public long NumExprs() { return Native.goalNumExprs(Context().nCtx(), NativeObject()); } public int NumExprs() { return Native.goalNumExprs(Context().nCtx(), NativeObject()); }
/** /**
* Indicates whether the goal is empty, and it is precise or the product of an under approximation. * Indicates whether the goal is empty, and it is precise or the product of an under approximation.
**/ **/
public boolean IsDecidedSat() { return Native.goalIsDecidedSat(Context().nCtx(), NativeObject()) != 0; } public boolean IsDecidedSat() { return Native.goalIsDecidedSat(Context().nCtx(), NativeObject()) ; }
/** /**
* Indicates whether the goal contains `false', and it is precise or the product of an over approximation. * Indicates whether the goal contains `false', and it is precise or the product of an over approximation.
**/ **/
public boolean IsDecidedUnsat() { return Native.goalIsDecidedUnsat(Context().nCtx(), NativeObject()) != 0; } public boolean IsDecidedUnsat() { return Native.goalIsDecidedUnsat(Context().nCtx(), NativeObject()) ; }
/** /**
* Translates (copies) the Goal to the target Context <paramref name="ctx"/>. * Translates (copies) the Goal to the target Context <paramref name="ctx"/>.
@ -133,11 +134,11 @@ import java.lang.Exception;
**/ **/
public Goal Simplify(Params p) public Goal Simplify(Params p)
{ {
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(); return Context().MkGoal();
else else
return res.Subgoals[0]; return res.Subgoals[0];
} }
@ -154,7 +155,7 @@ import java.lang.Exception;
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) ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0)); { super(ctx, Native.mkGoal(ctx.nCtx(), (models) ? true : false, (unsatCores) ? true : false, (proofs) ? true : false));
} }
@ -173,13 +174,13 @@ import java.lang.Exception;
void IncRef(long o) void IncRef(long o)
{ {
Context.Goal_DRQ.IncAndClear(Context, o); Context().Goal_DRQ().IncAndClear(Context(), o);
super.IncRef(o); super.IncRef(o);
} }
void DecRef(long o) void DecRef(long o)
{ {
Context.Goal_DRQ.Add(o); Context().Goal_DRQ().Add(o);
super.DecRef(o); super.DecRef(o);
} }

13
src/api/java/com/Microsoft/Z3/IDecRefQueue.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Collections; */ /* using System.Collections; */
@ -23,8 +24,8 @@ import java.lang.Exception;
protected Object m_lock = new Object(); protected Object m_lock = new Object();
protected List<Long> m_queue = new List<Long>(); protected LinkedList<Long> m_queue = new LinkedList<Long>();
final long m_move_limit = 1024; final int m_move_limit = 1024;
public abstract void IncRef(Context ctx, long obj); public abstract void IncRef(Context ctx, long obj);
public abstract void DecRef(Context ctx, long obj); public abstract void DecRef(Context ctx, long obj);
@ -34,7 +35,7 @@ import java.lang.Exception;
IncRef(ctx, o); IncRef(ctx, o);
if (m_queue.Count >= m_move_limit) Clear(ctx); if (m_queue.size() >= m_move_limit) Clear(ctx);
} }
public void Add(long o) public void Add(long o)
@ -43,7 +44,7 @@ import java.lang.Exception;
synchronized (m_lock) synchronized (m_lock)
{ {
m_queue.Add(o); m_queue.add(o);
} }
} }
@ -53,9 +54,9 @@ import java.lang.Exception;
synchronized (m_lock) synchronized (m_lock)
{ {
for (Iterator o = m_queue.iterator(); o.hasNext(); ) for (Long o: m_queue)
DecRef(ctx, o); DecRef(ctx, o);
m_queue.Clear(); m_queue.clear();
} }
} }
} }

1
src/api/java/com/Microsoft/Z3/IntExpr.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Collections.Generic; */ /* using System.Collections.Generic; */
/* using System.Linq; */ /* using System.Linq; */

17
src/api/java/com/Microsoft/Z3/IntNum.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Numerics; */ /* using System.Numerics; */
@ -29,7 +30,7 @@ import java.lang.Exception;
public long UInt64() public long UInt64()
{ {
long res = 0; long res = 0;
if (Native.getNumeralLong64(Context().nCtx(), NativeObject(), res) == 0) if (Native.getNumeralInt64(Context().nCtx(), NativeObject(), res) ^ true)
throw new Z3Exception("Numeral is not a 64 bit unsigned"); throw new Z3Exception("Numeral is not a 64 bit unsigned");
return res; return res;
} }
@ -40,7 +41,7 @@ import java.lang.Exception;
public int Int() public int Int()
{ {
int res = 0; int res = 0;
if (Native.getNumeralInt(Context().nCtx(), NativeObject(), res) == 0) if (Native.getNumeralInt(Context().nCtx(), NativeObject(), res) ^ true)
throw new Z3Exception("Numeral is not an int"); throw new Z3Exception("Numeral is not an int");
return res; return res;
} }
@ -51,7 +52,7 @@ import java.lang.Exception;
public long Int64() public long Int64()
{ {
long res = 0; long res = 0;
if (Native.getNumeralInt64(Context().nCtx(), NativeObject(), res) == 0) if (Native.getNumeralInt64(Context().nCtx(), NativeObject(), res) ^ true)
throw new Z3Exception("Numeral is not an int64"); throw new Z3Exception("Numeral is not an int64");
return res; return res;
} }
@ -59,11 +60,11 @@ import java.lang.Exception;
/** /**
* Retrieve the int value. * Retrieve the int value.
**/ **/
public long UInt() public int UInt()
{ {
long res = 0; int res = 0;
if (Native.getNumeralLong(Context().nCtx(), NativeObject(), res) == 0) if (Native.getNumeralInt(Context().nCtx(), NativeObject(), res) ^ true)
throw new Z3Exception("Numeral is not a long"); throw new Z3Exception("Numeral is not a int");
return res; return res;
} }
@ -72,7 +73,7 @@ import java.lang.Exception;
**/ **/
public BigInteger BigInteger() public BigInteger BigInteger()
{ {
return BigInteger.Parse(this.ToString()); return new BigInteger(this.toString());
} }
/** /**

1
src/api/java/com/Microsoft/Z3/IntSort.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Runtime.InteropServices; */ /* using System.Runtime.InteropServices; */

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -109,7 +110,7 @@ import java.lang.Exception;
ihead = 0, ihead = 0,
itail = 0; itail = 0;
NativeObject() = Native.mkListSort(ctx.nCtx(), name.NativeObject, elemSort.NativeObject, NativeObject() = 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);

1
src/api/java/com/Microsoft/Z3/Log.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -24,7 +25,7 @@ import java.lang.Exception;
{ {
Context.CheckContextMatch(a); Context().CheckContextMatch(a);
return ConstInterp(a.FuncDecl); return ConstInterp(a.FuncDecl);
} }
@ -37,16 +38,16 @@ import java.lang.Exception;
{ {
Context.CheckContextMatch(f); Context().CheckContextMatch(f);
if (f.Arity != 0 || if (f.Arity != 0 ||
Native.getSortKind(Context().nCtx(), Native.getRange(Context().nCtx(), f.NativeObject)) == (long)Z3_sort_kind.Z3_ARRAY_SORT) 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.");
long n = Native.modelGetConstInterp(Context().nCtx(), NativeObject(), f.NativeObject); long n = Native.modelGetConstInterp(Context().nCtx(), NativeObject(), f.NativeObject());
if (n == 0) if (n == 0)
return null; return null;
else else
return Expr.Create(Context, n); return Expr.Create(Context(), n);
} }
/** /**
@ -58,13 +59,13 @@ import java.lang.Exception;
{ {
Context.CheckContextMatch(f); Context().CheckContextMatch(f);
Z3_sort_kind sk = (Z3_sort_kind)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());
if (sk == Z3_sort_kind.Z3_ARRAY_SORT) if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
{ {
@ -72,10 +73,10 @@ import java.lang.Exception;
return null; return null;
else else
{ {
if (Native.isAsArray(Context().nCtx(), n) == 0) if (Native.isAsArray(Context().nCtx(), n) ^ true)
throw new Z3Exception("Argument was not an array constant"); throw new Z3Exception("Argument was not an array constant");
long fd = Native.getAsArrayFuncDecl(Context().nCtx(), n); long fd = Native.getAsArrayFuncDecl(Context().nCtx(), n);
return FuncInterp(new FuncDecl(Context, fd)); return FuncInterp(new FuncDecl(Context(), fd));
} }
} }
else else
@ -85,18 +86,18 @@ import java.lang.Exception;
} }
else else
{ {
long n = Native.modelGetFuncInterp(Context().nCtx(), NativeObject(), f.NativeObject); long n = Native.modelGetFuncInterp(Context().nCtx(), NativeObject(), f.NativeObject());
if (n == 0) if (n == 0)
return null; return null;
else else
return new FuncInterp(Context, n); return new FuncInterp(Context(), n);
} }
} }
/** /**
* The number of constants that have an interpretation in the model. * The number of constants that have an interpretation in the model.
**/ **/
public long NumConsts() { return Native.modelGetNumConsts(Context().nCtx(), NativeObject()); } public int NumConsts() { return Native.modelGetNumConsts(Context().nCtx(), NativeObject()); }
/** /**
* The function declarations of the constants in the model. * The function declarations of the constants in the model.
@ -105,17 +106,17 @@ import java.lang.Exception;
{ {
long n = NumConsts; int n = NumConsts();
FuncDecl[] res = new FuncDecl[n]; FuncDecl[] res = new FuncDecl[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.modelGetConstDecl(Context().nCtx(), NativeObject(), i)); res[i] = new FuncDecl(Context(), Native.modelGetConstDecl(Context().nCtx(), NativeObject(), i));
return res; return res;
} }
/** /**
* The number of function interpretations in the model. * The number of function interpretations in the model.
**/ **/
public long NumFuncs() { return Native.modelGetNumFuncs(Context().nCtx(), NativeObject()); } public int NumFuncs() { return Native.modelGetNumFuncs(Context().nCtx(), NativeObject()); }
/** /**
* The function declarations of the function interpretations in the model. * The function declarations of the function interpretations in the model.
@ -124,10 +125,10 @@ import java.lang.Exception;
{ {
long n = NumFuncs; int n = NumFuncs();
FuncDecl[] res = new FuncDecl[n]; FuncDecl[] res = new FuncDecl[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.modelGetFuncDecl(Context().nCtx(), NativeObject(), i)); res[i] = new FuncDecl(Context(), Native.modelGetFuncDecl(Context().nCtx(), NativeObject(), i));
return res; return res;
} }
@ -138,14 +139,14 @@ import java.lang.Exception;
{ {
var nFuncs = NumFuncs; var nFuncs = NumFuncs();
var nConsts = NumConsts; var nConsts = NumConsts();
long n = nFuncs + nConsts; int n = nFuncs + nConsts;
FuncDecl[] res = new FuncDecl[n]; FuncDecl[] res = new FuncDecl[n];
for (long i; i < nConsts; i++) for (int i = 0; i < nConsts; i++)
res[i] = new FuncDecl(Context, Native.modelGetConstDecl(Context().nCtx(), NativeObject(), i)); res[i] = new FuncDecl(Context(), Native.modelGetConstDecl(Context().nCtx(), NativeObject(), i));
for (long i; i < nFuncs; i++) for (int i = 0; i < nFuncs; i++)
res[nConsts + i] = new FuncDecl(Context, Native.modelGetFuncDecl(Context().nCtx(), NativeObject(), i)); res[nConsts + i] = new FuncDecl(Context(), Native.modelGetFuncDecl(Context().nCtx(), NativeObject(), i));
return res; return res;
} }
@ -180,10 +181,10 @@ import java.lang.Exception;
long v = 0; long v = 0;
if (Native.modelEval(Context().nCtx(), NativeObject(), t.NativeObject, (completion) ? 1 : 0, v) == 0) if (Native.modelEval(Context().nCtx(), NativeObject(), t.NativeObject(), (completion) ? true : false, v) ^ true)
throw new ModelEvaluationFailedException(); throw new ModelEvaluationFailedException();
else else
return Expr.Create(Context, v); return Expr.Create(Context(), v);
} }
/** /**
@ -200,7 +201,7 @@ import java.lang.Exception;
/** /**
* The number of uninterpreted sorts that the model has an interpretation for. * The number of uninterpreted sorts that the model has an interpretation for.
**/ **/
public long NumSorts () { return Native.modelGetNumSorts(Context().nCtx(), NativeObject()); } public int NumSorts () { return Native.modelGetNumSorts(Context().nCtx(), NativeObject()); }
/** /**
* The uninterpreted sorts that the model has an interpretation for. * The uninterpreted sorts that the model has an interpretation for.
@ -216,10 +217,10 @@ import java.lang.Exception;
{ {
long n = NumSorts; int n = NumSorts();
Sort[] res = new Sort[n]; Sort[] res = new Sort[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = Sort.Create(Context, Native.modelGetSort(Context().nCtx(), NativeObject(), i)); res[i] = Sort.Create(Context(), Native.modelGetSort(Context().nCtx(), NativeObject(), i));
return res; return res;
} }
@ -234,11 +235,11 @@ import java.lang.Exception;
ASTVector nUniv = new ASTVector(Context, Native.modelGetSortUniverse(Context().nCtx(), NativeObject(), s.NativeObject)); ASTVector nUniv = new ASTVector(Context(), Native.modelGetSortUniverse(Context().nCtx(), NativeObject(), s.NativeObject()));
long n = nUniv.Size; int n = nUniv.Size;
Expr[] res = new Expr[n]; Expr[] res = new Expr[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = Expr.Create(Context, nUniv[i].NativeObject); res[i] = Expr.Create(Context(), nUniv[i].NativeObject());
return res; return res;
} }
@ -271,13 +272,13 @@ import java.lang.Exception;
void IncRef(long o) void IncRef(long o)
{ {
Context.Model_DRQ.IncAndClear(Context, o); Context().Model_DRQ().IncAndClear(Context(), o);
super.IncRef(o); super.IncRef(o);
} }
void DecRef(long o) void DecRef(long o)
{ {
Context.Model_DRQ.Add(o); Context().Model_DRQ().Add(o);
super.DecRef(o); super.DecRef(o);
} }
} }

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

@ -4,8 +4,8 @@ public final class Native {
public static class IntPtr { public int value; } public static class IntPtr { public int value; }
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 static class errorHandler { public long ptr; }
static { System.loadLibrary("<mk_util.JavaDLLComponent instance at 0x0236D8F0>"); } static { System.loadLibrary("<mk_util.JavaDLLComponent instance at 0x0235B918>"); }
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);

17
src/api/java/com/Microsoft/Z3/ParamDescrs.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -21,7 +22,7 @@ import java.lang.Exception;
public void Validate(Params p) public void Validate(Params p)
{ {
Native.paramsValidate(Context().nCtx(), p.NativeObject, NativeObject()); Native.paramsValidate(Context().nCtx(), p.NativeObject(), NativeObject());
} }
/** /**
@ -30,7 +31,7 @@ import java.lang.Exception;
public Z3_param_kind GetKind(Symbol name) public Z3_param_kind GetKind(Symbol name)
{ {
return (Z3_param_kind)Native.paramDescrsGetKind(Context().nCtx(), NativeObject(), name.NativeObject); return Z3_param_kind.fromInt(Native.paramDescrsGetKind(Context().nCtx(), NativeObject(), name.NativeObject()));
} }
/** /**
@ -38,10 +39,10 @@ import java.lang.Exception;
**/ **/
public Symbol[] Names() public Symbol[] Names()
{ {
long sz = Native.paramDescrsSize(Context().nCtx(), NativeObject()); int sz = Native.paramDescrsSize(Context().nCtx(), NativeObject());
Symbol[] names = new Symbol[sz]; Symbol[] names = new Symbol[sz];
for (long i; i < sz; ++i) { for (int i = 0; i < sz; ++i) {
names[i] = Symbol.Create(Context, Native.paramDescrsGetName(Context().nCtx(), NativeObject(), i)); names[i] = Symbol.Create(Context(), Native.paramDescrsGetName(Context().nCtx(), NativeObject(), i));
} }
return names; return names;
} }
@ -49,7 +50,7 @@ import java.lang.Exception;
/** /**
* The size of the ParamDescrs. * The size of the ParamDescrs.
**/ **/
public long Size() { return Native.paramDescrsSize(Context().nCtx(), NativeObject()); } public int Size() { return Native.paramDescrsSize(Context().nCtx(), NativeObject()); }
/** /**
* Retrieves a string representation of the ParamDescrs. * Retrieves a string representation of the ParamDescrs.
@ -79,13 +80,13 @@ import java.lang.Exception;
void IncRef(long o) void IncRef(long o)
{ {
Context.ParamDescrs_DRQ.IncAndClear(Context, o); Context().ParamDescrs_DRQ().IncAndClear(Context(), o);
super.IncRef(o); super.IncRef(o);
} }
void DecRef(long o) void DecRef(long o)
{ {
Context.ParamDescrs_DRQ.Add(o); Context().ParamDescrs_DRQ().Add(o);
super.DecRef(o); super.DecRef(o);
} }
} }

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -22,17 +23,17 @@ import java.lang.Exception;
{ {
Native.paramsSetBool(Context().nCtx(), NativeObject(), name.NativeObject, (value) ? 1 : 0); Native.paramsSetBool(Context().nCtx(), NativeObject(), name.NativeObject(), (value) ? true : false);
} }
/** /**
* Adds a parameter setting. * Adds a parameter setting.
**/ **/
public void Add(Symbol name, long value) public void Add(Symbol name, int value)
{ {
Native.paramsSetLong(Context().nCtx(), NativeObject(), name.NativeObject, value); Native.paramsSetInt(Context().nCtx(), NativeObject(), name.NativeObject(), value);
} }
/** /**
@ -42,7 +43,7 @@ import java.lang.Exception;
{ {
Native.paramsSetDouble(Context().nCtx(), NativeObject(), name.NativeObject, value); Native.paramsSetDouble(Context().nCtx(), NativeObject(), name.NativeObject(), value);
} }
/** /**
@ -53,7 +54,7 @@ import java.lang.Exception;
Native.paramsSetSymbol(Context().nCtx(), NativeObject(), name.NativeObject, value.NativeObject); Native.paramsSetSymbol(Context().nCtx(), NativeObject(), name.NativeObject(), value.NativeObject());
} }
/** /**
@ -61,15 +62,15 @@ import java.lang.Exception;
**/ **/
public void Add(String name, boolean value) public void Add(String name, boolean value)
{ {
Native.paramsSetBool(Context().nCtx(), NativeObject(), Context.MkSymbol(name).NativeObject, (value) ? 1 : 0); Native.paramsSetBool(Context().nCtx(), NativeObject(), Context().MkSymbol(name).NativeObject(), (value) ? true : false);
} }
/** /**
* Adds a parameter setting. * Adds a parameter setting.
**/ **/
public void Add(String name, long value) public void Add(String name, int value)
{ {
Native.paramsSetLong(Context().nCtx(), NativeObject(), Context.MkSymbol(name).NativeObject, value); Native.paramsSetInt(Context().nCtx(), NativeObject(), Context().MkSymbol(name).NativeObject(), value);
} }
/** /**
@ -77,7 +78,7 @@ import java.lang.Exception;
**/ **/
public void Add(String name, double value) public void Add(String name, double value)
{ {
Native.paramsSetDouble(Context().nCtx(), NativeObject(), Context.MkSymbol(name).NativeObject, value); Native.paramsSetDouble(Context().nCtx(), NativeObject(), Context().MkSymbol(name).NativeObject(), value);
} }
/** /**
@ -87,7 +88,7 @@ import java.lang.Exception;
{ {
Native.paramsSetSymbol(Context().nCtx(), NativeObject(), Context.MkSymbol(name).NativeObject, value.NativeObject); Native.paramsSetSymbol(Context().nCtx(), NativeObject(), Context().MkSymbol(name).NativeObject(), value.NativeObject());
} }
/** /**
@ -118,13 +119,13 @@ import java.lang.Exception;
void IncRef(long o) void IncRef(long o)
{ {
Context.Params_DRQ.IncAndClear(Context, o); Context().Params_DRQ().IncAndClear(Context(), o);
super.IncRef(o); super.IncRef(o);
} }
void DecRef(long o) void DecRef(long o)
{ {
Context.Params_DRQ.Add(o); Context().Params_DRQ().Add(o);
super.DecRef(o); super.DecRef(o);
} }
} }

9
src/api/java/com/Microsoft/Z3/Pattern.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Runtime.InteropServices; */ /* using System.Runtime.InteropServices; */
@ -21,7 +22,7 @@ import java.lang.Exception;
/** /**
* The number of terms in the pattern. * The number of terms in the pattern.
**/ **/
public long NumTerms() { return Native.getPatternNumTerms(Context().nCtx(), NativeObject()); } public int NumTerms() { return Native.getPatternNumTerms(Context().nCtx(), NativeObject()); }
/** /**
* The terms in the pattern. * The terms in the pattern.
@ -30,10 +31,10 @@ import java.lang.Exception;
{ {
long n = NumTerms; int n = NumTerms();
Expr[] res = new Expr[n]; Expr[] res = new Expr[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = Expr.Create(Context, Native.getPattern(Context().nCtx(), NativeObject(), i)); res[i] = Expr.Create(Context(), Native.getPattern(Context().nCtx(), NativeObject(), i));
return res; return res;
} }

9
src/api/java/com/Microsoft/Z3/Probe.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Runtime.InteropServices; */ /* using System.Runtime.InteropServices; */
@ -29,8 +30,8 @@ import java.lang.Exception;
{ {
Context.CheckContextMatch(g); Context().CheckContextMatch(g);
return Native.probeApply(Context().nCtx(), NativeObject(), g.NativeObject); return Native.probeApply(Context().nCtx(), NativeObject(), g.NativeObject());
} }
/** /**
@ -67,13 +68,13 @@ import java.lang.Exception;
void IncRef(long o) void IncRef(long o)
{ {
Context.Probe_DRQ.IncAndClear(Context, o); Context().Probe_DRQ().IncAndClear(Context(), o);
super.IncRef(o); super.IncRef(o);
} }
void DecRef(long o) void DecRef(long o)
{ {
Context.Probe_DRQ.Add(o); Context().Probe_DRQ().Add(o);
super.DecRef(o); super.DecRef(o);
} }
} }

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -18,7 +19,7 @@ import java.lang.Exception;
/** /**
* Indicates whether the quantifier is universal. * Indicates whether the quantifier is universal.
**/ **/
public boolean IsUniversal() { return Native.isQuantifierForall(Context().nCtx(), NativeObject()) != 0; } public boolean IsUniversal() { return Native.isQuantifierForall(Context().nCtx(), NativeObject()) ; }
/** /**
* Indicates whether the quantifier is existential. * Indicates whether the quantifier is existential.
@ -28,12 +29,12 @@ import java.lang.Exception;
/** /**
* The weight of the quantifier. * The weight of the quantifier.
**/ **/
public long Weight() { return Native.getQuantifierWeight(Context().nCtx(), NativeObject()); } public int Weight() { return Native.getQuantifierWeight(Context().nCtx(), NativeObject()); }
/** /**
* The number of patterns. * The number of patterns.
**/ **/
public long NumPatterns() { return Native.getQuantifierNumPatterns(Context().nCtx(), NativeObject()); } public int NumPatterns() { return Native.getQuantifierNumPatterns(Context().nCtx(), NativeObject()); }
/** /**
* The patterns. * The patterns.
@ -42,17 +43,17 @@ import java.lang.Exception;
{ {
long n = NumPatterns; int n = NumPatterns();
Pattern[] res = new Pattern[n]; Pattern[] res = new Pattern[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = new Pattern(Context, Native.getQuantifierPatternAst(Context().nCtx(), NativeObject(), i)); res[i] = new Pattern(Context(), Native.getQuantifierPatternAst(Context().nCtx(), NativeObject(), i));
return res; return res;
} }
/** /**
* The number of no-patterns. * The number of no-patterns.
**/ **/
public long NumNoPatterns() { return Native.getQuantifierNumNoPatterns(Context().nCtx(), NativeObject()); } public int NumNoPatterns() { return Native.getQuantifierNumNoPatterns(Context().nCtx(), NativeObject()); }
/** /**
* The no-patterns. * The no-patterns.
@ -61,17 +62,17 @@ import java.lang.Exception;
{ {
long n = NumNoPatterns; int n = NumNoPatterns();
Pattern[] res = new Pattern[n]; Pattern[] res = new Pattern[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = new Pattern(Context, Native.getQuantifierNoPatternAst(Context().nCtx(), NativeObject(), i)); res[i] = new Pattern(Context(), Native.getQuantifierNoPatternAst(Context().nCtx(), NativeObject(), i));
return res; return res;
} }
/** /**
* The number of bound variables. * The number of bound variables.
**/ **/
public long NumBound() { return Native.getQuantifierNumBound(Context().nCtx(), NativeObject()); } public int NumBound() { return Native.getQuantifierNumBound(Context().nCtx(), NativeObject()); }
/** /**
* The symbols for the bound variables. * The symbols for the bound variables.
@ -80,10 +81,10 @@ import java.lang.Exception;
{ {
long n = NumBound; int n = NumBound();
Symbol[] res = new Symbol[n]; Symbol[] res = new Symbol[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = Symbol.Create(Context, Native.getQuantifierBoundName(Context().nCtx(), NativeObject(), i)); res[i] = Symbol.Create(Context(), Native.getQuantifierBoundName(Context().nCtx(), NativeObject(), i));
return res; return res;
} }
@ -94,10 +95,10 @@ import java.lang.Exception;
{ {
long n = NumBound; int n = NumBound();
Sort[] res = new Sort[n]; Sort[] res = new Sort[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = Sort.Create(Context, Native.getQuantifierBoundSort(Context().nCtx(), NativeObject(), i)); res[i] = Sort.Create(Context(), Native.getQuantifierBoundSort(Context().nCtx(), NativeObject(), i));
return res; return res;
} }
@ -108,10 +109,10 @@ import java.lang.Exception;
{ {
return new BoolExpr(Context, Native.getQuantifierBody(Context().nCtx(), NativeObject())); return new BoolExpr(Context(), Native.getQuantifierBody(Context().nCtx(), NativeObject()));
} }
Quantifier(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, long weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) Quantifier(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
{ super(ctx); { super(ctx);
@ -123,38 +124,38 @@ import java.lang.Exception;
Context.CheckContextMatch(patterns); Context().CheckContextMatch(patterns);
Context.CheckContextMatch(noPatterns); Context().CheckContextMatch(noPatterns);
Context.CheckContextMatch(sorts); Context().CheckContextMatch(sorts);
Context.CheckContextMatch(names); Context().CheckContextMatch(names);
Context.CheckContextMatch(body); Context().CheckContextMatch(body);
if (sorts.Length != names.Length) if (sorts.length != names.length)
throw new Z3Exception("Number of sorts does not match number of names"); throw new Z3Exception("Number of sorts does not match number of names");
long[] _patterns = AST.ArrayToNative(patterns); long[] _patterns = AST.ArrayToNative(patterns);
if (noPatterns == null && quantifierID == null && skolemID == null) if (noPatterns == null && quantifierID == null && skolemID == null)
{ {
NativeObject() = Native.mkQuantifier(ctx.nCtx(), (isForall) ? 1 : 0, weight, NativeObject() = 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) ? 1 : 0, weight, NativeObject() = 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());
} }
} }
Quantifier(Context ctx, boolean isForall, Expr[] bound, Expr body, long weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) Quantifier(Context ctx, boolean isForall, Expr[] bound, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
{ super(ctx); { super(ctx);
@ -163,26 +164,26 @@ import java.lang.Exception;
Context.CheckContextMatch(noPatterns); Context().CheckContextMatch(noPatterns);
Context.CheckContextMatch(patterns); Context().CheckContextMatch(patterns);
//Context.CheckContextMatch(bound); //Context().CheckContextMatch(bound);
Context.CheckContextMatch(body); Context().CheckContextMatch(body);
if (noPatterns == null && quantifierID == null && skolemID == null) if (noPatterns == null && quantifierID == null && skolemID == null)
{ {
NativeObject() = Native.mkQuantifierConst(ctx.nCtx(), (isForall) ? 1 : 0, weight, NativeObject() = 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) ? 1 : 0, weight, NativeObject() = 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());
} }
} }

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Numerics; */ /* using System.Numerics; */
@ -23,7 +24,7 @@ import java.lang.Exception;
{ {
return new IntNum(Context, Native.getNumerator(Context().nCtx(), NativeObject())); return new IntNum(Context(), Native.getNumerator(Context().nCtx(), NativeObject()));
} }
/** /**
@ -33,7 +34,7 @@ import java.lang.Exception;
{ {
return new IntNum(Context, Native.getDenominator(Context().nCtx(), NativeObject())); return new IntNum(Context(), Native.getDenominator(Context().nCtx(), NativeObject()));
} }
/** /**
@ -41,8 +42,8 @@ import java.lang.Exception;
**/ **/
public BigInteger BigIntNumerator() public BigInteger BigIntNumerator()
{ {
IntNum n = Numerator; IntNum n = Numerator();
return BigInteger.Parse(n.ToString()); return new BigInteger(n.toString());
} }
/** /**
@ -50,15 +51,15 @@ import java.lang.Exception;
**/ **/
public BigInteger BigIntDenominator() public BigInteger BigIntDenominator()
{ {
IntNum n = Denominator; IntNum n = Denominator();
return BigInteger.Parse(n.ToString()); return new BigInteger(n.toString());
} }
/** /**
* 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 ToDecimalString(long precision) public String ToDecimalString(int precision)
{ {
return Native.getNumeralDecimalString(Context().nCtx(), NativeObject(), precision); return Native.getNumeralDecimalString(Context().nCtx(), NativeObject(), precision);
} }

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Collections.Generic; */ /* using System.Collections.Generic; */
/* using System.Linq; */ /* using System.Linq; */

1
src/api/java/com/Microsoft/Z3/RealSort.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -18,7 +19,7 @@ import java.lang.Exception;
/** /**
* The arity of the relation sort. * The arity of the relation sort.
**/ **/
public long Arity() { return Native.getRelationArity(Context().nCtx(), NativeObject()); } public int Arity() { return Native.getRelationArity(Context().nCtx(), NativeObject()); }
/** /**
* The sorts of the columns of the relation sort. * The sorts of the columns of the relation sort.
@ -30,10 +31,10 @@ import java.lang.Exception;
if (m_columnSorts != null) if (m_columnSorts != null)
return m_columnSorts; return m_columnSorts;
long n = Arity; int n = Arity;
Sort[] res = new Sort[n]; Sort[] res = new Sort[n];
for (long i; 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));
return res; return res;
} }

3
src/api/java/com/Microsoft/Z3/SetSort.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -20,7 +21,7 @@ import java.lang.Exception;
} }
SetSort(Context ctx, Sort ty) SetSort(Context ctx, Sort ty)
{ super(ctx, Native.mkSetSort(ctx.nCtx(), ty.NativeObject)); { super(ctx, Native.mkSetSort(ctx.nCtx(), ty.NativeObject()));
} }

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -32,14 +33,14 @@ import java.lang.Exception;
{ {
Context.CheckContextMatch(value); Context().CheckContextMatch(value);
Native.solverSetParams(Context().nCtx(), NativeObject(), value.NativeObject); Native.solverSetParams(Context().nCtx(), NativeObject(), value.NativeObject());
} }
/** /**
* Retrieves parameter descriptions for solver. * Retrieves parameter descriptions for solver.
**/ **/
public ParamDescrs ParameterDescriptions() { return new ParamDescrs(Context, Native.solverGetParamDescrs(Context().nCtx(), NativeObject())); } public ParamDescrs ParameterDescriptions() { return new ParamDescrs(Context(), Native.solverGetParamDescrs(Context().nCtx(), NativeObject())); }
/** /**
@ -47,7 +48,7 @@ import java.lang.Exception;
* <seealso cref="Pop"/> * <seealso cref="Pop"/>
* <seealso cref="Push"/> * <seealso cref="Push"/>
**/ **/
public long NumScopes() { return Native.solverGetNumScopes(Context().nCtx(), NativeObject()); } public int NumScopes() { return Native.solverGetNumScopes(Context().nCtx(), NativeObject()); }
/** /**
* Creates a backtracking point. * Creates a backtracking point.
@ -63,7 +64,7 @@ import java.lang.Exception;
* <remarks>Note that an exception is thrown if <paramref name="n"/> is not smaller than <code>NumScopes</code></remarks> * <remarks>Note that an exception is thrown if <paramref name="n"/> is not smaller than <code>NumScopes</code></remarks>
* <seealso cref="Push"/> * <seealso cref="Push"/>
**/ **/
public void Pop(long n) public void Pop(int n)
{ {
Native.solverPop(Context().nCtx(), NativeObject(), n); Native.solverPop(Context().nCtx(), NativeObject(), n);
} }
@ -85,19 +86,19 @@ import java.lang.Exception;
Context.CheckContextMatch(constraints); Context().CheckContextMatch(constraints);
for (Iterator a = constraints.iterator(); a.hasNext(); ) for (BoolExpr a: constraints)
{ {
Native.solverAssert(Context().nCtx(), NativeObject(), a.NativeObject); Native.solverAssert(Context().nCtx(), NativeObject(), a.NativeObject());
} }
} }
/** /**
* The number of assertions in the solver. * The number of assertions in the solver.
**/ **/
public long 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;
} }
@ -108,11 +109,11 @@ import java.lang.Exception;
{ {
ASTVector ass = new ASTVector(Context, Native.solverGetAssertions(Context().nCtx(), NativeObject())); ASTVector ass = new ASTVector(Context(), Native.solverGetAssertions(Context().nCtx(), NativeObject()));
long n = ass.Size; int n = ass.Size;
BoolExpr[] res = new BoolExpr[n]; BoolExpr[] res = new BoolExpr[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = new BoolExpr(Context, ass[i].NativeObject); res[i] = new BoolExpr(Context(), ass[i].NativeObject());
return res; return res;
} }
@ -128,13 +129,13 @@ import java.lang.Exception;
{ {
Z3_lbool r; Z3_lbool r;
if (assumptions == null) if (assumptions == null)
r = (Z3_lbool)Native.solverCheck(Context().nCtx(), NativeObject()); r = Z3_lbool.fromInt(Native.solverCheck(Context().nCtx(), NativeObject()));
else else
r = (Z3_lbool)Native.solverCheckAssumptions(Context().nCtx(), NativeObject(), (long)assumptions.Length, AST.ArrayToNative(assumptions)); r = Z3_lbool.fromInt(Native.solverCheckAssumptions(Context().nCtx(), NativeObject(), (int)assumptions.length, AST.ArrayToNative(assumptions)));
switch (r) switch (r)
{ {
case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE; case Z3_L_TRUE: return Status.SATISFIABLE;
case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE; case Z3_L_FALSE: return Status.UNSATISFIABLE;
default: return Status.UNKNOWN; default: return Status.UNKNOWN;
} }
} }
@ -152,7 +153,7 @@ import java.lang.Exception;
if (x == 0) if (x == 0)
return null; return null;
else else
return new Model(Context, x); return new Model(Context(), x);
} }
/** /**
@ -168,7 +169,7 @@ import java.lang.Exception;
if (x == 0) if (x == 0)
return null; return null;
else else
return Expr.Create(Context, x); return Expr.Create(Context(), x);
} }
/** /**
@ -183,11 +184,11 @@ import java.lang.Exception;
{ {
ASTVector core = new ASTVector(Context, Native.solverGetUnsatCore(Context().nCtx(), NativeObject())); ASTVector core = new ASTVector(Context(), Native.solverGetUnsatCore(Context().nCtx(), NativeObject()));
long n = core.Size; int n = core.Size;
Expr[] res = new Expr[n]; Expr[] res = new Expr[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = Expr.Create(Context, core[i].NativeObject); res[i] = Expr.Create(Context(), core[i].NativeObject());
return res; return res;
} }
@ -208,7 +209,7 @@ import java.lang.Exception;
{ {
return new Statistics(Context, Native.solverGetStatistics(Context().nCtx(), NativeObject())); return new Statistics(Context(), Native.solverGetStatistics(Context().nCtx(), NativeObject()));
} }
/** /**
@ -239,13 +240,13 @@ import java.lang.Exception;
void IncRef(long o) void IncRef(long o)
{ {
Context.Solver_DRQ.IncAndClear(Context, o); Context().Solver_DRQ().IncAndClear(Context(), o);
super.IncRef(o); super.IncRef(o);
} }
void DecRef(long o) void DecRef(long o)
{ {
Context.Solver_DRQ.Add(o); Context().Solver_DRQ().Add(o);
super.DecRef(o); super.DecRef(o);
} }
} }

29
src/api/java/com/Microsoft/Z3/Sort.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -57,12 +58,12 @@ import java.lang.Exception;
/** /**
* Returns a unique identifier for the sort. * Returns a unique identifier for the sort.
**/ **/
public long Id() { return Native.getSortId(Context().nCtx(), NativeObject()); } public int Id() { return Native.getSortId(Context().nCtx(), NativeObject()); }
/** /**
* The kind of the sort. * The kind of the sort.
**/ **/
public Z3_sort_kind SortKind() { return (Z3_sort_kind)Native.getSortKind(Context().nCtx(), NativeObject()); } public Z3_sort_kind SortKind() { return Z3_sort_kind.fromInt(Native.getSortKind(Context().nCtx(), NativeObject())); }
/** /**
* The name of the sort * The name of the sort
@ -70,7 +71,7 @@ import java.lang.Exception;
public Symbol Name() public Symbol Name()
{ {
return Symbol.Create(Context, Native.getSortName(Context().nCtx(), NativeObject())); return Symbol.Create(Context(), Native.getSortName(Context().nCtx(), NativeObject()));
} }
/** /**
@ -89,7 +90,7 @@ import java.lang.Exception;
void CheckNativeObject(long obj) void CheckNativeObject(long obj)
{ {
if (Native.getAstKind(Context().nCtx(), obj) != (long)Z3_ast_kind.Z3_SORT_AST) if (Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_SORT_AST.toInt())
throw new Z3Exception("Underlying object is not a sort"); throw new Z3Exception("Underlying object is not a sort");
super.CheckNativeObject(obj); super.CheckNativeObject(obj);
} }
@ -99,17 +100,17 @@ import java.lang.Exception;
switch ((Z3_sort_kind)Native.getSortKind(ctx.nCtx(), obj)) switch (Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), obj)))
{ {
case Z3_sort_kind.Z3_ARRAY_SORT: return new ArraySort(ctx, obj); case Z3_ARRAY_SORT: return new ArraySort(ctx, obj);
case Z3_sort_kind.Z3_BOOL_SORT: return new BoolSort(ctx, obj); case Z3_BOOL_SORT: return new BoolSort(ctx, obj);
case Z3_sort_kind.Z3_BV_SORT: return new BitVecSort(ctx, obj); case Z3_BV_SORT: return new BitVecSort(ctx, obj);
case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeSort(ctx, obj); case Z3_DATATYPE_SORT: return new DatatypeSort(ctx, obj);
case Z3_sort_kind.Z3_INT_SORT: return new IntSort(ctx, obj); case Z3_INT_SORT: return new IntSort(ctx, obj);
case Z3_sort_kind.Z3_REAL_SORT: return new RealSort(ctx, obj); case Z3_REAL_SORT: return new RealSort(ctx, obj);
case Z3_sort_kind.Z3_UNINTERPRETED_SORT: return new UninterpretedSort(ctx, obj); case Z3_UNINTERPRETED_SORT: return new UninterpretedSort(ctx, obj);
case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainSort(ctx, obj); case Z3_FINITE_DOMAIN_SORT: return new FiniteDomainSort(ctx, obj);
case Z3_sort_kind.Z3_RELATION_SORT: return new RelationSort(ctx, obj); case Z3_RELATION_SORT: return new RelationSort(ctx, obj);
default: default:
throw new Z3Exception("Unknown sort kind"); throw new Z3Exception("Unknown sort kind");
} }

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -27,7 +28,7 @@ import java.lang.Exception;
/** /**
* The uint-value of the entry. * The uint-value of the entry.
**/ **/
public long UIntValue() { return m_long; } public int UIntValue() { return m_int; }
/** /**
* The double-value of the entry. * The double-value of the entry.
**/ **/
@ -35,7 +36,7 @@ import java.lang.Exception;
/** /**
* True if the entry is uint-valued. * True if the entry is uint-valued.
**/ **/
public boolean IsUInt() { return m_is_long; } public boolean IsUInt() { return m_is_int; }
/** /**
* True if the entry is double-valued. * True if the entry is double-valued.
**/ **/
@ -49,9 +50,9 @@ import java.lang.Exception;
if (IsUInt) if (IsUInt)
return m_long.ToString(); return m_int.toString();
else if (IsDouble) else if (IsDouble)
return m_double.ToString(); return m_double.toString();
else else
throw new Z3Exception("Unknown statistical entry type"); throw new Z3Exception("Unknown statistical entry type");
} }
@ -64,15 +65,15 @@ import java.lang.Exception;
return Key + ": " + Value; return Key + ": " + Value;
} }
private boolean m_is_long = false; private boolean m_is_int = false;
private boolean m_is_double = false; private boolean m_is_double = false;
private long m_long = 0; private int m_int = 0;
private double m_double = 0.0; private double m_double = 0.0;
Entry(String k, long v) Entry(String k, int v)
{ {
Key = k; Key = k;
m_is_long = true; m_is_int = true;
m_long = v; m_int = v;
} }
Entry(String k, double v) Entry(String k, double v)
{ {
@ -93,7 +94,7 @@ import java.lang.Exception;
/** /**
* The number of statistical data. * The number of statistical data.
**/ **/
public long Size() { return Native.statsSize(Context().nCtx(), NativeObject()); } public int Size() { return Native.statsSize(Context().nCtx(), NativeObject()); }
/** /**
* The data entries. * The data entries.
@ -104,15 +105,15 @@ import java.lang.Exception;
long n = Size; int n = Size;
Entry[] res = new Entry[n]; Entry[] res = new Entry[n];
for (long i; 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.statsIsLong(Context().nCtx(), NativeObject(), i) != 0) if (Native.statsIsInt(Context().nCtx(), NativeObject(), i) )
e = new Entry(k, Native.statsGetLongValue(Context().nCtx(), NativeObject(), i)); e = new Entry(k, Native.statsGetIntValue(Context().nCtx(), NativeObject(), i));
else if (Native.statsIsDouble(Context().nCtx(), NativeObject(), i) != 0) 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
throw new Z3Exception("Unknown data entry value"); throw new Z3Exception("Unknown data entry value");
@ -128,9 +129,9 @@ import java.lang.Exception;
{ {
long n = Size; int n = Size;
String[] res = new String[n]; String[] res = new String[n];
for (long i; 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);
return res; return res;
} }
@ -141,9 +142,9 @@ import java.lang.Exception;
**/ **/
public Entry get(String key) public Entry get(String key)
{ {
long n = Size; int n = Size;
Entry[] es = Entries; Entry[] es = Entries;
for (long i; 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];
return null; return null;
@ -169,13 +170,13 @@ import java.lang.Exception;
void IncRef(long o) void IncRef(long o)
{ {
Context.Statistics_DRQ.IncAndClear(Context, o); Context().Statistics_DRQ().IncAndClear(Context(), o);
super.IncRef(o); super.IncRef(o);
} }
void DecRef(long o) void DecRef(long o)
{ {
Context.Statistics_DRQ.Add(o); Context().Statistics_DRQ().Add(o);
super.DecRef(o); super.DecRef(o);
} }
} }

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

@ -7,27 +7,28 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/** /**
* Status values. * Status values.
**/ **/
public enum Status public class Status
{ {
/// <summary> /// <summary>
/// Used to signify an unsatisfiable status. /// Used to signify an unsatisfiable status.
/// </summary> /// </summary>
UNSATISFIABLE (1), public static final int UNSATISFIABLE = 1;
/// <summary> /// <summary>
/// Used to signify an unknown status. /// Used to signify an unknown status.
/// </summary> /// </summary>
UNKNOWN (0), public static final int UNKNOWN = 0;
/// <summary> /// <summary>
/// Used to signify a satisfiable status. /// Used to signify a satisfiable status.
/// </summary> /// </summary>
SATISFIABLE (1) public static final int SATISFIABLE = 1;
} }

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Runtime.InteropServices; */ /* using System.Runtime.InteropServices; */

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
/* using System.Runtime.InteropServices; */ /* using System.Runtime.InteropServices; */
@ -19,7 +20,7 @@ import java.lang.Exception;
/** /**
* The kind of the symbol (int or string) * The kind of the symbol (int or string)
**/ **/
protected Z3_symbol_kind Kind() { return (Z3_symbol_kind)Native.getSymbolKind(Context().nCtx(), NativeObject()); } protected Z3_symbol_kind Kind() { return Z3_symbol_kind.fromInt(Native.getSymbolKind(Context().nCtx(), NativeObject())); }
/** /**
* Indicates whether the symbol is of Int kind * Indicates whether the symbol is of Int kind
@ -43,7 +44,7 @@ import java.lang.Exception;
public String toString() public String toString()
{ {
if (IsIntSymbol()) if (IsIntSymbol())
return ((IntSymbol)this).Int.ToString(); return ((IntSymbol)this).Int.toString();
else if (IsStringSymbol()) else if (IsStringSymbol())
return ((StringSymbol)this).String; return ((StringSymbol)this).String;
else else
@ -62,10 +63,10 @@ import java.lang.Exception;
switch ((Z3_symbol_kind)Native.getSymbolKind(ctx.nCtx(), obj)) switch (Z3_symbol_kind.fromInt(Native.getSymbolKind(ctx.nCtx(), obj)))
{ {
case Z3_symbol_kind.Z3_INT_SYMBOL: return new IntSymbol(ctx, obj); case Z3_INT_SYMBOL: return new IntSymbol(ctx, obj);
case Z3_symbol_kind.Z3_STRING_SYMBOL: return new StringSymbol(ctx, obj); case Z3_STRING_SYMBOL: return new StringSymbol(ctx, obj);
default: default:
throw new Z3Exception("Unknown symbol kind encountered"); throw new Z3Exception("Unknown symbol kind encountered");
} }

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -32,7 +33,7 @@ import java.lang.Exception;
/** /**
* Retrieves parameter descriptions for Tactics. * Retrieves parameter descriptions for Tactics.
**/ **/
public ParamDescrs ParameterDescriptions() { return new ParamDescrs(Context, Native.tacticGetParamDescrs(Context().nCtx(), NativeObject())); } public ParamDescrs ParameterDescriptions() { return new ParamDescrs(Context(), Native.tacticGetParamDescrs(Context().nCtx(), NativeObject())); }
/** /**
@ -43,13 +44,13 @@ import java.lang.Exception;
Context.CheckContextMatch(g); Context().CheckContextMatch(g);
if (p == null) if (p == null)
return new ApplyResult(Context, Native.tacticApply(Context().nCtx(), NativeObject(), g.NativeObject)); return new ApplyResult(Context(), Native.tacticApply(Context().nCtx(), NativeObject(), g.NativeObject()));
else else
{ {
Context.CheckContextMatch(p); Context().CheckContextMatch(p);
return new ApplyResult(Context, Native.tacticApplyEx(Context().nCtx(), NativeObject(), g.NativeObject, p.NativeObject)); return new ApplyResult(Context(), Native.tacticApplyEx(Context().nCtx(), NativeObject(), g.NativeObject(), p.NativeObject()));
} }
} }
@ -72,7 +73,7 @@ import java.lang.Exception;
{ {
return Context.MkSolver(this); return Context().MkSolver(this);
} }
Tactic(Context ctx, long obj) Tactic(Context ctx, long obj)
@ -99,13 +100,13 @@ import java.lang.Exception;
void IncRef(long o) void IncRef(long o)
{ {
Context.Tactic_DRQ.IncAndClear(Context, o); Context().Tactic_DRQ().IncAndClear(Context(), o);
super.IncRef(o); super.IncRef(o);
} }
void DecRef(long o) void DecRef(long o)
{ {
Context.Tactic_DRQ.Add(o); Context().Tactic_DRQ().Add(o);
super.DecRef(o); super.DecRef(o);
} }
} }

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -22,13 +23,13 @@ import java.lang.Exception;
{ {
return new FuncDecl(Context, Native.getTupleSortMkDecl(Context().nCtx(), NativeObject())); return new FuncDecl(Context(), Native.getTupleSortMkDecl(Context().nCtx(), NativeObject()));
} }
/** /**
* The number of fields in the tuple. * The number of fields in the tuple.
**/ **/
public long NumFields() { return Native.getTupleSortNumFields(Context().nCtx(), NativeObject()); } public int NumFields() { return Native.getTupleSortNumFields(Context().nCtx(), NativeObject()); }
/** /**
* The field declarations. * The field declarations.
@ -37,20 +38,20 @@ import java.lang.Exception;
{ {
long n = NumFields; int n = NumFields();
FuncDecl[] res = new FuncDecl[n]; FuncDecl[] res = new FuncDecl[n];
for (long i; i < n; i++) for (int i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.getTupleSortFieldDecl(Context().nCtx(), NativeObject(), i)); res[i] = new FuncDecl(Context(), Native.getTupleSortFieldDecl(Context().nCtx(), NativeObject(), i));
return res; return res;
} }
TupleSort(Context ctx, Symbol name, long numFields, Symbol[] fieldNames, Sort[] fieldSorts) TupleSort(Context ctx, Symbol name, int numFields, Symbol[] fieldNames, Sort[] fieldSorts)
{ super(ctx); { super(ctx);
long t = 0; long t = 0;
NativeObject() = Native.mkTupleSort(ctx.nCtx(), name.NativeObject, numFields, NativeObject() = 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]);
} }

3
src/api/java/com/Microsoft/Z3/UninterpretedSort.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -20,7 +21,7 @@ import java.lang.Exception;
} }
UninterpretedSort(Context ctx, Symbol s) UninterpretedSort(Context ctx, Symbol s)
{ super(ctx, Native.mkUninterpretedSort(ctx.nCtx(), s.NativeObject)); { super(ctx, Native.mkUninterpretedSort(ctx.nCtx(), s.NativeObject()));
} }

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -21,9 +22,9 @@ import java.lang.Exception;
/** /**
* The major version * The major version
**/ **/
public long Major() public int Major()
{ {
long 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; return major;
} }
@ -31,9 +32,9 @@ import java.lang.Exception;
/** /**
* The minor version * The minor version
**/ **/
public long Minor() public int Minor()
{ {
long 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 minor; return minor;
} }
@ -41,9 +42,9 @@ import java.lang.Exception;
/** /**
* The build version * The build version
**/ **/
public long Build() public int Build()
{ {
long 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 build; return build;
} }
@ -51,9 +52,9 @@ import java.lang.Exception;
/** /**
* The revision * The revision
**/ **/
public long Revision() public int Revision()
{ {
long 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 revision; return revision;
} }
@ -65,8 +66,8 @@ import java.lang.Exception;
{ {
long 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 major.toString() + "." + minor.toString() + "." + build.toString() + "." + revision.toString();
} }
} }

1
src/api/java/com/Microsoft/Z3/Z3Exception.java
View file

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */

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

@ -7,6 +7,7 @@ package com.Microsoft.Z3;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*; import java.util.*;
import java.lang.Exception; import java.lang.Exception;
import com.Microsoft.Z3.Enumerations.*;
/* using System; */ /* using System; */
@ -105,14 +106,14 @@ import java.lang.Exception;
if (a == null) return null; if (a == null) return null;
long[] an = new long[a.Length]; long[] an = new long[a.length];
for (long i; i < a.Length; i++) for (int i = 0; i < a.length; i++)
if (a[i] != null) an[i] = a[i].NativeObject(); if (a[i] != null) an[i] = a[i].NativeObject();
return an; return an;
} }
static long ArrayLength(Z3Object[] a) static int ArrayLength(Z3Object[] a)
{ {
return (a == null)?0:(long)a.Length; return (a == null)?0:(int)a.length;
} }
} }

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

@ -11,14 +11,29 @@ CS="../dotnet/"
EXT=".cs" EXT=".cs"
EXCLUDE=["Enumerations.cs", "Native.cs", "AssemblyInfo.cs"] EXCLUDE=["Enumerations.cs", "Native.cs", "AssemblyInfo.cs"]
OUTDIR="com/Microsoft/Z3/" OUTDIR="com/Microsoft/Z3/"
ENUMS_FILE = "Enumerations.cs"
import os import os
import fileinput import fileinput
import string import string
import re import re
EXCLUDE_METHODS = [ [ "Context.cs", "public Expr MkNumeral(ulong" ],
[ "Context.cs", "public Expr MkNumeral(uint" ],
[ "Context.cs", "public RatNum MkReal(ulong" ],
[ "Context.cs", "public RatNum MkReal(uint" ],
[ "Context.cs", "public IntNum MkInt(ulong" ],
[ "Context.cs", "public IntNum MkInt(uint" ],
[ "Context.cs", "public BitVecNum MkBV(ulong" ],
[ "Context.cs", "public BitVecNum MkBV(uint" ],
]
ENUMS = []
def mk_java_bindings(): def mk_java_bindings():
print "Generating Java bindings (from C# bindings in " + CS + ")." print "Generating Java bindings (from C# bindings in " + CS + ")..."
print "Finding enumerations in " + ENUMS_FILE + "..."
find_enums(ENUMS_FILE)
for root, dirs, files in os.walk(CS): for root, dirs, files in os.walk(CS):
for fn in files: for fn in files:
if not fn in EXCLUDE and fn.endswith(EXT): if not fn in EXCLUDE and fn.endswith(EXT):
@ -31,14 +46,14 @@ def subst_getters(s, getters):
def type_replace(s): def type_replace(s):
s = s.replace(" bool", " boolean") s = s.replace(" bool", " boolean")
s = s.replace("(bool", "(boolean") s = s.replace("(bool", "(boolean")
s = s.replace("uint", "long") s = s.replace("uint", "int")
s = s.replace("ulong", "long") s = s.replace("ulong", "long")
s = s.replace("string", "String") s = s.replace("string", "String")
s = s.replace("IntPtr", "long") s = s.replace("IntPtr", "long")
s = s.replace("Dictionary<", "Map<") s = s.replace("Dictionary<", "Map<")
s = s.replace("UInt64", "long") s = s.replace("UInt64", "long")
s = s.replace("Int64", "long") s = s.replace("Int64", "long")
s = s.replace("List<long>", "List<Long>") s = s.replace("List<long>", "LinkedList<Long>")
s = s.replace("System.Exception", "Exception") s = s.replace("System.Exception", "Exception")
return s return s
@ -55,12 +70,54 @@ def rename_native(s):
s = c0 + c1 + c2 s = c0 + c1 + c2
return s return s
def find_enums(fn):
for line in fileinput.input(os.path.join(CS, fn)):
s = string.rstrip(string.lstrip(line))
if s.startswith("public enum"):
ENUMS.append(s.split(" ")[2])
def enum_replace(line):
for e in ENUMS:
if line.find("case") != -1:
line = line.replace(e + ".", "")
elif line.find("== (int)") != -1 or line.find("!= (int)") != -1:
line = re.sub("\(int\)" + e + "\.(?P<id>[A-Z0-9_]*)", e + ".\g<id>.toInt()", line)
elif line.find("==") != -1 or line.find("!=") != -1:
line = re.sub(e + "\.(?P<id>[A-Z0-9_]*)", e + ".\g<id>", line)
else:
# line = re.sub("\(\(" + e + "\)(?P<rest>.*\(.*)\)", "(" + e + ".values()[\g<rest>])", line)
line = re.sub("\(" + e + "\)(?P<rest>.*\(.*\))", e + ".fromInt(\g<rest>)", line)
return line
def replace_generals(a): def replace_generals(a):
a = re.sub(" NativeObject", " NativeObject()", a) a = re.sub(" NativeObject", " NativeObject()", a)
a = re.sub(".NativeObject;", ".NativeObject();", a) a = re.sub("\.NativeObject", ".NativeObject()", a)
a = re.sub("Context.nCtx", "Context().nCtx()", a) a = re.sub("(?P<h>[\.\(])Id", "\g<h>Id()", a)
a = re.sub("ctx.nCtx", "ctx.nCtx()", a) a = a.replace("(Context ==", "(Context() ==")
a = a.replace("(Context,", "(Context(),")
a = a.replace("Context.", "Context().")
a = a.replace(".nCtx", ".nCtx()")
a = a.replace("(nCtx", "(nCtx()")
a = re.sub("Context\(\).(?P<id>[^_]*)_DRQ", "Context().\g<id>_DRQ()", a)
a = re.sub("ASTKind", "ASTKind()", a) a = re.sub("ASTKind", "ASTKind()", a)
a = re.sub("IsExpr(?P<f>[ ;])", "IsExpr()\g<f>", a)
a = re.sub("IsNumeral(?P<f>[ ;])", "IsNumeral()\g<f>", a)
a = re.sub("IsInt(?P<f>[ ;])", "IsInt()\g<f>", a)
a = re.sub("IsReal(?P<f>[ ;])", "IsReal()\g<f>", a)
a = re.sub("IsVar(?P<f>[ ;\)])", "IsVar()\g<f>", a)
a = re.sub("FuncDecl.DeclKind", "FuncDecl().DeclKind()", a)
a = re.sub("FuncDecl.DomainSize", "FuncDecl().DomainSize()", a)
a = re.sub("(?P<h>[=&]) Num(?P<id>[a-zA-Z]*)", "\g<h> Num\g<id>()", a)
a = re.sub("= Denominator", "= Denominator()", a)
a = re.sub(", BoolSort(?P<f>[\)\.])", ", BoolSort()\g<f>", a)
a = re.sub(", RealSort(?P<f>[\)\.])", ", RealSort()\g<f>", a)
a = re.sub(", IntSort(?P<f>[\)\.])", ", IntSort()\g<f>", a)
a = a.replace("? 1 : 0", "? true : false")
if a.find("Native.") != -1 and a.find("!= 0") != -1:
a = a.replace("!= 0", "")
if a.find("Native.") != -1 and a.find("== 0") != -1:
a = a.replace("== 0", "^ true")
return a return a
def translate(filename): def translate(filename):
@ -82,6 +139,8 @@ def translate(filename):
in_getter_set = 0 in_getter_set = 0
had_ulong_res = 0 had_ulong_res = 0
in_enum = 0 in_enum = 0
missing_foreach_brace = 0
foreach_opened_brace = 0
for line in fileinput.input(os.path.join(CS, filename)): for line in fileinput.input(os.path.join(CS, filename)):
s = string.rstrip(string.lstrip(line)) s = string.rstrip(string.lstrip(line))
if in_javadoc: if in_javadoc:
@ -104,6 +163,13 @@ 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)):
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: if in_unsupported:
if s == "}": if s == "}":
in_unsupported = 0 in_unsupported = 0
@ -119,6 +185,7 @@ def translate(filename):
tgt.write("import java.math.BigInteger;\n") tgt.write("import java.math.BigInteger;\n")
tgt.write("import java.util.*;\n") tgt.write("import java.util.*;\n")
tgt.write("import java.lang.Exception;\n") tgt.write("import java.lang.Exception;\n")
tgt.write("import com.Microsoft.Z3.Enumerations.*;\n")
elif in_header == 1: elif in_header == 1:
# tgt.write(" * " + line.replace(filename, tgtfn)) # tgt.write(" * " + line.replace(filename, tgtfn))
pass pass
@ -134,14 +201,15 @@ def translate(filename):
tgt.write(t + "/* Overloaded operators are not translated. */\n") tgt.write(t + "/* Overloaded operators are not translated. */\n")
in_unsupported = 1 in_unsupported = 1
elif s.startswith("public enum"): elif s.startswith("public enum"):
tgt.write(line) tgt.write(line.replace("enum", "class"))
in_enum = 1 in_enum = 1
elif in_enum == 1: elif in_enum == 1:
if s == "}": if s == "}":
tgt.write(line) tgt.write(line)
in_enum = 0 in_enum = 0
else: else:
tgt.write(re.sub("(?P<id>.*)\W*=\W*(?P<val>[^\n,])", "\g<id> (\g<val>)", line)) line = re.sub("(?P<id>.*)\W*=\W*(?P<val>[^\n,])", "public static final int \g<id> = \g<val>;", line)
tgt.write(line.replace(",",""))
elif s.startswith("public class") or s.startswith("internal class") or s.startswith("internal abstract class"): elif s.startswith("public class") or s.startswith("internal class") or s.startswith("internal abstract class"):
a = line.replace(":", "extends").replace("internal ", "") a = line.replace(":", "extends").replace("internal ", "")
a = a.replace(", IComparable", "") a = a.replace(", IComparable", "")
@ -164,7 +232,7 @@ def translate(filename):
s = s.replace("internal virtual", "") s = s.replace("internal virtual", "")
s = s.replace("internal", "") s = s.replace("internal", "")
tokens = s.split(" ") tokens = s.split(" ")
print "TOKENS: " + str(len(tokens)) # print "TOKENS: " + str(len(tokens))
if len(tokens) == 3: if len(tokens) == 3:
in_getter = tokens[2] in_getter = tokens[2]
in_getter_type = type_replace((tokens[0] + " " + tokens[1])) in_getter_type = type_replace((tokens[0] + " " + tokens[1]))
@ -204,6 +272,7 @@ def translate(filename):
rest = type_replace(rest) rest = type_replace(rest)
rest = rename_native(rest) rest = rename_native(rest)
rest = replace_generals(rest) rest = replace_generals(rest)
rest = enum_replace(rest)
t = "" t = ""
for i in range(0, lastindent): for i in range(0, lastindent):
t += " " t += " "
@ -225,6 +294,7 @@ def translate(filename):
subst_getters(rest, getters) subst_getters(rest, getters)
rest = rename_native(rest) rest = rename_native(rest)
rest = replace_generals(rest) rest = replace_generals(rest)
rest = enum_replace(rest)
if in_bracket_op: if in_bracket_op:
tgt.write(d + rest) tgt.write(d + rest)
else: else:
@ -240,6 +310,7 @@ def translate(filename):
rest = type_replace(rest) rest = type_replace(rest)
rest = rename_native(rest) rest = rename_native(rest)
rest = replace_generals(rest) rest = replace_generals(rest)
rest = enum_replace(rest)
if in_bracket_op: if in_bracket_op:
tgt.write(t + in_getter_type + " " + in_getter + " " + rest + "\n") tgt.write(t + in_getter_type + " " + in_getter + " " + rest + "\n")
else: else:
@ -257,6 +328,7 @@ def translate(filename):
rest = type_replace(rest) rest = type_replace(rest)
rest = rename_native(rest) rest = rename_native(rest)
rest = replace_generals(rest) rest = replace_generals(rest)
rest = enum_replace(rest)
ac_acc = in_getter_type[:in_getter_type.find(' ')] ac_acc = in_getter_type[:in_getter_type.find(' ')]
ac_type = in_getter_type[in_getter_type.find(' ')+1:] ac_type = in_getter_type[in_getter_type.find(' ')+1:]
if in_bracket_op: if in_bracket_op:
@ -301,19 +373,43 @@ def translate(filename):
else: else:
for i in range(0, mbraces): for i in range(0, mbraces):
line = line.replace("\n", "}\n") line = line.replace("\n", "}\n")
if s.find("(") != -1: if (s.find("public") != -1 or s.find("protected") != -1 or s.find("internal") != -1) and s.find("(") != -1:
line = re.sub(" = [\w.]+(?P<d>[,;\)])", "\g<d>", line) line = re.sub(" = [\w.]+(?P<d>[,;\)])", "\g<d>", line)
a = type_replace(line) a = type_replace(line)
a = enum_replace(a)
a = re.sub("(?P<d>[\(, ])params ", "\g<d>", a) a = re.sub("(?P<d>[\(, ])params ", "\g<d>", a)
a = a.replace("base.", "super.") a = a.replace("base.", "super.")
a = re.sub("Contract.\w+\([\s\S]*\);", "", a) a = re.sub("Contract.\w+\([\s\S]*\);", "", a)
a = rename_native(a) a = rename_native(a)
a = re.sub("~\w+\(\)", "protected void finalize()", a) a = re.sub("~\w+\(\)", "protected void finalize()", a)
if missing_foreach_brace == 1:
# a = a.replace("\n", " // checked " + str(foreach_opened_brace) + "\n")
if foreach_opened_brace == 0 and a.find("{") != -1:
foreach_opened_brace = 1
elif foreach_opened_brace == 0 and a.find("}") == -1:
a = a.replace("\n", "}}\n")
foreach_opened_brace = 0
missing_foreach_brace = 0
elif foreach_opened_brace == 1 and a.find("}") != -1:
a = a.replace("\n", "}}\n")
foreach_opened_brace = 0
missing_foreach_brace = 0
# if a.find("foreach") != -1:
# missing_foreach_brace = 1
# a = re.sub("foreach\s*\((?P<t>[\w <>,]+)\s+(?P<i>\w+)\s+in\s+(?P<w>\w+)\)",
# "{ Iterator fe_i = \g<w>.iterator(); while (fe_i.hasNext()) { \g<t> \g<i> = (long)fe_i.next(); ",
# a)
a = re.sub("foreach\s*\((?P<t>[\w <>,]+)\s+(?P<i>\w+)\s+in\s+(?P<w>\w+)\)", a = re.sub("foreach\s*\((?P<t>[\w <>,]+)\s+(?P<i>\w+)\s+in\s+(?P<w>\w+)\)",
"for (Iterator \g<i> = \g<w>.iterator(); \g<i>.hasNext(); )", a) "for (\g<t> \g<i>: \g<w>)",
a)
if a.find("long o: m_queue") != -1:
a = a.replace("long", "Long")
a = a.replace("readonly ", "") a = a.replace("readonly ", "")
a = a.replace("const ", "final ") a = a.replace("const ", "final ")
a = a.replace("String ToString", "String toString") a = a.replace("String ToString", "String toString")
a = a.replace(".ToString", ".toString")
a = a.replace("internal ", "") a = a.replace("internal ", "")
a = a.replace("new static", "static") a = a.replace("new static", "static")
a = a.replace("new public", "public") a = a.replace("new public", "public")
@ -333,6 +429,13 @@ def translate(filename):
a = a.replace("out res", "res") a = a.replace("out res", "res")
a = a.replace("GC.ReRegisterForFinalize(m_ctx);", "") a = a.replace("GC.ReRegisterForFinalize(m_ctx);", "")
a = a.replace("GC.SuppressFinalize(this);", "") a = a.replace("GC.SuppressFinalize(this);", "")
a = a.replace(".Length", ".length")
a = a.replace("m_queue.Count", "m_queue.size()")
a = a.replace("m_queue.Add", "m_queue.add")
a = a.replace("m_queue.Clear", "m_queue.clear")
a = a.replace("for (long ", "for (int ")
a = a.replace("ReferenceEquals(Context, ctx)", "Context() == ctx")
a = a.replace("BigInteger.Parse", "new BigInteger")
if had_ulong_res == 0 and a.find("ulong res = 0") != -1: if had_ulong_res == 0 and a.find("ulong res = 0") != -1:
a = a.replace("ulong res = 0;", "LongPtr res = new LongPtr();") a = a.replace("ulong res = 0;", "LongPtr res = new LongPtr();")
elif had_ulong_res == 1: elif had_ulong_res == 1:
@ -348,7 +451,6 @@ def translate(filename):
a = re.sub("NativeObject = (?P<rest>.*);", "setNativeObject(\g<rest>);", a) a = re.sub("NativeObject = (?P<rest>.*);", "setNativeObject(\g<rest>);", a)
a = replace_generals(a) a = replace_generals(a)
tgt.write(a) tgt.write(a)
tgt.close() tgt.close()
mk_java_bindings() mk_java_bindings()