dos: update docstrings

dlinear/smt2/Driver.h

@@ -129,9 +129,12 @@ class Smt2Driver {
     bool is_var_;
   };
 
-  /// Returns a variable or constant expression associated with a name @p name.
-  ///
-  /// @throws if no variable or constant expression is associated with @p name.
+  /**
+   * Return a variable or constant expression associated with a name @p name.
+   * @param name name of the variable or constant expression
+   * @return the variable or constant expression with name @p name
+   * @throw if no variable or constant expression is associated with @p name
+   */
   const VariableOrConstant &lookup_variable(const std::string &name);
 
   void PushScope() { scope_.push(); }
@@ -153,8 +156,10 @@ class Smt2Driver {
 
   std::string &m_streamname() { return streamname_; }
 
-  /** Pointer to the current scanenr instance, this is used to connect the
-   * parser to the scanner. It is used in the yylex macro. */
+  /**
+   * Pointer to the current scanner instance, this is used to connect the
+   * parser to the scanner. It is used in the yylex macro.
+   */
   Smt2Scanner *scanner() { return scanner_; }
 
  private:

dlinear/solver/CompleteSoplexTheorySolver.cpp

@@ -27,7 +27,9 @@ CompleteSoplexTheorySolver::CompleteSoplexTheorySolver(PredicateAbstractor &pred
       var_to_enabled_theory_rows_{},
       nq_row_to_theory_rows_{},
       last_nq_status_{},
-      theory_rows_to_explanation_{} {}
+      theory_rows_to_explanation_{} {
+  DLINEAR_ASSERT(config.precision() == 0, "CompleteSoplexTheorySolver does not support a positive precision");
+}
 
 void CompleteSoplexTheorySolver::AddVariable(const Variable &var) {
   auto it = var_to_theory_col_.find(var.get_id());
@@ -125,14 +127,14 @@ std::vector<LiteralSet> CompleteSoplexTheorySolver::EnableLiteral(const Literal
 
     // Add the active bound to the LP solver bounds
     int theory_col = var_to_theory_col_[b_var.get_id()];
-    const TheorySolverBoundVector::Violation violation{theory_bounds_[theory_col].AddBound(value, type, spx_row)};
+    const TheorySolverBoundVector::BoundIterator violation{theory_bounds_[theory_col].AddBound(value, type, spx_row)};
 
     // If the bound is invalid, return the explanation and update the SAT solver immediately
     if (violation) return TheoryRowBoundsToExplanations(violation, spx_row);
     return {};
   }
 
-  SetSpxRow(spx_row, truth, formula.GetFreeVariables());
+  EnableSpxRow(spx_row, truth, formula.GetFreeVariables());
   return {};
 }
 
@@ -160,7 +162,7 @@ SatResult CompleteSoplexTheorySolver::CheckSat(const Box &box, mpq_class *actual
   }
 
   // Set the bounds for the variables
-  SetSPXVarBound();
+  EnableSPXVarBound();
 
   // Now we call the solver
   DLINEAR_DEBUG_FMT("CompleteSoplexTheorySolver::CheckSat: calling SoPlex (phase {})", simplex_sat_phase_);
@@ -491,22 +493,22 @@ bool CompleteSoplexTheorySolver::UpdateBitIncrementIteratorBasedOnExplanation(Bi
   return true;
 }
 
-void CompleteSoplexTheorySolver::SetSPXVarBound() {
-  SoplexTheorySolver::SetSPXVarBound();
+void CompleteSoplexTheorySolver::EnableSPXVarBound() {
+  SoplexTheorySolver::EnableSPXVarBound();
   // For all columns...
   for (const auto &theory_bound : theory_bounds_) {
     // ... for each active bound of that column...
-    for (TheorySolverBoundVector::Violation it{theory_bound.active_bounds()}; it; ++it) {
+    for (TheorySolverBoundVector::BoundIterator it{theory_bound.active_bounds()}; it; ++it) {
       const auto &[value, bound, spx_row] = *it;
       // ... if we are dealing with a strict bound, add the strict row to the LP problem
       if (bound == LpColBound::SU || bound == LpColBound::SL || bound == LpColBound::D) {
-        SoplexTheorySolver::SetSpxRow(spx_row);
+        SoplexTheorySolver::EnableSpxRow(spx_row);
       }
     }
   }
 }
 
-void CompleteSoplexTheorySolver::SetSpxRow(int spx_row, bool truth, const Variables &free_vars) {
+void CompleteSoplexTheorySolver::EnableSpxRow(int spx_row, bool truth, const Variables &free_vars) {
   for (const Variable &row_var : free_vars) {
     var_to_enabled_theory_rows_.at(row_var.get_id()).push_back(spx_row);
   }

dlinear/solver/CompleteSoplexTheorySolver.h

@@ -27,6 +27,14 @@
 
 namespace dlinear {
 
+/**
+ * CompleteSoPlexTheorySolver class.
+ *
+ * Complete solver using SoPlex.
+ * The linear is problem exactly, also dealing with strict inequalities.
+ * As a tradeoff, the objective function is used internally, so it is not possible to maximise or minimise an
+ * arbitrary expression.
+ */
 class CompleteSoplexTheorySolver : public SoplexTheorySolver {
  public:
   explicit CompleteSoplexTheorySolver(PredicateAbstractor& predicate_abstractor, const Config& config = Config{});
@@ -42,8 +50,8 @@ class CompleteSoplexTheorySolver : public SoplexTheorySolver {
   void Reset(const Box& box) override;
 
  private:
-  void SetSPXVarBound() override;
-  void SetSpxRow(int spx_row, bool truth, const Variables& free_vars) override;
+  void EnableSPXVarBound() override;
+  void EnableSpxRow(int spx_row, bool truth, const Variables& free_vars) override;
 
   /**
    * Internal method to check the satisfiability of the current LP problem.
@@ -57,12 +65,23 @@ class CompleteSoplexTheorySolver : public SoplexTheorySolver {
    */
   SatResult SpxCheckSat(mpq_class* actual_precision);
 
+  /**
+   * Update the explanation with the current LP solution.
+   *
+   * A solution has been found, but a strict inequality has been violated.
+   * The explanation must be updated using an artificial infeasibility core.
+   */
   void UpdateExplanationStrictInfeasible();
 
+  /** Update the explanation with the infeasible core. */
   void UpdateExplanationInfeasible();
 
   void Consolidate() override;
 
+  /**
+   * Get the index of the strict variable used to enforce the strict inequalities.
+   * @return index of the strict variable
+   */
   int strict_variable_idx() const;
 
   /**
@@ -94,8 +113,16 @@ class CompleteSoplexTheorySolver : public SoplexTheorySolver {
    */
   bool UpdateBitIncrementIteratorBasedOnExplanation(BitIncrementIterator& bit_iterator);
 
+  /**
+   * Find the non-equal rows in the current explanation.
+   * @return vector of the non-equal rows in the current explanation
+   */
   std::vector<size_t> IteratorNqRowsInExplanation() const;
 
+  /**
+   * Get the explanation from @link theory_rows_to_explanation_ @endlink.
+   * @param[out] explanation The explanation to be updated
+   */
   void GetExplanation(LiteralSet& explanation);
 
   std::vector<int> enabled_strict_theory_rows_;                          ///< Vector of enabled strict theory rows

dlinear/solver/DeltaSoplexTheorySolver.cpp

@@ -91,7 +91,7 @@ std::vector<LiteralSet> DeltaSoplexTheorySolver::EnableLiteral(const Literal &li
     // Update the truth value for the current iteration with the last SAT solver assignment
     theory_row_to_lit_[spx_row].second = truth;
 
-    SetSpxRow(spx_row, truth, {});
+    EnableSpxRow(spx_row, truth, {});
     return {};
   }
 
@@ -156,7 +156,7 @@ SatResult DeltaSoplexTheorySolver::CheckSat(const Box &box, mpq_class *actual_pr
   }
 
   // Set the bounds for the variables
-  SetSPXVarBound();
+  EnableSPXVarBound();
 
   // Now we call the solver
   DLINEAR_DEBUG_FMT("DeltaSoplexTheorySolver::CheckSat: calling SoPlex (phase {})", simplex_sat_phase_);
@@ -242,7 +242,7 @@ SatResult DeltaSoplexTheorySolver::CheckSat(const Box &box, mpq_class *actual_pr
   return sat_status;
 }
 
-void DeltaSoplexTheorySolver::SetSpxRow(int spx_row, bool truth, [[maybe_unused]] const Variables &free_vars) {
+void DeltaSoplexTheorySolver::EnableSpxRow(int spx_row, bool truth, [[maybe_unused]] const Variables &free_vars) {
   const LpRowSense sense = spx_sense_[spx_row];
   const mpq_class &rhs{spx_rhs_[spx_row]};
   if (truth) {

dlinear/solver/DeltaSoplexTheorySolver.h

@@ -28,6 +28,13 @@
 
 namespace dlinear {
 
+/**
+ * DeltaSoplexTheorySolver class.
+ *
+ * Delta complete solver using SoPlex.
+ * The LP problem is solver exactly, within a given precision, delta.
+ * Since the value of delta is considered strictly positive, strict inequalities will be relaxed and ignored.
+ */
 class DeltaSoplexTheorySolver : public SoplexTheorySolver {
  public:
   explicit DeltaSoplexTheorySolver(PredicateAbstractor& predicate_abstractor, const Config& config = Config{});
@@ -39,7 +46,7 @@ class DeltaSoplexTheorySolver : public SoplexTheorySolver {
   SatResult CheckSat(const Box& box, mpq_class* actual_precision, LiteralSet& explanation) override;
 
  private:
-  void SetSpxRow(int spx_row, bool truth, const Variables& free_vars) override;
+  void EnableSpxRow(int spx_row, bool truth, const Variables& free_vars) override;
 };
 
 }  // namespace dlinear

dlinear/solver/QsoptexTheorySolver.cpp

@@ -228,7 +228,7 @@ bool QsoptexTheorySolver::SetQSXVarBound(const Bound &bound, int qsx_col) {
   mpq_QSget_bound(qsx_, qsx_col, toChar(-type), &c_value);
   mpq_class opposite_bound{c_value};
   if ((type == LpColBound::L && opposite_bound < value) || (type == LpColBound::U && opposite_bound > value)) {
-    DLINEAR_DEBUG_FMT("SoplexSatSolver::SetSPXVarBound: variable {} has invalid bounds [{}, {}]", var,
+    DLINEAR_DEBUG_FMT("SoplexSatSolver::EnableSPXVarBound: variable {} has invalid bounds [{}, {}]", var,
                       type == LpColBound::L ? value : opposite_bound, type == LpColBound::L ? opposite_bound : value);
     return false;
   }

dlinear/solver/SoplexTheorySolver.cpp

@@ -252,27 +252,27 @@ void SoplexTheorySolver::UpdateExplanation(LiteralSet &explanation) {
   }
 }
 
-// bool SoplexTheorySolver::SetSPXVarBound(const TheorySolver::Bound &bound, int spx_col) {
+// bool SoplexTheorySolver::EnableSPXVarBound(const TheorySolver::Bound &bound, int spx_col) {
 //   const auto &[var, type, value] = bound;
-//   return SetSPXVarBound(var, type, value, spx_col);
+//   return EnableSPXVarBound(var, type, value, spx_col);
 // }
 
-void SoplexTheorySolver::SetSPXVarBound() {
+void SoplexTheorySolver::EnableSPXVarBound() {
   for (int theory_col = 0; theory_col < static_cast<int>(theory_bounds_.size()); theory_col++) {
     spx_.changeBoundsRational(theory_col, theory_bounds_[theory_col].active_lower_bound().get_mpq_t(),
                               theory_bounds_[theory_col].active_upper_bound().get_mpq_t());
   }
 }
 
-void SoplexTheorySolver::SetSpxRow(const int spx_row) {
+void SoplexTheorySolver::EnableSpxRow(const int spx_row) {
   const auto &[var, truth] = theory_row_to_lit_[spx_row];
-  SetSpxRow(spx_row, truth, predicate_abstractor_[var].GetFreeVariables());
+  EnableSpxRow(spx_row, truth, predicate_abstractor_[var].GetFreeVariables());
 }
-void SoplexTheorySolver::SetSpxRow(const int spx_row, const bool truth) {
-  SetSpxRow(spx_row, truth, predicate_abstractor_[theory_row_to_lit_[spx_row].first].GetFreeVariables());
+void SoplexTheorySolver::EnableSpxRow(const int spx_row, const bool truth) {
+  EnableSpxRow(spx_row, truth, predicate_abstractor_[theory_row_to_lit_[spx_row].first].GetFreeVariables());
 }
-void SoplexTheorySolver::SetSpxRow(int spx_row, const Variables &free_vars) {
-  SetSpxRow(spx_row, theory_row_to_lit_[spx_row].second, free_vars);
+void SoplexTheorySolver::EnableSpxRow(int spx_row, const Variables &free_vars) {
+  EnableSpxRow(spx_row, theory_row_to_lit_[spx_row].second, free_vars);
 }
 
 }  // namespace dlinear

dlinear/solver/SoplexTheorySolver.h

@@ -36,8 +36,8 @@ class SoplexTheorySolver : public TheorySolver {
   void Reset(const Box& box) override;
 
  protected:
-  static mpq_class infinity_;
-  static mpq_class ninfinity_;
+  static mpq_class infinity_;   ///< Positive infinity
+  static mpq_class ninfinity_;  ///< Negative infinity
 
   void UpdateModelBounds() override;
   void UpdateExplanation(LiteralSet& explanation) override;
@@ -86,12 +86,44 @@ class SoplexTheorySolver : public TheorySolver {
    */
   bool IsRowActive(int spx_row, const soplex::Rational& value);
 
-  virtual void SetSPXVarBound();
+  /** Set the bounds of the variables in the LP solver.  */
+  virtual void EnableSPXVarBound();
 
-  void SetSpxRow(int spx_row);
-  void SetSpxRow(int spx_row, bool truth);
-  void SetSpxRow(int spx_row, const Variables& free_vars);
-  virtual void SetSpxRow(int spx_row, bool truth, const Variables& free_vars) = 0;
+  /**
+   * Enable the @p spx_row row for the LP solver.
+   *
+   * The truth value and the free variables are collected from the state of the solver.
+   * @pre The row's coefficients must have been set correctly before calling this function
+   * @pre The row's truth value must have been updated correctly
+   * @pre The row's free variables must have been updated correctly
+   * @param spx_row index of the row to enable
+   */
+  void EnableSpxRow(int spx_row);
+  /**
+   * Enable the @p spx_row row for the LP solver.
+   *
+   * The free variables are collected from the state of the solver.
+   * @pre The row's coefficients must have been set correctly before calling this function
+   * @pre The row's truth value must have been updated correctly
+   * @param spx_row index of the row to enable
+   * @param truth truth value of the row
+   */
+  void EnableSpxRow(int spx_row, bool truth);
+  /**
+   * Enable the @p spx_row row for the LP solver.
+   * @pre The row's coefficients must have been set correctly before calling this function
+   * @param spx_row index of the row to enable
+   * @param free_vars free variables appearing in the row
+   */
+  void EnableSpxRow(int spx_row, const Variables& free_vars);
+  /**
+   * Enable the @p spx_row row for the LP solver.
+   * @pre The row's coefficients must have been set correctly before calling this function
+   * @param spx_row index of the row to enable
+   * @param truth truth value of the row
+   * @param free_vars free variables appearing in the row
+   */
+  virtual void EnableSpxRow(int spx_row, bool truth, const Variables& free_vars) = 0;
 
   /**
    * Parse a row and return the vector of coefficients to apply to the decisional variables.
@@ -102,6 +134,12 @@ class SoplexTheorySolver : public TheorySolver {
    * @return vector of coefficients to apply to the decisional variables in the row
    */
   soplex::DSVectorRational ParseRowCoeff(const Formula& formula);
+  /**
+   * Set the coefficients to apply to @p var on a specific row.
+   * @param coeffs vector of coefficients to apply to the decisional variables
+   * @param var variable to set the coefficients for
+   * @param value value to set the coefficients to
+   */
   void SetSPXVarCoeff(soplex::DSVectorRational& coeffs, const Variable& var, const mpq_class& value) const;
   void CreateArtificials(int spx_row);
 

dlinear/solver/TheorySolver.cpp

@@ -124,9 +124,9 @@ TheorySolver::Bound TheorySolver::GetBound(const Formula &formula, const bool tr
   DLINEAR_RUNTIME_ERROR_FMT("Formula {} not supported", formula);
 }
 
-std::vector<LiteralSet> TheorySolver::TheoryBoundsToExplanations(Violation violation, const int theory_col) const {
+std::vector<LiteralSet> TheorySolver::TheoryBoundsToExplanations(Violation violation, const int theory_bound) const {
   std::vector<LiteralSet> explanations{};
-  TheoryBoundsToExplanations(violation, theory_col, explanations);
+  TheoryBoundsToExplanations(violation, theory_bound, explanations);
   return explanations;
 }
 void TheorySolver::TheoryBoundsToExplanations(Violation violation, int theory_bound,
@@ -148,14 +148,14 @@ void TheorySolver::TheoryBoundsToExplanation(const int theory_col, const bool ac
   }
 }
 
-std::vector<LiteralSet> TheorySolver::TheoryRowBoundsToExplanations(Violation violation, const int theory_col) const {
+std::vector<LiteralSet> TheorySolver::TheoryRowBoundsToExplanations(Violation violation, const int theory_row) const {
   std::vector<LiteralSet> explanations{};
-  TheoryRowBoundsToExplanations(violation, theory_col, explanations);
+  TheoryRowBoundsToExplanations(violation, theory_row, explanations);
   return explanations;
 }
-void TheorySolver::TheoryRowBoundsToExplanations(Violation violation, int theory_bound,
+void TheorySolver::TheoryRowBoundsToExplanations(Violation violation, int theory_row,
                                                  std::vector<LiteralSet> &explanations) const {
-  const Literal row_lit{theory_row_to_lit_[theory_bound]};
+  const Literal row_lit{theory_row_to_lit_[theory_row]};
   DLINEAR_DEBUG_FMT("CompleteSoplexTheorySolver::TheoryRowBoundsToExplanations: {} violates {}", row_lit, violation);
   if (violation.nq_bounds_empty() || violation.bounds_empty()) {
     for (; violation; ++violation) explanations.push_back({row_lit, theory_row_to_lit_[std::get<2>(*violation)]});