
/***************************************************************************
 *
 * Instantiation Schema - N. Peltier - 08-09 *
 *
 ***************************************************************************/

/***************************************************************************
* This program is a Prolog implementation of an instantiation schema 
* developed by M. Echenim and N. Peltier from the CAPP team (LIG) 
***************************************************************************/

/***************************************************************************
 * The purpose of this program is NOT to apply the instantiation schema itself
 * but rather to check that the condition ensuring completness are
 * satisfied
 * This problem is decidable but not obvious since it envolves some
 * fix point computations (saturation w.r.t. various inference systems)
 *
 ***************************************************************************/

/***************************************************************************/
/* Warning: this program is a highly experimental software, which have been
*  developed for on-going theoretical research on proof by instantiation and
*  Satisfiability Modulo Theory */
/* It is delivered as it is, without any guarantee */
/***************************************************************************/
/*  Please report bugs or remarks to Nicolas.Peltier@imag.fr */
/***************************************************************************/

/* From the prolog interpretor, type "fish" to run the program */
/* then use the command load(<input_file>) to load a theory */ 

/****************************************************************************/
/* Restrained clause set */
/****************************************************************************/

/* check the property of term T */

term_has_property(T,restricted) :- !, /* C-restrictedness */
	term_is_restricted(T).
term_has_property(T,Prop) :- /* other: check negation instead */
	\+(term_does_not_have_prop(T,Prop)).

/* check that T is C-restricted */

term_is_restricted(T) :-
	var(T), !, fail.
term_is_restricted(T) :-
	T =.. [F|A],
	constructor(F),
	\+((member(X,A), \+(flat(X)))), !.
term_is_restricted(T) :-
	T =.. [F|A],
	args_are_restricted(A,F,1).
	
args_are_restricted([A|B],F,I) :-
	nonvarindex(F,I),
	term_is_restricted(A), !,
	args_are_restricted2(B).
args_are_restricted([A|B],F,I) :-
	flat(A), !, II is I + 1, args_are_restricted(B,F,II).

args_are_restricted2([]) :- !.
args_are_restricted2([A|B]) :-
	term_is_restricted(A), !,
	args_are_restricted2(B).
args_are_restricted2([A|B]) :-
	flat(A), !, args_are_restricted2(B).

/* check that T is not quasiflat (find a subterm not satisfying the 
*  desired property) */

term_does_not_have_prop(T,quasiflat) :-
	subterm(S,T),
	\+(var(S)),
	S =.. [F|A],
	flatindex(F,I),
	nth(I,X,A),
	compound(X).

/* check that T is not restricted (find a subterm not satisfying the 
*  desired property) */

term_does_not_have_prop(T,quasiclosed) :-
	subterm(S,T),
	\+(var(S)),
	S =.. [F|A],
	nth(I,X,A),
	nonvarindex(F,I),
	var(X).

/*************************************/
/* check that a clause is controlled */
/*************************************/

/* constrained clauses */
/* clause may contain "constraint literal", marking some variables as constant
   and adding some equations */

controlled_ccl(C) :-
	instantiate_cst(C), 	/* variables marked as cst must be instantiated */
	rm_constraints(C,CC), 		/* constraints are removed */
	controlled_cl(CC).	

/* check that ordinary clauses are (strongly) controlled */

controlled_cl(X) :-
	\+(non_variablepreserving_cl(X)),  /* X must be var preserving */
	all_literals_controlled(X).		   /* check that every literal is controlled */

/* all literals are controlled */
/* ignore constraint literal */

all_literals_controlled([]) :- !.

all_literals_controlled([L|Next]) :-
	(L = constraint_literal(_);
		(no_constructor(L),  /* no constructor */
		controlled_lit(L))), !,
	all_literals_controlled(Next).
all_literals_controlled([_L|_Next]) :-
	fail.

controlled_lit(X = Y) :- 
	var(X),
	var(Y), !.

controlled_lit(X = Y) :- 
	var(X),
	cst(Y), !.

controlled_lit(Y = X) :- 
	var(X),
	cst(Y), !.
	
controlled_lit(E) :- 
	((E = (X = Y));(E = not(X = Y))), !,
	\+(var(X)), 
	\+(var(Y)), 
	term_has_property(X,quasiflat),
	term_has_property(Y,quasiflat),
	term_has_property(X,quasiclosed),
	term_has_property(Y,quasiclosed).

controlled_lit(not(X)) :- !,
	controlled_lit(not(X = true)).

controlled_lit(X) :- !,
	controlled_lit(X = true).

/*******************************************/
/* Check that a clause set is controllable */
/*******************************************/

:- dynamic(n_controlled/1).
:- dynamic(new_cl/1). /* contains the clauses generated during current step */
:- dynamic(prev_cl/1). /* contains the clauses generated during the previous step */
:- dynamic(all_cl/1). /* contrains all the clauses */

/* compute the clause sets that can be derived from S using superposition
*  from equations f(c1,...,cn) = c | C, where C is flat ground */

all_superpositions(L) :-
	write('Computing [S]'), nl,
	write('----------------------'), nl,
	nl,
	assert_all_as_new(L),
	nl,
	fixpoint_loop.

/* Check that a set of clauses (id) is quasiflat */
all_clauses_id_are_quasiflat([]) :- !.
all_clauses_id_are_quasiflat([X|Y]) :- 
	lits(X,L), /* find literals of clause X */ 
	all_clauses_are_quasiflat(L),
	write(X), write(' is quasi-flat.'), nl,
	all_clauses_id_are_quasiflat(Y), !.

/* Check that a set of clauses is quasiflat */
/* (idem but use clauses themselves, not id) */

all_clauses_are_quasiflat([]) :- !.
all_clauses_are_quasiflat([X=Y|L]) :-  !,
	term_has_property(X,quasiflat), 
	term_has_property(Y,quasiflat), 
	all_clauses_are_quasiflat(L).
all_clauses_are_quasiflat([not(X=Y)|L]) :-  !,
	term_has_property(X,quasiflat), 
	term_has_property(Y,quasiflat), 
	all_clauses_are_quasiflat(L).

/* Compute all the clauses in [S] */
/* i.e. all the clauses that can be obtained from a given clause set */
/* by superposition from equations of the form f(c1,...,cn) -> c | C where
* C is flat ground */
/* clauses that are strongly controlled or valid are removed */
/* use fix point algo for computing all possible clauses */

fixpoint_loop :-
	compute_superpositions.
fixpoint_loop :- 
	\+(new_cl(_)), !. /* no new clause derived -> succeed */
fixpoint_loop :-  /* otherwise */
	retractall(prev_cl(_)), /* retract previous cl */
	new_to_prev, 		/* mark previously new clauses as old */
	retractall(new_cl(_)),  /* delete new clauses */ 
	fixpoint_loop.                /* proceed to next step in fixpoint iteration */

compute_superpositions :-
	prev_cl(NC), 	/* find a previous cl */
	lits(NC,C),	/* find its literal list */
	subterm(T,C,P), /* find a subterm in it */
	\+(var(T)),     /* cannot be a variable */
	T =.. [F|A],
	constructor(F), /* must have a constructor head */
	\+( (member(X,A), \+(flat(X)))), /* all args must be flat */
	mark_variables_as_cst(F,1,A,[],OUT), /* fix all variables to cst */
	replace_pos(P,V,C,CC), /* replace term by cst */
	append(CC,[constraint_literal(not(T=V)),constraint_literal(not(cst(V)))|OUT],CCC),		   /* add used equation as constraint */
	write_cl(CCC), nl, /* display the clause */
	/* clauses that are strongly controlled, redundant or valid are discarded */
	\+( (all_cl(NN), lits(NN,LLL), variant_of(LLL,CCC)) ),
	\+((controlled_ccl(CCC), write('... strongly controlled.'), nl)),
	\+( (valid_cl(CCC), write('... valid'), nl) ),
	gensym(ccc,Num), /* otherwise get an id */
	assertz(lits(Num,CCC)),		/* store clause as new */
	assertz(new_cl(Num)),  
	assertz(all_cl(Num)), 
	fail.

/* mark all the variables in the term as cst symbols */

mark_variables_as_cst(_,_,[],IN,IN) :- !.
mark_variables_as_cst(F,I,[X|Y],IN,OUT) :- 
	var(X), 
	nonvarindex(F,I), 
	\+((member(constraint_literal(not(cst(XX))),IN),XX == X)), !,
	II is I+1,
	mark_variables_as_cst(F,II,Y,[constraint_literal(not(cst(X)))|IN],OUT), !.
mark_variables_as_cst(F,I,[_|Y],IN,OUT) :- 
	II is I+1,
	mark_variables_as_cst(F,II,Y,IN,OUT), !.

/* assert all the clauses as new, except if it is strongly controlled */

assert_all_as_new(L) :-
	member(X,L), 
	assertz(passive(X)), 
	write('Clause '), write(X), 
	lits(X,XX), 
	(controlled_cl(XX) -> (write(' is strongly controlled.')); 
		(assertz(all_cl(X)), assertz(prev_cl(X))), write(' is non strongly controlled.')),
	nl,
	fail.
assert_all_as_new(_).

new_to_prev :-
	new_cl(C),
	retract(new_cl(C)),
	assertz(prev_cl(C)), !.
new_to_prev.

/* check that a term contains no constructor */

no_constructor(X) :-
	var(X), !.
no_constructor([]) :- !.
no_constructor([X|Y]) :- !,
	no_constructor(X),
	no_constructor(Y).
no_constructor(X) :-
	cst(X), !.
no_constructor(X) :-
	X =.. [F|Arg],
	\+(constructor(F)),
	no_constructor(Arg).

/**************************************************************************/
controllable(L) :-
	find_clset_name(L,LL),
	controllable_cl(LL).
controllable(_L) :-
	write('The clause set is non controllable.'), nl, fail.

controllable_cl(L) :-
	retractall(passive(_)),
	retractall(active(_)),
	retractall(all_cl(_)),
	retractall(new_cl(_)),
	retractall(prev_cl(_)),
	write('Check that the set is quasiflat'), nl,
	write('-----------------------------------------------'), nl,
	nl,
	all_clauses_id_are_quasiflat(L),
	nl,
	all_superpositions(L),
	nl,
	write('Checking C-restrictedness.'), nl,
	write('------------------------------------------------------------'), nl, nl, !,
	all_eligible_term_are_restricted,
	nl,
	write('Checking controllability.'), nl,
	write('-------------------------------------------'), nl, nl, !,
	cl_set_is_saturated,
	nl,
	write('The clause set is controllable.'), nl.

/* check that all eligible terms are either cst or restricted */
all_eligible_term_are_restricted :-
	all_cl(N),
	lits(N,C),
	write('Clause '), write_cl(C), nl,
	eligible_term(T,C,_,_), /* find eligible term */
	write(T), write(' is eligible '), nl,
	instantiate_cst(C),
	\+(cst(T)),	
	\+(term_has_property(T,restricted)), !, 
	write('Non restricted.'), nl, fail.
all_eligible_term_are_restricted.

cl_set_is_saturated :-
	\+(a_clause_can_be_derived).

/* check that no inference can be applied in the obtained cl set */

a_clause_can_be_derived :-
	all_cl(N),
	(R = eq_factoring(N); R = reflexivity(N)),
	apply_rule(Cl,R), 
	write(R), nl,
	cannot_discard(Cl),
	write(pb2).

a_clause_can_be_derived :-
	all_cl(N1),
	all_cl(N2),
	(C = superposition(N1,N2); C = paramodulation(N1,N2); C = resolution(N1,N2)),
	retractall(non_flat), 
	apply_rule(Cl,C), 
	write(C), nl,
	cannot_discard(Cl).

valid_cl(C) :-
	reflexive_normal_form(C,CC),
	valid(CC).

redundant_cl(C) :-
	simplify_cl(C,CC),
	((cl(DD), subsume(DD,CC));valid(CC)).

/* apply reflexivity for simplifying the clause */
/* X = a | P(X) -> P(a) */

reflexive_normal_form(C,CCC) :-
	(select(not(X = Y),C,CC); select(not(Y = X),C,CC)),
	var(X),
	\+(subterm_id(X,Y)), !,
	X = Y,
	reflexive_normal_form(CC,CCC).

reflexive_normal_form(C,CCC) :-
	select(constraint_literal(not(E)),C,CC),
	(E = (X = T); E = (T = X)),
	var(X), \+(subterm_id(X,T)), !,
	X = T,
	reflexive_normal_form(CC,CCC).

reflexive_normal_form(C,C).

/* apply some simplification rule: reflexivity and demodulation */
simplify_cl(C,CCC) :-
	(select(not(X = Y),C,CC); select(not(Y = X),C,CC)),
	var(X),
	\+(subterm_id(X,Y)), !,
	X = Y,
	simplify_cl(CC,CCC).

simplify_cl(C,CCC) :-
	select(constraint_literal(not(U = V)),C,CC),
	simplify_cl([not(U = V)|CC],CCC).

simplify_cl(C,CCC) :-
	set_match_mode,
	demodulate(C,CC), 
	clear_match_mode,
	\+(C == CC), !,
	simplify_cl(CC,CCC).
simplify_cl(C,C).

/* Check that the clause must be kept */

/* discard clause if constraint are violated */
cannot_discard(C) :-
	member(constraint_literal(not(cst(X))),C),
	\+(flat(X)), !, fail.

cannot_discard(C) :-
	write('Generate clause '), write_cl(C), nl, fail.

cannot_discard(C) :-  /* discard redundant clauses */
	redundant_cl(C), write('... redundant'), nl, !, fail.
cannot_discard(_C) :- non_ground, write('Non ground inference.'), nl, !.
cannot_discard(C) :- /* discard clause if stronly controlled AND unifer is flat */
	controlled_ccl(C), write('... strongly controlled'), nl, !, fail.

cannot_discard(_).

/***************************************************************************/
/* variable preserving clause */
/***************************************************************************/

:- dynamic(kindex/2).

/* compute the set of instantiable variable */

iv(X,L) :-
	iv(X,[],L).

/* check that X belongs to instantiable variable in clause C */
variable_instantiable_in_cl(X,C) :-
	member(L,C), 	
	variable_instantiable_in_lit(X,L).
variable_instantiable_in_lit(X,L) :- !,
	get_atom(L,U = V),
	(subterm(T,U);subterm(T,V)),
	\+(var(T)),
	T =.. [F|A],
	kindex(F,I),
	nth(I,XX,A),
	XX == X.

iv(X,Lin,Lout) :-
	var(X), !, Lout = Lin.

iv(X,Lin,Lout) :-
	X =.. [F|A],
	add_kindex(F,A,1,Lin,Laux), /* add the variable arguments if occur at kindex */
	iv_list(A,Laux,Lout).
iv_list([],Lout,Lout) :- !.
iv_list([X|Y],Lin,Lout) :-
	iv(X,Lin,Laux),
	iv_list(Y,Laux,Lout).

/* add_kindex(F,L,I,Lin,Lout) 
*  adds in a list Lin all the variable occurring in i-th position in L
*  if I+i-1 is a kindex of F */

add_kindex(_,[],_,Lin,Lin) :- !.
add_kindex(F,[A|B],I,Lin,Laux) :-
	(\+(kindex(F,I));\+(var(A))), !, 
	II is I+1,
	add_kindex(F,B,II,Lin,Laux).

add_kindex(F,[A|B],I,Lin,Laux) :-
	member(X,Lin),
	X == A, !,
	II is I+1,
	add_kindex(F,B,II,Lin,Laux).

add_kindex(F,[A|B],I,Lin,Laux) :-
	II is I+1,
	add_kindex(F,B,II,[A|Lin],Laux).

/* check that a set of clause id is (not) variable preserving */

non_variablepreserving_cl(Cl) :- /* find a literal that is not var preserving */
	select(Lit,Cl,Rest),
	\+(variablepreserving_lit(Lit,Rest)).

variablepreserving_lit(T = S,_) :-
	orient(T = S,A = B),
	\+(var(A)),
	\+(var(B)),
	iv(A,VT),
	iv(B,VS),
	identical_sets(VT,VS), !.
variablepreserving_lit(T = S,C) :-
	flat(T),
	flat(S),
	(var(T) -> variable_instantiable_in_cl(T,C); true),
	(var(S) -> variable_instantiable_in_cl(S,C); true), !.
variablepreserving_lit(not(T = S),_) :-
	(iv(T,[]);iv(S,[])), !.
variablepreserving_lit(not(T = S),_) :-
	var(T), 
	ch_iv_term(T,S), !.
variablepreserving_lit(not(S = T),_) :-
	var(T), 
	ch_iv_term(T,S).
variablepreserving_lit(not(T = S),C) :-
	iv(T,[],L),
	iv(S,L,LL),
	\+((member(X,LL), \+(variable_instantiable_in_cl(X,C)))).

:- dynamic(flatindex/2).   /* flat arguments index */
:- dynamic(nonvarindex/2). /* non var index */

constructor(F) :- /* constructor occur in "restricted_symbols" list */
	clset(restricted_symbols,F).

/*************************************************************************/
/* Display clause with equational constraints */
/*************************************************************************/

write_cl(C) :-
	w_prep(C,V,Lits,Cond),
	write(Lits), write_cond(Cond,V).

/* separate the clause between clausal part, equational constraint part
*  and constant constraints part */

w_prep([],[],[],[]) :- !.

w_prep([constraint_literal(not(cst(X)))|L],VV,Lits,Cond) :- !,
	w_prep(L,V,Lits,Cond),
	((member(XX,V), XX == X) -> VV = V; VV = [X|V]).
w_prep([constraint_literal(not(T = S))|L],V,Lits,[T=S|Cond]) :- !,
	w_prep(L,V,Lits,Cond).
w_prep([E|L],V,[E|Lits],Cond) :- !,
	w_prep(L,V,Lits,Cond).

write_cond([],[]) :- !.
write_cond([],V) :- 
	write(' where '), write(V), write(' are constant'), !.
write_cond([T = S|Y],V) :-
       write(' where '), write(T = S), write_cond2(Y,V).
write_cond2([],[]) :- !.
write_cond2([],V) :- !,
	write(' and '), write(V), write(' are constant'), !.
write_cond2([T = S|Y],V) :- !,
	write(', '), write(T = S), write_cond2(Y,V).

/*************/
/* syntax.pl */
/*************/

/* basic syntactic definitions and predicates */

/* Check that a term is a constant symbols (numericals are cst) */

cst(X) :-
	atom(X), !.
cst(X) :-
	number(X).

/* special constant symbol */
spec_const(lambda).

/* find a term in a clause */
/* T occurs in C ? */

subterm_cl(T,C) :-
	member(Lit,C),
	subterm_lit(T,Lit).

/* find a term in a literal */

subterm_lit(T,not(L)) :- !,
	subterm_lit(T,L).
subterm_lit(T,U = V) :- !,
	(subterm(T,U);subterm(T,V)).
subterm_lit(T,L) :- !,
	subterm(T,L).

/***************************************/
/* Check the basic properties of terms */
/***************************************/

flat(T) :- /* is a term flat ? */
	\+(compound(T)).

/***************************************/
/* remove constraint literals */
/***************************************/

rm_constraints([],[]).
rm_constraints([constraint_literal(_)|L],LL) :- !,
	rm_constraints(L,LL).
rm_constraints([E|L],[E|LL]) :- !,
	rm_constraints(L,LL).

/***************************************************************************/
/* Compute saturated sets */
/***************************************************************************/

/* A toy superposition prover */

:- dynamic(active/1).
:- dynamic(passive/1).
:- dynamic(given_clause/1).
:- dynamic(parents/2).
:- dynamic(lits/2).
:- dynamic(clauseset/2).
:- multifile(lits/2).
:- discontiguous(cl/1).
:- discontiguous(lits/2).
:- discontiguous(clset/2).
:- multifile(clset/2).

:- dynamic(clset/2).

saturate :-
	one_step, !,
	saturate.

saturate.  /* stop when active is empty */

saturate(S,S2) :-
	retractall(passive(_)),
	retractall(active(_)),
	findall(_,(member(SS,S), clset(SS,C),assertz(active(C))),_),
	saturate,
	findall(_,((passive(C);active(C)),assertz(clset(S2,C))),_),
	nl,
	write('------------------------------------------------------'), nl,
	display_all_cl(S). 

saturate(S) :-
	retractall(passive(_)),
	retractall(active(_)),
	findall(_,(clset(S,C),assertz(active(C))),_),
	retractall(clset(S,_)),
	saturate,
	findall(_,((passive(C);active(C)),assertz(clset(S,C))),_),
	nl,
	write('------------------------------------------------------'), nl,
	display_all_cl(S). 

cl(X) :-
	(active(X);passive(X)).

/**************************************************************************/
one_step :-
	find_given_clause(N),
	one_step(N).

one_step(N) :-
	retract(active(N)),
	assertz(passive(N)),
	assertz(given_clause(N)),
	apply_all_rules,
	retract(given_clause(N)).

apply_all_rules :-
	choose_a_rule(R),
	%	write(R), nl,
	apply_rule(C,R), 
	%	write(C), nl,
	process(C,R), fail.
apply_all_rules.

find_given_clause(N) :-
	active(N).

/**************************************************************************/
:- dynamic(match_mode/0).

lit_ident(X,Y) :-
	(var(X); var(Y)), !,
	X == Y.
lit_ident(not(X),not(Y)) :- !, lit_ident(X,Y).
lit_ident(X = Y,XX = YY) :- 
	lit_ident(X,XX),
	lit_ident(Y,YY), !.
lit_ident(Y = X,XX = YY) :- !,
	lit_ident(X,XX),
	lit_ident(Y,YY).
lit_ident(T,S) :-
	T == S.

set_match_mode :-
	assertz(match_mode).
clear_match_mode :-
	retract(match_mode).

:- dynamic(non_ground/0).  /* indicate whether the last inference is ground or not */


/* Check that T is ground in C, modulo constant constraints */

ground_test(T,C) :-
	term_variables(T,XX),
	member(X,XX),
	\+( (member(constraint_literal(not(cst(Y))),C), Y == X) ), !,
	assertz(non_ground).
	
ground_test(_,_).

init_ground_test :-
	retractall(non_ground).

/*************************/
/* syntactic unification */
/*************************/

s_unify(X,Y) :-
	X == Y, !.
s_unify(F,G) :-
	var(F), !,
	(subterm_id(F,G) -> fail; F = G).
s_unify(G,F) :-
	var(F), !,
	\+(match_mode), /* if match then fail */
	(subterm_id(F,G) -> fail; F = G). 

s_unify([],[]) :- !.
s_unify([X|Y],[XX|YY]) :- !,
	s_unify(X,XX),
	s_unify(Y,YY).

s_unify(X = Y,U = V) :- !,
	((s_unify(X,U),s_unify(Y,V));(s_unify(X,V),s_unify(Y,U))).

s_unify(X,Y) :- !,
	X =.. [F|A],
	Y =.. [F|B],
	s_unify(A,B).

/**************************************************************************/
/* Is a disjunction of literals valid ? */

valid(L) :-
	member(X,L),
	member(constraint_literal(not(Y)),L),
	lit_ident(X,Y), !.
valid(L) :-
	member(X,L),
	member(not(Y),L),
	lit_ident(X,Y), !.
valid(L) :-
	member(X = Y,L), lit_ident(X,Y),!.

/********************/
/* Subsumption test */
/********************/

variant_of(C,D) :-
	subsume_cl(C,D),
	subsume_cl(D,C).

/* Does C subsume D ? C and D must be clauses and are instantiated during the process */

subsume_cl(C,D) :-
	numbervars(D,0,_),
	subclause(C,D).

/* Does C subsume D ? C and D may be id or clauses */

subsume(C,D) :-
	(cl(C) -> lits(C,LC); LC = C),
	(cl(D) -> lits(D,LD); LD = D),
	subsume_cl(LC,LD).

subclause([],_LD) :- !.
subclause([X|L],LD) :- !,
	member(Y,LD),
	(Y = constraint_literal(YY);YY = Y),
	s_unify(X,YY), 
	subclause(L,LD).

/**************************************************************************/
/* Delete all the clauses subsumed by C */
/**************************************************************************/

backward_subsumption(C) :-
	cl(D), 
	subsume(C,D), !,
	write('Clause '), write(D), write(' is deleted.'), nl,
	delete_cl(D), fail.
backward_subsumption(_).

/**************************************************************************/
/* clause deletion */
/**************************************************************************/

delete_cl(C) :-
	active(C), !, retract(active(C)).

delete_cl(C) :-
	passive(C), !, retract(passive(C)).
/**************************************************************************/

process(C,P) :- /* process a clause with parent P */
	backward_subsumption(C),
	gensym(cl,N),
	assertz(active(N)),
	assertz(lits(N,C)),
	assertz(parents(N,P)),
	write('>>> '), 
	display_cl(N).

/* Display clauses */

display_cl(N) :-
	lits(N,C),
	parents(N,P), !,
	write(C), write(' '), write(P), nl.
display_cl(N) :-
	lits(N,C),
	write(C), write(' '), write('(hyp)'), nl.

display_all_cl :-
	(passive(C);active(C)),
	display_cl(C), fail.
display_all_cl.

display_all_cl(S) :-
	clset(S,C),
	display_cl(C), fail.
display_all_cl(_).

/**************************************************************************/
/* apply superposition from N1 on N2 */
/**************************************************************************/

apply_rule(Cl,superposition(N1,N2)) :-
	lits(N1,L1),
	lits(N2,L2),
	eligible(E1,L1,LL1),
	eligible(E2,L2,LL2),
	orient(E1,T = S),
	orient(E2,U = V),
	\+( (member(constraint_literal(not(cst(UU))),L2), UU == U) ),
	subterm(X,U,Pos),
	\+(var(X)),
	init_ground_test,
	ground_test(T,L1),
	ground_test(X,L2),
	s_unify(X,T),
	eligible(E1,L1,LL1),
	eligible(E2,L2,LL2),
	replace_pos(Pos,S,U,UU),
	append(LL1,LL2,LL),
	CCl = [UU = V|LL],
	simplify(CCl,Cl).

/**************************************************************************/
/* apply resolution on N1 and N2 */
/**************************************************************************/

apply_rule(Cl,resolution(N1,N2)) :-
	lits(N1,L1),
	lits(N2,L2),
	eligible(E1,L1,LL1),
	\+(E1 = (_=_)),
	eligible(not(E2),L2,LL2),
	init_ground_test,
	ground_test(E1,L1),
	ground_test(E2,L2),
	s_unify(E1,E2),
	eligible(E1,L1,LL1),
	eligible(not(E2),L2,LL2),
	append(LL1,LL2,CCl),
	simplify(CCl,Cl).

/**************************************************************************/
/* apply paramodulation from N1 on N2 */
/**************************************************************************/

apply_rule(Cl,paramodulation(N1,N2)) :-
	lits(N1,L1),
	lits(N2,L2),
	eligible(E1,L1,LL1),
	eligible(E2,L2,LL2),
	E2 = not(UUU = VV), 
	orient(E1,T = S),
	orient(UUU = VV,U = V),
	\+( (member(constraint_literal(not(cst(UU))),L2), UU == U) ),
	subterm(X,U,Pos),
	\+(var(X)),
	init_ground_test,
	ground_test(T,L1),
	ground_test(X,L2),
	s_unify(X,T),
	eligible(E1,L1,LL1),
	eligible_term(U,L2,_,_),
	replace_pos(Pos,S,U,UU),
	append(LL1,LL2,LL),
	CCl = [not(UU=V)|LL],
	simplify(CCl,Cl).

apply_rule(Cl,paramodulation(N1,N2)) :-
	lits(N1,L1),
	lits(N2,L2),
	eligible(E1,L1,LL1),
	eligible(U,L2,LL2),
	\+(U = (_ = _)), /* U is not an equality */
	\+(U = not(_ = _)), /* U is not an disequality */
	orient(E1,T = S),
	\+( (member(constraint_literal(not(cst(UU))),L2), UU == U) ),
	subterm(X,U,Pos),
	\+(var(X)),
	init_ground_test,
	ground_test(T,L1),
	ground_test(X,L2),
	s_unify(X,T),
	eligible(E1,L1,LL1),
	eligible(U,L2,LL2),
	replace_pos(Pos,S,U,UU),
	append(LL1,LL2,LL),
	CCl = [UU|LL],
	simplify(CCl,Cl).

/**************************************************************************/
/* apply reflexivity rule on N */
/**************************************************************************/

apply_rule(Cl,reflexivity(N)) :-
	lits(N,L),
	eligible(not(X = Y),L,LL),
	init_ground_test,
	ground_test(X,L),
	ground_test(Y,L),
	s_unify(X,Y),
	eligible(not(X = Y),L,LL),
	simplify(LL,Cl).

/**************************************************************************/
/* apply factoring on N */
/**************************************************************************/

apply_rule(Cl,eq_factoring(N)) :-
	lits(N,L),
	eligible(E1,L,LL),
	eligible(E2,LL,LLL),
	orient(E1,T = S),
	orient(E2,TT = SS),
	\+( (member(constraint_literal(not(cst(U))),LLL), U == T) ),
	\+( (member(constraint_literal(not(cst(U))),LLL), U == TT) ),
	init_ground_test,
	ground_test(T,L),
	ground_test(TT,L),
	s_unify(T,TT),
	eligible(E1,L,LL),
	eligible(E2,LL,LLL),
	CCl = [T = S,not(S = SS)|LLL],
	simplify(CCl,Cl).

apply_rule(Cl,factoring(N)) :-
	lits(N,L),
	eligible(E1,L,LL),
	select(E2,LL,LLL),
	\+(E1 = (_ = _)),
	init_ground_test,
	ground_test(E1,L),
	ground_test(E2,L),
	s_unify(E1,E2),
	eligible(E1,L,LL),
	CCl = [E1|LLL],
	simplify(CCl,Cl).

/***************************************************************************/
choose_a_rule(C) :-
	given_clause(N),
	(
		C = factoring(N); 
		C = eq_factoring(N); 
		C = reflexivity(N);
		(passive(NN), (
				C = superposition(N,NN);
				C = superposition(NN,N);
				C = paramodulation(NN,N);
				C = paramodulation(N,NN);
				C = resolution(N,NN);
				C = resolution(NN,N)
			)
		)
	).

/**************************************************************************/
/* apply demodulation */
/**************************************************************************/

demodulate(Cl,C) :-
	subterm(X,Cl,Pos),
	\+(var(X)),
	cl(N),
	lits(N,Demodulator),
	eligible(E,Demodulator,L),
	orient(E,T = S),
	s_unify(T,X), 
	compare_term(T,S),
	greater_than(E,L),
	subset_id_cl(L,Cl), !,
	replace_pos(Pos,S,Cl,C).
demodulate(Cl,Cl).
/**************************************************************************/

subset_id_cl([],_) :- !.
subset_id_cl([X|Y],L) :- 
	member(XX,L), X == XX, !,
	subset_id_cl(Y,L).
subset_id_cl([X|Y],L) :- 
	member(constraint_literal(XX),L), X == XX, !,
	subset_id_cl(Y,L).
	
simplify(K,_) :-
	valid(K), !, fail.
simplify(K,R) :-
	remove_duplicate(K,KK),
	remove_false_literals(KK,KKK),
	\+(KKK == K), !,
	simplify(KKK,R).
simplify(K,_) :-
	cl(D),
	subsume(D,K), 
	!, fail.
%simplify(K,Z) :-
%	findall(U,cond(U),L), /* append list of conditions (if any) */
%	append(L,K,X),
%	retractall(cond(_)),
simplify(X,Z) :-
	set_match_mode,
	demodulate(X,XX),
	\+(X == XX), !,
	clear_match_mode,
	simplify(XX,Z).
simplify(K,K) :- !.

/**************************************************************************/
/* decompose a clause C into a list of clauses */
/**************************************************************************/

decompose([],[[]]) :- !.
decompose([X],[[X]]) :- !.
decompose([X|C],[NC|Others]) :- 
	decompose(C,LL),
	find_all_with_common_var(X,LL,CV,Others),
	merge([[X]|CV],NC).

find_all_with_common_var(_X,[],[],[]) :- !.
find_all_with_common_var(X,[C1|C],L,O) :- 
	find_all_with_common_var(X,C,LL,OO),
	(common_var(X,C1) -> (L = [C1|LL], O = OO); (L = LL, O = [C1|OO])).

common_var(C,D) :-
	subterm(X,C),
	var(X),
	subterm_id(X,D).

/**************************************************************************/
remove_duplicate([],[]) :- !.
remove_duplicate([X|Y],Z) :-
	remove_duplicate(Y,YY),
	remove_duplicate_aux(X,YY,Z).
remove_duplicate_aux(X,Y,Y) :-
	member(XX,Y), lit_ident(XX,X), !.
remove_duplicate_aux(X,Y,[X|Y]).
/**************************************************************************/

/**************************************************************************/
/* Remove false literals */
/**************************************************************************/

remove_false_literals([],[]) :- !.
remove_false_literals([not(X = Y)|Z],ZZ) :-
	lit_ident(X,Y), !,
	remove_false_literals(Z,ZZ).
remove_false_literals([L|Z],[L|ZZ]) :-
	remove_false_literals(Z,ZZ).

/**************************************************************************/
/* A literal is eligible in a clause */
/* if it is selected */
/* or if the list of selected lit is empty and the literal is max */
/**************************************************************************/

eligible(X,L,LL) :-
	select(X2,L,LL2),
	\+(X2 = constraint_literal(_)),
	(var(LL) -> (X2 = X, LL = LL2); (X2 == X, LL == LL2)),
	selected_literals(L,S),
	(member(X,S);(S = [],not_lower_than2(X,LL))).

/* eligible term: a non variable term occurring in a max term in 
  an eligible literal */

eligible_term(T,C,Pos,LL) :-
	eligible(LL,C,_),
	get_atom(LL,L),
	find_max_term(L,TT),
	subterm(T,TT,Pos),
	\+(var(T)).

get_atom(not(U), U) :- !.
get_atom(U, U) :- !.

find_max_term(E,U) :-
	E = (_ = _), !,
	orient(E,U = _).
find_max_term(E,E).

flat_cl(C) :-
	member(L,C),
	non_flat_lit(L), !, fail.
flat_cl(_).

non_flat_lit(T = S) :- !,
	(non_flat_term(T);non_flat_term(S)).
non_flat_lit(not(T = S)) :-
	non_flat_lit(T = S).	
non_flat_lit(T) :-
	T =.. [_|A],
	member(X,A), 
	non_flat_term(X).

non_flat_term(T) :-
	\+(var(T)),
	T =.. [_|A],
	member(X,A),
	\+(var(X)),
	\+(ground(X)).

/**************************************************************************/
/* find all eligible literals */
/**************************************************************************/

get_all_eligible(E,NE,C) :-
	get_all_eligible(E,NE,C,C).

get_all_eligible([],[],[],_C) :- !.
get_all_eligible(E,NE,[L|C],D) :-
	get_all_eligible(EE,NEE,C,D),
	get_all_eligible_aux(E,NE,L,D,EE,NEE).

get_all_eligible_aux([L|EE],NEE,L,D,EE,NEE) :-
	eligible(X,D,_),
	X == L, !.
get_all_eligible_aux(EE,[L|NEE],L,_D,EE,NEE).

selected_literals(C,[S]) :-
	sel_lit(S), 
	member(S,C), !.

selected_literals(_,[]).

:- dynamic(sel_lit/1).

positive_literal(not(_L)) :- !, fail.
positive_literal(_).
negative_literal(not(_L)) :- !.
/*****************************************************************************/



/*************************************************************************
 * 
 * exec command and read from file 
 *
 *************************************************************************/
 
:- op(1000,fx,select_lit).
:- op(900,xfx,in).
:- op(900,fx,function).

read_command :-
	read(C),
	exec_com(C), !,
	read_command.
read_command.

exec_com(end_of_file) :- !, fail. 
exec_com(bye) :- !, fail. 
exec_com(function F : X) :- !, handle_fun_dec(F, X).
exec_com(X = Y) :-
	find_clset_name(Y,YY), /* replace idf denoting cl set by the cor. cl set */
	(clauseset(X,C) -> retract(clauseset(X,C)); true), /* remove clause set if it exists */
	findall(_,(member(U,YY), assertz(clset(X,U))),_).  /* add new clause set */ 

exec_com(X : Y) :-
	(lits(X,C) -> retract(lits(X,C)); true), /* remove clause if it exists */
	add_all_cst(Y), 
	assertz(lits(X,Y)). 			 /* add new clause */
exec_com(select_lit L) :-
	assertz(sel_lit(L)).
exec_com(G) :- G.  /* exec prolog goal */

find_clset_name([],[]) :- !.
find_clset_name([X|Y],R) :- !,
	find_clset_name(Y,YY),
	find_clset_name2(X,YY,R).
find_clset_name(Y,R) :-
	find_clset_name([Y],R).

find_clset_name2(X,YY,R) :-
	findall(U,clset(X,U),XX), 
	\+(XX = []), !,
	append(XX,YY,R).
find_clset_name2(X,YY,[X|YY]).

load(F) :-
	current_input(I),
	open(F,read,Stream),
	set_input(Stream),
	read_command, 
	close(Stream), 
	set_input(I).

/***************************************************************************/

/* function declaration */

handle_fun_dec(F,D) :-
	member(preserving = L,D),
	member(I,L),
	assertz(kindex(F,I)), fail.

handle_fun_dec(F,D) :-
	member(flat = L,D),
	member(I,L),
	assertz(flatindex(F,I)), fail.

handle_fun_dec(F,D) :-
	member(nonvar = L,D),
	member(I,L),
	assertz(nonvarindex(F,I)), fail.

handle_fun_dec(F,D) :-
	member(weight = W,D),
	assertz(w(F,W)), fail.

handle_fun_dec(_,_).

add_all_cst(T) :- /* add all cst */
	subterm(C,T),
	atom(C),
	assertz(clset(constants,C)), fail.

add_all_cst(_).

clset(constants,bb).
clset(constants,kk).

/**********************************************************************/
/* Compare two terms */
/**********************************************************************/

/**********************************************************************/
/* lpo */
/**********************************************************************/

/**********************************************************************/
/* check whether a term T1 is greater than T2 */
/**********************************************************************/

compare_term(T1,_T2) :-
	var(T1), !, fail.

compare_term(T1,T2) :-
	var(T2), !, subterm(S,T1), S == T2.

compare_term(not(X),Y) :- !,
	compare_term(X,Y).

compare_term(X,not(Y)) :- !,
	compare_term(X,Y).

compare_term(X = Y,XX = YY) :- !,
	multi_compare_lists([X,Y],[XX,YY]).

compare_term(X = Y,T) :- !,
	compare_term(X = Y,T = true).

compare_term(T,X = Y) :- !,
	compare_term(T = true,X = Y).

compare_term(T1,T2) :-
	T1 =.. [F1|A1],
	(
		/* either there exists a subterm X in T1 s.t. X >= T2 */
		(member(X,A1), (X == T2; compare_term(X,T2)));  
		( T2 =.. [F2|A2],
	       	  compare_term_aux(T1,F1,A1,T2,F2,A2))).

compare_term_aux(T1,F1,_A1,_T2,F2,A2) :-
	inf_fun(F2,F1),
	compare_term_with_list(T1,A2).

compare_term_aux(T1,F,A1,_T2,F,A2) :- 
	compare_lists(A1,A2),
	compare_term_with_list(T1,A2).

compare_term_with_list(_T,[]) :- !.
compare_term_with_list(T,[X|L]) :- 
	compare_term(T,X),
	compare_term_with_list(T,L).

compare_lists(L1,L2) :-
	lex_compare_lists(L1,L2).

/**********************************************************************/
/* lexigraphic comparison */
/**********************************************************************/

lex_compare_lists([X1|X2],[Y1|Y2]) :-
	X1 == Y1, !,
	lex_compare_lists(X2,Y2), !.

lex_compare_lists([X1|_X2],[Y1|_Y2]) :-
	compare_term(X1,Y1), !.
	
/**********************************************************************/
/* multiset comparison */
/**********************************************************************/

multi_compare_lists([_|_],[]) :- !.
multi_compare_lists(L,[X|Y]) :- 
	select(XX,L,LL), 
	XX == X, !,
	multi_compare_lists(LL,Y).
multi_compare_lists(L,[X|Y]) :- !,
	member(XX,L),
	compare_term(XX,X), !,
	multi_compare_lists(L,Y).

/**********************************************************************/

/**********************/
/* orient an equation */
/**********************/

/* two solutions are possible (backtrack) */

orient(X = Y,E) :-
	compare_term(X,Y), !, E= (X = Y).

orient(X = Y,E) :-
	compare_term(Y,X), !, E = (Y = X).

orient(X = Y,E) :-
	(E = (X = Y);E = (Y = X)).

/***********************************************************************/
/* check that L is maximal in CC */

select_max(X,L,LL) :-
	select(X,L,LL),
	not_lower_than2(X,LL).

not_lower_than2(L,CC) :-
	\+(\+(not_lower_than3(L,CC))).

not_lower_than3(L,CC) :-
	instantiate_cst(CC),
	not_lower_than(L,CC).

instantiate_cst([]) :- !.
instantiate_cst([constraint_literal(not(cst(X)))|L]) :- !,
	X = bb,
	instantiate_cst(L).
instantiate_cst([_|L]) :- !,
	instantiate_cst(L).

not_lower_than(L,CC) :-
	member(LL,CC),
	\+(LL = constraint_literal(_)),
	compare_term(LL,L), !, fail.

not_lower_than(_,_).

greater_than(_,[]) :- !.
greater_than(L,[X|Y]) :- !,
	compare_term(L,X),
	greater_than(L,Y).

/***********************************************************************/

:- dynamic(w/2).

inf_fun(F,G) :-
	F = $a(_X), \+(G = $a(_Y)), !. 
inf_fun(G,F) :-
	F = $a(_X), \+(G = $a(_Y)), !, fail. 
inf_fun(true,_) :- !.
inf_fun(_,true) :- !, fail.
inf_fun(X,Y) :- 
	clset(constants,X), 
	\+(clset(constants,Y)), !.
inf_fun(X,Y) :- 
	clset(constants,Y), 
	\+(clset(constants,X)), !, fail.
inf_fun(F,G) :-
	w(F,P1),
	w(G,P2), !,
	P1 < P2, !.
inf_fun(F,G) :- F @< G.


/*****************************************************/
/* Some useful predicates */
/*****************************************************/

/*****************************************************/
/* is S a subterm of T ? */
/*****************************************************/

subterm(_,T) :-
	\+(var(T)),
	T = constraint_literal(_), !, fail.
subterm(T,T).

subterm(X,T) :- 
	\+(var(T)),
	T =.. [_|Args],
	member(ST,Args),
	subterm(X,ST).

/* same with pos */

subterm(_,T,_) :-
	T = constraint_literal(_), !, fail.

subterm(T,T,[]).

subterm(X,T,[I|Pos]) :- 
	\+(var(T)),
	T =.. [_|Args],
	nth(I,ST,Args),
	subterm(X,ST,Pos).

proper_subterm(S,T) :-
	subterm(S,T),
	\+(S = T).

does_not_contain(T,S) :- /* true if T does not contain S */
	\+(subterm(S,T)).


/*****************************************************/
/* Same predicate but does not instantiate S */
/*****************************************************/

subterm_id(S,T) :-
	subterm(SS,T),
	S == SS.

/*****************************************************/
/* Apply a predicate P on all subterms of T */
/*****************************************************/

apply_term(P,T) :-
	apply(P,[T]),
	apply_term_rec(P,T).

apply_term_rec(_P,T) :-
	var(T), !.

apply_term_rec(P,T) :-
	T =.. [_|Args],
	maplist(apply_term(P),Args).

/************************************************************/

/* replace X by Y in T -> TT */

replace(X,Y,X,Y) :- !.
replace(_,_,[],[]) :- !.
replace(X,Y,[T1|T2],[TT1|TT2]) :- !,
	replace(X,Y,T1,TT1),
	replace(X,Y,T2,TT2).
replace(X,Y,T,TT) :- 
	T =.. [F|A],
	replace(X,Y,A,AA),
	TT =.. [F|AA].

/* same with pos */
replace_pos([],Y,_,Y) :- !.
replace_pos(_,_,V,V) :- 
	var(V), !.
replace_pos(X,Y,T,TT) :- 
	T =.. [F|A],
	replace_pos_list(X,Y,A,AA),
	TT =.. [F|AA].
replace_pos_list(_,_,[],[]) :- !.
replace_pos_list([1|Q],Y,[T1|T2],[TT1|T2]) :- !,
	replace_pos(Q,Y,T1,TT1).
replace_pos_list([P|Q],Y,[T1|T2],[T1|TT2]) :- 
	PP is P-1,
	replace_pos_list([PP|Q],Y,T2,TT2), !.

/* same but replace only identical terms */

replace_id(X,Y,T,Y) :- 
	X == T, !.
replace_id(_,_,T,T) :- 
	var(T), !.
replace_id(_,_,[],[]) :- !.
replace_id(X,Y,[T1|T2],[TT1|TT2]) :- !,
	replace_id(X,Y,T1,TT1),
	replace_id(X,Y,T2,TT2).
replace_id(X,Y,T,TT) :- 
	T =.. [F|A],
	replace_id(X,Y,A,AA),
	TT =.. [F|AA].

/**********************************************************/

/* as replace but with two lists [T1...Tn] and [S1...Sn] */
/* replace Ti by Si */

replace_list([],_,T,T) :- !.
replace_list([X1|L1],[X2|L2],T,S) :- 
	replace(X1,X2,T,TT),
	replace_list(L1,L2,TT,S).

/**********************************************************/
/* max element in list */
/* fail if empty list */
/* Use predicat Comp to compare */

max([X],X,_) :- !.
max([X|L],Y,Comp) :- !,
	max(L,Z,Comp),
	(apply(Comp,[X,Z]) -> Y = X; Y = Z).

/* nth element in list */

nth(1,X,[X|_]).
nth(N,X,[_|L]) :-
	nth(NN,X,L),
	N is NN+1.

/*********************************************************/
/* Delete all goals unifiable with G */
/*********************************************************/

retract_all(G) :-
	G, !,
	retract(G),
	retract_all(G).
retract_all(_).

/***************************************************************************/
/* merge the lists into a new list */
/* use == for comparision */
/***************************************************************************/

merge([],[]).
merge([X|Y],R) :-
	merge(Y,L),
	merge2(X,L,R).

merge2([],L,L) :- !.
merge2([X|Y],L,R) :- 
	merge2(Y,L,LL),
	((member(U,LL), U == X) -> R = LL; R = [X|LL]),!.

/*************************************************************************/
/* check whether all the elements in L1 are in L2 (== comparison) */
/*************************************************************************/

subset_id([],_L) :- !.
subset_id([X|Y],L) :-
	member(XX,L),
	X == XX,
	subset_id(Y,L).

identical_sets(X,Y) :-
	subset_id(X,Y),
	subset_id(Y,X).

set_dif(E1,[],E1) :- !.
set_dif([],_,[]) :- !.
set_dif(E,[Y|E2],D) :-
	select(X,E,EE),
	X == Y, !,
	set_dif(EE,E2,D).
set_dif(E,[_Y|E2],D) :-
	set_dif(E,E2,D).	

member_id(X,L) :-
	member(XX,L),
	XX == X.	
/*************************************************************************/

fish :- read_command. 
