From 0258cc6cea51e7384544d1e0d887241e34ae0868 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Thu, 23 May 2024 18:44:38 -0500
Subject: [PATCH] No division by 0 in rational constants
---
spec/doc.tex | 13 +++++++------
spec/rule_list.tex | 2 +-
2 files changed, 8 insertions(+), 7 deletions(-)
diff --git a/spec/doc.tex b/spec/doc.tex
index 6c05ce9..50ca0aa 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -712,9 +712,10 @@ 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} \\
+ \grNT{positive\_numeral} &\grRule & \text{any }\grNT{numeral}\text{ except } 0\\
+ \grNT{rational} &\grRule & -^{?}\grNT{numeral}/\grNT{positive\_numeral} \\
+ \grNT{negative\_numeral} &\grRule & -\grNT{numeral} \\
+ \grNT{negative\_decimal} &\grRule & -\grNT{decimal} \\
\end{array}
\]
\caption{The proof grammar.}
@@ -817,14 +818,14 @@ 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}$
+Furthermore, the non-terminals $\grNT{negative\_numeral}$ and $\grNT{negative\_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}$
+$\grNT{negative\_decimal}$ is always \inlineAlethe{Real}.
+The sort of terms produced by $\grNT{integer}$ and $\grNT{negative\_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
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 10e4aae..ca7d00d 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -429,7 +429,7 @@ where $\varphi_i$ is either $\neg l_i$ or $l_i$, but never $s_1
The constants $a_i$ are of sort \inlineAlethe{Real} and must be printed
using one of the productions $\grNT{rational}$
-$\grNT{decimal}$, $\grNT{neg\_decimal}$.
+$\grNT{decimal}$, $\grNT{negative\_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
--
GitLab