%%% Última revisión: 24/06/2003

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%											%%%
%%%		answerSAT.pl							%%%
%%%											%%%
%%%			assert_signature/1					%%%
%%%			answerSAT/1							%%%
%%%											%%%
%%%											%%%
%%%											%%%
%%%											%%%
%%%											%%%
%%%											%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- use_module(library(terms)).

%%%
%%% Declarations
%%%

%%% Answer representation
%%%
%%%	It is only necessary to represent the disequational part.
%%%	The disequational part is represented by a list of elements
%%%		cd/3, and each element cd/3 is a tuple of the form
%%%		(W,LV,T) where:
%%%		W:	existentially quantified variable of the
%%%				disequation
%%%		LV:	universally quantified variable list of the
%%%				disequation
%%%		T:	term of the disequation

%%% Intermediate information storage:
%%%
%%%	sat/3:
%%%		function that stores the domain of a existentially
%%%			quantified variable during the first step
%%%		P1: existentially quantified variable W
%%%		P2: Dom(W)
%%%		P3: name assigned to W (only used for output)
%%%
%%%	dis/4:
%%%		function used by the CHR handler that represents a
%%%			universally quantified collapsing disequation
%%%		P1: variable W of the disequation
%%%		P2: corresponding name of the variable W
%%%		P3: list of universally quantified variables of the term
%%%			of the disequation
%%%		P4: term of the disequation
%%%
%%%	diseq/3:
%%%		function used by the CHR handler that represents a
%%%			collapsing disequation
%%%		P1: variable W of the disequation
%%%		P2: corresponding name of the variable W
%%%		P4: term of the disequation
%%%
%%%	eq/3:
%%%		function used by the CHR handler that represents a
%%%			collapsing equation
%%%		P1: variable W of the sequation
%%%		P2: corresponding name of the variable W
%%%		P4: term of the equation

%%% Signature representation
%%% 
%%%	The signature is represented like a list of element (N,A) where
%%%		N is the name of the function and A is its arity. The
%%%		signature is stored by using the dinamic function
%%%		answer_sig/1.

:- dynamic answer_sig/1.

%%%
%%% End of declarations
%%%

%%%
%%%	sat CHR handler code
%%%

:- use_module(library(chr)).

handler sat.

option(debug_compile,on).

constraints dis/4, diseq/3, eq/3.

rules uqdiseq, nuqdiseq.

% Regla 1 uqdiseq: universally quantified collapsing disequation
uqdiseq	@	eq(W,N,TE) \ dis(W,N,LW,TD)	<=>	
							unify_dis(TE,TD,LW).

% Regla 2 nuqdiseq: not universally quantified collapsing
%				disequation
nuqdiseq	@	eq(W,N,TE) \ diseq(W,N,TD)	<=> TE == TD | false.

%%% unify_dis(in P1, in P2, in P3)
%%%	P1: term T1 to be unified
%%%	P2: term T2 to be unified
%%%	P3: list existentially quantified variables LW of the term T2

unify_dis(T1,T2,LW):-
		copy_term((LW,T2),(NLW,NT2)),
		unify_with_occurs_check(T1,NT2),
		!,
		add_dis(LW,NLW,ND),
		ND.
unify_dis(_,_,_).

%%% add_dis(in P1, in P2, out P3)
%%%	P1: list of existentially quantified variables LW (*)
%%%	P2: list terms LT
%%%	P3: disjunction of disequations obtained from unifying the
%%%		disequation term with the currently assigned term to the
%%%		disequation variable
%%%	(*) also terms

add_dis([],[],false).
add_dis([(W,N)|RW],[(T,N)|RT],(diseq(W,N,T);ND)):-
		var(W),
		!,
		add_dis(RW,RT,ND).
add_dis([_|LW],[_|LT],ND):-
		add_dis(LW,LT,ND).

%%%
%%%	End of sat CHR Handler code
%%%

%%% assert_signature(in P1)
%%%	P1: signature S
%%%	Action: to stablish the signature to be used by answerSAT
%%%			The signature is represented by a list of tuples
%%%			(N,A) where:
%%%				N: function name
%%%				A: function arity
%%%			The signature is stored in answer_sig/1

assert_signature(_):-
		retract((answer_sig(_))),
		fail.
assert_signature(S):-
		asserta((answer_sig(S))).

%%% answerSAT(in P1)
%%%	P1: disequational part of an answer R

answerSAT(false):-
		print('\n'),
		print('The answer false is not satisfiable'),
		print('\n').
answerSAT(true):-
		print('\n'),
		print('The answer true is satisfiable'),
		print('\n').
answerSAT(CI):-
		copy_term(CI,CI1),
		initialize_disequations(CI,CI1,0,LW1,LW2,NCI),
		print('\n'),
		print('The answer is:'),
		print('\n'),
		print_answer(NCI,''),
		print('\n'),
		print('\n'),
		initialize_domains(LW1,LW2,LD),
		print('The initial domains are: '),
		print('\n'),
		print_domain_list(LD),
		print('\n'),
		separate_disequations(NCI,NCI1,NCI2),
		print('First step'),
		print('\n'),
		print('=========='),
		print('\n'),
		print('\n'),
		print('The universally quantified collapsing '),
		print('disequations considered in the first step are: '),
		print('\n'),
		print_disequation_list(NCI1),
		print('\n'),
		answer_sig(S),
		sat_first_step(NCI1,S,LD,LD1),
		print('\n'),
		print('The domains after the first step are: '),
		print('\n'),
		print_domain_list(LD1),
		sat_second_step(LD1,NCI2),
		print('\n'),
		print('\n'),
		print('The answer is satisfiable'),
		!.
answerSAT(_):-
		print('\n'),
		print('\n'),
		print('The answer is not satisfiable').		

%%% initialize_disequations(in P1, in P2, in P3, out P4, out P5,
%%%					out P6)
%%%	P1: conjunction of disequations CI1 used to determine the
%%%		satisfiability of the answer
%%%	P2: conjunction of disequations CI2 for the output
%%%	P3: current counter for naming existentially quantified
%%%		variables
%%%	P4: list of existentially quantified variables of CI1
%%%	P5: list of existentially quantified variables (only used for
%%%		output)
%%%	P6: conjunction of disequations obtained from the two previous
%%%		one

initialize_disequations([],[],_,[],[],[]).
initialize_disequations([cd(W1,LV1,T1)|CI1],[cd(W2,LV2,T2)|CI2],N,
			[W1|LW1],[W2|LW2],[cd(W1,LV1,T1,W2,T2)|NCI]):-
		var(W2),
		!,
		N1 is N+1,
		number_codes(N1,L),
		atom_chars(W2,[87|L]),
		% 87: W ASCII code
		instantiate_variable_names(LV2,86,0),
		% 86: V ASCII code
		initialize_disequations(CI1,CI2,N1,LW1,LW2,NCI).
initialize_disequations([cd(W1,LV1,T1)|CI1],[cd(W2,LV2,T2)|CI2],N,
			LW1,LW2,[cd(W1,LV1,T1,W2,T2)|NCI]):-
		instantiate_variable_names(LV2,86,0),
		% 86: V ASCII code
		initialize_disequations(CI1,CI2,N,LW1,LW2,NCI).

%%% instantiate_variable_names(in P1, in P2, in P3)
%%%	P1: variable list LV  that is going to be instantiated with a
%%%		name (for the output)
%%%	P2: first letter of the variable name
%%%	P3: current index to assign a variale name

instantiate_variable_names([],_,_).
instantiate_variable_names([V|LV],N,I):-
		I1 is I+1,
		number_codes(I1,L),
		atom_chars(V,[N|L]),
		instantiate_variable_names(LV,N,I1).

%%% initialize_domains(in P1, in P2, out P3)
%%%	P1: existentially quantified variable list LW1
%%%	P2: existentially quantified variable list LW2 (only used for
%%%		output)
%%%	P3: initial domain list associated to each existentially
%%%		quantified variable

initialize_domains([],[],[]).
initialize_domains([W1|LW1],[W2|LW2],[sat(W1,D,W2)|LD]):-
		answer_sig(S),
		initialize_domain_values(S,D),
		initialize_domains(LW1,LW2,LD).

%%% initialize_domain_values(in P1, out P2)
%%%	P1: signature S of the answer
%%%	P2: signature S transformed to terms that are used to
%%%		initialize the domain values

initialize_domain_values([],[]).
initialize_domain_values([(N,A)|S],[F|NS]):-
		functor(F,N,A),
		initialize_domain_values(S,NS).

%%% separate_disequations(in P1, out P2, out P3)
%%%	P1: conjunction of disequations CI of the answer
%%%	P2: conjunction of disequations that hold the first step
%%%		condition
%%%	P3: conjunction of disequations that don't hold the first step
%%%		condition

separate_disequations([],[],[]).
separate_disequations([cd(W,LV,T,WE,TE)|CI],[cd(W,LV,T,WE,TE)|CI1],
										CI2):-
		sat_first_step_condition(LV,T,[]),
		!,
		separate_disequations(CI,CI1,CI2).
separate_disequations([cd(W,LV,T,WE,TE)|CI],CI1,
							[cd(W,LV,T,WE,TE)|CI2]):-
		separate_disequations(CI,CI1,CI2).

%%% sat_first_step_condition(in P1, in P2, out P3)
%%%	P1: universally quantified variable list LV
%%%	P2: term T
%%%	P3: variable list obtained from removing the variables that
%%%		occur in T from LV
%%%	Action:
%%%			success	if each variable in LV occurs at most
%%%						once in T
%%%			fail		if any variable in LV occurs more than
%%%						once in T

sat_first_step_condition(LV,T,NLV):-
		var(T),
		!,
		remove_variable_sat(LV,T,NLV).
sat_first_step_condition(LV,T,LV):-
		ground(T),
		!.
sat_first_step_condition(LV,T,NLV):-
		functor(T,_,N),
		sat_first_step_condition_sub(LV,T,0,N,NLV).

%%% remove_variable_sat(in P1, in P2, out P3)
%%%	P1: list of variables LV
%%%	P2: variable V
%%%	P3: list of variables obtained from removing V from LV
%%%	Action:
%%%		success	if the variable V occurs in LV
%%%		fail		if the variable V doesn't occur in LV

remove_variable_sat([V1|LV],V2,LV):-
		V1 == V2,
		!.
remove_variable_sat([V1|LV],V2,[V1|NLV]):-
		remove_variable_sat(LV,V2,NLV).

%%% sat_first_step_condition_sub(in P1, in P2, in P3, in P4, out P5)
%%%	P1: universally quantified variable list LV
%%%	P2: term T
%%%	P3: current subterm
%%%	P4: number of subterms
%%%	P5: variable list obtained from removing from LV the variables
%%%		that occur in T
%%%	Action:
%%%			success	if each variable in LV occurs at most
%%%						once in T
%%%			fail		if any variable in LV occurs more than
%%%						once in T

sat_first_step_condition_sub(LV,_,N,N,LV):-
		!.
sat_first_step_condition_sub(LV,T,M,N,NLV):-
		M1 is M+1,
		arg(M1,T,ST),
		sat_first_step_condition(LV,ST,LV1),
		sat_first_step_condition_sub(LV1,T,M1,N,NLV).

%%% sat_first_step(in P1, in P2, in P3, out P4)
%%%	P1: conjunction of disequations CI of the answer R
%%%	P2: signature S of the answer R
%%%	P3: intermediate information SI about the satisfiability of the
%%%		answer R represented by a list of sat/3 elements
%%%	P4: intermediate information about the satisfiability of the
%%%		answer R represented by a list of sat/3 elements after
%%%		adding to SI the information about the conjuncion of
%%%		disequations CI

sat_first_step([],_,SI,SI).
sat_first_step([I|CI],S,SI,NSI):-
		print('\n'),
		print('Current disequation: '),
		print_disequation(I),
		print('\n'),
		add_disequation_information(I,S,SI,SI1),
		sat_first_step(CI,S,SI1,NSI).

%%% add_disequation_information(in P1, in P2, in P3, out P4)
%%%	P1: disequation I
%%%	P2: signature S of the answer
%%%	P3: intermediate information SI about the satisfiability of the
%%%		answer R represented by a list of sat/3 elements
%%%	P4: intermediate information about the satisfiability of the
%%%		answer R represented by a list of sat/3 elements after
%%%		adding to SI the information about the disequation I

add_disequation_information(cd(W1,V,T,WE1,TE1),S,[sat(W2,C,WE2)|RSI],
									[SI|RSI]):-
		W1 == W2,
		!,
		update_disequation_information(cd(W1,V,T,WE1,TE1),S,
								sat(W2,C,WE2),SI).
add_disequation_information(I,S,[SI|RSI],[SI|NRSI]):-
		add_disequation_information(I,S,RSI,NRSI).

%%% update_disequation_information(in P1, in P2, in P3, out P4)
%%%	P1: disequation I
%%%	P2: signature S of the answer
%%%	P3: intermediate information SI about the satisfiability of the
%%%		answer R represented by a list of sat/3 elements
%%%	P4: intermediate information about the satisfiability of the
%%%		answer R represented by a list of sat/3 elements after
%%%		adding to SI the information about the disequation I

update_disequation_information(cd(W,_,T,WE,_),S,sat(W,C,WE),
									sat(W,NC,WE)):-
		print('Previous domain: '),
		print_domain(sat(W,C,WE)),
		update_domain_values(T,S,C,NC),
		print('Next domain: '),
		print_domain(sat(W,NC,WE)),
		print('\n'),
		NC \== [].
		
%%% update_domain_values(in P1, in P2, in P3, out P4)
%%%	P1: term T
%%%	P2: signature S
%%%	P3: domain of values D for the variable V
%%%	P4: domain of values for the variable V obtained from removing
%%%		from D the term T

update_domain_values(_,_,[],[]).
update_domain_values(T,S,[LT|RLT],NLT):-
		copy_term((T,LT),(T1,LT1)),
		T1 = LT1,
		!,
		get_new_domain_values(T,S,LT,NLT1),
		update_domain_values(T,S,RLT,NLT2),
		append_L(NLT2,NLT1,NLT).
update_domain_values(T,S,[LT|RLT],[LT|NRLT]):-
		update_domain_values(T,S,RLT,NRLT).

%%% get_new_domain_values(in P1, in P2, in P3, out P4)
%%%	P1: term T1
%%%	P2: signature S
%%%	P3: domain term T2
%%%	P4: new domain terms obtained from T1 and T2

get_new_domain_values(T,S,TC,LTC):-
		get_new_domain_values_sub(T,S,TC,0,LC),
		instantiate_domain_values(TC,LC,LTC).

%%% get_new_domain_values_sub(in P1, in P2, in P3, in P4, out P5)
%%%	P1: term T1
%%%	P2: signature S
%%%	P3: domain term T2
%%%	P4: current subterm
%%%	P5: list of terms (I,D) where I is the number of the subterm
%%%		and D is the set of domain values for I

get_new_domain_values_sub(T,S,TC,N,LSTC):-
		N1 is N+1,
		arg(N1,T,ST1),
		var(ST1),
		!,
		get_new_domain_values_sub(T,S,TC,N1,LSTC).
get_new_domain_values_sub(T,S,TC,N,[(N1,STC)|LSTC]):-
		N1 is N+1,
		arg(N1,T,ST1),
		arg(N1,TC,ST2),
		nonvar(ST1),
		nonvar(ST2),
		!,
		get_new_domain_values(ST1,S,ST2,STC),
		get_new_domain_values_sub(T,S,TC,N1,LSTC).
get_new_domain_values_sub(T,S,TC,N,[(N1,STC)|LSTC]):-
		N1 is N+1,
		arg(N1,T,ST1),
		arg(N1,TC,ST2),
		nonvar(ST1),
		var(ST2),
		!,
		get_complementary_terms(ST1,S,STC),
		get_new_domain_values_sub(T,S,TC,N1,LSTC).
get_new_domain_values_sub(_,_,_,_,[]).

%%% get_complementary_terms(in P1, in P2, out P3)
%%%	P1: term T
%%%	P2: signature S
%%%	P3: list of complementary terms to T

get_complementary_terms(T,S,LTC):-
		functor(T,N,A),
		functor(T1,N,A),
		initialize_domain_values_comp(S,(N,A),LTC1),
		get_complementary_terms_sub(T,S,0,LSC),
		instantiate_domain_values(T1,LSC,LTC2),
		append_L(LTC2,LTC1,LTC).

%%% initialize_domain_values_comp(in P1, in P2, out P3)
%%%	P1: signature S
%%%	P2: element E of the signature
%%%	P2: signature S transformed to terms that are used to
%%%		initialize the domain values without the element E

initialize_domain_values_comp([(N,A)|S],(N,A),LTC):-
		!,
		initialize_domain_values(S,LTC).
initialize_domain_values_comp([(N,A)|S],E,[TC|LTC]):-
		functor(TC,N,A),
		initialize_domain_values_comp(S,E,LTC).

%%% get_complementary_terms_sub(in P1, in P2, in P3, out P4)
%%%	P1: term T
%%%	P2: signature S
%%%	P3: current subterm
%%%	P4: list of terms (I,D) where I is the number of the subterm
%%%		and D is the set of domain values for I

get_complementary_terms_sub(T,_,N,[(N1,[])]):-
		N1 is N+1,
		arg(N1,T,ST),
		var(ST),
		!.
get_complementary_terms_sub(T,S,N,[(N1,STC)|LSTC]):-
		N1 is N+1,
		arg(N1,T,ST),
		!,
		get_complementary_terms(ST,S,STC),
		get_complementary_terms_sub(T,S,N1,LSTC).
get_complementary_terms_sub(_,_,_,[]).

%%% instantiate_domain_values(in P1, in P2, out P3)
%%%	P1: term T
%%%	P2: list of terms LT (I,D) where I is the number of the subterm
%%%		and D is the set of domain values for I
%%%	P3: domain terms obtained from T and LT

instantiate_domain_values(_,[],[]).
instantiate_domain_values(T1,[(_,[])|LP],LTC):-
		instantiate_domain_values(T1,LP,LTC).
instantiate_domain_values(T1,[(N,[T2|RT2])|LP],[NT|LTC]):-
		copy_term(T1,NT),
		arg(N,NT,T2),
		instantiate_domain_values(T1,[(N,RT2)|LP],LTC).

%%% sat_second_step(in P1, in P2)
%%%	P1: intermediate information SI about the satisfiability of the
%%%		answer R represented by a list of sat/3 elements
%%%	P2: conjunction of disequations DI that don't hold the first
%%%		step condition

sat_second_step(SI,CI):-
		sat_second_step_condition(SI,LV,LVE,LD,LDE),
		print('\n'),
		print('The variables with a finite domain are:'),
		print('\n'),
		print('Wf = '),
		print(LVE),
		print('\n'),
		(
		 (
		  LVE == []
		  );
		 (
		  LVE \== [],
		  print('\n'),
		  print('\n'),
		  print('Second step'),
		  print('\n'),
		  print('==========='),
		  print('\n'),
		  print('\n'),
		  print('The finite domains are: '),
		  print('\n'),
		  print_domain_list(LDE),
		  print('\n'),
		  get_second_step_disequations(LV,CI,NCI,NCIE),
		  print('The universally quantified collapsing '),
		  print('disequations considered in '),
		  print('the second step are: '),
		  print('\n'),
		  print_disequation_list(NCIE),
		  print('\n'),
		  get_second_step_assignment_value(LD,NCI)
		 )
		).

%%% sat_second_step_condition(in P1, out P2, out P3, out P4, out P5)
%%%	P1: intermediate information SI about the satisfiability of the
%%%		answer R represented by a list of sat/3 elements
%%%	P2: list of elements (V,VE) where V is the existentially
%%%		quantified variable and VE is the corresponding name
%%%	P3: list of existentially quantified variables with a finite
%%%		domain (only used for output)
%%%	P4: conjunction of disjunction of equations where each
%%%		disjunction represents the finite domain of a
%%%		existentially quantified variable
%%%	P5: finite domains (only used for output)

sat_second_step_condition([],[],[],true,[]).
sat_second_step_condition([sat(W,C,WE)|SI],[(W,WE)|LV],[WE|LVE],
							(D,LD),[sat(W,C,WE)|NSI]):-
		ground(C),
		!,
		second_step_domain(W,WE,C,D),
		sat_second_step_condition(SI,LV,LVE,LD,NSI).
sat_second_step_condition([_|SI],LV,LVE,LD,NSI):-
		sat_second_step_condition(SI,LV,LVE,LD,NSI).

%%% second_step_domain(in P1, in P2, in P3, out P4)
%%%	P1: existentially quantified variable W
%%%	P2: name of the existentially quantified variable W
%%%	P3: list of values of the domain of the variable W
%%%	P4: domain of the variable W represented by a disjunction of
%%%		equations

second_step_domain(_,_,[],false).
second_step_domain(W,WE,[C|LC],(eq(W,WE,C);D)):-
		second_step_domain(W,WE,LC,D).

%%% get_second_step_disequations(in P1, in P2, out P3, out P4)
%%%	P1: list of elements (V,VE) of existentially quantified
%%%		variables with a finite domain where V is the variable
%%%		and VE is the corresponding name
%%%	P2: conjunction of disequations CI
%%%	P3: conjunction of disequations obtained from CI after removing
%%%		the disequations that contain existentially quantified
%%%		variables not belonging to LV( (for computing purposes)
%%%	P4: conjuncion of disequations obtained from CI after removing
%%%		the disequations that contain existentially quantified
%%%		variables not belonging to LV (only for output purposes)

get_second_step_disequations(_,[],true,[]).
get_second_step_disequations(LV,[cd(W,V,T,WE,TE)|CI],
			(dis(W,WE,NLW,T),NCI1),[cd(W,V,T,WE,TE)|NCI2]):-
		occur_in_list_L((W,WE),LV),
		term_variables(T,LVT),
		delete_list_L(LVT,V,LW),
		disequation_second_step_condition(LV,LW),
		!,
		get_list_variables_names(LV,LW,NLW),
		get_second_step_disequations(LV,CI,NCI1,NCI2).
get_second_step_disequations(LV,[_|CI],NCI1,NCI2):-
		get_second_step_disequations(LV,CI,NCI1,NCI2).

%%% disequation_second_step_condition(in P1, in P2)
%%%	P1: list of existentially quantified variables with a finite
%%%		domain LW
%%%	P2: list of existentially quantified variables of the term LT
%%%	Action:
%%%			success	if each variable of LT occurs in LT
%%%			fail		if any variable of LT doesn't occur in
%%%						LW

disequation_second_step_condition(_,[]).
disequation_second_step_condition(LV,[V|LT]):-
		finite_domain_variable(V,LV),
		disequation_second_step_condition(LV,LT).

%%% finite_domain_variable(in P1, in P2)
%%%	P1: variable V
%%%	P2: list of existentially quantified variables with a finite
%%%		domain LV
%%%	Action:
%%%			success	if V occurs in LV
%%%			fail		if V doesn't occur in LV

finite_domain_variable(V1,[(V2,_)|_]):-
		V1 == V2,
		!.
finite_domain_variable(V,[_|LV]):-
		finite_domain_variable(V,LV).

%%% get_list_variables_names(in P1, in P2, out P3)
%%%	P1: list of existentially quantified variables with a finite
%%%		domain LW represented by a list of (V,VE) elements where
%%%		V is the variable and VE is the corresponding name
%%%	P2: list of existentially quantified variables with a finite
%%%		domain LV
%%%	P3: list of existentially quantified variables with a finite
%%%		domain obtained from joining to each variable of LV the
%%%		corresponding name

get_list_variables_names(_,[],[]).
get_list_variables_names(LW,[V|LV],[(V,VE)|NLW]):-
		get_variable_name(LW,V,VE),
		get_list_variables_names(LW,LV,NLW).

%%% get_variable_name(in P1, in P2, out P3)
%%%	P1: list of existentially quantified variables with a finite
%%%		domain LW represented by a list of (V,VE) elements where
%%%		V is the variable and VE is the corresponding name
%%%	P2: existentially quantified variable with a finite domain V
%%%	P3: corresponding name VE to V

get_variable_name([(V1,VE)|_],V2,VE):-
		V1 == V2,
		!.
get_variable_name([_|LW],V,VE):-
		get_variable_name(LW,V,VE).

%%% get_second_step_assignment_value(in P1, in P2)
%%%	P1: conjunction of disjunction of equations where each
%%%		disjunction represents the finite domain of a
%%%		existentially quantified variable
%%%	P2: conjunction of disequations for the second step

get_second_step_assignment_value(LD,CI):-
		(LD,CI),
		!,
		print('The assignment value is: '),
		print('\n'),
		findall_constraints(_,L),
		print_assignment_value(L).
get_second_step_assignment_value(_,_):-
		print('\n'),
		print('The assignment value does not exist'),
		print('\n'),
		fail.

%%%
%%% Output functions
%%%

%%% print_answer(in P1, in P2)
%%%	P1: conjunction of disequations CI of the answer
%%%	P2: auxiliary separator

print_answer([],_).
print_answer([cd(_,_,_,W,T)|CI],S):-
		print(S),
		print(W),
		print(' /= '),
		print(T),
		print_answer(CI,', ').

%%% print_domain_list(in P1)
%%%	P1: domain list of the answer

print_domain_list([]).
print_domain_list([D|LD]):-
		print_domain(D),
		print_domain_list(LD).

%%% print_domain(in P1)
%%%	P1: a domain of the answer

print_domain(sat(_,T,W)):-
		print('Dom('),
		print(W),
		print(') = '),
		copy_term(T,NT),
		term_variables(NT,LV),
		instantiate_no_name_variables(LV),
		print(NT),
		print('\n').

%%% instantiate_no_name_variables(in P1)
%%%	P1: variable list to be instantiated with '_' name

instantiate_no_name_variables([]).
instantiate_no_name_variables(['_'|LV]):-
		instantiate_no_name_variables(LV).

%%% print_disequation_list(in P1)
%%%	P1: disequation list CI of the answer

print_disequation_list([]).
print_disequation_list([I|CI]):-
		print_disequation(I),
		print_disequation_list(CI).

%%% print_disequation(in P1)
%%%	P1: a disequation of the answer

print_disequation(cd(_,_,_,W,T)):-
		print(W),
		print(' /= '),
		print(T),
		print('\n').

%%% print_assignment_value(in P1)
%%%	P1: assignment value list

print_assignment_value([]).
print_assignment_value([eq(_,VE,V)#Id|LV]):-
		!,
		print(VE),
		print(' = '),
		print(V),
		print('\n'),
		remove_constraint(Id),
		print_assignment_value(LV).
print_assignment_value([_#Id|LV]):-
		remove_constraint(Id),
		print_assignment_value(LV).

%%%
%%% End of output functions
%%%

%%%
%%% List operations
%%%

%%% append_L(in P1, in P2, out P3)
%%%	P1: list L1
%%%	P2: list L2
%%%	P3: list obtained from appending L2 to L1

append_L([],L,L).
append_L([E|L1],L2,[E|NL]):-
		append_L(L1,L2,NL).

%%% occur_in_list_L(in P1, in P2)
%%%	P1: element E
%%%	P2: list of elements L
%%%	Action:	success	if E occurs in L
%%%			fail		if E doesn't occur in L

occur_in_list_L(E1,[E2|_]):-
		E1 == E2,
		!.
occur_in_list_L(E,[_|L]):-
		occur_in_list_L(E,L).

%%% delete_list_L(in P1, in P2, out P3)
%%%	P1: list L1
%%%	P2: list L2
%%%	P3: list obtained from removing each element of L2 from L1

delete_list_L(L,[],L).
delete_list_L(L1,[E2|L2],NL):-
		delete_element_L(L1,E2,NL1),
		delete_list_L(NL1,L2,NL).

%%% delete_element_L(in P1, in P2, out P3)
%%%	P1: list L
%%%	P2: element E
%%%	P3: list obtained from removing the element E from L

delete_element_L([],_,[]).
delete_element_L([E1|L],E2,L):-
		E1 == E2,
		!.
delete_element_L([E1|L],E2,[E1|NL]):-
		delete_element_L(L,E2,NL).

%%%
%%% End of list operations
%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%											%%%
%%%		Auxiliary functions						%%%
%%%											%%%
%%%			initialize_disequations/6				%%%
%%%				instantiate_variable_names/3			%%%
%%%											%%%
%%%			initialize_domains/3					%%%
%%%				initialize_domains_values/2			%%%
%%%											%%%
%%%			separate_disequations/3					%%%
%%%				sat_first_step_condition/3			%%%
%%%					remove_variable_sat/3			%%%
%%%					sat_first_step_condition_sub/5	%%%
%%%											%%%
%%%			sat_first_step/4						%%%
%%%				add_disequation_information/4			%%%
%%%					update_disequation_information/4	%%%
%%%						update_domain_values/4		%%%
%%%							get_new_domain_values/4	%%%
%%%				get_new_domain_values_sub/5			%%%
%%%					get_complementary_terms/3		%%%
%%%					initialize_domain_values_comp/3	%%%
%%%					get_complementary_terms_sub/4		%%%
%%%					instantiate_domain_values/3		%%%
%%%											%%%
%%%			sat_second_step/2						%%%
%%%				sat_second_step_condition/5			%%%
%%%					second_step_domain/4			%%%
%%%				get_second_step_disequations/4		%%%
%%%					disequation_second_step_condition/2	%%%
%%%						finite_domain_variable/2	%%%
%%%					get_list_variable_names/3		%%%
%%%						get_variable_name/3		%%%
%%%				get_second_step_assignment_values/2		%%%
%%%											%%%
%%%											%%%
%%%		Output functions							%%%
%%%											%%%
%%%			print_answer/2						%%%
%%%											%%%
%%%			print_domain_list/1					%%%
%%%				print_domain/1					%%%
%%%					instantiate_no_name_variables/1	%%%
%%%											%%%
%%%			print_disequation_list/1				%%%
%%%				print_disequation/1				%%%
%%%											%%%
%%%			print_assignment_value/1				%%%
%%%											%%%
%%%											%%%
%%%		List_operations							%%%
%%%											%%%
%%%			append_L/3							%%%
%%%											%%%
%%%			occur_in_list_L/2						%%%
%%%											%%%
%%%			delete_list_L/3						%%%
%%%				delete_element_L/3				%%%
%%%											%%%
%%%											%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%