1%
    2%  epath.pl:  create and manipulate epistemic path terms.
    3%
    4%  Copyright 2008, Ryan Kelly
    5%
    6%  Syntax for epistemic paths is:
    7%
    8%    A           - primitive agent name
    9%    E1 ; E2     - sequence
   10%    E1 | E2     - choice
   11%    ?(C)        - test
   12%    E*          - iteration
   13%    !(X:T)      - nondet variable rebind with given type
   14%    -[X:V|..]   - variable assignment
   15%
   16
   17%
   18%  epath_not_refuted_values(E,VVIn,VVOut)  -  determine possible var values
   19%
   20%  If path E is entered with variable bindings from the set VVIn, then
   21%  it will terminate with bindings from the set VVOut.
   22%  Each of these is a list mapping vars to a list of possible values, e.g.
   23%  [X:[a,b,c], Y:[f,g]].  Vars not in the mapping are allowed to take on
   24%  any value.
   25%
   26%  Since this is a propositional domain, we can handle the star operator
   27%  as a simple fixpoint calculation and be sure it will eventually terminate.
   28%
   29
   30epath_not_refuted_values(A,VV,VV) :-
   31    agent(A).
   32epath_not_refuted_values(?(P),VVIn,VVOut) :-
   33    epath_not_refuted_values_test(VVIn,[],P,VVOut),
   34    vv_valid(VVOut).
   35epath_not_refuted_values(!(X:T),VVIn,VVOut) :-
   36    bagof(Val,call(T,Val),Vals),
   37    vv_update(VVIn,X,Vals,VVOut).
   38epath_not_refuted_values(-[],VVIn,VVIn).
   39epath_not_refuted_values(-[X:V|Xs],VVIn,VVOut) :-
   40    vv_update(VVIn,X,[V],VV2),
   41    epath_not_refuted_values(-Xs,VV2,VVOut).
   42epath_not_refuted_values(E1 ; E2,VVIn,VVOut) :-
   43    epath_not_refuted_values(E1,VVIn,VV2),
   44    epath_not_refuted_values(E2,VV2,VVOut).
   45epath_not_refuted_values(E1 | E2,VVIn,VVOut) :-
   46    ( epath_not_refuted_values(E1,VVIn,VV1) ->
   47        ( epath_not_refuted_values(E2,VVIn,VV2) ->
   48            vv_merge(VV1,VV2,VVOut)
   49        ;
   50            VVOut = VV1
   51        )
   52    ;
   53        epath_not_refuted_values(E2,VVIn,VVOut)
   54    ).
   55epath_not_refuted_values(E*,VVIn,VVOut) :-
   56    epath_not_refuted_values(E,VVIn,VV2),
   57    ( VV2 = VVIn ->
   58        VVOut = VV2
   59    ;
   60        epath_not_refuted_values(E*,VV2,VVOut)
   61    ).
   62
   63
   64epath_not_refuted_values_test([],_,_,[]).
   65epath_not_refuted_values_test([X:Vs|Xs],Sofar,P,VVOut) :-
   66    partition(epath_not_refuted_values_allowed(P,X,Xs,Sofar),Vs,Vs1,_),
   67    VVOut = [X:Vs1|VVOut2],
   68    Sofar2 = [X:Vs1|Sofar],
   69    epath_not_refuted_values_test(Xs,Sofar2,P,VVOut2).
   70
   71epath_not_refuted_values_allowed(P,X,Others1,Others2,V) :-
   72    epath_not_refuted_values_allowed_sub1(P,Others1,P1),
   73    epath_not_refuted_values_allowed_sub1(P1,Others2,P2),
   74    subs(X,V,P2,P3),
   75    simplify(P3,P4),
   76    P4 \= false.
   77
   78epath_not_refuted_values_allowed_sub1(P,[],P).
   79epath_not_refuted_values_allowed_sub1(P,[X:Vs|Xs],P2) :-
   80    member(Val,Vs),
   81    subs(X,Val,P,P1),
   82    epath_not_refuted_values_allowed_sub1(P1,Xs,P2).
   83    
   84
   85vv_valid([]).
   86vv_valid([_:Vs|Xs]) :-
   87    Vs \= [],
   88    vv_valid(Xs).
   89
   90vv_update([],X,Vs,[X:Vs]).
   91vv_update([X1:Vs1|Xs],X2,Vs2,Res) :-
   92    ( X1 == X2 ->
   93        Res = [X1:Vs2|Xs]
   94    ;
   95        Res = [X1:Vs1|Res2],
   96        vv_update(Xs,X2,Vs2,Res2)
   97    ).
   98
   99vv_merge([],VV2,VV2).
  100vv_merge([X:Vs|Xs],VV1,Res) :-
  101    vv_merge1(VV1,X,Vs,VV2),
  102    vv_merge(Xs,VV2,Res).
  103
  104vv_merge1([],X,Vs,[X:Vs]).
  105vv_merge1([X1:Vs1|Xs],X2,Vs2,Res) :-
  106    ( X1 == X2 ->
  107        union(Vs1,Vs2,VsU),
  108        Res = [X1:VsU|Xs]
  109    ;
  110        Res = [X1:Vs1|Res2],
  111        vv_merge1(Xs,X2,Vs2,Res2)
  112    ).
  113
  114
  115
  116%
  117%  epath_enum_vars(E,En)  -  enumerate all possible values of each path 
  118%                            variable in the epath, reducing it from FODL
  119%                            to VPDL and hence making it decidable
  120%
  121%  We expand any unions produced during enumeration over sequence operators,
  122%  in the hope that each branch will simplify given the new variable bindings.
  123%  We try to push var assignments as far to the right as possible, doing subs
  124%  into tests and simplifying.
  125%
  126
  127epath_enum_vars(E1 ; E2,En) :-
  128    epath_enum_vars(E1,En1),
  129    flatten_op('|',[En1],Ens1),
  130    epath_enum_vars(E2,En2),
  131    flatten_op('|',[En2],Ens2),
  132    epath_enum_vars_branches(Ens1,Ens2,Ens),
  133    epath_build('|',Ens,En).
  134epath_enum_vars(E1 | E2,En) :-
  135    flatten_op('|',[E1,E2],Es),
  136    maplist(epath_enum_vars,Es,Ens),
  137    epath_build('|',Ens,En).
  138epath_enum_vars(E*,En) :-
  139    epath_enum_vars(E,EnS),
  140    epath_build('*',EnS,En).
  141epath_enum_vars(?(P),?(P)).
  142epath_enum_vars(-VA,-VA).
  143epath_enum_vars(!(X:T),En) :-
  144    bagof(VA,V^(call(T,V),VA=(-[X:V])),VAs),
  145    epath_build('|',VAs,En).
  146epath_enum_vars(A,A) :-
  147    agent(A).
  148    
  149
  150epath_enum_vars_branches([],_,[]).
  151epath_enum_vars_branches([B|Bs],Es,[R|Rs]) :-
  152    ( epath_ends_with_assign(B,VA,Head) ->
  153        epath_enum_vars_branches_assign(Es,VA,Head,[],R)
  154    ;
  155        epath_enum_vars_branches_noassign(Es,B,[],R)
  156    ),
  157    epath_enum_vars_branches(Bs,Es,Rs).
  158
  159
  160epath_enum_vars_branches_assign([],_,_,Acc,R) :-
  161    joinlist('|',Acc,R).
  162epath_enum_vars_branches_assign([E|Es],VA,B,Acc,R) :-
  163    epath_push_assign(E,VA,Ea),
  164    epath_build(';',[B,Ea],R1),
  165    epath_enum_vars_branches_assign(Es,VA,B,[R1|Acc],R).
  166
  167epath_enum_vars_branches_noassign([],_,Acc,R) :-
  168    joinlist('|',Acc,R).
  169epath_enum_vars_branches_noassign([E|Es],B,Acc,R) :-
  170    epath_build(';',[B,E],R1),
  171    epath_enum_vars_branches_noassign(Es,B,[R1|Acc],R).
  172 
  173%
  174%  epath_ends_with_assign(E,VA,Head)  -  epath ends with a variable assignment
  175%
  176%  This predicate is true when E ends with a unique variable assignment
  177%  operator.  VA is bound to the assignment and Head is the remainder
  178%  of the path.
  179%
  180epath_ends_with_assign(E1 ; E2,VA,Head) :-
  181    epath_ends_with_assign(E2,VA2,Head2),
  182    ( Head2 = (?true) ->
  183        ( epath_ends_with_assign(E1,VA1,Head1) ->
  184            Head = Head1, vassign_merge(VA1,VA2,VA)
  185        ;
  186            Head = E1, VA=VA2
  187        )
  188    ;
  189        Head = (E1 ; Head2), VA=VA2
  190    ).
  191epath_ends_with_assign(E1 | E2,VA,Head) :-
  192    epath_ends_with_assign(E1,VA,Head1),
  193    epath_ends_with_assign(E2,VA2,Head2),
  194    VA == VA2,
  195    Head = (Head1 | Head2).
  196epath_ends_with_assign(-(VA),VA,?true).
  197
  198
  199%
  200%  epath_push_assign(E,VA,Ep)  -  push a variable assignment as far to the
  201%                                 right as possible.
  202%
  203%  This may involve, for example, pushing it over a test operator and
  204%  substituting the assigned values into the test formula.
  205%
  206epath_push_assign(E1 ; E2,VA,Ep) :-
  207    epath_push_assign(E1,VA,Ep1),
  208    ( epath_ends_with_assign(Ep1,VA2,Head) ->
  209        epath_push_assign(E2,VA2,Ep2),
  210        epath_build(';',[Head,Ep2],Ep)
  211    ;
  212        epath_build(';',[Ep1,E2],Ep)
  213    ).
  214epath_push_assign(E1 | E2,VA,Ep) :-
  215    epath_push_assign(E1,VA,Ep1),
  216    epath_push_assign(E2,VA,Ep2),
  217    epath_build('|',[Ep1,Ep2],Ep).
  218epath_push_assign(E*,VA,(-VA) ; (E*)).
  219epath_push_assign(!(X:T),VA,Ep) :-
  220    ( vassign_contains(VA,X) ->
  221        Ep = (-VA ; !(X:T))
  222    ;
  223        Ep = (!(X:T) ; -VA)
  224    ).
  225epath_push_assign(-VA2,VA,-VAm) :-
  226    vassign_merge(VA2,VA,VAm).
  227epath_push_assign(?(P),VA,?(Q) ; -VA) :-
  228    vassign_subs(VA,P,Q1),
  229    simplify(Q1,Q).
  230epath_push_assign(A,VA,A ; -VA) :-
  231    agent(A).
  232
  233
  234%
  235%  Predicates for manipulating a variable assignment list
  236%
  237vassign_merge([],VA,VA).
  238vassign_merge([(X:V)|Xs],VA2,VA) :-
  239    vassign_insert(X,V,VA2,VAt),
  240    vassign_merge(Xs,VAt,VA).
  241
  242vassign_insert(X,V,[],[X:V]).
  243vassign_insert(X,V,[(X2:V2)|Xs],VA) :-
  244    ( X == X2 ->
  245        VA = [(X2:V2)|Xs]
  246    ;
  247        vassign_insert(X,V,Xs,VAs),
  248        VA = [(X2:V2)|VAs]
  249    ).
  250
  251vassign_contains([(X:_)|Xs],Y) :-
  252    X == Y ; vassign_contains(Xs,Y).
  253
  254vassign_subs([],P,P).
  255vassign_subs([(X:V)|Xs],P,Q) :-
  256    subs(X,V,P,P2),
  257    vassign_subs(Xs,P2,Q).
  258
  259
  260%
  261%  epath_vars(E,Vars)  -  find all path variables (as opposed to formula-level
  262%                         variables) in the given epistemic path.
  263%
  264epath_vars(E1 ; E2,Vars) :-
  265    epath_vars(E1,Vars1),
  266    epath_vars(E2,Vars2),
  267    epath_vars_union(Vars1,Vars2,Vars), !.
  268epath_vars(E1 | E2,Vars) :-
  269    epath_vars(E1,Vars1),
  270    epath_vars(E2,Vars2),
  271    epath_vars_union(Vars1,Vars2,Vars), !.
  272epath_vars(E*,Vars) :-
  273    epath_vars(E,Vars), !.
  274epath_vars(!(X:T),[X:T]) :- !.
  275epath_vars(?(_),[]) :- !.
  276epath_vars(-VA,VA) :- !.
  277epath_vars(A,[]) :-
  278    agent(A).
  279
  280epath_vars_union([],Vars,Vars).
  281epath_vars_union([X:T|Vars1],Vars2,Vars) :-
  282    (ismember(X:T,Vars2) ->
  283        epath_vars_union(Vars1,Vars2,Vars)
  284    ;
  285        Vars = [X:T|VarsT],
  286        epath_vars_union(Vars1,Vars2,VarsT)
  287    ).
  288
  289%
  290%  epath_build(Op,Args,EPath)  -  build an epath, with simplification
  291%
  292%  This predicate builds an epath, applying simplifications appropriate
  293%  to the top-level operator but assuming all argument paths are already
  294%  simplified.
  295%
  296
  297epath_build('|',Es,E) :-
  298    flatten_op('|',Es,Es0),
  299    partition('='(?false),Es0,_,Es1),
  300    simplify_epath_choice_subsumes(Es1,Es2),
  301    simplify_epath_choice_union(Es2,Es3),
  302    ( Es3 = [] ->
  303        E = (?false)
  304    ;
  305        joinlist('|',Es3,E)
  306    ).
  307
  308epath_build(';',Es,E) :-
  309    flatten_op(';',Es,Es0),
  310    ( member(?false,Es0) -> 
  311        E = (?false)
  312    ;
  313        partition('='(?true),Es0,_,Es1),
  314        ( Es1 = [] ->
  315            E = (?true)
  316        ;
  317            simplify_epath_seq_combine(Es1,Ss),
  318            ( member(?false,Ss) ->
  319                E = (?false)
  320            ;
  321                joinlist(';',Ss,E)
  322            )
  323        )
  324    ).
  325
  326epath_build('*',E,Eb) :-
  327    simplify_star_contents(E,E1),
  328    ( E1 = (?(P)) ->
  329        Eb = (?(P))
  330    ;
  331        Eb = (E1*)
  332    ).
  333
  334
  335%
  336%  simplify_epath  -  simplify an epistemic path
  337%
  338%  we can do this by recursively stripping off the outermost operator,
  339%  simplifying the argument paths, then apply epath_build.
  340%
  341simplify_epath(X,_) :-
  342    var(X), !, throw(cant_simplify_a_free_epath).
  343simplify_epath(A,A) :-
  344    agent(A).
  345simplify_epath(E1 ; E2,Es) :-
  346    flatten_op(';',[E1,E2],Eseq),
  347    maplist(simplify_epath,Eseq,Esimp),
  348    epath_build(';',Esimp,Es).
  349simplify_epath(E1 | E2,Es) :-
  350    flatten_op('|',[E1,E2],Eseq),
  351    maplist(simplify_epath,Eseq,Esimp),
  352    epath_build('|',Esimp,Es).
  353simplify_epath(E*,Es) :-
  354    simplify_epath(E,E1s),
  355    epath_build('*',E1s,Es).
  356simplify_epath(?(P),?(S)) :-
  357    simplify(P,S).
  358simplify_epath(!(X:T),!(X:T)).
  359
  360
  361
  362epath_elim_impossible_branches(A,_,A) :-
  363    agent(A).
  364epath_elim_impossible_branches(?(P),VVPoss,?(P1)) :-
  365    ( epath_not_refuted_values(?(P),VVPoss,_) ->
  366        P1 = P
  367    ;
  368        P1 = false
  369    ).
  370epath_elim_impossible_branches(!(X:T),_,!(X:T)).
  371epath_elim_impossible_branches(-VA,_,-VA).
  372epath_elim_impossible_branches(E1 ; E2,VVPoss,Er) :-
  373    ( epath_not_refuted_values(E1,VVPoss,VV2) ->
  374        epath_elim_impossible_branches(E1,VVPoss,Er1),
  375        epath_elim_impossible_branches(E2,VV2,Er2),
  376        (Er1 = ?false ->
  377            Er = ?false
  378        ; Er2 = ?false ->
  379            Er = ?false
  380        ;
  381            Er = (Er1 ; Er2)
  382        )
  383    ;
  384        Er = (?false)
  385    ).
  386epath_elim_impossible_branches(E1 | E2,VVPoss,Er) :-
  387    epath_elim_impossible_branches(E1,VVPoss,Er1),
  388    epath_elim_impossible_branches(E2,VVPoss,Er2),
  389    (Er1 = ?false ->
  390       Er = Er2
  391    ; Er2 = ?false ->
  392       Er = Er1
  393    ;
  394       Er = (Er1 | Er2)
  395    ).
  396epath_elim_impossible_branches(E*,VVPoss,Er) :-
  397    ( epath_not_refuted_values(E*,VVPoss,VV2) ->
  398        epath_elim_impossible_branches(E,VV2,E2),
  399        (E2 = ?false ->
  400            Er = ?false
  401        ;
  402            Er = (E2*)
  403        )
  404    ;
  405        Er = (?false)
  406    ).
  407
  408%
  409%  Simplification for operations within a star.
  410%
  411simplify_star_contents(E1,E2) :-
  412    ( simplify_star_contents1(E1,Es) ->
  413        simplify_star_contents(Es,E2)
  414    ;
  415        E2 = E1
  416    ).
  417
  418simplify_star_contents1(E*,E).
  419
  420% Any choices within a star that are simply ?true can be removed,
  421% as we always have the option of staying in current state.
  422simplify_star_contents1(E1 | E2,Ep) :-
  423    flatten_op('|',[E1,E2],Es),
  424    partition('='(?true),Es,Ts,Es2),
  425    length(Ts,N), N > 0,
  426    joinlist('|',Es2,Ep).
  427%
  428%  Flatten stars in (B1* | (B2* | B3*)*)* 
  429simplify_star_contents1(E,Ep) :-
  430    ( E = ((B1*) | (((B2*) | (B3*))*)) ; E = ((((B1*) | (B2*))*) | (B3*)) ) ->
  431    Ep = ((B1*) | (B2*) | (B3*)).
  432
  433%
  434%  Remove choices that are subsumed by repetition of another branch
  435simplify_star_contents1(E1 | E2,Ep) :-
  436    flatten_op('|',[E1,E2],Es),
  437    simplify_epath_star_subsumes(Es,Ss),
  438    joinlist('|',Ss,Ep).
  439
  440simplify_epath_star_subsumes(Es,Ss) :-
  441    simplify_epath_star_subsumes(Es,[],0,Ss).
  442 
  443simplify_epath_star_subsumes([],Acc,1,Acc).
  444simplify_epath_star_subsumes([E|Es],Acc,HaveSimpd,Ss) :-
  445    ( member(E2,Acc), epath_subsumes(E2*,E) ->
  446        simplify_epath_star_subsumes(Es,Acc,1,Ss)
  447    ;
  448        partition(epath_subsumes(E*),Acc,Rem,Acc2),
  449        ( Rem = [] -> NewHaveSimpd = HaveSimpd ; NewHaveSimpd = 1 ),
  450        simplify_epath_star_subsumes(Es,[E|Acc2],NewHaveSimpd,Ss)
  451    ).
  452
  453
  454
  455%
  456%  simplify branches in a choice by removing any subsumed by another branch
  457%
  458simplify_epath_choice_subsumes(Es,Ss) :-
  459    simplify_epath_choice_subsumes(Es,[],Ss).
  460 
  461simplify_epath_choice_subsumes([],Acc,Acc).
  462simplify_epath_choice_subsumes([E|Es],Acc,Ss) :-
  463    ( member(E2,Acc), epath_subsumes(E2,E) ->
  464        simplify_epath_choice_subsumes(Es,Acc,Ss)
  465    ;
  466        partition(epath_subsumes(E),Acc,_,Acc2),
  467        simplify_epath_choice_subsumes(Es,[E|Acc2],Ss)
  468    ).
  469
  470%
  471%  simplify branches in a choice by combining two branches into a single,
  472%  simpler branch giving their union.
  473%
  474simplify_epath_choice_union(Es,Ss) :-
  475    simplify_epath_choice_union(Es,[],Ss).
  476
  477simplify_epath_choice_union([],Acc,Acc).
  478simplify_epath_choice_union([E|Es],Acc,Ss) :-
  479    ( (select(E1,Acc,Rest), simplify_epath_union(E,E1,Eu)) ->
  480        simplify_epath_choice_union([Eu|Es],Rest,Ss)
  481    ;
  482        simplify_epath_choice_union(Es,[E|Acc],Ss)
  483    ).
  484
  485
  486%
  487%  simplify_epath_seq_combine(Es,Ss)  -  simplify sequence of paths by
  488%                                        combining adjacent ones.
  489%
  490simplify_epath_seq_combine(Es,Ss) :-
  491    simplify_epath_seq_combine(Es,[],Ss).
  492
  493simplify_epath_seq_combine([E],Acc,Ss) :-
  494    reverse([E|Acc],Ss).
  495simplify_epath_seq_combine([E|Es],Acc,Ss) :-
  496    ( simplify_epath_combine([E|Es],Es2) ->
  497        simplify_epath_seq_combine_recheck(Es2,Acc,Ss)
  498    ;
  499      simplify_epath_seq_combine(Es,[E|Acc],Ss)
  500    ).
  501
  502:- index(simplify_eapth_seq_combine_recheck(0,1,0)).  503
  504simplify_epath_seq_combine_recheck(Es,[],Ss) :-
  505    simplify_epath_seq_combine(Es,[],Ss).
  506simplify_epath_seq_combine_recheck(Es,[A|Acc],Ss) :-
  507    ( simplify_epath_combine([A|Es],Es2) ->
  508        simplify_epath_seq_combine_recheck(Es2,Acc,Ss)
  509    ;
  510      simplify_epath_seq_combine(Es,[A|Acc],Ss)
  511    ).
  512
  513%
  514%  epath_subsumes(E1,E2)  -  detect common cases where one epath completely
  515%                            subsumes another.  That is, all worlds reachable
  516%                            by path E2 are also reachable by path E1.
  517%
  518%  epath_subsumes/2 is det, which we ensure using cuts
  519%
  520epath_subsumes(E,E) :- !.
  521epath_subsumes(E*,E1*) :-
  522    epath_subsumes(E*,E1), !.
  523epath_subsumes(E*,E1) :-
  524    epath_subsumes(E,E1), !.
  525epath_subsumes(E*,E1) :-
  526    epath_seq_split(E1,[P1,P2],[]),
  527    epath_subsumes(E*,P1),
  528    epath_subsumes(E*,P2), !.
  529epath_subsumes(E,E1 | E2) :-
  530    epath_subsumes(E,E1),
  531    epath_subsumes(E,E2), !.
  532epath_subsumes(E1 | E2,E) :-
  533    (epath_subsumes(E1,E) ; epath_subsumes(E2,E)), !.
  534epath_subsumes(E1 ; E2,E) :-
  535    epath_seq_split(E,[P1,P2],[]),
  536    epath_subsumes(E1,P1),
  537    epath_subsumes(E2,P2), !.
  538
  539%
  540%  simplify_epath_union(E1,E2,Eu)  -  simplify E1 and E2 into their union
  541%                                     (E1 | E2) <=> Eu
  542%
  543%  simplify_epath_combine(Es,Esc)  -    simplify E1;E2;P into Ec;P
  544%
  545%  This basically allows us to special-case a number of common forms.
  546%
  547simplify_epath_union(E1,E2,Eu) :-
  548    simplify_epath_union1(E1,E2,Eu)
  549    ;
  550    simplify_epath_union1(E2,E1,Eu).
  551
  552%  P1 | (P1 ; P2* ; P2)   =>   P1 ; P2*
  553simplify_epath_union1(E1,E2,Eu) :-
  554    P1 = E1,
  555    epath_seq_split(E2,[P1,P2*,P2],[]),
  556    epath_build('*',P2,P2S),
  557    epath_build(';',[P1,P2S],Eu).
  558%  P1 | (P2 ; P2* ; P1)   =>   P2* ; P1
  559simplify_epath_union1(E1,E2,Eu) :-
  560    P1 = E1,
  561    epath_seq_split(E2,[P2,P2*,P1],[]),
  562    epath_build('*',P2,P2S),
  563    epath_build(';',[P2S,P1],Eu).
  564%  P1 | (P2* ; P2 ; P1)   =>   P2* ; P1
  565simplify_epath_union1(E1,E2,Eu) :-
  566    P1 = E1,
  567    epath_seq_split(E2,[P2*,P2,P1],[]),
  568    epath_build('*',P2,P2S),
  569    epath_build(';',[P2S,P1],Eu).
  570% ?P1 | ?P2   =>   ?(P1 | P2)
  571simplify_epath_union1(?P1,?P2,?Pu) :-
  572    fml2cnf(P1 | P2,Pu1),
  573    simplify(Pu1,Pu).
  574
  575
  576% P1* ; (P2 ; (P1*))*   =>   (P1* | P2*)*
  577simplify_epath_combine(E,[Ec|Rest]) :-
  578    epath_seq_split(E,[P1*,Pr*],Rest),
  579    epath_seq_split(Pr,[P2,P1*],[]),
  580    epath_build('|',[P1*,P2*],Ec1),
  581    epath_build('*',Ec1,Ec).
  582% (P1* ; P2)* ; P1*   =>   (P1* | P2*)*
  583simplify_epath_combine(E,[Ec|Rest]) :-
  584    epath_seq_split(E,[Pr*,P1*],Rest),
  585    epath_seq_split(Pr,[P1*,P2],[]),
  586    epath_build('|',[P1,P2],Ec1),
  587    epath_build('*',Ec1,Ec).
  588% (P1* ; P2)* ; P1 ; P1*   =>   (P1* | P2*)*
  589simplify_epath_combine(E,[Ec|Rest]) :-
  590    epath_seq_split(E,[Pr*,P1,P1*],Rest),
  591    epath_seq_split(Pr,[P1*,P2],[]),
  592    epath_build('|',[P1,P2],Ec1),
  593    epath_build('*',Ec1,Ec).
  594% P1* ; P2*   =>   P1*   if P1 > P2
  595simplify_epath_combine(E,[Ec|Rest]) :-
  596    epath_seq_split(E,[P1*,P2*],Rest),
  597    ( epath_subsumes(P1,P2), Ec = P1
  598    ; epath_subsumes(P2,P1), Ec = P2
  599    ).
  600% ?P1 ; ?P2   =>   ?(P1 & P2)
  601simplify_epath_combine(E,[?(Pc)|Rest]) :-
  602    epath_seq_split(E,[?P1,?P2],Rest),
  603    fml2cnf(P1 & P2,Pc1),
  604    simplify(Pc1,Pc).
  605
  606%
  607%  epath_seq_split(E,Seqs,Rest)  -  nondeterminstically split sequence of ops
  608%
  609%  This predicate nondeterministically splits a series of sequence operators
  610%  into patterns that match the elements of the list Seqs.  Each free var in
  611%  Seqs may be given one or more elements from the sequence, while each
  612%  any entries in Seq that are nonvar will be unified with precisely one
  613%  element.
  614%
  615:- index(epath_seq_split(1,1,0)).  616
  617epath_seq_split(E1 ; E2,Seqs,Rest) :-
  618    flatten_op(';',[E1,E2],Es),
  619    epath_seq_split_prep(Seqs,Preps),
  620    epath_seq_split(Es,Preps,Rest),
  621    epath_seq_split_unprep(Preps,Seqs).
  622
  623epath_seq_split([E|Es],Seqs,Rest) :-
  624    epath_seq_split([E|Es],[],Seqs,Rest).
  625
  626epath_seq_split(Rest,[],[],Rest).
  627epath_seq_split(Rest,[S-Vs|Todo],[],Rest) :-
  628    reverse(Vs,VsR),
  629    ( var(S) ->
  630        S = VsR
  631    ;
  632        joinlist(';',VsR,S)
  633    ),
  634    epath_seq_split(Rest,Todo,[],Rest).
  635epath_seq_split([E|Es],Todo,[S|Seqs],Rest) :-
  636    ( var(S) ->
  637        ((Todo = [S2-Vs|Todo2], S2 == S) ->
  638            (epath_seq_split([E|Es],Todo,Seqs,Rest)
  639            ;
  640            epath_seq_split(Es,[S-[E|Vs]|Todo2],[S|Seqs],Rest))
  641        ;
  642            epath_seq_split(Es,[S-[E]|Todo],[S|Seqs],Rest)
  643        )
  644    ;
  645      epath_seq_split_unify(S,[E|Es],Es2), epath_seq_split(Es2,Todo,Seqs,Rest)
  646    ).
  647epath_seq_split([],Todo,[S],Rest) :-
  648    var(S), Todo = [S2-_|_], S2 == S, 
  649    epath_seq_split([],Todo,[],Rest).
  650
  651
  652epath_seq_split_unify(P,[E|Es],Es) :-
  653    var(P), P=E, !.
  654epath_seq_split_unify(P1 ; P2,Es,Es2) :-
  655    epath_seq_split_unify(P1,Es,Es1),
  656    epath_seq_split_unify(P2,Es1,Es2), !.
  657epath_seq_split_unify(E,[E|Es],Es).
  658
  659epath_seq_split_prep([],[]).
  660epath_seq_split_prep([S|Seqs],[P|Preps]) :-
  661    (var(S) -> true ; S=P ),
  662    epath_seq_split_prep(Seqs,Preps).
  663epath_seq_split_unprep([],[]).
  664epath_seq_split_unprep([P|Preps],[S|Seqs]) :-
  665    ( P = [_|_] -> joinlist(';',P,S) ; P=S ),
  666    epath_seq_split_unprep(Preps,Seqs).
  667
  668    
  669
  670%
  671%  copy_epath(EIn,EOut)  -  copy an epath, renaming path variables
  672%
  673%  This produces a copy of EIn with all path variables replaced by
  674%  fresh variables.  All free formula variables remain unchanged, while
  675%  all bound formula variables are also renamed.
  676%
  677copy_epath(E,Ec) :-
  678    epath_vars(E,EVarsT),
  679    maplist(arg(1),EVarsT,EVars),
  680    term_variables(E,TVars),
  681    vdelete_list(TVars,EVars,FVars),
  682    copy_term(E^FVars,E2^FVars2),
  683    FVars2=FVars,
  684    copy_epath_fmls(E2,Ec).
  685
  686copy_epath_fmls(E1 ; E2,E1c ; E2c) :-
  687    copy_epath_fmls(E1,E1c),
  688    copy_epath_fmls(E2,E2c).
  689copy_epath_fmls(E1 | E2,E1c | E2c) :-
  690    copy_epath_fmls(E1,E1c),
  691    copy_epath_fmls(E2,E2c).
  692copy_epath_fmls(E*,Ec*) :-
  693    copy_epath_fmls(E,Ec).
  694copy_epath_fmls(?(P),?(Pc)) :-
  695    copy_fml(P,Pc).
  696copy_epath_fmls(!(V:T),!(V:T)).
  697copy_epath_fmls(-VA,-VA).
  698copy_epath_fmls(A,A) :-
  699    agent(A).
  700
  701
  702%
  703%  pp_epath(E)  -  pretty-print an epistemic path
  704%
  705
  706pp_epath(E) :-
  707    pp_epath(E,0,0).
  708
  709pp_epath_list([E],_,_,O1,D1) :-
  710    pp_epath(E,O1,D1).
  711pp_epath_list([E1,E2|Es],Op,D,O1,D1) :-
  712    pp_epath(E1,O1,D1), nl,
  713    pp_inset(D), write(Op), nl,
  714    pp_epath_list([E2|Es],Op,D,D1,D1).
  715
  716
  717pp_epath(E1 ; E2,O,D) :-
  718    flatten_op(';',[E1,E2],Es),
  719    D1 is D + 1,
  720    O1 is O + 1,
  721    pp_epath_list(Es,';',D,O1,D1).
  722pp_epath(E1 | E2,O,D) :-
  723    flatten_op('|',[E1,E2],Es),
  724    D1 is D + 1,
  725    O1 is O + 1,
  726    pp_epath_list(Es,'|',D,O1,D1).
  727pp_epath(?(P),O,D) :-
  728    D1 is D + 1,
  729    pp_inset(O), write('?  '),
  730    pp_fml(P,0,D1).
  731pp_epath(!(V:T),O,_) :-
  732    pp_inset(O), write('!  '), write(V:T).
  733pp_epath(-VA,O,_) :-
  734    pp_inset(O), write('-  '), pp_epath_assign(VA).
  735pp_epath(E*,O,D) :-
  736    D1 is D + 1,
  737    pp_inset(O), write('*'), nl,
  738    pp_epath(E,D1,D1).
  739pp_epath(A,O,_) :-
  740    agent(A),
  741    pp_inset(O), write(A).
  742
  743
  744pp_epath_assign([]).
  745pp_epath_assign([(X:V)|Xs]) :-
  746    write(X), write(' <= '), write(V), write(',  '),
  747    pp_epath_assign(Xs)