docs: update docstring removing @brief

benchmark/BenchmarkProgram.h

@@ -17,15 +17,16 @@ namespace dlinear::benchmark {
 class BenchmarkProgram {
  public:
   /**
-   * @brief Create an instance of a BenchmarkProgram.
+   * Create an instance of a BenchmarkProgram.
+   * 
    * The object can than be used to run the benchmarks.
    * @param argc number of command line arguments. Passed by the main function
    * @param argv array of command line arguments. Passed by the main function
    */
   BenchmarkProgram(int argc, const char *argv[]);
 
   /**
-   * @brief Run the benchmarks.
+   * Run the benchmarks.
    * @return exit status
    */
   int Run();

benchmark/main.cpp

@@ -3,11 +3,12 @@
  * @author dlinear
  * @date 28 Aug 2023
  * @copyright 2023 dlinear
- * @brief Brief description
+ * @brief Main entry point for the benchmark program.
  *
- * Long Description
+ * The main function is used to start the benchmark program.
  */
 #include <csignal>
+
 #include "benchmark/BenchmarkProgram.h"
 
 using dlinear::benchmark::BenchmarkProgram;

benchmark/util/BenchArgParser.h

@@ -35,7 +35,7 @@ class BenchArgParser {
   void validateOptions();
 
   /**
-   * @brief Load all the files found in the path parameter matching the provided
+   * Load all the files found in the path parameter matching the provided
    * fileExtension and return them as a vector of strings.
    * @return vector of strings containing the files found in the path parameter
    */

benchmark/util/ConfigFileReader.cpp

@@ -3,9 +3,6 @@
  * @author dlinear
  * @date 28 Aug 2023
  * @copyright 2023 dlinear
- * @brief Brief description
- *
- * Long Description
  */
 
 #include "ConfigFileReader.h"

dlinear/solver/CompleteSoplexTheorySolver.h

@@ -58,7 +58,7 @@ class CompleteSoplexTheorySolver : public SoplexTheorySolver {
    *
    * It invokes the LP solver and returns the result, as well as the actual precision of the solution, if any.
    * If the LP problem is infeasible (or strictly infeasible), it will also update the explanation
-   * @link theory_rows_to_explanation_ @endlink.
+   * @ref theory_rows_to_explanation_.
    * @param actual_precision The actual precision of the solution, if any. Starts from the input, and is updated if the
    * LP solver returns a better precision
    * @return The result of the SAT check
@@ -120,7 +120,7 @@ class CompleteSoplexTheorySolver : public SoplexTheorySolver {
   std::vector<size_t> IteratorNqRowsInExplanation() const;
 
   /**
-   * Get the explanation from @link theory_rows_to_explanation_ @endlink.
+   * Get the explanation from @ref theory_rows_to_explanation_.
    * @param[out] explanation The explanation to be updated
    */
   void GetExplanation(LiteralSet& explanation);

dlinear/solver/Context.h

@@ -28,7 +28,7 @@
 namespace dlinear {
 
 /**
- * @brief Context class that holds a set of constraints and provide
+ * Context class that holds a set of constraints and provide
  * Assert/Push/Pop/CheckSat functionalities.
  *
  * @note The implementation details are in context_impl.h file.

dlinear/solver/SatSolver.h

@@ -75,34 +75,31 @@ class SatSolver {
   virtual void AddLearnedClause(const LiteralSet &literals) = 0;
   /**
    * Check the satisfiability of the current configuration.
-   *
    * @return a witness, satisfying model if the problem is SAT.
    * @return empty optional if UNSAT
    */
   virtual std::optional<Model> CheckSat() = 0;
   /**
    * Get the list of Literal which correspond to a theory literal that have been inserted into the SAT solver.
-   *
    * @return vector of literals
    */
   const std::vector<Literal> &theory_literals() const { return theory_literals_; }
 
  protected:
   /**
    * Add a clause @p f to the internal SAT solver.
-   * @p f must be a clause. That is, it is either a literal (b or ¬b)
+   * @pre @p f must be a clause. That is, it is either a literal (b or ¬b)
    * or a disjunction of literals (l₁ ∨ ... ∨ lₙ).
-   *
    * @param f clause to add
    */
   virtual void AddClauseToSat(const Formula &f) = 0;
   /**
    * Add a variable to the internal SAT solver.
+   *
    * Also update the two mapping between each symbolic Variable and the
    * internal SAT solver's variable (@ref var_to_sat_) and the other way around
    * (@ref sat_to_var_).
    * If the variable had already been mapped, this function does nothing.
-   *
    * @param var variable to add
    */
   virtual void MakeSatVar(const Variable &var) = 0;

dlinear/solver/SoplexTheorySolver.h

@@ -128,7 +128,7 @@ class SoplexTheorySolver : public TheorySolver {
   /**
    * Parse a row and return the vector of coefficients to apply to the decisional variables.
    *
-   * Parse an formula representing a row in order to produce store the rhs term in @link spx_rhs_ @endlink and create a
+   * Parse an formula representing a row in order to produce store the rhs term in @ref spx_rhs_ and create a
    * vector of coefficients for the row to pass to the LP solver
    * @param formula symbolic formula representing the row
    * @return vector of coefficients to apply to the decisional variables in the row
@@ -143,11 +143,10 @@ class SoplexTheorySolver : public TheorySolver {
   void SetSPXVarCoeff(soplex::DSVectorRational& coeffs, const Variable& var, const mpq_class& value) const;
   void CreateArtificials(int spx_row);
 
-  // Exact LP solver (SoPlex)
-  soplex::SoPlex spx_;
+  soplex::SoPlex spx_;  ///< SoPlex exact LP solver
 
-  std::vector<mpq_class> spx_rhs_;
-  std::vector<LpRowSense> spx_sense_;
+  std::vector<mpq_class> spx_rhs_;     ///< Right-hand side of the rows
+  std::vector<LpRowSense> spx_sense_;  ///< Sense of the rows
 };
 
 }  // namespace dlinear

dlinear/solver/TheorySolverBoundIterator.h

@@ -5,7 +5,7 @@
  * @licence Apache-2.0 license
  * @brief TheorySolverBoundIterator class.
  *
- * It is used to iterate over the bounds of a theory solver without copying each @ref TheorySolverBoundVector::Bound.
+ * It is used to iterate over the bounds of a theory solver without copying each @ref dlinear::TheorySolverBoundVector::Bound.
  * Usually the results of bound violation.
  */
 #pragma once
@@ -57,7 +57,7 @@ class TheorySolverBoundIterator {
    */
   TheorySolverBoundIterator(internal_iterator begin_bounds_it, internal_iterator end_bounds_it);
   /**
-   * @brief Construct an iterator from a pair of iterators, @p bounds.
+   * Construct an iterator from a pair of iterators, @p bounds.
    * @param bounds pair of iterators to the bounds, begin and end
    */
   explicit TheorySolverBoundIterator(std::pair<internal_iterator, internal_iterator> bounds);

dlinear/solver/TheorySolverBoundVector.h

@@ -119,22 +119,22 @@ class TheorySolverBoundVector {
   /**
    * Clear the vector and reset the active bounds.
    *
-   * Active bounds are set to @link inf_l_ @endlink and @link inf_u_ @endlink.
+   * Active bounds are set to @ref inf_l_ and @ref inf_u_.
    */
   void Clear();
   /**
-   * Clear the vector, update @link inf_l_ @endlink and @link inf_u_ @endlink and reset the active bounds.
+   * Clear the vector, update @ref inf_l_ and @ref inf_u_ and reset the active bounds.
    *
-   * More specifically, @link inf_l_ @endlink and @link inf_u_ @endlink are set to -@p inf and @p inf respectively.
-   * Active bounds are set to the new values of @link inf_l_ @endlink and @link inf_u_ @endlink.
+   * More specifically, @ref inf_l_ and @ref inf_u_ are set to -@p inf and @p inf respectively.
+   * Active bounds are set to the new values of @ref inf_l_ and @ref inf_u_.
    * @param inf new inf value
    */
   void Clear(mpq_class inf);
   /**
-   * Clear the vector, update @link inf_l_ @endlink and @link inf_u_ @endlink and reset the active bounds.
+   * Clear the vector, update @ref inf_l_ and @ref inf_u_ and reset the active bounds.
    *
-   * More specifically, @link inf_l_ @endlink and @link inf_u_ @endlink are set to @p inf_l and @p inf_u respectively.
-   * Active bounds are set to the new values of @link inf_l_ @endlink and @link inf_u_ @endlink.
+   * More specifically, @ref inf_l_ and @ref inf_u_ are set to @p inf_l and @p inf_u respectively.
+   * Active bounds are set to the new values of @ref inf_l_ and @ref inf_u_.
    * @param inf_l new lower bound
    * @param inf_u new upper bound
    */
@@ -249,7 +249,7 @@ class TheorySolverBoundVector {
 
  private:
   /**
-   * Return an iterator over @link bounds_ @endlink after the last lower bound and to the first upper bound.
+   * Return an iterator over @ref bounds_ after the last lower bound and to the first upper bound.
    * @return iterator after the last lower bound and to the first upper bound
    */
   [[nodiscard]] inline BoundVector::const_iterator LowerBoundEnd() const { return bounds_.cbegin() + n_lower_bounds_; }

dlinear/symbolic/NaiveCnfizer.cpp

@@ -3,9 +3,6 @@
  * @author dlinear
  * @date 18 Aug 2023
  * @copyright 2023 dlinear
- * @brief Brief description
- *
- * Long Description
  */
 
 #include "NaiveCnfizer.h"

dlinear/symbolic/Nnfizer.h

@@ -23,7 +23,7 @@ namespace dlinear {
  * When @code push_negation_into_relationals @endcode is true, it pushed
  * negations into relational formulas by flipping relational
  * @par Example:
- *   @f$ ¬(x >= 10) @f$ becomes @f$ (x < 10) @f$.
+ *   @f$ ¬(x \ge 10) @f$ becomes @f$ (x < 10) @f$
  *
  * @see https://en.wikipedia.org/wiki/Negation_normal_form
  */

dlinear/symbolic/PredicateAbstractor.cpp

@@ -3,9 +3,6 @@
  * @author dlinear
  * @date 17 Aug 2023
  * @copyright 2023 dlinear
- * @brief Brief description
- *
- * Long Description
  */
 
 #include "PredicateAbstractor.h"

dlinear/util/Box.h

@@ -217,7 +217,7 @@ class Box {
   [[nodiscard]] std::pair<Box, Box> bisect_int(int i) const;
 
   /**
-   * @brief Bisects the box at @p i -th dimension.
+   * Bisects the box at @p i -th dimension.
    * @pre @p i-th variable is bisectable.
    * @pre @p i-th variable is of continuous type.
    * @param i index of the dimension to bisect

dlinear/util/SortedVector.hpp

@@ -357,9 +357,9 @@ class SortedVector {
 
  private:
   /**
-   * Use the @link compare_ @endlink function to check if two elements are equal.
+   * Use the @ref compare_ function to check if two elements are equal.
    *
-   * Since the function only checks ordering, to make sure two elements are equal @link compare_ @endlink must be used twice.
+   * Since the function only checks ordering, to make sure two elements are equal @ref compare_ must be used twice.
    * @param lhs left-hand side element
    * @param rhs right-hand side element
    * @return true if the elements are equal

dlinear/util/Stats.h

@@ -48,13 +48,13 @@ class Stats {
    */
   [[nodiscard]] const Timer &timer() const { return timer_; }
   /**
-   * @brief Convert the current state of the object to a formatted string, only including the specific
+   * Convert the current state of the object to a formatted string, only including the specific
    * part the Stat object is concerned about
    * @return string representing a partial state of the Stats
    */
   [[nodiscard]] virtual std::string ToSegmentString() const;
   /**
-   * @brief Convert the current state of the object to a formatted string
+   * Convert the current state of the object to a formatted string
    * @return string representing the state of the Stats
    */
   [[nodiscard]] virtual std::string ToString() const;

dlinear/util/Timer.cpp

@@ -3,7 +3,6 @@
  * @author dlinear
  * @date 16 Aug 2023
  * @copyright 2023 dlinear
- * @brief Brief description
  */
 
 #include "Timer.h"

dlinear/util/filesystem.cpp

@@ -3,9 +3,6 @@
  * @author dlinear
  * @date 15 Aug 2023
  * @copyright 2023 dlinear
- * @brief Brief description
- *
- * Long Description
  */
 
 #include "filesystem.h"

dlinear/util/interrupt.h

@@ -15,7 +15,7 @@ extern volatile std::atomic_bool g_interrupted;  ///< Flag to indicate an interr
 
 /**
  * Signal handler for SIGINT.
- * Set the @link g_interrupted @endlink flag to true.
+ * Set the @ref g_interrupted flag to true.
  */
 void interrupt_handler(int);
 

docs/Doxyfile

@@ -209,7 +209,7 @@ SHORT_NAMES            = NO
 # description.)
 # The default value is: NO.
 
-JAVADOC_AUTOBRIEF      = NO
+JAVADOC_AUTOBRIEF      = YES
 
 # If the JAVADOC_BANNER tag is set to YES then doxygen will interpret a line
 # such as

docs/presentation/examples/gauss/main.cpp

@@ -89,7 +89,7 @@ class GaussBenchmark {
 };
 
 /**
- * @brief Usage:
+ * Usage:
  * ./gauss [size] [seed] [output_file] [diff_file]
  */
 int main(int argc, char const* argv[]) {