% Post processing of the induce_max solution 
% Best first general -> specific reduction of a set of clauses
% 	bounded by maximum number of nodes to be searched (use: set(nodes,...))
% Normal T-Reduce mode is to use a compression-based heuristic: ie P - N - L
%	where P = Positives covered by entire theory
%      	N = Negatives covered by entire theory
%      	L = Number of clauses in the theory
% This mode is set automatically (set(treduce,compression)
% Tie-break can be either on training set accuracy (use: set(tiebreak,acc) -- default)
% 	or on number of clauses (use: set(tiebreak,tsize))
% T-Reduce can use positive examples only by: set(treduce,posonly)
%	in this case, tie-break is automatically set to to tsize
% T-Reduce can do a greedy cover-set processing by setting openlist to some number
%	(use: set(openlist,...))
% Yucky feature: because Yap is compiled, need to declare the target
% 	predicate as dynamic before loading any files
% After this declaration, T-Reduce eats Aleph files and a theory
% 	and does the general -> specific reduction
% So, a suggested way for reducing theories for p/1 is:
%	yap -s5000 -h20000
%		[treduce].
%		dynamic p/1.
%		read_all(train).	% the Aleph input files
%		[hyp].			% induce_max theory in hyp.pl
%		treduce(p/1).

treduce_version('2.0').

:- op(500,fy,#).
:- op(500,fy,*).

:- system_predicate(false,false), hide(false).


index_theory(Name/Arity):-
	functor(Lit,Name,Arity),
	retractall(treduce_dyn,last_clause(_)),
	recorda(treduce_dyn,last_clause(0),_),
	index_clauses(Lit).

index_clauses(Head):-
	clause(Head,Body,_),
	p_message('indexing clause'), p_message((Head:-Body)),
	not(ground((Head:-Body))),
	goals_to_list(Body,BodyL),
	not(exists_duplicate([Head|BodyL])),
	recorded(treduce_dyn,last_clause(Last),Key),
	erase(Key),
	N1 is Last + 1,
	p1_message('indexed as'), p_message(N1),
	length([Head|BodyL],ClauseLength),
	recorda(treduce_dyn,last_clause(N1),_),
	recordz(treduce,theory(N1,ClauseLength,[Head|BodyL]),_),
	fail.
index_clauses(_).

cache_covers([],_,_).
cache_covers([Clause|Clauses],P,N):-
	theory_prove(pos,[Clause],P,PCvr,PCount),
	theory_prove(neg,[Clause],N,NCvr,NCount),
	recorda(treduce_dyn,covers(Clause,pos,PCvr,PCount),_),
	recorda(treduce_dyn,covers(Clause,neg,NCvr,NCount),_),
	p1_message(Clause), p_message(PCount/NCount),
	cache_covers(Clauses,P,N).

treduce(Name/Arity):-
	p_message('treduce'),
	set(record,false),
	index_theory(Name/Arity),
	p_message('theory indexed'),
	recorded(treduce_dyn,last_clause(LastClause),_),
	interval_to_list(1-LastClause,Clauses),
	recorded(treduce,atoms(pos,P),_),
	recorded(treduce,atoms(neg,N),_),
	p_message('caching individual clause coverage'),
	cache_covers(Clauses,P,N),
	compute_covers(pos,Clauses,PCvr,PCount),
	compute_covers(neg,Clauses,NCvr,NCount),
	NClauses is LastClause,
	compression_ok(PCount,NCount,NClauses,BestCompr,Compress),
	recorded(treduce,size(pos,TotP),_), recorded(treduce,size(neg,TotN),_),
	Tn is TotN - NCount,
	get_tiebreak([PCount,Tn,TotP,TotN,NClauses],TB),
	retractall(openlist,_),
	recorda(openlist,[],_),
	recorda(search,selected(Clauses,PCvr,NCvr),_),
        recorda(search,nextnode(0),_),
	recorda(nodes,node(0,Clauses,PCount,NCount,NClauses/TB),_),
	recorda(search,current(0,0,[Compress/0/TB]),_),
	show_theory(Compress,Clauses,TB),
	StartClock is cputime,
	search_theory(Searched,Nodes),
	StopClock is cputime,
	Time is StopClock - StartClock,
	recorded(search,selected(AllClauses,PCover,NCover),_),
	p1_message('nodes constructed'), p_message(Nodes),
	p1_message('nodes expanded'), p_message(Searched),
	p1_message('search time'), p_message(Time),
	p1_message('T-Reduce final theory'), p_message(AllClauses),
	show_indexedclauses(AllClauses),
	clean_up,
	!.

search_theory(Searched,Nodes):-
	recorded(search,nextnode(Node),Key),
	erase(Key),
	recorded(search,current(Last,NSearch,BestSoFar),Key1),
	NSearch1 is NSearch + 1,
	recorded(nodes,node(Node,Theory,_,_,NClauses/_),Key2),
	erase(Key2),
	get_theorygains(Last,Theory,BestSoFar,NClauses,Last1,NextBest),
	continue_search(NextBest),
	prune_open(NextBest),
	erase(Key1),
	get_nextbest,
	recorda(search,current(Last1,NSearch1,NextBest),_),
	fail.
search_theory(Searched,Nodes):-
	get_node_stats(Searched,Nodes).

get_node_stats(Searched,Nodes):-
	recorded(search,current(Nodes,Searched,_),Key),
	erase(Key).

continue_search(_):-
        recorded(search,current(Nodes,Searched,_),_),
        recorded(treduce,set(nodes,MaxNodes),_),
        Searched > MaxNodes, !,
        fail.
continue_search(_).

get_theorygains(Last,Theory,BestSoFar,NClauses,Last1,NextBest):-
	retractall(treduce_dyn,node_count(_)),
	retractall(treduce_dyn,best(_)),
	recorda(treduce_dyn,node_count(Last),_),
	recorda(treduce_dyn,best(BestSoFar),_),
	NClauses1 is NClauses - 1,
	delete(Clause,Theory,Clauses),
	not(recorded(treduce_dyn,seen(Clauses),_)),
	recorda(treduce_dyn,seen(Clauses),_),
	compute_covers(pos,Clauses,PCover,PCount),
	(recorded(treduce,set(treduce,posonly),_)->
		NCover = [],
		NCount = 0;
		compute_covers(neg,Clauses,NCover,NCount)),
	compression_ok(PCount,NCount,NClauses1,BestCompr,Compress),
	recorded(treduce,size(pos,TotP),_), recorded(treduce,size(neg,TotN),_),
	Tn is TotN - NCount,
	get_tiebreak([PCount,Tn,TotP,TotN,NClauses1],TB),
	% p1_message('clauses'), p1_message(Clauses), p_message(Compress/TB),
	recorded(treduce_dyn,best(Best),Key2),
	recorded(treduce_dyn,node_count(Last1),Key),
	Node1 is Last1 + 1,
	update_besttheory(Clauses,PCover,NCover,Best,[Compress/Node1/TB],Best1),
	(Best \= Best1 -> erase(Key2), recorda(treduce_dyn,best(Best1),_);
		true),
	NClauses1 > 1,
	erase(Key),
	recorda(treduce_dyn,node_count(Node1),_),
	print_node_count(Node1),
	recorda(nodes,node(Node1,Clauses,PCount,NCount,NClauses1/TB),_),
	update_open_list(Compress,BestCompr,Node1),
	fail.
get_theorygains(_,_,_,_,Last,Best):-
	recorded(treduce_dyn,node_count(Last),Key1),
	recorded(treduce_dyn,best(Best),Key2),
	erase(Key1), erase(Key2).

get_tiebreak([Tp,Tn,TotP,TotN,Clauses],TB):-
	recorded(treduce,set(tiebreak,acc),_), !,
	TB is (Tp+Tn)/(TotP+TotN).
get_tiebreak([Tp,Tn,TotP,TotN,Clauses],TB):-
	recorded(treduce,set(tiebreak,tsize),_), !,
	TB is -Clauses.

compute_covers(Type,Clauses,Cover,Count):-
	compute_listcovers(Type,Clauses,Cover),
	interval_count(Cover,Count).

compute_listcovers(_,[],[]).
compute_listcovers(Type,[Clause|Clauses],Cover):-
	compute_listcovers(Type,Clauses,Cover1),
	recorded(treduce_dyn,covers(Clause,Type,Cvr,_),_),
	intervals_intersection(Cvr,Cover1,Intersection),
	rm_intervals(Intersection,Cover1,Cover1Left),
	append(Cover1Left,Cvr,Cover).
	
show_nodes(nodes):-
	recorded(nodes,A,_),
	write(A), nl,nl,
	fail.
show_nodes(_).

print_node_count(NodeNum):-
        N is NodeNum mod 5000,
        (N = 0-> p1_message('nodes explored'),p_message(NodeNum); true).

compression_ok(PCount,NCount,TheoryCost,BestCompr,EstCompr):-
	recorded(treduce,set(treduce,compression),_), !,
	EstCompr is PCount - NCount - TheoryCost,
	BestCompr is PCount - 1,
	(BestCompr > 0), !.
compression_ok(PCount,_,_,PCount,PCount).


get_clauselength(Clause,L):-
	recorded(treduce,theory(Clause,L,_),_).


update_besttheory(Clauses,PCover,NCover,[Best/_/_],[Compress/Node/Acc],[Compress/Node/Acc]):-
	Compress > Best, !,
	recorded(search,selected(_,_,_),Key),
	erase(Key),
	recorda(search,selected(Clauses,PCover,NCover),_),
	show_theory(Compress,Clauses,Acc),
	record_theory(Compress,Clauses,Acc), !.
update_besttheory(Clauses,PCover,NCover,[Compress/_/A],[Compress/Node1/A1],[Compress/Node1/A1]):-
	A1 > A, !,
	recorded(search,selected(_,_,_),Key),
	erase(Key),
	recorda(search,selected(Clauses,PCover,NCover),_),
	show_theory(Compress,Clauses,A1),
	record_theory(Compress,Clauses,A1), !.
update_besttheory(_,_,_,Best,_,Best).

record_theory(Compression,Clauses,Accuracy):-
	recorded(treduce,set(record,true),_),
	recorded(treduce,set(recordfile,File),_), !,
	open(File,append,Stream),
	set_output(Stream),
	p_message('T-Reduce'),
	show_theory(Compression,Clauses,Accuracy),
	p_message('clauses in theory'),
	show_indexedclauses(Clauses),
	close(Stream),
	set_output(user_output).
record_theory(_,_,_).

record_search_stats(Nodes,Searched,Time):-
        recorded(treduce,set(record,true),_),
        recorded(treduce,set(recordfile,File),_), !,
        open(File,append,Stream),
        set_output(Stream),
        p1_message('nodes constructed'), p_message(Nodes),
        p1_message('nodes expanded'), p_message(Searched),
        p1_message('search time'), p_message(Time),
        close(Stream),
        set_output(user_output).
record_search_stats(_,_,_).

show_theory(Compression,Clauses,Accuracy):-
	p1_message('found theory'), p1_message(Clauses),
	p_message(Compression/Accuracy).

show_indexedclauses(Clauses):-
	member(Clause,Clauses),
	recorded(treduce,theory(Clause,_,Literals),_),
	pp_dclause(Literals),
	fail.
show_indexedclauses(_).


get_node([Gain|_],Key,Node):-
        recorded(gains,gain(Gain,Node),Key).
get_node([_|Gains],Key,Node):-
	get_node(Gains,Key,Node).

update_open_list(GainVal,Best,Node):-
        recordz(gains,gain(GainVal,Node),_),
        recorded(openlist,OpenList,Key),
        erase(Key),
        uniq_insert(descending,GainVal,OpenList,List1),
        recorda(openlist,List1,_), !.

restrict_open:-
        recorded(treduce,set(openlist,Size),_),
        retractall(treduce_dyn,in_beam(_)),
        recorda(treduce_dyn,in_beam(0),_),
        recorded(openlist,Gains,_),
        get_node(Gains,Key,NodeNum),
        recorded(treduce_dyn,in_beam(N),Key1),
        (N < Size->
                erase(Key1),
                N1 is N + 1,
                recorda(treduce_dyn,in_beam(N1),_);
                erase(Key),
                p1_message('non-admissible removal (resource bound)'), p_message(NodeNum),
		recorded(nodes,node(NodeNum,_,_,_,_),Key2),
		erase(Key2)),
        fail.
restrict_open.

prune_open(_):-
        recorded(treduce,set(beam,Size),_), 
        retractall(treduce_dyn,in_beam(_)),
        recorda(treduce_dyn,in_beam(0),_),
        recorded(openlist,Gains,_),
        get_node(Gains,Key,NodeNum),
        recorded(treduce_dyn,in_beam(N),Key1),
        (N < Size->
                erase(Key1),
                N1 is N + 1,
                recorda(treduce_dyn,in_beam(N1),_);
                erase(Key),
                p1_message('non-admissible removal (beam size)'), p_message(NodeNum),
		recorded(nodes,node(NodeNum,_,_,_,_),Key2),
                erase(Key2)),
        fail.
prune_open([BestCompress/BestNode/BestTB]):-
	recorded(treduce,set(treduce,compression),_), 
	recorded(gains,gain(Gain,Node),_),
	Node \= BestNode,
	recorded(nodes,node(Node,Clauses,P,N,L/TB1),Key),
	once(((P-1 =< BestCompress);(P-1 = BestCompress, TB1 =< BestTB))),
	p1_message(pruning), p_message(Clauses),
	erase(Key),
	fail.
prune_open([BestCompress/BestNode/BestTB]):-
	recorded(treduce,set(treduce,posonly),_), 
	recorded(gains,gain(Gain,Node),_),
	Node \= BestNode,
	recorded(nodes,node(Node,_,P,N,_/TB1),Key),
	((P =< BestCompress);(P=BestCompress,TB1=<BestTB)),
	p1_message(pruning), p_message(Clauses),
	erase(Key),
	fail.
prune_open(_).

get_nextbest:-
        recorded(openlist,[Gain|T],Key),
        recorded(gains,gain(Gain,Node),Key1), !,
        erase(Key1),
        recordz(search,nextnode(Node),_),
        (recorded(gains,gain(Gain,_),_)->true;
                erase(Key),
                recorda(openlist,T,_)).
get_nextbest:-
        recorded(openlist,[_|T],Key),
        erase(Key),
        recorda(openlist,T,_),
        get_nextbest, !.
get_nextbest.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% prove atoms specified by Type and index set using set of Clauses.
% dependent on data structure used for index set:
% currently index set is a list of intervals
% return atoms proved and their count

theory_prove(_,_,[],[],0).
theory_prove(Type,Clauses,[Interval|Intervals],IList,Count):-
	index_prove(Type,Clauses,Interval,I1,C1),
	theory_prove(Type,Clauses,Intervals,I2,C2),
	append(I2,I1,IList),
	Count is C1 + C2.

index_prove(_,_,Start-Finish,[],0):-
	Start > Finish, !.
index_prove(Type,Clauses,Start-Finish,IList,Count):-
	index_prove1(Type,Clauses,Start,Finish,Last),
        % recorda(treduce_dyn,prove_count(Start),_),
        % index_prove1(Type,Clauses,Finish),
        % recorded(treduce_dyn,prove_count(Last),Key), erase(Key),
	Last0 is Last - 1 ,
	Last1 is Last + 1,
	(Last0 >= Start->
		index_prove(Type,Clauses,Last1-Finish,Rest,Count1),
		IList = [Start-Last0|Rest],
		Count is Last - Start + Count1;
		index_prove(Type,Clauses,Last1-Finish,IList,Count)).


index_prove1(Type,Clauses,Last):-
        recorded(treduce_dyn,prove_count(Num),Key),
        Num =< Last,
        recorded(treduce,example(Type,Num,Head),_),
	once(prove1(Head,Clauses)),
        erase(Key),
        Num1 is Num + 1,
        recordz(treduce_dyn,prove_count(Num1),_),
        fail.
index_prove1(_,_,_).

index_prove1(_,_,Num,Last,Num):-
	Num > Last, !.
index_prove1(Type,Clauses,Num,Finish,Last):-
	recorded(treduce,example(Type,Num,Head),_),
	prove1(Head,Clauses), !,
	Num1 is Num + 1,
	index_prove1(Type,Clauses,Num1,Finish,Last).
index_prove1(_,_,Last,_,Last).

prove1(Head,[Clause|_]):-
	recorded(treduce,theory(Clause,_,[Head|Body]),_),
	prove1(Body), !.
prove1(Head,[_|Clauses]):-
	prove1(Head,Clauses).

prove1([]).
prove1([Goal|Goals]):-
	Goal,                   % should be depth bounded
	prove1(Goals), !.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% L I B R A R Y


treduce_help:-
        treduce_help(help/0).
treduce_help(Pred/Arity):-
        !,
        treduce_help_dir(HelpDir),
        concat(['more ',HelpDir,'/',Pred,'_',Arity],X),
        nl,
        system(X),
        nl.
treduce_help(Topic):-
        !,
        treduce_help_dir(HelpDir),
        concat(['more ',HelpDir,'/',Topic],X),
        nl,
        system(X),
        nl.

set(Variable,Value):-
	retractall(treduce,set(Variable,_)),
	recordz(treduce,set(Variable,Value),_),
	special_consideration(Variable,Value).

noset(Variable):-
        retractall(treduce,set(Variable,_)).

text(Literal,Text):-
	retractall(treduce,text(Literal,_)),
	recordz(treduce,text(Literal,Text),_).

determination(Pred1,Pred2):-
	recordz(treduce,determination(Pred1,Pred2),_).

commutative(Pred):-
	recordz(treduce,commutative(Pred),_).

symmetric(Pred):-
	set(check_symmetry,true),
	recordz(treduce,symmetric(Pred),_).

lazy_evaluate(Name/Arity):-
        recordz(treduce,lazy_evaluate(Name/Arity),_).

check_implication(Pred):-
	recordz(treduce,check_implication(Pred),_).

positive_only(Pred):-
	recordz(treduce,positive_only(Pred),_).

mode(Mode,Pred):-
	recordz(treduce,mode(Mode,Pred),_).
modeh(Mode,Pred):-
	recordz(treduce,mode(Mode,Pred),_).
modeb(Mode,Pred):-
	recordz(treduce,mode(Mode,Pred),_).

show(settings):-
	recorded(treduce,set(Parameter,Value),_),
	tab(8), write(Parameter=Value), nl,
	fail.
show(determinations):-
	show1(treduce,determination(_,_)).
show(modes):-
	show1(treduce,mode(_,_)).
show(sizes):-
	show1(treduce,size(_,_)).

show(theory):-
        nl,
        p_message('theory'),
        nl,
        recorded(treduce,rules(L),_),
        reverse(L,L1),
        member(ClauseNum,L1),
        eval_rule(ClauseNum,_),
        fail.

show(pos):-
	recorded(treduce,example(pos,_,Atom),_),
	uncompile(Atom,Atom1),
	write(Atom1), print('.'), nl,
	fail.
show(neg):-
	recorded(treduce,example(neg,_,Atom),_),
	uncompile(Atom,Atom1),
	write(Atom1), print('.'), nl,
	fail.

splitvars:-
        set(splitvars,true).


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

% private functions

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

special_consideration(noise,_):-
        noset(minacc), !.
special_consideration(minacc,_):-
        noset(noise), !.
special_consideration(search,compression):-
        set(evalfn,compression), !.
special_consideration(search,ida):-
        set(evalfn,coverage), !.
special_consideration(verbose,N):-
        set(verbosity,N), !.
special_consideration(treduce,posonly):-
	set(tiebreak,tsize), !.
special_consideration(_,_).


show(Area,Name/Arity):-
        functor(Pred,Name,Arity),
        show1(Area,Pred).


show1(Area,Pred):-
        recorded(Area,Pred,_),
        copy(Pred,Pred1), numbervars(Pred1,0,_),
        write(Pred1), write('.'), nl,
        fail.

view_examples(Type,List):-
        open('/tmp/treduce_tmp',write,S),
        view_examples1(Type,List),
        close(S),
        set_output(user_output),
        system('more /tmp/treduce_tmp'),
        system('/bin/rm /tmp/treduce_tmp').

view_examples1(Type,L):-
        recorded(treduce,example(Type,Num,Atom),_),
        member1(Num,L),
        write(Atom), write('.'), nl,
        fail.
view_examples1(_,_).

reset:-
        clean_up,
        retractall(treduce,_),
        set(nodes,10000),
	set(treduce,compression),
	set(tiebreak,acc).

show(_).
show(_,_).
show1(_).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% U T I L I T I E S


% concatenate elements of a list into an atom

concat([Atom],Atom):- !.
concat([H|T],Atom):-
	concat(T,AT),
	name(AT,L2),
	name(H,L1),
	append(L2,L1,L),
	name(Atom,L).

% get first N elements of a list
get_nlist(0,_,[]):- !.
get_nlist(_,[],[]):- !.
get_nlist(N,[H|T],[H|T1]):-
	N0 is N -1,
	get_nlist(N0,T,T1).

% convert a list of number/literal pairs to an list of ordered literals
get_ordered([],[]):- !.
get_ordered(List,Ordered):-
	merge_list(ascending,List,[],L1),
	get_elems(L1,Ordered).

% pretty print a definite clause: head of list is + literal
pp_dlist(L):-
	pp_dclause(L).

% pretty print a definite clause: head of list is + literal
pp_dclause([]):- !.
pp_dclause(Clause):-
	copy(Clause,[Head|Body]),
	numbervars([Head|Body],0,_),
	print(Head),
	(Body = [] -> print('.'), nl;
		print(' :-'),
		nl,
		print_lits(Body,1,4)).

print_lits([],_,_).
print_lits([Lit],LitNum,_):-
	!,
	print_lit(Lit,LitNum,LitNum,'.',_).
print_lits([Lit|Lits],LitNum,LastLit):-
	print_lit(Lit,LitNum,LastLit,', ',NextLit),
	print_lits(Lits,NextLit,LastLit).

print_lit(Lit,LitNum,LastLit,Sep,NextLit):-
	(LitNum = 1 -> tab(3);true),
	print(Lit), print(Sep),
	(LitNum=LastLit-> nl,NextLit=1; NextLit is LitNum + 1).

print_dclause(Clause):-
	recorded(treduce,set(debug,true),_),
	pp_dclause(Clause).
print_dclause(_).

% pretty print a clause using canned text

pp_theorytext(Name/Arity):-
	functor(Head,Name,Arity),
	clause(Head,Body,_),
	goals_to_list(Body,BodyL),
	copy([Head|BodyL],Clause),
	numbervars(Clause,0,_),
	pp_clausetext(Clause), nl,
	fail.
pp_theorytext(_).

pp_clausetext([Head|Body]):-
	recorded(treduce,text(Head,Text),_),
	print_text(Text),
	(Body = [] -> write('.'), nl;
		write(' if'), nl,
		print_littext(Body)).

print_littext([]).
print_littext([Lit|Rest]):-
	recorded(treduce,text(Lit,Text),_),
	tab(8),
	print_text(Text),
	(Rest = [] -> write('.'), nl;
		write(' and'), nl,
		print_littext(Rest)).

print_text([]).
print_text([Atom|T]):-
	write(Atom), write(' '),
	print_text(T).

prin_dmessage(Mess):-
	recorded(treduce,set(debug,true),_),!,
	print('['), print(Mess), print('] ').
prin_dmessage(_).

print_dmessage(Mess):-
	recorded(treduce,set(debug,true),_),!,
	print('['), print(Mess), print(']'), nl.
print_dmessage(_).

p1_message(Mess):-
	print('['), print(Mess), print('] ').
p_message(Mess):-
	print('['), print(Mess), print(']'), nl.

p1_message(0,Mess):-
	!,
	p1_message(Mess).
p_message(0,Mess):-
	!,
	p_message(Mess).
p1_message(Verbosity,Mess):-
	recorded(treduce,set(verbosity,Level),_),
	Verbosity =< Level, !,
	p1_message(Mess).
p_message(Verbosity,Mess):-
	recorded(treduce,set(verbosity,Level),_),
	Verbosity >= Level, !,
	p_message(Mess).
p1_message(_,_).
p_message(_,_).

delete_list([],L,L).
delete_list([H1|T1],L1,L):-
	delete(H1,L1,L2), !,
	delete_list(T1,L2,L).
delete_list([_|T1],L1,L):-
	delete_list(T1,L1,L).

delete(H,[H|T],T).
delete(H,[H1|T],[H1|T1]):-
	delete(H,T,T1).

delete1(H,[H|T],T):- !.
delete1(H,[H1|T],[H1|T1]):-
	delete1(H,T,T1).

delete2(_,[],[]):- !.
delete2(H,[H|T],T):- !.
delete2(H,[H1|T],[H1|T1]):-
	delete2(H,T,T1).

append(A,[],A).
append(A,[H|T],[H|T1]):-
	append(A,T,T1).

member1(H,[H|_]):- !.
member1(H,[_|T]):-
	member1(H,T).

in_list(X,[X1|_]):- same_val(X,X1).
in_list(X,[_|T]):-
	in_list(X,T).

member(X,[X|_]).
member(X,[_|T]):-
	member(X,T).

reverse(L1, L2) :- revzap(L1, [], L2).

revzap([X|L], L2, L3) :- revzap(L, [X|L2], L3).
revzap([], L, L).


clause_to_list((Head:-true),[Head]):- !.
clause_to_list((Head:-Body),[Head|L]):-
	!,
	goals_to_list(Body,L).
clause_to_list(Head,[Head]).

list_to_clause([Goal],(Goal:-true)):- !.
list_to_clause([Head|Goals],(Head:-Body)):-
	list_to_goals(Goals,Body).

list_to_goals([Goal],Goal):- !.
list_to_goals([Goal|Goals],(Goal,Goals1)):-
	list_to_goals(Goals,Goals1).

goals_to_list((true,Goals),T):-
	!,
	goals_to_list(Goals,T).
goals_to_list((Goal,Goals),[Goal|T]):-
	!,
	goals_to_list(Goals,T).
goals_to_list(true,[]):- !.
goals_to_list(Goal,[Goal]).


% returns intersection of S1, S2 and S1-Intersection
intersect1(Elems,[],[],Elems):- !.
intersect1([],_,[],[]):- !.
intersect1([Elem|Elems],S2,[Elem|Intersect],ElemsLeft):-
	member1(Elem,S2), !,
	intersect1(Elems,S2,Intersect,ElemsLeft).
intersect1([Elem|Elems],S2,Intersect,[Elem|ElemsLeft]):-
	intersect1(Elems,S2,Intersect,ElemsLeft).

% S1 improper subset S2
subset1(S1,S2):-
	intersect1(S1,S2,S1,[]).

% exists a set S1 in set of sets that is an improper subset of S2
exists_subset([S1|_],S2):-
	intersect1(S1,S2,S1,[]), !.
exists_subset([_|T],S2):-
	exists_subset(T,S2).

% two sets are equal

equal_set([],[]).
equal_set([H|T],S):-
	delete1(H,S,S1),
	equal_set(T,S1), !.

% X is a member of every list in a list of lists
member_lists(X,[List]):-
	!,
	member1(X,List).
member_lists(X,[List|Lists]):-
	member1(X,List),
	member_lists(X,Lists).

% mergesort lists removing duplicates
merge_list(_,[],L,L).
merge_list(Order,[H1|T],L1,L2):-
	member(H1,L1), !,
	merge_list(Order,T,L1,L2).
merge_list(Order,[H1|T],L1,L2):-
	insert(Order,H1,L1,L),
	merge_list(Order,T,L,L2).

% mergesort lists ignoring duplicates
fmerge_list(_,[],L,L).
fmerge_list(Order,[H1|T],L1,L2):-
	insert(Order,H1,L1,L),
	fmerge_list(Order,T,L,L2).

insert(_,X,[],[X]).
insert(descending,H,[H1|T],[H,H1|T]):-
	val(H,N), val(H1,N1),
	gt(N,N1), !.
insert(ascending,H,[H1|T],[H,H1|T]):-
	val(H,N), val(H1,N1),
	leq(N,N1), !.
insert(Order,H,[H1|T],[H1|T1]):-
	insert(Order,H,T,T1).

uniq_insert(_,X,[],[X]).
uniq_insert(descending,H,[H1|T],[H,H1|T]):-
	val(H,N), val(H1,N1),
	gt(N,N1), !.
uniq_insert(ascending,H,[H1|T],[H,H1|T]):-
	val(H,N), val(H1,N1),
	lt(N,N1), !.
uniq_insert(Order,H,[H|T],[H|T]):- !.
uniq_insert(Order,H,[H1|T],[H1|T1]):-
	uniq_insert(Order,H,T,T1).


gt([H1|_],[H2|_]):-
	H1 > H2, !.
gt([H1|T1],[H1|T2]):-
	!,
	gt(T1,T2).
gt(Num1,Num2):-
	number(Num1), number(Num2),
	Num1 > Num2.

gteq([H1|_],[H2|_]):-
	H1 >= H2, !.
gteq([H1|T1],[H1|T2]):-
	!,
	gteq(T1,T2).
gteq(Num1,Num2):-
	number(Num1), number(Num2),
	Num1 >= Num2.

lt([H1|_],[H2|_]):-
	H1 < H2, !.
lt([H1|T1],[H1|T2]):-
	!,
	lt(T1,T2).
lt(Num1,Num2):-
	number(Num1), number(Num2),
	Num1 < Num2.

leq([],[]):- !.
leq([H1|_],[H2|_]):-
	H1 < H2, !.
leq([H1|T1],[H1|T2]):-
	!,
	leq(T1,T2).
leq(Num1,Num2):-
	number(Num1), number(Num2),
	Num1 =< Num2.

min(A,B,A):-
        A < B, !.
min(A,B,B):-
        B =< A.

quicksort(_,[],[]).
quicksort(Order,[X|Tail],Sorted):-
        val(X,Xval),
        partition(Xval,Tail,Small,Big),
        quicksort(Order,Small,SSmall),
        quicksort(Order,Big,SBig),
        (Order=ascending-> append([X|SBig],SSmall,Sorted);
                append([X|SSmall],SBig,Sorted)).

partition(_,[],[],[]).
partition(X,[Y|Tail],[Y|Small],Big):-
        val(Y,Yval),
        gt(X,Yval), !,
        partition(X,Tail,Small,Big).
partition(X,[Y|Tail],Small,[Y|Big]):-
        partition(X,Tail,Small,Big).

% get all elems of a list by discarding key
get_elems([],[]):- !.
get_elems([Entry|T],[Elem|T1]):-
	val1(Entry,Elem),
	get_elems(T,T1).

% get all keys in a list by discarding elems
get_keys([],[]).
get_keys([Entry|T],[Elem|T1]):-
	val(Entry,Elem),
	get_keys(T,T1).

% get elems with specified keys
get_elems(_,[],[]).
get_elems(List,[Key|Keys],[Elem|Elems]):-
	member1(Key/Elem,List),
	get_elems(List,Keys,Elems).

update_list([],L,L).
update_list([H|T],L,Updated):-
	update(H,L,L1),
	update_list(T,L1,Updated).

update(H,[H|T],[H|T]):- !.
update(H,[H1|T],[H1|T1]):-
	update(H,T,T1).
update(H,[],[H]).

same_val(A1/B1,A2/B1):-
	!,
	A1 == A2.
same_val(A1,A2):-
	A1 == A2.

val(A/_,A):- !.
val(A,A).

val1(_/B,B):- !.
val1(A,A).

copy(Original,Copy):-
	recorda(treduce_dyn,tmp(Original),Key),
	recorded(treduce_dyn,tmp(Copy),Key),
	erase(Key).

exists_duplicate(Clause):-
        recorded(treduce,theory(N1,_,Clause1),_),
        copy(Clause1,C1),
        copy(Clause,C),
        numbervars(C1,0,_),
        numbervars(C,0,_),
        C = C1.

construct_name(Prefix,Type,Name):-
	name(Prefix,PString),
	suffix(Type,SString),
	append(SString,PString,FString),
	name(Name,FString).

suffix(pos,Suffix):- name('.f',Suffix).
suffix(neg,Suffix):- name('.n',Suffix).
suffix(rules,Suffix):- name('.b',Suffix).
	
% checks if 2 sets intersect
intersects(S1,S2):-
	member(Elem,S1), member1(Elem,S2), !.

% checks if bitsets represented as lists of intervals intersect
interval_intersects([L1-L2|_],I):-
	interval_intersects1(L1-L2,I), !.
interval_intersects([_|I1],I):-
	interval_intersects(I1,I).

interval_intersects1(L1-_,[M1-M2|_]):-
	L1 >= M1, L1 =< M2, !.
interval_intersects1(L1-L2,[M1-_|_]):-
	M1 >= L1, M1 =< L2, !.
interval_intersects1(L1-L2,[_|T]):-
	interval_intersects1(L1-L2,T).

interval_intersection(L1-L2,M1-M2,L1-L2):-
	L1 >= M1, L2 =< M2, !.
interval_intersection(L1-L2,M1-M2,M1-M2):-
	M1 >= L1, M2 =< L2, !.
interval_intersection(L1-L2,M1-M2,L1-M2):-
	L1 >= M1, M2 >= L1, M2 =< L2, !.
interval_intersection(L1-L2,M1-M2,M1-L2):-
	M1 >= L1, M1 =< L2, L2 =< M2, !.

intervals_intersection([],_,[]).
intervals_intersection([Interval|Intervals],I,Intersect):-
	intervals_intersection1(Interval,I,I1),
	intervals_intersection(Intervals,I,I2),
	append(I2,I1,Intersect).

intervals_intersection1(I1,[],[]).
intervals_intersection1(I1,[I2|I],[I3|T]):-
	interval_intersection(I1,I2,I3), !,
	intervals_intersection1(I1,I,T).
intervals_intersection1(I1,[I2|I],T):-
	intervals_intersection1(I1,I,T).

% finds length of intervals in a list
interval_count([],0).
interval_count([L1-L2|T],N):-
	N1 is L2 - L1 + 1,
	interval_count(T,N2),
	N is N1 + N2.

% convert list to intervals
list_to_intervals(List,Intervals):-
	quicksort(ascending,List,List1),
	list_to_intervals1(List1,Intervals).

list_to_intervals1([],[]).
list_to_intervals1([Start|T],[Start-Finish|I1]):-
	list_to_interval(Start,T,Finish,T1),
	list_to_intervals1(T1,I1).

list_to_interval(Finish,[],Finish,[]).
list_to_interval(Finish,[Next|T],Finish,[Next|T]):-
	Next - Finish > 1,
	!.
list_to_interval(_,[Start|T],Finish,Rest):-
	list_to_interval(Start,T,Finish,Rest).

% converts intervals into a list
intervals_to_list([],[]).
intervals_to_list([Interval|Intervals],L):-
	interval_to_list(Interval,L1),
	intervals_to_list(Intervals,L2),
	append(L2,L1,L), !.

% converts an interval into a list
interval_to_list(Start-Finish,[]):-
	Start > Finish, !.
interval_to_list(Start-Finish,[Start|T]):-
	Start1 is Start+1,
	interval_to_list(Start1-Finish,T), !.
interval_to_list(Element,[Element]).

interval_subsumes(Start1-Finish1,Start2-Finish2):-
	Start1 =< Start2,
	Finish1 >= Finish2.

interval_subtract(Start1-Finish1,Start1-Finish1,[]):- !.
interval_subtract(Start1-Finish1,Start1-Finish2,[S2-Finish1]):-
	!,
	S2 is Finish2 + 1.
interval_subtract(Start1-Finish1,Start2-Finish1,[Start1-S1]):-
	!,
	S1 is Start2 - 1.
interval_subtract(Start1-Finish1,Start2-Finish2,[Start1-S1,S2-Finish1]):-
	S1 is Start2 - 1,
	S2 is Finish2 + 1.

% compiler instructions
declare_dynamic(Pred/Arity):-
	dynamic Pred/Arity.


clean_up:-
	retractall(search,_),
	retractall(nodes,_),
	retractall(gains,_),
	retractall(vars,_),
	retractall(terms,_),
	retractall(lits,_),
	retractall(split,_),
	retractall(treduce_dyn,_).


retractall(Area,Fact):-
	recorded(Area,Fact,Key),
	erase(Key),
	fail.
retractall(_,_).

% i/o stuff

read_examples(Type,Pred):-
	construct_name(Pred,Type,File),
	open(File,read,Stream),
	retractall(treduce,example(Type,_,_)),
	retractall(treduce,size(Type,_)),
	recorda(treduce,size(Type,0),_),
	repeat,
	read(Stream,Example),
	(Example=end_of_file-> close(Stream);
	recorded(treduce,size(Type,N),Key), erase(Key),
	N1 is N + 1,
	skolemize(Example,Fact,Body,SkolemVars),
	recorda(treduce,size(Type,N1),_),
	record_skolemized(Type,N1,SkolemVars,Fact,Body),
	fail),
	!.
read_examples(_,_).

skolemize((Head:-Body),SHead,SBody,SkolemVars):-
	!,
	copy((Head:-Body),(SHead:-Body1)),
	numbervars((SHead:-Body1),0,SkolemVars),
	goals_to_list(Body1,SBody).
skolemize(UnitClause,Lit,[],SkolemVars):-
	copy(UnitClause,Lit),
	numbervars(Lit,0,SkolemVars).
skolemize(UnitClause,Lit):-
	skolemize(UnitClause,Lit,[],_).

record_skolemized(Type,N1,SkolemVars,Fact,Body):-
	recorda(treduce,example(Type,N1,Fact),_),
	add_backs(Body),
	add_skolem_types(SkolemVars,Fact,Body).

add_backs([]).
add_backs([Lit|Lits]):-
	recorda(treduce,back(Lit),_),
	functor(Lit,Name,Arity),
	declare_dynamic(Name/Arity),
	assertz(Lit),
	add_backs(Lits).

add_skolem_types(0,_,_):- !.
add_skolem_types(_,Head,Body):-
	add_skolem_types([Head]),
	add_skolem_types(Body).

add_skolem_types([]).
add_skolem_types([Lit|Lits]):-
	functor(Lit,PSym,Arity),
	get_modes(PSym/Arity,L),
	add_skolem_types1(Lit,L),
	add_skolem_types(Lits).

add_skolem_types1(_,[]):- !.
add_skolem_types1(Fact,[Lit|Lits]):-
	split_args(Lit,I,O,C),
	add_skolem_types2(Fact,I),
	add_skolem_types2(Fact,O),
	add_skolem_types2(Fact,C),
	add_skolem_types1(Fact,Lits).

add_skolem_types2(_,[]).
add_skolem_types2(Literal,[ArgNo/Type|Rest]):-
	arg(ArgNo,Literal,Arg),
	SkolemType =.. [Type,Arg],
	(recorded(treduce,back(SkolemType),_)-> true;
		recorda(treduce,back(SkolemType),_),
		asserta(SkolemType)),
	add_skolem_types2(Literal,Rest).

read_rules(Pred):-
	retractall(treduce,mode(_,_)),
	retractall(treduce,determination(_,_)),
	construct_name(Pred,rules,File),
	consult(File).

read_all(Pred):-
	clean_up,
	reset,
	read_rules(Pred),
	read_examples(pos,Pred),
	read_examples(neg,Pred),
	recorded(treduce,size(pos,P),_),
	recorda(treduce,atoms(pos,[1-P]),_),
	recorda(treduce,atoms_left(pos,[1-P]),_),
	recorded(treduce,size(neg,N),_),
	recorda(treduce,atoms(neg,[1-N]),_),
	recorda(treduce,atoms_left(neg,[1-N]),_),
	recorda(treduce,last_clause(0),_),
	Prior is P / (P + N),
	recorda(treduce,prior(Prior),_),
	reset_counts.

read_examples(Pred):-
	clean_up,
	reset,
	read_examples(pos,Pred),
	read_examples(neg,Pred),
	recorded(treduce,size(pos,P),_),
	recorda(treduce,atoms(pos,[1-P]),_),
	recorda(treduce,atoms_left(pos,[1-P]),_),
	recorded(treduce,size(neg,N),_),
	recorda(treduce,atoms(neg,[1-N]),_),
	recorda(treduce,atoms_left(neg,[1-N]),_),
	reset_counts.

reset_counts:-
	retractall(treduce_dyn,last_term(_)),
	retractall(treduce_dyn,last_var(_)),
	recorda(treduce_dyn,last_term(0),_),
	recorda(treduce_dyn,last_var(0),_), !.

% reset the number of successes for a literal: cut to avoid useless backtrack
reset_succ:-
        retractall(treduce_dyn,last_success(_)),
        recorda(treduce_dyn,last_success(0),_), !.

	
rm_intervals([],I,I).
rm_intervals([I1|I],Intervals,Result):-
	rm_interval(I1,Intervals,Intervals1),
	rm_intervals(I,Intervals1,Result).

rm_interval(_,[],[]).
rm_interval(I1,[Interval|Rest],Intervals):-
	interval_intersection(I1,Interval,I2), !,
	interval_subtract(Interval,I2,I3),
	rm_interval(I1,Rest,I4),
	append(I4,I3,Intervals).
rm_interval(I1,[Interval|Rest],[Interval|Intervals]):-
	rm_interval(I1,Rest,Intervals).

abs_val(P,P):-
	P >= 0, !.
abs_val(N,P):-
	P is -1*N.

% not(P):-
	% P, !, fail.
% not(_).

% once(P):- P, !.

:- reset, p_message('Settings'), show(settings).