diff --git a/scripts/mk_util.py b/scripts/mk_util.py index b69171a24..ae10d6740 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1854,8 +1854,25 @@ def mk_z3consts_java(api_files): efile.write(' **/\n') efile.write('public enum %s {\n' % name) efile.write + first = True 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.close() mode = SEARCHING diff --git a/scripts/update_api.py b/scripts/update_api.py index 7e1439375..1eef11705 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -509,6 +509,7 @@ def mk_java(): 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 StringPtr { public String value; }\n') + java_native.write(' public static class errorHandler { public long ptr; }\n') if is_windows(): java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java')) diff --git a/src/api/java/com/Microsoft/Z3/AST.java b/src/api/java/com/Microsoft/Z3/AST.java index c8471e2e8..069c07a4c 100644 --- a/src/api/java/com/Microsoft/Z3/AST.java +++ b/src/api/java/com/Microsoft/Z3/AST.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Collections; */ @@ -58,9 +59,9 @@ import java.lang.Exception; return 1; else { - if (Id < oAST.Id) + if (Id() < oAST.Id()) return -1; - else if (Id > oAST.Id) + else if (Id() > oAST.Id()) return +1; else return 0; @@ -79,7 +80,7 @@ import java.lang.Exception; /** * 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 . @@ -91,7 +92,7 @@ import java.lang.Exception; - if (ReferenceEquals(Context, ctx)) + if (Context() == ctx) return this; else return new AST(ctx, Native.translate(Context().nCtx(), NativeObject(), ctx.nCtx())); @@ -100,7 +101,7 @@ import java.lang.Exception; /** * 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 @@ -109,10 +110,10 @@ import java.lang.Exception; { switch (ASTKind()) { - case Z3_ast_kind.Z3_APP_AST: - case Z3_ast_kind.Z3_NUMERAL_AST: - case Z3_ast_kind.Z3_QUANTIFIER_AST: - case Z3_ast_kind.Z3_VAR_AST: return true; + case Z3_APP_AST: + case Z3_NUMERAL_AST: + case Z3_QUANTIFIER_AST: + case Z3_VAR_AST: return true; default: return false; } } @@ -174,22 +175,22 @@ import java.lang.Exception; void IncRef(long o) { // Console.WriteLine("AST IncRef()"); - if (Context == null) + if (Context() == null) throw new Z3Exception("inc() called on null context"); if (o == 0) throw new Z3Exception("inc() called on null AST"); - Context.AST_DRQ.IncAndClear(Context, o); + Context().AST_DRQ().IncAndClear(Context(), o); super.IncRef(o); } void DecRef(long o) { // Console.WriteLine("AST DecRef()"); - if (Context == null) + if (Context() == null) throw new Z3Exception("dec() called on null context"); if (o == 0) throw new Z3Exception("dec() called on null AST"); - Context.AST_DRQ.Add(o); + Context().AST_DRQ().Add(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_ast_kind.Z3_QUANTIFIER_AST: return new Quantifier(ctx, obj); - case Z3_ast_kind.Z3_SORT_AST: return Sort.Create(ctx, obj); - case Z3_ast_kind.Z3_APP_AST: - case Z3_ast_kind.Z3_NUMERAL_AST: - case Z3_ast_kind.Z3_VAR_AST: return Expr.Create(ctx, obj); + case Z3_FUNC_DECL_AST: return new FuncDecl(ctx, obj); + case Z3_QUANTIFIER_AST: return new Quantifier(ctx, obj); + case Z3_SORT_AST: return Sort.Create(ctx, obj); + case Z3_APP_AST: + case Z3_NUMERAL_AST: + case Z3_VAR_AST: return Expr.Create(ctx, obj); default: throw new Z3Exception("Unknown AST kind"); } diff --git a/src/api/java/com/Microsoft/Z3/ASTMap.java b/src/api/java/com/Microsoft/Z3/ASTMap.java index 837779234..defd7e736 100644 --- a/src/api/java/com/Microsoft/Z3/ASTMap.java +++ b/src/api/java/com/Microsoft/Z3/ASTMap.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* 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 **/ - public long Size() { return Native.astMapSize(Context().nCtx(), NativeObject()); } + public int Size() { return Native.astMapSize(Context().nCtx(), NativeObject()); } /** * The keys stored in the map. **/ 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) { - Context.ASTMap_DRQ.IncAndClear(Context, o); + Context().ASTMap_DRQ().IncAndClear(Context(), o); super.IncRef(o); } void DecRef(long o) { - Context.ASTMap_DRQ.Add(o); + Context().ASTMap_DRQ().Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/ASTVector.java b/src/api/java/com/Microsoft/Z3/ASTVector.java index 2bb1ab3e0..83d8173e6 100644 --- a/src/api/java/com/Microsoft/Z3/ASTVector.java +++ b/src/api/java/com/Microsoft/Z3/ASTVector.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -18,7 +19,7 @@ import java.lang.Exception; /** * 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. @@ -26,24 +27,24 @@ import java.lang.Exception; * Index * @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 . * The new size of the vector. **/ - public void Resize(long newSize) + public void Resize(int 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) { - Context.ASTVector_DRQ.IncAndClear(Context, o); + Context().ASTVector_DRQ().IncAndClear(Context(), o); super.IncRef(o); } void DecRef(long o) { - Context.ASTVector_DRQ.Add(o); + Context().ASTVector_DRQ().Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/AlgebraicNum.java b/src/api/java/com/Microsoft/Z3/AlgebraicNum.java index eccd15556..b9f5766ce 100644 --- a/src/api/java/com/Microsoft/Z3/AlgebraicNum.java +++ b/src/api/java/com/Microsoft/Z3/AlgebraicNum.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Numerics; */ @@ -23,11 +24,11 @@ import java.lang.Exception; * the precision of the result * @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; * * @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. * The result has at most decimal places. **/ - public String ToDecimal(long precision) + public String ToDecimal(int precision) { diff --git a/src/api/java/com/Microsoft/Z3/ApplyResult.java b/src/api/java/com/Microsoft/Z3/ApplyResult.java index 51be63496..016b2f055 100644 --- a/src/api/java/com/Microsoft/Z3/ApplyResult.java +++ b/src/api/java/com/Microsoft/Z3/ApplyResult.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -19,7 +20,7 @@ import java.lang.Exception; /** * 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. @@ -29,10 +30,10 @@ import java.lang.Exception; - long n = NumSubgoals; + int n = NumSubgoals(); Goal[] res = new Goal[n]; - for (long i; i < n; i++) - res[i] = new Goal(Context, Native.applyResultGetSubgoal(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = new Goal(Context(), Native.applyResultGetSubgoal(Context().nCtx(), NativeObject(), i)); return res; } @@ -41,12 +42,12 @@ import java.lang.Exception; * goal g, that the ApplyResult was obtained from. * @return A model for g **/ - 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) { - Context.ApplyResult_DRQ.IncAndClear(Context, o); + Context().ApplyResult_DRQ().IncAndClear(Context(), o); super.IncRef(o); } void DecRef(long o) { - Context.ApplyResult_DRQ.Add(o); + Context().ApplyResult_DRQ().Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/ArithExpr.java b/src/api/java/com/Microsoft/Z3/ArithExpr.java index 7920bdded..8df3bb0a5 100644 --- a/src/api/java/com/Microsoft/Z3/ArithExpr.java +++ b/src/api/java/com/Microsoft/Z3/ArithExpr.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Collections.Generic; */ /* using System.Linq; */ diff --git a/src/api/java/com/Microsoft/Z3/ArithSort.java b/src/api/java/com/Microsoft/Z3/ArithSort.java index a6e339e30..009112494 100644 --- a/src/api/java/com/Microsoft/Z3/ArithSort.java +++ b/src/api/java/com/Microsoft/Z3/ArithSort.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ diff --git a/src/api/java/com/Microsoft/Z3/ArrayExpr.java b/src/api/java/com/Microsoft/Z3/ArrayExpr.java index bc03135aa..27495fb64 100644 --- a/src/api/java/com/Microsoft/Z3/ArrayExpr.java +++ b/src/api/java/com/Microsoft/Z3/ArrayExpr.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Collections.Generic; */ /* using System.Linq; */ diff --git a/src/api/java/com/Microsoft/Z3/ArraySort.java b/src/api/java/com/Microsoft/Z3/ArraySort.java index cd00df084..b3c5ee7c3 100644 --- a/src/api/java/com/Microsoft/Z3/ArraySort.java +++ b/src/api/java/com/Microsoft/Z3/ArraySort.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* 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, Sort domain, Sort range) - { super(ctx, Native.mkArraySort(ctx.nCtx(), domain.NativeObject, range.NativeObject)); + { super(ctx, Native.mkArraySort(ctx.nCtx(), domain.NativeObject(), range.NativeObject())); diff --git a/src/api/java/com/Microsoft/Z3/BitVecExpr.java b/src/api/java/com/Microsoft/Z3/BitVecExpr.java index 62a03cd06..bbb13a873 100644 --- a/src/api/java/com/Microsoft/Z3/BitVecExpr.java +++ b/src/api/java/com/Microsoft/Z3/BitVecExpr.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Collections.Generic; */ /* using System.Linq; */ @@ -22,7 +23,7 @@ import java.lang.Exception; /** * 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 **/ diff --git a/src/api/java/com/Microsoft/Z3/BitVecNum.java b/src/api/java/com/Microsoft/Z3/BitVecNum.java index 81389dd4b..6a46fc852 100644 --- a/src/api/java/com/Microsoft/Z3/BitVecNum.java +++ b/src/api/java/com/Microsoft/Z3/BitVecNum.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Numerics; */ @@ -22,7 +23,7 @@ import java.lang.Exception; public long UInt64() { 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"); return res; } @@ -33,7 +34,7 @@ import java.lang.Exception; public int Int() { 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"); return res; } @@ -44,7 +45,7 @@ import java.lang.Exception; public long Int64() { 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"); return res; } @@ -52,11 +53,11 @@ import java.lang.Exception; /** * Retrieve the int value. **/ - public long UInt() + public int UInt() { - long res = 0; - if (Native.getNumeralLong(Context().nCtx(), NativeObject(), res) == 0) - throw new Z3Exception("Numeral is not a long"); + int res = 0; + if (Native.getNumeralInt(Context().nCtx(), NativeObject(), res) ^ true) + throw new Z3Exception("Numeral is not a int"); return res; } @@ -65,7 +66,7 @@ import java.lang.Exception; **/ public BigInteger BigInteger() { - return BigInteger.Parse(this.ToString()); + return new BigInteger(this.toString()); } /** diff --git a/src/api/java/com/Microsoft/Z3/BitVecSort.java b/src/api/java/com/Microsoft/Z3/BitVecSort.java index 0ed24573a..4f9f1a2e2 100644 --- a/src/api/java/com/Microsoft/Z3/BitVecSort.java +++ b/src/api/java/com/Microsoft/Z3/BitVecSort.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -18,8 +19,7 @@ import java.lang.Exception; /** * 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 size) { super(ctx, Native.mkBvSort(ctx.nCtx(), size)); { }} }; diff --git a/src/api/java/com/Microsoft/Z3/BoolExpr.java b/src/api/java/com/Microsoft/Z3/BoolExpr.java index 65778ba44..7644b4400 100644 --- a/src/api/java/com/Microsoft/Z3/BoolExpr.java +++ b/src/api/java/com/Microsoft/Z3/BoolExpr.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Collections.Generic; */ /* using System.Linq; */ diff --git a/src/api/java/com/Microsoft/Z3/BoolSort.java b/src/api/java/com/Microsoft/Z3/BoolSort.java index 9b05607ac..13d4f2f1d 100644 --- a/src/api/java/com/Microsoft/Z3/BoolSort.java +++ b/src/api/java/com/Microsoft/Z3/BoolSort.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ diff --git a/src/api/java/com/Microsoft/Z3/Constructor.java b/src/api/java/com/Microsoft/Z3/Constructor.java index caead4737..d7d534873 100644 --- a/src/api/java/com/Microsoft/Z3/Constructor.java +++ b/src/api/java/com/Microsoft/Z3/Constructor.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -18,7 +19,7 @@ import java.lang.Exception; /** * The number of fields of the constructor. **/ - public long NumFields() + public int NumFields() { init(); 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_constructorDecl = null; private FuncDecl[] m_accessorDecls = null; Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames, - Sort[] sorts, long[] sortRefs) + Sort[] sorts, int[] sortRefs) { super(ctx); @@ -86,12 +87,12 @@ import java.lang.Exception; if (n != AST.ArrayLength(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"); - 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, Symbol.ArrayToNative(fieldNames), Sort.ArrayToNative(sorts), @@ -110,11 +111,11 @@ import java.lang.Exception; long tester = 0; long[] accessors = new long[n]; Native.queryConstructor(Context().nCtx(), NativeObject(), n, constructor, tester, accessors); - m_constructorDecl = new FuncDecl(Context, constructor); - m_testerDecl = new FuncDecl(Context, tester); + m_constructorDecl = new FuncDecl(Context(), constructor); + m_testerDecl = new FuncDecl(Context(), tester); m_accessorDecls = new FuncDecl[n]; - for (long i; i < n; i++) - m_accessorDecls[i] = new FuncDecl(Context, accessors[i]); + for (int i = 0; i < n; i++) + m_accessorDecls[i] = new FuncDecl(Context(), accessors[i]); } } diff --git a/src/api/java/com/Microsoft/Z3/ConstructorList.java b/src/api/java/com/Microsoft/Z3/ConstructorList.java index 05b85e664..cb8be3b38 100644 --- a/src/api/java/com/Microsoft/Z3/ConstructorList.java +++ b/src/api/java/com/Microsoft/Z3/ConstructorList.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* 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))); } } diff --git a/src/api/java/com/Microsoft/Z3/Context.java b/src/api/java/com/Microsoft/Z3/Context.java index 69a01cb86..079bcaf43 100644 --- a/src/api/java/com/Microsoft/Z3/Context.java +++ b/src/api/java/com/Microsoft/Z3/Context.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Collections.Generic; */ @@ -34,7 +35,7 @@ import java.lang.Exception; long cfg = Native.mkConfig(); - for (Iterator kv = settings.iterator(); kv.hasNext(); ) + for (KeyValuePair kv: settings) Native.setParamValue(cfg, kv.Key, kv.Value); m_ctx = Native.mkContextRc(cfg); Native.delConfig(cfg); @@ -76,8 +77,8 @@ import java.lang.Exception; if (names == null) return null; - Symbol[] result = new Symbol[names.Length]; - for (int i; i < names.Length; ++i) result[i] = MkSymbol(names[i]); + Symbol[] result = new Symbol[names.length]; + for (int i = 0; i < names.length; ++i) result[i] = MkSymbol(names[i]); return result; } @@ -163,11 +164,11 @@ import java.lang.Exception; /** * Create a new bit-vector sort. **/ - public BitVecSort MkBitVecSort(long size) + public BitVecSort MkBitVecSort(int size) { - return new BitVecSort(this, size); + return new BitVecSort(this, Native.mkBvSort(nCtx(), size)); } /** @@ -198,7 +199,7 @@ import java.lang.Exception; CheckContextMatch(name); CheckContextMatch(fieldNames); CheckContextMatch(fieldSorts); - return new TupleSort(this, name, (long)fieldNames.Length, fieldNames, fieldSorts); + return new TupleSort(this, name, (int)fieldNames.length, fieldNames, fieldSorts); } /** @@ -287,7 +288,7 @@ import java.lang.Exception; * if the corresponding sort reference is 0, then the value in sort_refs should be an index * referring to one of the recursive datatypes that is declared. **/ - public Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, long[] sortRefs) + public Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) { @@ -305,7 +306,7 @@ import java.lang.Exception; * * @return **/ - public Constructor MkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, long[] sortRefs) + public Constructor MkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs) { @@ -356,21 +357,21 @@ import java.lang.Exception; CheckContextMatch(names); - long n = (long)names.Length; + int n = (int)names.length; ConstructorList[] cla = new ConstructorList[n]; long[] n_constr = new long[n]; - for (long i; i < n; i++) + for (int i = 0; i < n; i++) { - var constructor = c[i]; + Constructor[] constructor = c[i]; CheckContextMatch(constructor); cla[i] = new ConstructorList(this, constructor); n_constr[i] = cla[i].NativeObject(); } long[] n_res = new long[n]; - Native.mkDatatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr); + Native.mkDatatypes(nCtx(), n, Symbol.ArrayToNative(names), n_res, n_constr); DatatypeSort[] res = new DatatypeSort[n]; - for (long i; i < n; i++) + for (int i = 0; i < n; i++) res[i] = new DatatypeSort(this, n_res[i]); return res; } @@ -517,12 +518,12 @@ import java.lang.Exception; * The de-Bruijn index of the variable * The sort of the variable **/ - public Expr MkBound(long index, Sort ty) + public Expr MkBound(int index, Sort ty) { - return Expr.Create(this, Native.mkBound(nCtx, index, ty.NativeObject)); + return Expr.Create(this, Native.mkBound(nCtx(), index, ty.NativeObject())); } /** @@ -531,7 +532,7 @@ import java.lang.Exception; public Pattern MkPattern(Expr[] terms) { - if (terms.Length == 0) + if (terms.length == 0) throw new Z3Exception("Cannot create a pattern from zero terms"); @@ -539,7 +540,7 @@ import java.lang.Exception; long[] termsNative = AST.ArrayToNative(terms); - return new Pattern(this, Native.mkPattern(nCtx, (long)terms.Length, termsNative)); + return new Pattern(this, Native.mkPattern(nCtx(), (int)terms.length, termsNative)); } /** @@ -554,7 +555,7 @@ import java.lang.Exception; CheckContextMatch(name); CheckContextMatch(range); - return Expr.Create(this, Native.mkConst(nCtx, name.NativeObject, range.NativeObject)); + return Expr.Create(this, Native.mkConst(nCtx(), name.NativeObject(), range.NativeObject())); } /** @@ -578,7 +579,7 @@ import java.lang.Exception; CheckContextMatch(range); - return Expr.Create(this, Native.mkFreshConst(nCtx, prefix, range.NativeObject)); + return Expr.Create(this, Native.mkFreshConst(nCtx(), prefix, range.NativeObject())); } /** @@ -601,7 +602,7 @@ import java.lang.Exception; - return (BoolExpr)MkConst(name, BoolSort); + return (BoolExpr)MkConst(name, BoolSort()); } /** @@ -611,7 +612,7 @@ import java.lang.Exception; { - return (BoolExpr)MkConst(MkSymbol(name), BoolSort); + return (BoolExpr)MkConst(MkSymbol(name), BoolSort()); } /** @@ -622,7 +623,7 @@ import java.lang.Exception; - return (IntExpr)MkConst(name, IntSort); + return (IntExpr)MkConst(name, IntSort()); } /** @@ -633,7 +634,7 @@ import java.lang.Exception; - return (IntExpr)MkConst(name, IntSort); + return (IntExpr)MkConst(name, IntSort()); } /** @@ -644,7 +645,7 @@ import java.lang.Exception; - return (RealExpr)MkConst(name, RealSort); + return (RealExpr)MkConst(name, RealSort()); } /** @@ -654,13 +655,13 @@ import java.lang.Exception; { - return (RealExpr)MkConst(name, RealSort); + return (RealExpr)MkConst(name, RealSort()); } /** * Creates a bit-vector constant. **/ - public BitVecExpr MkBVConst(Symbol name, long size) + public BitVecExpr MkBVConst(Symbol name, int size) { @@ -671,7 +672,7 @@ import java.lang.Exception; /** * Creates a bit-vector constant. **/ - public BitVecExpr MkBVConst(String name, long size) + public BitVecExpr MkBVConst(String name, int size) { @@ -699,7 +700,7 @@ import java.lang.Exception; { - return new BoolExpr(this, Native.mkTrue(nCtx)); + return new BoolExpr(this, Native.mkTrue(nCtx())); } /** @@ -709,7 +710,7 @@ import java.lang.Exception; { - return new BoolExpr(this, Native.mkFalse(nCtx)); + return new BoolExpr(this, Native.mkFalse(nCtx())); } /** @@ -733,7 +734,7 @@ import java.lang.Exception; CheckContextMatch(x); CheckContextMatch(y); - return new BoolExpr(this, Native.mkEq(nCtx, x.NativeObject, y.NativeObject)); + return new BoolExpr(this, Native.mkEq(nCtx(), x.NativeObject(), y.NativeObject())); } /** @@ -747,7 +748,7 @@ import java.lang.Exception; CheckContextMatch(args); - return new BoolExpr(this, Native.mkDistinct(nCtx, (long)args.Length, AST.ArrayToNative(args))); + return new BoolExpr(this, Native.mkDistinct(nCtx(), (int)args.length, AST.ArrayToNative(args))); } /** @@ -759,7 +760,7 @@ import java.lang.Exception; CheckContextMatch(a); - return new BoolExpr(this, Native.mkNot(nCtx, a.NativeObject)); + return new BoolExpr(this, Native.mkNot(nCtx(), a.NativeObject())); } /** @@ -778,7 +779,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); CheckContextMatch(t3); - return Expr.Create(this, Native.mkIte(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject)); + return Expr.Create(this, Native.mkIte(nCtx(), t1.NativeObject(), t2.NativeObject(), t3.NativeObject())); } /** @@ -792,7 +793,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkIff(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkIff(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -806,7 +807,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkImplies(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkImplies(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -820,7 +821,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkXor(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkXor(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -833,7 +834,7 @@ import java.lang.Exception; CheckContextMatch(t); - return new BoolExpr(this, Native.mkAnd(nCtx, (long)t.Length, AST.ArrayToNative(t))); + return new BoolExpr(this, Native.mkAnd(nCtx(), (int)t.length, AST.ArrayToNative(t))); } /** @@ -846,7 +847,7 @@ import java.lang.Exception; CheckContextMatch(t); - return new BoolExpr(this, Native.mkOr(nCtx, (long)t.Length, AST.ArrayToNative(t))); + return new BoolExpr(this, Native.mkOr(nCtx(), (int)t.length, AST.ArrayToNative(t))); } /** @@ -859,7 +860,7 @@ import java.lang.Exception; CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Native.mkAdd(nCtx, (long)t.Length, AST.ArrayToNative(t))); + return (ArithExpr)Expr.Create(this, Native.mkAdd(nCtx(), (int)t.length, AST.ArrayToNative(t))); } /** @@ -872,7 +873,7 @@ import java.lang.Exception; CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Native.mkMul(nCtx, (long)t.Length, AST.ArrayToNative(t))); + return (ArithExpr)Expr.Create(this, Native.mkMul(nCtx(), (int)t.length, AST.ArrayToNative(t))); } /** @@ -885,7 +886,7 @@ import java.lang.Exception; CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Native.mkSub(nCtx, (long)t.Length, AST.ArrayToNative(t))); + return (ArithExpr)Expr.Create(this, Native.mkSub(nCtx(), (int)t.length, AST.ArrayToNative(t))); } /** @@ -897,7 +898,7 @@ import java.lang.Exception; CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Native.mkUnaryMinus(nCtx, t.NativeObject)); + return (ArithExpr)Expr.Create(this, Native.mkUnaryMinus(nCtx(), t.NativeObject())); } /** @@ -911,7 +912,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return (ArithExpr)Expr.Create(this, Native.mkDiv(nCtx, t1.NativeObject, t2.NativeObject)); + return (ArithExpr)Expr.Create(this, Native.mkDiv(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -926,7 +927,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new IntExpr(this, Native.mkMod(nCtx, t1.NativeObject, t2.NativeObject)); + return new IntExpr(this, Native.mkMod(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -941,7 +942,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new IntExpr(this, Native.mkRem(nCtx, t1.NativeObject, t2.NativeObject)); + return new IntExpr(this, Native.mkRem(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -955,7 +956,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return (ArithExpr)Expr.Create(this, Native.mkPower(nCtx, t1.NativeObject, t2.NativeObject)); + return (ArithExpr)Expr.Create(this, Native.mkPower(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -969,7 +970,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkLt(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkLt(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -983,7 +984,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkLe(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkLe(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -997,7 +998,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkGt(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkGt(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1011,7 +1012,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkGe(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkGe(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1030,7 +1031,7 @@ import java.lang.Exception; CheckContextMatch(t); - return new RealExpr(this, Native.mkInt2real(nCtx, t.NativeObject)); + return new RealExpr(this, Native.mkInt2real(nCtx(), t.NativeObject())); } /** @@ -1046,7 +1047,7 @@ import java.lang.Exception; CheckContextMatch(t); - return new IntExpr(this, Native.mkReal2int(nCtx, t.NativeObject)); + return new IntExpr(this, Native.mkReal2int(nCtx(), t.NativeObject())); } /** @@ -1058,7 +1059,7 @@ import java.lang.Exception; CheckContextMatch(t); - return new BoolExpr(this, Native.mkIsInt(nCtx, t.NativeObject)); + return new BoolExpr(this, Native.mkIsInt(nCtx(), t.NativeObject())); } /** @@ -1071,7 +1072,7 @@ import java.lang.Exception; CheckContextMatch(t); - return new BitVecExpr(this, Native.mkBvnot(nCtx, t.NativeObject)); + return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.NativeObject())); } /** @@ -1084,7 +1085,7 @@ import java.lang.Exception; CheckContextMatch(t); - return new BitVecExpr(this, Native.mkBvredand(nCtx, t.NativeObject)); + return new BitVecExpr(this, Native.mkBvredand(nCtx(), t.NativeObject())); } /** @@ -1097,7 +1098,7 @@ import java.lang.Exception; CheckContextMatch(t); - return new BitVecExpr(this, Native.mkBvredor(nCtx, t.NativeObject)); + return new BitVecExpr(this, Native.mkBvredor(nCtx(), t.NativeObject())); } /** @@ -1112,7 +1113,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvand(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvand(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1127,7 +1128,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvor(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1142,7 +1143,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvxor(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvxor(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1157,7 +1158,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvnand(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvnand(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1172,7 +1173,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvnor(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvnor(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1187,7 +1188,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvxnor(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvxnor(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1200,7 +1201,7 @@ import java.lang.Exception; CheckContextMatch(t); - return new BitVecExpr(this, Native.mkBvneg(nCtx, t.NativeObject)); + return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.NativeObject())); } /** @@ -1215,7 +1216,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvadd(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvadd(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1230,7 +1231,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvsub(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvsub(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1245,7 +1246,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvmul(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvmul(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1265,7 +1266,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvudiv(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvudiv(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1289,7 +1290,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvsdiv(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvsdiv(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1308,7 +1309,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvurem(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvurem(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1329,7 +1330,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvsrem(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvsrem(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1347,7 +1348,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvsmod(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvsmod(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1364,7 +1365,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvult(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkBvult(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1381,7 +1382,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvslt(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1398,7 +1399,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvule(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkBvule(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1415,7 +1416,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvsle(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1432,7 +1433,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvuge(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1449,7 +1450,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvsge(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1466,7 +1467,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvugt(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1483,7 +1484,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvsgt(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1504,7 +1505,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkConcat(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkConcat(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1516,13 +1517,13 @@ import java.lang.Exception; * The argument must have a bit-vector sort. * **/ - public BitVecExpr MkExtract(long high, long low, BitVecExpr t) + public BitVecExpr MkExtract(int high, int low, BitVecExpr t) { CheckContextMatch(t); - return new BitVecExpr(this, Native.mkExtract(nCtx, high, low, t.NativeObject)); + return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low, t.NativeObject())); } /** @@ -1533,13 +1534,13 @@ import java.lang.Exception; * The argument must have a bit-vector sort. * **/ - public BitVecExpr MkSignExt(long i, BitVecExpr t) + public BitVecExpr MkSignExt(int i, BitVecExpr t) { CheckContextMatch(t); - return new BitVecExpr(this, Native.mkSignExt(nCtx, i, t.NativeObject)); + return new BitVecExpr(this, Native.mkSignExt(nCtx(), i, t.NativeObject())); } /** @@ -1551,13 +1552,13 @@ import java.lang.Exception; * The argument must have a bit-vector sort. * **/ - public BitVecExpr MkZeroExt(long i, BitVecExpr t) + public BitVecExpr MkZeroExt(int i, BitVecExpr t) { CheckContextMatch(t); - return new BitVecExpr(this, Native.mkZeroExt(nCtx, i, t.NativeObject)); + return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i, t.NativeObject())); } /** @@ -1566,13 +1567,13 @@ import java.lang.Exception; * The argument must have a bit-vector sort. * **/ - public BitVecExpr MkRepeat(long i, BitVecExpr t) + public BitVecExpr MkRepeat(int i, BitVecExpr t) { CheckContextMatch(t); - return new BitVecExpr(this, Native.mkRepeat(nCtx, i, t.NativeObject)); + return new BitVecExpr(this, Native.mkRepeat(nCtx(), i, t.NativeObject())); } /** @@ -1595,7 +1596,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvshl(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvshl(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1618,7 +1619,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvlshr(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvlshr(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1643,7 +1644,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkBvashr(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkBvashr(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1653,13 +1654,13 @@ import java.lang.Exception; * The argument must have a bit-vector sort. * **/ - public BitVecExpr MkBVRotateLeft(long i, BitVecExpr t) + public BitVecExpr MkBVRotateLeft(int i, BitVecExpr t) { CheckContextMatch(t); - return new BitVecExpr(this, Native.mkRotateLeft(nCtx, i, t.NativeObject)); + return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i, t.NativeObject())); } /** @@ -1669,13 +1670,13 @@ import java.lang.Exception; * The argument must have a bit-vector sort. * **/ - public BitVecExpr MkBVRotateRight(long i, BitVecExpr t) + public BitVecExpr MkBVRotateRight(int i, BitVecExpr t) { CheckContextMatch(t); - return new BitVecExpr(this, Native.mkRotateRight(nCtx, i, t.NativeObject)); + return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i, t.NativeObject())); } /** @@ -1693,7 +1694,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1711,7 +1712,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BitVecExpr(this, Native.mkExtRotateRight(nCtx, t1.NativeObject, t2.NativeObject)); + return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1724,13 +1725,13 @@ import java.lang.Exception; * The argument must be of integer sort. * **/ - public BitVecExpr MkInt2BV(long n, IntExpr t) + public BitVecExpr MkInt2BV(int n, IntExpr t) { CheckContextMatch(t); - return new BitVecExpr(this, Native.mkInt2bv(nCtx, n, t.NativeObject)); + return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n, t.NativeObject())); } /** @@ -1754,7 +1755,7 @@ import java.lang.Exception; CheckContextMatch(t); - return new IntExpr(this, Native.mkBv2int(nCtx, t.NativeObject, (signed) ? 1 : 0)); + return new IntExpr(this, Native.mkBv2int(nCtx(), t.NativeObject(), (signed) ? true : false)); } /** @@ -1771,7 +1772,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0)); + return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1.NativeObject(), t2.NativeObject(), (isSigned) ? true : false)); } /** @@ -1788,7 +1789,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1805,7 +1806,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1822,7 +1823,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0)); + return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1.NativeObject(), t2.NativeObject(), (isSigned) ? true : false)); } /** @@ -1839,7 +1840,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1854,7 +1855,7 @@ import java.lang.Exception; CheckContextMatch(t); - return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx, t.NativeObject)); + return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(), t.NativeObject())); } /** @@ -1871,7 +1872,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0)); + return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1.NativeObject(), t2.NativeObject(), (isSigned) ? true : false)); } /** @@ -1888,7 +1889,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx, t1.NativeObject, t2.NativeObject)); + return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -1937,7 +1938,7 @@ import java.lang.Exception; CheckContextMatch(a); CheckContextMatch(i); - return Expr.Create(this, Native.mkSelect(nCtx, a.NativeObject, i.NativeObject)); + return Expr.Create(this, Native.mkSelect(nCtx(), a.NativeObject(), i.NativeObject())); } /** @@ -1967,7 +1968,7 @@ import java.lang.Exception; CheckContextMatch(a); CheckContextMatch(i); CheckContextMatch(v); - return new ArrayExpr(this, Native.mkStore(nCtx, a.NativeObject, i.NativeObject, v.NativeObject)); + return new ArrayExpr(this, Native.mkStore(nCtx(), a.NativeObject(), i.NativeObject(), v.NativeObject())); } /** @@ -1987,7 +1988,7 @@ import java.lang.Exception; CheckContextMatch(domain); CheckContextMatch(v); - return new ArrayExpr(this, Native.mkConstArray(nCtx, domain.NativeObject, v.NativeObject)); + return new ArrayExpr(this, Native.mkConstArray(nCtx(), domain.NativeObject(), v.NativeObject())); } /** @@ -2009,7 +2010,7 @@ import java.lang.Exception; CheckContextMatch(f); CheckContextMatch(args); - return (ArrayExpr)Expr.Create(this, Native.mkMap(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args))); + return (ArrayExpr)Expr.Create(this, Native.mkMap(nCtx(), f.NativeObject(), AST.ArrayLength(args), AST.ArrayToNative(args))); } /** @@ -2025,7 +2026,7 @@ import java.lang.Exception; CheckContextMatch(array); - return Expr.Create(this, Native.mkArrayDefault(nCtx, array.NativeObject)); + return Expr.Create(this, Native.mkArrayDefault(nCtx(), array.NativeObject())); } /** @@ -2049,7 +2050,7 @@ import java.lang.Exception; CheckContextMatch(domain); - return Expr.Create(this, Native.mkEmptySet(nCtx, domain.NativeObject)); + return Expr.Create(this, Native.mkEmptySet(nCtx(), domain.NativeObject())); } /** @@ -2061,7 +2062,7 @@ import java.lang.Exception; CheckContextMatch(domain); - return Expr.Create(this, Native.mkFullSet(nCtx, domain.NativeObject)); + return Expr.Create(this, Native.mkFullSet(nCtx(), domain.NativeObject())); } /** @@ -2075,7 +2076,7 @@ import java.lang.Exception; CheckContextMatch(set); CheckContextMatch(element); - return Expr.Create(this, Native.mkSetAdd(nCtx, set.NativeObject, element.NativeObject)); + return Expr.Create(this, Native.mkSetAdd(nCtx(), set.NativeObject(), element.NativeObject())); } @@ -2090,7 +2091,7 @@ import java.lang.Exception; CheckContextMatch(set); CheckContextMatch(element); - return Expr.Create(this, Native.mkSetDel(nCtx, set.NativeObject, element.NativeObject)); + return Expr.Create(this, Native.mkSetDel(nCtx(), set.NativeObject(), element.NativeObject())); } /** @@ -2102,7 +2103,7 @@ import java.lang.Exception; CheckContextMatch(args); - return Expr.Create(this, Native.mkSetUnion(nCtx, (long)args.Length, AST.ArrayToNative(args))); + return Expr.Create(this, Native.mkSetUnion(nCtx(), (int)args.length, AST.ArrayToNative(args))); } /** @@ -2115,7 +2116,7 @@ import java.lang.Exception; CheckContextMatch(args); - return Expr.Create(this, Native.mkSetIntersect(nCtx, (long)args.Length, AST.ArrayToNative(args))); + return Expr.Create(this, Native.mkSetIntersect(nCtx(), (int)args.length, AST.ArrayToNative(args))); } /** @@ -2129,7 +2130,7 @@ import java.lang.Exception; CheckContextMatch(arg1); CheckContextMatch(arg2); - return Expr.Create(this, Native.mkSetDifference(nCtx, arg1.NativeObject, arg2.NativeObject)); + return Expr.Create(this, Native.mkSetDifference(nCtx(), arg1.NativeObject(), arg2.NativeObject())); } /** @@ -2141,7 +2142,7 @@ import java.lang.Exception; CheckContextMatch(arg); - return Expr.Create(this, Native.mkSetComplement(nCtx, arg.NativeObject)); + return Expr.Create(this, Native.mkSetComplement(nCtx(), arg.NativeObject())); } /** @@ -2155,7 +2156,7 @@ import java.lang.Exception; CheckContextMatch(elem); CheckContextMatch(set); - return Expr.Create(this, Native.mkSetMember(nCtx, elem.NativeObject, set.NativeObject)); + return Expr.Create(this, Native.mkSetMember(nCtx(), elem.NativeObject(), set.NativeObject())); } /** @@ -2169,7 +2170,7 @@ import java.lang.Exception; CheckContextMatch(arg1); CheckContextMatch(arg2); - return Expr.Create(this, Native.mkSetSubset(nCtx, arg1.NativeObject, arg2.NativeObject)); + return Expr.Create(this, Native.mkSetSubset(nCtx(), arg1.NativeObject(), arg2.NativeObject())); } @@ -2185,7 +2186,7 @@ import java.lang.Exception; CheckContextMatch(ty); - return Expr.Create(this, Native.mkNumeral(nCtx, v, ty.NativeObject)); + return Expr.Create(this, Native.mkNumeral(nCtx(), v, ty.NativeObject())); } /** @@ -2201,9 +2202,18 @@ import java.lang.Exception; CheckContextMatch(ty); - return Expr.Create(this, Native.mkInt(nCtx, v, ty.NativeObject)); + return Expr.Create(this, Native.mkInt(nCtx(), v, ty.NativeObject())); } + /** + * Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. + * It is slightly faster than MakeNumeral since it is not necessary to parse a string. + * Value of the numeral + * Sort of the numeral + * @return A Term with value and type + **/ + /* Not translated because it would translate to a function with clashing types. */ + /** * Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. * It is slightly faster than MakeNumeral since it is not necessary to parse a string. @@ -2217,7 +2227,7 @@ import java.lang.Exception; CheckContextMatch(ty); - return Expr.Create(this, Native.mkUnsignedInt(nCtx, v, ty.NativeObject)); + return Expr.Create(this, Native.mkInt64(nCtx(), v, ty.NativeObject())); } /** @@ -2227,30 +2237,7 @@ import java.lang.Exception; * Sort of the numeral * @return A Term with value and type **/ - public Expr MkNumeral(long v, Sort ty) - { - - - - CheckContextMatch(ty); - return Expr.Create(this, Native.mkInt64(nCtx, v, ty.NativeObject)); - } - - /** - * Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. - * It is slightly faster than MakeNumeral since it is not necessary to parse a string. - * Value of the numeral - * Sort of the numeral - * @return A Term with value and type - **/ - public Expr MkNumeral(long v, Sort ty) - { - - - - CheckContextMatch(ty); - return Expr.Create(this, Native.mkUnsignedInt64(nCtx, v, ty.NativeObject)); - } + /* Not translated because it would translate to a function with clashing types. */ /** * Create a real from a fraction. @@ -2267,7 +2254,7 @@ import java.lang.Exception; - return new RatNum(this, Native.mkReal(nCtx, num, den)); + return new RatNum(this, Native.mkReal(nCtx(), num, den)); } /** @@ -2279,7 +2266,7 @@ import java.lang.Exception; { - return new RatNum(this, Native.mkNumeral(nCtx, v, RealSort.NativeObject)); + return new RatNum(this, Native.mkNumeral(nCtx(), v, RealSort().NativeObject())); } /** @@ -2291,9 +2278,16 @@ import java.lang.Exception; { - return new RatNum(this, Native.mkInt(nCtx, v, RealSort.NativeObject)); + return new RatNum(this, Native.mkInt(nCtx(), v, RealSort().NativeObject())); } + /** + * Create a real numeral. + * value of the numeral. + * @return A Term with value and sort Real + **/ + /* Not translated because it would translate to a function with clashing types. */ + /** * Create a real numeral. * value of the numeral. @@ -2303,7 +2297,7 @@ import java.lang.Exception; { - return new RatNum(this, Native.mkUnsignedInt(nCtx, v, RealSort.NativeObject)); + return new RatNum(this, Native.mkInt64(nCtx(), v, RealSort().NativeObject())); } /** @@ -2311,24 +2305,7 @@ import java.lang.Exception; * value of the numeral. * @return A Term with value and sort Real **/ - public RatNum MkReal(long v) - { - - - return new RatNum(this, Native.mkInt64(nCtx, v, RealSort.NativeObject)); - } - - /** - * Create a real numeral. - * value of the numeral. - * @return A Term with value and sort Real - **/ - public RatNum MkReal(long v) - { - - - return new RatNum(this, Native.mkUnsignedInt64(nCtx, v, RealSort.NativeObject)); - } + /* Not translated because it would translate to a function with clashing types. */ /** * Create an integer numeral. @@ -2338,7 +2315,7 @@ import java.lang.Exception; { - return new IntNum(this, Native.mkNumeral(nCtx, v, IntSort.NativeObject)); + return new IntNum(this, Native.mkNumeral(nCtx(), v, IntSort().NativeObject())); } /** @@ -2350,9 +2327,16 @@ import java.lang.Exception; { - return new IntNum(this, Native.mkInt(nCtx, v, IntSort.NativeObject)); + return new IntNum(this, Native.mkInt(nCtx(), v, IntSort().NativeObject())); } + /** + * Create an integer numeral. + * value of the numeral. + * @return A Term with value and sort Integer + **/ + /* Not translated because it would translate to a function with clashing types. */ + /** * Create an integer numeral. * value of the numeral. @@ -2362,7 +2346,7 @@ import java.lang.Exception; { - return new IntNum(this, Native.mkUnsignedInt(nCtx, v, IntSort.NativeObject)); + return new IntNum(this, Native.mkInt64(nCtx(), v, IntSort().NativeObject())); } /** @@ -2370,31 +2354,14 @@ import java.lang.Exception; * value of the numeral. * @return A Term with value and sort Integer **/ - public IntNum MkInt(long v) - { - - - return new IntNum(this, Native.mkInt64(nCtx, v, IntSort.NativeObject)); - } - - /** - * Create an integer numeral. - * value of the numeral. - * @return A Term with value and sort Integer - **/ - public IntNum MkInt(long v) - { - - - return new IntNum(this, Native.mkUnsignedInt64(nCtx, v, IntSort.NativeObject)); - } + /* Not translated because it would translate to a function with clashing types. */ /** * Create a bit-vector numeral. * A string representing the value in decimal notation. * the size of the bit-vector **/ - public BitVecNum MkBV(String v, long size) + public BitVecNum MkBV(String v, int size) { @@ -2406,7 +2373,7 @@ import java.lang.Exception; * value of the numeral. * the size of the bit-vector **/ - public BitVecNum MkBV(int v, long size) + public BitVecNum MkBV(int v, int size) { @@ -2418,19 +2385,14 @@ import java.lang.Exception; * value of the numeral. * the size of the bit-vector **/ - public BitVecNum MkBV(long v, long size) - { - - - return (BitVecNum)MkNumeral(v, MkBitVecSort(size)); - } + /* Not translated because it would translate to a function with clashing types. */ /** * Create a bit-vector numeral. * value of the numeral. * * the size of the bit-vector **/ - public BitVecNum MkBV(long v, long size) + public BitVecNum MkBV(long v, int size) { @@ -2442,12 +2404,7 @@ import java.lang.Exception; * value of the numeral. * the size of the bit-vector **/ - public BitVecNum MkBV(long v, long size) - { - - - return (BitVecNum)MkNumeral(v, MkBitVecSort(size)); - } + /* Not translated because it would translate to a function with clashing types. */ /** @@ -2469,7 +2426,7 @@ import java.lang.Exception; * optional symbol to track quantifier. * optional symbol to track skolem constants. **/ - public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, long weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) + public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2489,7 +2446,7 @@ import java.lang.Exception; /** * Create a universal Quantifier. **/ - public Quantifier MkForall(Expr[] boundConstants, Expr body, long weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) + public Quantifier MkForall(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2505,7 +2462,7 @@ import java.lang.Exception; * Create an existential Quantifier. * **/ - public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, long weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) + public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2523,7 +2480,7 @@ import java.lang.Exception; /** * Create an existential Quantifier. **/ - public Quantifier MkExists(Expr[] boundConstants, Expr body, long weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) + public Quantifier MkExists(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2538,7 +2495,7 @@ import java.lang.Exception; /** * Create a Quantifier. **/ - public Quantifier MkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr body, long weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) + public Quantifier MkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2561,7 +2518,7 @@ import java.lang.Exception; /** * Create a Quantifier. **/ - public Quantifier MkQuantifier(boolean universal, Expr[] boundConstants, Expr body, long weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) + public Quantifier MkQuantifier(boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { @@ -2594,7 +2551,7 @@ import java.lang.Exception; * * **/ - public void setPrintMode(Z3_ast_print_mode value) { Native.setAstPrintMode(nCtx, (long)value); } + public void setPrintMode(Z3_ast_print_mode value) { Native.setAstPrintMode(nCtx(), (int)value); } /** * Convert a benchmark into an SMT-LIB formatted string. @@ -2613,9 +2570,9 @@ import java.lang.Exception; - return Native.benchmarkToSmtlibString(nCtx, name, logic, status, attributes, - (long)assumptions.Length, AST.ArrayToNative(assumptions), - formula.NativeObject); + return Native.benchmarkToSmtlibString(nCtx(), name, logic, status, attributes, + (int)assumptions.length, AST.ArrayToNative(assumptions), + formula.NativeObject()); } /** @@ -2630,13 +2587,13 @@ import java.lang.Exception; **/ public void ParseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) { - long csn = Symbol.ArrayLength(sortNames); - long cs = Sort.ArrayLength(sorts); - long cdn = Symbol.ArrayLength(declNames); - long cd = AST.ArrayLength(decls); + int csn = Symbol.ArrayLength(sortNames); + int cs = Sort.ArrayLength(sorts); + int cdn = Symbol.ArrayLength(declNames); + int cd = AST.ArrayLength(decls); if (csn != cs || cdn != cd) throw new Z3Exception("Argument size mismatch"); - Native.parseSmtlibString(nCtx, str, + Native.parseSmtlibString(nCtx(), str, AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)); } @@ -2647,13 +2604,13 @@ import java.lang.Exception; **/ public void ParseSMTLIBFile(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) { - long csn = Symbol.ArrayLength(sortNames); - long cs = Sort.ArrayLength(sorts); - long cdn = Symbol.ArrayLength(declNames); - long cd = AST.ArrayLength(decls); + int csn = Symbol.ArrayLength(sortNames); + int cs = Sort.ArrayLength(sorts); + int cdn = Symbol.ArrayLength(declNames); + int cd = AST.ArrayLength(decls); if (csn != cs || cdn != cd) throw new Z3Exception("Argument size mismatch"); - Native.parseSmtlibFile(nCtx, fileName, + Native.parseSmtlibFile(nCtx(), fileName, AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)); } @@ -2661,7 +2618,7 @@ import java.lang.Exception; /** * The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. **/ - public long NumSMTLIBFormulas () { return Native.getSmtlibNumFormulas(nCtx); } + public int NumSMTLIBFormulas () { return Native.getSmtlibNumFormulas(nCtx()); } /** * The formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. @@ -2670,17 +2627,17 @@ import java.lang.Exception; { - long n = NumSMTLIBFormulas; + int n = NumSMTLIBFormulas(); BoolExpr[] res = new BoolExpr[n]; - for (long i; i < n; i++) - res[i] = (BoolExpr)Expr.Create(this, Native.getSmtlibFormula(nCtx, i)); + for (int i = 0; i < n; i++) + res[i] = (BoolExpr)Expr.Create(this, Native.getSmtlibFormula(nCtx(), i)); return res; } /** * The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. **/ - public long NumSMTLIBAssumptions () { return Native.getSmtlibNumAssumptions(nCtx); } + public int NumSMTLIBAssumptions () { return Native.getSmtlibNumAssumptions(nCtx()); } /** * The assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. @@ -2689,17 +2646,17 @@ import java.lang.Exception; { - long n = NumSMTLIBAssumptions; + int n = NumSMTLIBAssumptions(); BoolExpr[] res = new BoolExpr[n]; - for (long i; i < n; i++) - res[i] = (BoolExpr)Expr.Create(this, Native.getSmtlibAssumption(nCtx, i)); + for (int i = 0; i < n; i++) + res[i] = (BoolExpr)Expr.Create(this, Native.getSmtlibAssumption(nCtx(), i)); return res; } /** * The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. **/ - public long NumSMTLIBDecls () { return Native.getSmtlibNumDecls(nCtx); } + public int NumSMTLIBDecls () { return Native.getSmtlibNumDecls(nCtx()); } /** * The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. @@ -2708,17 +2665,17 @@ import java.lang.Exception; { - long n = NumSMTLIBDecls; + int n = NumSMTLIBDecls(); FuncDecl[] res = new FuncDecl[n]; - for (long i; i < n; i++) - res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx, i)); + for (int i = 0; i < n; i++) + res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i)); return res; } /** * The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. **/ - public long NumSMTLIBSorts () { return Native.getSmtlibNumSorts(nCtx); } + public int NumSMTLIBSorts () { return Native.getSmtlibNumSorts(nCtx()); } /** * The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. @@ -2727,10 +2684,10 @@ import java.lang.Exception; { - long n = NumSMTLIBSorts; + int n = NumSMTLIBSorts(); Sort[] res = new Sort[n]; - for (long i; i < n; i++) - res[i] = Sort.Create(this, Native.getSmtlibSort(nCtx, i)); + for (int i = 0; i < n; i++) + res[i] = Sort.Create(this, Native.getSmtlibSort(nCtx(), i)); return res; } @@ -2743,13 +2700,13 @@ import java.lang.Exception; { - long csn = Symbol.ArrayLength(sortNames); - long cs = Sort.ArrayLength(sorts); - long cdn = Symbol.ArrayLength(declNames); - long cd = AST.ArrayLength(decls); + int csn = Symbol.ArrayLength(sortNames); + int cs = Sort.ArrayLength(sorts); + int cdn = Symbol.ArrayLength(declNames); + int cd = AST.ArrayLength(decls); if (csn != cs || cdn != cd) throw new Z3Exception("Argument size mismatch"); - return (BoolExpr)Expr.Create(this, Native.parseSmtlib2String(nCtx, str, + return (BoolExpr)Expr.Create(this, Native.parseSmtlib2String(nCtx(), str, AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls))); } @@ -2762,13 +2719,13 @@ import java.lang.Exception; { - long csn = Symbol.ArrayLength(sortNames); - long cs = Sort.ArrayLength(sorts); - long cdn = Symbol.ArrayLength(declNames); - long cd = AST.ArrayLength(decls); + int csn = Symbol.ArrayLength(sortNames); + int cs = Sort.ArrayLength(sorts); + int cdn = Symbol.ArrayLength(declNames); + int cd = AST.ArrayLength(decls); if (csn != cs || cdn != cd) throw new Z3Exception("Argument size mismatch"); - return (BoolExpr)Expr.Create(this, Native.parseSmtlib2File(nCtx, fileName, + return (BoolExpr)Expr.Create(this, Native.parseSmtlib2File(nCtx(), fileName, AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls))); } @@ -2803,7 +2760,7 @@ import java.lang.Exception; /** * The number of supported tactics. **/ - public long NumTactics() { return Native.getNumTactics(nCtx); } + public int NumTactics() { return Native.getNumTactics(nCtx()); } /** * The names of all supported tactics. @@ -2812,10 +2769,10 @@ import java.lang.Exception; { - long n = NumTactics; + int n = NumTactics(); String[] res = new String[n]; - for (long i; i < n; i++) - res[i] = Native.getTacticName(nCtx, i); + for (int i = 0; i < n; i++) + res[i] = Native.getTacticName(nCtx(), i); return res; } @@ -2826,7 +2783,7 @@ import java.lang.Exception; { - return Native.tacticGetDescr(nCtx, name); + return Native.tacticGetDescr(nCtx(), name); } /** @@ -2856,19 +2813,19 @@ import java.lang.Exception; CheckContextMatch(ts); long last = 0; - if (ts != null && ts.Length > 0) + if (ts != null && ts.length > 0) { - last = ts[ts.Length - 1].NativeObject(); - for (int i = ts.Length - 2; i >= 0; i--) - last = Native.tacticAndThen(nCtx, ts[i].NativeObject, last); + last = ts[ts.length - 1].NativeObject(); + for (int i = ts.length - 2; i >= 0; i--) + last = Native.tacticAndThen(nCtx(), ts[i].NativeObject(), last); } if (last != 0) { - last = Native.tacticAndThen(nCtx, t2.NativeObject, last); - return new Tactic(this, Native.tacticAndThen(nCtx, t1.NativeObject, last)); + last = Native.tacticAndThen(nCtx(), t2.NativeObject(), last); + return new Tactic(this, Native.tacticAndThen(nCtx(), t1.NativeObject(), last)); } else - return new Tactic(this, Native.tacticAndThen(nCtx, t1.NativeObject, t2.NativeObject)); + return new Tactic(this, Native.tacticAndThen(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -2900,7 +2857,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new Tactic(this, Native.tacticOrElse(nCtx, t1.NativeObject, t2.NativeObject)); + return new Tactic(this, Native.tacticOrElse(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -2909,13 +2866,13 @@ import java.lang.Exception; * If does not terminate within milliseconds, then it fails. * **/ - public Tactic TryFor(Tactic t, long ms) + public Tactic TryFor(Tactic t, int ms) { CheckContextMatch(t); - return new Tactic(this, Native.tacticTryFor(nCtx, t.NativeObject, ms)); + return new Tactic(this, Native.tacticTryFor(nCtx(), t.NativeObject(), ms)); } /** @@ -2933,7 +2890,7 @@ import java.lang.Exception; CheckContextMatch(t); CheckContextMatch(p); - return new Tactic(this, Native.tacticWhen(nCtx, p.NativeObject, t.NativeObject)); + return new Tactic(this, Native.tacticWhen(nCtx(), p.NativeObject(), t.NativeObject())); } /** @@ -2950,20 +2907,20 @@ import java.lang.Exception; CheckContextMatch(p); CheckContextMatch(t1); CheckContextMatch(t2); - return new Tactic(this, Native.tacticCond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject)); + return new Tactic(this, Native.tacticCond(nCtx(), p.NativeObject(), t1.NativeObject(), t2.NativeObject())); } /** * Create a tactic that keeps applying until the goal is not * modified anymore or the maximum number of iterations is reached. **/ - public Tactic Repeat(Tactic t, long max) + public Tactic Repeat(Tactic t, int max) { CheckContextMatch(t); - return new Tactic(this, Native.tacticRepeat(nCtx, t.NativeObject, max)); + return new Tactic(this, Native.tacticRepeat(nCtx(), t.NativeObject(), max)); } /** @@ -2973,7 +2930,7 @@ import java.lang.Exception; { - return new Tactic(this, Native.tacticSkip(nCtx)); + return new Tactic(this, Native.tacticSkip(nCtx())); } /** @@ -2983,7 +2940,7 @@ import java.lang.Exception; { - return new Tactic(this, Native.tacticFail(nCtx)); + return new Tactic(this, Native.tacticFail(nCtx())); } /** @@ -2995,7 +2952,7 @@ import java.lang.Exception; CheckContextMatch(p); - return new Tactic(this, Native.tacticFailIf(nCtx, p.NativeObject)); + return new Tactic(this, Native.tacticFailIf(nCtx(), p.NativeObject())); } /** @@ -3006,7 +2963,7 @@ import java.lang.Exception; { - return new Tactic(this, Native.tacticFailIfNotDecided(nCtx)); + return new Tactic(this, Native.tacticFailIfNotDecided(nCtx())); } /** @@ -3020,7 +2977,7 @@ import java.lang.Exception; CheckContextMatch(t); CheckContextMatch(p); - return new Tactic(this, Native.tacticUsingParams(nCtx, t.NativeObject, p.NativeObject)); + return new Tactic(this, Native.tacticUsingParams(nCtx(), t.NativeObject(), p.NativeObject())); } /** @@ -3045,7 +3002,7 @@ import java.lang.Exception; CheckContextMatch(t); - return new Tactic(this, Native.tacticParOr(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t))); + return new Tactic(this, Native.tacticParOr(nCtx(), Tactic.ArrayLength(t), Tactic.ArrayToNative(t))); } /** @@ -3060,7 +3017,7 @@ import java.lang.Exception; CheckContextMatch(t1); CheckContextMatch(t2); - return new Tactic(this, Native.tacticParAndThen(nCtx, t1.NativeObject, t2.NativeObject)); + return new Tactic(this, Native.tacticParAndThen(nCtx(), t1.NativeObject(), t2.NativeObject())); } /** @@ -3069,13 +3026,13 @@ import java.lang.Exception; **/ public void Interrupt() { - Native.interrupt(nCtx); + Native.interrupt(nCtx()); } /** * The number of supported Probes. **/ - public long NumProbes() { return Native.getNumProbes(nCtx); } + public int NumProbes() { return Native.getNumProbes(nCtx()); } /** * The names of all supported Probes. @@ -3084,10 +3041,10 @@ import java.lang.Exception; { - long n = NumProbes; + int n = NumProbes(); String[] res = new String[n]; - for (long i; i < n; i++) - res[i] = Native.getProbeName(nCtx, i); + for (int i = 0; i < n; i++) + res[i] = Native.getProbeName(nCtx(), i); return res; } @@ -3098,7 +3055,7 @@ import java.lang.Exception; { - return Native.probeGetDescr(nCtx, name); + return Native.probeGetDescr(nCtx(), name); } /** @@ -3118,7 +3075,7 @@ import java.lang.Exception; { - return new Probe(this, Native.probeConst(nCtx, val)); + return new Probe(this, Native.probeConst(nCtx(), val)); } /** @@ -3133,7 +3090,7 @@ import java.lang.Exception; CheckContextMatch(p1); CheckContextMatch(p2); - return new Probe(this, Native.probeLt(nCtx, p1.NativeObject, p2.NativeObject)); + return new Probe(this, Native.probeLt(nCtx(), p1.NativeObject(), p2.NativeObject())); } /** @@ -3148,7 +3105,7 @@ import java.lang.Exception; CheckContextMatch(p1); CheckContextMatch(p2); - return new Probe(this, Native.probeGt(nCtx, p1.NativeObject, p2.NativeObject)); + return new Probe(this, Native.probeGt(nCtx(), p1.NativeObject(), p2.NativeObject())); } /** @@ -3163,7 +3120,7 @@ import java.lang.Exception; CheckContextMatch(p1); CheckContextMatch(p2); - return new Probe(this, Native.probeLe(nCtx, p1.NativeObject, p2.NativeObject)); + return new Probe(this, Native.probeLe(nCtx(), p1.NativeObject(), p2.NativeObject())); } /** @@ -3178,7 +3135,7 @@ import java.lang.Exception; CheckContextMatch(p1); CheckContextMatch(p2); - return new Probe(this, Native.probeGe(nCtx, p1.NativeObject, p2.NativeObject)); + return new Probe(this, Native.probeGe(nCtx(), p1.NativeObject(), p2.NativeObject())); } /** @@ -3193,7 +3150,7 @@ import java.lang.Exception; CheckContextMatch(p1); CheckContextMatch(p2); - return new Probe(this, Native.probeEq(nCtx, p1.NativeObject, p2.NativeObject)); + return new Probe(this, Native.probeEq(nCtx(), p1.NativeObject(), p2.NativeObject())); } /** @@ -3208,7 +3165,7 @@ import java.lang.Exception; CheckContextMatch(p1); CheckContextMatch(p2); - return new Probe(this, Native.probeAnd(nCtx, p1.NativeObject, p2.NativeObject)); + return new Probe(this, Native.probeAnd(nCtx(), p1.NativeObject(), p2.NativeObject())); } /** @@ -3223,7 +3180,7 @@ import java.lang.Exception; CheckContextMatch(p1); CheckContextMatch(p2); - return new Probe(this, Native.probeOr(nCtx, p1.NativeObject, p2.NativeObject)); + return new Probe(this, Native.probeOr(nCtx(), p1.NativeObject(), p2.NativeObject())); } /** @@ -3236,7 +3193,7 @@ import java.lang.Exception; CheckContextMatch(p); - return new Probe(this, Native.probeNot(nCtx, p.NativeObject)); + return new Probe(this, Native.probeNot(nCtx(), p.NativeObject())); } /** @@ -3252,9 +3209,9 @@ import java.lang.Exception; if (logic == null) - return new Solver(this, Native.mkSolver(nCtx)); + return new Solver(this, Native.mkSolver(nCtx())); else - return new Solver(this, Native.mkSolverForLogic(nCtx, logic.NativeObject)); + return new Solver(this, Native.mkSolverForLogic(nCtx(), logic.NativeObject())); } /** @@ -3275,7 +3232,7 @@ import java.lang.Exception; { - return new Solver(this, Native.mkSimpleSolver(nCtx)); + return new Solver(this, Native.mkSimpleSolver(nCtx())); } /** @@ -3290,7 +3247,7 @@ import java.lang.Exception; - return new Solver(this, Native.mkSolverFromTactic(nCtx, t.NativeObject)); + return new Solver(this, Native.mkSolverFromTactic(nCtx(), t.NativeObject())); } /** @@ -3343,13 +3300,13 @@ import java.lang.Exception; { - return Native.simplifyGetHelp(nCtx); + return Native.simplifyGetHelp(nCtx()); } /** * Retrieves parameter descriptions for simplifier. **/ - public ParamDescrs SimplifyParameterDescriptions() { return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx)); } + public ParamDescrs SimplifyParameterDescriptions() { return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx())); } /** * Enable/disable printing of warning messages to the console. @@ -3358,7 +3315,7 @@ import java.lang.Exception; **/ public static void ToggleWarningMessages(boolean enabled) { - Native.toggleWarningMessages((enabled) ? 1 : 0); + Native.toggleWarningMessages((enabled) ? true : false); } ///// @@ -3387,7 +3344,7 @@ import java.lang.Exception; **/ public void UpdateParamValue(String id, String value) { - Native.updateParamValue(nCtx, id, value); + Native.updateParamValue(nCtx(), id, value); } /** @@ -3400,8 +3357,8 @@ import java.lang.Exception; public String GetParamValue(String id) { long res = 0; - int r = Native.getParamValue(nCtx, id, res); - if (r == (int)Z3_lbool.Z3_L_FALSE) + int r = Native.getParamValue(nCtx(), id, res); + if (r == Z3_lbool.Z3_L_FALSE.toInt()) return null; else return Marshal.PtrToStringAnsi(res); @@ -3439,7 +3396,7 @@ import java.lang.Exception; if (arr != null) { - for (Iterator a = arr.iterator(); a.hasNext(); ) + for (Z3Object a: arr) { // It was an assume, now we added the precondition, and we made it into an assert CheckContextMatch(a); @@ -3499,7 +3456,7 @@ import java.lang.Exception; Fixedpoint.DecRefQueue Fixedpoint_DRQ () { return m_Fixedpoint_DRQ; } - long refCount = 0; + int refCount = 0; /** * Finalizer. diff --git a/src/api/java/com/Microsoft/Z3/DatatypeExpr.java b/src/api/java/com/Microsoft/Z3/DatatypeExpr.java index 4b18635cc..32835baf5 100644 --- a/src/api/java/com/Microsoft/Z3/DatatypeExpr.java +++ b/src/api/java/com/Microsoft/Z3/DatatypeExpr.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Collections.Generic; */ /* using System.Linq; */ diff --git a/src/api/java/com/Microsoft/Z3/DatatypeSort.java b/src/api/java/com/Microsoft/Z3/DatatypeSort.java index c108c3de9..4d2dd8992 100644 --- a/src/api/java/com/Microsoft/Z3/DatatypeSort.java +++ b/src/api/java/com/Microsoft/Z3/DatatypeSort.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -18,7 +19,7 @@ import java.lang.Exception; /** * 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. @@ -27,10 +28,10 @@ import java.lang.Exception; { - long n = NumConstructors; + int n = NumConstructors(); FuncDecl[] res = new FuncDecl[n]; - for (long i; i < n; i++) - res[i] = new FuncDecl(Context, Native.getDatatypeSortConstructor(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = new FuncDecl(Context(), Native.getDatatypeSortConstructor(Context().nCtx(), NativeObject(), i)); return res; } @@ -41,10 +42,10 @@ import java.lang.Exception; { - long n = NumConstructors; + int n = NumConstructors(); FuncDecl[] res = new FuncDecl[n]; - for (long i; i < n; i++) - res[i] = new FuncDecl(Context, Native.getDatatypeSortRecognizer(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = new FuncDecl(Context(), Native.getDatatypeSortRecognizer(Context().nCtx(), NativeObject(), i)); return res; } @@ -55,15 +56,15 @@ import java.lang.Exception; { - long n = NumConstructors; + int n = NumConstructors(); 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)); - long ds = fd.DomainSize; + FuncDecl fd = new FuncDecl(Context(), Native.getDatatypeSortConstructor(Context().nCtx(), NativeObject(), i)); + int ds = fd.DomainSize; FuncDecl[] tmp = new FuncDecl[ds]; - for (long j; j < ds; j++) - tmp[j] = new FuncDecl(Context, Native.getDatatypeSortConstructorAccessor(Context().nCtx(), NativeObject(), i, j)); + for (int j = 0; j < ds; j++) + tmp[j] = new FuncDecl(Context(), Native.getDatatypeSortConstructorAccessor(Context().nCtx(), NativeObject(), i, j)); res[i] = tmp; } return res; @@ -72,7 +73,7 @@ import java.lang.Exception; DatatypeSort(Context ctx, long obj) { super(ctx, obj); { }} 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))); diff --git a/src/api/java/com/Microsoft/Z3/EnumSort.java b/src/api/java/com/Microsoft/Z3/EnumSort.java index 77e0ac057..cfb9d099a 100644 --- a/src/api/java/com/Microsoft/Z3/EnumSort.java +++ b/src/api/java/com/Microsoft/Z3/EnumSort.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* 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_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); _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]); _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]); _consts = new Expr[n]; - for (long i; i < n; i++) + for (int i = 0; i < n; i++) _consts[i] = ctx.MkApp(_constdecls[i]); } }; diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.class b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.class new file mode 100644 index 000000000..b94349266 Binary files /dev/null and b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.class differ diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java index 2ba3f58ab..66841c073 100644 --- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java @@ -8,12 +8,26 @@ package com.Microsoft.Z3; * Z3_ast_kind **/ public enum Z3_ast_kind { -Z3_VAR_AST (2), -Z3_SORT_AST (4), -Z3_QUANTIFIER_AST (3), -Z3_UNKNOWN_AST (1000), -Z3_FUNC_DECL_AST (5), -Z3_NUMERAL_AST (0), -Z3_APP_AST (1), + Z3_VAR_AST (2), + Z3_SORT_AST (4), + Z3_QUANTIFIER_AST (3), + Z3_UNKNOWN_AST (1000), + Z3_FUNC_DECL_AST (5), + Z3_NUMERAL_AST (0), + 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; } } diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.class b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.class new file mode 100644 index 000000000..b14685118 Binary files /dev/null and b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.class differ diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java index 4aa4a2716..bfbbadd96 100644 --- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java @@ -8,9 +8,23 @@ package com.Microsoft.Z3; * Z3_ast_print_mode **/ public enum Z3_ast_print_mode { -Z3_PRINT_SMTLIB2_COMPLIANT (3), -Z3_PRINT_SMTLIB_COMPLIANT (2), -Z3_PRINT_SMTLIB_FULL (0), -Z3_PRINT_LOW_LEVEL (1), + Z3_PRINT_SMTLIB2_COMPLIANT (3), + Z3_PRINT_SMTLIB_COMPLIANT (2), + Z3_PRINT_SMTLIB_FULL (0), + 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; } } diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.class b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.class new file mode 100644 index 000000000..6ba48582b Binary files /dev/null and b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.class differ diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java index 3b0b01715..c9ae9aa35 100644 --- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java @@ -8,157 +8,171 @@ package com.Microsoft.Z3; * Z3_decl_kind **/ public enum Z3_decl_kind { -Z3_OP_LABEL (1792), -Z3_OP_PR_REWRITE (1294), -Z3_OP_UNINTERPRETED (2051), -Z3_OP_SUB (519), -Z3_OP_ZERO_EXT (1058), -Z3_OP_ADD (518), -Z3_OP_IS_INT (528), -Z3_OP_BREDOR (1061), -Z3_OP_BNOT (1051), -Z3_OP_BNOR (1054), -Z3_OP_PR_CNF_STAR (1315), -Z3_OP_RA_JOIN (1539), -Z3_OP_LE (514), -Z3_OP_SET_UNION (773), -Z3_OP_PR_UNDEF (1280), -Z3_OP_BREDAND (1062), -Z3_OP_LT (516), -Z3_OP_RA_UNION (1540), -Z3_OP_BADD (1028), -Z3_OP_BUREM0 (1039), -Z3_OP_OEQ (267), -Z3_OP_PR_MODUS_PONENS (1284), -Z3_OP_RA_CLONE (1548), -Z3_OP_REPEAT (1060), -Z3_OP_RA_NEGATION_FILTER (1544), -Z3_OP_BSMOD0 (1040), -Z3_OP_BLSHR (1065), -Z3_OP_BASHR (1066), -Z3_OP_PR_UNIT_RESOLUTION (1304), -Z3_OP_ROTATE_RIGHT (1068), -Z3_OP_ARRAY_DEFAULT (772), -Z3_OP_PR_PULL_QUANT (1296), -Z3_OP_PR_APPLY_DEF (1310), -Z3_OP_PR_REWRITE_STAR (1295), -Z3_OP_IDIV (523), -Z3_OP_PR_GOAL (1283), -Z3_OP_PR_IFF_TRUE (1305), -Z3_OP_LABEL_LIT (1793), -Z3_OP_BOR (1050), -Z3_OP_PR_SYMMETRY (1286), -Z3_OP_TRUE (256), -Z3_OP_SET_COMPLEMENT (776), -Z3_OP_CONCAT (1056), -Z3_OP_PR_NOT_OR_ELIM (1293), -Z3_OP_IFF (263), -Z3_OP_BSHL (1064), -Z3_OP_PR_TRANSITIVITY (1287), -Z3_OP_SGT (1048), -Z3_OP_RA_WIDEN (1541), -Z3_OP_PR_DEF_INTRO (1309), -Z3_OP_NOT (265), -Z3_OP_PR_QUANT_INTRO (1290), -Z3_OP_UGT (1047), -Z3_OP_DT_RECOGNISER (2049), -Z3_OP_SET_INTERSECT (774), -Z3_OP_BSREM (1033), -Z3_OP_RA_STORE (1536), -Z3_OP_SLT (1046), -Z3_OP_ROTATE_LEFT (1067), -Z3_OP_PR_NNF_NEG (1313), -Z3_OP_PR_REFLEXIVITY (1285), -Z3_OP_ULEQ (1041), -Z3_OP_BIT1 (1025), -Z3_OP_BIT0 (1026), -Z3_OP_EQ (258), -Z3_OP_BMUL (1030), -Z3_OP_ARRAY_MAP (771), -Z3_OP_STORE (768), -Z3_OP_PR_HYPOTHESIS (1302), -Z3_OP_RA_RENAME (1545), -Z3_OP_AND (261), -Z3_OP_TO_REAL (526), -Z3_OP_PR_NNF_POS (1312), -Z3_OP_PR_AND_ELIM (1292), -Z3_OP_MOD (525), -Z3_OP_BUDIV0 (1037), -Z3_OP_PR_TRUE (1281), -Z3_OP_BNAND (1053), -Z3_OP_PR_ELIM_UNUSED_VARS (1299), -Z3_OP_RA_FILTER (1543), -Z3_OP_FD_LT (1549), -Z3_OP_RA_EMPTY (1537), -Z3_OP_DIV (522), -Z3_OP_ANUM (512), -Z3_OP_MUL (521), -Z3_OP_UGEQ (1043), -Z3_OP_BSREM0 (1038), -Z3_OP_PR_TH_LEMMA (1318), -Z3_OP_BXOR (1052), -Z3_OP_DISTINCT (259), -Z3_OP_PR_IFF_FALSE (1306), -Z3_OP_BV2INT (1072), -Z3_OP_EXT_ROTATE_LEFT (1069), -Z3_OP_PR_PULL_QUANT_STAR (1297), -Z3_OP_BSUB (1029), -Z3_OP_PR_ASSERTED (1282), -Z3_OP_BXNOR (1055), -Z3_OP_EXTRACT (1059), -Z3_OP_PR_DER (1300), -Z3_OP_DT_CONSTRUCTOR (2048), -Z3_OP_GT (517), -Z3_OP_BUREM (1034), -Z3_OP_IMPLIES (266), -Z3_OP_SLEQ (1042), -Z3_OP_GE (515), -Z3_OP_BAND (1049), -Z3_OP_ITE (260), -Z3_OP_AS_ARRAY (778), -Z3_OP_RA_SELECT (1547), -Z3_OP_CONST_ARRAY (770), -Z3_OP_BSDIV (1031), -Z3_OP_OR (262), -Z3_OP_PR_HYPER_RESOLVE (1319), -Z3_OP_AGNUM (513), -Z3_OP_PR_PUSH_QUANT (1298), -Z3_OP_BSMOD (1035), -Z3_OP_PR_IFF_OEQ (1311), -Z3_OP_PR_LEMMA (1303), -Z3_OP_SET_SUBSET (777), -Z3_OP_SELECT (769), -Z3_OP_RA_PROJECT (1542), -Z3_OP_BNEG (1027), -Z3_OP_UMINUS (520), -Z3_OP_REM (524), -Z3_OP_TO_INT (527), -Z3_OP_PR_QUANT_INST (1301), -Z3_OP_SGEQ (1044), -Z3_OP_POWER (529), -Z3_OP_XOR3 (1074), -Z3_OP_RA_IS_EMPTY (1538), -Z3_OP_CARRY (1073), -Z3_OP_DT_ACCESSOR (2050), -Z3_OP_PR_TRANSITIVITY_STAR (1288), -Z3_OP_PR_NNF_STAR (1314), -Z3_OP_PR_COMMUTATIVITY (1307), -Z3_OP_ULT (1045), -Z3_OP_BSDIV0 (1036), -Z3_OP_SET_DIFFERENCE (775), -Z3_OP_INT2BV (1071), -Z3_OP_XOR (264), -Z3_OP_PR_MODUS_PONENS_OEQ (1317), -Z3_OP_BNUM (1024), -Z3_OP_BUDIV (1032), -Z3_OP_PR_MONOTONICITY (1289), -Z3_OP_PR_DEF_AXIOM (1308), -Z3_OP_FALSE (257), -Z3_OP_EXT_ROTATE_RIGHT (1070), -Z3_OP_PR_DISTRIBUTIVITY (1291), -Z3_OP_SIGN_EXT (1057), -Z3_OP_PR_SKOLEMIZE (1316), -Z3_OP_BCOMP (1063), -Z3_OP_RA_COMPLEMENT (1546), + Z3_OP_LABEL (1792), + Z3_OP_PR_REWRITE (1294), + Z3_OP_UNINTERPRETED (2051), + Z3_OP_SUB (519), + Z3_OP_ZERO_EXT (1058), + Z3_OP_ADD (518), + Z3_OP_IS_INT (528), + Z3_OP_BREDOR (1061), + Z3_OP_BNOT (1051), + Z3_OP_BNOR (1054), + Z3_OP_PR_CNF_STAR (1315), + Z3_OP_RA_JOIN (1539), + Z3_OP_LE (514), + Z3_OP_SET_UNION (773), + Z3_OP_PR_UNDEF (1280), + Z3_OP_BREDAND (1062), + Z3_OP_LT (516), + Z3_OP_RA_UNION (1540), + Z3_OP_BADD (1028), + Z3_OP_BUREM0 (1039), + Z3_OP_OEQ (267), + Z3_OP_PR_MODUS_PONENS (1284), + Z3_OP_RA_CLONE (1548), + Z3_OP_REPEAT (1060), + Z3_OP_RA_NEGATION_FILTER (1544), + Z3_OP_BSMOD0 (1040), + Z3_OP_BLSHR (1065), + Z3_OP_BASHR (1066), + Z3_OP_PR_UNIT_RESOLUTION (1304), + Z3_OP_ROTATE_RIGHT (1068), + Z3_OP_ARRAY_DEFAULT (772), + Z3_OP_PR_PULL_QUANT (1296), + Z3_OP_PR_APPLY_DEF (1310), + Z3_OP_PR_REWRITE_STAR (1295), + Z3_OP_IDIV (523), + Z3_OP_PR_GOAL (1283), + Z3_OP_PR_IFF_TRUE (1305), + Z3_OP_LABEL_LIT (1793), + Z3_OP_BOR (1050), + Z3_OP_PR_SYMMETRY (1286), + Z3_OP_TRUE (256), + Z3_OP_SET_COMPLEMENT (776), + Z3_OP_CONCAT (1056), + Z3_OP_PR_NOT_OR_ELIM (1293), + Z3_OP_IFF (263), + Z3_OP_BSHL (1064), + Z3_OP_PR_TRANSITIVITY (1287), + Z3_OP_SGT (1048), + Z3_OP_RA_WIDEN (1541), + Z3_OP_PR_DEF_INTRO (1309), + Z3_OP_NOT (265), + Z3_OP_PR_QUANT_INTRO (1290), + Z3_OP_UGT (1047), + Z3_OP_DT_RECOGNISER (2049), + Z3_OP_SET_INTERSECT (774), + Z3_OP_BSREM (1033), + Z3_OP_RA_STORE (1536), + Z3_OP_SLT (1046), + Z3_OP_ROTATE_LEFT (1067), + Z3_OP_PR_NNF_NEG (1313), + Z3_OP_PR_REFLEXIVITY (1285), + Z3_OP_ULEQ (1041), + Z3_OP_BIT1 (1025), + Z3_OP_BIT0 (1026), + Z3_OP_EQ (258), + Z3_OP_BMUL (1030), + Z3_OP_ARRAY_MAP (771), + Z3_OP_STORE (768), + Z3_OP_PR_HYPOTHESIS (1302), + Z3_OP_RA_RENAME (1545), + Z3_OP_AND (261), + Z3_OP_TO_REAL (526), + Z3_OP_PR_NNF_POS (1312), + Z3_OP_PR_AND_ELIM (1292), + Z3_OP_MOD (525), + Z3_OP_BUDIV0 (1037), + Z3_OP_PR_TRUE (1281), + Z3_OP_BNAND (1053), + Z3_OP_PR_ELIM_UNUSED_VARS (1299), + Z3_OP_RA_FILTER (1543), + Z3_OP_FD_LT (1549), + Z3_OP_RA_EMPTY (1537), + Z3_OP_DIV (522), + Z3_OP_ANUM (512), + Z3_OP_MUL (521), + Z3_OP_UGEQ (1043), + Z3_OP_BSREM0 (1038), + Z3_OP_PR_TH_LEMMA (1318), + Z3_OP_BXOR (1052), + Z3_OP_DISTINCT (259), + Z3_OP_PR_IFF_FALSE (1306), + Z3_OP_BV2INT (1072), + Z3_OP_EXT_ROTATE_LEFT (1069), + Z3_OP_PR_PULL_QUANT_STAR (1297), + Z3_OP_BSUB (1029), + Z3_OP_PR_ASSERTED (1282), + Z3_OP_BXNOR (1055), + Z3_OP_EXTRACT (1059), + Z3_OP_PR_DER (1300), + Z3_OP_DT_CONSTRUCTOR (2048), + Z3_OP_GT (517), + Z3_OP_BUREM (1034), + Z3_OP_IMPLIES (266), + Z3_OP_SLEQ (1042), + Z3_OP_GE (515), + Z3_OP_BAND (1049), + Z3_OP_ITE (260), + Z3_OP_AS_ARRAY (778), + Z3_OP_RA_SELECT (1547), + Z3_OP_CONST_ARRAY (770), + Z3_OP_BSDIV (1031), + Z3_OP_OR (262), + Z3_OP_PR_HYPER_RESOLVE (1319), + Z3_OP_AGNUM (513), + Z3_OP_PR_PUSH_QUANT (1298), + Z3_OP_BSMOD (1035), + Z3_OP_PR_IFF_OEQ (1311), + Z3_OP_PR_LEMMA (1303), + Z3_OP_SET_SUBSET (777), + Z3_OP_SELECT (769), + Z3_OP_RA_PROJECT (1542), + Z3_OP_BNEG (1027), + Z3_OP_UMINUS (520), + Z3_OP_REM (524), + Z3_OP_TO_INT (527), + Z3_OP_PR_QUANT_INST (1301), + Z3_OP_SGEQ (1044), + Z3_OP_POWER (529), + Z3_OP_XOR3 (1074), + Z3_OP_RA_IS_EMPTY (1538), + Z3_OP_CARRY (1073), + Z3_OP_DT_ACCESSOR (2050), + Z3_OP_PR_TRANSITIVITY_STAR (1288), + Z3_OP_PR_NNF_STAR (1314), + Z3_OP_PR_COMMUTATIVITY (1307), + Z3_OP_ULT (1045), + Z3_OP_BSDIV0 (1036), + Z3_OP_SET_DIFFERENCE (775), + Z3_OP_INT2BV (1071), + Z3_OP_XOR (264), + Z3_OP_PR_MODUS_PONENS_OEQ (1317), + Z3_OP_BNUM (1024), + Z3_OP_BUDIV (1032), + Z3_OP_PR_MONOTONICITY (1289), + Z3_OP_PR_DEF_AXIOM (1308), + Z3_OP_FALSE (257), + Z3_OP_EXT_ROTATE_RIGHT (1070), + Z3_OP_PR_DISTRIBUTIVITY (1291), + Z3_OP_SIGN_EXT (1057), + Z3_OP_PR_SKOLEMIZE (1316), + Z3_OP_BCOMP (1063), + 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; } } diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.class b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.class new file mode 100644 index 000000000..f9d486c4e Binary files /dev/null and b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.class differ diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java index ef5fa6f2c..0c1c22870 100644 --- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java @@ -8,18 +8,32 @@ package com.Microsoft.Z3; * Z3_error_code **/ public enum Z3_error_code { -Z3_INVALID_PATTERN (6), -Z3_MEMOUT_FAIL (7), -Z3_NO_PARSER (5), -Z3_OK (0), -Z3_INVALID_ARG (3), -Z3_EXCEPTION (12), -Z3_IOB (2), -Z3_INTERNAL_FATAL (9), -Z3_INVALID_USAGE (10), -Z3_FILE_ACCESS_ERROR (8), -Z3_SORT_ERROR (1), -Z3_PARSER_ERROR (4), -Z3_DEC_REF_ERROR (11), + Z3_INVALID_PATTERN (6), + Z3_MEMOUT_FAIL (7), + Z3_NO_PARSER (5), + Z3_OK (0), + Z3_INVALID_ARG (3), + Z3_EXCEPTION (12), + Z3_IOB (2), + Z3_INTERNAL_FATAL (9), + Z3_INVALID_USAGE (10), + Z3_FILE_ACCESS_ERROR (8), + Z3_SORT_ERROR (1), + Z3_PARSER_ERROR (4), + 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; } } diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.class b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.class new file mode 100644 index 000000000..0d278b16f Binary files /dev/null and b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.class differ diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java index 38e2fdf96..2d96c6e76 100644 --- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java @@ -8,9 +8,23 @@ package com.Microsoft.Z3; * Z3_goal_prec **/ public enum Z3_goal_prec { -Z3_GOAL_UNDER (1), -Z3_GOAL_PRECISE (0), -Z3_GOAL_UNDER_OVER (3), -Z3_GOAL_OVER (2), + Z3_GOAL_UNDER (1), + Z3_GOAL_PRECISE (0), + Z3_GOAL_UNDER_OVER (3), + 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; } } diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.class b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.class new file mode 100644 index 000000000..eeee15f26 Binary files /dev/null and b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.class differ diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java index 63ee2e227..d31f5c238 100644 --- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java @@ -8,8 +8,22 @@ package com.Microsoft.Z3; * Z3_lbool **/ public enum Z3_lbool { -Z3_L_TRUE (1), -Z3_L_UNDEF (0), -Z3_L_FALSE (-1), + Z3_L_TRUE (1), + Z3_L_UNDEF (0), + 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; } } diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.class b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.class new file mode 100644 index 000000000..84887bc3c Binary files /dev/null and b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.class differ diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java index e3d8c0e77..81b8ef7bd 100644 --- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java @@ -8,12 +8,26 @@ package com.Microsoft.Z3; * Z3_param_kind **/ public enum Z3_param_kind { -Z3_PK_BOOL (1), -Z3_PK_SYMBOL (3), -Z3_PK_OTHER (5), -Z3_PK_INVALID (6), -Z3_PK_UINT (0), -Z3_PK_STRING (4), -Z3_PK_DOUBLE (2), + Z3_PK_BOOL (1), + Z3_PK_SYMBOL (3), + Z3_PK_OTHER (5), + Z3_PK_INVALID (6), + Z3_PK_UINT (0), + Z3_PK_STRING (4), + 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; } } diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.class b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.class new file mode 100644 index 000000000..2a137da1e Binary files /dev/null and b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.class differ diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java index 0de56c3cd..c009104ba 100644 --- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java @@ -8,12 +8,26 @@ package com.Microsoft.Z3; * Z3_parameter_kind **/ public enum Z3_parameter_kind { -Z3_PARAMETER_FUNC_DECL (6), -Z3_PARAMETER_DOUBLE (1), -Z3_PARAMETER_SYMBOL (3), -Z3_PARAMETER_INT (0), -Z3_PARAMETER_AST (5), -Z3_PARAMETER_SORT (4), -Z3_PARAMETER_RATIONAL (2), + Z3_PARAMETER_FUNC_DECL (6), + Z3_PARAMETER_DOUBLE (1), + Z3_PARAMETER_SYMBOL (3), + Z3_PARAMETER_INT (0), + Z3_PARAMETER_AST (5), + Z3_PARAMETER_SORT (4), + 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; } } diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.class b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.class new file mode 100644 index 000000000..3a4c6b219 Binary files /dev/null and b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.class differ diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java index 59a69b4c0..43f5b2f14 100644 --- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java @@ -8,15 +8,29 @@ package com.Microsoft.Z3; * Z3_sort_kind **/ public enum Z3_sort_kind { -Z3_BV_SORT (4), -Z3_FINITE_DOMAIN_SORT (8), -Z3_ARRAY_SORT (5), -Z3_UNKNOWN_SORT (1000), -Z3_RELATION_SORT (7), -Z3_REAL_SORT (3), -Z3_INT_SORT (2), -Z3_UNINTERPRETED_SORT (0), -Z3_BOOL_SORT (1), -Z3_DATATYPE_SORT (6), + Z3_BV_SORT (4), + Z3_FINITE_DOMAIN_SORT (8), + Z3_ARRAY_SORT (5), + Z3_UNKNOWN_SORT (1000), + Z3_RELATION_SORT (7), + Z3_REAL_SORT (3), + Z3_INT_SORT (2), + Z3_UNINTERPRETED_SORT (0), + Z3_BOOL_SORT (1), + 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; } } diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.class b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.class new file mode 100644 index 000000000..6623e4b8d Binary files /dev/null and b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.class differ diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java index efe5804eb..2f08236de 100644 --- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java +++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java @@ -8,7 +8,21 @@ package com.Microsoft.Z3; * Z3_symbol_kind **/ public enum Z3_symbol_kind { -Z3_INT_SYMBOL (0), -Z3_STRING_SYMBOL (1), + Z3_INT_SYMBOL (0), + 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; } } diff --git a/src/api/java/com/Microsoft/Z3/Expr.java b/src/api/java/com/Microsoft/Z3/Expr.java index 13aa0bc1c..0851acf70 100644 --- a/src/api/java/com/Microsoft/Z3/Expr.java +++ b/src/api/java/com/Microsoft/Z3/Expr.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -25,9 +26,9 @@ import java.lang.Exception; if (p == null) - return Expr.Create(Context, Native.simplify(Context().nCtx(), NativeObject())); + return Expr.Create(Context(), Native.simplify(Context().nCtx(), NativeObject())); else - return Expr.Create(Context, Native.simplifyEx(Context().nCtx(), NativeObject(), p.NativeObject)); + return Expr.Create(Context(), Native.simplifyEx(Context().nCtx(), NativeObject(), p.NativeObject())); } /** @@ -36,19 +37,19 @@ import java.lang.Exception; public FuncDecl FuncDecl() { - return new FuncDecl(Context, Native.getAppDecl(Context().nCtx(), NativeObject())); + return new FuncDecl(Context(), Native.getAppDecl(Context().nCtx(), NativeObject())); } /** * Indicates whether the expression is the true or false expression * or something else (Z3_L_UNDEF). **/ - public Z3_lbool BoolValue() { return (Z3_lbool)Native.getBoolValue(Context().nCtx(), NativeObject()); } + public Z3_lbool BoolValue() { return Z3_lbool.fromInt(Native.getBoolValue(Context().nCtx(), NativeObject())); } /** * The number of arguments of the expression. **/ - public long NumArgs() { return Native.getAppNumArgs(Context().nCtx(), NativeObject()); } + public int NumArgs() { return Native.getAppNumArgs(Context().nCtx(), NativeObject()); } /** * The arguments of the expression. @@ -57,10 +58,10 @@ import java.lang.Exception; { - long n = NumArgs; + int n = NumArgs(); Expr[] res = new Expr[n]; - for (long i; i < n; i++) - res[i] = Expr.Create(Context, Native.getAppArg(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = Expr.Create(Context(), Native.getAppArg(Context().nCtx(), NativeObject(), i)); return res; } @@ -73,10 +74,10 @@ import java.lang.Exception; - Context.CheckContextMatch(args); - if (args.Length != NumArgs) + Context().CheckContextMatch(args); + if (args.length != NumArgs()) throw new Z3Exception("Number of arguments does not match"); - setNativeObject(Native.updateTerm(Context().nCtx(), NativeObject(), (long)args.Length, Expr.ArrayToNative(args))); + setNativeObject(Native.updateTerm(Context().nCtx(), NativeObject(), (int)args.length, Expr.ArrayToNative(args))); } /** @@ -95,11 +96,11 @@ import java.lang.Exception; - Context.CheckContextMatch(from); - Context.CheckContextMatch(to); - if (from.Length != to.Length) + Context().CheckContextMatch(from); + Context().CheckContextMatch(to); + if (from.length != to.length) throw new Z3Exception("Argument sizes do not match"); - return Expr.Create(Context, Native.substitute(Context().nCtx(), NativeObject(), (long)from.Length, Expr.ArrayToNative(from), Expr.ArrayToNative(to))); + return Expr.Create(Context(), Native.substitute(Context().nCtx(), NativeObject(), (int)from.length, Expr.ArrayToNative(from), Expr.ArrayToNative(to))); } /** @@ -127,8 +128,8 @@ import java.lang.Exception; - Context.CheckContextMatch(to); - return Expr.Create(Context, Native.substituteVars(Context().nCtx(), NativeObject(), (long)to.Length, Expr.ArrayToNative(to))); + Context().CheckContextMatch(to); + return Expr.Create(Context(), Native.substituteVars(Context().nCtx(), NativeObject(), (int)to.length, Expr.ArrayToNative(to))); } /** @@ -141,7 +142,7 @@ import java.lang.Exception; - if (ReferenceEquals(Context, ctx)) + if (Context() == ctx) return this; else return Expr.Create(ctx, Native.translate(Context().nCtx(), NativeObject(), ctx.nCtx())); @@ -152,19 +153,19 @@ import java.lang.Exception; **/ public String toString() { - return super.ToString(); + return super.toString(); } /** * Indicates whether the term is a numeral **/ - public boolean IsNumeral() { return Native.isNumeralAst(Context().nCtx(), NativeObject()) != 0; } + public boolean IsNumeral() { return Native.isNumeralAst(Context().nCtx(), NativeObject()) ; } /** * Indicates whether the term is well-sorted. * @return True if the term is well-sorted, false otherwise. **/ - public boolean IsWellSorted() { return Native.isWellSorted(Context().nCtx(), NativeObject()) != 0; } + public boolean IsWellSorted() { return Native.isWellSorted(Context().nCtx(), NativeObject()) ; } /** * The Sort of the term. @@ -172,28 +173,28 @@ import java.lang.Exception; public Sort Sort() { - return Sort.Create(Context, Native.getSort(Context().nCtx(), NativeObject())); + return Sort.Create(Context(), Native.getSort(Context().nCtx(), NativeObject())); } /** * Indicates whether the term represents a constant. **/ - public boolean IsConst() { return IsExpr && NumArgs == 0 && FuncDecl.DomainSize == 0; } + public boolean IsConst() { return IsExpr() && NumArgs() == 0 && FuncDecl().DomainSize() == 0; } /** * Indicates whether the term is an integer numeral. **/ - public boolean IsIntNum() { return IsNumeral && IsInt; } + public boolean IsIntNum() { return IsNumeral() && IsInt(); } /** * Indicates whether the term is a real numeral. **/ - public boolean IsRatNum() { return IsNumeral && IsReal; } + public boolean IsRatNum() { return IsNumeral() && IsReal(); } /** * Indicates whether the term is an algebraic number **/ - public boolean IsAlgebraicNumber() { return Native.isAlgebraicNumber(Context().nCtx(), NativeObject()) != 0; } + public boolean IsAlgebraicNumber() { return Native.isAlgebraicNumber(Context().nCtx(), NativeObject()) ; } /** @@ -201,168 +202,169 @@ import java.lang.Exception; **/ public boolean IsBool() { - return (IsExpr && + return (IsExpr() && Native.isEqSort(Context().nCtx(), Native.mkBoolSort(Context().nCtx()), - Native.getSort(Context().nCtx(), NativeObject())) != 0); + Native.getSort(Context().nCtx(), NativeObject())) ); } /** * Indicates whether the term is the constant true. **/ - public boolean IsTrue() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TRUE; } + public boolean IsTrue() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_TRUE; } /** * Indicates whether the term is the constant false. **/ - public boolean IsFalse() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FALSE; } + public boolean IsFalse() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_FALSE; } /** * Indicates whether the term is an equality predicate. **/ - public boolean IsEq() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EQ; } + public boolean IsEq() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_EQ; } /** * Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct). **/ - public boolean IsDistinct() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DISTINCT; } + public boolean IsDistinct() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_DISTINCT; } /** * Indicates whether the term is a ternary if-then-else term **/ - public boolean IsITE() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ITE; } + public boolean IsITE() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_ITE; } /** * Indicates whether the term is an n-ary conjunction **/ - public boolean IsAnd() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AND; } + public boolean IsAnd() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_AND; } /** * Indicates whether the term is an n-ary disjunction **/ - public boolean IsOr() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OR; } + public boolean IsOr() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_OR; } /** * Indicates whether the term is an if-and-only-if (Boolean equivalence, binary) **/ - public boolean IsIff() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IFF; } + public boolean IsIff() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_IFF; } /** * Indicates whether the term is an exclusive or **/ - public boolean IsXor() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR; } + public boolean IsXor() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_XOR; } /** * Indicates whether the term is a negation **/ - public boolean IsNot() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_NOT; } + public boolean IsNot() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_NOT; } /** * Indicates whether the term is an implication **/ - public boolean IsImplies() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } + public boolean IsImplies() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_IMPLIES; } /** * Indicates whether the term is of integer sort. **/ public boolean IsInt() { - return (Native.isNumeralAst(Context().nCtx(), NativeObject()) != 0 && - Native.getSortKind(Context().nCtx(), Native.getSort(Context().nCtx(), NativeObject())) == (long)Z3_sort_kind.Z3_INT_SORT); + return (Native.isNumeralAst(Context().nCtx(), NativeObject()) && + Native.getSortKind(Context().nCtx(), Native.getSort(Context().nCtx(), NativeObject())) == Z3_sort_kind.Z3_INT_SORT.toInt()); } /** * Indicates whether the term is of sort real. **/ - public boolean IsReal() { return Native.getSortKind(Context().nCtx(), Native.getSort(Context().nCtx(), NativeObject())) == (long)Z3_sort_kind.Z3_REAL_SORT; } + public boolean IsReal() { return Native.getSortKind(Context().nCtx(), Native.getSort(Context().nCtx(), NativeObject())) == Z3_sort_kind.Z3_REAL_SORT.toInt(); } /** * Indicates whether the term is an arithmetic numeral. **/ - public boolean IsArithmeticNumeral() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ANUM; } + public boolean IsArithmeticNumeral() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_ANUM; } /** * Indicates whether the term is a less-than-or-equal **/ - public boolean IsLE() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LE; } + public boolean IsLE() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_LE; } /** * Indicates whether the term is a greater-than-or-equal **/ - public boolean IsGE() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GE; } + public boolean IsGE() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_GE; } /** * Indicates whether the term is a less-than **/ - public boolean IsLT() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LT; } + public boolean IsLT() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_LT; } /** * Indicates whether the term is a greater-than **/ - public boolean IsGT() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GT; } + public boolean IsGT() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_GT; } /** * Indicates whether the term is addition (binary) **/ - public boolean IsAdd() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ADD; } + public boolean IsAdd() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_ADD; } /** * Indicates whether the term is subtraction (binary) **/ - public boolean IsSub() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SUB; } + public boolean IsSub() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_SUB; } /** * Indicates whether the term is a unary minus **/ - public boolean IsUMinus() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UMINUS; } + public boolean IsUMinus() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_UMINUS; } /** * Indicates whether the term is multiplication (binary) **/ - public boolean IsMul() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MUL; } + public boolean IsMul() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_MUL; } /** * Indicates whether the term is division (binary) **/ - public boolean IsDiv() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DIV; } + public boolean IsDiv() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_DIV; } /** * Indicates whether the term is integer division (binary) **/ - public boolean IsIDiv() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IDIV; } + public boolean IsIDiv() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_IDIV; } /** * Indicates whether the term is remainder (binary) **/ - public boolean IsRemainder() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REM; } + public boolean IsRemainder() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_REM; } /** * Indicates whether the term is modulus (binary) **/ - public boolean IsModulus() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MOD; } + public boolean IsModulus() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_MOD; } /** * Indicates whether the term is a coercion of integer to real (unary) **/ - public boolean IsIntToReal() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_REAL; } + public boolean IsIntToReal() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_TO_REAL; } /** * Indicates whether the term is a coercion of real to integer (unary) **/ - public boolean IsRealToInt() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_INT; } + public boolean IsRealToInt() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_TO_INT; } /** * Indicates whether the term is a check that tests whether a real is integral (unary) **/ - public boolean IsRealIsInt() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IS_INT; } + public boolean IsRealIsInt() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_IS_INT; } /** * Indicates whether the term is of an array sort. **/ public boolean IsArray() { - return (Native.isApp(Context().nCtx(), NativeObject()) != 0 && - (Z3_sort_kind)Native.getSortKind(Context().nCtx(), Native.getSort(Context().nCtx(), NativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT); + return (Native.isApp(Context().nCtx(), NativeObject()) && + Z3_sort_kind.fromInt(Native.getSortKind(Context().nCtx(), Native.getSort(Context().nCtx(), NativeObject()))) + == Z3_sort_kind.Z3_ARRAY_SORT); } /** @@ -370,366 +372,366 @@ import java.lang.Exception; * It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). * Array store takes at least 3 arguments. **/ - public boolean IsStore() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_STORE; } + public boolean IsStore() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_STORE; } /** * Indicates whether the term is an array select. **/ - public boolean IsSelect() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SELECT; } + public boolean IsSelect() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_SELECT; } /** * Indicates whether the term is a constant array. * For example, select(const(v),i) = v holds for every v and i. The function is unary. **/ - public boolean IsConstantArray() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONST_ARRAY; } + public boolean IsConstantArray() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_CONST_ARRAY; } /** * Indicates whether the term is a default array. * For example default(const(v)) = v. The function is unary. **/ - public boolean IsDefaultArray() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; } + public boolean IsDefaultArray() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; } /** * Indicates whether the term is an array map. * It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i. **/ - public boolean IsArrayMap() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_MAP; } + public boolean IsArrayMap() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_ARRAY_MAP; } /** * Indicates whether the term is an as-array term. * An as-array term is n array value that behaves as the function graph of the * function passed as parameter. **/ - public boolean IsAsArray() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AS_ARRAY; } + public boolean IsAsArray() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_AS_ARRAY; } /** * Indicates whether the term is set union **/ - public boolean IsSetUnion() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_UNION; } + public boolean IsSetUnion() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_SET_UNION; } /** * Indicates whether the term is set intersection **/ - public boolean IsSetIntersect() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_INTERSECT; } + public boolean IsSetIntersect() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_SET_INTERSECT; } /** * Indicates whether the term is set difference **/ - public boolean IsSetDifference() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; } + public boolean IsSetDifference() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; } /** * Indicates whether the term is set complement **/ - public boolean IsSetComplement() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; } + public boolean IsSetComplement() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; } /** * Indicates whether the term is set subset **/ - public boolean IsSetSubset() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_SUBSET; } + public boolean IsSetSubset() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_SET_SUBSET; } /** * Indicates whether the terms is of bit-vector sort. **/ - public boolean IsBV() { return Native.getSortKind(Context().nCtx(), Native.getSort(Context().nCtx(), NativeObject())) == (long)Z3_sort_kind.Z3_BV_SORT; } + public boolean IsBV() { return Native.getSortKind(Context().nCtx(), Native.getSort(Context().nCtx(), NativeObject())) == Z3_sort_kind.Z3_BV_SORT.toInt(); } /** * Indicates whether the term is a bit-vector numeral **/ - public boolean IsBVNumeral() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNUM; } + public boolean IsBVNumeral() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BNUM; } /** * Indicates whether the term is a one-bit bit-vector with value one **/ - public boolean IsBVBitOne() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT1; } + public boolean IsBVBitOne() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BIT1; } /** * Indicates whether the term is a one-bit bit-vector with value zero **/ - public boolean IsBVBitZero() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT0; } + public boolean IsBVBitZero() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BIT0; } /** * Indicates whether the term is a bit-vector unary minus **/ - public boolean IsBVUMinus() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNEG; } + public boolean IsBVUMinus() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BNEG; } /** * Indicates whether the term is a bit-vector addition (binary) **/ - public boolean IsBVAdd() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BADD; } + public boolean IsBVAdd() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BADD; } /** * Indicates whether the term is a bit-vector subtraction (binary) **/ - public boolean IsBVSub() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSUB; } + public boolean IsBVSub() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BSUB; } /** * Indicates whether the term is a bit-vector multiplication (binary) **/ - public boolean IsBVMul() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BMUL; } + public boolean IsBVMul() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BMUL; } /** * Indicates whether the term is a bit-vector signed division (binary) **/ - public boolean IsBVSDiv() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV; } + public boolean IsBVSDiv() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BSDIV; } /** * Indicates whether the term is a bit-vector unsigned division (binary) **/ - public boolean IsBVUDiv() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV; } + public boolean IsBVUDiv() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BUDIV; } /** * Indicates whether the term is a bit-vector signed remainder (binary) **/ - public boolean IsBVSRem() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM; } + public boolean IsBVSRem() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BSREM; } /** * Indicates whether the term is a bit-vector unsigned remainder (binary) **/ - public boolean IsBVURem() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM; } + public boolean IsBVURem() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BUREM; } /** * Indicates whether the term is a bit-vector signed modulus **/ - public boolean IsBVSMod() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD; } + public boolean IsBVSMod() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BSMOD; } /** * Indicates whether the term is a bit-vector signed division by zero **/ - boolean IsBVSDiv0 () { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV0; } + boolean IsBVSDiv0 () { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BSDIV0; } /** * Indicates whether the term is a bit-vector unsigned division by zero **/ - boolean IsBVUDiv0 () { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV0; } + boolean IsBVUDiv0 () { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BUDIV0; } /** * Indicates whether the term is a bit-vector signed remainder by zero **/ - boolean IsBVSRem0 () { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM0; } + boolean IsBVSRem0 () { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BSREM0; } /** * Indicates whether the term is a bit-vector unsigned remainder by zero **/ - boolean IsBVURem0 () { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM0; } + boolean IsBVURem0 () { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BUREM0; } /** * Indicates whether the term is a bit-vector signed modulus by zero **/ - boolean IsBVSMod0 () { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD0; } + boolean IsBVSMod0 () { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BSMOD0; } /** * Indicates whether the term is an unsigned bit-vector less-than-or-equal **/ - public boolean IsBVULE() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULEQ; } + public boolean IsBVULE() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_ULEQ; } /** * Indicates whether the term is a signed bit-vector less-than-or-equal **/ - public boolean IsBVSLE() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLEQ; } + public boolean IsBVSLE() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_SLEQ; } /** * Indicates whether the term is an unsigned bit-vector greater-than-or-equal **/ - public boolean IsBVUGE() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGEQ; } + public boolean IsBVUGE() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_UGEQ; } /** * Indicates whether the term is a signed bit-vector greater-than-or-equal **/ - public boolean IsBVSGE() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGEQ; } + public boolean IsBVSGE() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_SGEQ; } /** * Indicates whether the term is an unsigned bit-vector less-than **/ - public boolean IsBVULT() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULT; } + public boolean IsBVULT() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_ULT; } /** * Indicates whether the term is a signed bit-vector less-than **/ - public boolean IsBVSLT() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLT; } + public boolean IsBVSLT() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_SLT; } /** * Indicates whether the term is an unsigned bit-vector greater-than **/ - public boolean IsBVUGT() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGT; } + public boolean IsBVUGT() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_UGT; } /** * Indicates whether the term is a signed bit-vector greater-than **/ - public boolean IsBVSGT() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGT; } + public boolean IsBVSGT() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_SGT; } /** * Indicates whether the term is a bit-wise AND **/ - public boolean IsBVAND() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BAND; } + public boolean IsBVAND() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BAND; } /** * Indicates whether the term is a bit-wise OR **/ - public boolean IsBVOR() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BOR; } + public boolean IsBVOR() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BOR; } /** * Indicates whether the term is a bit-wise NOT **/ - public boolean IsBVNOT() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOT; } + public boolean IsBVNOT() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BNOT; } /** * Indicates whether the term is a bit-wise XOR **/ - public boolean IsBVXOR() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXOR; } + public boolean IsBVXOR() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BXOR; } /** * Indicates whether the term is a bit-wise NAND **/ - public boolean IsBVNAND() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNAND; } + public boolean IsBVNAND() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BNAND; } /** * Indicates whether the term is a bit-wise NOR **/ - public boolean IsBVNOR() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOR; } + public boolean IsBVNOR() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BNOR; } /** * Indicates whether the term is a bit-wise XNOR **/ - public boolean IsBVXNOR() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXNOR; } + public boolean IsBVXNOR() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BXNOR; } /** * Indicates whether the term is a bit-vector concatenation (binary) **/ - public boolean IsBVConcat() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONCAT; } + public boolean IsBVConcat() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_CONCAT; } /** * Indicates whether the term is a bit-vector sign extension **/ - public boolean IsBVSignExtension() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SIGN_EXT; } + public boolean IsBVSignExtension() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_SIGN_EXT; } /** * Indicates whether the term is a bit-vector zero extension **/ - public boolean IsBVZeroExtension() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ZERO_EXT; } + public boolean IsBVZeroExtension() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_ZERO_EXT; } /** * Indicates whether the term is a bit-vector extraction **/ - public boolean IsBVExtract() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXTRACT; } + public boolean IsBVExtract() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_EXTRACT; } /** * Indicates whether the term is a bit-vector repetition **/ - public boolean IsBVRepeat() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REPEAT; } + public boolean IsBVRepeat() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_REPEAT; } /** * Indicates whether the term is a bit-vector reduce OR **/ - public boolean IsBVReduceOR() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDOR; } + public boolean IsBVReduceOR() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BREDOR; } /** * Indicates whether the term is a bit-vector reduce AND **/ - public boolean IsBVReduceAND() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDAND; } + public boolean IsBVReduceAND() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BREDAND; } /** * Indicates whether the term is a bit-vector comparison **/ - public boolean IsBVComp() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BCOMP; } + public boolean IsBVComp() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BCOMP; } /** * Indicates whether the term is a bit-vector shift left **/ - public boolean IsBVShiftLeft() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSHL; } + public boolean IsBVShiftLeft() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BSHL; } /** * Indicates whether the term is a bit-vector logical shift right **/ - public boolean IsBVShiftRightLogical() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BLSHR; } + public boolean IsBVShiftRightLogical() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BLSHR; } /** * Indicates whether the term is a bit-vector arithmetic shift left **/ - public boolean IsBVShiftRightArithmetic() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BASHR; } + public boolean IsBVShiftRightArithmetic() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BASHR; } /** * Indicates whether the term is a bit-vector rotate left **/ - public boolean IsBVRotateLeft() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_LEFT; } + public boolean IsBVRotateLeft() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_ROTATE_LEFT; } /** * Indicates whether the term is a bit-vector rotate right **/ - public boolean IsBVRotateRight() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; } + public boolean IsBVRotateRight() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; } /** * Indicates whether the term is a bit-vector rotate left (extended) * Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one. **/ - public boolean IsBVRotateLeftExtended() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; } + public boolean IsBVRotateLeftExtended() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; } /** * Indicates whether the term is a bit-vector rotate right (extended) * Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one. **/ - public boolean IsBVRotateRightExtended() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; } + public boolean IsBVRotateRightExtended() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; } /** * Indicates whether the term is a coercion from integer to bit-vector * This function is not supported by the decision procedures. Only the most * rudimentary simplification rules are applied to this function. **/ - public boolean IsIntToBV() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INT2BV; } + public boolean IsIntToBV() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_INT2BV; } /** * Indicates whether the term is a coercion from bit-vector to integer * This function is not supported by the decision procedures. Only the most * rudimentary simplification rules are applied to this function. **/ - public boolean IsBVToInt() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BV2INT; } + public boolean IsBVToInt() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_BV2INT; } /** * Indicates whether the term is a bit-vector carry * Compute the carry bit in a full-adder. The meaning is given by the * equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3))) **/ - public boolean IsBVCarry() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CARRY; } + public boolean IsBVCarry() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_CARRY; } /** * Indicates whether the term is a bit-vector ternary XOR * The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3) **/ - public boolean IsBVXOR3() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR3; } + public boolean IsBVXOR3() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_XOR3; } /** * Indicates whether the term is a label (used by the Boogie Verification condition generator). * The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula. **/ - public boolean IsLabel() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL; } + public boolean IsLabel() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_LABEL; } /** * Indicates whether the term is a label literal (used by the Boogie Verification condition generator). * A label literal has a set of string parameters. It takes no arguments. **/ - public boolean IsLabelLit() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } + public boolean IsLabelLit() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT; } /** * Indicates whether the term is a binary equivalence modulo namings. * This binary predicate is used in proof terms. * It captures equisatisfiability and equivalence modulo renamings. **/ - public boolean IsOEQ() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OEQ; } + public boolean IsOEQ() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_OEQ; } /** * Indicates whether the term is a Proof for the expression 'true'. **/ - public boolean IsProofTrue() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRUE; } + public boolean IsProofTrue() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_TRUE; } /** * Indicates whether the term is a proof for a fact asserted by the user. **/ - public boolean IsProofAsserted() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ASSERTED; } + public boolean IsProofAsserted() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_ASSERTED; } /** * Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user. **/ - public boolean IsProofGoal() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_GOAL; } + public boolean IsProofGoal() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_GOAL; } /** * Indicates whether the term is proof via modus ponens @@ -740,7 +742,7 @@ import java.lang.Exception; * [mp T1 T2]: q * The second antecedents may also be a proof for (iff p q). **/ - public boolean IsProofModusPonens() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; } + public boolean IsProofModusPonens() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; } /** * Indicates whether the term is a proof for (R t t), where R is a reflexive relation. @@ -749,7 +751,7 @@ import java.lang.Exception; * equivalence modulo namings, equality and equivalence. * That is, R is either '~', '=' or 'iff'. **/ - public boolean IsProofReflexivity() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } + public boolean IsProofReflexivity() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } /** * Indicates whether the term is proof by symmetricity of a relation @@ -760,7 +762,7 @@ import java.lang.Exception; * T1 is the antecedent of this proof object. * **/ - public boolean IsProofSymmetry() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SYMMETRY; } + public boolean IsProofSymmetry() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_SYMMETRY; } /** * Indicates whether the term is a proof by transitivity of a relation @@ -772,7 +774,7 @@ import java.lang.Exception; * [trans T1 T2]: (R t u) * **/ - public boolean IsProofTransitivity() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; } + public boolean IsProofTransitivity() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; } /** * Indicates whether the term is a proof by condensed transitivity of a relation @@ -793,7 +795,7 @@ import java.lang.Exception; * antecedent (R a b) as an edge between a and b. * **/ - public boolean IsProofTransitivityStar() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; } + public boolean IsProofTransitivityStar() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; } /** @@ -807,7 +809,7 @@ import java.lang.Exception; * That is, reflexivity proofs are supressed to save space. * **/ - public boolean IsProofMonotonicity() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } + public boolean IsProofMonotonicity() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } /** * Indicates whether the term is a quant-intro proof @@ -817,7 +819,7 @@ import java.lang.Exception; * [quant-intro T1]: (~ (forall (x) p) (forall (x) q)) * **/ - public boolean IsProofQuantIntro() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } + public boolean IsProofQuantIntro() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } /** * Indicates whether the term is a distributivity proof object. @@ -835,7 +837,7 @@ import java.lang.Exception; * instantiated by f = or, and g = and. * **/ - public boolean IsProofDistributivity() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } + public boolean IsProofDistributivity() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } /** * Indicates whether the term is a proof by elimination of AND @@ -845,7 +847,7 @@ import java.lang.Exception; * [and-elim T1]: l_i * **/ - public boolean IsProofAndElimination() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } + public boolean IsProofAndElimination() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } /** * Indicates whether the term is a proof by eliminiation of not-or @@ -855,7 +857,7 @@ import java.lang.Exception; * [not-or-elim T1]: (not l_i) * **/ - public boolean IsProofOrElimination() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } + public boolean IsProofOrElimination() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } /** * Indicates whether the term is a proof by rewriting @@ -874,7 +876,7 @@ import java.lang.Exception; * (iff (or x false) x) * **/ - public boolean IsProofRewrite() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE; } + public boolean IsProofRewrite() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE; } /** * Indicates whether the term is a proof by rewriting @@ -890,7 +892,7 @@ import java.lang.Exception; * - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true) * **/ - public boolean IsProofRewriteStar() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } + public boolean IsProofRewriteStar() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } /** * Indicates whether the term is a proof for pulling quantifiers out. @@ -898,7 +900,7 @@ import java.lang.Exception; * A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents. * **/ - public boolean IsProofPullQuant() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } + public boolean IsProofPullQuant() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } /** * Indicates whether the term is a proof for pulling quantifiers out. @@ -908,7 +910,7 @@ import java.lang.Exception; * This proof object has no antecedents * **/ - public boolean IsProofPullQuantStar() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } + public boolean IsProofPullQuantStar() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } /** * Indicates whether the term is a proof for pushing quantifiers in. @@ -921,7 +923,7 @@ import java.lang.Exception; * This proof object has no antecedents * **/ - public boolean IsProofPushQuant() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } + public boolean IsProofPushQuant() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } /** * Indicates whether the term is a proof for elimination of unused variables. @@ -933,7 +935,7 @@ import java.lang.Exception; * This proof object has no antecedents. * **/ - public boolean IsProofElimUnusedVars() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; } + public boolean IsProofElimUnusedVars() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; } /** * Indicates whether the term is a proof for destructive equality resolution @@ -947,7 +949,7 @@ import java.lang.Exception; * Several variables can be eliminated simultaneously. * **/ - public boolean IsProofDER() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DER; } + public boolean IsProofDER() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_DER; } /** * Indicates whether the term is a proof for quantifier instantiation @@ -955,13 +957,13 @@ import java.lang.Exception; * A proof of (or (not (forall (x) (P x))) (P a)) * **/ - public boolean IsProofQuantInst() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } + public boolean IsProofQuantInst() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } /** * Indicates whether the term is a hypthesis marker. * Mark a hypothesis in a natural deduction style proof. **/ - public boolean IsProofHypothesis() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } + public boolean IsProofHypothesis() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } /** * Indicates whether the term is a proof by lemma @@ -974,7 +976,7 @@ import java.lang.Exception; * when T1 contains the hypotheses: l_1, ..., l_n. * **/ - public boolean IsProofLemma() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_LEMMA; } + public boolean IsProofLemma() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_LEMMA; } /** * Indicates whether the term is a proof by unit resolution @@ -986,7 +988,7 @@ import java.lang.Exception; * [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') * **/ - public boolean IsProofUnitResolution() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; } + public boolean IsProofUnitResolution() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; } /** * Indicates whether the term is a proof by iff-true @@ -995,7 +997,7 @@ import java.lang.Exception; * [iff-true T1]: (iff p true) * **/ - public boolean IsProofIFFTrue() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; } + public boolean IsProofIFFTrue() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; } /** * Indicates whether the term is a proof by iff-false @@ -1004,7 +1006,7 @@ import java.lang.Exception; * [iff-false T1]: (iff p false) * **/ - public boolean IsProofIFFFalse() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; } + public boolean IsProofIFFFalse() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; } /** * Indicates whether the term is a proof by commutativity @@ -1017,7 +1019,7 @@ import java.lang.Exception; * Remark: if f is bool, then = is iff. * **/ - public boolean IsProofCommutativity() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; } + public boolean IsProofCommutativity() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; } /** * Indicates whether the term is a proof for Tseitin-like axioms @@ -1053,7 +1055,7 @@ import java.lang.Exception; * bounded number of steps (=3). * **/ - public boolean IsProofDefAxiom() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; } + public boolean IsProofDefAxiom() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; } /** * Indicates whether the term is a proof for introduction of a name @@ -1076,7 +1078,7 @@ import java.lang.Exception; * [def-intro]: (= n e) * **/ - public boolean IsProofDefIntro() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } + public boolean IsProofDefIntro() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } /** * Indicates whether the term is a proof for application of a definition @@ -1086,7 +1088,7 @@ import java.lang.Exception; * n is a name for F. * **/ - public boolean IsProofApplyDef() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; } + public boolean IsProofApplyDef() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; } /** * Indicates whether the term is a proof iff-oeq @@ -1095,7 +1097,7 @@ import java.lang.Exception; * [iff~ T1]: (~ p q) * **/ - public boolean IsProofIFFOEQ() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; } + public boolean IsProofIFFOEQ() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; } /** * Indicates whether the term is a proof for a positive NNF step @@ -1123,7 +1125,7 @@ import java.lang.Exception; * over Boolean connectives 'and' and 'or'. * **/ - public boolean IsProofNNFPos() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_POS; } + public boolean IsProofNNFPos() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_POS; } /** * Indicates whether the term is a proof for a negative NNF step @@ -1148,7 +1150,7 @@ import java.lang.Exception; * (and (or r_1 r_2) (or r_1' r_2'))) * **/ - public boolean IsProofNNFNeg() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } + public boolean IsProofNNFNeg() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } /** * Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form. @@ -1160,7 +1162,7 @@ import java.lang.Exception; * This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. * **/ - public boolean IsProofNNFStar() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } + public boolean IsProofNNFStar() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } /** * Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form. @@ -1170,7 +1172,7 @@ import java.lang.Exception; * This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. * **/ - public boolean IsProofCNFStar() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } + public boolean IsProofCNFStar() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } /** * Indicates whether the term is a proof for a Skolemization step @@ -1183,7 +1185,7 @@ import java.lang.Exception; * This proof object has no antecedents. * **/ - public boolean IsProofSkolemize() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } + public boolean IsProofSkolemize() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } /** * Indicates whether the term is a proof by modus ponens for equi-satisfiability. @@ -1194,7 +1196,7 @@ import java.lang.Exception; * [mp~ T1 T2]: q * **/ - public boolean IsProofModusPonensOEQ() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } + public boolean IsProofModusPonensOEQ() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } /** * Indicates whether the term is a proof for theory lemma @@ -1213,15 +1215,16 @@ import java.lang.Exception; * - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test. * **/ - public boolean IsProofTheoryLemma() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; } + public boolean IsProofTheoryLemma() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; } /** * Indicates whether the term is of an array sort. **/ public boolean IsRelation() { - return (Native.isApp(Context().nCtx(), NativeObject()) != 0 && - (Z3_sort_kind)Native.getSortKind(Context().nCtx(), Native.getSort(Context().nCtx(), NativeObject())) == Z3_sort_kind.Z3_RELATION_SORT); + return (Native.isApp(Context().nCtx(), NativeObject()) && + Native.getSortKind(Context().nCtx(), Native.getSort(Context().nCtx(), NativeObject())) + == Z3_sort_kind.Z3_RELATION_SORT.toInt()); } /** @@ -1232,40 +1235,40 @@ import java.lang.Exception; * correspond to the n columns of the relation. * **/ - public boolean IsRelationStore() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_STORE; } + public boolean IsRelationStore() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_RA_STORE; } /** * Indicates whether the term is an empty relation **/ - public boolean IsEmptyRelation() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_EMPTY; } + public boolean IsEmptyRelation() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_RA_EMPTY; } /** * Indicates whether the term is a test for the emptiness of a relation **/ - public boolean IsIsEmptyRelation() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; } + public boolean IsIsEmptyRelation() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; } /** * Indicates whether the term is a relational join **/ - public boolean IsRelationalJoin() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_JOIN; } + public boolean IsRelationalJoin() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_RA_JOIN; } /** * Indicates whether the term is the union or convex hull of two relations. * The function takes two arguments. **/ - public boolean IsRelationUnion() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_UNION; } + public boolean IsRelationUnion() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_RA_UNION; } /** * Indicates whether the term is the widening of two relations * The function takes two arguments. **/ - public boolean IsRelationWiden() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_WIDEN; } + public boolean IsRelationWiden() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_RA_WIDEN; } /** * Indicates whether the term is a projection of columns (provided as numbers in the parameters). * The function takes one argument. **/ - public boolean IsRelationProject() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_PROJECT; } + public boolean IsRelationProject() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_RA_PROJECT; } /** * Indicates whether the term is a relation filter @@ -1277,7 +1280,7 @@ import java.lang.Exception; * So the first column in the relation has index 0. * **/ - public boolean IsRelationFilter() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_FILTER; } + public boolean IsRelationFilter() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_RA_FILTER; } /** * Indicates whether the term is an intersection of a relation with the negation of another. @@ -1293,7 +1296,7 @@ import java.lang.Exception; * x on the columns c1, d1, .., cN, dN. * **/ - public boolean IsRelationNegationFilter() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; } + public boolean IsRelationNegationFilter() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; } /** * Indicates whether the term is the renaming of a column in a relation @@ -1302,12 +1305,12 @@ import java.lang.Exception; * The parameters contain the renaming as a cycle. * **/ - public boolean IsRelationRename() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_RENAME; } + public boolean IsRelationRename() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_RA_RENAME; } /** * Indicates whether the term is the complement of a relation **/ - public boolean IsRelationComplement() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; } + public boolean IsRelationComplement() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; } /** * Indicates whether the term is a relational select @@ -1317,7 +1320,7 @@ import java.lang.Exception; * and the remaining n arguments correspond to a record. * **/ - public boolean IsRelationSelect() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_SELECT; } + public boolean IsRelationSelect() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_RA_SELECT; } /** * Indicates whether the term is a relational clone (copy) @@ -1329,21 +1332,21 @@ import java.lang.Exception; * to perform destructive updates to the first argument. * **/ - public boolean IsRelationClone() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_CLONE; } + public boolean IsRelationClone() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_RA_CLONE; } /** * Indicates whether the term is of an array sort. **/ public boolean IsFiniteDomain() { - return (Native.isApp(Context().nCtx(), NativeObject()) != 0 && - (Z3_sort_kind)Native.getSortKind(Context().nCtx(), Native.getSort(Context().nCtx(), NativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT); + return (Native.isApp(Context().nCtx(), NativeObject()) && + Native.getSortKind(Context().nCtx(), Native.getSort(Context().nCtx(), NativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT.toInt()); } /** * Indicates whether the term is a less than predicate over a finite domain. **/ - public boolean IsFiniteDomainLT() { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FD_LT; } + public boolean IsFiniteDomainLT() { return FuncDecl().DeclKind() == Z3_decl_kind.Z3_OP_FD_LT; } /** * The de-Burijn index of a bound variable. @@ -1364,9 +1367,9 @@ import java.lang.Exception; * index. * **/ - public long Index() + public int Index() { - if (!IsVar) + if (!IsVar()) throw new Z3Exception("Term is not a bound variable."); @@ -1385,9 +1388,9 @@ import java.lang.Exception; void CheckNativeObject(long obj) { - if (Native.isApp(Context().nCtx(), obj) == 0 && - (Z3_ast_kind)Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST && - (Z3_ast_kind)Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST) + if (Native.isApp(Context().nCtx(), obj) ^ true && + Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() && + Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt()) throw new Z3Exception("Underlying object is not a term"); super.CheckNativeObject(obj); } @@ -1398,7 +1401,7 @@ import java.lang.Exception; - long obj = Native.mkApp(ctx.nCtx(), f.NativeObject, + long obj = Native.mkApp(ctx.nCtx(), f.NativeObject(), AST.ArrayLength(arguments), AST.ArrayToNative(arguments)); return Create(ctx, obj); @@ -1409,33 +1412,33 @@ import java.lang.Exception; - Z3_ast_kind k = (Z3_ast_kind)Native.getAstKind(ctx.nCtx(), obj); + Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)); if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) return new Quantifier(ctx, obj); long s = Native.getSort(ctx.nCtx(), obj); - Z3_sort_kind sk = (Z3_sort_kind)Native.getSortKind(ctx.nCtx(), s); + Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), s)); - if (Native.isAlgebraicNumber(ctx.nCtx(), obj) != 0) // is this a numeral ast? + if (Native.isAlgebraicNumber(ctx.nCtx(), obj) ) // is this a numeral ast? return new AlgebraicNum(ctx, obj); - if (Native.isNumeralAst(ctx.nCtx(), obj) != 0) + if (Native.isNumeralAst(ctx.nCtx(), obj) ) { switch (sk) { - case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj); - case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj); - case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj); + case Z3_INT_SORT: return new IntNum(ctx, obj); + case Z3_REAL_SORT: return new RatNum(ctx, obj); + case Z3_BV_SORT: return new BitVecNum(ctx, obj); } } switch (sk) { - case Z3_sort_kind.Z3_BOOL_SORT: return new BoolExpr(ctx, obj); - case Z3_sort_kind.Z3_INT_SORT: return new IntExpr(ctx, obj); - case Z3_sort_kind.Z3_REAL_SORT: return new RealExpr(ctx, obj); - case Z3_sort_kind.Z3_BV_SORT: return new BitVecExpr(ctx, obj); - case Z3_sort_kind.Z3_ARRAY_SORT: return new ArrayExpr(ctx, obj); - case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj); + case Z3_BOOL_SORT: return new BoolExpr(ctx, obj); + case Z3_INT_SORT: return new IntExpr(ctx, obj); + case Z3_REAL_SORT: return new RealExpr(ctx, obj); + case Z3_BV_SORT: return new BitVecExpr(ctx, obj); + case Z3_ARRAY_SORT: return new ArrayExpr(ctx, obj); + case Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj); } return new Expr(ctx, obj); diff --git a/src/api/java/com/Microsoft/Z3/FiniteDomainSort.java b/src/api/java/com/Microsoft/Z3/FiniteDomainSort.java index 016d0fecc..49a2c40c5 100644 --- a/src/api/java/com/Microsoft/Z3/FiniteDomainSort.java +++ b/src/api/java/com/Microsoft/Z3/FiniteDomainSort.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -30,7 +31,7 @@ import java.lang.Exception; } 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)); diff --git a/src/api/java/com/Microsoft/Z3/Fixedpoint.java b/src/api/java/com/Microsoft/Z3/Fixedpoint.java index 0c38f9679..104fd354c 100644 --- a/src/api/java/com/Microsoft/Z3/Fixedpoint.java +++ b/src/api/java/com/Microsoft/Z3/Fixedpoint.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -31,14 +32,14 @@ import java.lang.Exception; public void setParameters(Params value) { - Context.CheckContextMatch(value); - Native.fixedpointSetParams(Context().nCtx(), NativeObject(), value.NativeObject); + Context().CheckContextMatch(value); + Native.fixedpointSetParams(Context().nCtx(), NativeObject(), value.NativeObject()); } /** * 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); - for (Iterator a = constraints.iterator(); a.hasNext(); ) + Context().CheckContextMatch(constraints); + 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); - Native.fixedpointRegisterRelation(Context().nCtx(), NativeObject(), f.NativeObject); + Context().CheckContextMatch(f); + Native.fixedpointRegisterRelation(Context().nCtx(), NativeObject(), f.NativeObject()); } /** @@ -74,20 +75,20 @@ import java.lang.Exception; { - Context.CheckContextMatch(rule); - Native.fixedpointAddRule(Context().nCtx(), NativeObject(), rule.NativeObject, AST.GetNativeObject(name)); + Context().CheckContextMatch(rule); + Native.fixedpointAddRule(Context().nCtx(), NativeObject(), rule.NativeObject(), AST.GetNativeObject(name)); } /** * Add table fact to the fixedpoint solver. **/ - public void AddFact(FuncDecl pred, long[] args) + public void AddFact(FuncDecl pred, int[] args) { - Context.CheckContextMatch(pred); - Native.fixedpointAddFact(Context().nCtx(), NativeObject(), pred.NativeObject, (long)args.Length, args); + Context().CheckContextMatch(pred); + Native.fixedpointAddFact(Context().nCtx(), NativeObject(), pred.NativeObject(), (int)args.length, args); } /** @@ -100,12 +101,12 @@ import java.lang.Exception; { - Context.CheckContextMatch(query); - Z3_lbool r = (Z3_lbool)Native.fixedpointQuery(Context().nCtx(), NativeObject(), query.NativeObject); + Context().CheckContextMatch(query); + Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(Context().nCtx(), NativeObject(), query.NativeObject())); switch (r) { - case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE; - case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE; + case Z3_L_TRUE: return Status.SATISFIABLE; + case Z3_L_FALSE: return Status.UNSATISFIABLE; 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(), AST.ArrayLength(relations), AST.ArrayToNative(relations)); switch (r) { - case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE; - case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE; + case Z3_L_TRUE: return Status.SATISFIABLE; + case Z3_L_FALSE: return Status.UNSATISFIABLE; default: return Status.UNKNOWN; } } @@ -159,8 +160,8 @@ import java.lang.Exception; { - Context.CheckContextMatch(rule); - Native.fixedpointUpdateRule(Context().nCtx(), NativeObject(), rule.NativeObject, AST.GetNativeObject(name)); + Context().CheckContextMatch(rule); + Native.fixedpointUpdateRule(Context().nCtx(), NativeObject(), rule.NativeObject(), AST.GetNativeObject(name)); } /** @@ -170,7 +171,7 @@ import java.lang.Exception; public Expr GetAnswer() { 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. **/ - 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) { - long res = Native.fixedpointGetCoverDelta(Context().nCtx(), NativeObject(), level, predicate.NativeObject); - return (res == 0) ? null : Expr.Create(Context, res); + long res = Native.fixedpointGetCoverDelta(Context().nCtx(), NativeObject(), level, predicate.NativeObject()); + 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) { - 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(), - 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())); - long n = v.Size; + ASTVector v = new ASTVector(Context(), Native.fixedpointGetRules(Context().nCtx(), NativeObject())); + int n = v.Size; BoolExpr[] res = new BoolExpr[n]; - for (long i; i < n; i++) - res[i] = new BoolExpr(Context, v[i].NativeObject); + for (int i = 0; i < n; i++) + res[i] = new BoolExpr(Context(), v[i].NativeObject()); return res; } @@ -261,11 +262,11 @@ import java.lang.Exception; { - ASTVector v = new ASTVector(Context, Native.fixedpointGetAssertions(Context().nCtx(), NativeObject())); - long n = v.Size; + ASTVector v = new ASTVector(Context(), Native.fixedpointGetAssertions(Context().nCtx(), NativeObject())); + int n = v.Size; BoolExpr[] res = new BoolExpr[n]; - for (long i; i < n; i++) - res[i] = new BoolExpr(Context, v[i].NativeObject); + for (int i = 0; i < n; i++) + res[i] = new BoolExpr(Context(), v[i].NativeObject()); return res; } @@ -294,13 +295,13 @@ import java.lang.Exception; void IncRef(long o) { - Context.Fixedpoint_DRQ.IncAndClear(Context, o); + Context().Fixedpoint_DRQ().IncAndClear(Context(), o); super.IncRef(o); } void DecRef(long o) { - Context.Fixedpoint_DRQ.Add(o); + Context().Fixedpoint_DRQ().Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/FuncDecl.java b/src/api/java/com/Microsoft/Z3/FuncDecl.java index 91579b085..aa716c028 100644 --- a/src/api/java/com/Microsoft/Z3/FuncDecl.java +++ b/src/api/java/com/Microsoft/Z3/FuncDecl.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -56,18 +57,18 @@ import java.lang.Exception; /** * 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 **/ - 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 * **/ - public long DomainSize() { return Native.getDomainSize(Context().nCtx(), NativeObject()); } + public int DomainSize() { return Native.getDomainSize(Context().nCtx(), NativeObject()); } /** * The domain of the function declaration @@ -79,8 +80,8 @@ import java.lang.Exception; var n = DomainSize; Sort[] res = new Sort[n]; - for (long i; i < n; i++) - res[i] = Sort.Create(Context, Native.getDomain(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = Sort.Create(Context(), Native.getDomain(Context().nCtx(), NativeObject(), i)); return res; } @@ -90,13 +91,13 @@ import java.lang.Exception; 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. **/ - 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 @@ -104,13 +105,13 @@ import java.lang.Exception; 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 **/ - public long NumParameters() { return Native.getDeclNumParameters(Context().nCtx(), NativeObject()); } + public int NumParameters() { return Native.getDeclNumParameters(Context().nCtx(), NativeObject()); } /** * 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]; - 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) { - case Z3_parameter_kind.Z3_PARAMETER_INT: + case Z3_PARAMETER_INT: res[i] = new Parameter(k, Native.getDeclIntParameter(Context().nCtx(), NativeObject(), i)); break; - case Z3_parameter_kind.Z3_PARAMETER_DOUBLE: + case Z3_PARAMETER_DOUBLE: res[i] = new Parameter(k, Native.getDeclDoubleParameter(Context().nCtx(), NativeObject(), i)); break; - case Z3_parameter_kind.Z3_PARAMETER_SYMBOL: - res[i] = new Parameter(k, Symbol.Create(Context, Native.getDeclSymbolParameter(Context().nCtx(), NativeObject(), i))); + case Z3_PARAMETER_SYMBOL: + res[i] = new Parameter(k, Symbol.Create(Context(), Native.getDeclSymbolParameter(Context().nCtx(), NativeObject(), i))); break; - case Z3_parameter_kind.Z3_PARAMETER_SORT: - res[i] = new Parameter(k, Sort.Create(Context, Native.getDeclSortParameter(Context().nCtx(), NativeObject(), i))); + case Z3_PARAMETER_SORT: + res[i] = new Parameter(k, Sort.Create(Context(), Native.getDeclSortParameter(Context().nCtx(), NativeObject(), i))); break; - case Z3_parameter_kind.Z3_PARAMETER_AST: - res[i] = new Parameter(k, new AST(Context, Native.getDeclAstParameter(Context().nCtx(), NativeObject(), i))); + case Z3_PARAMETER_AST: + res[i] = new Parameter(k, new AST(Context(), Native.getDeclAstParameter(Context().nCtx(), NativeObject(), i))); break; - case Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL: - res[i] = new Parameter(k, new FuncDecl(Context, Native.getDeclFuncDeclParameter(Context().nCtx(), NativeObject(), i))); + case Z3_PARAMETER_FUNC_DECL: + res[i] = new Parameter(k, new FuncDecl(Context(), Native.getDeclFuncDeclParameter(Context().nCtx(), NativeObject(), i))); break; - case Z3_parameter_kind.Z3_PARAMETER_RATIONAL: + case Z3_PARAMETER_RATIONAL: res[i] = new Parameter(k, Native.getDeclRationalParameter(Context().nCtx(), NativeObject(), i)); break; default: @@ -244,21 +245,21 @@ import java.lang.Exception; } 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) - { 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) { - 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"); super.CheckNativeObject(obj); } @@ -279,8 +280,8 @@ import java.lang.Exception; { - Context.CheckContextMatch(args); - return Expr.Create(Context, this, args); + Context().CheckContextMatch(args); + return Expr.Create(Context(), this, args); } } diff --git a/src/api/java/com/Microsoft/Z3/FuncInterp.java b/src/api/java/com/Microsoft/Z3/FuncInterp.java index 7544aba11..341b82ec5 100644 --- a/src/api/java/com/Microsoft/Z3/FuncInterp.java +++ b/src/api/java/com/Microsoft/Z3/FuncInterp.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -28,13 +29,13 @@ import java.lang.Exception; 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. **/ - public long NumArgs() { return Native.funcEntryGetNumArgs(Context().nCtx(), NativeObject()); } + public int NumArgs() { return Native.funcEntryGetNumArgs(Context().nCtx(), NativeObject()); } /** * 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]; - for (long i; i < n; i++) - res[i] = Expr.Create(Context, Native.funcEntryGetArg(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = Expr.Create(Context(), Native.funcEntryGetArg(Context().nCtx(), NativeObject(), i)); return res; } @@ -56,10 +57,10 @@ import java.lang.Exception; **/ public String toString() { - long n = NumArgs; + int n = NumArgs(); String res = "["; Expr[] args = Args; - for (long i; i < n; i++) + for (int i = 0; i < n; i++) res += args[i] + ", "; return res + Value + "]"; } @@ -81,13 +82,13 @@ import java.lang.Exception; void IncRef(long o) { - Context.FuncEntry_DRQ.IncAndClear(Context, o); + Context().FuncEntry_DRQ().IncAndClear(Context(), o); super.IncRef(o); } void DecRef(long o) { - Context.FuncEntry_DRQ.Add(o); + Context().FuncEntry_DRQ().Add(o); super.DecRef(o); } }; @@ -95,7 +96,7 @@ import java.lang.Exception; /** * 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 @@ -105,10 +106,10 @@ import java.lang.Exception; - long n = NumEntries; + int n = NumEntries(); Entry[] res = new Entry[n]; - for (long i; i < n; i++) - res[i] = new Entry(Context, Native.funcInterpGetEntry(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = new Entry(Context(), Native.funcInterpGetEntry(Context().nCtx(), NativeObject(), i)); 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 **/ - 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. @@ -134,12 +135,12 @@ import java.lang.Exception; { String 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 += "["; Expr[] args = e.Args; - for (long i; i < n; i++) + for (int i = 0; i < n; i++) { if (i != 0) res += ", "; res += args[i]; @@ -172,13 +173,13 @@ import java.lang.Exception; void IncRef(long o) { - Context.FuncInterp_DRQ.IncAndClear(Context, o); + Context().FuncInterp_DRQ().IncAndClear(Context(), o); super.IncRef(o); } void DecRef(long o) { - Context.FuncInterp_DRQ.Add(o); + Context().FuncInterp_DRQ().Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/Goal.java b/src/api/java/com/Microsoft/Z3/Goal.java index bfbefa203..9f522a768 100644 --- a/src/api/java/com/Microsoft/Z3/Goal.java +++ b/src/api/java/com/Microsoft/Z3/Goal.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* 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. * **/ - 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. @@ -54,18 +55,18 @@ import java.lang.Exception; - Context.CheckContextMatch(constraints); - for (Iterator c = constraints.iterator(); c.hasNext(); ) + Context().CheckContextMatch(constraints); + for (BoolExpr c: constraints) { // 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'. **/ - public boolean Inconsistent() { return Native.goalInconsistent(Context().nCtx(), NativeObject()) != 0; } + public boolean Inconsistent() { return Native.goalInconsistent(Context().nCtx(), NativeObject()) ; } /** * The depth of the goal. @@ -73,7 +74,7 @@ import java.lang.Exception; * This tracks how many transformations were applied to it. * **/ - 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. @@ -86,7 +87,7 @@ import java.lang.Exception; /** * 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. @@ -95,27 +96,27 @@ import java.lang.Exception; { - long n = Size; + int n = Size; BoolExpr[] res = new BoolExpr[n]; - for (long i; i < n; i++) - res[i] = new BoolExpr(Context, Native.goalFormula(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = new BoolExpr(Context(), Native.goalFormula(Context().nCtx(), NativeObject(), i)); return res; } /** * 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. **/ - 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. **/ - 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 . @@ -133,11 +134,11 @@ import java.lang.Exception; **/ public Goal Simplify(Params p) { - Tactic t = Context.MkTactic("simplify"); + Tactic t = Context().MkTactic("simplify"); ApplyResult res = t.Apply(this, p); if (res.NumSubgoals == 0) - return Context.MkGoal(); + return Context().MkGoal(); else return res.Subgoals[0]; } @@ -154,7 +155,7 @@ import java.lang.Exception; Goal(Context ctx, long obj) { super(ctx, obj); { }} 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) { - Context.Goal_DRQ.IncAndClear(Context, o); + Context().Goal_DRQ().IncAndClear(Context(), o); super.IncRef(o); } void DecRef(long o) { - Context.Goal_DRQ.Add(o); + Context().Goal_DRQ().Add(o); super.DecRef(o); } diff --git a/src/api/java/com/Microsoft/Z3/IDecRefQueue.java b/src/api/java/com/Microsoft/Z3/IDecRefQueue.java index 1b6291ce7..4d40bf66a 100644 --- a/src/api/java/com/Microsoft/Z3/IDecRefQueue.java +++ b/src/api/java/com/Microsoft/Z3/IDecRefQueue.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Collections; */ @@ -23,8 +24,8 @@ import java.lang.Exception; protected Object m_lock = new Object(); - protected List m_queue = new List(); - final long m_move_limit = 1024; + protected LinkedList m_queue = new LinkedList(); + final int m_move_limit = 1024; public abstract void IncRef(Context ctx, long obj); public abstract void DecRef(Context ctx, long obj); @@ -34,7 +35,7 @@ import java.lang.Exception; 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) @@ -43,7 +44,7 @@ import java.lang.Exception; synchronized (m_lock) { - m_queue.Add(o); + m_queue.add(o); } } @@ -53,9 +54,9 @@ import java.lang.Exception; synchronized (m_lock) { - for (Iterator o = m_queue.iterator(); o.hasNext(); ) + for (Long o: m_queue) DecRef(ctx, o); - m_queue.Clear(); + m_queue.clear(); } } } diff --git a/src/api/java/com/Microsoft/Z3/IntExpr.java b/src/api/java/com/Microsoft/Z3/IntExpr.java index 888e441b3..d493947d9 100644 --- a/src/api/java/com/Microsoft/Z3/IntExpr.java +++ b/src/api/java/com/Microsoft/Z3/IntExpr.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Collections.Generic; */ /* using System.Linq; */ diff --git a/src/api/java/com/Microsoft/Z3/IntNum.java b/src/api/java/com/Microsoft/Z3/IntNum.java index e4d0e72e2..494ac316b 100644 --- a/src/api/java/com/Microsoft/Z3/IntNum.java +++ b/src/api/java/com/Microsoft/Z3/IntNum.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Numerics; */ @@ -29,7 +30,7 @@ import java.lang.Exception; public long UInt64() { 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"); return res; } @@ -40,7 +41,7 @@ import java.lang.Exception; public int Int() { 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"); return res; } @@ -51,7 +52,7 @@ import java.lang.Exception; public long Int64() { 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"); return res; } @@ -59,11 +60,11 @@ import java.lang.Exception; /** * Retrieve the int value. **/ - public long UInt() + public int UInt() { - long res = 0; - if (Native.getNumeralLong(Context().nCtx(), NativeObject(), res) == 0) - throw new Z3Exception("Numeral is not a long"); + int res = 0; + if (Native.getNumeralInt(Context().nCtx(), NativeObject(), res) ^ true) + throw new Z3Exception("Numeral is not a int"); return res; } @@ -72,7 +73,7 @@ import java.lang.Exception; **/ public BigInteger BigInteger() { - return BigInteger.Parse(this.ToString()); + return new BigInteger(this.toString()); } /** diff --git a/src/api/java/com/Microsoft/Z3/IntSort.java b/src/api/java/com/Microsoft/Z3/IntSort.java index 29ff35136..b347cc149 100644 --- a/src/api/java/com/Microsoft/Z3/IntSort.java +++ b/src/api/java/com/Microsoft/Z3/IntSort.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ diff --git a/src/api/java/com/Microsoft/Z3/IntSymbol.java b/src/api/java/com/Microsoft/Z3/IntSymbol.java index 0132def21..1750d87e6 100644 --- a/src/api/java/com/Microsoft/Z3/IntSymbol.java +++ b/src/api/java/com/Microsoft/Z3/IntSymbol.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Runtime.InteropServices; */ diff --git a/src/api/java/com/Microsoft/Z3/ListSort.java b/src/api/java/com/Microsoft/Z3/ListSort.java index 96829c11e..4efee3783 100644 --- a/src/api/java/com/Microsoft/Z3/ListSort.java +++ b/src/api/java/com/Microsoft/Z3/ListSort.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -109,7 +110,7 @@ import java.lang.Exception; ihead = 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); nilDecl = new FuncDecl(ctx, inil); isNilDecl = new FuncDecl(ctx, iisnil); diff --git a/src/api/java/com/Microsoft/Z3/Log.java b/src/api/java/com/Microsoft/Z3/Log.java index bfcc2b1c5..2572f9880 100644 --- a/src/api/java/com/Microsoft/Z3/Log.java +++ b/src/api/java/com/Microsoft/Z3/Log.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ diff --git a/src/api/java/com/Microsoft/Z3/Model.java b/src/api/java/com/Microsoft/Z3/Model.java index e20a9d575..c0c0e2852 100644 --- a/src/api/java/com/Microsoft/Z3/Model.java +++ b/src/api/java/com/Microsoft/Z3/Model.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -24,7 +25,7 @@ import java.lang.Exception; { - Context.CheckContextMatch(a); + Context().CheckContextMatch(a); return ConstInterp(a.FuncDecl); } @@ -37,16 +38,16 @@ import java.lang.Exception; { - Context.CheckContextMatch(f); + Context().CheckContextMatch(f); 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."); - long n = Native.modelGetConstInterp(Context().nCtx(), NativeObject(), f.NativeObject); + long n = Native.modelGetConstInterp(Context().nCtx(), NativeObject(), f.NativeObject()); if (n == 0) return null; 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) { - 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) { @@ -72,10 +73,10 @@ import java.lang.Exception; return null; else { - if (Native.isAsArray(Context().nCtx(), n) == 0) + if (Native.isAsArray(Context().nCtx(), n) ^ true) throw new Z3Exception("Argument was not an array constant"); long fd = Native.getAsArrayFuncDecl(Context().nCtx(), n); - return FuncInterp(new FuncDecl(Context, fd)); + return FuncInterp(new FuncDecl(Context(), fd)); } } else @@ -85,18 +86,18 @@ import java.lang.Exception; } else { - long n = Native.modelGetFuncInterp(Context().nCtx(), NativeObject(), f.NativeObject); + long n = Native.modelGetFuncInterp(Context().nCtx(), NativeObject(), f.NativeObject()); if (n == 0) return null; else - return new FuncInterp(Context, n); + return new FuncInterp(Context(), n); } } /** * 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. @@ -105,17 +106,17 @@ import java.lang.Exception; { - long n = NumConsts; + int n = NumConsts(); FuncDecl[] res = new FuncDecl[n]; - for (long i; i < n; i++) - res[i] = new FuncDecl(Context, Native.modelGetConstDecl(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = new FuncDecl(Context(), Native.modelGetConstDecl(Context().nCtx(), NativeObject(), i)); return res; } /** * 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. @@ -124,10 +125,10 @@ import java.lang.Exception; { - long n = NumFuncs; + int n = NumFuncs(); FuncDecl[] res = new FuncDecl[n]; - for (long i; i < n; i++) - res[i] = new FuncDecl(Context, Native.modelGetFuncDecl(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = new FuncDecl(Context(), Native.modelGetFuncDecl(Context().nCtx(), NativeObject(), i)); return res; } @@ -138,14 +139,14 @@ import java.lang.Exception; { - var nFuncs = NumFuncs; - var nConsts = NumConsts; - long n = nFuncs + nConsts; + var nFuncs = NumFuncs(); + var nConsts = NumConsts(); + int n = nFuncs + nConsts; FuncDecl[] res = new FuncDecl[n]; - for (long i; i < nConsts; i++) - res[i] = new FuncDecl(Context, Native.modelGetConstDecl(Context().nCtx(), NativeObject(), i)); - for (long i; i < nFuncs; i++) - res[nConsts + i] = new FuncDecl(Context, Native.modelGetFuncDecl(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < nConsts; i++) + res[i] = new FuncDecl(Context(), Native.modelGetConstDecl(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < nFuncs; i++) + res[nConsts + i] = new FuncDecl(Context(), Native.modelGetFuncDecl(Context().nCtx(), NativeObject(), i)); return res; } @@ -180,10 +181,10 @@ import java.lang.Exception; 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(); 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. **/ - 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. @@ -216,10 +217,10 @@ import java.lang.Exception; { - long n = NumSorts; + int n = NumSorts(); Sort[] res = new Sort[n]; - for (long i; i < n; i++) - res[i] = Sort.Create(Context, Native.modelGetSort(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = Sort.Create(Context(), Native.modelGetSort(Context().nCtx(), NativeObject(), i)); return res; } @@ -234,11 +235,11 @@ import java.lang.Exception; - ASTVector nUniv = new ASTVector(Context, Native.modelGetSortUniverse(Context().nCtx(), NativeObject(), s.NativeObject)); - long n = nUniv.Size; + ASTVector nUniv = new ASTVector(Context(), Native.modelGetSortUniverse(Context().nCtx(), NativeObject(), s.NativeObject())); + int n = nUniv.Size; Expr[] res = new Expr[n]; - for (long i; i < n; i++) - res[i] = Expr.Create(Context, nUniv[i].NativeObject); + for (int i = 0; i < n; i++) + res[i] = Expr.Create(Context(), nUniv[i].NativeObject()); return res; } @@ -271,13 +272,13 @@ import java.lang.Exception; void IncRef(long o) { - Context.Model_DRQ.IncAndClear(Context, o); + Context().Model_DRQ().IncAndClear(Context(), o); super.IncRef(o); } void DecRef(long o) { - Context.Model_DRQ.Add(o); + Context().Model_DRQ().Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/Native.java b/src/api/java/com/Microsoft/Z3/Native.java index 261e0663f..e42d8b7ba 100644 --- a/src/api/java/com/Microsoft/Z3/Native.java +++ b/src/api/java/com/Microsoft/Z3/Native.java @@ -4,8 +4,8 @@ public final class Native { public static class IntPtr { public int value; } public static class LongPtr { public long value; } public static class StringPtr { public String value; } - public static class errorHandler {}; - static { System.loadLibrary(""); } + public static class errorHandler { public long ptr; } + static { System.loadLibrary(""); } public static native long mkConfig(); public static native void delConfig(long a0); public static native void setParamValue(long a0, String a1, String a2); diff --git a/src/api/java/com/Microsoft/Z3/ParamDescrs.java b/src/api/java/com/Microsoft/Z3/ParamDescrs.java index 37ee77b7e..edba1ceab 100644 --- a/src/api/java/com/Microsoft/Z3/ParamDescrs.java +++ b/src/api/java/com/Microsoft/Z3/ParamDescrs.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -21,7 +22,7 @@ import java.lang.Exception; 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) { - 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() { - long sz = Native.paramDescrsSize(Context().nCtx(), NativeObject()); + int sz = Native.paramDescrsSize(Context().nCtx(), NativeObject()); Symbol[] names = new Symbol[sz]; - for (long i; i < sz; ++i) { - names[i] = Symbol.Create(Context, Native.paramDescrsGetName(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < sz; ++i) { + names[i] = Symbol.Create(Context(), Native.paramDescrsGetName(Context().nCtx(), NativeObject(), i)); } return names; } @@ -49,7 +50,7 @@ import java.lang.Exception; /** * 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. @@ -79,13 +80,13 @@ import java.lang.Exception; void IncRef(long o) { - Context.ParamDescrs_DRQ.IncAndClear(Context, o); + Context().ParamDescrs_DRQ().IncAndClear(Context(), o); super.IncRef(o); } void DecRef(long o) { - Context.ParamDescrs_DRQ.Add(o); + Context().ParamDescrs_DRQ().Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/Params.java b/src/api/java/com/Microsoft/Z3/Params.java index d5c042d74..1107a80ee 100644 --- a/src/api/java/com/Microsoft/Z3/Params.java +++ b/src/api/java/com/Microsoft/Z3/Params.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* 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. **/ - 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) { - 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. **/ - 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) { - 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) { - Context.Params_DRQ.IncAndClear(Context, o); + Context().Params_DRQ().IncAndClear(Context(), o); super.IncRef(o); } void DecRef(long o) { - Context.Params_DRQ.Add(o); + Context().Params_DRQ().Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/Pattern.java b/src/api/java/com/Microsoft/Z3/Pattern.java index 0e87dc254..99fb53b9c 100644 --- a/src/api/java/com/Microsoft/Z3/Pattern.java +++ b/src/api/java/com/Microsoft/Z3/Pattern.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Runtime.InteropServices; */ @@ -21,7 +22,7 @@ import java.lang.Exception; /** * 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. @@ -30,10 +31,10 @@ import java.lang.Exception; { - long n = NumTerms; + int n = NumTerms(); Expr[] res = new Expr[n]; - for (long i; i < n; i++) - res[i] = Expr.Create(Context, Native.getPattern(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = Expr.Create(Context(), Native.getPattern(Context().nCtx(), NativeObject(), i)); return res; } diff --git a/src/api/java/com/Microsoft/Z3/Probe.java b/src/api/java/com/Microsoft/Z3/Probe.java index 537e9ef7f..8d1ba1a97 100644 --- a/src/api/java/com/Microsoft/Z3/Probe.java +++ b/src/api/java/com/Microsoft/Z3/Probe.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Runtime.InteropServices; */ @@ -29,8 +30,8 @@ import java.lang.Exception; { - Context.CheckContextMatch(g); - return Native.probeApply(Context().nCtx(), NativeObject(), g.NativeObject); + Context().CheckContextMatch(g); + return Native.probeApply(Context().nCtx(), NativeObject(), g.NativeObject()); } /** @@ -67,13 +68,13 @@ import java.lang.Exception; void IncRef(long o) { - Context.Probe_DRQ.IncAndClear(Context, o); + Context().Probe_DRQ().IncAndClear(Context(), o); super.IncRef(o); } void DecRef(long o) { - Context.Probe_DRQ.Add(o); + Context().Probe_DRQ().Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/Quantifier.java b/src/api/java/com/Microsoft/Z3/Quantifier.java index 8b4df947e..ad05c544b 100644 --- a/src/api/java/com/Microsoft/Z3/Quantifier.java +++ b/src/api/java/com/Microsoft/Z3/Quantifier.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -18,7 +19,7 @@ import java.lang.Exception; /** * 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. @@ -28,12 +29,12 @@ import java.lang.Exception; /** * 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. **/ - public long NumPatterns() { return Native.getQuantifierNumPatterns(Context().nCtx(), NativeObject()); } + public int NumPatterns() { return Native.getQuantifierNumPatterns(Context().nCtx(), NativeObject()); } /** * The patterns. @@ -42,17 +43,17 @@ import java.lang.Exception; { - long n = NumPatterns; + int n = NumPatterns(); Pattern[] res = new Pattern[n]; - for (long i; i < n; i++) - res[i] = new Pattern(Context, Native.getQuantifierPatternAst(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = new Pattern(Context(), Native.getQuantifierPatternAst(Context().nCtx(), NativeObject(), i)); return res; } /** * 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. @@ -61,17 +62,17 @@ import java.lang.Exception; { - long n = NumNoPatterns; + int n = NumNoPatterns(); Pattern[] res = new Pattern[n]; - for (long i; i < n; i++) - res[i] = new Pattern(Context, Native.getQuantifierNoPatternAst(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = new Pattern(Context(), Native.getQuantifierNoPatternAst(Context().nCtx(), NativeObject(), i)); return res; } /** * 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. @@ -80,10 +81,10 @@ import java.lang.Exception; { - long n = NumBound; + int n = NumBound(); Symbol[] res = new Symbol[n]; - for (long i; i < n; i++) - res[i] = Symbol.Create(Context, Native.getQuantifierBoundName(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = Symbol.Create(Context(), Native.getQuantifierBoundName(Context().nCtx(), NativeObject(), i)); return res; } @@ -94,10 +95,10 @@ import java.lang.Exception; { - long n = NumBound; + int n = NumBound(); Sort[] res = new Sort[n]; - for (long i; i < n; i++) - res[i] = Sort.Create(Context, Native.getQuantifierBoundSort(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = Sort.Create(Context(), Native.getQuantifierBoundSort(Context().nCtx(), NativeObject(), i)); 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); @@ -123,38 +124,38 @@ import java.lang.Exception; - Context.CheckContextMatch(patterns); - Context.CheckContextMatch(noPatterns); - Context.CheckContextMatch(sorts); - Context.CheckContextMatch(names); - Context.CheckContextMatch(body); + Context().CheckContextMatch(patterns); + Context().CheckContextMatch(noPatterns); + Context().CheckContextMatch(sorts); + Context().CheckContextMatch(names); + 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"); long[] _patterns = AST.ArrayToNative(patterns); 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(sorts), AST.ArrayToNative(sorts), Symbol.ArrayToNative(names), - body.NativeObject); + body.NativeObject()); } 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.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns), AST.ArrayLength(sorts), AST.ArrayToNative(sorts), 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); @@ -163,26 +164,26 @@ import java.lang.Exception; - Context.CheckContextMatch(noPatterns); - Context.CheckContextMatch(patterns); - //Context.CheckContextMatch(bound); - Context.CheckContextMatch(body); + Context().CheckContextMatch(noPatterns); + Context().CheckContextMatch(patterns); + //Context().CheckContextMatch(bound); + Context().CheckContextMatch(body); 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(patterns), AST.ArrayToNative(patterns), - body.NativeObject); + body.NativeObject()); } 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.ArrayLength(bound), AST.ArrayToNative(bound), AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns), - body.NativeObject); + body.NativeObject()); } } diff --git a/src/api/java/com/Microsoft/Z3/RatNum.java b/src/api/java/com/Microsoft/Z3/RatNum.java index 7921e70ef..ad0982a95 100644 --- a/src/api/java/com/Microsoft/Z3/RatNum.java +++ b/src/api/java/com/Microsoft/Z3/RatNum.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* 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() { - IntNum n = Numerator; - return BigInteger.Parse(n.ToString()); + IntNum n = Numerator(); + return new BigInteger(n.toString()); } /** @@ -50,15 +51,15 @@ import java.lang.Exception; **/ public BigInteger BigIntDenominator() { - IntNum n = Denominator; - return BigInteger.Parse(n.ToString()); + IntNum n = Denominator(); + return new BigInteger(n.toString()); } /** * Returns a string representation in decimal notation. * The result has at most decimal places. **/ - public String ToDecimalString(long precision) + public String ToDecimalString(int precision) { return Native.getNumeralDecimalString(Context().nCtx(), NativeObject(), precision); } diff --git a/src/api/java/com/Microsoft/Z3/RealExpr.java b/src/api/java/com/Microsoft/Z3/RealExpr.java index 8f2b139bd..2f06e4643 100644 --- a/src/api/java/com/Microsoft/Z3/RealExpr.java +++ b/src/api/java/com/Microsoft/Z3/RealExpr.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Collections.Generic; */ /* using System.Linq; */ diff --git a/src/api/java/com/Microsoft/Z3/RealSort.java b/src/api/java/com/Microsoft/Z3/RealSort.java index 39aa849ab..d85aeccd1 100644 --- a/src/api/java/com/Microsoft/Z3/RealSort.java +++ b/src/api/java/com/Microsoft/Z3/RealSort.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ diff --git a/src/api/java/com/Microsoft/Z3/RelationSort.java b/src/api/java/com/Microsoft/Z3/RelationSort.java index 3948e1651..85f083b57 100644 --- a/src/api/java/com/Microsoft/Z3/RelationSort.java +++ b/src/api/java/com/Microsoft/Z3/RelationSort.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -18,7 +19,7 @@ import java.lang.Exception; /** * 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. @@ -30,10 +31,10 @@ import java.lang.Exception; if (m_columnSorts != null) return m_columnSorts; - long n = Arity; + int n = Arity; Sort[] res = new Sort[n]; - for (long i; i < n; i++) - res[i] = Sort.Create(Context, Native.getRelationColumn(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = Sort.Create(Context(), Native.getRelationColumn(Context().nCtx(), NativeObject(), i)); return res; } diff --git a/src/api/java/com/Microsoft/Z3/SetSort.java b/src/api/java/com/Microsoft/Z3/SetSort.java index 2f008f4db..2ed16c09b 100644 --- a/src/api/java/com/Microsoft/Z3/SetSort.java +++ b/src/api/java/com/Microsoft/Z3/SetSort.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -20,7 +21,7 @@ import java.lang.Exception; } SetSort(Context ctx, Sort ty) - { super(ctx, Native.mkSetSort(ctx.nCtx(), ty.NativeObject)); + { super(ctx, Native.mkSetSort(ctx.nCtx(), ty.NativeObject())); } diff --git a/src/api/java/com/Microsoft/Z3/Solver.java b/src/api/java/com/Microsoft/Z3/Solver.java index a206114f1..5fda96bb1 100644 --- a/src/api/java/com/Microsoft/Z3/Solver.java +++ b/src/api/java/com/Microsoft/Z3/Solver.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -32,14 +33,14 @@ import java.lang.Exception; { - Context.CheckContextMatch(value); - Native.solverSetParams(Context().nCtx(), NativeObject(), value.NativeObject); + Context().CheckContextMatch(value); + Native.solverSetParams(Context().nCtx(), NativeObject(), value.NativeObject()); } /** * 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; * * **/ - public long NumScopes() { return Native.solverGetNumScopes(Context().nCtx(), NativeObject()); } + public int NumScopes() { return Native.solverGetNumScopes(Context().nCtx(), NativeObject()); } /** * Creates a backtracking point. @@ -63,7 +64,7 @@ import java.lang.Exception; * Note that an exception is thrown if is not smaller than NumScopes * **/ - public void Pop(long n) + public void Pop(int n) { Native.solverPop(Context().nCtx(), NativeObject(), n); } @@ -85,19 +86,19 @@ import java.lang.Exception; - Context.CheckContextMatch(constraints); - for (Iterator a = constraints.iterator(); a.hasNext(); ) + Context().CheckContextMatch(constraints); + 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. **/ - 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; } @@ -108,11 +109,11 @@ import java.lang.Exception; { - ASTVector ass = new ASTVector(Context, Native.solverGetAssertions(Context().nCtx(), NativeObject())); - long n = ass.Size; + ASTVector ass = new ASTVector(Context(), Native.solverGetAssertions(Context().nCtx(), NativeObject())); + int n = ass.Size; BoolExpr[] res = new BoolExpr[n]; - for (long i; i < n; i++) - res[i] = new BoolExpr(Context, ass[i].NativeObject); + for (int i = 0; i < n; i++) + res[i] = new BoolExpr(Context(), ass[i].NativeObject()); return res; } @@ -128,13 +129,13 @@ import java.lang.Exception; { Z3_lbool r; if (assumptions == null) - r = (Z3_lbool)Native.solverCheck(Context().nCtx(), NativeObject()); + r = Z3_lbool.fromInt(Native.solverCheck(Context().nCtx(), NativeObject())); 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) { - case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE; - case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE; + case Z3_L_TRUE: return Status.SATISFIABLE; + case Z3_L_FALSE: return Status.UNSATISFIABLE; default: return Status.UNKNOWN; } } @@ -152,7 +153,7 @@ import java.lang.Exception; if (x == 0) return null; else - return new Model(Context, x); + return new Model(Context(), x); } /** @@ -168,7 +169,7 @@ import java.lang.Exception; if (x == 0) return null; 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())); - long n = core.Size; + ASTVector core = new ASTVector(Context(), Native.solverGetUnsatCore(Context().nCtx(), NativeObject())); + int n = core.Size; Expr[] res = new Expr[n]; - for (long i; i < n; i++) - res[i] = Expr.Create(Context, core[i].NativeObject); + for (int i = 0; i < n; i++) + res[i] = Expr.Create(Context(), core[i].NativeObject()); 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) { - Context.Solver_DRQ.IncAndClear(Context, o); + Context().Solver_DRQ().IncAndClear(Context(), o); super.IncRef(o); } void DecRef(long o) { - Context.Solver_DRQ.Add(o); + Context().Solver_DRQ().Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/Sort.java b/src/api/java/com/Microsoft/Z3/Sort.java index d328071dd..f1933fccd 100644 --- a/src/api/java/com/Microsoft/Z3/Sort.java +++ b/src/api/java/com/Microsoft/Z3/Sort.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -57,12 +58,12 @@ import java.lang.Exception; /** * 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. **/ - 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 @@ -70,7 +71,7 @@ import java.lang.Exception; 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) { - 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"); 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_sort_kind.Z3_BOOL_SORT: return new BoolSort(ctx, obj); - case Z3_sort_kind.Z3_BV_SORT: return new BitVecSort(ctx, obj); - case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeSort(ctx, obj); - case Z3_sort_kind.Z3_INT_SORT: return new IntSort(ctx, obj); - case Z3_sort_kind.Z3_REAL_SORT: return new RealSort(ctx, obj); - case Z3_sort_kind.Z3_UNINTERPRETED_SORT: return new UninterpretedSort(ctx, obj); - case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainSort(ctx, obj); - case Z3_sort_kind.Z3_RELATION_SORT: return new RelationSort(ctx, obj); + case Z3_ARRAY_SORT: return new ArraySort(ctx, obj); + case Z3_BOOL_SORT: return new BoolSort(ctx, obj); + case Z3_BV_SORT: return new BitVecSort(ctx, obj); + case Z3_DATATYPE_SORT: return new DatatypeSort(ctx, obj); + case Z3_INT_SORT: return new IntSort(ctx, obj); + case Z3_REAL_SORT: return new RealSort(ctx, obj); + case Z3_UNINTERPRETED_SORT: return new UninterpretedSort(ctx, obj); + case Z3_FINITE_DOMAIN_SORT: return new FiniteDomainSort(ctx, obj); + case Z3_RELATION_SORT: return new RelationSort(ctx, obj); default: throw new Z3Exception("Unknown sort kind"); } diff --git a/src/api/java/com/Microsoft/Z3/Statistics.java b/src/api/java/com/Microsoft/Z3/Statistics.java index d0f4021ed..ec64ee0b3 100644 --- a/src/api/java/com/Microsoft/Z3/Statistics.java +++ b/src/api/java/com/Microsoft/Z3/Statistics.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -27,7 +28,7 @@ import java.lang.Exception; /** * The uint-value of the entry. **/ - public long UIntValue() { return m_long; } + public int UIntValue() { return m_int; } /** * The double-value of the entry. **/ @@ -35,7 +36,7 @@ import java.lang.Exception; /** * 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. **/ @@ -49,9 +50,9 @@ import java.lang.Exception; if (IsUInt) - return m_long.ToString(); + return m_int.toString(); else if (IsDouble) - return m_double.ToString(); + return m_double.toString(); else throw new Z3Exception("Unknown statistical entry type"); } @@ -64,15 +65,15 @@ import java.lang.Exception; return Key + ": " + Value; } - private boolean m_is_long = false; + private boolean m_is_int = false; private boolean m_is_double = false; - private long m_long = 0; + private int m_int = 0; private double m_double = 0.0; - Entry(String k, long v) + Entry(String k, int v) { Key = k; - m_is_long = true; - m_long = v; + m_is_int = true; + m_int = v; } Entry(String k, double v) { @@ -93,7 +94,7 @@ import java.lang.Exception; /** * 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. @@ -104,15 +105,15 @@ import java.lang.Exception; - long n = Size; + int n = Size; Entry[] res = new Entry[n]; - for (long i; i < n; i++) + for (int i = 0; i < n; i++) { Entry e; String k = Native.statsGetKey(Context().nCtx(), NativeObject(), i); - if (Native.statsIsLong(Context().nCtx(), NativeObject(), i) != 0) - e = new Entry(k, Native.statsGetLongValue(Context().nCtx(), NativeObject(), i)); - else if (Native.statsIsDouble(Context().nCtx(), NativeObject(), i) != 0) + if (Native.statsIsInt(Context().nCtx(), NativeObject(), i) ) + e = new Entry(k, Native.statsGetIntValue(Context().nCtx(), NativeObject(), i)); + else if (Native.statsIsDouble(Context().nCtx(), NativeObject(), i) ) e = new Entry(k, Native.statsGetDoubleValue(Context().nCtx(), NativeObject(), i)); else 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]; - for (long i; i < n; i++) + for (int i = 0; i < n; i++) res[i] = Native.statsGetKey(Context().nCtx(), NativeObject(), i); return res; } @@ -141,9 +142,9 @@ import java.lang.Exception; **/ public Entry get(String key) { - long n = Size; + int n = Size; Entry[] es = Entries; - for (long i; i < n; i++) + for (int i = 0; i < n; i++) if (es[i].Key == key) return es[i]; return null; @@ -169,13 +170,13 @@ import java.lang.Exception; void IncRef(long o) { - Context.Statistics_DRQ.IncAndClear(Context, o); + Context().Statistics_DRQ().IncAndClear(Context(), o); super.IncRef(o); } void DecRef(long o) { - Context.Statistics_DRQ.Add(o); + Context().Statistics_DRQ().Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/Status.java b/src/api/java/com/Microsoft/Z3/Status.java index 9eb75060c..64bd9f767 100644 --- a/src/api/java/com/Microsoft/Z3/Status.java +++ b/src/api/java/com/Microsoft/Z3/Status.java @@ -7,27 +7,28 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /** * Status values. **/ - public enum Status + public class Status { /// /// Used to signify an unsatisfiable status. /// - UNSATISFIABLE (1), +public static final int UNSATISFIABLE = 1; /// /// Used to signify an unknown status. /// - UNKNOWN (0), +public static final int UNKNOWN = 0; /// /// Used to signify a satisfiable status. /// - SATISFIABLE (1) +public static final int SATISFIABLE = 1; } diff --git a/src/api/java/com/Microsoft/Z3/StringSymbol.java b/src/api/java/com/Microsoft/Z3/StringSymbol.java index 27157599d..1ff869002 100644 --- a/src/api/java/com/Microsoft/Z3/StringSymbol.java +++ b/src/api/java/com/Microsoft/Z3/StringSymbol.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Runtime.InteropServices; */ diff --git a/src/api/java/com/Microsoft/Z3/Symbol.java b/src/api/java/com/Microsoft/Z3/Symbol.java index 54caf9f1c..b7653414d 100644 --- a/src/api/java/com/Microsoft/Z3/Symbol.java +++ b/src/api/java/com/Microsoft/Z3/Symbol.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ /* using System.Runtime.InteropServices; */ @@ -19,7 +20,7 @@ import java.lang.Exception; /** * 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 @@ -43,7 +44,7 @@ import java.lang.Exception; public String toString() { if (IsIntSymbol()) - return ((IntSymbol)this).Int.ToString(); + return ((IntSymbol)this).Int.toString(); else if (IsStringSymbol()) return ((StringSymbol)this).String; 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_symbol_kind.Z3_STRING_SYMBOL: return new StringSymbol(ctx, obj); + case Z3_INT_SYMBOL: return new IntSymbol(ctx, obj); + case Z3_STRING_SYMBOL: return new StringSymbol(ctx, obj); default: throw new Z3Exception("Unknown symbol kind encountered"); } diff --git a/src/api/java/com/Microsoft/Z3/Tactic.java b/src/api/java/com/Microsoft/Z3/Tactic.java index 275205be5..fd560847a 100644 --- a/src/api/java/com/Microsoft/Z3/Tactic.java +++ b/src/api/java/com/Microsoft/Z3/Tactic.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -32,7 +33,7 @@ import java.lang.Exception; /** * 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) - return new ApplyResult(Context, Native.tacticApply(Context().nCtx(), NativeObject(), g.NativeObject)); + return new ApplyResult(Context(), Native.tacticApply(Context().nCtx(), NativeObject(), g.NativeObject())); else { - Context.CheckContextMatch(p); - return new ApplyResult(Context, Native.tacticApplyEx(Context().nCtx(), NativeObject(), g.NativeObject, p.NativeObject)); + Context().CheckContextMatch(p); + 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) @@ -99,13 +100,13 @@ import java.lang.Exception; void IncRef(long o) { - Context.Tactic_DRQ.IncAndClear(Context, o); + Context().Tactic_DRQ().IncAndClear(Context(), o); super.IncRef(o); } void DecRef(long o) { - Context.Tactic_DRQ.Add(o); + Context().Tactic_DRQ().Add(o); super.DecRef(o); } } diff --git a/src/api/java/com/Microsoft/Z3/TupleSort.java b/src/api/java/com/Microsoft/Z3/TupleSort.java index 2e682343a..0ac03bb88 100644 --- a/src/api/java/com/Microsoft/Z3/TupleSort.java +++ b/src/api/java/com/Microsoft/Z3/TupleSort.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* 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. **/ - public long NumFields() { return Native.getTupleSortNumFields(Context().nCtx(), NativeObject()); } + public int NumFields() { return Native.getTupleSortNumFields(Context().nCtx(), NativeObject()); } /** * The field declarations. @@ -37,20 +38,20 @@ import java.lang.Exception; { - long n = NumFields; + int n = NumFields(); FuncDecl[] res = new FuncDecl[n]; - for (long i; i < n; i++) - res[i] = new FuncDecl(Context, Native.getTupleSortFieldDecl(Context().nCtx(), NativeObject(), i)); + for (int i = 0; i < n; i++) + res[i] = new FuncDecl(Context(), Native.getTupleSortFieldDecl(Context().nCtx(), NativeObject(), i)); 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); 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), t, new long[numFields]); } diff --git a/src/api/java/com/Microsoft/Z3/UninterpretedSort.java b/src/api/java/com/Microsoft/Z3/UninterpretedSort.java index f8b91103c..3c732901d 100644 --- a/src/api/java/com/Microsoft/Z3/UninterpretedSort.java +++ b/src/api/java/com/Microsoft/Z3/UninterpretedSort.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -20,7 +21,7 @@ import java.lang.Exception; } UninterpretedSort(Context ctx, Symbol s) - { super(ctx, Native.mkUninterpretedSort(ctx.nCtx(), s.NativeObject)); + { super(ctx, Native.mkUninterpretedSort(ctx.nCtx(), s.NativeObject())); } diff --git a/src/api/java/com/Microsoft/Z3/Version.java b/src/api/java/com/Microsoft/Z3/Version.java index ecf451e2f..c3fc4268d 100644 --- a/src/api/java/com/Microsoft/Z3/Version.java +++ b/src/api/java/com/Microsoft/Z3/Version.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -21,9 +22,9 @@ import java.lang.Exception; /** * 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); return major; } @@ -31,9 +32,9 @@ import java.lang.Exception; /** * 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); return minor; } @@ -41,9 +42,9 @@ import java.lang.Exception; /** * 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); return build; } @@ -51,9 +52,9 @@ import java.lang.Exception; /** * 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); 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); - return major.ToString() + "." + minor.ToString() + "." + build.ToString() + "." + revision.ToString(); + return major.toString() + "." + minor.toString() + "." + build.toString() + "." + revision.toString(); } } diff --git a/src/api/java/com/Microsoft/Z3/Z3Exception.java b/src/api/java/com/Microsoft/Z3/Z3Exception.java index 0bca047ab..7036558c7 100644 --- a/src/api/java/com/Microsoft/Z3/Z3Exception.java +++ b/src/api/java/com/Microsoft/Z3/Z3Exception.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ diff --git a/src/api/java/com/Microsoft/Z3/Z3Object.java b/src/api/java/com/Microsoft/Z3/Z3Object.java index 6a8392a86..d4bdf08f7 100644 --- a/src/api/java/com/Microsoft/Z3/Z3Object.java +++ b/src/api/java/com/Microsoft/Z3/Z3Object.java @@ -7,6 +7,7 @@ package com.Microsoft.Z3; import java.math.BigInteger; import java.util.*; import java.lang.Exception; +import com.Microsoft.Z3.Enumerations.*; /* using System; */ @@ -105,14 +106,14 @@ import java.lang.Exception; if (a == null) return null; - long[] an = new long[a.Length]; - for (long i; i < a.Length; i++) + long[] an = new long[a.length]; + for (int i = 0; i < a.length; i++) if (a[i] != null) an[i] = a[i].NativeObject(); 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; } } diff --git a/src/api/java/mk_java.py b/src/api/java/mk_java.py index 81b4a08b6..fe7f50a25 100644 --- a/src/api/java/mk_java.py +++ b/src/api/java/mk_java.py @@ -11,14 +11,29 @@ CS="../dotnet/" EXT=".cs" EXCLUDE=["Enumerations.cs", "Native.cs", "AssemblyInfo.cs"] OUTDIR="com/Microsoft/Z3/" +ENUMS_FILE = "Enumerations.cs" import os import fileinput import string 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(): - 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 fn in files: if not fn in EXCLUDE and fn.endswith(EXT): @@ -31,14 +46,14 @@ def subst_getters(s, getters): def type_replace(s): 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("string", "String") s = s.replace("IntPtr", "long") s = s.replace("Dictionary<", "Map<") s = s.replace("UInt64", "long") s = s.replace("Int64", "long") - s = s.replace("List", "List") + s = s.replace("List", "LinkedList") s = s.replace("System.Exception", "Exception") return s @@ -55,12 +70,54 @@ def rename_native(s): s = c0 + c1 + c2 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[A-Z0-9_]*)", e + ".\g.toInt()", line) + elif line.find("==") != -1 or line.find("!=") != -1: + line = re.sub(e + "\.(?P[A-Z0-9_]*)", e + ".\g", line) + else: + # line = re.sub("\(\(" + e + "\)(?P.*\(.*)\)", "(" + e + ".values()[\g])", line) + line = re.sub("\(" + e + "\)(?P.*\(.*\))", e + ".fromInt(\g)", line) + return line + def replace_generals(a): a = re.sub(" NativeObject", " NativeObject()", a) - a = re.sub(".NativeObject;", ".NativeObject();", a) - a = re.sub("Context.nCtx", "Context().nCtx()", a) - a = re.sub("ctx.nCtx", "ctx.nCtx()", a) + a = re.sub("\.NativeObject", ".NativeObject()", a) + a = re.sub("(?P[\.\(])Id", "\gId()", 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[^_]*)_DRQ", "Context().\g_DRQ()", a) a = re.sub("ASTKind", "ASTKind()", a) + a = re.sub("IsExpr(?P[ ;])", "IsExpr()\g", a) + a = re.sub("IsNumeral(?P[ ;])", "IsNumeral()\g", a) + a = re.sub("IsInt(?P[ ;])", "IsInt()\g", a) + a = re.sub("IsReal(?P[ ;])", "IsReal()\g", a) + a = re.sub("IsVar(?P[ ;\)])", "IsVar()\g", a) + a = re.sub("FuncDecl.DeclKind", "FuncDecl().DeclKind()", a) + a = re.sub("FuncDecl.DomainSize", "FuncDecl().DomainSize()", a) + a = re.sub("(?P[=&]) Num(?P[a-zA-Z]*)", "\g Num\g()", a) + a = re.sub("= Denominator", "= Denominator()", a) + a = re.sub(", BoolSort(?P[\)\.])", ", BoolSort()\g", a) + a = re.sub(", RealSort(?P[\)\.])", ", RealSort()\g", a) + a = re.sub(", IntSort(?P[\)\.])", ", IntSort()\g", 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 def translate(filename): @@ -82,6 +139,8 @@ def translate(filename): in_getter_set = 0 had_ulong_res = 0 in_enum = 0 + missing_foreach_brace = 0 + foreach_opened_brace = 0 for line in fileinput.input(os.path.join(CS, filename)): s = string.rstrip(string.lstrip(line)) if in_javadoc: @@ -104,6 +163,13 @@ def translate(filename): tgt.write(t + " **/\n") in_javadoc = 0 + for i in range(0, len(EXCLUDE_METHODS)): + if filename == EXCLUDE_METHODS[i][0] and s.startswith(EXCLUDE_METHODS[i][1]): + tgt.write(t + "/* Not translated because it would translate to a function with clashing types. */\n") + in_unsupported = 1 + break + + if in_unsupported: if s == "}": in_unsupported = 0 @@ -119,6 +185,7 @@ def translate(filename): tgt.write("import java.math.BigInteger;\n") tgt.write("import java.util.*;\n") tgt.write("import java.lang.Exception;\n") + tgt.write("import com.Microsoft.Z3.Enumerations.*;\n") elif in_header == 1: # tgt.write(" * " + line.replace(filename, tgtfn)) pass @@ -134,14 +201,15 @@ def translate(filename): tgt.write(t + "/* Overloaded operators are not translated. */\n") in_unsupported = 1 elif s.startswith("public enum"): - tgt.write(line) + tgt.write(line.replace("enum", "class")) in_enum = 1 elif in_enum == 1: if s == "}": tgt.write(line) in_enum = 0 else: - tgt.write(re.sub("(?P.*)\W*=\W*(?P[^\n,])", "\g (\g)", line)) + line = re.sub("(?P.*)\W*=\W*(?P[^\n,])", "public static final int \g = \g;", line) + tgt.write(line.replace(",","")) elif s.startswith("public class") or s.startswith("internal class") or s.startswith("internal abstract class"): a = line.replace(":", "extends").replace("internal ", "") a = a.replace(", IComparable", "") @@ -164,7 +232,7 @@ def translate(filename): s = s.replace("internal virtual", "") s = s.replace("internal", "") tokens = s.split(" ") - print "TOKENS: " + str(len(tokens)) + # print "TOKENS: " + str(len(tokens)) if len(tokens) == 3: in_getter = tokens[2] in_getter_type = type_replace((tokens[0] + " " + tokens[1])) @@ -204,6 +272,7 @@ def translate(filename): rest = type_replace(rest) rest = rename_native(rest) rest = replace_generals(rest) + rest = enum_replace(rest) t = "" for i in range(0, lastindent): t += " " @@ -225,6 +294,7 @@ def translate(filename): subst_getters(rest, getters) rest = rename_native(rest) rest = replace_generals(rest) + rest = enum_replace(rest) if in_bracket_op: tgt.write(d + rest) else: @@ -240,6 +310,7 @@ def translate(filename): rest = type_replace(rest) rest = rename_native(rest) rest = replace_generals(rest) + rest = enum_replace(rest) if in_bracket_op: tgt.write(t + in_getter_type + " " + in_getter + " " + rest + "\n") else: @@ -257,6 +328,7 @@ def translate(filename): rest = type_replace(rest) rest = rename_native(rest) rest = replace_generals(rest) + rest = enum_replace(rest) ac_acc = in_getter_type[:in_getter_type.find(' ')] ac_type = in_getter_type[in_getter_type.find(' ')+1:] if in_bracket_op: @@ -301,19 +373,43 @@ def translate(filename): else: for i in range(0, mbraces): 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[,;\)])", "\g", line) a = type_replace(line) + a = enum_replace(a) a = re.sub("(?P[\(, ])params ", "\g", a) a = a.replace("base.", "super.") a = re.sub("Contract.\w+\([\s\S]*\);", "", a) a = rename_native(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[\w <>,]+)\s+(?P\w+)\s+in\s+(?P\w+)\)", + # "{ Iterator fe_i = \g.iterator(); while (fe_i.hasNext()) { \g \g = (long)fe_i.next(); ", +# a) a = re.sub("foreach\s*\((?P[\w <>,]+)\s+(?P\w+)\s+in\s+(?P\w+)\)", - "for (Iterator \g = \g.iterator(); \g.hasNext(); )", a) + "for (\g \g: \g)", + a) + if a.find("long o: m_queue") != -1: + a = a.replace("long", "Long") a = a.replace("readonly ", "") a = a.replace("const ", "final ") a = a.replace("String ToString", "String toString") + a = a.replace(".ToString", ".toString") a = a.replace("internal ", "") a = a.replace("new static", "static") a = a.replace("new public", "public") @@ -333,6 +429,13 @@ def translate(filename): a = a.replace("out res", "res") a = a.replace("GC.ReRegisterForFinalize(m_ctx);", "") 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: a = a.replace("ulong res = 0;", "LongPtr res = new LongPtr();") elif had_ulong_res == 1: @@ -348,7 +451,6 @@ def translate(filename): a = re.sub("NativeObject = (?P.*);", "setNativeObject(\g);", a) a = replace_generals(a) tgt.write(a) - tgt.close() mk_java_bindings()