:- ensure_loaded('../Basis/internal_operators.pl').
:- use_module('../Basis/translations.pl').
:- ensure_loaded('../Transformations/to_cnf.pl').

%
%  resolve(+Clauses)
%    Starting with Clauses, new nonvalid clauses are generated using
%    the resolution rule until either the empty clause is generated,
%    in which case Clauses is unsatisfiable, or no new clause
%    can be generated, in which case Clauses is satisfiable
%    (a clause is valid iff it contains an atom and its negation)
%
resolve([]) :- !,
	write([]),
	write('\nThe set of clauses, being empty, is valid.').
resolve(Clauses) :-
	member([], Clauses), !,
	write_clauses(Clauses),
	write('\nThe set of clauses is unsatisfiable (since it contains []).').
resolve(Clauses) :-
	select(Clause1, Clauses, RemainingClauses),
	member(Clause2, RemainingClauses),
	clashing_clauses(Clause1, Literal1, Clause2, Literal2),
	delete(Clause1, Literal1, NewClause1),
	delete(Clause2, Literal2, NewClause2),
	merge_set(NewClause1, NewClause2, NewClause),
	\+ clashing_clauses(NewClause, _, NewClause, _),
	\+ member(NewClause, Clauses), !,
	write_clauses(Clauses), nl,
	resolve([NewClause| Clauses]).
resolve(Clauses) :-
	write_clauses(Clauses),
	write('\nThe set of clauses is satisfiable.').

%
%  clashing_clauses(+Clause1, -Literal1, +Clause2, -Literal2)
%    Succeeds if Literal1 belongs to Clause1, Literal2 to Clause2,
%    and one of Literal1, Literal2 is the negation of the other
%
clashing_clauses(Clause1, Atom, Clause2, neg Atom) :-
	member(Atom, Clause1),
	member(neg Atom, Clause2), !.
clashing_clauses(Clause1, neg Atom, Clause2, Atom) :-
	member(neg Atom, Clause1),
	member(Atom, Clause2).