Tseytin

:-op(450,fy,~). % Negation
:-(system_mode(true),op(502,xfy,’|’),system_mode(false)). % Disjunction
:-op(503,xfy,&). % Conjunction
:-op(504,xfx,=>). % Implication
:-op(505,xfx,<=>). % Equivalence

cnf(F, [(X) | CNF]) :- tseytin(F, X, [CNF]).

% Negation
tseytin(~ F, X, CNF) :- tseytin(F, X1, CNF1),
    CNF0=[(X , X1), (-X , -X1)],
    my_append(CNF0, CNF1, CNF).

% Disjunction
tseytin((F1 | F2), X, CNF) :- write('disjunction'), tseytin(F1, X1, CNF1), tseytin(F2, X2, CNF2),
    CNF0=[(-X , X1 , X2), (X , -X1), (X , -X2)],
    my_append(CNF0, CNF1, CNF2, CNF).

% Conjunction
tseytin((F1 & F2), X, CNF) :- tseytin(F1, X1, CNF1), tseytin(F2, X2, CNF2),
    CNF0=[(-X , X1), (-X , X2), (X , -X1 , -X2)],
    my_append(CNF0, CNF1, CNF2, CNF).

% Implication
tseytin((F1 => F2), X, CNF) :- write('implication \n'), tseytin(F1, X1, CNF1), tseytin(F2, X2, CNF2),
    CNF0=[(-X , -X1 , X2), (X1, X), (-X2, X)],
    my_append(CNF0, CNF1, CNF2, CNF).

% Equivalence
tseytin((F1 <=> F2), X, CNF) :- tseytin(F1, X1, CNF1), tseytin(F2, X2, CNF2),
    CNF0=[(-X , X2), (X , X1), (X1 , -X2)],
    my_append(CNF0, CNF1, CNF2, CNF).

tseytin(A, A, []) :- !.



my_append(A, B, C, [D]) :- append_(A, B, C, T), flatten2(T, D).
my_append(A, B, [D]) :- append_(A, B, T), flatten2(T, D).


append_(A, B, C, [A, B, C]).
append_([A], [B], [A, B]).
append_([],L,L).
append_(L,[],L).

flatten2([], []) :- !.
flatten2([L|Ls], FlatL) :-
    !,
    flatten2(L, NewL),
    flatten2(Ls, NewLs),
    append(NewL, NewLs, FlatL).
flatten2(L, [L]).