mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-05 06:46:11 +00:00
Code Activity

TPTP: quoted numeric tokens are distinct-objects/functors, not numerals

Browse source 
A double-quoted TPTP token such as "138" is a distinct object, and a
single-quoted '138' is a functor name; neither is an arithmetic numeral.
parse_name() strips the quotes, so the subsequent is_nonempty_digit_string
check was converting them into Int literals (then boxed Int->U),
mis-encoding distinct objects as equal numbers. Guard both numeral checks
(parse_term_primary and the atomic-formula parser) with !m_last_name_quoted
so only bare unquoted digit tokens become numerals.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-02 17:17:27 -07:00
parent cc5a2dae5e
commit c8e5dd0ca5
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/cmd_context/tptp_frontend.cpp
View file

@ -961,7 +961,7 @@ class tptp_parser {
if (n == "$true") return expr_ref(m.mk_true(), m);
if (n == "$false") return expr_ref(m.mk_false(), m);
if (is_nonempty_digit_string(n)) {
if (!m_last_name_quoted && is_nonempty_digit_string(n)) {
return parse_numeral_from_name(n);
}
@ -1416,7 +1416,7 @@ class tptp_parser {
if (n == "$true") return expr_ref(m.mk_true(), m);
if (n == "$false") return expr_ref(m.mk_false(), m);
if (is_nonempty_digit_string(n)) {
if (!m_last_name_quoted && is_nonempty_digit_string(n)) {
return parse_numeral_from_name(n);
}