%==============================================================================
% Project:	Microcontroller Programming in Datalog
% Version:	0.4
% Filename:	ctest.pl
% Purpose:	Main Program of Prototype for Constraint Checker
% Last Change:	29.03.2021
% Language:	Prolog (tested with SWI Prolog)
% Author:	Stefan Brass
% Email:	brass@informatik.uni-halle.de
% WWW:		http://www.informatik.uni-halle.de/~brass/
% Address:	Univ. Halle, Von-Seckendorff-Platz 1, D-06120 Halle, GERMANY
% Copyright:	(c) 2020-2021 by Stefan Brass
%==============================================================================


%==============================================================================
% README:
% ------
%
% - This is a Prolog program (tested with SWI Prolog).
%   If you do not have Prolog yet, download SWI Prolog from:
%       https://www.swi-prolog.org/
%   If you have another Prolog system, and my program should not work with
%   that, please let me know: brass@informatik.uni-halle.de.
%   I am interested in portable programming.
%
% - Start the Prolog system, and load ("consult") this program.
%   If this file 'ctest.pl' is in the same directory:
%       ?- [ctest].
%   (here, ?- is the prompt of the Prolog system).
%   Do not forget the full stop '.' at the end of the command.
%   If the file is not in the current directory of the Prolog system:
%       ?- ['C:/my/path/ctest.pl'].
%   SWI Prolog will understand / even on Windows.
%   If you want to use \, you must double that, because the backslash starts
%   special escape sequences.
%
% - If you just want to run the example from the paper:
%       ?- example.
%   This uses a built-in version of the example rules and constraints.
%
% - You can also load the example from the file blink0.mlg.
%   This is done with
%       ?- load(blink0).
%   You can also specify the full path, if necessary:
%       ?- load('C:/my/path/blink0.mlg').
%   To see the loaded rules and constraints
%   (already transformed to pure Datalog),
%   use
%	?- show.
%   To check whether the constraints are guaranteed to hold:
%       ?- ctest.
%
% - The currently available user commands (Prolog predicates) are listed with:
%       ?- h.
%
% - To leave Prolog:
%       ?- halt.
%   (Again, the full stop at the end is important in Prolog.)
%
% - The program will be developed further.
%   Please check for new versions at:
%   http://users.informatik.uni-halle.de/~brass/micrologS/ctest.pl
%   This is version 0.4 from March 29, 2021.
%
% - This version has a small self-built consistency check for the
%   arithmetic constraints.
%   It is probably not complete, however this is sufficient for the
%   correctness of the approach:
%   If the prover can show all violation conditions as inconsistent,
%   the constraints/invariants are guaranteed to be satisfied.
%   We will continue to work on this, but at the moment it seems more
%   interesting to add further techniques for showing that no actually
%   occurring model satisfies a violation condition.
%   It is possible that violation conditions are formally satisfiable,
%   but the corresponding models do not occur in the iteration for
%   computing the minimal model, and therefore the constraints are
%   actually satisfied.
%   Currently, we are trying to precompute information about occurring
%   states and state transitions.
%
%==============================================================================


%******************************************************************************
% Data of the Examples:
%******************************************************************************


%==============================================================================
% The Blink Example from the Paper (blink0):
%==============================================================================


%------------------------------------------------------------------------------
% blink0_rule(No, Head, BodyList):
%------------------------------------------------------------------------------

% Variables are encoded v(VarName). VarName should not end in a digit.

blink0_rule(1,
	call_pinMode(0,13,output),
	[]).
blink0_rule(2,
	turn_on(1),
	[]).
blink0_rule(3,
	delayed_turn_off(v('S'), v('From'), 1000),
		[turn_on(v('T')),
		ret_millis(v('T'), v('From')),
		succ(v('T'),v('S'))]).
blink0_rule(4,
	delayed_turn_off(v('S'),v('From'),v('Delay')),
		[delayed_turn_off(v('T'),v('From'),v('Delay')),
		ret_millis(v('T'),v('Now')),
		plus_lt(v('From'), v('Delay'), v('Now')),
		succ(v('T'),v('S'))]).
blink0_rule(5,
	turn_off(v('S')),
		[delayed_turn_off(v('T'),v('From'),v('Delay')),
		ret_millis(v('T'),v('Now')),
		plus_ge(v('From'), v('Delay'), v('Now')),
		succ(v('T'),v('S'))]).
blink0_rule(6,
	delayed_turn_on(v('S'),v('From'),1000),
		[turn_off(v('T')),
		ret_millis(v('T'),v('From')),
		succ(v('T'),v('S'))]).
blink0_rule(7,
	delayed_turn_on(v('S'),v('From'),v('Delay')),
		[delayed_turn_on(v('T'),v('From'),v('Delay')),
		ret_millis(v('T'),v('Now')),
		plus_lt(v('From'), v('Delay'), v('Now')),
		succ(v('T'),v('S'))]).
blink0_rule(8,
	turn_on(v('S')),
		[delayed_turn_on(v('T'),v('From'),v('Delay')),
		ret_millis(v('T'),v('Now')),
		plus_ge(v('From'),v('Delay'),v('Now')),
		succ(v('T'),v('S'))]).
blink0_rule(9,
	call_digitalWrite(v('T'), 13, high),
		[turn_on(v('T'))]).
blink0_rule(10,
	call_digitalWrite(v('T'), 13, low),
		[turn_off(v('T'))]).
blink0_rule(11,
	always(0),
	[]).
blink0_rule(12,
	always(v('S')),
		[always(v('T')),
		succ(v('T'),v('S'))]).
blink0_rule(13,
	call_millis(v('T')),
		[always(v('T'))]).

%------------------------------------------------------------------------------
% blink0_constraint(ID, Lit1, Lit2, Formula):
%------------------------------------------------------------------------------

% Variables are encoded v(VarName). VarName should not end in a digit.

blink0_constraint('A',
	call_digitalWrite(v('T'),v('Port'),v('ValX')),
	call_digitalWrite(v('T'),v('Port'),v('ValY')),
	ne(v('ValX'),v('ValY'))).

blink0_constraint('B',
	call_pinMode(v('T'),v('Port'),v('ModeX')),
	call_pinMode(v('T'),v('Port'),v('ModeY')),
	ne(v('ModeX'),v('ModeY'))).

blink0_constraint('C',
	turn_on(v('T')),
	turn_off(v('T')),
	true).

blink0_constraint('D',
	turn_on(v('T')),
	delayed_turn_off(v('T'),v('From'),v('Delay')),
	true).

blink0_constraint('E',
	turn_off(v('T')),
	delayed_turn_on(v('T'),v('From'),v('Delay')),
	true).

blink0_constraint('F',
	delayed_turn_on(v('T'),v('FromX'),v('DelayX')),
	delayed_turn_off(v('T'),v('FromY'),v('DelayY')),
	true).

blink0_constraint('G',
	turn_on(v('T')),
	delayed_turn_on(v('T'),v('From'),v('Delay')),
	true).

blink0_constraint('H',
	turn_off(v('T')),
	delayed_turn_off(v('T'),v('From'),v('Delay')),
	true).

blink0_constraint('I',
	delayed_turn_off(v('T'),v('FromX'),v('DelayX')),
	delayed_turn_off(v('T'),v('FromY'),v('DelayY')),
	or(ne(v('FromX'),v('FromY')), ne(v('DelayX'),v('DelayY')))).


blink0_constraint('J',
	delayed_turn_on(v('T'),v('FromX'),v('DelayX')),
	delayed_turn_on(v('T'),v('FromY'),v('DelayY')),
	or(ne(v('FromX'),v('FromY')), ne(v('DelayX'),v('DelayY')))).


%==============================================================================
% Another Version of a Blink Program which currently cannot be verified.
%==============================================================================

% This example is interesting.
% The difference is that turn_on becomes true in the same state
% that contains delayed_turn_on (when the time is reached).
% It needs more general constraints.
% We must specify that turn_on cannot be true at the same time with
% delayed_turn_on as long as the time of delayed_turn_on is not reached.
% We will work on permitting such constraints, too.
% The problem was found by the current implementation,
% so also a negative example like this one has some value.

%------------------------------------------------------------------------------
% blink1_rule(No, Head, BodyList):
%------------------------------------------------------------------------------

% Variables are encoded v(VarName). VarName should not end in a digit.

blink1_rule(1,
	call_pinMode(0,13,output),
	[]).
blink1_rule(2,
	turn_on(1),
	[]).
blink1_rule(3,
	delayed_turn_off(v('S'), v('From'), 1000),
		[turn_on(v('T')),
		ret_millis(v('T'), v('From')),
		succ(v('T'),v('S'))]).
blink1_rule(4,
	delayed_turn_off(v('S'),v('From'),v('Delay')),
		[delayed_turn_off(v('T'),v('From'),v('Delay')),
		ret_millis(v('T'),v('Now')),
		plus_lt(v('From'), v('Delay'), v('Now')),
		succ(v('T'),v('S'))]).
blink1_rule(5,
	turn_off(v('T')),
		[delayed_turn_off(v('T'),v('From'),v('Delay')),
		ret_millis(v('T'),v('Now')),
		plus_ge(v('From'), v('Delay'), v('Now'))]).
blink1_rule(6,
	delayed_turn_on(v('S'),v('From'),1000),
		[turn_off(v('T')),
		ret_millis(v('T'),v('From')),
		succ(v('T'),v('S'))]).
blink1_rule(7,
	delayed_turn_on(v('S'),v('From'),v('Delay')),
		[delayed_turn_on(v('T'),v('From'),v('Delay')),
		ret_millis(v('T'),v('Now')),
		plus_lt(v('From'), v('Delay'), v('Now')),
		succ(v('T'),v('S'))]).
blink1_rule(8,
	turn_on(v('T')),
		[delayed_turn_on(v('T'),v('From'),v('Delay')),
		ret_millis(v('T'),v('Now')),
		plus_ge(v('From'),v('Delay'),v('Now'))]).
blink1_rule(9,
	call_digitalWrite(v('T'), 13, high),
		[turn_on(v('T'))]).
blink1_rule(10,
	call_digitalWrite(v('T'), 13, low),
		[turn_off(v('T'))]).
blink1_rule(11,
	always(0),
	[]).
blink1_rule(12,
	always(v('S')),
		[always(v('T')),
		succ(v('T'),v('S'))]).
blink1_rule(13,
	call_millis(v('T')),
		[always(v('T'))]).

%------------------------------------------------------------------------------
% blink1_constraint(ID, Lit1, Lit2, Formula):
%------------------------------------------------------------------------------

% Variables are encoded v(VarName). VarName should not end in a digit.

blink1_constraint('A',
	call_digitalWrite(v('T'),v('Port'),v('ValX')),
	call_digitalWrite(v('T'),v('Port'),v('ValY')),
	ne(v('ValX'),v('ValY'))).

blink1_constraint('B',
	call_pinMode(v('T'),v('Port'),v('ModeX')),
	call_pinMode(v('T'),v('Port'),v('ModeY')),
	ne(v('ModeX'),v('ModeY'))).

blink1_constraint('C',
	turn_on(v('T')),
	turn_off(v('T')),
	true).

blink1_constraint('D',
	turn_on(v('T')),
	delayed_turn_off(v('T'),v('From'),v('Delay')),
	true).

blink1_constraint('E',
	turn_off(v('T')),
	delayed_turn_on(v('T'),v('From'),v('Delay')),
	true).

blink1_constraint('F',
	delayed_turn_on(v('T'),v('FromX'),v('DelayX')),
	delayed_turn_off(v('T'),v('FromY'),v('DelayY')),
	true).

blink1_constraint('G',
	delayed_turn_off(v('T'),v('FromX'),v('DelayX')),
	delayed_turn_off(v('T'),v('FromY'),v('DelayY')),
	or(ne(v('FromX'),v('FromY')), ne(v('DelayX'),v('DelayY')))).


blink1_constraint('H',
	delayed_turn_on(v('T'),v('FromX'),v('DelayX')),
	delayed_turn_on(v('T'),v('FromY'),v('DelayY')),
	or(ne(v('FromX'),v('FromY')), ne(v('DelayX'),v('DelayY')))).

blink1_constraint('I',
	ret_millis(v('T'),v('NowX')),
	ret_millis(v('T'),v('NowY')),
	ne(v('NowX'),v('NowY'))).


%******************************************************************************
% Some General Utility Predicates:
%******************************************************************************


%==============================================================================
% Definitions of Standard Predicates (to increase Portability):
%==============================================================================


%------------------------------------------------------------------------------
% list_append(+List1, +List2, -List12):
%------------------------------------------------------------------------------

% Some Prolog implementations have append, others not.
% To increase portability, we define our own version here:

list_append([], L, L).

list_append([E|R], L, [E|RL]) :-
	list_append(R, L, RL).

%------------------------------------------------------------------------------
% list_member(-Elem, +List):
%------------------------------------------------------------------------------

list_member(Elem, [Elem|_]).

list_member(Elem, [_|Rest]) :-
	list_member(Elem, Rest).

%------------------------------------------------------------------------------
% list_length(+List, -Length):
%------------------------------------------------------------------------------

list_length(List, Length) :-
	list_length_aux(List, 0, Length).

% list_length_aux(+List, -LengthIn, +LengthOut) - Tail Recursive Version:

list_length_aux([], Length, Length).

list_length_aux([_|Rest], LengthIn, LengthOut) :-
	Length is LengthIn + 1,
	list_length_aux(Rest, Length, LengthOut).

%------------------------------------------------------------------------------
% delete_all(+Pred, +Arity):
%------------------------------------------------------------------------------

% Delete all facts from dynamic database matching Head:

delete_all(Pred, Arity) :-
	functor(Head, Pred, Arity),
	retractall(Head).

% Note that in some Prologs it is called retract_all.


%==============================================================================
% File Interface:
%==============================================================================


%------------------------------------------------------------------------------
% file_ropen(+FileName, -Stream):
%------------------------------------------------------------------------------

% Open a file in read mode.
% open generates an exception in SWI Prolog if file does not exist.
% access_file checks the accessibility and fails if the file does not exist.

file_ropen(FileName, Stream) :-
	access_file(FileName, read),
	open(FileName, read, Stream).

%------------------------------------------------------------------------------
% file_close(+Stream):
%------------------------------------------------------------------------------

file_close(Stream) :-
	close(Stream).

%------------------------------------------------------------------------------
% file_lineno(+Stream, -LineNo):
%------------------------------------------------------------------------------

% This retuns the current line number in the file.

file_lineno(Stream, LineNo) :-
	line_count(Stream, LineNo).

%------------------------------------------------------------------------------
% file_eof(+Stream):
%------------------------------------------------------------------------------

% Is the current reading position in the file at the end of file?

file_eof(Stream) :-
	at_end_of_stream(Stream).

%------------------------------------------------------------------------------
% file_peekc(+Stream, -Char):
%------------------------------------------------------------------------------

% Have a look at the next character in the input stream, but do not read it.
% The character is returned as a one-character Prolog atom.

file_peekc(Stream, Char) :-
	peek_char(Stream, Char).

%------------------------------------------------------------------------------
% file_getc(+Stream, -Char):
%------------------------------------------------------------------------------

% Read the next character from the input stream.
% The character is returned as a one-character Prolog atom.

file_getc(Stream, Char) :-
	get_char(Stream, Char).


%==============================================================================
% Management of Options:
%==============================================================================


%------------------------------------------------------------------------------
% opt(+Opt):
%------------------------------------------------------------------------------

:- dynamic(opt/1).

%------------------------------------------------------------------------------
% opt_list(?OptChar, ?OptID, ?HelpText):
%------------------------------------------------------------------------------

opt_list('i', show_input_chars,  'Show input rules').
opt_list('t', show_input_tokens, 'Show input tokens').
opt_list('p', dbg_out_parser,    'Print debug output for parser').
opt_list('c', dbg_out_ccheck,    'Print debug output for consistency checker').
opt_list('r', dbg_out_rtry,      'Print debug output for each refutation try').

%------------------------------------------------------------------------------
% clear_opt: Reset all options back to normal.
%------------------------------------------------------------------------------

clear_opt :-
	delete_all(opt, 1).

%------------------------------------------------------------------------------
% set_opt(+Options): Set options by letter (several options in one atom).
%------------------------------------------------------------------------------

set_opt(Options) :-
	atom_chars(Options, OptionList),
	process_opt(OptionList, set).

%------------------------------------------------------------------------------
% del_opt(+Options): Unset options by letter (several options in one atom).
%------------------------------------------------------------------------------

del_opt(Options) :-
	atom_chars(Options, OptionList),
	process_opt(OptionList, del).

%------------------------------------------------------------------------------
% process_opt(+OptionList, +Mode):
%------------------------------------------------------------------------------

% Mode is set or del.

process_opt([], _).

process_opt([' '|MoreOptions], Mode) :-
	!,
	process_opt(MoreOptions, Mode).

process_opt([OptionChar|MoreOptions], Mode) :-
	decode_opt(OptionChar, OptionID),
	store_opt(OptionID, Mode),
	process_opt(MoreOptions, Mode).

%------------------------------------------------------------------------------
% decode_op(+OptionChar -OptionID):
%------------------------------------------------------------------------------

decode_opt(OptionChar, OptionID) :-
	opt_list(OptionChar, OptionID, _),
	!.

decode_opt(OptionChar, _) :-
	nl,
	write('Unknown Option: \''),
	write(OptionChar),
	write('\'.'),
	nl,
	fail.

%------------------------------------------------------------------------------
% store_opt(+OptionID, +Mode):
%------------------------------------------------------------------------------

store_opt(Option, set) :-
	opt(Option), % Already defined.
	!.

store_opt(Option, set) :-
	assert(opt(Option)),
	!.

store_opt(Option, del) :-
	opt(Option), % Defined, must be deleted.
	!,
	retract(opt(Option)).

store_opt(_, del). % Is not stored, nothing to do.

%------------------------------------------------------------------------------
% show_opt:
%------------------------------------------------------------------------------

show_opt :-
	write('Possible Options '),
	write('(+ marks currently set options, - options that are not set):'),
	nl,
	opt_list(OptChar, OptID, HelpText), % Backtracks over all options
	write('    '),
	write(OptChar),
	show_opt_status(OptID),
	write(': '),
	write(HelpText),
	nl,
	fail.

show_opt.

% show_opt_status(+OptID):

show_opt_status(OptID) :-
	opt(OptID),
	!,
	write('+').

show_opt_status(_) :-
	write('-').

%------------------------------------------------------------------------------
% opt_dcc: Is the debug output for consistency checks enabled?
%------------------------------------------------------------------------------

opt_dcc :-
	opt(dbg_out_ccheck).

%------------------------------------------------------------------------------
% opt_drt: Is the debug output for refutation tries enabled?
%------------------------------------------------------------------------------

opt_drt :-
	opt(dbg_out_rtry).


%******************************************************************************
% TYPES:
%******************************************************************************

% Each type T has a predicate is_T to check whether a Prolog term satisfies
% the structural constraints of type T
% and a predicate print_T to show a value of type T on standard output.

% Currently, basically no type checking is done
% (only in the make_T predicates which import data into the internal format).
% I am planning to add type asserstions with the is_T predicates
% to do at least runtime type checking (with the possibility to switch it off
% for increased performance).

% However, the types are helpful to understand the program structure
% and they are an abstraction layer over the Prolog data structures.
% When the types are used later, the internal functors should not be used,
% only the official interface predicates defined in this "Types" section.

% The print_T predicates usually fail if the value should not be of type T.


%==============================================================================
% Type "Chars" (List of One-Character Atoms):
%==============================================================================


%------------------------------------------------------------------------------
% is_chars(+Chars):
%------------------------------------------------------------------------------

is_chars([]).

is_chars([Char|Chars]) :-
	atom(Char), % Maybe I should check that only one character.
	is_chars(Chars).

%------------------------------------------------------------------------------
% print_chars(+Chars):
%------------------------------------------------------------------------------

% Print list of characters (encoded as one-character Prolog atoms).

print_chars([]).

print_chars([Char|Rest]) :-
	put_char(Char),
	print_chars(Rest).


%==============================================================================
% Type "Const" (Constants in Terms):
%==============================================================================


%------------------------------------------------------------------------------
% is_const(+Term):
%------------------------------------------------------------------------------

is_const(Term) :-
	atomic(Term).

is_const(str(Chars)) :-
	is_chars(Chars).

is_const(cconst(Name)) :-
	atom(Name).

%------------------------------------------------------------------------------
% print_const(+Const):
%------------------------------------------------------------------------------

print_const(cconst(Name)) :-
	!,
	write('#'),
	write(Name).

print_const(str(Chars)) :-
	!,
	write('\''),
	print_chars(Chars),
	write('\'').

print_const(Const) :-
	is_const(Const),
	write(Const).

%------------------------------------------------------------------------------
% const_number(+Const, -Number):
%------------------------------------------------------------------------------

% This can also be called for constants that are not numbers,
% then it should fail.

const_number(Const, Const) :-
	number(Const).


%==============================================================================
% Type "Var" (Variables in Terms):
%==============================================================================


%------------------------------------------------------------------------------
% is_var(+Term):
%------------------------------------------------------------------------------

is_var(v(_)).

is_var(v(_,_)).

%------------------------------------------------------------------------------
% print_var(+Var):
%------------------------------------------------------------------------------

print_var(v(VarName)) :-
	write(VarName).

print_var(v(VarName,No)) :-
	write(VarName),
	write('_'),
	write(No).


%==============================================================================
% Type "Term" (Terms Formulas and Rules):
%==============================================================================

% Terms in Datalog are Constants or Variables.

%------------------------------------------------------------------------------
% is_term(+Term):
%------------------------------------------------------------------------------

is_term(Term) :-
	is_const(Term).

is_term(Term) :-
	is_var(Term).

%------------------------------------------------------------------------------
% print_term(+Term):
%------------------------------------------------------------------------------

print_term(Var) :-
	is_var(Var),
	!,
	print_var(Var).

print_term(Const) :-
	is_const(Const),
	!,
	print_const(Const).


%==============================================================================
% Type "Pred" (Predicates that can be used in Rules):
%==============================================================================


%------------------------------------------------------------------------------
% is_pred(+Pred):
%------------------------------------------------------------------------------

is_pred(Pred) :-
	atom(Pred).

%------------------------------------------------------------------------------
% print_pred(+Pred):
%------------------------------------------------------------------------------

print_pred(Pred) :-
	write(Pred).

%------------------------------------------------------------------------------
% is_return_pred(+Pred):
%------------------------------------------------------------------------------

% TODO: This is simplified, only what is used in the example.

is_return_pred(ret_millis).


%==============================================================================
% Type "Atomic Formula" (with Comparison Operator or Built-In Predicate):
%==============================================================================


% This means only comparisons and built-in predicate calls
% that can occur in "Formulas",
% not the standard Datalog literals.

%------------------------------------------------------------------------------
% is_atomic_formula(+Formula):
%------------------------------------------------------------------------------

is_atomic_formula(true).
is_atomic_formula(false).
is_atomic_formula(eq(_,_)).
is_atomic_formula(ne(_,_)).
is_atomic_formula(lt(_,_)).
is_atomic_formula(le(_,_)).
is_atomic_formula(gt(_,_)).
is_atomic_formula(ge(_,_)).
is_atomic_formula(plus_lt(_,_,_)).
is_atomic_formula(plus_ge(_,_,_)).
is_atomic_formula(succ(_,_)).
is_atomic_formula(not_succ(_,_)).
is_atomic_formula(ret_millis(_,_)).
is_atomic_formula(not_ret_millis(_,_)).

%------------------------------------------------------------------------------
% complement_atomic_formula(+FormulaIn, -FormulaOut):
%------------------------------------------------------------------------------

complement_atomic_formula(true, false).
complement_atomic_formula(false, true).
complement_atomic_formula(eq(Term1,Term2), ne(Term1,Term2)).
complement_atomic_formula(ne(Term1,Term2), eq(Term1,Term2)).
complement_atomic_formula(lt(Term1,Term2), ge(Term1,Term2)).
complement_atomic_formula(le(Term1,Term2), gt(Term1,Term2)).
complement_atomic_formula(gt(Term1,Term2), le(Term1,Term2)).
complement_atomic_formula(ge(Term1,Term2), lt(Term1,Term2)).
complement_atomic_formula(plus_lt(T1,T2,T3), plus_ge(T1,T2,T3)).
complement_atomic_formula(plus_ge(T1,T2,T3), plus_lt(T1,T2,T3)).
complement_atomic_formula(succ(Term1,Term2), not_succ(Term1,Term2)).
complement_atomic_formula(not_succ(Term1,Term2), succ(Term1,Term2)).
complement_atomic_formula(ret_millis(Term1,Term2), not_ret_millis(Term1,Term2)).
complement_atomic_formula(not_ret_millis(Term1,Term2), ret_millis(Term1,Term2)).


%------------------------------------------------------------------------------
% print_atomic_formula(+Formula):
%------------------------------------------------------------------------------

print_atomic_formula(true) :-
	write('true').

print_atomic_formula(false) :-
	write('false').

print_atomic_formula(ne(Term1,Term2)) :-
	print_term(Term1),
	write('!='),
	print_term(Term2).

print_atomic_formula(eq(Term1,Term2)) :-
	print_term(Term1),
	write('='),
	print_term(Term2).

print_atomic_formula(lt(Term1,Term2)) :-
	print_term(Term1),
	write('<'),
	print_term(Term2).

print_atomic_formula(le(Term1,Term2)) :-
	print_term(Term1),
	write('<='),
	print_term(Term2).

print_atomic_formula(gt(Term1,Term2)) :-
	print_term(Term1),
	write('>'),
	print_term(Term2).

print_atomic_formula(ge(Term1,Term2)) :-
	print_term(Term1),
	write('>='),
	print_term(Term2).

print_atomic_formula(plus_lt(Term1,Term2,Term3)) :-
	print_term(Term1),
	write('+'),
	print_term(Term2),
	write('<'),
	print_term(Term3).

print_atomic_formula(plus_ge(Term1,Term2,Term3)) :-
	print_term(Term1),
	write('+'),
	print_term(Term2),
	write('>='),
	print_term(Term3).

print_atomic_formula(succ(Term1,Term2)) :-
	write('succ('),
	print_term(Term1),
	write(','),
	print_term(Term2),
	write(')').

print_atomic_formula(not_succ(Term1,Term2)) :-
	write('not_succ('),
	print_term(Term1),
	write(','),
	print_term(Term2),
	write(')').

print_atomic_formula(ret_millis(Term1,Term2)) :-
	write('ret_millis('),
	print_term(Term1),
	write(','),
	print_term(Term2),
	write(')').

print_atomic_formula(not_ret_millis(Term1,Term2)) :-
	write('not_ret_millis('),
	print_term(Term1),
	write(','),
	print_term(Term2),
	write(')').

%------------------------------------------------------------------------------
% eval_obvious_atomic(+AtomicFormula):
%------------------------------------------------------------------------------

% This predicate replaces atomic formulas with obvious truth values
% by true or false.
% If the truth value cannot be determined, the formula is left unchanged.
% This is only part of an optional simplification of the formula,
% so it is not absolutely essential to catch all cases.

% The logical constants cannot be further simplified:

eval_obvious_atomic(true, true) :-
	!.

eval_obvious_atomic(false, false) :-
	!.

% eq(Term1, Term2):

eval_obvious_atomic(eq(Term,Term), true) :-
	!.

eval_obvious_atomic(eq(Const1,Const2), false) :-
	is_const(Const1),
	is_const(Const2),
	Const1 \= Const2,
	!.

eval_obvious_atomic(eq(Term1,Term2), eq(Term1,Term2)) :-
	!.

% ne(Term1, Term2):

eval_obvious_atomic(ne(Term,Term), false) :-
	!.

eval_obvious_atomic(ne(Const1,Const2), true) :-
	is_const(Const1),
	is_const(Const2),
	Const1 \= Const2,
	!.

eval_obvious_atomic(ne(Term1,Term2), ne(Term1,Term2)) :-
	!.

% lt(Term1, Term2):

eval_obvious_atomic(lt(Term,Term), false) :-
	!.

eval_obvious_atomic(lt(Const1,Const2), true) :-
	is_const(Const1),
	is_const(Const2),
	const_number(Const1, Num1),
	const_number(Const2, Num2),
	Num1 < Num2,
	!.

eval_obvious_atomic(lt(Const1,Const2), false) :-
	is_const(Const1),
	is_const(Const2),
	const_number(Const1, Num1),
	const_number(Const2, Num2),
	Num1 >= Num2,
	!.

eval_obvious_atomic(lt(Term1,Term2), lt(Term1,Term2)) :-
	!.

% le(Term1, Term2):

eval_obvious_atomic(le(Term,Term), true) :-
	!.

eval_obvious_atomic(le(Const1,Const2), true) :-
	is_const(Const1),
	is_const(Const2),
	const_number(Const1, Num1),
	const_number(Const2, Num2),
	Num1 =< Num2,
	!.

eval_obvious_atomic(le(Const1,Const2), false) :-
	is_const(Const1),
	is_const(Const2),
	const_number(Const1, Num1),
	const_number(Const2, Num2),
	Num1 > Num2,
	!.

eval_obvious_atomic(le(Term1,Term2), le(Term1,Term2)) :-
	!.

% gt(Term1, Term2):

eval_obvious_atomic(gt(Term,Term), false) :-
	!.

eval_obvious_atomic(gt(Const1,Const2), true) :-
	is_const(Const1),
	is_const(Const2),
	const_number(Const1, Num1),
	const_number(Const2, Num2),
	Num1 > Num2,
	!.

eval_obvious_atomic(gt(Const1,Const2), false) :-
	is_const(Const1),
	is_const(Const2),
	const_number(Const1, Num1),
	const_number(Const2, Num2),
	Num1 =< Num2,
	!.

eval_obvious_atomic(gt(Term1,Term2), gt(Term1,Term2)) :-
	!.

% ge(Term1, Term2):

eval_obvious_atomic(ge(Term,Term), true) :-
	!.

eval_obvious_atomic(ge(Const1,Const2), true) :-
	is_const(Const1),
	is_const(Const2),
	const_number(Const1, Num1),
	const_number(Const2, Num2),
	Num1 >= Num2,
	!.

eval_obvious_atomic(ge(Const1,Const2), false) :-
	is_const(Const1),
	is_const(Const2),
	const_number(Const1, Num1),
	const_number(Const2, Num2),
	Num1 < Num2,
	!.

eval_obvious_atomic(ge(Term1,Term2), ge(Term1,Term2)) :-
	!.

% succ(Term1, Term2):

eval_obvious_atomic(succ(Term,Term), false) :-
	!.

eval_obvious_atomic(succ(_Term,0), false) :-
	!.

eval_obvious_atomic(succ(0,1), true) :-
	!.

eval_obvious_atomic(succ(Term1,Term2), succ(Term1,Term2)) :-
	!.

% not_succ(Term1, Term2):

eval_obvious_atomic(not_succ(Term,Term), true) :-
	!.

eval_obvious_atomic(not_succ(_Term,0), true) :-
	!.

eval_obvious_atomic(not_succ(0,1), false) :-
	!.

eval_obvious_atomic(not_succ(Term1,Term2), not_succ(Term1,Term2)) :-
	!.

% TODO: Cound do more here:

eval_obvious_atomic(plus_lt(T1,T2,T3), plus_lt(T1,T2,T3)) :-
	!.

eval_obvious_atomic(plus_ge(T1,T2,T3), plus_ge(T1,T2,T3)) :-
	!.

% ret_millis(Term1,Term2):

eval_obvious_atomic(ret_millis(0,_), false) :-
	!.

eval_obvious_atomic(ret_millis(Term1,Term2), ret_millis(Term1,Term2)) :-
	!.

% not_ret_millis(Term1,Term2):

eval_obvious_atomic(not_ret_millis(0,_), true) :-
	!.

eval_obvious_atomic(not_ret_millis(Term1,Term2), not_ret_millis(Term1,Term2)) :-
	!.

% We should be informed if we forgot a new kind of atomic formula:

eval_obvious_atomic(F1, F1) :-
	nl,
	write('***** eval_obvious_atomic: Unhandled Formula: '),
	write(F1),
	nl.


%==============================================================================
% Type "Formula" (and/or/nor-connection of Comparisons or Built-In Literals):
%==============================================================================


% Only comparisons and built-in predicate calls can occur in "Formulas",
% not the standard Datalog literals.

%------------------------------------------------------------------------------
% is_formula(+Formula):
%------------------------------------------------------------------------------

is_formula(Formula) :-
	is_atomic_formula(Formula),
	!.

is_formula(and(Formula1,Formula2)) :-
	!,
	is_formula(Formula1),
	is_formula(Formula2).

is_formula(or(Formula1,Formula2)) :-
	!,
	is_formula(Formula1),
	is_formula(Formula2).

is_formula(not(Formula1)) :-
	!,
	is_formula(Formula1).

%------------------------------------------------------------------------------
% print_formula(+Formula):
%------------------------------------------------------------------------------

print_formula(Formula) :-
	print_formula_not(Formula).

% The suffix indicates the priority that can be printed without (...).

% print_formula_atomic(+Formula):

print_formula_atomic(Formula) :-
	is_atomic_formula(Formula),
	!,
	print_atomic_formula(Formula).

print_formula_atomic(Formula) :-
	write('('),
	print_formula_or(Formula),
	write(')').

% We treat "and" and "or" as right-associative (fits better with lists).
% I.e. "p1 and p2 and p3" is and(p1, and(p2, p3)).

% print_formula_or(+Formula):

print_formula_or(or(Formula1,Formula2)) :-
	!,
	print_formula_and(Formula1),
	write(' | '),
	print_formula_or(Formula2).

print_formula_or(Formula) :-
	print_formula_and(Formula).

% print_formula_and(+Formula):

print_formula_and(and(Formula1,Formula2)) :-
	!,
	print_formula_not(Formula1),
	write(' & '),
	print_formula_and(Formula2).

print_formula_and(Formula) :-
	print_formula_not(Formula).

% print_formula_not(+Formula):

print_formula_not(not(Formula)) :-
	!,
	write('! '),
	print_formula_not(Formula).

print_formula_not(Formula) :-
	print_formula_atomic(Formula).

%------------------------------------------------------------------------------
% simplify_formula(+FormulaIn, -FormulaOut):
%------------------------------------------------------------------------------

% unused?
simplify_formula(FormulaIn, FormulaOut) :-
	eval_obvious(FormulaIn, FormulaOut).

%------------------------------------------------------------------------------
% eval_obvious(+FormulaIn, -FormulaOut):
%------------------------------------------------------------------------------

eval_obvious(FormulaIn, FormulaOut) :-
	is_atomic_formula(FormulaIn),
	!,
	eval_obvious_atomic(FormulaIn, FormulaOut).

eval_obvious(and(FIn1,FIn2), FOut) :-
	!,
	eval_obvious(FIn1, F1),
	eval_obvious(FIn2, F2),
	eval_obvious_and(F1, F2, FOut).

eval_obvious(or(FIn1,FIn2), FOut) :-
	!,
	eval_obvious(FIn1, F1),
	eval_obvious(FIn2, F2),
	eval_obvious_or(F1, F2, FOut).

eval_obvious(not(FIn1), FOut) :-
	!,
	eval_obvious(FIn1, F1),
	eval_obvious_not(F1, FOut).

eval_obvious(F1, F1) :-
	nl,
	write('***** eval_obvious: Unhandled Formula: '),
	write(F1),
	nl.

% eval_obvious_and(+F1, +F2, -F):

eval_obvious_and(true, F, F) :-
	!.

eval_obvious_and(false, _F, false) :-
	!.

eval_obvious_and(F, true, F) :-
	!.

eval_obvious_and(_F, false, false) :-
	!.

eval_obvious_and(F1, F2, and(F1,F2)).

% eval_obvious_or(+F1, +F2, -F):

eval_obvious_or(true, _F, true) :-
	!.

eval_obvious_or(false, F, F) :-
	!.

eval_obvious_or(_F, true, true) :-
	!.

eval_obvious_or(F, false, F) :-
	!.

eval_obvious_or(F1, F2, or(F1,F2)).

% eval_obvious_not(+F1, -F):

eval_obvious_not(true, false) :-
	!.

eval_obvious_not(false, true) :-
	!.

eval_obvious_not(F1, not(F1)).

%------------------------------------------------------------------------------
% normalize_and(+FormulaIn, -FormulaOut):
%------------------------------------------------------------------------------

% Make and-trees right-deep (corresponding to list).
% Note that we cannot use and_to_conj and conj_to_and,
% because the formulas might contain or and not.
% Here, we look only at the top part of the tree consisting of and.
% Subtrees with other operators are left untouched.

normalize_and(FormulaIn, FormulaOut) :-
	and_to_list(FormulaIn, List),
	list_to_and(List, FormulaOut).

% list_to_and(+List, -Formula):

list_to_and([Fo], Fo) :-
	!.

list_to_and([Fo1|Rest], and(Fo1,FoRest)) :-
	list_to_and(Rest, FoRest).

% and_to_list(+FormulaIn, -FormulaList):

and_to_list(and(Fo1, Fo2), List) :-
	!,
	and_to_list(Fo1, List1),
	and_to_list(Fo2, List2),
	list_append(List1, List2, List).

and_to_list(Fo, [Fo]).


%==============================================================================
% Type "Conj" (Conjunction as List of Atomic Formulas with Builtin Literals):
%==============================================================================

% The type "Conj" is a list of atomic formulas with built-in literals,
% especially
% false,
% true,
% eq(Term1,Term2),
% ne(Term1,Term2),
% succ(Term1,Term2),
% plus_lt(Term1,Term2,Term3),
% plus_ge(Term1,Term2,Term3).
% This type is the input to the consistency checker.

% In contrast, "Body" is also a list of (positive) literals (atomic formulas),
% but it includes literals with user-defined predicates.

%------------------------------------------------------------------------------
% is_conj(+Conj):
%------------------------------------------------------------------------------

is_conj([]).

is_conj([AtomicFormula|Rest]) :-
	is_atomic_formula(AtomicFormula),
	is_conj(Rest).

%------------------------------------------------------------------------------
% print_conj(+ListOfAtomicFormulas):
%------------------------------------------------------------------------------

% print_conj(+Conj):

print_conj([]) :-
	write('true').

print_conj([AtomicFormula|Rest]) :-
	is_atomic_formula(AtomicFormula),
	print_formula(AtomicFormula),
	print_conj_rest(Rest).

% print_conj_rest(+Conj):

print_conj_rest([]).

print_conj_rest([AtomicFormula|Rest]) :-
	write(', '),
	is_atomic_formula(AtomicFormula),
	print_formula(AtomicFormula),
	print_conj_rest(Rest).

%------------------------------------------------------------------------------
% print_conj_prover(+ListOfAtomicFormulas):
%------------------------------------------------------------------------------

% This is used for printing the derived atomic formulas of the prover.
% We print in inverse order, and one formula per line, doubly indented.

print_conj_prover([]).

print_conj_prover([AtomicFormula|Rest]) :-
	print_conj_prover(Rest),
	write('\t\t'),
	print_atomic_formula(AtomicFormula),
	nl.

%------------------------------------------------------------------------------
% conj_length(+ListOfAtomicFormulas, -Length):
%------------------------------------------------------------------------------

conj_length(Conj, Length) :-
	list_length(Conj, Length).

%------------------------------------------------------------------------------
% conj_contains_false(+Conj):
%------------------------------------------------------------------------------

% Check whether Conj contains false as a member (surely inconsistent).

conj_contains_false([false|_]) :-
	!.

conj_contains_false([_|Rest]) :-
	conj_contains_false(Rest).

%------------------------------------------------------------------------------
% conj_to_and(+List, -Formula):
%------------------------------------------------------------------------------

conj_to_and([], true).

conj_to_and([Fo], Fo) :-
	!.

conj_to_and([Fo1|Rest], and(Fo1,FoRest)) :-
	conj_to_and(Rest, FoRest).

%------------------------------------------------------------------------------
% and_to_conj(+FormulaIn, -FormulaList):
%------------------------------------------------------------------------------

% unused?

and_to_conj(and(Fo1, Fo2), List) :-
	!,
	and_to_conj(Fo1, List1),
	and_to_conj(Fo2, List2),
	list_append(List1, List2, List).

and_to_conj(Fo, [Fo]) :-
	is_atomic_formula(Fo).


%==============================================================================
% Type "DNF" (List of Conj-Lists interpreted as Disjunction of Conjunctions):
%==============================================================================


%------------------------------------------------------------------------------
% is_dnf(+DNF):
%------------------------------------------------------------------------------

is_dnf([]).

is_dnf([Conj|Rest]) :-
	is_conj(Conj),
	is_dnf(Rest).

%------------------------------------------------------------------------------
% print_dnf(+DNF):
%------------------------------------------------------------------------------

print_dnf([]) :-
	write('false').

print_dnf([Conj|Rest]) :-
	print_conj(Conj),
	print_dnf_rest(Rest).

% print_dnf_rest(+DNF):

print_dnf_rest([]).

print_dnf_rest([Conj|Rest]) :-
	write(' | '),
	print_conj(Conj),
	print_dnf_rest(Rest).

%------------------------------------------------------------------------------
% eliminate_not(+FormulaIn, -FormulaOut):
%------------------------------------------------------------------------------

% This is part of the translation of a formula to DNF.

eliminate_not(and(FIn1,FIn2), and(FOut1,FOut2)) :-
	!,
	eliminate_not(FIn1, FOut1),
	eliminate_not(FIn2, FOut2).

eliminate_not(or(FIn1,FIn2), or(FOut1,FOut2)) :-
	!,
	eliminate_not(FIn1, FOut1),
	eliminate_not(FIn2, FOut2).

eliminate_not(not(FIn1), FOut1) :-
	!,
	eliminate_not_negated(FIn1, FOut1).

eliminate_not(AtomicFormula, AtomicFormula) :-
	is_atomic_formula(AtomicFormula).

% eliminate_not_negated(+FormulaIn, -FormulaOut):

eliminate_not_negated(and(FIn1,FIn2), or(FOut1,FOut2)) :-
	!,
	eliminate_not_negated(FIn1, FOut1),
	eliminate_not_negated(FIn2, FOut2).

eliminate_not_negated(or(FIn1,FIn2), and(FOut1,FOut2)) :-
	!,
	eliminate_not_negated(FIn1, FOut1),
	eliminate_not_negated(FIn2, FOut2).

eliminate_not_negated(not(FIn1), FOut1) :-
	!,
	eliminate_not(FIn1, FOut1).

eliminate_not_negated(FIn, FOut) :-
	is_atomic_formula(FIn),
	complement_atomic_formula(FIn, FOut).

%------------------------------------------------------------------------------
% dnf(+FormulaIn, -DNF):
%------------------------------------------------------------------------------

% The input to DNF computation is a formula without negation.
% The output is a list of lists of atomic formulas.
% The inner lists are conjunctions, the outer one corresonds to a disjunction.

dnf(false, []) :-
	!.

dnf(true, [[]]) :-
	!.

dnf(AtomicFormula, [[AtomicFormula]]) :-
	is_atomic_formula(AtomicFormula).

dnf(and(F1,F2), DNF) :-
	dnf(F1, DNF1),
	dnf(F2, DNF2),
	dnf_multiply(DNF1, DNF2, DNF).

dnf(or(F1,F2), DNF) :-
	dnf(F1, DNF1),
	dnf(F2, DNF2),
	list_append(DNF1, DNF2, DNF).

% dnf_multiply(+DNFIn1, +DNFIn2, -DNFOut):

dnf_multiply([Conj1|Rest1], DNFIn2, DNFOut) :-
	dnf_and_all(Conj1, DNFIn2, DNFOut1),
	dnf_multiply(Rest1, DNFIn2, DNFOut2),
	list_append(DNFOut1, DNFOut2, DNFOut).

dnf_multiply([], _, []).

% dnf_and_all(+Conj, +DNFIn, -DNFOut):

dnf_and_all(_, [], []) :-
	!.

dnf_and_all(Conj1, [Conj2|Rest2], [ConjOut|RestOut]) :-
	list_append(Conj1, Conj2, ConjOut),
	dnf_and_all(Conj1, Rest2, RestOut).


%==============================================================================
% Type "Args" (List of Terms):
%==============================================================================


%------------------------------------------------------------------------------
% is_args(+Args):
%------------------------------------------------------------------------------

is_args([]).

is_args([Term|Args]) :-
	is_term(Term),
	is_args(Args).


%------------------------------------------------------------------------------
% print_args(+Args):
%------------------------------------------------------------------------------

print_args([]).

print_args([Arg|Rest]) :-
	write('('),
	print_term(Arg),
	print_args_rest(Rest),
	write(')').

% print_args_rest(+Args):

print_args_rest([]).

print_args_rest([Arg|Rest]) :-
	write(', '),
	print_term(Arg),
	print_args_rest(Rest).


%==============================================================================
% Type "Lit" (Literal in Rules):
%==============================================================================


%------------------------------------------------------------------------------
% is_lit(+Lit):
%------------------------------------------------------------------------------

is_lit(Lit) :-
	Lit =.. [Pred|Args],
	is_pred(Pred),
	is_args(Args).

%------------------------------------------------------------------------------
% print_lit(+Lit):
%------------------------------------------------------------------------------

% TODO: Introduce Type for Lits with Builtin Preds!

print_lit(plus_lt(X,Y,Z)) :-
	!,
	print_term(X),
	write(' + '),
	print_term(Y),
	write(' < '),
	print_term(Z).

print_lit(plus_ge(X,Y,Z)) :-
	!,
	print_term(X),
	write(' + '),
	print_term(Y),
	write(' >= '),
	print_term(Z).

print_lit(Lit) :-
	Lit =.. [Pred|Terms],
	print_pred(Pred),
	print_args(Terms).

%------------------------------------------------------------------------------
% lit_statearg(+Lit, -Arg):
%------------------------------------------------------------------------------

% ?unused

% The state/time argument is the first argument of standard literals.

lit_statearg(Lit, Arg) :-
	Lit =.. [_Pred, Arg|_].

% TODO: Check that Pred is not a built-in Predicate.


%------------------------------------------------------------------------------
% lit_pred(+Lit, -Pred):
%------------------------------------------------------------------------------

lit_pred(Lit, Pred) :-
	Lit =.. [Pred|_].

%==============================================================================
% Type "LitList" (List of Literals, e.g. Rule Body):
%==============================================================================


%------------------------------------------------------------------------------
% is_litlist(+LitList):
%------------------------------------------------------------------------------

is_litlist([]).

is_litlist([Lit|LitList]) :-
	is_lit(Lit),
	is_litlist(LitList).

%------------------------------------------------------------------------------
% print_litlist(+LitList):
%------------------------------------------------------------------------------

% One literal (indented by a TAB) is printed per line.

print_litlist([]).

print_litlist([Lit|Rest]) :-
	write('\t'),
	print_lit(Lit),
	print_litlist_rest(Rest).

% print_litlist_rest(+LitList):

print_litlist_rest([]).

print_litlist_rest([Lit|Rest]) :-
	write(', '),
	nl,
	write('\t'),
	print_lit(Lit),
	print_litlist_rest(Rest).


%==============================================================================
% Type "RID" (Rule Identifier):
%==============================================================================

% Typical rule identifiers are 1, 2, 3.

%------------------------------------------------------------------------------
% is_rid(+RID):
%------------------------------------------------------------------------------

is_rid(RID) :-
	integer(RID),
	RID > 0.

%------------------------------------------------------------------------------
% print_rid(+RID):
%------------------------------------------------------------------------------

print_rid(RID) :-
	write('('),
	write(RID),
	write(')').

%------------------------------------------------------------------------------
% make_rid(+No, -RID):
%------------------------------------------------------------------------------

make_rid(No, No) :-
	integer(No),
	No >= 1.


%==============================================================================
% Type "Rule":
%==============================================================================


%------------------------------------------------------------------------------
% is_rule(+Rule):
%------------------------------------------------------------------------------

is_rule(rule(No, Head, Body)) :-
	is_rid(No),
	is_lit(Head),
	is_litlist(Body).

% TODO: Should check that head does not contain built-in predicate!

%------------------------------------------------------------------------------
% print_rule(+Rule):
%------------------------------------------------------------------------------

print_rule(rule(No, Head, Body)) :-
	print_rid(No),
	write(' '),
	print_lit(Head),
	print_rule_body(Body),
	write('.'),
	nl.

% print_rule_body(+LitList): Handles facts specially (empty body).

print_rule_body([]).

print_rule_body([Lit|Rest]) :-
	write(' :- '),
	nl,
	print_litlist([Lit|Rest]).

%------------------------------------------------------------------------------
% rule_data(+Rule, -No, -Head, -Body):
%------------------------------------------------------------------------------

rule_data(rule(No, Head, Body), No, Head, Body).

%------------------------------------------------------------------------------
% make_rule(+No, +Head, +Body, -Rule):
%------------------------------------------------------------------------------

make_rule(No, Head, Body, rule(No, Head, Body)) :-
	is_rid(No),
	is_lit(Head),
	is_litlist(Body).


%==============================================================================
% Type "CID" (Constraint Identifier):
%==============================================================================

% Typical constraint identifiers are 'A', 'B', 'C'.

%------------------------------------------------------------------------------
% is_cid(+CID):
%------------------------------------------------------------------------------

is_cid(CID) :-
	atom(CID).

%------------------------------------------------------------------------------
% print_cid(+CID):
%------------------------------------------------------------------------------

print_cid(CID) :-
	write('('),
	write(CID),
	write(')').

%------------------------------------------------------------------------------
% make_cid(+No, -CID):
%------------------------------------------------------------------------------

make_cid(No, CID) :-
	integer(No),
	No >= 1,
	make_cid_cases(No, CID).

% make_cid_cases(+No, -CID):

make_cid_cases(No, CID) :-
	make_cid_letter(No, CID),
	!.

make_cid_cases(No, CID) :-
	number_chars(No, Chars),
	atom_chars(CID, ['C'|Chars]).

% make_cid_letter(+No, -CID):

make_cid_letter( 1, 'A').
make_cid_letter( 2, 'B').
make_cid_letter( 3, 'C').
make_cid_letter( 4, 'D').
make_cid_letter( 5, 'E').
make_cid_letter( 6, 'F').
make_cid_letter( 7, 'G').
make_cid_letter( 8, 'H').
make_cid_letter( 9, 'I').
make_cid_letter(10, 'J').
make_cid_letter(11, 'K').
make_cid_letter(12, 'L').
make_cid_letter(13, 'M').
make_cid_letter(14, 'N').
make_cid_letter(15, 'O').
make_cid_letter(16, 'P').
make_cid_letter(17, 'Q').
make_cid_letter(18, 'R').
make_cid_letter(19, 'S').
make_cid_letter(20, 'T').
make_cid_letter(21, 'U').
make_cid_letter(22, 'V').
make_cid_letter(23, 'W').
make_cid_letter(24, 'X').
make_cid_letter(25, 'Y').
make_cid_letter(26, 'Z').

%==============================================================================
% Type "Constraint":
%==============================================================================

% These are the generalized exclusion constraints from our paper.
% They have the form <- Lit1, Lit2, Formula
% where Formula is either true or a disjunction of disequations Term1 <> Term2
% between a term from Lit1 and a Term from Lit2.

%------------------------------------------------------------------------------
% is_constraint(+Constraint):
%------------------------------------------------------------------------------

is_constraint(constraint(ID, Lit1, Lit2, Formula)) :-
	is_cid(ID),
	is_lit(Lit1),
	is_lit(Lit2),
	is_formula(Formula).

% TODO: Should check that Lit1 and Lit2 have no built-in predicate.

%------------------------------------------------------------------------------
% print_constraint(+Constraint):
%------------------------------------------------------------------------------

print_constraint(constraint(ID, Lit1, Lit2, Formula)) :-
	print_cid(ID),
	write(' '),
	write('<- '),
	print_lit(Lit1),
	write(', '),
	print_lit(Lit2),
	print_opt_formula(Formula),
	write('.'),
	nl.

% print_opt_formula(+Formula):

print_opt_formula(true) :-
	!.

print_opt_formula(Formula) :-
	write(','),
	nl,
	write('       '),
	print_formula(Formula).

%------------------------------------------------------------------------------
% constraint_data(+Constraint, -ID, -Lit1, -Lit2, -Formula):
%------------------------------------------------------------------------------

constraint_data(constraint(ID,Lit1,Lit2,Formula), ID, Lit1, Lit2, Formula).


%------------------------------------------------------------------------------
% make_constraint(+ID, +Lit1, +Lit2, +Formula, +Constraint):
%------------------------------------------------------------------------------

make_constraint(ID, Lit1, Lit2, Formula, constraint(ID,Lit1,Lit2,Formula)) :-
	is_cid(ID),
	is_lit(Lit1),
	is_lit(Lit2),
	is_formula(Formula).


%==============================================================================
% Type "IDGen" (Generator for Rule and Constraint IDs):
%==============================================================================

% idgen(RNo,CNo) contains the number of rules and the number of constraints
% read so far.

%------------------------------------------------------------------------------
% is_idgen(+IDGen):
%------------------------------------------------------------------------------

is_idgen(idgen(RNo,CNo)) :-
	integer(RNo),
	RNo >= 0,
	integer(CNo),
	CNo >= 0.

%------------------------------------------------------------------------------
% print_idgen(+IDGen):
%------------------------------------------------------------------------------

print_idgen(idgen(RNo,CNo)) :-
	write('IDGen('),
	write(RNo),
	write(','),
	write(CNo),
	write(')').

%------------------------------------------------------------------------------
% idgen_init(-IDGen):
%------------------------------------------------------------------------------

idgen_init(idgen(0,0)).

%------------------------------------------------------------------------------
% idgen_next_rid(+IDGenIn, -RID, -IDGenOut):
%------------------------------------------------------------------------------

idgen_next_rid(idgen(RNo,CNo), RID, idgen(NextRNo,CNo)) :-
	NextRNo is RNo + 1,
	make_rid(NextRNo, RID).

%------------------------------------------------------------------------------
% idgen_next_cid(+IDGenIn, -CID, -IDGenOut):
%------------------------------------------------------------------------------

idgen_next_cid(idgen(RNo,CNo), CID, idgen(RNo,NextCNo)) :-
	NextCNo is CNo + 1,
	make_cid(NextCNo, CID).


%==============================================================================
% Type "VioCond" (Violation Conditions):
%==============================================================================


%------------------------------------------------------------------------------
% is_viocond(+VioCond):
%------------------------------------------------------------------------------

is_viocond(viocond(ID, No1, No2, LitList, Formula)) :-
	is_cid(ID),
	is_rid(No1),
	is_rid(No2),
	is_litlist(LitList),
	is_formula(Formula).

%------------------------------------------------------------------------------
% print_viocond(+VioCond):
%------------------------------------------------------------------------------

print_viocond(viocond(ID, No1, No2, LitList, Formula)) :-
	write('Constraint '),
	print_cid(ID),
	write(' with Rule '),
	print_rid(No1),
	write(' and Rule '),
	print_rid(No2),
	write(':'),
	nl,
	print_viocond_cases(LitList, Formula),
	write('.'),
	nl,
	nl.

% print_viocond_cases(+LitList, +Formula):

print_viocond_cases([], true) :-
	!,
	write('true').

print_viocond_cases([Lit|Rest], true) :-
	!,
	print_litlist([Lit|Rest]).

print_viocond_cases([], Formula) :-
	!,
	write('\t'),
	print_formula(Formula).

print_viocond_cases([Lit|Rest], Formula) :-
	print_litlist([Lit|Rest]),
	write(','),
	nl,
	write('\t'),
	print_formula(Formula).

%------------------------------------------------------------------------------
% make_viocond(+ID, +No1, +No2, +LitList, +Formula, -VioCond):
%------------------------------------------------------------------------------

make_viocond(ID, No1, No2, LitList, Formula,
		viocond(ID, No1, No2, LitList, Formula)).

%------------------------------------------------------------------------------
% viocond_lits(+VioCond, -LitList):
%------------------------------------------------------------------------------

viocond_lits(viocond(_ID, _No1, _No2, LitList, _Formula), LitList).

%------------------------------------------------------------------------------
% viocond_formula(+VioCond, -Formula):
%------------------------------------------------------------------------------

viocond_formula(viocond(_ID, _No1, _No2, _LitList, Formula), Formula).


%==============================================================================
% Type "VCList" (List of Violation Conditions):
%==============================================================================


%------------------------------------------------------------------------------
% is_vclist(+VCList):
%------------------------------------------------------------------------------

is_vclist([]).

is_vclist([VioCond|VCList]) :-
	is_viocond(VioCond),
	is_vclist(VCList).

%------------------------------------------------------------------------------
% print_vclist(+VCList):
%------------------------------------------------------------------------------

print_vclist([]).

print_vclist([VioCond|Rest]) :-
	print_viocond(VioCond),
	print_vclist(Rest).


%==============================================================================
% Type "VCStat" (Statistics for Violation Conditions):
%==============================================================================


%------------------------------------------------------------------------------
% is_vcstat(+VCStat):
%------------------------------------------------------------------------------

is_vcstat(vcstat(NumVCond,NumRefuted,NonRefutedList)) :-
	integer(NumVCond),
	NumVCond >= 0,
	integer(NumRefuted),
	NumRefuted >= 0,
	NumVCond >= NumRefuted,
	is_vclist(NonRefutedList),
	list_length(NonRefutedList, L),
	L is NumVCond - NumRefuted.

%------------------------------------------------------------------------------
% print_vcstat(+VCStat):
%------------------------------------------------------------------------------

print_vcstat(vcstat(NumVCond,NumRefuted,_)) :-
	write('Total Number of Violation Conditions: '),
	write(NumVCond),
	nl,
	write('Refuted:     '),
	write(NumRefuted),
	nl,
	NotRefuted is NumVCond - NumRefuted,
	write('Not Refuted: '),
	write(NotRefuted),
	nl.

%------------------------------------------------------------------------------
% print_vcstat(+VCStat):
%------------------------------------------------------------------------------

print_vcstat_long(vcstat(NumVCond,NumRefuted,NonRefutedList)) :-
	print_vcstat(vcstat(NumVCond,NumRefuted,NonRefutedList)),
	nl,
	print_opt_nonrefuted(NonRefutedList).

% print_opt_nonrefuted(+VCList):

print_opt_nonrefuted([]) :-
	write('*** All Violation conditions refuted, constraints proven ***'),
	nl.

print_opt_nonrefuted([VioCond|VCList]) :-
	write('Non Refuted Violation Conditions:'),
	nl,
	write('================================'),
	nl,
	nl,
	print_vclist([VioCond|VCList]).

%------------------------------------------------------------------------------
% init_vcstat(-VCStat):
%------------------------------------------------------------------------------

init_vcstat(vcstat(0,0,[])).

%------------------------------------------------------------------------------
% inc_refuted(+VCStatIn, -VCStatOut):
%------------------------------------------------------------------------------

inc_refuted(vcstat(NumVCondIn,NumRefutedIn,VCList),
		vcstat(NumVCondOut,NumRefutedOut,VCList)) :-
	NumVCondOut is NumVCondIn + 1,
	NumRefutedOut is NumRefutedIn + 1.

%------------------------------------------------------------------------------
% inc_nonrefuted(+VCStatIn, +VioCond, -VCStatOut):
%------------------------------------------------------------------------------

inc_nonrefuted(vcstat(NumVCondIn,NumRefuted,VCListIn),
		VioCond,
		vcstat(NumVCondOut,NumRefuted,VCListOut)) :-
	NumVCondOut is NumVCondIn + 1,
	list_append(VCListIn, [VioCond], VCListOut).


%==============================================================================
% Type "Refute" (Reason why Violation Condition is not Satisfiable):
%==============================================================================


%------------------------------------------------------------------------------
% is_refute(+Refute):
%------------------------------------------------------------------------------

is_refute(retfute0(VFormula)) :-
	is_formula(VFormula).

is_refute(refute1(Lit1,Lit2,ID,VFormula)) :-
	is_lit(Lit1),
	is_lit(Lit2),
	is_cid(ID),
	is_formula(VFormula).

%------------------------------------------------------------------------------
% print_refute(+Refute):
%------------------------------------------------------------------------------

print_refute(refute0(VFormula)) :-
	write('\tViolation condition is inconsistent:'),
	nl,
	write('\tVForm: '),
	print_formula(VFormula),
	nl.

print_refute(refute1(Lit1,Lit2,ID,VFormula)) :-
	write('\tViolation condition is inconsistent with constraint '),
	print_cid(ID),
	nl,
	write('\tLit 1: '),
	print_lit(Lit1),
	nl,
	write('\tLit 2: '),
	print_lit(Lit2),
	nl,
	write('\tVForm: '),
	print_formula(VFormula),
	nl.

%------------------------------------------------------------------------------
% make_refute0(+VFormula, -Refute):
%------------------------------------------------------------------------------

% The built-in literals together with the formula from the constraint
% of the violation were already inconsistent.
% It was not necessary to apply a constraint.

make_refute0(VFormula, refute0(VFormula)).

%------------------------------------------------------------------------------
% make_refute1(+Lit1, +Lit2, +ID, +VFormula, -Refute):
%------------------------------------------------------------------------------

% Violation condition was refuted by applying constraint ID
% to literals Lit1 and Lit2 of the violation condition.
% The resulting violation formula Cond was inconsistent.

make_refute1(Lit1, Lit2, ID, VFormula, refute1(Lit1,Lit2,ID,VFormula)).


%==============================================================================
% Type "Subst" (Substitutions):
%==============================================================================

% Substitutions are represented as lists of variable->Term mappings.
% However, it is necessary to repeatedly apply the mapping.
% E.g. [subst(X,Y), subst(Y,Z)] represents {X/Z, Y/Z}.
% In order to avoid cycles, we check that when X/T is added (at the end),
% there is no substitution for T. And of course, no substition for X.
% The unification algorithm guarantees this property.

%------------------------------------------------------------------------------
% is_subst(+Subst):
%------------------------------------------------------------------------------

is_subst([]).

is_subst([subst(Var,Term)|Rest]) :-
	is_var(Var),
	is_term(Term),
	is_subst(Rest).

%------------------------------------------------------------------------------
% empty_subst(-Subst):
%------------------------------------------------------------------------------

empty_subst([]).

%------------------------------------------------------------------------------
% subst_one(+Var, +Term, -Subst):
%------------------------------------------------------------------------------

subst_one(v(Var), Term, [subst(v(Var),Term)]) :-
	Term \= v(Var).

subst_one(v(Var,No), Term, [subst(v(Var,No),Term)]) :-
	Term \= v(Var,No).

%------------------------------------------------------------------------------
% subst_add(+SubstIn, +Var, +Term, -SubstOut):
%------------------------------------------------------------------------------

% SubstIn must not contain a mapping for Var alreay.

%subst_add(SubstIn, Var, Term, [subst(Var,Term)|SubstOut]) :-
%	no_subst_for(SubstIn, Var).

subst_add([], v(Var), Term, [subst(v(Var),Term)]) :-
	Term \= v(Var).

subst_add([], v(Var,No), Term, [subst(v(Var,No),Term)]) :-
	Term \= v(Var,No).

subst_add([subst(OtherVar,OtherTerm)|RestIn], Var, Term, 
		[subst(OtherVar,OtherTerm)|RestOut]) :-
	Var \= OtherVar,
	Term \= OtherVar,
	subst_add(RestIn, Var, Term, RestOut).

%------------------------------------------------------------------------------
% no_subst_for(+SubstIn, +Var):
%------------------------------------------------------------------------------

% unused?

no_subst_for([], _Var).

no_subst_for([subst(OtherVar,_)|Rest], Var) :-
	OtherVar \= Var,
	no_subst_for(Rest, Var).

%------------------------------------------------------------------------------
% do_subst_var(+Var, +Subst, -Term):
%------------------------------------------------------------------------------

do_subst_var(Var, Subst, Term) :-
	do_subst_var_search(Subst, Var, Subst, Term).

% do_subst_var_search(+RestSubst, +Var, +OriginalSubst, -Term):
do_subst_var_search([subst(Var,Term)|_], Var, Subst, TermOut) :-
	% If substitution was done, apply Subst again to result:
	do_subst_term(Term, Subst, TermOut).

do_subst_var_search([subst(OtherVar,_)|RestSubst], Var, Subst, Term) :-
	Var \= OtherVar,
	do_subst_var_search(RestSubst, Var, Subst, Term).

do_subst_var_search([], Var, _Subst, Var).
	% If no substitution was done, we are done.

%------------------------------------------------------------------------------
% do_subst_term(+TermIn, +Subst, -TermOut):
%------------------------------------------------------------------------------

do_subst_term(v(Var), Subst, TermOut) :-
	do_subst_var(v(Var), Subst, TermOut).

do_subst_term(v(Var,No), Subst, TermOut) :-
	do_subst_var(v(Var,No), Subst, TermOut).

do_subst_term(Const, _Subst, Const) :-
	is_const(Const).

%------------------------------------------------------------------------------
% do_subst_termlist(+TermsIn, +Subst, -TermsOut):
%------------------------------------------------------------------------------

do_subst_termlist([], _Subst, []).

do_subst_termlist([TermIn|RestIn], Subst, [TermOut|RestOut]) :-
	do_subst_term(TermIn, Subst, TermOut),
	do_subst_termlist(RestIn, Subst, RestOut).

%------------------------------------------------------------------------------
% do_subst_lit(+LitIn, +Subst, -LitOut):
%------------------------------------------------------------------------------

do_subst_lit(LitIn, Subst, LitOut) :-
	LitIn =.. [Pred|ArgsIn],
	do_subst_termlist(ArgsIn, Subst, ArgsOut),
	LitOut =.. [Pred|ArgsOut].

%------------------------------------------------------------------------------
% do_subst_litlist(+LitsIn, +Subst, -LitsOut):
%------------------------------------------------------------------------------

do_subst_litlist([], _Subst, []).

do_subst_litlist([LitIn|RestIn], Subst, [LitOut|RestOut]) :-
	do_subst_lit(LitIn, Subst, LitOut),
	do_subst_litlist(RestIn, Subst, RestOut).

%------------------------------------------------------------------------------
% do_subst_formula(+FormulaIn, +Subst, -FormulaOut):
%------------------------------------------------------------------------------

do_subst_formula(or(FormulaIn1,FormulaIn2), Subst,
			or(FormulaOut1,FormulaOut2)) :-
	!,
	do_subst_formula(FormulaIn1, Subst, FormulaOut1),
	do_subst_formula(FormulaIn2, Subst, FormulaOut2).

do_subst_formula(and(FormulaIn1,FormulaIn2), Subst,
			and(FormulaOut1,FormulaOut2)) :-
	!,
	do_subst_formula(FormulaIn1, Subst, FormulaOut1),
	do_subst_formula(FormulaIn2, Subst, FormulaOut2).

do_subst_formula(not(FormulaIn1), Subst,
			not(FormulaOut1)) :-
	!,
	do_subst_formula(FormulaIn1, Subst, FormulaOut1).

do_subst_formula(LitIn, Subst, LitOut) :-
	do_subst_lit(LitIn, Subst, LitOut).

%------------------------------------------------------------------------------
% print_subst(+Subst):
%------------------------------------------------------------------------------

% This prints the real substitution, as defined in theory,
% where variables are replaced once in parallel.
% Since the list contains only single replacement steps,
% we use do_subst_term to get the final version of the replacement term.

print_subst([]) :-
	write('{}').

print_subst([subst(Var,Term)|Rest]) :-
	write('{'),
	print_subst_pair(Var, Term, [subst(Var,Term)|Rest]),
	print_subst_rest(Rest, [subst(Var,Term)|Rest]),
	write('}').

% print_subst_pair(+Var, +Term, +Subst):

print_subst_pair(Var, Term, Subst) :-
	print_var(Var),
	write('/'),
	do_subst_term(Term, Subst, FinalTerm),
	print_term(FinalTerm).

% print_subst_rest(+PairList, +Subst):

print_subst_rest([], _Subst).

print_subst_rest([subst(Var,Term)|Rest], Subst) :-
	write(', '),
	print_subst_pair(Var, Term, Subst),
	print_subst_rest(Rest, Subst).

%==============================================================================
% Type "Token":
%==============================================================================

% The lexical scanner returns a list of tokens.

%------------------------------------------------------------------------------
% is_token(+Token):
%------------------------------------------------------------------------------

			% E.g.:
is_token(atom(_)).	% ab    (alphanumeric, starts with lowercase letter).
is_token(var(_)).	% X     (alphanumeric, starts with uppercase letter).
is_token(int(_)).	% 123   (sequence of digits).
is_token(str(_)).	% 'abc' (any characters enclosed in '...')
is_token(cconst(_)).	% #LOW  (alphanumeric after #, first must be letter)
is_token(lparen).	% (
is_token(rparen).	% )
is_token(comma).	% ,
is_token(fullstop) :-	% .     (followed by whitespace)
is_token(if).		% <- or :-
is_token(comp(eq)).	% =
is_token(comp(ne)).	% != or \=
is_token(comp(lt)).	% <
is_token(comp(le)).	% <= or =<
is_token(comp(gt)).	% >
is_token(comp(ge)).	% >=
is_token(plus).		% +
is_token(at(AtKeyword)) :-	% @next, @init, @start, @setup, @call, @ret
	at_keyword(AtKeyword).
is_token(or).		% |
is_token(and).		% &
is_token(param).	% ?
is_token(not).		% \+ or !

%------------------------------------------------------------------------------
% at_keyword(+Keyword):
%------------------------------------------------------------------------------

% Possible Keywords after @:
at_keyword(next).
at_keyword(this).
at_keyword(init).
at_keyword(start).
at_keyword(setup).
at_keyword(call).
at_keyword(ret).

%------------------------------------------------------------------------------
% comparison_op(+Op):
%------------------------------------------------------------------------------

% ? unused

comparison_op(eq).
comparison_op(ne).
comparison_op(lt).
comparison_op(le).
comparison_op(gt).
comparison_op(ge).

%------------------------------------------------------------------------------
% print_token(Token):
%------------------------------------------------------------------------------

print_token(atom(Atom)) :-
	write(Atom).

print_token(var(Var)) :-
	write(Var).

print_token(int(Int)) :-
	write(Int).

print_token(str(Str)) :-
	write('\''),
	print_chars(Str),
	write('\'').

print_token(cconst(Const)) :-
	write('#'),
	write(Const).

print_token(lparen) :-
	write('(').

print_token(rparen) :-
	write(')').

print_token(comma) :-
	write('\',\'').

print_token(fullstop) :-
	write('\'.\'').

print_token(if) :-
	write('<-').

print_token(comp(eq)) :-
	write('=').

print_token(comp(ne)) :-
	write('!=').

print_token(comp(lt)) :-
	write('<').

print_token(comp(le)) :-
	write('<=').

print_token(comp(gt)) :-
	write('>').

print_token(comp(ge)) :-
	write('>=').

print_token(at(AtKeyword)) :-
	at_keyword(AtKeyword),
	!,
	write('@'),
	write(AtKeyword).

print_token(plus) :-
	write('+').

print_token(or) :-
	write('|').

print_token(and) :-
	write('&').

print_token(not) :-
	write('\\+').

print_token(param) :-
	write('?').

%------------------------------------------------------------------------------
% print_token_list(+TokenList):
%------------------------------------------------------------------------------

print_token_list([]).

print_token_list([Token|Rest]) :-
	write('\t'),
	print_token(Token),
	nl,
	print_token_list(Rest).

%------------------------------------------------------------------------------
% print_token_type(Token):
%------------------------------------------------------------------------------

print_token_type(atom(_)) :-
	!,
	write('Atom').

print_token_type(var(_)) :-
	!,
	write('Variable').

print_token_type(int(_)) :-
	!,
	write('Integer').

print_token_type(str(_)) :-
	!,
	write('String').

print_token_type(cconst(_)) :-
	!,
	write('#-Const').

print_token_type(at(_)) :-
	!,
	write('@').

print_token_type(comp(_)) :-
	!,
	write('Comparison operator').

print_token_type(OtherToken) :-
	print_token(OtherToken),
	!.

print_token_type(Unknown) :-
	write('token type '),
	write(Unknown),
	write(' (??? Please inform programmer)').

%******************************************************************************
% Input Data, Parsing, Preprocessing:
%******************************************************************************


%==============================================================================
% Input Data:
%==============================================================================


%------------------------------------------------------------------------------
% input_rule(-Rule):
%------------------------------------------------------------------------------

:- dynamic(input_rule/1).

%------------------------------------------------------------------------------
% input_constraint(-Constraint):
%------------------------------------------------------------------------------

:- dynamic(input_constraint/1).

%------------------------------------------------------------------------------
% clear_input:
%------------------------------------------------------------------------------

clear_input :-
	delete_all(input_rule, 1),
	delete_all(input_constraint, 1).

%------------------------------------------------------------------------------
% blink1:
%------------------------------------------------------------------------------

% Set input_rule and input_constraint to the data of the example "Blink1".

blink1 :-
	clear_input,
	store_blink1_rules,
	store_blink1_constraints.

store_blink1_rules :-
	blink1_rule(No, Head, Body),
	make_rule(No, Head, Body, Rule),
	assert(input_rule(Rule)),
	fail.
store_blink1_rules.

store_blink1_constraints :-
	blink1_constraint(ID, Lit1, Lit2, Formula),
	make_constraint(ID, Lit1, Lit2, Formula, Constraint),
	assert(input_constraint(Constraint)),
	fail.
store_blink1_constraints.


%------------------------------------------------------------------------------
% blink0:
%------------------------------------------------------------------------------

% Set input_rule and input_constraint to the data of the example "Blink1".

blink0 :-
	clear_input,
	store_blink0_rules,
	store_blink0_constraints.

store_blink0_rules :-
	blink0_rule(No, Head, Body),
	make_rule(No, Head, Body, Rule),
	assert(input_rule(Rule)),
	fail.
store_blink0_rules.

store_blink0_constraints :-
	blink0_constraint(ID, Lit1, Lit2, Formula),
	make_constraint(ID, Lit1, Lit2, Formula, Constraint),
	assert(input_constraint(Constraint)),
	fail.
store_blink0_constraints.


%==============================================================================
% Read Source Program:
%==============================================================================


%------------------------------------------------------------------------------
% load(+FileName, +OptChars):
%------------------------------------------------------------------------------

load(FileName, OptChars) :-
	set_opt(OptChars),
	load(FileName).

%------------------------------------------------------------------------------
% load(+FileName):
%------------------------------------------------------------------------------

load(FileName) :-
	write('Loading input program \"'),
	write(FileName),
	write('\" ...'),
	nl,
	open_file_with_errmsg(FileName, Stream),
	idgen_init(IDGen),
	read_source_rules(Stream, IDGen),
	file_close(Stream).

%------------------------------------------------------------------------------
% open_file_with_errmsg(+FileName, -Stream):
%------------------------------------------------------------------------------

open_file_with_errmsg(FileName, Stream) :-
	file_ropen(FileName, Stream),
	!.

% Try to add extension '.mlg' to solve the problem:
open_file_with_errmsg(FileName, Stream) :-
	atom_chars(FileName, FileChars),
	atom_chars('.mlg', ExtChars),
	list_append(FileChars, ExtChars, Chars),
	atom_chars(FileWithExt, Chars),
	file_ropen(FileWithExt, Stream),
	!.

open_file_with_errmsg(FileName, _) :-
	write('Cannot open input file: \"'),
	write(FileName),
	write('\"!'),
	nl,
	fail.

%------------------------------------------------------------------------------
% read_source_rules(+Stream, +IDGen):
%------------------------------------------------------------------------------

read_source_rules(Stream, IDGen) :-
	skip_spaces(Stream),
	file_eof(Stream) -> 
		finished_reading
	;	file_lineno(Stream, FirstLine),
		read_source_rule(Stream, Chars, LastLineNo),
		!,
		show_source_rule(FirstLine, LastLineNo, Chars),
		parse(Chars, FirstLine, LastLineNo, IDGen, NextIDGen),
		read_source_rules(Stream, NextIDGen).

% finished_reading:

finished_reading :-
	err(_,_),
	!,
	nl,
	write('Finished reading source program (with errors).\n').

finished_reading :-
	write('Program successfully loaded.\n').

%------------------------------------------------------------------------------
% skip_spaces(+Stream): Position Stream on next non-space/comment character.
%------------------------------------------------------------------------------

skip_spaces(Stream) :-
	file_peekc(Stream, Char),
	(is_space(Char) -> file_getc(Stream, Char), skip_spaces(Stream);
	is_comment(Char) -> file_getc(Stream, Char), skip_comment(Stream),
				skip_spaces(Stream);
	true).

%------------------------------------------------------------------------------
% skip_comment(+Stream): Skip to end of line or end of file.
%------------------------------------------------------------------------------

skip_comment(Stream) :-
	file_getc(Stream, Char),
	(Char == end_of_file -> true;
	Char == '\n' -> true;
	skip_comment(Stream)).

%------------------------------------------------------------------------------
% read_source_rule(+Stream, -Chars, -LastLineNo): Read characters until '.'.
%------------------------------------------------------------------------------

% LastLineNo is the number of the line with the final '.':

read_source_rule(Stream, Chars, LastLineNo) :-
	file_getc(Stream, Char),
	read_source_rule_cont(Stream, Char, Chars, LastLineNo).

% read_source_rule_cont(+Stream, +Char, -Chars, -LastLineNo):

read_source_rule_cont(Stream, end_of_file, [], LastLineNo) :-
	!,
	line_count(Stream, LastLineNo).

read_source_rule_cont(Stream, '.', ['.'], LastLineNo) :-
	line_count(Stream, LastLineNo),
	whitespace(Stream),
	!.

read_source_rule_cont(Stream, '\'', ['\''|Rest], LastLineNo) :-
	file_getc(Stream, Next_Char),
	read_source_rule_str(Stream, Next_Char, Rest, LastLineNo).

read_source_rule_cont(Stream, '%', ['%'|Rest], LastLineNo) :-
	file_getc(Stream, Next_Char),
	read_source_rule_comment(Stream, Next_Char, Rest, LastLineNo).

read_source_rule_cont(Stream, Char, [Char|Rest], LastLineNo) :-
	file_getc(Stream, Next_Char),
	read_source_rule_cont(Stream, Next_Char, Rest, LastLineNo).

% There is a certain duplication with the lexical scanner here.
% We must continue reading characters if '.' occurs inside a string constant.
% The same, if it occurs inside a comment.
%
% read_source_rule_str(+Stream, +Char, -Chars, -LastLineNo):

read_source_rule_str(Stream, end_of_file, [], LastLineNo) :-
	!,
	line_count(Stream, LastLineNo).

read_source_rule_str(Stream, '\'', ['\''|Rest], LastLineNo) :-
	!,
	file_getc(Stream, Next_Char),
	read_source_rule_cont(Stream, Next_Char, Rest, LastLineNo).

read_source_rule_str(Stream, Char, [Char|Rest], LastLineNo) :-
	file_getc(Stream, Next_Char),
	read_source_rule_str(Stream, Next_Char, Rest, LastLineNo).

% read_source_rule_comment(+Stream, +Char, -Chars, -LastLineNo):

read_source_rule_comment(Stream, end_of_file, [], LastLineNo) :-
	!,
	line_count(Stream, LastLineNo).

read_source_rule_comment(Stream, '\n', ['\n'|Rest], LastLineNo) :-
	!,
	file_getc(Stream, Next_Char),
	read_source_rule_cont(Stream, Next_Char, Rest, LastLineNo).

read_source_rule_comment(Stream, Char, [Char|Rest], LastLineNo) :-
	file_getc(Stream, Next_Char),
	read_source_rule_comment(Stream, Next_Char, Rest, LastLineNo).

%------------------------------------------------------------------------------
% whitespace(+Stream):
%------------------------------------------------------------------------------

% True if at least one whitespace character in stream,
% skips all whitespace until line end.

whitespace(Stream) :-
	file_peekc(Stream, C),
	is_space(C),
	!,
	skip_whitespace_to_nl(Stream).

%------------------------------------------------------------------------------
% skip_whitespace_to_nl(+Stream):
%------------------------------------------------------------------------------

skip_whitespace_to_nl(Stream) :-
	file_peekc(Stream, '\n'),
	!,
	file_getc(Stream, '\n').

skip_whitespace_to_nl(Stream) :-
	file_peekc(Stream, C),
	is_space(C),
	file_getc(Stream, C),
	!,
	skip_whitespace_to_nl(Stream).

skip_whitespace_to_nl(_).

%------------------------------------------------------------------------------
% assert_facts(+Facts):
%------------------------------------------------------------------------------

%assert_facts([]).
%
%assert_facts([Fact|MoreFacts]) :-
%	assert(prog(Fact)),
%	assert_facts(MoreFacts).

%------------------------------------------------------------------------------
% show_source_rule(+FirstLineNo, +LastLineNo, +Chars):
%------------------------------------------------------------------------------

show_source_rule(FirstLineNo, LastLineNo, Chars) :-
	opt(show_input_chars),
	!,
	nl,
	write('Rule '),
	print_line_no(FirstLineNo, LastLineNo),
	write(':'),
	nl,
	print_chars(Chars),
	nl,
	nl.

show_source_rule(_, _, _).


%==============================================================================
% Syntax Error Messages:
%==============================================================================

% In order not to complicate scanner and parser, we use a dynamic database
% fact for storing information about the current line:
%     err_info(FirstLineNo, LastLineNo, Chars).
% This is asserted for every line (input rule) that is read,
% before parser and scanner are called.
% If an error occurs, this information is used, and the fact is deleted
% from the dynamic database. In this way, additional error messages for
% the same rule are suppressed (an error message is only printed when the fact
% still exists in the dynamic database).
% Error handling is added to the predicates by means of an additional rule
% in the end which prints the error message and then fails.
% Only the topmost parser predicate does not fail, but produces an error fact
% err(FirstLineNo, LastLineNo), so that parsing can continue with the next rule.
% The existence of such error facts shows that there were errors, and the
% input program should not be executed.

%------------------------------------------------------------------------------
% err(-FirstLineNo, -LastLineNo): Error occurred.
%------------------------------------------------------------------------------

:- dynamic(err/2).

%------------------------------------------------------------------------------
% err_info(-FirstLineNo, -LastLineNo, -Chars):
%------------------------------------------------------------------------------

% This predicate stores information about the rule that is currently being
% parsed to be used in a possible error message.

:- dynamic(err_info/3).

%------------------------------------------------------------------------------
% clear_err:
%------------------------------------------------------------------------------

clear_err :-
	delete_all(err, 2),
	delete_all(err_info, 3).

%------------------------------------------------------------------------------
% store_err_info(+FirstLineNo, +LastLineNo, +Chars):
%------------------------------------------------------------------------------

store_err_info(FirstLineNo, LastLineNo, Chars) :-
	delete_all(err_info, 3),
	assert(err_info(FirstLineNo, LastLineNo, Chars)).

%------------------------------------------------------------------------------
% syntax_error(+ErrMsg):
%------------------------------------------------------------------------------

% If this is the first error in the rule, the err_info fact still exists,
% and the error message is printed:

syntax_error(ErrMsg) :-
	err_info(FirstLineNo, LastLineNo, Chars),
	!,
	delete_all(err_info, 3),
	assert(err(FirstLineNo,LastLineNo)),
	nl,
	write('Syntax error '),
	print_line_no(FirstLineNo, LastLineNo),
	write(': '),
	print_errmsg_failsafe(ErrMsg),
	nl,
	print_chars(Chars),
	nl.

% Not the first error, simply ignore it:

syntax_error(_).

% print_line_no(+FirstLineNo, +LastLineNo):

print_line_no(LineNo, LineNo) :-
	!,
	write('in line '),
	write(LineNo).

print_line_no(FirstLineNo, LastLineNo) :-
	!,
	write('between line '),
	write(FirstLineNo),
	write(' and '),
	write(LastLineNo).

%------------------------------------------------------------------------------
% print_errmsg_failsafe(+ErrMsg):
%------------------------------------------------------------------------------

print_errmsg_failsafe(ErrMsg) :-
	print_errmsg(ErrMsg),
	!.

print_errmsg_failsafe(ErrMsg) :-
	nl,
	write('Sorry, no message for '),
	write(ErrMsg),
	write(' (please tell programmer).').


%------------------------------------------------------------------------------
% print_errmsg(+ErrMsg):
%------------------------------------------------------------------------------

print_errmsg(invalid_char(Char)) :-
	write('Invalid character \''),
	write(Char),
	write('\'.').

print_errmsg(string_not_closed) :-
	write('String not closed.').

print_errmsg(invalid_char_after_at(Char)) :-
	write('Invalid character \''),
	write(Char),
	write('\' after @.').

print_errmsg(missing_keyword_after_at) :-
	write('Missing keyword after @.').

print_errmsg(invalid_at_keyword(Keyword)) :-
	write('Invalid keyword \''),
	write(Keyword),
	write('\' after @.').

print_errmsg(invalid_char_after_hash(Char)) :-
	write('Invalid character \''),
	write(Char),
	write('\' after # (must be letter).').

print_errmsg(missing_const_after_hash) :-
	write('Missing constant after #.').

print_errmsg(expect(ExpectedTokens, TokenList, Place)) :-
	nl,
	write('Expected '),
	print_expected(ExpectedTokens),
	write(' '),
	write(Place),
	write(','),
	nl,
	write('    found '),
	print_found(TokenList),
	write('.').

print_errmsg(expect_end(TokenList, Place)) :-
	nl,
	write('Expected end of rule '),
	write(Place),
	write(','),
	nl,
	write('    found '),
	print_found(TokenList),
	write('.').

print_errmsg(unbound_var(Var)) :-
	write('Unbound Variable: '),
	write(Var),
	write('.').

print_errmsg(unknown_type(Type)) :-
	write('Unknown data type: '),
	write(Type),
	write('.').

print_errmsg(db_pred_in_head(Pred)) :-
	write('Database predicate in rule head: '),
	write(Pred),
	write('.').

print_errmsg(db_pred_already_in_head(Pred,Line)) :-
	write('DB predicate '),
	write(Pred),
	write(' already defined by rule in line '),
	write(Line),
	write('.').

print_errmsg(db_pred_already_declared(Pred,Line)) :-
	write('DB predicate '),
	write(Pred),
	write(' already declared in line '),
	write(Line),
	write('.').

print_errmsg(db_arg_name_undeclared(ArgName,Pred)) :-
	write('Argument '),
	write(ArgName),
	write(' of '),
	write(Pred),
	write('is not declared.').

print_errmsg(db_invalid_arg_no(ArgNo,Pred)) :-
	write('Argument number '),
	write(ArgNo),
	write(' of '),
	write(Pred),
	write('is invalid.').

print_errmsg(only_one_at) :-
	write('@ can only be used once per literal, '),
	write('either before or after the arguments.').

print_errmsg(invalid_at_in_constraint(At)) :-
	write('@'),
	write(At),
	write('cannot be used in constraint literals.').

print_errmsg(ret_forbidden_in_head) :-
	write('@ret cannot be used in the rule head').

print_errmsg(unknown_at_in_head(At)) :-
	write('Unknown @-keyword \''),
	write(At),
	write('\' in rule head').

print_errmsg(invalid_at_in_body(At)) :-
	write('@'),
	write(At),
	write('cannot be used in body literals.').

print_errmsg(params_only_in_head) :-
	write('The parameter marker ? can be used only in @call-literals '),
	write('in rule heads.').

print_errmsg(params_only_in_calls) :-
	write('The parameter marker ? can be used only in @call-literals.').

print_errmsg(negation_not_yet_supported) :-
	write('Negation of body literals is not yet supported.').

print_errmsg(invalid_plus_comp_op(Op)) :-
	write('Currently, only < and >= can be used with +, not '),
	print_token(comp(Op)),
	write('.').

print_errmsg(unhandled) :-
	write('Sorry, no specific message available.').

%------------------------------------------------------------------------------
% expect(+ExpectedTokens, +TokenList, +Place):
%------------------------------------------------------------------------------

expect(ExpectedTokens, [Token|_], _) :-
	member(Token, ExpectedTokens),
	!.

expect(ExpectedTokens, TokenList, Place) :-
	syntax_error(expect(ExpectedTokens, TokenList, Place)),
	fail.

%------------------------------------------------------------------------------
% expect_end(+TokenList, +Place):
%------------------------------------------------------------------------------

expect_end([], _) :-
	!.

expect_end(TokenList, Place) :-
	syntax_error(expect_end(TokenList, Place)),
	fail.

%------------------------------------------------------------------------------
% print_expected(+Tokens):
%------------------------------------------------------------------------------

print_expected([Token]) :-
	print_token_type(Token).

print_expected([Token1, Token2]) :-
	print_token_type(Token1),
	write(', or '),
	print_token_type(Token2).

print_expected([Token1, Token2, Token3 | MoreTokens]) :-
	print_token_type(Token1),
	write(', '),
	print_expected([Token2, Token3 | MoreTokens]).

%------------------------------------------------------------------------------
% print_found(+Tokens):
%------------------------------------------------------------------------------

print_found([Token|_]) :-
	print_token(Token),
	%print_token_info(Token),
	!.

print_found([Token|_]) :-
	write('invalid token: '),
	write(Token).

print_found([]) :-
	write('end of rule').


%------------------------------------------------------------------------------
% print_token_info(+Token):
%------------------------------------------------------------------------------

% Additional information about offending token in syntax error message:
%print_token_info(Keyword) :-
%	keyword(Keyword),
%	!,
%	write(' (keyword)').
%
%print_token_info(_).

%==============================================================================
% Lexical Scanner:
%==============================================================================

%------------------------------------------------------------------------------
%tokenize(+CharList, -TokenList).
%------------------------------------------------------------------------------

tokenize([Char|Chars], Tokens) :-
	is_space(Char),
	!,
	tokenize(Chars, Tokens).

tokenize([Char|Chars], Tokens) :-
	is_comment(Char),
	!,
	skip_to_newline(Chars, Rest),
	tokenize(Rest, Tokens).

tokenize([Char|Chars], [Token|Tokens]) :-
	is_lower(Char),
	!,
	tokenize_word(Char, Chars, RestChars, AtomChars),
	atom_chars(Atom, AtomChars),
	keyword_or_atom(Atom, Token),
	tokenize(RestChars, Tokens).

tokenize([Char|Chars], [var(Atom)|Tokens]) :-
	is_upper(Char),
	!,
	tokenize_word(Char, Chars, RestChars, AtomChars),
	atom_chars(Atom, AtomChars),
	tokenize(RestChars, Tokens).

tokenize([Char|Chars], [int(Int)|Tokens]) :-
	is_digit(Char),
	!,
	tokenize_int(Char, Chars, RestChars, Digits),
	make_int(Digits, Int),
	tokenize(RestChars, Tokens).

tokenize([Char|Chars], [str(Str)|Tokens]) :-
	is_quote(Char),
	!,
	tokenize_str(Char, Chars, RestChars, Str),
	tokenize(RestChars, Tokens).

tokenize(['('|Chars], [lparen|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize([')'|Chars], [rparen|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize([','|Chars], [comma|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['.'|Chars], [fullstop|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['<', '-' |Chars], [if|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize([':', '-' |Chars], [if|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['=', '<' |Chars], [comp(le)|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['<', '=' |Chars], [comp(le)|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['<' |Chars], [comp(lt)|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['>', '=' |Chars], [comp(ge)|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['>' |Chars], [comp(gt)|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['\\', '=' |Chars], [comp(ne)|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['!', '=' |Chars], [comp(ne)|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['=' |Chars], [comp(eq)|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['@' |Chars], [at(Keyword)|Tokens]) :-
	!,
	tokenize_at(Chars, RestChars, Keyword),
	tokenize(RestChars, Tokens).

tokenize(['#' |Chars], [cconst(Const)|Tokens]) :-
	!,
	tokenize_cconst(Chars, RestChars, Const),
	tokenize(RestChars, Tokens).

tokenize(['+' |Chars], [plus|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['?' |Chars], [param|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['|' |Chars], [or|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['&' |Chars], [and|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['!' |Chars], [not|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize([':', '-' |Chars], [prolog_if|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize(['\\', '+' |Chars], [not|Tokens]) :-
	!,
	tokenize(Chars, Tokens).

tokenize([InvalidChar |_], []) :-
	syntax_error(invalid_char(InvalidChar)),
	fail.

tokenize([], []).

%------------------------------------------------------------------------------
% tokenize_word(+CurrentChar, +MoreChars, -RemainingChars, -AtomChars).
%------------------------------------------------------------------------------

tokenize_word(Char, [NextChar|Chars], RestChars, [Char|AtomChars]) :-
	is_alnum(Char),
	!,
	tokenize_word(NextChar, Chars, RestChars, AtomChars).

tokenize_word(Char, Chars, [Char|Chars], []).

%------------------------------------------------------------------------------
% tokenize_int(Char, Chars, RestChars, Digits):
%------------------------------------------------------------------------------

tokenize_int(Digit, [NextChar|Chars], RestChars, [Digit|MoreDigits]) :-
	is_digit(Digit),
	!,
	tokenize_int(NextChar, Chars, RestChars, MoreDigits).

tokenize_int(Char, Chars, [Char|Chars], []).

%------------------------------------------------------------------------------
% make_int(+Digits, -Int):
%------------------------------------------------------------------------------

make_int(Digits, Int) :-
	make_int(Digits, 0, Int).

% make_int(+Digits, +IntIn, -IntOut):

make_int([], Int, Int).

make_int([Digit|RestDigits], IntIn, IntOut) :-
	digit_val(Digit, DigitVal),
	Int is IntIn * 10 + DigitVal,
	make_int(RestDigits, Int, IntOut).

%------------------------------------------------------------------------------
% tokenize_str(+Quote, +Chars, -RestChars, -Str)
%------------------------------------------------------------------------------

tokenize_str(Quote, ['\\','n'|Chars], RestChars, ['\n'|Str]) :-
	!,
	tokenize_str(Quote, Chars, RestChars, Str).

tokenize_str(Quote, [Char|Chars], RestChars, [Char|Str]) :-
	Char \= Quote,
	!,
	tokenize_str(Quote, Chars, RestChars, Str).

tokenize_str(Quote, [Quote|Chars], Chars, []) :-
	!.

tokenize_str(_, [], [], []) :-
	syntax_error(string_not_closed),
	fail.

%------------------------------------------------------------------------------
% tokenize_at(+Chars, -RestChars, -Keyword):
%------------------------------------------------------------------------------

tokenize_at(Chars, RestChars, Keyword) :-
	tokenize_at_first(Chars, RestChars1, FirstChar),
	tokenize_at_rest(RestChars1, RestChars, MoreChars),
	atom_chars(Keyword, [FirstChar|MoreChars]),
	check_at_keyword(Keyword).

%------------------------------------------------------------------------------
% tokenize_at_first(+Chars, -RestChars, -FirstChar):
%------------------------------------------------------------------------------

tokenize_at_first([FirstChar|RestChars], RestChars, FirstChar) :-
	is_lower(FirstChar),
	!.

tokenize_at_first([FirstChar|RestChars], RestChars, FirstChar) :-
	is_upper(FirstChar),
	!.

tokenize_at_first([FirstChar|RestChars], RestChars, FirstChar) :-
	syntax_error(invalid_char_after_at(FirstChar)),
	!,
	fail.

tokenize_at_first([], [], '.') :-
	syntax_error(missing_keyword_after_at),
	fail.

%------------------------------------------------------------------------------
% tokenize_at_rest(+Chars, -RestChars, -KeywordChars):
%------------------------------------------------------------------------------

tokenize_at_rest([Char|Chars], RestChars, [Char|KeywordChars]) :-
	is_lower(Char),
	!,
	tokenize_at_rest(Chars, RestChars, KeywordChars).

tokenize_at_rest([Char|Chars], RestChars, [Char|KeywordChars]) :-
	is_upper(Char),
	!,
	tokenize_at_rest(Chars, RestChars, KeywordChars).

tokenize_at_rest(RestChars, RestChars, []).

%------------------------------------------------------------------------------
% check_at_keyword(+Keyword):
%------------------------------------------------------------------------------

check_at_keyword(Keyword) :-
	at_keyword(Keyword),
	!.

check_at_keyword(Keyword) :-
	syntax_error(invalid_at_keyword(Keyword)),
	fail.
%------------------------------------------------------------------------------
% tokenize_cconst(+Chars, -RestChars, -Const):
%------------------------------------------------------------------------------

tokenize_cconst(Chars, RestChars, Const) :-
	tokenize_cconst_first(Chars, RestChars1, FirstChar),
	tokenize_word(FirstChar, RestChars1, RestChars, ConstChars),
	atom_chars(Const, ConstChars).

%------------------------------------------------------------------------------
% tokenize_cconst_first(+Chars, -RestChars, -FirstChar):
%------------------------------------------------------------------------------

tokenize_cconst_first([FirstChar|RestChars], RestChars, FirstChar) :-
	is_lower(FirstChar),
	!.

tokenize_cconst_first([FirstChar|RestChars], RestChars, FirstChar) :-
	is_upper(FirstChar),
	!.

tokenize_cconst_first([FirstChar|RestChars], RestChars, FirstChar) :-
	syntax_error(invalid_char_after_hash(FirstChar)),
	!,
	fail.

tokenize_cconst_first([], [], '.') :-
	syntax_error(missing_const_after_hash),
	fail.

%------------------------------------------------------------------------------
% keyword_or_atom(+Atom, -Token):
%------------------------------------------------------------------------------

%keyword_or_atom(Keyword, Keyword) :-
%	keyword(Keyword),
%	!.

keyword_or_atom(Atom, atom(Atom)).

%------------------------------------------------------------------------------
% keyword(+Keyword):
%------------------------------------------------------------------------------

% List of keywords (reserved words):
%keyword(db).
%keyword(type).
%keyword(fd).

%------------------------------------------------------------------------------
% skip_to_newline(+Chars, -Rest):
%------------------------------------------------------------------------------

skip_to_newline(['\n'|Rest], Rest) :-
	!.

skip_to_newline([], []).

skip_to_newline([Char|Chars], Rest) :-
	Char \== '\n',
	skip_to_newline(Chars, Rest).

%------------------------------------------------------------------------------
% digit_val(Digit, Int).
%------------------------------------------------------------------------------

digit_val('0', 0).
digit_val('1', 1).
digit_val('2', 2).
digit_val('3', 3).
digit_val('4', 4).
digit_val('5', 5).
digit_val('6', 6).
digit_val('7', 7).
digit_val('8', 8).
digit_val('9', 9).

%------------------------------------------------------------------------------
% is_space(Char).
%------------------------------------------------------------------------------

is_space(' ').
is_space('\t').
is_space('\n').
is_space('\r').

%------------------------------------------------------------------------------
% is_lower(Char).
%------------------------------------------------------------------------------

is_lower('a').
is_lower('b').
is_lower('c').
is_lower('d').
is_lower('e').
is_lower('f').
is_lower('g').
is_lower('h').
is_lower('i').
is_lower('j').
is_lower('k').
is_lower('l').
is_lower('m').
is_lower('n').
is_lower('o').
is_lower('p').
is_lower('q').
is_lower('r').
is_lower('s').
is_lower('t').
is_lower('u').
is_lower('v').
is_lower('w').
is_lower('x').
is_lower('y').
is_lower('z').

%------------------------------------------------------------------------------
% is_upper(Char).
%------------------------------------------------------------------------------

is_upper('A').
is_upper('B').
is_upper('C').
is_upper('D').
is_upper('E').
is_upper('F').
is_upper('G').
is_upper('H').
is_upper('I').
is_upper('J').
is_upper('K').
is_upper('L').
is_upper('M').
is_upper('N').
is_upper('O').
is_upper('P').
is_upper('Q').
is_upper('R').
is_upper('S').
is_upper('T').
is_upper('U').
is_upper('V').
is_upper('W').
is_upper('X').
is_upper('Y').
is_upper('Z').

%------------------------------------------------------------------------------
% is_digit(Char).
%------------------------------------------------------------------------------

is_digit('0').
is_digit('1').
is_digit('2').
is_digit('3').
is_digit('4').
is_digit('5').
is_digit('6').
is_digit('7').
is_digit('8').
is_digit('9').

%------------------------------------------------------------------------------
% is_alnum(Char).
%------------------------------------------------------------------------------

is_alnum(Char) :-
	is_lower(Char).

is_alnum(Char) :-
	is_upper(Char).

is_alnum(Char) :-
	is_digit(Char).

is_alnum('_').

%------------------------------------------------------------------------------
% is_comment(Char)
%------------------------------------------------------------------------------

is_comment('%').

%------------------------------------------------------------------------------
% is_whitespace(Char)
%------------------------------------------------------------------------------

is_whitespace(' ').
is_whitespace('\t').
is_whitespace('\n').
is_whitespace('\r').

%------------------------------------------------------------------------------
% show_input_tokens(+FirstLine, +LastLine, +Tokens):
%------------------------------------------------------------------------------

show_input_tokens(FirstLine, LastLine, Tokens) :-
	opt(show_input_tokens),
	!,
	write('Input Tokens '),
	print_line_no(FirstLine, LastLine),
	write(':'),
	nl,
	print_token_list(Tokens),
	nl.

show_input_tokens(_, _, _).

%==============================================================================
% Main Parser Predicate:
%==============================================================================

%------------------------------------------------------------------------------
% parse(+Chars, +FirstLineNo, +LastLineNo, +IDGenIn, -IDGenOut):
%------------------------------------------------------------------------------

parse(Chars, FirstLineNo, LastLineNo, IDGenIn, IDGenOut) :-
	store_err_info(FirstLineNo, LastLineNo, Chars),
	tokenize(Chars, Tokens),
	show_input_tokens(FirstLineNo, LastLineNo, Tokens),
	parse_rule_or_cons(Tokens, IDGenIn, IDGenOut),
	!.

parse(_, _FirstLineNo, _LastLineNo, IDGen, IDGen) :-
	syntax_error(unhandled).

%==============================================================================
% Parser for Source Program:
%==============================================================================

% Handling of syntax errors:
% -------------------------
%    At the start of each predicate, the next token is compared with the list
%    of possible tokens at this place (expected tokens).
%    If it is not in the list, a syntax error is written for the first such
%    error in a rule. Later messages are suppressed (see syntax_error above).
%    There is a predicate parse_N for each non-terminal N.
%    This predicate checks the token, and then calls xparse_N,
%    which does the real parsing, and often contains several rules that differ
%    in the first token.
%    Because of this treatment of syntax errors, backtracking cannot be used:
%    if one calls parse_N, one must be sure that N has to come.
%    (Actually, backtracking is ok, if after N different cases are treated.)
%    In seldom cases a specific token is expected in the middle of a rule body.
%    Then the check of the expected token is done first, to generate the
%    standard error message, in case the following unification should fail.

%------------------------------------------------------------------------------
% parse_rule_or_cons(+Tokens, +IDGenIn, -IDGenOut)
%------------------------------------------------------------------------------

parse_rule_or_cons(Tokens, IDGenIn, IDGenOut) :-
	dbg_parser(parse_rule_or_cons, Tokens),
	expect([atom(_),if], Tokens, 'at start of rule or constraint'),
	xparse_rule_or_cons(Tokens, IDGenIn, IDGenOut).

% xparse_rule_or_cons(+Tokens, +IDGenIn, -IDGenOut):

% Constraint:
xparse_rule_or_cons([if|Tokens], IDGenIn, IDGenOut) :-
	!,
	parse_con_lit(Tokens, Lit1, Tokens1),
	expect([comma], Tokens1, 'after first literal in constraint'),
	Tokens1 = [comma|Tokens2],
	parse_con_lit(Tokens2, Lit2, Tokens3), 
	parse_opt_formula(Tokens3, Formula, Tokens4),
	expect([fullstop], Tokens4, 'after constraint literals'),
	Tokens4 = [fullstop|Tokens5],
	!,
	expect_end(Tokens5, 'after constraint'),
% TODO: Semantic Check!
	idgen_next_cid(IDGenIn, CID, IDGenOut),
	make_constraint(CID, Lit1, Lit2, Formula, Constraint),
	assert(input_constraint(Constraint)).

% Fact:
xparse_rule_or_cons(Tokens, IDGenIn, IDGenOut) :-
	parse_head_lit(Tokens, HeadLit, _At, Tokens1),
	expect([if,fullstop], Tokens1, 'after head literal'),
	Tokens1 = [fullstop|RestTokens],
	!,
	expect_end(RestTokens, 'after fact'),
% TODO: Semantic Check!
	idgen_next_rid(IDGenIn, RID, IDGenOut),
	make_rule(RID, HeadLit, [], Rule),
	assert(input_rule(Rule)).

% TODO: Duplizierung Head literal parsen besser vermeiden!

% Rule:
xparse_rule_or_cons(Tokens, IDGenIn, IDGenOut) :-
	parse_head_lit(Tokens, HeadLit, At, Tokens1),
	expect([if], Tokens1, 'after head literal'),
	Tokens1 = [if|BodyTokens],
	parse_body(BodyTokens, BodyLits, Tokens2),
	expect([fullstop], Tokens2, 'after body'),
	Tokens2 = [fullstop|RestTokens],
	expect_end(RestTokens, 'after rule'),
	gen_body(At, BodyLits, FullBody),
% TODO: Semantic Check!
	idgen_next_rid(IDGenIn, RID, IDGenOut),
	make_rule(RID, HeadLit, FullBody, Rule),
	assert(input_rule(Rule)).


%==============================================================================
% >>> Parsing Predicates for Rule Body <<<
%==============================================================================


%------------------------------------------------------------------------------
% parse_body(+Tokens, -Body, -RestTokens)
%------------------------------------------------------------------------------

parse_body(Tokens, Body, RestTokens) :-
	dbg_parser(parse_body, Tokens),
	expect([not,atom(_),str(_),int(_),var(_)], Tokens, 'at start of body'),
	xparse_body(Tokens, Body, RestTokens).

% xparse_body(+Tokens, -Body, -RestTokens):

xparse_body(Tokens, [Lit|Body], RestTokens) :-
	parse_body_lit(Tokens, Lit, Tokens1),
	parse_body_rest(Tokens1, Body, RestTokens).

%------------------------------------------------------------------------------
% parse_body_rest(+Tokens, -Body, -RestTokens):
%------------------------------------------------------------------------------

% (begins with comma or fullstop).

parse_body_rest(Tokens, Body, RestTokens) :-
	dbg_parser(parse_body_rest, Tokens),
	expect([comma,fullstop], Tokens, 'after body literal'),
	xparse_body_rest(Tokens, Body, RestTokens).

% xparse_body_rest(+Tokens, -Body, -RestTokens):

xparse_body_rest([comma|Tokens], Body, RestTokens) :-
	!,
	parse_body(Tokens, Body, RestTokens).

xparse_body_rest([fullstop|Tokens], [], [fullstop|Tokens]).


%==============================================================================
% >>> Parsing Predicates for Literals <<<
%==============================================================================


%------------------------------------------------------------------------------
% parse_con_lit(+Tokens, -Lit, -RestTokens):
%------------------------------------------------------------------------------

% Standard literal in a constraint.
% (from predicate to rparen)

parse_con_lit(Tokens, Lit, RestTokens) :-
	dbg_parser(parse_con_lit, Tokens),
	expect([atom(_)], Tokens, 'at start of constraint literal'),
	xparse_con_lit(Tokens, Lit, RestTokens).

% xparse_con_lit(+Tokens, -Lit, -RestTokens):

xparse_con_lit([atom(Pred)|Tokens1], Lit, RestTokens) :-
	parse_opt_at(Tokens1, [lparen,comma,fullstop],
			"after predicate in constraint literal",
			At1, Tokens2),
	parse_opt_args(Tokens2, Args, Tokens3),
	parse_opt_at(Tokens3, [comma,fullstop], "after constraint literal",
			At2, RestTokens),
	only_one_at(At1, At2, At),
	gen_con_lit(Pred, At, Args, Lit).

%------------------------------------------------------------------------------
% parse_head_lit(+Tokens, -Lit, -At, -RestTokens)
%------------------------------------------------------------------------------

% (from predicate to rparen)

parse_head_lit(Tokens, Lit, At, RestTokens) :-
	dbg_parser(parse_head_lit, Tokens),
	expect([atom(_)], Tokens, 'at start of head literal'),
	xparse_head_lit(Tokens, Lit, At, RestTokens).

% xparse_head_lit(+Tokens, -Lit, -At, -RestTokens):

xparse_head_lit([atom(Pred)|Tokens1], Lit, At, RestTokens) :-
	parse_opt_at(Tokens1, [lparen,if,fullstop],
			"after predicate in head literal",
			At1, Tokens2),
	parse_opt_head_args(Tokens2, Args, NumParams, Tokens3),
	parse_opt_at(Tokens3, [if,fullstop], "after head literal",
			At2, RestTokens),
	only_one_at(At1, At2, At),
	gen_head_lit(Pred, At, Args, NumParams, Lit).

%------------------------------------------------------------------------------
% parse_opt_at(+Tokens, +Follow, +Place, -At, -RestTokens)
%------------------------------------------------------------------------------

% This can appear in the head or body of a rule,
% and in the literals of a constraint.
% Currently, it is allowed immediately after the predicate
% and alternatively after the argument list.
% To handle all these options, the caller must specify a list of tokens that
% might follow this nonterminal, and also a Place text that is printed in
% the error message if the current token is not at(_) or an element of Follow.

parse_opt_at(Tokens, Follow, Place, At, RestTokens) :-
	dbg_parser(parse_opt_at, Tokens),
	expect([at(_)|Follow], Tokens, Place),
	xparse_opt_at(Tokens, At, RestTokens).

xparse_opt_at([at(At)|Tokens], At, Tokens) :-
	!.

xparse_opt_at(Tokens, none, Tokens).

%------------------------------------------------------------------------------
% only_one_at(+At1, +At2, -At)
%------------------------------------------------------------------------------

only_one_at(none, At, At) :-
	!.

only_one_at(At, none, At) :-
	!.

only_one_at(_, At, At) :-
	syntax_error(only_one_at),
	fail.

%------------------------------------------------------------------------------
% parse_body_lit(+Tokens, -Lit, -RestTokens)
%------------------------------------------------------------------------------

% from optional negation to rparen

parse_body_lit(Tokens, Lit, RestTokens) :-
	dbg_parser(parse_body_lit, Tokens),
	expect([not,atom(_),int(_),str(_),var(_)], Tokens,
		'at start of literal'),
	xparse_body_lit(Tokens, Lit, RestTokens).

% xparse_body_lit(+Tokens, -Lit, -RestTokens):

xparse_body_lit([not|Tokens], negated(Lit), RestTokens) :-
	syntax_error(negation_not_yet_supported),
	parse_pos_body_lit(Tokens, Lit, RestTokens).

xparse_body_lit([Other|Tokens], Lit, RestTokens) :-
	Other \= not,
	parse_pos_body_lit([Other|Tokens], Lit, RestTokens).

%------------------------------------------------------------------------------
% parse_pos_body_lit(+Tokens, -Lit, -RestTokens)
%------------------------------------------------------------------------------

% (from predicate to rparen)

parse_pos_body_lit(Tokens, Lit, RestTokens) :-
	dbg_parser(parse_pos_body_lit, Tokens),
	expect([atom(_),int(_),str(_),var(_)], Tokens, 'at start of literal'),
	xparse_pos_body_lit(Tokens, Lit, RestTokens).

% xparse_pos_body_lit(+Tokens, -Lit, -RestTokens):

xparse_pos_body_lit([atom(Pred)|Tokens], Lit, RestTokens) :-
	expect([at(_),lparen,comma,fullstop,comp(_)], Tokens,
		'after predicate or comparison term'),
	Tokens=[NextTok|_],
	member(NextTok, [at(_),lparen,comma,fullstop]),
	!,
	parse_opt_at(Tokens, [lparen,comma,fullstop],
			"after predicate in body literal", At1, Tokens1),
	parse_opt_args(Tokens1, Args, Tokens2),
	parse_opt_at(Tokens2, [comma,fullstop],
			"after arguments in body literal", At2, RestTokens),
	only_one_at(At1, At2, At),
	gen_body_lit(Pred, At, Args, Lit).

xparse_pos_body_lit(Tokens, Lit, RestTokens) :-
	parse_arg(Tokens, Arg1, Tokens1),
	parse_comparison_rest(Tokens1, Arg1, Lit, RestTokens).

%------------------------------------------------------------------------------
% parse_comparison_rest(+Tokens, +Arg1, -Lit, -RestTokens)
%------------------------------------------------------------------------------

parse_comparison_rest(Tokens, Arg1, Lit, RestTokens) :-
	dbg_parser(parse_comparison_rest, Tokens),
	expect([comp(_),plus], Tokens, 'after first term of comparison'),
	xparse_comparison_rest(Tokens, Arg1, Lit, RestTokens).

% xparse_comparison_rest(+Tokens, +Arg1, -Lit, -RestTokens):

xparse_comparison_rest([comp(Op)|Tokens], Arg1, Lit, RestTokens) :-
	parse_arg(Tokens, Arg2, RestTokens),
	gen_comp_lit(Op, Arg1, Arg2, Lit).

xparse_comparison_rest([plus|Tokens], Arg1, Lit, RestTokens) :-
	parse_arg(Tokens, Arg2, Tokens1),
	expect([comp(_)], Tokens1, 'after sum in comparison'),
	Tokens1 = [comp(Op)|Tokens2],
	parse_arg(Tokens2, Arg3, RestTokens),
	gen_sum_comp_lit(Op, Arg1, Arg2, Arg3, Lit).

%==============================================================================
% >>> Parsing Predicates for Argument Lists of Literals <<<
%==============================================================================


%------------------------------------------------------------------------------
% parse_opt_head_args(+Tokens, -Args, -NumParams, -RestTokens)
%------------------------------------------------------------------------------

% (from lparen to rparen) or nothing.
% NumParams is the number of ? at the end of the argument list (only in @call).

parse_opt_head_args(Tokens, Args, NumParams, RestTokens) :-
	dbg_parser(parse_opt_head_args, Tokens),
	expect([lparen,at(_),if,fullstop], Tokens, 'at head argument list'),
	xparse_opt_head_args(Tokens, Args, NumParams, RestTokens).

xparse_opt_head_args([lparen|Tokens], Args, NumParams, RestTokens) :-
	!,
	parse_args([lparen|Tokens], Args, NumParams, RestTokens).

xparse_opt_head_args(Tokens, [], 0, Tokens).

%------------------------------------------------------------------------------
% parse_args(+Tokens, -Args, -NumParams, -RestTokens)
%------------------------------------------------------------------------------

% (from lparen to rparen)

parse_args(Tokens, Args, NumParams, RestTokens) :-
	dbg_parser(parse_args, Tokens),
	expect([lparen], Tokens, 'at start of argument list'),
	xparse_head_args(Tokens, Args, NumParams, RestTokens).

xparse_head_args([lparen|Tokens], Args, NumParams, RestTokens) :-
	parse_arg_list(Tokens, Args, NumParams, Tokens1),
	Tokens1 = [rparen|RestTokens].

%------------------------------------------------------------------------------
% parse_arg_list(+Tokens, -Args, -NumParams, -RestTokens):
%------------------------------------------------------------------------------

% (starts with term - i.e. '(' was already read, ')' will be read afterwards)

parse_arg_list(Tokens, Args, NumParams, RestTokens) :-
	dbg_parser(parse_arg_list, Tokens),
	expect([var(_),atom(_),int(_),str(_),cconst(_),param], Tokens,
		'as argument'),
	xparse_arg_list(Tokens, Args, NumParams, RestTokens).

xparse_arg_list([param|RestTokens], [], NumParams, RestTokens) :-
	!,
	parse_par_list([param|RestTokens], NumParams, RestTokens).

xparse_arg_list(Tokens, [Term|Args], NumParams, RestTokens) :-
	parse_arg(Tokens, Term, Tokens1),
	parse_args_rest(Tokens1, Args, NumParams, RestTokens).

%------------------------------------------------------------------------------
% parse_args_rest(+Tokens, -Args, -NumParams, -RestTokens).
%------------------------------------------------------------------------------

% (starts with comma or rparen)

parse_args_rest(Tokens, Args, NumParams, RestTokens) :-
	dbg_parser(parse_args_rest, Tokens),
	expect([comma, rparen], Tokens, 'after argument term'),
	xparse_args_rest(Tokens, Args, NumParams, RestTokens).

xparse_args_rest([comma|Tokens], Args, NumParams, RestTokens) :-
	parse_arg_list(Tokens, Args, NumParams, RestTokens).

xparse_args_rest([rparen|Tokens], [], 0, [rparen|Tokens]).


%==============================================================================
% >>> Parsing Predicates for ? Suffix of Argument List <<<
%==============================================================================

% This is allowed only for @call literals, but this is checked later.
% When this predicate is called, it can be any head or body literal
% with an argument list in (...).

%------------------------------------------------------------------------------
% parse_par_list(+Tokens, -NumParams, -RestTokens):
%------------------------------------------------------------------------------

% Called when ? appears in argument list.

parse_par_list(Tokens, NumParams, RestTokens) :-
	dbg_parser(parse_par_list, Tokens),
	expect([param], Tokens, 'in ?-suffix of argument list'),
	xparse_par_list(Tokens, NumParams, RestTokens).

xparse_par_list([param|Tokens], NumParams1, RestTokens) :-
	!,
	parse_par_rest(Tokens, NumParams, RestTokens),
	NumParams1 is NumParams + 1.

%------------------------------------------------------------------------------
% parse_par_rest(+Tokens, -NumParams, -RestTokens):
%------------------------------------------------------------------------------

% Called after ? in argument list

parse_par_rest(Tokens, NumParams, RestTokens) :-
	dbg_parser(parse_par_rest, Tokens),
	expect([comma,rparen], Tokens, 'after ? in argument list'),
	xparse_par_rest(Tokens, NumParams, RestTokens).

xparse_par_rest([comma|Tokens], NumParams, RestTokens) :-
	!,
	parse_par_list(Tokens, NumParams, RestTokens).

xparse_par_rest([rparen|Tokens], 0, [rparen|Tokens]).


%==============================================================================
% >>> Parsing Predicates for Argument List of Body Literals <<<
%==============================================================================


%------------------------------------------------------------------------------
% parse_opt_args(+Tokens, -Args, -RestTokens)
%------------------------------------------------------------------------------

% (from lparen to rparen) or nothing.

parse_opt_args(Tokens, Args, RestTokens) :-
	dbg_parser(parse_opt_args, Tokens),
	expect([lparen,comma,fullstop], Tokens, 'at argument list'),
	xparse_opt_args(Tokens, Args, RestTokens).

xparse_opt_args([lparen|Tokens], Args, RestTokens) :-
	!,
	parse_args([lparen|Tokens], Args, NumParams, RestTokens),
	check_params_only_in_head(NumParams).

xparse_opt_args(Tokens, [], Tokens).

%------------------------------------------------------------------------------
% check_params_only_in_head(+NumParams)
%------------------------------------------------------------------------------

check_params_only_in_head(0) :-
	!.

check_params_only_in_head(_) :-
	syntax_error(params_only_in_head).


%==============================================================================
% >>> Parsing Predicates for Single Argument (Term) - Used in Head and Body <<<
%==============================================================================


%------------------------------------------------------------------------------
% parse_arg(+Tokens, -Term, -RestTokens):
%------------------------------------------------------------------------------

parse_arg(Tokens, Term, RestTokens) :-
	dbg_parser(parse_arg, Tokens),
	expect([var(_),atom(_),int(_),str(_),cconst(_)], Tokens, 'as argument'),
	xparse_arg(Tokens, Term, RestTokens).

% xparse_arg(+Tokens, -Term, -RestTokens):

xparse_arg([atom(Atom)|Tokens], Atom, Tokens).

xparse_arg([int(Int)|Tokens], Int, Tokens).

xparse_arg([str(Str)|Tokens], str(Str), Tokens).

xparse_arg([cconst(Const)|Tokens], cconst(Const), Tokens).

xparse_arg([var(Var)|Tokens], v(Var), Tokens).


%==============================================================================
% >>> Parsing Predicates for Additional Formula in Constraints <<<
%==============================================================================


%------------------------------------------------------------------------------
% parse_opt_formula(+Tokens, -Formula, -RestTokens):
%------------------------------------------------------------------------------

% Currently, only disjunctions of disequalities are accepted (as in the paper).

parse_opt_formula(Tokens, Formula, RestTokens) :-
	dbg_parser(parse_opt_formula, Tokens),
	expect([comma,fullstop], Tokens, 'after literals in constraint'),
	xparse_opt_formula(Tokens, Formula, RestTokens).

xparse_opt_formula([comma|Tokens], Formula, RestTokens) :-
	!,
	parse_formula(Tokens, Formula, RestTokens).

xparse_opt_formula(Tokens, true, Tokens).


%------------------------------------------------------------------------------
% parse_formula(+Tokens, -Formula, -RestTokens):
%------------------------------------------------------------------------------

parse_formula(Tokens, Formula, RestTokens) :-
	dbg_parser(parse_formula, Tokens),
	expect([lparen,var(_),atom(_),int(_),str(_),cconst(_)], Tokens,
		'at start of constraint formula'),
	xparse_formula(Tokens, Formula, RestTokens).

xparse_formula([lparen|Tokens], Formula, RestTokens) :-
	!,
	parse_formula_disj(Tokens, Formula, Tokens1),
	expect([rparen], Tokens1, 'at end of parenthesized formula'),
	Tokens1 = [rparen|RestTokens].

xparse_formula(Tokens, Formula, RestTokens) :-
	parse_formula_atomic(Tokens, Formula, RestTokens).

%------------------------------------------------------------------------------
% parse_formula_disj(+Tokens, -Formula, -RestTokens):
%------------------------------------------------------------------------------

parse_formula_disj(Tokens, Formula, RestTokens) :-
	dbg_parser(parse_formula_disj, Tokens),
	expect([lparen,var(_),atom(_),int(_),str(_),cconst(_)], Tokens,
		'in constraint formula'),
	xparse_formula_disj(Tokens, Formula, RestTokens).

xparse_formula_disj([lparen|Tokens], Formula, RestTokens) :-
	!,
	parse_formula_disj(Tokens, Formula, Tokens1),
	expect([rparen], Tokens1, 'at end of parenthesized formula'),
	Tokens1 = [rparen|RestTokens].

xparse_formula_disj(Tokens, Formula, RestTokens) :-
	parse_formula_atomic(Tokens, Formula1, Tokens1),
	parse_formula_disj_rest(Tokens1, Formula1, Formula, RestTokens).

%------------------------------------------------------------------------------
% parse_formula_disj_rest(+Tokens, +LeftFormula, -Formula, -RestTokens):
%------------------------------------------------------------------------------

parse_formula_disj_rest(Tokens, LeftFormula, Formula, RestTokens) :-
	dbg_parser(parse_formula_disj_rest, Tokens),
	expect([or,rparen], Tokens, 'in constraint formula (disjunction)'),
	xparse_formula_disj_rest(Tokens, LeftFormula, Formula, RestTokens).

xparse_formula_disj_rest([or|Tokens], LeftFormula, Formula, RestTokens) :-
	!,
	parse_formula_disj(Tokens, RightFormula, RestTokens),
	Formula = or(LeftFormula,RightFormula).

xparse_formula_disj_rest(Tokens, Formula, Formula, Tokens).

%------------------------------------------------------------------------------
% parse_formula_atomic(+Tokens, -Formula, -RestTokens):
%------------------------------------------------------------------------------

parse_formula_atomic(Tokens, Formula, RestTokens) :-
	dbg_parser(parse_formula_atomic, Tokens),
	expect([var(_),atom(_),int(_),str(_),cconst(_)], Tokens,
		'at start of atomic constraint formula'),
	xparse_formula_atomic(Tokens, Formula, RestTokens).

xparse_formula_atomic(Tokens, Formula, RestTokens) :-
	!,
	parse_arg(Tokens, Term1, Tokens1),
	expect([comp(_)], Tokens1, 'in atomic constraint formula'),
	Tokens1 = [comp(Op)|Tokens2],
	parse_arg(Tokens2, Term2, RestTokens),
	gen_comp_lit(Op, Term1, Term2, Formula).


%==============================================================================
% Debug Output for Parser:
%==============================================================================


%------------------------------------------------------------------------------
% dbg_parser(+Pred, +Tokens):
%------------------------------------------------------------------------------

dbg_parser(Pred, Tokens) :-
	opt(dbg_out_parser),
	!,
	print_dbg_out_parser(Pred, Tokens).

dbg_parser(_, _).

%------------------------------------------------------------------------------
% print_dbg_out_parser(+Pred, +Tokens):
%------------------------------------------------------------------------------

print_dbg_out_parser(Pred, Tokens) :-
	write('\tParser: '),
	print_dbg_out_parser_pred(Pred),
	write(' '),
	print_dbg_out_parser_tokens(Tokens),
	nl.

%------------------------------------------------------------------------------
% print_dbg_out_parser_pred(+Pred):
%------------------------------------------------------------------------------

% To print parser predicate and token in columns, add spaces to width 20+1:

print_dbg_out_parser_pred(Pred) :-
	write(Pred),
	write(':'),
	atom_chars(Pred, PredChars),
	list_length(PredChars, Length),
	Spaces is 20 - Length,
	print_spaces(Spaces).

%------------------------------------------------------------------------------
% print_spaces(+NumSpaces):
%------------------------------------------------------------------------------

print_spaces(0) :-
	!.

print_spaces(N) :-
	N > 0,
	write(' '),
	NextN is N - 1,
	print_spaces(NextN).

%------------------------------------------------------------------------------
% print_dbg_out_parser_tokens(+Pred, +Tokens):
%------------------------------------------------------------------------------

print_dbg_out_parser_tokens([]) :-
	write('end of statement').

print_dbg_out_parser_tokens([Token|Rest]) :-
	print_token(Token),
	list_length(Rest, Length),
	write('   [+ '),
	write(Length),
	write(' more tokens]').

%==============================================================================
% Semantic Check:
%==============================================================================

%------------------------------------------------------------------------------
% gen_con_lit(+Pred, +At, +Args, -Lit):
%------------------------------------------------------------------------------

gen_con_lit(Pred, none, Args, Lit) :-
	!,
	Lit =.. [Pred,v('T')|Args].

gen_con_lit(Pred, call, Args, Lit) :-
	gen_call_pred(Pred, CallPred),
	!,
	Lit =.. [CallPred,v('T')|Args].

gen_con_lit(Pred, ret, Args, Lit) :-
	gen_ret_pred(Pred, RetPred),
	!,
	Lit =.. [RetPred,v('T')|Args].

gen_con_lit(_Pred, At, _Args, error) :-
	syntax_error(invalid_at_in_constraint(At)),
	fail.

%------------------------------------------------------------------------------
% gen_comp_lit(+Op, +Term1, +Term2, -Lit):
%------------------------------------------------------------------------------

gen_comp_lit(Op, Term1, Term2, Lit) :-
	Lit =.. [Op, Term1, Term2].

%------------------------------------------------------------------------------
% gen_sum_comp_lit(Op, Arg1, Arg2, Arg3, Lit):
%------------------------------------------------------------------------------

gen_sum_comp_lit(lt, Arg1, Arg2, Arg3, plus_lt(Arg1,Arg2,Arg3)) :-
	!,
	is_term(Arg1),
	is_term(Arg2),
	is_term(Arg3).

gen_sum_comp_lit(ge, Arg1, Arg2, Arg3, plus_ge(Arg1,Arg2,Arg3)) :-
	!,
	is_term(Arg1),
	is_term(Arg2),
	is_term(Arg3).

gen_sum_comp_lit(Op, _Arg1, _Arg2, _Arg3, error) :-
	syntax_error(invalid_plus_comp_op(Op)),
	fail.

%------------------------------------------------------------------------------
% gen_head_lit(+Pred, +At, +Args, +NumParams, -Lit):
%------------------------------------------------------------------------------

gen_head_lit(Pred, none, Args, NumParams, Lit) :-
	!,
	check_no_params(NumParams),
	Lit =.. [Pred,v('T')|Args].

gen_head_lit(Pred, next, Args, NumParams, Lit) :-
	!,
	check_no_params(NumParams),
	Lit =.. [Pred,v('S')|Args].

gen_head_lit(Pred, init, Args, NumParams, Lit) :-
	!,
	check_no_params(NumParams),
	Lit =.. [Pred,0|Args].

gen_head_lit(Pred, start, Args, NumParams, Lit) :-
	!,
	check_no_params(NumParams),
	Lit =.. [Pred,1|Args].

gen_head_lit(Pred, call, Args, _NumParams, Lit) :-
	gen_call_pred(Pred, CallPred),
	!,
	Lit =.. [CallPred,v('T')|Args].

gen_head_lit(Pred, setup, Args, _NumParams, Lit) :-
	gen_call_pred(Pred, CallPred),
	!,
	Lit =.. [CallPred,0|Args].

gen_head_lit(_Pred, ret, _Args, _NumParams, error) :-
	!,
	syntax_error(ret_forbidden_in_head),
	fail.

gen_head_lit(_Pred, At, _Args, _NumParams, error) :-
	syntax_error(unknown_at_in_head(At)),
	fail.

%------------------------------------------------------------------------------
% check_no_params(+NumArgs):
%------------------------------------------------------------------------------

check_no_params(0) :-
	!.

check_no_params(_) :-
	syntax_error(params_only_in_calls).

%------------------------------------------------------------------------------
% gen_body_lit(+Pred, +At, +Args, -Lit):
%------------------------------------------------------------------------------

gen_body_lit(Pred, none, Args, Lit) :-
	!,
	Lit =.. [Pred,v('T')|Args].

gen_body_lit(Pred, ret, Args, Lit) :-
	gen_ret_pred(Pred, RetPred),
	!,
	Lit =.. [RetPred,v('T')|Args].

gen_body_lit(_Pred, At, _Args, error) :-
	syntax_error(invalid_at_in_body(At)),
	fail.

%------------------------------------------------------------------------------
% gen_call_pred(+Pred, -CallPred):
%------------------------------------------------------------------------------

gen_call_pred(Pred, CallPred) :-
	atom_chars('call_', PrefixChars),
	atom_chars(Pred, PredChars),
	list_append(PrefixChars, PredChars, Chars),
	atom_chars(CallPred, Chars).

%------------------------------------------------------------------------------
% gen_ret_pred(+Pred, -RetPred):
%------------------------------------------------------------------------------

gen_ret_pred(Pred, RetPred) :-
	atom_chars('ret_', PrefixChars),
	atom_chars(Pred, PredChars),
	list_append(PrefixChars, PredChars, Chars),
	atom_chars(RetPred, Chars).

%------------------------------------------------------------------------------
% gen_body(+At, +BodyLits, -FullBody):
%------------------------------------------------------------------------------

% This adds the succ-Literal to the body for @next rules:

gen_body(next, BodyLits, FullBody) :-
	!,
	list_append(BodyLits, [succ(v('T'),v('S'))], FullBody).

gen_body(_, BodyLits, BodyLits).

%******************************************************************************
% SLD Resolution Steps, Unfolding, Computation of Violation Conditions:
%******************************************************************************


%==============================================================================
% Renaming of Variables:
%==============================================================================

% This translates v(Name) into v(Name,VerNo).

%------------------------------------------------------------------------------
% fresh_var_term(+TermIn, +VerNo, -TermOut):
%------------------------------------------------------------------------------

fresh_var_term(v(Name), VerNo, v(Name,VerNo)) :-
	!.

fresh_var_term(Const, _VerNo, Const) :-
	is_const(Const).

%------------------------------------------------------------------------------
% fresh_var_term_list(+TermListIn, +VerNo, -TermListOut):
%------------------------------------------------------------------------------

fresh_var_term_list([], _VerNo, []).

fresh_var_term_list([TermIn|RestIn], VerNo, [TermOut|RestOut]) :-
	fresh_var_term(TermIn, VerNo, TermOut),
	fresh_var_term_list(RestIn, VerNo, RestOut).

%------------------------------------------------------------------------------
% fresh_var_lit(+LitIn, +VerNo, -LitOut):
%------------------------------------------------------------------------------

fresh_var_lit(LitIn, VerNo, LitOut) :-
	LitIn =.. [Pred|ArgsIn],
	fresh_var_term_list(ArgsIn, VerNo, ArgsOut),
	LitOut =.. [Pred|ArgsOut].

%------------------------------------------------------------------------------
% fresh_var_lit_list(+LitListIn, +VerNo, -LitListOut):
%------------------------------------------------------------------------------

fresh_var_lit_list([], _VerNo, []).

fresh_var_lit_list([LitIn|RestIn], VerNo, [LitOut|RestOut]) :-
	fresh_var_lit(LitIn, VerNo, LitOut),
	fresh_var_lit_list(RestIn, VerNo, RestOut).

%------------------------------------------------------------------------------
% fresh_var_formula(+FormulaIn, +VerNo, -FormulaOut):
%------------------------------------------------------------------------------

fresh_var_formula(or(FormulaIn1,FormulaIn2), VerNo,
			or(FormulaOut1,FormulaOut2)) :-
	!,
	fresh_var_formula(FormulaIn1, VerNo, FormulaOut1),
	fresh_var_formula(FormulaIn2, VerNo, FormulaOut2).

fresh_var_formula(and(FormulaIn1,FormulaIn2), VerNo,
			and(FormulaOut1,FormulaOut2)) :-
	!,
	fresh_var_formula(FormulaIn1, VerNo, FormulaOut1),
	fresh_var_formula(FormulaIn2, VerNo, FormulaOut2).

fresh_var_formula(not(FormulaIn1), VerNo,
			not(FormulaOut1)) :-
	!,
	fresh_var_formula(FormulaIn1, VerNo, FormulaOut1).

fresh_var_formula(LitIn, VerNo, LitOut) :-
	fresh_var_lit(LitIn, VerNo, LitOut).

%------------------------------------------------------------------------------
% rule_with_fresh_var(+VerNo, -RuleNo, -Head, -Body):
%------------------------------------------------------------------------------

rule_with_fresh_var(VerNo, RuleNo, HeadOut, BodyOut) :-
	input_rule(rule(RuleNo, Head, Body)),
	fresh_var_lit(Head, VerNo, HeadOut),
	fresh_var_lit_list(Body, VerNo, BodyOut).

%------------------------------------------------------------------------------
% constraint_with_fresh_var(+VerNo, -ID, -Lit1, -Lit2, -Formula):
%------------------------------------------------------------------------------

constraint_with_fresh_var(VerNo, ID, LitOut1, LitOut2, FormulaOut) :-
	input_constraint(Constraint),
	constraint_data(Constraint, ID, Lit1, Lit2, Formula),
	fresh_var_lit(Lit1, VerNo, LitOut1),
	fresh_var_lit(Lit2, VerNo, LitOut2),
	fresh_var_formula(Formula, VerNo, FormulaOut).


%==============================================================================
% Generation of Unique Version Numbers:
%==============================================================================


%------------------------------------------------------------------------------
% unique_ver(-Ver):
%------------------------------------------------------------------------------

% Declaration of dynamic predicate:
:- dynamic(unique_ver/1).

%------------------------------------------------------------------------------
% init_unique_ver(+Ver):
%------------------------------------------------------------------------------

% Note: Versions 1 and 2 are fixed for the generation of violation conditions.
% Thus, this predicate should be called with version 3.
% The given version number for the variables is the first number returned.

init_unique_ver(Ver) :-
	delete_all(unique_ver, 1),
	assert(unique_ver(Ver)).

%------------------------------------------------------------------------------
% get_unique_ver(-Ver):
%------------------------------------------------------------------------------

get_unique_ver(Ver) :-
	unique_ver(Ver),
	!,
	retract(unique_ver(Ver)),
	NextVer is Ver + 1,
	assert(unique_ver(NextVer)).

get_unique_ver(error) :-
	nl,
	write('***** Error: unique_ver not initialized'),
	nl,
	fail.


%==============================================================================
% Unification:
%==============================================================================


%------------------------------------------------------------------------------
% unify_step(+Term1, +Term2, +SubstIn, -SubstOut):
%------------------------------------------------------------------------------

unify_step(v(Var), v(Var), Subst, Subst) :-
	!.

unify_step(v(Var,No), v(Var,No), Subst, Subst) :-
	!.

unify_step(v(Var), Term, SubstIn, SubstOut) :-
	!,
	subst_add(SubstIn, v(Var), Term, SubstOut).

unify_step(v(Var,No), Term, SubstIn, SubstOut) :-
	!,
	subst_add(SubstIn, v(Var,No), Term, SubstOut).

unify_step(Const, v(Var), SubstIn, SubstOut) :-
	is_const(Const),
	!,
	subst_add(SubstIn, v(Var), Const, SubstOut).

unify_step(Const, v(Var,No), SubstIn, SubstOut) :-
	is_const(Const),
	!,
	subst_add(SubstIn, v(Var,No), Const, SubstOut).

unify_step(Const, Const, Subst, Subst) :-
	is_const(Const).

%------------------------------------------------------------------------------
% unify_term(+Term1, +Term2, +SubstIn, -SubstOut):
%------------------------------------------------------------------------------

unify_term(Term1, Term2, SubstIn, SubstOut) :-
	do_subst_term(Term1, SubstIn, RealTerm1),
	do_subst_term(Term2, SubstIn, RealTerm2),
	unify_step(RealTerm1, RealTerm2, SubstIn, SubstOut).

%------------------------------------------------------------------------------
% unify_termlist(+TermList1, +TermList2, +SubstIn, -SubstOut):
%------------------------------------------------------------------------------

unify_termlist([], [], Subst, Subst).

unify_termlist([Term1|Rest1], [Term2|Rest2], SubstIn, SubstOut) :-
	unify_term(Term1, Term2, SubstIn, Subst),
	unify_termlist(Rest1, Rest2, Subst, SubstOut).

%------------------------------------------------------------------------------
% unify_lit(+Lit1, +Lit2, +SubstIn, -SubstOut):
%------------------------------------------------------------------------------

unify_lit(Lit1, Lit2, SubstIn, SubstOut) :-
	Lit1 =.. [Pred|Args1],
	Lit2 =.. [Pred|Args2],
	unify_termlist(Args1, Args2, SubstIn, SubstOut).

%------------------------------------------------------------------------------
% unify_lit(+Lit1, +Lit2, -Subst):
%------------------------------------------------------------------------------

unify_lit(Lit1, Lit2, Subst) :-
	empty_subst(EmptySubst),
	unify_lit(Lit1, Lit2, EmptySubst, Subst).

%------------------------------------------------------------------------------
% unify_pair(+Lits1, +Lits2, +SubstIn, -SubstOut):
%------------------------------------------------------------------------------

% unused?
unify_pair([A1,A2], [B1,B2], SubstIn, SubstOut) :-
	unify_lit(A1, B1, SubstIn, Subst),
	unify_lit(A2, B2, Subst, SubstOut).

%------------------------------------------------------------------------------
% unify_pair(+Lits1, +Lits2, -Subst):
%------------------------------------------------------------------------------

% unused?
unify_pair(Lits1, Lits2, Subst) :-
	empty_subst(EmptySubst),
	unify_pair(Lits1, Lits2, EmptySubst, Subst).


%==============================================================================
% Computation of Violation Conditions:
%==============================================================================


%------------------------------------------------------------------------------
% violation_cond(-VioCond):
%------------------------------------------------------------------------------

violation_cond(VioCond) :-
	input_constraint(Constraint),
	constraint_data(Constraint, ID, Lit1, Lit2, ConstraintFormula),
	rule_with_fresh_var(1, No1, Head1, BodyList1),
	unify_lit(Head1, Lit1, Subst1),
	rule_with_fresh_var(2, No2, Head2, BodyList2),
	unify_lit(Head2, Lit2, Subst1, Subst),
	do_subst_litlist(BodyList1, Subst, LitList1),
	do_subst_litlist(BodyList2, Subst, LitList2),
	list_append(LitList1, LitList2, LitList),
	do_subst_formula(ConstraintFormula, Subst, Formula),
	eval_obvious(Formula, SimplifiedFormula),
	SimplifiedFormula \= false,
	make_viocond(ID, No1, No2, LitList, SimplifiedFormula, VioCond).


%==============================================================================
% Refutation of Violation Conditions:
%==============================================================================


%------------------------------------------------------------------------------
% refute_violation_cond(+VioCond, -RefuteReason):
%------------------------------------------------------------------------------

refute_violation_cond(VioCond, Refute) :-
	viocond_lits(VioCond, LitList),
	viocond_formula(VioCond, Formula),
	%write('\tStart Refute: '),
	%nl,
	%print_litlist(LitList),
	%nl,
	%
	extract_builtin(LitList, BuiltinList),
	conj_to_and(BuiltinList, BuiltinFormula),
	%
	%write('\tBuiltIn: '),
	%print_formula(BuiltinFormula),
	%nl,
	refute_violation_cond_cases(LitList, Formula, BuiltinFormula, Refute).

%------------------------------------------------------------------------------
% refute_violation_cond_cases(+LitList, +Formula, +BuiltinFormula, -Refute):
%------------------------------------------------------------------------------

refute_violation_cond_cases(LitList, Formula, BuiltinFormula, Refute) :-
	refute_violation_cond0(LitList, Formula, BuiltinFormula, Refute),
	!.

refute_violation_cond_cases(LitList, Formula, BuiltinFormula, Refute) :-
	refute_violation_cond1(LitList, Formula, BuiltinFormula, Refute),
	!.

%------------------------------------------------------------------------------
% refute_violation_cond0(+LitList, +Formula, +BuiltinFormula, -RefuteReason):
%------------------------------------------------------------------------------

% This checks whether the BuiltinFormula (derived from LitList)
% together with Formula (from the violation condition inherited from constraint)
% is already inconsistent.

refute_violation_cond0(_LitList, Formula, BuiltinFormula, Refute) :-
	VFormula0 = and(BuiltinFormula,Formula),
	eval_obvious(VFormula0, VFormula1),
	normalize_and(VFormula1, VFormula),
	is_inconsistent(VFormula),
	make_refute0(VFormula, Refute).

%------------------------------------------------------------------------------
% refute_violation_cond1(+LitList, +Formula, +BuiltinFormula, -RefuteReason):
%------------------------------------------------------------------------------

% This checks whether the violation condition "LitList and Formula"
% can be refuted with a single application of a constraint,
% namely constraint ID, matched with Literals Lit1 and Lit2 from LitList.
% Note that more than one application of a constraint might be needed,
% but this predicate checks only a single application.
% Therefore, the current prototype is incomplete.
% However, if the violation condition can be refuted,
% one can be sure that a constraint violation cannot occur in the situation
% described by the violation condition.

refute_violation_cond1(LitList, Formula, BuiltinFormula, Refute) :-
	init_unique_ver(3),
	unique_ver(Ver), % This will be 3.
	list_member(LitB1, LitList),
	constraint_with_fresh_var(Ver, ID, LitA1, LitA2, ConstraintFormula),
	unify_lit(LitA1, LitB1, Subst1),
	list_member(LitB2, LitList),
	LitB2 \= LitB1,
	unify_lit(LitA2, LitB2, Subst1, Subst),
	%
	dbg_out_rt_match(ID, LitB1, LitB2),
	%
	match_cond(LitB1, Subst, Cond1),
	%write('\tCond1: '),
	%print_formula(Cond1),
	%nl,
	%
	match_cond(LitB2, Subst, Cond2),
	%write('\tCond2: '),
	%print_formula(Cond2),
	%nl,
	%
	do_subst_formula(ConstraintFormula, Subst, Cond3),
	%write('\tCond3: '),
	%print_formula(Cond3),
	%nl,
	normalize_and(and(Cond1, and(Cond2, Cond3)), MatchCond),
	NotMatchCond = not(MatchCond),
	VFormula0 = and(and(BuiltinFormula,Formula),NotMatchCond),
	eval_obvious(VFormula0, VFormula1),
	normalize_and(VFormula1, VFormula),
	is_inconsistent(VFormula),
	make_refute1(LitB1, LitB2, ID, VFormula, Refute).

% It is important that the literals from the violation condition
% are the second literal in the call to the unification,
% because variable-to-variable bindings are done from first to second literal,
% and we do not want new variables in the extended violation condition.

%------------------------------------------------------------------------------
% dbg_out_rt_match(+ID, +Lit1, +Lit2):
%------------------------------------------------------------------------------

% Optional debug output for refutation try.

dbg_out_rt_match(ID, Lit1, Lit2) :-
	opt_drt,
	!,
	write('\tTrying refutation with Constraint: ('),
	write(ID),
	write(')'),
	nl,
	write('\t\tLit1:  '),
	print_lit(Lit1),
	nl,
	write('\t\tLit2:  '),
	print_lit(Lit2),
	nl,
	nl.

dbg_out_rt_match(_ID, _Lit1, _Lit2).

%------------------------------------------------------------------------------
% match_cond(+Lit, +Subst, -Cond):
%------------------------------------------------------------------------------

match_cond(Lit, Subst, Cond) :-
	Lit =..[_Pred|Args],
	match_cond_list(Args, Subst, Cond).

% match_cond_list(+TermList, +Subst, -Cond):

match_cond_list([], _Subst, true).

match_cond_list([Term], Subst, eq(Term,TermOut)) :-
	do_subst_term(Term, Subst, TermOut).

match_cond_list([Term1,Term2|Rest], Subst, and(eq(Term1,TermOut1),RestCond)) :-
	do_subst_term(Term1, Subst, TermOut1),
	match_cond_list([Term2|Rest], Subst, RestCond).

%------------------------------------------------------------------------------
% extract_builtin(+Body, -BuiltinList):
%------------------------------------------------------------------------------

extract_builtin([], []).

extract_builtin([succ(Term1,Term2)|Rest], [succ(Term1,Term2)|BuiltinList]) :-
	!,
	extract_builtin(Rest, BuiltinList).

extract_builtin([plus_lt(T1,T2,T3)|Rest], [plus_lt(T1,T2,T3)|BuiltinList]) :-
	!,
	extract_builtin(Rest, BuiltinList).

extract_builtin([plus_ge(T1,T2,T3)|Rest], [plus_ge(T1,T2,T3)|BuiltinList]) :-
	!,
	extract_builtin(Rest, BuiltinList).

extract_builtin([ret_millis(T1,T2)|Rest], [ret_millis(T1,T2)|BuiltinList]) :-
	!,
	extract_builtin(Rest, BuiltinList).

extract_builtin([_|Rest], BuiltinList) :-
	extract_builtin(Rest, BuiltinList).


%******************************************************************************
% Consistency Checker:
%******************************************************************************


%==============================================================================
% Consistency Checker (Incomplete Detection of Inconsistencies):
%==============================================================================


%------------------------------------------------------------------------------
% is_inconsistent(+Formula):
%------------------------------------------------------------------------------

is_inconsistent(Formula) :-
	eval_obvious(Formula, Simplified),
	dbg_out_cc_start(Simplified),
	is_inconsistent1(Simplified),
	!,
	dbg_out_cc_success.

is_inconsistent(_Formula) :-
	dbg_out_cc_failure,
	fail.

%------------------------------------------------------------------------------
% is_inconsistent1(+Formula):
%------------------------------------------------------------------------------

% This is only to handle the trival case "false" (after simplification):

is_inconsistent1(false) :-
	!.

is_inconsistent1(Formula) :-
	eliminate_not(Formula,FormulaWithoutNot),
	%write('Not eliminated: '),
	%print_formula(FormulaWithoutNot),
	%nl,
	dnf(FormulaWithoutNot, DNF),
	%write('DNF: '),
	%print_dnf(DNF),
	%nl,
	is_inconsistent_dnf(DNF).

%------------------------------------------------------------------------------
% is_inconsistent_dnf(+DNF):
%------------------------------------------------------------------------------

is_inconsistent_dnf([]).

is_inconsistent_dnf([Conj|Rest]) :-
	is_inconsistent_conj(Conj),
	is_inconsistent_dnf(Rest).

%------------------------------------------------------------------------------
% dbg_out_cc_start(+Formula):
%------------------------------------------------------------------------------

dbg_out_cc_start(Formula) :-
	opt_dcc,
	!,
	write('\tInconsistency Check: '),
	print_formula(Formula),
	nl.

dbg_out_cc_start(_).

%------------------------------------------------------------------------------
% dbg_out_cc_success:
%------------------------------------------------------------------------------

dbg_out_cc_success :-
	opt_dcc,
	!,
	write('\tINCONSISTENT !'),
	nl,
	nl.

dbg_out_cc_success.

%------------------------------------------------------------------------------
% dbg_out_cc_failure:
%------------------------------------------------------------------------------

dbg_out_cc_failure :-
	opt_dcc,
	!,
	write('\tFailed to prove inconsistency.'),
	nl,
	nl.

dbg_out_cc_failure.

%==============================================================================
% Consistency Checker for Conjunctions:
%==============================================================================


%------------------------------------------------------------------------------
% is_inconsistent_conj(+AtomicFormulaList):
%------------------------------------------------------------------------------

is_inconsistent_conj(Conj) :-
	conj_contains_false(Conj),
	!.

is_inconsistent_conj(Conj) :-
	dbg_out_cc_conj(Conj),
	derive_all(Conj, AllConsequences),
	dbg_out_cc_derived(AllConsequences),
	conj_contains_false(AllConsequences).

%------------------------------------------------------------------------------
% dbg_out_cc_conj(+Conj):
%------------------------------------------------------------------------------

dbg_out_cc_conj(Conj) :-
	opt_dcc,
	!,
	write('\tCheck Conj.: '),
	print_conj(Conj),
	nl.

dbg_out_cc_conj(_).

%------------------------------------------------------------------------------
% dbg_out_cc_derived(+Conj):
%------------------------------------------------------------------------------

dbg_out_cc_derived(Conj) :-
	opt_dcc,
	!,
	conj_length(Conj, Length),
	write('\tDerived: '),
	write(Length),
	write(' Atomic Formulas.'),
	nl,
	print_conj_prover(Conj),
	nl.

dbg_out_cc_derived(_).

%------------------------------------------------------------------------------
% derive_all(+AtomicFormulaList, -ExtendedAtomicFormulaList):
%------------------------------------------------------------------------------

derive_all(Conj, AllConsequences) :-
	derive(Conj, AtomicFormula),
	\+ list_member(AtomicFormula, Conj),
	!,
	derive_all_break([AtomicFormula|Conj], AllConsequences).

derive_all(Conj, Conj).

% We can stop once false is derived:

derive_all_break([false|Conj], [false|Conj]) :-
	!.

derive_all_break(Conj, AllConsequences) :-
	derive_all(Conj, AllConsequences).

%------------------------------------------------------------------------------
% derive(+AtomicFormulaList, -AtomicFormula):
%------------------------------------------------------------------------------

derive(Conj, Consequence) :-
	list_member(AtomicFormula, Conj),
	consequence1(AtomicFormula, Consequence).

derive(Conj, Consequence) :-
	list_member(AtomicFormula1, Conj),
	list_member(AtomicFormula2, Conj),
	consequence2(AtomicFormula1, AtomicFormula2, Consequence).

derive(Conj, Consequence) :-
	list_member(AtomicFormula1, Conj),
	list_member(AtomicFormula2, Conj),
	list_member(AtomicFormula3, Conj),
	consequence3(AtomicFormula1, AtomicFormula2, AtomicFormula3,
			Consequence).

%derive(Conj, Consequence) :-
%	list_member(AtomicFormula1, Conj),
%	list_member(AtomicFormula2, Conj),
%	list_member(AtomicFormula3, Conj),
%	list_member(AtomicFormula4, Conj),
%	consequence4(AtomicFormula1, AtomicFormula2, AtomicFormula3,
%			AtomicFormula4, Consequence).

%------------------------------------------------------------------------------
% consequence1(+AtomicFormulaIn, -AtomicFormulaOut):
%------------------------------------------------------------------------------

% The consequence true is not interesting, but false is very interesting.
% Note that here, atomic formulas can also be built-in literals.

consequence1(eq(X,Y), eq(Y,X)) :-
	X \= Y.

consequence1(eq(Const1,Const2), false) :-
	is_const(Const1),
	is_const(Const2),
	Const1 \= Const2.

consequence1(ne(X,Y), ne(Y,X)).

consequence1(ne(Term,Term), false).

consequence1(succ(X,Y), ne(X,Y)).

consequence1(succ(0,Term), eq(Term,1)) :-
	Term \= 1.

consequence1(succ(Term,1), eq(Term,0)) :-
	Term \= 0.

consequence1(succ(_,0), false).

consequence1(ret_millis(0,_), false).

consequence1(lt(X,Y), ne(X,Y)).

consequence1(lt(X,Y), gt(Y,X)).

consequence1(lt(X,Y), le(X,Y)).

consequence1(le(X,Y), ge(Y,X)).

consequence1(ge(X,Y), le(Y,X)).

consequence1(gt(X,Y), ne(X,Y)).

consequence1(gt(X,Y), lt(Y,X)).

consequence1(gt(X,Y), ge(X,Y)).

% X + Y < Z. We know that the delay Y >= 0 and the start time X >= 0:
consequence1(plus_lt(X,_Y,Z), lt(X,Z)).

consequence1(plus_lt(_X,Y,Z), lt(Y,Z)).

% X + Y >= Z. We can only derive X>=0 and Y>=0.
% So far, all our numbers are non-negative, so this does not help much.

% This handles cases with two constants (TODO: There is some duplicate work):
consequence1(F, false) :-
	eval_obvious_atomic(F, Result),
	Result = false.

%------------------------------------------------------------------------------
% consequence2(+AtomicFormulaIn1, +AtomicFormulaIn2, -AtomicFormulaOut):
%------------------------------------------------------------------------------

% Equalities of the type X=X are not useful.

% Transitivity of eq:

consequence2(eq(X,Y), eq(Y,Z), eq(X,Z)) :-
	X \= Z.

% Can replace equals in ne:

consequence2(ne(X,Y), eq(Y,Y1), ne(X,Y1)).

consequence2(ne(X,Y), eq(X,X1), ne(X1,Y)).

% lt:

consequence2(lt(X,Y), eq(Y,Z), lt(X,Z)).

consequence2(lt(X,Y), le(Y,Z), lt(X,Z)).

consequence2(eq(X,Y), lt(Y,Z), lt(X,Z)).

consequence2(le(X,Y), lt(Y,Z), lt(X,Z)).

% le:

consequence2(le(X,Y), eq(Y,Z), le(X,Z)).

consequence2(le(X,Y), le(Y,Z), le(X,Z)).

consequence2(eq(X,Y), le(Y,Z), le(X,Z)).

% gt:

consequence2(gt(X,Y), eq(Y,Z), gt(X,Z)).

consequence2(gt(X,Y), ge(Y,Z), gt(X,Z)).

consequence2(eq(X,Y), gt(Y,Z), gt(X,Z)).

consequence2(ge(X,Y), gt(Y,Z), gt(X,Z)).

% ge:

consequence2(ge(X,Y), eq(Y,Z), ge(X,Z)).

consequence2(ge(X,Y), ge(Y,Z), ge(X,Z)).

consequence2(eq(X,Y), ge(Y,Z), ge(X,Z)).

% plus_lt (X+Y<Z):

consequence2(plus_lt(X,Y,Z), eq(X,X1), plus_lt(X1,Y,Z)).

consequence2(plus_lt(X,Y,Z), eq(Y,Y1), plus_lt(X,Y1,Z)).

consequence2(plus_lt(X,Y,Z), eq(Z,Z1), plus_lt(X,Y,Z1)).

consequence2(plus_lt(X,Y,Z), le(X1,X), plus_lt(X1,Y,Z)).

consequence2(plus_lt(X,Y,Z), le(Y1,Y), plus_lt(X,Y1,Z)).

consequence2(plus_lt(X,Y,Z), le(Z,Z1), plus_lt(X,Y,Z1)).

% plus_ge (X+Y>=Z):

consequence2(plus_ge(X,Y,Z), eq(X,X1), plus_ge(X1,Y,Z)).

consequence2(plus_ge(X,Y,Z), eq(Y,Y1), plus_ge(X,Y1,Z)).

consequence2(plus_ge(X,Y,Z), eq(Z,Z1), plus_ge(X,Y,Z1)).

consequence2(plus_ge(X,Y,Z), ge(X1,X), plus_ge(X1,Y,Z)).

consequence2(plus_ge(X,Y,Z), ge(Y1,Y), plus_ge(X,Y1,Z)).

consequence2(plus_ge(X,Y,Z), ge(Z,Z1), plus_ge(X,Y,Z1)).

% Conflict of plus_lt and plus_ge:

consequence2(plus_lt(X,Y,Z), plus_ge(X,Y,Z), false).

% succ:

consequence2(succ(X,Y), succ(X1,Y), eq(X,X1)) :-
	X \= X1.

consequence2(succ(X,Y), succ(X,Y1), eq(Y,Y1)) :-
	Y \= Y1.

consequence2(succ(X,Y), eq(X,X1), succ(X1,Y)).

consequence2(succ(X,Y), eq(Y,Y1), succ(X,Y1)).

% ret_millis:

consequence2(ret_millis(X,_), eq(X,0), false).

consequence2(ret_millis(X,Y), ret_millis(X,Y1), eq(Y,Y1)) :-
	Y \= Y1.

consequence2(ret_millis(X,Y), eq(X,X1), ret_millis(X1,Y)).

consequence2(ret_millis(X,Y), eq(Y,Y1), ret_millis(X,Y1)).

%------------------------------------------------------------------------------
% consequence3(+AtomicFIn1, +AtomicFIn2, +AtomicFIn3, -AtomicFormulaOut):
%------------------------------------------------------------------------------

consequence3(succ(X,Y), succ(X1,Y1), ne(X,X1),
		ne(Y,Y1)).

consequence3(succ(X,Y), succ(X1,Y1), ne(Y,Y1),
		ne(X,X1)).

consequence3(ret_millis(X,Y), ret_millis(X1,Y1), ne(Y,Y1),
		ne(X,X1)).

%------------------------------------------------------------------------------
% consequence4(+AtomicFIn1, +AtomicFIn2, +AtomicFIn3, +AtomicFIn4, -AtomicFOut):
%------------------------------------------------------------------------------

%consequence4(plus_lt(X1,Y1,Z), plus_ge(X2,Y2,Z), eq(X1,X2), eq(Y1,Y2), false).

%==============================================================================
% Tests of Consistency Checker:
%==============================================================================


%------------------------------------------------------------------------------
% Tests of the Inconsistency Checker:
%------------------------------------------------------------------------------

test_inconsistency :-
	test_inconsistency_pos,
	test_inconsistency_neg,
	nl,
	write('All tests successful!'),
	nl.

% test_inconsistency_pos:

test_inconsistency_pos :-
	write('Test1: X=Y, 1=2, X=Z'),
	nl,
	is_inconsistent_conj([eq(v('X'),v('Y')),eq(1,2),eq(v('X'),v('Z'))]),
	nl,
	write('Test2: 1=X, X=2'),
	nl,
	is_inconsistent_conj([eq(1,v('X')),eq(v('X'),2)]),
	nl,
	write('Test3: X=Y, A=B, Y=Z, X<>Z'),
	nl,
	Conj3=[eq(v('X'),v('Y')), eq(v('A'),v('B')), eq(v('Y'),v('Z')),
		ne(v('X'),v('Z'))],
	is_inconsistent_conj(Conj3),
	nl,
	!.

test_inconsistency_pos :-
	write('*** TEST FAILED ***'),
	nl.

% test_inconsistency_neg:

test_inconsistency_neg :-
	write('Test4: X=Y, 1=Z, X=Z, 1<>2 (consistent)'),
	nl,
	Conj=[eq(v('X'),v('Y')), eq(1,v('Z')), eq(v('X'),v('Z')), ne(1,2)],
	is_inconsistent_conj(Conj),
	write('*** TEST FAILED ***'),
	!,
	fail.

test_inconsistency_neg.


%******************************************************************************
% Another Approach for Refuting Violation Conds: Reachable States of Predicates
%******************************************************************************

% This is work in progress (unfinished, not yet used).


%==============================================================================
% Precomputation of Predicates in States:
%==============================================================================

botup_0(PredsIn, PredsOut) :-
	possible(PredsIn, Pred),
	\+ list_member(Pred, PredsIn),
	!,
	botup_0([Pred|PredsIn], PredsOut).

botup_0(Preds, Preds).

possible(PredsIn, Pred) :-
	input_rule(rule(_No, Head, BodyList)),
	can_be_true(BodyList, PredsIn),
	lit_pred(Head, Pred),
	lit_statearg(Head, StateArg),
	statearg_permits_0(StateArg).

% can_be_true(+BodyList, +TruePreds):

can_be_true([], _).

can_be_true([Lit|BodyList], TruePreds) :-
	lit_pred(Lit, Pred),
	list_member(Pred, TruePreds),
	!,
	can_be_true(BodyList, TruePreds).

% statearg_permits_0(+Arg):

statearg_permits_0(Arg) :-
	Arg \= 1.


%******************************************************************************
% Overall Control, Interaction with User, Main program:
%******************************************************************************


%==============================================================================
% Output All Data:
%==============================================================================


%------------------------------------------------------------------------------
% print_all_rules:
%------------------------------------------------------------------------------

print_all_rules :-
	input_rule(Rule),
	print_rule(Rule),
	nl,
	fail.

print_all_rules.

%------------------------------------------------------------------------------
% print_all_constraints:
%------------------------------------------------------------------------------

print_all_constraints :-
	input_constraint(Constraint),
	print_constraint(Constraint),
	nl,
	fail.

print_all_constraints.


%==============================================================================
% Main Work:
%==============================================================================


%------------------------------------------------------------------------------
% compute_violation_conds(-VCList):
%------------------------------------------------------------------------------

compute_violation_conds(VCList) :-
	findall(VioCond, violation_cond(VioCond), VCList).

%------------------------------------------------------------------------------
% check_violation_conds(+VCondsList, +VCStatIn, -VCStatOut):
%------------------------------------------------------------------------------

check_violation_conds([], VCStat, VCStat).

check_violation_conds([VioCond|Rest], VCStatIn, VCStatOut) :-
%	write('Checking violation condition ...'),
	nl,
	print_viocond(VioCond),
	check_violation_cond(VioCond, VCStatIn, VCStat),
	check_violation_conds(Rest, VCStat, VCStatOut).

%------------------------------------------------------------------------------
% check_violation_cond(+VioCond, +VCStatIn, -VCStatOut):
%------------------------------------------------------------------------------

check_violation_cond(VioCond, StatIn, StatOut) :-
	refute_violation_cond(VioCond, Refute),
	!,
	write('\tRefuted: '),
	nl,
	print_refute(Refute),
	nl,
	inc_refuted(StatIn, StatOut).

check_violation_cond(VioCond, StatIn, StatOut) :-
	write('\t*** CANNOT REFUTE! (but current prototype is incomplete.)'),
	nl,
	inc_nonrefuted(StatIn, VioCond, StatOut).

%==============================================================================
% Minimal User Interface:
%==============================================================================

%------------------------------------------------------------------------------
% show: Show loaded rules and constraints.
%------------------------------------------------------------------------------

show :-
	nl,
	write('Rules:'),
	nl,
	write('====='),
	nl,
	nl,
	print_all_rules,
	nl,
	write('Constraints:'),
	nl,
	write('==========='),
	nl,
	nl,
	print_all_constraints,
	nl.

%------------------------------------------------------------------------------
% Main Check of Constraints:
%------------------------------------------------------------------------------

% Note that the input (rules and constraints) must have been read before.

ctest :-
	show,
	nl,
%	write('Violation Conditions:'),
%	nl,
%	write('===================='),
%	nl,
%	nl,
%	compute_violation_conds(VCondsList),
%	print_violation_conds(VCondsList),
%	nl,
%	nl,
	write('Checking Violation Conditions:'),
	nl,
	write('============================='),
	nl,
	nl,
	compute_violation_conds(VCList),
	init_vcstat(EmptyVStat),
	check_violation_conds(VCList, EmptyVStat, VStat),
	nl,
	print_vcstat_long(VStat),
	nl.

%------------------------------------------------------------------------------
% Example:
%------------------------------------------------------------------------------

example :-
	blink0,
	ctest.

%------------------------------------------------------------------------------
% End program for non Prolog users:
%------------------------------------------------------------------------------

quit :-
	halt.

%------------------------------------------------------------------------------
% Reset all dynamic predicates:
%------------------------------------------------------------------------------

clear :-
	clear_opt,
	clear_input,
	clear_err.

%------------------------------------------------------------------------------
% Help:
%------------------------------------------------------------------------------

h :-
	write('You can use the following predicates: '),
	nl,
	write('- load(\'File\'): Load Microlog rules and constraints. '),
	nl,
	write('- blink0:       Load data of Blink example from paper.'),
	nl,
	write('- ctest:        Try to prove constraints from currently '),
	write('loaded example.'),
	nl,
	write('- example:      Does blink0 and ctest, i.e. runs the example '),
	write('from the paper.'),
	nl,
	write('- show:         Show loaded rules and constraints.'),
	nl,
	write('- show_opt:     Show list of all options.'),
	nl,
	write('- set_opt(o):   Set option(s) o.'),
	nl,
	write('- del_opt(o):   Unset option(s) o.'),
	nl,
	write('- clear_opt:    Reset all options back to normal.'),
	nl,
	write('- clear:        Delete loaded program, options, ... '),
	write('(fresh start).'),
	nl,
	write('- quit:         Leave program (stop Prolog interpreter).'),
	nl,
	nl,
	write('In Prolog, each input line must be ended with '),
	write('\'.\' (full stop).'),
	nl,
	nl,
	write('The prototype is being actively developed '),
	write('(last update: April 21, 2020),'),
	nl,
	write('a version with a parser for input files will be ready '),
	write('in a few days.'),
	nl,
	nl.

%------------------------------------------------------------------------------
% My current test goal:
%------------------------------------------------------------------------------

r :-
	load(blink0, t).

%------------------------------------------------------------------------------
% Main Program:
%------------------------------------------------------------------------------

init :-
	write('Welcome to the prototype '),
	write('of the Microlog constraint checker (Ver. 0.4).'),
	nl,
	write('- To run the example, enter: example. '),
	write('(Prolog requires the full stop \'.\')'),
	nl,
	write('- To get more help, enter: h.'),
	nl,
	write('- To leave Prolog, enter: halt.'),
	nl,
	nl,
	clear.

:- initialization(init).

