From 7658141c0bbf4904dc8fb86d0430dc4583841eaf Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 13 May 2026 15:57:34 +0000 Subject: [PATCH] Clean up implicit variable handling helpers in TPTP parser Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/38c3a47d-1e93-48d8-8fa4-1dfc724e76e5 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/cmd_context/tptp_frontend.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index 671059984..ba3d4ad3b 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -412,9 +412,13 @@ class tptp_parser { return false; } + bool should_create_implicit_var(std::string const& n) const { + return is_var_name(n) && m_implicit_scope; + } + app* get_or_create_implicit_var(std::string const& n) { if (!m_implicit_scope) - throw parse_error("internal parser error: implicit variable scope is missing (unexpected parser state)"); + throw parse_error("unexpected parser state: missing implicit variable scope"); auto it = m_implicit_scope->vars.find(n); if (it != m_implicit_scope->vars.end()) return it->second; app* c = m.mk_const(symbol(n), m_univ); @@ -536,7 +540,7 @@ class tptp_parser { expr_ref b(m); if (is_var_name(n) && find_bound(n, b)) return b; - if (is_var_name(n) && m_implicit_scope) + if (should_create_implicit_var(n)) return expr_ref(get_or_create_implicit_var(n), m); expr_ref_vector args(m); @@ -624,7 +628,7 @@ class tptp_parser { lhs = b; has_lhs = true; } - else if (is_var_name(n) && m_implicit_scope) { + else if (should_create_implicit_var(n)) { lhs = expr_ref(get_or_create_implicit_var(n), m); has_lhs = true; }