diff --git a/src/api/java/com/Microsoft/Z3/AST.java b/src/api/java/com/Microsoft/Z3/AST.java index ad4c9d94a..c8471e2e8 100644 --- a/src/api/java/com/Microsoft/Z3/AST.java +++ b/src/api/java/com/Microsoft/Z3/AST.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /* using System.Collections; */ /* using System.Collections.Generic; */ @@ -34,7 +38,7 @@ package com.Microsoft.Z3; /** * Object comparison. **/ - public boolean Equals(object o) + public boolean Equals(Object o) { AST casted = (AST) o; if (casted == null) return false; @@ -46,7 +50,7 @@ package com.Microsoft.Z3; * Another AST * @return Negative if the object should be sorted before , positive if after else zero. **/ - public int CompareTo(object other) + public int CompareTo(Object other) { if (other == null) return 1; AST oAST = (AST) other; @@ -69,13 +73,13 @@ package com.Microsoft.Z3; **/ public int GetHashCode() { - return (int)Native.getAstHash(Context.nCtx, NativeObject); + return (int)Native.getAstHash(Context().nCtx(), NativeObject()); } /** * A unique identifier for the AST (unique among all ASTs). **/ - public long Id() { return Native.getAstId(Context.nCtx, NativeObject); } + public long Id() { return Native.getAstId(Context().nCtx(), NativeObject()); } /** * Translates (copies) the AST to the Context . @@ -90,20 +94,20 @@ package com.Microsoft.Z3; if (ReferenceEquals(Context, ctx)) return this; else - return new AST(ctx, Native.translate(Context.nCtx, NativeObject, ctx.nCtx)); + return new AST(ctx, Native.translate(Context().nCtx(), NativeObject(), ctx.nCtx())); } /** * 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)Native.getAstKind(Context().nCtx(), NativeObject()); } /** * Indicates whether the AST is an Expr **/ public boolean IsExpr() { - switch (ASTKind) + switch (ASTKind()) { case Z3_ast_kind.Z3_APP_AST: case Z3_ast_kind.Z3_NUMERAL_AST: @@ -116,29 +120,29 @@ package com.Microsoft.Z3; /** * Indicates whether the AST is a BoundVariable **/ - public boolean IsVar() { return this.ASTKind == Z3_ast_kind.Z3_VAR_AST; } + public boolean IsVar() { return this.ASTKind() == Z3_ast_kind.Z3_VAR_AST; } /** * Indicates whether the AST is a Quantifier **/ - public boolean IsQuantifier() { return this.ASTKind == Z3_ast_kind.Z3_QUANTIFIER_AST; } + public boolean IsQuantifier() { return this.ASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST; } /** * Indicates whether the AST is a Sort **/ - public boolean IsSort() { return this.ASTKind == Z3_ast_kind.Z3_SORT_AST; } + public boolean IsSort() { return this.ASTKind() == Z3_ast_kind.Z3_SORT_AST; } /** * Indicates whether the AST is a FunctionDeclaration **/ - public boolean IsFuncDecl() { return this.ASTKind == Z3_ast_kind.Z3_FUNC_DECL_AST; } + public boolean IsFuncDecl() { return this.ASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST; } /** * A string representation of the AST. **/ public String toString() { - return Native.asttoString(Context.nCtx, NativeObject); + return Native.astToString(Context().nCtx(), NativeObject()); } /** @@ -148,53 +152,53 @@ package com.Microsoft.Z3; { - return Native.asttoString(Context.nCtx, NativeObject); + return Native.astToString(Context().nCtx(), NativeObject()); } - AST(Context ctx) { super(ctx); } - AST(Context ctx, IntPtr obj) { super(ctx, obj); } + AST(Context ctx) { super(ctx); { }} + AST(Context ctx, long obj) { super(ctx, obj); { }} - class DecRefQueue extends Z3.DecRefQueue + class DecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, IntPtr obj) + public void IncRef(Context ctx, long obj) { - Native.incRef(ctx.nCtx, obj); + Native.incRef(ctx.nCtx(), obj); } - public void DecRef(Context ctx, IntPtr obj) + public void DecRef(Context ctx, long obj) { - Native.decRef(ctx.nCtx, obj); + Native.decRef(ctx.nCtx(), obj); } }; - void IncRef(IntPtr o) + void IncRef(long o) { // Console.WriteLine("AST IncRef()"); if (Context == null) throw new Z3Exception("inc() called on null context"); - if (o == IntPtr.Zero) + if (o == 0) throw new Z3Exception("inc() called on null AST"); Context.AST_DRQ.IncAndClear(Context, o); super.IncRef(o); } - void DecRef(IntPtr o) + void DecRef(long o) { // Console.WriteLine("AST DecRef()"); if (Context == null) throw new Z3Exception("dec() called on null context"); - if (o == IntPtr.Zero) + if (o == 0) throw new Z3Exception("dec() called on null AST"); Context.AST_DRQ.Add(o); super.DecRef(o); } - static AST Create(Context ctx, IntPtr obj) + static AST Create(Context ctx, long obj) { - switch ((Z3_ast_kind)Native.getAstKind(ctx.nCtx, obj)) + switch ((Z3_ast_kind)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); diff --git a/src/api/java/com/Microsoft/Z3/ASTMap.java b/src/api/java/com/Microsoft/Z3/ASTMap.java index 7b95861b4..837779234 100644 --- a/src/api/java/com/Microsoft/Z3/ASTMap.java +++ b/src/api/java/com/Microsoft/Z3/ASTMap.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -20,7 +24,7 @@ package com.Microsoft.Z3; { - return Native.astMapContains(Context.nCtx, NativeObject, k.NativeObject) != 0; + return Native.astMapContains(Context().nCtx(), NativeObject(), k.NativeObject) != 0; } /** @@ -35,7 +39,7 @@ package com.Microsoft.Z3; - return new AST(Context, Native.astMapFind(Context.nCtx, NativeObject, k.NativeObject)); + return new AST(Context, Native.astMapFind(Context().nCtx(), NativeObject(), k.NativeObject)); } /** @@ -48,7 +52,7 @@ package com.Microsoft.Z3; - Native.astMapInsert(Context.nCtx, NativeObject, k.NativeObject, v.NativeObject); + Native.astMapInsert(Context().nCtx(), NativeObject(), k.NativeObject, v.NativeObject); } /** @@ -59,7 +63,7 @@ package com.Microsoft.Z3; { - Native.astMapErase(Context.nCtx, NativeObject, k.NativeObject); + Native.astMapErase(Context().nCtx(), NativeObject(), k.NativeObject); } /** @@ -67,20 +71,20 @@ package com.Microsoft.Z3; **/ public void Reset() { - Native.astMapReset(Context.nCtx, NativeObject); + Native.astMapReset(Context().nCtx(), NativeObject()); } /** * The size of the map **/ - public long Size() { return Native.astMapSize(Context.nCtx, NativeObject); } + public long 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())); } /** @@ -88,38 +92,38 @@ package com.Microsoft.Z3; **/ public String toString() { - return Native.astMaptoString(Context.nCtx, NativeObject); + return Native.astMapToString(Context().nCtx(), NativeObject()); } - ASTMap(Context ctx, IntPtr obj) - { super(ctx, obj); + ASTMap(Context ctx, long obj) + { super(ctx, obj); } ASTMap(Context ctx) - { super(ctx, Native.mkAstMap(ctx.nCtx)); + { super(ctx, Native.mkAstMap(ctx.nCtx())); } - class DecRefQueue extends Z3.DecRefQueue + class DecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, IntPtr obj) + public void IncRef(Context ctx, long obj) { - Native.astMapIncRef(ctx.nCtx, obj); + Native.astMapIncRef(ctx.nCtx(), obj); } - public void DecRef(Context ctx, IntPtr obj) + public void DecRef(Context ctx, long obj) { - Native.astMapDecRef(ctx.nCtx, obj); + Native.astMapDecRef(ctx.nCtx(), obj); } }; - void IncRef(IntPtr o) + void IncRef(long o) { Context.ASTMap_DRQ.IncAndClear(Context, o); super.IncRef(o); } - void DecRef(IntPtr o) + void DecRef(long 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 0ae2ff20a..2bb1ab3e0 100644 --- a/src/api/java/com/Microsoft/Z3/ASTVector.java +++ b/src/api/java/com/Microsoft/Z3/ASTVector.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -14,7 +18,7 @@ package com.Microsoft.Z3; /** * The size of the vector **/ - public long Size() { return Native.astVectorSize(Context.nCtx, NativeObject); } + public long Size() { return Native.astVectorSize(Context().nCtx(), NativeObject()); } /** * Retrieves the i-th object in the vector. @@ -26,13 +30,13 @@ package com.Microsoft.Z3; { - 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) { - Native.astVectorSet(Context.nCtx, NativeObject, i, value.NativeObject); + Native.astVectorSet(Context().nCtx(), NativeObject(), i, value.NativeObject); } /** @@ -41,7 +45,7 @@ package com.Microsoft.Z3; **/ public void Resize(long newSize) { - Native.astVectorResize(Context.nCtx, NativeObject, newSize); + Native.astVectorResize(Context().nCtx(), NativeObject(), newSize); } /** @@ -53,7 +57,7 @@ package com.Microsoft.Z3; { - Native.astVectorPush(Context.nCtx, NativeObject, a.NativeObject); + Native.astVectorPush(Context().nCtx(), NativeObject(), a.NativeObject); } /** @@ -66,7 +70,7 @@ package com.Microsoft.Z3; - return new ASTVector(Context, Native.astVectorTranslate(Context.nCtx, NativeObject, ctx.nCtx)); + return new ASTVector(Context, Native.astVectorTranslate(Context().nCtx(), NativeObject(), ctx.nCtx())); } /** @@ -74,32 +78,32 @@ package com.Microsoft.Z3; **/ public String toString() { - return Native.astVectortoString(Context.nCtx, NativeObject); + return Native.astVectorToString(Context().nCtx(), NativeObject()); } - ASTVector(Context ctx, IntPtr obj) { super(ctx, obj); } - ASTVector(Context ctx) { super(ctx, Native.mkAstVector(ctx.nCtx)); } + ASTVector(Context ctx, long obj) { super(ctx, obj); { }} + ASTVector(Context ctx) { super(ctx, Native.mkAstVector(ctx.nCtx())); { }} - class DecRefQueue extends Z3.DecRefQueue + class DecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, IntPtr obj) + public void IncRef(Context ctx, long obj) { - Native.astVectorIncRef(ctx.nCtx, obj); + Native.astVectorIncRef(ctx.nCtx(), obj); } - public void DecRef(Context ctx, IntPtr obj) + public void DecRef(Context ctx, long obj) { - Native.astVectorDecRef(ctx.nCtx, obj); + Native.astVectorDecRef(ctx.nCtx(), obj); } }; - void IncRef(IntPtr o) + void IncRef(long o) { Context.ASTVector_DRQ.IncAndClear(Context, o); super.IncRef(o); } - void DecRef(IntPtr o) + void DecRef(long 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 new file mode 100644 index 000000000..eccd15556 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/AlgebraicNum.java @@ -0,0 +1,62 @@ +/** + * This file was automatically generated from AlgebraicNum.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; +/* using System; */ + +/* using System.Numerics; */ + + /** + * Algebraic numbers + **/ + public class AlgebraicNum extends ArithExpr + { + /** + * Return a upper bound for a given real algebraic number. + * The interval isolating the number is smaller than 1/10^. + * + * the precision of the result + * @return A numeral Expr of sort Real + **/ + public RatNum ToUpper(long precision) + { + + + return new RatNum(Context, Native.getAlgebraicNumberUpper(Context().nCtx(), NativeObject(), precision)); + } + + /** + * Return a lower bound for the given real algebraic number. + * The interval isolating the number is smaller than 1/10^. + * + * + * @return A numeral Expr of sort Real + **/ + public RatNum ToLower(long 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) + { + + + return Native.getNumeralDecimalString(Context().nCtx(), NativeObject(), precision); + } + + AlgebraicNum(Context ctx, long obj) + { super(ctx, obj); + + } + } diff --git a/src/api/java/com/Microsoft/Z3/ApplyResult.java b/src/api/java/com/Microsoft/Z3/ApplyResult.java index 9bd613930..51be63496 100644 --- a/src/api/java/com/Microsoft/Z3/ApplyResult.java +++ b/src/api/java/com/Microsoft/Z3/ApplyResult.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -15,20 +19,20 @@ package com.Microsoft.Z3; /** * The number of Subgoals. **/ - public long NumSubgoals() { return Native.applyResultGetNumSubgoals(Context.nCtx, NativeObject); } + public long NumSubgoals() { return Native.applyResultGetNumSubgoals(Context().nCtx(), NativeObject()); } /** * Retrieves the subgoals from the ApplyResult. **/ public Goal[] Subgoals() { - - + + long n = NumSubgoals; Goal[] res = new Goal[n]; - for (long i = 0; i < n; i++) - res[i] = new Goal(Context, Native.applyResultGetSubgoal(Context.nCtx, NativeObject, i)); + for (long i; i < n; i++) + res[i] = new Goal(Context, Native.applyResultGetSubgoal(Context().nCtx(), NativeObject(), i)); return res; } @@ -42,7 +46,7 @@ package com.Microsoft.Z3; - return new Model(Context, Native.applyResultConvertModel(Context.nCtx, NativeObject, i, m.NativeObject)); + return new Model(Context, Native.applyResultConvertModel(Context().nCtx(), NativeObject(), i, m.NativeObject)); } /** @@ -50,33 +54,34 @@ package com.Microsoft.Z3; **/ public String toString() { - return Native.applyResulttoString(Context.nCtx, NativeObject); + return Native.applyResultToString(Context().nCtx(), NativeObject()); } - ApplyResult(Context ctx, IntPtr obj) { super(ctx, obj); + ApplyResult(Context ctx, long obj) + { super(ctx, obj); } - class DecRefQueue extends Z3.DecRefQueue + class DecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, IntPtr obj) + public void IncRef(Context ctx, long obj) { - Native.applyResultIncRef(ctx.nCtx, obj); + Native.applyResultIncRef(ctx.nCtx(), obj); } - public void DecRef(Context ctx, IntPtr obj) + public void DecRef(Context ctx, long obj) { - Native.applyResultDecRef(ctx.nCtx, obj); + Native.applyResultDecRef(ctx.nCtx(), obj); } - }; + }; - void IncRef(IntPtr o) + void IncRef(long o) { Context.ApplyResult_DRQ.IncAndClear(Context, o); super.IncRef(o); } - void DecRef(IntPtr o) + void DecRef(long 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 new file mode 100644 index 000000000..7920bdded --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/ArithExpr.java @@ -0,0 +1,31 @@ +/** + * This file was automatically generated from ArithExpr.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; +/* using System; */ +/* using System.Collections.Generic; */ +/* using System.Linq; */ +/* using System.Text; */ + + + /** + * Arithmetic expressions (int/real) + **/ + public class ArithExpr extends Expr + { + /** Constructor for ArithExpr + **/ + protected ArithExpr(Context ctx) + { super(ctx); + + } + ArithExpr(Context ctx, long obj) + { super(ctx, obj); + + } + } diff --git a/src/api/java/com/Microsoft/Z3/ArithSort.java b/src/api/java/com/Microsoft/Z3/ArithSort.java new file mode 100644 index 000000000..a6e339e30 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/ArithSort.java @@ -0,0 +1,19 @@ +/** + * This file was automatically generated from ArithSort.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ + + /** + * An arithmetic sort, i.e., Int or Real. + **/ + public class ArithSort extends Sort + { + ArithSort(Context ctx, long obj) { super(ctx, obj); { }} + }; diff --git a/src/api/java/com/Microsoft/Z3/ArrayExpr.java b/src/api/java/com/Microsoft/Z3/ArrayExpr.java new file mode 100644 index 000000000..bc03135aa --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/ArrayExpr.java @@ -0,0 +1,31 @@ +/** + * This file was automatically generated from ArrayExpr.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; +/* using System; */ +/* using System.Collections.Generic; */ +/* using System.Linq; */ +/* using System.Text; */ + + + /** + * Array expressions + **/ + public class ArrayExpr extends Expr + { + /** Constructor for ArrayExpr + **/ + protected ArrayExpr(Context ctx) + { super(ctx); + + } + ArrayExpr(Context ctx, long obj) + { super(ctx, obj); + + } + } diff --git a/src/api/java/com/Microsoft/Z3/ArraySort.java b/src/api/java/com/Microsoft/Z3/ArraySort.java new file mode 100644 index 000000000..cd00df084 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/ArraySort.java @@ -0,0 +1,46 @@ +/** + * This file was automatically generated from ArraySort.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ + + /** + * Array sorts. + **/ + public class ArraySort extends Sort + { + /** + * The domain of the array sort. + **/ + public Sort Domain() + { + + + return Sort.Create(Context, Native.getArraySortDomain(Context().nCtx(), NativeObject())); + } + + /** + * The range of the array sort. + **/ + public Sort Range() + { + + + 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)); + + + + } + }; + diff --git a/src/api/java/com/Microsoft/Z3/BitVecExpr.java b/src/api/java/com/Microsoft/Z3/BitVecExpr.java new file mode 100644 index 000000000..62a03cd06 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/BitVecExpr.java @@ -0,0 +1,31 @@ +/** + * This file was automatically generated from BitVecExpr.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; +/* using System; */ +/* using System.Collections.Generic; */ +/* using System.Linq; */ +/* using System.Text; */ + + + /** + * Bit-vector expressions + **/ + public class BitVecExpr extends Expr + { + + /** + * The size of the sort of a bit-vector term. + **/ + public long SortSize() { return ((BitVecSort)Sort).Size; } + + /** Constructor for BitVecExpr + **/ + protected BitVecExpr(Context ctx) { super(ctx); { }} + BitVecExpr(Context ctx, long obj) { super(ctx, obj); { }} + } diff --git a/src/api/java/com/Microsoft/Z3/BitVecNum.java b/src/api/java/com/Microsoft/Z3/BitVecNum.java new file mode 100644 index 000000000..81389dd4b --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/BitVecNum.java @@ -0,0 +1,80 @@ +/** + * This file was automatically generated from BitVecNum.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; +/* using System; */ + +/* using System.Numerics; */ + + /** + * Bit-vector numerals + **/ + public class BitVecNum extends BitVecExpr + { + /** + * Retrieve the 64-bit unsigned integer value. + **/ + public long UInt64() + { + long res = 0; + if (Native.getNumeralLong64(Context().nCtx(), NativeObject(), res) == 0) + throw new Z3Exception("Numeral is not a 64 bit unsigned"); + return res; + } + + /** + * Retrieve the int value. + **/ + public int Int() + { + int res = 0; + if (Native.getNumeralInt(Context().nCtx(), NativeObject(), res) == 0) + throw new Z3Exception("Numeral is not an int"); + return res; + } + + /** + * Retrieve the 64-bit int value. + **/ + public long Int64() + { + long res = 0; + if (Native.getNumeralInt64(Context().nCtx(), NativeObject(), res) == 0) + throw new Z3Exception("Numeral is not an int64"); + return res; + } + + /** + * Retrieve the int value. + **/ + public long UInt() + { + long res = 0; + if (Native.getNumeralLong(Context().nCtx(), NativeObject(), res) == 0) + throw new Z3Exception("Numeral is not a long"); + return res; + } + + /** + * Retrieve the BigInteger value. + **/ + public BigInteger BigInteger() + { + return BigInteger.Parse(this.ToString()); + } + + /** + * Returns a string representation of the numeral. + **/ + public String toString() + { + return Native.getNumeralString(Context().nCtx(), NativeObject()); + } + + BitVecNum(Context ctx, long obj) { super(ctx, obj); { }} + } diff --git a/src/api/java/com/Microsoft/Z3/BitVecSort.java b/src/api/java/com/Microsoft/Z3/BitVecSort.java new file mode 100644 index 000000000..0ed24573a --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/BitVecSort.java @@ -0,0 +1,25 @@ +/** + * This file was automatically generated from BitVecSort.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ + + /** + * Bit-vector sorts. + **/ + public class BitVecSort extends Sort + { + /** + * The size of the bit-vector sort. + **/ + public long 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 new file mode 100644 index 000000000..65778ba44 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/BoolExpr.java @@ -0,0 +1,27 @@ +/** + * This file was automatically generated from BoolExpr.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; +/* using System; */ +/* using System.Collections.Generic; */ +/* using System.Linq; */ +/* using System.Text; */ + + + /** + * Boolean expressions + **/ + public class BoolExpr extends Expr + { + /** Constructor for BoolExpr + **/ + protected BoolExpr(Context ctx) { super(ctx); { }} + /** Constructor for BoolExpr + **/ + BoolExpr(Context ctx, long obj) { super(ctx, obj); { }} + } diff --git a/src/api/java/com/Microsoft/Z3/BoolSort.java b/src/api/java/com/Microsoft/Z3/BoolSort.java new file mode 100644 index 000000000..9b05607ac --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/BoolSort.java @@ -0,0 +1,20 @@ +/** + * This file was automatically generated from BoolSort.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ + + /** + * A Boolean sort. + **/ + public class BoolSort extends Sort + { + BoolSort(Context ctx, long obj) { super(ctx, obj); { }} + BoolSort(Context ctx) { super(ctx, Native.mkBoolSort(ctx.nCtx())); { }} + }; diff --git a/src/api/java/com/Microsoft/Z3/Constructor.java b/src/api/java/com/Microsoft/Z3/Constructor.java index 7c9b2a85c..caead4737 100644 --- a/src/api/java/com/Microsoft/Z3/Constructor.java +++ b/src/api/java/com/Microsoft/Z3/Constructor.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -55,7 +59,7 @@ package com.Microsoft.Z3; **/ protected void finalize() { - Native.delConstructor(Context.nCtx, NativeObject); + Native.delConstructor(Context().nCtx(), NativeObject()); } @@ -73,7 +77,7 @@ package com.Microsoft.Z3; Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, long[] sortRefs) - { super(ctx); + { super(ctx); @@ -87,7 +91,7 @@ package com.Microsoft.Z3; if (sortRefs == null) sortRefs = new long[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), @@ -102,42 +106,15 @@ package com.Microsoft.Z3; if (m_testerDecl != null) return; - IntPtr constructor = IntPtr.Zero; - IntPtr tester = IntPtr.Zero; - IntPtr[] accessors = new IntPtr[n]; - Native.queryConstructor(Context.nCtx, NativeObject, n, constructor, tester, accessors); + long constructor = 0; + 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_accessorDecls = new FuncDecl[n]; - for (long i = 0; i < n; i++) + for (long i; i < n; i++) m_accessorDecls[i] = new FuncDecl(Context, accessors[i]); } } - - /** - * Lists of constructors - **/ - public class ConstructorList extends Z3Object - { - /** - * Destructor. - **/ - protected void finalize() - { - Native.delConstructorList(Context.nCtx, NativeObject); - } - - ConstructorList(Context ctx, IntPtr obj) - { super(ctx, obj); - - } - - ConstructorList(Context ctx, Constructor[] constructors) - { super(ctx); - - - - NativeObject = Native.mkConstructorList(Context.nCtx, (long)constructors.Length, Constructor.ArrayToNative(constructors)); - } - } diff --git a/src/api/java/com/Microsoft/Z3/ConstructorList.java b/src/api/java/com/Microsoft/Z3/ConstructorList.java new file mode 100644 index 000000000..05b85e664 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/ConstructorList.java @@ -0,0 +1,42 @@ +/** + * This file was automatically generated from ConstructorList.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ +/* using System.Collections.Generic; */ +/* using System.Linq; */ +/* using System.Text; */ + + + /** + * Lists of constructors + **/ + public class ConstructorList extends Z3Object + { + /** + * Destructor. + **/ + protected void finalize() + { + Native.delConstructorList(Context().nCtx(), NativeObject()); + } + + ConstructorList(Context ctx, long obj) + { super(ctx, obj); + + } + + ConstructorList(Context ctx, Constructor[] constructors) + { super(ctx); + + + + setNativeObject(Native.mkConstructorList(Context().nCtx(), (long)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 c18fb7414..69a01cb86 100644 --- a/src/api/java/com/Microsoft/Z3/Context.java +++ b/src/api/java/com/Microsoft/Z3/Context.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /* using System.Collections.Generic; */ /* using System.Runtime.InteropServices; */ @@ -17,20 +21,20 @@ package com.Microsoft.Z3; * Constructor. **/ public Context() - { super(); - m_ctx = Native.mkContextRc(IntPtr.Zero); + { super(); + m_ctx = Native.mkContextRc(0); InitContext(); } /** * Constructor. **/ - public Context(Dictionary settings) - { super(); + public Context(Map settings) + { super(); - IntPtr cfg = Native.mkConfig(); - for (KeyValuePair.Iterator kv = settings.iterator(); kv.hasNext(); ) + long cfg = Native.mkConfig(); + for (Iterator kv = settings.iterator(); kv.hasNext(); ) Native.setParamValue(cfg, kv.Key, kv.Value); m_ctx = Native.mkContextRc(cfg); Native.delConfig(cfg); @@ -73,11 +77,11 @@ package com.Microsoft.Z3; if (names == null) return null; Symbol[] result = new Symbol[names.Length]; - for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]); + for (int i; i < names.Length; ++i) result[i] = MkSymbol(names[i]); return result; } - private BoolSort m_booleanSort = null; + private BoolSort m_boolSort = null; private IntSort m_intSort = null; private RealSort m_realSort = null; @@ -88,7 +92,7 @@ package com.Microsoft.Z3; { - if (m_booleanSort == null) m_booleanSort = new BoolSort(this); return m_booleanSort; + if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort; } /** @@ -253,7 +257,7 @@ package com.Microsoft.Z3; /** * Create a new finite domain sort. **/ - public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size) + public FiniteDomainSort MkFiniteDomainSort(Symbol name, long size) { @@ -265,7 +269,7 @@ package com.Microsoft.Z3; /** * Create a new finite domain sort. **/ - public FiniteDomainSort MkFiniteDomainSort(String name, ulong size) + public FiniteDomainSort MkFiniteDomainSort(String name, long size) { @@ -354,19 +358,19 @@ package com.Microsoft.Z3; CheckContextMatch(names); long n = (long)names.Length; ConstructorList[] cla = new ConstructorList[n]; - IntPtr[] n_constr = new IntPtr[n]; - for (long i = 0; i < n; i++) + long[] n_constr = new long[n]; + for (long i; i < n; i++) { var constructor = c[i]; CheckContextMatch(constructor); cla[i] = new ConstructorList(this, constructor); - n_constr[i] = cla[i].NativeObject; + n_constr[i] = cla[i].NativeObject(); } - IntPtr[] n_res = new IntPtr[n]; + long[] n_res = new long[n]; Native.mkDatatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr); DatatypeSort[] res = new DatatypeSort[n]; - for (long i = 0; i < n; i++) + for (long i; i < n; i++) res[i] = new DatatypeSort(this, n_res[i]); return res; } @@ -534,7 +538,7 @@ package com.Microsoft.Z3; - IntPtr[] termsNative = AST.ArrayToNative(terms); + long[] termsNative = AST.ArrayToNative(terms); return new Pattern(this, Native.mkPattern(nCtx, (long)terms.Length, termsNative)); } @@ -2239,7 +2243,7 @@ package com.Microsoft.Z3; * Sort of the numeral * @return A Term with value and type **/ - public Expr MkNumeral(ulong v, Sort ty) + public Expr MkNumeral(long v, Sort ty) { @@ -2319,7 +2323,7 @@ package com.Microsoft.Z3; * value of the numeral. * @return A Term with value and sort Real **/ - public RatNum MkReal(ulong v) + public RatNum MkReal(long v) { @@ -2378,7 +2382,7 @@ package com.Microsoft.Z3; * value of the numeral. * @return A Term with value and sort Integer **/ - public IntNum MkInt(ulong v) + public IntNum MkInt(long v) { @@ -2438,7 +2442,7 @@ package com.Microsoft.Z3; * value of the numeral. * the size of the bit-vector **/ - public BitVecNum MkBV(ulong v, long size) + public BitVecNum MkBV(long v, long size) { @@ -2668,7 +2672,7 @@ package com.Microsoft.Z3; long n = NumSMTLIBFormulas; BoolExpr[] res = new BoolExpr[n]; - for (long i = 0; i < n; i++) + for (long i; i < n; i++) res[i] = (BoolExpr)Expr.Create(this, Native.getSmtlibFormula(nCtx, i)); return res; } @@ -2687,7 +2691,7 @@ package com.Microsoft.Z3; long n = NumSMTLIBAssumptions; BoolExpr[] res = new BoolExpr[n]; - for (long i = 0; i < n; i++) + for (long i; i < n; i++) res[i] = (BoolExpr)Expr.Create(this, Native.getSmtlibAssumption(nCtx, i)); return res; } @@ -2706,7 +2710,7 @@ package com.Microsoft.Z3; long n = NumSMTLIBDecls; FuncDecl[] res = new FuncDecl[n]; - for (long i = 0; i < n; i++) + for (long i; i < n; i++) res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx, i)); return res; } @@ -2725,7 +2729,7 @@ package com.Microsoft.Z3; long n = NumSMTLIBSorts; Sort[] res = new Sort[n]; - for (long i = 0; i < n; i++) + for (long i; i < n; i++) res[i] = Sort.Create(this, Native.getSmtlibSort(nCtx, i)); return res; } @@ -2810,7 +2814,7 @@ package com.Microsoft.Z3; long n = NumTactics; String[] res = new String[n]; - for (long i = 0; i < n; i++) + for (long i; i < n; i++) res[i] = Native.getTacticName(nCtx, i); return res; } @@ -2851,14 +2855,14 @@ package com.Microsoft.Z3; CheckContextMatch(t2); CheckContextMatch(ts); - IntPtr last = IntPtr.Zero; + long last = 0; if (ts != null && ts.Length > 0) { - last = ts[ts.Length - 1].NativeObject; + 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 != IntPtr.Zero) + if (last != 0) { last = Native.tacticAndThen(nCtx, t2.NativeObject, last); return new Tactic(this, Native.tacticAndThen(nCtx, t1.NativeObject, last)); @@ -3082,7 +3086,7 @@ package com.Microsoft.Z3; long n = NumProbes; String[] res = new String[n]; - for (long i = 0; i < n; i++) + for (long i; i < n; i++) res[i] = Native.getProbeName(nCtx, i); return res; } @@ -3310,7 +3314,7 @@ package com.Microsoft.Z3; * * The native pointer to wrap. **/ - public AST WrapAST(IntPtr nativeObject) + public AST WrapAST(long nativeObject) { return AST.Create(this, nativeObject); @@ -3327,9 +3331,9 @@ package com.Microsoft.Z3; * * The AST to unwrap. **/ - public IntPtr UnwrapAST(AST a) + public long UnwrapAST(AST a) { - return a.NativeObject; + return a.NativeObject(); } /** @@ -3395,20 +3399,20 @@ package com.Microsoft.Z3; **/ public String GetParamValue(String id) { - Native.IntPtr res = new Native.IntPtr(); + long res = 0; int r = Native.getParamValue(nCtx, id, res); - if (r == (int)Z3_lboolean.Z3_L_FALSE) + if (r == (int)Z3_lbool.Z3_L_FALSE) return null; else - return Marshal.PtrtoStringAnsi(res); + return Marshal.PtrToStringAnsi(res); } - IntPtr m_ctx = IntPtr.Zero; + long m_ctx = 0; Native.errorHandler mNErrHandler = null; - IntPtr nCtx () { return m_ctx; } + long nCtx () { return m_ctx; } - void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode) + void NativeErrorHandler(long ctx, Z3_error_code errorCode) { // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors. } @@ -3418,7 +3422,7 @@ package com.Microsoft.Z3; PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT; m_n_err_handler = new Native.errorHandler(NativeErrorHandler); // keep reference so it doesn't get collected. Native.setErrorHandler(m_ctx, m_n_err_handler); - GC.SuppressFinalize(this); + } void CheckContextMatch(Z3Object other) @@ -3435,7 +3439,7 @@ package com.Microsoft.Z3; if (arr != null) { - for (Z3Object.Iterator a = arr.iterator(); a.hasNext(); ) + for (Iterator a = arr.iterator(); a.hasNext(); ) { // It was an assume, now we added the precondition, and we made it into an assert CheckContextMatch(a); @@ -3509,7 +3513,7 @@ package com.Microsoft.Z3; { m_n_err_handler = null; Native.delContext(m_ctx); - m_ctx = IntPtr.Zero; + m_ctx = 0; } else GC.ReRegisterForFinalize(this); @@ -3536,7 +3540,7 @@ package com.Microsoft.Z3; Tactic_DRQ.Clear(this); Fixedpoint_DRQ.Clear(this); - m_booleanSort = null; + m_boolSort = null; m_intSort = null; m_realSort = null; } diff --git a/src/api/java/com/Microsoft/Z3/DatatypeExpr.java b/src/api/java/com/Microsoft/Z3/DatatypeExpr.java new file mode 100644 index 000000000..4b18635cc --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/DatatypeExpr.java @@ -0,0 +1,31 @@ +/** + * This file was automatically generated from DatatypeExpr.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; +/* using System; */ +/* using System.Collections.Generic; */ +/* using System.Linq; */ +/* using System.Text; */ + + + /** + * Datatype expressions + **/ + public class DatatypeExpr extends Expr + { + /** Constructor for DatatypeExpr + **/ + protected DatatypeExpr(Context ctx) + { super(ctx); + + } + DatatypeExpr(Context ctx, long obj) + { super(ctx, obj); + + } + } diff --git a/src/api/java/com/Microsoft/Z3/DatatypeSort.java b/src/api/java/com/Microsoft/Z3/DatatypeSort.java new file mode 100644 index 000000000..c108c3de9 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/DatatypeSort.java @@ -0,0 +1,80 @@ +/** + * This file was automatically generated from DatatypeSort.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ + + /** + * Datatype sorts. + **/ + public class DatatypeSort extends Sort + { + /** + * The number of constructors of the datatype sort. + **/ + public long NumConstructors() { return Native.getDatatypeSortNumConstructors(Context().nCtx(), NativeObject()); } + + /** + * The constructors. + **/ + public FuncDecl[] Constructors() + { + + + long n = NumConstructors; + FuncDecl[] res = new FuncDecl[n]; + for (long i; i < n; i++) + res[i] = new FuncDecl(Context, Native.getDatatypeSortConstructor(Context().nCtx(), NativeObject(), i)); + return res; + } + + /** + * The recognizers. + **/ + public FuncDecl[] Recognizers() + { + + + long n = NumConstructors; + FuncDecl[] res = new FuncDecl[n]; + for (long i; i < n; i++) + res[i] = new FuncDecl(Context, Native.getDatatypeSortRecognizer(Context().nCtx(), NativeObject(), i)); + return res; + } + + /** + * The constructor accessors. + **/ + public FuncDecl[][] Accessors() + { + + + long n = NumConstructors; + FuncDecl[][] res = new FuncDecl[n][]; + for (long i; i < n; i++) + { + FuncDecl fd = new FuncDecl(Context, Native.getDatatypeSortConstructor(Context().nCtx(), NativeObject(), i)); + long 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)); + res[i] = tmp; + } + return res; + } + + 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))); + + + + } + }; diff --git a/src/api/java/com/Microsoft/Z3/EnumSort.java b/src/api/java/com/Microsoft/Z3/EnumSort.java new file mode 100644 index 000000000..77e0ac057 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/EnumSort.java @@ -0,0 +1,82 @@ +/** + * This file was automatically generated from EnumSort.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ + + /** + * Enumeration sorts. + **/ + public class EnumSort extends Sort + { + /** + * The function declarations of the constants in the enumeration. + **/ + public FuncDecl[] ConstDecls() + { + + + return _constdecls; + } + + /** + * The constants in the enumeration. + **/ + public Expr[] Consts() + { + + + return _consts; + } + + /** + * The test predicates for the constants in the enumeration. + **/ + public FuncDecl[] TesterDecls() + { + + + return _testerdecls; + } + + + private void ObjectInvariant() + { + + + + } + + + + private FuncDecl[] _constdecls = null, _testerdecls = null; + private Expr[] _consts = null; + + EnumSort(Context ctx, Symbol name, Symbol[] enumNames) + { super(ctx); + + + + + 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, + Symbol.ArrayToNative(enumNames), n_constdecls, n_testers); + _constdecls = new FuncDecl[n]; + for (long i; i < n; i++) + _constdecls[i] = new FuncDecl(ctx, n_constdecls[i]); + _testerdecls = new FuncDecl[n]; + for (long i; i < n; i++) + _testerdecls[i] = new FuncDecl(ctx, n_testers[i]); + _consts = new Expr[n]; + for (long i; i < n; i++) + _consts[i] = ctx.MkApp(_constdecls[i]); + } + }; diff --git a/src/api/java/com/Microsoft/Z3/Expr.java b/src/api/java/com/Microsoft/Z3/Expr.java index 760fe813d..13aa0bc1c 100644 --- a/src/api/java/com/Microsoft/Z3/Expr.java +++ b/src/api/java/com/Microsoft/Z3/Expr.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -21,9 +25,9 @@ package com.Microsoft.Z3; 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)); } /** @@ -32,19 +36,19 @@ package com.Microsoft.Z3; 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_lboolean BoolValue() { return (Z3_lboolean)Native.getBooleanValue(Context.nCtx, NativeObject); } + public Z3_lbool BoolValue() { return (Z3_lbool)Native.getBoolValue(Context().nCtx(), NativeObject()); } /** * The number of arguments of the expression. **/ - public long NumArgs() { return Native.getAppNumArgs(Context.nCtx, NativeObject); } + public long NumArgs() { return Native.getAppNumArgs(Context().nCtx(), NativeObject()); } /** * The arguments of the expression. @@ -55,8 +59,8 @@ package com.Microsoft.Z3; long n = NumArgs; Expr[] res = new Expr[n]; - for (long i = 0; i < n; i++) - res[i] = Expr.Create(Context, Native.getAppArg(Context.nCtx, NativeObject, i)); + for (long i; i < n; i++) + res[i] = Expr.Create(Context, Native.getAppArg(Context().nCtx(), NativeObject(), i)); return res; } @@ -72,7 +76,7 @@ package com.Microsoft.Z3; Context.CheckContextMatch(args); if (args.Length != NumArgs) throw new Z3Exception("Number of arguments does not match"); - NativeObject = Native.updateTerm(Context.nCtx, NativeObject, (long)args.Length, Expr.ArrayToNative(args)); + setNativeObject(Native.updateTerm(Context().nCtx(), NativeObject(), (long)args.Length, Expr.ArrayToNative(args))); } /** @@ -95,7 +99,7 @@ package com.Microsoft.Z3; 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(), (long)from.Length, Expr.ArrayToNative(from), Expr.ArrayToNative(to))); } /** @@ -124,7 +128,7 @@ package com.Microsoft.Z3; Context.CheckContextMatch(to); - return Expr.Create(Context, Native.substituteVars(Context.nCtx, NativeObject, (long)to.Length, Expr.ArrayToNative(to))); + return Expr.Create(Context, Native.substituteVars(Context().nCtx(), NativeObject(), (long)to.Length, Expr.ArrayToNative(to))); } /** @@ -140,7 +144,7 @@ package com.Microsoft.Z3; if (ReferenceEquals(Context, ctx)) return this; else - return Expr.Create(ctx, Native.translate(Context.nCtx, NativeObject, ctx.nCtx)); + return Expr.Create(ctx, Native.translate(Context().nCtx(), NativeObject(), ctx.nCtx())); } /** @@ -148,19 +152,19 @@ package com.Microsoft.Z3; **/ 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()) != 0; } /** * 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()) != 0; } /** * The Sort of the term. @@ -168,7 +172,7 @@ package com.Microsoft.Z3; public Sort Sort() { - return Sort.Create(Context, Native.getSort(Context.nCtx, NativeObject)); + return Sort.Create(Context, Native.getSort(Context().nCtx(), NativeObject())); } /** @@ -189,7 +193,7 @@ package com.Microsoft.Z3; /** * 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()) != 0; } /** @@ -198,9 +202,9 @@ package com.Microsoft.Z3; public boolean IsBool() { return (IsExpr && - Native.isEqSort(Context.nCtx, - Native.mkBooleanSort(Context.nCtx), - Native.getSort(Context.nCtx, NativeObject)) != 0); + Native.isEqSort(Context().nCtx(), + Native.mkBoolSort(Context().nCtx()), + Native.getSort(Context().nCtx(), NativeObject())) != 0); } /** @@ -263,14 +267,14 @@ package com.Microsoft.Z3; **/ 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()) != 0 && + Native.getSortKind(Context().nCtx(), Native.getSort(Context().nCtx(), NativeObject())) == (long)Z3_sort_kind.Z3_INT_SORT); } /** * 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())) == (long)Z3_sort_kind.Z3_REAL_SORT; } /** * Indicates whether the term is an arithmetic numeral. @@ -357,8 +361,8 @@ package com.Microsoft.Z3; **/ 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()) != 0 && + (Z3_sort_kind)Native.getSortKind(Context().nCtx(), Native.getSort(Context().nCtx(), NativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT); } /** @@ -426,7 +430,7 @@ package com.Microsoft.Z3; /** * 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())) == (long)Z3_sort_kind.Z3_BV_SORT; } /** * Indicates whether the term is a bit-vector numeral @@ -1216,8 +1220,8 @@ package com.Microsoft.Z3; **/ 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()) != 0 && + (Z3_sort_kind)Native.getSortKind(Context().nCtx(), Native.getSort(Context().nCtx(), NativeObject())) == Z3_sort_kind.Z3_RELATION_SORT); } /** @@ -1332,8 +1336,8 @@ package com.Microsoft.Z3; **/ 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()) != 0 && + (Z3_sort_kind)Native.getSortKind(Context().nCtx(), Native.getSort(Context().nCtx(), NativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT); } /** @@ -1367,23 +1371,23 @@ package com.Microsoft.Z3; - return Native.getIndexValue(Context.nCtx, NativeObject); + return Native.getIndexValue(Context().nCtx(), NativeObject()); } /** * Constructor for Expr **/ - protected Expr(Context ctx) { super(ctx); } + protected Expr(Context ctx) { super(ctx); { }} /** * Constructor for Expr **/ - protected Expr(Context ctx, IntPtr obj) { super(ctx, obj); } + protected Expr(Context ctx, long obj) { super(ctx, obj); { }} - void CheckNativeObject(IntPtr obj) + 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) == 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) throw new Z3Exception("Underlying object is not a term"); super.CheckNativeObject(obj); } @@ -1394,27 +1398,27 @@ package com.Microsoft.Z3; - IntPtr 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); } - static Expr Create(Context ctx, IntPtr obj) + static Expr Create(Context ctx, long obj) { - Z3_ast_kind k = (Z3_ast_kind)Native.getAstKind(ctx.nCtx, obj); + Z3_ast_kind k = (Z3_ast_kind)Native.getAstKind(ctx.nCtx(), obj); if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) return new Quantifier(ctx, obj); - IntPtr s = Native.getSort(ctx.nCtx, obj); - Z3_sort_kind sk = (Z3_sort_kind)Native.getSortKind(ctx.nCtx, s); + long s = Native.getSort(ctx.nCtx(), obj); + Z3_sort_kind sk = (Z3_sort_kind)Native.getSortKind(ctx.nCtx(), s); - if (Native.isAlgebraicNumber(ctx.nCtx, obj) != 0) // is this a numeral ast? + if (Native.isAlgebraicNumber(ctx.nCtx(), obj) != 0) // is this a numeral ast? return new AlgebraicNum(ctx, obj); - if (Native.isNumeralAst(ctx.nCtx, obj) != 0) + if (Native.isNumeralAst(ctx.nCtx(), obj) != 0) { switch (sk) { @@ -1437,118 +1441,3 @@ package com.Microsoft.Z3; return new Expr(ctx, obj); } } - - /** - * Boolean expressions - **/ - public class BoolExpr extends Expr - { - /** Constructor for BoolExpr - **/ - protected BoolExpr(Context ctx) { super(ctx); } - /** Constructor for BoolExpr - **/ - BoolExpr(Context ctx, IntPtr obj) { super(ctx, obj); } - } - - /** - * Arithmetic expressions (int/real) - **/ - public class ArithExpr extends Expr - { - /** Constructor for ArithExpr - **/ - protected ArithExpr(Context ctx) - { super(ctx); - - } - ArithExpr(Context ctx, IntPtr obj) - { super(ctx, obj); - - } - } - - /** - * Int expressions - **/ - public class IntExpr extends ArithExpr - { - /** Constructor for IntExpr - **/ - protected IntExpr(Context ctx) - { super(ctx); - - } - IntExpr(Context ctx, IntPtr obj) - { super(ctx, obj); - - } - } - - /** - * Real expressions - **/ - public class RealExpr extends ArithExpr - { - /** Constructor for RealExpr - **/ - protected RealExpr(Context ctx) - { super(ctx); - - } - RealExpr(Context ctx, IntPtr obj) - { super(ctx, obj); - - } - } - - /** - * Bit-vector expressions - **/ - public class BitVecExpr extends Expr - { - - /** - * The size of the sort of a bit-vector term. - **/ - public long SortSize() { return ((BitVecSort)Sort).Size; } - - /** Constructor for BitVecExpr - **/ - protected BitVecExpr(Context ctx) { super(ctx); } - BitVecExpr(Context ctx, IntPtr obj) { super(ctx, obj); } - } - - /** - * Array expressions - **/ - public class ArrayExpr extends Expr - { - /** Constructor for ArrayExpr - **/ - protected ArrayExpr(Context ctx) - { super(ctx); - - } - ArrayExpr(Context ctx, IntPtr obj) - { super(ctx, obj); - - } - } - - /** - * Datatype expressions - **/ - public class DatatypeExpr extends Expr - { - /** Constructor for DatatypeExpr - **/ - protected DatatypeExpr(Context ctx) - { super(ctx); - - } - DatatypeExpr(Context ctx, IntPtr obj) - { super(ctx, obj); - - } - } diff --git a/src/api/java/com/Microsoft/Z3/FiniteDomainSort.java b/src/api/java/com/Microsoft/Z3/FiniteDomainSort.java new file mode 100644 index 000000000..016d0fecc --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/FiniteDomainSort.java @@ -0,0 +1,38 @@ +/** + * This file was automatically generated from FiniteDomainSort.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ + + /** + * Finite domain sorts. + **/ + public class FiniteDomainSort extends Sort + { + /** + * The size of the finite domain sort. + **/ + public long Size() + { + long res = 0; + Native.getFiniteDomainSortSize(Context().nCtx(), NativeObject(), res); + return res; + } + + FiniteDomainSort(Context ctx, long obj) + { super(ctx, obj); + + } + FiniteDomainSort(Context ctx, Symbol name, long 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 77ce576ac..0c38f9679 100644 --- a/src/api/java/com/Microsoft/Z3/Fixedpoint.java +++ b/src/api/java/com/Microsoft/Z3/Fixedpoint.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -18,7 +22,7 @@ package com.Microsoft.Z3; public String Help() { - return Native.fixedpointGetHelp(Context.nCtx, NativeObject); + return Native.fixedpointGetHelp(Context().nCtx(), NativeObject()); } /** @@ -28,13 +32,13 @@ package com.Microsoft.Z3; { Context.CheckContextMatch(value); - Native.fixedpointSetParams(Context.nCtx, NativeObject, value.NativeObject); + 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())); } /** @@ -46,9 +50,9 @@ package com.Microsoft.Z3; Context.CheckContextMatch(constraints); - for (BoolExpr.Iterator a = constraints.iterator(); a.hasNext(); ) + for (Iterator a = constraints.iterator(); a.hasNext(); ) { - Native.fixedpointAssert(Context.nCtx, NativeObject, a.NativeObject); + Native.fixedpointAssert(Context().nCtx(), NativeObject(), a.NativeObject); } } @@ -60,7 +64,7 @@ package com.Microsoft.Z3; Context.CheckContextMatch(f); - Native.fixedpointRegisterRelation(Context.nCtx, NativeObject, f.NativeObject); + Native.fixedpointRegisterRelation(Context().nCtx(), NativeObject(), f.NativeObject); } /** @@ -71,7 +75,7 @@ package com.Microsoft.Z3; Context.CheckContextMatch(rule); - Native.fixedpointAddRule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name)); + Native.fixedpointAddRule(Context().nCtx(), NativeObject(), rule.NativeObject, AST.GetNativeObject(name)); } /** @@ -83,7 +87,7 @@ package com.Microsoft.Z3; Context.CheckContextMatch(pred); - Native.fixedpointAddFact(Context.nCtx, NativeObject, pred.NativeObject, (long)args.Length, args); + Native.fixedpointAddFact(Context().nCtx(), NativeObject(), pred.NativeObject, (long)args.Length, args); } /** @@ -97,11 +101,11 @@ package com.Microsoft.Z3; Context.CheckContextMatch(query); - Z3_lboolean r = (Z3_lboolean)Native.fixedpointQuery(Context.nCtx, NativeObject, query.NativeObject); + Z3_lbool r = (Z3_lbool)Native.fixedpointQuery(Context().nCtx(), NativeObject(), query.NativeObject); switch (r) { - case Z3_lboolean.Z3_L_TRUE: return Status.SATISFIABLE; - case Z3_lboolean.Z3_L_FALSE: return Status.UNSATISFIABLE; + case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE; + case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE; default: return Status.UNKNOWN; } } @@ -118,12 +122,12 @@ package com.Microsoft.Z3; Context.CheckContextMatch(relations); - Z3_lboolean r = (Z3_lboolean)Native.fixedpointQueryRelations(Context.nCtx, NativeObject, + Z3_lbool r = (Z3_lbool)Native.fixedpointQueryRelations(Context().nCtx(), NativeObject(), AST.ArrayLength(relations), AST.ArrayToNative(relations)); switch (r) { - case Z3_lboolean.Z3_L_TRUE: return Status.SATISFIABLE; - case Z3_lboolean.Z3_L_FALSE: return Status.UNSATISFIABLE; + case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE; + case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE; default: return Status.UNKNOWN; } } @@ -134,7 +138,7 @@ package com.Microsoft.Z3; **/ public void Push() { - Native.fixedpointPush(Context.nCtx, NativeObject); + Native.fixedpointPush(Context().nCtx(), NativeObject()); } /** @@ -144,7 +148,7 @@ package com.Microsoft.Z3; **/ public void Pop() { - Native.fixedpointPop(Context.nCtx, NativeObject); + Native.fixedpointPop(Context().nCtx(), NativeObject()); } @@ -156,7 +160,7 @@ package com.Microsoft.Z3; Context.CheckContextMatch(rule); - Native.fixedpointUpdateRule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name)); + Native.fixedpointUpdateRule(Context().nCtx(), NativeObject(), rule.NativeObject, AST.GetNativeObject(name)); } /** @@ -165,8 +169,8 @@ package com.Microsoft.Z3; **/ public Expr GetAnswer() { - IntPtr ans = Native.fixedpointGetAnswer(Context.nCtx, NativeObject); - return (ans == IntPtr.Zero) ? null : Expr.Create(Context, ans); + long ans = Native.fixedpointGetAnswer(Context().nCtx(), NativeObject()); + return (ans == 0) ? null : Expr.Create(Context, ans); } /** @@ -176,7 +180,7 @@ package com.Microsoft.Z3; { - return Native.fixedpointGetReasonUnknown(Context.nCtx, NativeObject); + return Native.fixedpointGetReasonUnknown(Context().nCtx(), NativeObject()); } /** @@ -184,7 +188,7 @@ package com.Microsoft.Z3; **/ public long GetNumLevels(FuncDecl predicate) { - return Native.fixedpointGetNumLevels(Context.nCtx, NativeObject, predicate.NativeObject); + return Native.fixedpointGetNumLevels(Context().nCtx(), NativeObject(), predicate.NativeObject); } /** @@ -192,8 +196,8 @@ package com.Microsoft.Z3; **/ public Expr GetCoverDelta(int level, FuncDecl predicate) { - IntPtr res = Native.fixedpointGetCoverDelta(Context.nCtx, NativeObject, level, predicate.NativeObject); - return (res == IntPtr.Zero) ? null : Expr.Create(Context, res); + long res = Native.fixedpointGetCoverDelta(Context().nCtx(), NativeObject(), level, predicate.NativeObject); + return (res == 0) ? null : Expr.Create(Context, res); } /** @@ -202,7 +206,7 @@ package com.Microsoft.Z3; **/ 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); } /** @@ -210,7 +214,7 @@ package com.Microsoft.Z3; **/ public String toString() { - return Native.fixedpointtoString(Context.nCtx, NativeObject, 0, null); + return Native.fixedpointToString(Context().nCtx(), NativeObject(), 0, null); } /** @@ -220,7 +224,7 @@ package com.Microsoft.Z3; { - Native.fixedpointSetPredicateRepresentation(Context.nCtx, NativeObject, + Native.fixedpointSetPredicateRepresentation(Context().nCtx(), NativeObject(), f.NativeObject, AST.ArrayLength(kinds), Symbol.ArrayToNative(kinds)); } @@ -231,7 +235,7 @@ package com.Microsoft.Z3; public String toString(BoolExpr[] queries) { - return Native.fixedpointtoString(Context.nCtx, NativeObject, + return Native.fixedpointToString(Context().nCtx(), NativeObject(), AST.ArrayLength(queries), AST.ArrayToNative(queries)); } @@ -242,10 +246,10 @@ package com.Microsoft.Z3; { - ASTVector v = new ASTVector(Context, Native.fixedpointGetRules(Context.nCtx, NativeObject)); + ASTVector v = new ASTVector(Context, Native.fixedpointGetRules(Context().nCtx(), NativeObject())); long n = v.Size; BoolExpr[] res = new BoolExpr[n]; - for (long i = 0; i < n; i++) + for (long i; i < n; i++) res[i] = new BoolExpr(Context, v[i].NativeObject); return res; } @@ -257,44 +261,44 @@ package com.Microsoft.Z3; { - ASTVector v = new ASTVector(Context, Native.fixedpointGetAssertions(Context.nCtx, NativeObject)); + ASTVector v = new ASTVector(Context, Native.fixedpointGetAssertions(Context().nCtx(), NativeObject())); long n = v.Size; BoolExpr[] res = new BoolExpr[n]; - for (long i = 0; i < n; i++) + for (long i; i < n; i++) res[i] = new BoolExpr(Context, v[i].NativeObject); return res; } - Fixedpoint(Context ctx, IntPtr obj) - { super(ctx, obj); + Fixedpoint(Context ctx, long obj) + { super(ctx, obj); } Fixedpoint(Context ctx) - { super(ctx, Native.mkFixedpoint(ctx.nCtx)); + { super(ctx, Native.mkFixedpoint(ctx.nCtx())); } - class DecRefQueue extends Z3.DecRefQueue + class DecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, IntPtr obj) + public void IncRef(Context ctx, long obj) { - Native.fixedpointIncRef(ctx.nCtx, obj); + Native.fixedpointIncRef(ctx.nCtx(), obj); } - public void DecRef(Context ctx, IntPtr obj) + public void DecRef(Context ctx, long obj) { - Native.fixedpointDecRef(ctx.nCtx, obj); + Native.fixedpointDecRef(ctx.nCtx(), obj); } }; - void IncRef(IntPtr o) + void IncRef(long o) { Context.Fixedpoint_DRQ.IncAndClear(Context, o); super.IncRef(o); } - void DecRef(IntPtr o) + void DecRef(long 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 ddedcf4ee..91579b085 100644 --- a/src/api/java/com/Microsoft/Z3/FuncDecl.java +++ b/src/api/java/com/Microsoft/Z3/FuncDecl.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -26,7 +30,7 @@ package com.Microsoft.Z3; /** * Object comparison. **/ - public boolean Equals(object o) + public boolean Equals(Object o) { FuncDecl casted = (FuncDecl) o; if (casted == null) return false; @@ -46,24 +50,24 @@ package com.Microsoft.Z3; **/ public String toString() { - return Native.funcDecltoString(Context.nCtx, NativeObject); + return Native.funcDeclToString(Context().nCtx(), NativeObject()); } /** * Returns a unique identifier for the function declaration. **/ - public long Id() { return Native.getFuncDeclId(Context.nCtx, NativeObject); } + public long Id() { return Native.getFuncDeclId(Context().nCtx(), NativeObject()); } /** * The arity of the function declaration **/ - public long Arity() { return Native.getArity(Context.nCtx, NativeObject); } + public long 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 long DomainSize() { return Native.getDomainSize(Context().nCtx(), NativeObject()); } /** * The domain of the function declaration @@ -75,8 +79,8 @@ package com.Microsoft.Z3; var n = DomainSize; Sort[] res = new Sort[n]; - for (long i = 0; i < n; i++) - res[i] = Sort.Create(Context, Native.getDomain(Context.nCtx, NativeObject, i)); + for (long i; i < n; i++) + res[i] = Sort.Create(Context, Native.getDomain(Context().nCtx(), NativeObject(), i)); return res; } @@ -86,13 +90,13 @@ package com.Microsoft.Z3; 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)Native.getDeclKind(Context().nCtx(), NativeObject()); } /** * The name of the function declaration @@ -100,13 +104,13 @@ package com.Microsoft.Z3; 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 long NumParameters() { return Native.getDeclNumParameters(Context().nCtx(), NativeObject()); } /** * The parameters of the function declaration @@ -117,31 +121,31 @@ package com.Microsoft.Z3; long num = NumParameters; Parameter[] res = new Parameter[num]; - for (long i = 0; i < num; i++) + for (long i; i < num; i++) { - Z3_parameter_kind k = (Z3_parameter_kind)Native.getDeclParameterKind(Context.nCtx, NativeObject, i); + Z3_parameter_kind k = (Z3_parameter_kind)Native.getDeclParameterKind(Context().nCtx(), NativeObject(), i); switch (k) { case Z3_parameter_kind.Z3_PARAMETER_INT: - res[i] = new Parameter(k, Native.getDeclIntParameter(Context.nCtx, NativeObject, i)); + res[i] = new Parameter(k, Native.getDeclIntParameter(Context().nCtx(), NativeObject(), i)); break; case Z3_parameter_kind.Z3_PARAMETER_DOUBLE: - res[i] = new Parameter(k, Native.getDeclDoubleParameter(Context.nCtx, NativeObject, i)); + res[i] = new Parameter(k, Native.getDeclDoubleParameter(Context().nCtx(), NativeObject(), i)); break; case Z3_parameter_kind.Z3_PARAMETER_SYMBOL: - res[i] = new Parameter(k, Symbol.Create(Context, Native.getDeclSymbolParameter(Context.nCtx, NativeObject, i))); + res[i] = new Parameter(k, Symbol.Create(Context, Native.getDeclSymbolParameter(Context().nCtx(), NativeObject(), i))); break; case Z3_parameter_kind.Z3_PARAMETER_SORT: - res[i] = new Parameter(k, Sort.Create(Context, Native.getDeclSortParameter(Context.nCtx, NativeObject, i))); + res[i] = new Parameter(k, Sort.Create(Context, Native.getDeclSortParameter(Context().nCtx(), NativeObject(), i))); break; case Z3_parameter_kind.Z3_PARAMETER_AST: - res[i] = new Parameter(k, new AST(Context, Native.getDeclAstParameter(Context.nCtx, NativeObject, i))); + res[i] = new Parameter(k, new AST(Context, Native.getDeclAstParameter(Context().nCtx(), NativeObject(), i))); break; case Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL: - res[i] = new Parameter(k, new FuncDecl(Context, Native.getDeclFuncDeclParameter(Context.nCtx, NativeObject, i))); + res[i] = new Parameter(k, new FuncDecl(Context, Native.getDeclFuncDeclParameter(Context().nCtx(), NativeObject(), i))); break; case Z3_parameter_kind.Z3_PARAMETER_RATIONAL: - res[i] = new Parameter(k, Native.getDeclRationalParameter(Context.nCtx, NativeObject, i)); + res[i] = new Parameter(k, Native.getDeclRationalParameter(Context().nCtx(), NativeObject(), i)); break; default: throw new Z3Exception("Unknown function declaration parameter kind encountered"); @@ -195,7 +199,8 @@ package com.Microsoft.Z3; { this.kind = k; this.i = i; - } + } + Parameter(Z3_parameter_kind k, double d) { this.kind = k; @@ -233,31 +238,27 @@ package com.Microsoft.Z3; } } - FuncDecl(Context ctx, IntPtr obj) - { super(ctx, obj); + FuncDecl(Context ctx, long obj) + { super(ctx, obj); } FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range) - : base(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) - : base(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(IntPtr obj) + void CheckNativeObject(long obj) { - if (Native.getAstKind(Context.nCtx, obj) != (long)Z3_ast_kind.Z3_FUNC_DECL_AST) + if (Native.getAstKind(Context().nCtx(), obj) != (long)Z3_ast_kind.Z3_FUNC_DECL_AST) throw new Z3Exception("Underlying object is not a function declaration"); super.CheckNativeObject(obj); } @@ -267,15 +268,8 @@ package com.Microsoft.Z3; * * @return **/ - public Expr this[params() lic Expr this[params Expr[] args - { - public Expr this[params() - { - - - return Apply(args); - } - + /* operator this[] not translated */ + /** * Create expression that applies function to arguments. * diff --git a/src/api/java/com/Microsoft/Z3/FuncInterp.java b/src/api/java/com/Microsoft/Z3/FuncInterp.java index 6aeb33759..7544aba11 100644 --- a/src/api/java/com/Microsoft/Z3/FuncInterp.java +++ b/src/api/java/com/Microsoft/Z3/FuncInterp.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -21,15 +25,16 @@ package com.Microsoft.Z3; /** * Return the (symbolic) value of this entry. **/ - public Expr Value() { + public Expr Value() + { - return Expr.Create(Context, Native.funcEntryGetValue(Context.nCtx, NativeObject)); } - } + return Expr.Create(Context, Native.funcEntryGetValue(Context().nCtx(), NativeObject())); + } /** * The number of arguments of the entry. **/ - public long NumArgs() { return Native.funcEntryGetNumArgs(Context.nCtx, NativeObject); } + public long NumArgs() { return Native.funcEntryGetNumArgs(Context().nCtx(), NativeObject()); } /** * The arguments of the function entry. @@ -41,8 +46,8 @@ package com.Microsoft.Z3; long n = NumArgs; Expr[] res = new Expr[n]; - for (long i = 0; i < n; i++) - res[i] = Expr.Create(Context, Native.funcEntryGetArg(Context.nCtx, NativeObject, i)); + for (long i; i < n; i++) + res[i] = Expr.Create(Context, Native.funcEntryGetArg(Context().nCtx(), NativeObject(), i)); return res; } @@ -54,33 +59,33 @@ package com.Microsoft.Z3; long n = NumArgs; String res = "["; Expr[] args = Args; - for (long i = 0; i < n; i++) + for (long i; i < n; i++) res += args[i] + ", "; return res + Value + "]"; } - Entry(Context ctx, IntPtr obj) { super(ctx, obj); } + Entry(Context ctx, long obj) { super(ctx, obj); { }} - class DecRefQueue extends Z3.DecRefQueue + class DecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, IntPtr obj) + public void IncRef(Context ctx, long obj) { - Native.funcEntryIncRef(ctx.nCtx, obj); + Native.funcEntryIncRef(ctx.nCtx(), obj); } - public void DecRef(Context ctx, IntPtr obj) + public void DecRef(Context ctx, long obj) { - Native.funcEntryDecRef(ctx.nCtx, obj); + Native.funcEntryDecRef(ctx.nCtx(), obj); } }; - void IncRef(IntPtr o) + void IncRef(long o) { Context.FuncEntry_DRQ.IncAndClear(Context, o); super.IncRef(o); } - void DecRef(IntPtr o) + void DecRef(long o) { Context.FuncEntry_DRQ.Add(o); super.DecRef(o); @@ -90,7 +95,7 @@ package com.Microsoft.Z3; /** * The number of entries in the function interpretation. **/ - public long NumEntries() { return Native.funcInterpGetNumEntries(Context.nCtx, NativeObject); } + public long NumEntries() { return Native.funcInterpGetNumEntries(Context().nCtx(), NativeObject()); } /** * The entries in the function interpretation @@ -98,29 +103,29 @@ package com.Microsoft.Z3; public Entry[] Entries() { - Contract.Ensures(Contract.ForAll(0, Contract.Result().Length, - j => Contract.Result()[j] != null)); + long n = NumEntries; Entry[] res = new Entry[n]; - for (long i = 0; i < n; i++) - res[i] = new Entry(Context, Native.funcInterpGetEntry(Context.nCtx, NativeObject, i)); + for (long i; i < n; i++) + res[i] = new Entry(Context, Native.funcInterpGetEntry(Context().nCtx(), NativeObject(), i)); return res; } /** * The (symbolic) `else' value of the function interpretation. **/ - public Expr Else() { + public Expr Else() + { - 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 long Arity() { return Native.funcInterpGetArity(Context().nCtx(), NativeObject()); } /** * A string representation of the function interpretation. @@ -129,12 +134,12 @@ package com.Microsoft.Z3; { String res = ""; res += "["; - for (Entry.Iterator e = Entries.iterator(); e.hasNext(); ) + for (Iterator e = Entries.iterator(); e.hasNext(); ) { - long n = e.NumArgs; + long n = e.NumArgs; if (n > 1) res += "["; Expr[] args = e.Args; - for (long i = 0; i < n; i++) + for (long i; i < n; i++) { if (i != 0) res += ", "; res += args[i]; @@ -147,31 +152,31 @@ package com.Microsoft.Z3; return res; } - FuncInterp(Context ctx, IntPtr obj) - { super(ctx, obj); + FuncInterp(Context ctx, long obj) + { super(ctx, obj); } - class DecRefQueue extends Z3.DecRefQueue + class DecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, IntPtr obj) + public void IncRef(Context ctx, long obj) { - Native.funcInterpIncRef(ctx.nCtx, obj); + Native.funcInterpIncRef(ctx.nCtx(), obj); } - public void DecRef(Context ctx, IntPtr obj) + public void DecRef(Context ctx, long obj) { - Native.funcInterpDecRef(ctx.nCtx, obj); + Native.funcInterpDecRef(ctx.nCtx(), obj); } - }; + }; - void IncRef(IntPtr o) + void IncRef(long o) { Context.FuncInterp_DRQ.IncAndClear(Context, o); super.IncRef(o); } - void DecRef(IntPtr o) + void DecRef(long 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 171b81d47..bfbefa203 100644 --- a/src/api/java/com/Microsoft/Z3/Goal.java +++ b/src/api/java/com/Microsoft/Z3/Goal.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -21,7 +25,7 @@ package com.Microsoft.Z3; * 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)Native.goalPrecision(Context().nCtx(), NativeObject()); } /** * Indicates whether the goal is precise. @@ -51,17 +55,17 @@ package com.Microsoft.Z3; Context.CheckContextMatch(constraints); - for (BoolExpr.Iterator c = constraints.iterator(); c.hasNext(); ) + for (Iterator c = constraints.iterator(); c.hasNext(); ) { // 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()) != 0; } /** * The depth of the goal. @@ -69,20 +73,20 @@ package com.Microsoft.Z3; * This tracks how many transformations were applied to it. * **/ - public long Depth() { return Native.goalDepth(Context.nCtx, NativeObject); } + public long Depth() { return Native.goalDepth(Context().nCtx(), NativeObject()); } /** * Erases all formulas from the given goal. **/ public void Reset() { - Native.goalReset(Context.nCtx, NativeObject); + Native.goalReset(Context().nCtx(), NativeObject()); } /** * The number of formulas in the goal. **/ - public long Size() { return Native.goalSize(Context.nCtx, NativeObject); } + public long Size() { return Native.goalSize(Context().nCtx(), NativeObject()); } /** * The formulas in the goal. @@ -93,25 +97,25 @@ package com.Microsoft.Z3; long n = Size; BoolExpr[] res = new BoolExpr[n]; - for (long i = 0; i < n; i++) - res[i] = new BoolExpr(Context, Native.goalFormula(Context.nCtx, NativeObject, i)); + for (long i; 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 long 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()) != 0; } /** * 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()) != 0; } /** * Translates (copies) the Goal to the target Context . @@ -120,7 +124,7 @@ package com.Microsoft.Z3; { - return new Goal(ctx, Native.goalTranslate(Context.nCtx, NativeObject, ctx.nCtx)); + return new Goal(ctx, Native.goalTranslate(Context().nCtx(), NativeObject(), ctx.nCtx())); } /** @@ -144,36 +148,36 @@ package com.Microsoft.Z3; **/ public String toString() { - return Native.goaltoString(Context.nCtx, NativeObject); + return Native.goalToString(Context().nCtx(), NativeObject()); } - Goal(Context ctx, IntPtr obj) { super(ctx, obj); } + Goal(Context ctx, long obj) { super(ctx, obj); { }} Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs) - { super(ctx, Native.mkGoal(ctx.nCtx, (models); ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0)) + { super(ctx, Native.mkGoal(ctx.nCtx(), (models) ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0)); } - class DecRefQueue extends Z3.DecRefQueue + class DecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, IntPtr obj) + public void IncRef(Context ctx, long obj) { - Native.goalIncRef(ctx.nCtx, obj); + Native.goalIncRef(ctx.nCtx(), obj); } - public void DecRef(Context ctx, IntPtr obj) + public void DecRef(Context ctx, long obj) { - Native.goalDecRef(ctx.nCtx, obj); + Native.goalDecRef(ctx.nCtx(), obj); } }; - void IncRef(IntPtr o) + void IncRef(long o) { Context.Goal_DRQ.IncAndClear(Context, o); super.IncRef(o); } - void DecRef(IntPtr o) + void DecRef(long o) { Context.Goal_DRQ.Add(o); super.DecRef(o); diff --git a/src/api/java/com/Microsoft/Z3/DecRefQUeue.java b/src/api/java/com/Microsoft/Z3/IDecRefQueue.java similarity index 55% rename from src/api/java/com/Microsoft/Z3/DecRefQUeue.java rename to src/api/java/com/Microsoft/Z3/IDecRefQueue.java index 279887a7c..1b6291ce7 100644 --- a/src/api/java/com/Microsoft/Z3/DecRefQUeue.java +++ b/src/api/java/com/Microsoft/Z3/IDecRefQueue.java @@ -1,15 +1,19 @@ /** - * This file was automatically generated from DecRefQUeue.cs + * This file was automatically generated from IDecRefQueue.cs **/ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /* using System.Collections; */ /* using System.Collections.Generic; */ /* using System.Threading; */ - abstract class DecRefQueue + abstract class IDecRefQueue { private void ObjectInvariant() @@ -19,13 +23,13 @@ package com.Microsoft.Z3; protected Object m_lock = new Object(); - protected List m_queue = new List(); + protected List m_queue = new List(); final long m_move_limit = 1024; - public abstract void IncRef(Context ctx, IntPtr obj); - public abstract void DecRef(Context ctx, IntPtr obj); + public abstract void IncRef(Context ctx, long obj); + public abstract void DecRef(Context ctx, long obj); - public void IncAndClear(Context ctx, IntPtr o) + public void IncAndClear(Context ctx, long o) { @@ -33,9 +37,9 @@ package com.Microsoft.Z3; if (m_queue.Count >= m_move_limit) Clear(ctx); } - public void Add(IntPtr o) + public void Add(long o) { - if (o == IntPtr.Zero) return; + if (o == 0) return; synchronized (m_lock) { @@ -49,21 +53,21 @@ package com.Microsoft.Z3; synchronized (m_lock) { - for (IntPtr.Iterator o = m_queue.iterator(); o.hasNext(); ) + for (Iterator o = m_queue.iterator(); o.hasNext(); ) DecRef(ctx, o); m_queue.Clear(); } } } - abstract class DecRefQueueContracts extends DecRefQueue + abstract class DecRefQueueContracts extends IDecRefQueue { - public void IncRef(Context ctx, IntPtr obj) + public void IncRef(Context ctx, long obj) { } - public void DecRef(Context ctx, IntPtr obj) + public void DecRef(Context ctx, long obj) { } diff --git a/src/api/java/com/Microsoft/Z3/IntExpr.java b/src/api/java/com/Microsoft/Z3/IntExpr.java new file mode 100644 index 000000000..888e441b3 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/IntExpr.java @@ -0,0 +1,31 @@ +/** + * This file was automatically generated from IntExpr.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; +/* using System; */ +/* using System.Collections.Generic; */ +/* using System.Linq; */ +/* using System.Text; */ + + + /** + * Int expressions + **/ + public class IntExpr extends ArithExpr + { + /** Constructor for IntExpr + **/ + protected IntExpr(Context ctx) + { super(ctx); + + } + IntExpr(Context ctx, long obj) + { super(ctx, obj); + + } + } diff --git a/src/api/java/com/Microsoft/Z3/IntNum.java b/src/api/java/com/Microsoft/Z3/IntNum.java new file mode 100644 index 000000000..e4d0e72e2 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/IntNum.java @@ -0,0 +1,85 @@ +/** + * This file was automatically generated from IntNum.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; +/* using System; */ + +/* using System.Numerics; */ + + /** + * Integer Numerals + **/ + public class IntNum extends IntExpr + { + + IntNum(Context ctx, long obj) + { super(ctx, obj); + + } + + + /** + * Retrieve the 64-bit unsigned integer value. + **/ + public long UInt64() + { + long res = 0; + if (Native.getNumeralLong64(Context().nCtx(), NativeObject(), res) == 0) + throw new Z3Exception("Numeral is not a 64 bit unsigned"); + return res; + } + + /** + * Retrieve the int value. + **/ + public int Int() + { + int res = 0; + if (Native.getNumeralInt(Context().nCtx(), NativeObject(), res) == 0) + throw new Z3Exception("Numeral is not an int"); + return res; + } + + /** + * Retrieve the 64-bit int value. + **/ + public long Int64() + { + long res = 0; + if (Native.getNumeralInt64(Context().nCtx(), NativeObject(), res) == 0) + throw new Z3Exception("Numeral is not an int64"); + return res; + } + + /** + * Retrieve the int value. + **/ + public long UInt() + { + long res = 0; + if (Native.getNumeralLong(Context().nCtx(), NativeObject(), res) == 0) + throw new Z3Exception("Numeral is not a long"); + return res; + } + + /** + * Retrieve the BigInteger value. + **/ + public BigInteger BigInteger() + { + return BigInteger.Parse(this.ToString()); + } + + /** + * Returns a string representation of the numeral. + **/ + public String toString() + { + return Native.getNumeralString(Context().nCtx(), NativeObject()); + } + } diff --git a/src/api/java/com/Microsoft/Z3/IntSort.java b/src/api/java/com/Microsoft/Z3/IntSort.java new file mode 100644 index 000000000..29ff35136 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/IntSort.java @@ -0,0 +1,26 @@ +/** + * This file was automatically generated from IntSort.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ + + /** + * An Integer sort + **/ + public class IntSort extends ArithSort + { + IntSort(Context ctx, long obj) + { super(ctx, obj); + + } + IntSort(Context ctx) + { super(ctx, Native.mkIntSort(ctx.nCtx())); + + } + } diff --git a/src/api/java/com/Microsoft/Z3/IntSymbol.java b/src/api/java/com/Microsoft/Z3/IntSymbol.java new file mode 100644 index 000000000..0132def21 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/IntSymbol.java @@ -0,0 +1,45 @@ +/** + * This file was automatically generated from IntSymbol.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ +/* using System.Runtime.InteropServices; */ + + /** + * Numbered symbols + **/ + public class IntSymbol extends Symbol + { + /** + * The int value of the symbol. + * Throws an exception if the symbol is not of int kind. + **/ + public int Int() + { + if (!IsIntSymbol()) + throw new Z3Exception("Int requested from non-Int symbol"); + return Native.getSymbolInt(Context().nCtx(), NativeObject()); + } + + IntSymbol(Context ctx, long obj) + { super(ctx, obj); + + } + IntSymbol(Context ctx, int i) + { super(ctx, Native.mkIntSymbol(ctx.nCtx(), i)); + + } + + void CheckNativeObject(long obj) + { + if ((Z3_symbol_kind)Native.getSymbolKind(Context().nCtx(), obj) != Z3_symbol_kind.Z3_INT_SYMBOL) + throw new Z3Exception("Symbol is not of integer kind"); + super.CheckNativeObject(obj); + } + } diff --git a/src/api/java/com/Microsoft/Z3/ListSort.java b/src/api/java/com/Microsoft/Z3/ListSort.java new file mode 100644 index 000000000..96829c11e --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/ListSort.java @@ -0,0 +1,122 @@ +/** + * This file was automatically generated from ListSort.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ + + /** + * List sorts. + **/ + public class ListSort extends Sort + { + /** + * The declaration of the nil function of this list sort. + **/ + public FuncDecl NilDecl() + { + + return nilDecl; + } + + /** + * The empty list. + **/ + public Expr Nil() + { + + return nilConst; + } + + /** + * The declaration of the isNil function of this list sort. + **/ + public FuncDecl IsNilDecl() + { + + return isNilDecl; + } + + /** + * The declaration of the cons function of this list sort. + **/ + public FuncDecl ConsDecl() + { + + return consDecl; + } + + /** + * The declaration of the isCons function of this list sort. + * + **/ + public FuncDecl IsConsDecl() + { + + return isConsDecl; + } + + /** + * The declaration of the head function of this list sort. + **/ + public FuncDecl HeadDecl() + { + + return headDecl; + } + + /** + * The declaration of the tail function of this list sort. + **/ + public FuncDecl TailDecl() + { + + return tailDecl; + } + + + private void ObjectInvariant() + { + + + + + + + + } + + + + private FuncDecl nilDecl, isNilDecl, consDecl, isConsDecl, headDecl, tailDecl; + private Expr nilConst; + + ListSort(Context ctx, Symbol name, Sort elemSort) + { super(ctx); + + + + + long inil = 0, + iisnil = 0, + icons = 0, + iiscons = 0, + ihead = 0, + itail = 0; + + 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); + consDecl = new FuncDecl(ctx, icons); + isConsDecl = new FuncDecl(ctx, iiscons); + headDecl = new FuncDecl(ctx, ihead); + tailDecl = new FuncDecl(ctx, itail); + nilConst = ctx.MkConst(nilDecl); + } + }; diff --git a/src/api/java/com/Microsoft/Z3/Log.java b/src/api/java/com/Microsoft/Z3/Log.java index 35ac0e022..bfcc2b1c5 100644 --- a/src/api/java/com/Microsoft/Z3/Log.java +++ b/src/api/java/com/Microsoft/Z3/Log.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** diff --git a/src/api/java/com/Microsoft/Z3/Model.java b/src/api/java/com/Microsoft/Z3/Model.java index edd774f56..e20a9d575 100644 --- a/src/api/java/com/Microsoft/Z3/Model.java +++ b/src/api/java/com/Microsoft/Z3/Model.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -35,11 +39,11 @@ package com.Microsoft.Z3; 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)) == (long)Z3_sort_kind.Z3_ARRAY_SORT) throw new Z3Exception("Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp."); - IntPtr n = Native.modelGetConstInterp(Context.nCtx, NativeObject, f.NativeObject); - if (n == IntPtr.Zero) + long n = Native.modelGetConstInterp(Context().nCtx(), NativeObject(), f.NativeObject); + if (n == 0) return null; else return Expr.Create(Context, n); @@ -56,21 +60,21 @@ package com.Microsoft.Z3; 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)Native.getSortKind(Context().nCtx(), Native.getRange(Context().nCtx(), f.NativeObject)); if (f.Arity == 0) { - IntPtr n = Native.modelGetConstInterp(Context.nCtx, NativeObject, f.NativeObject); + long n = Native.modelGetConstInterp(Context().nCtx(), NativeObject(), f.NativeObject); if (sk == Z3_sort_kind.Z3_ARRAY_SORT) { - if (n == IntPtr.Zero) + if (n == 0) return null; else { - if (Native.isAsArray(Context.nCtx, n) == 0) + if (Native.isAsArray(Context().nCtx(), n) == 0) throw new Z3Exception("Argument was not an array constant"); - IntPtr fd = Native.getAsArrayFuncDecl(Context.nCtx, n); + long fd = Native.getAsArrayFuncDecl(Context().nCtx(), n); return FuncInterp(new FuncDecl(Context, fd)); } } @@ -81,8 +85,8 @@ package com.Microsoft.Z3; } else { - IntPtr n = Native.modelGetFuncInterp(Context.nCtx, NativeObject, f.NativeObject); - if (n == IntPtr.Zero) + long n = Native.modelGetFuncInterp(Context().nCtx(), NativeObject(), f.NativeObject); + if (n == 0) return null; else return new FuncInterp(Context, n); @@ -92,7 +96,7 @@ package com.Microsoft.Z3; /** * The number of constants that have an interpretation in the model. **/ - public long NumConsts() { return Native.modelGetNumConsts(Context.nCtx, NativeObject); } + public long NumConsts() { return Native.modelGetNumConsts(Context().nCtx(), NativeObject()); } /** * The function declarations of the constants in the model. @@ -103,15 +107,15 @@ package com.Microsoft.Z3; long n = NumConsts; FuncDecl[] res = new FuncDecl[n]; - for (long i = 0; i < n; i++) - res[i] = new FuncDecl(Context, Native.modelGetConstDecl(Context.nCtx, NativeObject, i)); + for (long i; 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 long NumFuncs() { return Native.modelGetNumFuncs(Context().nCtx(), NativeObject()); } /** * The function declarations of the function interpretations in the model. @@ -122,8 +126,8 @@ package com.Microsoft.Z3; long n = NumFuncs; FuncDecl[] res = new FuncDecl[n]; - for (long i = 0; i < n; i++) - res[i] = new FuncDecl(Context, Native.modelGetFuncDecl(Context.nCtx, NativeObject, i)); + for (long i; i < n; i++) + res[i] = new FuncDecl(Context, Native.modelGetFuncDecl(Context().nCtx(), NativeObject(), i)); return res; } @@ -138,10 +142,10 @@ package com.Microsoft.Z3; var nConsts = NumConsts; long n = nFuncs + nConsts; FuncDecl[] res = new FuncDecl[n]; - for (long i = 0; i < nConsts; i++) - res[i] = new FuncDecl(Context, Native.modelGetConstDecl(Context.nCtx, NativeObject, i)); - for (long i = 0; i < nFuncs; i++) - res[nConsts + i] = new FuncDecl(Context, Native.modelGetFuncDecl(Context.nCtx, NativeObject, i)); + 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)); return res; } @@ -153,7 +157,7 @@ package com.Microsoft.Z3; /** * An exception that is thrown when model evaluation fails. **/ - public ModelEvaluationFailedException() { super(); } + public ModelEvaluationFailedException() { super(); { }} } /** @@ -175,8 +179,8 @@ package com.Microsoft.Z3; - IntPtr v = IntPtr.Zero; - if (Native.modelEval(Context.nCtx, NativeObject, t.NativeObject, (completion) ? 1 : 0, v) == 0) + long v = 0; + if (Native.modelEval(Context().nCtx(), NativeObject(), t.NativeObject, (completion) ? 1 : 0, v) == 0) throw new ModelEvaluationFailedException(); else return Expr.Create(Context, v); @@ -196,7 +200,7 @@ package com.Microsoft.Z3; /** * The number of uninterpreted sorts that the model has an interpretation for. **/ - public long NumSorts () { return Native.modelGetNumSorts(Context.nCtx, NativeObject); } + public long NumSorts () { return Native.modelGetNumSorts(Context().nCtx(), NativeObject()); } /** * The uninterpreted sorts that the model has an interpretation for. @@ -214,8 +218,8 @@ package com.Microsoft.Z3; long n = NumSorts; Sort[] res = new Sort[n]; - for (long i = 0; i < n; i++) - res[i] = Sort.Create(Context, Native.modelGetSort(Context.nCtx, NativeObject, i)); + for (long i; i < n; i++) + res[i] = Sort.Create(Context, Native.modelGetSort(Context().nCtx(), NativeObject(), i)); return res; } @@ -230,10 +234,10 @@ package com.Microsoft.Z3; - ASTVector nUniv = new ASTVector(Context, Native.modelGetSortUniverse(Context.nCtx, NativeObject, s.NativeObject)); + ASTVector nUniv = new ASTVector(Context, Native.modelGetSortUniverse(Context().nCtx(), NativeObject(), s.NativeObject)); long n = nUniv.Size; Expr[] res = new Expr[n]; - for (long i = 0; i < n; i++) + for (long i; i < n; i++) res[i] = Expr.Create(Context, nUniv[i].NativeObject); return res; } @@ -244,34 +248,34 @@ package com.Microsoft.Z3; **/ public String toString() { - return Native.modeltoString(Context.nCtx, NativeObject); + return Native.modelToString(Context().nCtx(), NativeObject()); } - Model(Context ctx, IntPtr obj) - { super(ctx, obj); + Model(Context ctx, long obj) + { super(ctx, obj); } - class DecRefQueue extends Z3.DecRefQueue + class DecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, IntPtr obj) + public void IncRef(Context ctx, long obj) { - Native.modelIncRef(ctx.nCtx, obj); + Native.modelIncRef(ctx.nCtx(), obj); } - public void DecRef(Context ctx, IntPtr obj) + public void DecRef(Context ctx, long obj) { - Native.modelDecRef(ctx.nCtx, obj); + Native.modelDecRef(ctx.nCtx(), obj); } }; - void IncRef(IntPtr o) + void IncRef(long o) { Context.Model_DRQ.IncAndClear(Context, o); super.IncRef(o); } - void DecRef(IntPtr o) + void DecRef(long 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 31ca6f4bc..261e0663f 100644 --- a/src/api/java/com/Microsoft/Z3/Native.java +++ b/src/api/java/com/Microsoft/Z3/Native.java @@ -4,7 +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; } - static { System.loadLibrary(""); } + public static class errorHandler {}; + 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/Numeral.java b/src/api/java/com/Microsoft/Z3/Numeral.java deleted file mode 100644 index d0ed20dc9..000000000 --- a/src/api/java/com/Microsoft/Z3/Numeral.java +++ /dev/null @@ -1,264 +0,0 @@ -/** - * This file was automatically generated from Numeral.cs - **/ - -package com.Microsoft.Z3; -/* using System; */ - -/* using System.Numerics; */ - - /** - * Integer Numerals - **/ - public class IntNum extends IntExpr - { - - IntNum(Context ctx, IntPtr obj) - { super(ctx, obj); - - } - - - /** - * Retrieve the 64-bit unsigned integer value. - **/ - public UInt64 UInt64() - { - UInt64 res = 0; - if (Native.getNumeralLong64(Context.nCtx, NativeObject, res) == 0) - throw new Z3Exception("Numeral is not a 64 bit unsigned"); - return res; - } - - /** - * Retrieve the int value. - **/ - public int Int() - { - int res = 0; - if (Native.getNumeralInt(Context.nCtx, NativeObject, res) == 0) - throw new Z3Exception("Numeral is not an int"); - return res; - } - - /** - * Retrieve the 64-bit int value. - **/ - public Int64 Int64() - { - Int64 res = 0; - if (Native.getNumeralInt64(Context.nCtx, NativeObject, res) == 0) - throw new Z3Exception("Numeral is not an int64"); - return res; - } - - /** - * Retrieve the int value. - **/ - public long UInt() - { - long res = 0; - if (Native.getNumeralLong(Context.nCtx, NativeObject, res) == 0) - throw new Z3Exception("Numeral is not a long"); - return res; - } - - /** - * Retrieve the BigInteger value. - **/ - public BigInteger BigInteger() - { - return BigInteger.Parse(this.toString()); - } - - /** - * Returns a string representation of the numeral. - **/ - public String toString() - { - return Native.getNumeralString(Context.nCtx, NativeObject); - } - } - - /** - * Rational Numerals - **/ - public class RatNum extends RealExpr - { - /** - * The numerator of a rational numeral. - **/ - public IntNum Numerator() { - - - return new IntNum(Context, Native.getNumerator(Context.nCtx, NativeObject)); } - } - - /** - * The denominator of a rational numeral. - **/ - public IntNum Denominator() { - - - return new IntNum(Context, Native.getDenominator(Context.nCtx, NativeObject)); } - } - - /** - * Converts the numerator of the rational to a BigInteger - **/ - public BigInteger BigIntNumerator() - { - IntNum n = Numerator; - return BigInteger.Parse(n.toString()); - } - - /** - * Converts the denominator of the rational to a BigInteger - **/ - public BigInteger BigIntDenominator() - { - IntNum n = Denominator; - return BigInteger.Parse(n.toString()); - } - - /** - * Returns a string representation in decimal notation. - * The result has at most decimal places. - **/ - public String ToDecimalString(long precision) - { - return Native.getNumeralDecimalString(Context.nCtx, NativeObject, precision); - } - - /** - * Returns a string representation of the numeral. - **/ - public String toString() - { - return Native.getNumeralString(Context.nCtx, NativeObject); - } - - RatNum(Context ctx, IntPtr obj) - { super(ctx, obj); - - } - } - - - /** - * Bit-vector numerals - **/ - public class BitVecNum extends BitVecExpr - { - /** - * Retrieve the 64-bit unsigned integer value. - **/ - public UInt64 UInt64() - { - UInt64 res = 0; - if (Native.getNumeralLong64(Context.nCtx, NativeObject, res) == 0) - throw new Z3Exception("Numeral is not a 64 bit unsigned"); - return res; - } - - /** - * Retrieve the int value. - **/ - public int Int() - { - int res = 0; - if (Native.getNumeralInt(Context.nCtx, NativeObject, res) == 0) - throw new Z3Exception("Numeral is not an int"); - return res; - } - - /** - * Retrieve the 64-bit int value. - **/ - public Int64 Int64() - { - Int64 res = 0; - if (Native.getNumeralInt64(Context.nCtx, NativeObject, res) == 0) - throw new Z3Exception("Numeral is not an int64"); - return res; - } - - /** - * Retrieve the int value. - **/ - public long UInt() - { - long res = 0; - if (Native.getNumeralLong(Context.nCtx, NativeObject, res) == 0) - throw new Z3Exception("Numeral is not a long"); - return res; - } - - /** - * Retrieve the BigInteger value. - **/ - public BigInteger BigInteger() - { - return BigInteger.Parse(this.toString()); - } - - /** - * Returns a string representation of the numeral. - **/ - public String toString() - { - return Native.getNumeralString(Context.nCtx, NativeObject); - } - - BitVecNum(Context ctx, IntPtr obj) { super(ctx, obj); } - } - - /** - * Algebraic numbers - **/ - public class AlgebraicNum extends ArithExpr - { - /** - * Return a upper bound for a given real algebraic number. - * The interval isolating the number is smaller than 1/10^. - * - * the precision of the result - * @return A numeral Expr of sort Real - **/ - public RatNum ToUpper(long precision) - { - - - return new RatNum(Context, Native.getAlgebraicNumberUpper(Context.nCtx, NativeObject, precision)); - } - - /** - * Return a lower bound for the given real algebraic number. - * The interval isolating the number is smaller than 1/10^. - * - * - * @return A numeral Expr of sort Real - **/ - public RatNum ToLower(long 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) - { - - - return Native.getNumeralDecimalString(Context.nCtx, NativeObject, precision); - } - - AlgebraicNum(Context ctx, IntPtr obj) - { super(ctx, obj); - - } - } diff --git a/src/api/java/com/Microsoft/Z3/ParamDescrs.java b/src/api/java/com/Microsoft/Z3/ParamDescrs.java index abade80b2..37ee77b7e 100644 --- a/src/api/java/com/Microsoft/Z3/ParamDescrs.java +++ b/src/api/java/com/Microsoft/Z3/ParamDescrs.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -17,7 +21,7 @@ package com.Microsoft.Z3; public void Validate(Params p) { - Native.paramsValidate(Context.nCtx, p.NativeObject, NativeObject); + Native.paramsValidate(Context().nCtx(), p.NativeObject, NativeObject()); } /** @@ -26,7 +30,7 @@ package com.Microsoft.Z3; public Z3_param_kind GetKind(Symbol name) { - return (Z3_param_kind)Native.paramDescrsGetKind(Context.nCtx, NativeObject, name.NativeObject); + return (Z3_param_kind)Native.paramDescrsGetKind(Context().nCtx(), NativeObject(), name.NativeObject); } /** @@ -34,10 +38,10 @@ package com.Microsoft.Z3; **/ public Symbol[] Names() { - long sz = Native.paramDescrsSize(Context.nCtx, NativeObject); + long sz = Native.paramDescrsSize(Context().nCtx(), NativeObject()); Symbol[] names = new Symbol[sz]; - for (long i = 0; i < sz; ++i) { - names[i] = Symbol.Create(Context, Native.paramDescrsGetName(Context.nCtx, NativeObject, i)); + for (long i; i < sz; ++i) { + names[i] = Symbol.Create(Context, Native.paramDescrsGetName(Context().nCtx(), NativeObject(), i)); } return names; } @@ -45,41 +49,41 @@ package com.Microsoft.Z3; /** * The size of the ParamDescrs. **/ - public long Size() { return Native.paramDescrsSize(Context.nCtx, NativeObject); } + public long Size() { return Native.paramDescrsSize(Context().nCtx(), NativeObject()); } /** * Retrieves a string representation of the ParamDescrs. **/ public String toString() { - return Native.paramDescrstoString(Context.nCtx, NativeObject); + return Native.paramDescrsToString(Context().nCtx(), NativeObject()); } - ParamDescrs(Context ctx, IntPtr obj) - { super(ctx, obj); + ParamDescrs(Context ctx, long obj) + { super(ctx, obj); } - class DecRefQueue extends Z3.DecRefQueue + class DecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, IntPtr obj) + public void IncRef(Context ctx, long obj) { - Native.paramDescrsIncRef(ctx.nCtx, obj); + Native.paramDescrsIncRef(ctx.nCtx(), obj); } - public void DecRef(Context ctx, IntPtr obj) + public void DecRef(Context ctx, long obj) { - Native.paramDescrsDecRef(ctx.nCtx, obj); + Native.paramDescrsDecRef(ctx.nCtx(), obj); } }; - void IncRef(IntPtr o) + void IncRef(long o) { Context.ParamDescrs_DRQ.IncAndClear(Context, o); super.IncRef(o); } - void DecRef(IntPtr o) + void DecRef(long 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 040b6d67d..d5c042d74 100644 --- a/src/api/java/com/Microsoft/Z3/Params.java +++ b/src/api/java/com/Microsoft/Z3/Params.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -18,7 +22,7 @@ package com.Microsoft.Z3; { - Native.paramsSetBoolean(Context.nCtx, NativeObject, name.NativeObject, (value) ? 1 : 0); + Native.paramsSetBool(Context().nCtx(), NativeObject(), name.NativeObject, (value) ? 1 : 0); } /** @@ -28,7 +32,7 @@ package com.Microsoft.Z3; { - Native.paramsSetLong(Context.nCtx, NativeObject, name.NativeObject, value); + Native.paramsSetLong(Context().nCtx(), NativeObject(), name.NativeObject, value); } /** @@ -38,7 +42,7 @@ package com.Microsoft.Z3; { - Native.paramsSetDouble(Context.nCtx, NativeObject, name.NativeObject, value); + Native.paramsSetDouble(Context().nCtx(), NativeObject(), name.NativeObject, value); } /** @@ -49,7 +53,7 @@ package com.Microsoft.Z3; - Native.paramsSetSymbol(Context.nCtx, NativeObject, name.NativeObject, value.NativeObject); + Native.paramsSetSymbol(Context().nCtx(), NativeObject(), name.NativeObject, value.NativeObject); } /** @@ -57,7 +61,7 @@ package com.Microsoft.Z3; **/ public void Add(String name, boolean value) { - Native.paramsSetBoolean(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value) ? 1 : 0); + Native.paramsSetBool(Context().nCtx(), NativeObject(), Context.MkSymbol(name).NativeObject, (value) ? 1 : 0); } /** @@ -65,7 +69,7 @@ package com.Microsoft.Z3; **/ public void Add(String name, long value) { - Native.paramsSetLong(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value); + Native.paramsSetLong(Context().nCtx(), NativeObject(), Context.MkSymbol(name).NativeObject, value); } /** @@ -73,7 +77,7 @@ package com.Microsoft.Z3; **/ 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); } /** @@ -83,7 +87,7 @@ package com.Microsoft.Z3; { - Native.paramsSetSymbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value.NativeObject); + Native.paramsSetSymbol(Context().nCtx(), NativeObject(), Context.MkSymbol(name).NativeObject, value.NativeObject); } /** @@ -91,34 +95,34 @@ package com.Microsoft.Z3; **/ public String toString() { - return Native.paramstoString(Context.nCtx, NativeObject); + return Native.paramsToString(Context().nCtx(), NativeObject()); } Params(Context ctx) - { super(ctx, Native.mkParams(ctx.nCtx)); + { super(ctx, Native.mkParams(ctx.nCtx())); } - class DecRefQueue extends Z3.DecRefQueue + class DecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, IntPtr obj) + public void IncRef(Context ctx, long obj) { - Native.paramsIncRef(ctx.nCtx, obj); + Native.paramsIncRef(ctx.nCtx(), obj); } - public void DecRef(Context ctx, IntPtr obj) + public void DecRef(Context ctx, long obj) { - Native.paramsDecRef(ctx.nCtx, obj); + Native.paramsDecRef(ctx.nCtx(), obj); } }; - void IncRef(IntPtr o) + void IncRef(long o) { Context.Params_DRQ.IncAndClear(Context, o); super.IncRef(o); } - void DecRef(IntPtr o) + void DecRef(long 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 edc772dcf..0e87dc254 100644 --- a/src/api/java/com/Microsoft/Z3/Pattern.java +++ b/src/api/java/com/Microsoft/Z3/Pattern.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /* using System.Runtime.InteropServices; */ @@ -17,7 +21,7 @@ package com.Microsoft.Z3; /** * The number of terms in the pattern. **/ - public long NumTerms() { return Native.getPatternNumTerms(Context.nCtx, NativeObject); } + public long NumTerms() { return Native.getPatternNumTerms(Context().nCtx(), NativeObject()); } /** * The terms in the pattern. @@ -28,8 +32,8 @@ package com.Microsoft.Z3; long n = NumTerms; Expr[] res = new Expr[n]; - for (long i = 0; i < n; i++) - res[i] = Expr.Create(Context, Native.getPattern(Context.nCtx, NativeObject, i)); + for (long i; i < n; i++) + res[i] = Expr.Create(Context, Native.getPattern(Context().nCtx(), NativeObject(), i)); return res; } @@ -38,11 +42,11 @@ package com.Microsoft.Z3; **/ public String toString() { - return Native.patterntoString(Context.nCtx, NativeObject); + return Native.patternToString(Context().nCtx(), NativeObject()); } - Pattern(Context ctx, IntPtr obj) - { super(ctx, obj); + Pattern(Context ctx, long obj) + { super(ctx, obj); } } diff --git a/src/api/java/com/Microsoft/Z3/Probe.java b/src/api/java/com/Microsoft/Z3/Probe.java index 36f949966..537e9ef7f 100644 --- a/src/api/java/com/Microsoft/Z3/Probe.java +++ b/src/api/java/com/Microsoft/Z3/Probe.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /* using System.Runtime.InteropServices; */ @@ -26,45 +30,48 @@ package com.Microsoft.Z3; Context.CheckContextMatch(g); - return Native.probeApply(Context.nCtx, NativeObject, g.NativeObject); + return Native.probeApply(Context().nCtx(), NativeObject(), g.NativeObject); } /** * Apply the probe to a goal. **/ - public double this[Goal() - + public double get(Goal g) + { + - return Apply(g); } } + return Apply(g); + } - Probe(Context ctx, IntPtr obj) - { super(ctx, obj); + Probe(Context ctx, long obj) + { super(ctx, obj); + } Probe(Context ctx, String name) - { super(ctx, Native.mkProbe(ctx.nCtx, name)); + { super(ctx, Native.mkProbe(ctx.nCtx(), name)); } - class DecRefQueue extends Z3.DecRefQueue + class DecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, IntPtr obj) + public void IncRef(Context ctx, long obj) { - Native.probeIncRef(ctx.nCtx, obj); + Native.probeIncRef(ctx.nCtx(), obj); } - public void DecRef(Context ctx, IntPtr obj) + public void DecRef(Context ctx, long obj) { - Native.probeDecRef(ctx.nCtx, obj); + Native.probeDecRef(ctx.nCtx(), obj); } - }; + }; - void IncRef(IntPtr o) + void IncRef(long o) { Context.Probe_DRQ.IncAndClear(Context, o); super.IncRef(o); } - void DecRef(IntPtr o) + void DecRef(long 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 6c7c91be7..8b4df947e 100644 --- a/src/api/java/com/Microsoft/Z3/Quantifier.java +++ b/src/api/java/com/Microsoft/Z3/Quantifier.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -14,7 +18,7 @@ package com.Microsoft.Z3; /** * 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()) != 0; } /** * Indicates whether the quantifier is existential. @@ -24,12 +28,12 @@ package com.Microsoft.Z3; /** * The weight of the quantifier. **/ - public long Weight() { return Native.getQuantifierWeight(Context.nCtx, NativeObject); } + public long Weight() { return Native.getQuantifierWeight(Context().nCtx(), NativeObject()); } /** * The number of patterns. **/ - public long NumPatterns() { return Native.getQuantifierNumPatterns(Context.nCtx, NativeObject); } + public long NumPatterns() { return Native.getQuantifierNumPatterns(Context().nCtx(), NativeObject()); } /** * The patterns. @@ -40,15 +44,15 @@ package com.Microsoft.Z3; long n = NumPatterns; Pattern[] res = new Pattern[n]; - for (long i = 0; i < n; i++) - res[i] = new Pattern(Context, Native.getQuantifierPatternAst(Context.nCtx, NativeObject, i)); + for (long i; 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 long NumNoPatterns() { return Native.getQuantifierNumNoPatterns(Context().nCtx(), NativeObject()); } /** * The no-patterns. @@ -59,15 +63,15 @@ package com.Microsoft.Z3; long n = NumNoPatterns; Pattern[] res = new Pattern[n]; - for (long i = 0; i < n; i++) - res[i] = new Pattern(Context, Native.getQuantifierNoPatternAst(Context.nCtx, NativeObject, i)); + for (long i; 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 long NumBound() { return Native.getQuantifierNumBound(Context().nCtx(), NativeObject()); } /** * The symbols for the bound variables. @@ -78,8 +82,8 @@ package com.Microsoft.Z3; long n = NumBound; Symbol[] res = new Symbol[n]; - for (long i = 0; i < n; i++) - res[i] = Symbol.Create(Context, Native.getQuantifierBoundName(Context.nCtx, NativeObject, i)); + for (long i; i < n; i++) + res[i] = Symbol.Create(Context, Native.getQuantifierBoundName(Context().nCtx(), NativeObject(), i)); return res; } @@ -92,25 +96,23 @@ package com.Microsoft.Z3; long n = NumBound; Sort[] res = new Sort[n]; - for (long i = 0; i < n; i++) - res[i] = Sort.Create(Context, Native.getQuantifierBoundSort(Context.nCtx, NativeObject, i)); + for (long i; i < n; i++) + res[i] = Sort.Create(Context, Native.getQuantifierBoundSort(Context().nCtx(), NativeObject(), i)); return res; } /** * The body of the quantifier. **/ - public BoolExpr Body() { + public BoolExpr Body() + { - - return new BoolExpr(Context, Native.getQuantifierBody(Context.nCtx, NativeObject)); } - } - Quantifier(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, - long weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, - Symbol quantifierID = null, Symbol skolemID = null - ) - { super(ctx); + 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) + { super(ctx); @@ -130,18 +132,19 @@ package com.Microsoft.Z3; if (sorts.Length != names.Length) throw new Z3Exception("Number of sorts does not match number of names"); - IntPtr[] _patterns = AST.ArrayToNative(patterns); + long[] _patterns = AST.ArrayToNative(patterns); if (noPatterns == null && quantifierID == null && skolemID == null) { - NativeObject = Native.mkQuantifier(ctx.nCtx, (isForall) ? 1 : 0, weight, - AST.ArrayLength(patterns), AST.ArrayToNative(patterns), + NativeObject() = Native.mkQuantifier(ctx.nCtx(), (isForall) ? 1 : 0, weight, + AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(sorts), AST.ArrayToNative(sorts), Symbol.ArrayToNative(names), body.NativeObject); + } else { - NativeObject = Native.mkQuantifierEx(ctx.nCtx, (isForall) ? 1 : 0, weight, + NativeObject() = Native.mkQuantifierEx(ctx.nCtx(), (isForall) ? 1 : 0, weight, AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID), AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns), @@ -151,15 +154,12 @@ package com.Microsoft.Z3; } } - Quantifier(Context ctx, boolean isForall, Expr[] bound, Expr body, - long weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, - Symbol quantifierID = null, Symbol skolemID = null - ) - { super(ctx); + Quantifier(Context ctx, boolean isForall, Expr[] bound, Expr body, long weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) + { super(ctx); - + @@ -167,17 +167,17 @@ package com.Microsoft.Z3; 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) ? 1 : 0, weight, AST.ArrayLength(bound), AST.ArrayToNative(bound), AST.ArrayLength(patterns), AST.ArrayToNative(patterns), body.NativeObject); } else { - NativeObject = Native.mkQuantifierConstEx(ctx.nCtx, (isForall) ? 1 : 0, weight, + NativeObject() = Native.mkQuantifierConstEx(ctx.nCtx(), (isForall) ? 1 : 0, weight, AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID), AST.ArrayLength(bound), AST.ArrayToNative(bound), AST.ArrayLength(patterns), AST.ArrayToNative(patterns), @@ -187,11 +187,11 @@ package com.Microsoft.Z3; } - Quantifier(Context ctx, IntPtr obj) { super(ctx, obj); } + Quantifier(Context ctx, long obj) { super(ctx, obj); { }} - void CheckNativeObject(IntPtr obj) + void CheckNativeObject(long obj) { - if ((Z3_ast_kind)Native.getAstKind(Context.nCtx, obj) != Z3_ast_kind.Z3_QUANTIFIER_AST) + if ((Z3_ast_kind)Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST) throw new Z3Exception("Underlying object is not a quantifier"); super.CheckNativeObject(obj); } diff --git a/src/api/java/com/Microsoft/Z3/RatNum.java b/src/api/java/com/Microsoft/Z3/RatNum.java new file mode 100644 index 000000000..7921e70ef --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/RatNum.java @@ -0,0 +1,78 @@ +/** + * This file was automatically generated from RatNum.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; +/* using System; */ + +/* using System.Numerics; */ + + /** + * Rational Numerals + **/ + public class RatNum extends RealExpr + { + /** + * The numerator of a rational numeral. + **/ + public IntNum Numerator() + { + + + return new IntNum(Context, Native.getNumerator(Context().nCtx(), NativeObject())); + } + + /** + * The denominator of a rational numeral. + **/ + public IntNum Denominator() + { + + + return new IntNum(Context, Native.getDenominator(Context().nCtx(), NativeObject())); + } + + /** + * Converts the numerator of the rational to a BigInteger + **/ + public BigInteger BigIntNumerator() + { + IntNum n = Numerator; + return BigInteger.Parse(n.ToString()); + } + + /** + * Converts the denominator of the rational to a BigInteger + **/ + public BigInteger BigIntDenominator() + { + IntNum n = Denominator; + return BigInteger.Parse(n.ToString()); + } + + /** + * Returns a string representation in decimal notation. + * The result has at most decimal places. + **/ + public String ToDecimalString(long precision) + { + return Native.getNumeralDecimalString(Context().nCtx(), NativeObject(), precision); + } + + /** + * Returns a string representation of the numeral. + **/ + public String toString() + { + return Native.getNumeralString(Context().nCtx(), NativeObject()); + } + + RatNum(Context ctx, long obj) + { super(ctx, obj); + + } + } diff --git a/src/api/java/com/Microsoft/Z3/RealExpr.java b/src/api/java/com/Microsoft/Z3/RealExpr.java new file mode 100644 index 000000000..8f2b139bd --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/RealExpr.java @@ -0,0 +1,31 @@ +/** + * This file was automatically generated from RealExpr.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; +/* using System; */ +/* using System.Collections.Generic; */ +/* using System.Linq; */ +/* using System.Text; */ + + + /** + * Real expressions + **/ + public class RealExpr extends ArithExpr + { + /** Constructor for RealExpr + **/ + protected RealExpr(Context ctx) + { super(ctx); + + } + RealExpr(Context ctx, long obj) + { super(ctx, obj); + + } + } diff --git a/src/api/java/com/Microsoft/Z3/RealSort.java b/src/api/java/com/Microsoft/Z3/RealSort.java new file mode 100644 index 000000000..39aa849ab --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/RealSort.java @@ -0,0 +1,26 @@ +/** + * This file was automatically generated from RealSort.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ + + /** + * A real sort + **/ + public class RealSort extends ArithSort + { + RealSort(Context ctx, long obj) + { super(ctx, obj); + + } + RealSort(Context ctx) + { super(ctx, Native.mkRealSort(ctx.nCtx())); + + } + } diff --git a/src/api/java/com/Microsoft/Z3/RelationSort.java b/src/api/java/com/Microsoft/Z3/RelationSort.java new file mode 100644 index 000000000..3948e1651 --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/RelationSort.java @@ -0,0 +1,46 @@ +/** + * This file was automatically generated from RelationSort.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ + + /** + * Relation sorts. + **/ + public class RelationSort extends Sort + { + /** + * The arity of the relation sort. + **/ + public long Arity() { return Native.getRelationArity(Context().nCtx(), NativeObject()); } + + /** + * The sorts of the columns of the relation sort. + **/ + public Sort[] ColumnSorts() + { + + + if (m_columnSorts != null) + return m_columnSorts; + + long n = Arity; + Sort[] res = new Sort[n]; + for (long i; i < n; i++) + res[i] = Sort.Create(Context, Native.getRelationColumn(Context().nCtx(), NativeObject(), i)); + return res; + } + + private Sort[] m_columnSorts = null; + + RelationSort(Context ctx, long obj) + { super(ctx, obj); + + } + } diff --git a/src/api/java/com/Microsoft/Z3/SetSort.java b/src/api/java/com/Microsoft/Z3/SetSort.java new file mode 100644 index 000000000..2f008f4db --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/SetSort.java @@ -0,0 +1,27 @@ +/** + * This file was automatically generated from SetSort.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ + + /** + * Set sorts. + **/ + public class SetSort extends Sort + { + SetSort(Context ctx, long obj) + { super(ctx, obj); + + } + SetSort(Context ctx, Sort ty) + { 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 787e115ab..a206114f1 100644 --- a/src/api/java/com/Microsoft/Z3/Solver.java +++ b/src/api/java/com/Microsoft/Z3/Solver.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -18,7 +22,7 @@ package com.Microsoft.Z3; { - return Native.solverGetHelp(Context.nCtx, NativeObject); + return Native.solverGetHelp(Context().nCtx(), NativeObject()); } /** @@ -29,13 +33,13 @@ package com.Microsoft.Z3; Context.CheckContextMatch(value); - Native.solverSetParams(Context.nCtx, NativeObject, value.NativeObject); + 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())); } /** @@ -43,7 +47,7 @@ package com.Microsoft.Z3; * * **/ - public long NumScopes() { return Native.solverGetNumScopes(Context.nCtx, NativeObject); } + public long NumScopes() { return Native.solverGetNumScopes(Context().nCtx(), NativeObject()); } /** * Creates a backtracking point. @@ -51,7 +55,7 @@ package com.Microsoft.Z3; **/ public void Push() { - Native.solverPush(Context.nCtx, NativeObject); + Native.solverPush(Context().nCtx(), NativeObject()); } /** @@ -61,7 +65,7 @@ package com.Microsoft.Z3; **/ public void Pop(long n) { - Native.solverPop(Context.nCtx, NativeObject, n); + Native.solverPop(Context().nCtx(), NativeObject(), n); } /** @@ -70,7 +74,7 @@ package com.Microsoft.Z3; **/ public void Reset() { - Native.solverReset(Context.nCtx, NativeObject); + Native.solverReset(Context().nCtx(), NativeObject()); } /** @@ -82,9 +86,9 @@ package com.Microsoft.Z3; Context.CheckContextMatch(constraints); - for (BoolExpr.Iterator a = constraints.iterator(); a.hasNext(); ) + for (Iterator a = constraints.iterator(); a.hasNext(); ) { - Native.solverAssert(Context.nCtx, NativeObject, a.NativeObject); + Native.solverAssert(Context().nCtx(), NativeObject(), a.NativeObject); } } @@ -93,7 +97,7 @@ package com.Microsoft.Z3; **/ public long NumAssertions() { - ASTVector ass = new ASTVector(Context, Native.solverGetAssertions(Context.nCtx, NativeObject)); + ASTVector ass = new ASTVector(Context, Native.solverGetAssertions(Context().nCtx(), NativeObject())); return ass.Size; } @@ -104,10 +108,10 @@ package com.Microsoft.Z3; { - ASTVector ass = new ASTVector(Context, Native.solverGetAssertions(Context.nCtx, NativeObject)); + ASTVector ass = new ASTVector(Context, Native.solverGetAssertions(Context().nCtx(), NativeObject())); long n = ass.Size; BoolExpr[] res = new BoolExpr[n]; - for (long i = 0; i < n; i++) + for (long i; i < n; i++) res[i] = new BoolExpr(Context, ass[i].NativeObject); return res; } @@ -122,15 +126,15 @@ package com.Microsoft.Z3; **/ public Status Check(Expr[] assumptions) { - Z3_lboolean r; + Z3_lbool r; if (assumptions == null) - r = (Z3_lboolean)Native.solverCheck(Context.nCtx, NativeObject); + r = (Z3_lbool)Native.solverCheck(Context().nCtx(), NativeObject()); else - r = (Z3_lboolean)Native.solverCheckAssumptions(Context.nCtx, NativeObject, (long)assumptions.Length, AST.ArrayToNative(assumptions)); + r = (Z3_lbool)Native.solverCheckAssumptions(Context().nCtx(), NativeObject(), (long)assumptions.Length, AST.ArrayToNative(assumptions)); switch (r) { - case Z3_lboolean.Z3_L_TRUE: return Status.SATISFIABLE; - case Z3_lboolean.Z3_L_FALSE: return Status.UNSATISFIABLE; + case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE; + case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE; default: return Status.UNKNOWN; } } @@ -144,8 +148,8 @@ package com.Microsoft.Z3; **/ public Model Model() { - IntPtr x = Native.solverGetModel(Context.nCtx, NativeObject); - if (x == IntPtr.Zero) + long x = Native.solverGetModel(Context().nCtx(), NativeObject()); + if (x == 0) return null; else return new Model(Context, x); @@ -160,8 +164,8 @@ package com.Microsoft.Z3; **/ public Expr Proof() { - IntPtr x = Native.solverGetProof(Context.nCtx, NativeObject); - if (x == IntPtr.Zero) + long x = Native.solverGetProof(Context().nCtx(), NativeObject()); + if (x == 0) return null; else return Expr.Create(Context, x); @@ -179,10 +183,10 @@ package com.Microsoft.Z3; { - ASTVector core = new ASTVector(Context, Native.solverGetUnsatCore(Context.nCtx, NativeObject)); + ASTVector core = new ASTVector(Context, Native.solverGetUnsatCore(Context().nCtx(), NativeObject())); long n = core.Size; Expr[] res = new Expr[n]; - for (long i = 0; i < n; i++) + for (long i; i < n; i++) res[i] = Expr.Create(Context, core[i].NativeObject); return res; } @@ -194,7 +198,7 @@ package com.Microsoft.Z3; { - return Native.solverGetReasonUnknown(Context.nCtx, NativeObject); + return Native.solverGetReasonUnknown(Context().nCtx(), NativeObject()); } /** @@ -204,7 +208,7 @@ package com.Microsoft.Z3; { - return new Statistics(Context, Native.solverGetStatistics(Context.nCtx, NativeObject)); + return new Statistics(Context, Native.solverGetStatistics(Context().nCtx(), NativeObject())); } /** @@ -212,34 +216,34 @@ package com.Microsoft.Z3; **/ public String toString() { - return Native.solvertoString(Context.nCtx, NativeObject); + return Native.solverToString(Context().nCtx(), NativeObject()); } - Solver(Context ctx, IntPtr obj) - { super(ctx, obj); + Solver(Context ctx, long obj) + { super(ctx, obj); } - class DecRefQueue extends Z3.DecRefQueue + class DecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, IntPtr obj) + public void IncRef(Context ctx, long obj) { - Native.solverIncRef(ctx.nCtx, obj); + Native.solverIncRef(ctx.nCtx(), obj); } - public void DecRef(Context ctx, IntPtr obj) + public void DecRef(Context ctx, long obj) { - Native.solverDecRef(ctx.nCtx, obj); + Native.solverDecRef(ctx.nCtx(), obj); } }; - void IncRef(IntPtr o) + void IncRef(long o) { Context.Solver_DRQ.IncAndClear(Context, o); super.IncRef(o); } - void DecRef(IntPtr o) + void DecRef(long 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 8e4735389..d328071dd 100644 --- a/src/api/java/com/Microsoft/Z3/Sort.java +++ b/src/api/java/com/Microsoft/Z3/Sort.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -34,9 +38,9 @@ package com.Microsoft.Z3; * * @return **/ - public boolean Equals(object o) + public boolean Equals(Object o) { - Sort casted = o as Sort; + Sort casted = (Sort) o; if (casted == null) return false; return this == casted; } @@ -53,47 +57,49 @@ package com.Microsoft.Z3; /** * Returns a unique identifier for the sort. **/ - public long Id() { return Native.getSortId(Context.nCtx, NativeObject); } + public long 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)Native.getSortKind(Context().nCtx(), NativeObject()); } /** * The name of the sort **/ - public Symbol Name() { + public Symbol Name() + { - return Symbol.Create(Context, Native.getSortName(Context.nCtx, NativeObject)); } - } + return Symbol.Create(Context, Native.getSortName(Context().nCtx(), NativeObject())); + } /** * A string representation of the sort. **/ public String toString() { - return Native.sorttoString(Context.nCtx, NativeObject); + return Native.sortToString(Context().nCtx(), NativeObject()); + } /** * Sort constructor **/ - protected Sort(Context ctx) { super(ctx); } - Sort(Context ctx, IntPtr obj) { super(ctx, obj); } + protected Sort(Context ctx) { super(ctx); { }} + Sort(Context ctx, long obj) { super(ctx, obj); { }} - void CheckNativeObject(IntPtr obj) + void CheckNativeObject(long obj) { - if (Native.getAstKind(Context.nCtx, obj) != (long)Z3_ast_kind.Z3_SORT_AST) + if (Native.getAstKind(Context().nCtx(), obj) != (long)Z3_ast_kind.Z3_SORT_AST) throw new Z3Exception("Underlying object is not a sort"); super.CheckNativeObject(obj); } - static Sort Create(Context ctx, IntPtr obj) + static Sort Create(Context ctx, long obj) { - switch ((Z3_sort_kind)Native.getSortKind(ctx.nCtx, obj)) + switch ((Z3_sort_kind)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); @@ -108,476 +114,4 @@ package com.Microsoft.Z3; throw new Z3Exception("Unknown sort kind"); } } - } - - /** - * A Boolean sort. - **/ - public class BoolSort extends Sort - { - BoolSort(Context ctx, IntPtr obj) { super(ctx, obj); } - BoolSort(Context ctx) { super(ctx, Native.mkBooleanSort(ctx.nCtx)); } - }; - - /** - * An arithmetic sort, i.e., Int or Real. - **/ - public class ArithSort extends Sort - { - ArithSort(Context ctx, IntPtr obj) { super(ctx, obj); } - }; - - /** - * An Integer sort - **/ - public class IntSort extends ArithSort - { - IntSort(Context ctx, IntPtr obj) - { super(ctx, obj); - - } - IntSort(Context ctx) - { super(ctx, Native.mkIntSort(ctx.nCtx)); - - } - } - - /** - * A real sort - **/ - public class RealSort extends ArithSort - { - RealSort(Context ctx, IntPtr obj) - { super(ctx, obj); - - } - RealSort(Context ctx) - { super(ctx, Native.mkRealSort(ctx.nCtx)); - - } - } - - /** - * Bit-vector sorts. - **/ - public class BitVecSort extends Sort - { - /** - * The size of the bit-vector sort. - **/ - public long Size() { return Native.getBvSortSize(Context.nCtx, NativeObject); } - - BitVecSort(Context ctx, IntPtr obj) { super(ctx, obj); } - BitVecSort(Context ctx, long size) { super(ctx, Native.mkBvSort(ctx.nCtx, size)); } - }; - - /** - * Array sorts. - **/ - public class ArraySort extends Sort - { - /** - * The domain of the array sort. - **/ - public Sort Domain() { - - - return Sort.Create(Context, Native.getArraySortDomain(Context.nCtx, NativeObject)); } - } - - /** - * The range of the array sort. - **/ - public Sort Range() { - - - return Sort.Create(Context, Native.getArraySortRange(Context.nCtx, NativeObject)); } - } - - ArraySort(Context ctx, IntPtr obj) { super(ctx, obj); } - ArraySort(Context ctx, Sort domain, Sort range) - { super(ctx, Native.mkArraySort(ctx.nCtx, domain.NativeObject, range.NativeObject)); - - - - }; - - /** - * Datatype sorts. - **/ - public class DatatypeSort extends Sort - { - /** - * The number of constructors of the datatype sort. - **/ - public long NumConstructors() { return Native.getDatatypeSortNumConstructors(Context.nCtx, NativeObject); } - - /** - * The constructors. - **/ - public FuncDecl[] Constructors() - { - - - long n = NumConstructors; - FuncDecl[] res = new FuncDecl[n]; - for (long i = 0; i < n; i++) - res[i] = new FuncDecl(Context, Native.getDatatypeSortConstructor(Context.nCtx, NativeObject, i)); - return res; - } - - /** - * The recognizers. - **/ - public FuncDecl[] Recognizers() - { - - - long n = NumConstructors; - FuncDecl[] res = new FuncDecl[n]; - for (long i = 0; i < n; i++) - res[i] = new FuncDecl(Context, Native.getDatatypeSortRecognizer(Context.nCtx, NativeObject, i)); - return res; - } - - /** - * The constructor accessors. - **/ - public FuncDecl[][] Accessors() - { - - - long n = NumConstructors; - FuncDecl[][] res = new FuncDecl[n][]; - for (long i = 0; i < n; i++) - { - FuncDecl fd = new FuncDecl(Context, Native.getDatatypeSortConstructor(Context.nCtx, NativeObject, i)); - long ds = fd.DomainSize; - FuncDecl[] tmp = new FuncDecl[ds]; - for (long j = 0; j < ds; j++) - tmp[j] = new FuncDecl(Context, Native.getDatatypeSortConstructorAccessor(Context.nCtx, NativeObject, i, j)); - res[i] = tmp; - } - return res; - } - - DatatypeSort(Context ctx, IntPtr obj) { super(ctx, obj); } - - DatatypeSort(Context ctx, Symbol name, Constructor[] constructors) - { super(ctx, Native.mkDatatype(ctx.nCtx, name.NativeObject, (long)constructors.Length, ArrayToNative(constructors))); - - - - } - }; - - /** - * Uninterpreted Sorts - **/ - public class UninterpretedSort extends Sort - { - UninterpretedSort(Context ctx, IntPtr obj) - { super(ctx, obj); - - } - UninterpretedSort(Context ctx, Symbol s) - { super(ctx, Native.mkUninterpretedSort(ctx.nCtx, s.NativeObject)); - - - } - } - - /** - * Tuple sorts. - **/ - public class TupleSort extends Sort - { - /** - * The constructor function of the tuple. - **/ - public FuncDecl MkDecl() { - - - 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); } - - /** - * The field declarations. - **/ - public FuncDecl[] FieldDecls() - { - - - long n = NumFields; - FuncDecl[] res = new FuncDecl[n]; - for (long 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) - { super(ctx); - - - - IntPtr t = IntPtr.Zero; - NativeObject = Native.mkTupleSort(ctx.nCtx, name.NativeObject, numFields, - Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts), - t, new IntPtr[numFields]); - } - }; - - /** - * Enumeration sorts. - **/ - public class EnumSort extends Sort - { - /** - * The function declarations of the constants in the enumeration. - **/ - public FuncDecl[] ConstDecls() { - - - return _constdecls; } - } - - /** - * The constants in the enumeration. - **/ - public Expr[] Consts() { - - - return _consts; } - } - - /** - * The test predicates for the constants in the enumeration. - **/ - public FuncDecl[] TesterDecls() { - - - return _testerdecls; - } - - - private void ObjectInvariant() - { - - - - } - - - - private FuncDecl[] _constdecls = null, _testerdecls = null; - private Expr[] _consts = null; - - EnumSort(Context ctx, Symbol name, Symbol[] enumNames) - { super(ctx); - - - - - int n = enumNames.Length; - IntPtr[] n_constdecls = new IntPtr[n]; - IntPtr[] n_testers = new IntPtr[n]; - NativeObject = Native.mkEnumerationSort(ctx.nCtx, name.NativeObject, (long)n, - Symbol.ArrayToNative(enumNames), n_constdecls, n_testers); - _constdecls = new FuncDecl[n]; - for (long i = 0; i < n; i++) - _constdecls[i] = new FuncDecl(ctx, n_constdecls[i]); - _testerdecls = new FuncDecl[n]; - for (long i = 0; i < n; i++) - _testerdecls[i] = new FuncDecl(ctx, n_testers[i]); - _consts = new Expr[n]; - for (long i = 0; i < n; i++) - _consts[i] = ctx.MkApp(_constdecls[i]); - } - }; - - /** - * List sorts. - **/ - public class ListSort extends Sort - { - /** - * The declaration of the nil function of this list sort. - **/ - public FuncDecl NilDecl() - - return nilDecl; } } - - /** - * The empty list. - **/ - public Expr Nil() - { - - return nilConst; - } - - /** - * The declaration of the isNil function of this list sort. - **/ - public FuncDecl IsNilDecl() - { - - return isNilDecl; - } - - /** - * The declaration of the cons function of this list sort. - **/ - public FuncDecl ConsDecl() - { - - return consDecl; - } - - /** - * The declaration of the isCons function of this list sort. - * - **/ - public FuncDecl IsConsDecl() - { - - return isConsDecl; - } - - /** - * The declaration of the head function of this list sort. - **/ - public FuncDecl HeadDecl() - { - - return headDecl; - } - - /** - * The declaration of the tail function of this list sort. - **/ - public FuncDecl TailDecl() - { - - return tailDecl; - } - - - private void ObjectInvariant() - { - - - - - - - - } - - - - private FuncDecl nilDecl, isNilDecl, consDecl, isConsDecl, headDecl, tailDecl; - private Expr nilConst; - - ListSort(Context ctx, Symbol name, Sort elemSort) - { super(ctx); - - - - - IntPtr inil = IntPtr.Zero, - iisnil = IntPtr.Zero, - icons = IntPtr.Zero, - iiscons = IntPtr.Zero, - ihead = IntPtr.Zero, - itail = IntPtr.Zero; - - 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); - consDecl = new FuncDecl(ctx, icons); - isConsDecl = new FuncDecl(ctx, iiscons); - headDecl = new FuncDecl(ctx, ihead); - tailDecl = new FuncDecl(ctx, itail); - nilConst = ctx.MkConst(nilDecl); - } - }; - - /** - * Relation sorts. - **/ - public class RelationSort extends Sort - { - /** - * The arity of the relation sort. - **/ - public long Arity() { return Native.getRelationArity(Context.nCtx, NativeObject); } - - /** - * The sorts of the columns of the relation sort. - **/ - public Sort[] ColumnSorts() - { - - - if (m_columnSorts != null) - return m_columnSorts; - - long n = Arity; - Sort[] res = new Sort[n]; - for (long i = 0; i < n; i++) - res[i] = Sort.Create(Context, Native.getRelationColumn(Context.nCtx, NativeObject, i)); - return res; - } - - private Sort[] m_columnSorts = null; - - RelationSort(Context ctx, IntPtr obj) - { super(ctx, obj); - - } - } - - /** - * Finite domain sorts. - **/ - public class FiniteDomainSort extends Sort - { - /** - * The size of the finite domain sort. - **/ - public ulong Size() { ulong res = 0; Native.getFiniteDomainSortSize(Context.nCtx, NativeObject, ref res); return res; } - - FiniteDomainSort(Context ctx, IntPtr obj) - { super(ctx, obj); - - } - FiniteDomainSort(Context ctx, Symbol name, ulong size) - { super(ctx, Native.mkFiniteDomainSort(ctx.nCtx, name.NativeObject, size)); - - - - } - } - - /** - * Set sorts. - **/ - public class SetSort extends Sort - { - SetSort(Context ctx, IntPtr obj) - { super(ctx, obj); - - } - SetSort(Context ctx, Sort ty) - { super(ctx, Native.mkSetSort(ctx.nCtx, ty.NativeObject)); - - - } - } + } diff --git a/src/api/java/com/Microsoft/Z3/Statistics.java b/src/api/java/com/Microsoft/Z3/Statistics.java index d9aac9d67..d0f4021ed 100644 --- a/src/api/java/com/Microsoft/Z3/Statistics.java +++ b/src/api/java/com/Microsoft/Z3/Statistics.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -45,9 +49,9 @@ package com.Microsoft.Z3; if (IsUInt) - return m_long.toString(); + return m_long.ToString(); else if (IsDouble) - return m_double.toString(); + return m_double.ToString(); else throw new Z3Exception("Unknown statistical entry type"); } @@ -64,8 +68,18 @@ package com.Microsoft.Z3; private boolean m_is_double = false; private long m_long = 0; private double m_double = 0.0; - Entry(String k, long v) { Key = k; m_is_long = true; m_long = v; } - Entry(String k, double v) { Key = k; m_is_double = true; m_double = v; } + Entry(String k, long v) + { + Key = k; + m_is_long = true; + m_long = v; + } + Entry(String k, double v) + { + Key = k; + m_is_double = true; + m_double = v; + } } /** @@ -73,13 +87,13 @@ package com.Microsoft.Z3; **/ public String toString() { - return Native.statstoString(Context.nCtx, NativeObject); + return Native.statsToString(Context().nCtx(), NativeObject()); } /** * The number of statistical data. **/ - public long Size() { return Native.statsSize(Context.nCtx, NativeObject); } + public long Size() { return Native.statsSize(Context().nCtx(), NativeObject()); } /** * The data entries. @@ -92,14 +106,14 @@ package com.Microsoft.Z3; long n = Size; Entry[] res = new Entry[n]; - for (long i = 0; i < n; i++) + for (long i; 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) - e = new Entry(k, Native.statsGetDoubleValue(Context.nCtx, NativeObject, i)); + 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) + e = new Entry(k, Native.statsGetDoubleValue(Context().nCtx(), NativeObject(), i)); else throw new Z3Exception("Unknown data entry value"); res[i] = e; @@ -116,8 +130,8 @@ package com.Microsoft.Z3; long n = Size; String[] res = new String[n]; - for (long i = 0; i < n; i++) - res[i] = Native.statsGetKey(Context.nCtx, NativeObject, i); + for (long i; i < n; i++) + res[i] = Native.statsGetKey(Context().nCtx(), NativeObject(), i); return res; } @@ -129,37 +143,37 @@ package com.Microsoft.Z3; { long n = Size; Entry[] es = Entries; - for (long i = 0; i < n; i++) + for (long i; i < n; i++) if (es[i].Key == key) return es[i]; return null; } - Statistics(Context ctx, IntPtr obj) - { super(ctx, obj); + Statistics(Context ctx, long obj) + { super(ctx, obj); } - class DecRefQueue extends Z3.DecRefQueue + class DecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, IntPtr obj) + public void IncRef(Context ctx, long obj) { - Native.statsIncRef(ctx.nCtx, obj); + Native.statsIncRef(ctx.nCtx(), obj); } - public void DecRef(Context ctx, IntPtr obj) + public void DecRef(Context ctx, long obj) { - Native.statsDecRef(ctx.nCtx, obj); + Native.statsDecRef(ctx.nCtx(), obj); } }; - void IncRef(IntPtr o) + void IncRef(long o) { Context.Statistics_DRQ.IncAndClear(Context, o); super.IncRef(o); } - void DecRef(IntPtr o) + void DecRef(long 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 86c902285..9eb75060c 100644 --- a/src/api/java/com/Microsoft/Z3/Status.java +++ b/src/api/java/com/Microsoft/Z3/Status.java @@ -4,23 +4,30 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** * Status values. **/ - /** - * Used to signify an unsatisfiable status. - **/ - UNSATISFIABLE = -1, + public enum Status + { + /// + /// Used to signify an unsatisfiable status. + /// + UNSATISFIABLE (1), - /** - * Used to signify an unknown status. - **/ - UNKNOWN = 0, + /// + /// Used to signify an unknown status. + /// + UNKNOWN (0), - /** - * Used to signify a satisfiable status. - **/ - SATISFIABLE = 1 + /// + /// Used to signify a satisfiable status. + /// + SATISFIABLE (1) + } diff --git a/src/api/java/com/Microsoft/Z3/StringSymbol.java b/src/api/java/com/Microsoft/Z3/StringSymbol.java new file mode 100644 index 000000000..27157599d --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/StringSymbol.java @@ -0,0 +1,50 @@ +/** + * This file was automatically generated from StringSymbol.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ +/* using System.Runtime.InteropServices; */ + + + /** + * Named symbols + **/ + public class StringSymbol extends Symbol + { + /** + * The string value of the symbol. + * Throws an exception if the symbol is not of string kind. + **/ + public String String() + { + + + if (!IsStringSymbol()) + throw new Z3Exception("String requested from non-String symbol"); + return Native.getSymbolString(Context().nCtx(), NativeObject()); + } + + StringSymbol(Context ctx, long obj) + { super(ctx, obj); + + } + + StringSymbol(Context ctx, String s) + { super(ctx, Native.mkStringSymbol(ctx.nCtx(), s)); + + } + + void CheckNativeObject(long obj) + { + if ((Z3_symbol_kind)Native.getSymbolKind(Context().nCtx(), obj) != Z3_symbol_kind.Z3_STRING_SYMBOL) + throw new Z3Exception("Symbol is not of String kind"); + + super.CheckNativeObject(obj); + } + } diff --git a/src/api/java/com/Microsoft/Z3/Symbol.java b/src/api/java/com/Microsoft/Z3/Symbol.java index 972999e66..54caf9f1c 100644 --- a/src/api/java/com/Microsoft/Z3/Symbol.java +++ b/src/api/java/com/Microsoft/Z3/Symbol.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /* using System.Runtime.InteropServices; */ @@ -15,10 +19,7 @@ package com.Microsoft.Z3; /** * The kind of the symbol (int or string) **/ - protected Z3_symbol_kind Kind - { - get { return (Z3_symbol_kind)Native.getSymbolKind(Context.nCtx, NativeObject); } - } + protected Z3_symbol_kind Kind() { return (Z3_symbol_kind)Native.getSymbolKind(Context().nCtx(), NativeObject()); } /** * Indicates whether the symbol is of Int kind @@ -42,7 +43,7 @@ package com.Microsoft.Z3; public String toString() { if (IsIntSymbol()) - return ((IntSymbol)this).Int.toString(); + return ((IntSymbol)this).Int.ToString(); else if (IsStringSymbol()) return ((StringSymbol)this).String; else @@ -52,16 +53,16 @@ package com.Microsoft.Z3; /** * Symbol constructor **/ - protected Symbol(Context ctx, IntPtr obj) { super(ctx, obj); + protected Symbol(Context ctx, long obj) { super(ctx, obj); } - static Symbol Create(Context ctx, IntPtr obj) + static Symbol Create(Context ctx, long obj) { - switch ((Z3_symbol_kind)Native.getSymbolKind(ctx.nCtx, obj)) + switch ((Z3_symbol_kind)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); @@ -70,71 +71,3 @@ package com.Microsoft.Z3; } } } - - /** - * Numbered symbols - **/ - public class IntSymbol extends Symbol - { - /** - * The int value of the symbol. - * Throws an exception if the symbol is not of int kind. - **/ - public int Int() - { - if (!IsIntSymbol()) - throw new Z3Exception("Int requested from non-Int symbol"); - return Native.getSymbolInt(Context.nCtx, NativeObject); - } - - IntSymbol(Context ctx, IntPtr obj) - { super(ctx, obj); - - } - IntSymbol(Context ctx, int i) - { super(ctx, Native.mkIntSymbol(ctx.nCtx, i)); - - } - - void CheckNativeObject(IntPtr obj) - { - if ((Z3_symbol_kind)Native.getSymbolKind(Context.nCtx, obj) != Z3_symbol_kind.Z3_INT_SYMBOL) - throw new Z3Exception("Symbol is not of integer kind"); - super.CheckNativeObject(obj); - } - } - - /** - * Named symbols - **/ - public class StringSymbol extends Symbol - { - /** - * The string value of the symbol. - * Throws an exception if the symbol is not of string kind. - **/ - public String String() - { - - - if (!IsStringSymbol()) - throw new Z3Exception("String requested from non-String symbol"); - return Native.getSymbolString(Context.nCtx, NativeObject); - } - - StringSymbol(Context ctx, IntPtr obj) { super(ctx, obj); - - } - - StringSymbol(Context ctx, String s) { super(ctx, Native.mkStringSymbol(ctx.nCtx, s)); - - } - - void CheckNativeObject(IntPtr obj) - { - if ((Z3_symbol_kind)Native.getSymbolKind(Context.nCtx, obj) != Z3_symbol_kind.Z3_STRING_SYMBOL) - throw new Z3Exception("Symbol is not of String kind"); - - super.CheckNativeObject(obj); - } - } diff --git a/src/api/java/com/Microsoft/Z3/Tactic.java b/src/api/java/com/Microsoft/Z3/Tactic.java index ae74c3a6b..275205be5 100644 --- a/src/api/java/com/Microsoft/Z3/Tactic.java +++ b/src/api/java/com/Microsoft/Z3/Tactic.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -21,14 +25,14 @@ package com.Microsoft.Z3; { - return Native.tacticGetHelp(Context.nCtx, NativeObject); + return Native.tacticGetHelp(Context().nCtx(), NativeObject()); } /** * 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())); } /** @@ -41,11 +45,11 @@ package com.Microsoft.Z3; 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)); + return new ApplyResult(Context, Native.tacticApplyEx(Context().nCtx(), NativeObject(), g.NativeObject, p.NativeObject)); } } @@ -71,35 +75,35 @@ package com.Microsoft.Z3; return Context.MkSolver(this); } - Tactic(Context ctx, IntPtr obj) - { super(ctx, obj); + Tactic(Context ctx, long obj) + { super(ctx, obj); } Tactic(Context ctx, String name) - { super(ctx, Native.mkTactic(ctx.nCtx, name)); + { super(ctx, Native.mkTactic(ctx.nCtx(), name)); } - class DecRefQueue extends Z3.DecRefQueue + class DecRefQueue extends IDecRefQueue { - public void IncRef(Context ctx, IntPtr obj) + public void IncRef(Context ctx, long obj) { - Native.tacticIncRef(ctx.nCtx, obj); + Native.tacticIncRef(ctx.nCtx(), obj); } - public void DecRef(Context ctx, IntPtr obj) + public void DecRef(Context ctx, long obj) { - Native.tacticDecRef(ctx.nCtx, obj); + Native.tacticDecRef(ctx.nCtx(), obj); } }; - void IncRef(IntPtr o) + void IncRef(long o) { Context.Tactic_DRQ.IncAndClear(Context, o); super.IncRef(o); } - void DecRef(IntPtr o) + void DecRef(long 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 new file mode 100644 index 000000000..2e682343a --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/TupleSort.java @@ -0,0 +1,57 @@ +/** + * This file was automatically generated from TupleSort.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ + + /** + * Tuple sorts. + **/ + public class TupleSort extends Sort + { + /** + * The constructor function of the tuple. + **/ + public FuncDecl MkDecl() + { + + + 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()); } + + /** + * The field declarations. + **/ + public FuncDecl[] FieldDecls() + { + + + long n = NumFields; + FuncDecl[] res = new FuncDecl[n]; + for (long i; 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) + { super(ctx); + + + + long t = 0; + 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 new file mode 100644 index 000000000..f8b91103c --- /dev/null +++ b/src/api/java/com/Microsoft/Z3/UninterpretedSort.java @@ -0,0 +1,27 @@ +/** + * This file was automatically generated from UninterpretedSort.cs + **/ + +package com.Microsoft.Z3; + +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + +/* using System; */ + + /** + * Uninterpreted Sorts + **/ + public class UninterpretedSort extends Sort + { + UninterpretedSort(Context ctx, long obj) + { super(ctx, obj); + + } + UninterpretedSort(Context ctx, Symbol s) + { 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 8038f02d5..ecf451e2f 100644 --- a/src/api/java/com/Microsoft/Z3/Version.java +++ b/src/api/java/com/Microsoft/Z3/Version.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -63,6 +67,6 @@ package com.Microsoft.Z3; long 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 0e05add87..0bca047ab 100644 --- a/src/api/java/com/Microsoft/Z3/Z3Exception.java +++ b/src/api/java/com/Microsoft/Z3/Z3Exception.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -14,15 +18,15 @@ package com.Microsoft.Z3; /** * Constructor. **/ - public Z3Exception() { super(); } +public Z3Exception() { super(); { }} /** * Constructor. **/ - public Z3Exception(String message) { super(message); } +public Z3Exception(String message) { super(message); { }} /** * Constructor. **/ - public Z3Exception(String message, System.Exception inner) { super(message, inner); } +public Z3Exception(String message, Exception inner) { super(message, inner); { }} } diff --git a/src/api/java/com/Microsoft/Z3/Z3Object.java b/src/api/java/com/Microsoft/Z3/Z3Object.java index ca4258980..6a8392a86 100644 --- a/src/api/java/com/Microsoft/Z3/Z3Object.java +++ b/src/api/java/com/Microsoft/Z3/Z3Object.java @@ -4,6 +4,10 @@ package com.Microsoft.Z3; +import java.math.BigInteger; +import java.util.*; +import java.lang.Exception; + /* using System; */ /** @@ -25,21 +29,21 @@ package com.Microsoft.Z3; **/ public void Dispose() { - if (m_n_obj != IntPtr.Zero) + if (m_n_obj != 0) { DecRef(m_n_obj); - m_n_obj = IntPtr.Zero; + m_n_obj = 0; } if (m_ctx != null) { m_ctx.refCount--; if (m_ctx.refCount == 0) - GC.ReRegisterForFinalize(m_ctx); + m_ctx = null; } - GC.SuppressFinalize(this); + } @@ -50,7 +54,7 @@ package com.Microsoft.Z3; private Context m_ctx = null; - private IntPtr m_n_obj = IntPtr.Zero; + private long m_n_obj = 0; Z3Object(Context ctx) { @@ -60,7 +64,7 @@ package com.Microsoft.Z3; m_ctx = ctx; } - Z3Object(Context ctx, IntPtr obj) + Z3Object(Context ctx, long obj) { @@ -70,46 +74,40 @@ package com.Microsoft.Z3; m_n_obj = obj; } - void IncRef(IntPtr o) { } - void DecRef(IntPtr o) { } + void IncRef(long o) { } + void DecRef(long o) { } - void CheckNativeObject(IntPtr obj) { } + void CheckNativeObject(long obj) { } - IntPtr NativeObject - { - get { return m_n_obj; } - set + long NativeObject() { return m_n_obj; } + void setNativeObject(long value) { - if (value != IntPtr.Zero) { CheckNativeObject(value); IncRef(value); } - if (m_n_obj != IntPtr.Zero) { DecRef(m_n_obj); } + if (value != 0) { CheckNativeObject(value); IncRef(value); } + if (m_n_obj != 0) { DecRef(m_n_obj); } m_n_obj = value; } + + static long GetNativeObject(Z3Object s) + { + if (s == null) return 0; + return s.NativeObject(); } - static IntPtr GetNativeObject(Z3Object s) - { - if (s == null) return new IntPtr(); - return s.NativeObject; - } - - Context Context - { - get + Context Context() { return m_ctx; } - } - static IntPtr[] ArrayToNative(Z3Object[] a) + static long[] ArrayToNative(Z3Object[] a) { if (a == null) return null; - IntPtr[] an = new IntPtr[a.Length]; - for (long i = 0; i < a.Length; i++) - if (a[i] != null) an[i] = a[i].NativeObject; + long[] an = new long[a.Length]; + for (long i; i < a.Length; i++) + if (a[i] != null) an[i] = a[i].NativeObject(); return an; } diff --git a/src/api/java/mk_java.py b/src/api/java/mk_java.py index a2cc51274..81b4a08b6 100644 --- a/src/api/java/mk_java.py +++ b/src/api/java/mk_java.py @@ -29,9 +29,17 @@ def subst_getters(s, getters): s = s.replace(g, g + "()") def type_replace(s): - s = s.replace("bool", "boolean") + s = s.replace(" bool", " boolean") + s = s.replace("(bool", "(boolean") s = s.replace("uint", "long") + 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("System.Exception", "Exception") return s def rename_native(s): @@ -47,6 +55,13 @@ def rename_native(s): s = c0 + c1 + c2 return s +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("ASTKind", "ASTKind()", a) + return a def translate(filename): tgtfn = OUTDIR + filename.replace(EXT, ".java") @@ -65,6 +80,8 @@ def translate(filename): in_bracket_op = 0 in_getter_get = 0 in_getter_set = 0 + had_ulong_res = 0 + in_enum = 0 for line in fileinput.input(os.path.join(CS, filename)): s = string.rstrip(string.lstrip(line)) if in_javadoc: @@ -98,8 +115,10 @@ def translate(filename): in_header = 0 tgt.write(" * This file was automatically generated from " + filename + " \n") tgt.write(" **/\n") - tgt.write("\npackage com.Microsoft.Z3;\n") - + tgt.write("\npackage com.Microsoft.Z3;\n\n") + tgt.write("import java.math.BigInteger;\n") + tgt.write("import java.util.*;\n") + tgt.write("import java.lang.Exception;\n") elif in_header == 1: # tgt.write(" * " + line.replace(filename, tgtfn)) pass @@ -113,10 +132,20 @@ def translate(filename): for i in range(0, line.find(s)+1): t += " " tgt.write(t + "/* Overloaded operators are not translated. */\n") - in_unsupported = 1; + in_unsupported = 1 + elif s.startswith("public enum"): + tgt.write(line) + 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)) 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", "") + a = type_replace(a) tgt.write(a) in_class = 1 in_static_class = 0 @@ -129,10 +158,13 @@ def translate(filename): in_javadoc = 1 elif skip_brace and s == "{": skip_brace = 0 - elif s.find("public") != -1 and s.find("class") == -1 and s.find("event") == -1 and s.find("(") == -1: + elif ((s.find("public") != -1 or s.find("protected") != -1) and s.find("class") == -1 and s.find("event") == -1 and s.find("(") == -1) or s.startswith("internal virtual IntPtr NativeObject") or s.startswith("internal Context Context"): if (s.startswith("new")): s = s[3:] + s = s.replace("internal virtual", "") + s = s.replace("internal", "") tokens = s.split(" ") + print "TOKENS: " + str(len(tokens)) if len(tokens) == 3: in_getter = tokens[2] in_getter_type = type_replace((tokens[0] + " " + tokens[1])) @@ -140,6 +172,7 @@ def translate(filename): in_getter_type = in_getter_type.replace("static", "") lastindent = line.find(s) skip_brace = 1 + getters.append(in_getter) elif len(tokens) == 4: if tokens[2].startswith("this["): in_bracket_op = 1 @@ -152,21 +185,35 @@ def translate(filename): if in_static_class: in_getter_type = in_getter_type.replace("static", "") lastindent = line.find(s) - skip_brace = 1 + skip_brace = 1 + getters.append(in_getter) else: in_getter = tokens[2] in_getter_type = type_replace(tokens[0] + " " + tokens[1]) - if in_static_class: - in_getter_type = in_getter_type.replace("static", "") - rest = s[s.find("get ") + 4:-1] - subst_getters(rest, getters) - rest = type_replace(rest) - rest = rename_native(rest) - t = "" - for i in range(0, lastindent): - t += " " - tgt.write(t + in_getter_type + " " + in_getter + "() " + rest + "\n") - getters.append(in_getter) + if tokens[2].startswith("this["): + lastindent = line.find(s) + t = "" + for i in range(0, lastindent): t += " " + tgt.write(t + "/* operator this[] not translated */\n ") + in_unsupported = 1 + else: + if in_static_class: + in_getter_type = in_getter_type.replace("static", "") + rest = s[s.find("get ") + 4:-1] + subst_getters(rest, getters) + rest = type_replace(rest) + rest = rename_native(rest) + rest = replace_generals(rest) + t = "" + for i in range(0, lastindent): + t += " " + tgt.write(t + in_getter_type + " " + in_getter + "() " + rest + "\n") + if rest.find("}") == -1: + in_getter_get = 1 + else: + getters.append(in_getter) + in_getter = "" + in_getter_type = "" print "ACC: " + s + " --> " + in_getter elif s.find("{ get {") != -1: line = type_replace(line) @@ -177,6 +224,7 @@ def translate(filename): rest = re.sub("Contract.\w+\([\s\S]*\);", "", rest) subst_getters(rest, getters) rest = rename_native(rest) + rest = replace_generals(rest) if in_bracket_op: tgt.write(d + rest) else: @@ -185,12 +233,13 @@ def translate(filename): elif in_getter != "" and s.startswith("get"): t = "" for i in range(0, lastindent): - t += " " + t += " " if len(s) > 3: rest = s[3:] else: rest = "" subst_getters(rest, getters) rest = type_replace(rest) rest = rename_native(rest) + rest = replace_generals(rest) if in_bracket_op: tgt.write(t + in_getter_type + " " + in_getter + " " + rest + "\n") else: @@ -207,6 +256,7 @@ def translate(filename): rest = rest.replace("(Integer)value", "Integer(value)") rest = type_replace(rest) rest = rename_native(rest) + rest = replace_generals(rest) ac_acc = in_getter_type[:in_getter_type.find(' ')] ac_type = in_getter_type[in_getter_type.find(' ')+1:] if in_bracket_op: @@ -216,13 +266,13 @@ def translate(filename): tgt.write(t + ac_acc + " void set" + in_getter + "(" + ac_type + " value) " + rest + "\n") if rest.find("}") == -1: in_getter_set = 1 - elif in_getter != "" and in_getter_get and s == "}": + elif in_getter != "" and in_getter_get == 1 and s == "}": tgt.write(line) in_getter_get = 0 - elif in_getter != "" and in_getter_set and s == "}": + elif in_getter != "" and in_getter_set == 1 and s == "}": tgt.write(line) in_getter_set = 0 - elif in_getter != "" and not in_getter_get and not in_getter_set and s == "}": + elif in_getter != "" and in_getter_get == 0 and in_getter_set == 0 and s == "}": in_getter = "" in_getter_type == "" in_bracket_op = 0 @@ -232,19 +282,26 @@ def translate(filename): line = re.sub("(?P\w+)(?P[,;])", "\g\g", line) tgt.write(line); elif (not in_class and (s.startswith("{") or s.startswith("}"))) or s.startswith("[") or s.startswith("#"): - # print "Skipping: " + s; + # tgt.write("// Skipping: " + s) pass elif line == "}\n": pass else: # indent = line.find(s) + # tgt.write("// LINE: " + line) if line.find(": base") != -1: - line = re.sub(": base\((?P

[\w,.\(\) ]*)\)", "{ super(\g

);", line) - if line.find("; {") != -1: - line = line.replace("; {", ";") + line = re.sub(": base\((?P

[^\{]*)\)", "{ super(\g

);", line) + line = line[4:] + obraces = line.count("{") + cbraces = line.count("}") + mbraces = obraces - cbraces + # tgt.write("// obraces = " + str(obraces) + "\n") + if obraces == 1: + skip_brace = 1 else: - skip_brace = 1 - if s.startswith("public"): + for i in range(0, mbraces): + line = line.replace("\n", "}\n") + if s.find("(") != -1: line = re.sub(" = [\w.]+(?P[,;\)])", "\g", line) a = type_replace(line) a = re.sub("(?P[\(, ])params ", "\g", a) @@ -253,25 +310,43 @@ def translate(filename): a = rename_native(a) a = re.sub("~\w+\(\)", "protected void finalize()", a) a = re.sub("foreach\s*\((?P[\w <>,]+)\s+(?P\w+)\s+in\s+(?P\w+)\)", - "for (\g.Iterator \g = \g.iterator(); \g.hasNext(); )", a) + "for (Iterator \g = \g.iterator(); \g.hasNext(); )", a) a = a.replace("readonly ", "") a = a.replace("const ", "final ") - a = a.replace("ToString", "toString") + a = a.replace("String ToString", "String toString") a = a.replace("internal ", "") a = a.replace("new static", "static") a = a.replace("new public", "public") a = a.replace("override ", "") a = a.replace("virtual ", "") a = a.replace("o as AST", "(AST) o") + a = a.replace("o as Sort", "(Sort) o") a = a.replace("other as AST", "(AST) other") a = a.replace("o as FuncDecl", "(FuncDecl) o") + a = a.replace("IntPtr obj", "long obj") + a = a.replace("IntPtr o", "long o") + a = a.replace("new long()", "0") + a = a.replace("long.Zero", "0") + a = a.replace("object o", "Object o") + a = a.replace("object other", "Object other") a = a.replace("IntPtr res = IntPtr.Zero;", "Native.IntPtr res = new Native.IntPtr();") a = a.replace("out res", "res") + a = a.replace("GC.ReRegisterForFinalize(m_ctx);", "") + a = a.replace("GC.SuppressFinalize(this);", "") + 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: + a = a.replace("ref res)", "res)") + if a.find("return res;") != -1: + a = a.replace("return res;", "return res.value;") + had_ulong_res = 0 a = a.replace("lock (", "synchronized (") if in_static_class: a = a.replace("static", "") a = re.sub("ref (?P\w+)", "\g", a) subst_getters(a, getters) + a = re.sub("NativeObject = (?P.*);", "setNativeObject(\g);", a) + a = replace_generals(a) tgt.write(a) tgt.close()