diff --git a/src/api/java/Context.java b/src/api/java/Context.java index eb51af101..9fa17fcd4 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -326,13 +326,6 @@ public class Context extends IDisposable /** * Create a datatype constructor. - * @param name - * @param recognizer - * @param fieldNames - * @param sorts - * @param sortRefs - * - * @return **/ public Constructor mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs) @@ -395,10 +388,6 @@ public class Context extends IDisposable /** * Create mutually recursive data-types. - * @param names - * @param c - * - * @return **/ public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c) @@ -410,7 +399,7 @@ public class Context extends IDisposable * Update a datatype field at expression t with value v. * The function performs a record update at t. The field * that is passed in as argument is updated with value v, - * the remainig fields of t are unchanged. + * the remaining fields of t are unchanged. **/ public Expr MkUpdateField(FuncDecl field, Expr t, Expr v) throws Z3Exception @@ -506,8 +495,8 @@ public class Context extends IDisposable /** * Creates a fresh constant function declaration with a name prefixed with * {@code prefix"}. - * @see mkFuncDecl(String,Sort,Sort) - * @see mkFuncDecl(String,Sort[],Sort) + * @see #mkFuncDecl(String,Sort,Sort) + * @see #mkFuncDecl(String,Sort[],Sort) **/ public FuncDecl mkFreshConstDecl(String prefix, Sort range) @@ -1523,7 +1512,7 @@ public class Context extends IDisposable { checkContextMatch(t); return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(), - (signed) ? true : false)); + (signed))); } /** @@ -1663,8 +1652,8 @@ public class Context extends IDisposable * {@code [domain -> range]}, and {@code i} must have the sort * {@code domain}. The sort of the result is {@code range}. * - * @see mkArraySort - * @see mkStore + * @see #mkArraySort + * @see #mkStore **/ public Expr mkSelect(ArrayExpr a, Expr i) @@ -1689,8 +1678,8 @@ public class Context extends IDisposable * {@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 + * @see #mkArraySort + * @see #mkSelect **/ public ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v) @@ -1707,8 +1696,8 @@ public class Context extends IDisposable * Remarks: The resulting term is an array, such * that a {@code select} on an arbitrary index produces the value * {@code v}. - * @see mkArraySort - * @see mkSelect + * @see #mkArraySort + * @see #mkSelect * **/ public ArrayExpr mkConstArray(Sort domain, Expr v) @@ -1721,15 +1710,15 @@ public class Context extends IDisposable /** * Maps f on the argument arrays. - * Remarks: Eeach element of + * Remarks: Each 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 + * @see #mkArraySort + * @see #mkSelect + * @see #mkStore **/ public ArrayExpr mkMap(FuncDecl f, ArrayExpr... args) @@ -2122,12 +2111,13 @@ public class Context extends IDisposable * * @return A Term with value {@code num}/{@code den} * and sort Real - * @see mkNumeral(String,Sort) + * @see #mkNumeral(String,Sort) **/ public RatNum mkReal(int num, int den) { - if (den == 0) + if (den == 0) { throw new Z3Exception("Denominator is zero"); + } return new RatNum(this, Native.mkReal(nCtx(), num, den)); } @@ -2257,7 +2247,7 @@ public class Context extends IDisposable * 'names' of the bound variables, and {@code body} is the body * of the quantifier. Quantifiers are associated with weights indicating the * importance of using the quantifier during instantiation. - * Note that the bound variables are de-Bruijn indices created using {@link mkBound}. + * Note that the bound variables are de-Bruijn indices created using {@link #mkBound}. * Z3 applies the convention that the last element in {@code names} and * {@code sorts} refers to the variable with index 0, the second to last element * of {@code names} and {@code sorts} refers to the variable @@ -2287,7 +2277,7 @@ public class Context extends IDisposable /** * Creates an existential quantifier using de-Brujin indexed variables. - * @see mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol) + * @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, @@ -2414,7 +2404,7 @@ public class Context extends IDisposable /** * Parse the given file using the SMT-LIB parser. - * @see parseSMTLIBString + * @see #parseSMTLIBString **/ public void parseSMTLIBFile(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) @@ -2528,7 +2518,7 @@ public class Context extends IDisposable /** * Parse the given string using the SMT-LIB2 parser. - * @see parseSMTLIBString + * @see #parseSMTLIBString * * @return A conjunction of assertions in the scope (up to push/pop) at the * end of the string. @@ -2542,8 +2532,9 @@ public class Context extends IDisposable int cs = Sort.arrayLength(sorts); int cdn = Symbol.arrayLength(declNames); int cd = AST.arrayLength(decls); - if (csn != cs || cdn != cd) + if (csn != cs || cdn != cd) { throw new Z3Exception("Argument size mismatch"); + } return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(), str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts), AST.arrayLength(decls), @@ -2552,13 +2543,12 @@ public class Context extends IDisposable /** * Parse the given file using the SMT-LIB2 parser. - * @see parseSMTLIB2String + * @see #parseSMTLIB2String **/ public BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) { - int csn = Symbol.arrayLength(sortNames); int cs = Sort.arrayLength(sorts); int cdn = Symbol.arrayLength(declNames); @@ -2649,9 +2639,10 @@ public class Context extends IDisposable if (ts != null && ts.length > 0) { last = ts[ts.length - 1].getNativeObject(); - for (int i = ts.length - 2; i >= 0; i--) + for (int i = ts.length - 2; i >= 0; i--) { last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(), - last); + last); + } } if (last != 0) { @@ -2665,7 +2656,7 @@ public class Context extends IDisposable /** * Create a tactic that applies {@code t1} to a Goal and then - * {@code t2"/> to every subgoal produced by with assumptions for + * This API is an alternative to {@link #check} with assumptions for * extracting unsat cores. * Both APIs can be used in the same solver. The unsat core will contain a * combination - * of the Boolean variables provided using + * of the Boolean variables provided using {@code assertAndTrack} * and the Boolean literals - * provided using with assumptions. + * provided using {@link #check} with assumptions. **/ public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) { getContext().checkContextMatch(constraints); getContext().checkContextMatch(ps); - if (constraints.length != ps.length) + if (constraints.length != ps.length) { throw new Z3Exception("Argument size mismatch"); + } - for (int i = 0; i < constraints.length; i++) + for (int i = 0; i < constraints.length; i++) { Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(), - constraints[i].getNativeObject(), ps[i].getNativeObject()); + constraints[i].getNativeObject(), ps[i].getNativeObject()); + } } /** @@ -152,13 +154,13 @@ public class Solver extends Z3Object * using the Boolean constant p. * * Remarks: - * This API is an alternative to with assumptions for + * This API is an alternative to {@link #check} with assumptions for * extracting unsat cores. * Both APIs can be used in the same solver. The unsat core will contain a * combination - * of the Boolean variables provided using + * of the Boolean variables provided using {@link #assertAndTrack} * and the Boolean literals - * provided using with assumptions. + * provided using {@link #check} with assumptions. */ public void assertAndTrack(BoolExpr constraint, BoolExpr p) { @@ -194,9 +196,9 @@ public class Solver extends Z3Object /** * Checks whether the assertions in the solver are consistent or not. * Remarks: - * @see getModel - * @see getUnsatCore - * @see getProof + * @see #getModel + * @see #getUnsatCore + * @see #getProof **/ public Status check(Expr... assumptions) { @@ -223,9 +225,9 @@ public class Solver extends Z3Object /** * Checks whether the assertions in the solver are consistent or not. * Remarks: - * @see getModel - * @see getUnsatCore - * @see getProof + * @see #getModel + * @see #getUnsatCore + * @see #getProof **/ public Status check() { diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index dd556d71e..c92432ad3 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -27,8 +27,6 @@ public class Sort extends AST { /** * Equality operator for objects of type Sort. - * @param o - * @return **/ @Override public boolean equals(Object o) @@ -139,10 +137,10 @@ public class Sort extends AST return new FPSort(ctx, obj); case Z3_ROUNDING_MODE_SORT: return new FPRMSort(ctx, obj); - case Z3_SEQ_SORT: - return new SeqSort(ctx, obj); - case Z3_RE_SORT: - return new ReSort(ctx, obj); + case Z3_SEQ_SORT: + return new SeqSort(ctx, obj); + case Z3_RE_SORT: + return new ReSort(ctx, obj); default: throw new Z3Exception("Unknown sort kind"); }