%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% A Learning Engine for Proposing Hypotheses                              %
%                                                                         %
% A L E P H                                                               %
% Version 5    (last modified: Sun Mar 11 03:25:37 UTC 2007)              %
%                                                                         %
% This is the source for Aleph written and maintained                     %
% by Ashwin Srinivasan (ashwin@comlab.ox.ac.uk)                           %
%                                                                         %
%                                                                         %
% It was originally written to run with the Yap Prolog Compiler           %
% Yap can be found at: http://sourceforge.net/projects/yap/               %
% Yap must be compiled with -DDEPTH_LIMIT=1                               %
%                                                                         %
% It should also run with SWI Prolog, although performance may be         %
% sub-optimal.                                                            %
%                                                                         %
% If you obtain this version of Aleph and have not already done so        %
% please subscribe to the Aleph mailing list. You can do this by          %
% mailing majordomo@comlab.ox.ac.uk with the following command in the     %
% body of the mail message: subscribe aleph                               %
%                                                                         %
% Aleph is freely available for academic purposes.                        %
% If you intend to use it for commercial purposes then                    %
% please contact Ashwin Srinivasan first.                                 %
%                                                                         %
% A simple on-line manual is available on the Web at                      %
% www.comlab.ox.ac.uk/oucl/research/areas/machlearn/Aleph/index.html      %
%                                                                         %
%                                                                         %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% C O M P I L E R   S P E C I F I C


prolog_type(yap):-
	predicate_property(yap_flag(_,_),built_in), !.
prolog_type(swi).

init(yap):-
	source,
	system_predicate(false,false), hide(false),
	style_check(single_var),
	% yap_flag(profiling,on),
	assert_static((aleph_random(X):- X is random)),
	(predicate_property(alarm(_,_,_),built_in) ->
		assert_static((remove_alarm(X):- alarm(0,_,_)));
		assert_static(alarm(_,_,_)),
		assert_static(remove_alarm(_))),
	assert_static((aleph_consult(F):- consult(F))),
	assert_static((aleph_reconsult(F):- reconsult(F))),
        (predicate_property(thread_local(_),built_in) -> true;
		assert_static(thread_local(_))),
	assert_static(broadcast(_)),
	assert_static((aleph_background_predicate(Lit):-
				predicate_property(Lit,P),
				((P = static); (P = dynamic); (P = built_in)), !)),
	(predicate_property(delete_file(_),built_in) -> true;
		assert_static(delete_file(_))).

init(swi):-
	redefine_system_predicate(false),
	style_check(+singleton),
	style_check(-discontiguous),
	dynamic(false/0),
	dynamic(example/3),
	assert((aleph_random(X):- I = 1000000, X is float(random(I-1))/float(I))),
	arithmetic_function(inf/0), assert(inf(1e10)),
	assert((gc:- garbage_collect)),
	assert((depth_bound_call(G,L):-
			call_with_depth_limit(G,L,R),
			R \= depth_limit_exceeded)),
	(predicate_property(numbervars(_,_,_),built_in) -> true;
		assert((numbervars(A,B,C):- numbervars(A,'$VAR',B,C)))),
	assert((assert_static(X):- assert(X))),
	assert((system(X):- shell(X))),
	assert((exists(X):- exists_file(X))),
	assert((aleph_reconsult(F):- consult(F))),
	assert((aleph_consult(X):- aleph_open(X,read,S), repeat,
			read(S,F), (F = end_of_file -> close(S), !;
					assertz(F),fail))),
	use_module(library(broadcast)),
        (predicate_property(alarm(_,_,_),built_in) ->
		use_module(library(time));
                assert(alarm(_,_,_)),
                assert(remove_alarm(_))),
        (predicate_property(thread_local(_),built_in) -> true;
		assert(thread_local(_))),
	assert((aleph_background_predicate(Lit):-
				predicate_property(Lit,P),
				((P=interpreted);(P=built_in)), ! )),
	(predicate_property(delete_file(_),built_in) -> true;
		assert_static(delete_file(_))).

:- prolog_type(Type), init(Type).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% A L E P H


aleph_version(5).
aleph_version_date('Sun Mar 11 03:25:37 UTC 2007').
aleph_manual('http://www.comlab.ox.ac.uk/oucl/groups/machlearn/Aleph/index.html').

:- op(500,fy,#).
:- op(500,fy,*).
:- op(900,xfy,because).

:- dynamic '$aleph_feature'/2.
:- dynamic '$aleph_global'/2.
:- dynamic '$aleph_good'/3.

:- dynamic '$aleph_local'/2.

:- dynamic '$aleph_sat'/2.
:- dynamic '$aleph_sat_atom'/2.
:- dynamic '$aleph_sat_ovars'/2.
:- dynamic '$aleph_sat_ivars'/2.
:- dynamic '$aleph_sat_varsequiv'/2.
:- dynamic '$aleph_sat_varscopy'/3.
:- dynamic '$aleph_sat_terms'/4.
:- dynamic '$aleph_sat_vars'/4.
:- dynamic '$aleph_sat_litinfo'/6.

:- dynamic '$aleph_search_cache'/1.
:- dynamic '$aleph_search_prunecache'/1.
:- dynamic '$aleph_search'/2.
:- dynamic '$aleph_search_seen'/2.
:- dynamic '$aleph_search_expansion'/4.
:- dynamic '$aleph_search_gain'/4.
:- dynamic '$aleph_search_node'/8.

:- dynamic '$aleph_link_vars'/2.
:- dynamic '$aleph_has_vars'/3.
:- dynamic '$aleph_has_ovar'/4.
:- dynamic '$aleph_has_ivar'/4.
:- dynamic '$aleph_determination'/2.

:- thread_local('$aleph_search_cache'/1).
:- thread_local('$aleph_search_prunecache'/1).
:- thread_local('$aleph_search'/2).
:- thread_local('$aleph_search_seen'/2).
:- thread_local('$aleph_search_expansion'/4).
:- thread_local('$aleph_search_gain'/4).
:- thread_local('$aleph_search_node'/8).


:- multifile false/0.
:- multifile prune/1.
:- multifile refine/2.
:- multifile cost/3.
:- multifile prove/2.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% C O N S T R U C T   B O T T O M

% get_atoms(+Preds,+Depth,+MaxDepth,+Last,-LastLit)
% layered generation of ground atoms to add to bottom clause
%	Preds is list of PName/Arity entries obtained from the determinations
%	Depth is current variable-chain depth
%	MaxDepth is maximum allowed variable chain depth (i setting)
%	Last is last atom number so far
%	Lastlit is atom number after all atoms to MaxDepth have been generated
get_atoms([],_,_,Last,Last):- !.
get_atoms(Preds,Depth,MaxDepth,Last,LastLit):-
	Depth =< MaxDepth,
	Depth0 is Depth - 1,
	'$aleph_sat_terms'(_,Depth0,_,_),	% new terms generated ?
	!,
	get_atoms1(Preds,Depth,MaxDepth,Last,Last1),
	Depth1 is Depth + 1,
	get_atoms(Preds,Depth1,MaxDepth,Last1,LastLit).
get_atoms(_,_,_,Last,Last).

% auxiliary predicate used by get_atoms/5
get_atoms1([],_,_,Last,Last).
get_atoms1([Pred|Preds],Depth,MaxDepth,Last,LastLit):-
	gen_layer(Pred,Depth),
	flatten(Depth,MaxDepth,Last,Last1),
	get_atoms1(Preds,Depth,MaxDepth,Last1,LastLit).

% flatten(+Depth,+MaxDepth,+Last,-LastLit)
% flatten a set of ground atoms by replacing all in/out terms with variables
%	constants are wrapped in a special term called aleph_const(...)
%	eg suppose p/3 had modes p(+char,+char,#int)
%	then p(a,a,3) becomes p(X,X,aleph_const(3))
% ground atoms to be flattened are assumed to be in the i.d.b atoms
% vars and terms are actually integers which are stored in vars/terms databases
%	so eg above actually becomes p(1,1,aleph_const(3)).
%	where variable 1 stands for term 2 (say) which in turn stands for a
%	Depth is current variable-chain depth
%	MaxDepth is maximum allowed variable chain depth (i setting)
%	Last is last atom number so far
%	Lastlit is atom number after ground atoms here have been flattened
% If permute_bottom is set to true, then the order of ground atoms is
% shuffled. The empirical utility of doing this has been investigated by
% P. Schorn in "Random Local Bottom Clause Permutations for Better Search Space
% Exploration in Progol-like ILP Systems.", 16th International Conference on
% ILP (ILP 2006).
flatten(Depth,MaxDepth,Last,Last1):-
	retractall('$aleph_local'(flatten_num,_)),
	asserta('$aleph_local'(flatten_num,Last)),
	'$aleph_sat_atom'(_,_), !,
	(setting(permute_bottom,Permute) -> true; Permute = false),
	flatten_atoms(Permute,Depth,MaxDepth,Last1).
flatten(_,_,_,Last):-
	retract('$aleph_local'(flatten_num,Last)), !.

flatten_atoms(true,Depth,MaxDepth,Last1):-
	findall(L-M,retract('$aleph_sat_atom'(L,M)),LitModes),
	aleph_rpermute(LitModes,PLitModes),
	aleph_member(Lit1-Mode,PLitModes),
	retract('$aleph_local'(flatten_num,LastSoFar)),
	(Lit1 = not(Lit) -> Negated = true; Lit = Lit1, Negated = false),
	flatten_atom(Depth,MaxDepth,Lit,Negated,Mode,LastSoFar,Last1),
	asserta('$aleph_local'(flatten_num,Last1)),
	fail.
flatten_atoms(false,Depth,MaxDepth,Last1):-
	repeat,
	retract('$aleph_sat_atom'(Lit1,Mode)),
	retract('$aleph_local'(flatten_num,LastSoFar)),
	(Lit1 = not(Lit) -> Negated = true; Lit = Lit1, Negated = false),
	flatten_atom(Depth,MaxDepth,Lit,Negated,Mode,LastSoFar,Last1),
	asserta('$aleph_local'(flatten_num,Last1)),
	('$aleph_sat_atom'(_,_) ->
			fail;
			retract('$aleph_local'(flatten_num,Last1))), !.
flatten_atoms(_,_,_,Last):-
	retract('$aleph_local'(flatten_num,Last)), !.


% flatten_atom(+Depth,+Depth1,+Lit,+Negated,+Mode,+Last,-Last1)
%	update lits database by adding ``flattened atoms''. This involves:
%	replacing ground terms at +/- positions in Lit with variables
%	and wrapping # positions in Lit within a special term stucture
%	Mode contains actual mode and term-place numbers and types for +/-/# 
%	Last is the last literal number in the lits database at present
%	Last1 is the last literal number after the update
flatten_atom(Depth,Depth1,Lit,Negated,Mode,Last,Last1):-
	arg(3,Mode,O), arg(4,Mode,C),
	integrate_args(Depth,Lit,O),
	integrate_args(Depth,Lit,C),
	(Depth = Depth1 -> CheckOArgs = true; CheckOArgs = false),
	flatten_lits(Lit,CheckOArgs,Depth,Negated,Mode,Last,Last1).

% variabilise literals by replacing terms with variables
% if var splitting is on then new equalities are introduced into bottom clause
% if at final i-layer, then literals with o/p args that do not contain at least
% 	one output var from head are discarded
flatten_lits(Lit,CheckOArgs,Depth,Negated,Mode,Last,_):-
	functor(Lit,Name,Arity),
	asserta('$aleph_local'(flatten_lits,Last)),
	Depth1 is Depth - 1,
	functor(OldFAtom,Name,Arity),
	flatten_lit(Lit,Mode,OldFAtom,_,_),
	functor(FAtom,Name,Arity),
	apply_equivs(Depth1,Arity,OldFAtom,FAtom),
	retract('$aleph_local'(flatten_lits,OldLast)),
	(CheckOArgs = true -> 
		arg(3,Mode,Out),
		get_vars(FAtom,Out,OVars),
		(in_path(OVars) ->
			add_new_lit(Depth,FAtom,Mode,OldLast,Negated,NewLast);
			NewLast = OldLast) ;
		add_new_lit(Depth,FAtom,Mode,OldLast,Negated,NewLast)),
	asserta('$aleph_local'(flatten_lits,NewLast)),
	fail.
flatten_lits(_,_,_,_,_,_,Last1):-
	retract('$aleph_local'(flatten_lits,Last1)).


% flatten_lit(+Lit,+Mode,+FAtom,-IVars,-OVars)
% variabilise Lit as FAtom
%	Mode contains actual mode and 
%	In, Out, Const positions as term-place numbers with types
% 	replace ground terms with integers denoting variables
%	or special terms denoting constants
% 	variable numbers arising from variable splits are disallowed
%	returns Input and Output variable numbers
flatten_lit(Lit,mode(Mode,In,Out,Const),FAtom,IVars,OVars):-
	functor(Mode,_,Arity),
	once(copy_modeterms(Mode,FAtom,Arity)),
	flatten_vars(In,Lit,FAtom,IVars),
	flatten_vars(Out,Lit,FAtom,OVars),
	flatten_consts(Const,Lit,FAtom).

% flatten_vars(+TPList,+Lit,+FAtom,-Vars):-
% FAtom is Lit with terms-places in TPList replaced by variables
flatten_vars([],_,_,[]).
flatten_vars([Pos/Type|Rest],Lit,FAtom,[Var|Vars]):-
	tparg(Pos,Lit,Term),
	'$aleph_sat_terms'(TNo,_,Term,Type),
	'$aleph_sat_vars'(Var,TNo,_,_),
	\+('$aleph_sat_varscopy'(Var,_,_)),
	tparg(Pos,FAtom,Var),
	flatten_vars(Rest,Lit,FAtom,Vars).

% replace a list of terms at places marked by # in the modes
% with a special term structure denoting a constant
flatten_consts([],_,_).
flatten_consts([Pos/_|Rest],Lit,FAtom):-
	tparg(Pos,Lit,Term),
	tparg(Pos,FAtom,aleph_const(Term)),
	flatten_consts(Rest,Lit,FAtom).

% in_path(+ListOfOutputVars)
% check to avoid generating useless literals in the last i layer
in_path(OVars):-
	'$aleph_sat'(hovars,Vars), !,
	(Vars=[];OVars=[];intersects(Vars,OVars)).
in_path(_).

% update_equivs(+VariableEquivalences,+IDepth)
% update variable equivalences created at a particular i-depth
% is non-empty only if variable splitting is allowed
update_equivs([],_):- !.
update_equivs(Equivs,Depth):-
	retract('$aleph_sat_varsequiv'(Depth,Eq1)), !,
	update_equiv_lists(Equivs,Eq1,Eq2),
	asserta('$aleph_sat_varsequiv'(Depth,Eq2)).
update_equivs(Equivs,Depth):-
	Depth1 is Depth - 1,
	get_equivs(Depth1,Eq1),
	update_equiv_lists(Equivs,Eq1,Eq2),
	asserta('$aleph_sat_varsequiv'(Depth,Eq2)).

update_equiv_lists([],E,E):- !.
update_equiv_lists([Var/E1|Equivs],ESoFar,E):-
	aleph_delete(Var/E2,ESoFar,ELeft), !,
	update_list(E1,E2,E3),
	update_equiv_lists(Equivs,[Var/E3|ELeft],E).
update_equiv_lists([Equiv|Equivs],ESoFar,E):-
	update_equiv_lists(Equivs,[Equiv|ESoFar],E).

% get variable equivalences at a particular depth
% recursively descend to greatest depth below this for which equivs exist
% also returns the database reference of entry
get_equivs(Depth,[]):-
	Depth < 0, !.
get_equivs(Depth,Equivs):-
	'$aleph_sat_varsequiv'(Depth,Equivs), !.
get_equivs(Depth,E):-
	Depth1 is Depth - 1,
	get_equivs(Depth1,E).

% apply equivalences inherited from Depth to a flattened literal
% if no variable splitting, then succeeds only once
apply_equivs(Depth,Arity,Old,New):-
	get_equivs(Depth,Equivs),
	rename(Arity,Equivs,[],Old,New).

% rename args using list of Var/Equivalences
rename(_,[],_,L,L):- !.
rename(0,_,_,_,_):- !.
rename(Pos,Equivs,Subst0,Old,New):-
        arg(Pos,Old,OldVar),
        aleph_member(OldVar/Equiv,Equivs), !,
        aleph_member(NewVar,Equiv),
        arg(Pos,New,NewVar),
        Pos1 is Pos - 1,
        rename(Pos1,Equivs,[OldVar/NewVar|Subst0],Old,New).
rename(Pos,Equivs,Subst0,Old,New):-
        arg(Pos,Old,OldVar),
        (aleph_member(OldVar/NewVar,Subst0) ->
                arg(Pos,New,NewVar);
                arg(Pos,New,OldVar)),
        Pos1 is Pos - 1,
        rename(Pos1,Equivs,Subst0,Old,New).


% add a new literal to lits database
% performs variable splitting if splitvars is set to true
add_new_lit(Depth,FAtom,Mode,OldLast,Negated,NewLast):-
	arg(1,Mode,M),
	functor(FAtom,Name,Arity),
	functor(SplitAtom,Name,Arity),
	once(copy_modeterms(M,SplitAtom,Arity)),
	arg(2,Mode,In), arg(3,Mode,Out), arg(4,Mode,Const),
        split_vars(Depth,FAtom,In,Out,Const,SplitAtom,IVars,OVars,Equivs),
        update_equivs(Equivs,Depth),
        add_lit(OldLast,Negated,SplitAtom,In,Out,IVars,OVars,LitNum),
        insert_eqs(Equivs,Depth,LitNum,NewLast), !.

% modify the literal database: check if performing lazy evaluation
% of bottom clause, and update input and output terms in literal
add_lit(Last,Negated,FAtom,I,O,_,_,Last):-
	setting(construct_bottom,CBot),
	(CBot = false ; CBot = reduction), 
	(Negated = true -> Lit = not(FAtom); Lit = FAtom),
	'$aleph_sat_litinfo'(_,0,Lit,I,O,_), !.
add_lit(Last,Negated,FAtom,In,Out,IVars,OVars,LitNum):-
	LitNum is Last + 1,
	update_iterms(LitNum,IVars),
	update_oterms(LitNum,OVars,[],Dependents),
	add_litinfo(LitNum,Negated,FAtom,In,Out,Dependents),
	assertz('$aleph_sat_ivars'(LitNum,IVars)),
	assertz('$aleph_sat_ovars'(LitNum,OVars)), !.


% update lits database after checking that the atom does not exist
% used during updates of lit database by lazy evaluation
update_lit(LitNum,true,FAtom,I,O,D):-
	'$aleph_sat_litinfo'(LitNum,0,not(FAtom),I,O,D), !.
update_lit(LitNum,false,FAtom,I,O,D):-
	'$aleph_sat_litinfo'(LitNum,0,FAtom,I,O,D), !.
update_lit(LitNum,Negated,FAtom,I,O,D):-
	gen_nlitnum(LitNum),
	add_litinfo(LitNum,Negated,FAtom,I,O,D), 
	get_vars(FAtom,I,IVars),
	get_vars(FAtom,O,OVars),
	assertz('$aleph_sat_ivars'(LitNum,K,IVars)),
	assertz('$aleph_sat_ovars'(LitNum,K,OVars)), !.

% add a literal to lits database without checking
add_litinfo(LitNum,true,FAtom,I,O,D):-
	!,
	assertz('$aleph_sat_litinfo'(LitNum,0,not(FAtom),I,O,D)).
add_litinfo(LitNum,_,FAtom,I,O,D):-
	assertz('$aleph_sat_litinfo'(LitNum,0,FAtom,I,O,D)).
	
% update database with input terms of literal
update_iterms(_,[]).
update_iterms(LitNum,[VarNum|Vars]):-
	retract('$aleph_sat_vars'(VarNum,TNo,I,O)),
	update(I,LitNum,NewI),
	asserta('$aleph_sat_vars'(VarNum,TNo,NewI,O)),
	update_dependents(LitNum,O),
	update_iterms(LitNum,Vars).

% update database with output terms of literal
% return list of dependent literals
update_oterms(_,[],Dependents,Dependents).
update_oterms(LitNum,[VarNum|Vars],DSoFar,Dependents):-
	retract('$aleph_sat_vars'(VarNum,TNo,I,O)),
	update(O,LitNum,NewO),
	asserta('$aleph_sat_vars'(VarNum,TNo,I,NewO)),
	update_list(I,DSoFar,D1),
	update_oterms(LitNum,Vars,D1,Dependents).

% update Dependent list of literals with LitNum
update_dependents(_,[]).
update_dependents(LitNum,[Lit|Lits]):-
	retract('$aleph_sat_litinfo'(Lit,Depth,Atom,ITerms,OTerms,Dependents)),
	update(Dependents,LitNum,NewD),
	asserta('$aleph_sat_litinfo'(Lit,Depth,Atom,ITerms,OTerms,NewD)),
	update_dependents(LitNum,Lits).

% update dependents of head with literals that are simply generators
% 	that is, literals that require no input args
update_generators:-
	findall(L,('$aleph_sat_litinfo'(L,_,_,[],_,_),L>1),GList),
	GList \= [], !,
	retract('$aleph_sat_litinfo'(1,Depth,Lit,I,O,D)),
	aleph_append(D,GList,D1),
	asserta('$aleph_sat_litinfo'(1,Depth,Lit,I,O,D1)).
update_generators.

% mark literals 
mark_lits(Lits):-
	aleph_member(Lit,Lits),
	asserta('$aleph_local'(marked,Lit/0)),
	fail.
mark_lits(_).
	
% recursively mark literals with minimum depth to bind output vars in head
mark_lits([],_,_).
mark_lits(Lits,OldVars,Depth):-
	mark_lits(Lits,Depth,true,[],Predecessors,OldVars,NewVars),
	aleph_delete_list(Lits,Predecessors,P1),
	Depth1 is Depth + 1,
	mark_lits(P1,NewVars,Depth1).

mark_lits([],_,_,P,P,V,V).
mark_lits([Lit|Lits],Depth,GetPreds,PSoFar,P,VSoFar,V):-
	retract('$aleph_local'(marked,Lit/Depth0)), !,
	(Depth < Depth0 ->
		mark_lit(Lit,Depth,GetPreds,VSoFar,P1,V2),
		update_list(P1,PSoFar,P2),
		mark_lits(Lits,Depth,GetPreds,P2,P,V2,V);
		asserta('$aleph_local'(marked,Lit/Depth0)),
		mark_lits(Lits,Depth,GetPreds,PSoFar,P,VSoFar,V)).
mark_lits([Lit|Lits],Depth,GetPreds,PSoFar,P,VSoFar,V):-
	mark_lit(Lit,Depth,GetPreds,VSoFar,P1,V2), !,
	update_list(P1,PSoFar,P2),
	mark_lits(Lits,Depth,GetPreds,P2,P,V2,V).
mark_lits([_|Lits],Depth,GetPreds,PSoFar,P,VSoFar,V):-
	mark_lits(Lits,Depth,GetPreds,PSoFar,P,VSoFar,V).

mark_lit(Lit,Depth,GetPreds,VSoFar,P1,V1):-
	retract('$aleph_sat_litinfo'(Lit,_,Atom,I,O,D)),
	asserta('$aleph_local'(marked,Lit/Depth)),
	asserta('$aleph_sat_litinfo'(Lit,Depth,Atom,I,O,D)),
	(GetPreds = false ->
		P1 = [],
		V1 = VSoFar;
		get_vars(Atom,O,OVars),
		update_list(OVars,VSoFar,V1),
		get_predicates(D,V1,D1),
		mark_lits(D1,Depth,false,[],_,VSoFar,_),
		get_vars(Atom,I,IVars),
		get_predecessors(IVars,[],P1)).

% mark lits that produce outputs that are not used by any other literal
mark_floating_lits(Lit,Last):-
	Lit > Last, !.
mark_floating_lits(Lit,Last):-
	'$aleph_sat_litinfo'(Lit,_,_,_,O,D),
	O \= [],
	(D = []; D = [Lit]), !,
	asserta('$aleph_local'(marked,Lit/0)),
	Lit1 is Lit + 1,
	mark_floating_lits(Lit1,Last).
mark_floating_lits(Lit,Last):-
	Lit1 is Lit + 1,
	mark_floating_lits(Lit1,Last).
	
% mark lits in bottom clause that are specified redundant by user
% requires definition of redundant/2 that have distinguished first arg ``bottom''
mark_redundant_lits(Lit,Last):-
	Lit > Last, !.
mark_redundant_lits(Lit,Last):-
	get_pclause([Lit],[],Atom,_,_,_),
	redundant(bottom,Atom), !,
	asserta('$aleph_local'(marked,Lit/0)),
	Lit1 is Lit + 1,
	mark_redundant_lits(Lit1,Last).
mark_redundant_lits(Lit,Last):-
	Lit1 is Lit + 1,
	mark_redundant_lits(Lit1,Last).

% get literals that are linked and do not link to any others (ie predicates)
get_predicates([],_,[]).
get_predicates([Lit|Lits],Vars,[Lit|T]):-
	'$aleph_sat_litinfo'(Lit,_,Atom,I,_,[]),
	get_vars(Atom,I,IVars),
	aleph_subset1(IVars,Vars), !,
	get_predicates(Lits,Vars,T).
get_predicates([_|Lits],Vars,T):-
	get_predicates(Lits,Vars,T).

% get all predecessors in the bottom clause of a set of literals
get_predecessors([],[]).
get_predecessors([Lit|Lits],P):-
	(Lit = 1 -> Pred = [];
		get_ivars1(false,Lit,IVars),
		get_predecessors(IVars,[],Pred)),
	get_predecessors(Pred,PPred),
	update_list(Pred,PPred,P1),
	get_predecessors(Lits,P2),
	update_list(P2,P1,P).

% get list of literals in the bottom clause that produce a set of vars
get_predecessors([],P,P).
get_predecessors([Var|Vars],PSoFar,P):-
	'$aleph_sat_vars'(Var,_,_,O),
	update_list(O,PSoFar,P1),
	get_predecessors(Vars,P1,P).

% removal of literals in bottom clause by negative-based reduction.
% A greedy strategy is employed, as implemented within the ILP system
% Golem (see Muggleton and Feng, "Efficient induction
% of logic programs", Inductive Logic Programming, S. Muggleton (ed.),
% AFP Press). In this, given a clause H:- B1, B2,...Bn, let Bi be the
% first literal s.t. H:-B1,...,Bi covers no more than the allowable number
% of negatives. The clause H:- Bi,B1,...,Bi-1 is then reduced. The
% process continues until there is no change in the length of a clause
% within an iteration. The algorithm is O(n^2).
rm_nreduce(Last,N):-
	setting(nreduce_bottom,true), !,
	get_litnums(1,Last,BottomLits),
        '$aleph_global'(atoms,atoms(neg,Neg)),
	setting(depth,Depth),
	setting(prooftime,Time),
	setting(proof_strategy,Proof),
	setting(noise,Noise),
	neg_reduce(BottomLits,Neg,Last,Depth/Time/Proof,Noise),
	get_marked(1,Last,Lits),
	length(Lits,N),
	p1_message('negative-based removal'), p_message(N/Last).
rm_nreduce(_,0).

neg_reduce([Head|Body],Neg,Last,DepthTime,Noise):-
	get_pclause([Head],[],Clause,TV,_,_),
	neg_reduce(Body,Clause,TV,2,Neg,DepthTime,Noise,NewLast),
	NewLast \= Last, !,
	NewLast1 is NewLast - 1,
	aleph_remove_n(NewLast1,[Head|Body],Prefix,[LastLit|Rest]),
	mark_lits(Rest),
	insert_lastlit(LastLit,Prefix,Lits1),
	neg_reduce(Lits1,Neg,NewLast,DepthTime,Noise).
neg_reduce(_,_,_,_,_).

neg_reduce([],_,_,N,_,_,_,N).
neg_reduce([L1|Lits],C,TV,N,Neg,ProofFlags,Noise,LastLit):-
	get_pclause([L1],TV,Lit1,TV1,_,_),
	extend_clause(C,Lit1,Clause),
        prove(ProofFlags,neg,Clause,Neg,NegCover,Count),
	Count > Noise, !,
	N1 is N + 1,
	neg_reduce(Lits,Clause,TV1,N1,NegCover,ProofFlags,Noise,LastLit).
neg_reduce(_,_,_,N,_,_,_,N).

% insert_lastlit(LastLit,[1|Lits],Lits1):-
	% find_last_ancestor(Lits,LastLit,1,2,Last),
	% aleph_remove_n(Last,[1|Lits],Prefix,Suffix),
	% aleph_append([LastLit|Suffix],Prefix,Lits1).

insert_lastlit(LastLit,Lits,Lits1):-
	get_predecessors([LastLit],Prefix),
	aleph_delete_list(Prefix,Lits,Suffix),
	aleph_append([LastLit|Suffix],Prefix,Lits1).

	
find_last_ancestor([],_,Last,_,Last):- !.
find_last_ancestor([Lit|Lits],L,_,LitNum,Last):-
	'$aleph_sat_litinfo'(Lit,_,_,_,_,D), 
	aleph_member1(L,D), !,
	NextLit is LitNum + 1,
	find_last_ancestor(Lits,L,LitNum,NextLit,Last).
find_last_ancestor([_|Lits],L,Last0,LitNum,Last):-
	NextLit is LitNum + 1,
	find_last_ancestor(Lits,L,Last0,NextLit,Last).

% removal of literals that are repeated because of mode differences
rm_moderepeats(_,_):-
	'$aleph_sat_litinfo'(Lit1,_,Pred1,_,_,_),
	'$aleph_sat_litinfo'(Lit2,_,Pred1,_,_,_),
	Lit1 >= 1, Lit2 > Lit1,
	retract('$aleph_sat_litinfo'(Lit2,_,Pred1,_,_,_)),
	asserta('$aleph_local'(marked,Lit2/0)),
	fail.
rm_moderepeats(Last,N):-
	'$aleph_local'(marked,_), !,
	get_marked(1,Last,Lits),
	length(Lits,N),
	p1_message('repeated literals'), p_message(N/Last),
	remove_lits(Lits).
rm_moderepeats(_,0).
	
% removal of symmetric literals
rm_symmetric(_,_):-
	'$aleph_global'(symmetric,_),
	'$aleph_sat_litinfo'(Lit1,_,Pred1,[I1|T1],_,_),
	is_symmetric(Pred1,Name,Arity),
	get_vars(Pred1,[I1|T1],S1),
	'$aleph_sat_litinfo'(Lit2,_,Pred2,[I2|T2],_,_),
	Lit1 \= Lit2,
	is_symmetric(Pred2,Name,Arity),
	Pred1 =.. [_|Args1],
	Pred2 =.. [_|Args2],
	symmetric_match(Args1,Args2),
	get_vars(Pred2,[I2|T2],S2),
	equal_set(S1,S2),
	asserta('$aleph_local'(marked,Lit2/0)),
	retract('$aleph_sat_litinfo'(Lit2,_,Pred2,[I2|T2],_,_)),
	fail.
rm_symmetric(Last,N):-
	'$aleph_local'(marked,_), !,
	get_marked(1,Last,Lits),
	length(Lits,N),
	p1_message('symmetric literals'), p_message(N/Last),
	remove_lits(Lits).
rm_symmetric(_,0).

is_symmetric(not(Pred),not(Name),Arity):-
	!,
	functor(Pred,Name,Arity),
	'$aleph_global'(symmetric,symmetric(Name/Arity)).
is_symmetric(Pred,Name,Arity):-
	functor(Pred,Name,Arity),
	'$aleph_global'(symmetric,symmetric(Name/Arity)).

symmetric_match([],[]).
symmetric_match([aleph_const(Term)|Terms1],[aleph_const(Term)|Terms2]):-
	!,
	symmetric_match(Terms1,Terms2).
symmetric_match([Term1|Terms1],[Term2|Terms2]):-
	integer(Term1), integer(Term2),
	symmetric_match(Terms1,Terms2).
	
% removal of literals that are repeated because of commutativity
rm_commutative(_,_):-
	'$aleph_global'(commutative,commutative(Name/Arity)),
	p1_message('checking commutative literals'), p_message(Name/Arity),
	functor(Pred,Name,Arity), functor(Pred1,Name,Arity),
	'$aleph_sat_litinfo'(Lit1,_,Pred,[I1|T1],O1,_),
        % check for marked literals
	% (SWI-Prolog specific: suggested by Vasili Vrubleuski)
        \+('$aleph_local'(marked,Lit1/0)),
	get_vars(Pred,[I1|T1],S1),
	'$aleph_sat_litinfo'(Lit2,_,Pred1,[I2|T2],O2,_),
	Lit1 \= Lit2 ,
	O1 = O2,
	get_vars(Pred1,[I2|T2],S2),
	equal_set(S1,S2),
	asserta('$aleph_local'(marked,Lit2/0)),
	retract('$aleph_sat_litinfo'(Lit2,_,Pred1,[I2|T2],_,_)),
	fail.
rm_commutative(Last,N):-
	'$aleph_local'(marked,_), !,
	get_marked(1,Last,Lits),
	length(Lits,N),
	p1_message('commutative literals'), p_message(N/Last),
	remove_lits(Lits).
rm_commutative(_,0).

% recursive marking of literals that do not contribute to establishing
% variable chains to output vars in the head
% or produce outputs that are not used by any literal
% controlled by setting flag check_useless
rm_uselesslits(_,0):-
	setting(check_useless,false), !.
rm_uselesslits(Last,N):-
	'$aleph_sat'(hovars,OVars),
	OVars \= [], !,
	get_predecessors(OVars,[],P),
	'$aleph_sat'(hivars,IVars),
	mark_lits(P,IVars,0),
	get_unmarked(1,Last,Lits),
	length(Lits,N),
	p1_message('useless literals'), p_message(N/Last),
	remove_lits(Lits).
rm_uselesslits(_,0).

% call user-defined predicate redundant/2 to remove redundant
% literals from bottom clause. Redundancy checking only done on request
rm_redundant(_,0):-
	setting(check_redundant,false), !.
rm_redundant(Last,N):-
	mark_redundant_lits(1,Last),
	get_marked(1,Last,Lits),
	length(Lits,N),
	p1_message('redundant literals'), p_message(N/Last),
	remove_lits(Lits).

% get a list of unmarked literals
get_unmarked(Lit,Last,[]):-
	Lit > Last, !.
get_unmarked(Lit,Last,Lits):-
	retract('$aleph_local'(marked,Lit/_)), !,
	Next is Lit + 1,
	get_unmarked(Next,Last,Lits).
get_unmarked(Lit,Last,[Lit|Lits]):-
	retract('$aleph_sat_litinfo'(Lit,_,_,_,_,_)), !,
	Next is Lit + 1,
	get_unmarked(Next,Last,Lits).
get_unmarked(Lit,Last,Lits):-
	Next is Lit + 1,
	get_unmarked(Next,Last,Lits).

% get a list of marked literals
get_marked(Lit,Last,[]):-
	Lit > Last, !.
get_marked(Lit,Last,[Lit|Lits]):-
	retract('$aleph_local'(marked,Lit/_)), !,
	(retract('$aleph_sat_litinfo'(Lit,_,_,_,_,_)) ->
		true;
		true),
	Next is Lit + 1,
	get_marked(Next,Last,Lits).
get_marked(Lit,Last,Lits):-
	Next is Lit + 1,
	get_marked(Next,Last,Lits).

% update descendent lists of literals by removing useless literals
remove_lits(L):-
	retract('$aleph_sat_litinfo'(Lit,Depth,A,I,O,D)), 
	aleph_delete_list(L,D,D1),
	asserta('$aleph_sat_litinfo'(Lit,Depth,A,I,O,D1)),
	fail.
remove_lits(_).

% generate a new literal at depth Depth: forced backtracking will give all lits
gen_layer(Name/Arity,Depth):-
	(Name/Arity = (not)/1 ->
		'$aleph_global'(modeb,modeb(NSucc,not(Mode))),
		functor(Mode,Name1,Arity1),
		functor(Lit1,Name1,Arity1),
		once(copy_modeterms(Mode,Lit1,Arity1)),
		Lit = not(Lit1);
		functor(Mode,Name,Arity),
		functor(Lit,Name,Arity),
		'$aleph_global'(modeb,modeb(NSucc,Mode)),
		once(copy_modeterms(Mode,Lit,Arity))),
	split_args(Mode,Mode,Input,Output,Constants),
	(Input = [] -> Call1 = true, Call2 = true;
		aleph_delete(Arg/Type,Input,OtherInputs),
		Depth1 is Depth - 1,
		construct_incall(Lit,Depth1,[Arg/Type],Call1),
		construct_call(Lit,Depth,OtherInputs,Call2)),
	Call1,
	Call2,
	aleph_background_predicate(Lit),
	get_successes(Lit,NSucc,mode(Mode,Input,Output,Constants)),
	fail.
gen_layer(_,_).

get_successes(Literal,1,M):-
	depth_bound_call(Literal), 
	update_atoms(Literal,M), !.
get_successes(Literal,*,M):-
	depth_bound_call(Literal), 
	update_atoms(Literal,M).
get_successes(Literal,N,M):-
	integer(N),
	N > 1,
	reset_succ,
	get_nsuccesses(Literal,N,M).

% get at most N matches for a literal
get_nsuccesses(Literal,N,M):-
	depth_bound_call(Literal), 
	retract('$aleph_local'(last_success,Succ0)),
	Succ0 < N,
	Succ1 is Succ0 + 1,
	update_atoms(Literal,M),
	asserta('$aleph_local'(last_success,Succ1)),
	(Succ1 >= N -> !; true).

update_atoms(Atom,M):-
	'$aleph_sat_atom'(Atom,M), !.
update_atoms(Atom,M):-
	assertz('$aleph_sat_atom'(Atom,M)).

% call with input term that is an ouput of a previous literal
construct_incall(_,_,[],true):- !.
construct_incall(not(Lit),Depth,Args,Call):-
	!,
	construct_incall(Lit,Depth,Args,Call).
construct_incall(Lit,Depth,[Pos/Type],Call):-
	!,
	Call = legal_term(exact,Depth,Type,Term),
	tparg(Pos,Lit,Term).
construct_incall(Lit,Depth,[Pos/Type|Args],(Call,Calls)):-
	tparg(Pos,Lit,Term),
	Call = legal_term(exact,Depth,Type,Term),
	(var(Depth)-> construct_incall(Lit,_,Args,Calls);
		construct_incall(Lit,Depth,Args,Calls)).

construct_call(_,_,[],true):- !.
construct_call(not(Lit),Depth,Args,Call):-
	!,
	construct_call(Lit,Depth,Args,Call).
construct_call(Lit,Depth,[Pos/Type],Call):-
	!,
	Call = legal_term(upper,Depth,Type,Term),
	tparg(Pos,Lit,Term).
construct_call(Lit,Depth,[Pos/Type|Args],(Call,Calls)):-
	tparg(Pos,Lit,Term),
	Call = legal_term(upper,Depth,Type,Term),
	construct_call(Lit,Depth,Args,Calls).

% generator of legal terms seen so far
legal_term(exact,Depth,Type,Term):-
	'$aleph_sat_terms'(TNo,Depth,Term,Type),
	once('$aleph_sat_vars'(_,TNo,_,[_|_])).
% legal_term(exact,Depth,Type,Term):-
	% '$aleph_sat_varscopy'(NewVar,OldVar,Depth),
	% once('$aleph_sat_vars'(NewVar,TNo,_,_)),
	% '$aleph_sat_terms'(TNo,_,Term,Type),_).
legal_term(upper,Depth,Type,Term):-
	'$aleph_sat_terms'(TNo,Depth1,Term,Type),
	Depth1 \= unknown,
	Depth1 < Depth,
	once('$aleph_sat_vars'(_,TNo,_,[_|_])).
% legal_term(upper,Depth,Type,Term):-
	% '$aleph_sat_varscopy'(NewVar,OldVar,Depth),
	% once('$aleph_sat_vars'(NewVar,TNo,_,_)),
	% '$aleph_sat_terms'(TNo,Depth1,Term,Type),
	% Depth1 \= unknown.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% V A R I A B L E  -- S P L I T T I N G


split_vars(Depth,FAtom,I,O,C,SplitAtom,IVars,OVars,Equivs):-
	setting(splitvars,true), !,
        get_args(FAtom,I,[],IVarList),
        get_args(FAtom,O,[],OVarList),
	get_var_equivs(Depth,IVarList,OVarList,IVars,OVars0,Equivs0),
	(Equivs0 = [] ->
		OVars = OVars0, SplitAtom = FAtom, Equivs = Equivs0;
		functor(FAtom,Name,Arity),
		functor(SplitAtom,Name,Arity),
		copy_args(FAtom,SplitAtom,I),
		copy_args(FAtom,SplitAtom,C),
		rename_ovars(O,Depth,FAtom,SplitAtom,Equivs0,Equivs),
		get_argterms(SplitAtom,O,[],OVars)).
	% write('splitting: '), write(FAtom), write(' to: '), write(SplitAtom), nl.
split_vars(_,FAtom,I,O,_,FAtom,IVars,OVars,[]):-
	get_vars(FAtom,I,IVars),
	get_vars(FAtom,O,OVars).

% get equivalent classes of variables from co-references 
get_var_equivs(Depth,IVarList,OVarList,IVars,OVars,Equivs):-
	sort(IVarList,IVars),
	sort(OVarList,OVars),
	(Depth = 0 ->
		intersect1(IVars,OVarList,IOCoRefs,_),
		get_repeats(IVarList,IOCoRefs,ICoRefs);
		intersect1(IVars,OVarList,ICoRefs,_)),
	get_repeats(OVarList,ICoRefs,CoRefs),
	add_equivalences(CoRefs,Depth,Equivs).

add_equivalences([],_,[]).
add_equivalences([Var|Vars],Depth,[Var/E|Rest]):-
	% (Depth = 0 -> E = []; E = [Var]),
	E = [Var],
	add_equivalences(Vars,Depth,Rest).


get_repeats([],L,L).
get_repeats([Var|Vars],Ref1,L):-
	aleph_member1(Var,Vars), !,
	update(Ref1,Var,Ref2),
	get_repeats(Vars,Ref2,L).
get_repeats([_|Vars],Ref,L):-
	get_repeats(Vars,Ref,L).

% rename all output vars that are co-references
% updates vars database and return equivalent class of variables
rename_ovars([],_,_,_,L,L).
rename_ovars([ArgNo|Args],Depth,Old,New,CoRefs,Equivalences):-
	(ArgNo = Pos/_ -> true; Pos = ArgNo),
	tparg(Pos,Old,OldVar),
	aleph_delete(OldVar/Equiv,CoRefs,Rest), !,
	copy_var(OldVar,NewVar,Depth),
	tparg(Pos,New,NewVar),
	rename_ovars(Args,Depth,Old,New,[OldVar/[NewVar|Equiv]|Rest],Equivalences).
rename_ovars([ArgNo|Args],Depth,Old,New,CoRefs,Equivalences):-
	(ArgNo = Pos/_ -> true; Pos = ArgNo),
	tparg(Pos,Old,OldVar),
	tparg(Pos,New,OldVar),
	rename_ovars(Args,Depth,Old,New,CoRefs,Equivalences).

% create new  equalities to  allow co-references to re-appear in search
insert_eqs([],_,L,L).
insert_eqs([OldVar/Equivs|Rest],Depth,Last,NewLast):-
	'$aleph_sat_vars'(OldVar,TNo,_,_),
	'$aleph_sat_terms'(TNo,_,_,Type),
	add_eqs(Equivs,Depth,Type,Last,Last1),
	insert_eqs(Rest,Depth,Last1,NewLast).

add_eqs([],_,_,L,L).
add_eqs([V1|Rest],Depth,Type,Last,NewLast):-
	add_eqs(Rest,Depth,V1,Type,Last,Last1),
	add_eqs(Rest,Depth,Type,Last1,NewLast).

add_eqs([],_,_,_,L,L).
add_eqs([Var2|Rest],Depth,Var1,Type,Last,NewLast):-
	(Depth = 0 -> 
		add_lit(Last,false,(Var1=Var2),[1/Type],[2/Type],[Var1],[Var2],Last1);
		add_lit(Last,false,(Var1=Var2),[1/Type,2/Type],[],[Var1,Var2],[],Last1)),
	add_eqs(Rest,Depth,Var1,Type,Last1,NewLast).
	


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% utilities for updating mappings between terms and variables

% integrate terms specified by a list of arguments
% integrating a term means:
%	updating 2 databases: terms and vars
%	terms contains the term along with a term-id
%	vars contains a var-id <-> term-id mapping
% var and term-ids are integers
integrate_args(_,_,[]).
integrate_args(Depth,Literal,[Pos/Type|T]):-
        tparg(Pos,Literal,Term),
        integrate_term(Depth,Term/Type),
	(retract('$aleph_sat_terms'(TNo,Depth,Term,unknown)) ->
		asserta('$aleph_sat_terms'(TNo,Depth,Term,Type));
		true),
        integrate_args(Depth,Literal,T).


% integrate a term
integrate_term(Depth,Term/Type):-
        '$aleph_sat_terms'(TNo,Depth,Term,Type),
        '$aleph_sat_vars'(_,TNo,_,[_|_]), !.
integrate_term(Depth,Term/Type):-
        '$aleph_sat_terms'(TNo,Depth1,Term,Type),
        (Type = unknown ; '$aleph_sat_vars'(_,TNo,_,[])), !,
	(Depth1 = unknown ->
        	retract('$aleph_sat_terms'(TNo,Depth1,Term,Type)),
		asserta('$aleph_sat_terms'(TNo,Depth,Term,Type));
		true).
integrate_term(_,Term/Type):-
        '$aleph_sat_terms'(_,_,Term,Type),
        Type \= unknown,
        !.
integrate_term(Depth,Term/Type):-
	retract('$aleph_sat'(lastterm,Num)),
	retract('$aleph_sat'(lastvar,Var0)),
	TNo is Num + 1,
	Var is Var0 + 1,
	asserta('$aleph_sat'(lastterm,TNo)),
	asserta('$aleph_sat'(lastvar,Var)),
	asserta('$aleph_sat_vars'(Var,TNo,[],[])),
	asserta('$aleph_sat_terms'(TNo,Depth,Term,Type)).


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

% split_args(+Lit,?Mode,-Input,-Output,-Constants)
%       return term-places and types of +,-, and # args in Lit
%       by finding a matching mode declaration if Mode is given
%       otherwise first mode that matches is used
split_args(Lit,Mode,Input,Output,Constants):-
        functor(Lit,Psym,Arity),
	find_mode(mode,Psym/Arity,Mode),
        functor(Template,Psym,Arity),
	copy_modeterms(Mode,Template,Arity),
	Template = Lit,
	tp(Mode,TPList),
	split_tp(TPList,Input,Output,Constants).

% split_tp(+TPList,-Input,-Output,-Constants)
%	split term-place/type list into +,-,#
split_tp([],[],[],[]).
split_tp([(+Type)/Place|TP],[Place/Type|Input],Output,Constants):-
	!,
	split_tp(TP,Input,Output,Constants).
split_tp([(-Type)/Place|TP],Input,[Place/Type|Output],Constants):-
	!,
	split_tp(TP,Input,Output,Constants).
split_tp([(#Type)/Place|TP],Input,Output,[Place/Type|Constants]):-
	!,
	split_tp(TP,Input,Output,Constants).
split_tp([_|TP],Input,Output,Constants):-
	split_tp(TP,Input,Output,Constants).

% tp(+Literal,-TPList)
%	return terms and places in Literal
tp(Literal,TPList):-
	functor(Literal,_,Arity),
	tp_list(Literal,Arity,[],[],TPList).

tp_list(_,0,_,L,L):- !.
tp_list(Term,Pos,PlaceList,TpSoFar,TpList):-
	arg(Pos,Term,Arg),
	aleph_append([Pos],PlaceList,Places),
	unwrap_term(Arg,Places,[Arg/Places|TpSoFar],L1),
	Pos1 is Pos - 1,
	tp_list(Term,Pos1,PlaceList,L1,TpList).

unwrap_term(Term,_,L,L):-
	var(Term), !.
unwrap_term(Term,Place,TpSoFar,TpList):-
	functor(Term,_,Arity),
	tp_list(Term,Arity,Place,TpSoFar,TpList).

get_determs(PSym/Arity,L):-
	findall(Pred,'$aleph_global'(determination,determination(PSym/Arity,Pred)),L).

get_modes(PSym/Arity,L):-
	functor(Lit,PSym,Arity),
	findall(Lit,'$aleph_global'(mode,mode(_,Lit)),L).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% S E A R C H

% basic search engine for single clause search
search(S,Nodes):-
	arg(36,S,Time),
	Inf is inf,
	Time =\= Inf, 
	SearchTime is integer(Time),
	SearchTime > 0, !,
	catch(time_bound_call(SearchTime,searchlimit,graphsearch(S,_)),
		searchlimit,p_message('Time limit reached')),
	'$aleph_search'(current,current(_,Nodes,_)).
search(S,Nodes):-
	graphsearch(S,Nodes).

% basic search engine for theory-based search
tsearch(S,Nodes):-
        arg(36,S,Time),
	Inf is inf,
        Time =\= Inf,
        SearchTime is integer(Time),
        SearchTime > 0, !,
	alarm(SearchTime,throw(searchlimit),Id),
        catch(theorysearch(S,Nodes),searchlimit,p_message('Time limit reached')),
	remove_alarm(Id).
tsearch(S,Nodes):-
        theorysearch(S,Nodes).

graphsearch(S,Nodes):-
	next_node(_), !,
        arg(3,S,RefineOp),
	arg(23,S,LazyPreds),
        repeat,
	next_node(NodeRef),
        once(retract('$aleph_search'(current,current(LastE,Last,BestSoFar)))),
        expand(RefineOp,S,NodeRef,Node,Path,MinLength,Succ,PosCover,NegCover,OVars,
		PrefixClause,PrefixTV,PrefixLength),
        ((LazyPreds = []; RefineOp \= false)  -> Succ1 = Succ;
		lazy_evaluate(Succ,LazyPreds,Path,PosCover,NegCover,Succ1)),
	NextE is LastE + 1,
        get_gains(S,Last,BestSoFar,Path,PrefixClause,PrefixTV,PrefixLength,
                MinLength,Succ1,PosCover,NegCover,OVars,NextE,Last0,NextBest0),
	(RefineOp = false ->
        	get_sibgains(S,Node,Last0,NextBest0,Path,PrefixClause,
			PrefixTV,PrefixLength,MinLength,PosCover,NegCover,
			OVars,NextE,Last1,NextBest);
		Last1 = Last0, NextBest = NextBest0),
        asserta('$aleph_search'(current,current(NextE,Last1,NextBest))),
        NextL is Last + 1,
        asserta('$aleph_search_expansion'(NextE,Node,NextL,Last1)),
        (discontinue_search(S,NextBest,Last1) ->
                '$aleph_search'(current,current(_,Nodes,_));
                prune_open(S,BestSoFar,NextBest),
                get_nextbest(S,Next),
		Next = none,
		'$aleph_search'(current,current(_,Nodes,_))),
	!.
graphsearch(_,Nodes):-
	'$aleph_search'(current,current(_,Nodes,_)).

theorysearch(S,Nodes):-
        next_node(_), !,
        '$aleph_global'(atoms,atoms(pos,Pos)),
        '$aleph_global'(atoms,atoms(neg,Neg)),
        interval_count(Pos,P),
        interval_count(Neg,N),
        repeat,
        next_node(NodeRef),
	'$aleph_search_node'(NodeRef,Theory,_,_,_,_,_,_),
        once(retract('$aleph_search'(current,current(_,Last,BestSoFar)))),
        get_theory_gain(S,Last,BestSoFar,Theory,Pos,Neg,P,N,NextBest,Last1),
        asserta('$aleph_search'(current,current(0,Last1,NextBest))),
        (discontinue_search(S,NextBest,Last1) ->
                '$aleph_search'(current,current(_,Nodes,_));
                prune_open(S,BestSoFar,NextBest),
                get_nextbest(S,Next),
                Next = none,
                '$aleph_search'(current,current(_,Nodes,_))),
	 !.
theorysearch(_,Nodes):-
        '$aleph_search'(current,current(_,Nodes,_)).

next_node(NodeRef):-
	once('$aleph_search'(nextnode,NodeRef)), !.

get_search_settings(S):-
        functor(S,set,47),
	setting(nodes,MaxNodes), arg(1,S,MaxNodes),
	setting(explore,Explore), arg(2,S,Explore),
	setting(refineop,RefineOp), arg(3,S,RefineOp),
	setting(searchstrat,SearchStrat), setting(evalfn,EvalFn),
	arg(4,S,SearchStrat/EvalFn),
	(setting(greedy,Greedy)-> arg(5,S,Greedy); arg(5,S,false)),
	setting(verbosity,Verbose), arg(6,S,Verbose),
	setting(clauselength,CLength), arg(7,S,CLength),
	setting(caching,Cache), arg(8,S,Cache),
	(setting(prune_defs,Prune)-> arg(9,S,Prune); arg(9,S,false)),
	setting(lazy_on_cost,LCost), arg(10,S,LCost),
	setting(lazy_on_contradiction,LContra), arg(11,S,LContra),
	setting(lazy_negs,LNegs), arg(12,S,LNegs),
	setting(minpos,MinPos), arg(13,S,MinPos),
	setting(depth,Depth), arg(14,S,Depth),
	setting(cache_clauselength,CCLim), arg(15,S,CCLim),
        ('$aleph_global'(size,size(pos,PSize))-> arg(16,S,PSize); arg(16,S,0)),
	setting(noise,Noise), arg(17,S,Noise),
	setting(minacc,MinAcc), arg(18,S,MinAcc),
	setting(minscore,MinScore), arg(19,S,MinScore),
        ('$aleph_global'(size,size(rand,RSize))-> arg(20,S,RSize); arg(20,S,0)),
	setting(mingain,MinGain), arg(21,S,MinGain),
	setting(search,Search), arg(22,S,Search),
	findall(PN/PA,'$aleph_global'(lazy_evaluate,lazy_evaluate(PN/PA)),LazyPreds),
	arg(23,S,LazyPreds),
        ('$aleph_global'(size,size(neg,NSize))-> arg(24,S,NSize); arg(24,S,0)),
	setting(openlist,OSize), arg(25,S,OSize),
        setting(check_redundant,RCheck), arg(26,S,RCheck),
        ('$aleph_sat'(eq,Eq) -> arg(27,S,Eq); arg(27,S,false)),
        ('$aleph_sat'(hovars,HOVars) -> arg(28,S,HOVars); arg(28,S,HOVars)),
	setting(prooftime,PTime), arg(29,S,PTime),
	setting(construct_bottom,CBott), arg(30,S,CBott),
	(get_ovars1(false,1,HIVars) ->  arg(31,S,HIVars); arg(31,S,[])),
	setting(language,Lang), arg(32,S,Lang),
	setting(splitvars,Split), arg(33,S,Split),
	setting(proof_strategy,Proof), arg(34,S,Proof),
	setting(portray_search,VSearch), arg(35,S,VSearch),
	setting(searchtime,Time), arg(36,S,Time),
	setting(optimise_clauses,Optim), arg(37,S,Optim),
	setting(newvars,NewV), arg(38,S,NewV),
	(setting(rls_type,RlsType) -> arg(39,S,RlsType);arg(39,S,false)),
	setting(minposfrac,MinPosFrac), arg(40,S,MinPosFrac),
	(setting(recursion,Recursion) -> true; Recursion = false),
	prolog_type(Prolog), arg(41,S,Prolog),
	setting(interactive,Interactive), arg(42,S,Interactive),
	setting(lookahead,LookAhead), arg(43,S,LookAhead),
	(setting(construct_features,Features)-> arg(44,S,Features); arg(44,S,false)),
	setting(max_features,FMax), arg(45,S,FMax),
	setting(subsample,SS), arg(46,S,SS),
	setting(subsamplesize,SSize), arg(47,S,SSize).

% stop search from proceeding if certain
% conditions are reached. These are:
%	. minacc and minpos values reached in rrr search
%	. best hypothesis has accuracy 1.0 if evalfn=accuracy
%	. best hypothesis covers all positive examples
discontinue_search(S,[P,_,_,F|_]/_,_):-
	arg(39,S,RlsType),
	RlsType = rrr, 
	arg(13,S,MinPos),
	P >= MinPos,
	arg(19,S,MinScore),
	F >= MinScore, !.
discontinue_search(S,_,Nodes):-
        arg(1,S,MaxNodes),
        Nodes >= MaxNodes, !,
	p_message('node limit reached').
discontinue_search(S,_,_):-
        arg(44,S,Features),
	Features = true,
	arg(45,S,FMax),
	'$aleph_search'(last_good,LastGood),
        LastGood >= FMax, !,
	p_message('feature limit reached').
discontinue_search(S,[_,_,_,F|_]/_,_):-
        arg(4,S,_/Evalfn),
	Evalfn = accuracy,
	F = 1.0, !.
discontinue_search(S,Best,_):-
	arg(2,S,Explore),
	Explore = false,
        arg(4,S,_/Evalfn),
	Evalfn \= user,
	Evalfn \= posonly,
	arg(22,S,Search),
	Search \= ic,
	Best = [P|_]/_,
	arg(16,S,P).

update_max_head_count(N,0):-
	retractall('$aleph_local'(max_head_count,_)),
	asserta('$aleph_local'(max_head_count,N)), !.
update_max_head_count(Count,Last):-
	'$aleph_search_node'(Last,LitNum,_,_,PosCover,_,_,_), !,
	asserta('$aleph_local'(head_lit,LitNum)),
	interval_count(PosCover,N),
	Next is Last - 1,
	(N > Count -> update_max_head_count(N,Next);
		update_max_head_count(Count,Next)).
update_max_head_count(Count,Last):-
	Next is Last - 1,
	update_max_head_count(Count,Next).

expand(false,S,NodeRef,NodeRef,Path1,Length,Descendents,PosCover,NegCover,OVars,C,TV,CL):-
	!,
        '$aleph_search_node'(NodeRef,LitNum,Path,Length/_,PCover,NCover,OVars,_),
	arg(46,S,SSample),
	(SSample = false -> PosCover = PCover, NegCover = NCover;
		get_sample_cover(S,PosCover,NegCover)),
        aleph_append([LitNum],Path,Path1),
	get_pclause(Path1,[],C,TV,CL,_),
        '$aleph_sat_litinfo'(LitNum,_,_,_,_,Dependents),
        intersect1(Dependents,Path1,_,Succ),
        check_parents(Succ,OVars,Descendents,_).
expand(_,S,NodeRef,NodeRef,Path1,Length,[_],PosCover,NegCover,OVars,_,_,_):-
        retract('$aleph_search_node'(NodeRef,_,Path1,Length/_,_,_,OVars,_)),
	get_sample_cover(S,PosCover,NegCover).

get_sample_cover(S,PosCover,NegCover):-
        arg(5,S,Greedy),
        (Greedy = true ->
                '$aleph_global'(atoms_left,atoms_left(pos,PCover));
                arg(16,S,PSize),
                PCover = [1-PSize]),
        arg(4,S,_/Evalfn),
	(Evalfn = posonly -> 
                '$aleph_global'(atoms_left,atoms_left(rand,NCover));
                arg(24,S,NSize),
                NCover = [1-NSize]),
	arg(46,S,SSample),
	(SSample = false -> PosCover = PCover, NegCover = NCover;
		arg(47,S,SampleSize),
		interval_sample(SampleSize,PCover,PosCover),
		interval_sample(SampleSize,NCover,NegCover)).

get_ovars([],_,V,V).
get_ovars([LitNum|Lits],K,VarsSoFar,Vars):-
	get_ovars1(K,LitNum,OVars),
	aleph_append(VarsSoFar,OVars,Vars1),
	get_ovars(Lits,K,Vars1,Vars).

get_ovars1(false,LitNum,OVars):-
	'$aleph_sat_ovars'(LitNum,OVars), !.
get_ovars1(false,LitNum,OVars):-
	!,
	'$aleph_sat_litinfo'(LitNum,_,Atom,_,O,_),
	get_vars(Atom,O,OVars).
get_ovars1(K,LitNum,OVars):-
	'$aleph_sat_ovars'(LitNum,K,OVars), !.
get_ovars1(K,LitNum,OVars):-
	'$aleph_sat_litinfo'(LitNum,K,_,Atom,_,O,_),
	get_vars(Atom,O,OVars).

% get set of vars at term-places specified
get_vars(not(Literal),Args,Vars):-
	!,
	get_vars(Literal,Args,Vars).
get_vars(_,[],[]).
get_vars(Literal,[ArgNo|Args],Vars):-
	(ArgNo = Pos/_ -> true; Pos = ArgNo),
	tparg(Pos,Literal,Term),
	get_vars_in_term([Term],TV1),
	get_vars(Literal,Args,TV2),
	update_list(TV2,TV1,Vars).

get_vars_in_term([],[]).
get_vars_in_term([Var|Terms],[Var|TVars]):-
	integer(Var), !,
	get_vars_in_term(Terms,TVars).
get_vars_in_term([Term|Terms],TVars):-
	Term =.. [_|Terms1],
	get_vars_in_term(Terms1,TV1),
	get_vars_in_term(Terms,TV2),
	update_list(TV2,TV1,TVars).

% get terms at term-places specified
% need not be variables
get_argterms(not(Literal),Args,TermsSoFar,Terms):-
        !,
        get_argterms(Literal,Args,TermsSoFar,Terms).
get_argterms(_,[],Terms,Terms).
get_argterms(Literal,[ArgNo|Args],TermsSoFar,Terms):-
	(ArgNo = Pos/_ -> true; Pos = ArgNo),
        tparg(Pos,Literal,Term),
        update(TermsSoFar,Term,T1),
        get_argterms(Literal,Args,T1,Terms).

% get list of terms at arg positions specified
get_args(not(Literal),Args,TermsSoFar,Terms):-
        !,
        get_args(Literal,Args,TermsSoFar,Terms).
get_args(_,[],Terms,Terms).
get_args(Literal,[ArgNo|Args],TermsSoFar,Terms):-
	(ArgNo = Pos/_ -> true; Pos = ArgNo),
        tparg(Pos,Literal,Term),
        get_args(Literal,Args,[Term|TermsSoFar],Terms).


get_ivars([],_,V,V).
get_ivars([LitNum|Lits],K,VarsSoFar,Vars):-
	get_ivars1(K,LitNum,IVars),
	aleph_append(VarsSoFar,IVars,Vars1),
	get_ivars(Lits,K,Vars1,Vars).

get_ivars1(false,LitNum,IVars):-
	'$aleph_sat_ivars'(LitNum,IVars), !.
get_ivars1(false,LitNum,IVars):-
	!,
	'$aleph_sat_litinfo'(LitNum,_,Atom,I,_,_),
	get_vars(Atom,I,IVars).
get_ivars1(K,LitNum,IVars):-
	'$aleph_sat_ivars'(LitNum,K,IVars), !.
get_ivars1(K,LitNum,IVars):-
	'$aleph_sat_litinfo'(LitNum,K,_,Atom,I,_,_),
	get_vars(Atom,I,IVars).

check_parents([],_,[],[]).
check_parents([LitNum|Lits],OutputVars,[LitNum|DLits],Rest):-
	get_ivars1(false,LitNum,IVars),
	aleph_subset1(IVars,OutputVars), !,
	check_parents(Lits,OutputVars,DLits,Rest).
check_parents([LitNum|Lits],OutputVars,DLits,[LitNum|Rest]):-
	check_parents(Lits,OutputVars,DLits,Rest), !.

get_gains(S,Last,Best,_,_,_,_,_,_,_,_,_,_,Last,Best):-
        discontinue_search(S,Best,Last), !.
get_gains(_,Last,Best,_,_,_,_,_,[],_,_,_,_,Last,Best):- !.
get_gains(S,Last,Best,Path,C,TV,L,Min,[L1|Succ],Pos,Neg,OVars,E,Last1,NextBest):-
        get_gain(S,upper,Last,Best,Path,C,TV,L,Min,L1,Pos,Neg,OVars,E,Best1,Node1), !,
        get_gains(S,Node1,Best1,Path,C,TV,L,Min,Succ,Pos,Neg,OVars,E,Last1,NextBest).
get_gains(S,Last,BestSoFar,Path,C,TV,L,Min,[_|Succ],Pos,Neg,OVars,E,Last1,NextBest):-
        get_gains(S,Last,BestSoFar,Path,C,TV,L,Min,Succ,Pos,Neg,OVars,E,Last1,NextBest),
        !.

get_sibgains(S,Node,Last,Best,Path,C,TV,L,Min,Pos,Neg,OVars,E,Last1,NextBest):-
        '$aleph_search_node'(Node,LitNum,_,_,_,_,_,OldE),
        '$aleph_search_expansion'(OldE,_,_,LastSib),
        '$aleph_sat_litinfo'(LitNum,_,_,_,_,Desc),
        Node1 is Node + 1,
        arg(31,S,HIVars),
        aleph_delete_list(HIVars,OVars,LVars),
        get_sibgain(S,LVars,LitNum,Desc,Node1,LastSib,Last,
                Best,Path,C,TV,L,Min,Pos,Neg,OVars,E,NextBest,Last1), !.

get_sibgain(S,_,_,_,Node,Node1,Last,Best,_,_,_,_,_,_,_,_,_,Best,Last):-
        (Node > Node1;
        discontinue_search(S,Best,Last)), !.
get_sibgain(S,LVars,LitNum,Desc,Node,LastSib,Last,Best,Path,C,TV,L,Min,Pos,Neg,OVars,E,LBest,LNode):-
        arg(23,S,Lazy),
        get_sibpncover(Lazy,Node,Desc,Pos,Neg,Sib1,PC,NC),
        lazy_evaluate([Sib1],Lazy,Path,PC,NC,[Sib]),
        get_ivars1(false,Sib,SibIVars),
        (intersects(SibIVars,LVars) -> Flag = upper;
                get_ovars1(false,Sib,SibOVars),
                (intersects(SibOVars,LVars) -> Flag = upper; Flag = exact)),
        get_gain(S,Flag,Last,Best,Path,C,TV,L,Min,Sib,PC,NC,OVars,E,Best1,Node1), !,
        NextNode is Node + 1,
        get_sibgain(S,LVars,LitNum,Desc,NextNode,LastSib,Node1,Best1,Path,C,TV,L,
                        Min,Pos,Neg,OVars,E,LBest,LNode), !.
get_sibgain(S,LVars,LitNum,Desc,Node,LastSib,Last,Best,Path,C,TV,L,Min,Pos,Neg,OVars,E,Best1,Node1):-
	NextNode is Node + 1,
        get_sibgain(S,LVars,LitNum,Desc,NextNode,LastSib,Last,Best,Path,C,TV,L,
                        Min,Pos,Neg,OVars,E,Best1,Node1), !.


get_sibgain(S,LVars,LitNum,Node,LastSib,Last,Best,Path,C,TV,L,Min,Pos,Neg,OVars,E,Best1,Node1):-
	NextNode is Node + 1,
	get_sibgain(S,LVars,LitNum,NextNode,LastSib,Last,Best,Path,C,TV,L,Min,Pos,Neg,
			OVars,E,Best1,Node1), !.

get_sibpncover(Lazy,NodeNum,Desc,Pos,Neg,Sib,PC,NC):-
        '$aleph_search_node'(NodeNum,Sib,_,_,Pos1,Neg1,_,_),
        '$aleph_sat_litinfo'(Sib,_,Atom,_,_,_),
        \+(aleph_member1(Sib,Desc)),
        functor(Atom,Name,Arity),
        (aleph_member1(Name/Arity,Lazy) ->
                PC = Pos, NC = Neg;
                calc_intersection(Pos,Pos1,PC),
                calc_intersection(Neg,Neg1,NC)).

% in some cases, it is possible to simply use the intersection of
% covers cached. The conditions under which this is possible was developed
% in discussions with James Cussens
calc_intersection(A1/[B1-L1],A2/[B2-L2],A/[B-L]):-
	!,
	intervals_intersection(A1,A2,A),
	B3 is max(B1,B2),
	(intervals_intersects(A1,[B2-L2],X3-_) -> true; X3 = B3),
	(intervals_intersects(A2,[B1-L1],X4-_) -> true; X4 = B3),
	B4 is min(X3,B3),
	B is min(X4,B4),
	L is max(L1,L2).
calc_intersection(A1/_,A2,A):-
	!,
	intervals_intersection(A1,A2,A).
calc_intersection(A1,A2/_,A):-
	!,
	intervals_intersection(A1,A2,A).
calc_intersection(A1,A2,A):-
	intervals_intersection(A1,A2,A).

get_gain(S,_,Last,Best,Path,_,_,_,MinLength,_,Pos,Neg,OVars,E,Best1,NewLast):-
        arg(3,S,RefineOp),
        RefineOp \= false , !,
	get_refine_gain(S,Last,Best,Path,MinLength,Pos,Neg,OVars,E,Best1,NewLast).
get_gain(S,Flag,Last,Best/Node,Path,C,TV,Len1,MinLen,L1,Pos,Neg,OVars,E,Best1,Last1):-
	arg(26,S,RCheck),
	arg(33,S,SplitVars),
	retractall('$aleph_search'(covers,_)),
	retractall('$aleph_search'(coversn,_)),
        get_pclause([L1],TV,Lit1,_,Len2,LastD),
	split_ok(SplitVars,C,Lit1), !,
        extend_clause(C,Lit1,Clause),
	(RCheck = true ->
		(redundant(Clause,Lit1) -> fail; true);
		true),
        CLen is Len1 + Len2,
        length_ok(S,MinLen,CLen,LastD,EMin,ELength),
	% arg(41,S,Prolog),
        split_clause(Clause,Head,Body),
        % (Prolog = yap ->
		% assertz('$aleph_search'(pclause,pclause(Head,Body)),DbRef);
		% assertz('$aleph_search'(pclause,pclause(Head,Body)))),
	assertz('$aleph_search'(pclause,pclause(Head,Body))),
        arg(6,S,Verbosity),
        (Verbosity >= 1 ->
		pp_dclause(Clause);
	true),
        get_gain1(S,Flag,Clause,CLen,EMin/ELength,Last,Best/Node,
                        Path,L1,Pos,Neg,OVars,E,Best1),
        % (Prolog = yap ->
		% erase(DbRef);
		% retractall('$aleph_search'(pclause,_))),
	retractall('$aleph_search'(pclause,_)),
        Last1 is Last + 1.
get_gain(_,_,Last,Best,_,_,_,_,_,_,_,_,_,_,Best,Last).

get_refine_gain(S,Last,Best/Node,Path,MinLength,Pos,Neg,OVars,E,Best1,NewLast):-
        arg(3,S,RefineOp),
	RefineOp = rls,
	refine_prelims(Best/Node,Last),
	rls_refine(clauses,Path,Path1),
	get_refine_gain1(S,Path1,MinLength,Pos,Neg,OVars,E,Best1,NewLast),
	!.
get_refine_gain(S,Last,Best/Node,Path,MinLength,Pos,Neg,OVars,E,Best1,NewLast):-
        arg(3,S,RefineOp),
	RefineOp \= rls,
	refine_prelims(Best/Node,Last),
	Path = CL-[Example,Type,_,Clause],
	arg(30,S,ConstructBottom),
        arg(43,S,LookAhead),
        get_user_refinement(RefineOp,LookAhead,Clause,R,_),
	match_bot(ConstructBottom,R,R1,LitNums),
	Path1 = CL-[Example,Type,LitNums,R1],
	get_refine_gain1(S,Path1,MinLength,Pos,Neg,OVars,E,Best1,NewLast),
	!.
get_refine_gain(_,_,_,_,_,_,_,_,_,Best,Last):-
	retract('$aleph_search'(best_refinement,best_refinement(Best))),
	retract('$aleph_search'(last_refinement,last_refinement(Last))).

get_theory_gain(S,Last,BestSoFar,T0,Pos,Neg,P,N,Best1,NewLast):-
	refine_prelims(BestSoFar,Last),
	arg(3,S,RefineOp),
	(RefineOp = rls -> rls_refine(theories,T0,T1); fail),
	arg(23,S,LazyPreds),
	(LazyPreds = [] -> Theory = T1;
		lazy_evaluate_theory(T1,LazyPreds,Pos,Neg,Theory)),
	retract('$aleph_search'(best_refinement,best_refinement(OldBest))),
	retract('$aleph_search'(last_refinement,last_refinement(OldLast))),
        arg(6,S,Verbosity),
        (Verbosity >= 1 ->
                p_message('new refinement'),
                pp_dclauses(Theory);
        true),
	record_pclauses(Theory),
	get_theory_gain1(S,Theory,OldLast,OldBest,Pos,Neg,P,N,Best1),
	retractall('$aleph_search'(pclause,_)),
        NewLast is OldLast + 1,
	asserta('$aleph_search'(last_refinement,last_refinement(NewLast))),
        asserta('$aleph_search'(best_refinement,best_refinement(Best1))),
	(discontinue_search(S,Best1,NewLast) ->
		retract('$aleph_search'(last_refinement,last_refinement(_))),
		retract('$aleph_search'(best_refinement,best_refinement(_)));
		fail),
	!.
get_theory_gain(_,_,_,_,_,_,_,_,Best,Last):-
	'$aleph_search'(best_refinement,best_refinement(Best)),
	'$aleph_search'(last_refinement,last_refinement(Last)).

refine_prelims(Best,Last):-
	retractall('$aleph_search'(last_refinement,_)),
	retractall('$aleph_search'(best_refinement,_)),
        asserta('$aleph_search'(best_refinement,best_refinement(Best))),
	asserta('$aleph_search'(last_refinement,last_refinement(Last))).

get_refine_gain1(S,Path,MinLength,Pos,Neg,OVars,E,Best1,NewLast):-
        arg(23,S,LazyPreds),
	Path = CL-[Example,Type,Ids,Refine],
	(LazyPreds = [] -> Ids1 = Ids, Clause = Refine;
		lazy_evaluate_refinement(Ids,Refine,LazyPreds,Pos,Neg,Ids1,Clause)),
	retractall('$aleph_search'(covers,_)),
	retractall('$aleph_search'(coversn,_)),
	Path1 = CL-[Example,Type,Ids1,Clause],
	split_clause(Clause,Head,Body),
	nlits(Body,CLength0),
	CLength is CLength0 + 1,
	length_ok(S,MinLength,CLength,0,EMin,ELength),
	arg(41,S,Prolog),
	split_clause(Clause,Head,Body),
	(Prolog = yap ->
		assertz('$aleph_search'(pclause,pclause(Head,Body)),DbRef);
		assertz('$aleph_search'(pclause,pclause(Head,Body)))),
	retract('$aleph_search'(best_refinement,best_refinement(OldBest))),
	retract('$aleph_search'(last_refinement,last_refinement(OldLast))),
        arg(6,S,Verbosity),
        (Verbosity >= 1 ->
		p_message('new refinement'),
		pp_dclause(Clause);
	true),
	once(get_gain1(S,upper,Clause,CLength,EMin/ELength,OldLast,OldBest,
		Path1,[],Pos,Neg,OVars,E,Best1)),
	(Prolog = yap ->
		erase(DbRef);
		retractall('$aleph_search'(pclause,_))),
	NewLast is OldLast + 1,
	asserta('$aleph_search'(last_refinement,last_refinement(NewLast))),
        asserta('$aleph_search'(best_refinement,best_refinement(Best1))),
	(discontinue_search(S,Best1,NewLast) ->
		retract('$aleph_search'(last_refinement,last_refinement(_))),
		retract('$aleph_search'(best_refinement,best_refinement(_)));
		fail),
	!.

get_theory_gain1(S,Theory,Last,Best,Pos,Neg,P,N,Best1):-
        (false -> p_message('constraint violated'),
                Contradiction = true;
                Contradiction = false),
	Contradiction = false,
        Node1 is Last + 1,
	arg(32,S,Lang),
	theory_lang_ok(Theory,Lang),
	arg(38,S,NewVars),
	theory_newvars_ok(Theory,NewVars),
	arg(14,S,Depth),
	arg(29,S,Time),
	arg(34,S,Proof),
        prove(Depth/Time/Proof,pos,(X:-X),Pos,PCvr,TP),
        prove(Depth/Time/Proof,neg,(X:-X),Neg,NCvr,FP),
	arg(4,S,_/Evalfn),
	Correct is TP + (N - FP),
	Incorrect is FP + (P - TP),
	length(Theory,L),
	Label = [Correct,Incorrect,L],
	complete_label(Evalfn,Theory,Label,Label1),
	get_search_keys(heuristic,Label1,SearchKeys),
	arg(6,S,Verbosity),
	(Verbosity >= 1 -> p_message(Correct/Incorrect); true),
	asserta('$aleph_search_node'(Node1,Theory,[],0,PCvr,NCvr,[],0)),
	update_open_list(SearchKeys,Node1,Label1),
	update_best_theory(S,Theory,PCvr,NCvr,Best,Label1/Node1,Best1), !.
get_theory_gain1(_,_,_,Best,_,_,_,_,Best).

get_gain1(S,_,C,CL,_,Last,Best,Path,_,Pos,Neg,_,E,Best):-
        abandon_branch(S,C), !,
        Node1 is Last + 1,
        arg(3,S,RefineOp),
        arg(7,S,ClauseLength),
	arg(35,S,VSearch),
        (ClauseLength = CL -> true;
                (RefineOp = false  ->
                        asserta('$aleph_search_node'(Node1,0,Path,0,Pos,Neg,[],E));
			true)),
	(VSearch = true ->
		asserta('$aleph_search'(bad,Node1)),
		asserta('$aleph_search_node'(Node1,C));
		true).
get_gain1(S,_,Clause,_,_,_,Best,_,_,_,_,_,_,Best):-
        arg(8,S,Caching),
        Caching = true,
        skolemize(Clause,SHead,SBody,0,_),
        '$aleph_search_prunecache'([SHead|SBody]), !,
	arg(6,S,Verbosity),
        (Verbosity >= 1 -> p_message('in prune cache'); true).
get_gain1(S,Flag,C,CL,EMin/EL,Last,Best/Node,Path,L1,Pos,Neg,OVars,E,Best1):-
	split_clause(C,Head,Body),
	arg(22,S,Search),
        ((Search \== ic, false) -> p_message('constraint violated'),
                Contradiction = true;
                Contradiction = false),
        Node1 is Last + 1,
        arg(8,S,Caching),
        (Caching = true -> arg(15,S,CCLim),
		get_cache_entry(CCLim,C,Entry);
		Entry = false),
	arg(35,S,VSearch),
	(VSearch = true ->
		asserta('$aleph_search_node'(Node1,C));
		true),
        arg(3,S,RefineOp),
	refinement_ok(RefineOp,Entry),
	arg(32,S,Lang),
	lang_ok((Head:-Body),Lang),
	arg(38,S,NewVars),
	newvars_ok((Head:-Body),NewVars),
	arg(34,S,Proof),
	arg(37,S,Optim),
	rewrite_clause(Proof,Optim,(Head:-Body),(Head1:-Body1)),
	(Search = ic ->
		PCvr = [],
		Label = [_,_,CL],
		ccheck(S,(Head1:-Body1),NCvr,Label);
        	prove_examples(S,Flag,Contradiction,Entry,Best,CL,EL,
				(Head1:-Body1),Pos,Neg,PCvr,NCvr,Label)
	),
        arg(4,S,SearchStrat/Evalfn),
	arg(40,S,MinPosFrac),
	((MinPosFrac > 0.0 ; Evalfn = wracc) ->
		reset_clause_prior(S,Head1);
		true
	),
	arg(46,S,SSample),
	(SSample = true ->
		arg(47,S,SampleSize),
		estimate_label(SampleSize,Label,Label0);
		Label0 = Label),
	complete_label(Evalfn,C,Label0,Label1),
	compression_ok(Evalfn,Label1),
        get_search_keys(SearchStrat,Label1,SearchKeys),
        arg(6,S,Verbosity),
	arg(10,S,LCost),
	arg(11,S,LContra),
        ((Verbosity >= 1, LContra = false, LCost = false) ->
		Label = [A,B|_],
		p_message(A/B);
	true),
        arg(7,S,ClauseLength),
	(RefineOp = false ->
		get_ovars1(false,L1,OVars1),
		aleph_append(OVars1,OVars,OVars2);
		true),
        ((ClauseLength=CL, RefineOp = false) -> true;
		(RefineOp = false ->
                	asserta('$aleph_search_node'(Node1,L1,Path,EMin/EL,PCvr,
					NCvr,OVars2,E));
                	asserta('$aleph_search_node'(Node1,0,Path,EMin/EL,PCvr,
					NCvr,[],E))),
                	update_open_list(SearchKeys,Node1,Label1)),
	(VSearch = true ->
		asserta('$aleph_search'(label,label(Node1,Label)));
		true),
        (((RefineOp \= false,Contradiction=false);
		(arg(28,S,HOVars),clause_ok(Contradiction,HOVars,OVars2))) ->
                update_best(S,C,PCvr,NCvr,Best/Node,Label1/Node1,Best1);
                Best1=Best/Node),
	!.
get_gain1(_,_,_,_,_,_,Best,_,_,_,_,_,_,Best).


abandon_branch(S,C):-
        arg(9,S,PruneDefined),
        PruneDefined = true,
        prune(C), !,
        arg(6,S,Verbosity),
        (Verbosity >= 1 -> p_message(pruned); true).

clause_ok(false,V1,V2):-
        aleph_subset1(V1,V2).

% check to see if a clause is acceptable
% 	unacceptable if it fails noise, minacc, or minpos settings
%	unacceptable if it fails search or language constraints
clause_ok(_,_):-
	false, !, fail.
clause_ok(_,Label):-
	extract_pos(Label,P),
	extract_neg(Label,N),
	Acc is P/(P+N),
	setting(noise,Noise),
	setting(minacc,MinAcc),
	setting(minpos,MinPos),
	(N > Noise; Acc < MinAcc; P < MinPos), !, fail.
clause_ok(Clause,_):-
	prune(Clause), !, fail.
clause_ok(Clause,_):-
	setting(language,Lang),
	\+ lang_ok(Clause,Lang), !, fail.
clause_ok(Clause,_):-
	setting(newvars,NewVars),
	\+ newvars_ok(Clause,NewVars), !, fail.
clause_ok(_,_).

% check to see if refinement has been produced before
refinement_ok(false,_):- !.
refinement_ok(rls,_):- !.
refinement_ok(_,false):- !.
refinement_ok(_,Entry):-
	(check_cache(Entry,pos,_); check_cache(Entry,neg,_)), !,
	p_message('redundant refinement'),
	fail.
refinement_ok(_,_).


% specialised redundancy check with equality theory
% used only to check if equalities introduced by splitting vars make
% literal to be added redundant
split_ok(false,_,_):- !.
split_ok(_,Clause,Lit):-
	functor(Lit,Name,_),
	Name \= '=', 
	copy_term(Clause/Lit,Clause1/Lit1),
	lit_redun(Lit1,Clause1), !,
	p_message('redundant literal'), nl,
	fail.
split_ok(_,_,_).

lit_redun(Lit,(Head:-Body)):-
	!,
	lit_redun(Lit,(Head,Body)).
lit_redun(Lit,(L1,_)):-
	Lit == L1, !.
lit_redun(Lit,(L1,L2)):-
	!,
	execute_equality(L1),
	lit_redun(Lit,L2).
lit_redun(Lit,L):-
	Lit == L.

execute_equality(Lit):-
	functor(Lit,'=',2), !,
	Lit.
execute_equality(_).
	
theory_lang_ok([],_).
theory_lang_ok([_-[_,_,_,Clause]|T],Lang):-
        lang_ok(Lang,Clause),
        theory_lang_ok(Lang,T). 

theory_newvars_ok([],_).
theory_newvars_ok([_-[_,_,_,Clause]|T],NewV):-
        newvars_ok(NewV,Clause),
        theory_newvars_ok(T,NewV). 

lang_ok((Head:-Body),N):-
	!,
	(lang_ok(N,Head,Body) -> true;
		p_message('outside language bound'),
		fail).

lang_ok(N,_,_):- N is inf, !.
lang_ok(N,Head,Body):-
	get_psyms((Head,Body),PSymList),
	lang_ok1(PSymList,N).

newvars_ok((Head:-Body),N):-
	!,
	(newvars_ok(N,Head,Body) -> true;
		p_message('outside newvars bound'),
		fail).

newvars_ok(N,_,_):- N is inf, !.
newvars_ok(N,Head,Body):-
	vars_in_term([Head],[],HVars),
	goals_to_list(Body,BodyL),
	vars_in_term(BodyL,[],BVars),
        aleph_ord_subtract(BVars,HVars,NewVars),
	length(NewVars,N1),
	N1 =< N.

get_psyms((L,B),[N/A|Syms]):-
	!,
	functor(L,N,A),
	get_psyms(B,Syms).
get_psyms(true,[]):- !.
get_psyms(L,[N/A]):-
	functor(L,N,A).

lang_ok1([],_).
lang_ok1([Pred|Preds],N):-
        length(Preds,N0),
        aleph_delete_all(Pred,Preds,Preds1),
        length(Preds1,N1),
        PredOccurs is N0 - N1 + 1,
	PredOccurs =< N,
	lang_ok1(Preds1,N).

rewrite_clause(sld,_,_,(X:-X)):- !.
rewrite_clause(restricted_sld,true,(Head:-Body),(Head1:-Body1)):- 
	!,
        optimise((Head:-Body),(Head1:-Body1)).
rewrite_clause(_,_,Clause,Clause).

record_pclauses([]).
record_pclauses([_-[_,_,_,Clause]|T]):-
        split_clause(Clause,Head,Body),
        assertz('$aleph_search'(pclause,pclause(Head,Body))),
        record_pclauses(T).

% get pos/neg distribution of clause head
reset_clause_prior(S,Head):-
	arg(3,S,Refine),
	Refine = false, !,
	('$aleph_search'(clauseprior,_) -> true;
		get_clause_prior(S,Head,Prior),
		assertz('$aleph_search'(clauseprior,Prior))
	).
reset_clause_prior(S,Head):-
	copy_term(Head,Head1),
	numbervars(Head1,0,_),
	('$aleph_local'(clauseprior,prior(Head1,Prior)) ->
		true;
		get_clause_prior(S,Head,Prior),
		assertz('$aleph_local'(clauseprior,prior(Head1,Prior)))
	),
	retractall('$aleph_search'(clauseprior,_)),
	assertz('$aleph_search'(clauseprior,Prior)).

get_clause_prior(S,Head,Total-[P-pos,N-neg]):-
	arg(5,S,Greedy),
	arg(14,S,Depth),
	arg(29,S,Time),
	arg(34,S,Proof),
	(Greedy = true ->
		'$aleph_global'(atoms_left,atoms_left(pos,Pos));
		'$aleph_global'(atoms,atoms(pos,Pos))
	),
	'$aleph_global'(atoms_left,atoms_left(neg,Neg)),
	prove(Depth/Time/Proof,pos,(Head:-true),Pos,_,P),
	prove(Depth/Time/Proof,neg,(Head:-true),Neg,_,N),
	Total is P + N.

get_user_refinement(auto,L,Clause,Template,0):-
        auto_refine(L,Clause,Template).
get_user_refinement(user,_,Clause,Template,0):-
        refine(Clause,Template).

match_bot(false,Clause,Clause,[]).
match_bot(reduction,Clause,Clause1,Lits):-
	match_lazy_bottom(Clause,Lits),
	get_pclause(Lits,[],Clause1,_,_,_).
match_bot(saturation,Clause,Clause1,Lits):-
	once(get_aleph_clause(Clause,AlephClause)),
	match_bot_lits(AlephClause,[],Lits),
	get_pclause(Lits,[],Clause1,_,_,_).

match_bot_lits((Lit,Lits),SoFar,[LitNum|LitNums]):-
	!,
	match_bot_lit(Lit,LitNum),
	\+(aleph_member(LitNum,SoFar)),
	match_bot_lits(Lits,[LitNum|SoFar],LitNums).
match_bot_lits(Lit,SoFar,[LitNum]):-
	match_bot_lit(Lit,LitNum),
	\+(aleph_member(LitNum,SoFar)).

match_bot_lit(Lit,LitNum):-
	'$aleph_sat'(botsize,Last),
	'$aleph_sat_litinfo'(LitNum,_,Lit,_,_,_),
	LitNum >= 0,
	LitNum =< Last.

match_lazy_bottom(Clause,Lits):-
	once(get_aleph_clause(Clause,AlephClause)),
	copy_term(Clause,CClause),
	split_clause(CClause,CHead,CBody),
	example_saturated(CHead),
	store(stage),
	set(stage,saturation),
	match_lazy_bottom1(CBody),
	reinstate(stage),
	match_bot_lits(AlephClause,[],Lits).

match_lazy_bottom1(Body):-
	Body,
	match_body_modes(Body),
	fail.
match_lazy_bottom1(_):-
	flatten_matched_atoms(body).

match_body_modes((CLit,CLits)):-
        !,
        match_mode(body,CLit),
        match_body_modes(CLits).
match_body_modes(CLit):-
        match_mode(body,CLit).

match_mode(_,true):- !.
match_mode(Loc,CLit):-
	functor(CLit,Name,Arity),
        functor(Mode,Name,Arity),
	(Loc=head ->
		'$aleph_global'(modeh,modeh(_,Mode));
		'$aleph_global'(modeb,modeb(_,Mode))),
        split_args(Mode,Mode,I,O,C),
        (Loc = head ->
		update_atoms(CLit,mode(Mode,O,I,C));
		update_atoms(CLit,mode(Mode,I,O,C))),
	fail.
match_mode(_,_).

flatten_matched_atoms(Loc):-
        setting(i,IVal),
        (retract('$aleph_sat'(botsize,BSize))-> true;  BSize = 0),
        (retract('$aleph_sat'(lastlit,Last))-> true ; Last = 0),
        (Loc = head ->
                flatten(0,IVal,BSize,BSize1);
                flatten(0,IVal,Last,BSize1)),
        asserta('$aleph_sat'(botsize,BSize1)),
	(Last < BSize1 -> 
        	asserta('$aleph_sat'(lastlit,BSize1));
        	asserta('$aleph_sat'(lastlit,Last))), !.
flatten_matched_atoms(_).

% integrate head literal into lits database
% used during lazy evaluation of bottom clause
integrate_head_lit(HeadOVars):-
        example_saturated(Example),
	split_args(Example,_,_,Output,_),
	integrate_args(unknown,Example,Output),
        match_mode(head,Example),
	flatten_matched_atoms(head),
        get_ivars1(false,1,HeadOVars), !.
integrate_head_lit([]).


get_aleph_clause((Lit:-true),PLit):-
	!,
	get_aleph_lit(Lit,PLit).
get_aleph_clause((Lit:-Lits),(PLit,PLits)):-
	!,
	get_aleph_lit(Lit,PLit),
	get_aleph_lits(Lits,PLits).
get_aleph_clause(Lit,PLit):-
	get_aleph_lit(Lit,PLit).

get_aleph_lits((Lit,Lits),(PLit,PLits)):-
	!,
	get_aleph_lit(Lit,PLit),
	get_aleph_lits(Lits,PLits).
get_aleph_lits(Lit,PLit):-
	get_aleph_lit(Lit,PLit).

get_aleph_lit(Lit,PLit):-
	functor(Lit,Name,Arity),
	functor(PLit,Name,Arity),
	get_aleph_lit(Lit,PLit,Arity).

get_aleph_lit(_,_,0):- !.
get_aleph_lit(Lit,PLit,Arg):-
	arg(Arg,Lit,Term),
	(var(Term) -> arg(Arg,PLit,Term);arg(Arg,PLit,aleph_const(Term))),
	NextArg is Arg - 1,
	get_aleph_lit(Lit,PLit,NextArg), !.
	
% Claudien-style consistency checking as described by De Raedt and Dehaspe, 1996
% currently does not retain actual substitutions that result in inconsistencies
% also, only checks for constraints of the form false:- ...
% this simplifies the check of Body,not(Head) to just Body
ccheck(S,(false:-Body),[],[0,N|_]):-
	(Body = true ->
		N is inf;
		arg(11,S,LContra),
		(LContra = false -> 
        		arg(14,S,Depth),
        		arg(29,S,Time),
			findall(X,(resource_bound_call(Time,Depth,Body),X=1),XL),
			length(XL,N);
			lazy_ccheck(S,Body,N)
		)
	).

lazy_ccheck(S,Body,N):-
        arg(14,S,Depth),
        arg(17,S,Noise),
        arg(29,S,Time),
	retractall('$aleph_local'(subst_count,_)),
	asserta('$aleph_local'(subst_count,0)),
	resource_bound_call(Time,Depth,Body),
	retract('$aleph_local'(subst_count,N0)),
	N is N0 + 1,
	N > Noise, !.
lazy_ccheck(_,_,N):-
	retract('$aleph_local'(subst_count,N)).

% posonly formula as described by Muggleton, ILP-96
prove_examples(S,Flag,Contradiction,Entry,Best,CL,L2,Clause,Pos,Rand,PCover,RCover,[P,B,CL,I,G]):-
	arg(4,S,_/Evalfn),
	Evalfn = posonly, !,
        arg(11,S,LazyOnContra),
        ((LazyOnContra = true, Contradiction = true) ->
                prove_lazy_cached(S,Entry,Pos,Rand,PCover,RCover),
                interval_count(PCover,PC),
                interval_count(RCover,RC);
                prove_pos(S,Flag,Entry,Best,[PC,L2],Clause,Pos,PCover,PC),
                prove_rand(S,Flag,Entry,Clause,Rand,RCover,RC)),
        find_posgain(PCover,P),
        arg(16,S,M), arg(20,S,N),
        GC is (RC+1.0)/(N+2.0), % Laplace correction for small numbers
        A is log(P),
        B is log(GC),
        G is GC*M/P,
        C is CL/P,
        % Sz is CL*M/P,
        % D is M*G,
        %  I is M - D - Sz,
        I is A - B - C.
prove_examples(S,_,_,Entry,_,CL,_,_,Pos,Neg,Pos,Neg,[PC,NC,CL]):-
        arg(10,S,LazyOnCost),
        LazyOnCost = true, !,
        prove_lazy_cached(S,Entry,Pos,Neg,Pos1,Neg1),
        interval_count(Pos1,PC),
        interval_count(Neg1,NC).
prove_examples(S,_,true,Entry,_,CL,_,_,Pos,Neg,Pos,Neg,[PC,NC,CL]):-
        arg(11,S,LazyOnContra),
        LazyOnContra = true, !,
        prove_lazy_cached(S,Entry,Pos,Neg,Pos1,Neg1),
        interval_count(Pos1,PC),
        interval_count(Neg1,NC).
prove_examples(S,Flag,_,Ent,Best,CL,L2,Clause,Pos,Neg,PCover,NCover,[PC,NC,CL]):-
	arg(3,S,RefineOp),
	(RefineOp = false; RefineOp = auto),
        arg(7,S,ClauseLength),
        ClauseLength = CL, !,
	interval_count(Pos,MaxPCount),
        prove_neg(S,Flag,Ent,Best,[MaxPCount,CL],Clause,Neg,NCover,NC),
        arg(17,S,Noise), arg(18,S,MinAcc),
        maxlength_neg_ok(Noise/MinAcc,Ent,MaxPCount,NC),
        prove_pos(S,Flag,Ent,Best,[PC,L2],Clause,Pos,PCover,PC),
        maxlength_neg_ok(Noise/MinAcc,Ent,PC,NC),
	!.
prove_examples(S,Flag,_,Ent,Best,CL,L2,Clause,Pos,Neg,PCover,NCover,[PC,NC,CL]):-
        prove_pos(S,Flag,Ent,Best,[PC,L2],Clause,Pos,PCover,PC),
        prove_neg(S,Flag,Ent,Best,[PC,CL],Clause,Neg,NCover,NC),
	!.

prove_lazy_cached(S,Entry,Pos,Neg,Pos1,Neg1):-
        arg(8,S,Caching),
	Caching = true, !,
	(check_cache(Entry,pos,Pos1)->
		true;
		add_cache(Entry,pos,Pos),
		Pos1 = Pos),
	(check_cache(Entry,neg,Neg1)->
		true;
		add_cache(Entry,neg,Neg),
		Neg1 = Neg).
prove_lazy_cached(_,_,Pos,Neg,Pos,Neg).

complete_label(posonly,_,L,L):- !.
complete_label(user,Clause,[P,N,L],[P,N,L,Val]):-
        cost(Clause,[P,N,L],Cost), !,
	Val is -Cost.
complete_label(entropy,_,[P,N,L],[P,N,L,Val]):-
	evalfn(entropy,[P,N,L],Entropy),
	Val is -Entropy, !.
complete_label(gini,_,[P,N,L],[P,N,L,Val]):-
	evalfn(gini,[P,N,L],Gini),
	Val is -Gini, !.
complete_label(EvalFn,_,[P,N,L],[P,N,L,Val]):-
	evalfn(EvalFn,[P,N,L],Val), !.
complete_label(_,_,_,_):-
	p_message1('error'), p_message('incorrect evaluation/cost function'),
	fail.

% estimate label based on subsampling
estimate_label(Sample,[P,N|Rest],[P1,N1|Rest]):-
	'$aleph_global'(atoms_left,atoms_left(pos,Pos)),
	'$aleph_global'(atoms_left,atoms_left(neg,Neg)),
	interval_count(Pos,PC), interval_count(Neg,NC),
	PFrac is P/Sample,
	NFrac is N/Sample,
	P1 is integer(PFrac*PC),
	N1 is integer(NFrac*NC).

% get primary and secondary search keys for search
% use [Primary|Secondary] notation as it is the most compact
get_search_keys(bf,[_,_,L,F|_],[L1|F]):-
	!,
	L1 is -1*L.
get_search_keys(df,[_,_,L,F|_],[L|F]):- !.
get_search_keys(_,[_,_,L,F|_],[F|L1]):-
	L1 is -1*L.

prove_pos(_,_,_,_,_,_,[],[],0):- !.
prove_pos(S,_,Entry,BestSoFar,PosSoFar,Clause,_,PCover,PCount):-
        '$aleph_search'(covers,covers(PCover,PCount)), !,
        pos_ok(S,Entry,BestSoFar,PosSoFar,Clause,PCover).
prove_pos(S,Flag,Entry,BestSoFar,PosSoFar,Clause,Pos,PCover,PCount):-
        prove_cache(Flag,S,pos,Entry,Clause,Pos,PCover,PCount),
        pos_ok(S,Entry,BestSoFar,PosSoFar,Clause,PCover), !.

prove_neg(S,_,Entry,_,_,_,[],[],0):-
	arg(8,S,Caching),
	(Caching = true -> add_cache(Entry,neg,[]); true), !.
prove_neg(S,Flag,Entry,_,_,Clause,Neg,NCover,NCount):-
	arg(3,S,RefineOp),
	RefineOp = rls,  !,
        prove_cache(Flag,S,neg,Entry,Clause,Neg,NCover,NCount).
prove_neg(_,_,_,_,_,_,_,NCover,NCount):-
        '$aleph_search'(coversn,coversn(NCover,NCount)), !.
prove_neg(S,Flag,Entry,BestSoFar,PosSoFar,Clause,Neg,NCover,NCount):-
        arg(12,S,LazyNegs),
        LazyNegs = true, !,
        lazy_prove_neg(S,Flag,Entry,BestSoFar,PosSoFar,Clause,Neg,NCover,NCount).
prove_neg(S,Flag,Entry,[P,0,L1|_],[P,L2],Clause,Neg,[],0):-
	arg(4,S,bf/coverage),
        L2 is L1 - 1,
	!,
        prove_cache(Flag,S,neg,Entry,Clause,Neg,0,[],0), !.
prove_neg(S,Flag,Entry,[P,N|_],[P,L1],Clause,Neg,NCover,NCount):-
	arg(4,S,bf/coverage),
        !,
        arg(7,S,ClauseLength),
        (ClauseLength = L1 ->
		arg(2,S,Explore),
		(Explore = true -> MaxNegs is N; MaxNegs is N - 1),
                MaxNegs >= 0,
                prove_cache(Flag,S,neg,Entry,Clause,Neg,MaxNegs,NCover,NCount),
		NCount =< MaxNegs;
                prove_cache(Flag,S,neg,Entry,Clause,Neg,NCover,NCount)),
        !.
prove_neg(S,Flag,Entry,_,[P1,L1],Clause,Neg,NCover,NCount):-
        arg(7,S,ClauseLength),
        ClauseLength = L1,  !,
        arg(17,S,Noise), arg(18,S,MinAcc),
        get_max_negs(Noise/MinAcc,P1,N1),
        prove_cache(Flag,S,neg,Entry,Clause,Neg,N1,NCover,NCount),
	NCount =< N1,
        !.
prove_neg(S,Flag,Entry,_,_,Clause,Neg,NCover,NCount):-
        prove_cache(Flag,S,neg,Entry,Clause,Neg,NCover,NCount),
        !.

prove_rand(S,Flag,Entry,Clause,Rand,RCover,RCount):-
        prove_cache(Flag,S,rand,Entry,Clause,Rand,RCover,RCount),
        !.

lazy_prove_neg(S,Flag,Entry,[P,N|_],[P,_],Clause,Neg,NCover,NCount):-
	arg(4,S,bf/coverage),
        !,
        MaxNegs is N + 1,
        prove_cache(Flag,S,neg,Entry,Clause,Neg,MaxNegs,NCover,NCount),
        !.
lazy_prove_neg(S,Flag,Entry,_,[P1,_],Clause,Neg,NCover,NCount):-
        arg(17,S,Noise), arg(18,S,MinAcc),
        get_max_negs(Noise/MinAcc,P1,N1),
        MaxNegs is N1 + 1,
        prove_cache(Flag,S,neg,Entry,Clause,Neg,MaxNegs,NCover,NCount),
        !.

% Bug reported by Daniel Fredouille
% For MiAcc =:= 0, Negs was being set to P1 + 1. Unclear why.
% This definition is as it was up to Aleph 2.
get_max_negs(Noise/MinAcc,P1,N):-
        number(P1), 
	(MinAcc =:= 0.0 -> N is Noise;
        	(N1 is integer((1-MinAcc)*P1/MinAcc),
		(Noise < N1 -> N is Noise; N is N1))
	), !.
get_max_negs(Noise/_,_,Noise).


% update_open_list(+SearchKeys,+NodeRef,+Label)
% insert SearchKeys into openlist
update_open_list([K1|K2],NodeRef,Label):-
	assertz('$aleph_search_gain'(K1,K2,NodeRef,Label)),
	retract('$aleph_search'(openlist,OpenList)),
	uniq_insert(descending,[K1|K2],OpenList,List1),
	asserta('$aleph_search'(openlist,List1)).

pos_ok(S,_,_,_,_,_):-
	arg(3,S,RefineOp),
	(RefineOp = rls; RefineOp = user),  !.
pos_ok(S,Entry,_,[P,_],_,_):-
        arg(13,S,MinPos),
        P < MinPos, !,
        arg(8,S,Caching),
        (Caching = true ->
                add_prune_cache(Entry);
                true),
        fail.
pos_ok(S,Entry,_,[P,_],_,_):-
	arg(40,S,MinPosFrac),
	MinPosFrac > 0.0,
	'$aleph_search'(clauseprior,_-[P1-pos,_]),
	P/P1 < MinPosFrac, !,
        arg(8,S,Caching),
        (Caching = true ->
                add_prune_cache(Entry);
                true),
	fail.
pos_ok(S,_,[_,_,_,C1|_],[P,L],_,_):-
        arg(4,S,_/Evalfn),
	arg(2,S,Explore),
	((Evalfn = user; Explore = true) -> true;
        	evalfn(Evalfn,[P,0,L],C2),
		best_value(Evalfn,S,[P,0,L,C2],Max),
        	Max > C1), !.


maxlength_neg_ok(Noise/MinAcc,Entry,P,N):-
	((N > Noise); (P/(P+N) < MinAcc)), !,
        add_prune_cache(Entry),
	fail.
maxlength_neg_ok(_,_,_,_).

compression_ok(compression,[P,_,L|_]):-
	!,
	P - L + 1 > 0.
compression_ok(_,_).

length_ok(S,MinLen,ClauseLen,LastD,ExpectedMin,ExpectedCLen):-
        arg(3,S,RefineOp),
        (RefineOp = false  -> L1 = LastD; L1 = 0),
        (L1 < MinLen->ExpectedMin = L1;ExpectedMin = MinLen),
        ExpectedCLen is ClauseLen + ExpectedMin,
        arg(7,S,CLength),
        ExpectedCLen =< CLength, !.

update_best(S,_,_,_,Best,[P,_,_,F|_]/_,Best):-
        arg(13,S,MinPos),
        arg(19,S,MinScore),
	(P < MinPos;  F is -inf; F < MinScore), !.
update_best(S,_,_,_,Best,[P|_]/_,Best):-
	arg(40,S,MinPosFrac),
	MinPosFrac > 0.0,
	'$aleph_search'(clauseprior,_-[P1-pos,_]),
	P/P1 < MinPosFrac, !.
update_best(S,_,_,_,Best,[P,N,_,_|_]/_,Best):-
        arg(4,S,_/Evalfn),
	Evalfn \= posonly,
	% Evalfn \= user,
        arg(17,S,Noise),
        arg(18,S,MinAcc),
	arg(22,S,Search),
	Total is P + N,
	((N > Noise);(Search \= ic, Total > 0, P/Total < MinAcc)),   !.
update_best(S,Clause,PCover,NCover,Label/_,Label1/Node1,Label1/Node1):-
        Label = [_,_,_,Gain|_],
        Label1 = [_,_,_,Gain1|_],
        % (Gain1 = inf; Gain = -inf; Gain1 > Gain), !,
	Gain1 > Gain, !,
	retractall('$aleph_search'(selected,_)),
        asserta('$aleph_search'(selected,selected(Label1,Clause,PCover,NCover))),
        arg(35,S,VSearch),
        (VSearch = true ->
		retractall('$aleph_search'(best,_)),
                asserta('$aleph_search'(best,Node1)),
                asserta('$aleph_search'(good,Node1));
                true),
	update_good(Label1,Clause),
        show_clause(newbest,Label1,Clause,Node1),
        record_clause(newbest,Label1,Clause,Node1),
        record_clause(good,Label1,Clause,Node1).
update_best(S,Clause,_,_,Label/Node,Label1/Node1,Label/Node):-
        arg(35,S,VSearch),
        (VSearch = true ->
                asserta('$aleph_search'(good,Node1));
                true),
	update_good(Label1,Clause),
        show_clause(good,Label1,Clause,Node1),
        record_clause(good,Label1,Clause,Node1).

update_good(Label,Clause):- 
	setting(good,true), !,
	Label = [_,_,L|_],
	setting(check_good,Flag),
	update_good(Flag,L,Label,Clause).
update_good(_,_).

update_good(_,_,_,_):-
	setting(goodfile,_), !.
update_good(true,L,Label,Clause):-
	'$aleph_good'(L,Label,Clause), !.
update_good(_,L,Label,Clause):-
	assertz('$aleph_good'(L,Label,Clause)),
	(retract('$aleph_search'(last_good,Good)) ->
		Good1 is Good + 1;
		Good1 is 1),
	assertz('$aleph_search'(last_good,Good1)).

update_best_theory(S,_,_,_,Best,[P,N,_,F|_]/_,Best):-
	arg(17,S,Noise),
	arg(18,S,MinAcc),
	arg(19,S,MinScore),
	(N > Noise; P/(P+N) < MinAcc; F < MinScore),  !.
update_best_theory(_,Theory,PCover,NCover,Label/_,Label1/Node1,Label1/Node1):-
	Label = [_,_,_,Gain|_],
	Label1 = [_,_,_,Gain1|_],
	Gain1 > Gain, !, 
	retractall('$aleph_search'(selected,_)),
        asserta('$aleph_search'(selected,selected(Label1,Theory,PCover,NCover))),
	show_theory(newbest,Label1,Theory,Node1),
	record_theory(newbest,Label1,Theory,Node1),
	record_theory(good,Label1,Theory,Node1).
update_best_theory(_,Theory,_,_,Best,Label1/_,Best):-
	show_theory(good,Label1,Theory,Node1),
	record_theory(good,Label1,Theory,Node1).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% P R U N I N G   C L A U S E S

get_node([[K1|K2]|_],[K1|K2],Node):-
        '$aleph_search_gain'(K1,K2,Node,_).
get_node([_|Gains],Gain,Node):-
	get_node(Gains,Gain,Node).

prune_open(S,_,_):-
	arg(25,S,OSize),
	Inf is inf,
	OSize =\= Inf,
        retractall('$aleph_local'(in_beam,_)),
        asserta('$aleph_local'(in_beam,0)),
        '$aleph_search'(openlist,Gains),
        get_node(Gains,[K1|K2],NodeNum),
        '$aleph_local'(in_beam,N),
        (N < OSize->
        	retract('$aleph_local'(in_beam,N)),
                N1 is N + 1,
                asserta('$aleph_local'(in_beam,N1));
		retract('$aleph_search_gain'(K1,K2,NodeNum,_)),
		arg(6,S,Verbose),
                (Verbose < 1 ->
			true;
			p1_message('non-admissible removal'),
			p_message(NodeNum))),
        fail.
prune_open(S,_,_):-
        arg(2,S,Explore),
        arg(3,S,RefineOp),
	(Explore = true; RefineOp = rls; RefineOp = user), !.
prune_open(_,_/N,_/N):- !.
prune_open(S,_,[_,_,_,Best|_]/_):-
        arg(4,S,_/Evalfn),
	built_in_prune(Evalfn),
        '$aleph_search_gain'(_,_,_,Label),
	best_value(Evalfn,S,Label,Best1),
	Best1 =< Best, 
        retract('$aleph_search_gain'(_,_,_,Label)),
	fail.
prune_open(_,_,_).

built_in_prune(coverage).
built_in_prune(compression).
built_in_prune(posonly).
built_in_prune(laplace).
built_in_prune(wracc).
built_in_prune(mestimate).
built_in_prune(auto_m).

% pruning for posonly, laplace and m-estimates devised in
%	discussion with James Cussens
% pruning for weighted relative accuracy devised in
%	discussion with Steve Moyle
% corrections to best_value/4 after discussion with
% Mark Reid and James Cussens
best_value(gini,_,_,0.0):- !.
best_value(entropy,_,_,0.0):- !.
best_value(posonly,S,[P,_,L|_],Best):-
	arg(20,S,RSize),
	Best is log(P) + log(RSize+2.0) - (L+1)/P, !.
best_value(wracc,_,[P|_],Best):-
	('$aleph_search'(clauseprior,Total-[P1-pos,_]) ->
		Best is P*(Total - P1)/(Total^2);
		Best is 0.25), !.
best_value(Evalfn,_,[P,_,L|Rest],Best):-
	L1 is L + 1,	% need at least 1 extra literal to achieve best value
	evalfn(Evalfn,[P,0,L1|Rest],Best).


get_nextbest(S,NodeRef):-
        arg(22,S,Search),
	select_nextbest(Search,NodeRef).

% Select the next best node
% Incorporates the changes made by Filip Zelezny to
% achieve the `randomised rapid restart' (or rrr) technique
% within randomised local search
select_nextbest(rls,NodeRef):-
	retractall('$aleph_search'(nextnode,_)),
        setting(rls_type,Type),
        (retract('$aleph_search'(rls_parentstats,stats(PStats,_,_))) -> true; true),
        (rls_nextbest(Type,PStats,NodeRef,Label) ->
                asserta('$aleph_search'(rls_parentstats,stats(Label,[],[]))),
                setting(rls_type,RlsType),
                (RlsType = rrr ->
                      true;
                      assertz('$aleph_search'(nextnode,NodeRef)));
                NodeRef = none), !.
select_nextbest(_,NodeRef):-
	retractall('$aleph_search'(nextnode,_)),
	get_nextbest(NodeRef), !.
select_nextbest(_,none).

get_nextbest(NodeRef):-
        '$aleph_search'(openlist,[H|_]),
	H = [K1|K2],
        retract('$aleph_search_gain'(K1,K2,NodeRef,_)),
        assertz('$aleph_search'(nextnode,NodeRef)).
get_nextbest(NodeRef):-
        retract('$aleph_search'(openlist,[_|T])),
        asserta('$aleph_search'(openlist,T)),
        get_nextbest(NodeRef), !.
get_nextbest(none).

rls_nextbest(rrr,_,NodeRef,_):-
        get_nextbest(NodeRef).
rls_nextbest(gsat,_,NodeRef,Label):-
        retract('$aleph_search'(openlist,[H|_])),
	H = [K1|K2],
	asserta('$aleph_search'(openlist,[])),
	findall(N-L,'$aleph_search_gain'(K1,K2,N,L),Choices),
	length(Choices,Last),
	get_random(Last,N),
	aleph_remove_nth(N,Choices,NodeRef-Label,_),
	retractall('$aleph_search_gain'(_,_,_,_)).
rls_nextbest(wsat,PStats,NodeRef,Label):-
	setting(walk,WProb),
	aleph_random(P),
	P >= WProb, !,
	rls_nextbest(gsat,PStats,NodeRef,Label).
rls_nextbest(wsat,PStats,NodeRef,Label):-
	p_message('random walk'),
        retract('$aleph_search'(openlist,_)),
	asserta('$aleph_search'(openlist,[])),
	findall(N-L,'$aleph_search_gain'(_,_,N,L),AllNodes),
	potentially_good(AllNodes,PStats,Choices),
        length(Choices,Last),
        get_random(Last,N),
        aleph_remove_nth(N,Choices,NodeRef-Label,_),
	retractall('$aleph_search_gain'(_,_,_,_)).
rls_nextbest(anneal,[P,N|_],NodeRef,Label):-
	setting(temperature,Temp),
        retract('$aleph_search'(openlist,_)),
	asserta('$aleph_search'(openlist,[])),
	findall(N-L,'$aleph_search_gain'(_,_,N,L),AllNodes),
	length(AllNodes,Last),
	get_random(Last,S),
	aleph_remove_nth(S,AllNodes,NodeRef-Label,_),
	Label = [P1,N1|_],
	Gain is (P1 - N1) - (P - N),
	((P = 1); (Gain >= 0);(aleph_random(R), R < exp(Gain/Temp))).

potentially_good([],_,[]).
potentially_good([H|T],Label,[H|T1]):-
        H = _-Label1,
        potentially_good(Label,Label1), !,
        potentially_good(T,Label,T1).
potentially_good([_|T],Label,T1):-
        potentially_good(T,Label,T1).

potentially_good([1|_],[P1|_]):-
        !,
        P1 > 1.
potentially_good([P,_,L|_],[P1,_,L1|_]):-
        L1 =< L, !,
        P1 > P.
potentially_good([_,N|_],[_,N1|_]):-
        N1 < N.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% P R O V E

% prove with caching
% if entry exists in cache, then return it
% otherwise find and cache cover 
% if ``exact'' flag is set then only check proof for examples
% in the part left over due to lazy theorem-proving
% ideas in caching developed in discussions with James Cussens

prove_cache(exact,S,Type,Entry,Clause,Intervals,IList,Count):-
	!,
	(Intervals = Exact/Left ->
        	arg(14,S,Depth),
        	arg(29,S,Time),
        	arg(34,S,Proof),
        	prove(Depth/Time/Proof,Type,Clause,Left,IList1,Count1),
		aleph_append(IList1,Exact,IList),
		interval_count(Exact,Count0),
		Count is Count0 + Count1;
		IList = Intervals,
		interval_count(IList,Count)),
        arg(8,S,Caching),
        (Caching = true -> add_cache(Entry,Type,IList); true).
prove_cache(upper,S,Type,Entry,Clause,Intervals,IList,Count):-
        arg(8,S,Caching),
        Caching = true, !,
        arg(14,S,Depth),
        arg(29,S,Time),
        arg(34,S,Proof),
        (check_cache(Entry,Type,Cached)->
                prove_cached(S,Type,Entry,Cached,Clause,Intervals,IList,Count);
                prove_intervals(Depth/Time/Proof,Type,Clause,Intervals,IList,Count),
                add_cache(Entry,Type,IList)).
prove_cache(upper,S,Type,_,Clause,Intervals,IList,Count):-
        arg(14,S,Depth),
        arg(29,S,Time),
        arg(34,S,Proof),
	(Intervals = Exact/Left ->
		aleph_append(Left,Exact,IList1),
        	prove(Depth/Time/Proof,Type,Clause,IList1,IList,Count);
        	prove(Depth/Time/Proof,Type,Clause,Intervals,IList,Count)).

prove_intervals(DepthTime,Type,Clause,I1/Left,IList,Count):- 
	!,
	aleph_append(Left,I1,Intervals),
	prove(DepthTime,Type,Clause,Intervals,IList,Count).
prove_intervals(DepthTime,Type,Clause,Intervals,IList,Count):- 
	prove(DepthTime,Type,Clause,Intervals,IList,Count).

prove_cached(S,Type,Entry,I1/Left,Clause,Intervals,IList,Count):-
        !,
        arg(14,S,Depth),
        arg(29,S,Time),
        arg(34,S,Proof),
        prove(Depth/Time/Proof,Type,Clause,Left,I2,_),
        aleph_append(I2,I1,I),
        (Type = pos ->
                arg(5,S,Greedy),
                (Greedy = true ->
                        intervals_intersection(I,Intervals,IList);
                        IList = I);
                IList = I),
        interval_count(IList,Count),
        update_cache(Entry,Type,IList).
prove_cached(S,Type,Entry,I1,_,Intervals,IList,Count):-
	(Type = pos -> arg(5,S,Greedy),
		(Greedy = true ->
			intervals_intersection(I1,Intervals,IList);
			IList = I1);
		IList = I1),
	interval_count(IList,Count),
	update_cache(Entry,Type,IList).

% prove at most Max atoms
prove_cache(exact,S,Type,Entry,Clause,Intervals,Max,IList,Count):-
	!,
	(Intervals = Exact/Left ->
		interval_count(Exact,Count0),
		Max1 is Max - Count0,
        	arg(12,S,LNegs),
        	arg(14,S,Depth),
        	arg(29,S,Time),
        	arg(34,S,Proof),
        	prove(LNegs/false,Depth/Time/Proof,Type,Clause,Left,Max1,IList1,Count1),
		aleph_append(IList1,Exact,Exact1),
		find_lazy_left(S,Type,Exact1,Left1),
		IList = Exact1/Left1,
		Count is Count0 + Count1;
		IList = Intervals,
		interval_count(Intervals,Count)),
        arg(8,S,Caching),
        (Caching = true -> add_cache(Entry,Type,IList); true).
prove_cache(upper,S,Type,Entry,Clause,Intervals,Max,IList,Count):-
        arg(8,S,Caching),
        Caching = true, !,
        (check_cache(Entry,Type,Cached)->
                prove_cached(S,Type,Entry,Cached,Clause,Intervals,Max,IList,Count);
                (prove_intervals(S,Type,Clause,Intervals,Max,IList1,Count)->
                        find_lazy_left(S,Type,IList1,Left1),
                        add_cache(Entry,Type,IList1/Left1),
			IList = IList1/Left1,
                        retractall('$aleph_local'(example_cache,_));
                        collect_example_cache(IList),
                        add_cache(Entry,Type,IList),
                        fail)).
prove_cache(upper,S,Type,_,Clause,Intervals,Max,IList/Left1,Count):-
        arg(8,S,Caching),
        arg(12,S,LNegs),
        arg(14,S,Depth),
        arg(29,S,Time),
        arg(34,S,Proof),
	(Intervals = Exact/Left ->
		aleph_append(Left,Exact,IList1),
        	prove(LNegs/Caching,Depth/Time/Proof,Type,Clause,IList1,Max,IList,Count);
        	prove(LNegs/Caching,Depth/Time/Proof,Type,Clause,Intervals,Max,IList,Count)),
	find_lazy_left(S,Type,IList,Left1).

prove_intervals(S,Type,Clause,I1/Left,Max,IList,Count):-
        !,
        arg(8,S,Caching),
        arg(12,S,LNegs),
        arg(14,S,Depth),
        arg(29,S,Time),
        arg(34,S,Proof),
        aleph_append(Left,I1,Intervals),
        prove(LNegs/Caching,Depth/Time/Proof,Type,Clause,Intervals,Max,IList,Count).
prove_intervals(S,Type,Clause,Intervals,Max,IList,Count):-
        arg(8,S,Caching),
        arg(12,S,LNegs),
        arg(14,S,Depth),
        arg(29,S,Time),
        arg(34,S,Proof),
        prove(LNegs/Caching,Depth/Time/Proof,Type,Clause,Intervals,Max,IList,Count).


prove_cached(S,Type,Entry, I1/Left,Clause,_,Max,IList/Left1,Count):-
        !,
        arg(8,S,Caching),
        arg(12,S,LNegs),
        arg(14,S,Depth),
        arg(29,S,Time),
        arg(34,S,Proof),
        interval_count(I1,C1),
        Max1 is Max - C1,
        Max1 >= 0,
        (prove(LNegs/Caching,Depth/Time/Proof,Type,Clause,Left,Max1,I2,C2)->
                aleph_append(I2,I1,IList),
                Count is C2 + C1,
                find_lazy_left(S,Type,IList,Left1),
                update_cache(Entry,Type,IList/Left1),
                retractall('$aleph_local'(example_cache,_));
                collect_example_cache(I2/Left1),
                aleph_append(I2,I1,IList),
                update_cache(Entry,Type,IList/Left1),
                fail).
prove_cached(_,neg,_, I1/L1,_,_,_,I1/L1,C1):-
	!,
	interval_count(I1,C1).
prove_cached(S,_,_,I1,_,_,Max,I1,C1):-
	interval_count(I1,C1),
	arg(12,S,LNegs),
	(LNegs = true ->true; C1 =< Max).

collect_example_cache(Intervals/Left):-
	retract('$aleph_local'(example_cache,[Last|Rest])),
	aleph_reverse([Last|Rest],IList),
	list_to_intervals1(IList,Intervals),
	Next is Last + 1,
	'$aleph_global'(size,size(neg,LastN)),
	(Next > LastN -> Left = []; Left = [Next-LastN]).

find_lazy_left(S,_,_,[]):-
        arg(12,S,LazyNegs),
        LazyNegs = false, !.
find_lazy_left(_,_,[],[]).
find_lazy_left(S,Type,[_-F],Left):-
        !,
        F1 is F + 1,
	(Type = pos -> arg(16,S,Last);
		(Type = neg -> arg(24,S,Last);
			(Type = rand -> arg(20,S,Last); Last = F))),
        (F1 > Last -> Left = []; Left = [F1-Last]).
find_lazy_left(S,Type,[_|T1],Left):-
        find_lazy_left(S,Type,T1,Left).


% prove atoms specified by Type and index set using Clause.
% dependent on data structure used for index set:
% currently index set is a list of intervals
% return atoms proved and their count
% if tail-recursive version is needed see below

prove(_,_,_,[],[],0).
prove(Flags,Type,Clause,[Interval|Intervals],IList,Count):-
	index_prove(Flags,Type,Clause,Interval,I1,C1),
	prove(Flags,Type,Clause,Intervals,I2,C2),
	aleph_append(I2,I1,IList),
	Count is C1 + C2.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% T A I L - R E C U R S I V E  P R O V E/6
 
% use this rather than the prove/6 above for tail recursion
% written by James Cussens
 

% prove(DepthTime,Type,Clause,Intervals,IList,Count):-
       % prove2(Intervals,DepthTime,Type,Clause,0,IList,Count).
 
% code for tail recursive cover testing
% starts here

% when we know that Sofar is a variable.
prove2([],_,_,_,Count,[],Count).
prove2([Current-Finish|Intervals],Depth/Time/Proof,Type,(Head:-Body),InCount,Sofar,OutCount) :-
	example(Current,Type,Example),
	\+ prove1(Proof,Depth/Time,Example,(Head:-Body)), %uncovered
        !,
        (Current>=Finish ->
            prove2(Intervals,Depth/Time/Proof,Type,(Head:-Body),InCount,Sofar,OutCount);
            Next is Current+1,!,
            prove2([Next-Finish|Intervals],Depth/Time/Proof,Type,(Head:-Body),InCount,Sofar,OutCount)
        ).
prove2([Current-Finish|Intervals],ProofFlags,Type,Clause,InCount,Sofar,OutCount) :-
        (Current>=Finish ->
            Sofar=[Current-Current|Rest],
            MidCount is InCount+1,!,
            prove2(Intervals,ProofFlags,Type,Clause,MidCount,Rest,OutCount);
            Next is Current+1,
            Sofar=[Current-_Last|_Rest],!,
            prove3([Next-Finish|Intervals],ProofFlags,Type,Clause,InCount,Sofar,OutCount)
        ).
 
%when Sofar is not a variable
prove3([Current-Finish|Intervals],Depth/Time/Proof,Type,(Head:-Body),InCount,Sofar,OutCount) :-
	example(Current,Type,Example),
	\+ prove1(Proof,Depth/Time,Example,(Head:-Body)), %uncovered
        !,
        Last is Current-1, %found some previously
        Sofar=[Start-Last|Rest], %complete found interval
        MidCount is InCount+Current-Start,
        (Current>=Finish ->
            prove2(Intervals,Depth/Time/Proof,Type,(Head:-Body),MidCount,Rest,OutCount);
            Next is Current+1,!,
            prove2([Next-Finish|Intervals],Depth/Time/Proof,Type,(Head:-Body),MidCount,Rest,OutCount)
        ).
prove3([Current-Finish|Intervals],ProofFlags,Type,Clause,InCount,Sofar,OutCount) :-
        (Current>=Finish ->
            Sofar=[Start-Finish|Rest],
            MidCount is InCount+Finish-Start+1,!,
            prove2(Intervals,ProofFlags,Type,Clause,MidCount,Rest,OutCount);
            Next is Current+1,!,
            prove3([Next-Finish|Intervals],ProofFlags,Type,Clause,InCount,Sofar,OutCount)
        ).
 
 
% code for tail recursive cover testing
% ends here

index_prove(_,_,_,Start-Finish,[],0):-
	Start > Finish, !.
index_prove(ProofFlags,Type,Clause,Start-Finish,IList,Count):-
	index_prove1(ProofFlags,Type,Clause,Start,Finish,Last),
	Last0 is Last - 1 ,
	Last1 is Last + 1,
	(Last0 >= Start->
		index_prove(ProofFlags,Type,Clause,Last1-Finish,Rest,Count1),
		IList = [Start-Last0|Rest],
		Count is Last - Start + Count1;
		index_prove(ProofFlags,Type,Clause,Last1-Finish,IList,Count)).

prove1(G):-
	depth_bound_call(G), !.

prove1(user,_,Example,Clause):-
	prove(Clause,Example), !.
prove1(restricted_sld,Depth/Time,Example,(Head:-Body)):-
	\+((\+(((Example = Head),resource_bound_call(Time,Depth,Body))))), !.
prove1(sld,Depth/Time,Example,_):-
	\+(\+(resource_bound_call(Time,Depth,Example))), !.
	
index_prove1(_,_,_,Num,Last,Num):-
	Num > Last, !.
index_prove1(Depth/Time/Proof,Type,Clause,Num,Finish,Last):-
	example(Num,Type,Example),
	prove1(Proof,Depth/Time,Example,Clause), !,
	Num1 is Num + 1,
	index_prove1(Depth/Time/Proof,Type,Clause,Num1,Finish,Last).
index_prove1(_,_,_,Last,_,Last).


% proves at most Max atoms using Clause.

prove(_,_,_,_,[],_,[],0).
prove(Flags,ProofFlags,Type,Clause,[Interval|Intervals],Max,IList,Count):-
        index_prove(Flags,ProofFlags,Type,Clause,Interval,Max,I1,C1), !,
        Max1 is Max - C1,
        prove(Flags,ProofFlags,Type,Clause,Intervals,Max1,I2,C2),
        aleph_append(I2,I1,IList),
        Count is C1 + C2.


index_prove(_,_,_,_,Start-Finish,_,[],0):-
        Start > Finish, !.
index_prove(Flags,ProofFlags,Type,Clause,Start-Finish,Max,IList,Count):-
        index_prove1(Flags,ProofFlags,Type,Clause,Start,Finish,0,Max,Last),
        Last0 is Last - 1 ,
        Last1 is Last + 1,
        (Last0 >= Start->
                Max1 is Max - Last + Start,
		((Max1 = 0, Flags = true/_) ->
                        Rest = [], Count1 = 0;
                	index_prove(Flags,ProofFlags,Type,Clause,Last1-Finish,
					Max1,Rest,Count1)),
                IList = [Start-Last0|Rest],
                Count is Last - Start + Count1;
                index_prove(Flags,ProofFlags,Type,Clause,Last1-Finish,Max,IList,Count)).

index_prove1(false/_,_,_,_,_,_,Proved,Allowed,_):-
        Proved > Allowed, !, fail.
index_prove1(_,_,_,_,Num,Last,_,_,Num):-
        Num > Last, !.
index_prove1(true/_,_,_,_,Num,_,Allowed,Allowed,Num):- !.
index_prove1(LNegs/Caching,Depth/Time/Proof,Type,Clause,Num,Finish,Proved,Allowed,Last):-
	example(Num,Type,Example),
	prove1(Proof,Depth/Time,Example,Clause), !,
        Num1 is Num + 1,
        Proved1 is Proved + 1,
        (Caching = true ->
                (retract('$aleph_local'(example_cache,L)) ->
                        asserta('$aleph_local'(example_cache,[Num|L]));
                        asserta('$aleph_local'(example_cache,[Num])));
                true),
        index_prove1(LNegs/Caching,Depth/Time/Proof,Type,Clause,Num1,Finish,Proved1,Allowed,Last).
index_prove1(_,_,_,_,Last,_,_,_,Last).

% resource_bound_call(Time,Depth,Goals)
%	attempt to prove Goals using depth bounded theorem-prover
%	in at most Time secs
resource_bound_call(T,Depth,Goals):-
	Inf is inf,
	T =:= Inf,
	!,
	depth_bound_call(Goals,Depth).
resource_bound_call(T,Depth,Goals):-
        catch(time_bound_call(T,prooflimit,depth_bound_call(Goals,Depth)),
		prooflimit,fail).

time_bound_call(T,Exception,Goal):-
	alarm(T,throw(Exception),X),
        (Goal -> remove_alarm(X); remove_alarm(X), fail).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% C A C H I N G

clear_cache:-
	retractall('$aleph_search_cache'(_)),
	retractall('$aleph_search_prunecache'(_)).

check_cache(Entry,Type,I):-
	Entry \= false,
        '$aleph_search_cache'(Entry), !,
        functor(Entry,_,Arity),
        (Type = pos -> Arg is Arity - 1; Arg is Arity),
        arg(Arg,Entry,I),
	nonvar(I).

add_cache(false,_,_):- !.
add_cache(Entry,Type,I):-
        (retract('$aleph_search_cache'(Entry))-> true ; true),
        functor(Entry,_,Arity),
        (Type = pos -> Arg is Arity - 1; Arg is Arity),
        (arg(Arg,Entry,I)-> asserta('$aleph_search_cache'(Entry));
                        true), !.

update_cache(Entry,Type,I):-
        Entry \= false,
        functor(Entry,Name,Arity),
        (Type = pos -> Arg is Arity - 1; Arg is Arity),
        arg(Arg,Entry,OldI),
        OldI = _/_,
        retract('$aleph_search_cache'(Entry)),
        functor(NewEntry,Name,Arity),
        Arg0 is Arg - 1,
        copy_args(Entry,NewEntry,1,Arg0),
        arg(Arg,NewEntry,I),
        Arg1 is Arg + 1,
        copy_args(Entry,NewEntry,Arg1,Arity),
        asserta('$aleph_search_cache'(NewEntry)), !.
update_cache(_,_,_).

	
add_prune_cache(false):- !.
add_prune_cache(Entry):-
	('$aleph_global'(caching,set(caching,true))->
		functor(Entry,_,Arity),
		A1 is Arity - 2,
		arg(A1,Entry,Clause),
		asserta('$aleph_search_prunecache'(Clause));
		true).

get_cache_entry(Max,Clause,Entry):-
        skolemize(Clause,Head,Body,0,_),
	length(Body,L1),
	Max >= L1 + 1,
        aleph_hash_term([Head|Body],Entry), !.
get_cache_entry(_,_,false).

% upto 3-argument indexing using predicate names in a clause
aleph_hash_term([L0,L1,L2,L3,L4|T],Entry):-
        !,
        functor(L1,P1,_), functor(L2,P2,_),
        functor(L3,P3,_), functor(L4,P4,_),
        functor(Entry,P4,6),
        arg(1,Entry,P2), arg(2,Entry,P3),
        arg(3,Entry,P1), arg(4,Entry,[L0,L1,L2,L3,L4|T]).
aleph_hash_term([L0,L1,L2,L3],Entry):-
        !,
        functor(L1,P1,_), functor(L2,P2,_),
        functor(L3,P3,_),
        functor(Entry,P3,5),
        arg(1,Entry,P2), arg(2,Entry,P1),
        arg(3,Entry,[L0,L1,L2,L3]).
aleph_hash_term([L0,L1,L2],Entry):-
        !,
        functor(L1,P1,_), functor(L2,P2,_),
        functor(Entry,P2,4),
        arg(1,Entry,P1), arg(2,Entry,[L0,L1,L2]).
aleph_hash_term([L0,L1],Entry):-
        !,
        functor(L1,P1,_),
        functor(Entry,P1,3),
        arg(1,Entry,[L0,L1]).
aleph_hash_term([L0],Entry):-
        functor(L0,P0,_),
        functor(Entry,P0,3),
        arg(1,Entry,[L0]).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% T R E E S

construct_tree(Type):-
	setting(searchtime,Time),
	Inf is inf,
        Time =\= Inf,
        SearchTime is integer(Time),
        SearchTime > 0, !,
	catch(time_bound_call(SearchTime,searchlimit,find_tree(Type)),
		searchlimit,p_message('Time limit reached')).
construct_tree(Type):-
	find_tree(Type).

% find_tree(Type) where Type is one of
%      classification, regression, class_probability
find_tree(Type):-
	retractall('$aleph_search'(tree,_)),
	retractall('$aleph_search'(tree_besterror,_)),
	retractall('$aleph_search'(tree_gain,_)),
	retractall('$aleph_search'(tree_lastleaf,_)),
	retractall('$aleph_search'(tree_leaf,_)),
	retractall('$aleph_search'(tree_newleaf,_)),
	retractall('$aleph_search'(tree_startdistribution,_)),
	get_start_distribution(Type,Distribution),
	asserta('$aleph_search'(tree_startdistribution,d(Type,Distribution))),
	'$aleph_global'(atoms_left,atoms_left(pos,Pos)),
	setting(dependent,Argno),
	p_message('constructing tree'),
	stopwatch(StartClock),
	get_search_settings(S),
	auto_refine(false,Head),
	gen_leaf(Leaf),
	eval_treenode(S,Type,(Head:-true),[Argno],Pos,Examples,N,Cost),
	asserta('$aleph_search'(tree_leaf,l(Leaf,Leaf,[Head,Cost,N],Examples))),
	find_tree1([Leaf],S,Type,[Argno]),
	prune_rules(S,Type,[Argno]),
	stopwatch(StopClock),
	add_tree(S,Type,[Argno]),
	Time is StopClock - StartClock,
	p1_message('construction time'), p_message(Time).

get_start_distribution(regression,0-[0,0]):- !.
get_start_distribution(model,0-[0,0]):-
	setting(evalfn,mse), !.
get_start_distribution(model,0-Distribution):- 
	setting(evalfn,accuracy), !,
	(setting(classes,Classes) -> true;
		!,
		p_message('missing setting for classes'),
		fail),
	initialise_distribution(Classes,Distribution), !.
get_start_distribution(Tree,0-Distribution):-
	(Tree = classification; Tree = class_probability),
	(setting(classes,Classes) -> true;
		!,
		p_message('missing setting for classes'),
		fail),
	initialise_distribution(Classes,Distribution), !.
get_start_distribution(_,_):-
	p_message('incorrect/missing setting for tree_type or evalfn'),
	fail.

initialise_distribution([],[]).
initialise_distribution([Class|Classes],[0-Class|T]):-
	initialise_distribution(Classes,T).

laplace_correct([],[]).
laplace_correct([N-Class|Classes],[N1-Class|T]):-
	N1 is N + 1,
	laplace_correct(Classes,T).

find_tree1([],_,_,_).
find_tree1([Leaf|Leaves],S,Type,Predict):-
	can_split(S,Type,Predict,Leaf,Left,Right), !,
	split_leaf(Leaf,Left,Right,NewLeaves),
	aleph_append(NewLeaves,Leaves,LeavesLeft),
	find_tree1(LeavesLeft,S,Type,Predict).
find_tree1([_|LeavesLeft],S,Type,Predict):-
	find_tree1(LeavesLeft,S,Type,Predict).

prune_rules(S,Tree,Predict):-
	setting(prune_tree,true), 
	prune_rules1(Tree,S,Predict), !.
prune_rules(_,_,_).

% pessimistic pruning by employing corrections to observed errors
prune_rules1(class_probability,_,_):-
	p_message('no pruning for class probability trees'), !.
prune_rules1(model,_,_):-
	p_message('no pruning for model trees'), !.
prune_rules1(Tree,S,Predict):-
	p_message('pruning clauses'),
	'$aleph_search'(tree_leaf,l(Leaf,Parent,Clause,Examples)),
	prune_rule(Tree,S,Predict,Clause,Examples,NewClause,NewExamples),
	retract('$aleph_search'(tree_leaf,l(Leaf,Parent,Clause,Examples))),
	asserta('$aleph_search'(tree_newleaf,l(Leaf,Parent,NewClause,NewExamples))),
	fail.
prune_rules1(_,_,_):-
	retract('$aleph_search'(tree_newleaf,l(Leaf,Parent,NewClause,NewExamples))),
	asserta('$aleph_search'(tree_leaf,l(Leaf,Parent,NewClause,NewExamples))),
	fail.
prune_rules1(_,_,_).

prune_rule(Tree,S,PredictArg,[Clause,_,N],Examples,[PrunedClause,E1,NCov],NewEx):-
	node_stats(Tree,Examples,PredictArg,Total-Distribution),
	leaf_prediction(Tree,Total-Distribution,_,Incorrect),
	estimate_error(Tree,Incorrect,Total,Upper),
	split_clause(Clause,Head,Body),
	goals_to_list(Body,BodyL),
	arg(14,S,Depth),
	arg(29,S,Time),
	arg(34,S,Proof),
	greedy_prune_rule(Tree,Depth/Time/Proof,PredictArg,[Head|BodyL],Upper,C1L,E1),
	list_to_clause(C1L,PrunedClause),
	% p1_message('pruned clause'), p_message(Clause),
	% p_message('to'),
	% p_message(PrunedClause),
	(E1 < Upper ->
		'$aleph_global'(atoms_left,atoms_left(pos,Pos)),
        	prove(Depth/Time/Proof,pos,PrunedClause,Pos,NewEx,NCov);
		NewEx = Examples,
		NCov = N).


% estimate error using binomial distribution as done in C4.5
estimate_error(classification,Incorrect,Total,Error):-
	setting(confidence,Conf),
	estimate_error(1.0/0.0,0.0/1.0,Conf,Total,Incorrect,Error).

% estimate upper bound on sample std deviation by
% assuming the n values in a leaf are normally distributed.
% In this case, a (1-alpha)x100 confidence interval for the
% variance is (n-1)s^2/X^2(alpha/2) =< var =< (n-1)s^2/X^2(1-alpha/2)
estimate_error(regression,Sd,1,Sd):- !.
estimate_error(regression,Sd,N,Upper):-
	(setting(confidence,Conf) -> true; Conf = 0.95),
	Alpha is 1.0 - Conf,
	DF is N - 1,
	Prob is 1 - Alpha/2,
	chi_square(DF,Prob,ChiSq),
	Upper is Sd*sqrt((N-1)/ChiSq).

bound_error(classification,Error,Total,Lower,Upper):-
	(setting(confidence,Alpha) -> true; Alpha = 0.95),
	approx_z(Alpha,Z),
	Lower is Error - Z*sqrt(Error*(1-Error)/Total),
	Upper is Error + Z*sqrt(Error*(1-Error)/Total).

approx_z(P,2.58):- P >= 0.99, !.
approx_z(P,Z):- P >= 0.98, !, Z is 2.33 + (P-0.98)*(2.58-2.33)/(0.99-0.98).
approx_z(P,Z):- P >= 0.95, !, Z is 1.96 + (P-0.95)*(2.33-1.96)/(0.98-0.95).
approx_z(P,Z):- P >= 0.90, !, Z is 1.64 + (P-0.90)*(1.96-1.64)/(0.95-0.90).
approx_z(P,Z):- P >= 0.80, !, Z is 1.28 + (P-0.80)*(1.64-1.28)/(0.90-0.80).
approx_z(P,Z):- P >= 0.68, !, Z is 1.00 + (P-0.68)*(1.28-1.00)/(0.80-0.68).
approx_z(P,Z):- P >= 0.50, !, Z is 0.67 + (P-0.50)*(1.00-0.67)/(0.68-0.50).
approx_z(_,0.67).

greedy_prune_rule(Tree,Flags,PredictArg,Clause,Err0,NewClause,BestErr):-
	greedy_prune_rule1(Tree,Flags,PredictArg,Clause,Err0,Clause1,Err1),
	Clause \= Clause1, !,
	greedy_prune_rule(Tree,Flags,PredictArg,Clause1,Err1,NewClause,BestErr).
greedy_prune_rule(_,_,_,C,E,C,E).


greedy_prune_rule1(Tree,Flags,PredictArg,[Head|Body],Err0,_,_):-
	retractall('$aleph_search'(tree_besterror,_)),
	asserta('$aleph_search'(tree_besterror,besterror([Head|Body],Err0))),
	'$aleph_global'(atoms_left,atoms_left(pos,Pos)),
	aleph_delete(_,Body,Left),
	strip_negs(Left,Body1),
	aleph_mode_linked([Head|Body1]),
	list_to_clause([Head|Left],Clause),
        prove(Flags,pos,Clause,Pos,Ex1,_),
	node_stats(Tree,Ex1,PredictArg,Total-Distribution),
	leaf_prediction(Tree,Total-Distribution,_,Incorrect),
	estimate_error(Tree,Incorrect,Total,Upper),
	'$aleph_search'(tree_besterror,besterror(_,BestError)),
	Upper =< BestError, 
	retract('$aleph_search'(tree_besterror,besterror(_,BestError))),
	asserta('$aleph_search'(tree_besterror,besterror([Head|Left],Upper))),
	fail.
greedy_prune_rule1(_,_,_,_,_,Clause1,Err1):-
	retract('$aleph_search'(tree_besterror,besterror(Clause1,Err1))).

strip_negs([],[]).
strip_negs([not(L)|T],[L|T1]):-
	!,
	strip_negs(T,T1).
strip_negs([L|T],[L|T1]):-
	strip_negs(T,T1).
	
add_tree(_,Tree,Predict):-
	retract('$aleph_search'(tree_leaf,l(_,_,Leaf,Examples))),
	Leaf = [Clause,Cost,P],
	add_prediction(Tree,Clause,Predict,Examples,Clause1),
	p_message('best clause'),
	pp_dclause(Clause1),
        nlits(Clause,L),
	Gain is -Cost,
        asserta('$aleph_global'(hypothesis,hypothesis([P,0,L,Gain],Clause1,Examples,[]))),
	addhyp,
	fail.
add_tree(_,_,_).

add_prediction(Tree,Clause,PredictArg,Examples,Clause1):-
	split_clause(Clause,Head,_),
	(Tree = model ->
		setting(evalfn,Evalfn),
		add_model(Evalfn,Clause,PredictArg,Examples,Clause1,_,_);
		node_stats(Tree,Examples,PredictArg,Distribution),
		leaf_prediction(Tree,Distribution,Prediction,Error),
		tparg(PredictArg,Head,Var),
		add_prediction(Tree,Clause,Var,Prediction,Error,Clause1)).

add_prediction(classification,Clause,Var,Prediction,_,Clause1):-
	extend_clause(Clause,(Var = Prediction),Clause1).
add_prediction(class_probability,Clause,Var,Prediction,_,Clause1):-
	extend_clause(Clause,(random(Var,Prediction)),Clause1).
add_prediction(regression,Clause,Var,Mean,Sd,Clause1):-
	extend_clause(Clause,(random(Var,normal(Mean,Sd))),Clause1).

add_model(Evalfn,Clause,PredictArg,Examples,_,_,_):-
	retractall('$aleph_local'(tree_model,_,_,_)),
	Best is inf,
	split_clause(Clause,Head,_),
	tparg(PredictArg,Head,Var),
	asserta('$aleph_local'(tree_model,false,0,Best)),
	'$aleph_global'(model,model(Name/Arity)),
	functor(Model,Name,Arity),
	auto_extend(Clause,Model,C),
	leaf_predicts(Arity,Model,Var),
	lazy_evaluate_refinement([],C,[Name/Arity],Examples,[],[],C1),
	find_model_error(Evalfn,Examples,C1,PredictArg,Total,Error),
	'$aleph_local'(tree_model,_,_,BestSoFar),
	(Error < BestSoFar ->
		retract('$aleph_local'(tree_model,_,_,_)),
		asserta('$aleph_local'(tree_model,C1,Total,Error));
		true),
	fail.	
add_model(_,_,_,_,Clause,Total,Error):-
	retract('$aleph_local'(tree_model,Clause,Total,Error)).


find_model_error(Evalfn,Examples,(Head:-Body),[PredictArg],T,E):-
	functor(Head,_,Arity),
	findall(Actual-Pred,
			(aleph_member(Interval,Examples),
			aleph_member3(N,Interval),
			example(N,pos,Example),
			copy_iargs(Arity,Example,Head,PredictArg),
			once(Body),
			arg(PredictArg,Head,Pred), 
			arg(PredictArg,Example,Actual)
			), 
		L),
	sum_model_errors(L,Evalfn,0,0.0,T,E), !.

sum_model_errors([],_,N,E,N,E).
sum_model_errors([Act-Pred|T],Evalfn,NSoFar,ESoFar,N,E):-
	get_model_error(Evalfn,Act,Pred,E1),
	E1SoFar is ESoFar + E1,
	N1SoFar is NSoFar + 1,
	sum_model_errors(T,Evalfn,N1SoFar,E1SoFar,N,E).

get_model_error(mse,Act,Pred,E):-
	E is (Act-Pred)^2.
get_model_error(accuracy,Act,Pred,E):-
	(Act = Pred -> E is 0.0; E is 1.0).

leaf_predicts(0,_,_):- !, fail.
leaf_predicts(Arg,Model,Var):-
	arg(Arg,Model,Var1),
	var(Var1),
	Var1 == Var, !.
leaf_predicts(Arg,Model,Var):-
	Arg1 is Arg - 1,
	leaf_predicts(Arg1,Model,Var).
	
leaf_prediction(classification,Total-Distribution,Class,Incorrect):-
	find_maj_class(Distribution,N-Class),
	Incorrect is Total - N.
leaf_prediction(class_probability,T1-D1,NDistr,0):-
	length(D1,NClasses),
	laplace_correct(D1,LaplaceD1),
	LaplaceTotal is T1 + NClasses,
	normalise_distribution(LaplaceD1,LaplaceTotal,NDistr).
leaf_prediction(regression,_-[Mean,Sd],Mean,Sd).

find_maj_class([X],X):- !.
find_maj_class([N-Class|Rest],MajClass):-
	find_maj_class(Rest,N1-C1),
	(N > N1 -> MajClass = N-Class; MajClass = N1-C1).

can_split(S,Type,Predict,Leaf,Left,Right):-
	arg(21,S,MinGain),
	'$aleph_search'(tree_leaf,l(Leaf,_,[Clause,Cost,N],Examples)),
	Cost >= MinGain, 
	get_best_subtree(S,Type,Predict,[Clause,Cost,N],Examples,Gain,Left,Right),
	Gain >= MinGain,
	p_message('found clauses'),
	Left = [ClF,CostF|_], Right = [ClS,CostS|_],
	arg(4,S,_/Evalfn),
	pp_dclause(ClS),
	print_eval(Evalfn,CostS),
	pp_dclause(ClF),
	print_eval(Evalfn,CostF),
	p1_message('expected cost reduction'), p_message(Gain).

get_best_subtree(S,Type,Predict,[Clause,Cost,N],Examples,Gain,Left,Right):-
	arg(42,S,Interactive),
	arg(43,S,LookAhead),
	retractall('$aleph_search'(tree_gain,_)),
	MInf is -inf,
	(Interactive = false ->
		asserta('$aleph_search'(tree_gain,tree_gain(MInf,[],[])));
		true),
	split_clause(Clause,Head,Body),
	arg(4,S,_/Evalfn),
	arg(13,S,MinPos),
	auto_refine(LookAhead,Clause,ClS),
	tree_refine_ok(Type,ClS),
	eval_treenode(S,Type,ClS,Predict,Examples,ExS,NS,CostS),
	NS >= MinPos,
	rm_intervals(ExS,Examples,ExF),
	split_clause(ClS,Head,Body1),
	get_goaldiffs(Body,Body1,Diff),
	extend_clause(Clause,not(Diff),ClF),
	eval_treenode(S,Type,ClF,Predict,ExF,NF,CostF),
	NF >= MinPos,
	AvLeafCost is (NS*CostS + NF*CostF)/N,
	CostReduction is Cost - AvLeafCost,
	(Interactive = false ->
		pp_dclause(ClS), print_eval(Evalfn,CostS),
		pp_dclause(ClF), print_eval(Evalfn,CostF),
		p1_message('expected cost reduction'), p_message(CostReduction),
		'$aleph_search'(tree_gain,tree_gain(BestSoFar,_,_)),
		CostReduction > BestSoFar,
		retract('$aleph_search'(tree_gain,tree_gain(BestSoFar,_,_))),
		asserta('$aleph_search'(tree_gain,tree_gain(CostReduction,
							[ClF,CostF,NF,ExF],
							[ClS,CostS,NS,ExS])));
		asserta('$aleph_search'(tree_gain,tree_gain(CostReduction,
							[ClF,CostF,NF,ExF],
							[ClS,CostS,NS,ExS])))),

	AvLeafCost =< 0.0, 
	!,
	get_best_subtree(Interactive,Clause,Gain,Left,Right).
get_best_subtree(S,_,_,[Clause|_],_,Gain,Left,Right):-
	arg(42,S,Interactive),
	get_best_subtree(Interactive,Clause,Gain,Left,Right).

get_best_subtree(false,_,Gain,Left,Right):-
	retract('$aleph_search'(tree_gain,tree_gain(Gain,Left,Right))), !.
get_best_subtree(true,Clause,Gain,Left,Right):-
	nl, write('Extending path: '), nl,
	write('---------------'), nl,
	pp_dclause(Clause),
	findall(MCR-[Left,Right],
		('$aleph_search'(tree_gain,tree_gain(CostReduction,Left,Right)), 
		  MCR is -1*CostReduction), 
		SplitsList),
	keysort(SplitsList,Sorted),
	get_best_split(Clause,Sorted,Gain,Left,Right),
	retractall('$aleph_search'(tree_gain,_)).

get_best_split(Clause,Splits,Gain,Left,Right):-
	show_split_list(Clause,Splits),
	ask_best_split(Splits,Gain,Left,Right).

show_split_list(Clause,Splits):-
	tab(4), write('Split Information'), nl,
	tab(4), write('-----------------'), nl, nl,
	tab(4), write('No.'), 
	tab(4), write('Split'), 
	nl,
	tab(4), write('---'), 
	tab(4), write('-----'), 
	nl,
	show_split_list(Splits,1,Clause).

show_split_list([],_,_).
show_split_list([MCR-[[_,_,NF,_],[CLS,_,NS,_]]|Rest],SplitNum,Clause):-
	copy_term(Clause,ClauseCopy),
	split_clause(ClauseCopy,Head,Body),
	copy_term(CLS,CLSCopy),
	numbervars(CLSCopy,0,_),
	split_clause(CLSCopy,Head,Body1),
	get_goaldiffs(Body,Body1,Diff),
	Gain is -1*MCR,
	tab(4), write(SplitNum),
	tab(4), write(Diff), nl,
	tab(12), write('Succeeded (Right Branch): '), write(NS), nl,
	tab(12), write('Failed    (Left Branch) : '), write(NF), nl,
	tab(12), write('Cost Reduction          : '), write(Gain), nl, nl,
	NextSplit is SplitNum + 1,
	show_split_list(Rest,NextSplit,Clause).

ask_best_split(Splits,Gain,Left,Right):-
	repeat,
	tab(4), write('-> '),
	write('Select Split Number (or "none.")'), nl,
	read(Answer),
	(Answer = none ->
		Gain is -inf,
		Left = [],
		Right = [];
		SplitNum is integer(Answer),
		aleph_remove_nth(SplitNum,Splits,MCR-[Left,Right],_),
		Gain is -1*MCR
	),
	!.

tree_refine_ok(model,Clause):-
        '$aleph_global'(model,model(Name/Arity)),
	functor(Model,Name,Arity),
	in(Clause,Model), !,
	fail.
tree_refine_ok(_,_).


eval_treenode(S,Tree,Clause,PredictArg,PCov,N,Cost):-
	arg(4,S,_/Evalfn),
	treenode_cost(Tree,Evalfn,Clause,PCov,PredictArg,N,Cost).

eval_treenode(S,Tree,Clause,PredictArg,Pos,PCov,N,Cost):-
	arg(4,S,_/Evalfn),
	arg(13,S,MinPos),
	arg(14,S,Depth),
	arg(29,S,Time),
	arg(34,S,Proof),
        prove(Depth/Time/Proof,pos,Clause,Pos,PCov,PCount),
	PCount >= MinPos,
	treenode_cost(Tree,Evalfn,Clause,PCov,PredictArg,N,Cost).

treenode_cost(model,Evalfn,Clause,Covered,PredictArg,Total,Cost):-
	!,
	add_model(Evalfn,Clause,PredictArg,Covered,_,Total,Cost).
treenode_cost(Tree,Evalfn,_,Covered,PredictArg,Total,Cost):-
	node_stats(Tree,Covered,PredictArg,Total-Distribution),
	Total > 0,
	impurity(Tree,Evalfn,Total-Distribution,Cost).

node_stats(Tree,Covered,PredictArg,D):-
        '$aleph_search'(tree_startdistribution,d(Tree,D0)),
        (Tree = regression ->
                cont_distribution(Covered,PredictArg,D0,D);
                discr_distribution(Covered,PredictArg,D0,D)).

discr_distribution([],_,D,D).
discr_distribution([S-F|Intervals],PredictArg,T0-D0,D):-
	discr_distribution(S,F,PredictArg,T0-D0,T1-D1),
	discr_distribution(Intervals,PredictArg,T1-D1,D).

discr_distribution(N,F,_,D,D):- N > F, !.
discr_distribution(N,F,PredictArg,T0-D0,D):-
	example(N,pos,Example),
	tparg(PredictArg,Example,Actual),
	N1 is N + 1,
	T1 is T0 + 1,
	(aleph_delete(C0-Actual,D0,D1) ->
		C1 is C0 + 1,
		discr_distribution(N1,F,PredictArg,T1-[C1-Actual|D1],D);
		discr_distribution(N1,F,PredictArg,T1-[1-Actual|D0],D)).

cont_distribution([],_,T-[S,SS],T-[Mean,Sd]):-
	(T = 0 -> Mean = 0, Sd = 0;
		Mean is S/T,
		Sd is sqrt(SS/T - Mean*Mean)).
cont_distribution([S-F|Intervals],PredictArg,T0-D0,D):-
        cont_distribution(S,F,PredictArg,T0-D0,T1-D1),
        cont_distribution(Intervals,PredictArg,T1-D1,D).

cont_distribution(N,F,_,D,D):- N > F, !.
cont_distribution(N,F,PredictArg,T0-[S0,SS0],D):-
        example(N,pos,Example),
        tparg(PredictArg,Example,Actual),
	N1 is N + 1,
        T1 is T0 + 1,
	S1 is S0 + Actual,
	SS1 is SS0 + Actual*Actual,
        cont_distribution(N1,F,PredictArg,T1-[S1,SS1],D).

impurity(regression,sd,_-[_,Sd],Sd):- !.
impurity(classification,entropy,Total-Distribution,Cost):-
	sum_entropy(Distribution,Total,S),
	Cost is -S/(Total*log(2)), !.
impurity(classification,gini,Total-Distribution,Cost):-
	sum_gini(Distribution,Total,Cost), !.
impurity(class_probability,entropy,Total-Distribution,Cost):-
	sum_entropy(Distribution,Total,S),
	Cost is -S/(Total*log(2)), !.
impurity(class_probability,gini,Total-Distribution,Cost):-
	sum_gini(Distribution,Total,Cost), !.
impurity(_,_,_,_):-
	err_message('inappropriate settings for tree_type and/or evalfn'),
	fail.


sum_gini([],_,0).
sum_gini([N-_|Rest],Total,Sum):-
	N > 0, !,
	sum_gini(Rest,Total,C0),
	P is N/Total,
	Sum is P*(1-P) + C0.
sum_gini([_|Rest],Total,Sum):-
	sum_gini(Rest,Total,Sum).

sum_entropy([],_,0).
sum_entropy([N-_|Rest],Total,Sum):-
	N > 0, !,
	sum_entropy(Rest,Total,C0),
	Sum is N*log(N/Total) + C0.
sum_entropy([_|Rest],Total,Sum):-
	sum_entropy(Rest,Total,Sum).

% only binary splits
% left = condition at node fails
% right = condition at node succeeds
split_leaf(Leaf,LeftTree,RightTree,[Left,Right]):-
	retract('$aleph_search'(tree_leaf,l(Leaf,Parent,
						[Clause,Cost,N],Examples))),
	gen_leaf(Left),
	gen_leaf(Right),
	LeftTree = [ClF,CostF,NF,ExF],
	RightTree = [ClS,CostS,NS,ExS],
	asserta('$aleph_search'(tree,t(Leaf,Parent,[Clause,Cost,N],
					Examples,Left,Right))),
	asserta('$aleph_search'(tree_leaf,l(Left,Leaf,[ClF,CostF,NF],ExF))),
	asserta('$aleph_search'(tree_leaf,l(Right,Leaf,[ClS,CostS,NS],ExS))).

gen_leaf(Leaf1):-
	retract('$aleph_search'(tree_lastleaf,Leaf0)), !,
	Leaf1 is Leaf0 + 1,
	asserta('$aleph_search'(tree_lastleaf,Leaf1)).
gen_leaf(0):-
        asserta('$aleph_search'(tree_lastleaf,0)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% G C W S

% examine list of clauses to be specialised
% generate an exception theory for each clause that covers negative examples
gcws:-
	setting(evalfn,EvalFn),
	repeat,
	retract('$aleph_search'(sphyp,hypothesis([P,N,L|T],Clause,PCover,NCover))),
	(PCover = _/_ -> label_create(pos,Clause,Label1),
		extract_pos(Label1,PCover1),
		interval_count(PCover1,P1);
		PCover1 = PCover,
		P1 = P),
	(NCover = _/_ -> label_create(neg,Clause,Label2),
		extract_neg(Label2,NCover1),
		interval_count(NCover1,N1);
		NCover1 = NCover,
		N1 = N),
	(N1 = 0 -> NewClause = Clause, NewLabel = [P1,N1,L|T];
		MinAcc is P1/(2*P1 - 1),
		set(minacc,MinAcc),
		set(noise,N1),
		gcws(Clause,PCover1,NCover1,NewClause),
		L1 is L + 1,
		complete_label(EvalFn,NewClause,[P,0,L1],NewLabel)),
	assertz('$aleph_search'(gcwshyp,hypothesis(NewLabel,NewClause,PCover1,[]))),
	\+('$aleph_search'(sphyp,hypothesis(_,_,_,_))), !.


% gcws(+Clause,+PCvr,+NCvr,-Clause1)
%	specialise Clause that covers pos examples PCvr and neg examples NCvr
%	result is is Clause extended with a single negated literal
% clauses in exception theory are added to list for specialisation
gcws(Clause,PCover,NCover,Clause1):-
	gen_absym(AbName),
	split_clause(Clause,Head,Body),
	functor(Head,_,Arity),
	add_determinations(AbName/Arity,true),
	add_modes(AbName/Arity),
	gen_ab_examples(AbName/Arity,PCover,NCover),
	cwinduce,
	Head =.. [_|Args],
	AbLit =.. [AbName|Args],
	(Body = true -> Body1 = not(AbLit) ; app_lit(not(AbLit),Body,Body1)),
	Clause1 = (Head:-Body1).

% greedy set-cover based construction of abnormality theory 
% starts with the first exceptional example
% each clause obtained is added to list of clauses to be specialised 
cwinduce:-
	store(greedy),
        set(greedy,true),
        '$aleph_global'(atoms_left,atoms_left(pos,PosSet)),
        PosSet \= [],
        repeat,
	'$aleph_global'(atoms_left,atoms_left(pos,[Num-X|Y])),
	sat(Num),
	reduce,
	retract('$aleph_global'(hypothesis,hypothesis(Label,H,PCover,NCover))),
	asserta('$aleph_search'(sphyp,hypothesis(Label,H,PCover,NCover))),
        rm_seeds1(PCover,[Num-X|Y],NewPosLeft),
	retract('$aleph_global'(atoms_left,atoms_left(pos,[Num-X|Y]))),
        asserta('$aleph_global'(atoms_left,atoms_left(pos,NewPosLeft))),
	NewPosLeft = [],
        retract('$aleph_global'(atoms_left,atoms_left(pos,NewPosLeft))),
	reinstate(greedy), !.
cwinduce.


% gen_ab_examples(+Ab,+PCover,+NCover)
% obtain examples for abnormality predicate Ab by
%	pos examples are copies of neg examples in NCover
%	neg examples are copies of pos examples in PCover
% writes new examples to temporary ".f" and ".n" files
% to ensure example/3 remains a static predicate
% alters search parameters accordingly
gen_ab_examples(Ab/_,PCover,NCover):-
	PosFile = '.alephtmp.f',
	NegFile = '.alephtmp.n',
	create_examples(PosFile,Ab,neg,NCover,pos,PCover1),
	create_examples(NegFile,Ab,pos,PCover,neg,NCover1),
	aleph_consult(PosFile),
	aleph_consult(NegFile),
        retractall('$aleph_global'(atoms_left,_)),
        retractall('$aleph_global'(size,_)),
        asserta('$aleph_global'(atoms_left,atoms_left(pos,PCover1))),
        asserta('$aleph_global'(atoms_left,atoms_left(neg,NCover1))),
        interval_count(PCover1,PSize),
        interval_count(NCover1,NSize),
        asserta('$aleph_global'(size,size(pos,PSize))),
        asserta('$aleph_global'(size,size(neg,NSize))),
	delete_file(PosFile),
	delete_file(NegFile).

% create_examples(+File,+OldType,+OldE,+NewType,-NewE)
% copy OldE examples of OldType to give NewE examples of NewType 
% copy stored in File
create_examples(File,Ab,OldT,OldE,NewT,[Next-Last]):-
	'$aleph_global'(last_example,last_example(NewT,OldLast)),
	aleph_open(File,write,Stream),
	set_output(Stream),
	create_copy(OldE,OldT,NewT,Ab,OldLast,Last),
	close(Stream),
	set_output(user_output),
	Last > OldLast, !,
	retract('$aleph_global'(last_example,last_example(NewT,OldLast))),
	Next is OldLast + 1,
	asserta('$aleph_global'(last_example,last_example(NewT,Last))).
create_examples(_,_,_,_,_,[]).

create_copy([],_,_,_,L,L).
create_copy([X-Y|T],OldT,NewT,Ab,Num,Last):-
	create_copy(X,Y,OldT,NewT,Ab,Num,Num1),
	create_copy(T,OldT,NewT,Ab,Num1,Last).

create_copy(X,Y,_,_,_,L,L):- X > Y, !.
create_copy(X,Y,OldT,NewT,Ab,Num,Last):-
	example(X,OldT,Example),
	Example =.. [_|Args],
	NewExample =.. [Ab|Args],
	Num1 is Num + 1,
	aleph_writeq(example(Num1,NewT,NewExample)), write('.'), nl,
	X1 is X + 1,
	create_copy(X1,Y,OldT,NewT,Ab,Num1,Last).

% gen_absym(-Name)
% generate new abnormality predicate symbol
gen_absym(Name):-
	(retract('$aleph_global'(last_ab,last_ab(N))) ->
		N1 is N + 1;
		N1 is 0),
	asserta('$aleph_global'(last_ab,last_ab(N1))),
	concat([ab,N1],Name).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% C L A U S E   O P T I M I S A T I O N S


optimise(Clause,Clause1):-
	remove_redundant(Clause,Clause0),
	reorder_clause(Clause0,Clause1).

remove_redundant((Head:-Body),(Head1:-Body1)):-
	goals_to_list((Head,Body),ClauseL),
	remove_subsumed(ClauseL,[Head1|Body1L]),
	(Body1L = [] -> Body1 = true; list_to_goals(Body1L,Body1)).

reorder_clause((Head:-Body), Clause) :-
        % term_variables(Head,LHead),
        vars_in_term([Head],[],LHead),
        number_goals_and_get_vars(Body,LHead,1,_,[],Conj),
        calculate_independent_sets(Conj,[],BSets),
        compile_clause(BSets,Head,Clause).

number_goals_and_get_vars((G,Body),LHead,I0,IF,L0,[g(I0,LVF,NG)|LGs]) :- !,
        I is I0+1,
        get_goal_vars(G,LHead,LVF,NG),
        number_goals_and_get_vars(Body,LHead,I,IF,L0,LGs).
number_goals_and_get_vars(G,LHead,I,I,L0,[g(I,LVF,NG)|L0]) :-
        get_goal_vars(G,LHead,LVF,NG).

get_goal_vars(G,LHead,LVF,G) :-
        % term_variables(G,LV0),
        vars_in_term([G],[],LVI),
        aleph_ord_subtract(LVI,LHead,LVF).

calculate_independent_sets([],BSets,BSets).
calculate_independent_sets([G|Ls],BSets0,BSetsF) :-
        add_goal_to_set(G,BSets0,BSetsI),
        calculate_independent_sets(Ls,BSetsI,BSetsF).

add_goal_to_set(g(I,LV,G),Sets0,SetsF) :-
        add_to_sets(Sets0,LV,[g(I,LV,G)],SetsF).

add_to_sets([],LV,Gs,[[LV|Gs]]).
add_to_sets([[LV|Gs]|Sets0],LVC,GsC,[[LV|Gs]|SetsF]) :-
        aleph_ord_disjoint(LV,LVC), !,
        add_to_sets(Sets0,LVC,GsC,SetsF).
add_to_sets([[LV|Gs]|Sets0],LVC,GsC,SetsF) :-
        aleph_ord_union(LV,LVC,LVN),
        join_goals(Gs,GsC,GsN),
        add_to_sets(Sets0,LVN,GsN,SetsF).

join_goals([],L,L):- !.
join_goals(L,[],L):- !.
join_goals([g(I1,VL1,G1)|T],[g(I2,VL2,G2)|T2],Z) :-
        I1 < I2, !,
        Z = [g(I1,VL1,G1)|TN],
        join_goals(T,[g(I2,VL2,G2)|T2],TN).
join_goals([H|T],[g(I2,VL2,G2)|T2],Z) :-
        Z = [g(I2,VL2,G2)|TN],
        join_goals(T,[H|T2],TN).

compile_clause(Goals,Head,(Head:-Body)):-
        compile_clause2(Goals,Body).

compile_clause2([[_|B]], B1):-
	!,
        glist_to_goals(B,B1).
compile_clause2([[_|B]|Bs],(B1,!,NB)):-
        glist_to_goals(B,B1),
        compile_clause2(Bs,NB).

glist_to_goals([g(_,_,Goal)],Goal):- !.
glist_to_goals([g(_,_,Goal)|Goals],(Goal,Goals1)):-
        glist_to_goals(Goals,Goals1).

% remove literals subsumed in the body of a clause
remove_subsumed([Head|Lits],Lits1):-
	delete(Lit,Lits,Left),
	\+(\+(redundant(Lit,[Head|Lits],[Head|Left]))), !,
	remove_subsumed([Head|Left],Lits1).
remove_subsumed(L,L).

% determine if Lit is subsumed by a body literal
redundant(Lit,Lits,[Head|Body]):-
	copy_term([Head|Body],Rest1),
	member(Lit1,Body),
	Lit = Lit1,
	aleph_subsumes(Lits,Rest1).

aleph_subsumes(Lits,Lits1):-
	\+(\+((numbervars(Lits,0,_),numbervars(Lits1,0,_),aleph_subset1(Lits,Lits1)))).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% S A T  /  R E D U C E

sat(Num):-
	integer(Num),
	example(Num,pos,_),
	sat(pos,Num), !.
sat(Example):-
	record_example(check,uspec,Example,Num),
	sat(uspec,Num), !.

sat(Type,Num):-
        setting(construct_bottom,false), !,
        sat_prelims,
	example(Num,Type,Example),
	broadcast(start(sat(Num))),
	p1_message('sat'), p_message(Num), p_message(Example),
	record_sat_example(Num),
	asserta('$aleph_sat'(example,example(Num,Type))),
	asserta('$aleph_sat'(hovars,[])),
	broadcast(end(sat(Num, 0, 0.0))).
sat(Type,Num):-
	setting(construct_bottom,reduction), !,
	sat_prelims,
	example(Num,Type,Example),
	broadcast(start(sat(Num))),
	p1_message('sat'), p_message(Num), p_message(Example),
	record_sat_example(Num),
	asserta('$aleph_sat'(example,example(Num,Type))),
	integrate_head_lit(HeadOVars),
	asserta('$aleph_sat'(hovars,HeadOVars)),
	broadcast(end(sat(Num, 0, 0.0))).
sat(Type,Num):-
	set(stage,saturation),
	sat_prelims,
	example(Num,Type,Example),
	broadcast(start(sat(Num))),
	p1_message('sat'), p_message(Num), p_message(Example),
	record_sat_example(Num),
	asserta('$aleph_sat'(example,example(Num,Type))),
	split_args(Example,Mode,Input,Output,Constants),
	integrate_args(unknown,Example,Output),
	stopwatch(StartClock),
	assertz('$aleph_sat_atom'(Example,mode(Mode,Output,Input,Constants))),
	'$aleph_global'(i,set(i,Ival)),
	flatten(0,Ival,0,Last1),
	'$aleph_sat_litinfo'(1,_,Atom,_,_,_),
	get_vars(Atom,Output,HeadOVars),
	asserta('$aleph_sat'(hovars,HeadOVars)),
	get_vars(Atom,Input,HeadIVars),
	asserta('$aleph_sat'(hivars,HeadIVars)),
	functor(Example,Name,Arity), 
	get_determs(Name/Arity,L),
	('$aleph_global'(determination,determination(Name/Arity,'='/2))->
		asserta('$aleph_sat'(eq,true));
		asserta('$aleph_sat'(eq,false))),
	get_atoms(L,1,Ival,Last1,Last),
	stopwatch(StopClock),
	Time is StopClock - StartClock,
	asserta('$aleph_sat'(lastlit,Last)),
	asserta('$aleph_sat'(botsize,Last)),
	update_generators,
	rm_moderepeats(Last,Repeats),
	rm_commutative(Last,Commutative),
	rm_symmetric(Last,Symmetric),
	rm_redundant(Last,Redundant),
	rm_uselesslits(Last,NotConnected),
	rm_nreduce(Last,NegReduced),
	TotalLiterals is
		Last-Repeats-NotConnected-Commutative-Symmetric-Redundant-NegReduced,
	show(bottom),
	p1_message('literals'), p_message(TotalLiterals),
	p1_message('saturation time'), p_message(Time),
	broadcast(end(sat(Num, TotalLiterals, Time))),
	store(bottom),
	noset(stage).
sat(_,_):-
	noset(stage).

reduce:-
	setting(search,Search), 
	catch(reduce(Search),abort,reinstate_values), !.

% no search: add bottom clause as hypothesis
reduce(false):-
	!,
	add_bottom.
% iterative beam search as described by Ross Quinlan+MikeCameron-Jones,IJCAI-95
reduce(ibs):-
	!,
	retractall('$aleph_search'(ibs_rval,_)),
	retractall('$aleph_s