Add add_constraint method and update constraint handling in var class

- Implemented add_constraint method to incorporate previously created constraints into the solver.
- Updated set_lb, unset_lb, set_ub, and unset_ub methods to use const references for constraint parameters.
- Enhanced unit tests to verify the functionality of adding, retracting, and re-adding constraints.

Author: riccardodebenedictis

include/linspire.hpp

@@ -154,6 +154,16 @@ namespace linspire
      */
     [[nodiscard]] bool new_gt(const utils::lin &lhs, const utils::lin &rhs, bool strict = false, std::optional<std::reference_wrapper<constraint>> reason = std::nullopt) noexcept;
 
+    /**
+     * @brief Adds a previously created constraint to the solver.
+     *
+     * This function incorporates a previously defined constraint into the solver. It updates
+     * the internal state of the solver to account for the new constraint.
+     *
+     * @param c The constraint to be added.
+     */
+    void add_constraint(const constraint &c) noexcept;
+
     /**
      * @brief Retracts a previously added constraint from the solver.
      *
@@ -162,7 +172,7 @@ namespace linspire
      *
      * @param c The constraint to be retracted.
      */
-    void retract(constraint &c) noexcept;
+    void retract(const constraint &c) noexcept;
 
     /**
      * @brief Checks the consistency of the current set of constraints.
@@ -185,7 +195,7 @@ namespace linspire
      *
      * @return A constant reference to the vector of constraints representing the last conflict explanation.
      */
-    [[nodiscard]] const std::vector<std::reference_wrapper<constraint>> &get_conflict() const noexcept { return cnfl; }
+    [[nodiscard]] const std::vector<std::reference_wrapper<const constraint>> &get_conflict() const noexcept { return cnfl; }
 
     /**
      * @brief Checks if two linear expressions can be made equal.
@@ -237,11 +247,11 @@ namespace linspire
 
     void new_row(const utils::var x, utils::lin &&l) noexcept;
 
-    std::vector<var> vars;                                // index is the variable id
-    std::unordered_map<std::string, utils::var> exprs;    // the expressions (string to numeric variable) for which already exist slack variables..
-    std::map<utils::var, utils::lin> tableau;             // basic variable -> expression
-    std::vector<std::set<utils::var>> t_watches;          // for each variable `v`, a set of tableau rows watching `v`..
-    std::vector<std::reference_wrapper<constraint>> cnfl; // the last conflict explanation..
+    std::vector<var> vars;                                      // index is the variable id
+    std::unordered_map<std::string, utils::var> exprs;          // the expressions (string to numeric variable) for which already exist slack variables..
+    std::map<utils::var, utils::lin> tableau;                   // basic variable -> expression
+    std::vector<std::set<utils::var>> t_watches;                // for each variable `v`, a set of tableau rows watching `v`..
+    std::vector<std::reference_wrapper<const constraint>> cnfl; // the last conflict explanation..
 #ifdef LINSPIRE_ENABLE_LISTENERS
     std::unordered_map<utils::var, std::set<listener *>> listening; // for each variable, the listeners listening to it..
     std::set<listener *> listeners;                                 // the collection of listeners..

include/var.hpp

@@ -26,14 +26,14 @@ namespace linspire
     friend json::json to_json(const var &x) noexcept;
 
   private:
-    void set_lb(const utils::inf_rational &v, std::optional<std::reference_wrapper<constraint>> reason = std::nullopt) noexcept;
-    void unset_lb(const utils::inf_rational &v, constraint &reason) noexcept;
-    void set_ub(const utils::inf_rational &v, std::optional<std::reference_wrapper<constraint>> reason = std::nullopt) noexcept;
-    void unset_ub(const utils::inf_rational &v, constraint &reason) noexcept;
+    void set_lb(const utils::inf_rational &v, std::optional<std::reference_wrapper<const constraint>> reason = std::nullopt) noexcept;
+    void unset_lb(const utils::inf_rational &v, const constraint &reason) noexcept;
+    void set_ub(const utils::inf_rational &v, std::optional<std::reference_wrapper<const constraint>> reason = std::nullopt) noexcept;
+    void unset_ub(const utils::inf_rational &v, const constraint &reason) noexcept;
 
   private:
-    std::map<utils::inf_rational, std::set<constraint *>> lbs, ubs; // the lower and upper bounds with their reasons..
-    utils::inf_rational val;                                        // the current value of this variable..
+    std::map<utils::inf_rational, std::set<const constraint *>> lbs, ubs; // the lower and upper bounds with their reasons..
+    utils::inf_rational val;                                              // the current value of this variable..
   };
 
   [[nodiscard]] std::string to_string(const var &x) noexcept;

src/linspire.cpp

@@ -119,14 +119,20 @@ namespace linspire
     }
     bool solver::new_gt(const utils::lin &lhs, const utils::lin &rhs, bool strict, std::optional<std::reference_wrapper<constraint>> reason) noexcept { return new_lt(rhs, lhs, strict, reason); }
 
-    void solver::retract(constraint &c) noexcept
+    void solver::add_constraint(const constraint &c) noexcept
+    {
+        for (const auto &[x, lb] : c.lbs)
+            vars[x].set_lb(lb, c);
+        for (const auto &[x, ub] : c.ubs)
+            vars[x].set_ub(ub, c);
+    }
+
+    void solver::retract(const constraint &c) noexcept
     {
         for (const auto &[x, lb] : c.lbs)
             vars[x].unset_lb(lb, c);
-        c.lbs.clear();
         for (const auto &[x, ub] : c.ubs)
             vars[x].unset_ub(ub, c);
-        c.ubs.clear();
     }
 
     bool solver::check() noexcept

src/var.cpp

@@ -9,24 +9,24 @@ namespace linspire
     utils::inf_rational var::get_lb() const noexcept { return lbs.empty() ? utils::rational::negative_infinite : lbs.rbegin()->first; }
     utils::inf_rational var::get_ub() const noexcept { return ubs.empty() ? utils::rational::positive_infinite : ubs.begin()->first; }
 
-    void var::set_lb(const utils::inf_rational &v, std::optional<std::reference_wrapper<constraint>> reason) noexcept
+    void var::set_lb(const utils::inf_rational &v, std::optional<std::reference_wrapper<const constraint>> reason) noexcept
     {
         assert(v <= get_ub()); // we cannot set a lower bound greater than the current upper bound..
         if (reason)
         { // we add a new lower bound `v` with the given reason..
             if (auto it = lbs.find(v); it != lbs.end())
                 it->second.insert(&reason->get()); // we add the reason to the existing lower bound `v`..
             else
-                lbs.emplace(v, std::set<constraint *>{&reason->get()}); // we create a new lower bound `v`..
+                lbs.emplace(v, std::set<const constraint *>{&reason->get()}); // we create a new lower bound `v`..
         }
         else
         { // we remove all the lower bounds that are less than `v`..
             auto it = lbs.upper_bound(v);
             lbs.erase(lbs.begin(), it);
-            lbs.emplace(v, std::set<constraint *>());
+            lbs.emplace(v, std::set<const constraint *>());
         }
     }
-    void var::unset_lb(const utils::inf_rational &v, constraint &reason) noexcept
+    void var::unset_lb(const utils::inf_rational &v, const constraint &reason) noexcept
     {
         assert(lbs.find(v) != lbs.end());
         auto it = lbs.find(v);
@@ -35,24 +35,24 @@ namespace linspire
             lbs.erase(it);
     }
 
-    void var::set_ub(const utils::inf_rational &v, std::optional<std::reference_wrapper<constraint>> reason) noexcept
+    void var::set_ub(const utils::inf_rational &v, std::optional<std::reference_wrapper<const constraint>> reason) noexcept
     {
         assert(v >= get_lb()); // we cannot set an upper bound less than the current lower bound..
         if (reason)
         { // we add a new upper bound `v` with the given reason..
             if (auto it = ubs.find(v); it != ubs.end())
                 it->second.insert(&reason->get()); // we add the reason to the existing upper bound `v`..
             else
-                ubs.emplace(v, std::set<constraint *>{&reason->get()}); // we create a new upper bound `v`..
+                ubs.emplace(v, std::set<const constraint *>{&reason->get()}); // we create a new upper bound `v`..
         }
         else
         { // we remove all the upper bounds that are greater than `v`..
             auto it = ubs.lower_bound(v);
             ubs.erase(it, ubs.end());
-            ubs.emplace(v, std::set<constraint *>());
+            ubs.emplace(v, std::set<const constraint *>());
         }
     }
-    void var::unset_ub(const utils::inf_rational &v, constraint &reason) noexcept
+    void var::unset_ub(const utils::inf_rational &v, const constraint &reason) noexcept
     {
         assert(ubs.find(v) != ubs.end());
         auto it = ubs.find(v);

tests/test_linspire.cpp

@@ -183,13 +183,54 @@ void test4()
     assert(cons);
 }
 
+/**
+ * @brief Unit test for adding, retracting, and re-adding a constraint.
+ *
+ * This test verifies:
+ * - Adding a constraint and checking consistency.
+ * - Retracting the constraint and ensuring bounds are reset.
+ * - Adding the same constraint again and checking consistency.
+ */
+void test5()
+{
+    linspire::solver s;
+    auto x = s.new_var();
+
+    linspire::constraint c0;
+
+    // Add constraint: x >= 5
+    bool res0 = s.new_gt({{x, 1}}, 5, false, c0);
+    assert(res0);
+    bool cons = s.check();
+    assert(cons);
+    assert(s.lb(x) == 5);
+    assert(s.ub(x) == utils::rational::positive_infinite);
+    assert(s.val(x) >= 5);
+
+    // Retract constraint
+    s.retract(c0);
+    cons = s.check();
+    assert(cons);
+    assert(s.lb(x) == utils::rational::negative_infinite);
+    assert(s.ub(x) == utils::rational::positive_infinite);
+
+    // Add the same constraint again
+    s.add_constraint(c0);
+    cons = s.check();
+    assert(cons);
+    assert(s.lb(x) == 5);
+    assert(s.ub(x) == utils::rational::positive_infinite);
+    assert(s.val(x) >= 5);
+}
+
 int main()
 {
     test0();
     test1();
     test2();
     test3();
     test4();
+    test5();
 
     return 0;
 }