feat: avoid disabling rows in the LP solver at every reset, only doin…

…g it when necessary
TendTo · Jul 15, 2024 · a771eb5 · a771eb5
1 parent 6fdebcf
commit a771eb5
Show file tree

Hide file tree

Showing 6 changed files with 25 additions and 1 deletion.
diff --git a/dlinear/solver/CompleteSoplexTheorySolver.cpp b/dlinear/solver/CompleteSoplexTheorySolver.cpp
@@ -193,6 +193,8 @@ SatResult CompleteSoplexTheorySolver::CheckSat(const Box &box, mpq_class *actual
 
   // Set the bounds for the variables
   EnableSPXVarBound();
+  // Remove all the disabled rows from the LP solver
+  DisableSpxRows();
 
   // Now we call the solver
   DLINEAR_DEBUG_FMT("CompleteSoplexTheorySolver::CheckSat: calling SoPlex (phase {})", config_.simplex_sat_phase());
@@ -590,6 +592,7 @@ void CompleteSoplexTheorySolver::EnableSpxRow(int spx_row, bool truth) {
                     : Rational(soplex::infinity));
   spx_.changeRowRational(spx_row, lp_row);
 
+  theory_rows_state_.at(spx_row) = true;
   DLINEAR_TRACE_FMT("CompleteSoplexTheorySolver::EnableLinearLiteral: Row({}) ↦ {} {} {} | Sense({})", spx_row,
                     lp_row.lhs(), lp_row.rowVector(), lp_row.rhs(), sense);
 }

diff --git a/dlinear/solver/DeltaSoplexTheorySolver.cpp b/dlinear/solver/DeltaSoplexTheorySolver.cpp
@@ -160,6 +160,8 @@ SatResult DeltaSoplexTheorySolver::CheckSat(const Box &box, mpq_class *actual_pr
 
   // Set the bounds for the variables
   EnableSPXVarBound();
+  // Remove all the disabled rows from the LP solver
+  DisableSpxRows();
 
   // Now we call the solver
   DLINEAR_DEBUG_FMT("DeltaSoplexTheorySolver::CheckSat: calling SoPlex (phase {})", config_.simplex_sat_phase());
@@ -261,6 +263,7 @@ void DeltaSoplexTheorySolver::EnableSpxRow(int spx_row, bool truth) {
         sense == LpRowSense::LE || sense == LpRowSense::NQ ? Rational(gmp::to_mpq_t(rhs)) : Rational(-soplex::infinity),
         sense == LpRowSense::GE || sense == LpRowSense::NQ ? Rational(gmp::to_mpq_t(rhs)) : Rational(soplex::infinity));
   }
+  theory_rows_state_.at(spx_row) = true;
   DLINEAR_TRACE_FMT("DeltaSoplexTheorySolver::EnableLinearLiteral({}{})", truth ? "" : "¬", spx_row);
 }
 

diff --git a/dlinear/solver/SoplexTheorySolver.cpp b/dlinear/solver/SoplexTheorySolver.cpp
@@ -205,6 +205,7 @@ void SoplexTheorySolver::Reset(const Box &box) {
   DLINEAR_ASSERT(is_consolidated_, "The solver must be consolidate before resetting it");
 
   // Omitting to do this seems to cause problems in soplex
+  // https://github.com/scipopt/soplex/issues/38
   spx_.clearBasis();
   // Clear the preprocessor
   preprocessor_.Clear();
@@ -215,7 +216,7 @@ void SoplexTheorySolver::Reset(const Box &box) {
   for (auto &bound : theory_bounds_) bound.Clear();
   const int spx_rows = spx_.numRowsRational();
   DLINEAR_ASSERT(static_cast<std::size_t>(spx_rows) == theory_row_to_lit_.size(), "Row count mismatch");
-  for (int i = 0; i < spx_rows; i++) spx_.changeRangeRational(i, -soplex::infinity, soplex::infinity);
+  theory_rows_state_.assign(spx_rows, false);
 
   // Clear variable bounds
   [[maybe_unused]] const int spx_cols{spx_.numColsRational()};
@@ -278,6 +279,12 @@ void SoplexTheorySolver::UpdateExplanation(LiteralSet &explanation) {
   }
 }
 
+void SoplexTheorySolver::DisableSpxRows() {
+  for (int theory_row = 0; theory_row < spx_.numRowsRational(); theory_row++) {
+    if (!theory_rows_state_.at(theory_row)) spx_.changeRangeRational(theory_row, -soplex::infinity, soplex::infinity);
+  }
+}
+
 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(),

diff --git a/dlinear/solver/SoplexTheorySolver.h b/dlinear/solver/SoplexTheorySolver.h
@@ -112,6 +112,14 @@ class SoplexTheorySolver : public TheorySolver {
    */
   virtual void EnableSpxRow(int spx_row, bool truth) = 0;
 
+  /**
+   * Disable all disabled spx rows from the LP solver.
+   *
+   * Whether a row is disabled or not is determined by the @ref theory_row_state_ field,
+   * where a true value means the row is enabled and a false value means the row is disabled.
+   */
+  void DisableSpxRows();
+
   /**
    * Parse a row and return the vector of coefficients to apply to the decisional variables.
    *

diff --git a/dlinear/solver/TheorySolver.cpp b/dlinear/solver/TheorySolver.cpp
@@ -52,6 +52,7 @@ void TheorySolver::Consolidate() {
   DLINEAR_DEBUG("TheorySolver::Consolidate()");
   is_consolidated_ = true;
   enabled_theory_rows_.reserve(theory_row_to_lit_.size());
+  theory_rows_state_.resize(theory_row_to_lit_.size(), false);
 }
 
 bool TheorySolver::IsSimpleBound(const Formula &formula) {

diff --git a/dlinear/solver/TheorySolver.h b/dlinear/solver/TheorySolver.h
@@ -403,6 +403,8 @@ class TheorySolver {
                                                    ///< Rows that have been enabled in the current problem instance.
   TheorySolverBoundVectorVector theory_bounds_;    ///< Theory bounds.
                                                    ///< The bounds are the constraints on the values of the variables.
+  std::vector<bool> theory_rows_state_;            ///< Whether each theory row is active or not.
+
   ///< It also verifies that the bounds are consistent every time a new one is added.
 
   TheorySolverBoundPreprocessor preprocessor_;  ///< Preprocessor for the bounds.