diff --git a/src/logic_program.cpp b/src/logic_program.cpp index bf69f67..31d4a25 100644 --- a/src/logic_program.cpp +++ b/src/logic_program.cpp @@ -1248,10 +1248,9 @@ void LogicProgram::finalizeDisjunctions(Preprocessor& p, uint32 numSccs) { uint32 shifted = 0; stats.nonHcfs = uint32(nonHcfs_.size()); Literal bot = lit_false(); - DlpTr tr(this, PrgEdge::Gamma); - RuleTransform shifter(tr); Potassco::LitVec rb; VarVec rh; + DlpTr tr(this, PrgEdge::Gamma); for (uint32 id = 0, maxId = sizeVec(disj); id != maxId; ++id) { PrgDisj* d = disj[id]; Literal dx = d->inUpper() ? d->literal() : bot; @@ -1288,6 +1287,7 @@ void LogicProgram::finalizeDisjunctions(Preprocessor& p, uint32 numSccs) { // create shortcut for supports to avoid duplications during shifting Literal supportLit = dx != bot ? getEqAtomLit(dx, supports, p, sccMap) : dx; // create shifted rules and split disjunctions into non-hcf components + RuleTransform shifter(tr); for (VarVec::iterator hIt = head.begin(), hEnd = head.end(); hIt != hEnd; ++hIt) { uint32 scc = getAtom(*hIt)->scc(); if (scc == PrgNode::noScc || (sccMap[scc] & seen_scc) != 0) { @@ -1324,7 +1324,6 @@ void LogicProgram::finalizeDisjunctions(Preprocessor& p, uint32 numSccs) { nonHcfs_.add(scc); } if (!options().noGamma) { - tr.scc = scc; shifter.transform(sr, Potassco::size(sr.cond) < 4 ? RuleTransform::strategy_no_aux : RuleTransform::strategy_default); } else { diff --git a/tests/facade_test.cpp b/tests/facade_test.cpp index 7ac2e99..d9815c7 100644 --- a/tests/facade_test.cpp +++ b/tests/facade_test.cpp @@ -645,6 +645,35 @@ TEST_CASE("Facade", "[facade]") { } }; +TEST_CASE("Regressions", "[facade][regression]") { + Clasp::ClaspFacade libclasp; + Clasp::ClaspConfig config; + + SECTION("disjunctive shifting") { + config.solve.numModels = 0; + Clasp::Asp::LogicProgram& asp = libclasp.startAsp(config); + lpAdd(asp, + "x52 :- x2.\n" + "x2 :- x19.\n" + "x2 :- x16.\n" + "x6 :- x15.\n" + "x6 :- x14.\n" + "x6 :- x13.\n" + "x6 :- x12.\n" + "x19 :- x54.\n" + "x13 :- x60.\n" + "x12 :- x61.\n" + "x16 :- x52.\n" + "x12 | x13 | x14 | x15 | x16 | x19.\n" + "x54 :- x2.\n" + "x60 :- x6.\n" + "x61 :- x6.\n"); + libclasp.prepare(); + REQUIRE(libclasp.solve().sat()); + REQUIRE(libclasp.summary().numEnum == 2); + } +} + TEST_CASE("Incremental solving", "[facade]") { Clasp::ClaspFacade libclasp; Clasp::ClaspConfig config;