
    Backtracking is a fundamental concept to the way that CORAL solves
    logic programs.   Rules are evaluated from left-to-right, when
    a literal fails, this particular instatiation of this rule will
    fail, and so CORAL moves backward in the rule (to the left), to
    attempt to find new bindings for variables that may still succeed.
    A naive strategy for moving backward is to always move back to the
    previous literal.  Using this strategy, all combinations are attempted.

\subsection{Overview of backtracking}

    To avoid further evaluation where it cannot possibly be fruitful, 
    CORAL performs {\em backtracking analysis}.  The main concept
    here is that the bindings for the literal that failed must 
    change before it can succeed, therefore in many cases, you could
    skip back multiple literals at once.  How far to skip backward
    for a literal that fails can be in fact be computed at compile-time.

    A similar concept can be applied when a rule succeeds
    (when duplicates are being eliminated). Add in an understanding
    of {\em cuts}, which disallow backtracking that crosses them,
    and the majority of the current backtracking implementation
    should be clear.
   
    A more recent addition to CORAL's backtrack analysis, 
   {\em Binding-Time Analysis}, is
    due to the fact that non-ground facts (facts containing unbound
    variables) are no longer allowed.  With this restriction, CORAL
    can determine at compile-time {\em how} each literal will end
    up being evaluated, and can call a specialized function to 
    perform this directly (as opposed to figuring out what to do with
    a literal at run-time). 

    Remember that backtracking over more than a single literal
    is basically only an optimization, the answers
    obtained should always be the same as if obtained by the naive
    backtracking strategy mentioned above.

\subsection{Specifics}

\begin{itemize}
\item First-Failure Backtrack Point:\\
    Where to backtrack to in the rule when a right-hand-side
    literal fails the first time it is reached.
    Execution should backtrack to the rightmost point that 
    generates fresh bindings for it.
\begin{verbatim}
    p(X,Y,C) :- q(X,Z), r(Z,A,B), s(Z,C), t(A,B,C).
\end{verbatim}
    If \verb=s(Z,C)= fails the first time it is reached, execution
    should backtrack to \verb=q(X,Z)=, to generate a new binding for \verb=Z=.
    (If \verb=s(Z,C)= has already returned successfully, you would 
     use the next-failure backtrack point.)

\item Next-Failure Backtrack Point:\\
    Where to backtrack to in the rule when a right-hand-side
    literal fails after having been reached after it has 
    suceeded at least once. 
    In this case, execution should backtrack to the rightmost
    point that generates fresh bindings for the literal or any
    literal after it in the rule execution order.
\begin{verbatim}
    p(X,C) :- q(X,Z), r(A,B), s(Z,C), t(A,B,C).
\end{verbatim}
    If \verb=s(Z,C)= fails on a get-next, execution should backtrack
    to \verb=r(A,B)=, not to \verb=q(X,Z)=.
    Note that if the head literal is allowing
    duplicates (i.e. a multiset relation), then we would always 
    backtrack to only the previous literal as we need to allow
    the entire rule to succeed as many times as possible.
        
\item Success Backtrack Point:
    Where to backtrack to when the entire rule has succeeded.
    We want to backtrack to the right-most literal that generates
    new bindings for the head literal (assuming duplicate elimination)
\begin{verbatim}
    p(X,Y) :- q(X,Z), r(A,B), s(Z,C), t(A,B).
\end{verbatim}
    After the rule has suceeded, we would backtrack to \verb=q(X,Z)=,
    which can result in a new binding for \verb=X=.
    If the head is allowing duplicates, we would only backtrack to
    the previous literal, \verb=t(A,B)=.

\end{itemize}


 The backtracking analysis has been extended to also perform
 {\em Binding Analysis}.  A variable is bound at the first literal
 it is seen in.  This information is used to perform {\em matching},
 {\em assignment}, or an {\em equality check} in order to avoid
 performing a full {\em unification} against facts in the
 database (which are guarenteed to be ground).  To this end, the
 {\em SemiNaive} structure stores an array to identify what type
 of unification should be used when unifying against a term known
 to be ground; for other cases, the hint in the array is simply
 ignored, and full unification is used.

 
\noindent
Files to look at:
{\em
\begin{itemize}
\item BindTime.[Ch]     : Backtracking and BindTime Analysis.
\item BacktrackInfoArray.h
\item CompileRule.C 
\item SemiNaive.h  : Stores the backtrack points, and unification functions.
\item HashIndex.C  : Unification against ground facts.
\end{itemize}
}
