Merge branch 'devel/decimals' into 'master'

Document cvc5-style numerals

See merge request !5

spec/changelog.tex

@@ -22,11 +22,21 @@ Breaking changes:
         be \texttt{(x S) (:= (y S) x)}.
   \item The arguments for \proofRule{forall_inst} have been changed to
         no longer take the shape of bindings using \texttt{(:= x c)}.
-        Instead, the list of instatiation terms must follow the variable
+        Instead, the list of instantiation terms must follow the variable
         order and cover all the respective bound variables.
   \item The rules \proofRule{and_pos}, \proofRule{or_neg}, \proofRule{and},
         \proofRule{not_or} now have one argument that indicates which subterm
         they use.
+  \item Add new syntax for decimal and negative numbers and use it
+        for \proofRule{la_generic}.
+  \item Restrict sorting of numbers such that the sort of a constant is
+        only determined by its syntactic category.
+  \item Add new syntax for decimal and negative numbers and clarify that
+        the set of allowed symbols is restricted to not conflict with this
+        new syntax.
+  \item Always use decimals for the constants in \proofRule{la_generic}.
+  \item Restrict sorting of numbers such that the sort of a constant is
+        only determined by its syntactic category.
 \end{itemize}
 
 \noindent

spec/doc.tex

@@ -214,7 +214,7 @@ break
   \textsuperscript{1} Universidade Federal de Minas Gerais, Brazil\\
   \textsuperscript{2} Albert-Ludwig-Universität Freiburg, Germany\\
   \textsuperscript{3} Université de Liège, Belgium\\
-  \textsuperscript{4} University of Iowa, Iowa City, USA\\
+  \textsuperscript{4} The University of Iowa, Iowa City, USA\\
 }
 
 
@@ -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,
@@ -691,6 +691,12 @@ An Alethe proof is a list of commands.
 \begin{figure}[t]
 \[
   \begin{array}{r c l}
+
+\multicolumn{3}{c}{
+	\text{A }\grNT{symbol}\text{ is an SMT-LIB }\grNT{symbol}\text{ that is not a}}\\
+& & -\grNT{numeral}/\grNT{positive\_numeral},\\
+& & -\grNT{numeral},\text{ or} -\grNT{decimal}.\\
+
  \grNT{proof}           &\grRule & \grNT{proof\_command}^{*} \\
  \grNT{proof\_command}  &\grRule & \textAlethe{(assume}\; \grNT{symbol}\; \grNT{proof\_term}\;\grNT{attribute}^{*}\,\textAlethe{)} \\
                         &\grOr   & \textAlethe{(step}\; \grNT{symbol}\; \grNT{clause}
@@ -704,6 +710,9 @@ 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{nonpositive\_numeral} \\
+                        & \grOr  & \grNT{nonpositive\_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 +720,17 @@ 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{positive\_numeral}    &\grRule & \text{any }\grNT{numeral}\text{ except } 0\\
+ \grNT{rational}              &\grRule & -^{?}\grNT{numeral}/\grNT{positive\_numeral} \\
+ \grNT{nonpositive\_numeral}  &\grRule & -\grNT{numeral} \\
+ \grNT{nonpositive\_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
@@ -740,12 +753,17 @@ is based on the {\smtlib} grammar, as defined in the {\smtlib}
 standard~\cite[Appendix~B]{SMTLIB}.  The non-terminals
 $\grNT{attribute}$,
 $\grNT{function\_def}$,
-$\grNT{sorted\_var}$,
-$\grNT{symbol}$, and
+$\grNT{sorted\_var}$, 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.
+A special restriction applies to the $\grNT{symbol}$ non-terminal.
+Alethe has an extended set of number literals.  Since these can start
+with a negation sign, they overlap SMT-LIB's $\grNT{symbol}$ non-terminal.
+For example, \inlineAlethe{-1} is a valid $\grNT{symbol}$ in SMT-LIB.
+These sequences cannot be used as symbols when using Alethe.
+Note that symbols are also used to name user defined constants and functions
+in the input problem.  Hence, Alethe cannot express proofs about problems
+that use such symbols.
 
 Alethe proofs are a list of commands.
 The \inlineAlethe{assume} command introduces a new assumption. While this
@@ -800,6 +818,35 @@ 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{nonpositive\_numeral}$ and $\grNT{nonpositive\_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{nonpositive\_decimal}$ is always \inlineAlethe{Real}.
+The sort of terms produced by $\grNT{integer}$ and $\grNT{nonpositive\_numeral}$
+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}.
+
 \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 +1030,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.
 

spec/rule_list.tex

@@ -427,9 +427,9 @@ $i$. & \ctxsep & $\varphi_1$, \dots , $\varphi_o$  & \currule\, [$a_1$, \dots, $
 where $\varphi_i$ is either $\neg l_i$ or $l_i$, but never $s_1
 ≈ s_2$.
 
-If the current theory does not have rational numbers, then the $a_i$ are
-printed using integer division. They should, nevertheless, be interpreted
-as rational numbers. If $d_1$ or $d_2$ are $0$, they might not be printed.
+The constants $a_i$ are of sort \inlineAlethe{Real} and must be printed
+using one of the productions $\grNT{rational}$
+$\grNT{decimal}$, $\grNT{nonpositive\_decimal}$.
 
 To check the unsatisfiability of the negation of $\varphi_1\lor \dots
 \lor \varphi_o$ one performs the following steps for each literal. For
@@ -481,7 +481,7 @@ A simple \proofRule{la_generic} step in the logic \textsf{LRA} might look like t
 
 \begin{AletheVerb}
 (step t10 (cl (not (> (f a) (f b))) (not (= (f a) (f b))))
-    :rule la_generic :args (1.0 (- 1.0)))
+    :rule la_generic :args (1.0 -1.0))
 \end{AletheVerb}
 
 To verify this we have to check the insatisfiability of $(f\,a) > (f\,b) \land
@@ -495,7 +495,7 @@ not apply. Finally, after step~5 the conjunction is $(f\,a) - (f\,b) > 0 \land
 The following \proofRule{la_generic} step is from a \textsf{QF\_UFLIA} problem:
 \begin{AletheVerb}
 (step t11 (cl (not (<= f3 0)) (<= (+ 1 (* 4 f3)) 1))
-    :rule la_generic :args (1 (div 1 4)))
+    :rule la_generic :args (1.0 1/4))
 \end{AletheVerb}
 After normalization we get $-f_3 \geq 0 \land 4\times f_3 > 0$.
 This time step~4 applies and we can strengthen this to