diff --git a/src/solve_algorithms.cpp b/src/solve_algorithms.cpp index cd48e5d..a12c509 100644 --- a/src/solve_algorithms.cpp +++ b/src/solve_algorithms.cpp @@ -288,7 +288,7 @@ void SolveAlgorithm::detach() { s->popRootLevel(s->rootLevel()); core_ = new LitVec(); for (LitVec::const_iterator it = path_->begin(); it != path_->end(); ++it) { - if (isSentinel(*it) || s->isTrue(*it) || *it == ctx_->stepLiteral() || !ctx_->varInfo(it->var()).input()) + if (s->isTrue(*it) || *it == ctx_->stepLiteral()) continue; core_->push_back(*it); if (!s->pushRoot(*it)) { diff --git a/tests/facade_test.cpp b/tests/facade_test.cpp index 5b44897..d0ab78d 100644 --- a/tests/facade_test.cpp +++ b/tests/facade_test.cpp @@ -215,6 +215,33 @@ TEST_CASE("Facade", "[facade]") { libclasp.prepare(); REQUIRE(libclasp.solve().unsat()); } + + SECTION("testUnsatCore") { + config.solve.numModels = 0; + Clasp::Asp::LogicProgram& asp = libclasp.startAsp(config, true); + int expect = 0; + std::string prg; + SECTION("AssumeFalse") { + prg = "a.\n#assume{not a}."; + expect = -1; + } + SECTION("AssumeTrue") { + prg = "a :- b.\nb :- a.\n#assume{a}."; + expect = 1; + } + INFO(prg); + lpAdd(asp, prg.c_str()); + libclasp.prepare(); + REQUIRE(libclasp.solve().unsat()); + const LitVec* core = libclasp.summary().unsatCore(); + REQUIRE(core); + CHECK(core->size() == 1); + Potassco::LitVec out; + CHECK(asp.extractCore(*core, out)); + CHECK(out.size() == 1); + CHECK(out[0] == expect); + } + SECTION("testComputeBrave") { config.solve.numModels = 0; config.solve.enumMode = EnumOptions::enum_brave;