docs: update documentation

dlinear/libs/libgmp.h

@@ -86,8 +86,7 @@ inline mpq_t &to_mpq_t(mpq_class &cla) { return *reinterpret_cast<mpq_t *>(cla.g
  * Cast a mpq_t to a mpq_class.
  *
  * This works because the internal representation of a mpq_class is exactly
- * the same as that of a mpq_t (and, because we only take a reference, no
- * constructor or destructor is ever called).
+ * the same as that of a mpq_t (and, because we only take a reference, no constructor or destructor is ever called).
  * @param mpq mpq_t to cast
  * @return mpq_class reference
  */
@@ -97,18 +96,17 @@ inline const mpq_class &to_mpq_class(const mpq_t &mpq) { return reinterpret_cast
  * Cast a mpq_t to a mpq_class.
  *
  * This works because the internal representation of a mpq_class is exactly
- * the same as that of a mpq_t (and, because we only take a reference, no
- * constructor or destructor is ever called).
+ * the same as that of a mpq_t (and, because we only take a reference, no constructor or destructor is ever called).
  * @param mpq mpq_t to cast
  * @return mpq_class reference
  */
 inline mpq_class &to_mpq_class(mpq_t &mpq) { return reinterpret_cast<mpq_class &>(mpq); }  // NOLINT
 
 /**
  * Check if the char is either a digit or a plus/minus sign.
- * @param c The char to check.
- * @return True if the char is a digit or a plus/minus sign.
- * @return False otherwise.
+ * @param c The char to check
+ * @return true if the char is a digit or a plus/minus sign
+ * @return false if the char is not a digit or a plus/minus sign
  */
 inline bool is_digit_or_sign(char c) { return std::isdigit(c) || c == '+' || c == '-'; }
 

dlinear/libs/libqsopt_ex.h

@@ -67,7 +67,6 @@ class MpqArray {
  public:
   /**
    * Construct a new MpqArray object, allocating the array with @p nElements elements.
-   *
    * @param nElements The number of elements in the array.
    */
   explicit MpqArray(size_t nElements);
@@ -79,14 +78,12 @@ class MpqArray {
   ~MpqArray();
   /**
    * Obtain a constant pointer to the internal array.
-   *
    * @return internal mpq_t array as a constant pointer
    */
   explicit operator const mpq_t *() const { return array; }
 
   /**
    * Obtain a pointer to the internal array.
-   *
    * @return internal mpq_t array
    */
   explicit operator mpq_t *() { return array; }
@@ -95,6 +92,7 @@ class MpqArray {
 
   const mpq_t &operator[](const int idx) const { return array[idx]; }
 
+  /** @getter{size, array} */
   [[nodiscard]] size_t size() const { return array ? reinterpret_cast<size_t *>(array)[-1] : 0; }
 
   /**

dlinear/parser/Driver.h

@@ -153,6 +153,12 @@ class Driver {
   [[nodiscard]] const Stats &stats() const { return stats_; }
 
  protected:
+  /**
+   * Parse the stream.
+   * @param in input stream
+   * @return true if successfully parsed
+   * @return false if an error occurred
+   */
   virtual bool ParseStreamCore(std::istream &in) = 0;
 
   std::string stream_name_;  ///< The name of the stream being parsed.

dlinear/parser/mps/BoundType.cpp

@@ -16,6 +16,7 @@ BoundType ParseBoundType(const std::string& bound_type) { return ParseBoundType(
 
 BoundType ParseBoundType(const char bound_type[]) {
   while (*bound_type == ' ') ++bound_type;
+  DLINEAR_ASSERT(strlen(bound_type) == 2, "Bound type must be exactly 2 characters long");
   if (bound_type[2] != '\0' && bound_type[2] != ' ') DLINEAR_RUNTIME_ERROR_FMT("Invalid bound type: '{}'", bound_type);
   if ((bound_type[0] == 'l' || bound_type[0] == 'L') && (bound_type[1] == 'o' || bound_type[1] == 'O')) {
     return BoundType::LO;

dlinear/parser/mps/BoundType.h

@@ -71,7 +71,7 @@ BoundType ParseBoundType(const std::string &bound_type);
  *
  * Any leading or trailing spaces are ignored.
  * The input is case-insensitive.
- *
+ * @pre The input must be exactly 2 characters long.
  * @param bound_type C-string representation of the bound type
  * @return corresponding bound type
  */

dlinear/parser/mps/Driver.h

@@ -187,16 +187,30 @@ class MpsDriver : public Driver {
    */
   void End();
 
+  /** @getter{problem_name, MpsDriver} */
   [[nodiscard]] const std::string &problem_name() const { return problem_name_; }
+  /** @getsetter{problem_name, MpsDriver} */
   std::string &m_problem_name() { return problem_name_; }
+  /** @checker{enabled, strict mps} */
   [[nodiscard]] bool strict_mps() const { return strict_mps_; }
+  /**
+   * Set the strict mps mode.
+   * @param b new value of the strict mps mode
+   */
   void set_strict_mps(bool b) { strict_mps_ = b; }
+  /** @getter{number of assertions, MpsDriver} */
   [[nodiscard]] std::size_t n_assertions() const { return rhs_.size() + bounds_.size(); }
+  /** @checker{enabled, minimization} */
   [[nodiscard]] bool is_min() const { return is_min_; }
+  /** @getter{objective row name, MpsDriver} */
   [[nodiscard]] const std::string &obj_row() const { return obj_row_; }
+  /** @getter{scanner, MpsDriver} */
+  [[nodiscard]] MpsScanner *scanner() { return scanner_; }
 
-  MpsScanner *scanner() { return scanner_; }
-
+  /**
+   * Print the problem in the smt2 format.
+   * @param os output stream
+   */
   void ToSmt2(std::ostream &os) const;
 
  private:

dlinear/parser/mps/Sense.h

@@ -37,7 +37,6 @@ enum class Sense {
  *
  * Any leading or trailing spaces are ignored.
  * The input is case-insensitive.
- *
  * @param sense string representation of the sense
  * @return corresponding sense
  */
@@ -52,7 +51,6 @@ Sense ParseSense(const std::string &sense);
  *
  * Any leading or trailing spaces are ignored.
  * The input is case-insensitive.
- *
  * @param sense C-style string representation of the sense
  * @return corresponding sense
  */
@@ -66,7 +64,6 @@ Sense ParseSense(const char sense[]);
  * - 'N'
  *
  * The input is case-insensitive.
- *
  * @param sense character representation of the sense
  * @return corresponding sense
  */

dlinear/solver/Bound.h

@@ -14,7 +14,13 @@
 
 namespace dlinear {
 
-/** Bound. It is a tuple of value, bound type and index */
+/**
+ * Tuple containing the value, bound type and theory literal associated with the bound.
+ *
+ * It may also contain an explanation for the existence of the bound used to produce an explanation.
+ * @note For efficiency purposes, the value is just a pointer to the actual value.
+ * Therefore, it is important to ensure that the value is not deallocated while the bound is in use.
+ */
 struct Bound {
   Bound() = default;
   Bound(const mpq_class* value_, LpColBound lp_bound_, Literal theory_literal_, LiteralSet explanation_)

dlinear/solver/BoundPreprocessor.h

@@ -39,21 +39,112 @@ class BoundPreprocessor {
   using Explanations = std::set<LiteralSet>;
   using VarToEqBinomialMap = std::unordered_map<Variable, mpq_class>;
 
+  /**
+   * Construct a new Bound Preprocessor object using the @p predicate_abstractor.
+   * @param predicate_abstractor predicate abstractor containing the map between the variables and the literals
+   */
   explicit BoundPreprocessor(const PredicateAbstractor& predicate_abstractor);
 
+  /**
+   * Add a theory variable to the preprocessor.
+   *
+   * It will create a new entry in the theory_bounds_ map.
+   * @param var theory variable to add
+   */
   void AddVariable(const Variable& var);
 
+  /**
+   * Preprocess all the @p enabled_literals.
+   *
+   * It will enable the literals and propagate the bounds.
+   * If a conflict is detected, it will return the set of explanations.
+   * Enabled literals are cached and will not be enabled again in the future.
+   * @param enabled_literals literals to enable
+   * @return set of explanations from the enabled literals if a conflict is detected
+   * @return empty set if no conflict is detected
+   */
   std::set<LiteralSet> EnableLiterals(const std::vector<Literal>& enabled_literals);
+  /**
+   * Preprocess all the @p enabled_literals.
+   *
+   * It will enable the literals and propagate the bounds.
+   * If a conflict is detected, it will return the set of explanations.
+   * Enabled literals are cached and will not be enabled again in the future.
+   * @param enabled_literals literals to enable
+   * @param[out] explanations set of explanations from the enabled literals if a conflict is detected
+   */
   void EnableLiterals(const std::vector<Literal>& enabled_literals, std::set<LiteralSet>& explanation);
 
+  /**
+   * Enable the literal @p lit.
+   *
+   * It will enable the literal and propagate the bounds.
+   * If a conflict is detected, it will return the set of explanations.
+   * Enabled literals are cached and will not be enabled again in the future.
+   * @param lit literal to enable
+   * @return set of explanations from the enabled literal if a conflict is detected
+   * @return empty set if no conflict is detected
+   */
   std::set<LiteralSet> EnableLiteral(const Literal& lit);
+  /**
+   * Enable the literal @p lit.
+   *
+   * It will enable the literal and propagate the bounds.
+   * If a conflict is detected, it will return the set of explanations.
+   * Enabled literals are cached and will not be enabled again in the future.
+   * @param lit literal to enable
+   * @param[out] explanations set of explanations from the enabled literal if a conflict is detected
+   */
   void EnableLiteral(const Literal& lit, std::set<LiteralSet>& explanations);
 
+  /**
+   * Process all enabled literals.
+   *
+   * It will process the enabled literals and propagate the bounds.
+   * The bounds are propagated based on the BoundPropagationType and the formulae will be evaluated.
+   * If a conflict is detected, it will return the set of explanations.
+   * @return set of explanations from the enabled literals if a conflict is detected
+   * @return empty set if no conflict is detected
+   */
   Explanations Process();
+  /**
+   * Process all enabled literals.
+   *
+   * It will process the enabled literals and propagate the bounds.
+   * The bounds are propagated based on the BoundPropagationType and the formulae will be evaluated.
+   * If a conflict is detected, it will return the set of explanations.
+   * @param[out] explanations set of explanations from the enabled literals if a conflict is detected
+   */
   void Process(Explanations& explanations);
+  /**
+   * Process the enabled literals @p enabled_literals.
+   *
+   * It will process the enabled literals and propagate the bounds.
+   * The bounds are propagated based on the BoundPropagationType and the formulae will be evaluated.
+   * If a conflict is detected, it will return the set of explanations.
+   * @param enabled_literals literals to enable
+   * @return set of explanations from the enabled literals if a conflict is detected
+   * @return empty set if no conflict is detected
+   */
   Explanations Process(const LiteralSet& enabled_literals);
+  /**
+   * Process the enabled literals @p enabled_literals.
+   *
+   * It will process the enabled literals and propagate the bounds.
+   * The bounds are propagated based on the BoundPropagationType and the formulae will be evaluated.
+   * If a conflict is detected, it will return the set of explanations.
+   * @param enabled_literals literals to enable
+   * @param[out] explanations set of explanations from the enabled literals if a conflict is detected
+   */
   void Process(const LiteralSet& enabled_literals, Explanations& explanations);
 
+  /**
+   * Get the active explanation for the variable @p var.
+   *
+   * It will return the explanation for the variable @p var, justifying the active bounds.
+   * @param var variable to get the explanation for
+   * @param[out] explanation explanation for the variable @p var
+   */
   void GetActiveExplanation(const Variable& var, LiteralSet& explanation);
 
   /**
@@ -66,7 +157,19 @@ class BoundPreprocessor {
    */
   void SetInfinityBounds(const Variable& var, const mpq_class& lb, const mpq_class& ub);
 
+  /**
+   * Clear the preprocessor.
+   *
+   * It will clear the environment, the theory bounds, and the enabled literals.
+   */
   void Clear();
+  /**
+   * Clear the preprocessor using the @p fixed_preprocessor.
+   *
+   * It will clear the environment, the theory bounds, and the enabled literals by copying the values from the
+   * @p fixed_preprocessor.
+   * @param fixed_preprocessor preprocessor to use as a reference
+   */
   void Clear(const BoundPreprocessor& fixed_preprocessor);
 
   /** @getter{configuration, BoundPreprocessor} */

dlinear/solver/CadicalSatSolver.h

@@ -57,8 +57,8 @@ class CadicalSatSolver : public SatSolver {
  private:
   [[nodiscard]] std::set<int> GetMainActiveLiterals() override;
 
-  CaDiCaL::Solver sat_{};
-  int next_var_id_{1};
+  CaDiCaL::Solver sat_{}; ///< SAT solver
+  int next_var_id_{1};   ///< Next variable id
 };
 
 }  // namespace dlinear

dlinear/solver/ContextImpl.cpp

@@ -69,8 +69,8 @@ Context::Impl::Impl(Config &config, SmtSolverOutput *const output)
 }
 
 void Context::Impl::Assert(const Formula &f) {
-  if (is_true(f)) return;     // Skip trivially true assertions.
-  if (is_false(f)) {          // The formula is false. No point in adding it to the SAT solver. There is no point in continuing
+  if (is_true(f)) return;  // Skip trivially true assertions.
+  if (is_false(f)) {  // The formula is false. No point in adding it to the SAT solver. There is no point in continuing
     stack_.push_back(f);
     return;
   }

docs/Installation.md

@@ -60,7 +60,7 @@ sudo dpkg -i bazel-bin/dlinear/dlinear.deb
 
 ```bash
 # Add the PPA
-sudo add-apt-repository ppa:dlinear/dlinear
+sudo add-apt-repository ppa:tendto/dlinear
 # Update the package list
 sudo apt update
 # Install dlinear

docs/Theory.md

@@ -41,8 +41,8 @@ The fundamental property is that the new formula is satisfiable if and only if t
 
 The transformation uses three basic operators:
 
-| Original    | $ p \iff \text{formula} $                             | In CNF                                                                    |
-| ----------- | ----------------------------------------------------- | ------------------------------------------------------------------------- |
+| Original    | $ p \iff \text{formula} $                                           | In CNF                                                                    |
+| ----------- | ------------------------------------------------------------------- | ------------------------------------------------------------------------- |
 | $\neg a$    | $(\neg a \Longrightarrow p) \land (p \Longrightarrow \neg a)$       | $(a \lor p) \land (\neg a \lor \neg p)$                                   |
 | $a \land b$ | $(a \land b \Longrightarrow p) \land (p \Longrightarrow a \land b)$ | $(\neg a \lor \neg b \lor p) \land (a \lor \neg p) \land (b \lor \neg p)$ |
 | $a \lor b$  | $(a \lor b \Longrightarrow p) \land (p \Longrightarrow a \lor b)$   | $(a \lor b \lor \neg p) \land (\neg a \lor p) \land (\neg b \lor p)$      |

docs/Todo.md

@@ -31,7 +31,7 @@
     - [ ] Use Ubuntu 23.04+ for gcc 13+ support
 - [ ] Return multiple explanations instead of just one when dealing with active constraints
 - [ ] Improve iterations over nq bounds
-- [x] Add symbolic preprocessor for constraints in the form of $x \lessgtr y$
+- [x] Add symbolic preprocessor for constraints in the form of $x <> y$
 - [ ] Remove completely free variables, especially from nq constraints
 - [ ] Investigate out of memory
 - [x] Handle conflicting constraints in preprocessor