From b0b2e0cb02c335605335094d04c38b66427b2e77 Mon Sep 17 00:00:00 2001
From: Benjamin Kaufmann <benjamin.kaufmann@teufel.de>
Date: Fri, 24 Jun 2022 08:12:36 +0200
Subject: [PATCH] Issue #81: Unsatisfiable cores with complementary literals.

* Ensure that LogicProgram::extractCore() only unmarks seen literals
  instead of their variables so that it also correctly handles cores
  containing complementary literals.
---
 clasp/logic_program.h  |  2 +-
 clasp/shared_context.h |  1 +
 src/logic_program.cpp  |  4 ++--
 tests/facade_test.cpp  | 19 +++++++++++++++++++
 4 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/clasp/logic_program.h b/clasp/logic_program.h
index 55696d9..d24550b 100644
--- a/clasp/logic_program.h
+++ b/clasp/logic_program.h
@@ -438,7 +438,7 @@ class LogicProgram : public ProgramBuilder {
 	/*!
 	 * \param solverCore An unsat core found when solving under ProgramBuilder::getAssumptions().
 	 * \param prgLits The given unsat core expressed in terms of program literals.
-	 * \return Whether or not unsatCore was successfully mapped.
+	 * \return Whether unsatCore was successfully mapped.
 	 */
 	bool extractCore(const LitVec& unsatCore, Potassco::LitVec& prgLits) const;
 
diff --git a/clasp/shared_context.h b/clasp/shared_context.h
index b263c53..a52787f 100644
--- a/clasp/shared_context.h
+++ b/clasp/shared_context.h
@@ -796,6 +796,7 @@ class SharedContext {
 	void    setVarEq(Var v, bool b) { set(v, VarInfo::Eq, b); }
 	void    set(Var v, VarInfo::Flag f, bool b) { if (b != varInfo(v).has(f)) varInfo_[v].toggle(f); }
 	void    mark(Literal p)         { assert(validVar(p.var())); varInfo_[p.var()].rep |= (VarInfo::Mark_p + p.sign()); }
+	void    unmark(Literal p)       { assert(validVar(p.var())); varInfo_[p.var()].rep &= ~(VarInfo::Mark_p + p.sign()); }
 	void    unmark(Var v)           { assert(validVar(v)); varInfo_[v].rep &= ~(VarInfo::Mark_p|VarInfo::Mark_n); }
 	//! Eliminates the variable v from the problem.
 	/*!
diff --git a/src/logic_program.cpp b/src/logic_program.cpp
index 3967c6b..6ba946e 100644
--- a/src/logic_program.cpp
+++ b/src/logic_program.cpp
@@ -849,14 +849,14 @@ bool LogicProgram::extractCore(const LitVec& solverCore, Potassco::LitVec& prgLi
 			Literal lit = atom->assumption();
 			if (lit == lit_true() || !ctx()->marked(lit)) continue;
 			prgLits.push_back(atom->literal() == lit ? Potassco::lit(*it) : Potassco::neg(*it));
-			ctx()->unmark(lit.var());
+			ctx()->unmark(lit);
 			--marked;
 		}
 		for (Potassco::LitVec::const_iterator it = assume_.begin(), end = assume_.end(); it != end && marked; ++it) {
 			Literal lit = getLiteral(Potassco::id(*it));
 			if (!ctx()->marked(lit)) continue;
 			prgLits.push_back(*it);
-			ctx()->unmark(lit.var());
+			ctx()->unmark(lit);
 			--marked;
 		}
 	}
diff --git a/tests/facade_test.cpp b/tests/facade_test.cpp
index 5eb0c2e..3c3a1fe 100644
--- a/tests/facade_test.cpp
+++ b/tests/facade_test.cpp
@@ -270,6 +270,25 @@ TEST_CASE("Facade", "[facade]") {
 		CHECK(out[0] == expect);
 	}
 
+	SECTION("testIssue81") {
+		config.solve.numModels = 0;
+		Clasp::Asp::LogicProgram& asp = libclasp.startAsp(config, true);
+		lpAdd(asp, "{x}.\n"
+		           "a :- x.\n"
+		           "b :- not x.\n"
+		           "#assume{a,b}.");
+		libclasp.prepare();
+		REQUIRE(libclasp.solve().unsat());
+		const LitVec* core = libclasp.summary().unsatCore();
+		REQUIRE(core);
+		CHECK(core->size() == 2);
+		Potassco::LitVec out;
+		CHECK(asp.extractCore(*core, out));
+		CHECK(out.size() == 2);
+		CHECK(out[0] == 1);
+		CHECK(out[1] == 2);
+	}
+
 	SECTION("testComputeBrave") {
 		config.solve.numModels = 0;
 		config.solve.enumMode = EnumOptions::enum_brave;