Skip to content

Commit 59a58e5

Browse files
riccardodebenedictisriccardodebenedictis
committed
Implement var class: add lower and upper bound management; refactor solver methods to utilize new accessors
1 parent 081f617 commit 59a58e5

6 files changed

Lines changed: 167 additions & 95 deletions

File tree

‎CMakeLists.txt‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ project(LinSpire VERSION 0.2.0 LANGUAGES CXX)
44
include(CTest)
55
enable_testing()
66

7-
add_library(LinSpire src/linspire.cpp)
7+
add_library(LinSpire src/linspire.cpp src/var.cpp)
88
target_compile_features(LinSpire PUBLIC cxx_std_17)
99
target_include_directories(LinSpire PUBLIC $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/include>)
1010
if(NOT TARGET json)

‎include/linspire.hpp‎

Lines changed: 4 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,15 @@
11
#pragma once
2-
#include "lin.hpp"
3-
#include "inf_rational.hpp"
4-
#include "json.hpp"
2+
3+
#include "var.hpp"
54
#include <set>
65
#include <unordered_map>
7-
#include <memory>
86

97
namespace linspire
108
{
11-
class var;
12-
class constraint;
13-
149
class solver
1510
{
11+
friend class constraint;
12+
1613
public:
1714
/**
1815
* @brief Creates a new variable with specified lower and upper bounds.
@@ -219,28 +216,8 @@ namespace linspire
219216
std::map<utils::var, utils::inf_rational> lbs, ubs;
220217
};
221218

222-
class var
223-
{
224-
friend class solver;
225-
226-
public:
227-
var(const utils::inf_rational &lb = utils::inf_rational(utils::rational::negative_infinite), const utils::inf_rational &ub = utils::inf_rational(utils::rational::positive_infinite)) noexcept;
228-
229-
[[nodiscard]] utils::inf_rational lb() const noexcept;
230-
[[nodiscard]] utils::inf_rational ub() const noexcept;
231-
232-
friend std::string to_string(const var &x) noexcept;
233-
friend json::json to_json(const var &x) noexcept;
234-
235-
private:
236-
std::map<utils::inf_rational, std::set<std::shared_ptr<constraint>>> lbs, ubs;
237-
utils::inf_rational val;
238-
};
239-
240219
[[nodiscard]] std::string to_string(const solver &s) noexcept;
241220
[[nodiscard]] json::json to_json(const solver &s) noexcept;
242-
[[nodiscard]] std::string to_string(const var &x) noexcept;
243-
[[nodiscard]] json::json to_json(const var &x) noexcept;
244221
[[nodiscard]] json::json to_json(const utils::rational &r) noexcept;
245222
[[nodiscard]] json::json to_json(const utils::inf_rational &r) noexcept;
246223
[[nodiscard]] json::json to_json(const utils::lin &l) noexcept;

‎include/var.hpp‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
#pragma once
2+
3+
#include "lin.hpp"
4+
#include "inf_rational.hpp"
5+
#include "json.hpp"
6+
#include <set>
7+
#include <memory>
8+
9+
namespace linspire
10+
{
11+
class constraint;
12+
13+
class var
14+
{
15+
friend class solver;
16+
17+
public:
18+
var(const utils::var id, const utils::inf_rational &lb = utils::inf_rational(utils::rational::negative_infinite), const utils::inf_rational &ub = utils::inf_rational(utils::rational::positive_infinite)) noexcept;
19+
20+
[[nodiscard]] utils::inf_rational get_lb() const noexcept;
21+
[[nodiscard]] utils::inf_rational get_ub() const noexcept;
22+
[[nodiscard]] utils::inf_rational get_val() const noexcept { return val; }
23+
24+
friend std::string to_string(const var &x) noexcept;
25+
friend json::json to_json(const var &x) noexcept;
26+
27+
private:
28+
void set_lb(const utils::inf_rational &v, std::shared_ptr<constraint> reason = nullptr) noexcept;
29+
void unset_lb(const utils::inf_rational &v, std::shared_ptr<constraint> reason) noexcept;
30+
void set_ub(const utils::inf_rational &v, std::shared_ptr<constraint> reason = nullptr) noexcept;
31+
void unset_ub(const utils::inf_rational &v, std::shared_ptr<constraint> reason) noexcept;
32+
33+
private:
34+
const utils::var id; // the id of this variable in the solver..
35+
std::map<utils::inf_rational, std::set<std::shared_ptr<constraint>>> lbs, ubs; // the lower and upper bounds with their reasons..
36+
utils::inf_rational val; // the current value of this variable..
37+
};
38+
39+
[[nodiscard]] std::string to_string(const var &x) noexcept;
40+
[[nodiscard]] json::json to_json(const var &x) noexcept;
41+
} // namespace linspire

‎src/linspire.cpp‎

Lines changed: 33 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ namespace linspire
99
{
1010
assert(lb <= ub);
1111
const auto x = vars.size();
12-
vars.emplace_back(lb, ub);
12+
vars.emplace_back(x, lb, ub);
1313
t_watches.emplace_back();
1414
return x;
1515
}
@@ -28,8 +28,8 @@ namespace linspire
2828
return slack;
2929
}
3030

31-
utils::inf_rational solver::lb(const utils::var x) const noexcept { return vars[x].lb(); }
32-
utils::inf_rational solver::ub(const utils::var x) const noexcept { return vars[x].ub(); }
31+
utils::inf_rational solver::lb(const utils::var x) const noexcept { return vars[x].get_lb(); }
32+
utils::inf_rational solver::ub(const utils::var x) const noexcept { return vars[x].get_ub(); }
3333
utils::inf_rational solver::val(const utils::var x) const noexcept { return vars[x].val; }
3434

3535
bool solver::new_eq(const utils::lin &lhs, const utils::lin &rhs, std::shared_ptr<constraint> reason) noexcept
@@ -113,18 +113,10 @@ namespace linspire
113113
void solver::retract(const std::shared_ptr<constraint> c) noexcept
114114
{
115115
for (const auto &[x, lb] : c->lbs)
116-
{
117-
vars[x].lbs[lb].erase(c);
118-
if (vars[x].lbs[lb].empty())
119-
vars[x].lbs.erase(lb);
120-
}
116+
vars[x].unset_lb(lb, c);
121117
c->lbs.clear();
122118
for (const auto &[x, ub] : c->ubs)
123-
{
124-
vars[x].ubs[ub].erase(c);
125-
if (vars[x].ubs[ub].empty())
126-
vars[x].ubs.erase(ub);
127-
}
119+
vars[x].unset_ub(ub, c);
128120
c->ubs.clear();
129121
}
130122

@@ -187,57 +179,49 @@ namespace linspire
187179
bool solver::set_lb(const utils::var x, const utils::inf_rational &v, std::shared_ptr<constraint> reason) noexcept
188180
{
189181
assert(x < vars.size());
182+
assert(v > utils::rational::negative_infinite);
190183
LOG_TRACE("x" << std::to_string(x) << " = " << utils::to_string(val(x)) << " [" << utils::to_string(lb(x)) << " -> " << utils::to_string(v) << ", " << utils::to_string(ub(x)) << "]");
191-
if (v <= lb(x))
192-
return true; // no update needed..
193-
else if (v > ub(x))
194-
return false; // inconsistent bounds..
195-
184+
if (v > ub(x)) // inconsistent bound..
185+
return false;
196186
if (reason)
197-
{
198-
if (auto it = vars[x].lbs.find(v); it != vars[x].lbs.end())
199-
it->second.insert(reason);
187+
{ // we have a reason for this bound..
188+
if (auto it = reason->lbs.find(x); it != reason->lbs.end())
189+
{ // we already have a lower bound for this variable in the reason..
190+
if (it->second < v)
191+
{ // we update the lower bound only if the new one is more restrictive..
192+
vars.at(x).unset_lb(it->second, reason);
193+
it->second = v;
194+
}
195+
}
200196
else
201-
vars[x].lbs.emplace(v, std::set<std::shared_ptr<constraint>>{reason});
202-
reason->lbs.emplace(x, v);
203-
}
204-
else
205-
{
206-
auto &lbs = vars[x].lbs;
207-
auto it = lbs.upper_bound(v);
208-
lbs.erase(lbs.begin(), it);
209-
lbs.emplace(v, std::set<std::shared_ptr<constraint>>());
197+
reason->lbs.emplace(x, v);
210198
}
211-
199+
vars.at(x).set_lb(v, reason);
212200
if (val(x) < v && !is_basic(x))
213201
update(x, v);
214202
return true;
215203
}
216204
bool solver::set_ub(const utils::var x, const utils::inf_rational &v, std::shared_ptr<constraint> reason) noexcept
217205
{
218206
assert(x < vars.size());
207+
assert(v < utils::rational::positive_infinite);
219208
LOG_TRACE("x" << std::to_string(x) << " = " << utils::to_string(val(x)) << " [" << utils::to_string(lb(x)) << ", " << utils::to_string(v) << " <- " << utils::to_string(ub(x)) << "]");
220-
if (v >= ub(x))
221-
return true; // no update needed..
222-
else if (v < lb(x))
223-
return false; // inconsistent bounds..
224-
209+
if (v < lb(x)) // inconsistent bound..
210+
return false;
225211
if (reason)
226-
{
227-
if (auto it = vars[x].ubs.find(v); it != vars[x].ubs.end())
228-
it->second.insert(reason);
212+
{ // we have a reason for this bound..
213+
if (auto it = reason->ubs.find(x); it != reason->ubs.end())
214+
{ // we already have an upper bound for this variable in the reason..
215+
if (it->second > v)
216+
{ // we update the upper bound only if the new one is more restrictive..
217+
vars.at(x).unset_ub(it->second, reason);
218+
it->second = v;
219+
}
220+
}
229221
else
230-
vars[x].ubs.emplace(v, std::set<std::shared_ptr<constraint>>{reason});
231-
reason->ubs.emplace(x, v);
232-
}
233-
else
234-
{
235-
auto &ubs = vars[x].ubs;
236-
auto it = ubs.lower_bound(v);
237-
ubs.erase(it, ubs.end());
238-
ubs.emplace(v, std::set<std::shared_ptr<constraint>>());
222+
reason->ubs.emplace(x, v);
239223
}
240-
224+
vars.at(x).set_ub(v, reason);
241225
if (val(x) > v && !is_basic(x))
242226
update(x, v);
243227
return true;
@@ -350,11 +334,6 @@ namespace linspire
350334
tableau.emplace(x, std::move(l));
351335
}
352336

353-
var::var(const utils::inf_rational &lb, const utils::inf_rational &ub) noexcept { assert(lb < ub); }
354-
355-
utils::inf_rational var::lb() const noexcept { return lbs.empty() ? utils::rational::negative_infinite : lbs.rbegin()->first; }
356-
utils::inf_rational var::ub() const noexcept { return ubs.empty() ? utils::rational::positive_infinite : ubs.begin()->first; }
357-
358337
std::string to_string(const solver &s) noexcept
359338
{
360339
std::string str;
@@ -381,18 +360,6 @@ namespace linspire
381360

382361
json::json to_json(const utils::rational &r) noexcept { return json::json{{"num", r.numerator()}, {"den", r.denominator()}}; }
383362

384-
std::string to_string(const var &x) noexcept { return utils::to_string(x.val) + " [" + utils::to_string(x.lb()) + ", " + utils::to_string(x.ub()) + "]"; }
385-
386-
json::json to_json(const var &x) noexcept
387-
{
388-
json::json j = linspire::to_json(x.val);
389-
if (!x.lbs.empty())
390-
j["lb"] = linspire::to_json(x.lbs.rbegin()->first);
391-
if (!x.ubs.empty())
392-
j["ub"] = linspire::to_json(x.ubs.begin()->first);
393-
return j;
394-
}
395-
396363
json::json to_json(const utils::inf_rational &r) noexcept
397364
{
398365
json::json j = to_json(r.get_rational());

‎src/var.cpp‎

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,77 @@
1+
#include "var.hpp"
2+
#include "linspire.hpp"
3+
#include <cassert>
4+
5+
namespace linspire
6+
{
7+
var::var(const utils::var id, const utils::inf_rational &lb, const utils::inf_rational &ub) noexcept : id(id) { assert(lb < ub); }
8+
9+
utils::inf_rational var::get_lb() const noexcept { return lbs.empty() ? utils::rational::negative_infinite : lbs.rbegin()->first; }
10+
utils::inf_rational var::get_ub() const noexcept { return ubs.empty() ? utils::rational::positive_infinite : ubs.begin()->first; }
11+
12+
void var::set_lb(const utils::inf_rational &v, std::shared_ptr<constraint> reason) noexcept
13+
{
14+
assert(v <= get_ub()); // we cannot set a lower bound greater than the current upper bound..
15+
if (reason)
16+
{ // we add a new lower bound `v` with the given reason..
17+
if (auto it = lbs.find(v); it != lbs.end())
18+
it->second.insert(reason); // we add the reason to the existing lower bound `v`..
19+
else
20+
lbs.emplace(v, std::set<std::shared_ptr<constraint>>{reason}); // we create a new lower bound `v`..
21+
}
22+
else
23+
{ // we remove all the lower bounds that are less than `v`..
24+
auto it = lbs.upper_bound(v);
25+
lbs.erase(lbs.begin(), it);
26+
lbs.emplace(v, std::set<std::shared_ptr<constraint>>());
27+
}
28+
}
29+
void var::unset_lb(const utils::inf_rational &v, std::shared_ptr<constraint> reason) noexcept
30+
{
31+
assert(lbs.find(v) != lbs.end());
32+
assert(reason);
33+
auto it = lbs.find(v);
34+
it->second.erase(reason);
35+
if (it->second.empty())
36+
lbs.erase(it);
37+
}
38+
39+
void var::set_ub(const utils::inf_rational &v, std::shared_ptr<constraint> reason) noexcept
40+
{
41+
assert(v >= get_lb()); // we cannot set an upper bound less than the current lower bound..
42+
if (reason)
43+
{ // we add a new upper bound `v` with the given reason..
44+
if (auto it = ubs.find(v); it != ubs.end())
45+
it->second.insert(reason); // we add the reason to the existing upper bound `v`..
46+
else
47+
ubs.emplace(v, std::set<std::shared_ptr<constraint>>{reason}); // we create a new upper bound `v`..
48+
}
49+
else
50+
{ // we remove all the upper bounds that are greater than `v`..
51+
auto it = ubs.lower_bound(v);
52+
ubs.erase(it, ubs.end());
53+
ubs.emplace(v, std::set<std::shared_ptr<constraint>>());
54+
}
55+
}
56+
void var::unset_ub(const utils::inf_rational &v, std::shared_ptr<constraint> reason) noexcept
57+
{
58+
assert(ubs.find(v) != ubs.end());
59+
assert(reason);
60+
auto it = ubs.find(v);
61+
it->second.erase(reason);
62+
if (it->second.empty())
63+
ubs.erase(it);
64+
}
65+
66+
std::string to_string(const var &x) noexcept { return utils::to_string(x.val) + " [" + utils::to_string(x.get_lb()) + ", " + utils::to_string(x.get_ub()) + "]"; }
67+
68+
json::json to_json(const var &x) noexcept
69+
{
70+
json::json j = to_json(x.val);
71+
if (!x.lbs.empty())
72+
j["lb"] = to_json(x.lbs.rbegin()->first);
73+
if (!x.ubs.empty())
74+
j["ub"] = to_json(x.ubs.begin()->first);
75+
return j;
76+
}
77+
} // namespace linspire

‎tests/test_linspire.cpp‎

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,16 @@ void test1()
6868
assert(!cons);
6969
}
7070

71+
/**
72+
* @brief Unit test for the linspire::solver class.
73+
*
74+
* This test verifies the following functionalities:
75+
* - Creating variables and adding constraints sharing the same reason.
76+
* - Ensuring that the constraints are satisfiable and checking the solver's consistency.
77+
* - Testing the solver's ability to retract constraints and ensure bounds are reset.
78+
*
79+
* Assertions are used to ensure that each step behaves as expected.
80+
*/
7181
void test2()
7282
{
7383
linspire::solver s;
@@ -78,7 +88,7 @@ void test2()
7888
// x >= 0
7989
bool res0 = s.new_gt({{x, 1}}, 0, false, c0);
8090
assert(res0);
81-
// x >= 1
91+
// x >= 1 (we add this constraint with the same reason as the previous one)
8292
bool res1 = s.new_gt({{x, 1}}, 1, false, c0);
8393
assert(res1);
8494

0 commit comments

Comments
 (0)