1 // {{{ MIT License
2
3 // Copyright 2017 Roland Kaminski
4
5 // Permission is hereby granted, free of charge, to any person obtaining a copy
6 // of this software and associated documentation files (the "Software"), to
7 // deal in the Software without restriction, including without limitation the
8 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
9 // sell copies of the Software, and to permit persons to whom the Software is
10 // furnished to do so, subject to the following conditions:
11
12 // The above copyright notice and this permission notice shall be included in
13 // all copies or substantial portions of the Software.
14
15 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
20 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
21 // IN THE SOFTWARE.
22
23 // }}}
24
25 #include "tests.hh"
26 #include <iostream>
27 #include <fstream>
28 #include <sstream>
29
30 namespace Clingo { namespace Test {
31
32 namespace {
33
34 template <class V>
vec(V const & vec)35 std::vector<typename V::value_type> vec(V const &vec) {
36 std::vector<typename V::value_type> ret;
37 for (auto &&x : vec) {
38 ret.emplace_back(x);
39 }
40 return ret;
41 }
42
43 template <class V, class W>
cmp(V const & a,W const & b)44 bool cmp(V const &a, W const &b) {
45 return std::equal(a.begin(), a.end(), b.begin(), b.end(), [](auto &&x, auto &&y) {
46 return std::strcmp(x, y) == 0;
47 });
48 }
49
50 struct CB {
CBClingo::Test::__anonc0d366050111::CB51 CB(std::string &ret)
52 : ret(ret) { ret.clear(); }
operator ()Clingo::Test::__anonc0d366050111::CB53 void operator()(AST::Node const &x) {
54 std::ostringstream oss;
55 oss << x;
56 if (first) {
57 REQUIRE(oss.str() == "#program base.");
58 first = false;
59 }
60 else {
61 if (!ret.empty()) { ret+= "\n"; }
62 ret+= oss.str();
63 }
64 }
65 bool first = true;
66 std::string &ret;
67 };
68
parse(char const * prg)69 std::string parse(char const *prg) {
70 std::string ret;
71 AST::parse_string(prg, CB(ret));
72 return ret;
73 }
74
unpool(char const * prg)75 std::string unpool(char const *prg) {
76 std::string ret;
77 auto cb = CB(ret);
78 AST::parse_string(prg, [&](AST::Node const &ast) {
79 for (auto &unpooled : ast.unpool()) {
80 cb(unpooled);
81 }
82 });
83 return ret;
84 }
85
solve(char const * prg,PartSpan parts={{"base", {}}})86 ModelVec solve(char const *prg, PartSpan parts = {{"base", {}}}) {
87 MessageVec messages;
88 ModelVec models;
__anonc0d366050402() 89 Control ctl{{"0"}, [&messages](WarningCode code, char const *msg) { messages.emplace_back(code, msg); }};
90
__anonc0d366050502(AST::ProgramBuilder &b)91 AST::with_builder(ctl, [prg](AST::ProgramBuilder &b){
92 AST::parse_string(prg, [&b](AST::Node const &stm) { b.add(stm); });
93 });
94 ctl.ground(parts);
95 test_solve(ctl.solve(), models);
96 return models;
97 }
98
99 using StringVec = std::vector<std::string>;
parse_theory(char const * prg,char const * theory)100 StringVec parse_theory(char const *prg, char const *theory) {
101 MessageVec messages;
102 ModelVec models;
103 Control ctl{{"0"}, [&messages](WarningCode code, char const *msg) { messages.emplace_back(code, msg); }};
104 AST::with_builder(ctl, [prg, theory](AST::ProgramBuilder &b){
105 AST::parse_string(theory, [&b](AST::Node const &ast) { b.add(ast); });
106 AST::parse_string(prg, [&b](AST::Node const &ast) { b.add(ast); });
107 });
108 ctl.ground({{"base", {}}});
109 StringVec ret;
110 for (auto x : ctl.theory_atoms()) {
111 std::ostringstream oss;
112 oss << x;
113 ret.emplace_back(oss.str());
114 }
115 return ret;
116 }
117
118 } // namespace
119
120 TEST_CASE("parse-ast-v2", "[clingo]") {
121 SECTION("statement") {
122 REQUIRE(parse("a.") == "a.");
123 REQUIRE(parse("a:-b.") == "a :- b.");
124 REQUIRE(parse("#const a=10. [override]") == "#const a = 10. [override]");
125 REQUIRE(parse("#const a=10. [default]") == "#const a = 10.");
126 REQUIRE(parse("#const a=10.") == "#const a = 10.");
127 REQUIRE(parse("#show a/1.") == "#show a/1.");
128 REQUIRE(parse("#show $a/1.") == "#show $a/1.");
129 REQUIRE(parse("#show a : b.") == "#show a : b.");
130 REQUIRE(parse("#show $a : b.") == "#show $a : b.");
131 REQUIRE(parse("#show $a : b.") == "#show $a : b.");
132 REQUIRE(parse("#minimize{ 1:b }.") == ":~ b. [1@0]");
133 REQUIRE(parse("#script (python)\n42\n #end.") == "#script (python)\n42\n#end.");
134 REQUIRE(parse("#script (lua) \n42\n #end.") == "#script (lua)\n42\n#end.");
135 REQUIRE(parse("#script (other) \n42\n#end.") == "#script (other)\n42\n#end.");
136 REQUIRE(parse("#program p(k).") == "#program p(k).");
137 REQUIRE(parse("#external p(k).") == "#external p(k). [false]");
138 REQUIRE(parse("#external p(k). [true]") == "#external p(k). [true]");
139 REQUIRE(parse("#external p(k) : a, b.") == "#external p(k) : a; b. [false]");
140 REQUIRE(parse("#edge (u,v) : a, b.") == "#edge (u,v) : a; b.");
141 REQUIRE(parse("#heuristic a : b, c. [L@P,level]") == "#heuristic a : b; c. [L@P,level]");
142 REQUIRE(parse("#project a : b.") == "#project a : b.");
143 REQUIRE(parse("#project a/2.") == "#project a/2.");
144 REQUIRE(parse("#theory x {}.") == "#theory x {\n}.");
145 }
146 SECTION("theory definition") {
147 REQUIRE(parse("#theory x { t { ++ : 1, unary } }.") == "#theory x {\n" " t {\n" " ++ : 1, unary\n" " }\n" "}.");
148 REQUIRE(parse("#theory x { &a/0: t, any }.") == "#theory x {\n &a/0: t, any\n}.");
149 REQUIRE(parse("#theory x { &a/0: t, {+, -}, u, any }.") == "#theory x {\n &a/0: t, { +, - }, u, any\n}.");
150 }
151 SECTION("body literal") {
152 REQUIRE(parse(":-a.") == "#false :- a.");
153 REQUIRE(parse(":-not a.") == "#false :- not a.");
154 REQUIRE(parse(":-not not a.") == "#false :- not not a.");
155 REQUIRE(parse(":-a:b.") == "#false :- a: b.");
156 REQUIRE(parse(":-a:b,c;d.") == "#false :- a: b, c; d.");
157 REQUIRE(parse(":-1{a:b,c;e}2.") == "#false :- 1 <= { a: b, c; e } <= 2.");
158 REQUIRE(parse(":-{a:b,c;e}2.") == "#false :- 2 >= { a: b, c; e }.");
159 REQUIRE(parse(":-1#min{1,2:b,c;1:e}2.") == "#false :- 1 <= #min { 1,2: b, c; 1: e } <= 2.");
160 REQUIRE(parse(":-&p { 1: a,b; 2: c }.") == "#false :- &p { 1: a, b; 2: c }.");
161 REQUIRE(parse(":-#disjoint {1,2:$x:a,b}.") == "#false :- #disjoint { 1,2:1$*$x: a, b }.");
162 }
163 SECTION("head literal") {
164 REQUIRE(parse("a.") == "a.");
165 REQUIRE(parse("a:b.") == "a: b.");
166 REQUIRE(parse("a:b,c;d.") == "a: b, c; d.");
167 REQUIRE(parse("1{a:b,c;e}2.") == "1 <= { a: b, c; e } <= 2.");
168 REQUIRE(parse("{a:b,c;e}2.") == "2 >= { a: b, c; e }.");
169 REQUIRE(parse("1#min{1,2:h:b,c;1:e}2.") == "1 <= #min { 1,2: h: b, c; 1: e } <= 2.");
170 REQUIRE(parse("&p { 1 : a,b; 2 : c }.") == "&p { 1: a, b; 2: c }.");
171 REQUIRE(parse("&p { 1 : a,b; 2 : c } ** 33.") == "&p { 1: a, b; 2: c } ** 33.");
172 }
173 SECTION("literal") {
174 REQUIRE(parse("#true.") == "#true.");
175 REQUIRE(parse("#false.") == "#false.");
176 REQUIRE(parse("a.") == "a.");
177 REQUIRE(parse("not a.") == "not a.");
178 REQUIRE(parse("not not a.") == "not not a.");
179 REQUIRE(parse("1 != 3.") == "1 != 3.");
180 REQUIRE(parse("1 $< 2 $< 3.") == "1 $< 2 $< 3.");
181 REQUIRE(parse("1 $< 2 $< 3.") == "1 $< 2 $< 3.");
182 }
183 SECTION("terms") {
184 REQUIRE(parse("p(a).") == "p(a).");
185 REQUIRE(parse("p(X).") == "p(X).");
186 REQUIRE(parse("p(-a).") == "p(-a).");
187 REQUIRE(parse("p(~a).") == "p(~a).");
188 REQUIRE(parse("p(|a|).") == "p(|a|).");
189 REQUIRE(parse("p((a+b)).") == "p((a+b)).");
190 REQUIRE(parse("p((a-b)).") == "p((a-b)).");
191 REQUIRE(parse("p((a*b)).") == "p((a*b)).");
192 REQUIRE(parse("p((a/b)).") == "p((a/b)).");
193 REQUIRE(parse("p((a\\b)).") == "p((a\\b)).");
194 REQUIRE(parse("p((a?b)).") == "p((a?b)).");
195 REQUIRE(parse("p((a^b)).") == "p((a^b)).");
196 REQUIRE(parse("p(a..b).") == "p((a..b)).");
197 REQUIRE(parse("p((),(1,),f(),f(1,2)).") == "p((),(1,),f,f(1,2)).");
198 REQUIRE(parse("p(@f(a;b)).") == "p(@f(a;b)).");
199 REQUIRE(parse("p(a;b).") == "p(a;b).");
200 REQUIRE(parse("p((a,;b)).") == "p(((a,);b)).");
201 REQUIRE(parse("p(((a,);b)).") == "p(((a,);b)).");
202 REQUIRE(parse("1 $+ 3 $* $x $+ 7 $< 2 $< 3.") == "1$+3$*$x$+7 $< 2 $< 3.");
203 }
204 SECTION("theory terms") {
205 REQUIRE(parse("&p{ } !! a.") == "&p { } !! a.");
206 REQUIRE(parse("&p{ } !! X.") == "&p { } !! X.");
207 REQUIRE(parse("&p{ } !! [].") == "&p { } !! [].");
208 REQUIRE(parse("&p{ } !! [1].") == "&p { } !! [1].");
209 REQUIRE(parse("&p{ } !! [1,2].") == "&p { } !! [1,2].");
210 REQUIRE(parse("&p{ } !! ().") == "&p { } !! ().");
211 REQUIRE(parse("&p{ } !! (a).") == "&p { } !! a.");
212 REQUIRE(parse("&p{ } !! (a,).") == "&p { } !! (a,).");
213 REQUIRE(parse("&p{ } !! {}.") == "&p { } !! {}.");
214 REQUIRE(parse("&p{ } !! f().") == "&p { } !! f.");
215 REQUIRE(parse("&p{ } !! f(a,1).") == "&p { } !! f(a,1).");
216 REQUIRE(parse("&p{ } !! 1 + (x + y * z).") == "&p { } !! (1 + (x + y * z)).");
217 }
218 }
219
220 TEST_CASE("add-ast-v2", "[clingo]") {
221 SECTION("statement") {
222 REQUIRE(solve("a.") == ModelVec({{Id("a")}}));
223 REQUIRE(solve("a. c. b :- a, c.") == ModelVec({{Id("a"), Id("b"), Id("c")}}));
224 REQUIRE(solve("#const a=10. p(a).") == ModelVec({{Function("p", {Number(10)})}}));
225 REQUIRE(solve("a. b. #show a/0.") == ModelVec({{Id("a")}}));
226 REQUIRE(solve("$a$=1. $b$=2. #show $a/0.") == ModelVec({{Function("$", {Id("a"), Number(1)})}}));
227 REQUIRE(solve("a. #show b : a.") == ModelVec({{Id("a"), Id("b")}}));
228 REQUIRE(solve("$a$=1. $b$=2. #show. #show $a.") == ModelVec({{Function("$", {Id("a"), Number(1)})}}));
229 REQUIRE(solve("#minimize{ 1:b; 2:a }. {a;b}. :- not a, not b.") == ModelVec({{Id("b")}}));
230 #ifdef WITH_LUA
231 // NOTE: at the moment it is not possible to add additional script code - it is simply ignored
232 REQUIRE(solve("#script (lua) function x() return 32; end #end. p(@x()).") == ModelVec({SymbolVector{}}));
233 #endif
234 REQUIRE(solve("#edge (u,v) : a. #edge (v,u) : b. {a;b}.") == ModelVec({{}, {Id("a")}, {Id("b")}}));
235 REQUIRE(solve("#theory x {}.") == ModelVec({SymbolVector{}}));
236 // these just test parsing...
237 REQUIRE(solve("#external a.") == ModelVec({SymbolVector{}}));
238 REQUIRE(solve("#heuristic a : b, c. [1@2,level]") == ModelVec({SymbolVector{}}));
239 REQUIRE(solve("#project a.") == ModelVec({SymbolVector{}}));
240 REQUIRE(solve("#project a/0.") == ModelVec({SymbolVector{}}));
241 }
242 SECTION("body literal") {
243 REQUIRE(solve("{a}. :-a.") == ModelVec({SymbolVector{}}));
244 REQUIRE(solve("{a}. :-not a.") == ModelVec({{Id("a")}}));
245 REQUIRE(solve("{a}. :-not not a.") == ModelVec({SymbolVector{}}));
246 REQUIRE(solve(":-a:b.") == ModelVec({}));
247 REQUIRE(solve(":-0{a:b;c}1. {a;b;c}.") == ModelVec({{Id("a"), Id("b"), Id("c")}}));
248 REQUIRE(solve(":-0#min{1,2:a,b;2:c}2. {a;b;c}.") == ModelVec({{}, {Id("a")}, {Id("b")}}));
__anonc0d366050b02(char const *name, int value) 249 auto c = [](char const *name, int value) { return Function("$", {Id(name), Number(value)}); };
250 REQUIRE(solve("1 $<= $x $<= 2. 1 $<= $y $<= 2. :- #disjoint {1:$x; 2:$y}.") == ModelVec({{c("x", 1), c("y", 1)}, {c("x", 2), c("y", 2)}}));
251 }
252 SECTION("head literal") {
253 REQUIRE(solve("a.") == ModelVec({{Id("a")}}));
254 REQUIRE(solve("not a.") == ModelVec({SymbolVector{}}));
255 REQUIRE(solve("not not a.") == ModelVec({}));
256 REQUIRE(solve("a:b;c.{b}.") == ModelVec({{Id("a"), Id("b")}, {Id("b"), Id("c")}, {Id("c")}}));
257 REQUIRE(solve("1{a:b;b}2.") == ModelVec({{Id("a"), Id("b")}, {Id("b")}}));
258 REQUIRE(solve("#min{1,2:a;2:c}1.") == ModelVec({{Id("a")}, {Id("a"), Id("c")}}));
259 }
260 SECTION("literal") {
261 REQUIRE(solve("a.") == ModelVec({{Id("a")}}));
262 REQUIRE(solve("1=1.") == ModelVec({SymbolVector{}}));
263 REQUIRE(solve("1!=1.") == ModelVec({}));
264 REQUIRE(solve("#true.") == ModelVec({SymbolVector{}}));
265 REQUIRE(solve("#false.") == ModelVec({}));
266 REQUIRE(solve("1 $< 2 $< 3.") == ModelVec({SymbolVector{}}));
267 REQUIRE(solve("2 $< 3 $< 1.") == ModelVec({}));
268 }
269 SECTION("terms") {
__anonc0d366050c02(char const *s) 270 auto t = [](char const *s) { return ModelVec({{parse_term(s)}}); };
__anonc0d366050d02(std::initializer_list<char const *> l) 271 auto tt = [](std::initializer_list<char const *> l) {
272 SymbolVector ret;
273 for (auto const &s : l) { ret.emplace_back(parse_term(s)); }
274 return ModelVec{ret};
275 };
276 REQUIRE(solve("p(a).") == t("p(a)"));
277 REQUIRE(solve("p(X) :- X=a.") == t("p(a)"));
278 REQUIRE(solve("p(-1).") == t("p(-1)"));
279 REQUIRE(solve("p(|1|).") == t("p(|1|)"));
280 REQUIRE(solve("p((3+2)).") == t("p(5)"));
281 REQUIRE(solve("p((3-2)).") == t("p(1)"));
282 REQUIRE(solve("p((3*2)).") == t("p(6)"));
283 REQUIRE(solve("p((7/2)).") == t("p(3)"));
284 REQUIRE(solve("p((7\\2)).") == t("p(1)"));
285 REQUIRE(solve("p((7?2)).") == t("p(7)"));
286 REQUIRE(solve("p((7^2)).") == t("p(5)"));
287 REQUIRE(solve("p(3..3).") == t("p(3)"));
288 REQUIRE(solve("p(a;b).") == tt({"p(a)", "p(b)"}));
289 REQUIRE(solve("p((),(1,),f(),f(1,2)).") == t("p((),(1,),f,f(1,2))"));
290 REQUIRE(solve("p((a,;b)).") == tt({"p(b)", "p((a,))"}));
291 REQUIRE(solve("12 $< 1 $+ 3 $* $x $+ 7 $< 17. 0 $<= x $<= 4.") == ModelVec({{Function("$", {Id("x"), Number(2)})}}));
292 }
293 SECTION("theory") {
294 char const *theory = R"(
295 #theory x {
296 t {
297 * : 1, binary, left;
298 ^ : 2, binary, right;
299 - : 3, unary
300 };
301 &a/0 : t, directive;
302 &b/0 : t, {=}, t, any
303 }.
304 )";
305 REQUIRE(parse("&p{ } !! 1 + (x + y * z).") == "&p { } !! (1 + (x + y * z)).");
306 REQUIRE(parse_theory("&a{}.", theory) == StringVec({"&a{}"}));
307 REQUIRE(parse_theory("&a{1,2,3:a,b}. {a;b}.", theory) == StringVec({"&a{1,2,3: a,b}"}));
308 REQUIRE(parse_theory("&b{} = a.", theory) == StringVec({"&b{}=a"}));
309 REQUIRE(parse_theory("&b{} = X:-X=1.", theory) == StringVec({"&b{}=1"}));
310 REQUIRE(parse_theory("&b{} = [].", theory) == StringVec({"&b{}=[]"}));
311 REQUIRE(parse_theory("&b{} = [1].", theory) == StringVec({"&b{}=[1]"}));
312 REQUIRE(parse_theory("&b{} = [1,2].", theory) == StringVec({"&b{}=[1,2]"}));
313 REQUIRE(parse_theory("&b{} = ().", theory) == StringVec({"&b{}=()"}));
314 REQUIRE(parse_theory("&b{} = (a).", theory) == StringVec({"&b{}=a"}));
315 REQUIRE(parse_theory("&b{} = (a,).", theory) == StringVec({"&b{}=(a,)"}));
316 REQUIRE(parse_theory("&b{} = {}.", theory) == StringVec({"&b{}={}"}));
317 REQUIRE(parse_theory("&b{} = f().", theory) == StringVec({"&b{}=f()"}));
318 REQUIRE(parse_theory("&b{} = f(a,1).", theory) == StringVec({"&b{}=f(a,1)"}));
319 REQUIRE(parse_theory("&b{} = a*x.", theory) == StringVec({"&b{}=(a*x)"}));
320 REQUIRE(parse_theory("&b{} = -a*x*y^z^u.", theory) == StringVec({"&b{}=(((-a)*x)*(y^(z^u)))"}));
321 REQUIRE(parse_theory("&b{} = -(a*x*y^z^u).", theory) == StringVec({"&b{}=(-((a*x)*(y^(z^u))))"}));
322 }
323 }
324
325 TEST_CASE("build-ast-v2", "[clingo]") {
326 Location loc{"<string>", "<string>", 1, 1, 1, 1};
327 SECTION("string array") {
328 auto sym = AST::Node{AST::Type::SymbolicTerm, loc, Function("a", {})};
329 auto lst = std::vector<char const *>{"x", "y", "z"};
330 auto tue = AST::Node{AST::Type::TheoryUnparsedTermElement, lst, sym};
331
332 auto seq = tue.get(AST::Attribute::Operators).get<AST::StringVector>();
333 REQUIRE(!seq.empty());
334 REQUIRE(seq.size() == 3);
335 REQUIRE(cmp(seq, lst));
336 seq.insert(seq.begin(), "i");
337 REQUIRE(std::strcmp(seq[0], "i") == 0);
338 REQUIRE(seq.size() == 4);
339 seq.insert(seq.begin(), seq[3]);
340 REQUIRE(std::strcmp(seq[0], "z") == 0);
341 seq.erase(seq.begin());
342 seq.erase(seq.begin());
343 REQUIRE(cmp(seq, lst));
344 tue.set(AST::Attribute::Operators, seq);
345 REQUIRE(cmp(seq, lst));
346 tue.set(AST::Attribute::Operators, tue.deep_copy().get(AST::Attribute::Operators));
347 REQUIRE(cmp(seq, lst));
348 tue.set(AST::Attribute::Operators, tue.copy().get(AST::Attribute::Operators));
349 REQUIRE(cmp(seq, lst));
350 }
351 SECTION("ast array") {
352 auto lst = std::vector<AST::Node>{
353 AST::Node(AST::Type::Id, loc, "x"),
354 AST::Node(AST::Type::Id, loc, "y"),
355 AST::Node(AST::Type::Id, loc, "z")};
356 auto prg = AST::Node(AST::Type::Program, loc, "p", lst);
357 auto seq = prg.get(AST::Attribute::Parameters).get<AST::NodeVector>();
358 REQUIRE(seq.size() == 3);
359 REQUIRE(vec(seq) == lst);
360 REQUIRE(seq[0] == lst[0]);
361 seq.insert(seq.begin(), AST::Node(AST::Type::Id, loc, "i"));
362 lst.insert(lst.begin(), AST::Node(AST::Type::Id, loc, "i"));
363 REQUIRE(vec(seq) == lst);
364 seq.insert(seq.begin(), seq[3]);
365 lst.insert(lst.begin(), lst[3]);
366 REQUIRE(vec(seq) == lst);
367 seq.erase(seq.begin() + 2);
368 lst.erase(lst.begin() + 2);
369 REQUIRE(vec(seq) == lst);
370 }
371 SECTION("ast compare") {
372 Location alt{"<string>", "<string>", 1, 1, 1, 2};
373 auto x = AST::Node(AST::Type::Id, loc, "x");
374 auto y = AST::Node(AST::Type::Id, alt, "x");
375 auto z = AST::Node(AST::Type::Id, loc, "z");
376 REQUIRE(x == y);
377 REQUIRE(x == x);
378 REQUIRE(x != z);
379 REQUIRE(x.hash() == x.hash());
380 REQUIRE(x.hash() == y.hash());
381 REQUIRE(x.hash() != z.hash());
382 REQUIRE(x < z);
383 REQUIRE(x <= z);
384 REQUIRE(z > x);
385 REQUIRE(z >= x);
386 REQUIRE(y <= x);
387 REQUIRE(y >= x);
388 REQUIRE(x <= y);
389 REQUIRE(x >= y);
390 }
391 }
392
393 TEST_CASE("unpool-ast-v2", "[clingo]") {
394 SECTION("terms") {
395 REQUIRE(unpool("a(f(1;2)).") ==
396 "a(f(1)).\n"
397 "a(f(2)).");
398 REQUIRE(unpool("a((1,;2,)).") ==
399 "a((1,)).\n"
400 "a((2,)).");
401 REQUIRE(unpool("a((1;2)).") ==
402 "a(1).\n"
403 "a(2).");
404 REQUIRE(unpool("a((X;1)).") ==
405 "a(X).\n"
406 "a(1).");
407 REQUIRE(unpool("a((1;2;3;4;5)).") ==
408 "a(1).\n"
409 "a(2).\n"
410 "a(3).\n"
411 "a(4).\n"
412 "a(5).");
413 REQUIRE(unpool("a(|X;Y|).") ==
414 "a(|X|).\n"
415 "a(|Y|).");
416 REQUIRE(unpool("a(1+(2;3)).") ==
417 "a((1+2)).\n"
418 "a((1+3)).");
419 REQUIRE(unpool("a((1;2)+3).") ==
420 "a((1+3)).\n"
421 "a((2+3)).");
422 REQUIRE(unpool("a((1;2)+(3;4)).") ==
423 "a((1+3)).\n"
424 "a((1+4)).\n"
425 "a((2+3)).\n"
426 "a((2+4)).");
427 REQUIRE(unpool("a((1;2)..(3;4)).") ==
428 "a((1..3)).\n"
429 "a((1..4)).\n"
430 "a((2..3)).\n"
431 "a((2..4)).");
432 }
433 SECTION("csp") {
434 REQUIRE(unpool("$a(1;2) $< a(3;4)$*$b(5;6).") ==
435 "1$*$a(1) $< a(3)$*$b(5).\n"
436 "1$*$a(1) $< a(3)$*$b(6).\n"
437 "1$*$a(1) $< a(4)$*$b(5).\n"
438 "1$*$a(1) $< a(4)$*$b(6).\n"
439 "1$*$a(2) $< a(3)$*$b(5).\n"
440 "1$*$a(2) $< a(3)$*$b(6).\n"
441 "1$*$a(2) $< a(4)$*$b(5).\n"
442 "1$*$a(2) $< a(4)$*$b(6).");
443 REQUIRE(unpool("#disjoint { a(1;2): $a(3;4): a(5;6) }.") ==
444 "#false :- not #disjoint { "
445 "a(1):1$*$a(3): a(5); "
446 "a(1):1$*$a(3): a(6); "
447 "a(1):1$*$a(4): a(5); "
448 "a(1):1$*$a(4): a(6); "
449 "a(2):1$*$a(3): a(5); "
450 "a(2):1$*$a(3): a(6); "
451 "a(2):1$*$a(4): a(5); "
452 "a(2):1$*$a(4): a(6) "
453 "}.");
454 }
455 SECTION("head literal") {
456 REQUIRE(unpool("a(1;2).") ==
457 "a(1).\n"
458 "a(2).");
459 REQUIRE(unpool("a(1;2):a(3).") ==
460 "a(1): a(3).\n"
461 "a(2): a(3).");
462 // Note: I hope that this one matches what clingo currently does
463 // (in any case, it won't affect existing programs)
464 REQUIRE(unpool("a(1):a(2;3).") == "a(1): a(2); a(1): a(3).");
465 REQUIRE(unpool("a(1;2):a(3;4).") ==
466 "a(1): a(3); a(1): a(4).\n"
467 "a(2): a(3); a(1): a(4).\n"
468 "a(1): a(3); a(2): a(4).\n"
469 "a(2): a(3); a(2): a(4).");
470 REQUIRE(unpool("(1;2) { a(2;3): a(4;5) } (6;7).") ==
471 "1 <= { a(2): a(4); a(2): a(5); a(3): a(4); a(3): a(5) } <= 6.\n"
472 "1 <= { a(2): a(4); a(2): a(5); a(3): a(4); a(3): a(5) } <= 7.\n"
473 "2 <= { a(2): a(4); a(2): a(5); a(3): a(4); a(3): a(5) } <= 6.\n"
474 "2 <= { a(2): a(4); a(2): a(5); a(3): a(4); a(3): a(5) } <= 7.");
475 REQUIRE(unpool("(1;2) #min { (2;3): a(4;5): a(6;7) } (8;9).") ==
476 "1 <= #min { 2: a(4): a(6); 2: a(4): a(7); 2: a(5): a(6); 2: a(5): a(7); 3: a(4): a(6); 3: a(4): a(7); 3: a(5): a(6); 3: a(5): a(7) } <= 8.\n"
477 "1 <= #min { 2: a(4): a(6); 2: a(4): a(7); 2: a(5): a(6); 2: a(5): a(7); 3: a(4): a(6); 3: a(4): a(7); 3: a(5): a(6); 3: a(5): a(7) } <= 9.\n"
478 "2 <= #min { 2: a(4): a(6); 2: a(4): a(7); 2: a(5): a(6); 2: a(5): a(7); 3: a(4): a(6); 3: a(4): a(7); 3: a(5): a(6); 3: a(5): a(7) } <= 8.\n"
479 "2 <= #min { 2: a(4): a(6); 2: a(4): a(7); 2: a(5): a(6); 2: a(5): a(7); 3: a(4): a(6); 3: a(4): a(7); 3: a(5): a(6); 3: a(5): a(7) } <= 9.");
480 REQUIRE(unpool("&a(1;2) { 1 : a(3;4), a(5;6) }.") ==
481 "&a(1) { 1: a(3), a(5); 1: a(4), a(5); 1: a(3), a(6); 1: a(4), a(6) }.\n"
482 "&a(2) { 1: a(3), a(5); 1: a(4), a(5); 1: a(3), a(6); 1: a(4), a(6) }.");
483 REQUIRE(unpool("&a(0) { 1 : X=(1;2;3) }.") ==
484 "&a(0) { 1: X = 1; 1: X = 2; 1: X = 3 }.");
485 REQUIRE(unpool("(1;2) < (3;4).") ==
486 "1 < 3.\n"
487 "1 < 4.\n"
488 "2 < 3.\n"
489 "2 < 4.");
490 }
491 SECTION("body literal") {
492 REQUIRE(unpool(":- a(1;2).") ==
493 "#false :- a(1).\n"
494 "#false :- a(2).");
495 REQUIRE(unpool(":- a(1;2):a(3).") ==
496 "#false :- a(1): a(3).\n"
497 "#false :- a(2): a(3).");
498 REQUIRE(unpool(":- a(1):a(2;3).") ==
499 "#false :- a(1): a(2); a(1): a(3).");
500 REQUIRE(unpool(":- a(1;2):a(3;4).") ==
501 "#false :- a(1): a(3); a(1): a(4).\n"
502 "#false :- a(2): a(3); a(1): a(4).\n"
503 "#false :- a(1): a(3); a(2): a(4).\n"
504 "#false :- a(2): a(3); a(2): a(4).");
505 REQUIRE(unpool(":- (1;2) { a(2;3): a(4;5) } (6;7).") ==
506 "#false :- 1 <= { a(2): a(4); a(2): a(5); a(3): a(4); a(3): a(5) } <= 6.\n"
507 "#false :- 1 <= { a(2): a(4); a(2): a(5); a(3): a(4); a(3): a(5) } <= 7.\n"
508 "#false :- 2 <= { a(2): a(4); a(2): a(5); a(3): a(4); a(3): a(5) } <= 6.\n"
509 "#false :- 2 <= { a(2): a(4); a(2): a(5); a(3): a(4); a(3): a(5) } <= 7.");
510 REQUIRE(unpool(":- (1;2) #min { (2;3): a(4;5), a(6;7) } (8;9).") ==
511 "#false :- 1 <= #min { 2: a(4), a(6); 2: a(5), a(6); 2: a(4), a(7); 2: a(5), a(7); 3: a(4), a(6); 3: a(5), a(6); 3: a(4), a(7); 3: a(5), a(7) } <= 8.\n"
512 "#false :- 1 <= #min { 2: a(4), a(6); 2: a(5), a(6); 2: a(4), a(7); 2: a(5), a(7); 3: a(4), a(6); 3: a(5), a(6); 3: a(4), a(7); 3: a(5), a(7) } <= 9.\n"
513 "#false :- 2 <= #min { 2: a(4), a(6); 2: a(5), a(6); 2: a(4), a(7); 2: a(5), a(7); 3: a(4), a(6); 3: a(5), a(6); 3: a(4), a(7); 3: a(5), a(7) } <= 8.\n"
514 "#false :- 2 <= #min { 2: a(4), a(6); 2: a(5), a(6); 2: a(4), a(7); 2: a(5), a(7); 3: a(4), a(6); 3: a(5), a(6); 3: a(4), a(7); 3: a(5), a(7) } <= 9.");
515 REQUIRE(unpool(":- &a(1;2) { 1 : a(3;4), a(5;6) }.") ==
516 "#false :- &a(1) { 1: a(3), a(5); 1: a(4), a(5); 1: a(3), a(6); 1: a(4), a(6) }.\n"
517 "#false :- &a(2) { 1: a(3), a(5); 1: a(4), a(5); 1: a(3), a(6); 1: a(4), a(6) }.");
518 REQUIRE(unpool(":- (1;2) < (3;4).") ==
519 "#false :- 1 < 3.\n"
520 "#false :- 1 < 4.\n"
521 "#false :- 2 < 3.\n"
522 "#false :- 2 < 4.");
523 }
524 SECTION("statements") {
525 REQUIRE(unpool("a(1;2) :- a(3;4); a(5;6).") ==
526 "a(1) :- a(3); a(5).\n"
527 "a(2) :- a(3); a(5).\n"
528 "a(1) :- a(4); a(5).\n"
529 "a(2) :- a(4); a(5).\n"
530 "a(1) :- a(3); a(6).\n"
531 "a(2) :- a(3); a(6).\n"
532 "a(1) :- a(4); a(6).\n"
533 "a(2) :- a(4); a(6).");
534 REQUIRE(unpool("#show a(1;2) : a(3;4).") ==
535 "#show a(1) : a(3).\n"
536 "#show a(2) : a(3).\n"
537 "#show a(1) : a(4).\n"
538 "#show a(2) : a(4).");
539 REQUIRE(unpool(":~ a(1;2). [(3;4)@(5;6),(7;8)]") ==
540 ":~ a(1). [3@5,7]\n"
541 ":~ a(1). [3@5,8]\n"
542 ":~ a(1). [3@6,7]\n"
543 ":~ a(1). [3@6,8]\n"
544 ":~ a(1). [4@5,7]\n"
545 ":~ a(1). [4@5,8]\n"
546 ":~ a(1). [4@6,7]\n"
547 ":~ a(1). [4@6,8]\n"
548 ":~ a(2). [3@5,7]\n"
549 ":~ a(2). [3@5,8]\n"
550 ":~ a(2). [3@6,7]\n"
551 ":~ a(2). [3@6,8]\n"
552 ":~ a(2). [4@5,7]\n"
553 ":~ a(2). [4@5,8]\n"
554 ":~ a(2). [4@6,7]\n"
555 ":~ a(2). [4@6,8]");
556 REQUIRE(unpool("#external a(1;2) : a(3;4). [(5;6)]") ==
557 "#external a(1) : a(3). [5]\n"
558 "#external a(1) : a(3). [6]\n"
559 "#external a(2) : a(3). [5]\n"
560 "#external a(2) : a(3). [6]\n"
561 "#external a(1) : a(4). [5]\n"
562 "#external a(1) : a(4). [6]\n"
563 "#external a(2) : a(4). [5]\n"
564 "#external a(2) : a(4). [6]");
565 REQUIRE(unpool("#edge ((1;2),(3;4)) : a(5;6).") ==
566 "#edge (1,3) : a(5).\n"
567 "#edge (1,4) : a(5).\n"
568 "#edge (2,3) : a(5).\n"
569 "#edge (2,4) : a(5).\n"
570 "#edge (1,3) : a(6).\n"
571 "#edge (1,4) : a(6).\n"
572 "#edge (2,3) : a(6).\n"
573 "#edge (2,4) : a(6).");
574 REQUIRE(unpool("#heuristic a(1;2) : a(3;4). [a(5;6)@a(7;8),a(9;10)]") ==
575 "#heuristic a(1) : a(3). [a(5)@a(7),a(9)]\n"
576 "#heuristic a(1) : a(3). [a(5)@a(7),a(10)]\n"
577 "#heuristic a(1) : a(3). [a(5)@a(8),a(9)]\n"
578 "#heuristic a(1) : a(3). [a(5)@a(8),a(10)]\n"
579 "#heuristic a(1) : a(3). [a(6)@a(7),a(9)]\n"
580 "#heuristic a(1) : a(3). [a(6)@a(7),a(10)]\n"
581 "#heuristic a(1) : a(3). [a(6)@a(8),a(9)]\n"
582 "#heuristic a(1) : a(3). [a(6)@a(8),a(10)]\n"
583 "#heuristic a(2) : a(3). [a(5)@a(7),a(9)]\n"
584 "#heuristic a(2) : a(3). [a(5)@a(7),a(10)]\n"
585 "#heuristic a(2) : a(3). [a(5)@a(8),a(9)]\n"
586 "#heuristic a(2) : a(3). [a(5)@a(8),a(10)]\n"
587 "#heuristic a(2) : a(3). [a(6)@a(7),a(9)]\n"
588 "#heuristic a(2) : a(3). [a(6)@a(7),a(10)]\n"
589 "#heuristic a(2) : a(3). [a(6)@a(8),a(9)]\n"
590 "#heuristic a(2) : a(3). [a(6)@a(8),a(10)]\n"
591 "#heuristic a(1) : a(4). [a(5)@a(7),a(9)]\n"
592 "#heuristic a(1) : a(4). [a(5)@a(7),a(10)]\n"
593 "#heuristic a(1) : a(4). [a(5)@a(8),a(9)]\n"
594 "#heuristic a(1) : a(4). [a(5)@a(8),a(10)]\n"
595 "#heuristic a(1) : a(4). [a(6)@a(7),a(9)]\n"
596 "#heuristic a(1) : a(4). [a(6)@a(7),a(10)]\n"
597 "#heuristic a(1) : a(4). [a(6)@a(8),a(9)]\n"
598 "#heuristic a(1) : a(4). [a(6)@a(8),a(10)]\n"
599 "#heuristic a(2) : a(4). [a(5)@a(7),a(9)]\n"
600 "#heuristic a(2) : a(4). [a(5)@a(7),a(10)]\n"
601 "#heuristic a(2) : a(4). [a(5)@a(8),a(9)]\n"
602 "#heuristic a(2) : a(4). [a(5)@a(8),a(10)]\n"
603 "#heuristic a(2) : a(4). [a(6)@a(7),a(9)]\n"
604 "#heuristic a(2) : a(4). [a(6)@a(7),a(10)]\n"
605 "#heuristic a(2) : a(4). [a(6)@a(8),a(9)]\n"
606 "#heuristic a(2) : a(4). [a(6)@a(8),a(10)]");
607 REQUIRE(unpool("#project a(1;2) : a(3;4).") ==
608 "#project a(1) : a(3).\n"
609 "#project a(2) : a(3).\n"
610 "#project a(1) : a(4).\n"
611 "#project a(2) : a(4).");
612 }
613 SECTION("options") {
614 std::vector<AST::Node> prg;
__anonc0d366050e02(AST::Node &&ast) 615 AST::parse_string(":- a(1;2): a(3;4).", [&prg](AST::Node &&ast) { prg.emplace_back(std::move(ast)); });
616 AST::Node lit = *prg.back().get(AST::Attribute::Body).get<AST::NodeVector>().begin();
__anonc0d366050f02(bool other, bool condition) 617 auto unpool = [&lit](bool other, bool condition) {
618 std::vector<std::string> ret;
619 for (auto &ast : lit.unpool(other, condition)) {
620 ret.emplace_back(ast.to_string());
621 }
622 return ret;
623 };
624
625 REQUIRE(unpool(true, true) == std::vector<std::string>{
626 "a(1): a(3)",
627 "a(1): a(4)",
628 "a(2): a(3)",
629 "a(2): a(4)"});
630 REQUIRE(unpool(false, true) == std::vector<std::string>{
631 "a(1;2): a(3)",
632 "a(1;2): a(4)"});
633 REQUIRE(unpool(true, false) == std::vector<std::string>{
634 "a(1): a(3;4)",
635 "a(2): a(3;4)"});
636 REQUIRE(unpool(false, false) == std::vector<std::string>{
637 "a(1;2): a(3;4)"});
638 }
639 }
640
641 } } // namespace Test Clingo
642