%--------------------------------------------%
% Author: Elvis Samson / www.elvissamson.de  %
% E-Mail: elvis.samson@math.uni-giessen.de   %
% Date of last modification: 07 may-2003     %
% Version number: 083                        %
% Topic: Prolog analyzer of SQL clauses      %
%--------------------------------------------%

%-----------------------------------------------------------------%
% Run Example:                                                    %
% ?- consult('Prototyp.pl').                                      %
% ?- run.                                                         %
% |: select ...               ;                                   %
%-----------------------------------------------------------------%

%------------------------------------------------------------------------------
% scanner(-X)
%------------------------------------------------------------------------------

scanner(X) :- get_code(C), scan_newtoken(C,X), !. % analyze&transform into list
scanner(_) :- writeln('Scanner found failure in input. Stopped!'),
              abort.

%------------------------------------------------------------------------------
% scan_newtoken(+CurrChar, -TokenList)
%------------------------------------------------------------------------------

scan_newtoken(CurrChar,TokenList) :-     % skip Whitespace
        whitespace(CurrChar),
        get_code(NextChar),
        scan_newtoken(NextChar,TokenList).

scan_newtoken(L,[Token|Rest]) :-         % accept a letter (a-z)
        letter(L),
        scan_id(L,IdCharList,NextChar),  % scan follow.chars, put in IdCharList
        name(Word, IdCharList),          % put IdCharList into Word as a string
        classify(Word,Token),            % check if Word is reserverd sql-word
        scan_newtoken(NextChar,Rest).    % put nextchar from rest into NextChar

scan_newtoken(L,[Token|Rest]) :-         % accept operators e.g. =, <=, >=
        operator_char(L),
        scan_operator(L,IdCharList,NextChar),
        name(Word, IdCharList),
        classify_operator(Word,Token),
        scan_newtoken(NextChar,Rest).

scan_newtoken(CurrChar,[Token|Rest]) :-  % accept paranthesis
        paranthesisid(CurrChar),
        name(Word, [CurrChar]),
        classify_paranthesis(Word,Token),
        get_code(NextChar),              % unify NextChar with bext charcode
        scan_newtoken(NextChar,Rest).

scan_newtoken(CurrChar, [point|MoreTokens]) :-     % accept point
        point(CurrChar),
        get_code(NextChar),
        scan_newtoken(NextChar, MoreTokens).

scan_newtoken(CurrChar, [comma|MoreTokens]) :-     % accept comma
        comma(CurrChar),
        get_code(NextChar),
        scan_newtoken(NextChar, MoreTokens).

scan_newtoken(CurrChar, [Token|Rest]) :-           % accept *
        star(CurrChar),
        name(Word, [CurrChar]),
        classify(Word,Token),                      % make id(*)
        get_code(NextChar),
        scan_newtoken(NextChar, Rest).

scan_newtoken(L,[Token|Rest]) :-                   % accept digit numbers
        digit(L),
        scan_digit(L,IdCharList,NextChar),
        name(Word, IdCharList),
        classify_digit(Word,Token),
        scan_newtoken(NextChar,Rest).

scan_newtoken(L,[Token|Rest]) :-                   % accept string constants
        dq(L),                                     % which are inside " "
        get_code(C),
        scan_stringconst(C,IdCharList,_),
        name(Word, IdCharList),
        classify_const(Word,Token),
        get_code(NC),
        scan_newtoken(NC,Rest).

scan_newtoken(C,[]) :-   % accept a semicolon as the end of the sqlquery
        semicolon(C).    % check if C is a semicolon, return [].

%------------------------------------------------------------------------------
% classify(+X, -ClassifiedX)
%------------------------------------------------------------------------------

classify(X,X) :- reserved_word(X), !. % return reserved word X if it is one
classify(X,id(X)).                    % otherwise return id(X)

%------------------------------------------------------------------------------
% classify_const(+X,-strconst(X))
%------------------------------------------------------------------------------

classify_const(X,strconst(X)).

%------------------------------------------------------------------------------
% classify_operator(+x,-operator(..))
%------------------------------------------------------------------------------

classify_operator(X,operator(eq)) :- operator_eq(X).
classify_operator(X,operator(ne)) :- operator_ne(X).
classify_operator(X,operator(lt)) :- operator_lt(X).
classify_operator(X,operator(le)) :- operator_le(X).
classify_operator(X,operator(gt)) :- operator_gt(X).
classify_operator(X,operator(ge)) :- operator_ge(X).

classify_operator(X,operator(+)) :- operator_pl(X).
classify_operator(X,operator(-)) :- operator_mi(X).
classify_operator(X,operator(*)) :- operator_mu(X).
classify_operator(X,operator(/)) :- operator_di(X).

%------------------------------------------------------------------------------
% classify_digit(+X,-digit(X))
%------------------------------------------------------------------------------

classify_digit(X,digit(X)).                    % return digit(X)

%------------------------------------------------------------------------------
% classify_paranthesis(+X,-X)
%------------------------------------------------------------------------------

classify_paranthesis(X,X):- name(X,[40]), !.   % return (
classify_paranthesis(X,X):- name(X,[41]), !.   % return )

%------------------------------------------------------------------------------
% scan_id(+CurrChar, -IdCharList, -NextChar)
%------------------------------------------------------------------------------
% return as second argument a list incl. L with all id_chars after L

scan_id(L,[L|R],N) :-
        id_char(L),       % current L is a letter, digit or underscore
        !,                % cut
        get_code(C),      % unify c with the char code of next character
        scan_id(C,R,N).   % recursive until RestList R is [].
                          % On returnpath, [L|R] is filled up with Ls

scan_id(N,[],N).              % endpoint of recursion

%------------------------------------------------------------------------------
% scan_stringconst(+CurrChar, -IdCharList, -NextChar)
%------------------------------------------------------------------------------

scan_stringconst(L,[L|R],N) :-
        id_charc(L),      % current L is a letter, digit, underscore, . or 32
        !,                % cut
        get_code(C),      % unify c with the char code of next character
        scan_stringconst(C,R,N).   % recursive until RestList R is [].
                          % On returnpath, [L|R] is filled up with Ls

scan_stringconst(N,[],N). % :- N = 0'".              % endpoint of recursion

%------------------------------------------------------------------------------
% scan_operator(+CurrChar, -IdCharList, -NextChar)
%------------------------------------------------------------------------------

scan_operator(L,[L|R],N) :-
        operator_char(L),      % that satisfy this: current L is a operator
        !,                     % cut
        get_code(C),           % unify c with the char code of next character
        scan_operator(C,R,N).  % recursive until RestList R is []

scan_operator(N,[],N).         % endpoint of recursion

%------------------------------------------------------------------------------
% scan_paranthesis(+CurrChar, -IdCharList, -NextChar)
%------------------------------------------------------------------------------

scan_paranthesis(L,[L|R],N) :-
        paranthesis_char(L),
        !,
        get_code(C),
        scan_paranthesis(C,R,N).     % recursive until RestList R is []

scan_paranthesis(N,[],N).            % endpoint of recursion


%------------------------------------------------------------------------------
% scan_digit(+CurrChar, -IdCharList, -NextChar)
%------------------------------------------------------------------------------
% return as second argument a list incl. L with all id_digit_chars after L

scan_digit(L,[L|R],N) :-
        digit_char(L),     % L is a digit or point
        !,                 % cut: don't look for alter. id_char on backtracking
        get_code(C),       % unify c with the char code of the next character
        scan_digit(C,R,N). % recursive until RestList R is []

scan_digit(N,[],N).        % endpoint of recursion

%------------------------------------------------------------------------------

operator_char(C) :- C=0'=.
operator_char(C) :- C=0'<.
operator_char(C) :- C=0'>.

operator_char(C) :- C=0'+.
operator_char(C) :- C=0'-.
operator_char(C) :- C=0'*.
operator_char(C) :- C=0'/.

%------------------------------------------------------------------------------

operator_eq('=').
operator_ne('<>').
operator_lt('<').
operator_le('<=').
operator_gt('>').
operator_ge('>=').
operator_pl('+').
operator_mi('-').
operator_mu('*').
operator_di('/').

%------------------------------------------------------------------------------

paranthesis_char(C) :- C=0'(.
paranthesis_char(C) :- C=0').

%------------------------------------------------------------------------------

id_char(C) :- letter(C).
id_char(C) :- digit(C).
id_char(C) :- underscore(C).

%------------------------------------------------------------------------------

id_charc(C) :- letter(C).
id_charc(C) :- digit(C).
id_charc(C) :- underscore(C).
id_charc(C) :- point(C).
id_charc(32).

%------------------------------------------------------------------------------

digit_char(C) :- digit(C).
digit_char(C) :- point(C).

%------------------------------------------------------------------------------

whitespace(32).  % space
point(0'.).
semicolon(0';).
comma(0',).
star(42).        % * star
letter(X) :- X >= 0'a, X =< 0'z.
letter(X) :- X >= 0'A, X =< 0'Z.
digit(C) :- C >=48, C=<57.
dq(X) :- X=0'".
underscore(0'_).
paranthesisid(0'().
paranthesisid(0')).

%------------------------------------------------------------------------------

reserved_word(select).
reserved_word(from).
reserved_word(where).
reserved_word(as).
reserved_word(and).
reserved_word(or).
reserved_word(not).
reserved_word(order).
reserved_word(by).
reserved_word(exists).

%------------------------------------------------------------------------------
% Definition of grammar which accepts SQL subset
%------------------------------------------------------------------------------

query([S,F,[],[]]) --> [select], selectlist(S), [from], fromlist(F).
query([S,F,C,[]]) --> [select], selectlist(S), [from],
                      fromlist(F), [where], condition(C).
query([S,F,[],O]) --> [select], selectlist(S), [from],
                      fromlist(F), [order], [by], orderbylist(O).
query([S,F,C,O]) --> [select], selectlist(S), [from],
                     fromlist(F), [where], condition(C),
                     [order], [by], orderbylist(O).

selectlist([X]) --> sel_part(X).
selectlist([X|Rest]) --> sel_part(X), [comma], selectlist(Rest).

sel_part(column(T,C,N)) --> [id(T)], [point], [id(C)], [as], [id(N)].
sel_part(column(T,C,c(N))) --> [id(T)], [point], [id(C)], [as], [strconst(N)].
sel_part(column(T,C,N)) --> [id(T)], [point], [id(C)], [id(N)].
sel_part(column(T,C,c(N))) --> [id(T)], [point], [id(C)], [strconst(N)].
sel_part(column(T,C,[])) --> [id(T)], [point], [id(C)].
sel_part(column([],C,N)) --> [id(C)], [as], [id(N)].
sel_part(column([],C,c(N))) --> [id(C)], [as], [strconst(N)].
sel_part(column([],C,N)) --> [id(C)], [id(N)].
sel_part(column([],C,c(N))) --> [id(C)], [strconst(N)].
sel_part(column([],C,[])) --> [id(C)].
sel_part(column([],*,[])) --> [operator(*)].

fromlist([X]) --> tvar_decl(X).
fromlist([X|Rest]) --> tvar_decl(X), [comma], fromlist(Rest).

tvar_decl(tvar(X,X)) --> [id(X)].
tvar_decl(tvar(R,X)) --> [id(R)], [as], [id(X)].
tvar_decl(tvar(R,X)) --> [id(R)], [id(X)].

condition(or(X,Y)) --> condition_and(X), [or], condition(Y).
condition(X) --> condition_and(X).

condition_and(and(X,Y)) --> condition_not(X), [and], condition_and(Y).
condition_and(X) --> condition_not(X).
condition_not(not(X)) --> [not], comparison(X).
condition_not(X) --> comparison(X).
comparison(cond(S,X,T)) --> term(X), [operator(S)], term(T).
comparison(exists(X)) --> [exists], ['('], query(X), [')'].
comparison((X)) --> ['('], condition(X), [')'].

term(X) --> [id(X)].
term(dig(X)) --> [digit(X)].
term(str(X)) --> [strconst(X)].
term([T,C]) --> [id(T)], [point], [id(C)].

orderbylist([[X,Y]]) --> [id(X)], [point], [id(Y)].
orderbylist([X]) --> [id(X)].
orderbylist([digit(X)]) --> [digit(X)].
orderbylist([[X,Y]|S]) --> [id(X)], [point], [id(Y)], [comma], orderbylist(S).
orderbylist([X|S]) --> [id(X)], [comma], orderbylist(S).
orderbylist([digit(X)|S]) --> [digit(X)], [comma], orderbylist(S).

%------------------------------------------------------------------------------
% dcgcheck([+Select,+From,+Cond,+Order], [-NewSelect,-From,-NewCond,-NewOrder])
%------------------------------------------------------------------------------

dcgcheck([S,F,C,O],[NewS,F,NewC,NewO]) :-
                       dcgtablecheck(F),           % check the from-part first
                       !,
                       dcgselectcheck(S,F,NewS),   % check & fill select-part
                       !,
                       dcgconditioncheck(C,F,NewC),
                       !,
                       dcgorderbycheck(O,F,NewO).

%------------------------------------------------------------------------------
% dcgtablecheck(+Fromlist)
%------------------------------------------------------------------------------

dcgtablecheck([F|[]]) :- !,
                         dcgtablecheckeach(F).
dcgtablecheck([F|Rest]) :- dcgtablecheckeach(F),
                           dcgtablecheck(Rest).

%------------------------------------------------------------------------------
% dcgtablecheckeach(+tvar(T1,T2))
%------------------------------------------------------------------------------

dcgtablecheckeach(tvar(Ta,Ta)) :- table(Ta,_,_,_,_).
dcgtablecheckeach(tvar(Ta,Tu)) :- table(Ta,_,_,_,_),
                                  not(table(Tu,_,_,_,_)).
dcgtablecheckeach(tvar(Ta,_)) :- write('Error in From-Part found at table '),
                                 write(Ta),
                                 nl,
                                 abort.

%------------------------------------------------------------------------------
% dcgselectcheck(+Selectlist,+Fromlist,-NewSelectlist)
%------------------------------------------------------------------------------
% adds tupel. or table. for every column in selectclause

dcgselectcheck([S|[]],F,[NewS|[]]) :- !,
                                      dcgselectcheckeach(S,F,NewS).
dcgselectcheck([S|Rest],F,[NewS1|NewS2]) :- dcgselectcheckeach(S,F,NewS1),
                                            dcgselectcheck(Rest,F,NewS2).

%------------------------------------------------------------------------------
% dcgselectcheckeach(+Col,+From,-ColFull)
%------------------------------------------------------------------------------

dcgselectcheckeach(column([],C,N),F,column(NT,C,N)):- table(T,C,_,_,_),
                                                      tableInF(T,C,F,NT).
dcgselectcheckeach(column(T,C,N),F,column(NT,C,N)) :- tableInF(T,C,F,NT).
dcgselectcheckeach(column(_,*,_),_,column([],*,[])).
dcgselectcheckeach(column(_,C,_),_,[]) :-
   write('Error in Select-Part found, check columnname '),
   write(C),
   nl,
   abort.

%------------------------------------------------------------------------------
% dcgconditioncheck(-Condition,-FromList,+NewC)
%------------------------------------------------------------------------------

dcgconditioncheck([],_,[]).
dcgconditioncheck(and(F,G),FL,and(Z1,Z2)) :- dcgconditioncheck(F,FL,Z1),
                                             dcgconditioncheck(G,FL,Z2).
dcgconditioncheck(or(F,G),FL,or(Z1,Z2)) :- dcgconditioncheck(F,FL,Z1),
                                           dcgconditioncheck(G,FL,Z2).
dcgconditioncheck(not(A),FL,not(B)) :- dcgconditioncheck(A,FL,B).
dcgconditioncheck(exists([S1,F1,W1,O1]),FL,exists([S2,F1,W2,O2])) :-
       append(F1,FL,F2),
       dcgcheck([S1,F2,W1,O1],[S2,_,W2,O2]).
dcgconditioncheck(cond(C,L,R),FL,cond(C,LN,RN)) :- dcgcondcheck(L,FL,LN),
                                                   dcgcondcheck(R,FL,RN).

%------------------------------------------------------------------------------
% tableInF(+T,+C,+F,-NT)
%------------------------------------------------------------------------------
tableInF([],C,[tvar(T,_)|_],T) :- table(T,C,_,_,_).  % if table.column
tableInF([],C,[_|Rest],NT) :- tableInF([],C,Rest,NT).

tableInF(T,C,[tvar(T,NT)|_],NT) :- table(T,C,_,_,_).  % if table.column
tableInF(T,C,[tvar(OT,T)|_],T) :- table(OT,C,_,_,_). % if tupel.column
tableInF(T,C,[_|Rest],NT) :- tableInF(T,C,Rest,NT).

%------------------------------------------------------------------------------
% dcgcondcheck(+Element,+From,-NewElement)
%------------------------------------------------------------------------------

dcgcondcheck(dig(X),_,dig(X)) :- !.
dcgcondcheck(str(X),_,str(X)) :- !.
dcgcondcheck([T,C],F,[NT,C]) :- tableInF(T,C,F,NT).
dcgcondcheck(C,F,[NT,C]) :- tableInF([],C,F,NT).
% First Tables in From are local ones, take them first for column
% reference without table reference in th query
dcgcondcheck(A,F,_) :- write('Error, attribute '),
                       write(A),
                       write(' not in FROM-table '),
                       write(F),
                       nl,
                       abort.

%------------------------------------------------------------------------------
% dcgorderbycheck(-Orderby,-FromList,+NewO)
%------------------------------------------------------------------------------

dcgorderbycheck([],_,[]).
dcgorderbycheck([O|[]],F,[NO|[]]) :- dcgordercheck(O,F,NO).
dcgorderbycheck([O|Rest],F,[NO1|NO2]) :- dcgordercheck(O,F,NO1),
                                         dcgorderbycheck(Rest,F,NO2).
%------------------------------------------------------------------------------
% dcgodercheck(+Element,+From,-NewElement)
%------------------------------------------------------------------------------

dcgordercheck(digit(X),_,digit(X)).
dcgordercheck([T,O],F,[NT,O]) :- tableInF(T,O,F,NT).
dcgordercheck(O,F,[NT,O]) :- table(T,O,_,_,_), tableInF(T,O,F,NT).
dcgordercheck(A,F,_) :- write('Error in OrderBy, attribute '),
                        write(A),
                        write(' not in FROM-table '),
                        write(F),
                        nl,
                        abort.


%------------------------------------------------------------------------------
% EliminateNot( +WithNOT, -WithoutNOT)
%------------------------------------------------------------------------------
% Input is a SQL Query, Output the SQL Query where not( ) are eliminated

eliminateNot([S,F,[],O],[S,F,[],O]) :- write('Nothing to check. '),
                                       writeln('Where-Part missing.'),
                                       abort.
eliminateNot([S,F,W,O],[S,F,Z,O]) :- killNot(W,Z).       % get wherepart

eliminateNotinExists([S,F,W,O],[S,F,Z,O]) :- killNot(W,Z).

%------------------------------------------------------------------------------
% killnot(+WherePartOfSQLTree,-ResultTreeWithoutNot)
%------------------------------------------------------------------------------

killNot(and(F,G),and(Z1,Z2)) :- killNot(F,Z1), killNot(G,Z2).
killNot(or(F,G),or(Z1,Z2)) :- killNot(F,Z1), killNot(G,Z2).
killNot(cond(C,L,R),cond(C,L,R)).
killNot(exists(A),exists(Z)) :- eliminateNot(A,Z).
killNot(not(A),Z) :- switchNot(A,Z).

%------------------------------------------------------------------------------
% switchnot(+TreeElement,-SwitchedTreeElement)
%------------------------------------------------------------------------------
% not() causes a change/switch

switchNot(or(F,G),and(Z1,Z2)) :- switchNot(F,Z1), switchNot(G,Z2).
switchNot(and(F,G),or(Z1,Z2)) :- switchNot(F,Z1), switchNot(G,Z2).
switchNot(cond(C,L,R),Z) :- condNot(C,L,R,Z).
switchNot(exists(A),not(exists(Z))) :- eliminateNotinExists(A,Z).
switchNot(not(A),Z) :- killNot(A,Z).

%------------------------------------------------------------------------------
% condNot(+EqualitySymbol,+LeftOfEquation,+RightOfEquation,-OppositeCondition
%------------------------------------------------------------------------------

condNot(eq,B,C,cond(ne,B,C)).
condNot(ne,B,C,cond(eq,B,C)).
condNot(ge,B,C,cond(lt,B,C)).
condNot(gt,B,C,cond(le,B,C)).
condNot(le,B,C,cond(gt,B,C)).
condNot(lt,B,C,cond(ge,B,C)).

%------------------------------------------------------------------------------
% eliminateExists(+SQLQuery,-SQLQueryWithEliminatedExists)
%------------------------------------------------------------------------------
%eleminates Exists which is not direct or indirect in a NOT-Environment

eliminateExists([S,F,W,O],[S,NewF,ExistsWhere,O]) :-
                                          riseExists(ExistsFrom,W,ExistsWhere),
                                          appendifnotempty(F,ExistsFrom,NewF),
                                          !.

%------------------------------------------------------------------------------
% riseExists(-NewFrom,+WhereTree,-ResultTree)
%------------------------------------------------------------------------------

riseExists(NewF,and(L1,R1),and(L2,R2)) :- riseExists(NewF1,L1,L2),
                                          riseExists(NewF2,R1,R2),
                                          appendifnotempty(NewF1,NewF2,NewF),
                                          !.
riseExists(NewF,or(L1,R1),or(L2,R2))   :- riseExists(NewF1,L1,L2),
                                          riseExists(NewF2,R1,R2),
                                          appendifnotempty(NewF1,NewF2,NewF),
                                          !.
riseExists([],cond(C,L,R),cond(C,L,R)).
riseExists([],not(A),not(A)) :- !.
riseExists(F1,exists(A),W1) :- !, eliminateExists(A,[_,F1,W1,_]).

%------------------------------------------------------------------------------
% dnfstart(+SQLQuery,-ResultSQLQuery)
%------------------------------------------------------------------------------
% Make DNF

dnfstart([S,F,W,O],[S,F,Res,O]) :- dnf(W,Res),!.
dnfstart(_,_) :- writeln('Error while DNF building.'),
                 abort.

%------------------------------------------------------------------------------
% dnf(+TreeElement,-Result)
%------------------------------------------------------------------------------
% transforms wheretree into disjunctive normal form

dnf(and(F,G),R) :- dnf(F,F1), dnf(G,G1), mult(F1,G1,R).
dnf(or(F,G),H)  :- dnf(F,F1), dnf(G,G1), append(F1,G1,H).
dnf(cond(E,L,R),[[cond(E,L,R)]]).
dnf(not(exists([S,F,W,O])),[[not(exists([S,F,Res,O]))]]) :- dnf(W,Res).

%------------------------------------------------------------------------------
% mult(+Left,+Right,-Result)
%------------------------------------------------------------------------------
% multiplies each element of Left with Right and produces Result

mult([],_,[]).
mult([F|R],G,B) :- concat_every(F,G,X),
                   mult(R,G,Y),
                   append(X,Y,B).

%------------------------------------------------------------------------------
% concat_every(+Element1,+Elements2,-Result)
%------------------------------------------------------------------------------

concat_every(_,[],[]).
concat_every(K,[K1|D],[K2|D2]) :- append(K,K1,K2), concat_every(K,D,D2).


%------------------------------------------------------------------------------
% nodes(+DNF,-Nodes)
%------------------------------------------------------------------------------
% first foreach of procedure build_graph
% creates for every attribute or constant in each conjunction a node

nodes([X|[]],[Result1Set|[]]) :- conjunction(X,Result),
                                 makeset(Result, Result1Set).
nodes([X|Rest],[Result1Set|Result2Set]) :- conjunction(X,Result1),
                                           makeset(Result1, Result1Set),
                                           nodes(Rest,Result2),
                                           makeset(Result2, Result2Set).

%------------------------------------------------------------------------------
% conjunction(+Conjunction,-ElementsInConjunction)
%------------------------------------------------------------------------------

conjunction([X],Z)   :- conjcond(X,Z).
conjunction([X|Y],Z) :- conjcond(X,Result1),
                        conjunction(Y,Result2),
                        append(Result1,Result2,Z).

%------------------------------------------------------------------------------
% conjcond(+Condition,-BothElementsOfCondition)
%------------------------------------------------------------------------------

conjcond((cond(_,L,R)),Z) :- append([L],[R],Z).

%------------------------------------------------------------------------------
% makeset(+List,-Result)
%------------------------------------------------------------------------------

makeset([],[]).
makeset([H|T1],[H|T2]):- deleteall(H,T1,L), makeset(L,T2).

%------------------------------------------------------------------------------
% deleteall(+Element,+List,-List)
%------------------------------------------------------------------------------

deleteall(_,[],[]).
deleteall(X,[X|T1],L):- deleteall(X,T1,L).
deleteall(X,[H|T1],[H|T2]):- X \= H, deleteall(X,T1,T2).

%------------------------------------------------------------------------------
% equations(+DNF,+Nodes,-N)
%------------------------------------------------------------------------------
% Select DNF elements (conjunctions) and corresponding node elements from
% Nodes and build N

equations([D1|[]],[N1|[]],[R|[]]) :- donodes(D1,N1,R).
equations([D1|D2],[N1|N2],[F1|F2]) :- donodes(D1,N1,F1),
                                      equations(D2,N2,F2).

%------------------------------------------------------------------------------
% donodes(+Con,+Nodes,-N)
%------------------------------------------------------------------------------
% builds the graph elements N for every conjunction Con and corresponding
% Nodes and returns N

donodes([D1|[]],N,F1) :- checknodes(D1,N,F1).
donodes([D1|D2],N,F2) :- checknodes(D1,N,F1), donodes(D2,F1,F2).

%------------------------------------------------------------------------------
% checknodes(+Cond,+Nodes,-N)
%------------------------------------------------------------------------------
% Produces the set N

checknodes(cond(eq,L,R),N,[F|Z2]) :- getnode(L,N,N1),
                                     getnode(R,N,N2),
                                     deletefromlist(N1,N,Z1),
                                     deletefromlist(N2,Z1,Z2),
                                     appendifdifferent(N1,N2,G),
                                     flatten(G,F1),
                                     makeset(F1,F).
checknodes(cond(ne,_,_),N,N).
checknodes(cond(ge,_,_),N,N).
checknodes(cond(le,_,_),N,N).
checknodes(cond(lt,_,_),N,N).
checknodes(cond(gt,_,_),N,N).

%------------------------------------------------------------------------------
% appendifdifferent(+List1,+List2,-AppendedIfDifferentOtherwiseList1)
%------------------------------------------------------------------------------

appendifdifferent(A,A,A).
appendifdifferent(A,B,C) :- append([A],[B],C).

%------------------------------------------------------------------------------
% appendifnotempty(+List1,+List2,-ResultList)
%------------------------------------------------------------------------------
% appends only if both lists are not empty

appendifnotempty([],[],[]) :- !.
appendifnotempty([],E2,E2) :- !.
appendifnotempty(E1,[],E1) :- !.
appendifnotempty(E1,E2,E3) :- append(E1,E2,E3).

%------------------------------------------------------------------------------
% appendifnotempty2(+List1,+List2,-ResultList)
%------------------------------------------------------------------------------
% appends only if both lists are not empty

appendifnotempty2([],[],[]) :- !.
appendifnotempty2([],_,[]) :- !.
appendifnotempty2(_,[],[]) :- !.
appendifnotempty2(E1,E2,E3) :- append(E1,E2,E3),!.
appendifnotempty2(E1,E2,E3) :- append([E1],E2,E3),!.
appendifnotempty2(E1,E2,E3) :- append(E1,[E2],E3),!.
appendifnotempty2(E1,E2,E3) :- append([E1],[E2],E3),!.

%------------------------------------------------------------------------------
% econditions(+DNF,+NodeList,-E)
%------------------------------------------------------------------------------
% e_conditions stands for the set E of graph

econditions([D1|[]],[N1|[]],[E|[]])  :- edonodes(D1,N1,E).
econditions([D1|D2],[N1|N2],[E1|E2]) :- edonodes(D1,N1,E1),
                                        econditions(D2,N2,E2).

%------------------------------------------------------------------------------
% edonodes(+ElementsOfDNF,+Nodes,-Result)
%------------------------------------------------------------------------------

edonodes([D|[]],N,E)  :- echecknodes(D,N,E).
edonodes([D1|D2],N,E) :- echecknodes(D1,N,E1),
                         edonodes(D2,N,E2),
                         appendifnotempty(E1,E2,E).

%------------------------------------------------------------------------------
% echecknodes(+Condition,+Nodes,-Resultnode)
%------------------------------------------------------------------------------

echecknodes(cond(eq,_,_),_,[]).
echecknodes(cond(ne,_,_),_,[]).
echecknodes(cond(gt,L,R),N0,[(N2,N1,'<')])  :- getnode(L,N0,N1),
                                               getnode(R,N0,N2).
echecknodes(cond(ge,L,R),N0,[(N2,N1,'<=')]) :- getnode(L,N0,N1),
                                               getnode(R,N0,N2).
echecknodes(cond(lt,L,R),N0,[(N1,N2,'<')])  :- getnode(L,N0,N1),
                                               getnode(R,N0,N2).
echecknodes(cond(le,L,R),N0,[(N1,N2,'<=')]) :- getnode(L,N0,N1),
                                               getnode(R,N0,N2).

%------------------------------------------------------------------------------
% uconditions(+DNF,+NodeList,-U)
%------------------------------------------------------------------------------
% u_conditions stands for the set U of graph

uconditions([D1|[]],[N1|[]],[U|[]]) :- udonodes(D1,N1,U).
uconditions([D1|D2],[N1|N2],[U1|U2]) :- udonodes(D1,N1,U1),
                                        uconditions(D2,N2,U2).

%------------------------------------------------------------------------------
% udonodes(+ElementsOfDNF,+Nodes,-U)
%------------------------------------------------------------------------------

udonodes([D|[]],N,U)  :- uchecknodes(D,N,U).
udonodes([D1|D2],N,U) :- uchecknodes(D1,N,U1),
                         udonodes(D2,N,U2),
                         appendifnotempty(U1,U2,U).

%------------------------------------------------------------------------------
% uchecknodes(+Condition,+Nodes,-Resultnode)
%------------------------------------------------------------------------------

uchecknodes(cond(eq,_,_),_,[]).
uchecknodes(cond(gt,_,_),_,[]).
uchecknodes(cond(ge,_,_),_,[]).
uchecknodes(cond(lt,_,_),_,[]).
uchecknodes(cond(le,_,_),_,[]).
uchecknodes(cond(ne,L,R),N,[(N1,N2)]) :- getnode(L,N,N1),
                                         getnode(R,N,N2).

%------------------------------------------------------------------------------
% getnode(+Element,+NodeList,-NodeWhereElementIsPartOf)
%------------------------------------------------------------------------------

getnode(dig(L),_,dig(L)).  % numbers are not variables that contribute a node
getnode(L,[L|_],L).
getnode(L,[N|_],N) :- element(L,N).                % N is a list itsself
getnode(L,[_|NRest],N1) :- getnode(L,NRest,N1).    % find L in NRest

%------------------------------------------------------------------------------
% element(+Element,+List)
%------------------------------------------------------------------------------
% Either Element is first element of List or Element is part of the Restlist

element(E,[E|_]).
element(E,[_|Rest]) :- element(E,Rest).

%------------------------------------------------------------------------------
% deletefromlist(+Element,+List,-Resultlist)
%------------------------------------------------------------------------------
% deletes first accurance of Element from List and gives Resultlist back

deletefromlist(E,[E|List],List) :- !.
deletefromlist(E,[K|OldList],[K|NewList]) :- deletefromlist(E,OldList,NewList).
deletefromlist(_,[],[]).

%------------------------------------------------------------------------------
% deleteallfromlist(+Element,+List,-Resultlist)
%------------------------------------------------------------------------------
% deletes every accurance of Element from List and gives Resultlist back

deleteallfromlist(_,[],[]).
deleteallfromlist(E,[(E,_,_)|OldList],NewList) :- !,
                deleteallfromlist(E,OldList,NewList).
deleteallfromlist(E,[K|OldList],[K|NewList]) :-
                deleteallfromlist(E,OldList,NewList).


%------------------------------------------------------------------------------
% cycle(+Disjunctions,+Equaleties,-NewNodes)
%------------------------------------------------------------------------------
% separates graph N,E in disjunctionterms

cycle([D|[]],[E|[]],[NewN|[]])       :- !,
                                        checkforcycle(D,E,NewN).
cycle([D1|D2],[E1|E2],[NewN1|NewN2]) :- checkforcycle(D1,E1,NewN1),
                                        cycle(D2,E2,NewN2).

%------------------------------------------------------------------------------
% checkforcycle(+Nodes,+Equaleties,-NewNodes)
%------------------------------------------------------------------------------
% check every subgraph for cycles

% check last node, find following connected node and way back
checkforcycle([N|[]],E,[]) :- followingnode(N,_,E,R),
                              isempty(R), % inconsistency found
                              !.

% check last node, find following connected node and way back
checkforcycle([N|[]],E,NewN) :- followingnode(N,NN,E,_),
                                checkforway(NN,N,E,[N|[]],NewN).

% if the last node has no followingnode with no way
checkforcycle([N1|[]],_,[N1|[]]).


%check if there are at least 2 nodes
checkforcycle([N1|_],E,[]) :- followingnode(N1,_,E,R),
                              isempty(R), % inconsistency found
                              !.
                              
%check if there are at least 2 nodes
checkforcycle([N1|_],E,[]) :- followingnode(N1,NN,E,_),
                              checkforway(NN,N1,E,[N1|[]],NewN1),
                              % checkforway fails if no way was found
                              isempty(NewN1),
                              % if NewN1 is [], then inconsistency found
                              !.

%check if there are at least 2 nodes
checkforcycle([N1|N2],E,NewRes) :- followingnode(N1,NN,E,_),
                                   checkforway(NN,N1,E,[N1|[]],NewN1),
                                   % checkforway fails if no way was found
                                   % if inkonsistent, then NewN1 is []
                                   checkforcycle(N2,E,NewN2),
                                   appendifdifferent(NewN1,NewN2,NewRes).

% if no way found from first node back, then check the second node
checkforcycle([N1|N2],E,[N1|NewN]) :- checkforcycle(N2,E,NewN).

isempty([]).

%------------------------------------------------------------------------------
% followingnode(+Node1,-Node2,+Equaleties,-Check)
%------------------------------------------------------------------------------
% Check is [] if inconsistency found, else it is Node1

followingnode(N1,N1,E,[]) :- member((N1, N1, <),E),
                             write('Inconsistent: '),
                             write(N1),
                             write(' < '),
                             write(N1),
                             write(' not possible!'),
                             nl.
followingnode(N1,NN,E,N1) :- member((NN, N1, <),E).
followingnode(N1,NN,E,N1) :- member((NN, N1, <=),E).

%------------------------------------------------------------------------------
% checkforway(+Node1,+Node2,+Equaleties,+WalkedWay,-NewNodes)
%------------------------------------------------------------------------------

checkforway(NN,N,E,Walkedway,ResN) :- directway(NN,ZK,E),
                                      not(member(ZK,Walkedway)),
                                      checkforway(ZK,N,E,[NN|Walkedway],NewN),
                                      appendifnotempty2(ZK,NewN,ResN).
checkforway(NN,N,E,Walkedway,[SortedNodes]) :-
                                     directway(NN,N,E),
                                     append([NN],Walkedway,Res1),
                                     append([NN],Res1,Res2),
                                     shiftl(Res2,Res),
                                     noltinway(Res,E),
                                     !,
                                     flatten([NN|Walkedway],MergedNodes),
                                     sort(MergedNodes,SortedNodes).
checkforway(NN,N,E,Walkedway,[]) :- directway(NN,N,E),
                                    % there is a < in the path
                                    write('Inconsistent, found < in cycle '),
                                    write([NN|Walkedway]),
                                    nl.

%------------------------------------------------------------------------------
% shiftl(+List,-LeftShiftedList)
%------------------------------------------------------------------------------

shiftl([K|Rest],List) :-  append(Rest,[K], List).
shiftl([K|Rest],List) :- append([Rest],[K], List).

%------------------------------------------------------------------------------
% directway(+Node1,+Node2,+EList)
%------------------------------------------------------------------------------

directway(N1,N2,E) :- member((N2, N1, <),E).
directway(N1,N2,E) :- member((N2, N1, <=),E).

%------------------------------------------------------------------------------
% noltinway(+List,+EList)
%------------------------------------------------------------------------------
% checks that there is no lt (<) in a way

noltinway([N1,N2|[]],E) :-   member((N1, N2, <=),E).
noltinway([N1,N2|Rest],E) :- member((N1, N2, <=),E),
                             noltinway([N2|Rest],E).

%------------------------------------------------------------------------------
% checkforconstoruneq(+N,+U,-NNew,-UNew)
%------------------------------------------------------------------------------
% checks if node contain two distinct constants or {N,N} in U (of Graph)

checkforconstoruneq([N|[]],[U|[]],[NNew|[]],[UNew|[]])   :- !,
                                        checkconstoruneq(N,U,NNew,UNew).
checkforconstoruneq([N1|N2],[U1|U2],[N1New|N2New],[U1New|U2New]) :-
                                        checkconstoruneq(N1,U1,N1New,U1New),
                                        checkforconstoruneq(N2,U2,N2New,U2New).

%------------------------------------------------------------------------------
% checkconstoruneq(+NodeList,+U,-NNew,-UNew)
%------------------------------------------------------------------------------

checkconstoruneq([],U,[],U) :- !.

checkconstoruneq([N|[]],U,[N|[]],U)  :- ifdiffconst(N,[],I),
                                        isempty(I), % no inconsistency found
                                        ifelementu(N,U,IM),
                                        isempty(IM), % no inconsistency found
                                        !.
checkconstoruneq([_|[]],_,[],[])  :- writeln('Inconsistency found.'),
                                     !.
checkconstoruneq([N1|N2],U,NR,U) :- ifdiffconst(N1,[],I),
                                    isempty(I), % no inconsistency found
                                    ifelementu(N1,U,IM),
                                    isempty(IM), % no inconsistency found
                                    checkconstoruneq(N2,U,NR2,U),
                                    appendifnotempty2(N1,NR2,NR),
                                    !.
checkconstoruneq([_|_],_,[],[]) :- writeln('Inconsistency found.'),
                                   !.

%------------------------------------------------------------------------------
% ifdiffconst(+Nodes,+[],-InconsistencyMarker)
%------------------------------------------------------------------------------
% checks if different constants are in the same node

ifdiffconst([dig(N)|[]],DigList,I)  :- !,
                                       chdi(N,DigList,I).
ifdiffconst([dig(N1)|N2],DigList,I) :- !,
                                       chdi(N1,DigList,I1),
                                       ifdiffconst(N2,[N1|DigList],I2),
                                       appendifnotempty(I1,I2,I).
ifdiffconst([str(N)|[]],DigList,I)  :- !,
                                       chdi(N,DigList,I).
ifdiffconst([str(N1)|N2],DigList,I) :- !,
                                       chdi(N1,DigList,I1),
                                       ifdiffconst(N2,[N1|DigList],I2),
                                       appendifnotempty(I1,I2,I).
ifdiffconst([_|[]],_,[]) :- !.
ifdiffconst([_|N2],DigList,I) :- !, ifdiffconst(N2,DigList,I).
ifdiffconst(_,[],[]).

%------------------------------------------------------------------------------
% chdi(+N,+List,-InconsistencyMarker)
%------------------------------------------------------------------------------
% if second argument is not empty list, then more then one const was found!

chdi(_,[],[]).
chdi(_,[_],[i]):- !,
                  write('Node contains distinct constants -> Inconsistent'),
                  nl.


%------------------------------------------------------------------------------
% ifelementu(+N,+N,-InsonsistencyMarker)
%------------------------------------------------------------------------------
% check if (N,N) is in U

ifelementu(N,U,[i]) :- member((N,N),U),
                      !,
                      write('Error: Element '), write(N),
                      write(' in N and also in U -> Inconsistent '),
                      nl.
ifelementu(_,_,[]).

%------------------------------------------------------------------------------
% sorttopological(+N,+E,-TopologicalSortedN)
%------------------------------------------------------------------------------

sorttopological([N|[]],[E|[]],[ResN|[]]) :- !,
                                            top_sort(N,E,ResN).
sorttopological([N1|N2],[E1|E2],[ResN1|ResN2]) :- top_sort(N1,E1,ResN1),
                                                  sorttopological(N2,E2,ResN2).

%------------------------------------------------------------------------------
% top_sort(+N,+E,-TopSorted)
%------------------------------------------------------------------------------

top_sort(N,[],N).
top_sort([],_,[]).
top_sort(N,E,[X|SortedN]) :- member((X,_,_),E),
                             not(member((_,X,_),E)),
                             deletefromlist(X,N,ReducedN),
                             deleteallfromlist(X,E,ReducedE),
                             top_sort(ReducedN,ReducedE,SortedN).

%------------------------------------------------------------------------------
% element_i(+List,+Elementnumber,-Element)
%------------------------------------------------------------------------------
% returns element at position elementnumber of List

element_i([N|_],1,N) :- !.
element_i([_|Rest],I,NN) :- X is I-1,
                            !,
                            element_i(Rest,X,NN).
element_i(N,1,N) :- !.

%------------------------------------------------------------------------------
% contains_constant(+List,-Type,-Value)
%------------------------------------------------------------------------------
% if list has an element of type str() or dig() return that

contains_constant([str(X)|_],str,X).
contains_constant([dig(X)|_],dig,X).
contains_constant([_|Rest],Type,Value) :- contains_constant(Rest,Type,Value).
contains_constant(dig(X),dig,X).
contains_constant(str(X),str,X).

%------------------------------------------------------------------------------
% check_in_all_ranges(+NodeList,+Type,+Value,+FromList)
%------------------------------------------------------------------------------
% checks if Value is in the ranges of every element in NodeList

check_in_all_ranges(NI,Type,Value,From) :- in_all_ranges(NI,Type,Value,From).
check_in_all_ranges(_,_,_,_) :-
    writeln('Inconsistent -> ranges of attributes do not include constant'),
    !,
    fail.

%------------------------------------------------------------------------------
% in_all_ranges(+Node,+Type,+Value,+FromList)
%------------------------------------------------------------------------------
% check for every element of node, if const/str is in the range of elements

in_all_ranges([N|[]],Type,Value,From)   :- !,
                                           in_range(N,Type,Value,From).
in_all_ranges([N|Rest],Type,Value,From) :- !,
                                           in_range(N,Type,Value,From),
                                           !,
                                           in_all_ranges(Rest,Type,Value,From).
in_all_ranges(N,Type,Value,From) :- !,in_range(N,Type,Value,From).

%------------------------------------------------------------------------------
% in_range(+Node,+Type,+Value,+FromList)
%------------------------------------------------------------------------------

in_range(str(_),str,_,_) :- !.
in_range(N,str,_,From) :- string_type(N,From),
                          !.
in_range(N,str,_,_) :- % N not string type
                       write('Error: '),
                       write(N),
                       write(' N not string-type '),
                       !,
                       fail.
in_range(dig(X),dig,X,_).  % the same node
in_range(dig(X),dig,Y,_) :- write('Error: '),
                            write(X), write(' not in range of '), writeln(Y),
                            !,
                            fail.
in_range(N,dig,X,From) :- integer_type(N,From,L,R),
                          between(L,R,X),
                          !.
in_range(N,dig,X,From) :- integer_type(N,From,_,_),
                          % but not between
                          write('Error: '),
                          write(N),
                          write(' does not include value '),
                          writeln(X),
                          !,
                          fail.
in_range(N,dig,_,_) :- write('Error: '),
                       write(N),
                       write(' N not integer-type '),
                       !,
                       fail.


%------------------------------------------------------------------------------
% tupletotable(+Tupelname,+Fromlist,-Tablename)
%------------------------------------------------------------------------------


tupletotable(T,[tvar(OT,T)|_],OT) :- !.
tupletotable(T,[tvar(OT,Table)|_],OT) :- name(T,X),
                                         deletefromlist(102,X,X1),
                                         deletefromlist(40,X1,X2),
                                         deletefromlist(41,X2,X3),
                                         name(Table,X3).
tupletotable(T,[_|Rest],NT) :- tupletotable(T,Rest,NT).

%------------------------------------------------------------------------------
% string_type(+Attribute,+FromList)
%------------------------------------------------------------------------------
% checks if Attribute is a stringtype

string_type(N,From) :- separate(N,L,R),        % separates 'table.column' at .
%                       write('Test N:'),writeln(N),
%                       write('Test L:'),writeln(L),
%                       write('Test R:'),writeln(R),
%                       write('Test From:'),writeln(From),
                       tupletotable(L,From,T),
%                       write('Test T:'),writeln(T),
                       table(T,R,stringtype,_,_).

%------------------------------------------------------------------------------
% integer_type(+Attribute,+FromList,-RestrictLeftBorder,-RestrictRightBorder)
%------------------------------------------------------------------------------
% checks if Attribute is an Integertype

integer_type(N,From,BL,BR) :- separate(N,L,R), % separates 'table.column' at .
%                              write('N :'), writeln(N),
%                              write('Left :'), writeln(L),
%                              write('Right :'), writeln(R),
                              tupletotable(L,From,T),
%                              write('Table :'), writeln(T),
                              table(T,R,integertype,BL,BR),
                              !.
integer_type(N,From,_,_) :- separate(N,L,_), % separates 'table.column' at .
                            % L is a tuple or table but not in From-List
                            not(tupletotable(L,From,_)),
                            write('Error: Tuple/Table '), write(L),
                            write(' is not in From-List: '), write(From),
                            nl,
                            !,
                            fail.
integer_type(N,_,_,_) :- write('Error: You compare an integertype column '),
                         write('with a stringtype one, watch '),
                         writeln(N),
                         !,
                         fail.

%------------------------------------------------------------------------------
% constructmodel(+N,+E,+U,+FromList)
%------------------------------------------------------------------------------
% separates the disjunctions and calls for each construct

constructmodel([[]],_,_,_) :-
     !,
     writeln('Nothing to construct, watch output before for inconsistency!').

constructmodel([N|[]],[E|[]],[U|[]],From)    :- !,
                                                construct(N,E,U,From).
constructmodel([N1|N2],[E1|E2],[U1|U2],From) :-
                                       construct(N1,E1,U1,From),
                                       constructmodel(N2,E2,U2,From).

%------------------------------------------------------------------------------
% construct(+N,+E,+U,+FromList)
%------------------------------------------------------------------------------
% N is the actual list of nodes in conjunction

construct(N,E,U,From) :-  write('Construct Model for '),
                          writeln(N),
                          nl,
                          model_construction(N,E,U,1,[],[],[],From),
                          !. % construction successful

construct(N,_,_,_) :-  write('Construct Model for '),
                       write(N),
                       writeln(' failed, watch output for inconsistency!'),
                       nl.

%------------------------------------------------------------------------------
% model_construction(+N,+E,+U,+CounterI,+V,+Min+Max,+FromList)
%------------------------------------------------------------------------------
model_construction([],_,_,_,_,_,_,_) :- !.
model_construction(N,E,U,I,V,Min,Max,From) :-
          write('Compute set V,Min,Max of possible values for node N'),
          writeln(I),
          make_V(N,I,VNew,MinNew,MaxNew,NI,From),
          write('VNew: '), write(VNew),
          write(' MinNew: '), write(MinNew),
          write(' MaxNew: '), write(MaxNew), nl,
          write('Restrict V,Min,Max using condition to previous nodes.'),
          nl,
          restrictV(N,E,U,1,I,NI,V,Min,Max,VNew,MinNew,MaxNew,ResMin),
          write('ResMin: '), write(ResMin), nl,
          write('Find out how many different values must be tried.'),nl,
          countelements(N,End),
          Begin is I + 1,
          write('Begin: '), write(Begin),
          write('End: '), write(End), nl,
          count_k(Begin,End,K,U,N,NI),
          write('Counted k: '), write(K), nl,
          write('Add actual V,Min,Max to oldlist as last elements.'),nl,
          shiftl([VNew|V],VinclI),
          write('VNew: '), write(VinclI),nl,
          shiftl([ResMin|Min],MininclI),
          write('MinNew: '), write(MininclI),nl,
          shiftl([MaxNew|Max],MaxinclI),
          write('MaxNew: '), write(MaxinclI), nl,
          write('Assign values with backtracking, do loop 1 to '),
          write(K),nl,
          !,
          assignvalues(1,K,N,E,U,I,VinclI,MininclI,MaxinclI,From).
model_construction(_,_,_,I,_,_,_,_) :-
          write('Compute set V,Min,Max of possible values for node N'),
          write(I),
          writeln(' failed.'),
          !,
          fail.

%------------------------------------------------------------------------------
% assignvalues(+1,+K,+N,+E,+U,+I,+VinclI,+MininclI,+MaxinclI,+Fromlist)
%------------------------------------------------------------------------------

assignvalues(Begin,K,N,_,_,I,_,_,_,_) :-
          Begin=<K,
          write('Assignvalue 1 - Model constructed?'), nl,
          countelements(N,ElementsInN),
          I = ElementsInN, % done, model constructed
          write('Model constructed !!'),nl,nl.
assignvalues(Begin,K,_,_,_,_,VinclI,MininclI,MaxinclI,_) :-
          Begin=<K,
          write('Assignvalue 2 - V not empty?'), nl,
          last_element(VinclI,V),
          v_number(V),              % checks if V=[dig] or V=[int]
          last_element(MininclI,A), % check if Min>Max
          last_element(MaxinclI,B),
          A>B,
          write('Inconsistent -> Empty V'),
          !,
          fail.
assignvalues(Begin,K,N,E,U,I,VinclI,MininclI,MaxinclI,From) :-
          Begin=<K,
          write('Assignvalue 3 - Recursive call did construct model?'), nl,
          countelements(N,ElementsInN),
          I < ElementsInN,
          NewI is I + 1,
          write('Actual Node is nr. '), write(I),
          write(' of '), write(ElementsInN), nl,
          write('Start model_construction for next node with'),
          write(' V: '), write(VinclI),
          write(' and Min: '), write(MininclI),
          write(' and Max: '), write(MaxinclI), nl, nl,
          !,
          model_construction(N,E,U,NewI,VinclI,MininclI,MaxinclI,From).
assignvalues(Begin,K,N,E,U,I,VinclI,MininclI,MaxinclI,From) :-
          Begin=<K,
          write('Assignvalue 4 - try next value (max. k different values)'),nl,
          countelements(N,ElementsInN),
          I < ElementsInN,
          NewK is K + 1,
          last_element(VinclI,V),
          v_number(V),
          inc_last_element(MininclI,NewMinList),
%          write('NewK: '), write(NewK), nl,
%          write('Inc last element MininclI: '), write(MininclI), nl,
%          write('NewMinList: '), write(NewMinList), nl,
          !,
          assignvalues(Begin,NewK,N,E,U,I,VinclI,NewMinList,MaxinclI,From).

%------------------------------------------------------------------------------
% restrictV(+N,+E,+U,+J,+I,+NI,+V,+Min,+Max,+Type,+MinValue,+MaxValue,-ResMin)
%------------------------------------------------------------------------------
% Restrict actual MinValue,MaxValue using condition to previous nodes Min,Max
% start from J=1 to I-1

restrictV(_,_,_,I,I,_,_,_,_,_,NewMin,_,NewMin).
restrictV(N,E,U,J,I,NI,V,Min,Max,Type,MinValue,MaxValue,ResMin) :-
            J<I,
%            write('Restrict 2'), nl,
            element_i(N,J,NJ),     %choose j-nd element
%            write('Element actual node NI: '), write(NI), nl,
%            write('Element previous n. NJ: '), write(NJ), nl,
%            write('Check if there is an element in E.'), nl,
            element((NJ,NI,C),E), %exists edge with Ni?
            !,
%            write('Found (NJ,NI,C) in E with C: '), write(C), nl,
%            write('V: '), write(V), nl,
%            write('J: '), write(J), nl,
            element_i(V,J,VNjType),
%            write('Element VNjType: '), write(VNjType), nl,
%            write('Element VNiType: '), write(Type), nl,
%            write('Check if they have same type.'), nl,
            same_type(VNjType,Type),
            element_i(Min,J,VNjMin),  %get min(Nj)
%            write('MinValue Ni: '), write(MinValue), nl,
%            write('MaxValue Ni: '), write(MaxValue), nl,
%            write('MinValue Nj: '), write(VNjMin), nl,
            % computes the new minimal value depending on min/max-border
            check_borders(VNjMin,MinValue,MaxValue,NewMin1), % =<
%            write('NewMin1: '), write(NewMin1), nl,
%            write('Borders checked'), nl,
            % check if <= or <
            inc_if_not_equal(C,NewMin1,NewMin2),
%            write('NewMin2 checked: '), write(NewMin2), nl,
%            write('U: '), write(U), nl,
%            write('NJ: '), write(NJ), nl,
%            write('NI: '), write(NI), nl,
            % check if pair is in U
            inc_if_in_u(NewMin2,NewMin,U,NJ,NI),
%            write('InU checked, NewMin: '), write(NewMin), nl,
            NewJ is J+1,
%            write('NewJ: '), write(NewJ), nl,
            !,
            restrictV(N,E,U,NewJ,I,NI,V,Min,Max,Type,NewMin,MaxValue,ResMin).
restrictV(N,E,U,J,I,NI,V,Min,Max,Type,MinValue,MaxValue,ResMin) :-
            J<I,
            % V, Min, Max are the before nodes
            % Type, MinValue and MaxValue are the settings of actual node
%            write('Restrict 3'), nl,
            element_i(N,J,NJ),     %choose j-nd element
%            write('Element actual node NI: '), write(NI), nl,
%            write('Element previous n. NJ: '), write(NJ), nl,
%            write('There is no element in E but check if there is pair in U'),
            nl,
%            write('V: '), writeln(V),
%            write('Min: '), writeln(Min),
%            write('Max: '), writeln(Max),
%            write('Type: '), writeln(Type),
%            write('MinValue: '), writeln(MinValue),
%            write('MaxValue: '), writeln(MaxValue),
            inc_if_in_u(MinValue,NewMin,U,NJ,NI),
%            write('Inc: '), write(NewMin), nl,
            NewJ is J+1,
%            write('NewJ: '), write(NewJ), nl,
            restrictV(N,E,U,NewJ,I,NI,V,Min,Max,Type,NewMin,MaxValue,ResMin).
            
restrictV(N,E,U,J,I,NI,V,Min,Max,Type,MinValue,MaxValue,ResMin) :-
            J<I,
%            write('Restrict 4'), nl,
            NewJ is J+1,
            restrictV(N,E,U,NewJ,I,NI,V,Min,Max,Type,MinValue,MaxValue,ResMin).

%------------------------------------------------------------------------------
% inc_if_not_equal(+Operator,+Min,-NewMin)
%------------------------------------------------------------------------------

inc_if_not_equal(<=,NMin,NMin).
inc_if_not_equal(<,NMin,NewMin) :- NewMin is NMin + 1.

%------------------------------------------------------------------------------
% inc_if_in_u(+MinValue,-NewMin,+U,+NJ,+NI)
%------------------------------------------------------------------------------

inc_if_in_u(NMin,NewMin,U,NJ,NI) :- element_wo(NJ,NI,U),
                                    !,
                                    NewMin is NMin + 1.
inc_if_in_u(NMin,NMin,_,_,_).

%------------------------------------------------------------------------------
% check_borders(+Left1,+Left2,+Right2,-NewLeft1)
%------------------------------------------------------------------------------

check_borders(L1,L2,R2,L1) :- between(L2,R2,L1), % checks if L1 in [L2;R2]
                              !.
check_borders(L1,L2,_,L2) :- L1=<L2,
                             !.
check_borders(L1,L2,R2,L2) :-
    L1>=R2,
    write('Inconsistent -> Borders do not match E condition.'),
    nl,
    !,
    fail.

%------------------------------------------------------------------------------
% make_V(+N,+I,-VNew,-MinNew,-MaxNew,-NI,+FromList)
%------------------------------------------------------------------------------
% first if .. then (if .. then .. else) else construct of algorithm

make_V(N,I,VNew,MinNew,MinNew,NI,From) :-
                  write('1VList N: '), write(N), nl,
                  write('Get Element I='), write(I), nl,
                  % result can be single element or list of elements
                  element_i(N,I,NI),
                  write('Element NI: '), write(NI), nl,
                  contains_constant(NI,VNew,MinNew),
                  write('Contains Constant '), nl,
                  write('VNew: '), write(VNew), nl,
                  write('MinNew: '), write(MinNew), nl,
                  check_in_all_ranges(NI,VNew,MinNew,From).
make_V(N,I,VNew,MinNew,MinNew,NI,_) :-
                  element_i(N,I,NI),
                  contains_constant(NI,VNew,MinNew),
                  % but check_in_all_ranges failed
                  writeln('Inconsistency: Check in all ranges failed!'),
                  !,
                  fail.
make_V(N,I,VNew,MinNew,MaxNew,NI,From) :-
                  write('2VList N: '), write(N), nl,
                  write('Get Element I='), write(I), nl,
                  element_i(N,I,NI),
                  write('Element NI: '), write(NI), nl,
                  write('Contains no constant '), nl,
                  build_intersection(NI,VNew,MinNew,MaxNew,From),
                  !.
make_V(N,I,_,_,_,NI,_) :-
                  element_i(N,I,NI),
                  % but build_intersection failed
                  write('Inconsistency: Build intersection failed, '),
                  writeln('watch column types!'),
                  !,
                  fail.

%------------------------------------------------------------------------------
% v_number(+Type)
%------------------------------------------------------------------------------

v_number([dig]) :- !.
v_number([int]) :- !.

%------------------------------------------------------------------------------
% same_type(+Type1,+Type2)
%------------------------------------------------------------------------------

same_type(dig,int) :- !.
same_type(dig,dig) :- !.
same_type(int,int) :- !.
same_type(int,dig) :- !.
same_type(_,_) :- write('Inconsistent -> nodes not same type in E'),
                  nl,
                  !,
                  fail.

%------------------------------------------------------------------------------
% last_element(+List,-LastElementOfList)
%------------------------------------------------------------------------------

last_element([H|[]],H).
last_element([_|Rest],Last) :- last_element(Rest,Last).

%------------------------------------------------------------------------------
% inc_last_element(+List,-NewList)
%------------------------------------------------------------------------------

inc_last_element([H|[]],[LastInc|[]]) :- LastInc is H + 1.
inc_last_element([H|Rest],[H|LastNew]) :- inc_last_element(Rest,LastNew).

%------------------------------------------------------------------------------
% count_k(+Begin,+End,-K,+U,+N,+I)
%------------------------------------------------------------------------------

count_k(Begin,End,NewK,U,N,NI) :-  Begin=<End,
%                                   write('count N: '), write(N), nl,
%                                   write('count Begin: '), write(Begin), nl,
                                   element_i(N,Begin,NB),
%                                    write('count NI: '), write(NI), nl,
%                                    write('count NB: '), write(NB), nl,
%                                    write('count U: '), write(U), nl,
                                   element_wo(NI,NB,U),
%                                   write('Pair in U, NI: '), write(NI), nl,
                                   NewBegin is Begin + 1,
%                                   write('Newbegin: '), write(NewBegin), nl,
%                                   write('End: '), write(End), nl,
                                   count_k(NewBegin,End,K,U,N,NI),
                                   NewK is K + 1.
count_k(Begin,End,K,U,N,NI) :- Begin=<End,
                               NewBegin is Begin + 1,
                               count_k(NewBegin,End,K,U,N,NI).
count_k(Begin,End,1,_,_,_) :- Begin > End.

%------------------------------------------------------------------------------
% element_wo(+A,+B,+U)
%------------------------------------------------------------------------------
% element without order as a pair in U

element_wo(A,B,U) :- element((A,B),U).
element_wo(A,B,U) :- element((B,A),U).

%------------------------------------------------------------------------------
% countelements(+List,-number)
%------------------------------------------------------------------------------

countelements([_|[]],1).
countelements([_|Rest],Nr) :- countelements(Rest,RestNr),
                              Nr is RestNr + 1.

%------------------------------------------------------------------------------
% build_intersection(+List,-Type,-Min,-Max,+From)
%------------------------------------------------------------------------------
% either all elements in a node (+List) are string or integer type

build_intersection([N|[]],str,[],[],From) :-
      !,
      string_type(N,From).
build_intersection([N|Rest],str,[],[],From) :-
      string_type(N,From),
      !,
      rest_are_stringtype(Rest,From).
build_intersection([dig(N)|Rest],int,Min,Max,From) :-
      !,
      rest_are_integertype(Rest,Min1,Max1,From),
      bigger(N,Min1,Min),
      smaller(N,Max1,Max),
      !,
      max_biggerthen_min(Min,Max).
build_intersection([N|[]],int,Min,Max,From) :-
      !,
      integer_type(N,From,Min,Max).
build_intersection([N|Rest],int,Min,Max,From) :-
      !,
      integer_type(N,From,Min2,Max2),
      rest_are_integertype(Rest,Min1,Max1,From),
      bigger(Min2,Min1,Min),
      smaller(Max2,Max1,Max),
      !,
      max_biggerthen_min(Min,Max).
build_intersection(N,str,[],[],From) :- string_type(N,From),
                                        !.
build_intersection(dig(N),int,N,N,_) :- !.
build_intersection(N,int,Min,Max,From) :- !,
                                          integer_type(N,From,Min,Max).

%------------------------------------------------------------------------------
% rest_are_stringtype(+List,+From)
%------------------------------------------------------------------------------

rest_are_stringtype([N|[]],From) :- !,
                                    string_type(N,From).
rest_are_stringtype([N|Rest],From) :- string_type(N,From),
                                      rest_are_stringtype(Rest,From).

%------------------------------------------------------------------------------
% rest_are_integertype(+List,Min,Max,+From)
%------------------------------------------------------------------------------

rest_are_integertype([N|[]],Min,Max,From) :- !,
                                             integer_type(N,From,Min,Max).
rest_are_integertype([N|Rest],Min,Max,From) :- integer_type(N,From,Min1,Max1),
                                    rest_are_integertype(Rest,Min2,Max2,From),
                                    bigger(Min1,Min2,Min),
                                    smaller(Max1,Max2,Max).

%------------------------------------------------------------------------------
% bigger(+A,+B,-BiggestOfThem)
%------------------------------------------------------------------------------

bigger(A,B,A) :- A>=B.
bigger(_,B,B).

%------------------------------------------------------------------------------
% smaller(+A,+B,-SmallestOfThem)
%------------------------------------------------------------------------------

smaller(A,B,A) :- A=<B.
smaller(_,B,B).

%------------------------------------------------------------------------------
% max_biggerthen_min(+Min,+Max)
%------------------------------------------------------------------------------

max_biggerthen_min(Min,Max) :- Max >= Min.
max_biggerthen_min(Min,Max) :- Max < Min,
                 write('Inconsistent -> Range problem. Min bigger then Max'),
                 nl,
                 abort.

%------------------------------------------------------------------------------
% separate(+Element,-Leftpart,-Rightpart)
%------------------------------------------------------------------------------
% separates table.column into table and column

separate(N,L,R) :- name(N,NList),
                   split(46,NList,LList,RList),
                   name(L,LList),
                   name(R,RList).

%------------------------------------------------------------------------------
% split(+Element,+List,-L1,-L2)
%------------------------------------------------------------------------------
% splits List in L1 and L2 when first Element found in List.
% Element is not part of list L1 neither L2

split(E,[E|Rest],[],Rest).
split(E,[K|Rest],[K|L1],L2) :- not(E=K),
                               split(E,Rest,L1,L2).

%------------------------------------------------------------------------------
% newdnf(+DNF,-NewDNF)
%------------------------------------------------------------------------------
% start replacement of [tuple,attribute] by tuple.attribute

newdnf([K|[]],[R1|[]]) :- newdnfkon(K,R1).
newdnf([K|Rest],[R1|R2]) :- newdnfkon(K,R1),
                            newdnf(Rest,R2).

%------------------------------------------------------------------------------
% newdnfkon(+List,-Result)
%------------------------------------------------------------------------------

newdnfkon([K|[]],[R1|[]]) :- newdnfkondo(K,R1).
newdnfkon([K|Rest],[R1|R2]) :- newdnfkondo(K,R1),
                               newdnfkon(Rest,R2).

%------------------------------------------------------------------------------
% newdnfkondo(+Condition,-NewCondition)
%------------------------------------------------------------------------------
% replaces [tuple,attribute] by tuple.attribute

newdnfkondo(cond(A,[B,C],[D,E]),cond(A,R1,R2)) :-
    names(B,B1),
    names(C,C1),
    name('.',P),
    append(B1,P,B1P),
    append(B1P,C1,BC),
    name(R1,BC),
    names(D,D1),
    names(E,E1),
    append(D1,P,D1P),
    append(D1P,E1,DE),
    name(R2,DE).
newdnfkondo(cond(A,[B,C],D),cond(A,R1,D)) :-   % second arg is dig(nr) or str
    names(B,B1),
    names(C,C1),
    name('.',P),
    append(B1,P,B1P),
    append(B1P,C1,BC),
    name(R1,BC).
newdnfkondo(cond(A,B,[D,E]),cond(A,B,R2)) :-   % first arg is dig(nr) or str
    names(D,D1),
    names(E,E1),
    name('.',P),
    append(D1,P,D1P),
    append(D1P,E1,DE),
    name(R2,DE).
newdnfkondo(cond(A,B,C),cond(A,B,C)).   % both arg are dig(number)
%newdnfkondo(not(exists([S,F,W1,O])),not(exists([S,F,W2,O]))) :- newdnf(W1,W2).

%------------------------------------------------------------------------------
% getfromlist(+SQLQuery,-FromPartOfSQLQuery)
%------------------------------------------------------------------------------

getfromlist([_,From,_,_],From).

%------------------------------------------------------------------------------
% names(+Expression,-AsciiList)
%------------------------------------------------------------------------------
% like name(), but also names a function like f(a) to [102,40,97,41]

names(f(A),E):- name(A,B),            % (=40 )=41
                !,
                append(B,[41],C),
                append([40],C,D),
                append([102],D,E).
names(A,B):- name(A,B).

%------------------------------------------------------------------------------
% checkIfSkolemNecessary(+SQLQuery,-Skolemnized)
%------------------------------------------------------------------------------
% if DNF contains not(exists(..)) then skolemnisation is necessary

checkIfSkolemNecessary([_,F,W,_],Sk) :- checkIfSkolemConj(F,W,Sk).

%------------------------------------------------------------------------------
% checkIfSkolemConj(+From,+Where,-Skolemnized)
%------------------------------------------------------------------------------
% separate and check each conjunction element

checkIfSkolemConj(F,[W|[]],Sk)    :- !,
                                     checkIfSkolemIn(F,W,Sk).
checkIfSkolemConj(F,[W|WRest],Sk3):- checkIfSkolemIn(F,W,Sk1),
                                     !,
                                     checkIfSkolemConj(F,WRest,Sk2),
                                     appendifnotempty(Sk1,Sk2,Sk3).

%------------------------------------------------------------------------------
% checkIfSkolemIn(+From,+Where,-SkolemizedPart)
%------------------------------------------------------------------------------
% if not(exists(..)) is included, start, else return [] for Skolemlist

checkIfSkolemIn(F,W,FinalSkolem) :- member(not(exists(_)),W),
                        skolemnize(F,W,[],[],Exist,_,0),
                        !,
                        buildSetOfSkolem(Exist,Exist,FinalSkolem).
checkIfSkolemIn(_,_,[]).


%------------------------------------------------------------------------------
% buildSetOfSkolem(+ExistPart,+ExistPart,-FinalSkolemPart)
%------------------------------------------------------------------------------

buildSetOfSkolem([[f(A,[],B)]|[]],_,[f(A,[],B)|[]]).
buildSetOfSkolem([[f(A,[],B)]|Rest],Exist,[f(A,[],B)|F2]) :-
    buildSetOfSkolem(Rest,Exist,F2).
buildSetOfSkolem([[f(A,List,B)]|Rest],Exist,[f(A,List,B)|F2]) :-
    everyElOfListIsInEx(List,Exist),
    !,
    buildSetOfSkolem(Rest,Exist,F2).
buildSetOfSkolem([[f(_,_,_)]|Rest],Exist,F2) :-
    buildSetOfSkolem(Rest,Exist,F2).
buildSetOfSkolem([[f(_,[List],_)]|[]],Exist,[f(_,[List],_)|[]]) :-
    everyElOfListIsInEx(List,Exist),
    !.
buildSetOfSkolem([[f(_,_,_)]|[]],_,[]).

%------------------------------------------------------------------------------
% everyElOfListIsInEx(+List,+Exist)
%------------------------------------------------------------------------------

everyElOfListIsInEx([u(_,Table)|[]],Exist):- member([f(_,[],Table)],Exist).
everyElOfListIsInEx([u(_,Table)|[]],Exist):- member([f(_,List,Table)],Exist),
                                             elOfListHasExTupleVar(List,Exist).
everyElOfListIsInEx([u(_,Table)|Rest],Exist):- member([f(_,[],Table)],Exist),
                                               everyElOfListIsInEx(Rest,Exist).

%------------------------------------------------------------------------------
% elOfListHasExTupleVar(+List,+Exist)
%------------------------------------------------------------------------------

elOfListHasExTupleVar([u(_,Table)|_],Exist) :-
   member([f(_,[],Table)],Exist),
   !.
elOfListHasExTupleVar([u(_,Table)|_],Exist) :-
   member([f(_,List,Table)],Exist),
   !,
   everyElOfListIsInEx(List,Exist).
elOfListHasExTupleVar([_|Rest],Exist) :- elOfListHasExTupleVar(Rest,Exist).

%------------------------------------------------------------------------------
% skolemnize(+F,+W,+StartExistent,+SartUnivers,-Existential,-Universal,+Level)
%------------------------------------------------------------------------------
% constructs skolem functions
% makes set for existential variables which are in 0,2,4,.. Level

skolemnize(F,W,StEx,StUn,Exist3,Unive3,Level) :-  % more not exists subqueries
      0 is Level mod 2,
      addExSet(F,W,Exist1,StUn,StEx), % makes skolemfunc. for tuples in F
      member(not(exists([_,F1,[W1],_])),W), % find first subquery def. in W
      !,
      LevelNew is Level +1,
      skolemnize(F1,W1,Exist1,StUn,Exist2,Unive2,LevelNew),
      deletefromlist(not(exists([_,F1,[W1],_])),W,NewW), % del 1. notEx from W
      !,
      skolemfindmore(F,NewW,Exist2,Unive2,Exist3,Unive3,Level).
skolemnize(F,W,StEx,StUn,Exist1,StUn,Level) :- % no more subqu. in where-clause
      0 is Level mod 2,
      % but no more not exists subqueries
      addExSet(F,W,Exist1,StUn,StEx). % makes skolemfunc. for tuples in F

skolemnize(F,W,StEx,StUn,Exist3,Unive3,Level) :-  % subqueries in where clause
      1 is Level mod 2,
      addUnSet(F,StUn,NewStUn), % NewStUn = StUn + new univ.tv from F
      member(not(exists([_,F1,[W1],_])),W), % find subquery definition in W
      !,
      LevelNew is Level + 1,
      skolemnize(F1,W1,StEx,NewStUn,Exist,Unive,LevelNew),
      deletefromlist(not(exists([_,F1,[W1],_])),W,NewW), % del first notEx
      !,
      skolemfindmore(F,NewW,Exist,Unive,Exist3,Unive3,Level).
skolemnize(F,_,StEx,StUn,StEx,NewStUn,Level) :- % no subquery
      1 is Level mod 2,
      addUnSet(F,StUn,NewStUn). % NewStUn = StUn + new univ.tv from F


%------------------------------------------------------------------------------
% skolemfindmore(+F,+W,+Ex,+Un,-Existential,-Universal,+Level)
%------------------------------------------------------------------------------
% find more not exists expressions in the same (even) level.

skolemfindmore(F,W,Ex,Un,Exist3,Unive3,Level) :-
      member(not(exists([_,F1,[W1],_])),W),  % find next subquery def. in W
      !,
      LevelNew is Level +1,
      skolemnize(F1,W1,Ex,Un,Exist2,Unive2,LevelNew),
      % delete first notexists from w, try to find more
      deletefromlist(not(exists([_,F1,[W1],_])),W,NewW),
      skolemfindmore(F,NewW,Exist2,Unive2,Exist3,Unive3,Level).
skolemfindmore(_,_,E,U,E,U,_).

%------------------------------------------------------------------------------
% addUnSet(+From,+StartingUniversal,-NewStUn)
%------------------------------------------------------------------------------
% puts actual tables into universal list

addUnSet([F|[]],StUn,[U|StUn])     :- addToUnSet(F,U).
addUnSet([F|FRest],StUn,[U|URest]) :- addToUnSet(F,U),
                                      addUnSet(FRest,StUn,URest).

%------------------------------------------------------------------------------
% addToUnSet(+From,-Universal)
%------------------------------------------------------------------------------

addToUnSet(tvar(Table,Tuple),u(Tuple,Table)).

%------------------------------------------------------------------------------
% addExSet(+F,+W,-Exist1,+StUn,+StEx)
%------------------------------------------------------------------------------
% add foreach tuple in fromclause an ex. skolem function with opt. param.

% addExSet(F,W,Exist1,StUn,StEx),

addExSet([F|[]],W,[Ex|StEx],StUn,StEx) :- !,
                                          addToExSet(F,W,Ex,StUn).
addExSet([F|FRest],W,[Ex|ERest],StUn,StEx) :-
    addToExSet(F,W,Ex,StUn),
    !,
    addExSet(FRest,W,ERest,StUn,StEx).

%------------------------------------------------------------------------------
% addToExSet(+F,+W,-Exist1,+StUn)
%------------------------------------------------------------------------------

% first level; and levels, where no universal tuple variables before
addToExSet(tvar(Table,Tuple),_,[f(Tuple,[],Table)],[]) :- !.
addToExSet(tvar(Table,Tuple),W,[f(Tuple,URList,Table)],StUn) :-
      % check which universal tuple variables from StUn
      % appear in this query or in a subquery and put them into U(niversal)List
      flatten(W,NewW), % flatten the where part
      isInList(StUn,NewW,UList,Table),%elements from StUn into UList if in NewW
      !,
      makeset(UList,URList). % remove duplicate entries
      
%------------------------------------------------------------------------------
% isInList(+StUn,+W,-U,+Table)
%------------------------------------------------------------------------------
% checks if tuplevar from StUn appears in a cond(..) of W-List

isInList([],_,[],_). % no univ. tuple variables in enclosing levels (in Un)
isInList([u(Tuple,Table)|[]],W,[u(Tuple,Table)|[]],T) :- isInListCond(Tuple,W),
                                                         not(Table=T).
isInList([u(_,_)|[]],_,[],_).
isInList([_|[]],_,[],_).            % superfluos
isInList([u(Tuple,Table)|Rest],W,[u(Tuple,Table)|U2],T):-
                                         isInListCond(Tuple,W),
                                         not(Table=T),
                                         !,
                                         isInList(Rest,W,U2,T).
isInList([u(_,_)|Rest],W,U2,T):- !,
                                         isInList(Rest,W,U2,T).
isInList([_|Rest],W,U2) :- isInList(Rest,W,U2).

%------------------------------------------------------------------------------
% isInListCond(+T,+WhereList)
%------------------------------------------------------------------------------
% checks if a tuple T is part of a condition of actual WhereList

isInListCond(T,W) :- member(cond(_,[T,_],[_,_]),W),!.
isInListCond(T,W) :- member(cond(_,[_,_],[T,_]),W),!.

%------------------------------------------------------------------------------
% skolemnizeDNF(+DNF,+Skolemset,-WhereTree)
%------------------------------------------------------------------------------

skolemnizeDNF([_,_,W,_],[],W).
skolemnizeDNF([_,F,W,_],Skolem,Tree) :-
                                        write('WRes: '),
                                        writeln(W),
                                        dnfReplace(W,Skolem,WRes1,1,F),
                                        write('WResReplace: '),
                                        writeln(WRes1),
                                        !,
                                        skolemToTree(WRes1,WRes), % make tree
                                        write('SkolemToTree: '),
                                        writeln(WRes),
                                        !,
                                        killNot(WRes,Tree1), % remove not
                                        write('SkolemToTreeWithoutNot: '),
                                        writeln(Tree1),
                                        !,
                                        dnf(Tree1,Tree). % make DNF


%------------------------------------------------------------------------------
% skolemToTree(+WherePart,-Tree)
%------------------------------------------------------------------------------
% separates the or-parts

isListe([_|_]).

skolemToTree([W|[]],Res) :- skolemToTree(W,Res).
skolemToTree([W|Rest],or(R1,R2)) :- isListe(W),
                                    !,
                                    skolemToTree(W,R1),
                                    skolemToTree(Rest,R2).
                                    
skolemToTree([W|Rest],and(R1,R2)) :- skolemToTree(W,R1),
                                     skolemToTree(Rest,R2).

skolemToTree(cond(A,B,C),cond(A,B,C)) :- !.
skolemToTree(not(A),not(Res)) :- !,
                                 skolemToTree(A,Res).

%------------------------------------------------------------------------------
% dnfReplace(+WList,+Skolem,-W,+Level,+From)
%------------------------------------------------------------------------------
% separates disjuntions, replace each disjunction

dnfReplace([W|[]],Skolem,[WRes|[]],L,F) :- !,
                                           skolemnizeConj(W,Skolem,WRes,L,F).
dnfReplace([W|Rest],Skolem,[W1|W2],L,F) :- skolemnizeConj(W,Skolem,W1,L,F),
                                           dnfReplace(Rest,Skolem,W2,L,F).

%------------------------------------------------------------------------------
% skolemnizeConj(+WList,+Skolem,-W,+Level,From)
%------------------------------------------------------------------------------
% WList is a list of conjunctions

skolemnizeConj([W|[]],Skolem,[WRes|[]],L,F) :-
   !,
%   write(' SD0W: '), writeln(W),
%   write(' Level: '), writeln(L),
   skolemreplace(W,Skolem,WRes,L,F).
skolemnizeConj([W|Rest],Skolem,[W1|W2],L,F) :-
%   write(' SD1W: '), writeln(W),
%   write(' SDWRest: '), writeln(Rest),
%   write(' Level: '), writeln(L),
   skolemreplace(W,Skolem,W1,L,F),
%   write(' SD1W1: '), writeln(W1),
   !,
   skolemnizeConj(Rest,Skolem,W2,L,F).

%------------------------------------------------------------------------------
% skolemreplace(+Element,+Skolem,-NewElement,+Level,+From)
%------------------------------------------------------------------------------
% first or second arg is dig(nr) or str if D instead of [D]
% starting Level is 1

skolemreplace(cond(A,[B,C],[D,E]),Skolem,cond(A,[R1,C],[R2,E]),L,F) :-
   1 is L mod 2,
%   writeln('D1'),
   changeskolem(B,C,Skolem,R1,F),
   changeskolem(D,E,Skolem,R2,F).
%   writeln('D1D').
skolemreplace(cond(A,[B,C],D),Skolem,cond(A,[R1,C],D),L,F) :-
   1 is L mod 2,
   changeskolem(B,C,Skolem,R1,F).
skolemreplace(cond(A,B,[D,E]),Skolem,cond(A,B,[R2,E]),L,F) :-
   1 is L mod 2,
   changeskolem(D,E,Skolem,R2,F).
skolemreplace(cond(A,B,C),_,cond(A,B,C),L,_) :-
   1 is L mod 2.
skolemreplace(not(exists([_,F,[W1],_])),Skolem,not(W3),L,Fl) :-
   1 is L mod 2, % odd: 1,3,5,.. replace where by s(phi_1) or ... or s(phi_k)
   NewL is L + 1,
%   write('Level :'), writeln(L),
%   write('Global F:'), writeln(Fl),
%   write('Local F :'), writeln(F),
%   write('Skolem  :'), writeln(Skolem),
%   appendifnotempty(F,Fl,NewF),
%   write('L1W1: '),writeln(W1),
%   skolemnizeConj(W1,Skolem,WS,NewL,NewF),
   skolemOdd(F,F,Fl,Skolem,W1,W2,NewL),
   makeset(W2,W3).          % remove duplicates
%   write('L1W2:'),writeln(W2),
%   write('L1W3:'),writeln(W3).


skolemreplace(not(exists([_,F,[W1],_])),Skolem,not(W2),L,Fl) :-
   0 is L mod 2,  % 2,4,6,...
   NewL is L + 1,
%   write('Globel F:'), writeln(Fl),
%   write('Local F :'), writeln(F),
   appendifnotempty(F,Fl,NewF),
%   write('L2W1:'),writeln(W1),
%   write('NewL:'),writeln(NewL),
   skolemnizeConj(W1,Skolem,W2,NewL,NewF).
%   write('L2W2:'),writeln(W2).
skolemreplace(cond(A,[B,C],[D,E]),Skolem,cond(A,[R1,C],[R2,E]),L,F) :-
   0 is L mod 2,
%   writeln('D2'),
%   write('From:'), writeln(F),
   changeskolem(B,C,Skolem,R1,F),
   changeskolem(D,E,Skolem,R2,F).
%   writeln('D2D').
skolemreplace(cond(A,[B,C],D),Skolem,cond(A,[R1,C],D),L,F) :-
   0 is L mod 2,
   changeskolem(B,C,Skolem,R1,F).
skolemreplace(cond(A,B,[D,E]),Skolem,cond(A,B,[R2,E]),L,F) :-
   0 is L mod 2,
   changeskolem(D,E,Skolem,R2,F).
skolemreplace(cond(A,B,C),_,cond(A,B,C),L,_) :-
   0 is L mod 2.

%------------------------------------------------------------------------------
% skolemOdd(+LT,+ALT,+GlobalTables,+Skolem,+Where,-ResultList,+Level)
%------------------------------------------------------------------------------
% LT=Local Tables, ALT=AllLocalTables
% Interpretation of ResultList: Element_1 OR .. OR Element_k

skolemOdd([LT|[]],ALT,GT,S,W,[R1|R2],L) :-
      appendifnotempty([LT],GT,NewF),
      skolemnizeConj(W,S,R1,L,NewF),
      countTableInSkolem(LT,S,Number),  % more skolemfunctions for this table?
      Number > 1,                       % yes there are more possibilities
      removeTableFromSkolem(LT,S,NewSkolem), % then use next skolem function
      skolemOdd([LT|[]],ALT,GT,NewSkolem,W,R2,L).
skolemOdd([LT|[]],_ALT,GT,S,W,[R|[]],L) :-
      appendifnotempty([LT],GT,NewF),
      skolemnizeConj(W,S,R,L,NewF),
      countTableInSkolem(LT,S,Number),  % more skolemfunctions for this table?
      Number < 2.                       % no, not more available
      
skolemOdd([LT|LTMore],ALT,GT,S,W,R,L) :-
      appendifnotempty(ALT,GT,NewF),    % all accessable froms, local & higher
      skolemnizeConj(W,S,R1,L,NewF),    % do all, use first skolem fct f. table
      countTableInSkolem(LT,S,Number),  % more skolemfunctions for this table?
      Number > 1,                       % yes there are more possibilities, but
      skolemOdd(LTMore,ALT,GT,S,W,R2,L),% first donext tables withthis skol.fct
      removeTableFromSkolem(LT,S,NewSkolem), % then use next skolem function
      skolemOdd([LT|LTMore],ALT,GT,NewSkolem,W,R3,L), % & do all possibilities
      appendifnotempty(R1,R2,RX), % Result With First Skolem Function
      appendifnotempty(RX,R3,R).  % Result With Following Skolem Functions
skolemOdd([LT|LTMore],ALT,GT,S,W,R,L) :-
      appendifnotempty(ALT,GT,NewF),    % all accessable froms, local & higher
      skolemnizeConj(W,S,R1,L,NewF),    % do all, use first skolem fct f. table
      countTableInSkolem(LT,S,Number),  % more skolemfunctions for this table?
      Number < 2,                       % no, not more available, try to change
      skolemOdd(LTMore,ALT,GT,S,W,R2,L),% usage of skolem fct of other tables
      appendifnotempty(R1,R2,R).

countTableInSkolem(tvar(Table,_),[f(_,_,Table)|[]],1) :- !.
countTableInSkolem(tvar(_,_),[_|[]],0).
countTableInSkolem(tvar(Table,T),[f(_,_,Table)|Rest],Nr) :-
       !,
       countTableInSkolem(tvar(Table,T),Rest,RestNr),
       Nr is RestNr + 1.
countTableInSkolem(tvar(Table,T),[_|Rest],Nr) :-
       countTableInSkolem(tvar(Table,T),Rest,Nr).


removeTableFromSkolem(tvar(Table,_),S,NewSkolem) :-
    deletefromlist(f(_,_,Table),S,NewSkolem).


%------------------------------------------------------------------------------
% changeskolem(+Tuple,+Column,+Skolem,-SkolemFunction,+FromList)
%------------------------------------------------------------------------------

changeskolem(Tuple,_,Skolem,f(B),FromList) :-
   member(tvar(Table,Tuple),FromList),   % get Tablename of Tuple from FromList
   member(f(B,_,Table),Skolem).       % get Skolemfunction f(B) over that Table

%------------------------------------------------------------------------------
% addSkolemToFrom(+SkolemSet,+From,-SKFrom)
%------------------------------------------------------------------------------
addSkolemToFrom([],From,From):-!.
addSkolemToFrom([f(Name,_,Table)|[]], From, [tvar(Table,Name)|From]).
addSkolemToFrom([f(Name,_,Table)|SRest], From, [tvar(Table,Name)|SKF2]) :-
                                          addSkolemToFrom(SRest,From,SKF2).

%------------------------------------------------------------------------------
% Definitions of columns
%------------------------------------------------------------------------------

table(mitarbeiterkosten,name,stringtype,no,no).
table(mitarbeiterkosten,jahr,integertype,1945,2008).
table(mitarbeiterkosten,jahresgehalt,integertype,0,200000).
table(mitarbeiterkosten,urlaubstage,integertype,0,60).
table(mitarbeiterkosten,resturlaub,integertype,0,60).

table(mitarbeiterdaten,name,stringtype,no,no).
table(mitarbeiterdaten,strasse,stringtype,no,no).
table(mitarbeiterdaten,nummer,stringtype,no,no).
table(mitarbeiterdaten,wohnort,stringtype,no,no).
table(mitarbeiterdaten,plz,integertype,0,99999).

table(abteilungen,abteilungsname,stringtype,no,no).
table(abteilungen,gruendungsjahr,integertype,1950,2030).

table(mitarbeiter,name,stringtype,no,no).
table(mitarbeiter,abteilung,stringtype,no,no).

table(fuehrungskader,abteilungsname,stringtype,no,no).
table(fuehrungskader,mitarbeitername,stringtype,no,no).

%------------------------------------------------------------------------------
run :- scanner(TokenList),            % analyzes input & transforms into a list
       write('TokenList:  '),
       write(TokenList),              % prints TokenList to screen
       nl,
       phrase(query(Q),TokenList),    % analyzes TokenList with DCG
       write('DCG Result: '),
       write(Q),                      % prints result, accepted or not by DCG
       nl,
       !,
       dcgcheck(Q,QFilled),
       write('Filled Query: '),    % adds table or tuplenames to columns
       write(QFilled),
       nl,
       !,
       eliminateNot(QFilled,QNoNot),
       write('Query Eliminated NOT: '),
       write(QNoNot),
       nl,
       !,
       eliminateExists(QNoNot,QNoEx),
       % eliminates only EXISTS which is not in not()-Env
       write('Query Eliminated EXISTS: '),
       write(QNoEx),
       nl,
       !,
       dnfstart(QNoEx,DNF1), % Where-Part is a list of disjunctions
       write('DNF: '),
       write(DNF1),
       nl,
       !,
       % is not(exists) contained in query, then create & replace by skolemf.
       checkIfSkolemNecessary(DNF1,SkolemSet),
       write('SkolemSet: '),
       write(SkolemSet),
       nl,
       !,
       skolemnizeDNF(DNF1,SkolemSet,DNFS), % skolemnize if SkolemSet not []
       write('DNF-Where After Skolem: '),
       write(DNFS),
       nl,
       !,
       write('Final DNF: '),
       newdnf(DNFS,DNF), % Replaces [tuple,attribute] by tuple.attribute
       write(DNF),
       nl,
       !,
       write('List Of Elements In Every Disjunctionterm: '), % 1. foreach
       nodes(DNF,N),
       write(N),
       nl,
       write('--- Created Graph - Start ---'),
       nl,
       write('N: '),      % 2. foreach
       equations(DNF,N,FN),
       write(FN),
       nl,
       write('E: '),      % 3.+4. foreach
       econditions(DNF,FN,EC),             %
       write(EC),
       nl,
       write('U: '),      % 5. foreach
       uconditions(DNF,FN,UC),
       write(UC),
       nl,
       write('--- Created Graph - End -----'),
       nl,
       write('Looking for cycles in graph'),
       nl,
       !,
       cycle(FN,EC,NewN), % checks for cycles, removes inconsistent subgraphs
       nl,
       write('New Set N: '),
       write(NewN),
       nl,
       write('Check if node contain two distinct constants or {N,N} in U'),
       nl,
       !,
       checkforconstoruneq(NewN,UC,NWC,UWC),
       writeln('Remove inconsistent disjunctions from graph.'),
       write('  N Before: '), writeln(NewN),
       write('  U Before: '), writeln(UC),
       nl,
       write('  N After : '), writeln(NWC),
       write('  U After : '), writeln(UWC),
       !,
       write('Topological sorted N: '),
       sorttopological(NWC,EC,SortedN),
       write(SortedN),
       nl,
       !,
       getfromlist(QNoEx,From),
       !,
       addSkolemToFrom(SkolemSet,From,SKNew),
       !,
       makeset(SKNew,SKFrom), % remove duplicates
       write('NewFromSet: '), write(SKFrom),nl,
       write('Try to construct model: '),
       nl, nl,
       !,
       constructmodel(SortedN,EC,UWC,SKFrom).
run :- write('Analysing Input with DCG failed. Stopped!!').
