%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% 2diamond.lp
%%
%% (C) Thomas Linsbichler, Jörg Pührer, Hannes Strass, 2015
%%
%% Deciding realisability of sets of three-valued interpretations
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% converts result to readable diamond input
% create a formula from the interpretations (that represent disjuncts)
% first, transform assignments into literals
acTermPart(S, (t(S1),T), T, S1) :- ac(S, (t(S1),T), t).
acTermPart(S, (f(S1),T), T, neg(S1)) :- ac(S, (f(S1),T), 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 the absence of a list represents the empty disjunction "false"
acTerm(S, c(f)) :- s(S), not ac(S, _, t).
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