mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-22 09:59:36 +00:00
Code Activity

Add rational zero-denominator regression test for TPTP

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/f2be81f6-e506-47ea-a38a-46d1970add8c

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-12 18:54:41 +00:00 • committed by GitHub
parent e0c13aee15
commit 37bfafa407
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 25 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/cmd_context/tptp_frontend.cpp
View file

@ -331,7 +331,7 @@ class tptp_parser {
return s->get_name() == symbol("$tType"); return s->get_name() == symbol("$tType");
} }
static bool contains_only_digits(std::string const& s) { static bool is_nonempty_digit_string(std::string const& s) {
if (s.empty()) return false; if (s.empty()) return false;
for (char c : s) { for (char c : s) {
if (!std::isdigit(static_cast<unsigned char>(c))) if (!std::isdigit(static_cast<unsigned char>(c)))
@ -469,11 +469,11 @@ class tptp_parser {
if (n == "$true") return expr_ref(m.mk_true(), m); if (n == "$true") return expr_ref(m.mk_true(), m);
if (n == "$false") return expr_ref(m.mk_false(), m); if (n == "$false") return expr_ref(m.mk_false(), m);
if (contains_only_digits(n)) { if (is_nonempty_digit_string(n)) {
rational num(n.c_str()); rational num(n.c_str());
if (accept(token_kind::slash_tok)) { if (accept(token_kind::slash_tok)) {
std::string d = parse_name(); std::string d = parse_name();
if (!contains_only_digits(d)) if (!is_nonempty_digit_string(d))
throw parse_error("denominator of rational literal must be a sequence of digits"); throw parse_error("denominator of rational literal must be a sequence of digits");
rational den(d.c_str()); rational den(d.c_str());
if (den.is_zero()) if (den.is_zero())

26
src/test/tptp.cpp
View file

@ -3,6 +3,7 @@
#include <iostream> #include <iostream>
#include <sstream> #include <sstream>
#include "util/debug.h" #include "util/debug.h"
#include "util/error_codes.h"
#include "cmd_context/tptp_frontend.h" #include "cmd_context/tptp_frontend.h"
struct tptp_case { struct tptp_case {
@ -11,14 +12,26 @@ struct tptp_case {
char const* expected_status; char const* expected_status;
}; };
static std::string run_tptp(char const* input) { static unsigned run_tptp(char const* input, std::string& out, std::string& err) {
std::streambuf* old_out = std::cout.rdbuf(); std::streambuf* old_out = std::cout.rdbuf();
std::ostringstream out; std::streambuf* old_err = std::cerr.rdbuf();
std::cout.rdbuf(out.rdbuf()); std::ostringstream out_buf;
std::ostringstream err_buf;
std::cout.rdbuf(out_buf.rdbuf());
std::cerr.rdbuf(err_buf.rdbuf());
unsigned code = read_tptp_string(input); unsigned code = read_tptp_string(input);
std::cout.rdbuf(old_out); std::cout.rdbuf(old_out);
std::cerr.rdbuf(old_err);
out = out_buf.str();
err = err_buf.str();
return code;
}
static std::string run_tptp(char const* input) {
std::string out, err;
unsigned code = run_tptp(input, out, err);
ENSURE(code == 0); ENSURE(code == 0);
return out.str(); return out;
} }
// Required externs from shell/tptp_frontend.cpp; keep output minimal in tests. // Required externs from shell/tptp_frontend.cpp; keep output minimal in tests.
@ -73,4 +86,9 @@ R"(tff(c1,conjecture, $lesseq(2,2)).)",
std::string out = run_tptp(c.input); std::string out = run_tptp(c.input);
ENSURE(out.find(c.expected_status) != std::string::npos); ENSURE(out.find(c.expected_status) != std::string::npos);
} }
std::string out, err;
unsigned code = run_tptp("tff(c1,conjecture, $less(1/0,1)).", out, err);
ENSURE(code == ERR_PARSER);
ENSURE(err.find("denominator of rational literal cannot be zero") != std::string::npos);
} }