From 3c94083a233054f7fe8db5073a5071561252afae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 1 Jul 2022 15:29:36 -0700 Subject: [PATCH] fix doc errors Signed-off-by: Nikolaj Bjorner --- doc/website.dox.in | 4 ++-- src/api/dotnet/Context.cs | 8 ++++---- src/api/java/Context.java | 32 ++++++++++++++++---------------- src/api/java/Model.java | 2 +- src/api/java/Quantifier.java | 6 ++++++ src/api/z3_api.h | 4 ++-- 6 files changed, 31 insertions(+), 25 deletions(-) diff --git a/doc/website.dox.in b/doc/website.dox.in index 5d084550c..de5feb685 100644 --- a/doc/website.dox.in +++ b/doc/website.dox.in @@ -8,6 +8,6 @@ This website hosts the automatically generated documentation for the Z3 APIs. - - \ref @C_API@ - - \ref @CPP_API@ @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ @JS_API@ + - \ref @C_API@ + - \ref @CPP_API@ @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ @JS_API@ */ diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index c71289d4d..764beb470 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -4620,16 +4620,16 @@ namespace Microsoft.Z3 /// /// /// Produces a term that represents the conversion of the floating-point term t into a - /// bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, + /// bit-vector term of size sz in 2's complement format (signed when sign==true). If necessary, /// the result will be rounded according to rounding mode rm. /// /// RoundingMode term. /// FloatingPoint term /// Size of the resulting bit-vector. - /// Indicates whether the result is a signed or unsigned bit-vector. - public BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool signed) + /// Indicates whether the result is a signed or unsigned bit-vector. + public BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool sign) { - if (signed) + if (sign) return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz)); else return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz)); diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 7b5f8a936..4582439ec 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -1717,8 +1717,8 @@ public class Context implements AutoCloseable { * {@code [domain -> range]}, and {@code i} must have the sort * {@code domain}. The sort of the result is {@code range}. * - * @see #mkArraySort(Sort[], Sort) - * @see #mkStore + * @see #mkArraySort(Sort[], R) + * @see #mkStore(Expr> a, Expr i, Expr v) **/ public Expr mkSelect(Expr> a, Expr i) { @@ -1739,8 +1739,8 @@ public class Context implements AutoCloseable { * {@code [domains -> range]}, and {@code args} must have the sorts * {@code domains}. The sort of the result is {@code range}. * - * @see #mkArraySort(Sort[], Sort) - * @see #mkStore + * @see #mkArraySort(Sort[], R) + * @see #mkStore(Expr> a, Expr i, Expr v) **/ public Expr mkSelect(Expr> a, Expr[] args) { @@ -1763,8 +1763,8 @@ public class Context implements AutoCloseable { * {@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(Sort[], Sort) - * @see #mkSelect + * @see #mkArraySort(Sort[], R) + * @see #mkSelect(Expr> a, Expr i) **/ public ArrayExpr mkStore(Expr> a, Expr i, Expr v) @@ -1788,8 +1788,8 @@ public class Context implements AutoCloseable { * {@code select}) on all indices except for {@code args}, where it * maps to {@code v} (and the {@code select} of {@code a} * with respect to {@code args} may be a different value). - * @see #mkArraySort(Sort[], Sort) - * @see #mkSelect + * @see #mkArraySort(Sort[], R) + * @see #mkSelect(Expr> a, Expr i) **/ public ArrayExpr mkStore(Expr> a, Expr[] args, Expr v) @@ -1806,8 +1806,8 @@ public class Context implements AutoCloseable { * Remarks: The resulting term is an array, such * that a {@code select} on an arbitrary index produces the value * {@code v}. - * @see #mkArraySort(Sort[], Sort) - * @see #mkSelect + * @see #mkArraySort(Sort[], R) + * @see #mkSelect(Expr> a, Expr i) * **/ public ArrayExpr mkConstArray(D domain, Expr v) @@ -1826,9 +1826,9 @@ public class Context implements AutoCloseable { * {@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(Sort[], Sort) - * @see #mkSelect - * @see #mkStore + * @see #mkArraySort(Sort[], R) + * @see #mkSelect(Expr> a, Expr i) + * @see #mkStore(Expr> a, Expr i, Expr v) **/ @SafeVarargs @@ -2476,7 +2476,7 @@ public class Context implements AutoCloseable { * * @return A Term with value {@code num}/{@code den} * and sort Real - * @see #mkNumeral(String,Sort) + * @see #mkNumeral(String v, R ty) **/ public RatNum mkReal(int num, int den) { @@ -2612,7 +2612,7 @@ public class Context implements AutoCloseable { * '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 {#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 @@ -2707,7 +2707,7 @@ public class Context implements AutoCloseable { * with the sorts of the bound variables, {@code names} is an array with the * 'names' of the bound variables, and {@code body} is the body of the * lambda. - * Note that the bound variables are de-Bruijn indices created using {@link #mkBound} + * Note that the bound variables are de-Bruijn indices created using {#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 diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 032745fc5..ffc4dd47f 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -242,7 +242,7 @@ public class Model extends Z3Object { * values. We say this finite set is the "universe" of the sort. * * @see #getNumSorts - * @see #getSortUniverse + * @see #getSortUniverse(R s) * * @throws Z3Exception **/ diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index 89ff61a3d..efeac9bb5 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -161,6 +161,12 @@ public class Quantifier extends BoolExpr /** * Create a quantified expression. * + * @param ctx Context to create the quantifier on. + * @param isForall Quantifier type. + * @param sorts Sorts of bound variables. + * @param names Names of bound variables + * @param body Body of quantifier + * @param weight Weight used to indicate priority for qunatifier instantiation * @param patterns Nullable patterns * @param noPatterns Nullable noPatterns * @param quantifierID Nullable quantifierID diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 8c60a09d1..dbf8d9252 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6811,7 +6811,7 @@ extern "C" { /** \brief register a callback when a new expression with a registered function is used by the solver - The registered function appears at the top level and is created using \ref Z3_propagate_solver_declare. + The registered function appears at the top level and is created using \ref Z3_solver_propagate_declare. def_API('Z3_solver_propagate_created', VOID, (_in(CONTEXT), _in(SOLVER), _fnptr(Z3_created_eh))) */ @@ -6837,7 +6837,7 @@ extern "C" { /** Create uninterpreted function declaration for the user propagator. When expressions using the function are created by the solver invoke a callback - to \ref \Z3_solver_progate_created with arguments + to \ref \Z3_solver_propagate_created with arguments 1. context and callback solve 2. declared_expr: expression using function that was used as the top-level symbol 3. declared_id: a unique identifier (unique within the current scope) to track the expression.