/*
\section{Abductive cc implementation}
\begin{description}
\item[Authors] Vijay Saraswat, Philippe Codognet
\item[Bugs to:] saraswat@parc.xerox.com,codognet@minos.inria.fr
\item[Copyright:] \copyright Xerox Corporation, 1992, INRIA, 1992
\item[This File:] ab\_cc\_new.pl
\item[Last Modified]: Sun Mar 22 21:32:43 1992
\item[Brief Description:]
   The code in this file implements a top-level interpreter
   for abductive \cc.
   \begin{itemize}
   \item Source programs are of the form:
\begin{verbatim} 
                g::a.
\end{verbatim}
        where {\tt a} (agents) is given by:
\begin{verbatim} 
             a ::= true | g | c | c -> a  | a,a
\end{verbatim}
        `{\tt ,}' binds tighter than `{\tt ->}'.

   \item At this time constraints are given by:
\begin{verbatim} 
           c ::= X=t | c,c
\end{verbatim}
       Richer constraints will be added subsequently.

   \item  A top-level call is of the form:
\begin{verbatim} 
            abduce(Sys, Vars, Conclusion)
\end{verbatim}

         Here {\tt Sys} is an agent, {\tt Conclusion} is a constraint,
         and {\tt Vars} is a list of variables on which constraints
         can be abduced. {\tt Vars} is a list each of whose entry is
         of the form {\tt Varname-Var}, where {\tt Varname} is a constant (the
         name of the variable). The list should associate at most one
         name for a variable. The system prints out the constraints
         abduced on these variables so that running {\tt Sys} entails
         {\tt Conclusions}. Multiple explanations are generated on backtracking.

    \item The algorithm used is the following:
     \begin{itemize}
         \item Initialize {\tt Assumptions} to true. 
         \item Run {\tt Sys} as an agent, until it quiesces. 
             Note that this will reduce an abducible agent if its
             ask condition is satisfied. 
         \item If {\tt Conclusion} is entailed stop, and print
             {\tt Assumptions}.
         \item Otherwise check that the {\tt Conclusion} is still
             consistent. If so, and there is an 
             agent {\tt c -> a}, with the constrained variables in c
             lying in the given set of variables, assume  {\tt c}, and 
             continue with {\tt a} added to the current quiescent system.
             When this fails, continue at (2) with the next abducible
             agent.
         \end{itemize}
         The algorithm will generate explanations, not minimal explanations. 
          Minimization will be costly. Also, the same explanation may be
          generated multiple times, if there multiple derivations are possible.
    \end{itemize}
    Examples of the usage of this program are given in the files {\tt ex\_\{3,4,5\}.pl}
    in this directory. 

    To run this program, just consult this file into Prolog, and the files
    that describe your input \cc{} program.

\item[Gotchas:]
    There is no explicit syntax for existential quantification. Any variable
    occurring in the body of a definition g::a, and not occurring in the head,
    is automatically treated as an existential variable.
 
    Also, disjunction (backtracking) is not supported in this implementation.

\item[Exports:] {\tt abduce/3.}

\item[Things to do:]
    Augment with richer constraint. 
    Think of compilation.
    How can information in the Conclusion be used to focus the search
    for assumptions?
    See the gotchas.
\end{description}
\newpage{\footnotesize\begin{verbatim}*/
:- op( 1200, xfx, ::).

abduce(B, Vars, Cons):- abduce(B, Vars, true, Cons).
abduce(B, Vars, Ass, Cons) :- 
   run(B, NewB, true, Flag), 
   (Flag == reduced
       -> abduce(NewB, Vars,  Ass, Cons)
       ; (ask(Cons) 
             -> format("Explanation: ~p.~n", [Ass])
             ; (satisfiable(Cons), 
                try_each(NewB, Vars, Ass, Cons)))).

try_each(((Abs -> Agent), Rest), Vars, Ass, Cons) :-
    (ass(Abs, Vars, Ass, Ass_1), call(Abs), 
     abduce((Agent, Rest), Vars,  Ass_1, Cons)) ;
    try_each(Rest, Vars,  Ass, Cons).

run(true, NewB, B, _Flag):- !, NewB=B.
run(A=B, NewB, B, reduced) :- !, A=B, NewB=B.
run((Ask -> Agent), NewB, B, Flag) :- !,
     (ask(Ask)
        -> (Flag=reduced, run(Agent, NewB, B, _Flag))
        ; (satisfiable(Ask) 
              -> NewB = ((Ask -> Agent), B)
              ;  NewB = B)).
run((G1, G2), NewB, B, Flag) :- !, run(G1, NewB, B, Flag), run(G2, B, B, Flag).
run(Goal, NewB, B, reduced) :- (Goal :: Agent), run(Agent, NewB, B, _Flag).

ass(true, _Vars, Ass, Ass).
ass((G1, G2), Vars, Ass, Res) :- ass(G1, Vars, Ass, A), ass(G2, Vars, A, Res).
ass((A=B), Vars, Ass, (Extname=B, Ass)) :- memchk(A, Vars, Extname).

satisfiable(Ask):- \+(\+(call(Ask))).

ask((A1, A2)):- ask(A1), ask(A2).
ask(A=B):- A==B.

memchk(A, [Name-B | _], Name) :- A == B, !.
memchk(A, [_  | R], Name) :- memchk(A, R, Name). 


/*\end{verbatim}} */