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("testTheoryHeadEvenIfRuleIsDroppedLater") { 1178 lpAdd(lp.start(ctx), 1179 "{c}.\n" 1180 "b :- c.\n" 1181 ":- c.\n"); 1182 Potassco::TheoryData& t = lp.theoryData(); 1183 t.addTerm(0, "x"); 1184 t.addTerm(1, "c"); 1185 Potassco::Id_t term = 1; 1186 t.addElement(0, Potassco::toSpan(&term, 1), 0); 1187 term = 0; 1188 t.addAtom(b, 0, Potassco::toSpan(&term, 1)); 1189 REQUIRE(t.numAtoms() == 1); 1190 lp.endProgram(); 1191 REQUIRE(lp.getLiteral(a) == lit_false()); 1192 REQUIRE(lp.getLiteral(b) == lit_false()); 1193 REQUIRE(lp.getLiteral(c) == lit_false()); 1194 REQUIRE(t.numAtoms() == 0); 1195 } 1196 1197 SECTION("testTheoryHeadEvenIfRuleIsSkipped") { 1198 lpAdd(lp.start(ctx), 1199 "{a}.\n" 1200 "b :- a, not a.\n"); 1201 Potassco::TheoryData& t = lp.theoryData(); 1202 t.addTerm(0, "ta"); 1203 t.addAtom(b, 0, Potassco::toSpan<Potassco::Id_t>()); 1204 REQUIRE(t.numAtoms() == 1); 1205 lp.endProgram(); 1206 REQUIRE(lp.getLiteral(a) != lit_false()); 1207 REQUIRE(lp.getLiteral(b) == lit_false()); 1208 REQUIRE(t.numAtoms() == 0); 1209 } 1210 1211 SECTION("testFalseBodyTheoryAtomsAreKept") { 1212 lp.start(ctx); 1213 a = lp.newAtom(); 1214 Potassco::TheoryData& t = lp.theoryData(); 1215 t.addTerm(0, "Theory"); 1216 t.addAtom(a, 0, Potassco::toSpan<Potassco::Id_t>()); 1217 lpAdd(lp, ":- a."); 1218 lp.endProgram(); 1219 REQUIRE(lp.getLiteral(a) == lit_false()); 1220 REQUIRE(t.numAtoms() == 1); 1221 std::stringstream str; 1222 AspParser::write(lp, str, AspParser::format_aspif); 1223 REQUIRE(str.str().find("1 0 0 0 1 1") != std::string::npos); 1224 } 1225 SECTION("testOutputFactsNotSupportedInSmodels") { 1226 lp.start(ctx); 1227 lp.addOutput("Hallo", Potassco::toSpan<Potassco::Lit_t>()); 1228 lp.addOutput("World", Potassco::toSpan<Potassco::Lit_t>()); 1229 lp.endProgram(); 1230 REQUIRE_FALSE(lp.supportsSmodels()); 1231 } 1232 SECTION("testDisposeBug") { 1233 lp.start(ctx); 1234 lp.theoryData().addTerm(0, 99); 1235 lp.start(ctx); 1236 REQUIRE_FALSE(lp.theoryData().hasTerm(0)); 1237 } 1238 } 1239 1240 TEST_CASE("Incremental logic program", "[asp]") { 1241 SharedContext ctx; 1242 LogicProgram lp; 1243 Var a = 1, b = 2, c = 3, d = 4, e = 5, f = 6; 1244 SECTION("testSimple") { 1245 lp.start(ctx); 1246 lp.updateProgram(); 1247 lpAdd(lp, "a :- not b. b :- not a."); 1248 REQUIRE((lp.endProgram() && ctx.endInit())); 1249 REQUIRE(ctx.numVars() == 1); 1250 REQUIRE(lp.getLiteral(a) == ~lp.getLiteral(b)); 1251 lp.updateProgram(); 1252 lpAdd(lp, 1253 "c :- a, not d.\n" 1254 "d :- b, not c.\n" 1255 "e :- d.\n"); 1256 REQUIRE((lp.endProgram() && ctx.endInit())); 1257 REQUIRE(ctx.numVars() == 3); 1258 REQUIRE(lp.getLiteral(a) == ~lp.getLiteral(b)); 1259 REQUIRE(lp.getLiteral(e) == lp.getLiteral(d)); 1260 } 1261 SECTION("testDistinctFacts") { 1262 lp.start(ctx); 1263 lp.enableDistinctTrue(); 1264 lp.updateProgram(); 1265 lpAdd(lp, 1266 "a.\n" 1267 "b :- not c.\n" 1268 "c.\n"); 1269 REQUIRE((lp.endProgram() && ctx.endInit())); 1270 REQUIRE(ctx.numVars() == 0); 1271 REQUIRE(lp.getLiteral(a) == lit_true()); 1272 REQUIRE(lp.getLiteral(b) == lit_false()); 1273 REQUIRE(lp.getLiteral(b, MapLit_t::Refined) == lit_false()); 1274 REQUIRE(lp.getLiteral(c) == lit_true()); 1275 lp.updateProgram(); 1276 Var g = f + 1; 1277 lpAdd(lp, 1278 "g :- not f.\n" 1279 "d.\n" 1280 "e :- f.\n" 1281 "f.\n"); 1282 REQUIRE((lp.endProgram() && ctx.endInit())); 1283 REQUIRE(ctx.numVars() == 1); 1284 REQUIRE(lp.getLiteral(d) == lit_true()); 1285 REQUIRE(lp.getLiteral(e) == lit_true()); 1286 REQUIRE(lp.getLiteral(f) == lit_true()); 1287 REQUIRE(lp.getLiteral(g) == lit_false()); 1288 REQUIRE(lp.getLiteral(d, MapLit_t::Refined) == posLit(1)); 1289 REQUIRE(lp.getLiteral(e, MapLit_t::Refined) == posLit(1)); 1290 REQUIRE(lp.getLiteral(f, MapLit_t::Refined) == posLit(1)); 1291 REQUIRE(lp.getLiteral(g, MapLit_t::Refined) == negLit(1)); 1292 } 1293 SECTION("testDistinctFactsSimple") { 1294 lp.start(ctx, LogicProgram::AspOptions().noEq()); 1295 lp.enableDistinctTrue(); 1296 lp.updateProgram(); 1297 lpAdd(lp, "a.\n"); 1298 REQUIRE((lp.endProgram() && ctx.endInit())); 1299 REQUIRE(ctx.numVars() == 0); 1300 REQUIRE(lp.getLiteral(a) == lit_true()); 1301 lp.updateProgram(); 1302 lpAdd(lp, 1303 "b :- d.\n" 1304 "c :- e.\n" 1305 "d. e.\n"); 1306 REQUIRE((lp.endProgram() && ctx.endInit())); 1307 REQUIRE(ctx.numVars() == 1); 1308 REQUIRE(lp.getLiteral(b) == lit_true()); 1309 REQUIRE(lp.getLiteral(c) == lit_true()); 1310 REQUIRE(lp.getLiteral(d) == lit_true()); 1311 REQUIRE(lp.getLiteral(b, MapLit_t::Refined) == posLit(1)); 1312 REQUIRE(lp.getLiteral(c, MapLit_t::Refined) == posLit(1)); 1313 REQUIRE(lp.getLiteral(d, MapLit_t::Refined) == posLit(1)); 1314 lp.updateProgram(); 1315 lpAdd(lp, "f."); 1316 REQUIRE((lp.endProgram() && ctx.endInit())); 1317 REQUIRE(ctx.numVars() == 2); 1318 REQUIRE(lp.getLiteral(a, MapLit_t::Refined) == posLit(0)); 1319 REQUIRE(lp.getLiteral(b, MapLit_t::Refined) == posLit(1)); 1320 REQUIRE(lp.getLiteral(f, MapLit_t::Refined) == posLit(2)); 1321 } 1322 SECTION("testFreeze") { 1323 lp.start(ctx, LogicProgram::AspOptions().noEq()); 1324 lp.updateProgram(); 1325 lpAdd(lp, 1326 "{d}.\n" 1327 "a :- not c.\n" 1328 "b :- a, d.\n" 1329 "#external c."); 1330 REQUIRE((lp.endProgram() && ctx.endInit())); 1331 REQUIRE(lp.getLiteral(c) != lit_false()); 1332 Solver& solver = *ctx.master(); 1333 solver.assume(lp.getLiteral(c)); 1334 solver.propagate(); 1335 REQUIRE(ctx.master()->isFalse(lp.getLiteral(b))); 1336 solver.undoUntil(0); 1337 1338 lp.updateProgram(); 1339 lpAdd(lp, 1340 "{e}.\n" 1341 "c :- e.\n" 1342 "#external c. [release]"); 1343 1344 REQUIRE((lp.endProgram() && ctx.endInit())); 1345 solver.assume(lp.getLiteral(e)); 1346 solver.propagate(); 1347 REQUIRE(ctx.master()->isFalse(lp.getLiteral(b))); 1348 solver.undoUntil(0); 1349 solver.assume(~lp.getLiteral(e)); 1350 solver.propagate(); 1351 REQUIRE(ctx.master()->isFalse(lp.getLiteral(c))); 1352 solver.assume(lp.getLiteral(d)); 1353 solver.propagate(); 1354 REQUIRE(ctx.master()->isTrue(lp.getLiteral(b))); 1355 } 1356 SECTION("testFreezeValue") { 1357 lp.start(ctx, LogicProgram::AspOptions().noEq()); 1358 lp.updateProgram(); 1359 lp.freeze(a).freeze(b, value_true).freeze(c, value_false); 1360 1361 REQUIRE((lp.endProgram() && ctx.endInit())); 1362 LitVec assume; 1363 lp.getAssumptions(assume); 1364 Solver& solver = *ctx.master(); 1365 solver.pushRoot(assume); 1366 REQUIRE(solver.isFalse(lp.getLiteral(a))); 1367 REQUIRE(solver.isTrue(lp.getLiteral(b))); 1368 REQUIRE(solver.isFalse(lp.getLiteral(c))); 1369 solver.popRootLevel(solver.decisionLevel()); 1370 1371 lp.updateProgram(); 1372 lp.unfreeze(a).freeze(c, value_true).freeze(b, value_true).freeze(b, value_false); 1373 REQUIRE((lp.endProgram() && ctx.endInit())); 1374 assume.clear(); 1375 lp.getAssumptions(assume); 1376 REQUIRE((assume.size() == 2 && solver.isFalse(lp.getLiteral(a)))); 1377 solver.pushRoot(assume); 1378 REQUIRE(solver.isFalse(lp.getLiteral(b))); 1379 REQUIRE(solver.isTrue(lp.getLiteral(c))); 1380 } 1381 1382 SECTION("testFreezeOpen") { 1383 lp.start(ctx, LogicProgram::AspOptions().noEq()); 1384 // I1: 1385 // freeze(a, value_free) 1386 lp.updateProgram(); 1387 lp.freeze(a, value_free); 1388 REQUIRE((lp.endProgram() && ctx.endInit())); 1389 LitVec assume; 1390 lp.getAssumptions(assume); 1391 Solver& solver = *ctx.master(); 1392 REQUIRE(assume.empty()); 1393 REQUIRE(solver.value(lp.getLiteral(a).var()) == value_free); 1394 1395 // I2: 1396 lp.updateProgram(); 1397 REQUIRE((lp.endProgram() && ctx.endInit())); 1398 assume.clear(); 1399 lp.getAssumptions(assume); 1400 REQUIRE(assume.empty()); 1401 REQUIRE(solver.value(lp.getLiteral(a).var()) == value_free); 1402 1403 // I3: 1404 lp.updateProgram(); 1405 lp.freeze(a, value_true); 1406 REQUIRE((lp.endProgram() && ctx.endInit())); 1407 assume.clear(); 1408 lp.getAssumptions(assume); 1409 REQUIRE((assume.size() == 1 && assume[0] == lp.getLiteral(a))); 1410 } 1411 SECTION("testKeepFrozen") { 1412 lp.start(ctx); 1413 // I0: 1414 lp.updateProgram(); 1415 lp.freeze(a); 1416 1417 REQUIRE(lp.endProgram()); 1418 PrgAtom* x = lp.getAtom(a); 1419 Literal xLit = x->literal(); 1420 // I1: 1421 lp.updateProgram(); 1422 REQUIRE(lp.endProgram()); 1423 REQUIRE(x->literal() == xLit); 1424 REQUIRE(x->frozen()); 1425 } 1426 SECTION("testFreezeCompute") { 1427 lp.start(ctx); 1428 lp.updateProgram(); 1429 lpAdd(lp, 1430 "#external a. #external b. #external c. #external d.\n" 1431 ":- not a.\n" 1432 ":- not b.\n" 1433 ":- c.\n" 1434 ":- d.\n"); 1435 REQUIRE(lp.endProgram()); 1436 PrgAtom* x = lp.getAtom(a); 1437 PrgAtom* y = lp.getAtom(b); 1438 REQUIRE((x->frozen() && y->frozen())); 1439 REQUIRE(x->literal() != y->literal()); 1440 PrgAtom* z = lp.getAtom(c); 1441 PrgAtom* z2 = lp.getAtom(d); 1442 REQUIRE((z->frozen() && z2->frozen())); 1443 REQUIRE((z->literal() == z2->literal())); 1444 // I1: 1445 lp.updateProgram(); 1446 lpAdd(lp, ":- a."); 1447 REQUIRE_FALSE(lp.endProgram()); 1448 } 1449 SECTION("testUnfreezeUnsupp") { 1450 lp.start(ctx, LogicProgram::AspOptions().noEq()); 1451 lp.updateProgram(); 1452 lpAdd(lp, "a :- not b. #external b."); 1453 REQUIRE(lp.endProgram()); 1454 DefaultUnfoundedCheck* ufsCheck = 0; 1455 if (ctx.sccGraph.get()) { 1456 ctx.master()->addPost(ufsCheck = new DefaultUnfoundedCheck(*ctx.sccGraph)); 1457 } 1458 ctx.endInit(); 1459 lp.updateProgram(); 1460 lpAdd(lp, 1461 "c :- b.\n" 1462 "b :- c.\n" 1463 "#external b. [release]"); 1464 REQUIRE(lp.endProgram()); 1465 if (ctx.sccGraph.get() && !ufsCheck) { 1466 ctx.master()->addPost(ufsCheck = new DefaultUnfoundedCheck(*ctx.sccGraph)); 1467 } 1468 ctx.endInit(); 1469 REQUIRE(ctx.master()->isTrue(lp.getLiteral(a))); 1470 REQUIRE(ctx.master()->isFalse(lp.getLiteral(b))); 1471 REQUIRE(ctx.master()->isFalse(lp.getLiteral(c))); 1472 } 1473 1474 SECTION("testUnfreezeCompute") { 1475 lp.start(ctx); 1476 lp.updateProgram(); 1477 lpAdd(lp, 1478 "{d}.\n" 1479 "a :- b, c.\n" 1480 "b :- d.\n" 1481 "#external c."); 1482 REQUIRE((lp.endProgram() && ctx.endInit())); 1483 REQUIRE(3u == ctx.numConstraints()); 1484 1485 lp.updateProgram(); 1486 lpAdd(lp, 1487 "#external c.[release]\n" 1488 ":- c.\n"); 1489 REQUIRE((lp.endProgram() && ctx.endInit())); 1490 REQUIRE(3u >= ctx.numConstraints()); 1491 REQUIRE(ctx.master()->numFreeVars() == 1); 1492 } 1493 1494 SECTION("testCompute") { 1495 lp.start(ctx, LogicProgram::AspOptions()); 1496 lp.updateProgram(); 1497 Var x2 = 2, x3 = 3, x4 = 4; 1498 lpAdd(lp, 1499 "{x2;x3}.\n" 1500 "x1 :- x2, x3.\n" 1501 " :- x1.\n"); 1502 1503 REQUIRE((lp.endProgram() && ctx.endInit())); 1504 lp.updateProgram(); 1505 lpAdd(lp, "{x4}. :- x2, x4."); 1506 1507 REQUIRE((lp.endProgram() && ctx.endInit())); 1508 ctx.master()->assume(lp.getLiteral(x2)); 1509 ctx.master()->propagate(); 1510 REQUIRE(ctx.master()->isFalse(lp.getLiteral(x3))); 1511 REQUIRE(ctx.master()->isFalse(lp.getLiteral(x4))); 1512 } 1513 SECTION("testComputeBackprop") { 1514 lp.start(ctx, LogicProgram::AspOptions().backpropagate()); 1515 lp.updateProgram(); 1516 lpAdd(lp, 1517 "a :- not b.\n" 1518 "b :- not a.\n" 1519 " :- not a.\n"); 1520 REQUIRE((lp.endProgram() && ctx.endInit())); 1521 // I2: 1522 lp.updateProgram(); 1523 lpAdd(lp, "c :- b. d :- not b."); 1524 REQUIRE((lp.endProgram() && ctx.endInit())); 1525 REQUIRE_FALSE(lp.getAtom(c)->hasVar()); 1526 REQUIRE(lit_true() == lp.getLiteral(d)); 1527 } 1528 1529 SECTION("testBackpropStep") { 1530 lp.start(ctx); 1531 // I1: 1532 lp.updateProgram(); 1533 lpAdd(lp, "{a}."); 1534 REQUIRE((lp.endProgram() && ctx.endInit())); 1535 // I2: 1536 lp.updateProgram(); 1537 lpAdd(lp, "{c}. b :- a, c. :- not b."); 1538 REQUIRE((lp.endProgram() && ctx.endInit())); 1539 REQUIRE(ctx.master()->isTrue(lp.getLiteral(a))); 1540 } 1541 1542 SECTION("testEq") { 1543 lp.start(ctx); 1544 lp.updateProgram(); 1545 lpAdd(lp, 1546 "{c;d}.\n" 1547 "a :- c.\n" 1548 "a :- d.\n" 1549 "b :- a.\n"); 1550 1551 // b == a 1552 REQUIRE((lp.endProgram() && ctx.endInit())); 1553 REQUIRE(lp.isDefined(a)); 1554 REQUIRE_FALSE(lp.isDefined(b)); 1555 1556 std::stringstream exp("1 2 1 0 1"); 1557 REQUIRE(findSmodels(exp, lp)); 1558 lp.updateProgram(); 1559 lpAdd(lp, 1560 "e :- a, b.\n" 1561 "#output e : e.\n"); 1562 REQUIRE((lp.endProgram() && ctx.endInit())); 1563 exp.str("1 5 1 0 1\n5 e"); 1564 REQUIRE(findSmodels(exp, lp)); 1565 } 1566 1567 SECTION("testSimplifyRuleEq") { 1568 lp.start(ctx); 1569 lp.updateProgram(); 1570 lpAdd(lp, 1571 "{x3}.\n" 1572 "x1 :- x3.\n" 1573 "x2 :- x3.\n"); 1574 1575 // x1 == x2 1576 REQUIRE((lp.endProgram() && ctx.endInit())); 1577 uint32 x1 = lp.getAtom(1)->id(); 1578 uint32 x2 = lp.getAtom(2)->id(); 1579 REQUIRE(x1 == x2); 1580 1581 lp.updateProgram(); 1582 1583 lpAdd(lp, 1584 "{x4}.\n" 1585 "x5 :- 2{x1, x2, x4}."); 1586 REQUIRE(lp.endProgram()); 1587 REQUIRE(lp.getAtom(5)->supports() == 1); 1588 PrgBody* body = lp.getBody(lp.getAtom(5)->supps_begin()->node()); 1589 REQUIRE(body->type() == Potassco::Body_t::Sum); 1590 REQUIRE(body->bound() == 2); 1591 REQUIRE(body->size() == 2); 1592 1593 uint32 eqIdx = body->goal(0).var() == 4; 1594 REQUIRE(body->weight(eqIdx) == 2); 1595 REQUIRE(body->weight(1 - eqIdx) == 1); 1596 } 1597 1598 SECTION("testEqUnfreeze") { 1599 lp.start(ctx); 1600 lp.updateProgram(); 1601 lp.freeze(a); 1602 lp.endProgram(); 1603 lp.updateProgram(); 1604 lpAdd(lp, 1605 "{d}.\n" 1606 "a :- c.\n" 1607 "b :- d, not a.\n" 1608 "#external a. [release]"); 1609 1610 lp.endProgram(); 1611 REQUIRE((ctx.numVars() == 2 && ctx.master()->numFreeVars() == 1)); 1612 REQUIRE(lp.getLiteral(b) == lp.getLiteral(d)); 1613 } 1614 1615 SECTION("testEqComplement") { 1616 lp.start(ctx); 1617 lp.updateProgram(); 1618 lpAdd(lp, "a :- not b. b :- not a."); 1619 1620 REQUIRE((lp.endProgram() && ctx.endInit())); 1621 PrgAtom* na = lp.getAtom(a); 1622 PrgAtom* nb = lp.getAtom(b); 1623 REQUIRE(nb->literal() == ~na->literal()); 1624 // I1: 1625 lp.updateProgram(); 1626 lpAdd(lp, "c :- a, b."); 1627 REQUIRE(lp.endProgram()); 1628 PrgAtom* nc = lp.getAtom(c); 1629 REQUIRE(nc->hasVar() == false); 1630 } 1631 1632 SECTION("testEqUpdateAssigned") { 1633 lp.start(ctx); 1634 // I0: 1635 lp.updateProgram(); 1636 lp.freeze(a); 1637 REQUIRE((lp.endProgram() && ctx.endInit())); 1638 1639 // I1: 1640 lp.updateProgram(); 1641 lpAdd(lp, "a :- b. b :- a."); 1642 1643 PrgAtom* x = lp.getAtom(a); 1644 x->setValue(value_weak_true); 1645 lp.endProgram(); 1646 // only weak-true so still relevant in bodies! 1647 REQUIRE(x->deps_begin()->sign() == false); 1648 } 1649 1650 SECTION("testEqResetState") { 1651 lp.start(ctx); 1652 // I0: 1653 lp.updateProgram(); 1654 lpAdd(lp, "{a;b}."); 1655 REQUIRE((lp.endProgram() && ctx.endInit())); 1656 1657 // I1: 1658 lp.updateProgram(); 1659 lpAdd(lp, 1660 "c :- f.\n" 1661 "d :- g.\n" 1662 "c :- d, a.\n" 1663 "d :- c, b.\n" 1664 "f :- e, not h.\n" 1665 "g :- e, not i.\n" 1666 "{e}."); 1667 lp.endProgram(); 1668 REQUIRE(lp.getAtom(c)->scc() == 0); 1669 REQUIRE(lp.getAtom(d)->scc() == 0); 1670 } 1671 1672 SECTION("testUnfreezeUnsuppEq") { 1673 lp.start(ctx, LogicProgram::AspOptions().noScc()); 1674 // I0: 1675 lp.updateProgram(); 1676 lp.freeze(a); 1677 1678 REQUIRE((lp.endProgram() && ctx.endInit())); 1679 // I1: 1680 lp.updateProgram(); 1681 lpAdd(lp, 1682 "a :- b.\n" 1683 "b :- a, c.\n" 1684 "{c}.\n"); 1685 lp.endProgram(); 1686 PrgAtom* x = lp.getAtom(a); 1687 PrgAtom* y = lp.getAtom(b); 1688 REQUIRE(ctx.master()->isFalse(x->literal())); 1689 REQUIRE(ctx.master()->isFalse(y->literal())); 1690 } 1691 1692 SECTION("testUnfreezeEq") { 1693 lp.start(ctx); 1694 // I0: 1695 lp.updateProgram(); 1696 lp.freeze(a); 1697 1698 REQUIRE(lp.endProgram()); 1699 // I1: 1700 lp.updateProgram(); 1701 lpAdd(lp, 1702 "{c}.\n" 1703 "b :- c.\n" 1704 "a :- b.\n"); 1705 PrgAtom* x = lp.getAtom(a); 1706 lp.endProgram(); 1707 // body {b} is eq to body {c} 1708 REQUIRE(ctx.master()->value(x->var()) == value_free); 1709 REQUIRE((x->supports() == 1 && x->supps_begin()->node() == 1)); 1710 } 1711 1712 SECTION("testStats") { 1713 LpStats incStats; 1714 lp.start(ctx, LogicProgram::AspOptions().noEq()); 1715 // I1: 1716 lp.updateProgram(); 1717 lpAdd(lp, 1718 "a :- not b.\n" 1719 "b :- not a.\n" 1720 "#external c.\n"); 1721 REQUIRE((lp.endProgram() && ctx.endInit())); 1722 incStats = lp.stats; 1723 REQUIRE(uint32(3) == incStats.atoms); 1724 REQUIRE(uint32(2) == incStats.bodies[0].sum()); 1725 REQUIRE(uint32(2) == incStats.rules[0].sum()); 1726 REQUIRE(uint32(0) == incStats.ufsNodes); 1727 REQUIRE(uint32(0) == incStats.sccs); 1728 1729 // I2: 1730 lp.updateProgram(); 1731 lpAdd(lp, 1732 "{c, f}.\n" 1733 "d :- not c.\n" 1734 "d :- e, f.\n" 1735 "e :- d, f.\n"); 1736 REQUIRE((lp.endProgram() && ctx.endInit())); 1737 incStats.accu(lp.stats); 1738 REQUIRE(uint32(6) == incStats.atoms); 1739 REQUIRE(uint32(5) == incStats.bodies[0].sum()); 1740 REQUIRE(uint32(6) == incStats.rules[0].sum()); 1741 REQUIRE(uint32(1) == incStats.sccs); 1742 // I3: 1743 lp.updateProgram(); 1744 lpAdd(lp, 1745 "g :- d, not i.\n" 1746 "i :- not g.\n" 1747 "g :- h.\n" 1748 "h :- g, not f.\n"); 1749 REQUIRE((lp.endProgram() && ctx.endInit())); 1750 incStats.accu(lp.stats); 1751 REQUIRE(uint32(9) == incStats.atoms); 1752 REQUIRE(uint32(9) == incStats.bodies[0].sum()); 1753 REQUIRE(uint32(10) == incStats.rules[0].sum()); 1754 REQUIRE(uint32(2) == incStats.sccs); 1755 } 1756 1757 SECTION("testTransform") { 1758 lp.start(ctx, LogicProgram::AspOptions().noEq()); 1759 lp.setExtendedRuleMode(LogicProgram::mode_transform); 1760 // I1: 1761 lp.updateProgram(); 1762 lpAdd(lp, "{a}. % -> a :- not a'. a' :- not a."); 1763 REQUIRE((lp.endProgram() && ctx.endInit())); 1764 REQUIRE(ctx.sccGraph.get() == 0); 1765 // I2: 1766 lp.updateProgram(); 1767 lpAdd(lp, 1768 "% a' must not take up id!\n" 1769 "b :- a.\n" 1770 "b :- c.\n" 1771 "c :- b.\n"); 1772 REQUIRE((lp.endProgram() && ctx.endInit())); 1773 REQUIRE(ctx.sccGraph.get() != 0); 1774 } 1775 1776 SECTION("testBackpropCompute") { 1777 lp.start(ctx); 1778 // I0: 1779 lp.updateProgram(); 1780 lpAdd(lp, 1781 "a :- b.\n" 1782 " :- not a.\n" 1783 "#external b."); 1784 REQUIRE(lp.endProgram()); 1785 REQUIRE(lp.getRootId(a) == 2); 1786 PrgAtom* x = lp.getAtom(b); 1787 REQUIRE(x->value() == value_weak_true); 1788 // I1: 1789 lp.updateProgram(); 1790 lpAdd(lp, "b :- c. c :- b."); 1791 1792 // UNSAT: no support for b,c 1793 REQUIRE_FALSE(lp.endProgram()); 1794 } 1795 1796 SECTION("testBackpropSolver") { 1797 lp.start(ctx); 1798 // I0: 1799 lp.updateProgram(); 1800 lpAdd(lp, 1801 "{a}.\n" 1802 ":- not a.\n" 1803 ":- not b.\n" 1804 "#external b."); 1805 REQUIRE(lp.endProgram()); 1806 PrgAtom* na = lp.getAtom(a); 1807 PrgAtom* nb = lp.getAtom(b); 1808 REQUIRE(na->value() == value_true); 1809 REQUIRE(nb->value() == value_weak_true); 1810 // I1: 1811 lp.updateProgram(); 1812 REQUIRE(lp.endProgram()); 1813 REQUIRE(na->value() == value_true); 1814 REQUIRE(nb->value() == value_weak_true); 1815 } 1816 1817 SECTION("testFreezeUnfreeze") { 1818 lp.start(ctx); 1819 // I0: 1820 lp.updateProgram(); 1821 lpAdd(lp, 1822 "{a}." 1823 "#external b.\n" 1824 "#external b. [release]"); 1825 REQUIRE(lp.endProgram()); 1826 REQUIRE(lit_false() == lp.getLiteral(b)); 1827 // I1: 1828 lp.updateProgram(); 1829 lpAdd(lp, 1830 "#external c.\n" 1831 "c :- b."); 1832 REQUIRE(lp.endProgram()); 1833 REQUIRE(ctx.master()->isFalse(lp.getLiteral(b))); 1834 } 1835 SECTION("testSymbolUpdate") { 1836 lp.start(ctx); 1837 // I0: 1838 lp.updateProgram(); 1839 lpAdd(lp, "{a}."); 1840 lp.addOutput("a", a); 1841 REQUIRE(lp.endProgram()); 1842 uint32 os = ctx.output.size(); 1843 // I1: 1844 lp.updateProgram(); 1845 lpAdd(lp, "{b;c}."); 1846 lp.addOutput("b", b); 1847 1848 REQUIRE(lp.endProgram()); 1849 REQUIRE(!isSentinel(lp.getLiteral(c))); 1850 REQUIRE(os + 1 == ctx.output.size()); 1851 } 1852 SECTION("testFreezeDefined") { 1853 lp.start(ctx); 1854 // I0: 1855 lp.updateProgram(); 1856 lpAdd(lp, "{a}."); 1857 REQUIRE(lp.endProgram()); 1858 // I1: 1859 lp.updateProgram(); 1860 lpAdd(lp, "#external a."); 1861 REQUIRE(lp.endProgram()); 1862 REQUIRE(lp.getAtom(a)->frozen() == false); 1863 } 1864 SECTION("testUnfreezeDefined") { 1865 lp.start(ctx); 1866 // I0: 1867 lp.updateProgram(); 1868 lpAdd(lp, "{a}."); 1869 REQUIRE(lp.endProgram()); 1870 // I1: 1871 lp.updateProgram(); 1872 lpAdd(lp, "#external a. [release]"); 1873 REQUIRE(lp.endProgram()); 1874 REQUIRE(!ctx.master()->isFalse(lp.getLiteral(a))); 1875 } 1876 SECTION("testUnfreezeAsFact") { 1877 lp.start(ctx); 1878 // I0: 1879 lp.updateProgram(); 1880 lpAdd(lp, "#external a."); 1881 REQUIRE(lp.endProgram()); 1882 Literal litA = lp.getLiteral(a); 1883 // I1: 1884 lp.updateProgram(); 1885 lpAdd(lp, "a."); 1886 REQUIRE(true == lp.endProgram()); 1887 REQUIRE(litA == lp.getLiteral(a)); 1888 REQUIRE_FALSE(lp.isExternal(a)); 1889 REQUIRE(true == lp.isDefined(a)); 1890 REQUIRE(ctx.master()->isTrue(litA)); 1891 } 1892 SECTION("testImplicitUnfreeze") { 1893 lp.start(ctx); 1894 // I0: 1895 lp.updateProgram(); 1896 lpAdd(lp, "#external a."); 1897 REQUIRE(lp.endProgram()); 1898 REQUIRE(lp.getAtom(a)->frozen() == true); 1899 REQUIRE(!ctx.master()->isFalse(lp.getLiteral(a))); 1900 // I1: 1901 lp.updateProgram(); 1902 lpAdd(lp, "{a}."); 1903 REQUIRE(lp.endProgram()); 1904 REQUIRE(lp.getAtom(a)->frozen() == false); 1905 } 1906 SECTION("testRedefine") { 1907 lp.start(ctx); 1908 // I0: 1909 lp.updateProgram(); 1910 lpAdd(lp, "{a}."); 1911 REQUIRE(lp.endProgram()); 1912 // I1: 1913 lp.updateProgram(); 1914 REQUIRE_THROWS_AS(lpAdd(lp, "{a}."), RedefinitionError); 1915 } 1916 SECTION("testGetAssumptions") { 1917 lp.start(ctx); 1918 // I0: 1919 lp.updateProgram(); 1920 lpAdd(lp, "#external a. #external b."); 1921 REQUIRE(lp.endProgram()); 1922 LitVec assume; 1923 lp.getAssumptions(assume); 1924 REQUIRE((assume.size() == 2 && assume[0] == ~lp.getLiteral(a) && assume[1] == ~lp.getLiteral(b))); 1925 } 1926 1927 SECTION("testSimplifyCard") { 1928 lp.start(ctx); 1929 // I0: 1930 lp.updateProgram(); 1931 lpAdd(lp, "a."); 1932 REQUIRE(lp.endProgram()); 1933 lp.updateProgram(); 1934 lpAdd(lp, 1935 "b :- 1 {c, a}.\n" 1936 "d :- 1 {c, b}.\n" 1937 "c :- a, b."); 1938 REQUIRE(lp.endProgram()); 1939 } 1940 1941 SECTION("testSimplifyMinimize") { 1942 lp.start(ctx); 1943 // I0: 1944 lp.updateProgram(); 1945 lpAdd(lp, "a. #minimize{a}."); 1946 REQUIRE(lp.endProgram()); 1947 REQUIRE(ctx.minimize()->adjust(0) == 1); 1948 ctx.removeMinimize(); 1949 1950 lp.updateProgram(); 1951 lpAdd(lp, "#minimize{a}."); 1952 REQUIRE(lp.endProgram()); 1953 REQUIRE(ctx.hasMinimize()); 1954 REQUIRE(ctx.minimize()->adjust(0) == 1); 1955 REQUIRE(lp.endProgram()); 1956 } 1957 1958 SECTION("testEqOverNeg") { 1959 lp.start(ctx); 1960 // I0: {a}. 1961 lp.updateProgram(); 1962 lpAdd(lp, "{a}."); 1963 REQUIRE(lp.endProgram()); 1964 // I1: 1965 lp.updateProgram(); 1966 lpAdd(lp, 1967 "b :- not a.\n" 1968 "c :- b.\n" 1969 "c :- f.\n" 1970 "d :- c.\n" 1971 "e :- d.\n" 1972 "g :- c.\n" 1973 "h :- not f, c.\n" 1974 " :- not e.\n" 1975 " :- not h.\n"); 1976 REQUIRE(lp.endProgram()); 1977 REQUIRE((ctx.numVars() == 1 && ctx.master()->isFalse(lp.getLiteral(a)))); 1978 } 1979 SECTION("testKeepExternalValue") { 1980 lp.start(ctx); 1981 // I0: 1982 lp.updateProgram(); 1983 lpAdd(lp, 1984 "b.\n" 1985 "a :- c.\n" 1986 " :- a.\n" 1987 "#external c. [true]"); 1988 1989 REQUIRE((lp.endProgram() && ctx.endInit())); 1990 LitVec assume; 1991 lp.getAssumptions(assume); 1992 REQUIRE_FALSE(ctx.master()->pushRoot(assume)); 1993 1994 REQUIRE(lp.update()); 1995 REQUIRE((lp.endProgram() && ctx.endInit())); 1996 assume.clear(); 1997 lp.getAssumptions(assume); 1998 REQUIRE_FALSE(ctx.master()->pushRoot(assume)); 1999 2000 REQUIRE(lp.update()); 2001 lpAdd(lp, "c."); 2002 REQUIRE_FALSE(lp.endProgram()); 2003 } 2004 2005 SECTION("testWriteMinimize") { 2006 lp.start(ctx); 2007 lp.updateProgram(); 2008 lpAdd(lp, "{a}. #minimize{a}."); 2009 lp.endProgram(); 2010 std::stringstream exp("6 0 1 0 1 1"); 2011 REQUIRE(findSmodels(exp, lp)); 2012 lp.updateProgram(); 2013 lpAdd(lp, "{b}. #minimize{b}."); 2014 2015 lp.endProgram(); 2016 exp.str("6 0 2 0 1 2 1 1"); 2017 REQUIRE(findSmodels(exp, lp)); 2018 lp.updateProgram(); 2019 lpAdd(lp, "{c}."); 2020 lp.endProgram(); 2021 exp.clear(); 2022 exp.seekg(0, ios::beg); 2023 REQUIRE_FALSE(findSmodels(exp, lp)); 2024 } 2025 SECTION("testWriteExternal") { 2026 lp.start(ctx); 2027 lp.updateProgram(); 2028 lpAdd(lp, "#external a."); 2029 lp.endProgram(); 2030 std::stringstream str; 2031 AspParser::write(lp, str, AspParser::format_aspif); 2032 bool foundA = false, foundB = false; 2033 for (std::string x; std::getline(str, x);) { 2034 if (x.find("5 1 2") == 0) { foundA = true; } 2035 if (x.find("5 2 2") == 0) { foundB = true; } 2036 } 2037 REQUIRE((foundA && !foundB)); 2038 lp.updateProgram(); 2039 lpAdd(lp, "#external b."); 2040 lp.endProgram(); 2041 foundA = foundB = false; 2042 str.clear(); 2043 AspParser::write(lp, str, AspParser::format_aspif); 2044 for (std::string x; std::getline(str, x);) { 2045 if (x.find("5 1 2") == 0) { foundA = true; } 2046 if (x.find("5 2 2") == 0) { foundB = true; } 2047 } 2048 REQUIRE((!foundA && foundB)); 2049 } 2050 2051 SECTION("testWriteExternalBug") { 2052 lp.start(ctx); 2053 lp.updateProgram(); 2054 lpAdd(lp, 2055 "#external a." 2056 "#external b." 2057 "#external c." 2058 "#external d." 2059 "b."); 2060 lp.endProgram(); 2061 std::stringstream str; 2062 AspParser::write(lp, str, AspParser::format_aspif); 2063 int foundA = 0, foundB = 0, foundC = 0, foundD = 0; 2064 for (std::string x; std::getline(str, x);) { 2065 if (x.find("5 1 2") == 0) { ++foundA; } 2066 if (x.find("5 2 2") == 0) { ++foundB; } 2067 if (x.find("5 3 2") == 0) { ++foundC; } 2068 if (x.find("5 4 2") == 0) { ++foundD; } 2069 } 2070 REQUIRE(foundA == 1); 2071 REQUIRE(foundB == 0); 2072 REQUIRE(foundC == 1); 2073 REQUIRE(foundD == 1); 2074 } 2075 2076 SECTION("testWriteUnfreeze") { 2077 lp.start(ctx); 2078 lp.updateProgram(); 2079 lpAdd(lp, "#external a."); 2080 lp.endProgram(); 2081 lp.updateProgram(); 2082 lpAdd(lp, "#external a. [release]"); 2083 lp.endProgram(); 2084 REQUIRE(!lp.isExternal(a)); 2085 std::stringstream str; 2086 AspParser::write(lp, str, AspParser::format_aspif); 2087 bool found = false; 2088 for (std::string x; std::getline(str, x);) { 2089 if (x.find("5 1 3") == 0) { found = true; break; } 2090 } 2091 REQUIRE(found); 2092 } 2093 SECTION("testSetInputAtoms") { 2094 lp.start(ctx); 2095 lp.updateProgram(); 2096 lpAdd(lp, "{a;b;c}."); 2097 REQUIRE(lp.numAtoms() == 3); 2098 lp.setMaxInputAtom(lp.numAtoms()); 2099 Var d = lp.newAtom(); 2100 Var e = lp.newAtom(); 2101 REQUIRE((d == 4 && e == 5)); 2102 lp.endProgram(); 2103 REQUIRE((lp.numAtoms() == 5 && lp.startAuxAtom() == 4 && lp.stats.auxAtoms == 2)); 2104 lp.updateProgram(); 2105 INFO("aux atoms are removed on update"); 2106 REQUIRE(lp.numAtoms() == 3); 2107 REQUIRE_FALSE(lp.validAtom(d)); 2108 REQUIRE_FALSE(lp.validAtom(e)); 2109 REQUIRE(d == lp.newAtom()); 2110 } 2111 2112 SECTION("testFreezeIsExternal") { 2113 lp.start(ctx); 2114 lp.updateProgram(); 2115 lpAdd(lp, "{b}. #external a."); 2116 REQUIRE(true == lp.isExternal(a)); 2117 REQUIRE_FALSE(lp.isExternal(b)); 2118 lp.endProgram(); 2119 REQUIRE(true == lp.isExternal(a)); 2120 REQUIRE_FALSE(lp.isExternal(b)); 2121 } 2122 SECTION("testUnfreezeIsNotExternal") { 2123 lp.start(ctx); 2124 lp.updateProgram(); 2125 lpAdd(lp, 2126 "#external a.\n" 2127 "#external b. [release]\n" 2128 "#external a. [release]\n" 2129 "#external b.\n"); 2130 REQUIRE_FALSE(lp.isExternal(a)); 2131 REQUIRE_FALSE(lp.isExternal(b)); 2132 lp.endProgram(); 2133 REQUIRE_FALSE(lp.isExternal(a)); 2134 REQUIRE_FALSE(lp.isExternal(b)); 2135 } 2136 SECTION("testFreezeStaysExternal") { 2137 lp.start(ctx); 2138 lp.updateProgram(); 2139 lpAdd(lp, "#external a."); 2140 REQUIRE(lp.isExternal(a)); 2141 lp.endProgram(); 2142 REQUIRE(lp.isExternal(a)); 2143 lp.updateProgram(); 2144 REQUIRE(lp.isExternal(a)); 2145 lp.endProgram(); 2146 REQUIRE(lp.isExternal(a)); 2147 } 2148 SECTION("testDefinedIsNotExternal") { 2149 lp.start(ctx); 2150 lp.updateProgram(); 2151 lpAdd(lp, "#external a."); 2152 lp.endProgram(); 2153 lp.updateProgram(); 2154 lpAdd(lp, "a :- b."); 2155 REQUIRE_FALSE(lp.isExternal(a)); 2156 lp.endProgram(); 2157 REQUIRE_FALSE(lp.isExternal(a)); 2158 } 2159 SECTION("testFactIsNotExternal") { 2160 lp.start(ctx); 2161 lp.updateProgram(); 2162 lpAdd(lp, "a. #external a."); 2163 lp.endProgram(); 2164 REQUIRE_FALSE(lp.isExternal(a)); 2165 } 2166 2167 SECTION("testAssumptionsAreVolatile") { 2168 lp.start(ctx); 2169 lp.updateProgram(); 2170 lpAdd(lp, "{a}. #assume{a}."); 2171 REQUIRE(lp.endProgram()); 2172 LitVec assume; 2173 lp.getAssumptions(assume); 2174 REQUIRE((assume.size() == 1 && assume[0] == lp.getLiteral(a))); 2175 lp.updateProgram(); 2176 lpAdd(lp, "#assume{not a}."); 2177 REQUIRE(lp.endProgram()); 2178 assume.clear(); 2179 lp.getAssumptions(assume); 2180 REQUIRE((assume.size() == 1 && assume[0] == ~lp.getLiteral(a))); 2181 } 2182 2183 SECTION("testAssumptionsAreFrozen") { 2184 lpAdd(lp.start(ctx), "{a}. #assume{a}."); 2185 REQUIRE(lp.endProgram()); 2186 REQUIRE(lp.getLiteral(a).var() == 1); 2187 REQUIRE(ctx.varInfo(lp.getLiteral(a).var()).frozen()); 2188 } 2189 2190 SECTION("testProjectionIsExplicitAndCumulative") { 2191 lp.start(ctx); 2192 lp.updateProgram(); 2193 lpAdd(lp, "{a;b}. #project {a}."); 2194 REQUIRE(lp.endProgram()); 2195 2196 REQUIRE(ctx.output.projectMode() == ProjectMode_t::Explicit); 2197 REQUIRE(std::find(ctx.output.proj_begin(), ctx.output.proj_end(), lp.getLiteral(a)) != ctx.output.proj_end()); 2198 REQUIRE(std::find(ctx.output.proj_begin(), ctx.output.proj_end(), lp.getLiteral(b)) == ctx.output.proj_end()); 2199 2200 lp.updateProgram(); 2201 lpAdd(lp, "{c;d}. #project{d}."); 2202 REQUIRE(lp.endProgram()); 2203 2204 REQUIRE(ctx.output.projectMode() == ProjectMode_t::Explicit); 2205 REQUIRE(std::find(ctx.output.proj_begin(), ctx.output.proj_end(), lp.getLiteral(a)) != ctx.output.proj_end()); 2206 REQUIRE(std::find(ctx.output.proj_begin(), ctx.output.proj_end(), lp.getLiteral(b)) == ctx.output.proj_end()); 2207 REQUIRE(std::find(ctx.output.proj_begin(), ctx.output.proj_end(), lp.getLiteral(c)) == ctx.output.proj_end()); 2208 REQUIRE(std::find(ctx.output.proj_begin(), ctx.output.proj_end(), lp.getLiteral(d)) != ctx.output.proj_end()); 2209 } 2210 SECTION("testTheoryAtomsAreFrozenIncremental") { 2211 lp.start(ctx).update(); 2212 lpAdd(lp, "b :- a."); 2213 Potassco::TheoryData& t = lp.theoryData(); 2214 t.addTerm(0, "Theory"); 2215 t.addAtom(a, 0, Potassco::toSpan<Potassco::Id_t>()); 2216 lp.endProgram(); 2217 REQUIRE(lp.getLiteral(a) != lit_false()); 2218 REQUIRE(lp.getLiteral(b) != lit_false()); 2219 std::stringstream str; 2220 AspParser::write(lp, str, AspParser::format_aspif); 2221 for (std::string x; std::getline(str, x);) { 2222 REQUIRE(x.find("5 1") != 0); 2223 } 2224 lp.update(); 2225 lpAdd(lp, 2226 "{c}." 2227 "a :- c."); 2228 lp.endProgram(); 2229 ctx.endInit(); 2230 REQUIRE(ctx.master()->value(lp.getLiteral(a).var()) == value_free); 2231 ctx.addUnary(~lp.getLiteral(c)); 2232 ctx.master()->propagate(); 2233 REQUIRE(ctx.master()->isFalse(lp.getLiteral(a))); 2234 } 2235 SECTION("testFactTheoryAtomsAreNotExternal") { 2236 lp.start(ctx).updateProgram(); 2237 lpAdd(lp, "a."); 2238 Potassco::TheoryData& t = lp.theoryData(); 2239 t.addAtom(a, 0, Potassco::toSpan<Potassco::Id_t>()); 2240 lp.endProgram(); 2241 REQUIRE(lp.getLiteral(a) == lit_true()); 2242 REQUIRE(lp.isDefined(a)); 2243 REQUIRE(lp.isFact(a)); 2244 REQUIRE(!lp.isExternal(a)); 2245 REQUIRE(lp.getRootAtom(a)->supports() == 0); 2246 lp.updateProgram(); 2247 lpAdd(lp, "b."); 2248 t.addAtom(b, 0, Potassco::toSpan<Potassco::Id_t>()); 2249 lp.endProgram(); 2250 REQUIRE(lp.getLiteral(b) == lit_true()); 2251 REQUIRE(lp.isDefined(b)); 2252 REQUIRE(lp.isFact(b)); 2253 REQUIRE(lp.getRootAtom(b)->supports() == 0); 2254 } 2255 SECTION("testTheoryAtomsAreAdded") { 2256 lp.start(ctx).updateProgram(); 2257 lpAdd(lp, "{a;b}."); 2258 Potassco::TheoryData& t = lp.theoryData(); 2259 t.addAtom(c, 0, Potassco::toSpan<Potassco::Id_t>()); 2260 lp.endProgram(); 2261 REQUIRE(lp.getLiteral(c).var() != 0); 2262 REQUIRE(lp.isExternal(c)); 2263 lp.updateProgram(); 2264 lpAdd(lp, "c."); 2265 lp.endProgram(); 2266 REQUIRE(lp.isFact(c)); 2267 REQUIRE(!lp.isExternal(c)); 2268 REQUIRE(ctx.master()->isTrue(lp.getLiteral(c))); 2269 LitVec vec; 2270 lp.getAssumptions(vec); 2271 REQUIRE(vec.empty()); 2272 } 2273 } 2274 2275 TEST_CASE("Sat builder", "[sat]") { 2276 SharedContext ctx; 2277 SatBuilder builder; 2278 builder.startProgram(ctx); 2279 SECTION("testPrepare") { 2280 builder.prepareProblem(10); 2281 builder.endProgram(); 2282 REQUIRE(ctx.numVars() == 10); 2283 } 2284 SECTION("testNoClauses") { 2285 builder.prepareProblem(2); 2286 builder.endProgram(); 2287 REQUIRE(ctx.master()->numFreeVars() == 0); 2288 } 2289 SECTION("testAddClause") { 2290 builder.prepareProblem(2); 2291 LitVec clause; clause.push_back(posLit(1)); clause.push_back(posLit(2)); 2292 builder.addClause(clause); 2293 builder.endProgram(); 2294 REQUIRE(ctx.numConstraints() == 1); 2295 REQUIRE(!ctx.hasMinimize()); 2296 } 2297 SECTION("testAddSoftClause") { 2298 builder.prepareProblem(3); 2299 LitVec clause; 2300 clause.push_back(posLit(1)); 2301 builder.addClause(clause, 1); 2302 clause.clear(); 2303 clause.push_back(negLit(1)); 2304 clause.push_back(posLit(2)); 2305 clause.push_back(negLit(3)); 2306 builder.addClause(clause, 2); 2307 builder.endProgram(); 2308 REQUIRE(ctx.numConstraints() == 1); 2309 REQUIRE(ctx.minimize()->numRules() == 1); 2310 REQUIRE(ctx.numVars() > 3); 2311 } 2312 SECTION("testAddEmptySoftClause") { 2313 builder.prepareProblem(3); 2314 LitVec clause; 2315 clause.push_back(posLit(1)); 2316 // force 1 2317 builder.addClause(clause); 2318 2319 clause.clear(); 2320 clause.push_back(negLit(1)); 2321 builder.addClause(clause, 1); 2322 REQUIRE(builder.endProgram()); 2323 REQUIRE(ctx.minimize()->numRules() == 1); 2324 REQUIRE(ctx.minimize()->adjust(0) == 1); 2325 } 2326 SECTION("testAddConflicting") { 2327 builder.prepareProblem(3); 2328 LitVec clause; 2329 clause.push_back(posLit(1)); 2330 REQUIRE(builder.addClause(clause)); 2331 clause.clear(); 2332 clause.push_back(negLit(1)); 2333 REQUIRE(builder.addClause(clause) == false); 2334 clause.clear(); 2335 clause.push_back(posLit(2)); 2336 clause.push_back(posLit(3)); 2337 REQUIRE(builder.addClause(clause) == false); 2338 REQUIRE(builder.endProgram() == false); 2339 REQUIRE(ctx.ok() == false); 2340 } 2341 } 2342 2343 TEST_CASE("Pb builder", "[pb]") { 2344 SharedContext ctx; 2345 PBBuilder builder; 2346 builder.startProgram(ctx); 2347 SECTION("testPrepare") { 2348 builder.prepareProblem(10, 0, 0); 2349 builder.endProgram(); 2350 REQUIRE(ctx.numVars() == 10); 2351 } 2352 SECTION("testNegativeWeight") { 2353 builder.prepareProblem(5, 0, 0); 2354 WeightLitVec con; 2355 con.push_back(WeightLiteral(posLit(1), 2)); 2356 con.push_back(WeightLiteral(posLit(2), -2)); 2357 con.push_back(WeightLiteral(posLit(3), -1)); 2358 con.push_back(WeightLiteral(posLit(4), 1)); 2359 con.push_back(WeightLiteral(posLit(5), 1)); 2360 builder.addConstraint(con, 2); 2361 builder.endProgram(); 2362 REQUIRE(ctx.numConstraints() == 1); 2363 REQUIRE(ctx.master()->numAssignedVars() == 0); 2364 ctx.master()->assume(negLit(1)) && ctx.master()->propagate(); 2365 REQUIRE(ctx.master()->numFreeVars() == 0); 2366 } 2367 SECTION("testProduct") { 2368 builder.prepareProblem(3, 1, 1); 2369 LitVec p1(3), p2; 2370 p1[0] = posLit(1); 2371 p1[1] = posLit(2); 2372 p1[2] = posLit(3); 2373 p2 = p1; 2374 Literal x = builder.addProduct(p1); 2375 Literal y = builder.addProduct(p2); 2376 REQUIRE((x.var() == 4 && x == y)); 2377 } 2378 SECTION("testProductTrue") { 2379 builder.prepareProblem(3, 1, 1); 2380 LitVec p1(3); 2381 p1[0] = posLit(1); 2382 p1[1] = posLit(2); 2383 p1[2] = posLit(3); 2384 ctx.master()->force(posLit(1), 0); 2385 ctx.master()->force(posLit(2), 0); 2386 ctx.master()->force(posLit(3), 0); 2387 Literal x = builder.addProduct(p1); 2388 REQUIRE(x == lit_true()); 2389 } 2390 SECTION("testProductFalse") { 2391 builder.prepareProblem(3, 1, 1); 2392 LitVec p1(3); 2393 p1[0] = posLit(1); 2394 p1[1] = posLit(2); 2395 p1[2] = posLit(3); 2396 ctx.master()->force(negLit(2), 0); 2397 Literal x = builder.addProduct(p1); 2398 REQUIRE(x == lit_false()); 2399 } 2400 SECTION("testInconsistent") { 2401 builder.prepareProblem(1, 0, 0); 2402 WeightLitVec con; 2403 con.push_back(WeightLiteral(posLit(1), 1)); 2404 REQUIRE(builder.addConstraint(con, 1)); 2405 con.assign(1, WeightLiteral(posLit(1), 1)); 2406 REQUIRE_FALSE(builder.addConstraint(con, 0, true)); 2407 REQUIRE_FALSE(builder.endProgram()); 2408 } 2409 SECTION("testInconsistentW") { 2410 builder.prepareProblem(2, 0, 0); 2411 WeightLitVec con; 2412 con.push_back(WeightLiteral(posLit(1), 1)); 2413 REQUIRE(builder.addConstraint(con, 1)); 2414 con.assign(1, WeightLiteral(posLit(1), 3)); 2415 con.push_back(WeightLiteral(posLit(2), 2)); 2416 REQUIRE_FALSE(builder.addConstraint(con, 2, true)); 2417 REQUIRE_FALSE(builder.endProgram()); 2418 } 2419 SECTION("testCoefficientReductionOnEq") { 2420 builder.prepareProblem(4, 0, 0); 2421 WeightLitVec con; 2422 con.push_back(WeightLiteral(posLit(1), 3)); 2423 con.push_back(WeightLiteral(posLit(2), 2)); 2424 con.push_back(WeightLiteral(posLit(3), 1)); 2425 con.push_back(WeightLiteral(posLit(4), 1)); 2426 REQUIRE(builder.addConstraint(con, 2, true)); 2427 REQUIRE(builder.endProgram()); 2428 REQUIRE(ctx.master()->isFalse(posLit(1))); 2429 } 2430 } 2431 } } 2432