change indices for oracles

Author: polgreen

language/sygus.tex

@@ -1045,15 +1045,15 @@ \subsection{Asserting Oracle Constraints and Assumptions}
 \begin{itemize}
 \item $\paren{\constraintoraclekwd\mbox{ } N \mbox{ } 
 \paren{\paren{x_1\mbox{ }\sigma_1} \ldots \paren{x_n\mbox{ }\sigma_n}}\mbox{ }
-\paren{\paren{x_{n+1}\mbox{ }\sigma_{n+1}} \ldots \paren{x_{n+m}\mbox{ }\sigma_{n+m}}}  \mbox{ } t}$
+\paren{\paren{x'_{1}\mbox{ }\sigma'_{1}} \ldots \paren{x'_{m}\mbox{ }\sigma'_{m}}}  \mbox{ } t}$
 
 This informs the solver of the existance of an external binary with name $N$
 which can be used as means of adding new constraints to the problem.
 This command is well-formed only if $N$
-\emph{implements} a function of sort $\sigma_1 \times \ldots \times \sigma_n \rightarrow \sigma_{n+1} \times \ldots \times \sigma_{n+m}$
+\emph{implements} a function of sort $\sigma_1 \times \ldots \times \sigma_n \rightarrow \sigma'_{1} \times \ldots \times \sigma'_{m}$
 (for a definition of the expected implementation of an external binary, see Section~\ref{sec:oracleimplementations}),
 and $t$ is a well-sorted term of sort $\sbool$ 
-whose free symbols may include those in the current signature, as well as any symbol in $x_1 \ldots x_{m+n}$,
+whose free symbols may include those in the current signature, as well as any symbol in $x_1 \ldots x_{n}$ and $x'_1 \ldots x'_{m}$,
 and moreover is allowed based on the restrictions of the current logic.
 
 Assuming this command is well-formed,
@@ -1064,13 +1064,13 @@ \subsection{Asserting Oracle Constraints and Assumptions}
 }
 $c_1, \ldots, c_n$ for $x_1, \ldots x_n$ as input to the binary,
 and the binary generating a list of constant values
-$c_{n+1}, \ldots, c_{n+m}$ corresponding to the output $x_{n_1}, \ldots x_{n+m}$.
+$c'_{1}, \ldots, c'_{m}$ corresponding to the output $x'_{1}, \ldots x'_{m}$.
 The expected implementation for passing
 constant values as input and output 
 is described in Section~\ref{sec:oracleimplementations}.
 For each such call,
-the formula $t[c_1 \ldots c_{n+m}]$, i.e., 
-$t$ with all occurences of $x_1, \ldots, x_{n+m}$ replaced with $c_1, \ldots, c_{n+m}$, 
+the formula $t[c_1 \ldots c_{n} c'_1 \ldots c'_m]$, i.e., 
+$t$ with all occurences of $x_1, \ldots, x_{n}, x'_1, \ldots, x'_m$ replaced with $c_1, \ldots, c_{n}, c'_1, \ldots c'_m$, 
 is added to the current list of constraints $\varphi$ in the conjecture.
 
 Note that 
@@ -1082,10 +1082,10 @@ \subsection{Asserting Oracle Constraints and Assumptions}
 \item 
 $\paren{\assumeoraclekwd\mbox{ } N \mbox{ } 
 \paren{\paren{x_1\mbox{ }\sigma_1} \ldots \paren{x_n\mbox{ }\sigma_n}}\mbox{ }
-\paren{\paren{x_{n+1}\mbox{ }\sigma_{n+1}} \ldots \paren{x_{n+m}\mbox{ }\sigma_{n+m}}}  \mbox{ } t}$
+\paren{\paren{x'_{1}\mbox{ }\sigma'_{1}} \ldots \paren{x'_{m}\mbox{ }\sigma'_{m}}}  \mbox{ } t}$
 
 This command is identical to $\constraintoraclekwd$,
-but the term $t[c_1 \ldots c_{n+m}]$ obtained from a call to the external binary
+but the term $t[c_1 \ldots c_{n} c'_1 \ldots c'_m]$ obtained from a call to the external binary
 is added to the set of assumptions instead of the set of constraints.
 
 \end{itemize}
@@ -1903,16 +1903,17 @@ \section{Calling Oracles}
 The oracle is a binary that implements an iterface of sort $\sigma_1 \times \ldots \times \sigma_n \rightarrow \sigma$.
 \end{definition}
 The SyGuS solver makes queries to an oracle via a text file with the extension \textit{.oracle}. The oracle is called by the solver with the command \textit{oracle-name textfile.oracle}.
-The text file should contain the text $\paren{v_1 \ldots v_n}$ specifying values for each argument to the oracle, where $v_1 \ldots v_n$ are written using the same syntax for constant terms described in this document. The oracle will return the text $\paren{v_{n+1} \ldots v_{n+m}}$ specifying values for the return values of the oracle on the standard output channel.\\
+The text file should contain the text $\paren{v_1 \ldots v_n}$ specifying values for each argument to the oracle, where $v_1 \ldots v_n$ are written using the same syntax for constant terms described in this document. The oracle will return the text $\paren{v'_{1} \ldots v'_{m}}$ specifying values for the return values of the oracle on the standard output channel.\\
+
 
 
 \noindent Consider an oracle that implements the interface declared with the following command:\\\\
 $\paren{\constraintoraclekwd\mbox{ } N \mbox{ }
 \paren{\paren{x_1\mbox{ }\sigma_1} \ldots \paren{x_n\mbox{ }\sigma_n}}\mbox{ }
-\paren{\paren{x_{n+1}\mbox{ }\sigma_{n+1}} \ldots \paren{x_{n+m}\mbox{ }\sigma_{n+m}}}  \mbox{ } t}$ \\
+\paren{\paren{x'_{1}\mbox{ }\sigma'_{1}} \ldots \paren{x'_{m}\mbox{ }\sigma'_{m}}}  \mbox{ } t}$ \\
 
-The text file must contain a list of values $\paren{v_1 \ldots v_n}$ for the input parameters $x_1 \ldots x_n$, and $v_i$ must have the same sort of $\sigma_i$.
-The oracle will return a list of values $\paren{v_{n+1} \ldots v_{n+m}}$, corresponding to the output parameters $x_{n+1} \ldots x_{n+m}$.
+The text file must contain a list of values $\paren{v_1 \ldots v_n}$ for the input parameters $x_1 \ldots x_n$, and $v_i$ must have the same sort as $\sigma_i$.
+The oracle will return a list of values $\paren{v'_{1} \ldots v'_{m}}$, corresponding to the output parameters $x'_{1} \ldots x'_{m}$, and $v'_i$ must have the same sort as $\sigma'_i$.
 %
 The solver calls the oracle with the command ${\tt N \,\,textfile.oracle}$, where ${\tt N}$ is the name of the oracle implememtation as specified in the oracle constraint declaration.