From ce07160d644f93e09166b81e07522e1c2a1fcf9f Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 13 May 2026 13:19:14 -0400 Subject: [PATCH] TPTP frontend: enforce implicit universal quantification for free variables and add regression coverage (#9527) Discussion #9524 reported systematic TPTP result polarity errors (notably `Unsatisfiable/Theorem` cases returned as `Satisfiable`) and timeout-path instability in the frontend. The dominant issue was semantic: free variables in FOF/CNF formulas were parsed as constants instead of implicitly universally quantified variables. - **Parser semantics: free variables now follow TPTP rules** - In `/home/runner/work/z3/z3/src/cmd_context/tptp_frontend.cpp`, free variables encountered while parsing an annotated formula are now collected in formula scope and wrapped with a top-level `forall`. - This applies to both term and atomic-formula paths, so variable occurrences are treated consistently. - Explicitly bound quantifier variables continue to take precedence over implicit ones. - **Scoped implementation cleanup** - Added scoped state for implicit-variable collection to avoid leaking parser state across formulas. - Kept variable binding order stable so quantifier construction is deterministic. - **Timeout-path robustness** - Updated frontend exception catches to `const&` in the TPTP stream entrypoint to make timeout/error handling behavior consistent with thrown exception forms. - **Regression tests** - Extended `/home/runner/work/z3/z3/src/test/tptp.cpp` with focused cases for: - FOF free-variable implicit universal quantification. - CNF free-variable implicit universal quantification. ```tptp cnf(c1,axiom, p(X)). cnf(c2,axiom, ~ p(a)). ``` This now maps to `forall X. p(X)` plus `~p(a)`, yielding `% SZS status Unsatisfiable` as expected. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/cmd_context/tptp_frontend.cpp | 53 +++++++++++++++++++++++++++++-- src/test/tptp.cpp | 8 +++++ 2 files changed, 59 insertions(+), 2 deletions(-) diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index 2c7030ec9..e787fc29f 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -265,6 +265,11 @@ class tptp_parser { func_decl_ref_vector m_pinned_decls; // prevents cached func_decls from being freed std::unordered_map, sort*>> m_typed_decls; std::vector> m_bound; + struct implicit_var_scope { + std::unordered_map vars; + ptr_vector order; + }; + implicit_var_scope* m_implicit_scope = nullptr; std::unordered_set m_seen_files; std::string m_input; @@ -454,6 +459,39 @@ 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("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); + m_implicit_scope->vars.emplace(n, c); + m_implicit_scope->order.push_back(c); + return c; + } + + class scoped_implicit_vars { + tptp_parser& m_p; + implicit_var_scope* m_prev_scope; + public: + scoped_implicit_vars(tptp_parser& p, implicit_var_scope& scope): + m_p(p), + m_prev_scope(p.m_implicit_scope) { + m_p.m_implicit_scope = &scope; + } + scoped_implicit_vars(scoped_implicit_vars const&) = delete; + scoped_implicit_vars& operator=(scoped_implicit_vars const&) = delete; + scoped_implicit_vars(scoped_implicit_vars&&) = delete; + scoped_implicit_vars& operator=(scoped_implicit_vars&&) = delete; + ~scoped_implicit_vars() { + m_p.m_implicit_scope = m_prev_scope; + } + }; + expr_ref mk_quantifier(bool is_forall, ptr_vector const& bound, expr_ref const& body) { SASSERT(body); if (bound.empty()) return body; @@ -607,6 +645,8 @@ class tptp_parser { expr_ref b(m); if (is_var_name(n) && find_bound(n, b)) return b; + if (should_create_implicit_var(n)) + return expr_ref(get_or_create_implicit_var(n), m); expr_ref_vector args(m); if (accept(token_kind::lparen)) { @@ -823,6 +863,10 @@ class tptp_parser { lhs = b; has_lhs = true; } + else if (should_create_implicit_var(n)) { + lhs = expr_ref(get_or_create_implicit_var(n), m); + has_lhs = true; + } } if (is(token_kind::equal_tok) || is(token_kind::neq_tok)) { @@ -1076,7 +1120,12 @@ class tptp_parser { parse_type_decl_formula(); } else { + implicit_var_scope implicit_scope; + scoped_implicit_vars scoped(*this, implicit_scope); expr_ref f = parse_formula(); + if (!implicit_scope.order.empty()) { + f = mk_quantifier(true, implicit_scope.order, f); + } if (role == "conjecture") { m_has_conjecture = true; f = m.mk_not(f); @@ -1249,7 +1298,7 @@ static unsigned read_tptp_stream(std::istream& in, char const* current_file) { std::cerr << "TPTP parse error: " << ex.what() << "\n"; return ERR_PARSER; } - catch (z3_error& ex) { + catch (z3_error const& ex) { if (ex.error_code() == ERR_TIMEOUT) { std::cout << "% SZS status Timeout\n"; return 0; @@ -1257,7 +1306,7 @@ static unsigned read_tptp_stream(std::istream& in, char const* current_file) { std::cerr << "TPTP frontend error: " << ex.what() << "\n"; return ERR_INTERNAL_FATAL; } - catch (z3_exception& ex) { + catch (z3_exception const& ex) { std::cerr << "TPTP frontend error: " << ex.what() << "\n"; return ERR_INTERNAL_FATAL; } diff --git a/src/test/tptp.cpp b/src/test/tptp.cpp index b7ef79520..6b7bdf1b7 100644 --- a/src/test/tptp.cpp +++ b/src/test/tptp.cpp @@ -65,6 +65,14 @@ fof(c1,conjecture, mortal(socrates)).)", {"simple-sat", R"(fof(a1,axiom, p(a)).)", "% SZS status Satisfiable"}, + {"fof-implicit-forall", +R"(fof(a1,axiom, p(X)). +fof(c1,conjecture, p(a)).)", + "% SZS status Theorem"}, + {"cnf-implicit-forall", +R"(cnf(c1,axiom, p(X)). +cnf(c2,axiom, ~ p(a)).)", + "% SZS status Unsatisfiable"}, {"tff-negative-literal", R"(tff(c1,conjecture, $less(-2,2)).)", "% SZS status Theorem"},