remove vars from oracle fun declaration (#20)

We didn't need the variables, just the sorts

Author: polgreen

language/sygus.tex

@@ -650,7 +650,7 @@ \subsection{Commands}
   \term} \\
   & | & \paren{\constraintoraclekwd\mbox{ }\symbol\mbox{ } \paren{\kstar{\sortedvar}}\mbox{ }\paren{\kstar{\sortedvar}}\mbox{ }
   \term} \\
- & | & \paren{\oracledeckwd\mbox{ }\symbol\mbox{ }\symbol\mbox{ }\paren{\kstar{\sortedvar}}\mbox{ }\sortexpr\mbox{ }} \\
+ & | & \paren{\oracledeckwd\mbox{ }\symbol\mbox{ }\symbol\mbox{ }\paren{\kstar{\sortexpr}}\mbox{ }\sortexpr\mbox{ }} \\
  & | &\paren{\iooracledeckwd\mbox{ }\symbol\mbox{ } \symbol\mbox{ }} \\
  & | &\paren{\cexoracledeckwd\mbox{ }\symbol\mbox{ } \symbol\mbox{ }} \\
  & | &\paren{\memoracledeckwd\mbox{ }\symbol\mbox{ } \symbol\mbox{ }} \\
@@ -1264,7 +1264,7 @@ \subsection{Asserting Oracle Constraints and Assumptions}
 \subsection{Declaring Oracle Functional Symbols}
 
 \begin{itemize}
-\item $\paren{\oracledeckwd\mbox{ }S\mbox{ } N\mbox{ }\paren{\paren{x_1\mbox{ }\sigma_1} \ldots \paren{x_n\mbox{ }\sigma_n}}\mbox{ }\sigma}$
+\item $\paren{\oracledeckwd\mbox{ }S\mbox{ } N\mbox{ }\paren{\sigma_1 \ldots \sigma_n}\mbox{ }\sigma}$
 
 This adds to the current signature a symbol $S$ of function sort 
 $\sigma_1 \times \ldots \times \sigma_n \rightarrow \sigma$
@@ -1282,6 +1282,7 @@ \subsection{Declaring Oracle Functional Symbols}
 }
 \end{array}
 \]
+where $x_1, \ldots, x_n$ and $x$ are fresh variables.
 \end{itemize}
 % The solver can call $S$ as many times as is necessary, and for every input on which $S$ has not been called, $S$ is treated as a universally quantified uninterpreted function. For more details see \cref{sec:correctness-oracles}.
 
@@ -1368,11 +1369,10 @@ \subsection{Pre-defined Oracle Types}
 
 This oracle is mandatory to call in order to determine correctness of the synthesis function and so it is syntactic sugar for:
 
-$\paren{\oracledeckwd\mbox{ }S\mbox{ }N\mbox{ }\paren{\paren{
-x_1\mbox{ }
+$\paren{\oracledeckwd\mbox{ }S\mbox{ }N\mbox{ }\paren{
 \paren{
-\funsortkwd \mbox{ } \sigma_1 \ldots \sigma_n\mbox{ }\sigma }}}
-\sbool}\\
+\funsortkwd \mbox{ } \sigma_1 \ldots \sigma_n\mbox{ }\sigma }}
+\mbox{ }\sbool}\\
 %
 \paren{\constraintkwd \mbox{ } \paren{S \mbox{ } F}}
 $
@@ -1393,11 +1393,10 @@ \subsection{Pre-defined Oracle Types}
 $
 
 $
-\paren{\oracledeckwd\mbox{ }S\mbox{ }N\mbox{ }\paren{\paren{
-x_1\mbox{ }
+\paren{\oracledeckwd\mbox{ }S\mbox{ }N\mbox{ }\paren{
 \paren{
-\funsortkwd \mbox{ } \sigma_1 \ldots \sigma_n\mbox{ }\sigma }}}
-\sbool}\\
+\funsortkwd \mbox{ } \sigma_1 \ldots \sigma_n\mbox{ }\sigma }}
+\mbox{ }\sbool}\\
 %
 \paren{\constraintkwd \mbox{ } \paren{S \mbox{ } F}}
 $