\1
g, that the ApplyResult was obtained from.
+ * @return A model for g
+ **/
+ public Model ConvertModel(Integer i, Model m)
+ {
+
+
+
+ return new Model(Context, Native.applyResultConvertModel(Context.nCtx, NativeObject, i, m.NativeObject));
+ }
+
+ /**
+ * A string representation of the ApplyResult.
+ **/
+ public String toString()
+ {
+ return Native.applyResulttoString(Context.nCtx, NativeObject);
+ }
+
+ ApplyResult(Context ctx, IntPtr obj) { super(ctx, obj);
+
+ }
+
+ class DecRefQueue extends Z3.DecRefQueue
+ {
+ public void IncRef(Context ctx, IntPtr obj)
+ {
+ Native.applyResultIncRef(ctx.nCtx, obj);
+ }
+
+ public void DecRef(Context ctx, IntPtr obj)
+ {
+ Native.applyResultDecRef(ctx.nCtx, obj);
+ }
+ };
+
+ void IncRef(IntPtr o)
+ {
+ Context.ApplyResultDRQ.IncAndClear(Context, o);
+ super.IncRef(o);
+ }
+
+ void DecRef(IntPtr o)
+ {
+ Context.ApplyResultDRQ.Add(o);
+ super.DecRef(o);
+ }
+ }
diff --git a/src/api/java/com/Microsoft/Z3/Constructor.java b/src/api/java/com/Microsoft/Z3/Constructor.java
new file mode 100644
index 000000000..2f9a2009e
--- /dev/null
+++ b/src/api/java/com/Microsoft/Z3/Constructor.java
@@ -0,0 +1,130 @@
+/**
+ * This file was automatically generated from Constructor.cs
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+ /**
+ * Constructors are used for datatype sorts.
+ **/
+ public class Constructor extends Z3Object
+ {
+ /**
+ * The number of fields of the constructor.
+ **/
+ public Integer NumFields() { init(); return n; }
+
+ /**
+ * The function declaration of the constructor.
+ **/
+ public FuncDecl ConstructorDecl() {
+
+ init(); return mConstructorDecl; }
+
+ /**
+ * The function declaration of the tester.
+ **/
+ public FuncDecl TesterDecl() {
+
+ init(); return mTesterDecl; }
+
+ /**
+ * The function declarations of the accessors
+ **/
+ public FuncDecl[] AccessorDecls() {
+
+ init(); return mAccessorDecls; }
+
+ /**
+ * Destructor.
+ **/
+ protected void finalize()
+ {
+ Native.delConstructor(Context.nCtx, NativeObject);
+ }
+
+
+ private void ObjectInvariant()
+ {
+
+
+ }
+
+
+ private Integer n = 0;
+ private FuncDecl mTesterDecl = null;
+ private FuncDecl mConstructorDecl = null;
+ private FuncDecl[] mAccessorDecls = null;
+
+ Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames,
+ Sort[] sorts, Integer[] sortRefs)
+ { super(ctx);
+
+
+
+
+ n = AST.ArrayLength(fieldNames);
+
+ if (n != AST.ArrayLength(sorts))
+ throw new Z3Exception("Number of field names does not match number of sorts");
+ if (sortRefs != null && sortRefs.Length != n)
+ throw new Z3Exception("Number of field names does not match number of sort refs");
+
+ if (sortRefs == null) sortRefs = new Integer[n];
+
+ NativeObject = Native.mkConstructor(ctx.nCtx, name.NativeObject, recognizer.NativeObject,
+ n,
+ Symbol.ArrayToNative(fieldNames),
+ Sort.ArrayToNative(sorts),
+ sortRefs);
+
+ }
+
+ private void init()
+ {
+
+
+
+
+ if (mTesterDecl != null) return;
+ IntPtr constructor = IntPtr.Zero;
+ IntPtr tester = IntPtr.Zero;
+ IntPtr[] accessors = new IntPtr[n];
+ Native.queryConstructor(Context.nCtx, NativeObject, n, constructor, tester, accessors);
+ mConstructorDecl = new FuncDecl(Context, constructor);
+ mTesterDecl = new FuncDecl(Context, tester);
+ mAccessorDecls = new FuncDecl[n];
+ for (Integer i = 0; i < n; i++)
+ mAccessorDecls[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, (Integer)constructors.Length, Constructor.ArrayToNative(constructors));
+ }
+ }
diff --git a/src/api/java/com/Microsoft/Z3/Context.java b/src/api/java/com/Microsoft/Z3/Context.java
new file mode 100644
index 000000000..471c82120
--- /dev/null
+++ b/src/api/java/com/Microsoft/Z3/Context.java
@@ -0,0 +1,3534 @@
+/**
+ * This file was automatically generated from Context.cs
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+/* using System.Collections.Generic; */
+/* using System.Runtime.InteropServices; */
+
+ /**
+ * The main interaction with Z3 happens via the Context.
+ **/
+ public class Context extends IDisposable
+ {
+ /**
+ * Constructor.
+ **/
+ public Context()
+ { super();
+ mCtx = Native.mkContextRc(IntPtr.Zero);
+ InitContext();
+ }
+
+ /**
+ * Constructor.
+ **/
+ public Context(Dictionarydistinct term.
+ **/
+ public BoolExpr MkDistinct(Expr[] args)
+ {
+
+
+
+
+
+ CheckContextMatch(args);
+ return new BoolExpr(this, Native.mkDistinct(nCtx, (Integer)args.Length, AST.ArrayToNative(args)));
+ }
+
+ /**
+ * Mk an expression representing not(a).
+ **/
+ public BoolExpr MkNot(BoolExpr a)
+ {
+
+
+
+ CheckContextMatch(a);
+ return new BoolExpr(this, Native.mkNot(nCtx, a.NativeObject));
+ }
+
+ /**
+ * Create an expression representing an if-then-else: ite(t1, t2, t3).
+ * An expression with Boolean sort
+ * An expression
+ * An expression with the same sort as t1 iff t2.
+ **/
+ public BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
+ {
+
+
+
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.mkIff(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ /**
+ * Create an expression representing t1 -> t2.
+ **/
+ public BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
+ {
+
+
+
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.mkImplies(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ /**
+ * Create an expression representing t1 xor t2.
+ **/
+ public BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
+ {
+
+
+
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.mkXor(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ /**
+ * Create an expression representing t[0] and t[1] and ....
+ **/
+ public BoolExpr MkAnd(BoolExpr[] t)
+ {
+
+
+
+
+ CheckContextMatch(t);
+ return new BoolExpr(this, Native.mkAnd(nCtx, (Integer)t.Length, AST.ArrayToNative(t)));
+ }
+
+ /**
+ * Create an expression representing t[0] or t[1] or ....
+ **/
+ public BoolExpr MkOr(BoolExpr[] t)
+ {
+
+
+
+
+ CheckContextMatch(t);
+ return new BoolExpr(this, Native.mkOr(nCtx, (Integer)t.Length, AST.ArrayToNative(t)));
+ }
+
+ /**
+ * Create an expression representing t[0] + t[1] + ....
+ **/
+ public ArithExpr MkAdd(ArithExpr[] t)
+ {
+
+
+
+
+ CheckContextMatch(t);
+ return (ArithExpr)Expr.Create(this, Native.mkAdd(nCtx, (Integer)t.Length, AST.ArrayToNative(t)));
+ }
+
+ /**
+ * Create an expression representing t[0] * t[1] * ....
+ **/
+ public ArithExpr MkMul(ArithExpr[] t)
+ {
+
+
+
+
+ CheckContextMatch(t);
+ return (ArithExpr)Expr.Create(this, Native.mkMul(nCtx, (Integer)t.Length, AST.ArrayToNative(t)));
+ }
+
+ /**
+ * Create an expression representing t[0] - t[1] - ....
+ **/
+ public ArithExpr MkSub(ArithExpr[] t)
+ {
+
+
+
+
+ CheckContextMatch(t);
+ return (ArithExpr)Expr.Create(this, Native.mkSub(nCtx, (Integer)t.Length, AST.ArrayToNative(t)));
+ }
+
+ /**
+ * Create an expression representing -t.
+ **/
+ public ArithExpr MkUnaryMinus(ArithExpr t)
+ {
+
+
+
+ CheckContextMatch(t);
+ return (ArithExpr)Expr.Create(this, Native.mkUnaryMinus(nCtx, t.NativeObject));
+ }
+
+ /**
+ * Create an expression representing t1 / t2.
+ **/
+ public ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
+ {
+
+
+
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return (ArithExpr)Expr.Create(this, Native.mkDiv(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ /**
+ * Create an expression representing t1 mod t2.
+ * t1 rem t2.
+ * t1 ^ t2.
+ **/
+ public ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
+ {
+
+
+
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return (ArithExpr)Expr.Create(this, Native.mkPower(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ /**
+ * Create an expression representing t1 < t2
+ **/
+ public BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
+ {
+
+
+
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.mkLt(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ /**
+ * Create an expression representing t1 <= t2
+ **/
+ public BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
+ {
+
+
+
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.mkLe(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ /**
+ * Create an expression representing t1 > t2
+ **/
+ public BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
+ {
+
+
+
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.mkGt(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ /**
+ * Create an expression representing t1 >= t2
+ **/
+ public BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
+ {
+
+
+
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.mkGe(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ /**
+ * Coerce an integer to a real.
+ * k and
+ * and asserting MakeInt2Real(k) <= t1 < MkInt2Real(k)+1.
+ * The argument must be of integer sort.
+ * t1/t2 if \c t2 is
+ * different from zero. If t2 is zero, then the result
+ * is undefined.
+ * The arguments must have the same bit-vector sort.
+ * t1/t2 if \c t2 is different from zero, and t1*t2 >= 0.
+ *
+ * - The \c ceiling of t1/t2 if \c t2 is different from zero, and t1*t2 < 0.
+ *
+ * If t2 is zero, then the result is undefined.
+ * The arguments must have the same bit-vector sort.
+ * t1 - (t1 /u t2) * t2, where /u represents unsigned division.
+ * If t2 is zero, then the result is undefined.
+ * The arguments must have the same bit-vector sort.
+ * t1 - (t1 /s t2) * t2, where /s represents signed division.
+ * The most significant bit (sign) of the result is equal to the most significant bit of \c t1.
+ *
+ * If t2 is zero, then the result is undefined.
+ * The arguments must have the same bit-vector sort.
+ * t2 is zero, then the result is undefined.
+ * The arguments must have the same bit-vector sort.
+ * n1+n2, where n1 (n2)
+ * is the size of t1 (t2).
+ *
+ **/
+ public BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
+ {
+
+
+
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.mkConcat(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ /**
+ * Bit-vector extraction.
+ * m to yield a new bitvector of size n, where
+ * n = high - low + 1.
+ * The argument m+i, where \c m is the size of the given bit-vector.
+ * The argument m+i, where \c m is the size of the
+ * given bit-vector.
+ * The argument 2^x where \c x is the value of 2^x where \c x is the value of [0..2^N-1], where
+ * N are the number of bits in a is the array and i is the index
+ * of the array that gets read.
+ *
+ * The node a must have an array sort [domain -> range],
+ * and i must have the sort domain.
+ * The sort of the result is range.
+ * a must have an array sort [domain -> range],
+ * i must have sort domain,
+ * v must have sort range. The sort of the result is [domain -> range].
+ * The semantics of this function is given by the theory of arrays described in the SMT-LIB
+ * standard. See http://smtlib.org for more details.
+ * The result of this function is an array that is equal to a
+ * (with respect to select)
+ * on all indices except for i, where it maps to v
+ * (and the select of a with
+ * respect to i may be a different value).
+ * selecton an arbitrary index
+ * produces the value v.
+ * args must be of an array sort [domain_i -> range_i].
+ * The function declaration f must have type range_1 .. range_n -> range.
+ * v must have sort range. The sort of the result is [domain_i -> range].
+ * [num]* / [num]*.
+ * The sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size.
+ * @return A Term with value MakeNumeral since it is not necessary to parse a string.
+ * Value of the numeral
+ * Sort of the numeral
+ * @return A Term with value MakeNumeral since it is not necessary to parse a string.
+ * Value of the numeral
+ * Sort of the numeral
+ * @return A Term with value MakeNumeral since it is not necessary to parse a string.
+ * Value of the numeral
+ * Sort of the numeral
+ * @return A Term with value MakeNumeral since it is not necessary to parse a string.
+ * Value of the numeral
+ * Sort of the numeral
+ * @return A Term with value MkPattern.
+ * array containing the anti-patterns created using MkPattern.
+ * optional symbol to track quantifier.
+ * optional symbol to track skolem constants.
+ **/
+ public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, Integer weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
+ {
+
+
+
+
+
+
+
+
+
+
+
+ return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
+ }
+
+
+ /**
+ * Create a universal Quantifier.
+ **/
+ public Quantifier MkForall(Expr[] boundConstants, Expr body, Integer weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
+ {
+
+
+
+
+
+
+
+ return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
+ }
+
+ /**
+ * Create an existential Quantifier.
+ * ParseSMTLIBString or ParseSMTLIBFile.
+ **/
+ public Integer NumSMTLIBFormulas () { return Native.getSmtlibNumFormulas(nCtx); }
+
+ /**
+ * The formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
+ **/
+ public BoolExpr[] SMTLIBFormulas()
+ {
+
+
+ Integer n = NumSMTLIBFormulas;
+ BoolExpr[] res = new BoolExpr[n];
+ for (Integer i = 0; i < n; i++)
+ res[i] = (BoolExpr)Expr.Create(this, Native.getSmtlibFormula(nCtx, i));
+ return res;
+ }
+
+ /**
+ * The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
+ **/
+ public Integer NumSMTLIBAssumptions () { return Native.getSmtlibNumAssumptions(nCtx); }
+
+ /**
+ * The assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
+ **/
+ public BoolExpr[] SMTLIBAssumptions()
+ {
+
+
+ Integer n = NumSMTLIBAssumptions;
+ BoolExpr[] res = new BoolExpr[n];
+ for (Integer i = 0; i < n; i++)
+ res[i] = (BoolExpr)Expr.Create(this, Native.getSmtlibAssumption(nCtx, i));
+ return res;
+ }
+
+ /**
+ * The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
+ **/
+ public Integer NumSMTLIBDecls () { return Native.getSmtlibNumDecls(nCtx); }
+
+ /**
+ * The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
+ **/
+ public FuncDecl[] SMTLIBDecls()
+ {
+
+
+ Integer n = NumSMTLIBDecls;
+ FuncDecl[] res = new FuncDecl[n];
+ for (Integer i = 0; i < n; i++)
+ res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx, i));
+ return res;
+ }
+
+ /**
+ * The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
+ **/
+ public Integer NumSMTLIBSorts () { return Native.getSmtlibNumSorts(nCtx); }
+
+ /**
+ * The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
+ **/
+ public Sort[] SMTLIBSorts()
+ {
+
+
+ Integer n = NumSMTLIBSorts;
+ Sort[] res = new Sort[n];
+ for (Integer i = 0; i < n; i++)
+ res[i] = Sort.Create(this, Native.getSmtlibSort(nCtx, i));
+ return res;
+ }
+
+ /**
+ * Parse the given string using the SMT-LIB2 parser.
+ * AndThen.
+ * skip tactic.
+ * UsingParamsPush and Pop, but it
+ * will always solve each check from scratch.
+ * Expr.Simplify.
+ **/
+ public String SimplifyHelp()
+ {
+
+
+ return Native.simplifyGetHelp(nCtx);
+ }
+
+ /**
+ * Retrieves parameter descriptions for simplifier.
+ **/
+ public ParamDescrs SimplifyParameterDescriptions() { return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx)); }
+
+ /**
+ * Enable/disable printing of warning messages to the console.
+ * z3.exe -ini?
+ * Only a few configuration parameters are mutable once the context is created.
+ * An exception is thrown when trying to modify an immutable parameter.
+ * from[i] in the expression with to[i], for i smaller than num_exprs.
+ * from and to must have size num_exprs.
+ * For every i smaller than num_exprs, we must have that
+ * sort of from[i] must be equal to sort of to[i].
+ * from in the expression with to.
+ * i smaller than num_exprs, the variable with de-Bruijn index i is replaced with term to[i].
+ * n+1 arguments, where the first argument is the relation and the remaining n elements
+ * correspond to the n columns of the relation.
+ * PushModelEvaluationFailedException is thrown.
+ * Eval.
+ **/
+ public Expr Evaluate(Expr t, boolean completion)
+ {
+
+
+
+ return Eval(t, completion);
+ }
+
+ /**
+ * The number of uninterpreted sorts that the model has an interpretation for.
+ **/
+ public Integer NumSorts () { return Native.modelGetNumSorts(Context.nCtx, NativeObject); }
+
+ /**
+ * The uninterpreted sorts that the model has an interpretation for.
+ * Context.NumProbes
+ * and Context.ProbeNames.
+ * It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end.
+ **/
+ public class Probe extends Z3Object
+ {
+ /**
+ * Execute the probe over the goal.
+ * @return A probe always produce a double value.
+ * "Boolean" probes return 0.0 for false, and a value different from 0.0 for true.
+ **/
+ public double Apply(Goal g)
+ {
+
+
+ Context.CheckContextMatch(g);
+ return Native.probeApply(Context.nCtx, NativeObject, g.NativeObject);
+ }
+
+ /**
+ * Apply the probe to a goal.
+ **/
+ public double this[Goal()
+
+
+ return Apply(g); } }
+
+ Probe(Context ctx, IntPtr obj)
+ { super(ctx, obj);
+
+ Probe(Context ctx, String name)
+ { super(ctx, Native.mkProbe(ctx.nCtx, name));
+
+ }
+
+ class DecRefQueue extends Z3.DecRefQueue
+ {
+ public void IncRef(Context ctx, IntPtr obj)
+ {
+ Native.probeIncRef(ctx.nCtx, obj);
+ }
+
+ public void DecRef(Context ctx, IntPtr obj)
+ {
+ Native.probeDecRef(ctx.nCtx, obj);
+ }
+ };
+
+ void IncRef(IntPtr o)
+ {
+ Context.ProbeDRQ.IncAndClear(Context, o);
+ super.IncRef(o);
+ }
+
+ void DecRef(IntPtr o)
+ {
+ Context.ProbeDRQ.Add(o);
+ super.DecRef(o);
+ }
+ }
diff --git a/src/api/java/com/Microsoft/Z3/Quantifier.java b/src/api/java/com/Microsoft/Z3/Quantifier.java
new file mode 100644
index 000000000..1a279aff0
--- /dev/null
+++ b/src/api/java/com/Microsoft/Z3/Quantifier.java
@@ -0,0 +1,198 @@
+/**
+ * This file was automatically generated from Quantifier.cs
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+ /**
+ * Quantifier expressions.
+ **/
+ public class Quantifier extends BoolExpr
+ {
+ /**
+ * Indicates whether the quantifier is universal.
+ **/
+ public boolean IsUniversal() { return Native.isQuantifierForall(Context.nCtx, NativeObject) != 0; }
+
+ /**
+ * Indicates whether the quantifier is existential.
+ **/
+ public boolean IsExistential() { return !IsUniversal; }
+
+ /**
+ * The weight of the quantifier.
+ **/
+ public Integer Weight() { return Native.getQuantifierWeight(Context.nCtx, NativeObject); }
+
+ /**
+ * The number of patterns.
+ **/
+ public Integer NumPatterns() { return Native.getQuantifierNumPatterns(Context.nCtx, NativeObject); }
+
+ /**
+ * The patterns.
+ **/
+ public Pattern[] Patterns()
+ {
+
+
+ Integer n = NumPatterns;
+ Pattern[] res = new Pattern[n];
+ for (Integer i = 0; i < n; i++)
+ res[i] = new Pattern(Context, Native.getQuantifierPatternAst(Context.nCtx, NativeObject, i));
+ return res;
+ }
+
+ /**
+ * The number of no-patterns.
+ **/
+ public Integer NumNoPatterns() { return Native.getQuantifierNumNoPatterns(Context.nCtx, NativeObject); }
+
+ /**
+ * The no-patterns.
+ **/
+ public Pattern[] NoPatterns()
+ {
+
+
+ Integer n = NumNoPatterns;
+ Pattern[] res = new Pattern[n];
+ for (Integer i = 0; i < n; i++)
+ res[i] = new Pattern(Context, Native.getQuantifierNoPatternAst(Context.nCtx, NativeObject, i));
+ return res;
+ }
+
+ /**
+ * The number of bound variables.
+ **/
+ public Integer NumBound() { return Native.getQuantifierNumBound(Context.nCtx, NativeObject); }
+
+ /**
+ * The symbols for the bound variables.
+ **/
+ public Symbol[] BoundVariableNames()
+ {
+
+
+ Integer n = NumBound;
+ Symbol[] res = new Symbol[n];
+ for (Integer i = 0; i < n; i++)
+ res[i] = Symbol.Create(Context, Native.getQuantifierBoundName(Context.nCtx, NativeObject, i));
+ return res;
+ }
+
+ /**
+ * The sorts of the bound variables.
+ **/
+ public Sort[] BoundVariableSorts()
+ {
+
+
+ Integer n = NumBound;
+ Sort[] res = new Sort[n];
+ for (Integer i = 0; i < n; i++)
+ res[i] = Sort.Create(Context, Native.getQuantifierBoundSort(Context.nCtx, NativeObject, i));
+ return res;
+ }
+
+ /**
+ * The body of the quantifier.
+ **/
+ public BoolExpr Body() {
+
+
+ return new BoolExpr(Context, Native.getQuantifierBody(Context.nCtx, NativeObject)); }
+
+ Quantifier(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body,
+ Integer weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null,
+ Symbol quantifierID = null, Symbol skolemID = null
+ )
+ { super(ctx);
+
+
+
+
+
+
+
+
+
+
+ Context.CheckContextMatch(patterns);
+ Context.CheckContextMatch(noPatterns);
+ Context.CheckContextMatch(sorts);
+ Context.CheckContextMatch(names);
+ Context.CheckContextMatch(body);
+
+ if (sorts.Length != names.Length)
+ throw new Z3Exception("Number of sorts does not match number of names");
+
+ IntPtr[] 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),
+ AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
+ Symbol.ArrayToNative(names),
+ body.NativeObject);
+ }
+ else
+ {
+ 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),
+ AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
+ Symbol.ArrayToNative(names),
+ body.NativeObject);
+ }
+ }
+
+ Quantifier(Context ctx, boolean isForall, Expr[] bound, Expr body,
+ Integer weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null,
+ Symbol quantifierID = null, Symbol skolemID = null
+ )
+ { super(ctx);
+
+
+
+
+
+
+
+ Context.CheckContextMatch(noPatterns);
+ Context.CheckContextMatch(patterns);
+ //Context.CheckContextMatch(bound);
+ Context.CheckContextMatch(body);
+
+ if (noPatterns == null && quantifierID == null && skolemID == null)
+ {
+ NativeObject = Native.mkQuantifierConst(ctx.nCtx, (isForall) ? 1 : 0, weight,
+ AST.ArrayLength(bound), AST.ArrayToNative(bound),
+ AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
+ body.NativeObject);
+ }
+ else
+ {
+ 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),
+ AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
+ body.NativeObject);
+ }
+ }
+
+
+ Quantifier(Context ctx, IntPtr obj) { super(ctx, obj); }
+
+ void CheckNativeObject(IntPtr obj)
+ {
+ if ((Z3AstKind)Native.getAstKind(Context.nCtx, obj) != Z3AstKind.Z3QUANTIFIERAST)
+ throw new Z3Exception("Underlying object is not a quantifier");
+ super.CheckNativeObject(obj);
+ }
+ }
diff --git a/src/api/java/com/Microsoft/Z3/Solver.java b/src/api/java/com/Microsoft/Z3/Solver.java
new file mode 100644
index 000000000..a28687722
--- /dev/null
+++ b/src/api/java/com/Microsoft/Z3/Solver.java
@@ -0,0 +1,247 @@
+/**
+ * This file was automatically generated from Solver.cs
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+ /**
+ * Solvers.
+ **/
+ public class Solver extends Z3Object
+ {
+ /**
+ * A string that describes all available solver parameters.
+ **/
+ public String Help()
+ {
+
+
+ return Native.solverGetHelp(Context.nCtx, NativeObject);
+ }
+
+ /**
+ * Sets the solver parameters.
+ **/
+ public void setParameters(Params value)
+ {
+
+
+ Context.CheckContextMatch(value);
+ Native.solverSetParams(Context.nCtx, NativeObject, value.NativeObject);
+ }
+
+ /**
+ * Retrieves parameter descriptions for solver.
+ **/
+ public ParamDescrs ParameterDescriptions() { return new ParamDescrs(Context, Native.solverGetParamDescrs(Context.nCtx, NativeObject)); }
+
+
+ /**
+ * The current number of backtracking points (scopes).
+ * NumScopesCheck.
+ * null if Check was not invoked before,
+ * if its results was not SATISFIABLE, or if model production is not enabled.
+ * Check.
+ * null if Check was not invoked before,
+ * if its results was not UNSATISFIABLE, or if proof production is disabled.
+ * Check.
+ * Assertions
+ * The result is empty if Check was not invoked before,
+ * if its results was not UNSATISFIABLE, or if core production is disabled.
+ * Check returned UNKNOWN.
+ **/
+ public String ReasonUnknown()
+ {
+
+
+ return Native.solverGetReasonUnknown(Context.nCtx, NativeObject);
+ }
+
+ /**
+ * Solver statistics.
+ **/
+ public Statistics Statistics()
+ {
+
+
+ return new Statistics(Context, Native.solverGetStatistics(Context.nCtx, NativeObject));
+ }
+
+ /**
+ * A string representation of the solver.
+ **/
+ public String toString()
+ {
+ return Native.solvertoString(Context.nCtx, NativeObject);
+ }
+
+ Solver(Context ctx, IntPtr obj)
+ { super(ctx, obj);
+
+ }
+
+ class DecRefQueue extends Z3.DecRefQueue
+ {
+ public void IncRef(Context ctx, IntPtr obj)
+ {
+ Native.solverIncRef(ctx.nCtx, obj);
+ }
+
+ public void DecRef(Context ctx, IntPtr obj)
+ {
+ Native.solverDecRef(ctx.nCtx, obj);
+ }
+ };
+
+ void IncRef(IntPtr o)
+ {
+ Context.SolverDRQ.IncAndClear(Context, o);
+ super.IncRef(o);
+ }
+
+ void DecRef(IntPtr o)
+ {
+ Context.SolverDRQ.Add(o);
+ super.DecRef(o);
+ }
+ }
diff --git a/src/api/java/com/Microsoft/Z3/Sort.java b/src/api/java/com/Microsoft/Z3/Sort.java
new file mode 100644
index 000000000..f75624f1a
--- /dev/null
+++ b/src/api/java/com/Microsoft/Z3/Sort.java
@@ -0,0 +1,579 @@
+/**
+ * This file was automatically generated from Sort.cs
+ **/
+
+package com.Microsoft.Z3;
+
+/* using System; */
+
+ /**
+ * The Sort class implements type information for ASTs.
+ **/
+ public class Sort extends AST
+ {
+ /**
+ * Comparison operator.
+ * A Sort
+ * A Sort
+ * @return True if DoubleEntry or a UIntEntry
+ **/
+ public class Entry
+ {
+ /**
+ * The key of the entry.
+ **/
+ /**
+ * The uint-value of the entry.
+ **/
+ public Integer UIntValue() { return mInteger; }
+ /**
+ * The double-value of the entry.
+ **/
+ public double DoubleValue() { return mDouble; }
+ /**
+ * True if the entry is uint-valued.
+ **/
+ public boolean IsUInt() { return mIsInteger; }
+ /**
+ * True if the entry is double-valued.
+ **/
+ public boolean IsDouble() { return mIsDouble; }
+
+ /**
+ * The string representation of the the entry's value.
+ **/
+ public String Value()
+ {
+
+
+ if (IsUInt)
+ return mInteger.toString();
+ else if (IsDouble)
+ return mDouble.toString();
+ else
+ throw new Z3Exception("Unknown statistical entry type");
+ }
+
+ /**
+ * The string representation of the Entry.
+ **/
+ public String toString()
+ {
+ return Key + ": " + Value;
+ }
+
+ private boolean mIsInteger = false;
+ private boolean mIsDouble = false;
+ private Integer mInteger = 0;
+ private double mDouble = 0.0;
+ Entry(String k, Integer v) { Key = k; mIsInteger = true; mInteger = v; }
+ Entry(String k, double v) { Key = k; mIsDouble = true; mDouble = v; }
+ }
+
+ /**
+ * A string representation of the statistical data.
+ **/
+ public String toString()
+ {
+ return Native.statstoString(Context.nCtx, NativeObject);
+ }
+
+ /**
+ * The number of statistical data.
+ **/
+ public Integer Size() { return Native.statsSize(Context.nCtx, NativeObject); }
+
+ /**
+ * The data entries.
+ **/
+ public Entry[] Entries()
+ {
+
+
+
+
+ Integer n = Size;
+ Entry[] res = new Entry[n];
+ for (Integer i = 0; i < n; i++)
+ {
+ Entry e;
+ String k = Native.statsGetKey(Context.nCtx, NativeObject, i);
+ if (Native.statsIsInteger(Context.nCtx, NativeObject, i) != 0)
+ e = new Entry(k, Native.statsGetIntegerValue(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;
+ return res;
+ }
+ }
+
+ /**
+ * The statistical counters.
+ **/
+ public String[] Keys()
+ {
+
+
+ Integer n = Size;
+ String[] res = new String[n];
+ for (Integer i = 0; i < n; i++)
+ res[i] = Native.statsGetKey(Context.nCtx, NativeObject, i);
+ return res;
+ }
+
+ /**
+ * The value of a particular statistical counter.
+ * Context.NumTactics
+ * and Context.TacticNames.
+ * It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end.
+ **/
+ public class Tactic extends Z3Object
+ {
+ /**
+ * A string containing a description of parameters accepted by the tactic.
+ **/
+ public String Help()
+ {
+
+
+ return Native.tacticGetHelp(Context.nCtx, NativeObject);
+ }
+
+
+ /**
+ * Retrieves parameter descriptions for Tactics.
+ **/
+ public ParamDescrs ParameterDescriptions() { return new ParamDescrs(Context, Native.tacticGetParamDescrs(Context.nCtx, NativeObject)); }
+
+
+ /**
+ * Execute the tactic over the goal.
+ **/
+ public ApplyResult Apply(Goal g, Params p)
+ {
+
+
+
+ Context.CheckContextMatch(g);
+ if (p == null)
+ 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));
+ }
+ }
+
+ /**
+ * Apply the tactic to a goal.
+ **/
+ public ApplyResult this[Goal g]()
+ {
+
+
+
+ return Apply(g);
+ }
+
+ /**
+ * Creates a solver that is implemented using the given tactic.
+ * ")
+ a = a.replace("[\w,.\(\) ]*)\)", "{ super(\g
);", line)
+ if line.find("; {") != -1:
+ line = line.replace("; {", ";")
+ else:
+ skip_brace = 1
+ if s.startswith("public"):
+ line = re.sub(" = [\w.]+(?P