diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 5bea58054..30d303d6c 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -28,7 +28,8 @@ public class AST extends Z3Object /** * Object comparison. - * @param o another AST + * + * @param o another AST **/ public boolean equals(Object o) { @@ -46,10 +47,12 @@ public class AST extends Z3Object } /** - * Object Comparison. @param other Another AST + * Object Comparison. + * @param other Another AST * - * @return Negative if the object should be sorted before , positive if after else zero. + * @return Negative if the object should be sorted before {@code other}, + * positive if after else zero. + * @throws Z3Exception on error **/ public int compareTo(Object other) throws Z3Exception { @@ -90,6 +93,7 @@ public class AST extends Z3Object /** * A unique identifier for the AST (unique among all ASTs). + * @throws Z3Exception on error **/ public int getId() throws Z3Exception { @@ -97,10 +101,11 @@ public class AST extends Z3Object } /** - * Translates (copies) the AST to the Context . A context + * Translates (copies) the AST to the Context {@code ctx}. + * @param ctx A context * - * @return A copy of the AST which is associated with + * @return A copy of the AST which is associated with {@code ctx} + * @throws Z3Exception on error **/ public AST translate(Context ctx) throws Z3Exception { @@ -114,6 +119,7 @@ public class AST extends Z3Object /** * The kind of the AST. + * @throws Z3Exception on error **/ public Z3_ast_kind getASTKind() throws Z3Exception { @@ -123,6 +129,8 @@ public class AST extends Z3Object /** * Indicates whether the AST is an Expr + * @throws Z3Exception on error + * @throws Z3Exception on error **/ public boolean isExpr() throws Z3Exception { @@ -140,6 +148,8 @@ public class AST extends Z3Object /** * Indicates whether the AST is an application + * @return a boolean + * @throws Z3Exception on error **/ public boolean isApp() throws Z3Exception { @@ -147,7 +157,9 @@ public class AST extends Z3Object } /** - * Indicates whether the AST is a BoundVariable + * Indicates whether the AST is a BoundVariable. + * @return a boolean + * @throws Z3Exception on error **/ public boolean isVar() throws Z3Exception { @@ -156,6 +168,8 @@ public class AST extends Z3Object /** * Indicates whether the AST is a Quantifier + * @return a boolean + * @throws Z3Exception on error **/ public boolean isQuantifier() throws Z3Exception { @@ -213,8 +227,10 @@ public class AST extends Z3Object void incRef(long o) throws Z3Exception { // Console.WriteLine("AST IncRef()"); - if (getContext() == null || o == 0) - return; + if (getContext() == null) + throw new Z3Exception("inc() called on null context"); + if (o == 0) + throw new Z3Exception("inc() called on null AST"); getContext().ast_DRQ().incAndClear(getContext(), o); super.incRef(o); } @@ -222,8 +238,10 @@ public class AST extends Z3Object void decRef(long o) throws Z3Exception { // Console.WriteLine("AST DecRef()"); - if (getContext() == null || o == 0) - return; + if (getContext() == null) + throw new Z3Exception("dec() called on null context"); + if (o == 0) + throw new Z3Exception("dec() called on null AST"); getContext().ast_DRQ().add(o); super.decRef(o); } diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java index a26140a3d..3d63939ca 100644 --- a/src/api/java/ASTMap.java +++ b/src/api/java/ASTMap.java @@ -23,10 +23,10 @@ package com.microsoft.z3; class ASTMap extends Z3Object { /** - * Checks whether the map contains the key . An AST + * Checks whether the map contains the key {@code k}. + * @param k An AST * - * @return True if is a key in the map, false + * @return True if {@code k} is a key in the map, false * otherwise. **/ public boolean contains(AST k) throws Z3Exception @@ -37,9 +37,10 @@ class ASTMap extends Z3Object } /** - * Finds the value associated with the key . - * This function signs an error when is not a key in - * the map. @param k An AST + * Finds the value associated with the key {@code k}. + * Remarks: This function signs an error when {@code k} is not a key in + * the map. + * @param k An AST * * @throws Z3Exception **/ @@ -50,8 +51,9 @@ class ASTMap extends Z3Object } /** - * Stores or replaces a new key/value pair in the map. The - * key AST @param v The value AST + * Stores or replaces a new key/value pair in the map. + * @param k The key AST + * @param v The value AST **/ public void insert(AST k, AST v) throws Z3Exception { @@ -61,12 +63,11 @@ class ASTMap extends Z3Object } /** - * Erases the key from the map. An - * AST + * Erases the key {@code k} from the map. + * @param k An AST **/ public void erase(AST k) throws Z3Exception { - Native.astMapErase(getContext().nCtx(), getNativeObject(), k.getNativeObject()); } diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index 99879848f..d4df02244 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -31,9 +31,10 @@ class ASTVector extends Z3Object } /** - * Retrieves the i-th object in the vector. May throw an - * IndexOutOfBoundsException when is out of - * range. @param i Index + * Retrieves the i-th object in the vector. + * Remarks: May throw an {@code IndexOutOfBoundsException} when + * {@code i} is out of range. + * @param i Index * * @return An AST * @throws Z3Exception @@ -52,8 +53,8 @@ class ASTVector extends Z3Object } /** - * Resize the vector to . The new size of the vector. + * Resize the vector to {@code newSize}. + * @param newSize The new size of the vector. **/ public void resize(int newSize) throws Z3Exception { @@ -61,8 +62,9 @@ class ASTVector extends Z3Object } /** - * Add the AST to the back of the vector. The size is - * increased by 1. @param a An AST + * Add the AST {@code a} to the back of the vector. The size is + * increased by 1. + * @param a An AST **/ public void push(AST a) throws Z3Exception { @@ -70,8 +72,8 @@ class ASTVector extends Z3Object } /** - * Translates all ASTs in the vector to . A context + * Translates all ASTs in the vector to {@code ctx}. + * @param ctx A context * * @return A new ASTVector * @throws Z3Exception diff --git a/src/api/java/AlgebraicNum.java b/src/api/java/AlgebraicNum.java index a45e5a58e..322b24d39 100644 --- a/src/api/java/AlgebraicNum.java +++ b/src/api/java/AlgebraicNum.java @@ -24,28 +24,30 @@ 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^. - * @see Expr.IsAlgebraicNumber the - * precision of the result + * isolating the number is smaller than 1/10^{@code precision}. + * + * @see Expr#isAlgebraicNumber + * @param precision the precision of the result * * @return A numeral Expr of sort Real + * @throws Z3Exception on error **/ public RatNum toUpper(int precision) throws Z3Exception { - return new RatNum(getContext(), - Native.getAlgebraicNumberUpper( - getContext().nCtx(), - getNativeObject(), - precision)); + return new RatNum(getContext(), Native.getAlgebraicNumberUpper(getContext() + .nCtx(), getNativeObject(), precision)); } /** * Return a lower bound for the given real algebraic number. The interval - * isolating the number is smaller than 1/10^. - * @see Expr.IsAlgebraicNumber @param precision + * isolating the number is smaller than 1/10^{@code precision}. + * + * @see Expr#isAlgebraicNumber + * @param precision precision * * @return A numeral Expr of sort Real + * @throws Z3Exception on error **/ public RatNum toLower(int precision) throws Z3Exception { @@ -55,8 +57,11 @@ public class AlgebraicNum extends ArithExpr } /** - * Returns a string representation in decimal notation. The result - * has at most decimal places. + * Returns a string representation in decimal notation. + * Remarks: The result has at most {@code precision} decimal places. + * @param precision precision + * @return String + * @throws Z3Exception on error **/ public String toDecimal(int precision) throws Z3Exception { diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java index c550c05ae..d21a78a9c 100644 --- a/src/api/java/ApplyResult.java +++ b/src/api/java/ApplyResult.java @@ -48,10 +48,10 @@ public class ApplyResult extends Z3Object } /** - * Convert a model for the subgoal into a model for the - * original goal g, that the ApplyResult was obtained from. + * Convert a model for the subgoal {@code i} into a model for the + * original goal {@code g}, that the ApplyResult was obtained from. * - * @return A model for g + * @return A model for {@code g} * @throws Z3Exception **/ public Model convertModel(int i, Model m) throws Z3Exception diff --git a/src/api/java/ArithExpr.java b/src/api/java/ArithExpr.java index 97873f0b0..996b98afc 100644 --- a/src/api/java/ArithExpr.java +++ b/src/api/java/ArithExpr.java @@ -23,7 +23,7 @@ package com.microsoft.z3; public class ArithExpr extends Expr { /** - * Constructor for ArithExpr + * Constructor for ArithExpr **/ ArithExpr(Context ctx, long obj) throws Z3Exception { diff --git a/src/api/java/ArrayExpr.java b/src/api/java/ArrayExpr.java index 2985d19a2..154a56af4 100644 --- a/src/api/java/ArrayExpr.java +++ b/src/api/java/ArrayExpr.java @@ -24,7 +24,7 @@ package com.microsoft.z3; public class ArrayExpr extends Expr { /** - * Constructor for ArrayExpr + * Constructor for ArrayExpr **/ ArrayExpr(Context ctx, long obj) throws Z3Exception { diff --git a/src/api/java/ArraySort.java b/src/api/java/ArraySort.java index a371fa3cb..ab545b7c1 100644 --- a/src/api/java/ArraySort.java +++ b/src/api/java/ArraySort.java @@ -25,6 +25,8 @@ public class ArraySort extends Sort /** * The domain of the array sort. * @throws Z3Exception + * @throws Z3Exception on error + * @return a sort **/ public Sort getDomain() throws Z3Exception { @@ -35,6 +37,8 @@ public class ArraySort extends Sort /** * The range of the array sort. * @throws Z3Exception + * @throws Z3Exception on error + * @return a sort **/ public Sort getRange() throws Z3Exception { diff --git a/src/api/java/BitVecExpr.java b/src/api/java/BitVecExpr.java index a7c704497..69a97de40 100644 --- a/src/api/java/BitVecExpr.java +++ b/src/api/java/BitVecExpr.java @@ -26,6 +26,8 @@ public class BitVecExpr extends Expr /** * The size of the sort of a bit-vector term. * @throws Z3Exception + * @throws Z3Exception on error + * @return an int **/ public int getSortSize() throws Z3Exception { @@ -33,7 +35,7 @@ public class BitVecExpr extends Expr } /** - * Constructor for BitVecExpr + * Constructor for BitVecExpr **/ BitVecExpr(Context ctx, long obj) throws Z3Exception { diff --git a/src/api/java/BitVecSort.java b/src/api/java/BitVecSort.java index be406c806..69d74151c 100644 --- a/src/api/java/BitVecSort.java +++ b/src/api/java/BitVecSort.java @@ -24,6 +24,8 @@ public class BitVecSort extends Sort { /** * The size of the bit-vector sort. + * @throws Z3Exception on error + * @return an int **/ public int getSize() throws Z3Exception { diff --git a/src/api/java/BoolExpr.java b/src/api/java/BoolExpr.java index 8f9d10d18..ea3cdbfb4 100644 --- a/src/api/java/BoolExpr.java +++ b/src/api/java/BoolExpr.java @@ -23,8 +23,17 @@ package com.microsoft.z3; public class BoolExpr extends Expr { /** - * Constructor for BoolExpr + * Constructor for BoolExpr + **/ + protected BoolExpr(Context ctx) + { + super(ctx); + } + + /** + * Constructor for BoolExpr * @throws Z3Exception + * @throws Z3Exception on error **/ BoolExpr(Context ctx, long obj) throws Z3Exception { diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java index 4813c2b0a..a5440092c 100644 --- a/src/api/java/Constructor.java +++ b/src/api/java/Constructor.java @@ -25,6 +25,8 @@ public class Constructor extends Z3Object /** * The number of fields of the constructor. * @throws Z3Exception + * @throws Z3Exception on error + * @return an int **/ public int getNumFields() throws Z3Exception { @@ -34,6 +36,7 @@ public class Constructor extends Z3Object /** * The function declaration of the constructor. * @throws Z3Exception + * @throws Z3Exception on error **/ public FuncDecl ConstructorDecl() throws Z3Exception { @@ -47,6 +50,7 @@ public class Constructor extends Z3Object /** * The function declaration of the tester. * @throws Z3Exception + * @throws Z3Exception on error **/ public FuncDecl getTesterDecl() throws Z3Exception { @@ -60,6 +64,7 @@ public class Constructor extends Z3Object /** * The function declarations of the accessors * @throws Z3Exception + * @throws Z3Exception on error **/ public FuncDecl[] getAccessorDecls() throws Z3Exception { @@ -75,6 +80,7 @@ public class Constructor extends Z3Object /** * Destructor. + * @throws Z3Exception on error **/ protected void finalize() throws Z3Exception { diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java index 315a2e535..b38678b8a 100644 --- a/src/api/java/ConstructorList.java +++ b/src/api/java/ConstructorList.java @@ -24,6 +24,7 @@ public class ConstructorList extends Z3Object { /** * Destructor. + * @throws Z3Exception on error **/ protected void finalize() throws Z3Exception { diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 2b4c47d76..f7fa471fb 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -38,7 +38,7 @@ public class Context extends IDisposable /** * Constructor. - * + * Remarks: * The following parameters can be set: * - proof (Boolean) Enable proof generation * - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting @@ -51,8 +51,7 @@ public class Context extends IDisposable * - model_validate validate models produced by solvers * - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver * Note that in previous versions of Z3, this constructor was also used to set global and - * module parameters. For this purpose we should now use - * + * module parameters. For this purpose we should now use {@code Global.setParameter} **/ public Context(Map settings) throws Z3Exception { @@ -66,9 +65,9 @@ public class Context extends IDisposable } /** - * Creates a new symbol using an integer. Not all integers can be - * passed to this function. The legal range of unsigned integers is 0 to - * 2^30-1. + * Creates a new symbol using an integer. + * Remarks: Not all integers can be passed to this function. + * The legal range of unsigned integers is 0 to 2^30-1. **/ public IntSymbol mkSymbol(int i) throws Z3Exception { @@ -135,7 +134,6 @@ public class Context extends IDisposable **/ public BoolSort mkBoolSort() throws Z3Exception { - return new BoolSort(this); } @@ -144,7 +142,6 @@ public class Context extends IDisposable **/ public UninterpretedSort mkUninterpretedSort(Symbol s) throws Z3Exception { - checkContextMatch(s); return new UninterpretedSort(this, s); } @@ -154,7 +151,6 @@ public class Context extends IDisposable **/ public UninterpretedSort mkUninterpretedSort(String str) throws Z3Exception { - return mkUninterpretedSort(mkSymbol(str)); } @@ -163,7 +159,6 @@ public class Context extends IDisposable **/ public IntSort mkIntSort() throws Z3Exception { - return new IntSort(this); } @@ -172,7 +167,6 @@ public class Context extends IDisposable **/ public RealSort mkRealSort() throws Z3Exception { - return new RealSort(this); } @@ -181,7 +175,6 @@ public class Context extends IDisposable **/ public BitVecSort mkBitVecSort(int size) throws Z3Exception { - return new BitVecSort(this, Native.mkBvSort(nCtx(), size)); } @@ -190,7 +183,6 @@ public class Context extends IDisposable **/ public ArraySort mkArraySort(Sort domain, Sort range) throws Z3Exception { - checkContextMatch(domain); checkContextMatch(range); return new ArraySort(this, domain, range); @@ -202,7 +194,6 @@ public class Context extends IDisposable public TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts) throws Z3Exception { - checkContextMatch(name); checkContextMatch(fieldNames); checkContextMatch(fieldSorts); @@ -216,7 +207,6 @@ public class Context extends IDisposable public EnumSort mkEnumSort(Symbol name, Symbol... enumNames) throws Z3Exception { - checkContextMatch(name); checkContextMatch(enumNames); return new EnumSort(this, name, enumNames); @@ -236,7 +226,6 @@ public class Context extends IDisposable **/ public ListSort mkListSort(Symbol name, Sort elemSort) throws Z3Exception { - checkContextMatch(name); checkContextMatch(elemSort); return new ListSort(this, name, elemSort); @@ -247,7 +236,6 @@ public class Context extends IDisposable **/ public ListSort mkListSort(String name, Sort elemSort) throws Z3Exception { - checkContextMatch(elemSort); return new ListSort(this, mkSymbol(name), elemSort); } @@ -258,7 +246,6 @@ public class Context extends IDisposable public FiniteDomainSort mkFiniteDomainSort(Symbol name, long size) throws Z3Exception { - checkContextMatch(name); return new FiniteDomainSort(this, name, size); } @@ -269,20 +256,19 @@ public class Context extends IDisposable public FiniteDomainSort mkFiniteDomainSort(String name, long size) throws Z3Exception { - return new FiniteDomainSort(this, mkSymbol(name), size); } /** - * Create a datatype constructor. constructor - * name name of recognizer - * function. names of the constructor - * fields. field sorts, 0 if the field sort - * refers to a recursive sort. reference to - * datatype sort that is an argument to the constructor; if the - * corresponding sort reference is 0, then the value in sort_refs should be + * Create a datatype constructor. + * @param name constructor name + * @param recognizer name of recognizer function. + * @param fieldNames names of the constructor fields. + * @param sorts field sorts, 0 if the field sort refers to a recursive sort. + * @param sortRefs reference to datatype sort that is an argument to the + * constructor; if the corresponding sort reference is 0, then the value in sort_refs should be * an index referring to one of the recursive datatypes that is - * declared. + * declared. **/ public Constructor mkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) @@ -294,9 +280,12 @@ public class Context extends IDisposable } /** - * Create a datatype constructor. @param name @param fieldNames @param sortRefs + * Create a datatype constructor. + * @param name + * @param recognizer + * @param fieldNames + * @param sorts + * @param sortRefs * * @return **/ @@ -315,7 +304,6 @@ public class Context extends IDisposable public DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors) throws Z3Exception { - checkContextMatch(name); checkContextMatch(constructors); return new DatatypeSort(this, name, constructors); @@ -327,20 +315,18 @@ public class Context extends IDisposable public DatatypeSort mkDatatypeSort(String name, Constructor[] constructors) throws Z3Exception { - checkContextMatch(constructors); return new DatatypeSort(this, mkSymbol(name), constructors); } /** - * Create mutually recursive datatypes. names of - * datatype sorts list of constructors, one list per - * sort. + * Create mutually recursive datatypes. + * @param names names of datatype sorts + * @param c list of constructors, one list per sort. **/ public DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c) throws Z3Exception { - checkContextMatch(names); int n = (int) names.length; ConstructorList[] cla = new ConstructorList[n]; @@ -363,15 +349,15 @@ public class Context extends IDisposable } /** - * Create mutually recursive data-types. @param names + * Create mutually recursive data-types. + * @param names + * @param c * * @return **/ public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c) throws Z3Exception { - return mkDatatypeSorts(MkSymbols(names), c); } @@ -381,7 +367,6 @@ public class Context extends IDisposable public FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range) throws Z3Exception { - checkContextMatch(name); checkContextMatch(domain); checkContextMatch(range); @@ -394,7 +379,6 @@ public class Context extends IDisposable public FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range) throws Z3Exception { - checkContextMatch(name); checkContextMatch(domain); checkContextMatch(range); @@ -408,7 +392,6 @@ public class Context extends IDisposable public FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range) throws Z3Exception { - checkContextMatch(domain); checkContextMatch(range); return new FuncDecl(this, mkSymbol(name), domain, range); @@ -420,7 +403,6 @@ public class Context extends IDisposable public FuncDecl mkFuncDecl(String name, Sort domain, Sort range) throws Z3Exception { - checkContextMatch(domain); checkContextMatch(range); Sort[] q = new Sort[] { domain }; @@ -428,14 +410,14 @@ public class Context extends IDisposable } /** - * Creates a fresh function declaration with a name prefixed with . @see MkFuncDecl(string,Sort,Sort) + * Creates a fresh function declaration with a name prefixed with + * {@code prefix}. + * @see mkFuncDecl(String,Sort,Sort) + * @see mkFuncDecl(String,Sort[],Sort) **/ public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range) throws Z3Exception { - checkContextMatch(domain); checkContextMatch(range); return new FuncDecl(this, prefix, domain, range); @@ -446,7 +428,6 @@ public class Context extends IDisposable **/ public FuncDecl mkConstDecl(Symbol name, Sort range) throws Z3Exception { - checkContextMatch(name); checkContextMatch(range); return new FuncDecl(this, name, null, range); @@ -457,27 +438,27 @@ public class Context extends IDisposable **/ public FuncDecl mkConstDecl(String name, Sort range) throws Z3Exception { - checkContextMatch(range); return new FuncDecl(this, mkSymbol(name), null, range); } /** * Creates a fresh constant function declaration with a name prefixed with - * . @see MkFuncDecl(string,Sort,Sort) - * @see MkFuncDecl(string,Sort[],Sort) + * {@code prefix"}. + * @see mkFuncDecl(String,Sort,Sort) + * @see mkFuncDecl(String,Sort[],Sort) **/ public FuncDecl mkFreshConstDecl(String prefix, Sort range) throws Z3Exception { - checkContextMatch(range); return new FuncDecl(this, prefix, null, range); } /** - * Creates a new bound variable. The de-Bruijn index of - * the variable @param ty The sort of the variable + * Creates a new bound variable. + * @param index The de-Bruijn index of the variable + * @param ty The sort of the variable **/ public Expr mkBound(int index, Sort ty) throws Z3Exception { @@ -499,46 +480,46 @@ public class Context extends IDisposable } /** - * Creates a new Constant of sort and named - * . + * Creates a new Constant of sort {@code range} and named + * {@code name}. **/ public Expr mkConst(Symbol name, Sort range) throws Z3Exception { checkContextMatch(name); checkContextMatch(range); - return Expr.create(this, Native.mkConst(nCtx(), name.getNativeObject(), range.getNativeObject())); + return Expr.create( + this, + Native.mkConst(nCtx(), name.getNativeObject(), + range.getNativeObject())); } /** - * Creates a new Constant of sort and named - * . + * Creates a new Constant of sort {@code range} and named + * {@code name}. **/ public Expr mkConst(String name, Sort range) throws Z3Exception { - return mkConst(mkSymbol(name), range); } /** - * Creates a fresh Constant of sort and a name - * prefixed with . + * Creates a fresh Constant of sort {@code range} and a name + * prefixed with {@code prefix}. **/ public Expr mkFreshConst(String prefix, Sort range) throws Z3Exception { - checkContextMatch(range); return Expr.create(this, Native.mkFreshConst(nCtx(), prefix, range.getNativeObject())); } /** - * Creates a fresh constant from the FuncDecl . A decl of a 0-arity function + * Creates a fresh constant from the FuncDecl {@code f}. + * @param f A decl of a 0-arity function **/ public Expr mkConst(FuncDecl f) throws Z3Exception { - return mkApp(f, (Expr[]) null); } @@ -547,7 +528,6 @@ public class Context extends IDisposable **/ public BoolExpr mkBoolConst(Symbol name) throws Z3Exception { - return (BoolExpr) mkConst(name, getBoolSort()); } @@ -556,7 +536,6 @@ public class Context extends IDisposable **/ public BoolExpr mkBoolConst(String name) throws Z3Exception { - return (BoolExpr) mkConst(mkSymbol(name), getBoolSort()); } @@ -565,7 +544,6 @@ public class Context extends IDisposable **/ public IntExpr mkIntConst(Symbol name) throws Z3Exception { - return (IntExpr) mkConst(name, getIntSort()); } @@ -574,7 +552,6 @@ public class Context extends IDisposable **/ public IntExpr mkIntConst(String name) throws Z3Exception { - return (IntExpr) mkConst(name, getIntSort()); } @@ -583,7 +560,6 @@ public class Context extends IDisposable **/ public RealExpr mkRealConst(Symbol name) throws Z3Exception { - return (RealExpr) mkConst(name, getRealSort()); } @@ -592,7 +568,6 @@ public class Context extends IDisposable **/ public RealExpr mkRealConst(String name) throws Z3Exception { - return (RealExpr) mkConst(name, getRealSort()); } @@ -601,7 +576,6 @@ public class Context extends IDisposable **/ public BitVecExpr mkBVConst(Symbol name, int size) throws Z3Exception { - return (BitVecExpr) mkConst(name, mkBitVecSort(size)); } @@ -610,7 +584,6 @@ public class Context extends IDisposable **/ public BitVecExpr mkBVConst(String name, int size) throws Z3Exception { - return (BitVecExpr) mkConst(name, mkBitVecSort(size)); } @@ -649,7 +622,7 @@ public class Context extends IDisposable } /** - * Creates the equality = . + * Creates the equality {@code x"/> = An expression with Boolean - * sort @param t2 An expression An - * expression with the same sort as + * {@code ite(t1, t2, t3)}. + * @param t1 An expression with Boolean sort + * @param t2 An expression + * @param t3 An expression with the same sort as {@code t2} **/ public Expr mkITE(BoolExpr t1, Expr t2, Expr t3) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); checkContextMatch(t3); @@ -696,11 +668,10 @@ public class Context extends IDisposable } /** - * Create an expression representing t1 iff t2. + * Create an expression representing {@code t1 iff t2}. **/ public BoolExpr mkIff(BoolExpr t1, BoolExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(), @@ -708,11 +679,10 @@ public class Context extends IDisposable } /** - * Create an expression representing t1 -> t2. + * Create an expression representing {@code t1 -> t2}. **/ public BoolExpr mkImplies(BoolExpr t1, BoolExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkImplies(nCtx(), @@ -720,11 +690,10 @@ public class Context extends IDisposable } /** - * Create an expression representing t1 xor t2. + * Create an expression representing {@code t1 xor t2}. **/ public BoolExpr mkXor(BoolExpr t1, BoolExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(), @@ -732,77 +701,70 @@ public class Context extends IDisposable } /** - * Create an expression representing t[0] and t[1] and .... + * Create an expression representing {@code t[0] and t[1] and ...}. **/ public BoolExpr mkAnd(BoolExpr... t) throws Z3Exception { - checkContextMatch(t); return new BoolExpr(this, Native.mkAnd(nCtx(), (int) t.length, AST.arrayToNative(t))); } /** - * Create an expression representing t[0] or t[1] or .... + * Create an expression representing {@code t[0] or t[1] or ...}. **/ public BoolExpr mkOr(BoolExpr... t) throws Z3Exception { - checkContextMatch(t); return new BoolExpr(this, Native.mkOr(nCtx(), (int) t.length, AST.arrayToNative(t))); } /** - * Create an expression representing t[0] + t[1] + .... + * Create an expression representing {@code t[0] + t[1] + ...}. **/ public ArithExpr mkAdd(ArithExpr... t) throws Z3Exception { - checkContextMatch(t); return (ArithExpr) Expr.create(this, Native.mkAdd(nCtx(), (int) t.length, AST.arrayToNative(t))); } /** - * Create an expression representing t[0] * t[1] * .... + * Create an expression representing {@code t[0] * t[1] * ...}. **/ public ArithExpr mkMul(ArithExpr... t) throws Z3Exception { - checkContextMatch(t); return (ArithExpr) Expr.create(this, Native.mkMul(nCtx(), (int) t.length, AST.arrayToNative(t))); } /** - * Create an expression representing t[0] - t[1] - .... + * Create an expression representing {@code t[0] - t[1] - ...}. **/ public ArithExpr mkSub(ArithExpr... t) throws Z3Exception { - checkContextMatch(t); return (ArithExpr) Expr.create(this, Native.mkSub(nCtx(), (int) t.length, AST.arrayToNative(t))); } /** - * Create an expression representing -t. + * Create an expression representing {@code -t}. **/ public ArithExpr mkUnaryMinus(ArithExpr t) throws Z3Exception { - checkContextMatch(t); return (ArithExpr) Expr.create(this, Native.mkUnaryMinus(nCtx(), t.getNativeObject())); } /** - * Create an expression representing t1 / t2. + * Create an expression representing {@code t1 / t2}. **/ public ArithExpr mkDiv(ArithExpr t1, ArithExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(), @@ -810,12 +772,12 @@ public class Context extends IDisposable } /** - * Create an expression representing t1 mod t2. The - * arguments must have int type. + * Create an expression representing {@code t1 mod t2}. + * Remarks: The + * arguments must have int type. **/ public IntExpr mkMod(IntExpr t1, IntExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(), @@ -823,12 +785,12 @@ public class Context extends IDisposable } /** - * Create an expression representing t1 rem t2. The - * arguments must have int type. + * Create an expression representing {@code t1 rem t2}. + * Remarks: The + * arguments must have int type. **/ public IntExpr mkRem(IntExpr t1, IntExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(), @@ -836,11 +798,10 @@ public class Context extends IDisposable } /** - * Create an expression representing t1 ^ t2. + * Create an expression representing {@code t1 ^ t2}. **/ public ArithExpr mkPower(ArithExpr t1, ArithExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return (ArithExpr) Expr.create( @@ -850,11 +811,10 @@ public class Context extends IDisposable } /** - * Create an expression representing t1 < t2 + * Create an expression representing {@code t1 < t2} **/ public BoolExpr mkLt(ArithExpr t1, ArithExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(), @@ -862,11 +822,10 @@ public class Context extends IDisposable } /** - * Create an expression representing t1 <= t2 + * Create an expression representing {@code t1 <= t2} **/ public BoolExpr mkLe(ArithExpr t1, ArithExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(), @@ -874,11 +833,10 @@ public class Context extends IDisposable } /** - * Create an expression representing t1 > t2 + * Create an expression representing {@code t1 > t2} **/ public BoolExpr mkGt(ArithExpr t1, ArithExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(), @@ -886,11 +844,10 @@ public class Context extends IDisposable } /** - * Create an expression representing t1 >= t2 + * Create an expression representing {@code t1 >= t2} **/ public BoolExpr mkGe(ArithExpr t1, ArithExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(), @@ -898,30 +855,30 @@ public class Context extends IDisposable } /** - * Coerce an integer to a real. There is also a converse operation + * Coerce an integer to a real. + * Remarks: There is also a converse operation * exposed. It follows the semantics prescribed by the SMT-LIB standard. * * You can take the floor of a real by creating an auxiliary integer Term - * k and and asserting - * MakeInt2Real(k) <= t1 < MkInt2Real(k)+1. The argument - * must be of integer sort. + * {@code k} and and asserting + * {@code MakeInt2Real(k) <= t1 < MkInt2Real(k)+1}. The argument + * must be of integer sort. **/ public RealExpr mkInt2Real(IntExpr t) throws Z3Exception { - checkContextMatch(t); return new RealExpr(this, Native.mkInt2real(nCtx(), t.getNativeObject())); } /** - * Coerce a real to an integer. The semantics of this function + * Coerce a real to an integer. + * Remarks: The semantics of this function * follows the SMT-LIB standard for the function to_int. The argument must - * be of real sort. + * be of real sort. **/ public IntExpr mkReal2Int(RealExpr t) throws Z3Exception { - checkContextMatch(t); return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject())); } @@ -931,29 +888,28 @@ public class Context extends IDisposable **/ public BoolExpr mkIsInteger(RealExpr t) throws Z3Exception { - checkContextMatch(t); return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject())); } /** - * Bitwise negation. The argument must have a bit-vector - * sort. + * Bitwise negation. + * Remarks: The argument must have a bit-vector + * sort. **/ public BitVecExpr mkBVNot(BitVecExpr t) throws Z3Exception { - checkContextMatch(t); return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject())); } /** * Take conjunction of bits in a vector, return vector of length 1. - * The argument must have a bit-vector sort. + * + * Remarks: The argument must have a bit-vector sort. **/ public BitVecExpr mkBVRedAND(BitVecExpr t) throws Z3Exception { - checkContextMatch(t); return new BitVecExpr(this, Native.mkBvredand(nCtx(), t.getNativeObject())); @@ -961,23 +917,23 @@ public class Context extends IDisposable /** * Take disjunction of bits in a vector, return vector of length 1. - * The argument must have a bit-vector sort. + * + * Remarks: The argument must have a bit-vector sort. **/ public BitVecExpr mkBVRedOR(BitVecExpr t) throws Z3Exception { - checkContextMatch(t); return new BitVecExpr(this, Native.mkBvredor(nCtx(), t.getNativeObject())); } /** - * Bitwise conjunction. The arguments must have a bit-vector - * sort. + * Bitwise conjunction. + * Remarks: The arguments must have a bit-vector + * sort. **/ public BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvand(nCtx(), @@ -985,12 +941,12 @@ public class Context extends IDisposable } /** - * Bitwise disjunction. The arguments must have a bit-vector - * sort. + * Bitwise disjunction. + * Remarks: The arguments must have a bit-vector + * sort. **/ public BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(), @@ -998,12 +954,12 @@ public class Context extends IDisposable } /** - * Bitwise XOR. The arguments must have a bit-vector - * sort. + * Bitwise XOR. + * Remarks: The arguments must have a bit-vector + * sort. **/ public BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvxor(nCtx(), @@ -1011,12 +967,12 @@ public class Context extends IDisposable } /** - * Bitwise NAND. The arguments must have a bit-vector - * sort. + * Bitwise NAND. + * Remarks: The arguments must have a bit-vector + * sort. **/ public BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvnand(nCtx(), @@ -1024,12 +980,12 @@ public class Context extends IDisposable } /** - * Bitwise NOR. The arguments must have a bit-vector - * sort. + * Bitwise NOR. + * Remarks: The arguments must have a bit-vector + * sort. **/ public BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvnor(nCtx(), @@ -1037,12 +993,12 @@ public class Context extends IDisposable } /** - * Bitwise XNOR. The arguments must have a bit-vector - * sort. + * Bitwise XNOR. + * Remarks: The arguments must have a bit-vector + * sort. **/ public BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvxnor(nCtx(), @@ -1050,23 +1006,23 @@ public class Context extends IDisposable } /** - * Standard two's complement unary minus. The arguments must have a - * bit-vector sort. + * Standard two's complement unary minus. + * Remarks: The arguments must have a + * bit-vector sort. **/ public BitVecExpr mkBVNeg(BitVecExpr t) throws Z3Exception { - checkContextMatch(t); return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject())); } /** - * Two's complement addition. The arguments must have the same - * bit-vector sort. + * Two's complement addition. + * Remarks: The arguments must have the same + * bit-vector sort. **/ public BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvadd(nCtx(), @@ -1074,12 +1030,12 @@ public class Context extends IDisposable } /** - * Two's complement subtraction. The arguments must have the same - * bit-vector sort. + * Two's complement subtraction. + * Remarks: The arguments must have the same + * bit-vector sort. **/ public BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvsub(nCtx(), @@ -1087,12 +1043,12 @@ public class Context extends IDisposable } /** - * Two's complement multiplication. The arguments must have the - * same bit-vector sort. + * Two's complement multiplication. + * Remarks: The arguments must have the + * same bit-vector sort. **/ public BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvmul(nCtx(), @@ -1100,14 +1056,14 @@ public class Context extends IDisposable } /** - * Unsigned division. It is defined as the floor of - * t1/t2 if \c t2 is different from zero. If t2 is + * Unsigned division. + * Remarks: It is defined as the floor of + * {@code t1/t2} if \c t2 is different from zero. If {@code t2} is * zero, then the result is undefined. The arguments must have the same - * bit-vector sort. + * bit-vector sort. **/ public BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvudiv(nCtx(), @@ -1115,20 +1071,20 @@ public class Context extends IDisposable } /** - * Signed division. It is defined in the following way: + * Signed division. + * Remarks: It is defined in the following way: * - * - The \c floor of t1/t2 if \c t2 is different from zero, and - * t1*t2 >= 0. + * - The \c floor of {@code t1/t2} if \c t2 is different from zero, and + * {@code t1*t2 >= 0}. * - * - The \c ceiling of t1/t2 if \c t2 is different from zero, - * and t1*t2 < 0. + * - The \c ceiling of {@code t1/t2} if \c t2 is different from zero, + * and {@code t1*t2 < 0}. * - * If t2 is zero, then the result is undefined. The arguments - * must have the same bit-vector sort. + * If {@code t2} is zero, then the result is undefined. The arguments + * must have the same bit-vector sort. **/ public BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvsdiv(nCtx(), @@ -1136,14 +1092,14 @@ public class Context extends IDisposable } /** - * Unsigned remainder. It is defined as - * 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. + * Unsigned remainder. + * Remarks: It is defined as + * {@code t1 - (t1 /u t2) * t2}, where {@code /u} represents + * unsigned division. If {@code t2} is zero, then the result is + * undefined. The arguments must have the same bit-vector sort. **/ public BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvurem(nCtx(), @@ -1151,17 +1107,17 @@ public class Context extends IDisposable } /** - * Signed remainder. It is defined as - * t1 - (t1 /s t2) * t2, where /s represents + * Signed remainder. + * Remarks: It is defined as + * {@code t1 - (t1 /s t2) * t2}, where {@code /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. + * If {@code t2} is zero, then the result is undefined. The arguments + * must have the same bit-vector sort. **/ public BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvsrem(nCtx(), @@ -1169,13 +1125,13 @@ public class Context extends IDisposable } /** - * Two's complement signed remainder (sign follows divisor). If - * t2 is zero, then the result is undefined. The arguments must - * have the same bit-vector sort. + * Two's complement signed remainder (sign follows divisor). + * Remarks: If + * {@code t2} is zero, then the result is undefined. The arguments must + * have the same bit-vector sort. **/ public BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvsmod(nCtx(), @@ -1183,12 +1139,12 @@ public class Context extends IDisposable } /** - * Unsigned less-than The arguments must have the same bit-vector - * sort. + * Unsigned less-than + * Remarks: The arguments must have the same bit-vector + * sort. **/ public BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(), @@ -1196,12 +1152,12 @@ public class Context extends IDisposable } /** - * Two's complement signed less-than The arguments must have the - * same bit-vector sort. + * Two's complement signed less-than + * Remarks: The arguments must have the + * same bit-vector sort. **/ public BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(), @@ -1209,12 +1165,12 @@ public class Context extends IDisposable } /** - * Unsigned less-than or equal to. The arguments must have the - * same bit-vector sort. + * Unsigned less-than or equal to. + * Remarks: The arguments must have the + * same bit-vector sort. **/ public BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(), @@ -1222,12 +1178,12 @@ public class Context extends IDisposable } /** - * Two's complement signed less-than or equal to. The arguments - * must have the same bit-vector sort. + * Two's complement signed less-than or equal to. + * Remarks: The arguments + * must have the same bit-vector sort. **/ public BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(), @@ -1235,12 +1191,12 @@ public class Context extends IDisposable } /** - * Unsigned greater than or equal to. The arguments must have the - * same bit-vector sort. + * Unsigned greater than or equal to. + * Remarks: The arguments must have the + * same bit-vector sort. **/ public BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(), @@ -1248,12 +1204,12 @@ public class Context extends IDisposable } /** - * Two's complement signed greater than or equal to. The arguments - * must have the same bit-vector sort. + * Two's complement signed greater than or equal to. + * Remarks: The arguments + * must have the same bit-vector sort. **/ public BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(), @@ -1261,12 +1217,12 @@ public class Context extends IDisposable } /** - * Unsigned greater-than. The arguments must have the same - * bit-vector sort. + * Unsigned greater-than. + * Remarks: The arguments must have the same + * bit-vector sort. **/ public BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(), @@ -1274,12 +1230,12 @@ public class Context extends IDisposable } /** - * Two's complement signed greater-than. The arguments must have - * the same bit-vector sort. + * Two's complement signed greater-than. + * Remarks: The arguments must have + * the same bit-vector sort. **/ public BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(), @@ -1287,17 +1243,17 @@ public class Context extends IDisposable } /** - * Bit-vector concatenation. The arguments must have a bit-vector - * sort. + * Bit-vector concatenation. + * Remarks: The arguments must have a bit-vector + * sort. * - * @return The result is a bit-vector of size n1+n2, where - * n1 (n2) is the size of t1 - * (t2). + * @return The result is a bit-vector of size {@code n1+n2}, where + * {@code n1} ({@code n2}) is the size of {@code t1} + * ({@code t2}). * **/ public BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkConcat(nCtx(), @@ -1305,74 +1261,74 @@ public class Context extends IDisposable } /** - * Bit-vector extraction. Extract the bits - * down to from a bitvector of size m to - * yield a new bitvector of size n, where - * n = high - low + 1. The argument must - * have a bit-vector sort. + * Bit-vector extraction. + * Remarks: Extract the bits {@code high} + * down to {@code low} from a bitvector of size {@code m} to + * yield a new bitvector of size {@code n}, where + * {@code n = high - low + 1}. The argument {@code t} must + * have a bit-vector sort. **/ public BitVecExpr mkExtract(int high, int low, BitVecExpr t) throws Z3Exception { - checkContextMatch(t); return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low, t.getNativeObject())); } /** - * Bit-vector sign extension. Sign-extends the given bit-vector to - * the (signed) equivalent bitvector of size m+i, where \c m is - * the size of the given bit-vector. The argument must - * have a bit-vector sort. + * Bit-vector sign extension. + * Remarks: Sign-extends the given bit-vector to + * the (signed) equivalent bitvector of size {@code m+i}, where \c m is + * the size of the given bit-vector. The argument {@code t} must + * have a bit-vector sort. **/ public BitVecExpr mkSignExt(int i, BitVecExpr t) throws Z3Exception { - checkContextMatch(t); return new BitVecExpr(this, Native.mkSignExt(nCtx(), i, t.getNativeObject())); } /** - * Bit-vector zero extension. Extend the given bit-vector with - * zeros to the (unsigned) equivalent bitvector of size m+i, - * where \c m is the size of the given bit-vector. The argument must have a bit-vector sort. + * Bit-vector zero extension. + * Remarks: Extend the given bit-vector with + * zeros to the (unsigned) equivalent bitvector of size {@code m+i}, + * where \c m is the size of the given bit-vector. The argument {@code t} + * must have a bit-vector sort. **/ public BitVecExpr mkZeroExt(int i, BitVecExpr t) throws Z3Exception { - checkContextMatch(t); return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i, t.getNativeObject())); } /** - * Bit-vector repetition. The argument must - * have a bit-vector sort. + * Bit-vector repetition. + * Remarks: The argument {@code t} must + * have a bit-vector sort. **/ public BitVecExpr mkRepeat(int i, BitVecExpr t) throws Z3Exception { - checkContextMatch(t); return new BitVecExpr(this, Native.mkRepeat(nCtx(), i, t.getNativeObject())); } /** - * Shift left. It is equivalent to multiplication by - * 2^x where \c x is the value of . + * Shift left. + * Remarks: It is equivalent to multiplication by + * {@code 2^x} where \c x is the value of {@code t2}. * * NB. The semantics of shift operations varies between environments. This * definition does not necessarily capture directly the semantics of the * programming language or assembly architecture you are modeling. * - * The arguments must have a bit-vector sort. + * The arguments must have a bit-vector sort. **/ public BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvshl(nCtx(), @@ -1380,18 +1336,18 @@ public class Context extends IDisposable } /** - * Logical shift right It is equivalent to unsigned division by - * 2^x where \c x is the value of . + * Logical shift right + * Remarks: It is equivalent to unsigned division by + * {@code 2^x} where \c x is the value of {@code t2}. * * NB. The semantics of shift operations varies between environments. This * definition does not necessarily capture directly the semantics of the * programming language or assembly architecture you are modeling. * - * The arguments must have a bit-vector sort. + * The arguments must have a bit-vector sort. **/ public BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvlshr(nCtx(), @@ -1399,7 +1355,8 @@ public class Context extends IDisposable } /** - * Arithmetic shift right It is like logical shift right except + * Arithmetic shift right + * Remarks: It is like logical shift right except * that the most significant bits of the result always copy the most * significant bit of the second argument. * @@ -1407,11 +1364,10 @@ public class Context extends IDisposable * definition does not necessarily capture directly the semantics of the * programming language or assembly architecture you are modeling. * - * The arguments must have a bit-vector sort. + * The arguments must have a bit-vector sort. **/ public BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvashr(nCtx(), @@ -1419,38 +1375,38 @@ public class Context extends IDisposable } /** - * Rotate Left. Rotate bits of \c t to the left \c i times. The - * argument must have a bit-vector sort. + * Rotate Left. + * Remarks: Rotate bits of \c t to the left \c i times. The + * argument {@code t} must have a bit-vector sort. **/ public BitVecExpr mkBVRotateLeft(int i, BitVecExpr t) throws Z3Exception { - checkContextMatch(t); return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i, t.getNativeObject())); } /** - * Rotate Right. Rotate bits of \c t to the right \c i times. The - * argument must have a bit-vector sort. + * Rotate Right. + * Remarks: Rotate bits of \c t to the right \c i times. The + * argument {@code t} must have a bit-vector sort. **/ public BitVecExpr mkBVRotateRight(int i, BitVecExpr t) throws Z3Exception { - checkContextMatch(t); return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i, t.getNativeObject())); } /** - * Rotate Left. Rotate bits of to the left - * times. The arguments must have the same bit-vector - * sort. + * Rotate Left. + * Remarks: Rotate bits of {@code t1} to the left + * {@code t2} times. The arguments must have the same bit-vector + * sort. **/ public BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(), @@ -1458,14 +1414,14 @@ public class Context extends IDisposable } /** - * Rotate Right. Rotate bits of to the - * right times. The arguments must have the same - * bit-vector sort. + * Rotate Right. + * Remarks: Rotate bits of {@code t1} to the + * right{@code t2} times. The arguments must have the same + * bit-vector sort. **/ public BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(), @@ -1473,38 +1429,37 @@ public class Context extends IDisposable } /** - * Create an bit bit-vector from the integer argument - * . NB. This function is essentially treated + * Create an {@code n} bit bit-vector from the integer argument + * {@code t}. + * Remarks: NB. This function is essentially treated * as uninterpreted. So you cannot expect Z3 to precisely reflect the * semantics of this function when solving constraints with this function. * - * The argument must be of integer sort. + * The argument must be of integer sort. **/ public BitVecExpr mkInt2BV(int n, IntExpr t) throws Z3Exception { - checkContextMatch(t); return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n, t.getNativeObject())); } /** - * Create an integer from the bit-vector argument . - * If \c is_signed is false, then the bit-vector \c t1 is treated + * Create an integer from the bit-vector argument {@code t}. + * Remarks: If \c is_signed is false, then the bit-vector \c t1 is treated * as unsigned. So the result is non-negative and in the range - * [0..2^N-1], where N are the number of bits in . If \c is_signed is true, \c t1 is treated as a signed + * {@code [0..2^N-1]}, where N are the number of bits in {@code t}. + * If \c is_signed is true, \c t1 is treated as a signed * bit-vector. * * NB. This function is essentially treated as uninterpreted. So you cannot * expect Z3 to precisely reflect the semantics of this function when * solving constraints with this function. * - * The argument must be of bit-vector sort. + * The argument must be of bit-vector sort. **/ public IntExpr mkBV2Int(BitVecExpr t, boolean signed) throws Z3Exception { - checkContextMatch(t); return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(), (signed) ? true : false)); @@ -1512,12 +1467,12 @@ public class Context extends IDisposable /** * Create a predicate that checks that the bit-wise addition does not - * overflow. The arguments must be of bit-vector sort. + * overflow. + * Remarks: The arguments must be of bit-vector sort. **/ public BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1 @@ -1527,12 +1482,12 @@ public class Context extends IDisposable /** * Create a predicate that checks that the bit-wise addition does not - * underflow. The arguments must be of bit-vector sort. + * underflow. + * Remarks: The arguments must be of bit-vector sort. **/ public BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(), @@ -1541,12 +1496,12 @@ public class Context extends IDisposable /** * Create a predicate that checks that the bit-wise subtraction does not - * overflow. The arguments must be of bit-vector sort. + * overflow. + * Remarks: The arguments must be of bit-vector sort. **/ public BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(), @@ -1555,12 +1510,12 @@ public class Context extends IDisposable /** * Create a predicate that checks that the bit-wise subtraction does not - * underflow. The arguments must be of bit-vector sort. + * underflow. + * Remarks: The arguments must be of bit-vector sort. **/ public BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1 @@ -1570,12 +1525,12 @@ public class Context extends IDisposable /** * Create a predicate that checks that the bit-wise signed division does not - * overflow. The arguments must be of bit-vector sort. + * overflow. + * Remarks: The arguments must be of bit-vector sort. **/ public BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(), @@ -1584,11 +1539,11 @@ public class Context extends IDisposable /** * Create a predicate that checks that the bit-wise negation does not - * overflow. The arguments must be of bit-vector sort. + * overflow. + * Remarks: The arguments must be of bit-vector sort. **/ public BoolExpr mkBVNegNoOverflow(BitVecExpr t) throws Z3Exception { - checkContextMatch(t); return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(), t.getNativeObject())); @@ -1596,12 +1551,12 @@ public class Context extends IDisposable /** * Create a predicate that checks that the bit-wise multiplication does not - * overflow. The arguments must be of bit-vector sort. + * overflow. + * Remarks: The arguments must be of bit-vector sort. **/ public BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1 @@ -1611,12 +1566,12 @@ public class Context extends IDisposable /** * Create a predicate that checks that the bit-wise multiplication does not - * underflow. The arguments must be of bit-vector sort. + * underflow. + * Remarks: The arguments must be of bit-vector sort. **/ public BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(), @@ -1629,7 +1584,6 @@ public class Context extends IDisposable public ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range) throws Z3Exception { - return (ArrayExpr) mkConst(name, mkArraySort(domain, range)); } @@ -1639,22 +1593,24 @@ public class Context extends IDisposable public ArrayExpr mkArrayConst(String name, Sort domain, Sort range) throws Z3Exception { - return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range)); } /** - * Array read. The argument a is the array and - * i is the index of the array that gets read. + * Array read. + * Remarks: The argument {@code a} is the array and + * {@code 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. - * @see MkArraySort"/> @see MkSelect + * array that is equal to {@code a} (with respect to + * {@code select}) on all indices except for {@code i}, where it + * maps to {@code v} (and the {@code select} of {@code a} + * with respect to {@code i} may be a different value). + * @see mkArraySort + * @see mkSelect + **/ public ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v) throws Z3Exception { - checkContextMatch(a); checkContextMatch(i); checkContextMatch(v); @@ -1687,14 +1645,16 @@ public class Context extends IDisposable } /** - * Create a constant array. The resulting term is an array, such - * that a selecton an arbitrary index produces the value - * v. @see MkArraySort"/> @see MkStore + * Maps f on the argument arrays. + * Remarks: Eeach element of + * {@code args} must be of an array sort + * {@code [domain_i -> range_i]}. The function declaration + * {@code f} must have type {@code range_1 .. range_n -> range}. + * {@code v} must have sort range. The sort of the result is + * {@code [domain_i -> range]}. + * @see mkArraySort + * @see mkSelect + * @see mkStore + **/ public ArrayExpr mkMap(FuncDecl f, ArrayExpr... args) throws Z3Exception { - checkContextMatch(f); checkContextMatch(args); return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(), @@ -1721,13 +1684,13 @@ public class Context extends IDisposable } /** - * Access the array default value. Produces the default range + * Access the array default value. + * Remarks: Produces the default range * value, for arrays that can be represented as finite maps with a default - * range value. + * range value. **/ public Expr mkTermArray(ArrayExpr array) throws Z3Exception { - checkContextMatch(array); return Expr.create(this, Native.mkArrayDefault(nCtx(), array.getNativeObject())); @@ -1738,7 +1701,6 @@ public class Context extends IDisposable **/ public SetSort mkSetSort(Sort ty) throws Z3Exception { - checkContextMatch(ty); return new SetSort(this, ty); } @@ -1748,7 +1710,6 @@ public class Context extends IDisposable **/ public Expr mkEmptySet(Sort domain) throws Z3Exception { - checkContextMatch(domain); return Expr.create(this, Native.mkEmptySet(nCtx(), domain.getNativeObject())); @@ -1759,7 +1720,6 @@ public class Context extends IDisposable **/ public Expr mkFullSet(Sort domain) throws Z3Exception { - checkContextMatch(domain); return Expr.create(this, Native.mkFullSet(nCtx(), domain.getNativeObject())); @@ -1770,7 +1730,6 @@ public class Context extends IDisposable **/ public Expr mkSetAdd(Expr set, Expr element) throws Z3Exception { - checkContextMatch(set); checkContextMatch(element); return Expr.create( @@ -1784,7 +1743,6 @@ public class Context extends IDisposable **/ public Expr mkSetDel(Expr set, Expr element) throws Z3Exception { - checkContextMatch(set); checkContextMatch(element); return Expr.create( @@ -1798,7 +1756,6 @@ public class Context extends IDisposable **/ public Expr mkSetUnion(Expr... args) throws Z3Exception { - checkContextMatch(args); return Expr.create( this, @@ -1811,7 +1768,6 @@ public class Context extends IDisposable **/ public Expr mkSetIntersection(Expr... args) throws Z3Exception { - checkContextMatch(args); return Expr.create( this, @@ -1824,7 +1780,6 @@ public class Context extends IDisposable **/ public Expr mkSetDifference(Expr arg1, Expr arg2) throws Z3Exception { - checkContextMatch(arg1); checkContextMatch(arg2); return Expr.create( @@ -1838,7 +1793,6 @@ public class Context extends IDisposable **/ public Expr mkSetComplement(Expr arg) throws Z3Exception { - checkContextMatch(arg); return Expr.create(this, Native.mkSetComplement(nCtx(), arg.getNativeObject())); @@ -1849,7 +1803,6 @@ public class Context extends IDisposable **/ public Expr mkSetMembership(Expr elem, Expr set) throws Z3Exception { - checkContextMatch(elem); checkContextMatch(set); return Expr.create( @@ -1863,7 +1816,6 @@ public class Context extends IDisposable **/ public Expr mkSetSubset(Expr arg1, Expr arg2) throws Z3Exception { - checkContextMatch(arg1); checkContextMatch(arg2); return Expr.create( @@ -1873,19 +1825,18 @@ public class Context extends IDisposable } /** - * Create a Term of a given sort. A string representing the - * Term value in decimal notation. If the given sort is a real, then the + * Create a Term of a given sort. + * @param v A string representing the term value in decimal notation. If the given sort is a real, then the * Term can be a rational, that is, a string of the form - * [num]* / [num]*. The sort of the + * {@code [num]* / [num]*}. + * @param ty The sort of the * numeral. In the current implementation, the given sort can be an int, - * real, or bit-vectors of arbitrary size. + * real, or bit-vectors of arbitrary size. * - * @return A Term with value and sort + * @return A Term with value {@code v} and sort {@code ty} **/ public Expr mkNumeral(String v, Sort ty) throws Z3Exception { - checkContextMatch(ty); return Expr.create(this, Native.mkNumeral(nCtx(), v, ty.getNativeObject())); @@ -1894,16 +1845,15 @@ public class Context extends IDisposable /** * Create a Term of a given sort. This function can be use to create * numerals that fit in a machine integer. It is slightly faster than - * MakeNumeral since it is not necessary to parse a string. - * @param v Value of the numeral Sort of the - * numeral + * {@code MakeNumeral} since it is not necessary to parse a string. * - * @return A Term with value and type + * @param v Value of the numeral + * @param ty Sort of the numeral + * + * @return A Term with value {@code v} and type {@code ty} **/ public Expr mkNumeral(int v, Sort ty) throws Z3Exception { - checkContextMatch(ty); return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject())); } @@ -1911,27 +1861,28 @@ public class Context extends IDisposable /** * Create a Term of a given sort. This function can be use to create * numerals that fit in a machine integer. It is slightly faster than - * MakeNumeral since it is not necessary to parse a string. - * @param v Value of the numeral Sort of the - * numeral + * {@code MakeNumeral} since it is not necessary to parse a string. * - * @return A Term with value and type + * @param v Value of the numeral + * @param ty Sort of the numeral + * + * @return A Term with value {@code v} and type {@code ty} **/ public Expr mkNumeral(long v, Sort ty) throws Z3Exception { - checkContextMatch(ty); return Expr.create(this, Native.mkInt64(nCtx(), v, ty.getNativeObject())); } /** - * Create a real from a fraction. numerator of - * rational. @param den denominator of rational. + * Create a real from a fraction. + * @param num numerator of rational. + * @param den denominator of rational. * - * @return A Term with value / - * and sort Real @see MkNumeral(string, Sort) + * @return A Term with value {@code num}/{@code den} + * and sort Real + * @see mkNumeral(String,Sort) **/ public RatNum mkReal(int num, int den) throws Z3Exception { @@ -1942,10 +1893,10 @@ public class Context extends IDisposable } /** - * Create a real numeral. A string representing the Term - * value in decimal notation. + * Create a real numeral. + * @param v A string representing the Term value in decimal notation. * - * @return A Term with value and sort Real + * @return A Term with value {@code v} and sort Real **/ public RatNum mkReal(String v) throws Z3Exception { @@ -1955,9 +1906,10 @@ public class Context extends IDisposable } /** - * Create a real numeral. @param v value of the numeral. + * Create a real numeral. + * @param v value of the numeral. * - * @return A Term with value and sort Real + * @return A Term with value {@code v} and sort Real **/ public RatNum mkReal(int v) throws Z3Exception { @@ -1967,9 +1919,10 @@ public class Context extends IDisposable } /** - * Create a real numeral. @param v value of the numeral. + * Create a real numeral. + * @param v value of the numeral. * - * @return A Term with value and sort Real + * @return A Term with value {@code v} and sort Real **/ public RatNum mkReal(long v) throws Z3Exception { @@ -1979,8 +1932,8 @@ public class Context extends IDisposable } /** - * Create an integer numeral. A string representing the Term - * value in decimal notation. + * Create an integer numeral. + * @param v A string representing the Term value in decimal notation. **/ public IntNum mkInt(String v) throws Z3Exception { @@ -1990,9 +1943,10 @@ public class Context extends IDisposable } /** - * Create an integer numeral. @param v value of the numeral. + * Create an integer numeral. + * @param v value of the numeral. * - * @return A Term with value and sort Integer + * @return A Term with value {@code v} and sort Integer **/ public IntNum mkInt(int v) throws Z3Exception { @@ -2002,9 +1956,10 @@ public class Context extends IDisposable } /** - * Create an integer numeral. @param v value of the numeral. + * Create an integer numeral. + * @param v value of the numeral. * - * @return A Term with value and sort Integer + * @return A Term with value {@code v} and sort Integer **/ public IntNum mkInt(long v) throws Z3Exception { @@ -2014,54 +1969,56 @@ public class Context extends IDisposable } /** - * Create a bit-vector numeral. A string representing the - * value in decimal notation. the size of the - * bit-vector + * Create a bit-vector numeral. + * @param v A string representing the value in decimal notation. + * @param size the size of the bit-vector **/ public BitVecNum mkBV(String v, int size) throws Z3Exception { - return (BitVecNum) mkNumeral(v, mkBitVecSort(size)); } /** - * Create a bit-vector numeral. value of the - * numeral. @param size the size of the bit-vector + * Create a bit-vector numeral. + * @param v value of the numeral. + * @param size the size of the bit-vector **/ public BitVecNum mkBV(int v, int size) throws Z3Exception { - return (BitVecNum) mkNumeral(v, mkBitVecSort(size)); } /** - * Create a bit-vector numeral. value of the - * numeral. * @param size the size of the bit-vector + * Create a bit-vector numeral. + * @param v value of the numeral. * + * @param size the size of the bit-vector **/ public BitVecNum mkBV(long v, int size) throws Z3Exception { - return (BitVecNum) mkNumeral(v, mkBitVecSort(size)); } /** - * Create a universal Quantifier. Creates a forall formula, where - * is the weight, is - * an array of patterns, is an array with the sorts - * of the bound variables, is an array with the - * 'names' of the bound variables, and is the body + * Create a universal Quantifier. + * Remarks: Creates a forall formula, where + * {@code weight"/> is the weight, names of the bound variables the - * body of the quantifier. quantifiers are + * importance of using the quantifier during instantiation. + * + * @param sorts the sorts of the bound variables. + * @param names names of the bound variables + * @param body the body of the quantifier. + * @param weight quantifiers are * associated with weights indicating the importance of using the quantifier - * during instantiation. By default, pass the weight 0. array containing the patterns created using - * MkPattern. array containing - * the anti-patterns created using MkPattern. optional symbol to track quantifier. optional symbol to track skolem constants. + * during instantiation. By default, pass the weight 0. + * @param patterns array containing the patterns created using + * {@code MkPattern}. + * @param noPatterns array containing the anti-patterns created using {@code MkPattern}. + * @param quantifierID optional symbol to track quantifier. + * @param skolemID optional symbol to track skolem constants. **/ public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, @@ -2085,8 +2042,8 @@ public class Context extends IDisposable } /** - * Create an existential Quantifier. + * Create an existential Quantifier. + * @see mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol) **/ public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, @@ -2143,15 +2100,18 @@ public class Context extends IDisposable } /** - * Selects the format used for pretty-printing expressions. The + * Selects the format used for pretty-printing expressions. + * Remarks: The * default mode for pretty printing expressions is to produce SMT-LIB style * output where common subexpressions are printed at each occurrence. The * mode is called Z3_PRINT_SMTLIB_FULL. To print shared common * subexpressions only once, use the Z3_PRINT_LOW_LEVEL mode. To print in * way that conforms to SMT-LIB standards and uses let expressions to share - * common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT. @see Pattern.ToString() @see Sort.ToString() + * common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT. + * @see AST#toString + * @see Pattern#toString + * @see FuncDecl#toString + * @see Sort#toString **/ public void setPrintMode(Z3_ast_print_mode value) throws Z3Exception { @@ -2159,14 +2119,15 @@ public class Context extends IDisposable } /** - * Convert a benchmark into an SMT-LIB formatted string. Name of the benchmark. The argument is optional. - * @param logic The benchmark logic. The status string (sat, unsat, or unknown) Other attributes, such as source, difficulty or - * category. Auxiliary - * assumptions. Formula to be checked for - * consistency in conjunction with assumptions. + * Convert a benchmark into an SMT-LIB formatted string. + * @param name Name of the benchmark. The argument is optional. + * + * @param logic The benchmark logic. + * @param status The status string (sat, unsat, or unknown) + * @param attributes Other attributes, such as source, difficulty or + * category. + * @param assumptions Auxiliary assumptions. + * @param formula Formula to be checked for consistency in conjunction with assumptions. * * @return A string representation of the benchmark. **/ @@ -2181,13 +2142,13 @@ public class Context extends IDisposable } /** - * Parse the given string using the SMT-LIB parser. The symbol + * Parse the given string using the SMT-LIB parser. + * Remarks: The symbol * table of the parser can be initialized using the given sorts and - * declarations. The symbols in the arrays and - * don't need to match the names of the sorts - * and declarations in the arrays and . This is a useful feature since we can use arbitrary names - * to reference sorts and declarations. + * declarations. The symbols in the arrays {@code sortNames} and + * {@code declNames} don't need to match the names of the sorts + * and declarations in the arrays {@code sorts} and {@code decls}. This is a useful feature since we can use arbitrary names + * to reference sorts and declarations. **/ public void parseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception @@ -2205,8 +2166,8 @@ public class Context extends IDisposable } /** - * Parse the given file using the SMT-LIB parser. + * Parse the given file using the SMT-LIB parser. + * @see parseSMTLIBString **/ public void parseSMTLIBFile(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) @@ -2226,7 +2187,7 @@ public class Context extends IDisposable /** * The number of SMTLIB formulas parsed by the last call to - * ParseSMTLIBString or ParseSMTLIBFile. + * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}. **/ public int getNumSMTLIBFormulas() throws Z3Exception { @@ -2234,8 +2195,8 @@ public class Context extends IDisposable } /** - * The formulas parsed by the last call to ParseSMTLIBString or - * ParseSMTLIBFile. + * The formulas parsed by the last call to {@code ParseSMTLIBString} or + * {@code ParseSMTLIBFile}. **/ public BoolExpr[] getSMTLIBFormulas() throws Z3Exception { @@ -2250,7 +2211,7 @@ public class Context extends IDisposable /** * The number of SMTLIB assumptions parsed by the last call to - * ParseSMTLIBString or ParseSMTLIBFile. + * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}. **/ public int getNumSMTLIBAssumptions() throws Z3Exception { @@ -2258,8 +2219,8 @@ public class Context extends IDisposable } /** - * The assumptions parsed by the last call to ParseSMTLIBString - * or ParseSMTLIBFile. + * The assumptions parsed by the last call to {@code ParseSMTLIBString} + * or {@code ParseSMTLIBFile}. **/ public BoolExpr[] getSMTLIBAssumptions() throws Z3Exception { @@ -2274,7 +2235,7 @@ public class Context extends IDisposable /** * The number of SMTLIB declarations parsed by the last call to - * ParseSMTLIBString or ParseSMTLIBFile. + * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}. **/ public int getNumSMTLIBDecls() throws Z3Exception { @@ -2283,7 +2244,7 @@ public class Context extends IDisposable /** * The declarations parsed by the last call to - * ParseSMTLIBString or ParseSMTLIBFile. + * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}. **/ public FuncDecl[] getSMTLIBDecls() throws Z3Exception { @@ -2297,7 +2258,7 @@ public class Context extends IDisposable /** * The number of SMTLIB sorts parsed by the last call to - * ParseSMTLIBString or ParseSMTLIBFile. + * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}. **/ public int getNumSMTLIBSorts() throws Z3Exception { @@ -2306,7 +2267,7 @@ public class Context extends IDisposable /** * The declarations parsed by the last call to - * ParseSMTLIBString or ParseSMTLIBFile. + * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}. **/ public Sort[] getSMTLIBSorts() throws Z3Exception { @@ -2319,8 +2280,8 @@ public class Context extends IDisposable } /** - * Parse the given string using the SMT-LIB2 parser. + * Parse the given string using the SMT-LIB2 parser. + * @see parseSMTLIBString * * @return A conjunction of assertions in the scope (up to push/pop) at the * end of the string. @@ -2343,8 +2304,8 @@ public class Context extends IDisposable } /** - * Parse the given file using the SMT-LIB2 parser. + * Parse the given file using the SMT-LIB2 parser. + * @see parseSMTLIB2String **/ public BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) @@ -2365,18 +2326,18 @@ public class Context extends IDisposable } /** - * Creates a new Goal. Note that the Context must have been - * created with proof generation support if is set - * to true here. Indicates whether model - * generation should be enabled. Indicates - * whether unsat core generation should be enabled. Indicates whether proof generation should be - * enabled. + * Creates a new Goal. + * Remarks: Note that the Context must have been + * created with proof generation support if {@code proofs} is set + * to true here. + * @param models Indicates whether model generation should be enabled. + * @param unsatCores Indicates whether unsat core generation should be enabled. + * @param proofs Indicates whether proof generation should be + * enabled. **/ public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs) throws Z3Exception { - return new Goal(this, models, unsatCores, proofs); } @@ -2385,7 +2346,6 @@ public class Context extends IDisposable **/ public Params mkParams() throws Z3Exception { - return new Params(this); } @@ -2416,7 +2376,6 @@ public class Context extends IDisposable **/ public String getTacticDescription(String name) throws Z3Exception { - return Native.tacticGetDescr(nCtx(), name); } @@ -2425,13 +2384,12 @@ public class Context extends IDisposable **/ public Tactic mkTactic(String name) throws Z3Exception { - return new Tactic(this, name); } /** - * Create a tactic that applies to a Goal and then - * to every subgoal produced by . + * Create a tactic that applies {@code t1} to a Goal and then + * {@code t2"/> to every subgoal produced by to a Goal and then - * to every subgoal produced by . - * Shorthand for AndThen. + * Create a tactic that applies {@code t1} to a Goal and then + * {@code t2"/> to every subgoal produced by to a Goal and if - * it fails then returns the result of applied to the + * Create a tactic that first applies {@code t1} to a Goal and if + * it fails then returns the result of {@code t2} applied to the * Goal. **/ public Tactic orElse(Tactic t1, Tactic t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new Tactic(this, Native.tacticOrElse(nCtx(), @@ -2483,28 +2441,26 @@ public class Context extends IDisposable } /** - * Create a tactic that applies to a goal for milliseconds. If does not - * terminate within milliseconds, then it fails. - * + * Create a tactic that applies {@code t} to a goal for {@code ms} milliseconds. + * Remarks: If {@code t} does not + * terminate within {@code ms} milliseconds, then it fails. + * **/ public Tactic tryFor(Tactic t, int ms) throws Z3Exception { - checkContextMatch(t); return new Tactic(this, Native.tacticTryFor(nCtx(), t.getNativeObject(), ms)); } /** - * Create a tactic that applies to a given goal if the - * probe evaluates to true. If evaluates to false, then the new tactic behaves like the - * skip tactic. + * Create a tactic that applies {@code t} to a given goal if the + * probe {@code p} evaluates to true. + * Remarks: If {@code p} evaluates to false, then the new tactic behaves like the + * {@code skip} tactic. **/ public Tactic when(Probe p, Tactic t) throws Z3Exception { - checkContextMatch(t); checkContextMatch(p); return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(), @@ -2512,13 +2468,12 @@ public class Context extends IDisposable } /** - * Create a tactic that applies to a given goal if the - * probe evaluates to true and + * Create a tactic that applies {@code t1} to a given goal if the + * probe {@code p"/> evaluates to true and until the goal - * is not modified anymore or the maximum number of iterations is reached. + * Create a tactic that keeps applying {@code t} until the goal + * is not modified anymore or the maximum number of iterations {@code max} is reached. **/ public Tactic repeat(Tactic t, int max) throws Z3Exception { - checkContextMatch(t); return new Tactic(this, Native.tacticRepeat(nCtx(), t.getNativeObject(), max)); @@ -2544,7 +2497,6 @@ public class Context extends IDisposable **/ public Tactic skip() throws Z3Exception { - return new Tactic(this, Native.tacticSkip(nCtx())); } @@ -2553,17 +2505,15 @@ public class Context extends IDisposable **/ public Tactic fail() throws Z3Exception { - return new Tactic(this, Native.tacticFail(nCtx())); } /** - * Create a tactic that fails if the probe evaluates to + * Create a tactic that fails if the probe {@code p} evaluates to * false. **/ public Tactic failIf(Probe p) throws Z3Exception { - checkContextMatch(p); return new Tactic(this, Native.tacticFailIf(nCtx(), p.getNativeObject())); @@ -2579,8 +2529,8 @@ public class Context extends IDisposable } /** - * Create a tactic that applies using the given set of - * parameters . + * Create a tactic that applies {@code t} using the given set of + * parameters {@code p}. **/ public Tactic usingParams(Tactic t, Params p) throws Z3Exception { @@ -2591,9 +2541,10 @@ public class Context extends IDisposable } /** - * Create a tactic that applies using the given set of - * parameters . Alias for - * UsingParams + * Create a tactic that applies {@code t} using the given set of + * parameters {@code p}. + * Remarks: Alias for + * {@code UsingParams} **/ public Tactic with(Tactic t, Params p) throws Z3Exception { @@ -2611,13 +2562,11 @@ public class Context extends IDisposable } /** - * Create a tactic that applies to a given goal and - * then to every subgoal produced by . The subgoals are processed in parallel. + * Create a tactic that applies {@code t1} to a given goal and + * then {@code t2} to every subgoal produced by {@code t1}. The subgoals are processed in parallel. **/ public Tactic parAndThen(Tactic t1, Tactic t2) throws Z3Exception { - checkContextMatch(t1); checkContextMatch(t2); return new Tactic(this, Native.tacticParAndThen(nCtx(), @@ -2625,8 +2574,9 @@ public class Context extends IDisposable } /** - * Interrupt the execution of a Z3 procedure. This procedure can be - * used to interrupt: solvers, simplifiers and tactics. + * Interrupt the execution of a Z3 procedure. + * Remarks: This procedure can be + * used to interrupt: solvers, simplifiers and tactics. **/ public void interrupt() throws Z3Exception { @@ -2672,7 +2622,7 @@ public class Context extends IDisposable } /** - * Create a probe that always evaluates to . + * Create a probe that always evaluates to {@code val}. **/ public Probe constProbe(double val) throws Z3Exception { @@ -2681,12 +2631,10 @@ public class Context extends IDisposable /** * Create a probe that evaluates to "true" when the value returned by - * is less than the value returned by + * {@code p1} is less than the value returned by {@code p2} **/ public Probe lt(Probe p1, Probe p2) throws Z3Exception { - checkContextMatch(p1); checkContextMatch(p2); return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(), @@ -2695,12 +2643,10 @@ public class Context extends IDisposable /** * Create a probe that evaluates to "true" when the value returned by - * is greater than the value returned by + * {@code p1} is greater than the value returned by {@code p2} **/ public Probe gt(Probe p1, Probe p2) throws Z3Exception { - checkContextMatch(p1); checkContextMatch(p2); return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(), @@ -2709,12 +2655,11 @@ public class Context extends IDisposable /** * Create a probe that evaluates to "true" when the value returned by - * is less than or equal the value returned by - * + * {@code p1} is less than or equal the value returned by + * {@code p2} **/ public Probe le(Probe p1, Probe p2) throws Z3Exception { - checkContextMatch(p1); checkContextMatch(p2); return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(), @@ -2723,8 +2668,8 @@ public class Context extends IDisposable /** * Create a probe that evaluates to "true" when the value returned by - * is greater than or equal the value returned by - * + * {@code p1} is greater than or equal the value returned by + * {@code p2} **/ public Probe ge(Probe p1, Probe p2) throws Z3Exception { @@ -2736,8 +2681,7 @@ public class Context extends IDisposable /** * Create a probe that evaluates to "true" when the value returned by - * is equal to the value returned by + * {@code p1} is equal to the value returned by {@code p2} **/ public Probe eq(Probe p1, Probe p2) throws Z3Exception { @@ -2748,8 +2692,7 @@ public class Context extends IDisposable } /** - * Create a probe that evaluates to "true" when the value and evaluate to "true". + * Create a probe that evaluates to "true" when the value {@code p1} and {@code p2} evaluate to "true". **/ public Probe and(Probe p1, Probe p2) throws Z3Exception { @@ -2760,8 +2703,7 @@ public class Context extends IDisposable } /** - * Create a probe that evaluates to "true" when the value or evaluate to "true". + * Create a probe that evaluates to "true" when the value {@code p1} or {@code p2} evaluate to "true". **/ public Probe or(Probe p1, Probe p2) throws Z3Exception { @@ -2772,21 +2714,20 @@ public class Context extends IDisposable } /** - * Create a probe that evaluates to "true" when the value does not evaluate to "true". + * Create a probe that evaluates to "true" when the value {@code p} does not evaluate to "true". **/ public Probe not(Probe p) throws Z3Exception { - checkContextMatch(p); return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject())); } /** - * Creates a new (incremental) solver. This solver also uses a set + * Creates a new (incremental) solver. + * Remarks: This solver also uses a set * of builtin tactics for handling the first check-sat command, and * check-sat commands that take more than a given number of milliseconds to - * be solved. + * be solved. **/ public Solver mkSolver() throws Z3Exception { @@ -2794,10 +2735,11 @@ public class Context extends IDisposable } /** - * Creates a new (incremental) solver. This solver also uses a set + * Creates a new (incremental) solver. + * Remarks: This solver also uses a set * of builtin tactics for handling the first check-sat command, and * check-sat commands that take more than a given number of milliseconds to - * be solved. + * be solved. **/ public Solver mkSolver(Symbol logic) throws Z3Exception { @@ -2805,15 +2747,16 @@ public class Context extends IDisposable if (logic == null) return new Solver(this, Native.mkSolver(nCtx())); else - return new Solver(this, Native.mkSolverForLogic(nCtx(), logic.getNativeObject())); + return new Solver(this, Native.mkSolverForLogic(nCtx(), + logic.getNativeObject())); } /** - * Creates a new (incremental) solver. @see MkSolver(Symbol) + * Creates a new (incremental) solver. + * @see mkSolver(Symbol) **/ public Solver mkSolver(String logic) throws Z3Exception { - return mkSolver(mkSymbol(logic)); } @@ -2822,19 +2765,20 @@ public class Context extends IDisposable **/ public Solver mkSimpleSolver() throws Z3Exception { - return new Solver(this, Native.mkSimpleSolver(nCtx())); } /** - * Creates a solver that is implemented using the given tactic. - * The solver supports the commands Push and Pop, - * but it will always solve each check from scratch. + * Creates a solver that is implemented using the given tactic. + * Remarks: + * The solver supports the commands {@code Push} and {@code Pop}, + * but it will always solve each check from scratch. **/ public Solver mkSolver(Tactic t) throws Z3Exception { - return new Solver(this, Native.mkSolverFromTactic(nCtx(), t.getNativeObject())); + return new Solver(this, Native.mkSolverFromTactic(nCtx(), + t.getNativeObject())); } /** @@ -2842,826 +2786,34 @@ public class Context extends IDisposable **/ public Fixedpoint mkFixedpoint() throws Z3Exception { - return new Fixedpoint(this); } - - /** Begin Floating-Point Arithmetic **/ - - /** Rounding Modes: RoundingMode Sort **/ - - /** - * Create the floating-point RoundingMode sort. - * @throws Z3Exception on error - **/ - public FPRMSort mkFPRoundingModeSort() throws Z3Exception - { - return new FPRMSort(this); - } - - /** Rounding Modes: Numerals **/ - - /** - * Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. - * @throws Z3Exception on error - **/ - public FPRMNum mkFPRoundNearestTiesToEven() throws Z3Exception - { - return new FPRMNum(this, Native.mkFpaRoundNearestTiesToEven(nCtx())); - } - - /** - * Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. - * @throws Z3Exception - **/ - public FPRMNum mkFPRNE() throws Z3Exception - { - return new FPRMNum(this, Native.mkFpaRne(nCtx())); - } - - /** - * Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. - * @throws Z3Exception - **/ - public FPRMNum mkFPRoundNearestTiesToAway() throws Z3Exception - { - return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx())); - } - - /** - * Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. - * @throws Z3Exception - **/ - public FPRMNum mkFPRNA() throws Z3Exception - { - return new FPRMNum(this, Native.mkFpaRna(nCtx())); - } - - /** - * Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. - * @throws Z3Exception - **/ - public FPRMNum mkFPRoundTowardPositive() throws Z3Exception - { - return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx())); - } - - /** - * Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. - * @throws Z3Exception - **/ - public FPRMNum mkFPRTP() throws Z3Exception - { - return new FPRMNum(this, Native.mkFpaRtp(nCtx())); - } - - /** - * Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. - * @throws Z3Exception - **/ - public FPRMNum mkFPRoundTowardNegative() throws Z3Exception - { - return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx())); - } - - /** - * Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. - * @throws Z3Exception - **/ - public FPRMNum mkFPRTN() throws Z3Exception - { - return new FPRMNum(this, Native.mkFpaRtn(nCtx())); - } - - /** - * Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. - * @throws Z3Exception - **/ - public FPRMNum mkFPRoundTowardZero() throws Z3Exception - { - return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx())); - } - - /** - * Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. - * @throws Z3Exception - **/ - public FPRMNum mkFPRTZ() throws Z3Exception - { - return new FPRMNum(this, Native.mkFpaRtz(nCtx())); - } - - /** FloatingPoint Sorts **/ - - /** - * Create a FloatingPoint sort. - * @param ebits exponent bits in the FloatingPoint sort. - * @param sbits significand bits in the FloatingPoint sort. - * @throws Z3Exception - **/ - public FPSort mkFPSort(int ebits, int sbits) throws Z3Exception - { - return new FPSort(this, ebits, sbits); - } - - /** - * Create the half-precision (16-bit) FloatingPoint sort. - * @throws Z3Exception - **/ - public FPSort mkFPSortHalf() throws Z3Exception - { - return new FPSort(this, Native.mkFpaSortHalf(nCtx())); - } - - /** - * Create the half-precision (16-bit) FloatingPoint sort. - * @throws Z3Exception - **/ - public FPSort mkFPSort16() throws Z3Exception - { - return new FPSort(this, Native.mkFpaSort16(nCtx())); - } - - /** - * Create the single-precision (32-bit) FloatingPoint sort. - * @throws Z3Exception - **/ - public FPSort mkFPSortSingle() throws Z3Exception - { - return new FPSort(this, Native.mkFpaSortSingle(nCtx())); - } - - /** - * Create the single-precision (32-bit) FloatingPoint sort. - * @throws Z3Exception - **/ - public FPSort mkFPSort32() throws Z3Exception - { - return new FPSort(this, Native.mkFpaSort16(nCtx())); - } - - /** - * Create the double-precision (64-bit) FloatingPoint sort. - * @throws Z3Exception - **/ - public FPSort mkFPSortDouble() throws Z3Exception - { - return new FPSort(this, Native.mkFpaSortDouble(nCtx())); - } - - /** - * Create the double-precision (64-bit) FloatingPoint sort. - * @throws Z3Exception - **/ - public FPSort mkFPSort64() throws Z3Exception - { - return new FPSort(this, Native.mkFpaSort64(nCtx())); - } - - /** - * Create the quadruple-precision (128-bit) FloatingPoint sort. - * @throws Z3Exception - **/ - public FPSort mkFPSortQuadruple() throws Z3Exception - { - return new FPSort(this, Native.mkFpaSortQuadruple(nCtx())); - } - - /** - * Create the quadruple-precision (128-bit) FloatingPoint sort. - * @throws Z3Exception - **/ - public FPSort mkFPSort128() throws Z3Exception - { - return new FPSort(this, Native.mkFpaSort128(nCtx())); - } - - /** FloatingPoint Numerals **/ - - /** - * Create a NaN of sort s. - * @throws Z3Exception - * @param s FloatingPoint sort. - **/ - public FPNum mkFPNaN(FPSort s) throws Z3Exception - { - return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject())); - } - - /** - * Create a floating-point infinity of sort s. - * @throws Z3Exception - * @param s FloatingPoint sort. - * @param negative indicates whether the result should be negative. - **/ - public FPNum mkFPInf(FPSort s, boolean negative) throws Z3Exception - { - return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative)); - } - - /** - * Create a floating-point zero of sort s. - * @throws Z3Exception - * @param s FloatingPoint sort. - * @param negative indicates whether the result should be negative. - **/ - public FPNum mkFPZero(FPSort s, boolean negative) throws Z3Exception - { - return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative)); - } - - /** - * Create a numeral of FloatingPoint sort from a float. - * @throws Z3Exception - * @param v numeral value. - * @param s FloatingPoint sort. - **/ - public FPNum mkFPNumeral(float v, FPSort s) throws Z3Exception - { - return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject())); - } - - /** - * Create a numeral of FloatingPoint sort from a float. - * @throws Z3Exception - * @param v numeral value. - * @param s FloatingPoint sort. - **/ - public FPNum mkFPNumeral(double v, FPSort s) throws Z3Exception - { - return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject())); - } - - /** - * Create a numeral of FloatingPoint sort from an int. - * @param v numeral value. - * @param s FloatingPoint sort. - * @throws Z3Exception - **/ - public FPNum mkFPNumeral(int v, FPSort s) throws Z3Exception - { - return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject())); - } - - /** - * Create a numeral of FloatingPoint sort from a sign bit and two integers. - * @param sgn the sign. - * @param sig the significand. - * @param exp the exponent. - * @param s FloatingPoint sort. - * @throws Z3Exception - **/ - public FPNum mkFPNumeral(boolean sgn, int sig, int exp, FPSort s) throws Z3Exception - { - return new FPNum(this, Native.mkFpaNumeralUintInt(nCtx(), sgn, sig, exp, s.getNativeObject())); - } - - /** - * Create a numeral of FloatingPoint sort from a sign bit and two long integers. - * @param sgn the sign. - * @param sig the significand. - * @param exp the exponent. - * @param s FloatingPoint sort. - * @throws Z3Exception - **/ - public FPNum mkFPNumeral(boolean sgn, long sig, long exp, FPSort s) throws Z3Exception - { - return new FPNum(this, Native.mkFpaNumeralUint64Int64(nCtx(), sgn, sig, exp, s.getNativeObject())); - } - - /** - * Create a numeral of FloatingPoint sort from a float. - * @param v numeral value. - * @param s FloatingPoint sort. - * @throws Z3Exception - **/ - public FPNum mkFP(float v, FPSort s) throws Z3Exception - { - return mkFPNumeral(v, s); - } - - /** - * Create a numeral of FloatingPoint sort from a float. - * @param v numeral value. - * @param s FloatingPoint sort. - * @throws Z3Exception - **/ - public FPNum mkFP(double v, FPSort s) throws Z3Exception - { - return mkFPNumeral(v, s); - } - - /** - * Create a numeral of FloatingPoint sort from an int. - * @param v numeral value. - * @param s FloatingPoint sort. - * @throws Z3Exception - **/ - public FPNum mkFP(int v, FPSort s) throws Z3Exception - { - return mkFPNumeral(v, s); - } - - /** - * Create a numeral of FloatingPoint sort from a sign bit and two integers. - * @param sgn the sign. - * @param sig the significand. - * @param exp the exponent. - * @param s FloatingPoint sort. - * @throws Z3Exception - **/ - public FPNum mkFP(boolean sgn, int exp, int sig, FPSort s) throws Z3Exception - { - return mkFPNumeral(sgn, sig, exp, s); - } - - /** - * Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers. - * @param sgn the sign. - * @param sig the significand. - * @param exp the exponent. - * @param s FloatingPoint sort. - * @throws Z3Exception - **/ - public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s) throws Z3Exception - { - return mkFPNumeral(sgn, sig, exp, s); - } - - /** FloatingPoint Operators **/ - - /** - * Floating-point absolute value - * @param t floating-point term - * @throws Z3Exception - **/ - public FPExpr mkFPAbs(FPExpr t) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject())); - } - - /** - * Floating-point negation - * @param t floating-point term - * @throws Z3Exception - **/ - public FPExpr mkFPNeg(FPExpr t) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject())); - } - - /** - * Floating-point addition - * @param rm rounding mode term - * @param t1 floating-point term - * @param t2 floating-point term - * @throws Z3Exception - **/ - public FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject())); - } - - /** - * Floating-point subtraction - * @param rm rounding mode term - * @param t1 floating-point term - * @param t2 floating-point term - * @throws Z3Exception - **/ - public FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject())); - } - - /** - * Floating-point multiplication - * @param rm rounding mode term - * @param t1 floating-point term - * @param t2 floating-point term - * @throws Z3Exception - **/ - public FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject())); - } - - /** - * Floating-point division - * @param rm rounding mode term - * @param t1 floating-point term - * @param t2 floating-point term - * @throws Z3Exception - **/ - public FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject())); - } - - /** - * Floating-point fused multiply-add - * - * Remarks: The result is round((t1 * t2) + t3) - * @param rm rounding mode term - * @param t1 floating-point term - * @param t2 floating-point term - * @param t3 floating-point term - * @throws Z3Exception - **/ - public FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject())); - } - - /** - * Floating-point square root - * @param rm rounding mode term - * @param t floating-point term - * @throws Z3Exception - **/ - public FPExpr mkFPSqrt(FPRMExpr rm, FPExpr t) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject())); - } - - /** - * Floating-point remainder - * @param t1 floating-point term - * @param t2 floating-point term - * @throws Z3Exception - **/ - public FPExpr mkFPRem(FPExpr t1, FPExpr t2) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject())); - } /** - * Floating-point roundToIntegral. Rounds a floating-point number to - * the closest integer, again represented as a floating-point number. - * @param rm term of RoundingMode sort - * @param t2 floating-point term - * @throws Z3Exception - */ - public FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject())); - } - - /** - * Minimum of floating-point numbers. - * @param t1 floating-point term - * @param t2 floating-point term - * @throws Z3Exception - **/ - public FPExpr mkFPMin(FPExpr t1, FPExpr t2) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject())); - } - - /** - * Maximum of floating-point numbers. - * @param t1 floating-point term - * @param t2 floating-point term - * @throws Z3Exception - **/ - public FPExpr mkFPMax(FPExpr t1, FPExpr t2) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject())); - } - - /** - * Floating-point less than or equal. - * @param t1 floating-point term - * @param t2 floating-point term - * @throws Z3Exception - **/ - public BoolExpr mkFPLEq(FPExpr t1, FPExpr t2) throws Z3Exception - { - - return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject())); - } - - /** - * Floating-point less than. - * @param t1 floating-point term - * @param t2 floating-point term - * @throws Z3Exception - **/ - public BoolExpr mkFPLt(FPExpr t1, FPExpr t2) throws Z3Exception - { - - return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject())); - } - - /** - * Floating-point greater than or equal. - * @param t1 floating-point term - * @param t2 floating-point term - * @throws Z3Exception - **/ - public BoolExpr mkFPGEq(FPExpr t1, FPExpr t2) throws Z3Exception - { - - return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject())); - } - - /** - * Floating-point greater than. - * @param t1 floating-point term - * @param t2 floating-point term - * @throws Z3Exception - **/ - public BoolExpr mkFPGt(FPExpr t1, FPExpr t2) throws Z3Exception - { - - return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject())); - } - - /** - * Floating-point equality. - * - * Remarks: Note that this is IEEE 754 equality (as opposed to standard =). - * @param t1 floating-point term - * @param t2 floating-point term - * @throws Z3Exception - **/ - public BoolExpr mkFPEq(FPExpr t1, FPExpr t2) throws Z3Exception - { - return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject())); - } - - /** - * Predicate indicating whether t is a normal floating-point number. - * @param t floating-point term - * @throws Z3Exception - **/ - public BoolExpr mkFPIsNormal(FPExpr t) throws Z3Exception - { - - return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject())); - } - - /** - * Predicate indicating whether t is a subnormal floating-point number. - * @param t floating-point term - * @throws Z3Exception - **/ - public BoolExpr mkFPIsSubnormal(FPExpr t) throws Z3Exception - { - return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject())); - } - - /** - * Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0. - * @param t floating-point term - * @throws Z3Exception - **/ - public BoolExpr mkFPIsZero(FPExpr t) throws Z3Exception - { - return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject())); - } - - /** - * Predicate indicating whether t is a floating-point number representing +oo or -oo. - * @param t floating-point term - * @throws Z3Exception - **/ - public BoolExpr mkFPIsInfinite(FPExpr t) throws Z3Exception - { - return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject())); - } - - /** - * Predicate indicating whether t is a NaN. - * @param t floating-point term - * @throws Z3Exception - **/ - public BoolExpr mkFPIsNaN(FPExpr t) throws Z3Exception - { - return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject())); - } - - /** - * Predicate indicating whether t is a negative floating-point number. - * @param t floating-point term - * @throws Z3Exception - **/ - public BoolExpr mkFPIsNegative(FPExpr t) throws Z3Exception - { - return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject())); - } - - /** - * Predicate indicating whether t is a positive floating-point number. - * @param t floating-point term - * @throws Z3Exception - **/ - public BoolExpr mkFPIsPositive(FPExpr t) throws Z3Exception - { - return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject())); - } - - /** Conversions to FloatingPoint terms **/ - - /** - * Create an expression of FloatingPoint sort from three bit-vector expressions. - * - * Remarks: This is the operator named `fp' in the SMT FP theory definition. - * Note that sgn is required to be a bit-vector of size 1. Significand and exponent - * are required to be greater than 1 and 2 respectively. The FloatingPoint sort - * of the resulting expression is automatically determined from the bit-vector sizes - * of the arguments. - * @param sgn bit-vector term (of size 1) representing the sign. - * @param sig bit-vector term representing the significand. - * @param exp bit-vector term representing the exponent. - * @throws Z3Exception - **/ - public FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject())); - } - - /** - * Conversion of a single IEEE 754-2008 bit-vector into a floating-point number. - * - * Remarks: Produces a term that represents the conversion of a bit-vector term bv to a - * floating-point term of sort s. The bit-vector size of bv (m) must be equal - * to ebits+sbits of s. The format of the bit-vector is as defined by the - * IEEE 754-2008 interchange format. - * @param bv bit-vector value (of size m). - * @param s FloatingPoint sort (ebits+sbits == m) - * @throws Z3Exception - **/ - public FPExpr mkFPToFP(BitVecExpr bv, FPSort s) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject())); - } - - /** - * Conversion of a FloatingPoint term into another term of different FloatingPoint sort. - * - * Remarks: Produces a term that represents the conversion of a floating-point term t to a - * floating-point term of sort s. If necessary, the result will be rounded according - * to rounding mode rm. - * @param rm RoundingMode term. - * @param t FloatingPoint term. - * @param s FloatingPoint sort. - * @throws Z3Exception - **/ - public FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject())); - } - - /** - * Conversion of a term of real sort into a term of FloatingPoint sort. - * - * Remarks: Produces a term that represents the conversion of term t of real sort into a - * floating-point term of sort s. If necessary, the result will be rounded according - * to rounding mode rm. - * @param rm RoundingMode term. - * @param t term of Real sort. - * @param s FloatingPoint sort. - * @throws Z3Exception - **/ - public FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject())); - } - - /** - * Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort. - * - * Remarks: Produces a term that represents the conversion of the bit-vector term t into a - * floating-point term of sort s. The bit-vector t is taken to be in signed - * 2's complement format (when signed==true, otherwise unsigned). If necessary, the - * result will be rounded according to rounding mode rm. - * @param rm RoundingMode term. - * @param t term of bit-vector sort. - * @param s FloatingPoint sort. - * @param signed flag indicating whether t is interpreted as signed or unsigned bit-vector. - * @throws Z3Exception - **/ - public FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed) throws Z3Exception - { - if (signed) - return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject())); - else - return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject())); - } - - /** - * Conversion of a floating-point number to another FloatingPoint sort s. - * - * Remarks: Produces a term that represents the conversion of a floating-point term t to a different - * FloatingPoint sort s. If necessary, rounding according to rm is applied. - * @param s FloatingPoint sort - * @param rm floating-point rounding mode term - * @param t floating-point term - * @throws Z3Exception - **/ - public FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t) throws Z3Exception - { - return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject())); - } - - /** Conversions from FloatingPoint terms **/ - - /** - * Conversion of a floating-point term into a bit-vector. - * - * Remarks: Produces a term that represents the conversion of the floating-poiunt term t into a - * bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, - * the result will be rounded according to rounding mode rm. - * @param rm RoundingMode term. - * @param t FloatingPoint term - * @param sz Size of the resulting bit-vector. - * @param signed Indicates whether the result is a signed or unsigned bit-vector. - * @throws Z3Exception - **/ - public BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed) throws Z3Exception - { - if (signed) - return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz)); - else - return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz)); - } - - /** - * Conversion of a floating-point term into a real-numbered term. - * - * Remarks: Produces a term that represents the conversion of the floating-poiunt term t into a - * real number. Note that this type of conversion will often result in non-linear - * constraints over real terms. - * @param t FloatingPoint term - * @throws Z3Exception - **/ - public RealExpr mkFPToReal(FPExpr t) throws Z3Exception - { - return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject())); - } - - /** Z3-specific extensions **/ - - /** - * Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. - * - * Remarks: The size of the resulting bit-vector is automatically determined. Note that - * IEEE 754-2008 allows multiple different representations of NaN. This conversion - * knows only one NaN and it will always produce the same bit-vector represenatation of - * that NaN. - * @param t FloatingPoint term. - * @throws Z3Exception - **/ - public BitVecExpr mkFPToIEEEBV(FPExpr t) throws Z3Exception - { - return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject())); - } - - /** - * Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort. - * - * Remarks: Produces a term that represents the conversion of sig * 2^exp into a - * floating-point term of sort s. If necessary, the result will be rounded - * according to rounding mode rm. - * @param rm RoundingMode term. - * @param sig Significand term of Real sort. - * @param exp Exponent term of Int sort. - * @param s FloatingPoint sort. - * @throws Z3Exception - **/ - public BitVecExpr mkFPToFP(FPRMExpr rm, RealExpr sig, IntExpr exp, FPSort s) throws Z3Exception - { - return new BitVecExpr(this, Native.mkFpaToFpRealInt(nCtx(), rm.getNativeObject(), sig.getNativeObject(), exp.getNativeObject(), s.getNativeObject())); - } - - /** End Floating-Point Arithmetic **/ - - /** - * Wraps an AST. - * Remarks: This function is used for transitions between - * native and managed objects. Note that - * must be a native object obtained from Z3 (e.g., through {@code unwrapAST}) - * and that it must have a correct reference count. - * @see Native.incRef - * @see wnwrapAST - * The native pointer to wrap. + * Wraps an AST. + * Remarks: This function is used for transitions between + * native and managed objects. Note that {@code nativeObject} + * must be a native object obtained from Z3 (e.g., through + * {@code UnwrapAST}) and that it must have a correct reference count. + * @see Native#incRef + * @see unwrapAST + * @param nativeObject The native pointer to wrap. **/ public AST wrapAST(long nativeObject) throws Z3Exception { - return AST.create(this, nativeObject); } /** * Unwraps an AST. - * Remarks: This function is used for transitions between + * Remarks: This function is used for transitions between * native and managed objects. It returns the native pointer to the AST. * Note that AST objects are reference counted and unwrapping an AST * disables automatic reference counting, i.e., all references to the IntPtr - * that is returned must be handled externally and through native calls - * @see Native.incRef - * @see wrapAST + * that is returned must be handled externally and through native calls (see + * e.g., + * @see Native#incRef + * @see wrapAST * @param a The AST to unwrap. **/ public long unwrapAST(AST a) @@ -3671,11 +2823,10 @@ public class Context extends IDisposable /** * Return a string describing all available parameters to - * Expr.Simplify. + * {@code Expr.Simplify}. **/ public String SimplifyHelp() throws Z3Exception { - return Native.simplifyGetHelp(nCtx()); } @@ -3688,9 +2839,10 @@ public class Context extends IDisposable } /** - * Enable/disable printing of warning messages to the console. Note + * Enable/disable printing of warning messages to the console. + * Remarks: Note * that this function is static and effects the behaviour of all contexts - * globally. + * globally. **/ public static void ToggleWarningMessages(boolean enabled) throws Z3Exception @@ -3699,11 +2851,12 @@ public class Context extends IDisposable } /** - * Update a mutable configuration parameter. The list of all + * Update a mutable configuration parameter. + * Remarks: The list of all * configuration parameters can be obtained using the Z3 executable: - * z3.exe -ini? Only a few configuration parameters are mutable + * {@code 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. + * an immutable parameter. **/ public void updateParamValue(String id, String value) throws Z3Exception { diff --git a/src/api/java/DatatypeExpr.java b/src/api/java/DatatypeExpr.java index d4612e6ff..c0f247b7a 100644 --- a/src/api/java/DatatypeExpr.java +++ b/src/api/java/DatatypeExpr.java @@ -23,7 +23,7 @@ package com.microsoft.z3; public class DatatypeExpr extends Expr { /** - * Constructor for DatatypeExpr + * Constructor for DatatypeExpr **/ DatatypeExpr(Context ctx, long obj) throws Z3Exception { diff --git a/src/api/java/DatatypeSort.java b/src/api/java/DatatypeSort.java index 9c339d932..4a31b6c38 100644 --- a/src/api/java/DatatypeSort.java +++ b/src/api/java/DatatypeSort.java @@ -24,6 +24,8 @@ public class DatatypeSort extends Sort { /** * The number of constructors of the datatype sort. + * @throws Z3Exception on error + * @return an int **/ public int getNumConstructors() throws Z3Exception { @@ -35,6 +37,7 @@ public class DatatypeSort extends Sort * The constructors. * * @throws Z3Exception + * @throws Z3Exception on error **/ public FuncDecl[] getConstructors() throws Z3Exception { @@ -50,6 +53,7 @@ public class DatatypeSort extends Sort * The recognizers. * * @throws Z3Exception + * @throws Z3Exception on error **/ public FuncDecl[] getRecognizers() throws Z3Exception { @@ -65,6 +69,7 @@ public class DatatypeSort extends Sort * The constructor accessors. * * @throws Z3Exception + * @throws Z3Exception on error **/ public FuncDecl[][] getAccessors() throws Z3Exception { diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java index 51bdfe0e8..06e1ade73 100644 --- a/src/api/java/EnumSort.java +++ b/src/api/java/EnumSort.java @@ -24,6 +24,7 @@ public class EnumSort extends Sort { /** * The function declarations of the constants in the enumeration. + * @throws Z3Exception on error **/ public FuncDecl[] getConstDecls() throws Z3Exception { @@ -36,6 +37,8 @@ public class EnumSort extends Sort /** * The constants in the enumeration. + * @throws Z3Exception on error + * @return an Expr **/ public Expr[] getConsts() throws Z3Exception { @@ -48,6 +51,7 @@ public class EnumSort extends Sort /** * The test predicates for the constants in the enumeration. + * @throws Z3Exception on error **/ public FuncDecl[] getTesterDecls() throws Z3Exception { diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 57f53ec6b..f94eb12cb 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -31,6 +31,9 @@ public class Expr extends AST { /** * Returns a simplified version of the expression + * @return Expr + * @throws Z3Exception on error + * @return an Expr **/ public Expr simplify() throws Z3Exception { @@ -40,8 +43,12 @@ public class Expr extends AST /** * Returns a simplified version of the expression * A set of - * parameters @param p a Params object to configure the simplifier - * @see Context.SimplifyHelp + * parameters + * @param p a Params object to configure the simplifier + * @see Context#SimplifyHelp + * @return an Expr + * @throws Z3Exception on error + * @return an Expr **/ public Expr simplify(Params p) throws Z3Exception { @@ -59,6 +66,8 @@ public class Expr extends AST /** * The function declaration of the function that is applied in this * expression. + * @return a FuncDecl + * @throws Z3Exception on error **/ public FuncDecl getFuncDecl() throws Z3Exception { @@ -69,6 +78,8 @@ public class Expr extends AST /** * Indicates whether the expression is the true or false expression or * something else (Z3_L_UNDEF). + * @throws Z3Exception on error + * @return a Z3_lbool **/ public Z3_lbool getBoolValue() throws Z3Exception { @@ -78,6 +89,8 @@ public class Expr extends AST /** * The number of arguments of the expression. + * @throws Z3Exception on error + * @return an int **/ public int getNumArgs() throws Z3Exception { @@ -86,6 +99,8 @@ public class Expr extends AST /** * The arguments of the expression. + * @throws Z3Exception on error + * @return an Expr[] **/ public Expr[] getArgs() throws Z3Exception { @@ -98,9 +113,11 @@ public class Expr extends AST } /** - * Update the arguments of the expression using the arguments The number of new arguments should coincide with the + * Update the arguments of the expression using the arguments {@code args} + * The number of new arguments should coincide with the * current number of arguments. + * @param args arguments + * @throws Z3Exception on error **/ public void update(Expr[] args) throws Z3Exception { @@ -112,13 +129,16 @@ public class Expr extends AST } /** - * Substitute every occurrence of from[i] in the expression - * with to[i], for i smaller than - * num_exprs. The result is the new expression. The - * arrays 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]. + * Substitute every occurrence of {@code from[i]} in the expression + * with {@code to[i]}, for {@code i} smaller than + * {@code num_exprs}. + * Remarks: The result is the new expression. The + * arrays {@code from} and {@code to} must have size + * {@code num_exprs}. For every {@code i} smaller than + * {@code num_exprs}, we must have that sort of {@code from[i]} + * must be equal to sort of {@code to[i]}. + * @throws Z3Exception on error + * @return an Expr **/ public Expr substitute(Expr[] from, Expr[] to) throws Z3Exception { @@ -132,8 +152,11 @@ public class Expr extends AST } /** - * Substitute every occurrence of from in the expression with - * to. @see Substitute(Expr[],Expr[]) + * Substitute every occurrence of {@code from} in the expression with + * {@code to}. + * @see Expr#substitute(Expr[],Expr[]) + * @throws Z3Exception on error + * @return an Expr **/ public Expr substitute(Expr from, Expr to) throws Z3Exception { @@ -143,9 +166,13 @@ public class Expr extends AST /** * Substitute the free variables in the expression with the expressions in - * For every i smaller than - * num_exprs, the variable with de-Bruijn index i - * is replaced with term to[i]. + * {@code to} + * Remarks: For every {@code i} smaller than * {@code num_exprs}, the + * variable with de-Bruijn index {@code i} * is replaced with term + * {@code to[i]}. + * @throws Z3Exception on error + * @throws Z3Exception on error + * @return an Expr **/ public Expr substituteVars(Expr[] to) throws Z3Exception { @@ -156,11 +183,13 @@ public class Expr extends AST } /** - * Translates (copies) the term to the Context . + * Translates (copies) the term to the Context {@code ctx}. + * * @param ctx A context * - * @return A copy of the term which is associated with + * @return A copy of the term which is associated with {@code ctx} + * @throws Z3Exception on error + * @return an Expr **/ public Expr translate(Context ctx) throws Z3Exception { @@ -184,6 +213,8 @@ public class Expr extends AST /** * Indicates whether the term is a numeral + * @throws Z3Exception on error + * @return a boolean **/ public boolean isNumeral() throws Z3Exception { @@ -194,6 +225,8 @@ public class Expr extends AST * Indicates whether the term is well-sorted. * * @return True if the term is well-sorted, false otherwise. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isWellSorted() throws Z3Exception { @@ -202,6 +235,8 @@ public class Expr extends AST /** * The Sort of the term. + * @throws Z3Exception on error + * @return a sort **/ public Sort getSort() throws Z3Exception { @@ -211,6 +246,8 @@ public class Expr extends AST /** * Indicates whether the term represents a constant. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isConst() throws Z3Exception { @@ -219,6 +256,8 @@ public class Expr extends AST /** * Indicates whether the term is an integer numeral. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isIntNum() throws Z3Exception { @@ -227,6 +266,8 @@ public class Expr extends AST /** * Indicates whether the term is a real numeral. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isRatNum() throws Z3Exception { @@ -235,6 +276,8 @@ public class Expr extends AST /** * Indicates whether the term is an algebraic number + * @throws Z3Exception on error + * @return a boolean **/ public boolean isAlgebraicNumber() throws Z3Exception { @@ -243,6 +286,8 @@ public class Expr extends AST /** * Indicates whether the term has Boolean sort. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBool() throws Z3Exception { @@ -253,6 +298,8 @@ public class Expr extends AST /** * Indicates whether the term is the constant true. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isTrue() throws Z3Exception { @@ -261,6 +308,8 @@ public class Expr extends AST /** * Indicates whether the term is the constant false. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isFalse() throws Z3Exception { @@ -269,6 +318,8 @@ public class Expr extends AST /** * Indicates whether the term is an equality predicate. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isEq() throws Z3Exception { @@ -278,6 +329,8 @@ public class Expr extends AST /** * Indicates whether the term is an n-ary distinct predicate (every argument * is mutually distinct). + * @throws Z3Exception on error + * @return a boolean **/ public boolean isDistinct() throws Z3Exception { @@ -286,6 +339,8 @@ public class Expr extends AST /** * Indicates whether the term is a ternary if-then-else term + * @throws Z3Exception on error + * @return a boolean **/ public boolean isITE() throws Z3Exception { @@ -294,6 +349,8 @@ public class Expr extends AST /** * Indicates whether the term is an n-ary conjunction + * @throws Z3Exception on error + * @return a boolean **/ public boolean isAnd() throws Z3Exception { @@ -302,6 +359,8 @@ public class Expr extends AST /** * Indicates whether the term is an n-ary disjunction + * @throws Z3Exception on error + * @return a boolean **/ public boolean isOr() throws Z3Exception { @@ -311,6 +370,8 @@ public class Expr extends AST /** * Indicates whether the term is an if-and-only-if (Boolean equivalence, * binary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isIff() throws Z3Exception { @@ -319,6 +380,8 @@ public class Expr extends AST /** * Indicates whether the term is an exclusive or + * @throws Z3Exception on error + * @return a boolean **/ public boolean isXor() throws Z3Exception { @@ -327,6 +390,8 @@ public class Expr extends AST /** * Indicates whether the term is a negation + * @throws Z3Exception on error + * @return a boolean **/ public boolean isNot() throws Z3Exception { @@ -335,6 +400,8 @@ public class Expr extends AST /** * Indicates whether the term is an implication + * @throws Z3Exception on error + * @return a boolean **/ public boolean isImplies() throws Z3Exception { @@ -343,6 +410,8 @@ public class Expr extends AST /** * Indicates whether the term is of integer sort. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isInt() throws Z3Exception { @@ -354,6 +423,8 @@ public class Expr extends AST /** * Indicates whether the term is of sort real. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isReal() throws Z3Exception { @@ -364,6 +435,8 @@ public class Expr extends AST /** * Indicates whether the term is an arithmetic numeral. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isArithmeticNumeral() throws Z3Exception { @@ -372,6 +445,8 @@ public class Expr extends AST /** * Indicates whether the term is a less-than-or-equal + * @throws Z3Exception on error + * @return a boolean **/ public boolean isLE() throws Z3Exception { @@ -380,6 +455,8 @@ public class Expr extends AST /** * Indicates whether the term is a greater-than-or-equal + * @throws Z3Exception on error + * @return a boolean **/ public boolean isGE() throws Z3Exception { @@ -388,6 +465,8 @@ public class Expr extends AST /** * Indicates whether the term is a less-than + * @throws Z3Exception on error + * @return a boolean **/ public boolean isLT() throws Z3Exception { @@ -396,6 +475,8 @@ public class Expr extends AST /** * Indicates whether the term is a greater-than + * @throws Z3Exception on error + * @return a boolean **/ public boolean isGT() throws Z3Exception { @@ -404,6 +485,8 @@ public class Expr extends AST /** * Indicates whether the term is addition (binary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isAdd() throws Z3Exception { @@ -412,6 +495,8 @@ public class Expr extends AST /** * Indicates whether the term is subtraction (binary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isSub() throws Z3Exception { @@ -420,6 +505,8 @@ public class Expr extends AST /** * Indicates whether the term is a unary minus + * @throws Z3Exception on error + * @return a boolean **/ public boolean isUMinus() throws Z3Exception { @@ -428,6 +515,8 @@ public class Expr extends AST /** * Indicates whether the term is multiplication (binary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isMul() throws Z3Exception { @@ -436,6 +525,8 @@ public class Expr extends AST /** * Indicates whether the term is division (binary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isDiv() throws Z3Exception { @@ -444,6 +535,8 @@ public class Expr extends AST /** * Indicates whether the term is integer division (binary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isIDiv() throws Z3Exception { @@ -452,6 +545,8 @@ public class Expr extends AST /** * Indicates whether the term is remainder (binary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isRemainder() throws Z3Exception { @@ -460,6 +555,8 @@ public class Expr extends AST /** * Indicates whether the term is modulus (binary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isModulus() throws Z3Exception { @@ -468,6 +565,8 @@ public class Expr extends AST /** * Indicates whether the term is a coercion of integer to real (unary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isIntToReal() throws Z3Exception { @@ -476,6 +575,8 @@ public class Expr extends AST /** * Indicates whether the term is a coercion of real to integer (unary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isRealToInt() throws Z3Exception { @@ -485,6 +586,8 @@ public class Expr extends AST /** * Indicates whether the term is a check that tests whether a real is * integral (unary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isRealIsInt() throws Z3Exception { @@ -493,6 +596,8 @@ public class Expr extends AST /** * Indicates whether the term is of an array sort. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isArray() throws Z3Exception { @@ -502,9 +607,10 @@ public class Expr extends AST } /** - * Indicates whether the term is an array store. It satisfies - * select(store(a,i,v),j) = if i = j then v else select(a,j). Array store - * takes at least 3 arguments. + * Indicates whether the term is an array store. + * Remarks: It satisfies * select(store(a,i,v),j) = if i = j then v else select(a,j). Array store * takes at least 3 arguments. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isStore() throws Z3Exception { @@ -513,6 +619,8 @@ public class Expr extends AST /** * Indicates whether the term is an array select. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isSelect() throws Z3Exception { @@ -520,9 +628,10 @@ public class Expr extends AST } /** - * Indicates whether the term is a constant array. For example, - * select(const(v),i) = v holds for every v and i. The function is - * unary. + * Indicates whether the term is a constant array. + * Remarks: For example, * select(const(v),i) = v holds for every v and i. The function is * unary. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isConstantArray() throws Z3Exception { @@ -530,8 +639,10 @@ public class Expr extends AST } /** - * Indicates whether the term is a default array. For example - * default(const(v)) = v. The function is unary. + * Indicates whether the term is a default array. + * Remarks: For example default(const(v)) = v. The function is unary. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isDefaultArray() throws Z3Exception { @@ -539,8 +650,11 @@ public class Expr extends AST } /** - * Indicates whether the term is an array map. It satisfies - * map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i. + * Indicates whether the term is an array map. + * Remarks: It satisfies + * map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isArrayMap() throws Z3Exception { @@ -548,9 +662,10 @@ public class Expr extends AST } /** - * Indicates whether the term is an as-array term. An as-array term - * is n array value that behaves as the function graph of the function - * passed as parameter. + * Indicates whether the term is an as-array term. + * Remarks: An as-array term * is n array value that behaves as the function graph of the function * passed as parameter. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isAsArray() throws Z3Exception { @@ -559,6 +674,8 @@ public class Expr extends AST /** * Indicates whether the term is set union + * @throws Z3Exception on error + * @return a boolean **/ public boolean isSetUnion() throws Z3Exception { @@ -567,6 +684,8 @@ public class Expr extends AST /** * Indicates whether the term is set intersection + * @throws Z3Exception on error + * @return a boolean **/ public boolean isSetIntersect() throws Z3Exception { @@ -575,6 +694,8 @@ public class Expr extends AST /** * Indicates whether the term is set difference + * @throws Z3Exception on error + * @return a boolean **/ public boolean isSetDifference() throws Z3Exception { @@ -583,6 +704,8 @@ public class Expr extends AST /** * Indicates whether the term is set complement + * @throws Z3Exception on error + * @return a boolean **/ public boolean isSetComplement() throws Z3Exception { @@ -591,6 +714,8 @@ public class Expr extends AST /** * Indicates whether the term is set subset + * @throws Z3Exception on error + * @return a boolean **/ public boolean isSetSubset() throws Z3Exception { @@ -599,6 +724,8 @@ public class Expr extends AST /** * Indicates whether the terms is of bit-vector sort. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBV() throws Z3Exception { @@ -609,6 +736,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector numeral + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVNumeral() throws Z3Exception { @@ -617,6 +746,8 @@ public class Expr extends AST /** * Indicates whether the term is a one-bit bit-vector with value one + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVBitOne() throws Z3Exception { @@ -625,6 +756,8 @@ public class Expr extends AST /** * Indicates whether the term is a one-bit bit-vector with value zero + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVBitZero() throws Z3Exception { @@ -633,6 +766,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector unary minus + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVUMinus() throws Z3Exception { @@ -641,6 +776,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector addition (binary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVAdd() throws Z3Exception { @@ -649,6 +786,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector subtraction (binary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVSub() throws Z3Exception { @@ -657,6 +796,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector multiplication (binary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVMul() throws Z3Exception { @@ -665,6 +806,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector signed division (binary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVSDiv() throws Z3Exception { @@ -673,6 +816,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector unsigned division (binary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVUDiv() throws Z3Exception { @@ -681,6 +826,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector signed remainder (binary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVSRem() throws Z3Exception { @@ -689,6 +836,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector unsigned remainder (binary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVURem() throws Z3Exception { @@ -697,6 +846,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector signed modulus + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVSMod() throws Z3Exception { @@ -705,46 +856,58 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector signed division by zero + * @return a boolean + * @throws Z3Exception on error **/ - boolean IsBVSDiv0() throws Z3Exception + boolean isBVSDiv0() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV0; } /** * Indicates whether the term is a bit-vector unsigned division by zero + * @return a boolean + * @throws Z3Exception on error **/ - boolean IsBVUDiv0() throws Z3Exception + boolean isBVUDiv0() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV0; } /** * Indicates whether the term is a bit-vector signed remainder by zero + * @return a boolean + * @throws Z3Exception on error **/ - boolean IsBVSRem0() throws Z3Exception + boolean isBVSRem0() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM0; } /** * Indicates whether the term is a bit-vector unsigned remainder by zero + * @return a boolean + * @throws Z3Exception on error **/ - boolean IsBVURem0() throws Z3Exception + boolean isBVURem0() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM0; } /** * Indicates whether the term is a bit-vector signed modulus by zero + * @return a boolean + * @throws Z3Exception on error **/ - boolean IsBVSMod0() throws Z3Exception + boolean isBVSMod0() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD0; } /** * Indicates whether the term is an unsigned bit-vector less-than-or-equal + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVULE() throws Z3Exception { @@ -753,6 +916,8 @@ public class Expr extends AST /** * Indicates whether the term is a signed bit-vector less-than-or-equal + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVSLE() throws Z3Exception { @@ -762,6 +927,8 @@ public class Expr extends AST /** * Indicates whether the term is an unsigned bit-vector * greater-than-or-equal + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVUGE() throws Z3Exception { @@ -770,6 +937,8 @@ public class Expr extends AST /** * Indicates whether the term is a signed bit-vector greater-than-or-equal + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVSGE() throws Z3Exception { @@ -778,6 +947,8 @@ public class Expr extends AST /** * Indicates whether the term is an unsigned bit-vector less-than + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVULT() throws Z3Exception { @@ -786,6 +957,8 @@ public class Expr extends AST /** * Indicates whether the term is a signed bit-vector less-than + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVSLT() throws Z3Exception { @@ -794,6 +967,8 @@ public class Expr extends AST /** * Indicates whether the term is an unsigned bit-vector greater-than + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVUGT() throws Z3Exception { @@ -802,6 +977,8 @@ public class Expr extends AST /** * Indicates whether the term is a signed bit-vector greater-than + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVSGT() throws Z3Exception { @@ -810,6 +987,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-wise AND + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVAND() throws Z3Exception { @@ -818,6 +997,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-wise OR + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVOR() throws Z3Exception { @@ -826,6 +1007,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-wise NOT + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVNOT() throws Z3Exception { @@ -834,6 +1017,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-wise XOR + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVXOR() throws Z3Exception { @@ -842,6 +1027,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-wise NAND + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVNAND() throws Z3Exception { @@ -850,6 +1037,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-wise NOR + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVNOR() throws Z3Exception { @@ -858,6 +1047,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-wise XNOR + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVXNOR() throws Z3Exception { @@ -866,6 +1057,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector concatenation (binary) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVConcat() throws Z3Exception { @@ -874,6 +1067,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector sign extension + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVSignExtension() throws Z3Exception { @@ -882,6 +1077,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector zero extension + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVZeroExtension() throws Z3Exception { @@ -890,6 +1087,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector extraction + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVExtract() throws Z3Exception { @@ -898,6 +1097,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector repetition + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVRepeat() throws Z3Exception { @@ -906,6 +1107,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector reduce OR + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVReduceOR() throws Z3Exception { @@ -914,6 +1117,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector reduce AND + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVReduceAND() throws Z3Exception { @@ -922,6 +1127,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector comparison + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVComp() throws Z3Exception { @@ -930,6 +1137,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector shift left + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVShiftLeft() throws Z3Exception { @@ -938,6 +1147,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector logical shift right + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVShiftRightLogical() throws Z3Exception { @@ -946,6 +1157,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector arithmetic shift left + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVShiftRightArithmetic() throws Z3Exception { @@ -954,6 +1167,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector rotate left + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVRotateLeft() throws Z3Exception { @@ -962,6 +1177,8 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector rotate right + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVRotateRight() throws Z3Exception { @@ -970,8 +1187,10 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector rotate left (extended) - * Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator - * instead of a parametric one. + * Remarks: Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator + * instead of a parametric one. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVRotateLeftExtended() throws Z3Exception { @@ -980,8 +1199,10 @@ public class Expr extends AST /** * Indicates whether the term is a bit-vector rotate right (extended) - * Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator - * instead of a parametric one. + * Remarks: Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator + * instead of a parametric one. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVRotateRightExtended() throws Z3Exception { @@ -990,9 +1211,10 @@ public class Expr extends AST /** * Indicates whether the term is a coercion from integer to bit-vector - * This function is not supported by the decision procedures. Only - * the most rudimentary simplification rules are applied to this - * function. + * + * Remarks: This function is not supported by the decision procedures. Only * the most rudimentary simplification rules are applied to this * function. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isIntToBV() throws Z3Exception { @@ -1001,9 +1223,10 @@ public class Expr extends AST /** * Indicates whether the term is a coercion from bit-vector to integer - * This function is not supported by the decision procedures. Only - * the most rudimentary simplification rules are applied to this - * function. + * + * Remarks: This function is not supported by the decision procedures. Only * the most rudimentary simplification rules are applied to this * function. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVToInt() throws Z3Exception { @@ -1011,9 +1234,10 @@ public class Expr extends AST } /** - * Indicates whether the term is a bit-vector carry Compute the - * carry bit in a full-adder. The meaning is given by the equivalence (carry - * l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3))) + * Indicates whether the term is a bit-vector carry + * Remarks: Compute the * carry bit in a full-adder. The meaning is given by the equivalence (carry * l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3))) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVCarry() throws Z3Exception { @@ -1021,9 +1245,10 @@ public class Expr extends AST } /** - * Indicates whether the term is a bit-vector ternary XOR The - * meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor - * l1 l2) l3) + * Indicates whether the term is a bit-vector ternary XOR + * Remarks: The * meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor * l1 l2) l3) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isBVXOR3() throws Z3Exception { @@ -1032,8 +1257,11 @@ public class Expr extends AST /** * Indicates whether the term is a label (used by the Boogie Verification - * condition generator). The label has two parameters, a string and - * a Boolean polarity. It takes one argument, a formula. + * condition generator). + * Remarks: The label has two parameters, a string and + * a Boolean polarity. It takes one argument, a formula. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isLabel() throws Z3Exception { @@ -1042,8 +1270,11 @@ public class Expr extends AST /** * Indicates whether the term is a label literal (used by the Boogie - * Verification condition generator). A label literal has a set of - * string parameters. It takes no arguments. + * Verification condition generator). + * Remarks: A label literal has a set of + * string parameters. It takes no arguments. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isLabelLit() throws Z3Exception { @@ -1052,8 +1283,10 @@ public class Expr extends AST /** * Indicates whether the term is a binary equivalence modulo namings. - * This binary predicate is used in proof terms. It captures - * equisatisfiability and equivalence modulo renamings. + * Remarks: This binary predicate is used in proof terms. It captures + * equisatisfiability and equivalence modulo renamings. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isOEQ() throws Z3Exception { @@ -1062,6 +1295,8 @@ public class Expr extends AST /** * Indicates whether the term is a Proof for the expression 'true'. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofTrue() throws Z3Exception { @@ -1070,6 +1305,8 @@ public class Expr extends AST /** * Indicates whether the term is a proof for a fact asserted by the user. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofAsserted() throws Z3Exception { @@ -1079,6 +1316,8 @@ public class Expr extends AST /** * Indicates whether the term is a proof for a fact (tagged as goal) * asserted by the user. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofGoal() throws Z3Exception { @@ -1086,10 +1325,13 @@ public class Expr extends AST } /** - * Indicates whether the term is proof via modus ponens Given a + * Indicates whether the term is proof via modus ponens + * Remarks: Given a * proof for p and a proof for (implies p q), produces a proof for q. T1: p * T2: (implies p q) [mp T1 T2]: q The second antecedents may also be a - * proof for (iff p q). + * proof for (iff p q). + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofModusPonens() throws Z3Exception { @@ -1098,10 +1340,13 @@ public class Expr extends AST /** * Indicates whether the term is a proof for (R t t), where R is a reflexive - * relation. This proof object has no antecedents. The only + * relation. + * Remarks: This proof object has no antecedents. The only * reflexive relations that are used are equivalence modulo namings, * equality and equivalence. That is, R is either '~', '=' or - * 'iff'. + * 'iff'. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofReflexivity() throws Z3Exception { @@ -1110,9 +1355,10 @@ public class Expr extends AST /** * Indicates whether the term is proof by symmetricity of a relation - * Given an symmetric relation R and a proof for (R t s), produces - * a proof for (R s t). T1: (R t s) [symmetry T1]: (R s t) T1 is the - * antecedent of this proof object. + * + * Remarks: Given an symmetric relation R and a proof for (R t s), produces * a proof for (R s t). T1: (R t s) [symmetry T1]: (R s t) T1 is the * antecedent of this proof object. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofSymmetry() throws Z3Exception { @@ -1121,9 +1367,10 @@ public class Expr extends AST /** * Indicates whether the term is a proof by transitivity of a relation - * Given a transitive relation R, and proofs for (R t s) and (R s - * u), produces a proof for (R t u). T1: (R t s) T2: (R s u) [trans T1 T2]: - * (R t u) + * + * Remarks: Given a transitive relation R, and proofs for (R t s) and (R s * u), produces a proof for (R t u). T1: (R t s) T2: (R s u) [trans T1 T2]: * (R t u) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofTransitivity() throws Z3Exception { @@ -1132,7 +1379,8 @@ public class Expr extends AST /** * Indicates whether the term is a proof by condensed transitivity of a - * relation Condensed transitivity proof. This proof object is + * relation + * Remarks: Condensed transitivity proof. This proof object is * only used if the parameter PROOF_MODE is 1. It combines several symmetry * and transitivity proofs. Example: T1: (R a b) T2: (R c b) T3: (R c d) * [trans* T1 T2 T3]: (R a d) R must be a symmetric and transitive relation. @@ -1141,7 +1389,9 @@ public class Expr extends AST * checker must check if it is possible to prove (R s t) using the * antecedents, symmetry and transitivity. That is, if there is a path from * s to t, if we view every antecedent (R a b) as an edge between a and b. - * + * + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofTransitivityStar() throws Z3Exception { @@ -1149,11 +1399,14 @@ public class Expr extends AST } /** - * Indicates whether the term is a monotonicity proof object. T1: + * Indicates whether the term is a monotonicity proof object. + * Remarks: T1: * (R t_1 s_1) ... Tn: (R t_n s_n) [monotonicity T1 ... Tn]: (R (f t_1 ... * t_n) (f s_1 ... s_n)) Remark: if t_i == s_i, then the antecedent Ti is * suppressed. That is, reflexivity proofs are supressed to save space. - * + * + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofMonotonicity() throws Z3Exception { @@ -1161,9 +1414,10 @@ public class Expr extends AST } /** - * Indicates whether the term is a quant-intro proof Given a proof - * for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)). T1: - * (~ p q) [quant-intro T1]: (~ (forall (x) p) (forall (x) q)) + * Indicates whether the term is a quant-intro proof + * Remarks: Given a proof * for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)). T1: * (~ p q) [quant-intro T1]: (~ (forall (x) p) (forall (x) q)) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofQuantIntro() throws Z3Exception { @@ -1171,7 +1425,8 @@ public class Expr extends AST } /** - * Indicates whether the term is a distributivity proof object. + * Indicates whether the term is a distributivity proof object. + * Remarks: * Given that f (= or) distributes over g (= and), produces a proof for (= * (f a (g c d)) (g (f a c) (f a d))) If f and g are associative, this proof * also justifies the following equality: (= (f (g a b) (g c d)) (g (f a c) @@ -1179,7 +1434,9 @@ public class Expr extends AST * arguments. * * This proof object has no antecedents. Remark. This rule is used by the - * CNF conversion pass and instantiated by f = or, and g = and. + * CNF conversion pass and instantiated by f = or, and g = and. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofDistributivity() throws Z3Exception { @@ -1187,9 +1444,10 @@ public class Expr extends AST } /** - * Indicates whether the term is a proof by elimination of AND - * Given a proof for (and l_1 ... l_n), produces a proof for l_i T1: (and - * l_1 ... l_n) [and-elim T1]: l_i + * Indicates whether the term is a proof by elimination of AND + * Remarks: * Given a proof for (and l_1 ... l_n), produces a proof for l_i T1: (and * l_1 ... l_n) [and-elim T1]: l_i + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofAndElimination() throws Z3Exception { @@ -1197,9 +1455,10 @@ public class Expr extends AST } /** - * Indicates whether the term is a proof by eliminiation of not-or - * Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). - * T1: (not (or l_1 ... l_n)) [not-or-elim T1]: (not l_i) + * Indicates whether the term is a proof by eliminiation of not-or + * Remarks: * Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). * T1: (not (or l_1 ... l_n)) [not-or-elim T1]: (not l_i) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofOrElimination() throws Z3Exception { @@ -1207,7 +1466,8 @@ public class Expr extends AST } /** - * Indicates whether the term is a proof by rewriting A proof for + * Indicates whether the term is a proof by rewriting + * Remarks: A proof for * a local rewriting step (= t s). The head function symbol of t is * interpreted. * @@ -1216,7 +1476,9 @@ public class Expr extends AST * equi-satisfiability (~ t s). Remark: if f is bool, then = is iff. * * Examples: (= (+ x 0) x) (= (+ x 1 2) (+ 3 x)) (iff (or x false) x) - * + * + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofRewrite() throws Z3Exception { @@ -1224,7 +1486,8 @@ public class Expr extends AST } /** - * Indicates whether the term is a proof by rewriting A proof for + * Indicates whether the term is a proof by rewriting + * Remarks: A proof for * rewriting an expression t into an expression s. This proof object is used * if the parameter PROOF_MODE is 1. This proof object can have n * antecedents. The antecedents are proofs for equalities used as @@ -1232,7 +1495,9 @@ public class Expr extends AST * parameter PROOF_MODE is 2. The cases are: - When applying contextual * simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to * Booleans (BIT2BOOL=true) - When pulling ite expression up - * (PULL_CHEAP_ITE_TREES=true) + * (PULL_CHEAP_ITE_TREES=true) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofRewriteStar() throws Z3Exception { @@ -1241,8 +1506,10 @@ public class Expr extends AST /** * Indicates whether the term is a proof for pulling quantifiers out. - * A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) - * r))). This proof object has no antecedents. + * Remarks: A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) + * r))). This proof object has no antecedents. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofPullQuant() throws Z3Exception { @@ -1251,9 +1518,10 @@ public class Expr extends AST /** * Indicates whether the term is a proof for pulling quantifiers out. - * A proof for (iff P Q) where Q is in prenex normal form. This - * proof object is only used if the parameter PROOF_MODE is 1. This proof - * object has no antecedents + * + * Remarks: A proof for (iff P Q) where Q is in prenex normal form. This * proof object is only used if the parameter PROOF_MODE is 1. This proof * object has no antecedents + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofPullQuantStar() throws Z3Exception { @@ -1262,10 +1530,12 @@ public class Expr extends AST /** * Indicates whether the term is a proof for pushing quantifiers in. - * A proof for: (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] + * Remarks: A proof for: (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] * ... p_n[x_1 ... x_m])) (and (forall (x_1 ... x_m) p_1[x_1 ... x_m]) ... * (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) This proof object has no - * antecedents + * antecedents + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofPushQuant() throws Z3Exception { @@ -1274,11 +1544,14 @@ public class Expr extends AST /** * Indicates whether the term is a proof for elimination of unused - * variables. A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) + * variables. + * Remarks: A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) * p[x_1 ... x_n]) (forall (x_1 ... x_n) p[x_1 ... x_n])) * * It is used to justify the elimination of unused variables. This proof - * object has no antecedents. + * object has no antecedents. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofElimUnusedVars() throws Z3Exception { @@ -1287,12 +1560,14 @@ public class Expr extends AST /** * Indicates whether the term is a proof for destructive equality resolution - * A proof for destructive equality resolution: (iff (forall (x) + * Remarks: A proof for destructive equality resolution: (iff (forall (x) * (or (not (= x t)) P[x])) P[t]) if x does not occur in t. * * This proof object has no antecedents. * - * Several variables can be eliminated simultaneously. + * Several variables can be eliminated simultaneously. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofDER() throws Z3Exception { @@ -1301,7 +1576,10 @@ public class Expr extends AST /** * Indicates whether the term is a proof for quantifier instantiation - * A proof of (or (not (forall (x) (P x))) (P a)) + * + * Remarks: A proof of (or (not (forall (x) (P x))) (P a)) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofQuantInst() throws Z3Exception { @@ -1309,8 +1587,11 @@ public class Expr extends AST } /** - * Indicates whether the term is a hypthesis marker. Mark a - * hypothesis in a natural deduction style proof. + * Indicates whether the term is a hypthesis marker. + * Remarks: Mark a + * hypothesis in a natural deduction style proof. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofHypothesis() throws Z3Exception { @@ -1318,12 +1599,15 @@ public class Expr extends AST } /** - * Indicates whether the term is a proof by lemma T1: false [lemma + * Indicates whether the term is a proof by lemma + * Remarks: T1: false [lemma * T1]: (or (not l_1) ... (not l_n)) * * This proof object has one antecedent: a hypothetical proof for false. It * converts the proof in a proof for (or (not l_1) ... (not l_n)), when T1 - * contains the hypotheses: l_1, ..., l_n. + * contains the hypotheses: l_1, ..., l_n. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofLemma() throws Z3Exception { @@ -1331,9 +1615,10 @@ public class Expr extends AST } /** - * Indicates whether the term is a proof by unit resolution T1: - * (or l_1 ... l_n l_1' ... l_m') T2: (not l_1) ... T(n+1): (not l_n) - * [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') + * Indicates whether the term is a proof by unit resolution + * Remarks: T1: * (or l_1 ... l_n l_1' ... l_m') T2: (not l_1) ... T(n+1): (not l_n) * [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofUnitResolution() throws Z3Exception { @@ -1341,8 +1626,11 @@ public class Expr extends AST } /** - * Indicates whether the term is a proof by iff-true T1: p - * [iff-true T1]: (iff p true) + * Indicates whether the term is a proof by iff-true + * Remarks: T1: p + * [iff-true T1]: (iff p true) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofIFFTrue() throws Z3Exception { @@ -1350,8 +1638,11 @@ public class Expr extends AST } /** - * Indicates whether the term is a proof by iff-false T1: (not p) - * [iff-false T1]: (iff p false) + * Indicates whether the term is a proof by iff-false + * Remarks: T1: (not p) + * [iff-false T1]: (iff p false) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofIFFFalse() throws Z3Exception { @@ -1359,13 +1650,16 @@ public class Expr extends AST } /** - * Indicates whether the term is a proof by commutativity [comm]: + * Indicates whether the term is a proof by commutativity + * Remarks: [comm]: * (= (f a b) (f b a)) * * f is a commutative operator. * * This proof object has no antecedents. Remark: if f is bool, then = is - * iff. + * iff. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofCommutativity() throws Z3Exception { @@ -1373,7 +1667,8 @@ public class Expr extends AST } /** - * Indicates whether the term is a proof for Tseitin-like axioms + * Indicates whether the term is a proof for Tseitin-like axioms + * Remarks: * Proof object used to justify Tseitin's like axioms: * * (or (not (and p q)) p) (or (not (and p q)) q) (or (not (and p q r)) p) @@ -1388,7 +1683,9 @@ public class Expr extends AST * tautologies. Note also that 'and' and 'or' can take multiple arguments. * You can recover the propositional tautologies by unfolding the Boolean * connectives in the axioms a small bounded number of steps (=3). - * + * + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofDefAxiom() throws Z3Exception { @@ -1397,7 +1694,7 @@ public class Expr extends AST /** * Indicates whether the term is a proof for introduction of a name - * Introduces a name for a formula/term. Suppose e is an + * Remarks: Introduces a name for a formula/term. Suppose e is an * expression with free variables x, and def-intro introduces the name n(x). * The possible cases are: * @@ -1409,7 +1706,9 @@ public class Expr extends AST * When e is of the form (ite cond th el): [def-intro]: (and (or (not cond) * (= n th)) (or cond (= n el))) * - * Otherwise: [def-intro]: (= n e) + * Otherwise: [def-intro]: (= n e) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofDefIntro() throws Z3Exception { @@ -1418,8 +1717,10 @@ public class Expr extends AST /** * Indicates whether the term is a proof for application of a definition - * [apply-def T1]: F ~ n F is 'equivalent' to n, given that T1 is - * a proof that n is a name for F. + * Remarks: [apply-def T1]: F ~ n F is 'equivalent' to n, given that T1 is + * a proof that n is a name for F. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofApplyDef() throws Z3Exception { @@ -1427,8 +1728,11 @@ public class Expr extends AST } /** - * Indicates whether the term is a proof iff-oeq T1: (iff p q) - * [iff~ T1]: (~ p q) + * Indicates whether the term is a proof iff-oeq + * Remarks: T1: (iff p q) + * [iff~ T1]: (~ p q) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofIFFOEQ() throws Z3Exception { @@ -1436,7 +1740,8 @@ public class Expr extends AST } /** - * Indicates whether the term is a proof for a positive NNF step + * Indicates whether the term is a proof for a positive NNF step + * Remarks: * Proof for a (positive) NNF step. Example: * * T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: s_2 ~ r_2' @@ -1453,7 +1758,9 @@ public class Expr extends AST * top-level connective is changed during NNF conversion. The relevant * Boolean connectives for NNF_POS are 'implies', 'iff', 'xor', 'ite'. * NNF_NEG furthermore handles the case where negation is pushed over - * Boolean connectives 'and' and 'or'. + * Boolean connectives 'and' and 'or'. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofNNFPos() throws Z3Exception { @@ -1461,7 +1768,8 @@ public class Expr extends AST } /** - * Indicates whether the term is a proof for a negative NNF step + * Indicates whether the term is a proof for a negative NNF step + * Remarks: * Proof for a (negative) NNF step. Examples: * * T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n [nnf-neg T1 ... Tn]: (not @@ -1469,7 +1777,9 @@ public class Expr extends AST * (not s_n) ~ r_n [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 * ... r_n) and T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: * s_2 ~ r_2' [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2)) (and (or r_1 - * r_2) (or r_1' r_2'))) + * r_2) (or r_1' r_2'))) + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofNNFNeg() throws Z3Exception { @@ -1478,13 +1788,16 @@ public class Expr extends AST /** * Indicates whether the term is a proof for (~ P Q) here Q is in negation - * normal form. A proof for (~ P Q) where Q is in negation normal + * normal form. + * Remarks: A proof for (~ P Q) where Q is in negation normal * form. * * This proof object is only used if the parameter PROOF_MODE is 1. * * This proof object may have n antecedents. Each antecedent is a - * PR_DEF_INTRO. + * PR_DEF_INTRO. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofNNFStar() throws Z3Exception { @@ -1493,10 +1806,13 @@ public class Expr extends AST /** * Indicates whether the term is a proof for (~ P Q) where Q is in - * conjunctive normal form. A proof for (~ P Q) where Q is in + * conjunctive normal form. + * Remarks: A proof for (~ P Q) where Q is in * conjunctive normal form. This proof object is only used if the parameter * PROOF_MODE is 1. This proof object may have n antecedents. Each - * antecedent is a PR_DEF_INTRO. + * antecedent is a PR_DEF_INTRO. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofCNFStar() throws Z3Exception { @@ -1504,13 +1820,16 @@ public class Expr extends AST } /** - * Indicates whether the term is a proof for a Skolemization step + * Indicates whether the term is a proof for a Skolemization step + * Remarks: * Proof for: * * [sk]: (~ (not (forall x (p x y))) (not (p (sk y) y))) [sk]: (~ (exists x * (p x y)) (p (sk y) y)) * - * This proof object has no antecedents. + * This proof object has no antecedents. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofSkolemize() throws Z3Exception { @@ -1519,8 +1838,11 @@ public class Expr extends AST /** * Indicates whether the term is a proof by modus ponens for - * equi-satisfiability. Modus ponens style rule for - * equi-satisfiability. T1: p T2: (~ p q) [mp~ T1 T2]: q + * equi-satisfiability. + * Remarks: Modus ponens style rule for + * equi-satisfiability. T1: p T2: (~ p q) [mp~ T1 T2]: q + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofModusPonensOEQ() throws Z3Exception { @@ -1528,7 +1850,8 @@ public class Expr extends AST } /** - * Indicates whether the term is a proof for theory lemma Generic + * Indicates whether the term is a proof for theory lemma + * Remarks: Generic * proof for theory lemmas. * * The theory lemma function comes with one or more parameters. The first @@ -1539,7 +1862,9 @@ public class Expr extends AST * (negated) inequalities and obtain a contradiction. - triangle-eq - * Indicates a lemma related to the equivalence: (iff (= t1 t2) (and (<= * t1 t2) (<= t2 t1))) - gcd-test - Indicates an integer linear - * arithmetic lemma that uses a gcd test. + * arithmetic lemma that uses a gcd test. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isProofTheoryLemma() throws Z3Exception { @@ -1548,6 +1873,8 @@ public class Expr extends AST /** * Indicates whether the term is of an array sort. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isRelation() throws Z3Exception { @@ -1558,10 +1885,13 @@ public class Expr extends AST } /** - * Indicates whether the term is an relation store Insert a record - * into a relation. The function takes n+1 arguments, where the - * first argument is the relation and the remaining n elements - * correspond to the n columns of the relation. + * Indicates whether the term is an relation store + * Remarks: Insert a record + * into a relation. The function takes {@code n+1} arguments, where the + * first argument is the relation and the remaining {@code n} elements + * correspond to the {@code n} columns of the relation. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isRelationStore() throws Z3Exception { @@ -1570,6 +1900,8 @@ public class Expr extends AST /** * Indicates whether the term is an empty relation + * @throws Z3Exception on error + * @return a boolean **/ public boolean isEmptyRelation() throws Z3Exception { @@ -1578,6 +1910,8 @@ public class Expr extends AST /** * Indicates whether the term is a test for the emptiness of a relation + * @throws Z3Exception on error + * @return a boolean **/ public boolean isIsEmptyRelation() throws Z3Exception { @@ -1586,6 +1920,8 @@ public class Expr extends AST /** * Indicates whether the term is a relational join + * @throws Z3Exception on error + * @return a boolean **/ public boolean isRelationalJoin() throws Z3Exception { @@ -1594,7 +1930,10 @@ public class Expr extends AST /** * Indicates whether the term is the union or convex hull of two relations. - * The function takes two arguments. + * + * Remarks: The function takes two arguments. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isRelationUnion() throws Z3Exception { @@ -1602,8 +1941,11 @@ public class Expr extends AST } /** - * Indicates whether the term is the widening of two relations The - * function takes two arguments. + * Indicates whether the term is the widening of two relations + * Remarks: The + * function takes two arguments. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isRelationWiden() throws Z3Exception { @@ -1612,8 +1954,11 @@ public class Expr extends AST /** * Indicates whether the term is a projection of columns (provided as - * numbers in the parameters). The function takes one - * argument. + * numbers in the parameters). + * Remarks: The function takes one + * argument. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isRelationProject() throws Z3Exception { @@ -1621,11 +1966,14 @@ public class Expr extends AST } /** - * Indicates whether the term is a relation filter Filter + * Indicates whether the term is a relation filter + * Remarks: Filter * (restrict) a relation with respect to a predicate. The first argument is * a relation. The second argument is a predicate with free de-Brujin * indices corresponding to the columns of the relation. So the first column - * in the relation has index 0. + * in the relation has index 0. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isRelationFilter() throws Z3Exception { @@ -1634,7 +1982,8 @@ public class Expr extends AST /** * Indicates whether the term is an intersection of a relation with the - * negation of another. Intersect the first relation with respect + * negation of another. + * Remarks: Intersect the first relation with respect * to negation of the second relation (the function takes two arguments). * Logically, the specification can be described by a function * @@ -1642,7 +1991,9 @@ public class Expr extends AST * * where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, * such that target are elements in x in pos, such that there is no y in neg - * that agrees with x on the columns c1, d1, .., cN, dN. + * that agrees with x on the columns c1, d1, .., cN, dN. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isRelationNegationFilter() throws Z3Exception { @@ -1651,8 +2002,10 @@ public class Expr extends AST /** * Indicates whether the term is the renaming of a column in a relation - * The function takes one argument. The parameters contain the - * renaming as a cycle. + * Remarks: The function takes one argument. The parameters contain the + * renaming as a cycle. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isRelationRename() throws Z3Exception { @@ -1661,6 +2014,8 @@ public class Expr extends AST /** * Indicates whether the term is the complement of a relation + * @throws Z3Exception on error + * @return a boolean **/ public boolean isRelationComplement() throws Z3Exception { @@ -1668,10 +2023,13 @@ public class Expr extends AST } /** - * Indicates whether the term is a relational select Check if a - * record is an element of the relation. The function takes n+1 + * Indicates whether the term is a relational select + * Remarks: Check if a + * record is an element of the relation. The function takes {@code n+1} * arguments, where the first argument is a relation, and the remaining - * n arguments correspond to a record. + * {@code n} arguments correspond to a record. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isRelationSelect() throws Z3Exception { @@ -1679,11 +2037,15 @@ public class Expr extends AST } /** - * Indicates whether the term is a relational clone (copy) Create + * Indicates whether the term is a relational clone (copy) + * Remarks: Create * a fresh copy (clone) of a relation. The function is logically the * identity, but in the context of a register machine allows for terms of - * kind @see IsRelationUnion to perform destructive updates to - * the first argument. + * kind {@code isRelationUnion} to perform destructive updates to + * the first argument. + * @see isRelationUnion + * @throws Z3Exception on error + * @return a boolean **/ public boolean isRelationClone() throws Z3Exception { @@ -1692,6 +2054,8 @@ public class Expr extends AST /** * Indicates whether the term is of an array sort. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isFiniteDomain() throws Z3Exception { @@ -1703,392 +2067,31 @@ public class Expr extends AST /** * Indicates whether the term is a less than predicate over a finite domain. + * @throws Z3Exception on error + * @return a boolean **/ public boolean isFiniteDomainLT() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FD_LT; } - - /** - * Indicates whether the terms is of floating-point sort. - * @throws Z3Exception - */ - public boolean isFP() throws Z3Exception { return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_FLOATING_POINT_SORT; } - - /** - * Indicates whether the terms is of floating-point rounding mode sort. - * @return - * @throws Z3Exception - */ - public boolean isFPRM() throws Z3Exception { return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ROUNDING_MODE_SORT; } - - /** - * Indicates whether the term is a floating-point numeral - * @return - * @throws Z3Exception - */ - public boolean isFPNumeral() throws Z3Exception { return isFP() && isNumeral(); } - - /** - * Indicates whether the term is a floating-point rounding mode numeral - * @return - * @throws Z3Exception - */ - public boolean isFPRMNumeral() throws Z3Exception { return isFPRM() && isNumeral(); } - - /** - * Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven - * @return - * @throws Z3Exception - */ - public boolean isFPRMNumRoundNearestTiesToEven() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } - - /** - * Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway - * @return - * @throws Z3Exception - */ - public boolean isFPRMNumRoundNearestTiesToAway() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } - - /** - * Indicates whether the term is the floating-point rounding numeral roundTowardNegative - * @return - * @throws Z3Exception - */ - public boolean isFPRMNumRoundTowardNegative() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } - - /** - * Indicates whether the term is the floating-point rounding numeral roundTowardPositive - * @return - * @throws Z3Exception - */ - public boolean isFPRMNumRoundTowardPositive() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } - - /** - * Indicates whether the term is the floating-point rounding numeral roundTowardZero - * @return - * @throws Z3Exception - */ - public boolean isFPRMNumRoundTowardZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } - - /** - * Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven - * @return - * @throws Z3Exception - */ - public boolean isFPRMNumRNE() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } - - /** - * Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway - * @return - * @throws Z3Exception - */ - public boolean isFPRMNumRNA() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } - - /** - * Indicates whether the term is the floating-point rounding numeral roundTowardNegative - * @return - * @throws Z3Exception - */ - public boolean isFPRMNumRTN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } - - /** - * Indicates whether the term is the floating-point rounding numeral roundTowardPositive - * @return - * @throws Z3Exception - */ - public boolean isFPRMNumRTP() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } - - /** - * Indicates whether the term is the floating-point rounding numeral roundTowardZero - * @return - * @throws Z3Exception - */ - public boolean isFPRMNumRTZ() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } - - /** - * Indicates whether the term is a floating-point rounding mode numeral - * @return - * @throws Z3Exception - */ - public boolean isFPRMNum() throws Z3Exception { - return isApp() && - (getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY || - getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN || - getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE || - getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE || - getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO); - } - - /** - * Indicates whether the term is a floating-point +oo - * @return - * @throws Z3Exception - */ - public boolean isFPPlusInfinity() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_PLUS_INF; } - - /** - * Indicates whether the term is a floating-point -oo - * @return - * @throws Z3Exception - */ - public boolean isFPMinusInfinity() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MINUS_INF; } - - /** - * Indicates whether the term is a floating-point NaN - * @return - * @throws Z3Exception - */ - public boolean isFPNaN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_NAN; } - - /** - * Indicates whether the term is a floating-point +zero - * @return - * @throws Z3Exception - */ - public boolean isFPPlusZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_PLUS_ZERO; } - - /** - * Indicates whether the term is a floating-point -zero - * @return - * @throws Z3Exception - */ - public boolean isFPMinusZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MINUS_ZERO; } - - /** - * Indicates whether the term is a floating-point addition term - * @return - * @throws Z3Exception - */ - public boolean isFPAdd() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_ADD; } - - - /** - * Indicates whether the term is a floating-point subtraction term - * @return - * @throws Z3Exception - */ - public boolean isFPSub() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_SUB; } - - /** - * Indicates whether the term is a floating-point negation term - * @return - * @throws Z3Exception - */ - public boolean isFPNeg() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_NEG; } - - /** - * Indicates whether the term is a floating-point multiplication term - * @return - * @throws Z3Exception - */ - public boolean isFPMul() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MUL; } - - /** - * Indicates whether the term is a floating-point divison term - * @return - * @throws Z3Exception - */ - public boolean isFPDiv() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_DIV; } - - /** - * Indicates whether the term is a floating-point remainder term - * @return - * @throws Z3Exception - */ - public boolean isFPRem() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_REM; } - - /** - * Indicates whether the term is a floating-point term absolute value term - * @return - * @throws Z3Exception - */ - public boolean isFPAbs() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_ABS; } - - /** - * Indicates whether the term is a floating-point minimum term - * @return - * @throws Z3Exception - */ - public boolean isFPMin() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MIN; } - - /** - * Indicates whether the term is a floating-point maximum term - * @return - * @throws Z3Exception - */ - public boolean isFPMax() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MAX; } - - /** - * Indicates whether the term is a floating-point fused multiply-add term - * @return - * @throws Z3Exception - */ - public boolean isFPFMA() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_FMA; } - - /** - * Indicates whether the term is a floating-point square root term - * @return - * @throws Z3Exception - */ - public boolean isFPSqrt() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_SQRT; } - - /** - * Indicates whether the term is a floating-point roundToIntegral term - * @return - * @throws Z3Exception - */ - public boolean isFPRoundToIntegral() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_ROUND_TO_INTEGRAL; } - - /** - * Indicates whether the term is a floating-point equality term - * @return - * @throws Z3Exception - */ - public boolean isFPEq() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_EQ; } - - /** - * Indicates whether the term is a floating-point less-than term - * @return - * @throws Z3Exception - */ - public boolean isFPLt() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_LT; } - - /** - * Indicates whether the term is a floating-point greater-than term - * @return - * @throws Z3Exception - */ - public boolean isFPGt() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_GT; } - - /** - * Indicates whether the term is a floating-point less-than or equal term - * @return - * @throws Z3Exception - */ - public boolean isFPLe() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_LE; } - - /** - * Indicates whether the term is a floating-point greater-than or erqual term - * @return - * @throws Z3Exception - */ - public boolean isFPGe() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_GE; } - - /** - * Indicates whether the term is a floating-point isNaN predicate term - * @return - * @throws Z3Exception - */ - public boolean isFPisNaN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_NAN; } - - /** - * Indicates whether the term is a floating-point isInf predicate term - * @return - * @throws Z3Exception - */ - public boolean isFPisInf() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_INF; } - - /** - * Indicates whether the term is a floating-point isZero predicate term - * @return - * @throws Z3Exception - */ - public boolean isFPisZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_ZERO; } - - /** - * Indicates whether the term is a floating-point isNormal term - * @return - * @throws Z3Exception - */ - public boolean isFPisNormal() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_NORMAL; } - - /** - * Indicates whether the term is a floating-point isSubnormal predicate term - * @return - * @throws Z3Exception - */ - public boolean isFPisSubnormal() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_SUBNORMAL; } - - /** - * Indicates whether the term is a floating-point isNegative predicate term - * @return - * @throws Z3Exception - */ - public boolean isFPisNegative() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE; } - - /** - * Indicates whether the term is a floating-point isPositive predicate term - * @return - * @throws Z3Exception - */ - public boolean isFPisPositive() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE; } - - /** - * Indicates whether the term is a floating-point constructor term - * @return - * @throws Z3Exception - */ - public boolean isFPFP() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_FP; } - - /** - * Indicates whether the term is a floating-point conversion term - * @return - * @throws Z3Exception - */ - public boolean isFPToFp() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_FP; } - - /** - * Indicates whether the term is a floating-point conversion from unsigned bit-vector term - * @return - * @throws Z3Exception - */ - public boolean isFPToFpUnsigned() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_FP_UNSIGNED; } - - /** - * Indicates whether the term is a floating-point conversion to unsigned bit-vector term - * @return - * @throws Z3Exception - */ - public boolean isFPToUBV() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_UBV; } - - /** - * Indicates whether the term is a floating-point conversion to signed bit-vector term - * @return - * @throws Z3Exception - */ - public boolean isFPToSBV() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_SBV; } - - /** - * Indicates whether the term is a floating-point conversion to real term - * @return - * @throws Z3Exception - */ - public boolean isFPToReal() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_REAL; } - - /** - * Indicates whether the term is a floating-point conversion to IEEE-754 bit-vector term1 - * @return - * @throws Z3Exception - */ - public boolean isFPToIEEEBV() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_IEEE_BV; } - - /** - * The de-Burijn index of a bound variable. Bound variables are + * The de-Burijn index of a bound variable. + * Remarks: Bound variables are * indexed by de-Bruijn indices. It is perhaps easiest to explain the * meaning of de-Bruijn indices by indicating the compilation process from - * non-de-Bruijn formulas to de-Bruijn format. + * non-de-Bruijn formulas to de-Bruijn format. {@code * abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0) * abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi)) * abs1(x, x, n) = b_n * abs1(y, x, n) = y * abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n)) * abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1)) - * The last line is significant: the index of a bound variable is + * } The last line is significant: the index of a bound variable is * different depending on the scope in which it appears. The deeper x - * appears, the higher is its index. + * appears, the higher is its index. + * @throws Z3Exception on error + * @return an int **/ public int getIndex() throws Z3Exception { @@ -2101,9 +2104,22 @@ public class Expr extends AST /** * Constructor for Expr **/ + protected Expr(Context ctx) + { + super(ctx); + { + } + } + + /** + * Constructor for Expr + * @throws Z3Exception on error + **/ protected Expr(Context ctx, long obj) throws Z3Exception { super(ctx, obj); + { + } } void checkNativeObject(long obj) throws Z3Exception @@ -2129,7 +2145,8 @@ public class Expr extends AST if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) return new Quantifier(ctx, obj); long s = Native.getSort(ctx.nCtx(), obj); - Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), s)); + Z3_sort_kind sk = Z3_sort_kind + .fromInt(Native.getSortKind(ctx.nCtx(), s)); if (Native.isAlgebraicNumber(ctx.nCtx(), obj)) // is this a numeral ast? return new AlgebraicNum(ctx, obj); @@ -2144,10 +2161,6 @@ public class Expr extends AST return new RatNum(ctx, obj); case Z3_BV_SORT: return new BitVecNum(ctx, obj); - case Z3_FLOATING_POINT_SORT: - return new FPNum(ctx, obj); - case Z3_ROUNDING_MODE_SORT: - return new FPRMNum(ctx, obj); default: ; } } @@ -2166,10 +2179,6 @@ public class Expr extends AST return new ArrayExpr(ctx, obj); case Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj); - case Z3_FLOATING_POINT_SORT: - return new FPExpr(ctx, obj); - case Z3_ROUNDING_MODE_SORT: - return new FPRMExpr(ctx, obj); default: ; } diff --git a/src/api/java/FiniteDomainSort.java b/src/api/java/FiniteDomainSort.java index 4cb2ab917..cece06f1a 100644 --- a/src/api/java/FiniteDomainSort.java +++ b/src/api/java/FiniteDomainSort.java @@ -24,6 +24,7 @@ public class FiniteDomainSort extends Sort { /** * The size of the finite domain sort. + * @throws Z3Exception on error **/ public long getSize() throws Z3Exception { diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index 37653bbd0..587f47cbb 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -163,7 +163,8 @@ public class Fixedpoint extends Z3Object } /** - * Creates a backtracking point. @see Pop + * Creates a backtracking point. + * @see pop **/ public void push() throws Z3Exception { @@ -171,9 +172,11 @@ public class Fixedpoint extends Z3Object } /** - * Backtrack one backtracking point. Note that an exception is - * thrown if Pop is called without a corresponding Push - * @see Push + * Backtrack one backtracking point. + * Remarks: Note that an exception is thrown if {#code pop} + * is called without a corresponding {@code push} + * + * @see push **/ public void pop() throws Z3Exception { diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index 573ebd102..5307951e5 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -29,7 +29,7 @@ public class FuncDecl extends AST /** * Comparison operator. * - * @return True if and share the + * @return True if {@code a"/> and and do not + * @return True if {@code a"/> and + * The size of the domain of the function declaration + * @see getArity **/ public int getDomainSize() throws Z3Exception { @@ -221,7 +221,7 @@ public class FuncDecl extends AST private String r; /** - * The int value of the parameter. + * The int value of the parameter. **/ public int getInt() throws Z3Exception { @@ -231,7 +231,7 @@ public class FuncDecl extends AST } /** - * The double value of the parameter. + * The double value of the parameter. **/ public double getDouble() throws Z3Exception { @@ -241,7 +241,7 @@ public class FuncDecl extends AST } /** - * The Symbol value of the parameter. + * The Symbol value of the parameter. **/ public Symbol getSymbol() throws Z3Exception { @@ -251,7 +251,7 @@ public class FuncDecl extends AST } /** - * The Sort value of the parameter. + * The Sort value of the parameter. **/ public Sort getSort() throws Z3Exception { @@ -261,7 +261,7 @@ public class FuncDecl extends AST } /** - * The AST value of the parameter. + * The AST value of the parameter. **/ public AST getAST() throws Z3Exception { @@ -271,7 +271,7 @@ public class FuncDecl extends AST } /** - * The FunctionDeclaration value of the parameter. + * The FunctionDeclaration value of the parameter. **/ public FuncDecl getFuncDecl() throws Z3Exception { @@ -281,7 +281,7 @@ public class FuncDecl extends AST } /** - * The rational string value of the parameter. + * The rational string value of the parameter. **/ public String getRational() throws Z3Exception { @@ -375,8 +375,8 @@ public class FuncDecl extends AST } /** - * Create expression that applies function to arguments. + * Create expression that applies function to arguments. + * @param args * * @return **/ diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java index 243ade71f..fd0c10d2e 100644 --- a/src/api/java/FuncInterp.java +++ b/src/api/java/FuncInterp.java @@ -34,7 +34,8 @@ public class FuncInterp extends Z3Object * Return the (symbolic) value of this entry. * * @throws Z3Exception - **/ + * @throws Z3Exception on error + **/ public Expr getValue() throws Z3Exception { return Expr.create(getContext(), @@ -43,7 +44,8 @@ public class FuncInterp extends Z3Object /** * The number of arguments of the entry. - **/ + * @throws Z3Exception on error + **/ public int getNumArgs() throws Z3Exception { return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject()); @@ -53,7 +55,8 @@ public class FuncInterp extends Z3Object * The arguments of the function entry. * * @throws Z3Exception - **/ + * @throws Z3Exception on error + **/ public Expr[] getArgs() throws Z3Exception { int n = getNumArgs(); @@ -103,6 +106,8 @@ public class FuncInterp extends Z3Object /** * The number of entries in the function interpretation. + * @throws Z3Exception on error + * @return an int **/ public int getNumEntries() throws Z3Exception { @@ -113,6 +118,7 @@ public class FuncInterp extends Z3Object * The entries in the function interpretation * * @throws Z3Exception + * @throws Z3Exception on error **/ public Entry[] getEntries() throws Z3Exception { @@ -128,6 +134,8 @@ public class FuncInterp extends Z3Object * The (symbolic) `else' value of the function interpretation. * * @throws Z3Exception + * @throws Z3Exception on error + * @return an Expr **/ public Expr getElse() throws Z3Exception { @@ -137,6 +145,8 @@ public class FuncInterp extends Z3Object /** * The arity of the function interpretation + * @throws Z3Exception on error + * @return an int **/ public int getArity() throws Z3Exception { diff --git a/src/api/java/Global.java b/src/api/java/Global.java index 2fa3abbbe..b31c4a7ae 100644 --- a/src/api/java/Global.java +++ b/src/api/java/Global.java @@ -19,16 +19,16 @@ package com.microsoft.z3; /** * Global functions for Z3. - * + * Remarks: * This (static) class contains functions that effect the behaviour of Z3 * globally across contexts, etc. - * + * **/ public final class Global { /** * Set a global (or module) parameter, which is shared by all Z3 contexts. - * + * Remarks: * When a Z3 module is initialized it will use the value of these parameters * when Z3_params objects are not provided. * The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'. @@ -36,11 +36,11 @@ public final class Global * The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'. * Thus, the following parameter names are considered equivalent: "pp.decimal-precision" and "PP.DECIMAL_PRECISION". * This function can be used to set parameters for a specific Z3 module. - * This can be done by using .. + * This can be done by using <module-name>.<parameter-name>. * For example: * Z3_global_param_set('pp.decimal', 'true') * will set the parameter "decimal" in the module "pp" to true. - * + * **/ public static void setParameter(String id, String value) { @@ -49,11 +49,10 @@ public final class Global /** * Get a global (or module) parameter. - * - * Returns null if the parameter @param id parameter id does not exist. + * Remarks: * This function cannot be invoked simultaneously from different threads without synchronization. * The result string stored in param_value is stored in a shared location. - * + * @return null if the parameter {@code id} does not exist. **/ public static String getParameter(String id) { @@ -66,10 +65,9 @@ public final class Global /** * Restore the value of all global (and module) parameters. - * + * Remarks: * This command will not affect already created objects (such as tactics and solvers) - * - * @see SetParameter + * @see setParameter **/ public static void resetParameters() { diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index aba8b0149..5a9221b63 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -26,11 +26,12 @@ import com.microsoft.z3.enumerations.Z3_goal_prec; public class Goal extends Z3Object { /** - * The precision of the goal. Goals can be transformed using over + * The precision of the goal. + * Remarks: Goals can be transformed using over * and under approximations. An under approximation is applied when the * objective is to find a model for a given goal. An over approximation is * applied when the objective is to find a proof for a given goal. - * + * **/ public Z3_goal_prec getPrecision() throws Z3Exception { @@ -72,7 +73,7 @@ public class Goal extends Z3Object } /** - * Adds the to the given goal. + * Adds the {@code constraints} to the given goal. * * @throws Z3Exception **/ @@ -95,8 +96,9 @@ public class Goal extends Z3Object } /** - * The depth of the goal. This tracks how many transformations - * were applied to it. + * The depth of the goal. + * Remarks: This tracks how many transformations + * were applied to it. **/ public int getDepth() throws Z3Exception { @@ -162,8 +164,7 @@ public class Goal extends Z3Object } /** - * Translates (copies) the Goal to the target Context . + * Translates (copies) the Goal to the target Context {@code ctx}. * * @throws Z3Exception **/ @@ -174,8 +175,9 @@ public class Goal extends Z3Object } /** - * Simplifies the goal. Essentially invokes the `simplify' tactic - * on the goal. + * Simplifies the goal. + * Remarks: Essentially invokes the `simplify' tactic + * on the goal. **/ public Goal simplify() throws Z3Exception { @@ -189,8 +191,9 @@ public class Goal extends Z3Object } /** - * Simplifies the goal. Essentially invokes the `simplify' tactic - * on the goal. + * Simplifies the goal. + * Remarks: Essentially invokes the `simplify' tactic + * on the goal. **/ public Goal simplify(Params p) throws Z3Exception { diff --git a/src/api/java/IntExpr.java b/src/api/java/IntExpr.java index de3ae222a..642a58a54 100644 --- a/src/api/java/IntExpr.java +++ b/src/api/java/IntExpr.java @@ -23,7 +23,8 @@ package com.microsoft.z3; public class IntExpr extends ArithExpr { /** - * Constructor for IntExpr + * Constructor for IntExpr + * @throws Z3Exception on error **/ IntExpr(Context ctx, long obj) throws Z3Exception { diff --git a/src/api/java/IntSymbol.java b/src/api/java/IntSymbol.java index b0f1af685..a677c9102 100644 --- a/src/api/java/IntSymbol.java +++ b/src/api/java/IntSymbol.java @@ -25,8 +25,9 @@ import com.microsoft.z3.enumerations.Z3_symbol_kind; public class IntSymbol extends Symbol { /** - * The int value of the symbol. Throws an exception if the symbol - * is not of int kind. + * The int value of the symbol. + * Remarks: Throws an exception if the symbol + * is not of int kind. **/ public int getInt() throws Z3Exception { diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 43ae86162..c1590e07f 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -22,11 +22,11 @@ import java.lang.String; import com.microsoft.z3.enumerations.Z3_lbool; -/** +/** * The InterpolationContext is suitable for generation of interpolants. - * - * For more information on interpolation please refer - * too the C/C++ API, which is well documented. + * + * Remarks: For more information on interpolation please refer + * too the C/C++ API, which is well documented. **/ public class InterpolationContext extends Context { @@ -42,7 +42,9 @@ public class InterpolationContext extends Context /** * Constructor. * - * @see Context.Context(Dictionary<string, string>) + * + * Remarks: + * @see Context#Context **/ public InterpolationContext(Map settings) throws Z3Exception { @@ -56,7 +58,7 @@ public class InterpolationContext extends Context /** * Create an expression that marks a formula position for interpolation. - * @throws Z3Exception + * @throws Z3Exception **/ public BoolExpr MkInterpolant(BoolExpr a) throws Z3Exception { @@ -66,9 +68,9 @@ public class InterpolationContext extends Context /** * Computes an interpolant. - * For more information on interpolation please refer + * Remarks: For more information on interpolation please refer * too the function Z3_get_interpolant in the C/C++ API, which is - * well documented. + * well documented. * @throws Z3Exception **/ Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception @@ -87,9 +89,9 @@ public class InterpolationContext extends Context /** * Computes an interpolant. - * For more information on interpolation please refer + * Remarks: For more information on interpolation please refer * too the function Z3_compute_interpolant in the C/C++ API, which is - * well documented. + * well documented. * @throws Z3Exception **/ Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception @@ -105,23 +107,23 @@ public class InterpolationContext extends Context return Z3_lbool.fromInt(r); } - /// + /// /// Return a string summarizing cumulative time used for interpolation. - /// - /// For more information on interpolation please refer + /// + /// Remarks: For more information on interpolation please refer /// too the function Z3_interpolation_profile in the C/C++ API, which is - /// well documented. + /// well documented. public String InterpolationProfile() throws Z3Exception { return Native.interpolationProfile(nCtx()); } - /// + /// /// Checks the correctness of an interpolant. - /// - /// For more information on interpolation please refer + /// + /// Remarks: For more information on interpolation please refer /// too the function Z3_check_interpolant in the C/C++ API, which is - /// well documented. + /// well documented. public int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory) throws Z3Exception { Native.StringPtr n_err_str = new Native.StringPtr(); @@ -137,12 +139,12 @@ public class InterpolationContext extends Context return r; } - /// + /// /// Reads an interpolation problem from a file. - /// - /// For more information on interpolation please refer + /// + /// Remarks: For more information on interpolation please refer /// too the function Z3_read_interpolation_problem in the C/C++ API, which is - /// well documented. + /// well documented. public int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception { Native.IntPtr n_num = new Native.IntPtr(); @@ -168,12 +170,12 @@ public class InterpolationContext extends Context return r; } - /// + /// /// Writes an interpolation problem to a file. - /// - /// For more information on interpolation please refer + /// + /// Remarks: For more information on interpolation please refer /// too the function Z3_write_interpolation_problem in the C/C++ API, which is - /// well documented. + /// well documented. public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception { Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory)); diff --git a/src/api/java/Log.java b/src/api/java/Log.java index 254da1bc6..3e8f0050b 100644 --- a/src/api/java/Log.java +++ b/src/api/java/Log.java @@ -18,17 +18,18 @@ Notes: package com.microsoft.z3; /** - * Interaction logging for Z3. Note that this is a global, static log + * Interaction logging for Z3. + * Remarks: Note that this is a global, static log * and if multiple Context objects are created, it logs the interaction with all - * of them. + * of them. **/ public final class Log { private static boolean m_is_open = false; /** - * Open an interaction log file. the name of the file - * to open + * Open an interaction log file. + * @param filename the name of the file to open * * @return True if opening the log file succeeds, false otherwise. **/ @@ -48,7 +49,7 @@ public final class Log } /** - * Appends the user-provided string to the interaction + * Appends the user-provided string {@code s} to the interaction * log. * @throws Z3Exception **/ diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 1ebe7973b..70f0e91c5 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -25,8 +25,9 @@ import com.microsoft.z3.enumerations.Z3_sort_kind; public class Model extends Z3Object { /** - * Retrieves the interpretation (the assignment) of in - * the model. @param a A Constant + * Retrieves the interpretation (the assignment) of {@code a} in + * the model. + * @param a A Constant * * @return An expression if the constant has an interpretation in the model, * null otherwise. @@ -39,8 +40,9 @@ public class Model extends Z3Object } /** - * Retrieves the interpretation (the assignment) of in - * the model. @param f A function declaration of zero arity + * Retrieves the interpretation (the assignment) of {@code f} in + * the model. + * @param f A function declaration of zero arity * * @return An expression if the function has an interpretation in the model, * null otherwise. @@ -65,9 +67,8 @@ public class Model extends Z3Object } /** - * Retrieves the interpretation (the assignment) of a non-constant in the model. A function declaration of - * non-zero arity + * Retrieves the interpretation (the assignment) of a non-constant {@code f} in the model. + * @param f A function declaration of non-zero arity * * @return A FunctionInterpretation if the function has an interpretation in * the model, null otherwise. @@ -196,16 +197,15 @@ public class Model extends Z3Object } /** - * Evaluates the expression in the current model. - * This function may fail if contains - * quantifiers, is partial (MODEL_PARTIAL enabled), or if is not well-sorted. In this case a - * ModelEvaluationFailedException is thrown. An expression When this flag + * Evaluates the expression {@code t} in the current model. + * Remarks: This function may fail if {@code t} contains + * quantifiers, is partial (MODEL_PARTIAL enabled), or if {@code t} is not well-sorted. In this case a + * {@code ModelEvaluationFailedException} is thrown. + * @param t An expression {@code completion} When this flag * is enabled, a model value will be assigned to any constant or function - * that does not have an interpretation in the model. + * that does not have an interpretation in the model. * - * @return The evaluation of in the model. + * @return The evaluation of {@code t} in the model. * @throws Z3Exception **/ public Expr eval(Expr t, boolean completion) throws Z3Exception @@ -219,7 +219,7 @@ public class Model extends Z3Object } /** - * Alias for Eval. + * Alias for {@code Eval}. * * @throws Z3Exception **/ @@ -239,10 +239,12 @@ public class Model extends Z3Object /** * The uninterpreted sorts that the model has an interpretation for. - * Z3 also provides an intepretation for uninterpreted sorts used + * Remarks: Z3 also provides an intepretation for uninterpreted sorts used * in a formula. The interpretation for a sort is a finite set of distinct - * values. We say this finite set is the "universe" of the sort. - * @see NumSorts"/> . @see Sorts An - * uninterpreted sort + * sort {@code s}. + * @param s An uninterpreted sort * * @return An array of expressions, where each is an element of the universe - * of + * of {@code s} * @throws Z3Exception **/ public Expr[] getSortUniverse(Sort s) throws Z3Exception diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java index 17ad81b5c..335bd038c 100644 --- a/src/api/java/Probe.java +++ b/src/api/java/Probe.java @@ -21,8 +21,8 @@ package com.microsoft.z3; * Probes are used to inspect a goal (aka problem) and collect information that * may be used to decide which solver and/or preprocessing step will be used. * The complete list of probes may be obtained using the procedures - * Context.NumProbes and Context.ProbeNames. It may - * also be obtained using the command (help-tactics) in the SMT 2.0 + * {@code Context.NumProbes} and {@code Context.ProbeNames}. It may + * also be obtained using the command {@code (help-tactics)} in the SMT 2.0 * front-end. **/ public class Probe extends Z3Object diff --git a/src/api/java/RatNum.java b/src/api/java/RatNum.java index f937ea593..2e92a9429 100644 --- a/src/api/java/RatNum.java +++ b/src/api/java/RatNum.java @@ -61,8 +61,9 @@ public class RatNum extends RealExpr } /** - * Returns a string representation in decimal notation. The result - * has at most decimal places. + * Returns a string representation in decimal notation. + * Remarks: The result + * has at most {@code precision} decimal places. **/ public String toDecimalString(int precision) throws Z3Exception { diff --git a/src/api/java/RealExpr.java b/src/api/java/RealExpr.java index c699e13e2..579d344e1 100644 --- a/src/api/java/RealExpr.java +++ b/src/api/java/RealExpr.java @@ -23,7 +23,7 @@ package com.microsoft.z3; public class RealExpr extends ArithExpr { /** - * Constructor for RealExpr + * Constructor for RealExpr **/ RealExpr(Context ctx, long obj) throws Z3Exception { diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index 4a7c1ed09..b9c9ebca6 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -56,8 +56,9 @@ public class Solver extends Z3Object } /** - * The current number of backtracking points (scopes). @see Pop - * @see Push + * The current number of backtracking points (scopes). + * @see pop + * @see push **/ public int getNumScopes() throws Z3Exception { @@ -66,7 +67,8 @@ public class Solver extends Z3Object } /** - * Creates a backtracking point. @see Pop + * Creates a backtracking point. + * @see pop **/ public void push() throws Z3Exception { @@ -74,7 +76,8 @@ public class Solver extends Z3Object } /** - * Backtracks one backtracking point. . + * Backtracks one backtracking point. + * Remarks: . **/ public void pop() throws Z3Exception { @@ -82,9 +85,11 @@ public class Solver extends Z3Object } /** - * Backtracks backtracking points. Note that - * an exception is thrown if is not smaller than - * NumScopes @see Push + * Backtracks {@code n} backtracking points. + * Remarks: Note that + * an exception is thrown if {@code n} is not smaller than + * {@code NumScopes} + * @see push **/ public void pop(int n) throws Z3Exception { @@ -92,8 +97,9 @@ public class Solver extends Z3Object } /** - * Resets the Solver. This removes all assertions from the - * solver. + * Resets the Solver. + * Remarks: This removes all assertions from the + * solver. **/ public void reset() throws Z3Exception { @@ -115,12 +121,12 @@ public class Solver extends Z3Object } } - // / + // / // / Assert multiple constraints into the solver, and track them (in the // unsat) core // / using the Boolean constants in ps. - // / - // / + // / + // / Remarks: // / This API is an alternative to with assumptions for // extracting unsat cores. // / Both APIs can be used in the same solver. The unsat core will contain a @@ -128,7 +134,7 @@ public class Solver extends Z3Object // / of the Boolean variables provided using // and the Boolean literals // / provided using with assumptions. - // / + // / public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) throws Z3Exception { getContext().checkContextMatch(constraints); @@ -141,11 +147,11 @@ public class Solver extends Z3Object constraints[i].getNativeObject(), ps[i].getNativeObject()); } - // / + // / // / Assert a constraint into the solver, and track it (in the unsat) core // / using the Boolean constant p. - // / - // / + // / + // / Remarks: // / This API is an alternative to with assumptions for // extracting unsat cores. // / Both APIs can be used in the same solver. The unsat core will contain a @@ -153,7 +159,7 @@ public class Solver extends Z3Object // / of the Boolean variables provided using // and the Boolean literals // / provided using with assumptions. - // / + // / public void assertAndTrack(BoolExpr constraint, BoolExpr p) throws Z3Exception { getContext().checkContextMatch(constraint); @@ -193,8 +199,10 @@ public class Solver extends Z3Object /** * Checks whether the assertions in the solver are consistent or not. - * @see Model"/> + * Remarks: + * @see getModel + * @see getUnsatCore + * @see getProof **/ public Status check(Expr... assumptions) throws Z3Exception { @@ -219,8 +227,10 @@ public class Solver extends Z3Object /** * Checks whether the assertions in the solver are consistent or not. - * @see Model"/> + * Remarks: + * @see getModel + * @see getUnsatCore + * @see getProof **/ public Status check() throws Z3Exception { @@ -228,10 +238,11 @@ public class Solver extends Z3Object } /** - * The model of the last Check. The result is - * null if Check was not invoked before, if its - * results was not SATISFIABLE, or if model production is not - * enabled. + * The model of the last {@code Check}. + * Remarks: The result is + * {@code null} if {@code Check} was not invoked before, if its + * results was not {@code SATISFIABLE}, or if model production is not + * enabled. * * @throws Z3Exception **/ @@ -245,10 +256,11 @@ public class Solver extends Z3Object } /** - * The proof of the last Check. The result is - * null if Check was not invoked before, if its - * results was not UNSATISFIABLE, or if proof production is - * disabled. + * The proof of the last {@code Check}. + * Remarks: The result is + * {@code null} if {@code Check} was not invoked before, if its + * results was not {@code UNSATISFIABLE}, or if proof production is + * disabled. * * @throws Z3Exception **/ @@ -262,10 +274,11 @@ public class Solver extends Z3Object } /** - * The unsat core of the last Check. The unsat core - * is a subset of Assertions The result is empty if - * Check was not invoked before, if its results was not - * UNSATISFIABLE, or if core production is disabled. + * The unsat core of the last {@code Check}. + * Remarks: The unsat core + * is a subset of {@code Assertions} The result is empty if + * {@code Check} was not invoked before, if its results was not + * {@code UNSATISFIABLE}, or if core production is disabled. * * @throws Z3Exception **/ @@ -282,8 +295,8 @@ public class Solver extends Z3Object } /** - * A brief justification of why the last call to Check returned - * UNKNOWN. + * A brief justification of why the last call to {@code Check} returned + * {@code UNKNOWN}. **/ public String getReasonUnknown() throws Z3Exception { diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index fa556e67f..270abd43f 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -28,8 +28,8 @@ public class Sort extends AST /* Overloaded operators are not translated. */ /** - * Equality operator for objects of type Sort. - * + * Equality operator for objects of type Sort. + * @param o * @return **/ public boolean equals(Object o) diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java index 315feeaa2..88a897d15 100644 --- a/src/api/java/Statistics.java +++ b/src/api/java/Statistics.java @@ -24,7 +24,7 @@ public class Statistics extends Z3Object { /** * Statistical data is organized into pairs of [Key, Entry], where every - * Entry is either a DoubleEntry or a UIntEntry + * Entry is either a {@code DoubleEntry} or a {@code UIntEntry} **/ public class Entry { @@ -176,8 +176,9 @@ public class Statistics extends Z3Object } /** - * The value of a particular statistical counter. Returns null if - * the key is unknown. + * The value of a particular statistical counter. + * Remarks: Returns null if + * the key is unknown. * * @throws Z3Exception **/ diff --git a/src/api/java/StringSymbol.java b/src/api/java/StringSymbol.java index 09273c946..4692b0fb9 100644 --- a/src/api/java/StringSymbol.java +++ b/src/api/java/StringSymbol.java @@ -25,8 +25,9 @@ import com.microsoft.z3.enumerations.Z3_symbol_kind; public class StringSymbol extends Symbol { /** - * The string value of the symbol. Throws an exception if the - * symbol is not of string kind. + * The string value of the symbol. + * Remarks: Throws an exception if the + * symbol is not of string kind. **/ public String getString() throws Z3Exception { diff --git a/src/api/java/Tactic.java b/src/api/java/Tactic.java index 6573a1407..0286e786d 100644 --- a/src/api/java/Tactic.java +++ b/src/api/java/Tactic.java @@ -20,8 +20,8 @@ package com.microsoft.z3; /** * Tactics are the basic building block for creating custom solvers for specific * problem domains. The complete list of tactics may be obtained using - * Context.NumTactics and Context.TacticNames. It may - * also be obtained using the command (help-tactics) in the SMT 2.0 + * {@code Context.NumTactics} and {@code Context.TacticNames}. It may + * also be obtained using the command {@code (help-tactics)} in the SMT 2.0 * front-end. **/ public class Tactic extends Z3Object @@ -73,8 +73,8 @@ public class Tactic extends Z3Object } /** - * Creates a solver that is implemented using the given tactic. + * Creates a solver that is implemented using the given tactic. + * @see Context#mkSolver(Tactic) * @throws Z3Exception **/ public Solver getSolver() throws Z3Exception diff --git a/src/api/java/Version.java b/src/api/java/Version.java index 3f019390b..6e2fe5084 100644 --- a/src/api/java/Version.java +++ b/src/api/java/Version.java @@ -18,7 +18,8 @@ Notes: package com.microsoft.z3; /** - * Version information. Note that this class is static. + * Version information. + * Remarks: Note that this class is static. **/ public class Version {