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(<arg>)` 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

@@ -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)) {

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) {