%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% show.lp
%%
%% (C) Thomas Linsbichler, Jörg Pührer, Hannes Strass, 2015
%%
%% Deciding realisability of sets of three-valued interpretations
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% converts result to readable output
% the ternary member predicate can access members of lists and also identfies the rest of the list
member(T, (T, I), I) :- int((T, I)).
member(T, (X, I), (X, R)) :- int((X, I)), member(T, I, R), X != T.
% every disjunct of the expanded DNF is a candidate clause
candidate(S, I) :- ac(S, I, t).
% every resolvent of two candidate clauses is a candidate clause
candidate(S, R) :-
candidate(S, C1),
candidate(S, C2),
member(t(P), C1, R),
member(f(P), C2, R).
% we are interested in the smallest possible clauses
iMinimalCandidate(S, I) :-
candidate(S, I),
not existsSmallerCandidate(S, I).
existsSmallerCandidate(S, I) :-
candidate(S, I),
candidate(S, J),
ileq(J, I),
nileq(I, J).
% create a formula from the identified minimal disjuncts
% first, transform assignments into literals
acTermPart(S, (t(S1),T), T, S1) :- iMinimalCandidate(S, (t(S1),T)).
acTermPart(S, (f(S1),T), T, neg(S1)) :- iMinimalCandidate(S, (f(S1),T)).
% next, collect literals into conjunctions
acTermPart(S,I,T, and(F, S1)) :- acTermPart(S,I,(t(S1),T),F).
acTermPart(S,I,T, and(F, neg(S1))) :- acTermPart(S,I,(f(S1),T),F).
% note that a single disjunct is to be interpreted as a conjunction
% therefore, the empty list represents "true"
% whereas the absence of a list represents the empty disjunction "false"
acTerm(S, c(v)) :- iMinimalCandidate(S, nil).
acTerm(S, c(f)) :- s(S), not iMinimalCandidate(S, _).
acTerm(S, F) :- acTermPart(S,I,nil,F).
% establish an ordering on relevant disjuncts
acTermSuccessor(S,F1,F2) :- acTerm(S,F1), acTerm(S,F2), F1