1 //
2 // Copyright (c) 2015-2017 Benjamin Kaufmann
3 //
4 // This file is part of Potassco.
5 //
6 // Permission is hereby granted, free of charge, to any person obtaining a copy
7 // of this software and associated documentation files (the "Software"), to
8 // deal in the Software without restriction, including without limitation the
9 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
10 // sell copies of the Software, and to permit persons to whom the Software is
11 // furnished to do so, subject to the following conditions:
12 //
13 // The above copyright notice and this permission notice shall be included in
14 // all copies or substantial portions of the Software.
15 //
16 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
21 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
22 // IN THE SOFTWARE.
23 //
24
25 #include "catch.hpp"
26 #include "test_common.h"
27 #include <potassco/convert.h>
28 #include <sstream>
29 #include <cstring>
30 #include <map>
31 #include <unordered_map>
32 namespace Potassco {
33 namespace Test {
34 namespace Smodels {
35 using AtomTab = std::vector<std::string>;
36 using LitVec = std::vector<Lit_t>;
37 using RawRule = std::vector<int>;
finalize(std::stringstream & str,const AtomTab & atoms=AtomTab (),const std::string & bpos="",const std::string & bneg="1")38 static void finalize(std::stringstream& str, const AtomTab& atoms = AtomTab(), const std::string& bpos = "", const std::string& bneg = "1") {
39 str << "0\n";
40 for (const auto& s : atoms) str << s << "\n";
41 str << "0\nB+\n" << bpos;
42 if (!bpos.empty() && bpos.back() != '\n') str << "\n";
43 str << "0\nB-\n";
44 str << bneg;
45 if (!bneg.empty() && bneg.back() != '\n') str << "\n";
46 str << "0\n1\n";
47 }
48
49 enum class Rule_t : unsigned {
50 Basic = 1, Cardinality = 2, Choice = 3, Weight = 5, Optimize = 6, Disjunctive = 8,
51 ClaspAssignExt = 91, ClaspReleaseExt = 92
52 };
53
54 class ReadObserver : public Test::ReadObserver {
55 public:
rule(Head_t ht,const AtomSpan & head,const LitSpan & body)56 virtual void rule(Head_t ht, const AtomSpan& head, const LitSpan& body) override {
57 if (empty(head)) {
58 if (ht == Head_t::Choice) return;
59 compute.push_back(-lit(body[0]));
60 }
61 else {
62 Rule_t rt = Rule_t::Basic;
63 std::vector<int> r(1, at(head, 0));
64 if (size(head) > 1 || ht == Head_t::Choice) {
65 r[0] = static_cast<int>(size(head));
66 r.insert(r.end(), begin(head), end(head));
67 rt = ht == Head_t::Choice ? Rule_t::Choice : Rule_t::Disjunctive;
68 }
69 r.insert(r.end(), begin(body), end(body));
70 rules[rt].push_back(std::move(r));
71 }
72 }
rule(Head_t ht,const AtomSpan & head,Weight_t bound,const WeightLitSpan & body)73 virtual void rule(Head_t ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) override {
74 int rt = isSmodelsRule(ht, head, bound, body);
75 REQUIRE(rt != 0);
76 REQUIRE(size(head) == 1);
77 std::vector<int> r(1, at(head, 0));
78 r.push_back(bound);
79 for (auto&& x : body) {
80 r.push_back(lit(x));
81 if (rt == (int)Rule_t::Weight) r.push_back(weight(x));
82 }
83 rules[static_cast<Rule_t>(rt)].push_back(std::move(r));
84 }
minimize(Weight_t prio,const WeightLitSpan & lits)85 virtual void minimize(Weight_t prio, const WeightLitSpan& lits) override {
86 std::vector<int> r; r.reserve((size(lits) * 2) + 1);
87 r.push_back(prio);
88 for (auto&& x : lits) {
89 r.push_back(lit(x));
90 r.push_back(weight(x));
91 }
92 rules[Rule_t::Optimize].push_back(std::move(r));
93 }
project(const AtomSpan &)94 virtual void project(const AtomSpan&) override {}
output(const StringSpan & str,const LitSpan & cond)95 virtual void output(const StringSpan& str, const LitSpan& cond) override {
96 REQUIRE(size(cond) == 1);
97 atoms[*begin(cond)].assign(begin(str), end(str));
98 }
99
external(Atom_t a,Value_t v)100 virtual void external(Atom_t a, Value_t v) override {
101 if (v != Value_t::Release) {
102 rules[Rule_t::ClaspAssignExt].push_back(RawRule{static_cast<int>(a), static_cast<int>(v)});
103 }
104 else {
105 rules[Rule_t::ClaspReleaseExt].push_back(RawRule{static_cast<int>(a)});
106 }
107 }
assume(const LitSpan &)108 virtual void assume(const LitSpan&) override {}
109
110 using RuleMap = std::map<Rule_t, std::vector<std::vector<int> > >;
111 using AtomMap = std::unordered_map<int, std::string>;
112 RuleMap rules;
113 LitVec compute;
114 AtomMap atoms;
115 };
116 TEST_CASE("Smodels reader ", "[smodels]") {
117 std::stringstream input;
118 ReadObserver observer;
119 SECTION("read empty") {
120 finalize(input);
121 REQUIRE(Potassco::readSmodels(input, observer) == 0);
122 REQUIRE(observer.nStep == 1);
123 REQUIRE(observer.incremental == false);
124 REQUIRE(observer.compute.size() == 1);
125 REQUIRE(observer.compute[0] == -1);
126 }
127 SECTION("read basic rule") {
128 input << "1 2 4 2 4 2 3 5\n";
129 finalize(input);
130 REQUIRE(Potassco::readSmodels(input, observer) == 0);
131 REQUIRE(observer.rules[Rule_t::Basic].size() == 1);
132 RawRule exp = {2, -4, -2, 3, 5};
133 REQUIRE(observer.rules[Rule_t::Basic][0] == exp);
134 }
135 SECTION("read choice/disjunctive rule") {
136 input << "3 2 3 4 2 1 5 6\n";
137 input << "8 2 3 4 2 1 5 6\n";
138 finalize(input);
139 REQUIRE(Potassco::readSmodels(input, observer) == 0);
140 REQUIRE(observer.rules[Rule_t::Choice].size() == 1);
141 REQUIRE(observer.rules[Rule_t::Disjunctive].size() == 1);
142
143 RawRule r1 = {2, 3, 4, -5, 6};
144 REQUIRE(observer.rules[Rule_t::Choice][0] == r1);
145 REQUIRE(observer.rules[Rule_t::Disjunctive][0] == r1);
146 }
147 SECTION("read card/weight rule") {
148 input << "2 2 2 1 1 3 4\n";
149 input << "5 3 3 3 1 4 5 6 1 2 3\n";
150 finalize(input);
151 REQUIRE(Potassco::readSmodels(input, observer) == 0);
152 REQUIRE(observer.rules[Rule_t::Cardinality].size() == 1);
153 REQUIRE(observer.rules[Rule_t::Weight].size() == 1);
154
155 RawRule r1 = {2, 1, -3, 4};
156 RawRule r2 = {3, 3, -4, 1, 5, 2, 6, 3};
157 REQUIRE(observer.rules[Rule_t::Cardinality][0] == r1);
158 REQUIRE(observer.rules[Rule_t::Weight][0] == r2);
159 }
160 SECTION("read min rule") {
161 input << "6 0 3 1 4 5 6 1 3 2\n";
162 input << "6 0 3 1 4 5 6 1 3 2\n";
163 finalize(input);
164 REQUIRE(Potassco::readSmodels(input, observer) == 0);
165 REQUIRE(observer.rules[Rule_t::Optimize].size() == 2);
166 RawRule r = {0, -4, 1, 5, 3, 6, 2};
167 REQUIRE(observer.rules[Rule_t::Optimize][0] == r);
168 r[0] = 1;
169 REQUIRE(observer.rules[Rule_t::Optimize][1] == r);
170 }
171 SECTION("read atom names") {
172 finalize(input, {"1 Foo", "2 Bar", "3 Test(X,Y)"});
173 REQUIRE(Potassco::readSmodels(input, observer) == 0);
174 REQUIRE(observer.atoms.size() == 3);
175 REQUIRE(observer.atoms[1] == "Foo");
176 REQUIRE(observer.atoms[2] == "Bar");
177 REQUIRE(observer.atoms[3] == "Test(X,Y)");
178 }
179 SECTION("read compute") {
180 finalize(input, {}, "2\n3", "1\n4\n5");
181 REQUIRE(Potassco::readSmodels(input, observer) == 0);
182 REQUIRE(observer.compute.size() == 5);
183 const auto& c = observer.compute;
184 REQUIRE(std::find(c.begin(), c.end(), 2) != c.end());
185 REQUIRE(std::find(c.begin(), c.end(), 3) != c.end());
186 REQUIRE(std::find(c.begin(), c.end(), -1) != c.end());
187 REQUIRE(std::find(c.begin(), c.end(), -4) != c.end());
188 REQUIRE(std::find(c.begin(), c.end(), -5) != c.end());
189 }
190 SECTION("read external") {
191 input << "0\n0\nB+\n0\nB-\n0\nE\n1\n2\n4\n0\n1\n";
192 REQUIRE(Potassco::readSmodels(input, observer) == 0);
193 REQUIRE(observer.rules[Rule_t::ClaspAssignExt].size() == 3);
194 REQUIRE(observer.rules[Rule_t::ClaspAssignExt][0] == RawRule({1, 0}));
195 REQUIRE(observer.rules[Rule_t::ClaspAssignExt][1] == RawRule({2, 0}));
196 REQUIRE(observer.rules[Rule_t::ClaspAssignExt][2] == RawRule({4, 0}));
197 }
198 }
199
200 TEST_CASE("SmodelsExtReader ", "[smodels][smodels_ext]") {
201 std::stringstream input;
202 ReadObserver observer;
203 SmodelsInput::Options opts; opts.enableClaspExt();
204 SECTION("read incremental") {
205 input << "90 0\n";
206 finalize(input);
207 input << "90 0\n";
208 finalize(input);
209 REQUIRE(Potassco::readSmodels(input, observer, 0, opts) == 0);
210 REQUIRE(observer.incremental == true);
211 REQUIRE(observer.nStep == 2);
212 }
213 SECTION("read external") {
214 input << "91 2 0\n";
215 input << "91 3 1\n";
216 input << "91 4 2\n";
217 finalize(input);
218 REQUIRE(Potassco::readSmodels(input, observer, 0, opts) == 0);
219 REQUIRE(observer.rules[Rule_t::ClaspAssignExt].size() == 3);
220 REQUIRE(observer.rules[Rule_t::ClaspAssignExt][0] == RawRule({2, static_cast<int>(Value_t::False)}));
221 REQUIRE(observer.rules[Rule_t::ClaspAssignExt][1] == RawRule({3, static_cast<int>(Value_t::True)}));
222 REQUIRE(observer.rules[Rule_t::ClaspAssignExt][2] == RawRule({4, static_cast<int>(Value_t::Free)}));
223 }
224 SECTION("read release") {
225 input << "91 2 0\n";
226 input << "92 2\n";
227 finalize(input);
228 REQUIRE(Potassco::readSmodels(input, observer, 0, opts) == 0);
229 REQUIRE(observer.rules[Rule_t::ClaspAssignExt].size() == 1);
230 REQUIRE(observer.rules[Rule_t::ClaspReleaseExt].size() == 1);
231 REQUIRE(observer.rules[Rule_t::ClaspAssignExt][0] == RawRule({2, static_cast<int>(Value_t::False)}));
232 REQUIRE(observer.rules[Rule_t::ClaspReleaseExt][0] == RawRule({2}));
233 }
234 }
235
236 TEST_CASE("Write smodels", "[smodels]") {
237 std::stringstream str, exp;
238 SmodelsOutput writer(str, false, 0);
239 ReadObserver observer;
240 writer.initProgram(false);
241 SECTION("empty program is valid") {
242 writer.endStep();
243 exp << "0\n0\nB+\n0\nB-\n0\n1\n";
244 REQUIRE(str.str() == exp.str());
245 }
246 SECTION("body literals are correctly reordered") {
247 Atom_t a = 1;
248 Vec<Lit_t> body ={2, -3, -4, 5};
249 writer.rule(Head_t::Disjunctive, toSpan(&a, 1), toSpan(body));
250 writer.endStep();
251 REQUIRE(readSmodels(str, observer) == 0);
252 REQUIRE(observer.rules[Rule_t::Basic].size() == 1);
253 RawRule r ={1, -3, -4, 2, 5};
254 REQUIRE(observer.rules[Rule_t::Basic][0] == r);
255 }
256 SECTION("body literals with weights are correctly reordered") {
257 Atom_t a = 1;
258 Vec<WeightLit_t> body ={{2, 2}, {-3, 1}, {-4, 3}, {5, 4}};
259 writer.rule(Head_t::Disjunctive, toSpan(&a, 1), 4, toSpan(body));
260 writer.endStep();
261 REQUIRE(readSmodels(str, observer) == 0);
262 REQUIRE(observer.rules[Rule_t::Weight].size() == 1);
263 RawRule r ={1, 4, -3, 1, -4, 3, 2, 2, 5, 4};
264 REQUIRE(observer.rules[Rule_t::Weight][0] == r);
265 }
266 SECTION("weights are removed from count bodies") {
267 Atom_t a = 1;
268 Vec<WeightLit_t> body ={{2, 1}, {-3, 1}, {-4, 1}, {5, 1}};
269 writer.rule(Head_t::Disjunctive, toSpan(&a, 1), 3, toSpan(body));
270 writer.endStep();
271 REQUIRE(readSmodels(str, observer) == 0);
272 REQUIRE(observer.rules[Rule_t::Cardinality].size() == 1);
273 RawRule r ={1, 3, -3, -4, 2, 5};
274 REQUIRE(observer.rules[Rule_t::Cardinality][0] == r);
275 }
276 SECTION("all head atoms are written") {
277 Vec<Atom_t> atoms ={1, 2, 3, 4};
278 writer.rule(Head_t::Disjunctive, toSpan(atoms), toSpan<Lit_t>());
279 writer.rule(Head_t::Choice, toSpan(atoms), toSpan<Lit_t>());
280 writer.endStep();
281 REQUIRE(readSmodels(str, observer) == 0);
282 REQUIRE(observer.rules[Rule_t::Disjunctive].size() == 1);
283 REQUIRE(observer.rules[Rule_t::Choice].size() == 1);
284 RawRule r ={4, 1, 2, 3, 4};
285 REQUIRE(observer.rules[Rule_t::Disjunctive][0] == r);
286 REQUIRE(observer.rules[Rule_t::Choice][0] == r);
287 }
288 SECTION("minimize rules are written without priority") {
289 Vec<WeightLit_t> body ={{2, 2}, {-3, 1}, {-4, 3}, {5, 4}};
290 writer.minimize(10, toSpan(body));
291 writer.endStep();
292 REQUIRE(readSmodels(str, observer) == 0);
293 REQUIRE(observer.rules[Rule_t::Optimize].size() == 1);
294 RawRule r ={0, -3, 1, -4, 3, 2, 2, 5, 4};
295 REQUIRE(observer.rules[Rule_t::Optimize][0] == r);
296 }
297 SECTION("output is written to symbol table") {
298 Lit_t a = 1;
299 std::string an = "Hallo";
300 writer.output(toSpan(an), toSpan(&a, 1));
301 writer.endStep();
302 REQUIRE(readSmodels(str, observer) == 0);
303 REQUIRE(observer.atoms[a] == an);
304 }
305 SECTION("output must be added after rules") {
306 Lit_t a = 1;
307 std::string an = "Hallo";
308 writer.output(toSpan(an), toSpan(&a, 1));
309 Atom_t b = 2;
310 REQUIRE_THROWS(writer.rule(Head_t::Disjunctive, toSpan(&b, 1), toSpan<Lit_t>()));
311 }
312 SECTION("compute statement is written via assume") {
313 Atom_t a = 1;
314 Vec<Lit_t> body ={2, -3, -4, 5};
315 writer.rule(Head_t::Disjunctive, toSpan(&a, 1), toSpan(body));
316 Lit_t na = -1;
317 writer.assume(toSpan(&na, 1));
318 writer.endStep();
319 REQUIRE(readSmodels(str, observer) == 0);
320 REQUIRE(observer.rules[Rule_t::Basic].size() == 1);
321 RawRule r ={1, -3, -4, 2, 5};
322 REQUIRE(observer.rules[Rule_t::Basic][0] == r);
323 REQUIRE(observer.compute.size() == 1);
324 REQUIRE(observer.compute[0] == na);
325 }
326 SECTION("compute statement can contain multiple literals") {
327 Vec<Lit_t> compute ={-1, 2, -3, -4, 5, 6};
328 writer.assume(toSpan(compute));
329 writer.endStep();
330 REQUIRE(readSmodels(str, observer) == 0);
331 // B+ followed by B-
__anon1aeb9a260102(Lit_t x) 332 std::stable_partition(compute.begin(), compute.end(), [](Lit_t x) {return x > 0; });
333 REQUIRE(observer.compute == compute);
334 }
335 SECTION("only one compute statement supported") {
336 Lit_t na = -1, b = 2;
337 writer.assume(toSpan(&na, 1));
338 REQUIRE_THROWS(writer.assume(toSpan(&b, 1)));
339 }
340 SECTION("complex directives are not supported") {
341 REQUIRE_THROWS(writer.project(toSpan<Atom_t>()));
342 REQUIRE_THROWS(writer.external(1, Value_t::False));
343 REQUIRE_THROWS(writer.heuristic(1, Heuristic_t::Sign, 1, 0, toSpan<Lit_t>()));
344 REQUIRE_THROWS(writer.acycEdge(1, 2, toSpan<Lit_t>()));
345 }
346 }
347
348 TEST_CASE("Match heuristic predicate", "[smodels]") {
349 const char* in;
350 StringSpan atom;
351 Heuristic_t type;
352 int bias; unsigned prio;
353 SECTION("do not match invalid predicate name") {
354 REQUIRE(0 == matchDomHeuPred(in = "heuristic()", atom, type, bias, prio));
355 REQUIRE(0 == matchDomHeuPred(in = "_heu()", atom, type, bias, prio));
356 }
357 SECTION("do not match predicate with wrong arity") {
358 REQUIRE(-1 == matchDomHeuPred(in = "_heuristic(x)", atom, type, bias, prio));
359 REQUIRE(-2 == matchDomHeuPred(in = "_heuristic(x,sign)", atom, type, bias, prio));
360 REQUIRE(-4 == matchDomHeuPred(in = "_heuristic(x,sign,1,2,3)", atom, type, bias, prio));
361 }
362 SECTION("do not match predicate with invalid parameter") {
363 REQUIRE(-2 == matchDomHeuPred(in = "_heuristic(x,invalid,1)", atom, type, bias, prio));
364 REQUIRE(-3 == matchDomHeuPred(in = "_heuristic(x,sign,foo)", atom, type, bias, prio));
365 REQUIRE(-4 == matchDomHeuPred(in = "_heuristic(x,sign,1,-10)", atom, type, bias, prio));
366 REQUIRE(-3 == matchDomHeuPred(in = "_heuristic(x,sign,1a,-10)", atom, type, bias, prio));
367 REQUIRE(-2 == matchDomHeuPred(in = "_heuristic(x,sign(),1)", atom, type, bias, prio));
368 }
369 SECTION("match _heuristic/3 and assign implicit priority") {
370 REQUIRE(1 == matchDomHeuPred(in = "_heuristic(x,level,-10)", atom, type, bias, prio));
371 REQUIRE(prio == 10);
372 REQUIRE(1 == matchDomHeuPred(in = "_heuristic(x,sign,-2147483648)", atom, type, bias, prio));
373 REQUIRE(prio == static_cast<unsigned>(2147483647)+1);
374 REQUIRE(bias == std::numeric_limits<int32_t>::min());
375 }
376 SECTION("match _heuristic/4") {
377 REQUIRE(1 == matchDomHeuPred(in = "_heuristic(x,level,-10,123)", atom, type, bias, prio));
378 REQUIRE(bias == -10);
379 REQUIRE(prio == 123);
380 }
381 SECTION("match complex atom name") {
382 REQUIRE(1 == matchDomHeuPred(in = "_heuristic(_heuristic(x,y,z),init,1)", atom, type, bias, prio));
383 REQUIRE(type == Heuristic_t::Init);
384 }
385 }
386
387
388 TEST_CASE("SmodelsOutput supports extended programs", "[smodels_ext]") {
389 std::stringstream str, exp;
390 SmodelsOutput out(str, true, 0);
391 SmodelsConvert writer(out, true);
392 writer.initProgram(true);
393 writer.beginStep();
394 exp << "90 0\n";
395 Vec<Atom_t> head = {1, 2};
396 Vec<Lit_t> body = {3, -4};
397 Vec<WeightLit_t> min = {{-1, 2}, {2, 1}};
398 writer.rule(Head_t::Choice, toSpan(head), toSpan(body));
399 exp << (int)Rule_t::Choice << " 2 2 3 2 1 5 4\n";
400 writer.external(3, Value_t::False);
401 writer.external(4, Value_t::False);
402 writer.minimize(0, toSpan(min));
403 writer.heuristic(1, Heuristic_t::Sign, 1, 0, toSpan<Lit_t>());
404 exp << "1 6 0 0\n";
405 exp << (int)Rule_t::Optimize << " 0 2 1 2 3 2 1\n";
406 exp << (int)Rule_t::ClaspAssignExt << " 4 0\n";
407 exp << (int)Rule_t::ClaspAssignExt << " 5 0\n";
408 exp << "0\n6 _heuristic(_atom(2),sign,1,0)\n2 _atom(2)\n0\nB+\n0\nB-\n1\n0\n1\n";
409 writer.endStep();
410 writer.beginStep();
411 exp << "90 0\n";
412 head[0] = 3; head[1] = 4;
413 writer.rule(Head_t::Choice, toSpan(head), toSpan<Lit_t>());
414 exp << (int)Rule_t::Choice << " 2 4 5 0 0\n";
415 writer.endStep();
416 exp << "0\n0\nB+\n0\nB-\n1\n0\n1\n";
417 REQUIRE(str.str() == exp.str());
418 }
419
420
421 TEST_CASE("Convert to smodels", "[convert]") {
422 using BodyLits = std::initializer_list<Lit_t>;
423 using AggLits = std::initializer_list<WeightLit_t>;
424 ReadObserver observer;
425 SmodelsConvert convert(observer, true);
426 convert.initProgram(false);
427 convert.beginStep();
428 SECTION("convert rule") {
429 Atom_t a = 1;
430 BodyLits lits = {4, -3, -2, 5};
431 convert.rule(Head_t::Disjunctive, {&a, 1}, {begin(lits), lits.size()});
432 REQUIRE(observer.rules[Rule_t::Basic].size() == 1);
433 RawRule r ={convert.get(a), convert.get(4), convert.get(-3), convert.get(-2), convert.get(5)};
434 REQUIRE(observer.rules[Rule_t::Basic][0] == r);
435 }
436 SECTION("convert mixed rule") {
437 std::initializer_list<Atom_t> h = {1, 2, 3};
438 AggLits lits = {{4, 2}, {-3, 3}, {-2, 1}, {5, 4}};
439 convert.rule(Head_t::Choice, {begin(h), h.size()}, 3, {begin(lits), lits.size()});
440 REQUIRE(observer.rules[Rule_t::Choice].size() == 1);
441 REQUIRE(observer.rules[Rule_t::Weight].size() == 1);
442 int aux = (int)convert.maxAtom();
443 RawRule cr = {3, convert.get(1), convert.get(2), convert.get(3), aux};
444 RawRule sr = {aux, 3, convert.get(4), 2, convert.get(-3), 3, convert.get(-2), 1, convert.get(5), 4};
445 REQUIRE(cr == observer.rules[Rule_t::Choice][0]);
446 REQUIRE(sr == observer.rules[Rule_t::Weight][0]);
447 }
448
449 SECTION("convert minimize") {
450 AggLits m1 = {{4, 1}, {-3, -2}, {-2, 1}, {5, -1}};
451 AggLits m2 = {{8, 1}, {-7, 2}, {-6, 1}, {9, 1}};
452 convert.minimize(3, {begin(m2), 2});
453 convert.minimize(10, {begin(m1), m1.size()});
454 convert.minimize(3, {begin(m2)+2, 2});
455 REQUIRE(observer.rules[Rule_t::Optimize].size() == 0);
456 convert.endStep();
457 REQUIRE(observer.rules[Rule_t::Optimize].size() == 2);
458
459 RawRule m3 = {3, convert.get(8), 1, convert.get(-7), 2, convert.get(-6), 1, convert.get(9), 1};
460 RawRule m10 ={10, convert.get(4), 1, convert.get(3), 2, convert.get(-2), 1, convert.get(-5), 1};
461 REQUIRE(observer.rules[Rule_t::Optimize][0] == m3);
462 REQUIRE(observer.rules[Rule_t::Optimize][1] == m10);
463 }
464 SECTION("convert output") {
465 LitVec c = {1, -2, 3};
466 convert.output({"Foo", 3}, toSpan(c));
467 convert.endStep();
468 REQUIRE(observer.rules[Rule_t::Basic].size() == 1);
469 REQUIRE(convert.maxAtom() == 5);
470 Atom_t aux = observer.rules[Rule_t::Basic][0][0];
471 REQUIRE(std::strcmp(convert.getName(aux), "Foo") == 0);
472 }
473
474 SECTION("convert external") {
475 convert.external(1, Value_t::Free);
476 convert.external(2, Value_t::True);
477 convert.external(3, Value_t::False);
478 convert.external(4, Value_t::Release);
479 convert.endStep();
480 REQUIRE(observer.rules[Rule_t::ClaspAssignExt].size() == 3);
481 REQUIRE(observer.rules[Rule_t::ClaspReleaseExt].size() == 1);
482 REQUIRE(observer.rules[Rule_t::ClaspAssignExt][0][1] == Value_t::Free);
483 REQUIRE(observer.rules[Rule_t::ClaspAssignExt][1][1] == Value_t::True);
484 REQUIRE(observer.rules[Rule_t::ClaspAssignExt][2][1] == Value_t::False);
485 }
486 SECTION("edges are converted to atoms") {
487 Lit_t a = 1;
488 convert.output({"a", 1}, {&a, 1});
489 convert.acycEdge(0, 1, {&a, 1});
490 LitVec c = {1, 2, 3};
491 convert.acycEdge(1, 0, toSpan(c));
492 convert.endStep();
493 REQUIRE(observer.rules[Rule_t::Basic].size() == 2);
494 REQUIRE(observer.atoms[observer.rules[Rule_t::Basic][0][0]] == "_edge(0,1)");
495 REQUIRE(observer.atoms[observer.rules[Rule_t::Basic][1][0]] == "_edge(1,0)");
496 }
497
498 SECTION("heuristics are converted to atoms") {
499 SECTION("empty condition") {
500 Lit_t a = 1;
501 convert.heuristic(static_cast<Atom_t>(a), Heuristic_t::Factor, 10, 2, toSpan<Lit_t>());
502 convert.output({"a", 1}, {&a, 1});
503 convert.endStep();
504 REQUIRE(observer.rules[Rule_t::Basic].size() == 1);
505 REQUIRE(convert.maxAtom() == 3);
506 REQUIRE(observer.atoms[observer.rules[Rule_t::Basic][0][0]] == "_heuristic(a,factor,10,2)");
507 }
508 SECTION("named condition requires aux atom while unnamed does not") {
509 Lit_t a = 1, b = 2, c = 3;
510 convert.output({"a", 1}, {&a, 1});
511 convert.output({"b", 1}, {&b, 1});
512 convert.heuristic(static_cast<Atom_t>(a), Heuristic_t::Level, 10, 2, toSpan(&b, 1));
513 convert.heuristic(static_cast<Atom_t>(a), Heuristic_t::Init, 10, 2, toSpan(&c, 1));
514 convert.endStep();
515 REQUIRE(observer.rules[Rule_t::Basic].size() == 1);
516 REQUIRE(observer.atoms[observer.rules[Rule_t::Basic][0][0]] == "_heuristic(a,level,10,2)");
517 REQUIRE(observer.atoms[convert.get(c)] == "_heuristic(a,init,10,2)");
518 }
519 SECTION("unused atom is ignored") {
520 Lit_t a = 1;
521 convert.heuristic(static_cast<Atom_t>(a), Heuristic_t::Sign, -1, 2, toSpan<Lit_t>());
522 convert.endStep();
523 REQUIRE(observer.rules[Rule_t::Basic].size() == 1);
524 REQUIRE(convert.maxAtom() == 2);
525 REQUIRE(observer.atoms.empty());
526 }
527 SECTION("unnamed atom requires aux name") {
528 Atom_t a = 1;
529 convert.rule(Head_t::Choice, {&a, 1}, toSpan<Lit_t>());
530 convert.heuristic(a, Heuristic_t::Sign, -1, 2, toSpan<Lit_t>());
531 convert.endStep();
532 REQUIRE(observer.rules[Rule_t::Basic].size() == 1);
533 REQUIRE(convert.maxAtom() == 3);
534 REQUIRE(observer.atoms[2] == "_atom(2)");
535 REQUIRE(observer.atoms[3] == "_heuristic(_atom(2),sign,-1,2)");
536 }
537 }
538 }
toSpan(const char * str)539 inline StringSpan toSpan(const char* str) {
540 return Potassco::toSpan(str, std::strlen(str));
541 }
542 using Potassco::toSpan;
543
544 TEST_CASE("Test Atom to directive conversion", "[clasp]") {
545 ReadObserver observer;
546 std::stringstream str;
547 SmodelsOutput writer(str, false, 0);
548 SmodelsInput::Options opts; opts.enableClaspExt().convertEdges().convertHeuristic();
549 std::vector<Atom_t> atoms = {1, 2, 3, 4, 5, 6};
550 writer.initProgram(false);
551 writer.beginStep();
552 writer.rule(Potassco::Head_t::Choice, Potassco::toSpan(atoms), Potassco::toSpan<Potassco::Lit_t>());
553 SECTION("_edge(X,Y) atoms are converted to edges directives") {
554 Lit_t a = 1, b = 2, c = 3;
555 writer.output(toSpan("_edge(1,2)"), toSpan(&a, 1));
556 writer.output(toSpan("_edge(\"1,2\",\"2,1\")"), toSpan(&b, 1));
557 writer.output(toSpan("_edge(\"2,1\",\"1,2\")"), toSpan(&c, 1));
558 writer.endStep();
559 REQUIRE(readSmodels(str, observer, 0, opts) == 0);
560 REQUIRE(observer.edges.size() == 3);
561 REQUIRE(observer.edges[0].cond == Vec<Lit_t>({a}));
562 REQUIRE(observer.edges[0].s == 0);
563 REQUIRE(observer.edges[0].t == 1);
564 REQUIRE(observer.edges[1].cond == Vec<Lit_t>({b}));
565 REQUIRE(observer.edges[1].s == observer.edges[2].t);
566 REQUIRE(observer.edges[2].cond == Vec<Lit_t>({c}));
567 }
568 SECTION("Test acyc") {
569 Lit_t a = 1, b = 2;
570 SECTION("_acyc_ atoms are converted to edge directives") {
571 writer.output(toSpan("_acyc_1_1234_4321"), toSpan(&a, 1));
572 writer.output(toSpan("_acyc_1_4321_1234"), toSpan(&b, 1));
573 }
574 SECTION("_acyc_ and _edge atoms can be mixed") {
575 writer.output(toSpan("_acyc_1_1234_4321"), toSpan(&a, 1));
576 writer.output(toSpan("_edge(4321,1234)"), toSpan(&b, 1));
577 }
578 writer.endStep();
579 REQUIRE(readSmodels(str, observer, 0, opts) == 0);
580 REQUIRE(observer.edges.size() == 2);
581 REQUIRE(observer.edges[0].cond == Vec<Lit_t>({a}));
582 REQUIRE(observer.edges[1].cond == Vec<Lit_t>({b}));
583 REQUIRE(observer.edges[0].s == observer.edges[1].t);
584 REQUIRE(observer.edges[0].t == observer.edges[1].s);
585 }
586 SECTION("_heuristic atoms are converted to heuristic directive") {
587 Lit_t a = 1, b = 2, h1 = 3, h2 = 4, h3 = 5, h4 = 6;
588 writer.output(toSpan("f(a,b,c,d(q(r(s))))"), toSpan(&a, 1));
589 writer.output(toSpan("f(\"a,b(c,d)\")"), toSpan(&b, 1));
590 writer.output(toSpan("_heuristic(f(a,b,c,d(q(r(s)))),sign,-1)"), toSpan(&h1, 1));
591 writer.output(toSpan("_heuristic(f(a,b,c,d(q(r(s)))),true,1)"), toSpan(&h2, 1));
592 writer.output(toSpan("_heuristic(f(\"a,b(c,d)\"),level,-1,10)"), toSpan(&h3, 1));
593 writer.output(toSpan("_heuristic(f(\"a,b(c,d)\"),factor,2,1)"), toSpan(&h4, 1));
594 writer.endStep();
595 REQUIRE(readSmodels(str, observer, 0, opts) == 0);
596 REQUIRE(observer.heuristics.size() == 4);
597 Heuristic exp[] ={
598 {static_cast<Atom_t>(a), Heuristic_t::Sign, -1, 1, {h1}},
599 {static_cast<Atom_t>(a), Heuristic_t::True, 1, 1, {h2}},
600 {static_cast<Atom_t>(b), Heuristic_t::Level, -1, 10, {h3}},
601 {static_cast<Atom_t>(b), Heuristic_t::Factor, 2, 1, {h4}}
602 };
603 REQUIRE(std::equal(std::begin(exp), std::end(exp), observer.heuristics.begin()) == true);
604 }
605 }
606
607 }}}
608