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

Polish tptp stream parser naming and simplify test asserts

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/1be7cf7e-2747-43ba-9a33-2e71dad2d14d

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

8
src/cmd_context/tptp_frontend.cpp
View file

@ -727,7 +727,7 @@ public:
m_sorts.emplace("$real", m_arith.mk_real());
}
void parse_stream(std::istream& in, std::string const& current_file) {
void parse_input(std::istream& in, std::string const& current_file) {
std::ostringstream buf;
buf << in.rdbuf();
m_input = buf.str();
@ -744,11 +744,11 @@ public:
out << "failed to open file '" << filename << "'";
throw parse_error(out.str());
}
parse_stream(in, filename);
parse_input(in, filename);
}
void parse_stream(std::istream& in) {
parse_stream(in, ".");
parse_input(in, ".");
}
bool has_conjecture() const { return m_has_conjecture; }
@ -792,7 +792,7 @@ static unsigned read_tptp_stream(std::istream& in, char const* current_file) {
ctx.set_solver_factory(mk_smt_strategic_solver_factory());
tptp_parser p(ctx);
p.parse_stream(in, current_file ? current_file : ".");
p.parse_input(in, current_file ? current_file : ".");
// Suppress default check-sat output; TPTP frontend reports SZS status explicitly.
std::ostringstream sink;

2
src/test/tptp.cpp
View file

@ -54,8 +54,6 @@ R"(fof(a1,axiom, p(a)).)",
};
for (auto const& c : cases) {
std::string out = run_tptp(c.input);
if (out.find(c.expected_status) == std::string::npos)
std::cerr << "Unexpected TPTP status for case: " << c.name << "\n" << out << "\n";
ENSURE(out.find(c.expected_status) != std::string::npos);
}
}