1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2% A Learning Engine for Proposing Hypotheses                              %
    3%                                                                         %
    4% A L E P H                                                               %
    5% Version 5    (last modified: Sun Mar 11 03:25:37 UTC 2007)              %
    6%                                                                         %
    7% This is the source for Aleph written and maintained                     %
    8% by Ashwin Srinivasan (ashwin@comlab.ox.ac.uk)                           %
    9%                                                                         %
   10%                                                                         %
   11% It was originally written to run with the Yap Prolog Compiler           %
   12% Yap can be found at: http://sourceforge.net/projects/yap/               %
   13% Yap must be compiled with -DDEPTH_LIMIT=1                               %
   14%                                                                         %
   15% It should also run with SWI Prolog, although performance may be         %
   16% sub-optimal.                                                            %
   17%                                                                         %
   18% If you obtain this version of Aleph and have not already done so        %
   19% please subscribe to the Aleph mailing list. You can do this by          %
   20% mailing majordomo@comlab.ox.ac.uk with the following command in the     %
   21% body of the mail message: subscribe aleph                               %
   22%                                                                         %
   23% Aleph is freely available for academic purposes.                        %
   24% If you intend to use it for commercial purposes then                    %
   25% please contact Ashwin Srinivasan first.                                 %
   26%                                                                         %
   27% A simple on-line manual is available on the Web at                      %
   28% www.comlab.ox.ac.uk/oucl/research/areas/machlearn/Aleph/index.html      %
   29%                                                                         %
   30%                                                                         %
   31%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   32 
   33
   34%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   35% C O M P I L E R   S P E C I F I C
   36
   37
   38prolog_type(yap):-
   39	predicate_property(yap_flag(_,_),built_in), !.
   40prolog_type(swi).
   41
   42init(yap):-
   43	source,
   44	system_predicate(false,false), hide(false),
   45	style_check(single_var),
   46	% yap_flag(profiling,on),
   47	assert_static((aleph_random(X):- X is random)),
   48	(predicate_property(alarm(_,_,_),built_in) ->
   49		assert_static((remove_alarm(X):- alarm(0,_,_)));
   50		assert_static(alarm(_,_,_)),
   51		assert_static(remove_alarm(_))),
   52	assert_static((aleph_consult(F):- consult(F))),
   53	assert_static((aleph_reconsult(F):- reconsult(F))),
   54        (predicate_property(thread_local(_),built_in) -> true;
   55		assert_static(thread_local(_))),
   56	assert_static(broadcast(_)),
   57	assert_static((aleph_background_predicate(Lit):-
   58				predicate_property(Lit,P),
   59				((P = static); (P = dynamic); (P = built_in)), !)),
   60	(predicate_property(delete_file(_),built_in) -> true;
   61		assert_static(delete_file(_))).
   62
   63init(swi):-
   64	redefine_system_predicate(false),
   65	style_check(+singleton),
   66	style_check(-discontiguous),
   67	dynamic(false/0),
   68	dynamic(example/3),
   69	assert((aleph_random(X):- I = 1000000, X is float(random(I-1))/float(I))),
   70	assert((gc:- garbage_collect)),
   71	assert((depth_bound_call(G,L):-
   72			call_with_depth_limit(G,L,R),
   73			R \= depth_limit_exceeded)),
   74	(predicate_property(numbervars(_,_,_),built_in) -> true;
   75		assert((numbervars(A,B,C):- numbervars(A,'$VAR',B,C)))),
   76	assert((assert_static(X):- assert(X))),
   77	assert((system(X):- shell(X))),
   78	assert((exists(X):- exists_file(X))),
   79	assert((aleph_reconsult(F):- consult(F))),
   80	assert((aleph_consult(X):- aleph_open(X,read,S), repeat,
   81			read(S,F), (F = end_of_file -> close(S), !;
   82					assertz(F),fail))),
   83	use_module(library(broadcast)),
   84	use_module(library(time)),
   85        (predicate_property(thread_local(_),built_in) -> true;
   86		assert(thread_local(_))),
   87	assert((aleph_background_predicate(Lit):-
   88				predicate_property(Lit,P),
   89				((P=interpreted);(P=built_in)), ! )),
   90	(predicate_property(delete_file(_),built_in) -> true;
   91		assert_static(delete_file(_))).
   92:- if(current_prolog_flag(dialect,swi)). 
   93:- use_module(library(arithmetic)). 
   94:- arithmetic_function(inf/0). 
   95:- init(swi).   96inf(1e10).
   97:- else.   98:- init(yap).   99:- endif. 
  100
  101
  102%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  103% A L E P H
  104
  105
  106aleph_version(5).
  107aleph_version_date('Sun Mar 11 03:25:37 UTC 2007').
  108aleph_manual('http://www.comlab.ox.ac.uk/oucl/groups/machlearn/Aleph/index.html').
  109
  110:- op(500,fy,#).  111:- op(500,fy,*).  112:- op(900,xfy,because).  113
  114:- dynamic '$aleph_feature'/2.  115:- dynamic '$aleph_global'/2.  116:- dynamic '$aleph_good'/3.  117
  118:- dynamic '$aleph_local'/2.  119
  120:- dynamic '$aleph_sat'/2.  121:- dynamic '$aleph_sat_atom'/2.  122:- dynamic '$aleph_sat_ovars'/2.  123:- dynamic '$aleph_sat_ivars'/2.  124:- dynamic '$aleph_sat_varsequiv'/2.  125:- dynamic '$aleph_sat_varscopy'/3.  126:- dynamic '$aleph_sat_terms'/4.  127:- dynamic '$aleph_sat_vars'/4.  128:- dynamic '$aleph_sat_litinfo'/6.  129
  130:- dynamic '$aleph_search_cache'/1.  131:- dynamic '$aleph_search_prunecache'/1.  132:- dynamic '$aleph_search'/2.  133:- dynamic '$aleph_search_seen'/2.  134:- dynamic '$aleph_search_expansion'/4.  135:- dynamic '$aleph_search_gain'/4.  136:- dynamic '$aleph_search_node'/8.  137
  138:- dynamic '$aleph_link_vars'/2.  139:- dynamic '$aleph_has_vars'/3.  140:- dynamic '$aleph_has_ovar'/4.  141:- dynamic '$aleph_has_ivar'/4.  142:- dynamic '$aleph_determination'/2.  143
  144:- thread_local('$aleph_search_cache'/1).  145:- thread_local('$aleph_search_prunecache'/1).  146:- thread_local('$aleph_search'/2).  147:- thread_local('$aleph_search_seen'/2).  148:- thread_local('$aleph_search_expansion'/4).  149:- thread_local('$aleph_search_gain'/4).  150:- thread_local('$aleph_search_node'/8).  151
  152
  153:- multifile false/0.  154:- multifile prune/1.  155:- multifile refine/2.  156:- multifile cost/3.  157:- multifile prove/2.  158
  159%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  160% C O N S T R U C T   B O T T O M
  161
  162% get_atoms(+Preds,+Depth,+MaxDepth,+Last,-LastLit)
  163% layered generation of ground atoms to add to bottom clause
  164%	Preds is list of PName/Arity entries obtained from the determinations
  165%	Depth is current variable-chain depth
  166%	MaxDepth is maximum allowed variable chain depth (i setting)
  167%	Last is last atom number so far
  168%	Lastlit is atom number after all atoms to MaxDepth have been generated
  169get_atoms([],_,_,Last,Last):- !.
  170get_atoms(Preds,Depth,MaxDepth,Last,LastLit):-
  171	Depth =< MaxDepth,
  172	Depth0 is Depth - 1,
  173	'$aleph_sat_terms'(_,Depth0,_,_),	% new terms generated ?
  174	!,
  175	get_atoms1(Preds,Depth,MaxDepth,Last,Last1),
  176	Depth1 is Depth + 1,
  177	get_atoms(Preds,Depth1,MaxDepth,Last1,LastLit).
  178get_atoms(_,_,_,Last,Last).
  179
  180% auxiliary predicate used by get_atoms/5
  181get_atoms1([],_,_,Last,Last).
  182get_atoms1([Pred|Preds],Depth,MaxDepth,Last,LastLit):-
  183	gen_layer(Pred,Depth),
  184	flatten(Depth,MaxDepth,Last,Last1),
  185	get_atoms1(Preds,Depth,MaxDepth,Last1,LastLit).
  186
  187% flatten(+Depth,+MaxDepth,+Last,-LastLit)
  188% flatten a set of ground atoms by replacing all in/out terms with variables
  189%	constants are wrapped in a special term called aleph_const(...)
  190%	eg suppose p/3 had modes p(+char,+char,#int)
  191%	then p(a,a,3) becomes p(X,X,aleph_const(3))
  192% ground atoms to be flattened are assumed to be in the i.d.b atoms
  193% vars and terms are actually integers which are stored in vars/terms databases
  194%	so eg above actually becomes p(1,1,aleph_const(3)).
  195%	where variable 1 stands for term 2 (say) which in turn stands for a
  196%	Depth is current variable-chain depth
  197%	MaxDepth is maximum allowed variable chain depth (i setting)
  198%	Last is last atom number so far
  199%	Lastlit is atom number after ground atoms here have been flattened
  200% If permute_bottom is set to true, then the order of ground atoms is
  201% shuffled. The empirical utility of doing this has been investigated by
  202% P. Schorn in "Random Local Bottom Clause Permutations for Better Search Space
  203% Exploration in Progol-like ILP Systems.", 16th International Conference on
  204% ILP (ILP 2006).
  205flatten(Depth,MaxDepth,Last,Last1):-
  206	retractall('$aleph_local'(flatten_num,_)),
  207	asserta('$aleph_local'(flatten_num,Last)),
  208	'$aleph_sat_atom'(_,_), !,
  209	(setting(permute_bottom,Permute) -> true; Permute = false),
  210	flatten_atoms(Permute,Depth,MaxDepth,Last1).
  211flatten(_,_,_,Last):-
  212	retract('$aleph_local'(flatten_num,Last)), !.
  213
  214flatten_atoms(true,Depth,MaxDepth,Last1):-
  215	findall(L-M,retract('$aleph_sat_atom'(L,M)),LitModes),
  216	aleph_rpermute(LitModes,PLitModes),
  217	aleph_member(Lit1-Mode,PLitModes),
  218	retract('$aleph_local'(flatten_num,LastSoFar)),
  219	(Lit1 = not(Lit) -> Negated = true; Lit = Lit1, Negated = false),
  220	flatten_atom(Depth,MaxDepth,Lit,Negated,Mode,LastSoFar,Last1),
  221	asserta('$aleph_local'(flatten_num,Last1)),
  222	fail.
  223flatten_atoms(false,Depth,MaxDepth,Last1):-
  224	repeat,
  225	retract('$aleph_sat_atom'(Lit1,Mode)),
  226	retract('$aleph_local'(flatten_num,LastSoFar)),
  227	(Lit1 = not(Lit) -> Negated = true; Lit = Lit1, Negated = false),
  228	flatten_atom(Depth,MaxDepth,Lit,Negated,Mode,LastSoFar,Last1),
  229	asserta('$aleph_local'(flatten_num,Last1)),
  230	('$aleph_sat_atom'(_,_) ->
  231			fail;
  232			retract('$aleph_local'(flatten_num,Last1))), !.
  233flatten_atoms(_,_,_,Last):-
  234	retract('$aleph_local'(flatten_num,Last)), !.
  235
  236
  237% flatten_atom(+Depth,+Depth1,+Lit,+Negated,+Mode,+Last,-Last1)
  238%	update lits database by adding ``flattened atoms''. This involves:
  239%	replacing ground terms at +/- positions in Lit with variables
  240%	and wrapping # positions in Lit within a special term stucture
  241%	Mode contains actual mode and term-place numbers and types for +/-/# 
  242%	Last is the last literal number in the lits database at present
  243%	Last1 is the last literal number after the update
  244flatten_atom(Depth,Depth1,Lit,Negated,Mode,Last,Last1):-
  245	arg(3,Mode,O), arg(4,Mode,C),
  246	integrate_args(Depth,Lit,O),
  247	integrate_args(Depth,Lit,C),
  248	(Depth = Depth1 -> CheckOArgs = true; CheckOArgs = false),
  249	flatten_lits(Lit,CheckOArgs,Depth,Negated,Mode,Last,Last1).
  250
  251% variabilise literals by replacing terms with variables
  252% if var splitting is on then new equalities are introduced into bottom clause
  253% if at final i-layer, then literals with o/p args that do not contain at least
  254% 	one output var from head are discarded
  255flatten_lits(Lit,CheckOArgs,Depth,Negated,Mode,Last,_):-
  256	functor(Lit,Name,Arity),
  257	asserta('$aleph_local'(flatten_lits,Last)),
  258	Depth1 is Depth - 1,
  259	functor(OldFAtom,Name,Arity),
  260	flatten_lit(Lit,Mode,OldFAtom,_,_),
  261	functor(FAtom,Name,Arity),
  262	apply_equivs(Depth1,Arity,OldFAtom,FAtom),
  263	retract('$aleph_local'(flatten_lits,OldLast)),
  264	(CheckOArgs = true -> 
  265		arg(3,Mode,Out),
  266		get_vars(FAtom,Out,OVars),
  267		(in_path(OVars) ->
  268			add_new_lit(Depth,FAtom,Mode,OldLast,Negated,NewLast);
  269			NewLast = OldLast) ;
  270		add_new_lit(Depth,FAtom,Mode,OldLast,Negated,NewLast)),
  271	asserta('$aleph_local'(flatten_lits,NewLast)),
  272	fail.
  273flatten_lits(_,_,_,_,_,_,Last1):-
  274	retract('$aleph_local'(flatten_lits,Last1)).
  275
  276
  277% flatten_lit(+Lit,+Mode,+FAtom,-IVars,-OVars)
  278% variabilise Lit as FAtom
  279%	Mode contains actual mode and 
  280%	In, Out, Const positions as term-place numbers with types
  281% 	replace ground terms with integers denoting variables
  282%	or special terms denoting constants
  283% 	variable numbers arising from variable splits are disallowed
  284%	returns Input and Output variable numbers
  285flatten_lit(Lit,mode(Mode,In,Out,Const),FAtom,IVars,OVars):-
  286	functor(Mode,_,Arity),
  287	once(copy_modeterms(Mode,FAtom,Arity)),
  288	flatten_vars(In,Lit,FAtom,IVars),
  289	flatten_vars(Out,Lit,FAtom,OVars),
  290	flatten_consts(Const,Lit,FAtom).
  291
  292% flatten_vars(+TPList,+Lit,+FAtom,-Vars):-
  293% FAtom is Lit with terms-places in TPList replaced by variables
  294flatten_vars([],_,_,[]).
  295flatten_vars([Pos/Type|Rest],Lit,FAtom,[Var|Vars]):-
  296	tparg(Pos,Lit,Term),
  297	'$aleph_sat_terms'(TNo,_,Term,Type),
  298	'$aleph_sat_vars'(Var,TNo,_,_),
  299	\+('$aleph_sat_varscopy'(Var,_,_)),
  300	tparg(Pos,FAtom,Var),
  301	flatten_vars(Rest,Lit,FAtom,Vars).
  302
  303% replace a list of terms at places marked by # in the modes
  304% with a special term structure denoting a constant
  305flatten_consts([],_,_).
  306flatten_consts([Pos/_|Rest],Lit,FAtom):-
  307	tparg(Pos,Lit,Term),
  308	tparg(Pos,FAtom,aleph_const(Term)),
  309	flatten_consts(Rest,Lit,FAtom).
  310
  311% in_path(+ListOfOutputVars)
  312% check to avoid generating useless literals in the last i layer
  313in_path(OVars):-
  314	'$aleph_sat'(hovars,Vars), !,
  315	(Vars=[];OVars=[];intersects(Vars,OVars)).
  316in_path(_).
  317
  318% update_equivs(+VariableEquivalences,+IDepth)
  319% update variable equivalences created at a particular i-depth
  320% is non-empty only if variable splitting is allowed
  321update_equivs([],_):- !.
  322update_equivs(Equivs,Depth):-
  323	retract('$aleph_sat_varsequiv'(Depth,Eq1)), !,
  324	update_equiv_lists(Equivs,Eq1,Eq2),
  325	asserta('$aleph_sat_varsequiv'(Depth,Eq2)).
  326update_equivs(Equivs,Depth):-
  327	Depth1 is Depth - 1,
  328	get_equivs(Depth1,Eq1),
  329	update_equiv_lists(Equivs,Eq1,Eq2),
  330	asserta('$aleph_sat_varsequiv'(Depth,Eq2)).
  331
  332update_equiv_lists([],E,E):- !.
  333update_equiv_lists([Var/E1|Equivs],ESoFar,E):-
  334	aleph_delete(Var/E2,ESoFar,ELeft), !,
  335	update_list(E1,E2,E3),
  336	update_equiv_lists(Equivs,[Var/E3|ELeft],E).
  337update_equiv_lists([Equiv|Equivs],ESoFar,E):-
  338	update_equiv_lists(Equivs,[Equiv|ESoFar],E).
  339
  340% get variable equivalences at a particular depth
  341% recursively descend to greatest depth below this for which equivs exist
  342% also returns the database reference of entry
  343get_equivs(Depth,[]):-
  344	Depth < 0, !.
  345get_equivs(Depth,Equivs):-
  346	'$aleph_sat_varsequiv'(Depth,Equivs), !.
  347get_equivs(Depth,E):-
  348	Depth1 is Depth - 1,
  349	get_equivs(Depth1,E).
  350
  351% apply equivalences inherited from Depth to a flattened literal
  352% if no variable splitting, then succeeds only once
  353apply_equivs(Depth,Arity,Old,New):-
  354	get_equivs(Depth,Equivs),
  355	rename(Arity,Equivs,[],Old,New).
  356
  357% rename args using list of Var/Equivalences
  358rename(_,[],_,L,L):- !.
  359rename(0,_,_,_,_):- !.
  360rename(Pos,Equivs,Subst0,Old,New):-
  361        arg(Pos,Old,OldVar),
  362        aleph_member(OldVar/Equiv,Equivs), !,
  363        aleph_member(NewVar,Equiv),
  364        arg(Pos,New,NewVar),
  365        Pos1 is Pos - 1,
  366        rename(Pos1,Equivs,[OldVar/NewVar|Subst0],Old,New).
  367rename(Pos,Equivs,Subst0,Old,New):-
  368        arg(Pos,Old,OldVar),
  369        (aleph_member(OldVar/NewVar,Subst0) ->
  370                arg(Pos,New,NewVar);
  371                arg(Pos,New,OldVar)),
  372        Pos1 is Pos - 1,
  373        rename(Pos1,Equivs,Subst0,Old,New).
  374
  375
  376% add a new literal to lits database
  377% performs variable splitting if splitvars is set to true
  378add_new_lit(Depth,FAtom,Mode,OldLast,Negated,NewLast):-
  379	arg(1,Mode,M),
  380	functor(FAtom,Name,Arity),
  381	functor(SplitAtom,Name,Arity),
  382	once(copy_modeterms(M,SplitAtom,Arity)),
  383	arg(2,Mode,In), arg(3,Mode,Out), arg(4,Mode,Const),
  384        split_vars(Depth,FAtom,In,Out,Const,SplitAtom,IVars,OVars,Equivs),
  385        update_equivs(Equivs,Depth),
  386        add_lit(OldLast,Negated,SplitAtom,In,Out,IVars,OVars,LitNum),
  387        insert_eqs(Equivs,Depth,LitNum,NewLast), !.
  388
  389% modify the literal database: check if performing lazy evaluation
  390% of bottom clause, and update input and output terms in literal
  391add_lit(Last,Negated,FAtom,I,O,_,_,Last):-
  392	setting(construct_bottom,CBot),
  393	(CBot = false ; CBot = reduction), 
  394	(Negated = true -> Lit = not(FAtom); Lit = FAtom),
  395	'$aleph_sat_litinfo'(_,0,Lit,I,O,_), !.
  396add_lit(Last,Negated,FAtom,In,Out,IVars,OVars,LitNum):-
  397	LitNum is Last + 1,
  398	update_iterms(LitNum,IVars),
  399	update_oterms(LitNum,OVars,[],Dependents),
  400	add_litinfo(LitNum,Negated,FAtom,In,Out,Dependents),
  401	assertz('$aleph_sat_ivars'(LitNum,IVars)),
  402	assertz('$aleph_sat_ovars'(LitNum,OVars)), !.
  403
  404
  405% update lits database after checking that the atom does not exist
  406% used during updates of lit database by lazy evaluation
  407update_lit(LitNum,true,FAtom,I,O,D):-
  408	'$aleph_sat_litinfo'(LitNum,0,not(FAtom),I,O,D), !.
  409update_lit(LitNum,false,FAtom,I,O,D):-
  410	'$aleph_sat_litinfo'(LitNum,0,FAtom,I,O,D), !.
  411update_lit(LitNum,Negated,FAtom,I,O,D):-
  412	gen_nlitnum(LitNum),
  413	add_litinfo(LitNum,Negated,FAtom,I,O,D), 
  414	get_vars(FAtom,I,IVars),
  415	get_vars(FAtom,O,OVars),
  416	assertz('$aleph_sat_ivars'(LitNum,K,IVars)),
  417	assertz('$aleph_sat_ovars'(LitNum,K,OVars)), !.
  418
  419% add a literal to lits database without checking
  420add_litinfo(LitNum,true,FAtom,I,O,D):-
  421	!,
  422	assertz('$aleph_sat_litinfo'(LitNum,0,not(FAtom),I,O,D)).
  423add_litinfo(LitNum,_,FAtom,I,O,D):-
  424	assertz('$aleph_sat_litinfo'(LitNum,0,FAtom,I,O,D)).
  425	
  426% update database with input terms of literal
  427update_iterms(_,[]).
  428update_iterms(LitNum,[VarNum|Vars]):-
  429	retract('$aleph_sat_vars'(VarNum,TNo,I,O)),
  430	update(I,LitNum,NewI),
  431	asserta('$aleph_sat_vars'(VarNum,TNo,NewI,O)),
  432	update_dependents(LitNum,O),
  433	update_iterms(LitNum,Vars).
  434
  435% update database with output terms of literal
  436% return list of dependent literals
  437update_oterms(_,[],Dependents,Dependents).
  438update_oterms(LitNum,[VarNum|Vars],DSoFar,Dependents):-
  439	retract('$aleph_sat_vars'(VarNum,TNo,I,O)),
  440	update(O,LitNum,NewO),
  441	asserta('$aleph_sat_vars'(VarNum,TNo,I,NewO)),
  442	update_list(I,DSoFar,D1),
  443	update_oterms(LitNum,Vars,D1,Dependents).
  444
  445% update Dependent list of literals with LitNum
  446update_dependents(_,[]).
  447update_dependents(LitNum,[Lit|Lits]):-
  448	retract('$aleph_sat_litinfo'(Lit,Depth,Atom,ITerms,OTerms,Dependents)),
  449	update(Dependents,LitNum,NewD),
  450	asserta('$aleph_sat_litinfo'(Lit,Depth,Atom,ITerms,OTerms,NewD)),
  451	update_dependents(LitNum,Lits).
  452
  453% update dependents of head with literals that are simply generators
  454% 	that is, literals that require no input args
  455update_generators:-
  456	findall(L,('$aleph_sat_litinfo'(L,_,_,[],_,_),L>1),GList),
  457	GList \= [], !,
  458	retract('$aleph_sat_litinfo'(1,Depth,Lit,I,O,D)),
  459	aleph_append(D,GList,D1),
  460	asserta('$aleph_sat_litinfo'(1,Depth,Lit,I,O,D1)).
  461update_generators.
  462
  463% mark literals 
  464mark_lits(Lits):-
  465	aleph_member(Lit,Lits),
  466	asserta('$aleph_local'(marked,Lit/0)),
  467	fail.
  468mark_lits(_).
  469	
  470% recursively mark literals with minimum depth to bind output vars in head
  471mark_lits([],_,_).
  472mark_lits(Lits,OldVars,Depth):-
  473	mark_lits(Lits,Depth,true,[],Predecessors,OldVars,NewVars),
  474	aleph_delete_list(Lits,Predecessors,P1),
  475	Depth1 is Depth + 1,
  476	mark_lits(P1,NewVars,Depth1).
  477
  478mark_lits([],_,_,P,P,V,V).
  479mark_lits([Lit|Lits],Depth,GetPreds,PSoFar,P,VSoFar,V):-
  480	retract('$aleph_local'(marked,Lit/Depth0)), !,
  481	(Depth < Depth0 ->
  482		mark_lit(Lit,Depth,GetPreds,VSoFar,P1,V2),
  483		update_list(P1,PSoFar,P2),
  484		mark_lits(Lits,Depth,GetPreds,P2,P,V2,V);
  485		asserta('$aleph_local'(marked,Lit/Depth0)),
  486		mark_lits(Lits,Depth,GetPreds,PSoFar,P,VSoFar,V)).
  487mark_lits([Lit|Lits],Depth,GetPreds,PSoFar,P,VSoFar,V):-
  488	mark_lit(Lit,Depth,GetPreds,VSoFar,P1,V2), !,
  489	update_list(P1,PSoFar,P2),
  490	mark_lits(Lits,Depth,GetPreds,P2,P,V2,V).
  491mark_lits([_|Lits],Depth,GetPreds,PSoFar,P,VSoFar,V):-
  492	mark_lits(Lits,Depth,GetPreds,PSoFar,P,VSoFar,V).
  493
  494mark_lit(Lit,Depth,GetPreds,VSoFar,P1,V1):-
  495	retract('$aleph_sat_litinfo'(Lit,_,Atom,I,O,D)),
  496	asserta('$aleph_local'(marked,Lit/Depth)),
  497	asserta('$aleph_sat_litinfo'(Lit,Depth,Atom,I,O,D)),
  498	(GetPreds = false ->
  499		P1 = [],
  500		V1 = VSoFar;
  501		get_vars(Atom,O,OVars),
  502		update_list(OVars,VSoFar,V1),
  503		get_predicates(D,V1,D1),
  504		mark_lits(D1,Depth,false,[],_,VSoFar,_),
  505		get_vars(Atom,I,IVars),
  506		get_predecessors(IVars,[],P1)).
  507
  508% mark lits that produce outputs that are not used by any other literal
  509mark_floating_lits(Lit,Last):-
  510	Lit > Last, !.
  511mark_floating_lits(Lit,Last):-
  512	'$aleph_sat_litinfo'(Lit,_,_,_,O,D),
  513	O \= [],
  514	(D = []; D = [Lit]), !,
  515	asserta('$aleph_local'(marked,Lit/0)),
  516	Lit1 is Lit + 1,
  517	mark_floating_lits(Lit1,Last).
  518mark_floating_lits(Lit,Last):-
  519	Lit1 is Lit + 1,
  520	mark_floating_lits(Lit1,Last).
  521	
  522% mark lits in bottom clause that are specified redundant by user
  523% requires definition of redundant/2 that have distinguished first arg ``bottom''
  524mark_redundant_lits(Lit,Last):-
  525	Lit > Last, !.
  526mark_redundant_lits(Lit,Last):-
  527	get_pclause([Lit],[],Atom,_,_,_),
  528	redundant(bottom,Atom), !,
  529	asserta('$aleph_local'(marked,Lit/0)),
  530	Lit1 is Lit + 1,
  531	mark_redundant_lits(Lit1,Last).
  532mark_redundant_lits(Lit,Last):-
  533	Lit1 is Lit + 1,
  534	mark_redundant_lits(Lit1,Last).
  535
  536% get literals that are linked and do not link to any others (ie predicates)
  537get_predicates([],_,[]).
  538get_predicates([Lit|Lits],Vars,[Lit|T]):-
  539	'$aleph_sat_litinfo'(Lit,_,Atom,I,_,[]),
  540	get_vars(Atom,I,IVars),
  541	aleph_subset1(IVars,Vars), !,
  542	get_predicates(Lits,Vars,T).
  543get_predicates([_|Lits],Vars,T):-
  544	get_predicates(Lits,Vars,T).
  545
  546% get all predecessors in the bottom clause of a set of literals
  547get_predecessors([],[]).
  548get_predecessors([Lit|Lits],P):-
  549	(Lit = 1 -> Pred = [];
  550		get_ivars1(false,Lit,IVars),
  551		get_predecessors(IVars,[],Pred)),
  552	get_predecessors(Pred,PPred),
  553	update_list(Pred,PPred,P1),
  554	get_predecessors(Lits,P2),
  555	update_list(P2,P1,P).
  556
  557% get list of literals in the bottom clause that produce a set of vars
  558get_predecessors([],P,P).
  559get_predecessors([Var|Vars],PSoFar,P):-
  560	'$aleph_sat_vars'(Var,_,_,O),
  561	update_list(O,PSoFar,P1),
  562	get_predecessors(Vars,P1,P).
  563
  564% removal of literals in bottom clause by negative-based reduction.
  565% A greedy strategy is employed, as implemented within the ILP system
  566% Golem (see Muggleton and Feng, "Efficient induction
  567% of logic programs", Inductive Logic Programming, S. Muggleton (ed.),
  568% AFP Press). In this, given a clause H:- B1, B2,...Bn, let Bi be the
  569% first literal s.t. H:-B1,...,Bi covers no more than the allowable number
  570% of negatives. The clause H:- Bi,B1,...,Bi-1 is then reduced. The
  571% process continues until there is no change in the length of a clause
  572% within an iteration. The algorithm is O(n^2).
  573rm_nreduce(Last,N):-
  574	setting(nreduce_bottom,true), !,
  575	get_litnums(1,Last,BottomLits),
  576        '$aleph_global'(atoms,atoms(neg,Neg)),
  577	setting(depth,Depth),
  578	setting(prooftime,Time),
  579	setting(proof_strategy,Proof),
  580	setting(noise,Noise),
  581	neg_reduce(BottomLits,Neg,Last,Depth/Time/Proof,Noise),
  582	get_marked(1,Last,Lits),
  583	length(Lits,N),
  584	p1_message('negative-based removal'), p_message(N/Last).
  585rm_nreduce(_,0).
  586
  587neg_reduce([Head|Body],Neg,Last,DepthTime,Noise):-
  588	get_pclause([Head],[],Clause,TV,_,_),
  589	neg_reduce(Body,Clause,TV,2,Neg,DepthTime,Noise,NewLast),
  590	NewLast \= Last, !,
  591	NewLast1 is NewLast - 1,
  592	aleph_remove_n(NewLast1,[Head|Body],Prefix,[LastLit|Rest]),
  593	mark_lits(Rest),
  594	insert_lastlit(LastLit,Prefix,Lits1),
  595	neg_reduce(Lits1,Neg,NewLast,DepthTime,Noise).
  596neg_reduce(_,_,_,_,_).
  597
  598neg_reduce([],_,_,N,_,_,_,N).
  599neg_reduce([L1|Lits],C,TV,N,Neg,ProofFlags,Noise,LastLit):-
  600	get_pclause([L1],TV,Lit1,TV1,_,_),
  601	extend_clause(C,Lit1,Clause),
  602        prove(ProofFlags,neg,Clause,Neg,NegCover,Count),
  603	Count > Noise, !,
  604	N1 is N + 1,
  605	neg_reduce(Lits,Clause,TV1,N1,NegCover,ProofFlags,Noise,LastLit).
  606neg_reduce(_,_,_,N,_,_,_,N).
  607
  608% insert_lastlit(LastLit,[1|Lits],Lits1):-
  609	% find_last_ancestor(Lits,LastLit,1,2,Last),
  610	% aleph_remove_n(Last,[1|Lits],Prefix,Suffix),
  611	% aleph_append([LastLit|Suffix],Prefix,Lits1).
  612
  613insert_lastlit(LastLit,Lits,Lits1):-
  614	get_predecessors([LastLit],Prefix),
  615	aleph_delete_list(Prefix,Lits,Suffix),
  616	aleph_append([LastLit|Suffix],Prefix,Lits1).
  617
  618	
  619find_last_ancestor([],_,Last,_,Last):- !.
  620find_last_ancestor([Lit|Lits],L,_,LitNum,Last):-
  621	'$aleph_sat_litinfo'(Lit,_,_,_,_,D), 
  622	aleph_member1(L,D), !,
  623	NextLit is LitNum + 1,
  624	find_last_ancestor(Lits,L,LitNum,NextLit,Last).
  625find_last_ancestor([_|Lits],L,Last0,LitNum,Last):-
  626	NextLit is LitNum + 1,
  627	find_last_ancestor(Lits,L,Last0,NextLit,Last).
  628
  629% removal of literals that are repeated because of mode differences
  630rm_moderepeats(_,_):-
  631	'$aleph_sat_litinfo'(Lit1,_,Pred1,_,_,_),
  632	'$aleph_sat_litinfo'(Lit2,_,Pred1,_,_,_),
  633	Lit1 >= 1, Lit2 > Lit1,
  634	retract('$aleph_sat_litinfo'(Lit2,_,Pred1,_,_,_)),
  635	asserta('$aleph_local'(marked,Lit2/0)),
  636	fail.
  637rm_moderepeats(Last,N):-
  638	'$aleph_local'(marked,_), !,
  639	get_marked(1,Last,Lits),
  640	length(Lits,N),
  641	p1_message('repeated literals'), p_message(N/Last),
  642	remove_lits(Lits).
  643rm_moderepeats(_,0).
  644	
  645% removal of symmetric literals
  646rm_symmetric(_,_):-
  647	'$aleph_global'(symmetric,_),
  648	'$aleph_sat_litinfo'(Lit1,_,Pred1,[I1|T1],_,_),
  649	is_symmetric(Pred1,Name,Arity),
  650	get_vars(Pred1,[I1|T1],S1),
  651	'$aleph_sat_litinfo'(Lit2,_,Pred2,[I2|T2],_,_),
  652	Lit1 \= Lit2,
  653	is_symmetric(Pred2,Name,Arity),
  654	Pred1 =.. [_|Args1],
  655	Pred2 =.. [_|Args2],
  656	symmetric_match(Args1,Args2),
  657	get_vars(Pred2,[I2|T2],S2),
  658	equal_set(S1,S2),
  659	asserta('$aleph_local'(marked,Lit2/0)),
  660	retract('$aleph_sat_litinfo'(Lit2,_,Pred2,[I2|T2],_,_)),
  661	fail.
  662rm_symmetric(Last,N):-
  663	'$aleph_local'(marked,_), !,
  664	get_marked(1,Last,Lits),
  665	length(Lits,N),
  666	p1_message('symmetric literals'), p_message(N/Last),
  667	remove_lits(Lits).
  668rm_symmetric(_,0).
  669
  670is_symmetric(not(Pred),not(Name),Arity):-
  671	!,
  672	functor(Pred,Name,Arity),
  673	'$aleph_global'(symmetric,symmetric(Name/Arity)).
  674is_symmetric(Pred,Name,Arity):-
  675	functor(Pred,Name,Arity),
  676	'$aleph_global'(symmetric,symmetric(Name/Arity)).
  677
  678symmetric_match([],[]).
  679symmetric_match([aleph_const(Term)|Terms1],[aleph_const(Term)|Terms2]):-
  680	!,
  681	symmetric_match(Terms1,Terms2).
  682symmetric_match([Term1|Terms1],[Term2|Terms2]):-
  683	integer(Term1), integer(Term2),
  684	symmetric_match(Terms1,Terms2).
  685	
  686% removal of literals that are repeated because of commutativity
  687rm_commutative(_,_):-
  688	'$aleph_global'(commutative,commutative(Name/Arity)),
  689	p1_message('checking commutative literals'), p_message(Name/Arity),
  690	functor(Pred,Name,Arity), functor(Pred1,Name,Arity),
  691	'$aleph_sat_litinfo'(Lit1,_,Pred,[I1|T1],O1,_),
  692        % check for marked literals
  693	% (SWI-Prolog specific: suggested by Vasili Vrubleuski)
  694        \+('$aleph_local'(marked,Lit1/0)),
  695	get_vars(Pred,[I1|T1],S1),
  696	'$aleph_sat_litinfo'(Lit2,_,Pred1,[I2|T2],O2,_),
  697	Lit1 \= Lit2 ,
  698	O1 = O2,
  699	get_vars(Pred1,[I2|T2],S2),
  700	equal_set(S1,S2),
  701	asserta('$aleph_local'(marked,Lit2/0)),
  702	retract('$aleph_sat_litinfo'(Lit2,_,Pred1,[I2|T2],_,_)),
  703	fail.
  704rm_commutative(Last,N):-
  705	'$aleph_local'(marked,_), !,
  706	get_marked(1,Last,Lits),
  707	length(Lits,N),
  708	p1_message('commutative literals'), p_message(N/Last),
  709	remove_lits(Lits).
  710rm_commutative(_,0).
  711
  712% recursive marking of literals that do not contribute to establishing
  713% variable chains to output vars in the head
  714% or produce outputs that are not used by any literal
  715% controlled by setting flag check_useless
  716rm_uselesslits(_,0):-
  717	setting(check_useless,false), !.
  718rm_uselesslits(Last,N):-
  719	'$aleph_sat'(hovars,OVars),
  720	OVars \= [], !,
  721	get_predecessors(OVars,[],P),
  722	'$aleph_sat'(hivars,IVars),
  723	mark_lits(P,IVars,0),
  724	get_unmarked(1,Last,Lits),
  725	length(Lits,N),
  726	p1_message('useless literals'), p_message(N/Last),
  727	remove_lits(Lits).
  728rm_uselesslits(_,0).
  729
  730% call user-defined predicate redundant/2 to remove redundant
  731% literals from bottom clause. Redundancy checking only done on request
  732rm_redundant(_,0):-
  733	setting(check_redundant,false), !.
  734rm_redundant(Last,N):-
  735	mark_redundant_lits(1,Last),
  736	get_marked(1,Last,Lits),
  737	length(Lits,N),
  738	p1_message('redundant literals'), p_message(N/Last),
  739	remove_lits(Lits).
  740
  741% get a list of unmarked literals
  742get_unmarked(Lit,Last,[]):-
  743	Lit > Last, !.
  744get_unmarked(Lit,Last,Lits):-
  745	retract('$aleph_local'(marked,Lit/_)), !,
  746	Next is Lit + 1,
  747	get_unmarked(Next,Last,Lits).
  748get_unmarked(Lit,Last,[Lit|Lits]):-
  749	retract('$aleph_sat_litinfo'(Lit,_,_,_,_,_)), !,
  750	Next is Lit + 1,
  751	get_unmarked(Next,Last,Lits).
  752get_unmarked(Lit,Last,Lits):-
  753	Next is Lit + 1,
  754	get_unmarked(Next,Last,Lits).
  755
  756% get a list of marked literals
  757get_marked(Lit,Last,[]):-
  758	Lit > Last, !.
  759get_marked(Lit,Last,[Lit|Lits]):-
  760	retract('$aleph_local'(marked,Lit/_)), !,
  761	(retract('$aleph_sat_litinfo'(Lit,_,_,_,_,_)) ->
  762		true;
  763		true),
  764	Next is Lit + 1,
  765	get_marked(Next,Last,Lits).
  766get_marked(Lit,Last,Lits):-
  767	Next is Lit + 1,
  768	get_marked(Next,Last,Lits).
  769
  770% update descendent lists of literals by removing useless literals
  771remove_lits(L):-
  772	retract('$aleph_sat_litinfo'(Lit,Depth,A,I,O,D)), 
  773	aleph_delete_list(L,D,D1),
  774	asserta('$aleph_sat_litinfo'(Lit,Depth,A,I,O,D1)),
  775	fail.
  776remove_lits(_).
  777
  778% generate a new literal at depth Depth: forced backtracking will give all lits
  779gen_layer(Name/Arity,Depth):-
  780	(Name/Arity = (not)/1 ->
  781		'$aleph_global'(modeb,modeb(NSucc,not(Mode))),
  782		functor(Mode,Name1,Arity1),
  783		functor(Lit1,Name1,Arity1),
  784		once(copy_modeterms(Mode,Lit1,Arity1)),
  785		Lit = not(Lit1);
  786		functor(Mode,Name,Arity),
  787		functor(Lit,Name,Arity),
  788		'$aleph_global'(modeb,modeb(NSucc,Mode)),
  789		once(copy_modeterms(Mode,Lit,Arity))),
  790	split_args(Mode,Mode,Input,Output,Constants),
  791	(Input = [] -> Call1 = true, Call2 = true;
  792		aleph_delete(Arg/Type,Input,OtherInputs),
  793		Depth1 is Depth - 1,
  794		construct_incall(Lit,Depth1,[Arg/Type],Call1),
  795		construct_call(Lit,Depth,OtherInputs,Call2)),
  796	Call1,
  797	Call2,
  798	aleph_background_predicate(Lit),
  799	get_successes(Lit,NSucc,mode(Mode,Input,Output,Constants)),
  800	fail.
  801gen_layer(_,_).
  802
  803get_successes(Literal,1,M):-
  804	depth_bound_call(Literal), 
  805	update_atoms(Literal,M), !.
  806get_successes(Literal,*,M):-
  807	depth_bound_call(Literal), 
  808	update_atoms(Literal,M).
  809get_successes(Literal,N,M):-
  810	integer(N),
  811	N > 1,
  812	reset_succ,
  813	get_nsuccesses(Literal,N,M).
  814
  815% get at most N matches for a literal
  816get_nsuccesses(Literal,N,M):-
  817	depth_bound_call(Literal), 
  818	retract('$aleph_local'(last_success,Succ0)),
  819	Succ0 < N,
  820	Succ1 is Succ0 + 1,
  821	update_atoms(Literal,M),
  822	asserta('$aleph_local'(last_success,Succ1)),
  823	(Succ1 >= N -> !; true).
  824
  825update_atoms(Atom,M):-
  826	'$aleph_sat_atom'(Atom,M), !.
  827update_atoms(Atom,M):-
  828	assertz('$aleph_sat_atom'(Atom,M)).
  829
  830% call with input term that is an ouput of a previous literal
  831construct_incall(_,_,[],true):- !.
  832construct_incall(not(Lit),Depth,Args,Call):-
  833	!,
  834	construct_incall(Lit,Depth,Args,Call).
  835construct_incall(Lit,Depth,[Pos/Type],Call):-
  836	!,
  837	Call = legal_term(exact,Depth,Type,Term),
  838	tparg(Pos,Lit,Term).
  839construct_incall(Lit,Depth,[Pos/Type|Args],(Call,Calls)):-
  840	tparg(Pos,Lit,Term),
  841	Call = legal_term(exact,Depth,Type,Term),
  842	(var(Depth)-> construct_incall(Lit,_,Args,Calls);
  843		construct_incall(Lit,Depth,Args,Calls)).
  844
  845construct_call(_,_,[],true):- !.
  846construct_call(not(Lit),Depth,Args,Call):-
  847	!,
  848	construct_call(Lit,Depth,Args,Call).
  849construct_call(Lit,Depth,[Pos/Type],Call):-
  850	!,
  851	Call = legal_term(upper,Depth,Type,Term),
  852	tparg(Pos,Lit,Term).
  853construct_call(Lit,Depth,[Pos/Type|Args],(Call,Calls)):-
  854	tparg(Pos,Lit,Term),
  855	Call = legal_term(upper,Depth,Type,Term),
  856	construct_call(Lit,Depth,Args,Calls).
  857
  858% generator of legal terms seen so far
  859legal_term(exact,Depth,Type,Term):-
  860	'$aleph_sat_terms'(TNo,Depth,Term,Type),
  861	once('$aleph_sat_vars'(_,TNo,_,[_|_])).
  862% legal_term(exact,Depth,Type,Term):-
  863	% '$aleph_sat_varscopy'(NewVar,OldVar,Depth),
  864	% once('$aleph_sat_vars'(NewVar,TNo,_,_)),
  865	% '$aleph_sat_terms'(TNo,_,Term,Type),_).
  866legal_term(upper,Depth,Type,Term):-
  867	'$aleph_sat_terms'(TNo,Depth1,Term,Type),
  868	Depth1 \= unknown,
  869	Depth1 < Depth,
  870	once('$aleph_sat_vars'(_,TNo,_,[_|_])).
  871% legal_term(upper,Depth,Type,Term):-
  872	% '$aleph_sat_varscopy'(NewVar,OldVar,Depth),
  873	% once('$aleph_sat_vars'(NewVar,TNo,_,_)),
  874	% '$aleph_sat_terms'(TNo,Depth1,Term,Type),
  875	% Depth1 \= unknown.
  876
  877%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  878% V A R I A B L E  -- S P L I T T I N G
  879
  880
  881split_vars(Depth,FAtom,I,O,C,SplitAtom,IVars,OVars,Equivs):-
  882	setting(splitvars,true), !,
  883        get_args(FAtom,I,[],IVarList),
  884        get_args(FAtom,O,[],OVarList),
  885	get_var_equivs(Depth,IVarList,OVarList,IVars,OVars0,Equivs0),
  886	(Equivs0 = [] ->
  887		OVars = OVars0, SplitAtom = FAtom, Equivs = Equivs0;
  888		functor(FAtom,Name,Arity),
  889		functor(SplitAtom,Name,Arity),
  890		copy_args(FAtom,SplitAtom,I),
  891		copy_args(FAtom,SplitAtom,C),
  892		rename_ovars(O,Depth,FAtom,SplitAtom,Equivs0,Equivs),
  893		get_argterms(SplitAtom,O,[],OVars)).
  894	% write('splitting: '), write(FAtom), write(' to: '), write(SplitAtom), nl.
  895split_vars(_,FAtom,I,O,_,FAtom,IVars,OVars,[]):-
  896	get_vars(FAtom,I,IVars),
  897	get_vars(FAtom,O,OVars).
  898
  899% get equivalent classes of variables from co-references 
  900get_var_equivs(Depth,IVarList,OVarList,IVars,OVars,Equivs):-
  901	sort(IVarList,IVars),
  902	sort(OVarList,OVars),
  903	(Depth = 0 ->
  904		intersect1(IVars,OVarList,IOCoRefs,_),
  905		get_repeats(IVarList,IOCoRefs,ICoRefs);
  906		intersect1(IVars,OVarList,ICoRefs,_)),
  907	get_repeats(OVarList,ICoRefs,CoRefs),
  908	add_equivalences(CoRefs,Depth,Equivs).
  909
  910add_equivalences([],_,[]).
  911add_equivalences([Var|Vars],Depth,[Var/E|Rest]):-
  912	% (Depth = 0 -> E = []; E = [Var]),
  913	E = [Var],
  914	add_equivalences(Vars,Depth,Rest).
  915
  916
  917get_repeats([],L,L).
  918get_repeats([Var|Vars],Ref1,L):-
  919	aleph_member1(Var,Vars), !,
  920	update(Ref1,Var,Ref2),
  921	get_repeats(Vars,Ref2,L).
  922get_repeats([_|Vars],Ref,L):-
  923	get_repeats(Vars,Ref,L).
  924
  925% rename all output vars that are co-references
  926% updates vars database and return equivalent class of variables
  927rename_ovars([],_,_,_,L,L).
  928rename_ovars([ArgNo|Args],Depth,Old,New,CoRefs,Equivalences):-
  929	(ArgNo = Pos/_ -> true; Pos = ArgNo),
  930	tparg(Pos,Old,OldVar),
  931	aleph_delete(OldVar/Equiv,CoRefs,Rest), !,
  932	copy_var(OldVar,NewVar,Depth),
  933	tparg(Pos,New,NewVar),
  934	rename_ovars(Args,Depth,Old,New,[OldVar/[NewVar|Equiv]|Rest],Equivalences).
  935rename_ovars([ArgNo|Args],Depth,Old,New,CoRefs,Equivalences):-
  936	(ArgNo = Pos/_ -> true; Pos = ArgNo),
  937	tparg(Pos,Old,OldVar),
  938	tparg(Pos,New,OldVar),
  939	rename_ovars(Args,Depth,Old,New,CoRefs,Equivalences).
  940
  941% create new  equalities to  allow co-references to re-appear in search
  942insert_eqs([],_,L,L).
  943insert_eqs([OldVar/Equivs|Rest],Depth,Last,NewLast):-
  944	'$aleph_sat_vars'(OldVar,TNo,_,_),
  945	'$aleph_sat_terms'(TNo,_,_,Type),
  946	add_eqs(Equivs,Depth,Type,Last,Last1),
  947	insert_eqs(Rest,Depth,Last1,NewLast).
  948
  949add_eqs([],_,_,L,L).
  950add_eqs([V1|Rest],Depth,Type,Last,NewLast):-
  951	add_eqs(Rest,Depth,V1,Type,Last,Last1),
  952	add_eqs(Rest,Depth,Type,Last1,NewLast).
  953
  954add_eqs([],_,_,_,L,L).
  955add_eqs([Var2|Rest],Depth,Var1,Type,Last,NewLast):-
  956	(Depth = 0 -> 
  957		add_lit(Last,false,(Var1=Var2),[1/Type],[2/Type],[Var1],[Var2],Last1);
  958		add_lit(Last,false,(Var1=Var2),[1/Type,2/Type],[],[Var1,Var2],[],Last1)),
  959	add_eqs(Rest,Depth,Var1,Type,Last1,NewLast).
  960	
  961
  962
  963%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  964% utilities for updating mappings between terms and variables
  965
  966% integrate terms specified by a list of arguments
  967% integrating a term means:
  968%	updating 2 databases: terms and vars
  969%	terms contains the term along with a term-id
  970%	vars contains a var-id <-> term-id mapping
  971% var and term-ids are integers
  972integrate_args(_,_,[]).
  973integrate_args(Depth,Literal,[Pos/Type|T]):-
  974        tparg(Pos,Literal,Term),
  975        integrate_term(Depth,Term/Type),
  976	(retract('$aleph_sat_terms'(TNo,Depth,Term,unknown)) ->
  977		asserta('$aleph_sat_terms'(TNo,Depth,Term,Type));
  978		true),
  979        integrate_args(Depth,Literal,T).
  980
  981
  982% integrate a term
  983integrate_term(Depth,Term/Type):-
  984        '$aleph_sat_terms'(TNo,Depth,Term,Type),
  985        '$aleph_sat_vars'(_,TNo,_,[_|_]), !.
  986integrate_term(Depth,Term/Type):-
  987        '$aleph_sat_terms'(TNo,Depth1,Term,Type),
  988        (Type = unknown ; '$aleph_sat_vars'(_,TNo,_,[])), !,
  989	(Depth1 = unknown ->
  990        	retract('$aleph_sat_terms'(TNo,Depth1,Term,Type)),
  991		asserta('$aleph_sat_terms'(TNo,Depth,Term,Type));
  992		true).
  993integrate_term(_,Term/Type):-
  994        '$aleph_sat_terms'(_,_,Term,Type),
  995        Type \= unknown,
  996        !.
  997integrate_term(Depth,Term/Type):-
  998	retract('$aleph_sat'(lastterm,Num)),
  999	retract('$aleph_sat'(lastvar,Var0)),
 1000	TNo is Num + 1,
 1001	Var is Var0 + 1,
 1002	asserta('$aleph_sat'(lastterm,TNo)),
 1003	asserta('$aleph_sat'(lastvar,Var)),
 1004	asserta('$aleph_sat_vars'(Var,TNo,[],[])),
 1005	asserta('$aleph_sat_terms'(TNo,Depth,Term,Type)).
 1006
 1007
 1008%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1009
 1010% split_args(+Lit,?Mode,-Input,-Output,-Constants)
 1011%       return term-places and types of +,-, and # args in Lit
 1012%       by finding a matching mode declaration if Mode is given
 1013%       otherwise first mode that matches is used
 1014split_args(Lit,Mode,Input,Output,Constants):-
 1015        functor(Lit,Psym,Arity),
 1016	find_mode(mode,Psym/Arity,Mode),
 1017        functor(Template,Psym,Arity),
 1018	copy_modeterms(Mode,Template,Arity),
 1019	Template = Lit,
 1020	tp(Mode,TPList),
 1021	split_tp(TPList,Input,Output,Constants).
 1022
 1023% split_tp(+TPList,-Input,-Output,-Constants)
 1024%	split term-place/type list into +,-,#
 1025split_tp([],[],[],[]).
 1026split_tp([(+Type)/Place|TP],[Place/Type|Input],Output,Constants):-
 1027	!,
 1028	split_tp(TP,Input,Output,Constants).
 1029split_tp([(-Type)/Place|TP],Input,[Place/Type|Output],Constants):-
 1030	!,
 1031	split_tp(TP,Input,Output,Constants).
 1032split_tp([(#Type)/Place|TP],Input,Output,[Place/Type|Constants]):-
 1033	!,
 1034	split_tp(TP,Input,Output,Constants).
 1035split_tp([_|TP],Input,Output,Constants):-
 1036	split_tp(TP,Input,Output,Constants).
 1037
 1038% tp(+Literal,-TPList)
 1039%	return terms and places in Literal
 1040tp(Literal,TPList):-
 1041	functor(Literal,_,Arity),
 1042	tp_list(Literal,Arity,[],[],TPList).
 1043
 1044tp_list(_,0,_,L,L):- !.
 1045tp_list(Term,Pos,PlaceList,TpSoFar,TpList):-
 1046	arg(Pos,Term,Arg),
 1047	aleph_append([Pos],PlaceList,Places),
 1048	unwrap_term(Arg,Places,[Arg/Places|TpSoFar],L1),
 1049	Pos1 is Pos - 1,
 1050	tp_list(Term,Pos1,PlaceList,L1,TpList).
 1051
 1052unwrap_term(Term,_,L,L):-
 1053	var(Term), !.
 1054unwrap_term(Term,Place,TpSoFar,TpList):-
 1055	functor(Term,_,Arity),
 1056	tp_list(Term,Arity,Place,TpSoFar,TpList).
 1057
 1058get_determs(PSym/Arity,L):-
 1059	findall(Pred,'$aleph_global'(determination,determination(PSym/Arity,Pred)),L).
 1060
 1061get_modes(PSym/Arity,L):-
 1062	functor(Lit,PSym,Arity),
 1063	findall(Lit,'$aleph_global'(mode,mode(_,Lit)),L).
 1064
 1065
 1066%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1067% S E A R C H
 1068
 1069% basic search engine for single clause search
 1070search(S,Nodes):-
 1071	arg(36,S,Time),
 1072	Inf is inf,
 1073	Time =\= Inf, 
 1074	SearchTime is integer(Time),
 1075	SearchTime > 0, !,
 1076	catch(time_bound_call(SearchTime,searchlimit,graphsearch(S,_)),
 1077		searchlimit,p_message('Time limit reached')),
 1078	'$aleph_search'(current,current(_,Nodes,_)).
 1079search(S,Nodes):-
 1080	graphsearch(S,Nodes).
 1081
 1082% basic search engine for theory-based search
 1083tsearch(S,Nodes):-
 1084        arg(36,S,Time),
 1085	Inf is inf,
 1086        Time =\= Inf,
 1087        SearchTime is integer(Time),
 1088        SearchTime > 0, !,
 1089	alarm(SearchTime,throw(searchlimit),Id),
 1090        catch(theorysearch(S,Nodes),searchlimit,p_message('Time limit reached')),
 1091	remove_alarm(Id).
 1092tsearch(S,Nodes):-
 1093        theorysearch(S,Nodes).
 1094
 1095graphsearch(S,Nodes):-
 1096	next_node(_), !,
 1097        arg(3,S,RefineOp),
 1098	arg(23,S,LazyPreds),
 1099        repeat,
 1100	next_node(NodeRef),
 1101        once(retract('$aleph_search'(current,current(LastE,Last,BestSoFar)))),
 1102        expand(RefineOp,S,NodeRef,Node,Path,MinLength,Succ,PosCover,NegCover,OVars,
 1103		PrefixClause,PrefixTV,PrefixLength),
 1104        ((LazyPreds = []; RefineOp \= false)  -> Succ1 = Succ;
 1105		lazy_evaluate(Succ,LazyPreds,Path,PosCover,NegCover,Succ1)),
 1106	NextE is LastE + 1,
 1107        get_gains(S,Last,BestSoFar,Path,PrefixClause,PrefixTV,PrefixLength,
 1108                MinLength,Succ1,PosCover,NegCover,OVars,NextE,Last0,NextBest0),
 1109	(RefineOp = false ->
 1110        	get_sibgains(S,Node,Last0,NextBest0,Path,PrefixClause,
 1111			PrefixTV,PrefixLength,MinLength,PosCover,NegCover,
 1112			OVars,NextE,Last1,NextBest);
 1113		Last1 = Last0, NextBest = NextBest0),
 1114        asserta('$aleph_search'(current,current(NextE,Last1,NextBest))),
 1115        NextL is Last + 1,
 1116        asserta('$aleph_search_expansion'(NextE,Node,NextL,Last1)),
 1117        (discontinue_search(S,NextBest,Last1) ->
 1118                '$aleph_search'(current,current(_,Nodes,_));
 1119                prune_open(S,BestSoFar,NextBest),
 1120                get_nextbest(S,Next),
 1121		Next = none,
 1122		'$aleph_search'(current,current(_,Nodes,_))),
 1123	!.
 1124graphsearch(_,Nodes):-
 1125	'$aleph_search'(current,current(_,Nodes,_)).
 1126
 1127theorysearch(S,Nodes):-
 1128        next_node(_), !,
 1129        '$aleph_global'(atoms,atoms(pos,Pos)),
 1130        '$aleph_global'(atoms,atoms(neg,Neg)),
 1131        interval_count(Pos,P),
 1132        interval_count(Neg,N),
 1133        repeat,
 1134        next_node(NodeRef),
 1135	'$aleph_search_node'(NodeRef,Theory,_,_,_,_,_,_),
 1136        once(retract('$aleph_search'(current,current(_,Last,BestSoFar)))),
 1137        get_theory_gain(S,Last,BestSoFar,Theory,Pos,Neg,P,N,NextBest,Last1),
 1138        asserta('$aleph_search'(current,current(0,Last1,NextBest))),
 1139        (discontinue_search(S,NextBest,Last1) ->
 1140                '$aleph_search'(current,current(_,Nodes,_));
 1141                prune_open(S,BestSoFar,NextBest),
 1142                get_nextbest(S,Next),
 1143                Next = none,
 1144                '$aleph_search'(current,current(_,Nodes,_))),
 1145	 !.
 1146theorysearch(_,Nodes):-
 1147        '$aleph_search'(current,current(_,Nodes,_)).
 1148
 1149next_node(NodeRef):-
 1150	once('$aleph_search'(nextnode,NodeRef)), !.
 1151
 1152get_search_settings(S):-
 1153        functor(S,set,47),
 1154	setting(nodes,MaxNodes), arg(1,S,MaxNodes),
 1155	setting(explore,Explore), arg(2,S,Explore),
 1156	setting(refineop,RefineOp), arg(3,S,RefineOp),
 1157	setting(searchstrat,SearchStrat), setting(evalfn,EvalFn),
 1158	arg(4,S,SearchStrat/EvalFn),
 1159	(setting(greedy,Greedy)-> arg(5,S,Greedy); arg(5,S,false)),
 1160	setting(verbosity,Verbose), arg(6,S,Verbose),
 1161	setting(clauselength,CLength), arg(7,S,CLength),
 1162	setting(caching,Cache), arg(8,S,Cache),
 1163	(setting(prune_defs,Prune)-> arg(9,S,Prune); arg(9,S,false)),
 1164	setting(lazy_on_cost,LCost), arg(10,S,LCost),
 1165	setting(lazy_on_contradiction,LContra), arg(11,S,LContra),
 1166	setting(lazy_negs,LNegs), arg(12,S,LNegs),
 1167	setting(minpos,MinPos), arg(13,S,MinPos),
 1168	setting(depth,Depth), arg(14,S,Depth),
 1169	setting(cache_clauselength,CCLim), arg(15,S,CCLim),
 1170        ('$aleph_global'(size,size(pos,PSize))-> arg(16,S,PSize); arg(16,S,0)),
 1171	setting(noise,Noise), arg(17,S,Noise),
 1172	setting(minacc,MinAcc), arg(18,S,MinAcc),
 1173	setting(minscore,MinScore), arg(19,S,MinScore),
 1174        ('$aleph_global'(size,size(rand,RSize))-> arg(20,S,RSize); arg(20,S,0)),
 1175	setting(mingain,MinGain), arg(21,S,MinGain),
 1176	setting(search,Search), arg(22,S,Search),
 1177	findall(PN/PA,'$aleph_global'(lazy_evaluate,lazy_evaluate(PN/PA)),LazyPreds),
 1178	arg(23,S,LazyPreds),
 1179        ('$aleph_global'(size,size(neg,NSize))-> arg(24,S,NSize); arg(24,S,0)),
 1180	setting(openlist,OSize), arg(25,S,OSize),
 1181        setting(check_redundant,RCheck), arg(26,S,RCheck),
 1182        ('$aleph_sat'(eq,Eq) -> arg(27,S,Eq); arg(27,S,false)),
 1183        ('$aleph_sat'(hovars,HOVars) -> arg(28,S,HOVars); arg(28,S,_HOVars)),
 1184	setting(prooftime,PTime), arg(29,S,PTime),
 1185	setting(construct_bottom,CBott), arg(30,S,CBott),
 1186	(get_ovars1(false,1,HIVars) ->  arg(31,S,HIVars); arg(31,S,[])),
 1187	setting(language,Lang), arg(32,S,Lang),
 1188	setting(splitvars,Split), arg(33,S,Split),
 1189	setting(proof_strategy,Proof), arg(34,S,Proof),
 1190	setting(portray_search,VSearch), arg(35,S,VSearch),
 1191	setting(searchtime,Time), arg(36,S,Time),
 1192	setting(optimise_clauses,Optim), arg(37,S,Optim),
 1193	setting(newvars,NewV), arg(38,S,NewV),
 1194	(setting(rls_type,RlsType) -> arg(39,S,RlsType);arg(39,S,false)),
 1195	setting(minposfrac,MinPosFrac), arg(40,S,MinPosFrac),
 1196	(setting(recursion,_Recursion) -> true; _Recursion = false),
 1197	prolog_type(Prolog), arg(41,S,Prolog),
 1198	setting(interactive,Interactive), arg(42,S,Interactive),
 1199	setting(lookahead,LookAhead), arg(43,S,LookAhead),
 1200	(setting(construct_features,Features)-> arg(44,S,Features); arg(44,S,false)),
 1201	setting(max_features,FMax), arg(45,S,FMax),
 1202	setting(subsample,SS), arg(46,S,SS),
 1203	setting(subsamplesize,SSize), arg(47,S,SSize).
 1204
 1205% stop search from proceeding if certain
 1206% conditions are reached. These are:
 1207%	. minacc and minpos values reached in rrr search
 1208%	. best hypothesis has accuracy 1.0 if evalfn=accuracy
 1209%	. best hypothesis covers all positive examples
 1210discontinue_search(S,[P,_,_,F|_]/_,_):-
 1211	arg(39,S,RlsType),
 1212	RlsType = rrr, 
 1213	arg(13,S,MinPos),
 1214	P >= MinPos,
 1215	arg(19,S,MinScore),
 1216	F >= MinScore, !.
 1217discontinue_search(S,_,Nodes):-
 1218        arg(1,S,MaxNodes),
 1219        Nodes >= MaxNodes, !,
 1220	p_message('node limit reached').
 1221discontinue_search(S,_,_):-
 1222        arg(44,S,Features),
 1223	Features = true,
 1224	arg(45,S,FMax),
 1225	'$aleph_search'(last_good,LastGood),
 1226        LastGood >= FMax, !,
 1227	p_message('feature limit reached').
 1228discontinue_search(S,[_,_,_,F|_]/_,_):-
 1229        arg(4,S,_/Evalfn),
 1230	Evalfn = accuracy,
 1231	F = 1.0, !.
 1232discontinue_search(S,Best,_):-
 1233	arg(2,S,Explore),
 1234	Explore = false,
 1235        arg(4,S,_/Evalfn),
 1236	Evalfn \= user,
 1237	Evalfn \= posonly,
 1238	arg(22,S,Search),
 1239	Search \= ic,
 1240	Best = [P|_]/_,
 1241	arg(16,S,P).
 1242
 1243update_max_head_count(N,0):-
 1244	retractall('$aleph_local'(max_head_count,_)),
 1245	asserta('$aleph_local'(max_head_count,N)), !.
 1246update_max_head_count(Count,Last):-
 1247	'$aleph_search_node'(Last,LitNum,_,_,PosCover,_,_,_), !,
 1248	asserta('$aleph_local'(head_lit,LitNum)),
 1249	interval_count(PosCover,N),
 1250	Next is Last - 1,
 1251	(N > Count -> update_max_head_count(N,Next);
 1252		update_max_head_count(Count,Next)).
 1253update_max_head_count(Count,Last):-
 1254	Next is Last - 1,
 1255	update_max_head_count(Count,Next).
 1256
 1257expand(false,S,NodeRef,NodeRef,Path1,Length,Descendents,PosCover,NegCover,OVars,C,TV,CL):-
 1258	!,
 1259        '$aleph_search_node'(NodeRef,LitNum,Path,Length/_,PCover,NCover,OVars,_),
 1260	arg(46,S,SSample),
 1261	(SSample = false -> PosCover = PCover, NegCover = NCover;
 1262		get_sample_cover(S,PosCover,NegCover)),
 1263        aleph_append([LitNum],Path,Path1),
 1264	get_pclause(Path1,[],C,TV,CL,_),
 1265        '$aleph_sat_litinfo'(LitNum,_,_,_,_,Dependents),
 1266        intersect1(Dependents,Path1,_,Succ),
 1267        check_parents(Succ,OVars,Descendents,_).
 1268expand(_,S,NodeRef,NodeRef,Path1,Length,[_],PosCover,NegCover,OVars,_,_,_):-
 1269        retract('$aleph_search_node'(NodeRef,_,Path1,Length/_,_,_,OVars,_)),
 1270	get_sample_cover(S,PosCover,NegCover).
 1271
 1272get_sample_cover(S,PosCover,NegCover):-
 1273        arg(5,S,Greedy),
 1274        (Greedy = true ->
 1275                '$aleph_global'(atoms_left,atoms_left(pos,PCover));
 1276                arg(16,S,PSize),
 1277                PCover = [1-PSize]),
 1278        arg(4,S,_/Evalfn),
 1279	(Evalfn = posonly -> 
 1280                '$aleph_global'(atoms_left,atoms_left(rand,NCover));
 1281                arg(24,S,NSize),
 1282                NCover = [1-NSize]),
 1283	arg(46,S,SSample),
 1284	(SSample = false -> PosCover = PCover, NegCover = NCover;
 1285		arg(47,S,SampleSize),
 1286		interval_sample(SampleSize,PCover,PosCover),
 1287		interval_sample(SampleSize,NCover,NegCover)).
 1288
 1289get_ovars([],_,V,V).
 1290get_ovars([LitNum|Lits],K,VarsSoFar,Vars):-
 1291	get_ovars1(K,LitNum,OVars),
 1292	aleph_append(VarsSoFar,OVars,Vars1),
 1293	get_ovars(Lits,K,Vars1,Vars).
 1294
 1295get_ovars1(false,LitNum,OVars):-
 1296	'$aleph_sat_ovars'(LitNum,OVars), !.
 1297get_ovars1(false,LitNum,OVars):-
 1298	!,
 1299	'$aleph_sat_litinfo'(LitNum,_,Atom,_,O,_),
 1300	get_vars(Atom,O,OVars).
 1301get_ovars1(K,LitNum,OVars):-
 1302	'$aleph_sat_ovars'(LitNum,K,OVars), !.
 1303get_ovars1(K,LitNum,OVars):-
 1304	'$aleph_sat_litinfo'(LitNum,K,_,Atom,_,O,_),
 1305	get_vars(Atom,O,OVars).
 1306
 1307% get set of vars at term-places specified
 1308get_vars(not(Literal),Args,Vars):-
 1309	!,
 1310	get_vars(Literal,Args,Vars).
 1311get_vars(_,[],[]).
 1312get_vars(Literal,[ArgNo|Args],Vars):-
 1313	(ArgNo = Pos/_ -> true; Pos = ArgNo),
 1314	tparg(Pos,Literal,Term),
 1315	get_vars_in_term([Term],TV1),
 1316	get_vars(Literal,Args,TV2),
 1317	update_list(TV2,TV1,Vars).
 1318
 1319get_vars_in_term([],[]).
 1320get_vars_in_term([Var|Terms],[Var|TVars]):-
 1321	integer(Var), !,
 1322	get_vars_in_term(Terms,TVars).
 1323get_vars_in_term([Term|Terms],TVars):-
 1324	Term =.. [_|Terms1],
 1325	get_vars_in_term(Terms1,TV1),
 1326	get_vars_in_term(Terms,TV2),
 1327	update_list(TV2,TV1,TVars).
 1328
 1329% get terms at term-places specified
 1330% need not be variables
 1331get_argterms(not(Literal),Args,TermsSoFar,Terms):-
 1332        !,
 1333        get_argterms(Literal,Args,TermsSoFar,Terms).
 1334get_argterms(_,[],Terms,Terms).
 1335get_argterms(Literal,[ArgNo|Args],TermsSoFar,Terms):-
 1336	(ArgNo = Pos/_ -> true; Pos = ArgNo),
 1337        tparg(Pos,Literal,Term),
 1338        update(TermsSoFar,Term,T1),
 1339        get_argterms(Literal,Args,T1,Terms).
 1340
 1341% get list of terms at arg positions specified
 1342get_args(not(Literal),Args,TermsSoFar,Terms):-
 1343        !,
 1344        get_args(Literal,Args,TermsSoFar,Terms).
 1345get_args(_,[],Terms,Terms).
 1346get_args(Literal,[ArgNo|Args],TermsSoFar,Terms):-
 1347	(ArgNo = Pos/_ -> true; Pos = ArgNo),
 1348        tparg(Pos,Literal,Term),
 1349        get_args(Literal,Args,[Term|TermsSoFar],Terms).
 1350
 1351
 1352get_ivars([],_,V,V).
 1353get_ivars([LitNum|Lits],K,VarsSoFar,Vars):-
 1354	get_ivars1(K,LitNum,IVars),
 1355	aleph_append(VarsSoFar,IVars,Vars1),
 1356	get_ivars(Lits,K,Vars1,Vars).
 1357
 1358get_ivars1(false,LitNum,IVars):-
 1359	'$aleph_sat_ivars'(LitNum,IVars), !.
 1360get_ivars1(false,LitNum,IVars):-
 1361	!,
 1362	'$aleph_sat_litinfo'(LitNum,_,Atom,I,_,_),
 1363	get_vars(Atom,I,IVars).
 1364get_ivars1(K,LitNum,IVars):-
 1365	'$aleph_sat_ivars'(LitNum,K,IVars), !.
 1366get_ivars1(K,LitNum,IVars):-
 1367	'$aleph_sat_litinfo'(LitNum,K,_,Atom,I,_,_),
 1368	get_vars(Atom,I,IVars).
 1369
 1370check_parents([],_,[],[]).
 1371check_parents([LitNum|Lits],OutputVars,[LitNum|DLits],Rest):-
 1372	get_ivars1(false,LitNum,IVars),
 1373	aleph_subset1(IVars,OutputVars), !,
 1374	check_parents(Lits,OutputVars,DLits,Rest).
 1375check_parents([LitNum|Lits],OutputVars,DLits,[LitNum|Rest]):-
 1376	check_parents(Lits,OutputVars,DLits,Rest), !.
 1377
 1378get_gains(S,Last,Best,_,_,_,_,_,_,_,_,_,_,Last,Best):-
 1379        discontinue_search(S,Best,Last), !.
 1380get_gains(_,Last,Best,_,_,_,_,_,[],_,_,_,_,Last,Best):- !.
 1381get_gains(S,Last,Best,Path,C,TV,L,Min,[L1|Succ],Pos,Neg,OVars,E,Last1,NextBest):-
 1382        get_gain(S,upper,Last,Best,Path,C,TV,L,Min,L1,Pos,Neg,OVars,E,Best1,Node1), !,
 1383        get_gains(S,Node1,Best1,Path,C,TV,L,Min,Succ,Pos,Neg,OVars,E,Last1,NextBest).
 1384get_gains(S,Last,BestSoFar,Path,C,TV,L,Min,[_|Succ],Pos,Neg,OVars,E,Last1,NextBest):-
 1385        get_gains(S,Last,BestSoFar,Path,C,TV,L,Min,Succ,Pos,Neg,OVars,E,Last1,NextBest),
 1386        !.
 1387
 1388get_sibgains(S,Node,Last,Best,Path,C,TV,L,Min,Pos,Neg,OVars,E,Last1,NextBest):-
 1389        '$aleph_search_node'(Node,LitNum,_,_,_,_,_,OldE),
 1390        '$aleph_search_expansion'(OldE,_,_,LastSib),
 1391        '$aleph_sat_litinfo'(LitNum,_,_,_,_,Desc),
 1392        Node1 is Node + 1,
 1393        arg(31,S,HIVars),
 1394        aleph_delete_list(HIVars,OVars,LVars),
 1395        get_sibgain(S,LVars,LitNum,Desc,Node1,LastSib,Last,
 1396                Best,Path,C,TV,L,Min,Pos,Neg,OVars,E,NextBest,Last1), !.
 1397
 1398get_sibgain(S,_,_,_,Node,Node1,Last,Best,_,_,_,_,_,_,_,_,_,Best,Last):-
 1399        (Node > Node1;
 1400        discontinue_search(S,Best,Last)), !.
 1401get_sibgain(S,LVars,LitNum,Desc,Node,LastSib,Last,Best,Path,C,TV,L,Min,Pos,Neg,OVars,E,LBest,LNode):-
 1402        arg(23,S,Lazy),
 1403        get_sibpncover(Lazy,Node,Desc,Pos,Neg,Sib1,PC,NC),
 1404        lazy_evaluate([Sib1],Lazy,Path,PC,NC,[Sib]),
 1405        get_ivars1(false,Sib,SibIVars),
 1406        (intersects(SibIVars,LVars) -> Flag = upper;
 1407                get_ovars1(false,Sib,SibOVars),
 1408                (intersects(SibOVars,LVars) -> Flag = upper; Flag = exact)),
 1409        get_gain(S,Flag,Last,Best,Path,C,TV,L,Min,Sib,PC,NC,OVars,E,Best1,Node1), !,
 1410        NextNode is Node + 1,
 1411        get_sibgain(S,LVars,LitNum,Desc,NextNode,LastSib,Node1,Best1,Path,C,TV,L,
 1412                        Min,Pos,Neg,OVars,E,LBest,LNode), !.
 1413get_sibgain(S,LVars,LitNum,Desc,Node,LastSib,Last,Best,Path,C,TV,L,Min,Pos,Neg,OVars,E,Best1,Node1):-
 1414	NextNode is Node + 1,
 1415        get_sibgain(S,LVars,LitNum,Desc,NextNode,LastSib,Last,Best,Path,C,TV,L,
 1416                        Min,Pos,Neg,OVars,E,Best1,Node1), !.
 1417
 1418
 1419get_sibgain(S,LVars,LitNum,Node,LastSib,Last,Best,Path,C,TV,L,Min,Pos,Neg,OVars,E,Best1,Node1):-
 1420	NextNode is Node + 1,
 1421	get_sibgain(S,LVars,LitNum,NextNode,LastSib,Last,Best,Path,C,TV,L,Min,Pos,Neg,
 1422			OVars,E,Best1,Node1), !.
 1423
 1424get_sibpncover(Lazy,NodeNum,Desc,Pos,Neg,Sib,PC,NC):-
 1425        '$aleph_search_node'(NodeNum,Sib,_,_,Pos1,Neg1,_,_),
 1426        '$aleph_sat_litinfo'(Sib,_,Atom,_,_,_),
 1427        \+(aleph_member1(Sib,Desc)),
 1428        functor(Atom,Name,Arity),
 1429        (aleph_member1(Name/Arity,Lazy) ->
 1430                PC = Pos, NC = Neg;
 1431                calc_intersection(Pos,Pos1,PC),
 1432                calc_intersection(Neg,Neg1,NC)).
 1433
 1434% in some cases, it is possible to simply use the intersection of
 1435% covers cached. The conditions under which this is possible was developed
 1436% in discussions with James Cussens
 1437calc_intersection(A1/[B1-L1],A2/[B2-L2],A/[B-L]):-
 1438	!,
 1439	intervals_intersection(A1,A2,A),
 1440	B3 is max(B1,B2),
 1441	(intervals_intersects(A1,[B2-L2],X3-_) -> true; X3 = B3),
 1442	(intervals_intersects(A2,[B1-L1],X4-_) -> true; X4 = B3),
 1443	B4 is min(X3,B3),
 1444	B is min(X4,B4),
 1445	L is max(L1,L2).
 1446calc_intersection(A1/_,A2,A):-
 1447	!,
 1448	intervals_intersection(A1,A2,A).
 1449calc_intersection(A1,A2/_,A):-
 1450	!,
 1451	intervals_intersection(A1,A2,A).
 1452calc_intersection(A1,A2,A):-
 1453	intervals_intersection(A1,A2,A).
 1454
 1455get_gain(S,_,Last,Best,Path,_,_,_,MinLength,_,Pos,Neg,OVars,E,Best1,NewLast):-
 1456        arg(3,S,RefineOp),
 1457        RefineOp \= false , !,
 1458	get_refine_gain(S,Last,Best,Path,MinLength,Pos,Neg,OVars,E,Best1,NewLast).
 1459get_gain(S,Flag,Last,Best/Node,Path,C,TV,Len1,MinLen,L1,Pos,Neg,OVars,E,Best1,Last1):-
 1460	arg(26,S,RCheck),
 1461	arg(33,S,SplitVars),
 1462	retractall('$aleph_search'(covers,_)),
 1463	retractall('$aleph_search'(coversn,_)),
 1464        get_pclause([L1],TV,Lit1,_,Len2,LastD),
 1465	split_ok(SplitVars,C,Lit1), !,
 1466        extend_clause(C,Lit1,Clause),
 1467	(RCheck = true ->
 1468		(redundant(Clause,Lit1) -> fail; true);
 1469		true),
 1470        CLen is Len1 + Len2,
 1471        length_ok(S,MinLen,CLen,LastD,EMin,ELength),
 1472	% arg(41,S,Prolog),
 1473        split_clause(Clause,Head,Body),
 1474        % (Prolog = yap ->
 1475		% assertz('$aleph_search'(pclause,pclause(Head,Body)),DbRef);
 1476		% assertz('$aleph_search'(pclause,pclause(Head,Body)))),
 1477	assertz('$aleph_search'(pclause,pclause(Head,Body))),
 1478        arg(6,S,Verbosity),
 1479        (Verbosity >= 1 ->
 1480		pp_dclause(Clause);
 1481	true),
 1482        get_gain1(S,Flag,Clause,CLen,EMin/ELength,Last,Best/Node,
 1483                        Path,L1,Pos,Neg,OVars,E,Best1),
 1484        % (Prolog = yap ->
 1485		% erase(DbRef);
 1486		% retractall('$aleph_search'(pclause,_))),
 1487	retractall('$aleph_search'(pclause,_)),
 1488        Last1 is Last + 1.
 1489get_gain(_,_,Last,Best,_,_,_,_,_,_,_,_,_,_,Best,Last).
 1490
 1491get_refine_gain(S,Last,Best/Node,Path,MinLength,Pos,Neg,OVars,E,Best1,NewLast):-
 1492        arg(3,S,RefineOp),
 1493	RefineOp = rls,
 1494	refine_prelims(Best/Node,Last),
 1495	rls_refine(clauses,Path,Path1),
 1496	get_refine_gain1(S,Path1,MinLength,Pos,Neg,OVars,E,Best1,NewLast),
 1497	!.
 1498get_refine_gain(S,Last,Best/Node,Path,MinLength,Pos,Neg,OVars,E,Best1,NewLast):-
 1499        arg(3,S,RefineOp),
 1500	RefineOp \= rls,
 1501	refine_prelims(Best/Node,Last),
 1502	Path = CL-[Example,Type,_,Clause],
 1503	arg(30,S,ConstructBottom),
 1504        arg(43,S,LookAhead),
 1505        get_user_refinement(RefineOp,LookAhead,Clause,R,_),
 1506	match_bot(ConstructBottom,R,R1,LitNums),
 1507	Path1 = CL-[Example,Type,LitNums,R1],
 1508	get_refine_gain1(S,Path1,MinLength,Pos,Neg,OVars,E,Best1,NewLast),
 1509	!.
 1510get_refine_gain(_,_,_,_,_,_,_,_,_,Best,Last):-
 1511	retract('$aleph_search'(best_refinement,best_refinement(Best))),
 1512	retract('$aleph_search'(last_refinement,last_refinement(Last))).
 1513
 1514get_theory_gain(S,Last,BestSoFar,T0,Pos,Neg,P,N,Best1,NewLast):-
 1515	refine_prelims(BestSoFar,Last),
 1516	arg(3,S,RefineOp),
 1517	(RefineOp = rls -> rls_refine(theories,T0,T1); fail),
 1518	arg(23,S,LazyPreds),
 1519	(LazyPreds = [] -> Theory = T1;
 1520		lazy_evaluate_theory(T1,LazyPreds,Pos,Neg,Theory)),
 1521	retract('$aleph_search'(best_refinement,best_refinement(OldBest))),
 1522	retract('$aleph_search'(last_refinement,last_refinement(OldLast))),
 1523        arg(6,S,Verbosity),
 1524        (Verbosity >= 1 ->
 1525                p_message('new refinement'),
 1526                pp_dclauses(Theory);
 1527        true),
 1528	record_pclauses(Theory),
 1529	get_theory_gain1(S,Theory,OldLast,OldBest,Pos,Neg,P,N,Best1),
 1530	retractall('$aleph_search'(pclause,_)),
 1531        NewLast is OldLast + 1,
 1532	asserta('$aleph_search'(last_refinement,last_refinement(NewLast))),
 1533        asserta('$aleph_search'(best_refinement,best_refinement(Best1))),
 1534	(discontinue_search(S,Best1,NewLast) ->
 1535		retract('$aleph_search'(last_refinement,last_refinement(_))),
 1536		retract('$aleph_search'(best_refinement,best_refinement(_)));
 1537		fail),
 1538	!.
 1539get_theory_gain(_,_,_,_,_,_,_,_,Best,Last):-
 1540	'$aleph_search'(best_refinement,best_refinement(Best)),
 1541	'$aleph_search'(last_refinement,last_refinement(Last)).
 1542
 1543refine_prelims(Best,Last):-
 1544	retractall('$aleph_search'(last_refinement,_)),
 1545	retractall('$aleph_search'(best_refinement,_)),
 1546        asserta('$aleph_search'(best_refinement,best_refinement(Best))),
 1547	asserta('$aleph_search'(last_refinement,last_refinement(Last))).
 1548
 1549get_refine_gain1(S,Path,MinLength,Pos,Neg,OVars,E,Best1,NewLast):-
 1550        arg(23,S,LazyPreds),
 1551	Path = CL-[Example,Type,Ids,Refine],
 1552	(LazyPreds = [] -> Ids1 = Ids, Clause = Refine;
 1553		lazy_evaluate_refinement(Ids,Refine,LazyPreds,Pos,Neg,Ids1,Clause)),
 1554	retractall('$aleph_search'(covers,_)),
 1555	retractall('$aleph_search'(coversn,_)),
 1556	Path1 = CL-[Example,Type,Ids1,Clause],
 1557	split_clause(Clause,Head,Body),
 1558	nlits(Body,CLength0),
 1559	CLength is CLength0 + 1,
 1560	length_ok(S,MinLength,CLength,0,EMin,ELength),
 1561	arg(41,S,Prolog),
 1562	split_clause(Clause,Head,Body),
 1563	(Prolog = yap ->
 1564		assertz('$aleph_search'(pclause,pclause(Head,Body)),DbRef);
 1565		assertz('$aleph_search'(pclause,pclause(Head,Body)))),
 1566	retract('$aleph_search'(best_refinement,best_refinement(OldBest))),
 1567	retract('$aleph_search'(last_refinement,last_refinement(OldLast))),
 1568        arg(6,S,Verbosity),
 1569        (Verbosity >= 1 ->
 1570		p_message('new refinement'),
 1571		pp_dclause(Clause);
 1572	true),
 1573	once(get_gain1(S,upper,Clause,CLength,EMin/ELength,OldLast,OldBest,
 1574		Path1,[],Pos,Neg,OVars,E,Best1)),
 1575	(Prolog = yap ->
 1576		erase(DbRef);
 1577		retractall('$aleph_search'(pclause,_))),
 1578	NewLast is OldLast + 1,
 1579	asserta('$aleph_search'(last_refinement,last_refinement(NewLast))),
 1580        asserta('$aleph_search'(best_refinement,best_refinement(Best1))),
 1581	(discontinue_search(S,Best1,NewLast) ->
 1582		retract('$aleph_search'(last_refinement,last_refinement(_))),
 1583		retract('$aleph_search'(best_refinement,best_refinement(_)));
 1584		fail),
 1585	!.
 1586
 1587get_theory_gain1(S,Theory,Last,Best,Pos,Neg,P,N,Best1):-
 1588        (false -> p_message('constraint violated'),
 1589                Contradiction = true;
 1590                Contradiction = false),
 1591	Contradiction = false,
 1592        Node1 is Last + 1,
 1593	arg(32,S,Lang),
 1594	theory_lang_ok(Theory,Lang),
 1595	arg(38,S,NewVars),
 1596	theory_newvars_ok(Theory,NewVars),
 1597	arg(14,S,Depth),
 1598	arg(29,S,Time),
 1599	arg(34,S,Proof),
 1600        prove(Depth/Time/Proof,pos,(X:-X),Pos,PCvr,TP),
 1601        prove(Depth/Time/Proof,neg,(X:-X),Neg,NCvr,FP),
 1602	arg(4,S,_/Evalfn),
 1603	Correct is TP + (N - FP),
 1604	Incorrect is FP + (P - TP),
 1605	length(Theory,L),
 1606	Label = [Correct,Incorrect,L],
 1607	complete_label(Evalfn,Theory,Label,Label1),
 1608	get_search_keys(heuristic,Label1,SearchKeys),
 1609	arg(6,S,Verbosity),
 1610	(Verbosity >= 1 -> p_message(Correct/Incorrect); true),
 1611	asserta('$aleph_search_node'(Node1,Theory,[],0,PCvr,NCvr,[],0)),
 1612	update_open_list(SearchKeys,Node1,Label1),
 1613	update_best_theory(S,Theory,PCvr,NCvr,Best,Label1/Node1,Best1), !.
 1614get_theory_gain1(_,_,_,Best,_,_,_,_,Best).
 1615
 1616get_gain1(S,_,C,CL,_,Last,Best,Path,_,Pos,Neg,_,E,Best):-
 1617        abandon_branch(S,C), !,
 1618        Node1 is Last + 1,
 1619        arg(3,S,RefineOp),
 1620        arg(7,S,ClauseLength),
 1621	arg(35,S,VSearch),
 1622        (ClauseLength = CL -> true;
 1623                (RefineOp = false  ->
 1624                        asserta('$aleph_search_node'(Node1,0,Path,0,Pos,Neg,[],E));
 1625			true)),
 1626	(VSearch = true ->
 1627		asserta('$aleph_search'(bad,Node1)),
 1628		asserta('$aleph_search_node'(Node1,C));
 1629		true).
 1630get_gain1(S,_,Clause,_,_,_,Best,_,_,_,_,_,_,Best):-
 1631        arg(8,S,Caching),
 1632        Caching = true,
 1633        skolemize(Clause,SHead,SBody,0,_),
 1634        '$aleph_search_prunecache'([SHead|SBody]), !,
 1635	arg(6,S,Verbosity),
 1636        (Verbosity >= 1 -> p_message('in prune cache'); true).
 1637get_gain1(S,Flag,C,CL,EMin/EL,Last,Best/Node,Path,L1,Pos,Neg,OVars,E,Best1):-
 1638	split_clause(C,Head,Body),
 1639	arg(22,S,Search),
 1640        ((Search \== ic, false) -> p_message('constraint violated'),
 1641                Contradiction = true;
 1642                Contradiction = false),
 1643        Node1 is Last + 1,
 1644        arg(8,S,Caching),
 1645        (Caching = true -> arg(15,S,CCLim),
 1646		get_cache_entry(CCLim,C,Entry);
 1647		Entry = false),
 1648	arg(35,S,VSearch),
 1649	(VSearch = true ->
 1650		asserta('$aleph_search_node'(Node1,C));
 1651		true),
 1652        arg(3,S,RefineOp),
 1653	refinement_ok(RefineOp,Entry),
 1654	arg(32,S,Lang),
 1655	lang_ok((Head:-Body),Lang),
 1656	arg(38,S,NewVars),
 1657	newvars_ok((Head:-Body),NewVars),
 1658	arg(34,S,Proof),
 1659	arg(37,S,Optim),
 1660	rewrite_clause(Proof,Optim,(Head:-Body),(Head1:-Body1)),
 1661	(Search = ic ->
 1662		PCvr = [],
 1663		Label = [_,_,CL],
 1664		ccheck(S,(Head1:-Body1),NCvr,Label);
 1665        	prove_examples(S,Flag,Contradiction,Entry,Best,CL,EL,
 1666				(Head1:-Body1),Pos,Neg,PCvr,NCvr,Label)
 1667	),
 1668        arg(4,S,SearchStrat/Evalfn),
 1669	arg(40,S,MinPosFrac),
 1670	((MinPosFrac > 0.0 ; Evalfn = wracc) ->
 1671		reset_clause_prior(S,Head1);
 1672		true
 1673	),
 1674	arg(46,S,SSample),
 1675	(SSample = true ->
 1676		arg(47,S,SampleSize),
 1677		estimate_label(SampleSize,Label,Label0);
 1678		Label0 = Label),
 1679	complete_label(Evalfn,C,Label0,Label1),
 1680	compression_ok(Evalfn,Label1),
 1681        get_search_keys(SearchStrat,Label1,SearchKeys),
 1682        arg(6,S,Verbosity),
 1683	arg(10,S,LCost),
 1684	arg(11,S,LContra),
 1685        ((Verbosity >= 1, LContra = false, LCost = false) ->
 1686		Label = [A,B|_],
 1687		p_message(A/B);
 1688	true),
 1689        arg(7,S,ClauseLength),
 1690	(RefineOp = false ->
 1691		get_ovars1(false,L1,OVars1),
 1692		aleph_append(OVars1,OVars,OVars2);
 1693		true),
 1694        ((ClauseLength=CL, RefineOp = false) -> true;
 1695		(RefineOp = false ->
 1696                	asserta('$aleph_search_node'(Node1,L1,Path,EMin/EL,PCvr,
 1697					NCvr,OVars2,E));
 1698                	asserta('$aleph_search_node'(Node1,0,Path,EMin/EL,PCvr,
 1699					NCvr,[],E))),
 1700                	update_open_list(SearchKeys,Node1,Label1)),
 1701	(VSearch = true ->
 1702		asserta('$aleph_search'(label,label(Node1,Label)));
 1703		true),
 1704        (((RefineOp \= false,Contradiction=false);
 1705		(arg(28,S,HOVars),clause_ok(Contradiction,HOVars,OVars2))) ->
 1706                update_best(S,C,PCvr,NCvr,Best/Node,Label1/Node1,Best1);
 1707                Best1=Best/Node),
 1708	!.
 1709get_gain1(_,_,_,_,_,_,Best,_,_,_,_,_,_,Best).
 1710
 1711
 1712abandon_branch(S,C):-
 1713        arg(9,S,PruneDefined),
 1714        PruneDefined = true,
 1715        prune(C), !,
 1716        arg(6,S,Verbosity),
 1717        (Verbosity >= 1 -> p_message(pruned); true).
 1718
 1719clause_ok(false,V1,V2):-
 1720        aleph_subset1(V1,V2).
 1721
 1722% check to see if a clause is acceptable
 1723% 	unacceptable if it fails noise, minacc, or minpos settings
 1724%	unacceptable if it fails search or language constraints
 1725clause_ok(_,_):-
 1726	false, !, fail.
 1727clause_ok(_,Label):-
 1728	extract_pos(Label,P),
 1729	extract_neg(Label,N),
 1730	Acc is P/(P+N),
 1731	setting(noise,Noise),
 1732	setting(minacc,MinAcc),
 1733	setting(minpos,MinPos),
 1734	(N > Noise; Acc < MinAcc; P < MinPos), !, fail.
 1735clause_ok(Clause,_):-
 1736	prune(Clause), !, fail.
 1737clause_ok(Clause,_):-
 1738	setting(language,Lang),
 1739	\+ lang_ok(Clause,Lang), !, fail.
 1740clause_ok(Clause,_):-
 1741	setting(newvars,NewVars),
 1742	\+ newvars_ok(Clause,NewVars), !, fail.
 1743clause_ok(_,_).
 1744
 1745% check to see if refinement has been produced before
 1746refinement_ok(false,_):- !.
 1747refinement_ok(rls,_):- !.
 1748refinement_ok(_,false):- !.
 1749refinement_ok(_,Entry):-
 1750	(check_cache(Entry,pos,_); check_cache(Entry,neg,_)), !,
 1751	p_message('redundant refinement'),
 1752	fail.
 1753refinement_ok(_,_).
 1754
 1755
 1756% specialised redundancy check with equality theory
 1757% used only to check if equalities introduced by splitting vars make
 1758% literal to be added redundant
 1759split_ok(false,_,_):- !.
 1760split_ok(_,Clause,Lit):-
 1761	functor(Lit,Name,_),
 1762	Name \= '=', 
 1763	copy_term(Clause/Lit,Clause1/Lit1),
 1764	lit_redun(Lit1,Clause1), !,
 1765	p_message('redundant literal'), nl,
 1766	fail.
 1767split_ok(_,_,_).
 1768
 1769lit_redun(Lit,(Head:-Body)):-
 1770	!,
 1771	lit_redun(Lit,(Head,Body)).
 1772lit_redun(Lit,(L1,_)):-
 1773	Lit == L1, !.
 1774lit_redun(Lit,(L1,L2)):-
 1775	!,
 1776	execute_equality(L1),
 1777	lit_redun(Lit,L2).
 1778lit_redun(Lit,L):-
 1779	Lit == L.
 1780
 1781execute_equality(Lit):-
 1782	functor(Lit,'=',2), !,
 1783	Lit.
 1784execute_equality(_).
 1785	
 1786theory_lang_ok([],_).
 1787theory_lang_ok([_-[_,_,_,Clause]|T],Lang):-
 1788        lang_ok(Lang,Clause),
 1789        theory_lang_ok(Lang,T). 
 1790
 1791theory_newvars_ok([],_).
 1792theory_newvars_ok([_-[_,_,_,Clause]|T],NewV):-
 1793        newvars_ok(NewV,Clause),
 1794        theory_newvars_ok(T,NewV). 
 1795
 1796lang_ok((Head:-Body),N):-
 1797	!,
 1798	(lang_ok(N,Head,Body) -> true;
 1799		p_message('outside language bound'),
 1800		fail).
 1801
 1802lang_ok(N,_,_):- N is inf, !.
 1803lang_ok(N,Head,Body):-
 1804	get_psyms((Head,Body),PSymList),
 1805	lang_ok1(PSymList,N).
 1806
 1807newvars_ok((Head:-Body),N):-
 1808	!,
 1809	(newvars_ok(N,Head,Body) -> true;
 1810		p_message('outside newvars bound'),
 1811		fail).
 1812
 1813newvars_ok(N,_,_):- N is inf, !.
 1814newvars_ok(N,Head,Body):-
 1815	vars_in_term([Head],[],HVars),
 1816	goals_to_list(Body,BodyL),
 1817	vars_in_term(BodyL,[],BVars),
 1818        aleph_ord_subtract(BVars,HVars,NewVars),
 1819	length(NewVars,N1),
 1820	N1 =< N.
 1821
 1822get_psyms((L,B),[N/A|Syms]):-
 1823	!,
 1824	functor(L,N,A),
 1825	get_psyms(B,Syms).
 1826get_psyms(true,[]):- !.
 1827get_psyms(L,[N/A]):-
 1828	functor(L,N,A).
 1829
 1830lang_ok1([],_).
 1831lang_ok1([Pred|Preds],N):-
 1832        length(Preds,N0),
 1833        aleph_delete_all(Pred,Preds,Preds1),
 1834        length(Preds1,N1),
 1835        PredOccurs is N0 - N1 + 1,
 1836	PredOccurs =< N,
 1837	lang_ok1(Preds1,N).
 1838
 1839rewrite_clause(sld,_,_,(X:-X)):- !.
 1840rewrite_clause(restricted_sld,true,(Head:-Body),(Head1:-Body1)):- 
 1841	!,
 1842        optimise((Head:-Body),(Head1:-Body1)).
 1843rewrite_clause(_,_,Clause,Clause).
 1844
 1845record_pclauses([]).
 1846record_pclauses([_-[_,_,_,Clause]|T]):-
 1847        split_clause(Clause,Head,Body),
 1848        assertz('$aleph_search'(pclause,pclause(Head,Body))),
 1849        record_pclauses(T).
 1850
 1851% get pos/neg distribution of clause head
 1852reset_clause_prior(S,Head):-
 1853	arg(3,S,Refine),
 1854	Refine = false, !,
 1855	('$aleph_search'(clauseprior,_) -> true;
 1856		get_clause_prior(S,Head,Prior),
 1857		assertz('$aleph_search'(clauseprior,Prior))
 1858	).
 1859reset_clause_prior(S,Head):-
 1860	copy_term(Head,Head1),
 1861	numbervars(Head1,0,_),
 1862	('$aleph_local'(clauseprior,prior(Head1,Prior)) ->
 1863		true;
 1864		get_clause_prior(S,Head,Prior),
 1865		assertz('$aleph_local'(clauseprior,prior(Head1,Prior)))
 1866	),
 1867	retractall('$aleph_search'(clauseprior,_)),
 1868	assertz('$aleph_search'(clauseprior,Prior)).
 1869
 1870get_clause_prior(S,Head,Total-[P-pos,N-neg]):-
 1871	arg(5,S,Greedy),
 1872	arg(14,S,Depth),
 1873	arg(29,S,Time),
 1874	arg(34,S,Proof),
 1875	(Greedy = true ->
 1876		'$aleph_global'(atoms_left,atoms_left(pos,Pos));
 1877		'$aleph_global'(atoms,atoms(pos,Pos))
 1878	),
 1879	'$aleph_global'(atoms_left,atoms_left(neg,Neg)),
 1880	prove(Depth/Time/Proof,pos,(Head:-true),Pos,_,P),
 1881	prove(Depth/Time/Proof,neg,(Head:-true),Neg,_,N),
 1882	Total is P + N.
 1883
 1884get_user_refinement(auto,L,Clause,Template,0):-
 1885        auto_refine(L,Clause,Template).
 1886get_user_refinement(user,_,Clause,Template,0):-
 1887        refine(Clause,Template).
 1888
 1889match_bot(false,Clause,Clause,[]).
 1890match_bot(reduction,Clause,Clause1,Lits):-
 1891	match_lazy_bottom(Clause,Lits),
 1892	get_pclause(Lits,[],Clause1,_,_,_).
 1893match_bot(saturation,Clause,Clause1,Lits):-
 1894	once(get_aleph_clause(Clause,AlephClause)),
 1895	match_bot_lits(AlephClause,[],Lits),
 1896	get_pclause(Lits,[],Clause1,_,_,_).
 1897
 1898match_bot_lits((Lit,Lits),SoFar,[LitNum|LitNums]):-
 1899	!,
 1900	match_bot_lit(Lit,LitNum),
 1901	\+(aleph_member(LitNum,SoFar)),
 1902	match_bot_lits(Lits,[LitNum|SoFar],LitNums).
 1903match_bot_lits(Lit,SoFar,[LitNum]):-
 1904	match_bot_lit(Lit,LitNum),
 1905	\+(aleph_member(LitNum,SoFar)).
 1906
 1907match_bot_lit(Lit,LitNum):-
 1908	'$aleph_sat'(botsize,Last),
 1909	'$aleph_sat_litinfo'(LitNum,_,Lit,_,_,_),
 1910	LitNum >= 0,
 1911	LitNum =< Last.
 1912
 1913match_lazy_bottom(Clause,Lits):-
 1914	once(get_aleph_clause(Clause,AlephClause)),
 1915	copy_term(Clause,CClause),
 1916	split_clause(CClause,CHead,CBody),
 1917	example_saturated(CHead),
 1918	store(stage),
 1919	set(stage,saturation),
 1920	match_lazy_bottom1(CBody),
 1921	reinstate(stage),
 1922	match_bot_lits(AlephClause,[],Lits).
 1923
 1924match_lazy_bottom1(Body):-
 1925	Body,
 1926	match_body_modes(Body),
 1927	fail.
 1928match_lazy_bottom1(_):-
 1929	flatten_matched_atoms(body).
 1930
 1931match_body_modes((CLit,CLits)):-
 1932        !,
 1933        match_mode(body,CLit),
 1934        match_body_modes(CLits).
 1935match_body_modes(CLit):-
 1936        match_mode(body,CLit).
 1937
 1938match_mode(_,true):- !.
 1939match_mode(Loc,CLit):-
 1940	functor(CLit,Name,Arity),
 1941        functor(Mode,Name,Arity),
 1942	(Loc=head ->
 1943		'$aleph_global'(modeh,modeh(_,Mode));
 1944		'$aleph_global'(modeb,modeb(_,Mode))),
 1945        split_args(Mode,Mode,I,O,C),
 1946        (Loc = head ->
 1947		update_atoms(CLit,mode(Mode,O,I,C));
 1948		update_atoms(CLit,mode(Mode,I,O,C))),
 1949	fail.
 1950match_mode(_,_).
 1951
 1952flatten_matched_atoms(Loc):-
 1953        setting(i,IVal),
 1954        (retract('$aleph_sat'(botsize,BSize))-> true;  BSize = 0),
 1955        (retract('$aleph_sat'(lastlit,Last))-> true ; Last = 0),
 1956        (Loc = head ->
 1957                flatten(0,IVal,BSize,BSize1);
 1958                flatten(0,IVal,Last,BSize1)),
 1959        asserta('$aleph_sat'(botsize,BSize1)),
 1960	(Last < BSize1 -> 
 1961        	asserta('$aleph_sat'(lastlit,BSize1));
 1962        	asserta('$aleph_sat'(lastlit,Last))), !.
 1963flatten_matched_atoms(_).
 1964
 1965% integrate head literal into lits database
 1966% used during lazy evaluation of bottom clause
 1967integrate_head_lit(HeadOVars):-
 1968        example_saturated(Example),
 1969	split_args(Example,_,_,Output,_),
 1970	integrate_args(unknown,Example,Output),
 1971        match_mode(head,Example),
 1972	flatten_matched_atoms(head),
 1973        get_ivars1(false,1,HeadOVars), !.
 1974integrate_head_lit([]).
 1975
 1976
 1977get_aleph_clause((Lit:-true),PLit):-
 1978	!,
 1979	get_aleph_lit(Lit,PLit).
 1980get_aleph_clause((Lit:-Lits),(PLit,PLits)):-
 1981	!,
 1982	get_aleph_lit(Lit,PLit),
 1983	get_aleph_lits(Lits,PLits).
 1984get_aleph_clause(Lit,PLit):-
 1985	get_aleph_lit(Lit,PLit).
 1986
 1987get_aleph_lits((Lit,Lits),(PLit,PLits)):-
 1988	!,
 1989	get_aleph_lit(Lit,PLit),
 1990	get_aleph_lits(Lits,PLits).
 1991get_aleph_lits(Lit,PLit):-
 1992	get_aleph_lit(Lit,PLit).
 1993
 1994get_aleph_lit(Lit,PLit):-
 1995	functor(Lit,Name,Arity),
 1996	functor(PLit,Name,Arity),
 1997	get_aleph_lit(Lit,PLit,Arity).
 1998
 1999get_aleph_lit(_,_,0):- !.
 2000get_aleph_lit(Lit,PLit,Arg):-
 2001	arg(Arg,Lit,Term),
 2002	(var(Term) -> arg(Arg,PLit,Term);arg(Arg,PLit,aleph_const(Term))),
 2003	NextArg is Arg - 1,
 2004	get_aleph_lit(Lit,PLit,NextArg), !.
 2005	
 2006% Claudien-style consistency checking as described by De Raedt and Dehaspe, 1996
 2007% currently does not retain actual substitutions that result in inconsistencies
 2008% also, only checks for constraints of the form false:- ...
 2009% this simplifies the check of Body,not(Head) to just Body
 2010ccheck(S,(false:-Body),[],[0,N|_]):-
 2011	(Body = true ->
 2012		N is inf;
 2013		arg(11,S,LContra),
 2014		(LContra = false -> 
 2015        		arg(14,S,Depth),
 2016        		arg(29,S,Time),
 2017			findall(X,(resource_bound_call(Time,Depth,Body),X=1),XL),
 2018			length(XL,N);
 2019			lazy_ccheck(S,Body,N)
 2020		)
 2021	).
 2022
 2023lazy_ccheck(S,Body,N):-
 2024        arg(14,S,Depth),
 2025        arg(17,S,Noise),
 2026        arg(29,S,Time),
 2027	retractall('$aleph_local'(subst_count,_)),
 2028	asserta('$aleph_local'(subst_count,0)),
 2029	resource_bound_call(Time,Depth,Body),
 2030	retract('$aleph_local'(subst_count,N0)),
 2031	N is N0 + 1,
 2032	N > Noise, !.
 2033lazy_ccheck(_,_,N):-
 2034	retract('$aleph_local'(subst_count,N)).
 2035
 2036% posonly formula as described by Muggleton, ILP-96
 2037prove_examples(S,Flag,Contradiction,Entry,Best,CL,L2,Clause,Pos,Rand,PCover,RCover,[P,B,CL,I,G]):-
 2038	arg(4,S,_/Evalfn),
 2039	Evalfn = posonly, !,
 2040        arg(11,S,LazyOnContra),
 2041        ((LazyOnContra = true, Contradiction = true) ->
 2042                prove_lazy_cached(S,Entry,Pos,Rand,PCover,RCover),
 2043                interval_count(PCover,_PC),
 2044                interval_count(RCover,RC);
 2045                prove_pos(S,Flag,Entry,Best,[PC,L2],Clause,Pos,PCover,PC),
 2046                prove_rand(S,Flag,Entry,Clause,Rand,RCover,RC)),
 2047        find_posgain(PCover,P),
 2048        arg(16,S,M), arg(20,S,N),
 2049        GC is (RC+1.0)/(N+2.0), % Laplace correction for small numbers
 2050        A is log(P),
 2051        B is log(GC),
 2052        G is GC*M/P,
 2053        C is CL/P,
 2054        % Sz is CL*M/P,
 2055        % D is M*G,
 2056        %  I is M - D - Sz,
 2057        I is A - B - C.
 2058prove_examples(S,_,_,Entry,_,CL,_,_,Pos,Neg,Pos,Neg,[PC,NC,CL]):-
 2059        arg(10,S,LazyOnCost),
 2060        LazyOnCost = true, !,
 2061        prove_lazy_cached(S,Entry,Pos,Neg,Pos1,Neg1),
 2062        interval_count(Pos1,PC),
 2063        interval_count(Neg1,NC).
 2064prove_examples(S,_,true,Entry,_,CL,_,_,Pos,Neg,Pos,Neg,[PC,NC,CL]):-
 2065        arg(11,S,LazyOnContra),
 2066        LazyOnContra = true, !,
 2067        prove_lazy_cached(S,Entry,Pos,Neg,Pos1,Neg1),
 2068        interval_count(Pos1,PC),
 2069        interval_count(Neg1,NC).
 2070prove_examples(S,Flag,_,Ent,Best,CL,L2,Clause,Pos,Neg,PCover,NCover,[PC,NC,CL]):-
 2071	arg(3,S,RefineOp),
 2072	(RefineOp = false; RefineOp = auto),
 2073        arg(7,S,ClauseLength),
 2074        ClauseLength = CL, !,
 2075	interval_count(Pos,MaxPCount),
 2076        prove_neg(S,Flag,Ent,Best,[MaxPCount,CL],Clause,Neg,NCover,NC),
 2077        arg(17,S,Noise), arg(18,S,MinAcc),
 2078        maxlength_neg_ok(Noise/MinAcc,Ent,MaxPCount,NC),
 2079        prove_pos(S,Flag,Ent,Best,[PC,L2],Clause,Pos,PCover,PC),
 2080        maxlength_neg_ok(Noise/MinAcc,Ent,PC,NC),
 2081	!.
 2082prove_examples(S,Flag,_,Ent,Best,CL,L2,Clause,Pos,Neg,PCover,NCover,[PC,NC,CL]):-
 2083        prove_pos(S,Flag,Ent,Best,[PC,L2],Clause,Pos,PCover,PC),
 2084        prove_neg(S,Flag,Ent,Best,[PC,CL],Clause,Neg,NCover,NC),
 2085	!.
 2086
 2087prove_lazy_cached(S,Entry,Pos,Neg,Pos1,Neg1):-
 2088        arg(8,S,Caching),
 2089	Caching = true, !,
 2090	(check_cache(Entry,pos,Pos1)->
 2091		true;
 2092		add_cache(Entry,pos,Pos),
 2093		Pos1 = Pos),
 2094	(check_cache(Entry,neg,Neg1)->
 2095		true;
 2096		add_cache(Entry,neg,Neg),
 2097		Neg1 = Neg).
 2098prove_lazy_cached(_,_,Pos,Neg,Pos,Neg).
 2099
 2100complete_label(posonly,_,L,L):- !.
 2101complete_label(user,Clause,[P,N,L],[P,N,L,Val]):-
 2102        cost(Clause,[P,N,L],Cost), !,
 2103	Val is -Cost.
 2104complete_label(entropy,_,[P,N,L],[P,N,L,Val]):-
 2105	evalfn(entropy,[P,N,L],Entropy),
 2106	Val is -Entropy, !.
 2107complete_label(gini,_,[P,N,L],[P,N,L,Val]):-
 2108	evalfn(gini,[P,N,L],Gini),
 2109	Val is -Gini, !.
 2110complete_label(EvalFn,_,[P,N,L],[P,N,L,Val]):-
 2111	evalfn(EvalFn,[P,N,L],Val), !.
 2112complete_label(_,_,_,_):-
 2113	p_message1('error'), p_message('incorrect evaluation/cost function'),
 2114	fail.
 2115
 2116% estimate label based on subsampling
 2117estimate_label(Sample,[P,N|Rest],[P1,N1|Rest]):-
 2118	'$aleph_global'(atoms_left,atoms_left(pos,Pos)),
 2119	'$aleph_global'(atoms_left,atoms_left(neg,Neg)),
 2120	interval_count(Pos,PC), interval_count(Neg,NC),
 2121	PFrac is P/Sample,
 2122	NFrac is N/Sample,
 2123	P1 is integer(PFrac*PC),
 2124	N1 is integer(NFrac*NC).
 2125
 2126% get primary and secondary search keys for search
 2127% use [Primary|Secondary] notation as it is the most compact
 2128get_search_keys(bf,[_,_,L,F|_],[L1|F]):-
 2129	!,
 2130	L1 is -1*L.
 2131get_search_keys(df,[_,_,L,F|_],[L|F]):- !.
 2132get_search_keys(_,[_,_,L,F|_],[F|L1]):-
 2133	L1 is -1*L.
 2134
 2135prove_pos(_,_,_,_,_,_,[],[],0):- !.
 2136prove_pos(S,_,Entry,BestSoFar,PosSoFar,Clause,_,PCover,PCount):-
 2137        '$aleph_search'(covers,covers(PCover,PCount)), !,
 2138        pos_ok(S,Entry,BestSoFar,PosSoFar,Clause,PCover).
 2139prove_pos(S,Flag,Entry,BestSoFar,PosSoFar,Clause,Pos,PCover,PCount):-
 2140        prove_cache(Flag,S,pos,Entry,Clause,Pos,PCover,PCount),
 2141        pos_ok(S,Entry,BestSoFar,PosSoFar,Clause,PCover), !.
 2142
 2143prove_neg(S,_,Entry,_,_,_,[],[],0):-
 2144	arg(8,S,Caching),
 2145	(Caching = true -> add_cache(Entry,neg,[]); true), !.
 2146prove_neg(S,Flag,Entry,_,_,Clause,Neg,NCover,NCount):-
 2147	arg(3,S,RefineOp),
 2148	RefineOp = rls,  !,
 2149        prove_cache(Flag,S,neg,Entry,Clause,Neg,NCover,NCount).
 2150prove_neg(_,_,_,_,_,_,_,NCover,NCount):-
 2151        '$aleph_search'(coversn,coversn(NCover,NCount)), !.
 2152prove_neg(S,Flag,Entry,BestSoFar,PosSoFar,Clause,Neg,NCover,NCount):-
 2153        arg(12,S,LazyNegs),
 2154        LazyNegs = true, !,
 2155        lazy_prove_neg(S,Flag,Entry,BestSoFar,PosSoFar,Clause,Neg,NCover,NCount).
 2156prove_neg(S,Flag,Entry,[P,0,L1|_],[P,L2],Clause,Neg,[],0):-
 2157	arg(4,S,bf/coverage),
 2158        L2 is L1 - 1,
 2159	!,
 2160        prove_cache(Flag,S,neg,Entry,Clause,Neg,0,[],0), !.
 2161prove_neg(S,Flag,Entry,[P,N|_],[P,L1],Clause,Neg,NCover,NCount):-
 2162	arg(4,S,bf/coverage),
 2163        !,
 2164        arg(7,S,ClauseLength),
 2165        (ClauseLength = L1 ->
 2166		arg(2,S,Explore),
 2167		(Explore = true -> MaxNegs is N; MaxNegs is N - 1),
 2168                MaxNegs >= 0,
 2169                prove_cache(Flag,S,neg,Entry,Clause,Neg,MaxNegs,NCover,NCount),
 2170		NCount =< MaxNegs;
 2171                prove_cache(Flag,S,neg,Entry,Clause,Neg,NCover,NCount)),
 2172        !.
 2173prove_neg(S,Flag,Entry,_,[P1,L1],Clause,Neg,NCover,NCount):-
 2174        arg(7,S,ClauseLength),
 2175        ClauseLength = L1,  !,
 2176        arg(17,S,Noise), arg(18,S,MinAcc),
 2177        get_max_negs(Noise/MinAcc,P1,N1),
 2178        prove_cache(Flag,S,neg,Entry,Clause,Neg,N1,NCover,NCount),
 2179	NCount =< N1,
 2180        !.
 2181prove_neg(S,Flag,Entry,_,_,Clause,Neg,NCover,NCount):-
 2182        prove_cache(Flag,S,neg,Entry,Clause,Neg,NCover,NCount),
 2183        !.
 2184
 2185prove_rand(S,Flag,Entry,Clause,Rand,RCover,RCount):-
 2186        prove_cache(Flag,S,rand,Entry,Clause,Rand,RCover,RCount),
 2187        !.
 2188
 2189lazy_prove_neg(S,Flag,Entry,[P,N|_],[P,_],Clause,Neg,NCover,NCount):-
 2190	arg(4,S,bf/coverage),
 2191        !,
 2192        MaxNegs is N + 1,
 2193        prove_cache(Flag,S,neg,Entry,Clause,Neg,MaxNegs,NCover,NCount),
 2194        !.
 2195lazy_prove_neg(S,Flag,Entry,_,[P1,_],Clause,Neg,NCover,NCount):-
 2196        arg(17,S,Noise), arg(18,S,MinAcc),
 2197        get_max_negs(Noise/MinAcc,P1,N1),
 2198        MaxNegs is N1 + 1,
 2199        prove_cache(Flag,S,neg,Entry,Clause,Neg,MaxNegs,NCover,NCount),
 2200        !.
 2201
 2202% Bug reported by Daniel Fredouille
 2203% For MiAcc =:= 0, Negs was being set to P1 + 1. Unclear why.
 2204% This definition is as it was up to Aleph 2.
 2205get_max_negs(Noise/MinAcc,P1,N):-
 2206        number(P1), 
 2207	(MinAcc =:= 0.0 -> N is Noise;
 2208        	(N1 is integer((1-MinAcc)*P1/MinAcc),
 2209		(Noise < N1 -> N is Noise; N is N1))
 2210	), !.
 2211get_max_negs(Noise/_,_,Noise).
 2212
 2213
 2214% update_open_list(+SearchKeys,+NodeRef,+Label)
 2215% insert SearchKeys into openlist
 2216update_open_list([K1|K2],NodeRef,Label):-
 2217	assertz('$aleph_search_gain'(K1,K2,NodeRef,Label)),
 2218	retract('$aleph_search'(openlist,OpenList)),
 2219	uniq_insert(descending,[K1|K2],OpenList,List1),
 2220	asserta('$aleph_search'(openlist,List1)).
 2221
 2222pos_ok(S,_,_,_,_,_):-
 2223	arg(3,S,RefineOp),
 2224	(RefineOp = rls; RefineOp = user),  !.
 2225pos_ok(S,Entry,_,[P,_],_,_):-
 2226        arg(13,S,MinPos),
 2227        P < MinPos, !,
 2228        arg(8,S,Caching),
 2229        (Caching = true ->
 2230                add_prune_cache(Entry);
 2231                true),
 2232        fail.
 2233pos_ok(S,Entry,_,[P,_],_,_):-
 2234	arg(40,S,MinPosFrac),
 2235	MinPosFrac > 0.0,
 2236	'$aleph_search'(clauseprior,_-[P1-pos,_]),
 2237	P/P1 < MinPosFrac, !,
 2238        arg(8,S,Caching),
 2239        (Caching = true ->
 2240                add_prune_cache(Entry);
 2241                true),
 2242	fail.
 2243pos_ok(S,_,[_,_,_,C1|_],[P,L],_,_):-
 2244        arg(4,S,_/Evalfn),
 2245	arg(2,S,Explore),
 2246	((Evalfn = user; Explore = true) -> true;
 2247        	evalfn(Evalfn,[P,0,L],C2),
 2248		best_value(Evalfn,S,[P,0,L,C2],Max),
 2249        	Max > C1), !.
 2250
 2251
 2252maxlength_neg_ok(Noise/MinAcc,Entry,P,N):-
 2253	((N > Noise); (P/(P+N) < MinAcc)), !,
 2254        add_prune_cache(Entry),
 2255	fail.
 2256maxlength_neg_ok(_,_,_,_).
 2257
 2258compression_ok(compression,[P,_,L|_]):-
 2259	!,
 2260	P - L + 1 > 0.
 2261compression_ok(_,_).
 2262
 2263length_ok(S,MinLen,ClauseLen,LastD,ExpectedMin,ExpectedCLen):-
 2264        arg(3,S,RefineOp),
 2265        (RefineOp = false  -> L1 = LastD; L1 = 0),
 2266        (L1 < MinLen->ExpectedMin = L1;ExpectedMin = MinLen),
 2267        ExpectedCLen is ClauseLen + ExpectedMin,
 2268        arg(7,S,CLength),
 2269        ExpectedCLen =< CLength, !.
 2270
 2271update_best(S,_,_,_,Best,[P,_,_,F|_]/_,Best):-
 2272        arg(13,S,MinPos),
 2273        arg(19,S,MinScore),
 2274	(P < MinPos;  F is -inf; F < MinScore), !.
 2275update_best(S,_,_,_,Best,[P|_]/_,Best):-
 2276	arg(40,S,MinPosFrac),
 2277	MinPosFrac > 0.0,
 2278	'$aleph_search'(clauseprior,_-[P1-pos,_]),
 2279	P/P1 < MinPosFrac, !.
 2280update_best(S,_,_,_,Best,[P,N,_,_|_]/_,Best):-
 2281        arg(4,S,_/Evalfn),
 2282	Evalfn \= posonly,
 2283	% Evalfn \= user,
 2284        arg(17,S,Noise),
 2285        arg(18,S,MinAcc),
 2286	arg(22,S,Search),
 2287	Total is P + N,
 2288	((N > Noise);(Search \= ic, Total > 0, P/Total < MinAcc)),   !.
 2289update_best(S,Clause,PCover,NCover,Label/_,Label1/Node1,Label1/Node1):-
 2290        Label = [_,_,_,GainE|_],
 2291        Label1 = [_,_,_,Gain1E|_],
 2292	arithmetic_expression_value(GainE,Gain),
 2293	arithmetic_expression_value(Gain1E,Gain1),
 2294        % (Gain1 = inf; Gain = -inf; Gain1 > Gain), !,
 2295	Gain1 > Gain, !,
 2296	retractall('$aleph_search'(selected,_)),
 2297        asserta('$aleph_search'(selected,selected(Label1,Clause,PCover,NCover))),
 2298        arg(35,S,VSearch),
 2299        (VSearch = true ->
 2300		retractall('$aleph_search'(best,_)),
 2301                asserta('$aleph_search'(best,Node1)),
 2302                asserta('$aleph_search'(good,Node1));
 2303                true),
 2304	update_good(Label1,Clause),
 2305        show_clause(newbest,Label1,Clause,Node1),
 2306        record_clause(newbest,Label1,Clause,Node1),
 2307        record_clause(good,Label1,Clause,Node1).
 2308update_best(S,Clause,_,_,Label/Node,Label1/Node1,Label/Node):-
 2309        arg(35,S,VSearch),
 2310        (VSearch = true ->
 2311                asserta('$aleph_search'(good,Node1));
 2312                true),
 2313	update_good(Label1,Clause),
 2314        show_clause(good,Label1,Clause,Node1),
 2315        record_clause(good,Label1,Clause,Node1).
 2316
 2317update_good(Label,Clause):- 
 2318	setting(good,true), !,
 2319	Label = [_,_,L|_],
 2320	setting(check_good,Flag),
 2321	update_good(Flag,L,Label,Clause).
 2322update_good(_,_).
 2323
 2324update_good(_,_,_,_):-
 2325	setting(goodfile,_), !.
 2326update_good(true,L,Label,Clause):-
 2327	'$aleph_good'(L,Label,Clause), !.
 2328update_good(_,L,Label,Clause):-
 2329	assertz('$aleph_good'(L,Label,Clause)),
 2330	(retract('$aleph_search'(last_good,Good)) ->
 2331		Good1 is Good + 1;
 2332		Good1 is 1),
 2333	assertz('$aleph_search'(last_good,Good1)).
 2334
 2335update_best_theory(S,_,_,_,Best,[P,N,_,F|_]/_,Best):-
 2336	arg(17,S,Noise),
 2337	arg(18,S,MinAcc),
 2338	arg(19,S,MinScore),
 2339	(N > Noise; P/(P+N) < MinAcc; F < MinScore),  !.
 2340update_best_theory(_,Theory,PCover,NCover,Label/_,Label1/Node1,Label1/Node1):-
 2341	Label = [_,_,_,GainE|_],
 2342	Label1 = [_,_,_,Gain1E|_],
 2343	arithmetic_expression_value(GainE,Gain),
 2344	arithmetic_expression_value(Gain1E,Gain1),
 2345	Gain1 > Gain, !, 
 2346	retractall('$aleph_search'(selected,_)),
 2347        asserta('$aleph_search'(selected,selected(Label1,Theory,PCover,NCover))),
 2348	show_theory(newbest,Label1,Theory,Node1),
 2349	record_theory(newbest,Label1,Theory,Node1),
 2350	record_theory(good,Label1,Theory,Node1).
 2351update_best_theory(_,Theory,_,_,Best,Label1/_,Best):-
 2352	show_theory(good,Label1,Theory,Node1),
 2353	record_theory(good,Label1,Theory,Node1).
 2354
 2355%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2356% P R U N I N G   C L A U S E S
 2357
 2358get_node([[K1|K2]|_],[K1|K2],Node):-
 2359        '$aleph_search_gain'(K1,K2,Node,_).
 2360get_node([_|Gains],Gain,Node):-
 2361	get_node(Gains,Gain,Node).
 2362
 2363prune_open(S,_,_):-
 2364	arg(25,S,OSize),
 2365	Inf is inf,
 2366	OSize =\= Inf,
 2367        retractall('$aleph_local'(in_beam,_)),
 2368        asserta('$aleph_local'(in_beam,0)),
 2369        '$aleph_search'(openlist,Gains),
 2370        get_node(Gains,[K1|K2],NodeNum),
 2371        '$aleph_local'(in_beam,N),
 2372        (N < OSize->
 2373        	retract('$aleph_local'(in_beam,N)),
 2374                N1 is N + 1,
 2375                asserta('$aleph_local'(in_beam,N1));
 2376		retract('$aleph_search_gain'(K1,K2,NodeNum,_)),
 2377		arg(6,S,Verbose),
 2378                (Verbose < 1 ->
 2379			true;
 2380			p1_message('non-admissible removal'),
 2381			p_message(NodeNum))),
 2382        fail.
 2383prune_open(S,_,_):-
 2384        arg(2,S,Explore),
 2385        arg(3,S,RefineOp),
 2386	(Explore = true; RefineOp = rls; RefineOp = user), !.
 2387prune_open(_,_/N,_/N):- !.
 2388prune_open(S,_,[_,_,_,Best|_]/_):-
 2389        arg(4,S,_/Evalfn),
 2390	built_in_prune(Evalfn),
 2391        '$aleph_search_gain'(_,_,_,Label),
 2392	best_value(Evalfn,S,Label,Best1),
 2393	Best1 =< Best, 
 2394        retract('$aleph_search_gain'(_,_,_,Label)),
 2395	fail.
 2396prune_open(_,_,_).
 2397
 2398built_in_prune(coverage).
 2399built_in_prune(compression).
 2400built_in_prune(posonly).
 2401built_in_prune(laplace).
 2402built_in_prune(wracc).
 2403built_in_prune(mestimate).
 2404built_in_prune(auto_m).
 2405
 2406% pruning for posonly, laplace and m-estimates devised in
 2407%	discussion with James Cussens
 2408% pruning for weighted relative accuracy devised in
 2409%	discussion with Steve Moyle
 2410% corrections to best_value/4 after discussion with
 2411% Mark Reid and James Cussens
 2412best_value(gini,_,_,0.0):- !.
 2413best_value(entropy,_,_,0.0):- !.
 2414best_value(posonly,S,[P,_,L|_],Best):-
 2415	arg(20,S,RSize),
 2416	Best is log(P) + log(RSize+2.0) - (L+1)/P, !.
 2417best_value(wracc,_,[P|_],Best):-
 2418	('$aleph_search'(clauseprior,Total-[P1-pos,_]) ->
 2419		Best is P*(Total - P1)/(Total^2);
 2420		Best is 0.25), !.
 2421best_value(Evalfn,_,[P,_,L|Rest],Best):-
 2422	L1 is L + 1,	% need at least 1 extra literal to achieve best value
 2423	evalfn(Evalfn,[P,0,L1|Rest],Best).
 2424
 2425
 2426get_nextbest(S,NodeRef):-
 2427        arg(22,S,Search),
 2428	select_nextbest(Search,NodeRef).
 2429
 2430% Select the next best node
 2431% Incorporates the changes made by Filip Zelezny to
 2432% achieve the `randomised rapid restart' (or rrr) technique
 2433% within randomised local search
 2434select_nextbest(rls,NodeRef):-
 2435	retractall('$aleph_search'(nextnode,_)),
 2436        setting(rls_type,Type),
 2437        (retract('$aleph_search'(rls_parentstats,stats(PStats,_,_))) -> true; true),
 2438        (rls_nextbest(Type,PStats,NodeRef,Label) ->
 2439                asserta('$aleph_search'(rls_parentstats,stats(Label,[],[]))),
 2440                setting(rls_type,RlsType),
 2441                (RlsType = rrr ->
 2442                      true;
 2443                      assertz('$aleph_search'(nextnode,NodeRef)));
 2444                NodeRef = none), !.
 2445select_nextbest(_,NodeRef):-
 2446	retractall('$aleph_search'(nextnode,_)),
 2447	get_nextbest(NodeRef), !.
 2448select_nextbest(_,none).
 2449
 2450get_nextbest(NodeRef):-
 2451        '$aleph_search'(openlist,[H|_]),
 2452	H = [K1|K2],
 2453        retract('$aleph_search_gain'(K1,K2,NodeRef,_)),
 2454        assertz('$aleph_search'(nextnode,NodeRef)).
 2455get_nextbest(NodeRef):-
 2456        retract('$aleph_search'(openlist,[_|T])),
 2457        asserta('$aleph_search'(openlist,T)),
 2458        get_nextbest(NodeRef), !.
 2459get_nextbest(none).
 2460
 2461rls_nextbest(rrr,_,NodeRef,_):-
 2462        get_nextbest(NodeRef).
 2463rls_nextbest(gsat,_,NodeRef,Label):-
 2464        retract('$aleph_search'(openlist,[H|_])),
 2465	H = [K1|K2],
 2466	asserta('$aleph_search'(openlist,[])),
 2467	findall(N-L,'$aleph_search_gain'(K1,K2,N,L),Choices),
 2468	length(Choices,Last),
 2469	get_random(Last,N),
 2470	aleph_remove_nth(N,Choices,NodeRef-Label,_),
 2471	retractall('$aleph_search_gain'(_,_,_,_)).
 2472rls_nextbest(wsat,PStats,NodeRef,Label):-
 2473	setting(walk,WProb),
 2474	aleph_random(P),
 2475	P >= WProb, !,
 2476	rls_nextbest(gsat,PStats,NodeRef,Label).
 2477rls_nextbest(wsat,PStats,NodeRef,Label):-
 2478	p_message('random walk'),
 2479        retract('$aleph_search'(openlist,_)),
 2480	asserta('$aleph_search'(openlist,[])),
 2481	findall(N-L,'$aleph_search_gain'(_,_,N,L),AllNodes),
 2482	potentially_good(AllNodes,PStats,Choices),
 2483        length(Choices,Last),
 2484        get_random(Last,N),
 2485        aleph_remove_nth(N,Choices,NodeRef-Label,_),
 2486	retractall('$aleph_search_gain'(_,_,_,_)).
 2487rls_nextbest(anneal,[P,N|_],NodeRef,Label):-
 2488	setting(temperature,Temp),
 2489        retract('$aleph_search'(openlist,_)),
 2490	asserta('$aleph_search'(openlist,[])),
 2491	findall(N-L,'$aleph_search_gain'(_,_,N,L),AllNodes),
 2492	length(AllNodes,Last),
 2493	get_random(Last,S),
 2494	aleph_remove_nth(S,AllNodes,NodeRef-Label,_),
 2495	Label = [P1,N1|_],
 2496	Gain is (P1 - N1) - (P - N),
 2497	((P = 1); (Gain >= 0);(aleph_random(R), R < exp(Gain/Temp))).
 2498
 2499potentially_good([],_,[]).
 2500potentially_good([H|T],Label,[H|T1]):-
 2501        H = _-Label1,
 2502        potentially_good(Label,Label1), !,
 2503        potentially_good(T,Label,T1).
 2504potentially_good([_|T],Label,T1):-
 2505        potentially_good(T,Label,T1).
 2506
 2507potentially_good([1|_],[P1|_]):-
 2508        !,
 2509        P1 > 1.
 2510potentially_good([P,_,L|_],[P1,_,L1|_]):-
 2511        L1 =< L, !,
 2512        P1 > P.
 2513potentially_good([_,N|_],[_,N1|_]):-
 2514        N1 < N.
 2515
 2516
 2517%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2518% P R O V E
 2519
 2520% prove with caching
 2521% if entry exists in cache, then return it
 2522% otherwise find and cache cover 
 2523% if ``exact'' flag is set then only check proof for examples
 2524% in the part left over due to lazy theorem-proving
 2525% ideas in caching developed in discussions with James Cussens
 2526
 2527prove_cache(exact,S,Type,Entry,Clause,Intervals,IList,Count):-
 2528	!,
 2529	(Intervals = Exact/Left ->
 2530        	arg(14,S,Depth),
 2531        	arg(29,S,Time),
 2532        	arg(34,S,Proof),
 2533        	prove(Depth/Time/Proof,Type,Clause,Left,IList1,Count1),
 2534		aleph_append(IList1,Exact,IList),
 2535		interval_count(Exact,Count0),
 2536		Count is Count0 + Count1;
 2537		IList = Intervals,
 2538		interval_count(IList,Count)),
 2539        arg(8,S,Caching),
 2540        (Caching = true -> add_cache(Entry,Type,IList); true).
 2541prove_cache(upper,S,Type,Entry,Clause,Intervals,IList,Count):-
 2542        arg(8,S,Caching),
 2543        Caching = true, !,
 2544        arg(14,S,Depth),
 2545        arg(29,S,Time),
 2546        arg(34,S,Proof),
 2547        (check_cache(Entry,Type,Cached)->
 2548                prove_cached(S,Type,Entry,Cached,Clause,Intervals,IList,Count);
 2549                prove_intervals(Depth/Time/Proof,Type,Clause,Intervals,IList,Count),
 2550                add_cache(Entry,Type,IList)).
 2551prove_cache(upper,S,Type,_,Clause,Intervals,IList,Count):-
 2552        arg(14,S,Depth),
 2553        arg(29,S,Time),
 2554        arg(34,S,Proof),
 2555	(Intervals = Exact/Left ->
 2556		aleph_append(Left,Exact,IList1),
 2557        	prove(Depth/Time/Proof,Type,Clause,IList1,IList,Count);
 2558        	prove(Depth/Time/Proof,Type,Clause,Intervals,IList,Count)).
 2559
 2560prove_intervals(DepthTime,Type,Clause,I1/Left,IList,Count):- 
 2561	!,
 2562	aleph_append(Left,I1,Intervals),
 2563	prove(DepthTime,Type,Clause,Intervals,IList,Count).
 2564prove_intervals(DepthTime,Type,Clause,Intervals,IList,Count):- 
 2565	prove(DepthTime,Type,Clause,Intervals,IList,Count).
 2566
 2567prove_cached(S,Type,Entry,I1/Left,Clause,Intervals,IList,Count):-
 2568        !,
 2569        arg(14,S,Depth),
 2570        arg(29,S,Time),
 2571        arg(34,S,Proof),
 2572        prove(Depth/Time/Proof,Type,Clause,Left,I2,_),
 2573        aleph_append(I2,I1,I),
 2574        (Type = pos ->
 2575                arg(5,S,Greedy),
 2576                (Greedy = true ->
 2577                        intervals_intersection(I,Intervals,IList);
 2578                        IList = I);
 2579                IList = I),
 2580        interval_count(IList,Count),
 2581        update_cache(Entry,Type,IList).
 2582prove_cached(S,Type,Entry,I1,_,Intervals,IList,Count):-
 2583	(Type = pos -> arg(5,S,Greedy),
 2584		(Greedy = true ->
 2585			intervals_intersection(I1,Intervals,IList);
 2586			IList = I1);
 2587		IList = I1),
 2588	interval_count(IList,Count),
 2589	update_cache(Entry,Type,IList).
 2590
 2591% prove at most Max atoms
 2592prove_cache(exact,S,Type,Entry,Clause,Intervals,Max,IList,Count):-
 2593	!,
 2594	(Intervals = Exact/Left ->
 2595		interval_count(Exact,Count0),
 2596		Max1 is Max - Count0,
 2597        	arg(12,S,LNegs),
 2598        	arg(14,S,Depth),
 2599        	arg(29,S,Time),
 2600        	arg(34,S,Proof),
 2601        	prove(LNegs/false,Depth/Time/Proof,Type,Clause,Left,Max1,IList1,Count1),
 2602		aleph_append(IList1,Exact,Exact1),
 2603		find_lazy_left(S,Type,Exact1,Left1),
 2604		IList = Exact1/Left1,
 2605		Count is Count0 + Count1;
 2606		IList = Intervals,
 2607		interval_count(Intervals,Count)),
 2608        arg(8,S,Caching),
 2609        (Caching = true -> add_cache(Entry,Type,IList); true).
 2610prove_cache(upper,S,Type,Entry,Clause,Intervals,Max,IList,Count):-
 2611        arg(8,S,Caching),
 2612        Caching = true, !,
 2613        (check_cache(Entry,Type,Cached)->
 2614                prove_cached(S,Type,Entry,Cached,Clause,Intervals,Max,IList,Count);
 2615                (prove_intervals(S,Type,Clause,Intervals,Max,IList1,Count)->
 2616                        find_lazy_left(S,Type,IList1,Left1),
 2617                        add_cache(Entry,Type,IList1/Left1),
 2618			IList = IList1/Left1,
 2619                        retractall('$aleph_local'(example_cache,_));
 2620                        collect_example_cache(IList),
 2621                        add_cache(Entry,Type,IList),
 2622                        fail)).
 2623prove_cache(upper,S,Type,_,Clause,Intervals,Max,IList/Left1,Count):-
 2624        arg(8,S,Caching),
 2625        arg(12,S,LNegs),
 2626        arg(14,S,Depth),
 2627        arg(29,S,Time),
 2628        arg(34,S,Proof),
 2629	(Intervals = Exact/Left ->
 2630		aleph_append(Left,Exact,IList1),
 2631        	prove(LNegs/Caching,Depth/Time/Proof,Type,Clause,IList1,Max,IList,Count);
 2632        	prove(LNegs/Caching,Depth/Time/Proof,Type,Clause,Intervals,Max,IList,Count)),
 2633	find_lazy_left(S,Type,IList,Left1).
 2634
 2635prove_intervals(S,Type,Clause,I1/Left,Max,IList,Count):-
 2636        !,
 2637        arg(8,S,Caching),
 2638        arg(12,S,LNegs),
 2639        arg(14,S,Depth),
 2640        arg(29,S,Time),
 2641        arg(34,S,Proof),
 2642        aleph_append(Left,I1,Intervals),
 2643        prove(LNegs/Caching,Depth/Time/Proof,Type,Clause,Intervals,Max,IList,Count).
 2644prove_intervals(S,Type,Clause,Intervals,Max,IList,Count):-
 2645        arg(8,S,Caching),
 2646        arg(12,S,LNegs),
 2647        arg(14,S,Depth),
 2648        arg(29,S,Time),
 2649        arg(34,S,Proof),
 2650        prove(LNegs/Caching,Depth/Time/Proof,Type,Clause,Intervals,Max,IList,Count).
 2651
 2652
 2653prove_cached(S,Type,Entry, I1/Left,Clause,_,Max,IList/Left1,Count):-
 2654        !,
 2655        arg(8,S,Caching),
 2656        arg(12,S,LNegs),
 2657        arg(14,S,Depth),
 2658        arg(29,S,Time),
 2659        arg(34,S,Proof),
 2660        interval_count(I1,C1),
 2661        Max1 is Max - C1,
 2662        Max1 >= 0,
 2663        (prove(LNegs/Caching,Depth/Time/Proof,Type,Clause,Left,Max1,I2,C2)->
 2664                aleph_append(I2,I1,IList),
 2665                Count is C2 + C1,
 2666                find_lazy_left(S,Type,IList,Left1),
 2667                update_cache(Entry,Type,IList/Left1),
 2668                retractall('$aleph_local'(example_cache,_));
 2669                collect_example_cache(I2/Left1),
 2670                aleph_append(I2,I1,IList),
 2671                update_cache(Entry,Type,IList/Left1),
 2672                fail).
 2673prove_cached(_,neg,_, I1/L1,_,_,_,I1/L1,C1):-
 2674	!,
 2675	interval_count(I1,C1).
 2676prove_cached(S,_,_,I1,_,_,Max,I1,C1):-
 2677	interval_count(I1,C1),
 2678	arg(12,S,LNegs),
 2679	(LNegs = true ->true; C1 =< Max).
 2680
 2681collect_example_cache(Intervals/Left):-
 2682	retract('$aleph_local'(example_cache,[Last|Rest])),
 2683	aleph_reverse([Last|Rest],IList),
 2684	list_to_intervals1(IList,Intervals),
 2685	Next is Last + 1,
 2686	'$aleph_global'(size,size(neg,LastN)),
 2687	(Next > LastN -> Left = []; Left = [Next-LastN]).
 2688
 2689find_lazy_left(S,_,_,[]):-
 2690        arg(12,S,LazyNegs),
 2691        LazyNegs = false, !.
 2692find_lazy_left(_,_,[],[]).
 2693find_lazy_left(S,Type,[_-F],Left):-
 2694        !,
 2695        F1 is F + 1,
 2696	(Type = pos -> arg(16,S,Last);
 2697		(Type = neg -> arg(24,S,Last);
 2698			(Type = rand -> arg(20,S,Last); Last = F))),
 2699        (F1 > Last -> Left = []; Left = [F1-Last]).
 2700find_lazy_left(S,Type,[_|T1],Left):-
 2701        find_lazy_left(S,Type,T1,Left).
 2702
 2703
 2704% prove atoms specified by Type and index set using Clause.
 2705% dependent on data structure used for index set:
 2706% currently index set is a list of intervals
 2707% return atoms proved and their count
 2708% if tail-recursive version is needed see below
 2709
 2710prove(_,_,_,[],[],0).
 2711prove(Flags,Type,Clause,[Interval|Intervals],IList,Count):-
 2712	index_prove(Flags,Type,Clause,Interval,I1,C1),
 2713	prove(Flags,Type,Clause,Intervals,I2,C2),
 2714	aleph_append(I2,I1,IList),
 2715	Count is C1 + C2.
 2716
 2717
 2718%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2719% T A I L - R E C U R S I V E  P R O V E/6
 2720 
 2721% use this rather than the prove/6 above for tail recursion
 2722% written by James Cussens
 2723 
 2724
 2725% prove(DepthTime,Type,Clause,Intervals,IList,Count):-
 2726       % prove2(Intervals,DepthTime,Type,Clause,0,IList,Count).
 2727 
 2728% code for tail recursive cover testing
 2729% starts here
 2730
 2731% when we know that Sofar is a variable.
 2732prove2([],_,_,_,Count,[],Count).
 2733prove2([Current-Finish|Intervals],Depth/Time/Proof,Type,(Head:-Body),InCount,Sofar,OutCount) :-
 2734	example(Current,Type,Example),
 2735	\+ prove1(Proof,Depth/Time,Example,(Head:-Body)), %uncovered
 2736        !,
 2737        (Current>=Finish ->
 2738            prove2(Intervals,Depth/Time/Proof,Type,(Head:-Body),InCount,Sofar,OutCount);
 2739            Next is Current+1,!,
 2740            prove2([Next-Finish|Intervals],Depth/Time/Proof,Type,(Head:-Body),InCount,Sofar,OutCount)
 2741        ).
 2742prove2([Current-Finish|Intervals],ProofFlags,Type,Clause,InCount,Sofar,OutCount) :-
 2743        (Current>=Finish ->
 2744            Sofar=[Current-Current|Rest],
 2745            MidCount is InCount+1,!,
 2746            prove2(Intervals,ProofFlags,Type,Clause,MidCount,Rest,OutCount);
 2747            Next is Current+1,
 2748            Sofar=[Current-_Last|_Rest],!,
 2749            prove3([Next-Finish|Intervals],ProofFlags,Type,Clause,InCount,Sofar,OutCount)
 2750        ).
 2751 
 2752%when Sofar is not a variable
 2753prove3([Current-Finish|Intervals],Depth/Time/Proof,Type,(Head:-Body),InCount,Sofar,OutCount) :-
 2754	example(Current,Type,Example),
 2755	\+ prove1(Proof,Depth/Time,Example,(Head:-Body)), %uncovered
 2756        !,
 2757        Last is Current-1, %found some previously
 2758        Sofar=[Start-Last|Rest], %complete found interval
 2759        MidCount is InCount+Current-Start,
 2760        (Current>=Finish ->
 2761            prove2(Intervals,Depth/Time/Proof,Type,(Head:-Body),MidCount,Rest,OutCount);
 2762            Next is Current+1,!,
 2763            prove2([Next-Finish|Intervals],Depth/Time/Proof,Type,(Head:-Body),MidCount,Rest,OutCount)
 2764        ).
 2765prove3([Current-Finish|Intervals],ProofFlags,Type,Clause,InCount,Sofar,OutCount) :-
 2766        (Current>=Finish ->
 2767            Sofar=[Start-Finish|Rest],
 2768            MidCount is InCount+Finish-Start+1,!,
 2769            prove2(Intervals,ProofFlags,Type,Clause,MidCount,Rest,OutCount);
 2770            Next is Current+1,!,
 2771            prove3([Next-Finish|Intervals],ProofFlags,Type,Clause,InCount,Sofar,OutCount)
 2772        ).
 2773 
 2774 
 2775% code for tail recursive cover testing
 2776% ends here
 2777
 2778index_prove(_,_,_,Start-Finish,[],0):-
 2779	Start > Finish, !.
 2780index_prove(ProofFlags,Type,Clause,Start-Finish,IList,Count):-
 2781	index_prove1(ProofFlags,Type,Clause,Start,Finish,Last),
 2782	Last0 is Last - 1 ,
 2783	Last1 is Last + 1,
 2784	(Last0 >= Start->
 2785		index_prove(ProofFlags,Type,Clause,Last1-Finish,Rest,Count1),
 2786		IList = [Start-Last0|Rest],
 2787		Count is Last - Start + Count1;
 2788		index_prove(ProofFlags,Type,Clause,Last1-Finish,IList,Count)).
 2789
 2790prove1(G):-
 2791	depth_bound_call(G), !.
 2792
 2793prove1(user,_,Example,Clause):-
 2794	prove(Clause,Example), !.
 2795prove1(restricted_sld,Depth/Time,Example,(Head:-Body)):-
 2796	\+((\+(((Example = Head),resource_bound_call(Time,Depth,Body))))), !.
 2797prove1(sld,Depth/Time,Example,_):-
 2798	\+(\+(resource_bound_call(Time,Depth,Example))), !.
 2799	
 2800index_prove1(_,_,_,Num,Last,Num):-
 2801	Num > Last, !.
 2802index_prove1(Depth/Time/Proof,Type,Clause,Num,Finish,Last):-
 2803	example(Num,Type,Example),
 2804	prove1(Proof,Depth/Time,Example,Clause), !,
 2805	Num1 is Num + 1,
 2806	index_prove1(Depth/Time/Proof,Type,Clause,Num1,Finish,Last).
 2807index_prove1(_,_,_,Last,_,Last).
 2808
 2809
 2810% proves at most Max atoms using Clause.
 2811
 2812prove(_,_,_,_,[],_,[],0).
 2813prove(Flags,ProofFlags,Type,Clause,[Interval|Intervals],Max,IList,Count):-
 2814        index_prove(Flags,ProofFlags,Type,Clause,Interval,Max,I1,C1), !,
 2815        Max1 is Max - C1,
 2816        prove(Flags,ProofFlags,Type,Clause,Intervals,Max1,I2,C2),
 2817        aleph_append(I2,I1,IList),
 2818        Count is C1 + C2.
 2819
 2820
 2821index_prove(_,_,_,_,Start-Finish,_,[],0):-
 2822        Start > Finish, !.
 2823index_prove(Flags,ProofFlags,Type,Clause,Start-Finish,Max,IList,Count):-
 2824        index_prove1(Flags,ProofFlags,Type,Clause,Start,Finish,0,Max,Last),
 2825        Last0 is Last - 1 ,
 2826        Last1 is Last + 1,
 2827        (Last0 >= Start->
 2828                Max1 is Max - Last + Start,
 2829		((Max1 = 0, Flags = true/_) ->
 2830                        Rest = [], Count1 = 0;
 2831                	index_prove(Flags,ProofFlags,Type,Clause,Last1-Finish,
 2832					Max1,Rest,Count1)),
 2833                IList = [Start-Last0|Rest],
 2834                Count is Last - Start + Count1;
 2835                index_prove(Flags,ProofFlags,Type,Clause,Last1-Finish,Max,IList,Count)).
 2836
 2837index_prove1(false/_,_,_,_,_,_,Proved,Allowed,_):-
 2838        Proved > Allowed, !, fail.
 2839index_prove1(_,_,_,_,Num,Last,_,_,Num):-
 2840        Num > Last, !.
 2841index_prove1(true/_,_,_,_,Num,_,Allowed,Allowed,Num):- !.
 2842index_prove1(LNegs/Caching,Depth/Time/Proof,Type,Clause,Num,Finish,Proved,Allowed,Last):-
 2843	example(Num,Type,Example),
 2844	prove1(Proof,Depth/Time,Example,Clause), !,
 2845        Num1 is Num + 1,
 2846        Proved1 is Proved + 1,
 2847        (Caching = true ->
 2848                (retract('$aleph_local'(example_cache,L)) ->
 2849                        asserta('$aleph_local'(example_cache,[Num|L]));
 2850                        asserta('$aleph_local'(example_cache,[Num])));
 2851                true),
 2852        index_prove1(LNegs/Caching,Depth/Time/Proof,Type,Clause,Num1,Finish,Proved1,Allowed,Last).
 2853index_prove1(_,_,_,_,Last,_,_,_,Last).
 2854
 2855% resource_bound_call(Time,Depth,Goals)
 2856%	attempt to prove Goals using depth bounded theorem-prover
 2857%	in at most Time secs
 2858resource_bound_call(T,Depth,Goals):-
 2859	Inf is inf,
 2860	T =:= Inf,
 2861	!,
 2862	depth_bound_call(Goals,Depth).
 2863resource_bound_call(T,Depth,Goals):-
 2864        catch(time_bound_call(T,prooflimit,depth_bound_call(Goals,Depth)),
 2865		prooflimit,fail).
 2866
 2867time_bound_call(T,Exception,Goal):-
 2868	alarm(T,throw(Exception),X),
 2869        (Goal -> remove_alarm(X); remove_alarm(X), fail).
 2870
 2871%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2872% C A C H I N G
 2873
 2874clear_cache:-
 2875	retractall('$aleph_search_cache'(_)),
 2876	retractall('$aleph_search_prunecache'(_)).
 2877
 2878check_cache(Entry,Type,I):-
 2879	Entry \= false,
 2880        '$aleph_search_cache'(Entry), !,
 2881        functor(Entry,_,Arity),
 2882        (Type = pos -> Arg is Arity - 1; Arg is Arity),
 2883        arg(Arg,Entry,I),
 2884	nonvar(I).
 2885
 2886add_cache(false,_,_):- !.
 2887add_cache(Entry,Type,I):-
 2888        (retract('$aleph_search_cache'(Entry))-> true ; true),
 2889        functor(Entry,_,Arity),
 2890        (Type = pos -> Arg is Arity - 1; Arg is Arity),
 2891        (arg(Arg,Entry,I)-> asserta('$aleph_search_cache'(Entry));
 2892                        true), !.
 2893
 2894update_cache(Entry,Type,I):-
 2895        Entry \= false,
 2896        functor(Entry,Name,Arity),
 2897        (Type = pos -> Arg is Arity - 1; Arg is Arity),
 2898        arg(Arg,Entry,OldI),
 2899        OldI = _/_,
 2900        retract('$aleph_search_cache'(Entry)),
 2901        functor(NewEntry,Name,Arity),
 2902        Arg0 is Arg - 1,
 2903        copy_args(Entry,NewEntry,1,Arg0),
 2904        arg(Arg,NewEntry,I),
 2905        Arg1 is Arg + 1,
 2906        copy_args(Entry,NewEntry,Arg1,Arity),
 2907        asserta('$aleph_search_cache'(NewEntry)), !.
 2908update_cache(_,_,_).
 2909
 2910	
 2911add_prune_cache(false):- !.
 2912add_prune_cache(Entry):-
 2913	('$aleph_global'(caching,set(caching,true))->
 2914		functor(Entry,_,Arity),
 2915		A1 is Arity - 2,
 2916		arg(A1,Entry,Clause),
 2917		asserta('$aleph_search_prunecache'(Clause));
 2918		true).
 2919
 2920get_cache_entry(Max,Clause,Entry):-
 2921        skolemize(Clause,Head,Body,0,_),
 2922	length(Body,L1),
 2923	Max >= L1 + 1,
 2924        aleph_hash_term([Head|Body],Entry), !.
 2925get_cache_entry(_,_,false).
 2926
 2927% upto 3-argument indexing using predicate names in a clause
 2928aleph_hash_term([L0,L1,L2,L3,L4|T],Entry):-
 2929        !,
 2930        functor(L1,P1,_), functor(L2,P2,_),
 2931        functor(L3,P3,_), functor(L4,P4,_),
 2932        functor(Entry,P4,6),
 2933        arg(1,Entry,P2), arg(2,Entry,P3),
 2934        arg(3,Entry,P1), arg(4,Entry,[L0,L1,L2,L3,L4|T]).
 2935aleph_hash_term([L0,L1,L2,L3],Entry):-
 2936        !,
 2937        functor(L1,P1,_), functor(L2,P2,_),
 2938        functor(L3,P3,_),
 2939        functor(Entry,P3,5),
 2940        arg(1,Entry,P2), arg(2,Entry,P1),
 2941        arg(3,Entry,[L0,L1,L2,L3]).
 2942aleph_hash_term([L0,L1,L2],Entry):-
 2943        !,
 2944        functor(L1,P1,_), functor(L2,P2,_),
 2945        functor(Entry,P2,4),
 2946        arg(1,Entry,P1), arg(2,Entry,[L0,L1,L2]).
 2947aleph_hash_term([L0,L1],Entry):-
 2948        !,
 2949        functor(L1,P1,_),
 2950        functor(Entry,P1,3),
 2951        arg(1,Entry,[L0,L1]).
 2952aleph_hash_term([L0],Entry):-
 2953        functor(L0,P0,_),
 2954        functor(Entry,P0,3),
 2955        arg(1,Entry,[L0]).
 2956%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2957% T R E E S
 2958
 2959construct_tree(Type):-
 2960	setting(searchtime,Time),
 2961	Inf is inf,
 2962        Time =\= Inf,
 2963        SearchTime is integer(Time),
 2964        SearchTime > 0, !,
 2965	catch(time_bound_call(SearchTime,searchlimit,find_tree(Type)),
 2966		searchlimit,p_message('Time limit reached')).
 2967construct_tree(Type):-
 2968	find_tree(Type).
 2969
 2970% find_tree(Type) where Type is one of
 2971%      classification, regression, class_probability
 2972find_tree(Type):-
 2973	retractall('$aleph_search'(tree,_)),
 2974	retractall('$aleph_search'(tree_besterror,_)),
 2975	retractall('$aleph_search'(tree_gain,_)),
 2976	retractall('$aleph_search'(tree_lastleaf,_)),
 2977	retractall('$aleph_search'(tree_leaf,_)),
 2978	retractall('$aleph_search'(tree_newleaf,_)),
 2979	retractall('$aleph_search'(tree_startdistribution,_)),
 2980	get_start_distribution(Type,Distribution),
 2981	asserta('$aleph_search'(tree_startdistribution,d(Type,Distribution))),
 2982	'$aleph_global'(atoms_left,atoms_left(pos,Pos)),
 2983	setting(dependent,Argno),
 2984	p_message('constructing tree'),
 2985	stopwatch(StartClock),
 2986	get_search_settings(S),
 2987	auto_refine(false,Head),
 2988	gen_leaf(Leaf),
 2989	eval_treenode(S,Type,(Head:-true),[Argno],Pos,Examples,N,Cost),
 2990	asserta('$aleph_search'(tree_leaf,l(Leaf,Leaf,[Head,Cost,N],Examples))),
 2991	find_tree1([Leaf],S,Type,[Argno]),
 2992	prune_rules(S,Type,[Argno]),
 2993	stopwatch(StopClock),
 2994	add_tree(S,Type,[Argno]),
 2995	Time is StopClock - StartClock,
 2996	p1_message('construction time'), p_message(Time).
 2997
 2998get_start_distribution(regression,0-[0,0]):- !.
 2999get_start_distribution(model,0-[0,0]):-
 3000	setting(evalfn,mse), !.
 3001get_start_distribution(model,0-Distribution):- 
 3002	setting(evalfn,accuracy), !,
 3003	(setting(classes,Classes) -> true;
 3004		!,
 3005		p_message('missing setting for classes'),
 3006		fail),
 3007	initialise_distribution(Classes,Distribution), !.
 3008get_start_distribution(Tree,0-Distribution):-
 3009	(Tree = classification; Tree = class_probability),
 3010	(setting(classes,Classes) -> true;
 3011		!,
 3012		p_message('missing setting for classes'),
 3013		fail),
 3014	initialise_distribution(Classes,Distribution), !.
 3015get_start_distribution(_,_):-
 3016	p_message('incorrect/missing setting for tree_type or evalfn'),
 3017	fail.
 3018
 3019initialise_distribution([],[]).
 3020initialise_distribution([Class|Classes],[0-Class|T]):-
 3021	initialise_distribution(Classes,T).
 3022
 3023laplace_correct([],[]).
 3024laplace_correct([N-Class|Classes],[N1-Class|T]):-
 3025	N1 is N + 1,
 3026	laplace_correct(Classes,T).
 3027
 3028find_tree1([],_,_,_).
 3029find_tree1([Leaf|Leaves],S,Type,Predict):-
 3030	can_split(S,Type,Predict,Leaf,Left,Right), !,
 3031	split_leaf(Leaf,Left,Right,NewLeaves),
 3032	aleph_append(NewLeaves,Leaves,LeavesLeft),
 3033	find_tree1(LeavesLeft,S,Type,Predict).
 3034find_tree1([_|LeavesLeft],S,Type,Predict):-
 3035	find_tree1(LeavesLeft,S,Type,Predict).
 3036
 3037prune_rules(S,Tree,Predict):-
 3038	setting(prune_tree,true), 
 3039	prune_rules1(Tree,S,Predict), !.
 3040prune_rules(_,_,_).
 3041
 3042% pessimistic pruning by employing corrections to observed errors
 3043prune_rules1(class_probability,_,_):-
 3044	p_message('no pruning for class probability trees'), !.
 3045prune_rules1(model,_,_):-
 3046	p_message('no pruning for model trees'), !.
 3047prune_rules1(Tree,S,Predict):-
 3048	p_message('pruning clauses'),
 3049	'$aleph_search'(tree_leaf,l(Leaf,Parent,Clause,Examples)),
 3050	prune_rule(Tree,S,Predict,Clause,Examples,NewClause,NewExamples),
 3051	retract('$aleph_search'(tree_leaf,l(Leaf,Parent,Clause,Examples))),
 3052	asserta('$aleph_search'(tree_newleaf,l(Leaf,Parent,NewClause,NewExamples))),
 3053	fail.
 3054prune_rules1(_,_,_):-
 3055	retract('$aleph_search'(tree_newleaf,l(Leaf,Parent,NewClause,NewExamples))),
 3056	asserta('$aleph_search'(tree_leaf,l(Leaf,Parent,NewClause,NewExamples))),
 3057	fail.
 3058prune_rules1(_,_,_).
 3059
 3060prune_rule(Tree,S,PredictArg,[Clause,_,N],Examples,[PrunedClause,E1,NCov],NewEx):-
 3061	node_stats(Tree,Examples,PredictArg,Total-Distribution),
 3062	leaf_prediction(Tree,Total-Distribution,_,Incorrect),
 3063	estimate_error(Tree,Incorrect,Total,Upper),
 3064	split_clause(Clause,Head,Body),
 3065	goals_to_list(Body,BodyL),
 3066	arg(14,S,Depth),
 3067	arg(29,S,Time),
 3068	arg(34,S,Proof),
 3069	greedy_prune_rule(Tree,Depth/Time/Proof,PredictArg,[Head|BodyL],Upper,C1L,E1),
 3070	list_to_clause(C1L,PrunedClause),
 3071	% p1_message('pruned clause'), p_message(Clause),
 3072	% p_message('to'),
 3073	% p_message(PrunedClause),
 3074	(E1 < Upper ->
 3075		'$aleph_global'(atoms_left,atoms_left(pos,Pos)),
 3076        	prove(Depth/Time/Proof,pos,PrunedClause,Pos,NewEx,NCov);
 3077		NewEx = Examples,
 3078		NCov = N).
 3079
 3080
 3081% estimate error using binomial distribution as done in C4.5
 3082estimate_error(classification,Incorrect,Total,Error):-
 3083	setting(confidence,Conf),
 3084	estimate_error(1.0/0.0,0.0/1.0,Conf,Total,Incorrect,Error).
 3085
 3086% estimate upper bound on sample std deviation by
 3087% assuming the n values in a leaf are normally distributed.
 3088% In this case, a (1-alpha)x100 confidence interval for the
 3089% variance is (n-1)s^2/X^2(alpha/2) =< var =< (n-1)s^2/X^2(1-alpha/2)
 3090estimate_error(regression,Sd,1,Sd):- !.
 3091estimate_error(regression,Sd,N,Upper):-
 3092	(setting(confidence,Conf) -> true; Conf = 0.95),
 3093	Alpha is 1.0 - Conf,
 3094	DF is N - 1,
 3095	Prob is 1 - Alpha/2,
 3096	chi_square(DF,Prob,ChiSq),
 3097	Upper is Sd*sqrt((N-1)/ChiSq).
 3098
 3099bound_error(classification,Error,Total,Lower,Upper):-
 3100	(setting(confidence,Alpha) -> true; Alpha = 0.95),
 3101	approx_z(Alpha,Z),
 3102	Lower is Error - Z*sqrt(Error*(1-Error)/Total),
 3103	Upper is Error + Z*sqrt(Error*(1-Error)/Total).
 3104
 3105approx_z(P,2.58):- P >= 0.99, !.
 3106approx_z(P,Z):- P >= 0.98, !, Z is 2.33 + (P-0.98)*(2.58-2.33)/(0.99-0.98).
 3107approx_z(P,Z):- P >= 0.95, !, Z is 1.96 + (P-0.95)*(2.33-1.96)/(0.98-0.95).
 3108approx_z(P,Z):- P >= 0.90, !, Z is 1.64 + (P-0.90)*(1.96-1.64)/(0.95-0.90).
 3109approx_z(P,Z):- P >= 0.80, !, Z is 1.28 + (P-0.80)*(1.64-1.28)/(0.90-0.80).
 3110approx_z(P,Z):- P >= 0.68, !, Z is 1.00 + (P-0.68)*(1.28-1.00)/(0.80-0.68).
 3111approx_z(P,Z):- P >= 0.50, !, Z is 0.67 + (P-0.50)*(1.00-0.67)/(0.68-0.50).
 3112approx_z(_,0.67).
 3113
 3114greedy_prune_rule(Tree,Flags,PredictArg,Clause,Err0,NewClause,BestErr):-
 3115	greedy_prune_rule1(Tree,Flags,PredictArg,Clause,Err0,Clause1,Err1),
 3116	Clause \= Clause1, !,
 3117	greedy_prune_rule(Tree,Flags,PredictArg,Clause1,Err1,NewClause,BestErr).
 3118greedy_prune_rule(_,_,_,C,E,C,E).
 3119
 3120
 3121greedy_prune_rule1(Tree,Flags,PredictArg,[Head|Body],Err0,_,_):-
 3122	retractall('$aleph_search'(tree_besterror,_)),
 3123	asserta('$aleph_search'(tree_besterror,besterror([Head|Body],Err0))),
 3124	'$aleph_global'(atoms_left,atoms_left(pos,Pos)),
 3125	aleph_delete(_,Body,Left),
 3126	strip_negs(Left,Body1),
 3127	aleph_mode_linked([Head|Body1]),
 3128	list_to_clause([Head|Left],Clause),
 3129        prove(Flags,pos,Clause,Pos,Ex1,_),
 3130	node_stats(Tree,Ex1,PredictArg,Total-Distribution),
 3131	leaf_prediction(Tree,Total-Distribution,_,Incorrect),
 3132	estimate_error(Tree,Incorrect,Total,Upper),
 3133	'$aleph_search'(tree_besterror,besterror(_,BestError)),
 3134	Upper =< BestError, 
 3135	retract('$aleph_search'(tree_besterror,besterror(_,BestError))),
 3136	asserta('$aleph_search'(tree_besterror,besterror([Head|Left],Upper))),
 3137	fail.
 3138greedy_prune_rule1(_,_,_,_,_,Clause1,Err1):-
 3139	retract('$aleph_search'(tree_besterror,besterror(Clause1,Err1))).
 3140
 3141strip_negs([],[]).
 3142strip_negs([not(L)|T],[L|T1]):-
 3143	!,
 3144	strip_negs(T,T1).
 3145strip_negs([L|T],[L|T1]):-
 3146	strip_negs(T,T1).
 3147	
 3148add_tree(_,Tree,Predict):-
 3149	retract('$aleph_search'(tree_leaf,l(_,_,Leaf,Examples))),
 3150	Leaf = [Clause,Cost,P],
 3151	add_prediction(Tree,Clause,Predict,Examples,Clause1),
 3152	p_message('best clause'),
 3153	pp_dclause(Clause1),
 3154        nlits(Clause,L),
 3155	Gain is -Cost,
 3156        asserta('$aleph_global'(hypothesis,hypothesis([P,0,L,Gain],Clause1,Examples,[]))),
 3157	addhyp,
 3158	fail.
 3159add_tree(_,_,_).
 3160
 3161add_prediction(Tree,Clause,PredictArg,Examples,Clause1):-
 3162	split_clause(Clause,Head,_),
 3163	(Tree = model ->
 3164		setting(evalfn,Evalfn),
 3165		add_model(Evalfn,Clause,PredictArg,Examples,Clause1,_,_);
 3166		node_stats(Tree,Examples,PredictArg,Distribution),
 3167		leaf_prediction(Tree,Distribution,Prediction,Error),
 3168		tparg(PredictArg,Head,Var),
 3169		add_prediction(Tree,Clause,Var,Prediction,Error,Clause1)).
 3170
 3171add_prediction(classification,Clause,Var,Prediction,_,Clause1):-
 3172	extend_clause(Clause,(Var = Prediction),Clause1).
 3173add_prediction(class_probability,Clause,Var,Prediction,_,Clause1):-
 3174	extend_clause(Clause,(random(Var,Prediction)),Clause1).
 3175add_prediction(regression,Clause,Var,Mean,Sd,Clause1):-
 3176	extend_clause(Clause,(random(Var,normal(Mean,Sd))),Clause1).
 3177
 3178add_model(Evalfn,Clause,PredictArg,Examples,_,_,_):-
 3179	retractall('$aleph_local'(tree_model,_,_,_)),
 3180	Best is inf,
 3181	split_clause(Clause,Head,_),
 3182	tparg(PredictArg,Head,Var),
 3183	asserta('$aleph_local'(tree_model,false,0,Best)),
 3184	'$aleph_global'(model,model(Name/Arity)),
 3185	functor(Model,Name,Arity),
 3186	auto_extend(Clause,Model,C),
 3187	leaf_predicts(Arity,Model,Var),
 3188	lazy_evaluate_refinement([],C,[Name/Arity],Examples,[],[],C1),
 3189	find_model_error(Evalfn,Examples,C1,PredictArg,Total,Error),
 3190	'$aleph_local'(tree_model,_,_,BestSoFar),
 3191	(Error < BestSoFar ->
 3192		retract('$aleph_local'(tree_model,_,_,_)),
 3193		asserta('$aleph_local'(tree_model,C1,Total,Error));
 3194		true),
 3195	fail.	
 3196add_model(_,_,_,_,Clause,Total,Error):-
 3197	retract('$aleph_local'(tree_model,Clause,Total,Error)).
 3198
 3199
 3200find_model_error(Evalfn,Examples,(Head:-Body),[PredictArg],T,E):-
 3201	functor(Head,_,Arity),
 3202	findall(Actual-Pred,
 3203			(aleph_member(Interval,Examples),
 3204			aleph_member3(N,Interval),
 3205			example(N,pos,Example),
 3206			copy_iargs(Arity,Example,Head,PredictArg),
 3207			once(Body),
 3208			arg(PredictArg,Head,Pred), 
 3209			arg(PredictArg,Example,Actual)
 3210			), 
 3211		L),
 3212	sum_model_errors(L,Evalfn,0,0.0,T,E), !.
 3213
 3214sum_model_errors([],_,N,E,N,E).
 3215sum_model_errors([Act-Pred|T],Evalfn,NSoFar,ESoFar,N,E):-
 3216	get_model_error(Evalfn,Act,Pred,E1),
 3217	E1SoFar is ESoFar + E1,
 3218	N1SoFar is NSoFar + 1,
 3219	sum_model_errors(T,Evalfn,N1SoFar,E1SoFar,N,E).
 3220
 3221get_model_error(mse,Act,Pred,E):-
 3222	E is (Act-Pred)^2.
 3223get_model_error(accuracy,Act,Pred,E):-
 3224	(Act = Pred -> E is 0.0; E is 1.0).
 3225
 3226leaf_predicts(0,_,_):- !, fail.
 3227leaf_predicts(Arg,Model,Var):-
 3228	arg(Arg,Model,Var1),
 3229	var(Var1),
 3230	Var1 == Var, !.
 3231leaf_predicts(Arg,Model,Var):-
 3232	Arg1 is Arg - 1,
 3233	leaf_predicts(Arg1,Model,Var).
 3234	
 3235leaf_prediction(classification,Total-Distribution,Class,Incorrect):-
 3236	find_maj_class(Distribution,N-Class),
 3237	Incorrect is Total - N.
 3238leaf_prediction(class_probability,T1-D1,NDistr,0):-
 3239	length(D1,NClasses),
 3240	laplace_correct(D1,LaplaceD1),
 3241	LaplaceTotal is T1 + NClasses,
 3242	normalise_distribution(LaplaceD1,LaplaceTotal,NDistr).
 3243leaf_prediction(regression,_-[Mean,Sd],Mean,Sd).
 3244
 3245find_maj_class([X],X):- !.
 3246find_maj_class([N-Class|Rest],MajClass):-
 3247	find_maj_class(Rest,N1-C1),
 3248	(N > N1 -> MajClass = N-Class; MajClass = N1-C1).
 3249
 3250can_split(S,Type,Predict,Leaf,Left,Right):-
 3251	arg(21,S,MinGain),
 3252	'$aleph_search'(tree_leaf,l(Leaf,_,[Clause,Cost,N],Examples)),
 3253	Cost >= MinGain, 
 3254	get_best_subtree(S,Type,Predict,[Clause,Cost,N],Examples,Gain,Left,Right),
 3255	Gain >= MinGain,
 3256	p_message('found clauses'),
 3257	Left = [ClF,CostF|_], Right = [ClS,CostS|_],
 3258	arg(4,S,_/Evalfn),
 3259	pp_dclause(ClS),
 3260	print_eval(Evalfn,CostS),
 3261	pp_dclause(ClF),
 3262	print_eval(Evalfn,CostF),
 3263	p1_message('expected cost reduction'), p_message(Gain).
 3264
 3265get_best_subtree(S,Type,Predict,[Clause,Cost,N],Examples,Gain,Left,Right):-
 3266	arg(42,S,Interactive),
 3267	arg(43,S,LookAhead),
 3268	retractall('$aleph_search'(tree_gain,_)),
 3269	MInf is -inf,
 3270	(Interactive = false ->
 3271		asserta('$aleph_search'(tree_gain,tree_gain(MInf,[],[])));
 3272		true),
 3273	split_clause(Clause,Head,Body),
 3274	arg(4,S,_/Evalfn),
 3275	arg(13,S,MinPos),
 3276	auto_refine(LookAhead,Clause,ClS),
 3277	tree_refine_ok(Type,ClS),
 3278	eval_treenode(S,Type,ClS,Predict,Examples,ExS,NS,CostS),
 3279	NS >= MinPos,
 3280	rm_intervals(ExS,Examples,ExF),
 3281	split_clause(ClS,Head,Body1),
 3282	get_goaldiffs(Body,Body1,Diff),
 3283	extend_clause(Clause,not(Diff),ClF),
 3284	eval_treenode(S,Type,ClF,Predict,ExF,NF,CostF),
 3285	NF >= MinPos,
 3286	AvLeafCost is (NS*CostS + NF*CostF)/N,
 3287	CostReduction is Cost - AvLeafCost,
 3288	(Interactive = false ->
 3289		pp_dclause(ClS), print_eval(Evalfn,CostS),
 3290		pp_dclause(ClF), print_eval(Evalfn,CostF),
 3291		p1_message('expected cost reduction'), p_message(CostReduction),
 3292		'$aleph_search'(tree_gain,tree_gain(BestSoFar,_,_)),
 3293		CostReduction > BestSoFar,
 3294		retract('$aleph_search'(tree_gain,tree_gain(BestSoFar,_,_))),
 3295		asserta('$aleph_search'(tree_gain,tree_gain(CostReduction,
 3296							[ClF,CostF,NF,ExF],
 3297							[ClS,CostS,NS,ExS])));
 3298		asserta('$aleph_search'(tree_gain,tree_gain(CostReduction,
 3299							[ClF,CostF,NF,ExF],
 3300							[ClS,CostS,NS,ExS])))),
 3301
 3302	AvLeafCost =< 0.0, 
 3303	!,
 3304	get_best_subtree(Interactive,Clause,Gain,Left,Right).
 3305get_best_subtree(S,_,_,[Clause|_],_,Gain,Left,Right):-
 3306	arg(42,S,Interactive),
 3307	get_best_subtree(Interactive,Clause,Gain,Left,Right).
 3308
 3309get_best_subtree(false,_,Gain,Left,Right):-
 3310	retract('$aleph_search'(tree_gain,tree_gain(Gain,Left,Right))), !.
 3311get_best_subtree(true,Clause,Gain,Left,Right):-
 3312	nl, write('Extending path: '), nl,
 3313	write('---------------'), nl,
 3314	pp_dclause(Clause),
 3315	findall(MCR-[Left,Right],
 3316		('$aleph_search'(tree_gain,tree_gain(CostReduction,Left,Right)), 
 3317		  MCR is -1*CostReduction), 
 3318		SplitsList),
 3319	keysort(SplitsList,Sorted),
 3320	get_best_split(Clause,Sorted,Gain,Left,Right),
 3321	retractall('$aleph_search'(tree_gain,_)).
 3322
 3323get_best_split(Clause,Splits,Gain,Left,Right):-
 3324	show_split_list(Clause,Splits),
 3325	ask_best_split(Splits,Gain,Left,Right).
 3326
 3327show_split_list(Clause,Splits):-
 3328	tab(4), write('Split Information'), nl,
 3329	tab(4), write('-----------------'), nl, nl,
 3330	tab(4), write('No.'), 
 3331	tab(4), write('Split'), 
 3332	nl,
 3333	tab(4), write('---'), 
 3334	tab(4), write('-----'), 
 3335	nl,
 3336	show_split_list(Splits,1,Clause).
 3337
 3338show_split_list([],_,_).
 3339show_split_list([MCR-[[_,_,NF,_],[CLS,_,NS,_]]|Rest],SplitNum,Clause):-
 3340	copy_term(Clause,ClauseCopy),
 3341	split_clause(ClauseCopy,Head,Body),
 3342	copy_term(CLS,CLSCopy),
 3343	numbervars(CLSCopy,0,_),
 3344	split_clause(CLSCopy,Head,Body1),
 3345	get_goaldiffs(Body,Body1,Diff),
 3346	Gain is -1*MCR,
 3347	tab(4), write(SplitNum),
 3348	tab(4), write(Diff), nl,
 3349	tab(12), write('Succeeded (Right Branch): '), write(NS), nl,
 3350	tab(12), write('Failed    (Left Branch) : '), write(NF), nl,
 3351	tab(12), write('Cost Reduction          : '), write(Gain), nl, nl,
 3352	NextSplit is SplitNum + 1,
 3353	show_split_list(Rest,NextSplit,Clause).
 3354
 3355ask_best_split(Splits,Gain,Left,Right):-
 3356	repeat,
 3357	tab(4), write('-> '),
 3358	write('Select Split Number (or "none.")'), nl,
 3359	read(Answer),
 3360	(Answer = none ->
 3361		Gain is -inf,
 3362		Left = [],
 3363		Right = [];
 3364		SplitNum is integer(Answer),
 3365		aleph_remove_nth(SplitNum,Splits,MCR-[Left,Right],_),
 3366		Gain is -1*MCR
 3367	),
 3368	!.
 3369
 3370tree_refine_ok(model,Clause):-
 3371        '$aleph_global'(model,model(Name/Arity)),
 3372	functor(Model,Name,Arity),
 3373	in(Clause,Model), !,
 3374	fail.
 3375tree_refine_ok(_,_).
 3376
 3377
 3378eval_treenode(S,Tree,Clause,PredictArg,PCov,N,Cost):-
 3379	arg(4,S,_/Evalfn),
 3380	treenode_cost(Tree,Evalfn,Clause,PCov,PredictArg,N,Cost).
 3381
 3382eval_treenode(S,Tree,Clause,PredictArg,Pos,PCov,N,Cost):-
 3383	arg(4,S,_/Evalfn),
 3384	arg(13,S,MinPos),
 3385	arg(14,S,Depth),
 3386	arg(29,S,Time),
 3387	arg(34,S,Proof),
 3388        prove(Depth/Time/Proof,pos,Clause,Pos,PCov,PCount),
 3389	PCount >= MinPos,
 3390	treenode_cost(Tree,Evalfn,Clause,PCov,PredictArg,N,Cost).
 3391
 3392treenode_cost(model,Evalfn,Clause,Covered,PredictArg,Total,Cost):-
 3393	!,
 3394	add_model(Evalfn,Clause,PredictArg,Covered,_,Total,Cost).
 3395treenode_cost(Tree,Evalfn,_,Covered,PredictArg,Total,Cost):-
 3396	node_stats(Tree,Covered,PredictArg,Total-Distribution),
 3397	Total > 0,
 3398	impurity(Tree,Evalfn,Total-Distribution,Cost).
 3399
 3400node_stats(Tree,Covered,PredictArg,D):-
 3401        '$aleph_search'(tree_startdistribution,d(Tree,D0)),
 3402        (Tree = regression ->
 3403                cont_distribution(Covered,PredictArg,D0,D);
 3404                discr_distribution(Covered,PredictArg,D0,D)).
 3405
 3406discr_distribution([],_,D,D).
 3407discr_distribution([S-F|Intervals],PredictArg,T0-D0,D):-
 3408	discr_distribution(S,F,PredictArg,T0-D0,T1-D1),
 3409	discr_distribution(Intervals,PredictArg,T1-D1,D).
 3410
 3411discr_distribution(N,F,_,D,D):- N > F, !.
 3412discr_distribution(N,F,PredictArg,T0-D0,D):-
 3413	example(N,pos,Example),
 3414	tparg(PredictArg,Example,Actual),
 3415	N1 is N + 1,
 3416	T1 is T0 + 1,
 3417	(aleph_delete(C0-Actual,D0,D1) ->
 3418		C1 is C0 + 1,
 3419		discr_distribution(N1,F,PredictArg,T1-[C1-Actual|D1],D);
 3420		discr_distribution(N1,F,PredictArg,T1-[1-Actual|D0],D)).
 3421
 3422cont_distribution([],_,T-[S,SS],T-[Mean,Sd]):-
 3423	(T = 0 -> Mean = 0, Sd = 0;
 3424		Mean is S/T,
 3425		Sd is sqrt(SS/T - Mean*Mean)).
 3426cont_distribution([S-F|Intervals],PredictArg,T0-D0,D):-
 3427        cont_distribution(S,F,PredictArg,T0-D0,T1-D1),
 3428        cont_distribution(Intervals,PredictArg,T1-D1,D).
 3429
 3430cont_distribution(N,F,_,D,D):- N > F, !.
 3431cont_distribution(N,F,PredictArg,T0-[S0,SS0],D):-
 3432        example(N,pos,Example),
 3433        tparg(PredictArg,Example,Actual),
 3434	N1 is N + 1,
 3435        T1 is T0 + 1,
 3436	S1 is S0 + Actual,
 3437	SS1 is SS0 + Actual*Actual,
 3438        cont_distribution(N1,F,PredictArg,T1-[S1,SS1],D).
 3439
 3440impurity(regression,sd,_-[_,Sd],Sd):- !.
 3441impurity(classification,entropy,Total-Distribution,Cost):-
 3442	sum_entropy(Distribution,Total,S),
 3443	Cost is -S/(Total*log(2)), !.
 3444impurity(classification,gini,Total-Distribution,Cost):-
 3445	sum_gini(Distribution,Total,Cost), !.
 3446impurity(class_probability,entropy,Total-Distribution,Cost):-
 3447	sum_entropy(Distribution,Total,S),
 3448	Cost is -S/(Total*log(2)), !.
 3449impurity(class_probability,gini,Total-Distribution,Cost):-
 3450	sum_gini(Distribution,Total,Cost), !.
 3451impurity(_,_,_,_):-
 3452	err_message('inappropriate settings for tree_type and/or evalfn'),
 3453	fail.
 3454
 3455
 3456sum_gini([],_,0).
 3457sum_gini([N-_|Rest],Total,Sum):-
 3458	N > 0, !,
 3459	sum_gini(Rest,Total,C0),
 3460	P is N/Total,
 3461	Sum is P*(1-P) + C0.
 3462sum_gini([_|Rest],Total,Sum):-
 3463	sum_gini(Rest,Total,Sum).
 3464
 3465sum_entropy([],_,0).
 3466sum_entropy([N-_|Rest],Total,Sum):-
 3467	N > 0, !,
 3468	sum_entropy(Rest,Total,C0),
 3469	Sum is N*log(N/Total) + C0.
 3470sum_entropy([_|Rest],Total,Sum):-
 3471	sum_entropy(Rest,Total,Sum).
 3472
 3473% only binary splits
 3474% left = condition at node fails
 3475% right = condition at node succeeds
 3476split_leaf(Leaf,LeftTree,RightTree,[Left,Right]):-
 3477	retract('$aleph_search'(tree_leaf,l(Leaf,Parent,
 3478						[Clause,Cost,N],Examples))),
 3479	gen_leaf(Left),
 3480	gen_leaf(Right),
 3481	LeftTree = [ClF,CostF,NF,ExF],
 3482	RightTree = [ClS,CostS,NS,ExS],
 3483	asserta('$aleph_search'(tree,t(Leaf,Parent,[Clause,Cost,N],
 3484					Examples,Left,Right))),
 3485	asserta('$aleph_search'(tree_leaf,l(Left,Leaf,[ClF,CostF,NF],ExF))),
 3486	asserta('$aleph_search'(tree_leaf,l(Right,Leaf,[ClS,CostS,NS],ExS))).
 3487
 3488gen_leaf(Leaf1):-
 3489	retract('$aleph_search'(tree_lastleaf,Leaf0)), !,
 3490	Leaf1 is Leaf0 + 1,
 3491	asserta('$aleph_search'(tree_lastleaf,Leaf1)).
 3492gen_leaf(0):-
 3493        asserta('$aleph_search'(tree_lastleaf,0)).
 3494
 3495%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3496% G C W S
 3497
 3498% examine list of clauses to be specialised
 3499% generate an exception theory for each clause that covers negative examples
 3500gcws:-
 3501	setting(evalfn,EvalFn),
 3502	repeat,
 3503	retract('$aleph_search'(sphyp,hypothesis([P,N,L|T],Clause,PCover,NCover))),
 3504	(PCover = _/_ -> label_create(pos,Clause,Label1),
 3505		extract_pos(Label1,PCover1),
 3506		interval_count(PCover1,P1);
 3507		PCover1 = PCover,
 3508		P1 = P),
 3509	(NCover = _/_ -> label_create(neg,Clause,Label2),
 3510		extract_neg(Label2,NCover1),
 3511		interval_count(NCover1,N1);
 3512		NCover1 = NCover,
 3513		N1 = N),
 3514	(N1 = 0 -> NewClause = Clause, NewLabel = [P1,N1,L|T];
 3515		MinAcc is P1/(2*P1 - 1),
 3516		set(minacc,MinAcc),
 3517		set(noise,N1),
 3518		gcws(Clause,PCover1,NCover1,NewClause),
 3519		L1 is L + 1,
 3520		complete_label(EvalFn,NewClause,[P,0,L1],NewLabel)),
 3521	assertz('$aleph_search'(gcwshyp,hypothesis(NewLabel,NewClause,PCover1,[]))),
 3522	\+('$aleph_search'(sphyp,hypothesis(_,_,_,_))), !.
 3523
 3524
 3525% gcws(+Clause,+PCvr,+NCvr,-Clause1)
 3526%	specialise Clause that covers pos examples PCvr and neg examples NCvr
 3527%	result is is Clause extended with a single negated literal
 3528% clauses in exception theory are added to list for specialisation
 3529gcws(Clause,PCover,NCover,Clause1):-
 3530	gen_absym(AbName),
 3531	split_clause(Clause,Head,Body),
 3532	functor(Head,_,Arity),
 3533	add_determinations(AbName/Arity,true),
 3534	add_modes(AbName/Arity),
 3535	gen_ab_examples(AbName/Arity,PCover,NCover),
 3536	cwinduce,
 3537	Head =.. [_|Args],
 3538	AbLit =.. [AbName|Args],
 3539	(Body = true -> Body1 = not(AbLit) ; app_lit(not(AbLit),Body,Body1)),
 3540	Clause1 = (Head:-Body1).
 3541
 3542% greedy set-cover based construction of abnormality theory 
 3543% starts with the first exceptional example
 3544% each clause obtained is added to list of clauses to be specialised 
 3545cwinduce:-
 3546	store(greedy),
 3547        set(greedy,true),
 3548        '$aleph_global'(atoms_left,atoms_left(pos,PosSet)),
 3549        PosSet \= [],
 3550        repeat,
 3551	'$aleph_global'(atoms_left,atoms_left(pos,[Num-X|Y])),
 3552	sat(Num),
 3553	reduce,
 3554	retract('$aleph_global'(hypothesis,hypothesis(Label,H,PCover,NCover))),
 3555	asserta('$aleph_search'(sphyp,hypothesis(Label,H,PCover,NCover))),
 3556        rm_seeds1(PCover,[Num-X|Y],NewPosLeft),
 3557	retract('$aleph_global'(atoms_left,atoms_left(pos,[Num-X|Y]))),
 3558        asserta('$aleph_global'(atoms_left,atoms_left(pos,NewPosLeft))),
 3559	NewPosLeft = [],
 3560        retract('$aleph_global'(atoms_left,atoms_left(pos,NewPosLeft))),
 3561	reinstate(greedy), !.
 3562cwinduce.
 3563
 3564
 3565% gen_ab_examples(+Ab,+PCover,+NCover)
 3566% obtain examples for abnormality predicate Ab by
 3567%	pos examples are copies of neg examples in NCover
 3568%	neg examples are copies of pos examples in PCover
 3569% writes new examples to temporary ".f" and ".n" files
 3570% to ensure example/3 remains a static predicate
 3571% alters search parameters accordingly
 3572gen_ab_examples(Ab/_,PCover,NCover):-
 3573	PosFile = '.alephtmp.f',
 3574	NegFile = '.alephtmp.n',
 3575	create_examples(PosFile,Ab,neg,NCover,pos,PCover1),
 3576	create_examples(NegFile,Ab,pos,PCover,neg,NCover1),
 3577	aleph_consult(PosFile),
 3578	aleph_consult(NegFile),
 3579        retractall('$aleph_global'(atoms_left,_)),
 3580        retractall('$aleph_global'(size,_)),
 3581        asserta('$aleph_global'(atoms_left,atoms_left(pos,PCover1))),
 3582        asserta('$aleph_global'(atoms_left,atoms_left(neg,NCover1))),
 3583        interval_count(PCover1,PSize),
 3584        interval_count(NCover1,NSize),
 3585        asserta('$aleph_global'(size,size(pos,PSize))),
 3586        asserta('$aleph_global'(size,size(neg,NSize))),
 3587	delete_file(PosFile),
 3588	delete_file(NegFile).
 3589
 3590% create_examples(+File,+OldType,+OldE,+NewType,-NewE)
 3591% copy OldE examples of OldType to give NewE examples of NewType 
 3592% copy stored in File
 3593create_examples(File,Ab,OldT,OldE,NewT,[Next-Last]):-
 3594	'$aleph_global'(last_example,last_example(NewT,OldLast)),
 3595	aleph_open(File,write,Stream),
 3596	set_output(Stream),
 3597	create_copy(OldE,OldT,NewT,Ab,OldLast,Last),
 3598	close(Stream),
 3599	set_output(user_output),
 3600	Last > OldLast, !,
 3601	retract('$aleph_global'(last_example,last_example(NewT,OldLast))),
 3602	Next is OldLast + 1,
 3603	asserta('$aleph_global'(last_example,last_example(NewT,Last))).
 3604create_examples(_,_,_,_,_,[]).
 3605
 3606create_copy([],_,_,_,L,L).
 3607create_copy([X-Y|T],OldT,NewT,Ab,Num,Last):-
 3608	create_copy(X,Y,OldT,NewT,Ab,Num,Num1),
 3609	create_copy(T,OldT,NewT,Ab,Num1,Last).
 3610
 3611create_copy(X,Y,_,_,_,L,L):- X > Y, !.
 3612create_copy(X,Y,OldT,NewT,Ab,Num,Last):-
 3613	example(X,OldT,Example),
 3614	Example =.. [_|Args],
 3615	NewExample =.. [Ab|Args],
 3616	Num1 is Num + 1,
 3617	aleph_writeq(example(Num1,NewT,NewExample)), write('.'), nl,
 3618	X1 is X + 1,
 3619	create_copy(X1,Y,OldT,NewT,Ab,Num1,Last).
 3620
 3621% gen_absym(-Name)
 3622% generate new abnormality predicate symbol
 3623gen_absym(Name):-
 3624	(retract('$aleph_global'(last_ab,last_ab(N))) ->
 3625		N1 is N + 1;
 3626		N1 is 0),
 3627	asserta('$aleph_global'(last_ab,last_ab(N1))),
 3628	concat([ab,N1],Name).
 3629%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3630% C L A U S E   O P T I M I S A T I O N S
 3631
 3632
 3633optimise(Clause,Clause1):-
 3634	remove_redundant(Clause,Clause0),
 3635	reorder_clause(Clause0,Clause1).
 3636
 3637remove_redundant((Head:-Body),(Head1:-Body1)):-
 3638	goals_to_list((Head,Body),ClauseL),
 3639	remove_subsumed(ClauseL,[Head1|Body1L]),
 3640	(Body1L = [] -> Body1 = true; list_to_goals(Body1L,Body1)).
 3641
 3642reorder_clause((Head:-Body), Clause) :-
 3643        % term_variables(Head,LHead),
 3644        vars_in_term([Head],[],LHead),
 3645        number_goals_and_get_vars(Body,LHead,1,_,[],Conj),
 3646        calculate_independent_sets(Conj,[],BSets),
 3647        compile_clause(BSets,Head,Clause).
 3648
 3649number_goals_and_get_vars((G,Body),LHead,I0,IF,L0,[g(I0,LVF,NG)|LGs]) :- !,
 3650        I is I0+1,
 3651        get_goal_vars(G,LHead,LVF,NG),
 3652        number_goals_and_get_vars(Body,LHead,I,IF,L0,LGs).
 3653number_goals_and_get_vars(G,LHead,I,I,L0,[g(I,LVF,NG)|L0]) :-
 3654        get_goal_vars(G,LHead,LVF,NG).
 3655
 3656get_goal_vars(G,LHead,LVF,G) :-
 3657        % term_variables(G,LV0),
 3658        vars_in_term([G],[],LVI),
 3659        aleph_ord_subtract(LVI,LHead,LVF).
 3660
 3661calculate_independent_sets([],BSets,BSets).
 3662calculate_independent_sets([G|Ls],BSets0,BSetsF) :-
 3663        add_goal_to_set(G,BSets0,BSetsI),
 3664        calculate_independent_sets(Ls,BSetsI,BSetsF).
 3665
 3666add_goal_to_set(g(I,LV,G),Sets0,SetsF) :-
 3667        add_to_sets(Sets0,LV,[g(I,LV,G)],SetsF).
 3668
 3669add_to_sets([],LV,Gs,[[LV|Gs]]).
 3670add_to_sets([[LV|Gs]|Sets0],LVC,GsC,[[LV|Gs]|SetsF]) :-
 3671        aleph_ord_disjoint(LV,LVC), !,
 3672        add_to_sets(Sets0,LVC,GsC,SetsF).
 3673add_to_sets([[LV|Gs]|Sets0],LVC,GsC,SetsF) :-
 3674        aleph_ord_union(LV,LVC,LVN),
 3675        join_goals(Gs,GsC,GsN),
 3676        add_to_sets(Sets0,LVN,GsN,SetsF).
 3677
 3678join_goals([],L,L):- !.
 3679join_goals(L,[],L):- !.
 3680join_goals([g(I1,VL1,G1)|T],[g(I2,VL2,G2)|T2],Z) :-
 3681        I1 < I2, !,
 3682        Z = [g(I1,VL1,G1)|TN],
 3683        join_goals(T,[g(I2,VL2,G2)|T2],TN).
 3684join_goals([H|T],[g(I2,VL2,G2)|T2],Z) :-
 3685        Z = [g(I2,VL2,G2)|TN],
 3686        join_goals(T,[H|T2],TN).
 3687
 3688compile_clause(Goals,Head,(Head:-Body)):-
 3689        compile_clause2(Goals,Body).
 3690
 3691compile_clause2([[_|B]], B1):-
 3692	!,
 3693        glist_to_goals(B,B1).
 3694compile_clause2([[_|B]|Bs],(B1,!,NB)):-
 3695        glist_to_goals(B,B1),
 3696        compile_clause2(Bs,NB).
 3697
 3698glist_to_goals([g(_,_,Goal)],Goal):- !.
 3699glist_to_goals([g(_,_,Goal)|Goals],(Goal,Goals1)):-
 3700        glist_to_goals(Goals,Goals1).
 3701
 3702% remove literals subsumed in the body of a clause
 3703remove_subsumed([Head|Lits],Lits1):-
 3704	delete(Lit,Lits,Left),
 3705	\+(\+(redundant(Lit,[Head|Lits],[Head|Left]))), !,
 3706	remove_subsumed([Head|Left],Lits1).
 3707remove_subsumed(L,L).
 3708
 3709% determine if Lit is subsumed by a body literal
 3710redundant(Lit,Lits,[Head|Body]):-
 3711	copy_term([Head|Body],Rest1),
 3712	member(Lit1,Body),
 3713	Lit = Lit1,
 3714	aleph_subsumes(Lits,Rest1).
 3715
 3716aleph_subsumes(Lits,Lits1):-
 3717	\+(\+((numbervars(Lits,0,_),numbervars(Lits1,0,_),aleph_subset1(Lits,Lits1)))).
 3718
 3719
 3720%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 3721% S A T  /  R E D U C E
 3722
 3723sat(Num):-
 3724	integer(Num),
 3725	example(Num,pos,_),
 3726	sat(pos,Num), !.
 3727sat(Example):-
 3728	record_example(check,uspec,Example,Num),
 3729	sat(uspec,Num), !.
 3730
 3731sat(Type,Num):-
 3732        setting(construct_bottom,false), !,
 3733        sat_prelims,
 3734	example(Num,Type,Example),
 3735	broadcast(start(sat(Num))),
 3736	p1_message('sat'), p_message(Num), p_message(Example),
 3737	record_sat_example(Num),
 3738	asserta('$aleph_sat'(example,example(Num,Type))),
 3739	asserta('$aleph_sat'(hovars,[])),
 3740	broadcast(end(sat(Num, 0, 0.0))).
 3741sat(Type,Num):-
 3742	setting(construct_bottom,reduction), !,
 3743	sat_prelims,
 3744	example(Num,Type,Example),
 3745	broadcast(start(sat(Num))),
 3746	p1_message('sat'), p_message(Num), p_message(Example),
 3747	record_sat_example(Num),
 3748	asserta('$aleph_sat'(example,example(Num,Type))),
 3749	integrate_head_lit(HeadOVars),
 3750	asserta('$aleph_sat'(hovars,HeadOVars)),
 3751	broadcast(end(sat(Num, 0, 0.0))).
 3752sat(Type,Num):-
 3753	set(stage,saturation),
 3754	sat_prelims,
 3755	example(Num,Type,Example),
 3756	broadcast(start(sat(Num))),
 3757	p1_message('sat'), p_message(Num), p_message(Example),
 3758	record_sat_example(Num),
 3759	asserta('$aleph_sat'(example,example(Num,Type))),
 3760	split_args(Example,Mode,Input,Output,Constants),
 3761	integrate_args(unknown,Example,Output),
 3762	stopwatch(StartClock),
 3763	assertz('$aleph_sat_atom'(Example,mode(Mode,Output,Input,Constants))),
 3764	'$aleph_global'(i,set(i,Ival)),
 3765	flatten(0,Ival,0,Last1),
 3766	'$aleph_sat_litinfo'(1,_,Atom,_,_,_),
 3767	get_vars(Atom,Output,HeadOVars),
 3768	asserta('$aleph_sat'(hovars,HeadOVars)),
 3769	get_vars(Atom,Input,HeadIVars),
 3770	asserta('$aleph_sat'(hivars,HeadIVars)),
 3771	functor(Example,Name,Arity), 
 3772	get_determs(Name/Arity,L),
 3773	('$aleph_global'(determination,determination(Name/Arity,'='/2))->
 3774		asserta('$aleph_sat'(eq,true));
 3775		asserta('$aleph_sat'(eq,false))),
 3776	get_atoms(L,1,Ival,Last1,Last),
 3777	stopwatch(StopClock),
 3778	Time is StopClock - StartClock,
 3779	asserta('$aleph_sat'(lastlit,Last)),
 3780	asserta('$aleph_sat'(botsize,Last)),
 3781	update_generators,
 3782	rm_moderepeats(Last,Repeats),
 3783	rm_commutative(Last,Commutative),
 3784	rm_symmetric(Last,Symmetric),
 3785	rm_redundant(Last,Redundant),
 3786	rm_uselesslits(Last,NotConnected),
 3787	rm_nreduce(Last,NegReduced),
 3788	TotalLiterals is
 3789		Last-Repeats-NotConnected-Commutative-Symmetric-Redundant-NegReduced,
 3790	show(bottom),
 3791	p1_message('literals'), p_message(TotalLiterals),
 3792	p1_message('saturation time'), p_message(Time),
 3793	broadcast(end(sat(Num, TotalLiterals, Time))),
 3794	store(bottom),
 3795	noset(stage).
 3796sat(_,_):-
 3797	noset(stage).
 3798
 3799reduce:-
 3800	setting(search,Search), 
 3801	catch(reduce(Search),abort,reinstate_values), !.
 3802
 3803% no search: add bottom clause as hypothesis
 3804reduce(false):-
 3805	!,
 3806	add_bottom.
 3807% iterative beam search as described by Ross Quinlan+MikeCameron-Jones,IJCAI-95
 3808reduce(ibs):-
 3809	!,
 3810	retractall('$aleph_search'(ibs_rval,_)),
 3811	retractall('$aleph_search'(ibs_nodes,_)),
 3812	retractall('$aleph_search'(ibs_selected,_)),
 3813	store_values([openlist,caching,explore]),
 3814	set(openlist,1),
 3815	set(caching,true),
 3816	set(explore,true),
 3817	asserta('$aleph_search'(ibs_rval,1.0)),
 3818	asserta('$aleph_search'(ibs_nodes,0)),
 3819	setting(evalfn,Evalfn),
 3820	get_start_label(Evalfn,Label),
 3821	('$aleph_sat'(example,example(Num,Type)) ->
 3822		example(Num,Type,Example),
 3823		asserta('$aleph_search'(ibs_selected,selected(Label,(Example:-true),
 3824				[Num-Num],[])));
 3825		asserta('$aleph_search'(ibs_selected,selected(Label,(false:-true),
 3826				[],[])))),
 3827	stopwatch(Start),
 3828	repeat,
 3829	setting(openlist,OldOpen),
 3830	p1_message('ibs beam width'), p_message(OldOpen),
 3831	find_clause(bf),
 3832	'$aleph_search'(current,current(_,Nodes0,[PC,NC|_]/_)),
 3833	N is NC + PC,
 3834	estimate_error_rate(Nodes0,0.5,N,NC,NewR),
 3835	p1_message('ibs estimated error'), p_message(NewR),
 3836	retract('$aleph_search'(ibs_rval,OldR)),
 3837	retract('$aleph_search'(ibs_nodes,Nodes1)),
 3838        '$aleph_search'(selected,selected(BL,RCl,PCov,NCov)),
 3839	NewOpen is 2*OldOpen,
 3840	Nodes2 is Nodes0 + Nodes1,
 3841	set(openlist,NewOpen),
 3842	asserta('$aleph_search'(ibs_rval,NewR)),
 3843	asserta('$aleph_search'(ibs_nodes,Nodes2)),
 3844	((NewR >= OldR; NewOpen > 512) -> true;
 3845		retract('$aleph_search'(ibs_selected,selected(_,_,_,_))),
 3846		asserta('$aleph_search'(ibs_selected,selected(BL,RCl,PCov,NCov))),
 3847		fail),
 3848	!,
 3849	stopwatch(Stop),
 3850	Time is Stop - Start,
 3851	retractall('$aleph_search'(ibs_rval,_)),
 3852	retract('$aleph_search'(ibs_nodes,Nodes)),
 3853        retract('$aleph_search'(ibs_selected,selected(BestLabel,RClause,PCover,NCover))),
 3854	add_hyp(BestLabel,RClause,PCover,NCover),
 3855	p1_message('ibs clauses constructed'), p_message(Nodes),
 3856	p1_message('ibs search time'), p_message(Time),
 3857	p_message('ibs best clause'),
 3858	pp_dclause(RClause),
 3859	show_stats(Evalfn,BestLabel),
 3860	record_search_stats(RClause,Nodes,Time),
 3861	reinstate_values([openlist,caching,explore]).
 3862
 3863% iterative deepening search
 3864reduce(id):-
 3865	!,
 3866	retractall('$aleph_search'(id_nodes,_)),
 3867	retractall('$aleph_search'(id_selected,_)),
 3868	store_values([caching,clauselength]),
 3869	setting(clauselength,MaxCLen),
 3870	set(clauselength,1),
 3871	set(caching,true),
 3872	asserta('$aleph_search'(id_nodes,0)),
 3873	setting(evalfn,Evalfn),
 3874	get_start_label(Evalfn,Label),
 3875	('$aleph_sat'(example,example(Num,Type)) ->
 3876		example(Num,Type,Example),
 3877		asserta('$aleph_search'(id_selected,selected(Label,(Example:-true),
 3878				[Num-Num],[])));
 3879		asserta('$aleph_search'(id_selected,selected(Label,(false:-true),
 3880				[],[])))),
 3881	stopwatch(Start),
 3882	repeat,
 3883	setting(clauselength,OldCLen),
 3884	p1_message('id clauselength setting'), p_message(OldCLen),
 3885	find_clause(df),
 3886	'$aleph_search'(current,current(_,Nodes0,_)),
 3887	retract('$aleph_search'(id_nodes,Nodes1)),
 3888        '$aleph_search'(selected,selected([P,N,L,F|T],RCl,PCov,NCov)),
 3889	'$aleph_search'(id_selected,selected([_,_,_,F1|_],_,_,_)),
 3890	NewCLen is OldCLen + 1,
 3891	Nodes2 is Nodes0 + Nodes1,
 3892	set(clauselength,NewCLen),
 3893	'$aleph_search'(id_nodes,Nodes2),
 3894	(F1 >= F -> true;
 3895		retract('$aleph_search'(id_selected,selected([_,_,_,F1|_],_,_,_))),
 3896		asserta('$aleph_search'(id_selected,selected([P,N,L,F|T],RCl,PCov,NCov))),
 3897		set(best,[P,N,L,F|T])),
 3898	NewCLen > MaxCLen,
 3899	!,
 3900	stopwatch(Stop),
 3901	Time is Stop - Start,
 3902	retract('$aleph_search'(id_nodes,Nodes)),
 3903        retract('$aleph_search'(id_selected,selected(BestLabel,RClause,PCover,NCover))),
 3904	add_hyp(BestLabel,RClause,PCover,NCover),
 3905	p1_message('id clauses constructed'), p_message(Nodes),
 3906	p1_message('id search time'), p_message(Time),
 3907	p_message('id best clause'),
 3908	pp_dclause(RClause),
 3909	show_stats(Evalfn,BestLabel),
 3910	record_search_stats(RClause,Nodes,Time),
 3911	noset(best),
 3912	reinstate_values([caching,clauselength]).
 3913
 3914% iterative language search as described by Rui Camacho, 1996
 3915reduce(ils):-
 3916	!,
 3917	retractall('$aleph_search'(ils_nodes,_)),
 3918	retractall('$aleph_search'(ils_selected,_)), 
 3919	store_values([caching,language]),
 3920	set(searchstrat,bf),
 3921	set(language,1),
 3922	set(caching,true),
 3923	asserta('$aleph_search'(ils_nodes,0)),
 3924	setting(evalfn,Evalfn),
 3925	get_start_label(Evalfn,Label),
 3926	('$aleph_sat'(example,example(Num,Type)) ->
 3927		example(Num,Type,Example),
 3928		asserta('$aleph_search'(ils_selected,selected(Label,(Example:-true),
 3929				[Num-Num],[])));
 3930		asserta('$aleph_search'(ils_selected,selected(Label,(false:-true),
 3931				[],[])))),
 3932	stopwatch(Start),
 3933	repeat,
 3934	setting(language,OldLang),
 3935	p1_message('ils language setting'), p_message(OldLang),
 3936	find_clause(bf),
 3937	'$aleph_search'(current,current(_,Nodes0,_)),
 3938	retract('$aleph_search'(ils_nodes,Nodes1)),
 3939        '$aleph_search'(selected,selected([P,N,L,F|T],RCl,PCov,NCov)),
 3940	'$aleph_search'(ils_selected,selected([_,_,_,F1|_],_,_,_)),
 3941	NewLang is OldLang + 1,
 3942	Nodes2 is Nodes0 + Nodes1,
 3943	set(language,NewLang),
 3944	asserta('$aleph_search'(ils_nodes,Nodes2)),
 3945	(F1 >= F -> true;
 3946		retract('$aleph_search'(ils_selected,selected([_,_,_,F1|_],_,_,_))),
 3947		asserta('$aleph_search'(ils_selected,selected([P,N,L,F|T],RCl,PCov,NCov))),
 3948		set(best,[P,N,L,F|T]),
 3949		fail),
 3950	!,
 3951	stopwatch(Stop),
 3952	Time is Stop - Start,
 3953	retract('$aleph_search'(ils_nodes,Nodes)),
 3954        retract('$aleph_search'(ils_selected,selected(BestLabel,RClause,PCover,NCover))),
 3955	add_hyp(BestLabel,RClause,PCover,NCover),
 3956	p1_message('ils clauses constructed'), p_message(Nodes),
 3957	p1_message('ils search time'), p_message(Time),
 3958	p_message('ils best clause'),
 3959	pp_dclause(RClause),
 3960	show_stats(Evalfn,BestLabel),
 3961	record_search_stats(RClause,Nodes,Time),
 3962	noset(best),
 3963	reinstate_values([caching,language]).
 3964
 3965
 3966% implementation of a randomised local search for clauses
 3967% currently, this can use either: simulated annealing with a fixed temp
 3968% or a GSAT-like algorithm
 3969% the choice of these is specified by the parameter: rls_type
 3970% both annealing and GSAT employ random multiple restarts
 3971% and a limit on the number of moves
 3972%	the number of restarts is specified by set(tries,...)
 3973%	the number of moves is specified by set(moves,...)
 3974% annealing currently restricted to using a fixed temperature
 3975%	the temperature is specified by set(temperature,...)
 3976%	the use of a fixed temp. makes it equivalent to the Metropolis alg.
 3977% GSAT if given a ``random-walk probability'' performs Selman et als walksat
 3978%	the walk probability is specified by set(walk,...)
 3979%	a walk probability of 0 is equivalent to doing standard GSAT
 3980reduce(rls):-
 3981	!,
 3982	setting(tries,MaxTries),
 3983	MaxTries >= 1,
 3984	store_values([caching,refine,refineop]),
 3985	set(searchstrat,heuristic),
 3986	set(caching,true),
 3987	setting(refine,Refine),
 3988	(Refine \= false  -> true; set(refineop,rls)),
 3989	setting(threads,Threads),
 3990	rls_search(Threads, MaxTries, Time, Nodes, selected(BestLabel,
 3991					RBest,PCover,NCover)),
 3992	add_hyp(BestLabel,RBest,PCover,NCover),
 3993	p1_message('rls nodes constructed'), p_message(Nodes),
 3994	p1_message('rls search time'), p_message(Time),
 3995	p_message('rls best result'),
 3996	pp_dclause(RBest),
 3997	setting(evalfn,Evalfn),
 3998	show_stats(Evalfn,BestLabel),
 3999	record_search_stats(RBest,Nodes,Time),
 4000	noset(best),
 4001	reinstate_values([caching,refine,refineop]).
 4002
 4003
 4004% stochastic clause selection based on ordinal optimisation
 4005% see papers by Y.C. Ho and colleagues for more details
 4006reduce(scs):-
 4007	!,
 4008	store_values([tries,moves,rls_type,clauselength_distribution]),
 4009	stopwatch(Start),
 4010	(setting(scs_sample,SampleSize) -> true;
 4011		setting(scs_percentile,K),
 4012		K > 0.0,
 4013		setting(scs_prob,P),
 4014		P < 1.0,
 4015		SampleSize is integer(log(1-P)/log(1-K/100) + 1)),
 4016	(setting(scs_type,informed)->
 4017		(setting(clauselength_distribution,_D) -> true;
 4018			setting(clauselength,CL),
 4019			estimate_clauselength_distribution(CL,100,K,D),
 4020			% max_in_list(D,Prob-Length),
 4021			% p1_message('using clauselength distribution'),
 4022			% p_message([Prob-Length]),
 4023			% set(clauselength_distribution,[Prob-Length]));
 4024			p1_message('using clauselength distribution'),
 4025			p_message(D),
 4026			set(clauselength_distribution,D));
 4027		true),
 4028	set(tries,SampleSize),
 4029	set(moves,0),
 4030	set(rls_type,gsat),
 4031	reduce(rls),
 4032	stopwatch(Stop),
 4033	Time is Stop - Start,
 4034	'$aleph_search'(rls_nodes,Nodes),
 4035        '$aleph_search'(rls_selected,selected(BestLabel,RBest,_,_)),
 4036	p1_message('scs nodes constructed'), p_message(Nodes),
 4037	p1_message('scs search time'), p_message(Time),
 4038	p_message('scs best result'),
 4039	pp_dclause(RBest),
 4040	setting(evalfn,Evalfn),
 4041	show_stats(Evalfn,BestLabel),
 4042	record_search_stats(RBest,Nodes,Time),
 4043	p1_message('scs search time'), p_message(Time),
 4044	reinstate_values([tries,moves,rls_type,clauselength_distribution]).
 4045
 4046% simple association rule search
 4047% For a much more sophisticated approach see: L. Dehaspe, PhD Thesis, 1998
 4048% Here, simply find all rules within search that cover at least
 4049% a pre-specificed fraction of the positive examples
 4050reduce(ar):-
 4051	!,
 4052	clear_cache,
 4053	(setting(pos_fraction,PFrac) -> true;
 4054		p_message('value required for pos_fraction parameter'),
 4055		fail),
 4056        '$aleph_global'(atoms_left,atoms_left(pos,Pos)),
 4057	retract('$aleph_global'(atoms_left,atoms_left(neg,Neg))),
 4058	interval_count(Pos,P),
 4059	MinPos is PFrac*P,
 4060	store_values([minpos,evalfn,explore,caching,minacc,good]),
 4061	set(searchstrat,bf),
 4062	set(minpos,MinPos),
 4063	set(evalfn,coverage),
 4064	set(explore,true),
 4065	set(caching,true),
 4066	set(minacc,0.0),
 4067	set(good,true),
 4068	asserta('$aleph_global'(atoms_left,atoms_left(neg,[]))),
 4069	find_clause(bf),
 4070	show(good),
 4071	retract('$aleph_global'(atoms_left,atoms_left(neg,[]))),
 4072	asserta('$aleph_global'(atoms_left,atoms_left(neg,Neg))),
 4073	reinstate_values([minpos,evalfn,explore,caching,minacc,good]).
 4074
 4075% search for integrity constraints
 4076% modelled on the work by L. De Raedt and L. Dehaspe, 1996
 4077reduce(ic):-
 4078	!,
 4079	store_values([minpos,minscore,evalfn,explore,refineop]),
 4080	setting(refineop,RefineOp),
 4081	(RefineOp = false -> set(refineop,auto); true),
 4082	set(minpos,0),
 4083	set(searchstrat,bf),
 4084	set(evalfn,coverage),
 4085	set(explore,true),
 4086	setting(noise,N),
 4087	MinScore is -N,
 4088	set(minscore,MinScore),
 4089	find_clause(bf),
 4090	reinstate_values([minpos,minscore,evalfn,explore,refineop]).
 4091
 4092reduce(bf):-
 4093	!,
 4094	find_clause(bf).
 4095
 4096reduce(df):-
 4097	!,
 4098	find_clause(df).
 4099
 4100reduce(heuristic):-
 4101	!,
 4102	find_clause(heuristic).
 4103
 4104
 4105% find_clause(Search) where Search is one of bf, df, heuristic
 4106find_clause(Search):-
 4107	set(stage,reduction),
 4108	set(searchstrat,Search),
 4109	p_message('reduce'),
 4110	reduce_prelims(L,P,N),
 4111	asserta('$aleph_search'(openlist,[])),
 4112	get_search_settings(S),
 4113	arg(4,S,_/Evalfn),
 4114	get_start_label(Evalfn,Label),
 4115	('$aleph_sat'(example,example(Num,Type)) ->
 4116		example(Num,Type,Example),
 4117		asserta('$aleph_search'(selected,selected(Label,(Example:-true),
 4118							[Num-Num],[])));
 4119		asserta('$aleph_search'(selected,selected(Label,(false:-true),[],[])))),
 4120	arg(13,S,MinPos),
 4121	interval_count(P,PosLeft),
 4122	PosLeft >= MinPos,
 4123	'$aleph_search'(selected,selected(L0,C0,P0,N0)),
 4124	add_hyp(L0,C0,P0,N0),
 4125        ('$aleph_global'(max_set,max_set(Type,Num,Label1,ClauseNum))->
 4126		BestSoFar = Label1/ClauseNum;
 4127		('$aleph_global'(best,set(best,Label2))->
 4128			BestSoFar = Label2/0;
 4129			BestSoFar = Label/0)),
 4130        asserta('$aleph_search'(best_label,BestSoFar)),
 4131	p1_message('best label so far'), p_message(BestSoFar),
 4132        arg(3,S,RefineOp),
 4133	stopwatch(StartClock),
 4134        (RefineOp = false ->
 4135                get_gains(S,0,BestSoFar,[],false,[],0,L,[1],P,N,[],1</