Unsatisfiable cores with complementary literals

[rkaminsk]

For the program

{x}.
a :- x.
b :- not x.

with assumptions a and b, cores are not reported correctly.

The reason seems to be the LogicProgram::extractCore function. It correctly marks literals by sign but unmarks variables (unmarking both the positive and negative sign). As far as I can see the following patch should fix the problem:

diff --git a/src/logic_program.cpp b/src/logic_program.cpp
index 3967c6b..f52d1d0 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()->varInfo(lit.var()).toggle(lit.sign() ? VarInfo::Mark_n : VarInfo::Mark_p);
            --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()->varInfo(lit.var()).toggle(lit.sign() ? VarInfo::Mark_n : VarInfo::Mark_p);
            --marked;
        }
    }

Does that fix the problem? Should there maybe an unmark function for literals?

[BenKaufmann]

Thanks @rkaminsk! I added a SharedContext::unmark(Literal) (varInfo() returns the info by value and therefore can't be used to unset the stored flag).

[rkaminsk]

Thanks @rkaminsk! I added a SharedContext::unmark(Literal) (varInfo() returns the info by value and therefore can't be used to unset the stored flag).

Oops, should have paid more attention. Thanks for fixing this!