From 855d4a4fc088811048d2a02c3c6f6585aa21dab6 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Fri, 30 Jul 2021 19:00:58 +0200
Subject: [PATCH] Fix choice grammar, and refactor grammar while we're at it
---
spec/changelog.tex | 6 ++++++
spec/doc.tex | 17 ++++++++---------
2 files changed, 14 insertions(+), 9 deletions(-)
diff --git a/spec/changelog.tex b/spec/changelog.tex
index 69bbc74..c088145 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -4,6 +4,11 @@ List of rules:
\begin{itemize}
\item Improve description of $\proofRule{sko\_ex}$.
\end{itemize}
+\noindent
+Corrections:
+\begin{itemize}
+ \item Grammar: the \texttt{choice} binder can only bind one variable.
+\end{itemize}
\noindent
Clarifications:
@@ -14,6 +19,7 @@ Clarifications:
\item Fix linear arithmetic example in introduction.
\end{itemize}
+
\subsection*{0.1 --- \DTMdisplaydate{2021}{07}{10}{-1}}
This is the first public release of this document. It coincides with
diff --git a/spec/doc.tex b/spec/doc.tex
index bc950bf..b1673e3 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -1033,28 +1033,27 @@ production for the $\grT{choice}$ binder.
\grNT{proof\_command} &\grRule& \grT{(assume}\; \grNT{symbol}\; \grNT{proof\_term}\; \grT{)}\\
&\grOr & \grT{(step}\; \grNT{symbol}\; \grNT{clause}
\; \grT{:rule}\; \grNT{symbol}\\
- & & \quad\grNT{step\_annotation}\; \grT{)}\\
+ & & \quad\grNT{step\_annotation}^{?}\; \grT{)}\\
& \grOr & \grT{(anchor}\; \grT{:step}\; \grNT{symbol}\; \grT{)}\\
& \grOr & \grT{(anchor}\; \grT{:step}\; \grNT{symbol}\;
\grT{:args}\; \grNT{proof\_args}\; \grT{)}\\
& \grOr & \grT{(define-fun}\; \grNT{function\_def}\; \grT{)}\\
\grNT{clause} &\grRule& \grT{(cl}\; \grNT{proof\_term}^{*}\; \grT{)}\\
- \grNT{step\_annotation} &\grRule&
- \grT{:premises (}\; \grNT{symbol}^{+}\; \grT{)}\;\\
- & \grOr & \grT{:args}\; \grNT{proof_args}\\
- & \grOr & \grT{:premises (}\; \grNT{symbol}^{+}\; \grT{)}\;
- \grT{:args}\; \grNT{proof_args}\\
+
+ \grNT{step\_annotation} &\grRule& \grNT{premises\_annotation}^{?}\;\grNT{args\_annotation}\\
+
+ \grNT{premises\_annotation} &\grRule& \grT{:premises (}\; \grNT{symbol}^{+}\grT{)}\\
+ \grNT{args\_annotation} &\grRule& \grT{:args}\; \grNT{proof_args}\\
+
\grNT{proof\_args} &\grRule& \grT{(}\; \grNT{proof\_arg}^{+}\; \grT{)}\\
\grNT{proof\_arg} &\grRule& \grNT{symbol} \grOr
\grT{(}\; \grNT{symbol}\; \grNT{proof\_term}\; \grT{)}\\
\grNT{proof\_term} &\grRule& \grNT{term}\text{ extended with }\\
- & & \grT{(choice (}\; \grNT{sorted\_var}^{+}\;\grT{)}\; \grNT{proof\_term}\; \grT{)}
+ & & \grT{(choice (}\; \grNT{sorted\_var}\;\grT{)}\; \grNT{proof\_term}\; \grT{)}
\end{array}\]
}\par}
\caption{The proof grammar}\label{fig:grammar}
\end{figure}
-% PF TODO: factorize <arg_annotation> and <premise_annotation>
-% PF TODO: introduce ^? to denote optional non-terminal
Input problems in the SMT-LIB standard contain a list of \emph{commands}
that modify the internal state of the solver. In agreement
--
GitLab