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

Java API: Updates, this is still work in progress.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2012-11-23 19:24:56 +00:00
parent 7defd469bb
commit eb812f0fad
59 changed files with 2105 additions and 1570 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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;
* <param name="other">Another AST</param>
* @return Negative if the object should be sorted before <paramref name="other"/>, 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 <paramref name="ctx"/>.
@ -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);

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

@ -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);

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

@ -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);

62
src/api/java/com/Microsoft/Z3/AlgebraicNum.java Normal file
View file

@ -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^<paramref name="precision"/>.
* <seealso cref="Expr.IsAlgebraicNumber"/>
* <param name="precision">the precision of the result</param>
* @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^<paramref name="precision"/>.
* <seealso cref="Expr.IsAlgebraicNumber"/>
* <param name="precision"></param>
* @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.
* <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>
**/
public String ToDecimal(long precision)
{
return Native.getNumeralDecimalString(Context().nCtx(), NativeObject(), precision);
}
AlgebraicNum(Context ctx, long obj)
{ super(ctx, obj);
}
}

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

@ -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);

31
src/api/java/com/Microsoft/Z3/ArithExpr.java Normal file
View file

@ -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 </summary>
**/
protected ArithExpr(Context ctx)
{ super(ctx);
}
ArithExpr(Context ctx, long obj)
{ super(ctx, obj);
}
}

19
src/api/java/com/Microsoft/Z3/ArithSort.java Normal file
View file

@ -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); { }}
};

31
src/api/java/com/Microsoft/Z3/ArrayExpr.java Normal file
View file

@ -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 </summary>
**/
protected ArrayExpr(Context ctx)
{ super(ctx);
}
ArrayExpr(Context ctx, long obj)
{ super(ctx, obj);
}
}

46
src/api/java/com/Microsoft/Z3/ArraySort.java Normal file
View file

@ -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));
}
};

31
src/api/java/com/Microsoft/Z3/BitVecExpr.java Normal file
View file

@ -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 </summary>
**/
protected BitVecExpr(Context ctx) { super(ctx); { }}
BitVecExpr(Context ctx, long obj) { super(ctx, obj); { }}
}

80
src/api/java/com/Microsoft/Z3/BitVecNum.java Normal file
View file

@ -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); { }}
}

25
src/api/java/com/Microsoft/Z3/BitVecSort.java Normal file
View file

@ -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)); { }}
};

27
src/api/java/com/Microsoft/Z3/BoolExpr.java Normal file
View file

@ -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 </summary>
**/
protected BoolExpr(Context ctx) { super(ctx); { }}
/** Constructor for BoolExpr </summary>
**/
BoolExpr(Context ctx, long obj) { super(ctx, obj); { }}
}

20
src/api/java/com/Microsoft/Z3/BoolSort.java Normal file
View file

@ -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())); { }}
};

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

@ -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));
}
}

42
src/api/java/com/Microsoft/Z3/ConstructorList.java Normal file
View file

@ -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)));
}
}

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

@ -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<String, String> settings)
{ super();
public Context(Map<String, String> settings)
{ super();
IntPtr cfg = Native.mkConfig();
for (KeyValuePair<String, String>.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;
* <param name="ty">Sort of the numeral</param>
* @return A Term with value <paramref name="v"/> and type <paramref name="ty"/>
**/
public Expr MkNumeral(ulong v, Sort ty)
public Expr MkNumeral(long v, Sort ty)
{
@ -2319,7 +2323,7 @@ package com.Microsoft.Z3;
* <param name="v">value of the numeral.</param>
* @return A Term with value <paramref name="v"/> and sort Real
**/
public RatNum MkReal(ulong v)
public RatNum MkReal(long v)
{
@ -2378,7 +2382,7 @@ package com.Microsoft.Z3;
* <param name="v">value of the numeral.</param>
* @return A Term with value <paramref name="v"/> and sort Integer
**/
public IntNum MkInt(ulong v)
public IntNum MkInt(long v)
{
@ -2438,7 +2442,7 @@ package com.Microsoft.Z3;
* <param name="v">value of the numeral.</param>
* <param name="size">the size of the bit-vector</param>
**/
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;
* <seealso cref="UnwrapAST"/>
* <param name="nativeObject">The native pointer to wrap.</param>
**/
public AST WrapAST(IntPtr nativeObject)
public AST WrapAST(long nativeObject)
{
return AST.Create(this, nativeObject);
@ -3327,9 +3331,9 @@ package com.Microsoft.Z3;
* <seealso cref="WrapAST"/>
* <param name="a">The AST to unwrap.</param>
**/
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;
}

31
src/api/java/com/Microsoft/Z3/DatatypeExpr.java Normal file
View file

@ -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 </summary>
**/
protected DatatypeExpr(Context ctx)
{ super(ctx);
}
DatatypeExpr(Context ctx, long obj)
{ super(ctx, obj);
}
}

80
src/api/java/com/Microsoft/Z3/DatatypeSort.java Normal file
View file

@ -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)));
}
};

82
src/api/java/com/Microsoft/Z3/EnumSort.java Normal file
View file

@ -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]);
}
};

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

@ -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 </summary>
**/
protected BoolExpr(Context ctx) { super(ctx); }
/** Constructor for BoolExpr </summary>
**/
BoolExpr(Context ctx, IntPtr obj) { super(ctx, obj); }
}
/**
* Arithmetic expressions (int/real)
**/
public class ArithExpr extends Expr
{
/** Constructor for ArithExpr </summary>
**/
protected ArithExpr(Context ctx)
{ super(ctx);
}
ArithExpr(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
}
/**
* Int expressions
**/
public class IntExpr extends ArithExpr
{
/** Constructor for IntExpr </summary>
**/
protected IntExpr(Context ctx)
{ super(ctx);
}
IntExpr(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
}
/**
* Real expressions
**/
public class RealExpr extends ArithExpr
{
/** Constructor for RealExpr </summary>
**/
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 </summary>
**/
protected BitVecExpr(Context ctx) { super(ctx); }
BitVecExpr(Context ctx, IntPtr obj) { super(ctx, obj); }
}
/**
* Array expressions
**/
public class ArrayExpr extends Expr
{
/** Constructor for ArrayExpr </summary>
**/
protected ArrayExpr(Context ctx)
{ super(ctx);
}
ArrayExpr(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
}
/**
* Datatype expressions
**/
public class DatatypeExpr extends Expr
{
/** Constructor for DatatypeExpr </summary>
**/
protected DatatypeExpr(Context ctx)
{ super(ctx);
}
DatatypeExpr(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
}

38
src/api/java/com/Microsoft/Z3/FiniteDomainSort.java Normal file
View file

@ -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));
}
}

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

@ -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);

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

@ -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
* <seealso cref="Arity"/>
**/
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;
* <param name="args"></param>
* @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.
* <param name="args"></param>

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

@ -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<Entry[]>().Length,
j => Contract.Result<Entry[]>()[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);

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

@ -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.
* </remarks>
**/
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.
* </remarks>
**/
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 <paramref name="ctx"/>.
@ -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);

28
src/api/java/com/Microsoft/Z3/DecRefQUeue.java → src/api/java/com/Microsoft/Z3/IDecRefQueue.java
View file

@ -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<IntPtr> m_queue = new List<IntPtr>();
protected List<Long> m_queue = new List<Long>();
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)
{
}

31
src/api/java/com/Microsoft/Z3/IntExpr.java Normal file
View file

@ -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 </summary>
**/
protected IntExpr(Context ctx)
{ super(ctx);
}
IntExpr(Context ctx, long obj)
{ super(ctx, obj);
}
}

85
src/api/java/com/Microsoft/Z3/IntNum.java Normal file
View file

@ -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());
}
}

26
src/api/java/com/Microsoft/Z3/IntSort.java Normal file
View file

@ -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()));
}
}

45
src/api/java/com/Microsoft/Z3/IntSymbol.java Normal file
View file

@ -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.
* <remarks>Throws an exception if the symbol is not of int kind. </remarks>
**/
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);
}
}

122
src/api/java/com/Microsoft/Z3/ListSort.java Normal file
View file

@ -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);
}
};

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

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

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

@ -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);

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

@ -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("<mk_util.JavaDLLComponent instance at 0x0251B738>"); }
public static class errorHandler {};
static { System.loadLibrary("<mk_util.JavaDLLComponent instance at 0x0236D8F0>"); }
public static native long mkConfig();
public static native void delConfig(long a0);
public static native void setParamValue(long a0, String a1, String a2);

264
src/api/java/com/Microsoft/Z3/Numeral.java
View file

@ -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.
* <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>
**/
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^<paramref name="precision"/>.
* <seealso cref="Expr.IsAlgebraicNumber"/>
* <param name="precision">the precision of the result</param>
* @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^<paramref name="precision"/>.
* <seealso cref="Expr.IsAlgebraicNumber"/>
* <param name="precision"></param>
* @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.
* <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>
**/
public String ToDecimal(long precision)
{
return Native.getNumeralDecimalString(Context.nCtx, NativeObject, precision);
}
AlgebraicNum(Context ctx, IntPtr obj)
{ super(ctx, obj);
}
}

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

@ -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);

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

@ -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);

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

@ -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);
}
}

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

@ -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);

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

@ -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);
}

78
src/api/java/com/Microsoft/Z3/RatNum.java Normal file
View file

@ -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.
* <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>
**/
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);
}
}

31
src/api/java/com/Microsoft/Z3/RealExpr.java Normal file
View file

@ -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 </summary>
**/
protected RealExpr(Context ctx)
{ super(ctx);
}
RealExpr(Context ctx, long obj)
{ super(ctx, obj);
}
}

26
src/api/java/com/Microsoft/Z3/RealSort.java Normal file
View file

@ -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()));
}
}

46
src/api/java/com/Microsoft/Z3/RelationSort.java Normal file
View file

@ -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);
}
}

27
src/api/java/com/Microsoft/Z3/SetSort.java Normal file
View file

@ -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));
}
}

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

@ -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;
* <seealso cref="Pop"/>
* <seealso cref="Push"/>
**/
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);

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

@ -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;
* <param name="o"></param>
* @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));
}
}
}

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

@ -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);

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

@ -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
{
/// <summary>
/// Used to signify an unsatisfiable status.
/// </summary>
UNSATISFIABLE (1),
/**
* Used to signify an unknown status.
**/
UNKNOWN = 0,
/// <summary>
/// Used to signify an unknown status.
/// </summary>
UNKNOWN (0),
/**
* Used to signify a satisfiable status.
**/
SATISFIABLE = 1
/// <summary>
/// Used to signify a satisfiable status.
/// </summary>
SATISFIABLE (1)
}

50
src/api/java/com/Microsoft/Z3/StringSymbol.java Normal file
View file

@ -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.
* <remarks>Throws an exception if the symbol is not of string kind.</remarks>
**/
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);
}
}

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

@ -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.
* <remarks>Throws an exception if the symbol is not of int kind. </remarks>
**/
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.
* <remarks>Throws an exception if the symbol is not of string kind.</remarks>
**/
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);
}
}

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

@ -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);

57
src/api/java/com/Microsoft/Z3/TupleSort.java Normal file
View file

@ -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]);
}
};

27
src/api/java/com/Microsoft/Z3/UninterpretedSort.java Normal file
View file

@ -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));
}
}

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

@ -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();
}
}

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

@ -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); { }}
}

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

@ -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;
}

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

@ -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<long>", "List<Long>")
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<id>.*)\W*=\W*(?P<val>[^\n,])", "\g<id> (\g<val>)", 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<n>\w+)(?P<c>[,;])", "\g<n>\g<c>", 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<p>[\w,.\(\) ]*)\)", "{ super(\g<p>);", line)
if line.find("; {") != -1:
line = line.replace("; {", ";")
line = re.sub(": base\((?P<p>[^\{]*)\)", "{ super(\g<p>);", 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<d>[,;\)])", "\g<d>", line)
a = type_replace(line)
a = re.sub("(?P<d>[\(, ])params ", "\g<d>", 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<t>[\w <>,]+)\s+(?P<i>\w+)\s+in\s+(?P<w>\w+)\)",
"for (\g<t>.Iterator \g<i> = \g<w>.iterator(); \g<i>.hasNext(); )", a)
"for (Iterator \g<i> = \g<w>.iterator(); \g<i>.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<id>\w+)", "\g<id>", a)
subst_getters(a, getters)
a = re.sub("NativeObject = (?P<rest>.*);", "setNativeObject(\g<rest>);", a)
a = replace_generals(a)
tgt.write(a)
tgt.close()