1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
|
#include "gringo/term.hh"
#include "tests/tests.hh"
namespace Gringo {
namespace Input {
namespace Test {
struct DummyContext : IEContext {
void gatherIEs(IESolver &solver) const override { static_cast<void>(solver); }
void addIEBound(VarTerm const &var, IEBound const &bound) override { bounds.emplace(&var, bound); }
IEBoundMap bounds;
};
TEST_CASE("iesolver", "[iesolver]") {
SECTION("base") {
auto valX = std::make_shared<Symbol>(Symbol::createNum(0));
auto valY = std::make_shared<Symbol>(Symbol::createNum(0));
Location loc{"", 0, 0, "", 0, 0};
auto X = make_locatable<VarTerm>(loc, "X", valX);
auto Y = make_locatable<VarTerm>(loc, "Y", valY);
DummyContext ctx;
IESolver slv{ctx};
slv.add({{{1, X.get()}}, 2}, false);
slv.add({{{1, Y.get()}, {-1, X.get()}}, 1}, false);
slv.add({{{-1, X.get()}, {-1, Y.get()}}, -100}, false);
slv.compute();
auto const bounds = std::move(ctx.bounds);
auto itX = bounds.find(X.get());
auto itY = bounds.find(Y.get());
REQUIRE(!bounds.empty());
REQUIRE(itX != bounds.end());
REQUIRE(itY != bounds.end());
REQUIRE(itX->second.isSet(IEBound::Lower));
REQUIRE(itX->second.isSet(IEBound::Upper));
REQUIRE(itY->second.isSet(IEBound::Lower));
REQUIRE(itY->second.isSet(IEBound::Upper));
REQUIRE(itX->second.get(IEBound::Lower) == 2);
REQUIRE(itX->second.get(IEBound::Upper) == 97);
REQUIRE(itY->second.get(IEBound::Lower) == 3);
REQUIRE(itY->second.get(IEBound::Upper) == 98);
}
SECTION("bug") {
// X=1..2, Y=0, Z=X+3*Y.
auto valX = std::make_shared<Symbol>(Symbol::createNum(0));
auto valY = std::make_shared<Symbol>(Symbol::createNum(0));
auto valZ = std::make_shared<Symbol>(Symbol::createNum(0));
Location loc{"", 0, 0, "", 0, 0};
auto X = make_locatable<VarTerm>(loc, "X", valX);
auto Y = make_locatable<VarTerm>(loc, "Y", valY);
auto Z = make_locatable<VarTerm>(loc, "Z", valZ);
DummyContext ctx;
IESolver slv{ctx};
// X=1..2
slv.add({{{1, X.get()}}, 1}, false); // X>=1
slv.add({{{-1, X.get()}}, -2}, false); // X<=2
// Y=0
slv.add({{{1, Y.get()}}, 0}, false); // Y>=0
slv.add({{{-1, Y.get()}}, 0}, false); // Y<=0
// Z-X-3*Y=0
slv.add({{{1, Z.get()}, {-1, X.get()}, {-3, Y.get()}}, 0}, false); // Z-X-3*Y>=0
slv.add({{{-1, Z.get()}, {1, X.get()}, {3, Y.get()}}, 0}, false); // -Z+X+3*Y<=0
slv.compute();
auto const bounds = std::move(ctx.bounds);
auto itX = bounds.find(X.get());
auto itY = bounds.find(Y.get());
auto itZ = bounds.find(Z.get());
REQUIRE(!bounds.empty());
REQUIRE(itX != bounds.end());
REQUIRE(itY != bounds.end());
REQUIRE(itZ != bounds.end());
REQUIRE(itX->second.isSet(IEBound::Lower));
REQUIRE(itX->second.isSet(IEBound::Upper));
REQUIRE(itY->second.isSet(IEBound::Lower));
REQUIRE(itY->second.isSet(IEBound::Upper));
REQUIRE(itZ->second.isSet(IEBound::Lower));
REQUIRE(itZ->second.isSet(IEBound::Upper));
REQUIRE(itX->second.get(IEBound::Lower) == 1);
REQUIRE(itX->second.get(IEBound::Upper) == 2);
REQUIRE(itY->second.get(IEBound::Lower) == 0);
REQUIRE(itY->second.get(IEBound::Upper) == 0);
REQUIRE(itZ->second.get(IEBound::Lower) == 1);
REQUIRE(itZ->second.get(IEBound::Upper) == 2);
}
}
} // namespace Test
} // namespace Input
} // namespace Gringo
|
