/* 

  Explanation-Based Generalization (EBG) in Picat v3.

  This is a port of the program minihyper.pl in
  I. Bratko, "Prolog Programming for Artificial Intelligence", 4th edn.,
  Pearson Education / Addison-Wesley 2012
  Page 621ff (Figures 25.6, 25.7)

  Note: Since this program use clause/2 which is in the bp context,
        we have to load the database using assertz, load_gifts/0.

  This Picat model was created by Hakan Kjellerstrand, hakank@gmail.com
  See also my Picat page: http://www.hakank.org/picat/

*/

module ebg_v3.


%  Figure 25.7  Explanation-based generalization.


%   ebg( Goal, GeneralizedGoal, SufficientCondition):
%     SufficientCondition in terms of operational predicates
%     guarantees that generalization of Goal, GeneralizedGoal, is true.
%     GeneralizedGoal must not be a variable

ebg( true, true, true)  :-  !.

ebg( Goal, GenGoal, GenGoal)  :-
  operational( GenGoal), 
  call( Goal).

ebg( (Goal1,Goal2), (Gen1,Gen2), Cond)  :- !,
  ebg( Goal1, Gen1, Cond1),
  ebg( Goal2, Gen2, Cond2),
  andx( Cond1, Cond2, Cond).     % Cond = (Cond1,Cond2) simplified

ebg( Goal, GenGoal, Cond)  :-
  not operational( Goal),
  bp.clause( GenGoal, GenBody),
  bp.copy_term( (GenGoal,GenBody), (Goal,Body)),    % Fresh copy of (GenGoal,GenBody)
  ebg( Body, GenBody, Cond).

% and( Cond1, Cond2, Cond) if
%  Cond is (possibly simplified) conjunction of Cond1 and Cond2

andx( true, Cond, Cond)  :-  !.        % (true and Cond) <==> Cond
andx( Cond, true, Cond)  :-  !.        % (Cond and true) <==> Cond
andx( Cond1, Cond2, ( Cond1, Cond2)).