Simplify

Author: ajreynol

language/sygus.tex

@@ -1058,12 +1058,9 @@ \subsection{Asserting Oracle Constraints and Assumptions}
 
 Assuming this command is well-formed,
 the interaction between the synthesis solver and the binary
-can be understood as the solver passing \emph{constant values}\footnote{
-A definition of constant value for $T$ coincides with terms generated by the
-SyGuS grammar term $\paren{\constantkwd\mbox{ }T}$.
-}
+can be understood as the solver passing values
 $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
+and the binary generating a list of values
 $d_{1}, \ldots, d_{m}$ corresponding to the output $y_{1}, \ldots y_{m}$.
 The expected implementation for passing
 constant values as input and output