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

Refine TPTP frontend ownership and stream restoration semantics

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/2a6b01d0-c799-4e44-aa73-ef228cb4402e

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-10 15:23:04 +00:00 • committed by GitHub
parent 1c490cbc85
commit 428d0b4b66
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 7 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/shell/tptp_frontend.cpp
View file

@ -60,9 +60,10 @@ struct parse_error : public std::exception {
class scoped_regular_stream {
cmd_context& m_ctx;
std::string m_prev;
public:
scoped_regular_stream(cmd_context& ctx, std::ostream& out): m_ctx(ctx) { m_ctx.set_regular_stream(out); }
~scoped_regular_stream() { m_ctx.set_regular_stream("stdout"); }
scoped_regular_stream(cmd_context& ctx, std::ostream& out): m_ctx(ctx), m_prev(ctx.get_regular_stream_name()) { m_ctx.set_regular_stream(out); }
~scoped_regular_stream() { m_ctx.set_regular_stream(m_prev.c_str()); }
};
struct token {
@ -374,10 +375,10 @@ class tptp_parser {
return false;
}
expr_ref mk_quantifier(bool is_forall, ptr_vector<app> const& bound, expr* body) {
expr_ref mk_quantifier(bool is_forall, ptr_vector<app> const& bound, expr_ref const& body) {
SASSERT(body);
if (bound.empty()) return expr_ref(body, m);
return is_forall ? ::mk_forall(m, bound.size(), bound.data(), body) : ::mk_exists(m, bound.size(), bound.data(), body);
if (bound.empty()) return body;
return is_forall ? ::mk_forall(m, bound.size(), bound.data(), body.get()) : ::mk_exists(m, bound.size(), bound.data(), body.get());
}
parsed_type parse_type_atom() {
@ -767,7 +768,7 @@ expr_ref tptp_parser::parse_term() {
expr_ref_vector args(m);
for (unsigned i = 0; i < a->get_num_args(); ++i) args.push_back(a->get_arg(i));
args.push_back(arg);
e = m.mk_app(d, args.size(), args.data());
e = expr_ref(m.mk_app(d, args.size(), args.data()), m);
}
return e;
}