From 36fffb3a2fb9c7b6aba44a23851f67ce6978801a Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 13 May 2026 06:03:53 -0400 Subject: [PATCH] TPTP frontend: fix TFF numeric atom typing, decimal literals, and `$uminus` (#9518) This PR targets the main TFF frontend parsing failures: bare numeric atoms were being treated as uninterpreted terms (`U`) in formula position, decimal literals were not parsed, and `$uminus` was not recognized as an arithmetic builtin. These issues caused widespread parse/type failures in arithmetic-heavy TPTP inputs. - **Numeric atom parsing in formulas (TFF)** - Added a shared numeric-literal parser path for term/formula contexts. - In atomic formulas, numeric LHS now parses as arithmetic numerals before `=`/`!=` handling, avoiding `U` vs `Int/Real` mismatches. - **Decimal literal support** - Extended numeral parsing to accept `d.d` forms and construct `Real` numerals. - Keeps existing integer (`d`) and rational (`d/d`) behavior on the same code path. - **`$uminus` builtin support** - Added explicit handling for `$uminus()` in term parsing. - Enforces arity 1 and arithmetic-argument checks; maps directly to arithmetic unary minus. - **Focused regression coverage** - Added/updated TPTP unit cases for: - bare integer inequality: `31 != 12` - decimal arithmetic literal usage - `$uminus` in arithmetic predicates Example of now-supported inputs: ```tptp tff(c1,conjecture, 31 != 12). tff(c2,conjecture, ~ $less(-3.25,-8.69)). tff(c3,conjecture, $less($uminus(2),0)). ``` --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/cmd_context/tptp_frontend.cpp | 59 +++++++++++++++++++++++++------ src/test/tptp.cpp | 9 +++++ 2 files changed, 57 insertions(+), 11 deletions(-) diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index 8ab66ac1d..52f52209c 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -340,6 +340,32 @@ class tptp_parser { return true; } + expr_ref parse_numeral_from_name(std::string const& n) { + SASSERT(is_nonempty_digit_string(n)); + rational num(n.c_str()); + if (accept(token_kind::dot)) { + std::string frac = parse_name(); + if (!is_nonempty_digit_string(frac)) + throw parse_error("fractional part of decimal literal must be a sequence of digits"); + rational den(1); + for (unsigned i = 0; i < frac.size(); ++i) { + den *= rational(10); + } + rational frac_num(frac.c_str()); + return expr_ref(m_arith.mk_numeral(num + frac_num / den, false), m); + } + if (accept(token_kind::slash_tok)) { + std::string d = parse_name(); + if (!is_nonempty_digit_string(d)) + throw parse_error("denominator of rational literal must be a sequence of digits"); + rational den(d.c_str()); + if (den.is_zero()) + throw parse_error("denominator of rational literal cannot be zero"); + return expr_ref(m_arith.mk_numeral(num / den, false), m); + } + return expr_ref(m_arith.mk_numeral(num, true), m); + } + static std::string mk_decl_key(std::string const& name, unsigned arity, char tag) { return std::to_string(name.size()) + ":" + name + "\x1f" + std::to_string(arity) + "\x1f" + tag; } @@ -470,17 +496,7 @@ class tptp_parser { if (n == "$false") return expr_ref(m.mk_false(), m); if (is_nonempty_digit_string(n)) { - rational num(n.c_str()); - if (accept(token_kind::slash_tok)) { - std::string d = parse_name(); - if (!is_nonempty_digit_string(d)) - throw parse_error("denominator of rational literal must be a sequence of digits"); - rational den(d.c_str()); - if (den.is_zero()) - throw parse_error("denominator of rational literal cannot be zero"); - return expr_ref(m_arith.mk_numeral(num / den, false), m); - } - return expr_ref(m_arith.mk_numeral(num, true), m); + return parse_numeral_from_name(n); } expr_ref b(m); @@ -495,6 +511,15 @@ class tptp_parser { } } + if (n == "$uminus") { + if (args.size() != 1) + throw parse_error("arithmetic function '$uminus' expects arity 1"); + expr_ref a(args.get(0), m); + if (!m_arith.is_int_real(a)) + throw parse_error("arithmetic function '$uminus' expects arithmetic argument"); + return expr_ref(m_arith.mk_uminus(a), m); + } + func_decl* f = mk_decl(n, args.size(), false); return expr_ref(args.empty() ? m.mk_const(f) : m.mk_app(f, args.size(), args.data()), m); } @@ -512,6 +537,18 @@ 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)) { + expr_ref lhs = parse_numeral_from_name(n); + if (is(token_kind::equal_tok) || is(token_kind::neq_tok)) { + bool neq = accept(token_kind::neq_tok); + if (!neq) expect(token_kind::equal_tok, "'='"); + expr_ref rhs = parse_term(); + expr_ref eq(m.mk_eq(lhs, rhs), m); + return neq ? expr_ref(m.mk_not(eq), m) : eq; + } + throw parse_error("numeric term used as formula"); + } + expr_ref_vector args(m); if (accept(token_kind::lparen)) { if (!accept(token_kind::rparen)) { diff --git a/src/test/tptp.cpp b/src/test/tptp.cpp index 2ae2fb4f6..b7ef79520 100644 --- a/src/test/tptp.cpp +++ b/src/test/tptp.cpp @@ -81,6 +81,15 @@ R"(tff(c1,conjecture, ? [X: $int] : $less(12,X)).)", "% SZS status Theorem"}, {"tff-lesseq-built-in", R"(tff(c1,conjecture, $lesseq(2,2)).)", + "% SZS status Theorem"}, + {"tff-bare-integer-equality", +R"(tff(c1,conjecture, 31 != 12).)", + "% SZS status Theorem"}, + {"tff-decimal-literal", +R"(tff(c1,conjecture, ~ $less(-3.25,-8.69)).)", + "% SZS status Theorem"}, + {"tff-uminus-built-in", +R"(tff(c1,conjecture, $less($uminus(2),0)).)", "% SZS status Theorem"} }; for (auto const& c : cases) {