From 9cb5726a3a26c329ef5310b0b461b03dd0864799 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 29 Sep 2021 15:06:36 -0700
Subject: [PATCH] [API] Update comments w.r.t. SymFPU, fix typos (#7263)

Previously, SymFPU was an optional dependency but it is now required.
The comments in the API were not updated to reflect that. This commit
fixes the comments.
---
 src/api/cpp/cvc5.h | 32 +++++++++++++-------------------
 1 file changed, 13 insertions(+), 19 deletions(-)

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 248bb8bda..293e5c270 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -674,7 +674,7 @@ class CVC5_EXPORT Sort
   std::string getUninterpretedSortName() const;
 
   /**
-   * @return true if an uninterpreted sort is parameterezied
+   * @return true if an uninterpreted sort is parameterized
    */
   bool isUninterpretedSortParameterized() const;
 
@@ -771,7 +771,7 @@ class CVC5_EXPORT Sort
   const Solver* d_solver;
 
   /**
-   * The interal type wrapped by this sort.
+   * The internal type wrapped by this sort.
    * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
    *       to memory allocation (cvc5::Type is already ref counted, so this
    *       could be a unique_ptr instead).
@@ -1085,7 +1085,7 @@ class CVC5_EXPORT Term
   Term substitute(const Term& term, const Term& replacement) const;
 
   /**
-   * @return the result of simulatenously replacing 'terms' by 'replacements'
+   * @return the result of simultaneously replacing 'terms' by 'replacements'
    * in this term
    */
   Term substitute(const std::vector<Term>& terms,
@@ -1806,7 +1806,7 @@ class CVC5_EXPORT DatatypeSelector
   Term getSelectorTerm() const;
 
   /**
-   * Get the upater operator of this datatype selector.
+   * Get the updater operator of this datatype selector.
    * @return the updater term
    */
   Term getUpdaterTerm() const;
@@ -3007,7 +3007,7 @@ class CVC5_EXPORT Solver
    * This method is called when the DatatypeDecl objects dtypedecls have been
    * built using "unresolved" sorts.
    *
-   * We associate each sort in unresolvedSorts with exacly one datatype from
+   * We associate each sort in unresolvedSorts with exactly one datatype from
    * dtypedecls. In particular, it must have the same name as exactly one
    * datatype declaration in dtypedecls.
    *
@@ -3024,7 +3024,7 @@ class CVC5_EXPORT Solver
 
   /**
    * Create function sort.
-   * @param domain the sort of the fuction argument
+   * @param domain the sort of the function argument
    * @param codomain the sort of the function return value
    * @return the function sort
    */
@@ -3448,8 +3448,7 @@ class CVC5_EXPORT Solver
   Term mkConstArray(const Sort& sort, const Term& val) const;
 
   /**
-   * Create a positive infinity floating-point constant. Requires cvc5 to be
-   * compiled with SymFPU support.
+   * Create a positive infinity floating-point constant.
    * @param exp Number of bits in the exponent
    * @param sig Number of bits in the significand
    * @return the floating-point constant
@@ -3457,8 +3456,7 @@ class CVC5_EXPORT Solver
   Term mkPosInf(uint32_t exp, uint32_t sig) const;
 
   /**
-   * Create a negative infinity floating-point constant. Requires cvc5 to be
-   * compiled with SymFPU support.
+   * Create a negative infinity floating-point constant.
    * @param exp Number of bits in the exponent
    * @param sig Number of bits in the significand
    * @return the floating-point constant
@@ -3466,8 +3464,7 @@ class CVC5_EXPORT Solver
   Term mkNegInf(uint32_t exp, uint32_t sig) const;
 
   /**
-   * Create a not-a-number (NaN) floating-point constant. Requires cvc5 to be
-   * compiled with SymFPU support.
+   * Create a not-a-number (NaN) floating-point constant.
    * @param exp Number of bits in the exponent
    * @param sig Number of bits in the significand
    * @return the floating-point constant
@@ -3475,8 +3472,7 @@ class CVC5_EXPORT Solver
   Term mkNaN(uint32_t exp, uint32_t sig) const;
 
   /**
-   * Create a positive zero (+0.0) floating-point constant. Requires cvc5 to be
-   * compiled with SymFPU support.
+   * Create a positive zero (+0.0) floating-point constant.
    * @param exp Number of bits in the exponent
    * @param sig Number of bits in the significand
    * @return the floating-point constant
@@ -3484,8 +3480,7 @@ class CVC5_EXPORT Solver
   Term mkPosZero(uint32_t exp, uint32_t sig) const;
 
   /**
-   * Create a negative zero (-0.0) floating-point constant. Requires cvc5 to be
-   * compiled with SymFPU support.
+   * Create a negative zero (-0.0) floating-point constant.
    * @param exp Number of bits in the exponent
    * @param sig Number of bits in the significand
    * @return the floating-point constant
@@ -3520,8 +3515,7 @@ class CVC5_EXPORT Solver
   Term mkAbstractValue(uint64_t index) const;
 
   /**
-   * Create a floating-point constant (requires cvc5 to be compiled with symFPU
-   * support).
+   * Create a floating-point constant.
    * @param exp Size of the exponent
    * @param sig Size of the significand
    * @param val Value of the floating-point constant as a bit-vector term
@@ -3912,7 +3906,7 @@ class CVC5_EXPORT Solver
    * ( get-proof )
    * \endverbatim
    * Requires to enable option 'produce-proofs'.
-   * @return a string representing the proof, according to the the value of
+   * @return a string representing the proof, according to the value of
    * proof-format-mode.
    */
   std::string getProof() const;
-- 
2.30.2