1% Simple illustration of the use of user-defined refinement operators
    2%       in Aleph using Michalski's trains problem.
    3% To run do the following:
    4%       a. Load Aleph
    5%       b. read_all(train).
    6%       c. sat(1).
    7%       d. reduce.

?- sat(1),reduce(C). */

   11:- use_module(library(aleph)).   12:- if(current_predicate(use_rendering/1)).   13:- use_rendering(prolog).   14:- endif.   15:- aleph.   16:- aleph_set(i,2).   17:- aleph_set(verbose,1).   18:- aleph_set(refine,user).   19
   20:- modeh(1,eastbound(+train)).   21:- modeb(1,short(+car)).   22:- modeb(1,closed(+car)).   23:- modeb(1,long(+car)).   24:- modeb(1,open_car(+car)).   25:- modeb(1,double(+car)).   26:- modeb(1,jagged(+car)).   27:- modeb(1,shape(+car,#shape)).
   28:- modeb(1,load(+car,#shape,#int)).
   29:- modeb(1,wheels(+car,#int)).
   30:- modeb(*,has_car(+train,-car)).   31
   32:- determination(eastbound/1,short/1).   33:- determination(eastbound/1,closed/1).   34:- determination(eastbound/1,long/1).   35:- determination(eastbound/1,open_car/1).   36:- determination(eastbound/1,double/1).   37:- determination(eastbound/1,jagged/1).   38:- determination(eastbound/1,shape/2).   39:- determination(eastbound/1,wheels/2).   40:- determination(eastbound/1,has_car/2).   41:- determination(eastbound/1,load/3).   42
   43:-begin_bg.   44% type definitions
   45car(car_11).  car(car_12).  car(car_13).  car(car_14).
   46car(car_21).  car(car_22).  car(car_23).
   47car(car_31).  car(car_32).  car(car_33).
   48car(car_41).  car(car_42).  car(car_43).  car(car_44).
   49car(car_51).  car(car_52).  car(car_53).
   50car(car_61).  car(car_62).
   51car(car_71).  car(car_72).  car(car_73).
   52car(car_81).  car(car_82).
   53car(car_91).  car(car_92).  car(car_93).  car(car_94).
   54car(car_101).  car(car_102).
   55
   56shape(elipse).  shape(hexagon).  shape(rectangle).  shape(u_shaped).
   57shape(triangle). shape(circle). shape(nil).
   58
   59train(east1).  train(east2).  train(east3).  train(east4).  train(east5).
   60train(west6).  train(west7).  train(west8).  train(west9).  train(west10).
   61
   62% eastbound train 1
   63short(car_12).		% 0
   64closed(car_12).		% 1
   65long(car_11).		% 2
   66long(car_13).
   67short(car_14).
   68open_car(car_11).		% 3
   69open_car(car_13).
   70open_car(car_14).
   71shape(car_11,rectangle). % 4,5
   72shape(car_12,rectangle).
   73shape(car_13,rectangle).
   74shape(car_14,rectangle).
   75load(car_11,rectangle,3). % 6,7,8
   76load(car_12,triangle,1).
   77load(car_13,hexagon,1).
   78load(car_14,circle,1).
   79wheels(car_11,2).	  % 9,10
   80wheels(car_12,2).
   81wheels(car_13,3).
   82wheels(car_14,2).
   83has_car(east1,car_11). % 11,12
   84has_car(east1,car_12).
   85has_car(east1,car_13).
   86has_car(east1,car_14).
   87
   88% eastbound train 2
   89has_car(east2,car_21).
   90has_car(east2,car_22).
   91has_car(east2,car_23).
   92short(car_21).
   93short(car_22).
   94short(car_23).
   95shape(car_21,u_shaped).
   96shape(car_22,u_shaped).
   97shape(car_23,rectangle).
   98open_car(car_21).
   99open_car(car_22).
  100closed(car_23).
  101load(car_21,triangle,1).
  102load(car_22,rectangle,1).
  103load(car_23,circle,2).
  104wheels(car_21,2).
  105wheels(car_22,2).
  106wheels(car_23,2).
  107
  108% eastbound train 3
  109has_car(east3,car_31).
  110has_car(east3,car_32).
  111has_car(east3,car_33).
  112short(car_31).
  113short(car_32).
  114long(car_33).
  115shape(car_31,rectangle).
  116shape(car_32,hexagon).
  117shape(car_33,rectangle).
  118open_car(car_31).
  119closed(car_32).
  120closed(car_33).
  121load(car_31,circle,1).
  122load(car_32,triangle,1).
  123load(car_33,triangle,1).
  124wheels(car_31,2).
  125wheels(car_32,2).
  126wheels(car_33,3).
  127
  128% eastbound train 4
  129has_car(east4,car_41).
  130has_car(east4,car_42).
  131has_car(east4,car_43).
  132has_car(east4,car_44).
  133short(car_41).
  134short(car_42).
  135short(car_43).
  136short(car_44).
  137shape(car_41,u_shaped).
  138shape(car_42,rectangle).
  139shape(car_43,elipse).
  140shape(car_44,rectangle).
  141double(car_42).
  142open_car(car_41).
  143open_car(car_42).
  144closed(car_43).
  145open_car(car_44).
  146load(car_41,triangle,1).
  147load(car_42,triangle,1).
  148load(car_43,rectangle,1).
  149load(car_44,rectangle,1).
  150wheels(car_41,2).
  151wheels(car_42,2).
  152wheels(car_43,2).
  153wheels(car_44,2).
  154
  155% eastbound train 5
  156has_car(east5,car_51).
  157has_car(east5,car_52).
  158has_car(east5,car_53).
  159short(car_51).
  160short(car_52).
  161short(car_53).
  162shape(car_51,rectangle).
  163shape(car_52,rectangle).
  164shape(car_53,rectangle).
  165double(car_51).
  166open_car(car_51).
  167closed(car_52).
  168closed(car_53).
  169load(car_51,triangle,1).
  170load(car_52,rectangle,1).
  171load(car_53,circle,1).
  172wheels(car_51,2).
  173wheels(car_52,3).
  174wheels(car_53,2).
  175
  176% westbound train 6
  177has_car(west6,car_61).
  178has_car(west6,car_62).
  179long(car_61).
  180short(car_62).
  181shape(car_61,rectangle).
  182shape(car_62,rectangle).
  183closed(car_61).
  184open_car(car_62).
  185load(car_61,circle,3).
  186load(car_62,triangle,1).
  187wheels(car_61,2).
  188wheels(car_62,2).
  189
  190% westbound train 7
  191has_car(west7,car_71).
  192has_car(west7,car_72).
  193has_car(west7,car_73).
  194short(car_71).
  195short(car_72).
  196long(car_73).
  197shape(car_71,rectangle).
  198shape(car_72,u_shaped).
  199shape(car_73,rectangle).
  200double(car_71).
  201open_car(car_71).
  202open_car(car_72).
  203jagged(car_73).
  204load(car_71,circle,1).
  205load(car_72,triangle,1).
  206load(car_73,nil,0).
  207wheels(car_71,2).
  208wheels(car_72,2).
  209wheels(car_73,2).
  210
  211% westbound train 8
  212has_car(west8,car_81).
  213has_car(west8,car_82).
  214long(car_81).
  215short(car_82).
  216shape(car_81,rectangle).
  217shape(car_82,u_shaped).
  218closed(car_81).
  219open_car(car_82).
  220load(car_81,rectangle,1).
  221load(car_82,circle,1).
  222wheels(car_81,3).
  223wheels(car_82,2).
  224
  225% westbound train 9
  226has_car(west9,car_91).
  227has_car(west9,car_92).
  228has_car(west9,car_93).
  229has_car(west9,car_94).
  230short(car_91).
  231long(car_92).
  232short(car_93).
  233short(car_94).
  234shape(car_91,u_shaped).
  235shape(car_92,rectangle).
  236shape(car_93,rectangle).
  237shape(car_94,u_shaped).
  238open_car(car_91).
  239jagged(car_92).
  240open_car(car_93).
  241open_car(car_94).
  242load(car_91,circle,1).
  243load(car_92,rectangle,1).
  244load(car_93,rectangle,1).
  245load(car_93,circle,1).
  246wheels(car_91,2).
  247wheels(car_92,2).
  248wheels(car_93,2).
  249wheels(car_94,2).
  250
  251% westbound train 10
  252has_car(west10,car_101).
  253has_car(west10,car_102).
  254short(car_101).
  255long(car_102).
  256shape(car_101,u_shaped).
  257shape(car_102,rectangle).
  258open_car(car_101).
  259open_car(car_102).
  260load(car_101,rectangle,1).
  261load(car_102,rectangle,2).
  262wheels(car_101,2).
  263wheels(car_102,2).
  264
  265
  266refine(aleph_false,eastbound(_)).
  267refine(eastbound(X),(eastbound(X):-has_car(X,_))).
  268refine(eastbound(X),(eastbound(X):-has_car(X,Y),short(Y))).
  269refine((eastbound(X):-has_car(X,Y),short(Y)),Clause):-
  270	Clause = (eastbound(X):-has_car(X,Y),short(Y),closed(Y)).
  271:-end_bg.  272
  273:-begin_in_pos.  274eastbound(east1).
  275eastbound(east2).
  276eastbound(east3).
  277eastbound(east4).
  278eastbound(east5).
  279:-end_in_pos.  280:-begin_in_neg.  281eastbound(west6).
  282eastbound(west7).
  283eastbound(west8).
  284eastbound(west9).
  285eastbound(west10).
  286:-end_in_neg.