mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 15:15:35 +00:00
Code Activity

fix tptp frontend numerals decimals and uminus

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

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-13 01:42:53 +00:00 • committed by GitHub
parent fe84156ad7
commit 975d34e290
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 57 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

59
src/cmd_context/tptp_frontend.cpp
View file

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

9
src/test/tptp.cpp
View file

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