1% Simple illustration of the use of lazy evaluation
    2% 	a FOIL-like inequality predicate is called during
    3% 	the search to obtain a constant that does not appear in
    4%	the bottom clause
    5% To run do the following:
    6%	a. Load Aleph
    7%	b. read_all(ineq).
    8%	c. sat(1).
    9%	d. reduce.

   13:- use_module(library(aleph)).   14:- if(current_predicate(use_rendering/1)).   15:- use_rendering(prolog).   16:- endif.   17:- aleph.   18
   19:- modeh(1,p(+number)).   20:- modeb(1,gteq(+number,#number)).   21
   22:- lazy_evaluate(gteq/2).   23
   24:- determination(p/1,gteq/2).   25
   26
   27:-begin_bg.   28% definition to use during lazy evaluation
   29lteq([P,N],Value):-
   30        !,
   31        find_cutoff(lte,P,N,Value).
   32% definition to use during normal evaluation
   33lteq(X,Value):-
   34	number(X), number(Value), !,
   35        X =< Value.
   36% definition to use during construction of bottom clause
   37lteq(X,X).
   38 
   39% definition to use during lazy evaluation
   40gteq([P,N],Value):-
   41        !,
   42        find_cutoff(gte,P,N,Value).
   43% definition to use during normal evaluation
   44gteq(X,Value):-
   45	number(X), number(Value), !,
   46        X >= Value.
   47% definition to use during construction of bottom clause
   48gteq(X,X).
   49
   50
   51find_cutoff(gte,[],N,Value):-
   52	!,
   53	list_max(N,Value).
   54find_cutoff(gte,P,[],Value):-
   55	!,
   56	list_min(P,Value).
   57find_cutoff(lte,[],N,Value):-
   58	!,
   59	list_min(N,Value).
   60find_cutoff(lte,P,[],Value):-
   61	!,
   62	list_max(P,Value).
   63find_cutoff(C,P,N,Value):-
   64        sort(P,Ps), sort(N,Ns),         	% Ps, Ns are in ascending order
   65        length(P,P0), length(N,N0),
   66        PriorFrac is P0/(P0+N0),
   67        PriorBits is -log(PriorFrac)/log(2),    % bits required to encode a prior pos
   68        find_loss(C,Ps,P,N,P0,N0,PriorBits,PLosses),   % losses made by each pos cutoff
   69        find_loss(C,Ns,P,N,P0,N0,PriorBits,NLosses),   % losses made by each neg cutoff
   70	keysort(PLosses,[PL1-PV1|_]),
   71	keysort(NLosses,[NL1-NV1|_]),
   72	(NL1 < PL1 -> Value is NV1 ; Value is PV1).
   73
   74
   75find_loss(_,[],_,_,_,_,_,[]).
   76find_loss(C,[X|T],Ps,Ns,P0,N0,PriorBits,[Loss-X|T1]):-
   77	find_covered(C,X,Ps,P0,P1),
   78	find_covered(C,X,Ns,N0,N1),
   79        PostFrac is (P1+0.001)/(P1+N1),
   80        PostBits is -log(PostFrac)/log(2),      % bits required to encode a post pos
   81        GainBits is P1*(PriorBits - PostBits),  % total bits gained
   82        Loss is -GainBits,
   83        find_loss(C,T,Ps,Ns,P0,N0,PriorBits,T1).
   84
   85find_covered(lte,_,[],N,N):- !.
   86find_covered(lte,X,[Y|T],N,N1):-
   87	Y > X, !,
   88	length([Y|T],N0),
   89	N1 is N - N0.
   90find_covered(gte,_,[],_,0):- !.
   91find_covered(gte,X,[Y|T],_,N1):-
   92	Y >= X, !,
   93	length([Y|T],N1).
   94find_covered(C,X,[_|T],N,N1):-
   95	find_covered(C,X,T,N,N1).
   96
   97list_max([H|T],X):-
   98	find_elem(max,T,H,X).
   99
  100list_min([H|T],X):-
  101	find_elem(min,T,H,X).
  102
  103find_elem(_,[],X,X).
  104find_elem(max,[H|T],X,Y):-
  105	(H > X -> find_elem(max,T,H,Y); find_elem(max,T,X,Y)).
  106find_elem(min,[H|T],X,Y):-
  107	(H < X -> find_elem(min,T,H,Y); find_elem(min,T,X,Y)).
  108:-end_bg.  109:-begin_in_pos.  110p(3).
  111p(5).
  112p(8).
  113p(9).
  114p(10).
  115:-end_in_pos.  116:-begin_in_neg.  117p(1).
  118p(2).
  119p(4).
  120p(6).
  121
  122:-end_in_neg.