From 975d34e290f071ee26cbcec4f063bd26f762dc83 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 13 May 2026 01:42:53 +0000
Subject: [PATCH] fix tptp frontend numerals decimals and uminus

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/82e477c0-dbdc-4983-b04c-236cf2bc43dc

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