:- module(rrtrafo, [domain_restrict_clauses/3]).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% 
%%%% domain_restrict_clauses(+Cs, +Options, -Cs1)
%%%%
%%%%    Perform domain or range restriction transformations.
%%%%
%%%%    Cs and Cs1 are lists of tme clauses.
%%%%
%%%%    Options is a list of options:
%%%% 
%%%%      mode = Mode (default standard)
%%%% 
%%%%          Mode is 'standard' or 'rr':
%%%%      
%%%%          standard - Perform "domain restriction transformation":
%%%%      
%%%%                      - If the input problem
%%%%                         - contains a disjunctive clause (i.e. is non-Horn)
%%%%                         - and is not range restricted
%%%%                      - Then add
%%%%                         - clauses constructing the domain
%%%%                         - for each variable in a literal in a
%%%%                           disjunctive head
%%%%                           - add a domain literal to the body of that
%%%%                             clause
%%%%      
%%%%                      - This transformation is not a fixedpoint
%%%%                        since its result may not be range restricted.
%%%%      
%%%%                   - This transformation can be used for hyper tableau
%%%%                     systems which can handle variables in derived units
%%%%      
%%%%          rr       - Perform range restriction transformation:
%%%%      
%%%%                     - If the input is not range restricted
%%%%      	       - Then add
%%%%      	         - clauses constructing the domain
%%%%      		 - for each variable in a head literal that does not
%%%%      		   appear in a body literal
%%%%                         - add a domain literal to the body of that clause
%%%%      	        
%%%%      	     -  This transformation can be used for hyper tableau
%%%%                    systems and satchmo systems.
%%%%
%%%%		  ehyper	- Add clauses constructing the domain, regardless of 
%%%%					  input composition.
%%%%					- Do not perform any range restricting transformations.
%%%%
%%%%          suppress - Return the input without transformation
%%%%                 
%%%%
%%%%      fixed_dom = true|false (default false)
%%%%      
%%%%          - Do only generate domain construction clauses constants.
%%%%            This is obviously incomplete for theorem proving.
%%%%      	           
%%%%      input_dom = true|false (default false)
%%%%      
%%%%          - Add to the domain construction clauses facts for all
%%%%            compound ground terms in the input.
%%%% 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

domain_restrict_clauses(Cs, Options, Cs) :-
	get_option(mode, Options, suppress, standard),
	!.
domain_restrict_clauses(Cs, Options, Cs1) :-
	get_option(mode, Options, ehyper, standard),
	!,
	 \+ \+ (member(C1, Cs), is_disjunctive(C1),
			member(C2, Cs), \+ is_range_restricted(C2)) ->
	     (msg('Input has a disjunctive clause.'),
	     dom_clauses(Cs, TDCs),
		 append(TDCs, Cs, Cs1))
		;(Cs=Cs1).
domain_restrict_clauses(Cs, Options, Cs1) :-
	get_option(mode, Options, Mode, standard),
	(( \+ \+
	   (member(C2, Cs),
	    \+ is_range_restricted(C2),
	    numbervars(C2, 0, _),
	    msg('Input is not range restricted: ~q.', [C2]) ) ->
	   ( \+ \+ (member(C1, Cs), is_disjunctive(C1)) ->
	     msg('Input has a disjunctive clause.'),
	     true
	   ; Mode = rr ->
             msg('Input is horn but option rr is set.'),
	     true
	   ; msg('Input is Horn.') ->
	     fail
	   ) ->
	     true  
	 ; msg('Input is range restricted'),
	   fail
	 ) ->
	  ( Mode = rr ->
            msg('Applying range restriction transformation.'),	    
	    map_restrict_rr(Cs, Cs2)
	  ; msg('Applying hyper tableau domain restriction transformation.'),
	    map_restrict(Cs, Cs2)
	  ),
	  ( get_option(fixed_dom, Options, true, false) ->
	    dom_clauses_for_constants_only(Cs, DCs)
	  ; dom_clauses(Cs, DCs)
	  ),
          ( get_option(input_dom, Options, true, false) ->
	    dom_clauses_for_input_terms(Cs, TDCs),
	    append(TDCs, DCs, DCs1)
	  ; DCs1 = DCs
	  ),
	  append(DCs1, Cs2, Cs1)
	; msg('Not applying domain restriction transformation.'),
	  Cs1 = Cs
	).

get_option(Option, Options, Value, Default) :-
	( memberchk(Option=Value, Options) ->
	  true
	; Value = Default
	).

map_restrict([X|Xs], [X1|Xs1]) :-
	restrict(X, X1),
	map_restrict(Xs, Xs1).
map_restrict([], []).

restrict((H :- B), (H :- B1)) :-
        H = (_;_),
	!,
	free_variables(H, Vs),
	map_add_dom_lit(Vs, B, B1).
restrict(H, (H :- B)) :-
        H = (_;_),
	\+ ground(H),
	!,
	free_variables(H, Vs),
	map_dom_lit(Vs, B).
restrict(C, C).

map_restrict_rr([X|Xs], [X1|Xs1]) :-
	restrict_rr(X, X1),
	map_restrict_rr(Xs, Xs1).
map_restrict_rr([], []).

restrict_rr((H :- B), (H :- B1)) :-
        !,
	free_variables(H, VHs),
	free_variables(B, VBs),
	abs_subtract(VHs, VBs, Vs),
	map_add_dom_lit(Vs, B, B1).
restrict_rr(H, (H :- B)) :-
        \+ ground(H),
	!,
	free_variables(H, Vs),
	map_dom_lit(Vs, B).
restrict_rr(C, C).

abs_subtract([X|Xs], Ys, Zs) :-
	( member(Y, Ys),
	  X == Y ->
	  Zs = Zs1
	; Zs = [X|Zs1]
	),
	abs_subtract(Xs, Ys, Zs1).
abs_subtract([], _, []).

map_add_dom_lit([], B, B).
map_add_dom_lit([V|Vs], B, ('$krh_dom'(V), B1)) :-
	map_add_dom_lit(Vs, B, B1).

map_dom_lit([V], '$krh_dom'(V)).
map_dom_lit([V|Vs], ('$krh_dom'(V), B)) :-
	map_dom_lit(Vs, B).

dom_clauses(Cs, DCs) :-
	dom_clauses(Cs, false, DCs).

dom_clauses_for_constants_only(Cs, DCs) :-
	dom_clauses(Cs, true, DCs).

dom_clauses(Cs, ConstantsOnly, DCs) :-
	findall(F/N,
		cs_function_symbol(Cs, F, N),
		Funs),
	sort(Funs, Funs1),
	( memberchk(_/0, Funs1) ->
	  Funs2 = Funs1
	; msg('No constant symbol - adding one.'),
	  Funs2 = ['$krh_c'/0|Funs1]
	),
	( member(_/N, Funs2), N > 0 ->
	  true
	; msg('All symbols are constants.')
	),
	( ConstantsOnly = true ->
	  map_dom_clause_constants_only(Funs2, DCs)
	; map_dom_clause(Funs2, DCs)
	).

map_dom_clause([X|Xs], [X1|Xs1]) :-
	dom_clause(X, X1),
	map_dom_clause(Xs, Xs1).
map_dom_clause([], []).

map_dom_clause_constants_only([F/0|Xs], [X1|Xs1]) :-
	!,
	dom_clause(F/0, X1),
	map_dom_clause_constants_only(Xs, Xs1).
map_dom_clause_constants_only([_|Xs], Xs1) :-
	map_dom_clause_constants_only(Xs, Xs1).
map_dom_clause_constants_only([], []).

dom_clause(F/0, '$krh_dom'(F)) :-
	!.
dom_clause(F/N, ('$krh_dom'(F1) :- Body)) :-
        N > 0,
        functor(F1, F, N),
	map_dom_clause_arg(N, F1, Body).

map_dom_clause_arg(1, T, '$krh_dom'(V)) :-
	!,
	arg(1, T, V).
map_dom_clause_arg(N, T, ('$krh_dom'(V), B)) :-
	N > 1,
	arg(N, T, V),
	N1 is N - 1,
	map_dom_clause_arg(N1, T, B).

is_disjunctive((H :- _)) :-
        !,
	H = (_; _).
is_disjunctive((_ ; _)).

is_range_restricted((H :- B)) :-
        !,
        free_variables(H, HVs),
	free_variables(B, BVs),
	\+ ( member(V, HVs),
	     \+ ( member(V1, BVs), V == V1 ) ).
is_range_restricted(H) :-
	ground(H).

cs_function_symbol(Cs, F, N) :-
	member(C, Cs),
	( C = (H :- B) ->
	  ( fs(H, F, N)
	  ; fs(B, F, N)
	  )
	; fs(C, F, N)
	).

fs((A;B), F, N) :-
	!,
	( fs(A, F, N)
	; fs(B, F, N)
	).
fs((A,B), F, N) :-
	!,
	( fs(A, F, N)
	; fs(B, F, N)
	).
/* Special logical operators such as \+ and findall: */
fs(\+(A), F, N) :-
	!,
	fs(A, F, N).
fs(not(A), F, N) :-
	!,
	fs(A, F, N).
fs(findall(A,B,C), F, N) :-
	!,
	( fst(A, F, N)
	; fs(B, F, N)
	; fst(C, F, N)
	).
fs(A, F, N) :-
	functor(A, _, N1),
	map_fst(N1, A, F, N).

map_fst(N, T, F, M) :-
	N > 0,
	( arg(N, T, T1),
	  fst(T1, F, M)
	; N1 is N - 1,
	  map_fst(N1, T, F, M)
	).
fst(T, F, N) :-
	nonvar(T),
	functor(T, F1, N1),
	( F = F1, N = N1
	; map_fst(N1, T, F, N)
	).

msg(Msg) :-
	msg(Msg, []).
msg(Msg, Args) :-
	write(user_error, '% Pre: '),
	format(user_error, Msg, Args),
	nl(user_error),
	flush_output(user_error).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

dom_clauses_for_input_terms(Cs, DCs) :-
	findall(T, cs_term(Cs, T), Ts),
	sort(Ts, Ts1),
	map_term_dom_clause(Ts1, DCs).

term_dom_clause(T, '$krh_dom'(T)).

map_term_dom_clause([X|Xs], [X1|Xs1]) :-
	term_dom_clause(X, X1),
	map_term_dom_clause(Xs, Xs1).
map_term_dom_clause([], []).

% cs_term(Cs, T) :-
% 	member(C, Cs),
% 	( C = (H :- B) ->
% 	  ( tm(H, T)
% 	  ; tm(B, T)
% 	  )
% 	; tm(C, T)
% 	).

cs_term(Cs, T) :-
	member(C, Cs),
	( C = (H :- _) ->
	  tm(H, T)
	; tm(C, T)
	).

tm((A;B), T) :-
	!,
	( tm(A, T)
	; tm(B, T)
	).
tm((A,B), T) :-
	!,
	( tm(A, T)
	; tm(B, T)
	).
/* Special logical operators such as \+ and findall: */
tm(\+(A), T) :-
	!,
	tm(A, T).
tm(findall(A,B,C), T) :-
	!,
	( tmt(A, T)
	; tm(B, T)
	; tmt(C, T)
	).
tm(A, T) :-
	functor(A, _, N1),
	map_tmt(N1, A, T).

map_tmt(N, E, T) :-
	N > 0,
	( arg(N, E, T1),
	  tmt(T1, T)
	; N1 is N - 1,
	  map_tmt(N1, E, T)
	).

tmt(T, _) :-
	atomic(T),
	!,
	fail.
tmt(T, _) :-
	var(T),
	!,
	fail.
tmt(T, T) :-
	ground(T).
tmt(T, T1) :-
	functor(T, _, N1),
	map_tmt(N1, T, T1).