1 // 2 // Copyright (c) 2006-2017 Benjamin Kaufmann 3 // 4 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ 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 #include <clasp/logic_program.h> 25 #include <clasp/program_builder.h> 26 #include <clasp/solver.h> 27 #include <clasp/unfounded_check.h> 28 #include <clasp/minimize_constraint.h> 29 #include "lpcompare.h" 30 #include "catch.hpp" 31 using namespace std; 32 namespace Clasp { namespace Test { 33 using namespace Clasp::Asp; 34 struct ClauseObserver : public DecisionHeuristic { doSelectClasp::Test::ClauseObserver35 Literal doSelect(Solver&){return Literal();} updateVarClasp::Test::ClauseObserver36 void updateVar(const Solver&, Var, uint32) {} newConstraintClasp::Test::ClauseObserver37 void newConstraint(const Solver&, const Literal* first, LitVec::size_type size, ConstraintType) { 38 Clause c; 39 for (LitVec::size_type i = 0; i < size; ++i, ++first) { 40 c.push_back(*first); 41 } 42 std::sort(c.begin(), c.end()); 43 clauses_.push_back(c); 44 } 45 typedef std::vector<Literal> Clause; 46 typedef std::vector<Clause> Clauses; 47 Clauses clauses_; 48 }; 49 50 TEST_CASE("Logic program types", "[asp]") { 51 SECTION("testInvalidNodeId") { 52 REQUIRE_THROWS_AS(PrgNode(PrgNode::noNode + 1), std::overflow_error); 53 } 54 SECTION("testMergeValue") { 55 PrgAtom lhs(0), rhs(1); 56 ValueRep ok[15] = { 57 value_free, value_free, value_free, 58 value_free, value_true, value_true, 59 value_free, value_false, value_false, 60 value_free, value_weak_true, value_weak_true, 61 value_true, value_weak_true, value_true 62 }; 63 ValueRep fail[4] = {value_true, value_false, value_weak_true, value_false}; 64 for (uint32 x = 0; x != 2; ++x) { 65 for (uint32 i = 0; i != 15; i += 3) { 66 lhs.clearLiteral(true); 67 rhs.clearLiteral(true); 68 REQUIRE(lhs.assignValue(ok[i+x])); 69 REQUIRE(rhs.assignValue(ok[i+(!x)])); 70 REQUIRE(mergeValue(&lhs, &rhs)); 71 REQUIRE((lhs.value() == ok[i+2] && rhs.value() == ok[i+2])); 72 } 73 } 74 for (uint32 x = 0; x != 2; ++x) { 75 for (uint32 i = 0; i != 4; i += 2) { 76 lhs.clearLiteral(true); 77 rhs.clearLiteral(true); 78 REQUIRE(lhs.assignValue(fail[i+x])); 79 REQUIRE(rhs.assignValue(fail[i+(!x)])); 80 REQUIRE(!mergeValue(&lhs, &rhs)); 81 } 82 } 83 } 84 } 85 TEST_CASE("Logic program", "[asp]") { 86 Var a = 1, b = 2, c = 3, d = 4, e = 5, f = 6; 87 SharedContext ctx; 88 LogicProgram lp; 89 SECTION("testIgnoreRules") { 90 lpAdd(lp.start(ctx), "a :- a. b :- a.\n"); 91 REQUIRE(1u == lp.stats.rules[0].sum()); 92 } 93 SECTION("testDuplicateRule") { 94 lpAdd(lp.start(ctx, LogicProgram::AspOptions().iterations(1)), 95 "{b}.\n" 96 "a :- b.\n" 97 "a :- b.\n"); 98 REQUIRE((lp.endProgram() && ctx.endInit())); 99 REQUIRE(lp.getLiteral(a) == lp.getLiteral(b)); 100 } 101 102 SECTION("testNotAChoice") { 103 lpAdd(lp.start(ctx), 104 "{b}.\n" 105 "{a} :- not b." 106 "a :-not b."); 107 REQUIRE((lp.endProgram() && ctx.endInit())); 108 ctx.master()->assume(~lp.getLiteral(b)) && ctx.master()->propagate(); 109 // if b is false, a must be true because a :- not b. is stronger than {a} :- not b. 110 REQUIRE(ctx.master()->isTrue(lp.getLiteral(a))); 111 } 112 113 SECTION("testNotAChoiceMerge") { 114 lpAdd(lp.start(ctx), 115 "{b}.\n" 116 "{a} :- b.\n" 117 "a :- b, not c."); 118 REQUIRE((lp.endProgram() && ctx.endInit())); 119 REQUIRE(lp.getLiteral(a) == lp.getLiteral(b)); 120 } 121 122 SECTION("testMergeToSelfblocker") { 123 lpAdd(lp.start(ctx), 124 "a :- not b.\n" 125 "b :- a.\n"); 126 REQUIRE_FALSE((lp.endProgram() && ctx.endInit())); 127 } 128 129 SECTION("testMergeToSelfblocker2") { 130 lpAdd(lp.start(ctx), 131 "a :- not d.\n" 132 "a :- not c.\n" 133 "b :- not c.\n" 134 "c :- a."); 135 REQUIRE((lp.endProgram() && ctx.endInit())); 136 REQUIRE(ctx.master()->isTrue(lp.getLiteral(a))); 137 REQUIRE(ctx.numVars() == 0); 138 } 139 SECTION("testMergeToSelfblocker3") { 140 lpAdd(lp.start(ctx), 141 "b :- a.\n" 142 "{c}.\n" 143 "d :- 2 {a, b}.\n" 144 "e :- 2 {a}.\n" 145 "a :- not d, not e.\n"); 146 REQUIRE_FALSE(lp.endProgram()); 147 } 148 149 SECTION("testDerivedTAUT") { 150 lpAdd(lp.start(ctx), 151 "{x1;x2}.\n" 152 "x3 :- not x2.\n" 153 "x4 :- x3.\n" 154 "x3 :- x1, x4.\n"); 155 REQUIRE((lp.endProgram() && ctx.endInit())); 156 REQUIRE(ctx.numVars() == 2); 157 } 158 159 SECTION("testOneLoop") { 160 lpAdd(lp.start(ctx), 161 "a :- not b.\n" 162 "b :- not a.\n"); 163 REQUIRE((lp.endProgram() && ctx.endInit())); 164 REQUIRE( 1u == ctx.numVars() ); 165 REQUIRE( 0u == ctx.numConstraints() ); 166 REQUIRE( lp.getLiteral(a) == ~lp.getLiteral(b) ); 167 } 168 169 SECTION("testZeroLoop") { 170 lpAdd(lp.start(ctx), 171 "a :- b.\n" 172 "b :- a.\n" 173 "a :- not c.\n" 174 "c :- not a."); 175 REQUIRE((lp.endProgram() && ctx.endInit())); 176 REQUIRE( 1u == ctx.numVars() ); 177 REQUIRE( 0u == ctx.numConstraints() ); 178 REQUIRE( lp.getLiteral(a) == lp.getLiteral(b) ); 179 } 180 181 SECTION("testEqSuccs") { 182 lpAdd(lp.start(ctx), 183 "{a;b}.\n" 184 "c :- a, b.\n" 185 "d :- a, b.\n"); 186 REQUIRE((lp.endProgram() && ctx.endInit())); 187 REQUIRE( 3u == ctx.numVars() ); 188 REQUIRE( 3u == ctx.numConstraints() ); 189 REQUIRE( lp.getLiteral(c) == lp.getLiteral(d) ); 190 } 191 192 SECTION("testEqCompute") { 193 lpAdd(lp.start(ctx), 194 "{c}.\n" 195 "a :- not c.\n" 196 "a :- b.\n" 197 "b :- a.\n" 198 " :- not b."); 199 REQUIRE((lp.endProgram() && ctx.endInit())); 200 REQUIRE(ctx.master()->isTrue(lp.getLiteral(a))); 201 REQUIRE(lp.getLiteral(a) == lp.getLiteral(b)); 202 REQUIRE(lp.isFact(a)); 203 REQUIRE(lp.isFact(b)); 204 } 205 206 SECTION("testFactsAreAsserted") { 207 lpAdd(lp.start(ctx), 208 "a :- not b.\n" 209 "c."); 210 REQUIRE((lp.endProgram() && ctx.endInit())); 211 REQUIRE(ctx.master()->isTrue(lp.getLiteral(a))); 212 REQUIRE(ctx.master()->isTrue(lp.getLiteral(c))); 213 } 214 SECTION("testSelfblockersAreAsserted") { 215 lpAdd(lp.start(ctx), 216 "x1 :- not x1.\n" 217 "x2 :- not x1.\n"); 218 REQUIRE_FALSE((lp.endProgram() && ctx.endInit())); 219 } 220 SECTION("testConstraintsAreAsserted") { 221 lpAdd(lp.start(ctx), 222 "a :- not b.\n" 223 "b :- not a.\n" 224 " :- a."); 225 REQUIRE((lp.endProgram() && ctx.endInit())); 226 REQUIRE(ctx.master()->isFalse(lp.getLiteral(a))); 227 } 228 229 SECTION("testConflictingCompute") { 230 lpAdd(lp.start(ctx), 231 " :- a.\n" 232 " :- not a."); 233 REQUIRE_FALSE((lp.endProgram() && ctx.endInit())); 234 REQUIRE(!ctx.ok()); 235 } 236 SECTION("testForceUnsuppAtomFails") { 237 lpAdd(lp.start(ctx), "a :- not b. :- not b."); 238 REQUIRE_FALSE((lp.endProgram() && ctx.endInit())); 239 } 240 241 SECTION("testTrivialConflictsAreDeteced") { 242 lpAdd(lp.start(ctx), "a :- not a. :- not a."); 243 REQUIRE_FALSE((lp.endProgram() && ctx.endInit())); 244 245 } 246 SECTION("testBuildEmpty") { 247 lp.start(ctx); 248 lp.endProgram(); 249 REQUIRE(0u == ctx.numVars()); 250 REQUIRE(0u == ctx.numConstraints()); 251 } 252 SECTION("testAddOneFact") { 253 lpAdd(lp.start(ctx), "a."); 254 REQUIRE(lp.endProgram()); 255 REQUIRE(0u == ctx.numVars()); 256 // a fact does not introduce a constraint, it is just a top-level assignment 257 REQUIRE(0u == ctx.numConstraints()); 258 REQUIRE(lp.isFact(a)); 259 } 260 261 SECTION("testTwoFactsOnlyOneVar") { 262 lpAdd(lp.start(ctx), "a. b."); 263 REQUIRE(lp.endProgram()); 264 REQUIRE(0u == ctx.numVars()); 265 REQUIRE(0u == ctx.numConstraints()); 266 REQUIRE(lp.isFact(a)); 267 REQUIRE(lp.isFact(b)); 268 } 269 270 SECTION("testDontAddDuplicateSumBodies") { 271 lpAdd(lp.start(ctx), 272 "{a; b; c}.\n" 273 "d :- 2 {a=1, b=2, not c=1}.\n" 274 "e :- 2 {a=1, b=2, not c=1}.\n"); 275 REQUIRE(lp.endProgram()); 276 REQUIRE(lp.numBodies() == 2); 277 } 278 279 SECTION("testAddLargeSumBody") { 280 VarVec atoms; 281 Potassco::WLitVec lits; 282 lp.start(ctx); 283 for (uint32 i = 1; i != 21; ++i) { atoms.push_back(i); } 284 lp.addRule(Head_t::Choice, Potassco::toSpan(atoms), Potassco::toSpan<Potassco::Lit_t>()); 285 286 atoms.assign(1, 20); 287 for (int32 i = 1; i != 20; ++i) { 288 Potassco::WeightLit_t wl = {i&1 ? Potassco::lit(i) : Potassco::neg(i), i}; 289 lits.push_back(wl); 290 } 291 lp.addRule(Head_t::Disjunctive, Potassco::toSpan(atoms), 10, Potassco::toSpan(lits)); 292 lits.clear(); 293 for (int32 i = 20; --i;) { 294 Potassco::WeightLit_t wl = {i&1 ? Potassco::lit(i) : Potassco::neg(i), 20 - i}; 295 lits.push_back(wl); 296 } 297 lp.addRule(Head_t::Disjunctive, Potassco::toSpan(atoms), 10, Potassco::toSpan(lits)); 298 REQUIRE(lp.endProgram()); 299 REQUIRE(lp.numBodies() == 3u); 300 } 301 SECTION("testDontAddDuplicateSimpBodies") { 302 lpAdd(lp.start(ctx), 303 "{x1;x2;x3;x4}.\n" 304 "x1 :- x2, x3, x4.\n" 305 "x1 :- 8 {x3=2, x2=3, x4=4}."); 306 REQUIRE(lp.endProgram()); 307 REQUIRE(lp.numBodies() == 2); 308 } 309 310 SECTION("testDontAddUnsupportedExtNoEq") { 311 lpAdd(lp.start(ctx, LogicProgram::AspOptions().noEq()), 312 "a :- not d.\n" 313 "c :- a, d.\n" 314 "b :- 2 {a, c, not d}. % -> a\n"); 315 REQUIRE((lp.endProgram() && ctx.endInit())); 316 REQUIRE(ctx.master()->isFalse(lp.getLiteral(c))); 317 REQUIRE(ctx.master()->isTrue(lp.getLiteral(a))); 318 REQUIRE(ctx.master()->isTrue(lp.getLiteral(b))); 319 } 320 321 SECTION("testAssertSelfblockers") { 322 lpAdd(lp.start(ctx), 323 "a :- b, not c.\n" 324 "c :- b, not c.\n" 325 "b."); 326 // Program is unsat because b must be true and false at the same time. 327 REQUIRE_FALSE((lp.endProgram() && ctx.endInit())); 328 } 329 330 SECTION("testRegressionR1") { 331 lpAdd(lp.start(ctx), "b. b :- not c."); 332 REQUIRE((lp.endProgram() && ctx.endInit())); 333 REQUIRE(lp.getLiteral(b) == lit_true()); 334 REQUIRE(lp.getLiteral(c) == lit_false()); 335 REQUIRE(ctx.numVars() == 0); 336 } 337 338 SECTION("testRegressionR2") { 339 lpAdd(lp.start(ctx), 340 "b :- not c.\n" 341 "b :- not d.\n" 342 "c :- not b.\n" 343 "d :- not b.\n" 344 "b."); 345 REQUIRE((lp.endProgram() && ctx.endInit())); 346 REQUIRE(lp.getLiteral(b) == lit_true()); 347 REQUIRE(lp.getLiteral(c) == lit_false()); 348 REQUIRE(lp.getLiteral(d) == lit_false()); 349 REQUIRE(ctx.numVars() == 0); 350 } 351 SECTION("testFuzzBug") { 352 lpAdd(lp.start(ctx), "x1 :- not x1, not x2, not x3, not x2, not x1, not x4."); 353 REQUIRE_FALSE((lp.endProgram() && ctx.endInit())); 354 } 355 SECTION("testBackpropNoEqBug") { 356 lpAdd(lp.start(ctx, LogicProgram::AspOptions().noEq().backpropagate()), 357 "{x2;x3;x4} :- x5.\n" 358 "x1 :- x7, x5.\n" 359 "x5.\n" 360 "x7 :- x2, x3.\n" 361 "x7 :- x6.\n" 362 "x6 :- x8.\n" 363 "x8 :- x4.\n" 364 ":- x1."); 365 REQUIRE((lp.endProgram() && ctx.endInit())); 366 REQUIRE(ctx.master()->isFalse(lp.getLiteral(6))); 367 } 368 369 SECTION("testCloneProgram") { 370 lpAdd(lp.start(ctx), 371 "{x1;x2;x3}.\n" 372 "x4 :- x1, x2, x3."); 373 REQUIRE((lp.endProgram() && ctx.endInit())); 374 REQUIRE( uint32(4) >= ctx.numVars() ); 375 REQUIRE( uint32(4) >= ctx.numConstraints() ); 376 377 SharedContext ctx2; 378 REQUIRE((lp.clone(ctx2) && ctx2.endInit())); 379 REQUIRE( ctx.numVars() == ctx2.numVars() ); 380 REQUIRE( ctx.numConstraints() == ctx2.numConstraints() ); 381 REQUIRE(!ctx.isShared()); 382 REQUIRE(!ctx2.isShared()); 383 REQUIRE(ctx.output.size() == ctx2.output.size() ); 384 } 385 386 SECTION("testBug") { 387 lpAdd(lp.start(ctx), 388 "x1 :- x2.\n" 389 "x2 :- x3, x1.\n" 390 "x3 :- x4.\n" 391 "x4 :-not x3.\n"); 392 REQUIRE_FALSE((lp.endProgram() && ctx.endInit())); 393 } 394 395 SECTION("testSatBodyBug") { 396 lpAdd(lp.start(ctx), 397 "{c;b;a}.\n" 398 "a.\n" 399 "b :- 1 {a, c}.\n" 400 "d :- b, c.\n"); 401 REQUIRE(std::distance(lp.getAtom(c)->deps_begin(), lp.getAtom(c)->deps_end()) <= 2u); 402 REQUIRE((lp.endProgram() && ctx.endInit())); 403 REQUIRE(std::distance(lp.getAtom(c)->deps_begin(), lp.getAtom(c)->deps_end()) == 1u); 404 REQUIRE(std::distance(lp.getAtom(b)->deps_begin(), lp.getAtom(b)->deps_end()) == 0u); 405 REQUIRE(value_free == ctx.master()->value(lp.getLiteral(c).var())); 406 } 407 SECTION("testDepBodyBug") { 408 lpAdd(lp.start(ctx), 409 "{d;e;f}.\n" 410 "a :- d, e.\n" 411 "b :- a." 412 "c :- b, f, a.\n"); 413 REQUIRE(lp.endProgram()); 414 REQUIRE((lp.getAtom(a)->deps_end() - lp.getAtom(a)->deps_begin()) == 2); 415 } 416 417 SECTION("testAddUnknownAtomToMinimize") { 418 lpAdd(lp.start(ctx), "#minimize{a}."); 419 REQUIRE((lp.endProgram() && ctx.endInit())); 420 REQUIRE(lp.hasMinimize()); 421 } 422 423 SECTION("testWriteWeakTrue") { 424 lpAdd(lp.start(ctx), 425 "{c}.\n" 426 "a :- not b, c.\n" 427 "b :- not a.\n" 428 " :- not a.\n"); 429 REQUIRE((lp.endProgram() && ctx.endInit())); 430 Var a = lp.falseAtom(); 431 std::stringstream exp; 432 exp << "1 " << a << " 1 1 3\n"; 433 REQUIRE(findSmodels(exp, lp)); 434 } 435 436 SECTION("testSimplifyBodyEqBug") { 437 lpAdd(lp.start(ctx), 438 "{d;e;f}.\n" 439 "a :- d,f.\n" 440 "b :- d,f.\n" 441 "c :- a, e, b.\n"); 442 REQUIRE((lp.endProgram() && ctx.endInit())); 443 PrgAtom* na = lp.getAtom(a); 444 PrgAtom* nb = lp.getAtom(b); 445 REQUIRE((nb->eq() && nb->id() == a)); 446 REQUIRE((na->deps_end() - na->deps_begin()) == 1); 447 } 448 449 SECTION("testNoEqSameLitBug") { 450 lpAdd(lp.start(ctx, LogicProgram::AspOptions().noEq()), 451 "{x4;x5}.\n" 452 "x1 :- x4,x5.\n" 453 "x2 :- x4,x5.\n" 454 "x3 :- x1, x2.\n"); 455 REQUIRE((lp.endProgram() && ctx.endInit())); 456 REQUIRE(ctx.numVars() == 5); 457 } 458 459 SECTION("testAssertEqSelfblocker") { 460 lpAdd(lp.start(ctx), 461 "a :- not b, not c.\n" 462 "a :- not d, not e.\n" 463 "b :- not c.\n" 464 "c :- not b.\n" 465 "d :- not e.\n" 466 "e :- not d.\n"); 467 REQUIRE((lp.endProgram() && ctx.endInit())); 468 REQUIRE(2u == ctx.numVars()); 469 REQUIRE(ctx.master()->isFalse(lp.getLiteral(a))); 470 } 471 472 SECTION("testAddClauses") { 473 ClauseObserver o; 474 ctx.master()->setHeuristic(&o, Ownership_t::Retain); 475 lpAdd(lp.start(ctx), 476 "a :- not b.\n" 477 "a :- b, c.\n" 478 "b :- not a.\n" 479 "c :- not b.\n"); 480 REQUIRE((lp.endProgram() && ctx.endInit())); 481 REQUIRE(3u == ctx.numVars()); 482 REQUIRE(0u == ctx.master()->numAssignedVars()); 483 484 REQUIRE(8u == ctx.numConstraints()); 485 486 Var bodyNotB = 1; 487 Var bodyBC = 3; 488 REQUIRE(Var_t::Body == ctx.varInfo(3).type()); 489 Literal litA = lp.getLiteral(a); 490 REQUIRE(lp.getLiteral(b) == ~lp.getLiteral(a)); 491 492 // a - HeadClauses 493 ClauseObserver::Clause ac; 494 ac.push_back(~litA); 495 ac.push_back(posLit(bodyNotB)); 496 ac.push_back(posLit(bodyBC)); 497 std::sort(ac.begin(), ac.end()); 498 REQUIRE(std::find(o.clauses_.begin(), o.clauses_.end(), ac) != o.clauses_.end()); 499 500 // bodyNotB - Body clauses 501 ClauseObserver::Clause cl; 502 cl.push_back(negLit(bodyNotB)); cl.push_back(~lp.getLiteral(b)); 503 std::sort(cl.begin(), cl.end()); 504 REQUIRE(std::find(o.clauses_.begin(), o.clauses_.end(), cl) != o.clauses_.end()); 505 cl.clear(); 506 cl.push_back(posLit(bodyNotB)); cl.push_back(lp.getLiteral(b)); 507 std::sort(cl.begin(), cl.end()); 508 REQUIRE(std::find(o.clauses_.begin(), o.clauses_.end(), cl) != o.clauses_.end()); 509 cl.clear(); 510 cl.push_back(negLit(bodyNotB)); cl.push_back(litA); 511 std::sort(cl.begin(), cl.end()); 512 REQUIRE(std::find(o.clauses_.begin(), o.clauses_.end(), cl) != o.clauses_.end()); 513 514 // bodyBC - Body clauses 515 cl.clear(); 516 cl.push_back(negLit(bodyBC)); cl.push_back(lp.getLiteral(b)); 517 std::sort(cl.begin(), cl.end()); 518 REQUIRE(std::find(o.clauses_.begin(), o.clauses_.end(), cl) != o.clauses_.end()); 519 cl.clear(); 520 cl.push_back(negLit(bodyBC)); cl.push_back(lp.getLiteral(c)); 521 std::sort(cl.begin(), cl.end()); 522 REQUIRE(std::find(o.clauses_.begin(), o.clauses_.end(), cl) != o.clauses_.end()); 523 cl.clear(); 524 cl.push_back(posLit(bodyBC)); cl.push_back(~lp.getLiteral(b)); cl.push_back(~lp.getLiteral(c)); 525 std::sort(cl.begin(), cl.end()); 526 REQUIRE(std::find(o.clauses_.begin(), o.clauses_.end(), cl) != o.clauses_.end()); 527 cl.clear(); 528 cl.push_back(negLit(bodyBC)); cl.push_back(litA); 529 std::sort(cl.begin(), cl.end()); 530 REQUIRE(std::find(o.clauses_.begin(), o.clauses_.end(), cl) != o.clauses_.end()); 531 } 532 533 SECTION("testAddEmptyMinimizeConstraint") { 534 lpAdd(lp.start(ctx), "#minimize{}."); 535 REQUIRE(lp.endProgram()); 536 REQUIRE(ctx.hasMinimize()); 537 } 538 539 SECTION("testNonTight") { 540 lpAdd(lp.start(ctx), 541 "b :- c.\n" 542 "c :- b.\n" 543 "b :- not a.\n" 544 "c :- not a.\n" 545 "a :- not b.\n"); 546 REQUIRE((lp.endProgram() && ctx.endInit())); 547 REQUIRE( lp.stats.sccs != 0 ); 548 } 549 550 SECTION("testIgnoreCondFactsInLoops") { 551 lpAdd(lp.start(ctx), 552 "{a}.\n" 553 "b :- a.\n" 554 "a :- b.\n"); 555 REQUIRE((lp.endProgram() && ctx.endInit())); 556 REQUIRE( lp.stats.sccs == 0); 557 } 558 559 SECTION("testCrEqBug") { 560 lpAdd(lp.start(ctx), 561 "a.\n" 562 "{b}.\n"); 563 REQUIRE((lp.endProgram() && ctx.endInit())); 564 REQUIRE(1u == ctx.numVars()); 565 REQUIRE(value_free == ctx.master()->value(lp.getLiteral(b).var())); 566 } 567 568 SECTION("testEqOverComp") { 569 lpAdd(lp.start(ctx), 570 "a :- not b.\n" 571 "a :- b.\n" 572 "b :- not c.\n" 573 "c :- not a.\n"); 574 REQUIRE(lp.endProgram()); 575 REQUIRE(lp.getLiteral(a) == lp.getLiteral(b)); 576 REQUIRE((ctx.master()->numFreeVars() == 0 && ctx.master()->isTrue(lp.getLiteral(a)))); 577 } 578 579 SECTION("testEqOverBodiesOfDiffType") { 580 lpAdd(lp.start(ctx), 581 "{a;b}.\n" 582 "d :- 2{a, b, c}.\n" 583 "c :- d.\n" 584 " :- b.\n"); 585 REQUIRE((lp.endProgram() && ctx.endInit())); 586 REQUIRE(3u >= ctx.numVars()); 587 REQUIRE(ctx.master()->isFalse(lp.getLiteral(b))); 588 REQUIRE(ctx.master()->isFalse(lp.getLiteral(c))); 589 REQUIRE(ctx.master()->isFalse(lp.getLiteral(d))); 590 } 591 592 SECTION("testNoBodyUnification") { 593 Var g = 7; 594 lpAdd(lp.start(ctx), 595 "{a;b;c}.\n" 596 "d :- a, g.\n" 597 "d :- b.\n" 598 "e :- not d.\n" 599 "f :- not e.\n" 600 "g :- d.\n" 601 "g :- c.\n"); 602 REQUIRE((lp.endProgram() && ctx.sccGraph.get())); 603 ctx.master()->addPost(new DefaultUnfoundedCheck(*ctx.sccGraph)); 604 REQUIRE(ctx.endInit()); 605 ctx.master()->assume(~lp.getLiteral(b)); 606 ctx.master()->propagate(); 607 ctx.master()->assume(~lp.getLiteral(c)); 608 ctx.master()->propagate(); 609 REQUIRE(ctx.master()->isFalse(lp.getLiteral(g))); 610 } 611 612 SECTION("testNoEqAtomReplacement") { 613 lpAdd(lp.start(ctx), 614 "{a;b}.\n" 615 "c :- a.\n" 616 "c :- b.\n" 617 "d :- not c.\n" 618 "e :- not d.\n"); 619 REQUIRE((lp.endProgram() && ctx.endInit())); 620 ctx.master()->assume(~lp.getLiteral(a)); 621 ctx.master()->propagate(); 622 ctx.master()->assume(~lp.getLiteral(b)); 623 ctx.master()->propagate(); 624 REQUIRE(ctx.master()->isFalse(lp.getLiteral(c))); 625 } 626 627 SECTION("testAllBodiesSameLit") { 628 lpAdd(lp.start(ctx), 629 "{a}.\n" 630 "b :- not a.\n" 631 "c :- not b.\n" 632 "d :- b.\n" 633 "d :- not c.\n" 634 "b :- d.\n"); 635 REQUIRE((lp.endProgram() && ctx.endInit())); 636 REQUIRE(lp.getLiteral(b) == lp.getLiteral(d)); 637 REQUIRE(lp.getLiteral(a) != lp.getLiteral(c)); 638 ctx.master()->assume(lp.getLiteral(a)) && ctx.master()->propagate(); 639 REQUIRE(ctx.master()->value(lp.getLiteral(c).var()) == value_free); 640 ctx.master()->assume(~lp.getLiteral(c)) && ctx.master()->propagate(); 641 REQUIRE((ctx.master()->numFreeVars() == 0 && ctx.master()->isTrue(lp.getLiteral(b)))); 642 } 643 644 SECTION("testAllBodiesSameLit2") { 645 lpAdd(lp.start(ctx), 646 "{a;e}.\n" 647 "b :- not a.\n" 648 "c :- not b.\n" 649 "d :- b.\n" 650 "d :- not c.\n" 651 "b :- d, e.\n"); 652 REQUIRE((lp.endProgram() && ctx.endInit())); 653 REQUIRE(lp.getLiteral(b) == lp.getLiteral(d)); 654 REQUIRE(lp.getLiteral(a) != lp.getLiteral(c)); 655 ctx.master()->assume(lp.getLiteral(a)) && ctx.master()->propagate(); 656 REQUIRE(ctx.master()->value(lp.getLiteral(c).var()) == value_free); 657 ctx.master()->assume(~lp.getLiteral(c)) && ctx.master()->propagate(); 658 REQUIRE((ctx.master()->numFreeVars() == 0 && ctx.master()->isTrue(lp.getLiteral(b)))); 659 REQUIRE(ctx.numVars() == 4); 660 } 661 662 SECTION("testCompLit") { 663 lpAdd(lp.start(ctx), 664 "{d}.\n" 665 "a :- not c.\n" 666 "c :- not a.\n" 667 "b :- a, c.\n" 668 "e :- a, d, not c. % a == ~c -> {a,c} = F -> {a, not c} = {a, d}\n"); 669 REQUIRE((lp.endProgram() && ctx.endInit())); 670 REQUIRE(3u == ctx.numVars()); 671 REQUIRE(ctx.master()->isFalse(lp.getLiteral(b))); 672 } 673 674 SECTION("testFunnySelfblockerOverEqByTwo") { 675 lpAdd(lp.start(ctx), 676 "{a,b,c}.\n" 677 "d :- a, b.\n" 678 "e :- a, b.\n" 679 "f :- b, c.\n" 680 "g :- b, c.\n" 681 "f :- d, not f.\n" 682 "h :- e, not g.\n" 683 "i :- a, h.\n" 684 "% -> d == e, f == g -> {e, not g} == {d, not f} -> F" 685 "% -> h == i are both unsupported!"); 686 Var h = 8, i = 9; 687 REQUIRE((lp.endProgram() && ctx.endInit())); 688 REQUIRE(ctx.master()->isFalse(lp.getLiteral(h))); 689 REQUIRE(ctx.master()->isFalse(lp.getLiteral(i))); 690 } 691 692 SECTION("testSimplifyToTrue") { 693 lpAdd(lp.start(ctx), 694 "a.\n" 695 "b :- 1 {c, a}."); 696 REQUIRE(lp.endProgram()); 697 REQUIRE(lp.numBodies() <= 1); 698 } 699 700 SECTION("testSimplifyToCardBug") { 701 lpAdd(lp.start(ctx), 702 "a. b.\n" 703 "c :- 168 {not a = 576, not b=381}.\n" 704 " :- c.\n"); 705 REQUIRE(lp.endProgram()); 706 REQUIRE(ctx.master()->numFreeVars() == 0); 707 } 708 709 SECTION("testSimplifyCompBug") { 710 Var h = 8; 711 lpAdd(lp.start(ctx, LogicProgram::AspOptions().iterations(1)), 712 "a :- not b.\n" 713 "a :- b.\n" 714 "b :- not c.\n" 715 "c :- not a.\n" 716 "d. e. g. {f}.\n" 717 "h :- d, e, b, f, g.\n"); 718 REQUIRE(lp.endProgram()); 719 PrgAtom* x = lp.getAtom(h); 720 PrgBody* B = lp.getBody(x->supps_begin()->node()); 721 REQUIRE((B->size() == 2 && !B->goal(0).sign() && B->goal(1).sign())); 722 REQUIRE(B->goal(0).var() == f); 723 REQUIRE(B->goal(1).var() == c); 724 } 725 726 SECTION("testBPWeight") { 727 lpAdd(lp.start(ctx), 728 "{a, b, c, d}.\n" 729 "e :- 2 {a=1, b=2, not c=2, d=1}.\n" 730 " :- e."); 731 REQUIRE(lp.endProgram()); 732 REQUIRE(ctx.master()->isFalse(lp.getLiteral(b))); 733 REQUIRE(ctx.master()->isTrue(lp.getLiteral(c))); 734 } 735 736 SECTION("testExtLitsAreFrozen") { 737 Var g = 7, h = 8, i = 9; 738 lpAdd(lp.start(ctx), 739 "{a, b, c, d, e, f, g}.\n" 740 " h :- 2 {b, c, d}.\n" 741 "i :- 2 {c=1, d=2, e=1}.\n" 742 "#minimize {f, g}.\n"); 743 REQUIRE(lp.endProgram()); 744 REQUIRE_FALSE(ctx.varInfo(lp.getLiteral(a).var()).frozen()); 745 REQUIRE(ctx.varInfo(lp.getLiteral(b).var()).frozen()); 746 REQUIRE(ctx.varInfo(lp.getLiteral(c).var()).frozen()); 747 REQUIRE(ctx.varInfo(lp.getLiteral(d).var()).frozen()); 748 REQUIRE(ctx.varInfo(lp.getLiteral(e).var()).frozen()); 749 REQUIRE(ctx.varInfo(lp.getLiteral(h).var()).frozen()); 750 REQUIRE(ctx.varInfo(lp.getLiteral(i).var()).frozen()); 751 752 // minimize lits only frozen if constraint is actually used 753 REQUIRE_FALSE(ctx.varInfo(lp.getLiteral(f).var()).frozen()); 754 REQUIRE_FALSE(ctx.varInfo(lp.getLiteral(g).var()).frozen()); 755 ctx.minimize(); 756 REQUIRE(ctx.varInfo(lp.getLiteral(f).var()).frozen()); 757 REQUIRE(ctx.varInfo(lp.getLiteral(g).var()).frozen()); 758 } 759 760 SECTION("testExternalsAreFrozen") { 761 lpAdd(lp.start(ctx), 762 "#external a.\n"); 763 REQUIRE(lp.endProgram()); 764 REQUIRE(lp.getLiteral(a).var() == 1); 765 REQUIRE(ctx.varInfo(lp.getLiteral(a).var()).frozen()); 766 } 767 768 SECTION("testComputeTrueBug") { 769 lpAdd(lp.start(ctx), 770 "a :- not b.\n" 771 "b :- a.\n" 772 "a :- c.\n" 773 "c :- a.\n" 774 " :- not a.\n"); 775 REQUIRE_FALSE((lp.endProgram() && ctx.endInit())); 776 } 777 778 SECTION("testBackprop") { 779 lpAdd(lp.start(ctx, LogicProgram::AspOptions().backpropagate()), 780 "{e;f;g}.\n" 781 "d :- e, a.\n" 782 "a :- f, d.\n" 783 "b :- e, g.\n" 784 "c :- f, g.\n" 785 "h :- e, not d.\n" 786 "h :- f, not b.\n" 787 "h :- g, not c.\n" 788 " :- h.\n"); 789 REQUIRE((lp.endProgram() && ctx.endInit())); 790 REQUIRE(ctx.numVars() == 0); 791 } 792 SECTION("testBackpropTrueCon") { 793 Var x2 = 2, x3 = 3; 794 lpAdd(lp.start(ctx, LogicProgram::AspOptions().backpropagate()), 795 "x7.\n" 796 "{x2;x3}.\n" 797 "x4 :- not x6.\n" 798 " :- not x5.\n" 799 "x5 :- 1 {not x2, not x3}."); 800 REQUIRE((lp.endProgram() && ctx.endInit())); 801 ctx.master()->assume(lp.getLiteral(x2)) && ctx.master()->propagate(); 802 REQUIRE(ctx.master()->isFalse(lp.getLiteral(x3))); 803 ctx.master()->undoUntil(0); 804 ctx.master()->assume(lp.getLiteral(x3)) && ctx.master()->propagate(); 805 REQUIRE(ctx.master()->isFalse(lp.getLiteral(x2))); 806 } 807 SECTION("testBuildUnsat") { 808 lpAdd(lp.start(ctx), "x1. :- x1."); 809 REQUIRE_FALSE(lp.endProgram()); 810 std::stringstream exp("1 2 0 0\n0\n0\nB+\n0\nB-\n2\n0\n1\n"); 811 REQUIRE(compareSmodels(exp, lp)); 812 } 813 814 SECTION("testDontAddOnePredsThatAreNotHeads") { 815 lpAdd(lp.start(ctx), 816 "x1 :-not x2, not x3.\n" 817 "x3.\n" 818 "#output a : x1.\n" 819 "#output b : x2.\n" 820 "#output c : x3."); 821 REQUIRE(lp.endProgram()); 822 REQUIRE(0u == ctx.numVars()); 823 std::stringstream exp("1 3 0 0 \n0\n3 c\n0\nB+\n0\nB-\n0\n1\n"); 824 REQUIRE(compareSmodels(exp, lp)); 825 } 826 827 SECTION("testDontAddDuplicateBodies") { 828 lpAdd(lp.start(ctx), 829 "a :- b, not c.\n" 830 "d :- b, not c.\n" 831 "b. c."); 832 lp.addOutput("a", a).addOutput("b", b).addOutput("c", c); 833 REQUIRE(lp.endProgram()); 834 REQUIRE(0u == ctx.numVars()); 835 std::stringstream exp("1 2 0 0 \n1 3 0 0 \n0\n2 b\n3 c\n0\nB+\n0\nB-\n0\n1\n"); 836 REQUIRE(compareSmodels(exp, lp)); 837 } 838 SECTION("testDontAddUnsupported") { 839 lpAdd(lp.start(ctx), 840 "x1 :- x3, x2.\n" 841 "x3 :- not x4.\n" 842 "x2 :- x1."); 843 REQUIRE(lp.endProgram()); 844 std::stringstream exp("1 3 0 0 \n0"); 845 REQUIRE(compareSmodels(exp, lp)); 846 } 847 SECTION("testDontAddUnsupportedNoEq") { 848 lpAdd(lp.start(ctx, LogicProgram::AspOptions().noEq()), 849 "x1 :- x3, x2.\n" 850 "x3 :- not x4.\n" 851 "x2 :- x1."); 852 lp.addOutput("a", a).addOutput("b", b).addOutput("c", c); 853 REQUIRE(lp.endProgram()); 854 REQUIRE(ctx.numVars() <= 2u); 855 std::stringstream exp("1 3 0 0 \n0\n3 c\n0\nB+\n0\nB-\n0\n1\n"); 856 REQUIRE(compareSmodels(exp, lp)); 857 } 858 SECTION("testAddCardConstraint") { 859 lpAdd(lp.start(ctx), 860 "a :- 1 { not b, c, d }.\n" 861 "{b;c}."); 862 lp.addOutput("a", a).addOutput("b", b).addOutput("c", c); 863 864 REQUIRE(lp.endProgram()); 865 REQUIRE(3u == ctx.numVars()); 866 867 std::stringstream exp("2 1 2 1 1 2 3 \n3 2 2 3 0 0 \n0\n1 a\n2 b\n3 c\n0\nB+\n0\nB-\n0\n1\n"); 868 REQUIRE(compareSmodels(exp, lp)); 869 } 870 871 SECTION("testAddWeightConstraint") { 872 lpAdd(lp.start(ctx), 873 "a :- 2 {not b=1, c=2, d=2}.\n" 874 "{b;c}."); 875 lp.addOutput("a", a).addOutput("b", b).addOutput("c", c).addOutput("d", d); 876 877 REQUIRE(lp.endProgram()); 878 REQUIRE(3u == ctx.numVars()); 879 std::stringstream exp("5 1 2 2 1 2 3 1 2 \n3 2 2 3 0 0 \n0\n1 a\n2 b\n3 c\n0\nB+\n0\nB-\n0\n1\n"); 880 REQUIRE(compareSmodels(exp, lp)); 881 } 882 SECTION("testAddMinimizeConstraint") { 883 lpAdd(lp.start(ctx), 884 "a :- not b.\n" 885 "b :- not a.\n" 886 "#minimize{a}@0.\n" 887 "#minimize{b}@1.\n" 888 "#output a : a. #output b : b."); 889 REQUIRE(lp.endProgram()); 890 std::stringstream exp; 891 exp 892 << "6 0 1 0 1 1 \n" 893 << "6 0 1 0 2 1 \n" 894 << "1 1 1 1 2 \n" 895 << "1 2 1 1 1 \n" 896 << "0\n1 a\n2 b\n0\nB+\n0\nB-\n0\n1\n"; 897 REQUIRE(compareSmodels(exp, lp)); 898 } 899 SECTION("testEqOverChoiceRule") { 900 lpAdd(lp.start(ctx), 901 "{a}.\n" 902 "b :- a.\n"); 903 REQUIRE(lp.endProgram()); 904 REQUIRE(1u == ctx.numVars()); 905 std::stringstream exp; 906 exp 907 << "3 1 1 0 0 \n" 908 << "1 2 1 0 1 \n" 909 << "0\n0\nB+\n0\nB-\n0\n1\n"; 910 REQUIRE(compareSmodels(exp, lp)); 911 } 912 SECTION("testRemoveKnownAtomFromWeightRule") { 913 lpAdd(lp.start(ctx), 914 "{c, d}.\n" 915 "a." 916 "e :- 5 {a = 2, not b = 2, c = 1, d = 1}.\n"); 917 REQUIRE(lp.endProgram()); 918 std::stringstream exp; 919 exp << "1 1 0 0 \n" // a. 920 << "3 2 3 4 0 0 \n" // {c, d}. 921 << "2 5 2 0 1 3 4 \n" // e :- 1 { c, d }. 922 << "0\n"; 923 REQUIRE(compareSmodels(exp, lp)); 924 } 925 926 SECTION("testMergeEquivalentAtomsInConstraintRule") { 927 lpAdd(lp.start(ctx), 928 "{a, c}.\n" 929 "a :- b.\n" 930 "b :- a.\n" 931 "d :- 2 {a, b, c}.\n"); 932 REQUIRE(lp.endProgram()); 933 std::stringstream exp("5 4 2 2 0 1 3 2 1"); 934 // d :- 2 [a=2, c]. 935 REQUIRE(findSmodels(exp, lp)); 936 } 937 938 SECTION("testMergeEquivalentAtomsInWeightRule") { 939 lpAdd(lp.start(ctx), 940 "{a, c, e}.\n" 941 "a :- b.\n" 942 "b :- a.\n" 943 "d :- 3 {a = 1, c = 4, b = 2, e=1}.\n"); 944 REQUIRE(lp.endProgram()); 945 // x :- 3 [a=3, c=3,d=1]. 946 std::stringstream exp("5 4 3 3 0 1 3 5 3 3 1"); 947 REQUIRE(findSmodels(exp, lp)); 948 } 949 950 SECTION("testBothLitsInConstraintRule") { 951 lpAdd(lp.start(ctx), 952 "{a}.\n" 953 "b :- a.\n" 954 "c :- b.\n" 955 "d :- 1 {a, b, not b, not c}.\n"); 956 REQUIRE(lp.endProgram()); 957 // d :- 1 [a=2, not a=2]. 958 std::stringstream exp("5 4 1 2 1 1 1 2 2"); 959 REQUIRE(findSmodels(exp, lp)); 960 } 961 962 SECTION("testBothLitsInWeightRule") { 963 lpAdd(lp.start(ctx), 964 "{a, e}.\n" 965 "b :- a.\n" 966 "c :- b.\n" 967 "d :- 3 {a=3, not b=1, not c=3, e=2}.\n"); 968 REQUIRE(lp.endProgram()); 969 // d :- 3 [a=3, not a=4, e=2]. 970 std::stringstream exp("5 4 3 3 1 1 1 5 4 3 2"); 971 REQUIRE(findSmodels(exp, lp)); 972 } 973 974 SECTION("testWeightlessAtomsInWeightRule") { 975 lpAdd(lp.start(ctx), 976 "{a, b, c}.\n" 977 "d :- 1 {a=1, b=1, c=0}.\n"); 978 REQUIRE(lp.endProgram()); 979 // d :- 1 {a, b}. 980 std::stringstream exp("2 4 2 0 1 1 2"); 981 REQUIRE(findSmodels(exp, lp)); 982 } 983 984 SECTION("testSimplifyToNormal") { 985 lpAdd(lp.start(ctx), 986 "{a}.\n" 987 "b :- 2 {a=2,not c=1}.\n"); 988 REQUIRE(lp.endProgram()); 989 // b :- a. 990 std::stringstream exp("1 2 1 0 1"); 991 REQUIRE(findSmodels(exp, lp)); 992 } 993 SECTION("writeIntegrityConstraint") { 994 lpAdd(lp.start(ctx), 995 "{a;b;c}." 996 "a :- c, not b.\n" 997 "b :- c, not b.\n"); 998 REQUIRE(lp.endProgram()); 999 1000 // falseAtom :- c, not b. 1001 // compute {not falseAtom}. 1002 std::stringstream exp("1 4 2 1 2 3\nB-\n4"); 1003 REQUIRE(findSmodels(exp, lp)); 1004 } 1005 SECTION("testBackpropWrite") { 1006 lpAdd(lp.start(ctx, LogicProgram::AspOptions().backpropagate()), 1007 "a|b.\n" 1008 "c :- a.\n" 1009 "a :- c.\n" 1010 "d :- not c.\n" 1011 "e :- a,c.\n" 1012 " :- e.\n"); 1013 REQUIRE((lp.endProgram() && ctx.endInit())); 1014 REQUIRE(ctx.numVars() == 0); 1015 REQUIRE(ctx.master()->isFalse(lp.getLiteral(a))); 1016 REQUIRE(ctx.master()->isFalse(lp.getLiteral(c))); 1017 REQUIRE(ctx.master()->isTrue(lp.getLiteral(b))); 1018 REQUIRE(ctx.master()->isTrue(lp.getLiteral(d))); 1019 1020 std::stringstream exp("1 2 0 0\n1 4 0 0"); 1021 REQUIRE(findSmodels(exp, lp)); 1022 REQUIRE(!lp.isDefined(a)); 1023 REQUIRE(!lp.isDefined(c)); 1024 } 1025 1026 SECTION("testStatisticsObject") { 1027 StatisticObject stats = StatisticObject::map(&lp.stats); 1028 for (uint32 i = 0, end = stats.size(); i != end; ++i) { 1029 const char* k = stats.key(i); 1030 StatisticObject x = stats.at(k); 1031 REQUIRE(x.value() == 0.0); 1032 } 1033 lpAdd(lp.start(ctx), 1034 "a :- not b.\n" 1035 "b :- not a.\n"); 1036 lp.endProgram(); 1037 REQUIRE(stats.at("atoms").value() == (double)lp.stats.atoms); 1038 REQUIRE(stats.at("rules").value() == (double)lp.stats.rules[0].sum()); 1039 } 1040 SECTION("testFactIsDefined") { 1041 lp.start(ctx); 1042 lpAdd(lp, "a."); 1043 lp.endProgram(); 1044 REQUIRE(lp.isDefined(a)); 1045 } 1046 SECTION("testBogusAtomIsNotDefined") { 1047 lp.start(ctx); 1048 lp.endProgram(); 1049 REQUIRE_FALSE(lp.isDefined(0xDEAD)); 1050 REQUIRE_FALSE(lp.isExternal(0xDEAD)); 1051 REQUIRE(lit_false() == lp.getLiteral(0xDEAD)); 1052 } 1053 SECTION("testMakeAtomicCondition") { 1054 lpAdd(lp.start(ctx), "{a;b}."); 1055 Potassco::Lit_t cond[2] = { Potassco::lit(a), Potassco::neg(b) }; 1056 Id_t c1 = lp.newCondition(Potassco::toSpan(cond, 1)); 1057 Id_t c2 = lp.newCondition(Potassco::toSpan(cond + 1, 1)); 1058 REQUIRE(lp.endProgram()); 1059 REQUIRE(lp.getLiteral(c1) == lp.getLiteral(a)); 1060 REQUIRE(lp.getLiteral(c2) == ~lp.getLiteral(b)); 1061 } 1062 1063 SECTION("testMakeComplexCondition") { 1064 lpAdd(lp.start(ctx), "{a;b}."); 1065 Potassco::Lit_t cond[2] = { Potassco::lit(a), Potassco::neg(b) }; 1066 Id_t c1 = lp.newCondition(Potassco::toSpan(cond, 0)); 1067 Id_t c2 = lp.newCondition(Potassco::toSpan(cond, 2)); 1068 REQUIRE((lp.endProgram() && ctx.endInit())); 1069 REQUIRE(lp.getLiteral(c1) == lit_true()); 1070 Literal c2Lit = lp.getLiteral(c2); 1071 Solver& s = *ctx.master(); 1072 REQUIRE(value_free == s.value(c2Lit.var())); 1073 REQUIRE((s.assume(c2Lit) && s.propagate())); 1074 REQUIRE(s.isTrue(lp.getLiteral(a))); 1075 REQUIRE(s.isFalse(lp.getLiteral(b))); 1076 } 1077 SECTION("testMakeFalseCondition") { 1078 lp.start(ctx); 1079 Var a = lp.newAtom(); 1080 Potassco::Lit_t cond[2] ={Potassco::lit(a), Potassco::neg(a)}; 1081 Id_t c1 = lp.newCondition(Potassco::toSpan(cond, 2)); 1082 REQUIRE((lp.endProgram() && ctx.endInit())); 1083 REQUIRE(lp.getLiteral(c1) == lit_false()); 1084 REQUIRE_THROWS_AS(solverLiteral(lp, c1), std::logic_error); 1085 } 1086 SECTION("testMakeInvalidCondition") { 1087 lp.start(ctx); 1088 Var a = lp.newAtom(); 1089 Var b = lp.newAtom(); 1090 Potassco::Lit_t cond[2] ={Potassco::lit(a), Potassco::neg(b)}; 1091 Id_t c1 = lp.newCondition(Potassco::toSpan(cond, 2)); 1092 Potassco::Lit_t cAsLit = static_cast<Potassco::Lit_t>(c1); 1093 REQUIRE_THROWS_AS(lp.newCondition(Potassco::toSpan(&cAsLit, 1)), std::overflow_error); 1094 } 1095 SECTION("testExtractCondition") { 1096 lpAdd(lp.start(ctx), "{a;b}."); 1097 Potassco::Lit_t cond[2] = { Potassco::lit(a), Potassco::lit(b) }; 1098 Id_t c1 = lp.newCondition(Potassco::toSpan(cond, 2)); 1099 REQUIRE(lp.endProgram()); 1100 1101 Potassco::LitVec ext; 1102 lp.extractCondition(c1, ext); 1103 REQUIRE((ext.size() == 2 && std::equal(ext.begin(), ext.end(), cond))); 1104 1105 lp.dispose(false); 1106 REQUIRE_THROWS_AS(lp.extractCondition(c1, ext), std::logic_error); 1107 } 1108 SECTION("testGetConditionAfterDispose") { 1109 lpAdd(lp.start(ctx), "{a;b}."); 1110 Potassco::Lit_t cond[2] = { Potassco::lit(a), Potassco::lit(b) }; 1111 Id_t c1 = lp.newCondition(Potassco::toSpan(cond, 2)); 1112 REQUIRE(lp.endProgram()); 1113 1114 REQUIRE(!isSentinel(lp.getLiteral(c1))); 1115 lp.dispose(false); 1116 REQUIRE_THROWS_AS(lp.getLiteral(c1), std::logic_error); 1117 } 1118 1119 SECTION("testTheoryAtomsAreFrozen") { 1120 lpAdd(lp.start(ctx), "b :- a."); 1121 Potassco::TheoryData& t = lp.theoryData(); 1122 t.addTerm(0, "Theory"); 1123 t.addAtom(a, 0, Potassco::toSpan<Potassco::Id_t>()); 1124 lp.endProgram(); 1125 REQUIRE(lp.getLiteral(a) != lit_false()); 1126 REQUIRE(lp.isExternal(a)); 1127 REQUIRE(lp.getLiteral(b) != lit_false()); 1128 ctx.endInit(); 1129 REQUIRE(ctx.varInfo(lp.getLiteral(a).var()).frozen()); 1130 } 1131 1132 SECTION("testAcceptIgnoresAuxChoicesFromTheoryAtoms") { 1133 lp.start(ctx); 1134 a = lp.newAtom(); 1135 Potassco::TheoryData& t = lp.theoryData(); 1136 t.addTerm(0, "Theory"); 1137 t.addAtom(a, 0, Potassco::toSpan<Potassco::Id_t>()); 1138 lp.endProgram(); 1139 REQUIRE(lp.getLiteral(a) != lit_false()); 1140 std::stringstream str; 1141 AspParser::write(lp, str, AspParser::format_aspif); 1142 for (std::string x; std::getline(str, x);) { 1143 REQUIRE(x.find("1 1") != 0); 1144 REQUIRE(x.find("5 1") != 0); 1145 } 1146 ctx.endInit(); 1147 REQUIRE(ctx.varInfo(lp.getLiteral(a).var()).frozen()); 1148 } 1149 SECTION("testFalseHeadTheoryAtomsAreRemoved") { 1150 lpAdd(lp.start(ctx), "a :- b."); 1151 Potassco::TheoryData& t = lp.theoryData(); 1152 t.addTerm(0, "Theory"); 1153 t.addAtom(a, 0, Potassco::toSpan<Potassco::Id_t>()); 1154 lp.endProgram(); 1155 REQUIRE(lp.getLiteral(a) == lit_false()); 1156 REQUIRE(lp.getLiteral(b) == lit_false()); 1157 REQUIRE(t.numAtoms() == 0); 1158 } 1159 1160 SECTION("testTheoryHeadEvenIfRuleIsDropped") { 1161 lpAdd(lp.start(ctx), 1162 ":- b.\n" 1163 "a :- b, c.\n"); 1164 Potassco::TheoryData& t = lp.theoryData(); 1165 t.addTerm(0, "ta"); 1166 t.addTerm(1, "tc"); 1167 t.addAtom(a, 0, Potassco::toSpan<Potassco::Id_t>()); 1168 t.addAtom(c, 1, Potassco::toSpan<Potassco::Id_t>()); 1169 REQUIRE(t.numAtoms() == 2); 1170 lp.endProgram(); 1171 REQUIRE(lp.getLiteral(a) == lit_false()); 1172 REQUIRE(lp.getLiteral(b) == lit_false()); 1173 REQUIRE(lp.getLiteral(c) != lit_false()); 1174 REQUIRE(t.numAtoms() == 1); 1175 } 1176 1177 SECTION("testFalseBodyTheoryAtomsAreKept") { 1178 lp.start(ctx); 1179 a = lp.newAtom(); 1180 Potassco::TheoryData& t = lp.theoryData(); 1181 t.addTerm(0, "Theory"); 1182 t.addAtom(a, 0, Potassco::toSpan<Potassco::Id_t>()); 1183 lpAdd(lp, ":- a."); 1184 lp.endProgram(); 1185 REQUIRE(lp.getLiteral(a) == lit_false()); 1186 REQUIRE(t.numAtoms() == 1); 1187 std::stringstream str; 1188 AspParser::write(lp, str, AspParser::format_aspif); 1189 REQUIRE(str.str().find("1 0 0 0 1 1") != std::string::npos); 1190 } 1191 SECTION("testOutputFactsNotSupportedInSmodels") { 1192 lp.start(ctx); 1193 lp.addOutput("Hallo", Potassco::toSpan<Potassco::Lit_t>()); 1194 lp.addOutput("World", Potassco::toSpan<Potassco::Lit_t>()); 1195 lp.endProgram(); 1196 REQUIRE_FALSE(lp.supportsSmodels()); 1197 } 1198 SECTION("testDisposeBug") { 1199 lp.start(ctx); 1200 lp.theoryData().addTerm(0, 99); 1201 lp.start(ctx); 1202 REQUIRE_FALSE(lp.theoryData().hasTerm(0)); 1203 } 1204 } 1205 1206 TEST_CASE("Incremental logic program", "[asp]") { 1207 SharedContext ctx; 1208 LogicProgram lp; 1209 Var a = 1, b = 2, c = 3, d = 4, e = 5, f = 6; 1210 SECTION("testSimple") { 1211 lp.start(ctx); 1212 lp.updateProgram(); 1213 lpAdd(lp, "a :- not b. b :- not a."); 1214 REQUIRE((lp.endProgram() && ctx.endInit())); 1215 REQUIRE(ctx.numVars() == 1); 1216 REQUIRE(lp.getLiteral(a) == ~lp.getLiteral(b)); 1217 lp.updateProgram(); 1218 lpAdd(lp, 1219 "c :- a, not d.\n" 1220 "d :- b, not c.\n" 1221 "e :- d.\n"); 1222 REQUIRE((lp.endProgram() && ctx.endInit())); 1223 REQUIRE(ctx.numVars() == 3); 1224 REQUIRE(lp.getLiteral(a) == ~lp.getLiteral(b)); 1225 REQUIRE(lp.getLiteral(e) == lp.getLiteral(d)); 1226 } 1227 SECTION("testDistinctFacts") { 1228 lp.start(ctx); 1229 lp.enableDistinctTrue(); 1230 lp.updateProgram(); 1231 lpAdd(lp, 1232 "a.\n" 1233 "b :- not c.\n" 1234 "c.\n"); 1235 REQUIRE((lp.endProgram() && ctx.endInit())); 1236 REQUIRE(ctx.numVars() == 0); 1237 REQUIRE(lp.getLiteral(a) == lit_true()); 1238 REQUIRE(lp.getLiteral(b) == lit_false()); 1239 REQUIRE(lp.getLiteral(b, MapLit_t::Refined) == lit_false()); 1240 REQUIRE(lp.getLiteral(c) == lit_true()); 1241 lp.updateProgram(); 1242 Var g = f + 1; 1243 lpAdd(lp, 1244 "g :- not f.\n" 1245 "d.\n" 1246 "e :- f.\n" 1247 "f.\n"); 1248 REQUIRE((lp.endProgram() && ctx.endInit())); 1249 REQUIRE(ctx.numVars() == 1); 1250 REQUIRE(lp.getLiteral(d) == lit_true()); 1251 REQUIRE(lp.getLiteral(e) == lit_true()); 1252 REQUIRE(lp.getLiteral(f) == lit_true()); 1253 REQUIRE(lp.getLiteral(g) == lit_false()); 1254 REQUIRE(lp.getLiteral(d, MapLit_t::Refined) == posLit(1)); 1255 REQUIRE(lp.getLiteral(e, MapLit_t::Refined) == posLit(1)); 1256 REQUIRE(lp.getLiteral(f, MapLit_t::Refined) == posLit(1)); 1257 REQUIRE(lp.getLiteral(g, MapLit_t::Refined) == negLit(1)); 1258 } 1259 SECTION("testDistinctFactsSimple") { 1260 lp.start(ctx, LogicProgram::AspOptions().noEq()); 1261 lp.enableDistinctTrue(); 1262 lp.updateProgram(); 1263 lpAdd(lp, "a.\n"); 1264 REQUIRE((lp.endProgram() && ctx.endInit())); 1265 REQUIRE(ctx.numVars() == 0); 1266 REQUIRE(lp.getLiteral(a) == lit_true()); 1267 lp.updateProgram(); 1268 lpAdd(lp, 1269 "b :- d.\n" 1270 "c :- e.\n" 1271 "d. e.\n"); 1272 REQUIRE((lp.endProgram() && ctx.endInit())); 1273 REQUIRE(ctx.numVars() == 1); 1274 REQUIRE(lp.getLiteral(b) == lit_true()); 1275 REQUIRE(lp.getLiteral(c) == lit_true()); 1276 REQUIRE(lp.getLiteral(d) == lit_true()); 1277 REQUIRE(lp.getLiteral(b, MapLit_t::Refined) == posLit(1)); 1278 REQUIRE(lp.getLiteral(c, MapLit_t::Refined) == posLit(1)); 1279 REQUIRE(lp.getLiteral(d, MapLit_t::Refined) == posLit(1)); 1280 lp.updateProgram(); 1281 lpAdd(lp, "f."); 1282 REQUIRE((lp.endProgram() && ctx.endInit())); 1283 REQUIRE(ctx.numVars() == 2); 1284 REQUIRE(lp.getLiteral(a, MapLit_t::Refined) == posLit(0)); 1285 REQUIRE(lp.getLiteral(b, MapLit_t::Refined) == posLit(1)); 1286 REQUIRE(lp.getLiteral(f, MapLit_t::Refined) == posLit(2)); 1287 } 1288 SECTION("testFreeze") { 1289 lp.start(ctx, LogicProgram::AspOptions().noEq()); 1290 lp.updateProgram(); 1291 lpAdd(lp, 1292 "{d}.\n" 1293 "a :- not c.\n" 1294 "b :- a, d.\n" 1295 "#external c."); 1296 REQUIRE((lp.endProgram() && ctx.endInit())); 1297 REQUIRE(lp.getLiteral(c) != lit_false()); 1298 Solver& solver = *ctx.master(); 1299 solver.assume(lp.getLiteral(c)); 1300 solver.propagate(); 1301 REQUIRE(ctx.master()->isFalse(lp.getLiteral(b))); 1302 solver.undoUntil(0); 1303 1304 lp.updateProgram(); 1305 lpAdd(lp, 1306 "{e}.\n" 1307 "c :- e.\n" 1308 "#external c. [release]"); 1309 1310 REQUIRE((lp.endProgram() && ctx.endInit())); 1311 solver.assume(lp.getLiteral(e)); 1312 solver.propagate(); 1313 REQUIRE(ctx.master()->isFalse(lp.getLiteral(b))); 1314 solver.undoUntil(0); 1315 solver.assume(~lp.getLiteral(e)); 1316 solver.propagate(); 1317 REQUIRE(ctx.master()->isFalse(lp.getLiteral(c))); 1318 solver.assume(lp.getLiteral(d)); 1319 solver.propagate(); 1320 REQUIRE(ctx.master()->isTrue(lp.getLiteral(b))); 1321 } 1322 SECTION("testFreezeValue") { 1323 lp.start(ctx, LogicProgram::AspOptions().noEq()); 1324 lp.updateProgram(); 1325 lp.freeze(a).freeze(b, value_true).freeze(c, value_false); 1326 1327 REQUIRE((lp.endProgram() && ctx.endInit())); 1328 LitVec assume; 1329 lp.getAssumptions(assume); 1330 Solver& solver = *ctx.master(); 1331 solver.pushRoot(assume); 1332 REQUIRE(solver.isFalse(lp.getLiteral(a))); 1333 REQUIRE(solver.isTrue(lp.getLiteral(b))); 1334 REQUIRE(solver.isFalse(lp.getLiteral(c))); 1335 solver.popRootLevel(solver.decisionLevel()); 1336 1337 lp.updateProgram(); 1338 lp.unfreeze(a).freeze(c, value_true).freeze(b, value_true).freeze(b, value_false); 1339 REQUIRE((lp.endProgram() && ctx.endInit())); 1340 assume.clear(); 1341 lp.getAssumptions(assume); 1342 REQUIRE((assume.size() == 2 && solver.isFalse(lp.getLiteral(a)))); 1343 solver.pushRoot(assume); 1344 REQUIRE(solver.isFalse(lp.getLiteral(b))); 1345 REQUIRE(solver.isTrue(lp.getLiteral(c))); 1346 } 1347 1348 SECTION("testFreezeOpen") { 1349 lp.start(ctx, LogicProgram::AspOptions().noEq()); 1350 // I1: 1351 // freeze(a, value_free) 1352 lp.updateProgram(); 1353 lp.freeze(a, value_free); 1354 REQUIRE((lp.endProgram() && ctx.endInit())); 1355 LitVec assume; 1356 lp.getAssumptions(assume); 1357 Solver& solver = *ctx.master(); 1358 REQUIRE(assume.empty()); 1359 REQUIRE(solver.value(lp.getLiteral(a).var()) == value_free); 1360 1361 // I2: 1362 lp.updateProgram(); 1363 REQUIRE((lp.endProgram() && ctx.endInit())); 1364 assume.clear(); 1365 lp.getAssumptions(assume); 1366 REQUIRE(assume.empty()); 1367 REQUIRE(solver.value(lp.getLiteral(a).var()) == value_free); 1368 1369 // I3: 1370 lp.updateProgram(); 1371 lp.freeze(a, value_true); 1372 REQUIRE((lp.endProgram() && ctx.endInit())); 1373 assume.clear(); 1374 lp.getAssumptions(assume); 1375 REQUIRE((assume.size() == 1 && assume[0] == lp.getLiteral(a))); 1376 } 1377 SECTION("testKeepFrozen") { 1378 lp.start(ctx); 1379 // I0: 1380 lp.updateProgram(); 1381 lp.freeze(a); 1382 1383 REQUIRE(lp.endProgram()); 1384 PrgAtom* x = lp.getAtom(a); 1385 Literal xLit = x->literal(); 1386 // I1: 1387 lp.updateProgram(); 1388 REQUIRE(lp.endProgram()); 1389 REQUIRE(x->literal() == xLit); 1390 REQUIRE(x->frozen()); 1391 } 1392 SECTION("testFreezeCompute") { 1393 lp.start(ctx); 1394 lp.updateProgram(); 1395 lpAdd(lp, 1396 "#external a. #external b. #external c. #external d.\n" 1397 ":- not a.\n" 1398 ":- not b.\n" 1399 ":- c.\n" 1400 ":- d.\n"); 1401 REQUIRE(lp.endProgram()); 1402 PrgAtom* x = lp.getAtom(a); 1403 PrgAtom* y = lp.getAtom(b); 1404 REQUIRE((x->frozen() && y->frozen())); 1405 REQUIRE(x->literal() != y->literal()); 1406 PrgAtom* z = lp.getAtom(c); 1407 PrgAtom* z2 = lp.getAtom(d); 1408 REQUIRE((z->frozen() && z2->frozen())); 1409 REQUIRE((z->literal() == z2->literal())); 1410 // I1: 1411 lp.updateProgram(); 1412 lpAdd(lp, ":- a."); 1413 REQUIRE_FALSE(lp.endProgram()); 1414 } 1415 SECTION("testUnfreezeUnsupp") { 1416 lp.start(ctx, LogicProgram::AspOptions().noEq()); 1417 lp.updateProgram(); 1418 lpAdd(lp, "a :- not b. #external b."); 1419 REQUIRE(lp.endProgram()); 1420 DefaultUnfoundedCheck* ufsCheck = 0; 1421 if (ctx.sccGraph.get()) { 1422 ctx.master()->addPost(ufsCheck = new DefaultUnfoundedCheck(*ctx.sccGraph)); 1423 } 1424 ctx.endInit(); 1425 lp.updateProgram(); 1426 lpAdd(lp, 1427 "c :- b.\n" 1428 "b :- c.\n" 1429 "#external b. [release]"); 1430 REQUIRE(lp.endProgram()); 1431 if (ctx.sccGraph.get() && !ufsCheck) { 1432 ctx.master()->addPost(ufsCheck = new DefaultUnfoundedCheck(*ctx.sccGraph)); 1433 } 1434 ctx.endInit(); 1435 REQUIRE(ctx.master()->isTrue(lp.getLiteral(a))); 1436 REQUIRE(ctx.master()->isFalse(lp.getLiteral(b))); 1437 REQUIRE(ctx.master()->isFalse(lp.getLiteral(c))); 1438 } 1439 1440 SECTION("testUnfreezeCompute") { 1441 lp.start(ctx); 1442 lp.updateProgram(); 1443 lpAdd(lp, 1444 "{d}.\n" 1445 "a :- b, c.\n" 1446 "b :- d.\n" 1447 "#external c."); 1448 REQUIRE((lp.endProgram() && ctx.endInit())); 1449 REQUIRE(3u == ctx.numConstraints()); 1450 1451 lp.updateProgram(); 1452 lpAdd(lp, 1453 "#external c.[release]\n" 1454 ":- c.\n"); 1455 REQUIRE((lp.endProgram() && ctx.endInit())); 1456 REQUIRE(3u >= ctx.numConstraints()); 1457 REQUIRE(ctx.master()->numFreeVars() == 1); 1458 } 1459 1460 SECTION("testCompute") { 1461 lp.start(ctx, LogicProgram::AspOptions()); 1462 lp.updateProgram(); 1463 Var x2 = 2, x3 = 3, x4 = 4; 1464 lpAdd(lp, 1465 "{x2;x3}.\n" 1466 "x1 :- x2, x3.\n" 1467 " :- x1.\n"); 1468 1469 REQUIRE((lp.endProgram() && ctx.endInit())); 1470 lp.updateProgram(); 1471 lpAdd(lp, "{x4}. :- x2, x4."); 1472 1473 REQUIRE((lp.endProgram() && ctx.endInit())); 1474 ctx.master()->assume(lp.getLiteral(x2)); 1475 ctx.master()->propagate(); 1476 REQUIRE(ctx.master()->isFalse(lp.getLiteral(x3))); 1477 REQUIRE(ctx.master()->isFalse(lp.getLiteral(x4))); 1478 } 1479 SECTION("testComputeBackprop") { 1480 lp.start(ctx, LogicProgram::AspOptions().backpropagate()); 1481 lp.updateProgram(); 1482 lpAdd(lp, 1483 "a :- not b.\n" 1484 "b :- not a.\n" 1485 " :- not a.\n"); 1486 REQUIRE((lp.endProgram() && ctx.endInit())); 1487 // I2: 1488 lp.updateProgram(); 1489 lpAdd(lp, "c :- b. d :- not b."); 1490 REQUIRE((lp.endProgram() && ctx.endInit())); 1491 REQUIRE_FALSE(lp.getAtom(c)->hasVar()); 1492 REQUIRE(lit_true() == lp.getLiteral(d)); 1493 } 1494 1495 SECTION("testBackpropStep") { 1496 lp.start(ctx); 1497 // I1: 1498 lp.updateProgram(); 1499 lpAdd(lp, "{a}."); 1500 REQUIRE((lp.endProgram() && ctx.endInit())); 1501 // I2: 1502 lp.updateProgram(); 1503 lpAdd(lp, "{c}. b :- a, c. :- not b."); 1504 REQUIRE((lp.endProgram() && ctx.endInit())); 1505 REQUIRE(ctx.master()->isTrue(lp.getLiteral(a))); 1506 } 1507 1508 SECTION("testEq") { 1509 lp.start(ctx); 1510 lp.updateProgram(); 1511 lpAdd(lp, 1512 "{c;d}.\n" 1513 "a :- c.\n" 1514 "a :- d.\n" 1515 "b :- a.\n"); 1516 1517 // b == a 1518 REQUIRE((lp.endProgram() && ctx.endInit())); 1519 REQUIRE(lp.isDefined(a)); 1520 REQUIRE_FALSE(lp.isDefined(b)); 1521 1522 std::stringstream exp("1 2 1 0 1"); 1523 REQUIRE(findSmodels(exp, lp)); 1524 lp.updateProgram(); 1525 lpAdd(lp, 1526 "e :- a, b.\n" 1527 "#output e : e.\n"); 1528 REQUIRE((lp.endProgram() && ctx.endInit())); 1529 exp.str("1 5 1 0 1\n5 e"); 1530 REQUIRE(findSmodels(exp, lp)); 1531 } 1532 1533 SECTION("testSimplifyRuleEq") { 1534 lp.start(ctx); 1535 lp.updateProgram(); 1536 lpAdd(lp, 1537 "{x3}.\n" 1538 "x1 :- x3.\n" 1539 "x2 :- x3.\n"); 1540 1541 // x1 == x2 1542 REQUIRE((lp.endProgram() && ctx.endInit())); 1543 uint32 x1 = lp.getAtom(1)->id(); 1544 uint32 x2 = lp.getAtom(2)->id(); 1545 REQUIRE(x1 == x2); 1546 1547 lp.updateProgram(); 1548 1549 lpAdd(lp, 1550 "{x4}.\n" 1551 "x5 :- 2{x1, x2, x4}."); 1552 REQUIRE(lp.endProgram()); 1553 REQUIRE(lp.getAtom(5)->supports() == 1); 1554 PrgBody* body = lp.getBody(lp.getAtom(5)->supps_begin()->node()); 1555 REQUIRE(body->type() == Potassco::Body_t::Sum); 1556 REQUIRE(body->bound() == 2); 1557 REQUIRE(body->size() == 2); 1558 1559 uint32 eqIdx = body->goal(0).var() == 4; 1560 REQUIRE(body->weight(eqIdx) == 2); 1561 REQUIRE(body->weight(1 - eqIdx) == 1); 1562 } 1563 1564 SECTION("testEqUnfreeze") { 1565 lp.start(ctx); 1566 lp.updateProgram(); 1567 lp.freeze(a); 1568 lp.endProgram(); 1569 lp.updateProgram(); 1570 lpAdd(lp, 1571 "{d}.\n" 1572 "a :- c.\n" 1573 "b :- d, not a.\n" 1574 "#external a. [release]"); 1575 1576 lp.endProgram(); 1577 REQUIRE((ctx.numVars() == 2 && ctx.master()->numFreeVars() == 1)); 1578 REQUIRE(lp.getLiteral(b) == lp.getLiteral(d)); 1579 } 1580 1581 SECTION("testEqComplement") { 1582 lp.start(ctx); 1583 lp.updateProgram(); 1584 lpAdd(lp, "a :- not b. b :- not a."); 1585 1586 REQUIRE((lp.endProgram() && ctx.endInit())); 1587 PrgAtom* na = lp.getAtom(a); 1588 PrgAtom* nb = lp.getAtom(b); 1589 REQUIRE(nb->literal() == ~na->literal()); 1590 // I1: 1591 lp.updateProgram(); 1592 lpAdd(lp, "c :- a, b."); 1593 REQUIRE(lp.endProgram()); 1594 PrgAtom* nc = lp.getAtom(c); 1595 REQUIRE(nc->hasVar() == false); 1596 } 1597 1598 SECTION("testEqUpdateAssigned") { 1599 lp.start(ctx); 1600 // I0: 1601 lp.updateProgram(); 1602 lp.freeze(a); 1603 REQUIRE((lp.endProgram() && ctx.endInit())); 1604 1605 // I1: 1606 lp.updateProgram(); 1607 lpAdd(lp, "a :- b. b :- a."); 1608 1609 PrgAtom* x = lp.getAtom(a); 1610 x->setValue(value_weak_true); 1611 lp.endProgram(); 1612 // only weak-true so still relevant in bodies! 1613 REQUIRE(x->deps_begin()->sign() == false); 1614 } 1615 1616 SECTION("testEqResetState") { 1617 lp.start(ctx); 1618 // I0: 1619 lp.updateProgram(); 1620 lpAdd(lp, "{a;b}."); 1621 REQUIRE((lp.endProgram() && ctx.endInit())); 1622 1623 // I1: 1624 lp.updateProgram(); 1625 lpAdd(lp, 1626 "c :- f.\n" 1627 "d :- g.\n" 1628 "c :- d, a.\n" 1629 "d :- c, b.\n" 1630 "f :- e, not h.\n" 1631 "g :- e, not i.\n" 1632 "{e}."); 1633 lp.endProgram(); 1634 REQUIRE(lp.getAtom(c)->scc() == 0); 1635 REQUIRE(lp.getAtom(d)->scc() == 0); 1636 } 1637 1638 SECTION("testUnfreezeUnsuppEq") { 1639 lp.start(ctx, LogicProgram::AspOptions().noScc()); 1640 // I0: 1641 lp.updateProgram(); 1642 lp.freeze(a); 1643 1644 REQUIRE((lp.endProgram() && ctx.endInit())); 1645 // I1: 1646 lp.updateProgram(); 1647 lpAdd(lp, 1648 "a :- b.\n" 1649 "b :- a, c.\n" 1650 "{c}.\n"); 1651 lp.endProgram(); 1652 PrgAtom* x = lp.getAtom(a); 1653 PrgAtom* y = lp.getAtom(b); 1654 REQUIRE(ctx.master()->isFalse(x->literal())); 1655 REQUIRE(ctx.master()->isFalse(y->literal())); 1656 } 1657 1658 SECTION("testUnfreezeEq") { 1659 lp.start(ctx); 1660 // I0: 1661 lp.updateProgram(); 1662 lp.freeze(a); 1663 1664 REQUIRE(lp.endProgram()); 1665 // I1: 1666 lp.updateProgram(); 1667 lpAdd(lp, 1668 "{c}.\n" 1669 "b :- c.\n" 1670 "a :- b.\n"); 1671 PrgAtom* x = lp.getAtom(a); 1672 lp.endProgram(); 1673 // body {b} is eq to body {c} 1674 REQUIRE(ctx.master()->value(x->var()) == value_free); 1675 REQUIRE((x->supports() == 1 && x->supps_begin()->node() == 1)); 1676 } 1677 1678 SECTION("testStats") { 1679 LpStats incStats; 1680 lp.start(ctx, LogicProgram::AspOptions().noEq()); 1681 // I1: 1682 lp.updateProgram(); 1683 lpAdd(lp, 1684 "a :- not b.\n" 1685 "b :- not a.\n" 1686 "#external c.\n"); 1687 REQUIRE((lp.endProgram() && ctx.endInit())); 1688 incStats = lp.stats; 1689 REQUIRE(uint32(3) == incStats.atoms); 1690 REQUIRE(uint32(2) == incStats.bodies[0].sum()); 1691 REQUIRE(uint32(2) == incStats.rules[0].sum()); 1692 REQUIRE(uint32(0) == incStats.ufsNodes); 1693 REQUIRE(uint32(0) == incStats.sccs); 1694 1695 // I2: 1696 lp.updateProgram(); 1697 lpAdd(lp, 1698 "{c, f}.\n" 1699 "d :- not c.\n" 1700 "d :- e, f.\n" 1701 "e :- d, f.\n"); 1702 REQUIRE((lp.endProgram() && ctx.endInit())); 1703 incStats.accu(lp.stats); 1704 REQUIRE(uint32(6) == incStats.atoms); 1705 REQUIRE(uint32(5) == incStats.bodies[0].sum()); 1706 REQUIRE(uint32(6) == incStats.rules[0].sum()); 1707 REQUIRE(uint32(1) == incStats.sccs); 1708 // I3: 1709 lp.updateProgram(); 1710 lpAdd(lp, 1711 "g :- d, not i.\n" 1712 "i :- not g.\n" 1713 "g :- h.\n" 1714 "h :- g, not f.\n"); 1715 REQUIRE((lp.endProgram() && ctx.endInit())); 1716 incStats.accu(lp.stats); 1717 REQUIRE(uint32(9) == incStats.atoms); 1718 REQUIRE(uint32(9) == incStats.bodies[0].sum()); 1719 REQUIRE(uint32(10) == incStats.rules[0].sum()); 1720 REQUIRE(uint32(2) == incStats.sccs); 1721 } 1722 1723 SECTION("testTransform") { 1724 lp.start(ctx, LogicProgram::AspOptions().noEq()); 1725 lp.setExtendedRuleMode(LogicProgram::mode_transform); 1726 // I1: 1727 lp.updateProgram(); 1728 lpAdd(lp, "{a}. % -> a :- not a'. a' :- not a."); 1729 REQUIRE((lp.endProgram() && ctx.endInit())); 1730 REQUIRE(ctx.sccGraph.get() == 0); 1731 // I2: 1732 lp.updateProgram(); 1733 lpAdd(lp, 1734 "% a' must not take up id!\n" 1735 "b :- a.\n" 1736 "b :- c.\n" 1737 "c :- b.\n"); 1738 REQUIRE((lp.endProgram() && ctx.endInit())); 1739 REQUIRE(ctx.sccGraph.get() != 0); 1740 } 1741 1742 SECTION("testBackpropCompute") { 1743 lp.start(ctx); 1744 // I0: 1745 lp.updateProgram(); 1746 lpAdd(lp, 1747 "a :- b.\n" 1748 " :- not a.\n" 1749 "#external b."); 1750 REQUIRE(lp.endProgram()); 1751 REQUIRE(lp.getRootId(a) == 2); 1752 PrgAtom* x = lp.getAtom(b); 1753 REQUIRE(x->value() == value_weak_true); 1754 // I1: 1755 lp.updateProgram(); 1756 lpAdd(lp, "b :- c. c :- b."); 1757 1758 // UNSAT: no support for b,c 1759 REQUIRE_FALSE(lp.endProgram()); 1760 } 1761 1762 SECTION("testBackpropSolver") { 1763 lp.start(ctx); 1764 // I0: 1765 lp.updateProgram(); 1766 lpAdd(lp, 1767 "{a}.\n" 1768 ":- not a.\n" 1769 ":- not b.\n" 1770 "#external b."); 1771 REQUIRE(lp.endProgram()); 1772 PrgAtom* na = lp.getAtom(a); 1773 PrgAtom* nb = lp.getAtom(b); 1774 REQUIRE(na->value() == value_true); 1775 REQUIRE(nb->value() == value_weak_true); 1776 // I1: 1777 lp.updateProgram(); 1778 REQUIRE(lp.endProgram()); 1779 REQUIRE(na->value() == value_true); 1780 REQUIRE(nb->value() == value_weak_true); 1781 } 1782 1783 SECTION("testFreezeUnfreeze") { 1784 lp.start(ctx); 1785 // I0: 1786 lp.updateProgram(); 1787 lpAdd(lp, 1788 "{a}." 1789 "#external b.\n" 1790 "#external b. [release]"); 1791 REQUIRE(lp.endProgram()); 1792 REQUIRE(lit_false() == lp.getLiteral(b)); 1793 // I1: 1794 lp.updateProgram(); 1795 lpAdd(lp, 1796 "#external c.\n" 1797 "c :- b."); 1798 REQUIRE(lp.endProgram()); 1799 REQUIRE(ctx.master()->isFalse(lp.getLiteral(b))); 1800 } 1801 SECTION("testSymbolUpdate") { 1802 lp.start(ctx); 1803 // I0: 1804 lp.updateProgram(); 1805 lpAdd(lp, "{a}."); 1806 lp.addOutput("a", a); 1807 REQUIRE(lp.endProgram()); 1808 uint32 os = ctx.output.size(); 1809 // I1: 1810 lp.updateProgram(); 1811 lpAdd(lp, "{b;c}."); 1812 lp.addOutput("b", b); 1813 1814 REQUIRE(lp.endProgram()); 1815 REQUIRE(!isSentinel(lp.getLiteral(c))); 1816 REQUIRE(os + 1 == ctx.output.size()); 1817 } 1818 SECTION("testFreezeDefined") { 1819 lp.start(ctx); 1820 // I0: 1821 lp.updateProgram(); 1822 lpAdd(lp, "{a}."); 1823 REQUIRE(lp.endProgram()); 1824 // I1: 1825 lp.updateProgram(); 1826 lpAdd(lp, "#external a."); 1827 REQUIRE(lp.endProgram()); 1828 REQUIRE(lp.getAtom(a)->frozen() == false); 1829 } 1830 SECTION("testUnfreezeDefined") { 1831 lp.start(ctx); 1832 // I0: 1833 lp.updateProgram(); 1834 lpAdd(lp, "{a}."); 1835 REQUIRE(lp.endProgram()); 1836 // I1: 1837 lp.updateProgram(); 1838 lpAdd(lp, "#external a. [release]"); 1839 REQUIRE(lp.endProgram()); 1840 REQUIRE(!ctx.master()->isFalse(lp.getLiteral(a))); 1841 } 1842 SECTION("testUnfreezeAsFact") { 1843 lp.start(ctx); 1844 // I0: 1845 lp.updateProgram(); 1846 lpAdd(lp, "#external a."); 1847 REQUIRE(lp.endProgram()); 1848 Literal litA = lp.getLiteral(a); 1849 // I1: 1850 lp.updateProgram(); 1851 lpAdd(lp, "a."); 1852 REQUIRE(true == lp.endProgram()); 1853 REQUIRE(litA == lp.getLiteral(a)); 1854 REQUIRE_FALSE(lp.isExternal(a)); 1855 REQUIRE(true == lp.isDefined(a)); 1856 REQUIRE(ctx.master()->isTrue(litA)); 1857 } 1858 SECTION("testImplicitUnfreeze") { 1859 lp.start(ctx); 1860 // I0: 1861 lp.updateProgram(); 1862 lpAdd(lp, "#external a."); 1863 REQUIRE(lp.endProgram()); 1864 REQUIRE(lp.getAtom(a)->frozen() == true); 1865 REQUIRE(!ctx.master()->isFalse(lp.getLiteral(a))); 1866 // I1: 1867 lp.updateProgram(); 1868 lpAdd(lp, "{a}."); 1869 REQUIRE(lp.endProgram()); 1870 REQUIRE(lp.getAtom(a)->frozen() == false); 1871 } 1872 SECTION("testRedefine") { 1873 lp.start(ctx); 1874 // I0: 1875 lp.updateProgram(); 1876 lpAdd(lp, "{a}."); 1877 REQUIRE(lp.endProgram()); 1878 // I1: 1879 lp.updateProgram(); 1880 REQUIRE_THROWS_AS(lpAdd(lp, "{a}."), RedefinitionError); 1881 } 1882 SECTION("testGetAssumptions") { 1883 lp.start(ctx); 1884 // I0: 1885 lp.updateProgram(); 1886 lpAdd(lp, "#external a. #external b."); 1887 REQUIRE(lp.endProgram()); 1888 LitVec assume; 1889 lp.getAssumptions(assume); 1890 REQUIRE((assume.size() == 2 && assume[0] == ~lp.getLiteral(a) && assume[1] == ~lp.getLiteral(b))); 1891 } 1892 1893 SECTION("testSimplifyCard") { 1894 lp.start(ctx); 1895 // I0: 1896 lp.updateProgram(); 1897 lpAdd(lp, "a."); 1898 REQUIRE(lp.endProgram()); 1899 lp.updateProgram(); 1900 lpAdd(lp, 1901 "b :- 1 {c, a}.\n" 1902 "d :- 1 {c, b}.\n" 1903 "c :- a, b."); 1904 REQUIRE(lp.endProgram()); 1905 } 1906 1907 SECTION("testSimplifyMinimize") { 1908 lp.start(ctx); 1909 // I0: 1910 lp.updateProgram(); 1911 lpAdd(lp, "a. #minimize{a}."); 1912 REQUIRE(lp.endProgram()); 1913 REQUIRE(ctx.minimize()->adjust(0) == 1); 1914 ctx.removeMinimize(); 1915 1916 lp.updateProgram(); 1917 lpAdd(lp, "#minimize{a}."); 1918 REQUIRE(lp.endProgram()); 1919 REQUIRE(ctx.hasMinimize()); 1920 REQUIRE(ctx.minimize()->adjust(0) == 1); 1921 REQUIRE(lp.endProgram()); 1922 } 1923 1924 SECTION("testEqOverNeg") { 1925 lp.start(ctx); 1926 // I0: {a}. 1927 lp.updateProgram(); 1928 lpAdd(lp, "{a}."); 1929 REQUIRE(lp.endProgram()); 1930 // I1: 1931 lp.updateProgram(); 1932 lpAdd(lp, 1933 "b :- not a.\n" 1934 "c :- b.\n" 1935 "c :- f.\n" 1936 "d :- c.\n" 1937 "e :- d.\n" 1938 "g :- c.\n" 1939 "h :- not f, c.\n" 1940 " :- not e.\n" 1941 " :- not h.\n"); 1942 REQUIRE(lp.endProgram()); 1943 REQUIRE((ctx.numVars() == 1 && ctx.master()->isFalse(lp.getLiteral(a)))); 1944 } 1945 SECTION("testKeepExternalValue") { 1946 lp.start(ctx); 1947 // I0: 1948 lp.updateProgram(); 1949 lpAdd(lp, 1950 "b.\n" 1951 "a :- c.\n" 1952 " :- a.\n" 1953 "#external c. [true]"); 1954 1955 REQUIRE((lp.endProgram() && ctx.endInit())); 1956 LitVec assume; 1957 lp.getAssumptions(assume); 1958 REQUIRE_FALSE(ctx.master()->pushRoot(assume)); 1959 1960 REQUIRE(lp.update()); 1961 REQUIRE((lp.endProgram() && ctx.endInit())); 1962 assume.clear(); 1963 lp.getAssumptions(assume); 1964 REQUIRE_FALSE(ctx.master()->pushRoot(assume)); 1965 1966 REQUIRE(lp.update()); 1967 lpAdd(lp, "c."); 1968 REQUIRE_FALSE(lp.endProgram()); 1969 } 1970 1971 SECTION("testWriteMinimize") { 1972 lp.start(ctx); 1973 lp.updateProgram(); 1974 lpAdd(lp, "{a}. #minimize{a}."); 1975 lp.endProgram(); 1976 std::stringstream exp("6 0 1 0 1 1"); 1977 REQUIRE(findSmodels(exp, lp)); 1978 lp.updateProgram(); 1979 lpAdd(lp, "{b}. #minimize{b}."); 1980 1981 lp.endProgram(); 1982 exp.str("6 0 2 0 1 2 1 1"); 1983 REQUIRE(findSmodels(exp, lp)); 1984 lp.updateProgram(); 1985 lpAdd(lp, "{c}."); 1986 lp.endProgram(); 1987 exp.clear(); 1988 exp.seekg(0, ios::beg); 1989 REQUIRE_FALSE(findSmodels(exp, lp)); 1990 } 1991 SECTION("testWriteExternal") { 1992 lp.start(ctx); 1993 lp.updateProgram(); 1994 lpAdd(lp, "#external a."); 1995 lp.endProgram(); 1996 std::stringstream str; 1997 AspParser::write(lp, str, AspParser::format_aspif); 1998 bool foundA = false, foundB = false; 1999 for (std::string x; std::getline(str, x);) { 2000 if (x.find("5 1 2") == 0) { foundA = true; } 2001 if (x.find("5 2 2") == 0) { foundB = true; } 2002 } 2003 REQUIRE((foundA && !foundB)); 2004 lp.updateProgram(); 2005 lpAdd(lp, "#external b."); 2006 lp.endProgram(); 2007 foundA = foundB = false; 2008 str.clear(); 2009 AspParser::write(lp, str, AspParser::format_aspif); 2010 for (std::string x; std::getline(str, x);) { 2011 if (x.find("5 1 2") == 0) { foundA = true; } 2012 if (x.find("5 2 2") == 0) { foundB = true; } 2013 } 2014 REQUIRE((!foundA && foundB)); 2015 } 2016 2017 SECTION("testWriteExternalBug") { 2018 lp.start(ctx); 2019 lp.updateProgram(); 2020 lpAdd(lp, 2021 "#external a." 2022 "#external b." 2023 "#external c." 2024 "#external d." 2025 "b."); 2026 lp.endProgram(); 2027 std::stringstream str; 2028 AspParser::write(lp, str, AspParser::format_aspif); 2029 int foundA = 0, foundB = 0, foundC = 0, foundD = 0; 2030 for (std::string x; std::getline(str, x);) { 2031 if (x.find("5 1 2") == 0) { ++foundA; } 2032 if (x.find("5 2 2") == 0) { ++foundB; } 2033 if (x.find("5 3 2") == 0) { ++foundC; } 2034 if (x.find("5 4 2") == 0) { ++foundD; } 2035 } 2036 REQUIRE(foundA == 1); 2037 REQUIRE(foundB == 0); 2038 REQUIRE(foundC == 1); 2039 REQUIRE(foundD == 1); 2040 } 2041 2042 SECTION("testWriteUnfreeze") { 2043 lp.start(ctx); 2044 lp.updateProgram(); 2045 lpAdd(lp, "#external a."); 2046 lp.endProgram(); 2047 lp.updateProgram(); 2048 lpAdd(lp, "#external a. [release]"); 2049 lp.endProgram(); 2050 REQUIRE(!lp.isExternal(a)); 2051 std::stringstream str; 2052 AspParser::write(lp, str, AspParser::format_aspif); 2053 bool found = false; 2054 for (std::string x; std::getline(str, x);) { 2055 if (x.find("5 1 3") == 0) { found = true; break; } 2056 } 2057 REQUIRE(found); 2058 } 2059 SECTION("testSetInputAtoms") { 2060 lp.start(ctx); 2061 lp.updateProgram(); 2062 lpAdd(lp, "{a;b;c}."); 2063 REQUIRE(lp.numAtoms() == 3); 2064 lp.setMaxInputAtom(lp.numAtoms()); 2065 Var d = lp.newAtom(); 2066 Var e = lp.newAtom(); 2067 REQUIRE((d == 4 && e == 5)); 2068 lp.endProgram(); 2069 REQUIRE((lp.numAtoms() == 5 && lp.startAuxAtom() == 4 && lp.stats.auxAtoms == 2)); 2070 lp.updateProgram(); 2071 INFO("aux atoms are removed on update"); 2072 REQUIRE(lp.numAtoms() == 3); 2073 REQUIRE_FALSE(lp.validAtom(d)); 2074 REQUIRE_FALSE(lp.validAtom(e)); 2075 REQUIRE(d == lp.newAtom()); 2076 } 2077 2078 SECTION("testFreezeIsExternal") { 2079 lp.start(ctx); 2080 lp.updateProgram(); 2081 lpAdd(lp, "{b}. #external a."); 2082 REQUIRE(true == lp.isExternal(a)); 2083 REQUIRE_FALSE(lp.isExternal(b)); 2084 lp.endProgram(); 2085 REQUIRE(true == lp.isExternal(a)); 2086 REQUIRE_FALSE(lp.isExternal(b)); 2087 } 2088 SECTION("testUnfreezeIsNotExternal") { 2089 lp.start(ctx); 2090 lp.updateProgram(); 2091 lpAdd(lp, 2092 "#external a.\n" 2093 "#external b. [release]\n" 2094 "#external a. [release]\n" 2095 "#external b.\n"); 2096 REQUIRE_FALSE(lp.isExternal(a)); 2097 REQUIRE_FALSE(lp.isExternal(b)); 2098 lp.endProgram(); 2099 REQUIRE_FALSE(lp.isExternal(a)); 2100 REQUIRE_FALSE(lp.isExternal(b)); 2101 } 2102 SECTION("testFreezeStaysExternal") { 2103 lp.start(ctx); 2104 lp.updateProgram(); 2105 lpAdd(lp, "#external a."); 2106 REQUIRE(lp.isExternal(a)); 2107 lp.endProgram(); 2108 REQUIRE(lp.isExternal(a)); 2109 lp.updateProgram(); 2110 REQUIRE(lp.isExternal(a)); 2111 lp.endProgram(); 2112 REQUIRE(lp.isExternal(a)); 2113 } 2114 SECTION("testDefinedIsNotExternal") { 2115 lp.start(ctx); 2116 lp.updateProgram(); 2117 lpAdd(lp, "#external a."); 2118 lp.endProgram(); 2119 lp.updateProgram(); 2120 lpAdd(lp, "a :- b."); 2121 REQUIRE_FALSE(lp.isExternal(a)); 2122 lp.endProgram(); 2123 REQUIRE_FALSE(lp.isExternal(a)); 2124 } 2125 SECTION("testFactIsNotExternal") { 2126 lp.start(ctx); 2127 lp.updateProgram(); 2128 lpAdd(lp, "a. #external a."); 2129 lp.endProgram(); 2130 REQUIRE_FALSE(lp.isExternal(a)); 2131 } 2132 2133 SECTION("testAssumptionsAreVolatile") { 2134 lp.start(ctx); 2135 lp.updateProgram(); 2136 lpAdd(lp, "{a}. #assume{a}."); 2137 REQUIRE(lp.endProgram()); 2138 LitVec assume; 2139 lp.getAssumptions(assume); 2140 REQUIRE((assume.size() == 1 && assume[0] == lp.getLiteral(a))); 2141 lp.updateProgram(); 2142 lpAdd(lp, "#assume{not a}."); 2143 REQUIRE(lp.endProgram()); 2144 assume.clear(); 2145 lp.getAssumptions(assume); 2146 REQUIRE((assume.size() == 1 && assume[0] == ~lp.getLiteral(a))); 2147 } 2148 2149 SECTION("testAssumptionsAreFrozen") { 2150 lpAdd(lp.start(ctx), "{a}. #assume{a}."); 2151 REQUIRE(lp.endProgram()); 2152 REQUIRE(lp.getLiteral(a).var() == 1); 2153 REQUIRE(ctx.varInfo(lp.getLiteral(a).var()).frozen()); 2154 } 2155 2156 SECTION("testProjectionIsExplicitAndCumulative") { 2157 lp.start(ctx); 2158 lp.updateProgram(); 2159 lpAdd(lp, "{a;b}. #project {a}."); 2160 REQUIRE(lp.endProgram()); 2161 2162 REQUIRE(ctx.output.projectMode() == ProjectMode_t::Explicit); 2163 REQUIRE(std::find(ctx.output.proj_begin(), ctx.output.proj_end(), lp.getLiteral(a)) != ctx.output.proj_end()); 2164 REQUIRE(std::find(ctx.output.proj_begin(), ctx.output.proj_end(), lp.getLiteral(b)) == ctx.output.proj_end()); 2165 2166 lp.updateProgram(); 2167 lpAdd(lp, "{c;d}. #project{d}."); 2168 REQUIRE(lp.endProgram()); 2169 2170 REQUIRE(ctx.output.projectMode() == ProjectMode_t::Explicit); 2171 REQUIRE(std::find(ctx.output.proj_begin(), ctx.output.proj_end(), lp.getLiteral(a)) != ctx.output.proj_end()); 2172 REQUIRE(std::find(ctx.output.proj_begin(), ctx.output.proj_end(), lp.getLiteral(b)) == ctx.output.proj_end()); 2173 REQUIRE(std::find(ctx.output.proj_begin(), ctx.output.proj_end(), lp.getLiteral(c)) == ctx.output.proj_end()); 2174 REQUIRE(std::find(ctx.output.proj_begin(), ctx.output.proj_end(), lp.getLiteral(d)) != ctx.output.proj_end()); 2175 } 2176 SECTION("testTheoryAtomsAreFrozenIncremental") { 2177 lp.start(ctx).update(); 2178 lpAdd(lp, "b :- a."); 2179 Potassco::TheoryData& t = lp.theoryData(); 2180 t.addTerm(0, "Theory"); 2181 t.addAtom(a, 0, Potassco::toSpan<Potassco::Id_t>()); 2182 lp.endProgram(); 2183 REQUIRE(lp.getLiteral(a) != lit_false()); 2184 REQUIRE(lp.getLiteral(b) != lit_false()); 2185 std::stringstream str; 2186 AspParser::write(lp, str, AspParser::format_aspif); 2187 for (std::string x; std::getline(str, x);) { 2188 REQUIRE(x.find("5 1") != 0); 2189 } 2190 lp.update(); 2191 lpAdd(lp, 2192 "{c}." 2193 "a :- c."); 2194 lp.endProgram(); 2195 ctx.endInit(); 2196 REQUIRE(ctx.master()->value(lp.getLiteral(a).var()) == value_free); 2197 ctx.addUnary(~lp.getLiteral(c)); 2198 ctx.master()->propagate(); 2199 REQUIRE(ctx.master()->isFalse(lp.getLiteral(a))); 2200 } 2201 SECTION("testFactTheoryAtomsAreNotExternal") { 2202 lp.start(ctx).updateProgram(); 2203 lpAdd(lp, "a."); 2204 Potassco::TheoryData& t = lp.theoryData(); 2205 t.addAtom(a, 0, Potassco::toSpan<Potassco::Id_t>()); 2206 lp.endProgram(); 2207 REQUIRE(lp.getLiteral(a) == lit_true()); 2208 REQUIRE(lp.isDefined(a)); 2209 REQUIRE(lp.isFact(a)); 2210 REQUIRE(!lp.isExternal(a)); 2211 REQUIRE(lp.getRootAtom(a)->supports() == 0); 2212 lp.updateProgram(); 2213 lpAdd(lp, "b."); 2214 t.addAtom(b, 0, Potassco::toSpan<Potassco::Id_t>()); 2215 lp.endProgram(); 2216 REQUIRE(lp.getLiteral(b) == lit_true()); 2217 REQUIRE(lp.isDefined(b)); 2218 REQUIRE(lp.isFact(b)); 2219 REQUIRE(lp.getRootAtom(b)->supports() == 0); 2220 } 2221 SECTION("testTheoryAtomsAreAdded") { 2222 lp.start(ctx).updateProgram(); 2223 lpAdd(lp, "{a;b}."); 2224 Potassco::TheoryData& t = lp.theoryData(); 2225 t.addAtom(c, 0, Potassco::toSpan<Potassco::Id_t>()); 2226 lp.endProgram(); 2227 REQUIRE(lp.getLiteral(c).var() != 0); 2228 REQUIRE(lp.isExternal(c)); 2229 lp.updateProgram(); 2230 lpAdd(lp, "c."); 2231 lp.endProgram(); 2232 REQUIRE(lp.isFact(c)); 2233 REQUIRE(!lp.isExternal(c)); 2234 REQUIRE(ctx.master()->isTrue(lp.getLiteral(c))); 2235 LitVec vec; 2236 lp.getAssumptions(vec); 2237 REQUIRE(vec.empty()); 2238 } 2239 } 2240 2241 TEST_CASE("Sat builder", "[sat]") { 2242 SharedContext ctx; 2243 SatBuilder builder; 2244 builder.startProgram(ctx); 2245 SECTION("testPrepare") { 2246 builder.prepareProblem(10); 2247 builder.endProgram(); 2248 REQUIRE(ctx.numVars() == 10); 2249 } 2250 SECTION("testNoClauses") { 2251 builder.prepareProblem(2); 2252 builder.endProgram(); 2253 REQUIRE(ctx.master()->numFreeVars() == 0); 2254 } 2255 SECTION("testAddClause") { 2256 builder.prepareProblem(2); 2257 LitVec clause; clause.push_back(posLit(1)); clause.push_back(posLit(2)); 2258 builder.addClause(clause); 2259 builder.endProgram(); 2260 REQUIRE(ctx.numConstraints() == 1); 2261 REQUIRE(!ctx.hasMinimize()); 2262 } 2263 SECTION("testAddSoftClause") { 2264 builder.prepareProblem(3); 2265 LitVec clause; 2266 clause.push_back(posLit(1)); 2267 builder.addClause(clause, 1); 2268 clause.clear(); 2269 clause.push_back(negLit(1)); 2270 clause.push_back(posLit(2)); 2271 clause.push_back(negLit(3)); 2272 builder.addClause(clause, 2); 2273 builder.endProgram(); 2274 REQUIRE(ctx.numConstraints() == 1); 2275 REQUIRE(ctx.minimize()->numRules() == 1); 2276 REQUIRE(ctx.numVars() > 3); 2277 } 2278 SECTION("testAddEmptySoftClause") { 2279 builder.prepareProblem(3); 2280 LitVec clause; 2281 clause.push_back(posLit(1)); 2282 // force 1 2283 builder.addClause(clause); 2284 2285 clause.clear(); 2286 clause.push_back(negLit(1)); 2287 builder.addClause(clause, 1); 2288 REQUIRE(builder.endProgram()); 2289 REQUIRE(ctx.minimize()->numRules() == 1); 2290 REQUIRE(ctx.minimize()->adjust(0) == 1); 2291 } 2292 SECTION("testAddConflicting") { 2293 builder.prepareProblem(3); 2294 LitVec clause; 2295 clause.push_back(posLit(1)); 2296 REQUIRE(builder.addClause(clause)); 2297 clause.clear(); 2298 clause.push_back(negLit(1)); 2299 REQUIRE(builder.addClause(clause) == false); 2300 clause.clear(); 2301 clause.push_back(posLit(2)); 2302 clause.push_back(posLit(3)); 2303 REQUIRE(builder.addClause(clause) == false); 2304 REQUIRE(builder.endProgram() == false); 2305 REQUIRE(ctx.ok() == false); 2306 } 2307 } 2308 2309 TEST_CASE("Pb builder", "[pb]") { 2310 SharedContext ctx; 2311 PBBuilder builder; 2312 builder.startProgram(ctx); 2313 SECTION("testPrepare") { 2314 builder.prepareProblem(10, 0, 0); 2315 builder.endProgram(); 2316 REQUIRE(ctx.numVars() == 10); 2317 } 2318 SECTION("testNegativeWeight") { 2319 builder.prepareProblem(5, 0, 0); 2320 WeightLitVec con; 2321 con.push_back(WeightLiteral(posLit(1), 2)); 2322 con.push_back(WeightLiteral(posLit(2), -2)); 2323 con.push_back(WeightLiteral(posLit(3), -1)); 2324 con.push_back(WeightLiteral(posLit(4), 1)); 2325 con.push_back(WeightLiteral(posLit(5), 1)); 2326 builder.addConstraint(con, 2); 2327 builder.endProgram(); 2328 REQUIRE(ctx.numConstraints() == 1); 2329 REQUIRE(ctx.master()->numAssignedVars() == 0); 2330 ctx.master()->assume(negLit(1)) && ctx.master()->propagate(); 2331 REQUIRE(ctx.master()->numFreeVars() == 0); 2332 } 2333 SECTION("testProduct") { 2334 builder.prepareProblem(3, 1, 1); 2335 LitVec p1(3), p2; 2336 p1[0] = posLit(1); 2337 p1[1] = posLit(2); 2338 p1[2] = posLit(3); 2339 p2 = p1; 2340 Literal x = builder.addProduct(p1); 2341 Literal y = builder.addProduct(p2); 2342 REQUIRE((x.var() == 4 && x == y)); 2343 } 2344 SECTION("testProductTrue") { 2345 builder.prepareProblem(3, 1, 1); 2346 LitVec p1(3); 2347 p1[0] = posLit(1); 2348 p1[1] = posLit(2); 2349 p1[2] = posLit(3); 2350 ctx.master()->force(posLit(1), 0); 2351 ctx.master()->force(posLit(2), 0); 2352 ctx.master()->force(posLit(3), 0); 2353 Literal x = builder.addProduct(p1); 2354 REQUIRE(x == lit_true()); 2355 } 2356 SECTION("testProductFalse") { 2357 builder.prepareProblem(3, 1, 1); 2358 LitVec p1(3); 2359 p1[0] = posLit(1); 2360 p1[1] = posLit(2); 2361 p1[2] = posLit(3); 2362 ctx.master()->force(negLit(2), 0); 2363 Literal x = builder.addProduct(p1); 2364 REQUIRE(x == lit_false()); 2365 } 2366 SECTION("testInconsistent") { 2367 builder.prepareProblem(1, 0, 0); 2368 WeightLitVec con; 2369 con.push_back(WeightLiteral(posLit(1), 1)); 2370 REQUIRE(builder.addConstraint(con, 1)); 2371 con.assign(1, WeightLiteral(posLit(1), 1)); 2372 REQUIRE_FALSE(builder.addConstraint(con, 0, true)); 2373 REQUIRE_FALSE(builder.endProgram()); 2374 } 2375 SECTION("testInconsistentW") { 2376 builder.prepareProblem(2, 0, 0); 2377 WeightLitVec con; 2378 con.push_back(WeightLiteral(posLit(1), 1)); 2379 REQUIRE(builder.addConstraint(con, 1)); 2380 con.assign(1, WeightLiteral(posLit(1), 3)); 2381 con.push_back(WeightLiteral(posLit(2), 2)); 2382 REQUIRE_FALSE(builder.addConstraint(con, 2, true)); 2383 REQUIRE_FALSE(builder.endProgram()); 2384 } 2385 SECTION("testCoefficientReductionOnEq") { 2386 builder.prepareProblem(4, 0, 0); 2387 WeightLitVec con; 2388 con.push_back(WeightLiteral(posLit(1), 3)); 2389 con.push_back(WeightLiteral(posLit(2), 2)); 2390 con.push_back(WeightLiteral(posLit(3), 1)); 2391 con.push_back(WeightLiteral(posLit(4), 1)); 2392 REQUIRE(builder.addConstraint(con, 2, true)); 2393 REQUIRE(builder.endProgram()); 2394 REQUIRE(ctx.master()->isFalse(posLit(1))); 2395 } 2396 } 2397 } } 2398