Document cvc5-style numerals

This documents the addition of cvc5-style numerals.

spec/doc.tex

@@ -647,7 +647,7 @@ The concrete text representation of the Alethe proofs
 is based on the {\smtlib} standard. Figure~\ref{fig:proof_ex} shows an
 example proof as printed by {\verit} with light edits for readability.
 %
-The format follows the {\smtlib} standard when possible.
+The format broadly follows the {\smtlib} standard.
 %
 Input problems in the {\smtlib} format are scripts.  An {\smtlib} script
 is a list of commands that manipulate the SMT solver.  For example,
@@ -704,6 +704,7 @@ An Alethe proof is a list of commands.
  \grNT{clause}          &\grRule & \textAlethe{(cl}\; \grNT{proof\_term}^{*}\,\textAlethe{)} \\
  \grNT{proof\_term}     &\grRule & \grNT{term}\text{ extended with } \\
                         &        & \textAlethe{(choice (}\, \grNT{sorted\_var}\,\textAlethe{)}\; \grNT{proof\_term}\,\textAlethe{)}  \\
+                        & \grOr  & \grNT{rational}\;\grOr\;\grNT{neg\_numeral}\;\grOr\;\grNT{neg\_decimal} \\
  \grNT{premises\_annotation} &\grRule & \textAlethe{:premises (}\; \grNT{symbol}^{+}\textAlethe{)} \\
  \grNT{args\_annotation}     &\grRule & \textAlethe{:args}\,\textAlethe{(}\,\grNT{step\_arg}^{+}\,\textAlethe{)}  \\
  \grNT{step\_arg}            &\grRule & \grNT{symbol}\;\grOr\;
@@ -711,13 +712,16 @@ An Alethe proof is a list of commands.
  \grNT{context\_annotation}  &\grRule & \textAlethe{:args}\,\textAlethe{(}\,\grNT{context\_assignment}^{+}\,\textAlethe{)}  \\
  \grNT{context\_assignment}  &\grRule & \grNT{sorted\_var} \\
                              & \grOr  & \textAlethe{(:=}\, \grNT{sorted\_var}\;\grNT{proof\_term}\,\textAlethe{)} \\
+ \grNT{rational}             &\grRule & -^{?}\grNT{numeral}/\grNT{numeral} \\
+ \grNT{neg\_numeral}         &\grRule & -\grNT{numeral} \\
+ \grNT{neg\_decimal}        &\grRule & -\grNT{decimal} \\
   \end{array}
   \]
   \caption{The proof grammar.}
   \label{fig:grammar}
 \end{figure}
 
-Every Alethe proof is associated with an  {\smtlib} problem
+Every Alethe proof is associated with an {\smtlib} problem
 that is proved by the Alethe proof.  This can either be a concrete
 problem file or, if the incremental solving commands of {\smtlib}
 are used, the implicit problem constructed at the invocation of a
@@ -743,9 +747,7 @@ $\grNT{function\_def}$,
 $\grNT{sorted\_var}$,
 $\grNT{symbol}$, and
 $\grNT{term}$
-are as defined in the standard. The non-terminal $\grNT{proof\_term}$
-corresponds to the $\grNT{term}$ non-terminal of {\smtlib}, but is
-extended with the additional production for the \inlineAlethe{choice}\index{choice} binder.
+are as defined in the standard.
 
 Alethe proofs are a list of commands.
 The \inlineAlethe{assume} command introduces a new assumption. While this
@@ -800,6 +802,36 @@ annotations.  This can be used for debugging, or other purposes.
 A consumer of Alethe proofs {\em must} be able to parse proofs
 that contain such annotations.
 
+\paragraph{Terms}
+The non-terminal $\grNT{proof\_term}$ is an extended version of the {\smtlib}
+non-terminal $\grNT{term}$.
+First, it has an additional production for the
+\inlineAlethe{choice}\index{choice} binder.
+%
+Second, it has productions to express rationals and negative integers
+concisely.
+%
+A difficulty when parsing {\smtlib} terms is that numerical constants
+are not easy to distinguish from general terms.
+For example, $-\frac{1}{2}$ is written as
+\inlineAlethe{(/ (- 1) 2)}.
+The $\grNT{rational}$ non-terminal makes it possible to write this constant
+as a single literal: \inlineAlethe{-1/2}.
+Furthermore, the non-terminals $\grNT{neg\_numeral}$ and $\grNT{neg\_decimal}$
+achieve the same for unary negation.
+
+The sorting rules for $\grNT{proof\_term}$ are as for {\smtlib} terms with
+one key difference.
+The sort of terms produced by $\grNT{rational}$, $\grNT{decimal}$, and
+$\grNT{neg\_decimal}$ is always \inlineAlethe{Real}.
+The sort of terms produced by $\grNT{integer}$ and $\grNT{neg\_integer}$
+is always \inlineAlethe{Int}.
+For example, in standard {\smtlib}, the term \inlineAlethe{(+ 5 3)}
+has the sort \inlineAlethe{Int} in the logic \texttt{QF\_LIA}, but
+has the sort \inlineAlethe{Real} in \texttt{QF\_LRA}.
+In Alethe, this term always has the sort \inlineAlethe{Int},
+and would not be well sorted in the logic \texttt{QF\_LRA}.
+
 \paragraph{Subproofs}
 The abstract notation denotes subproofs by marking them with a vertical
 line.  To map this notation to a list of commands, Alethe \index{anchor}uses the
@@ -983,8 +1015,12 @@ Overall, the following aspects are treated implicitly by Alethe.
   introduces {\verit} to print Skolem terms as defined functions. User defined
   functions in the input problem are not supported by {\verit} in proof production
   mode.}
+  \item If the input problem is in a logic without integers, then constants from
+        $\grNT{numeral}$ in the input problem will be printed using
+        $\grNT{decimal}$ or $\grNT{rational}$ in the proof.
 \end{itemize}
 
+\noindent
 Alethe proofs contain steps for other aspects that are commonly left implicit, such
 as renaming of bound variables, and the application of substitutions.