explainunsat output structure not maximally imprecise

[Matthias van der Hallen]

When allowing only three colors in our standard 'graph coloring' example, the subset (France, Belgium, Luxembourg, Germany) isn't colorable anymore. Let's encode this in idp:

http://dtai.cs.kuleuven.be/krr/idp-ide/?src=2b1cfc131685fa4ce862

Now, explainunsat(T,S,V) correctly discards any Border facts containing Holland. However, it retains Border facts containing Austria and Swiss.

structure S_reduced : V {
  Area = { "Austria"; "Belgium"; "France"; "Germany"; "Luxembourg"; "Swiss" }
  Color = { "Blue"; "Red"; "Yellow" }
  Border<ct> = { "Austria","Swiss"; "Belgium","France"; "Belgium","Germany"; "Belgium","Luxembourg"; "Germany","Austria"; "Germany","France"; "Germany","Luxembourg"; "Germany","Swiss"; "Luxembourg","France"; "Swiss","France" }
  Border<cf> = {  }
  Coloring<ct> = {  }
  Coloring<cf> = {  }
}

[Ruben Lapauw]

UnsatExtraction.cpp:

if(assumeStruc){
    assumifyStructure(structure, vAssume, newtheory, emptyStruc, assume.assumeFalse, assume.assumeTrue);
}

ModelExpansion.hpp:

struct MXAssumptions{
    std::vector<DomainAtom> assumeFalse;
    std::vector<Predicate*> assumeAllFalse;
    std::vector<DomainAtom> assumeTrue;
...
    MXAssumptions(const std::vector<DomainAtom>& assumeFalse = std::vector<DomainAtom>()
                , const std::vector<Predicate*>& assumeAllFalse = std::vector<Predicate*>()
                , const std::vector<DomainAtom>& assumeTrue = std::vector<DomainAtom>()
    ): assumeFalse(assumeFalse), assumeAllFalse(assumeAllFalse), assumeTrue(assumeTrue){
}

ModelExpansion.cpp:

for(auto lit: mx->getUnsatExplanation()){
    auto symbol = grounding->translator()->getSymbol(lit.getAtom());
    auto args = grounding->translator()->getArgs(lit.getAtom());
    result.unsat_in_function_of_ct_lits.push_back({symbol, args});
}

MinimizeMarkers.cpp:

auto mxresult = ModelExpansion::doModelExpansion(newtheory, s, NULL, NULL,  markers);
auto core = mxresult.unsat_in_function_of_ct_lits;
...
    auto mxresult = ModelExpansion::doModelExpansion(newtheory, s, NULL, NULL, { core, { } });

Where have the assumeTrue's gone?

[Bart Bogaerts]

Vroeger waren er geen assumetrues; dat is pas van zodra de structuur er bij betrokken is geraakt. Dit is waarschijnlijk oude code die niet mee aangepast is toen.

[Ingmar Dasseville]

solven in PR #384