From fce83df3fc2a957952cea442eccb056cf8370da0 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 8 May 2026 17:22:02 +0000
Subject: [PATCH] Fix TPTP frontend build integration and validate with tests

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/ba80bc5a-d80f-4d9f-8ed4-a962f697697c

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 scripts/mk_project.py       |  4 +--
 src/shell/tptp_frontend.cpp | 54 ++++++++++++++++++-------------------
 2 files changed, 28 insertions(+), 30 deletions(-)

diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 7b4d444ea..7faaa4f60 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -98,7 +98,7 @@ def init_project_def():
     API_files = ['z3_api.h', 'z3_ast_containers.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_fixedpoint.h', 'z3_optimization.h', 'z3_fpa.h', 'z3_spacer.h']
     add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'qe', 'euf', 'arith_tactics'], 'cmd_context/extra_cmds')
     add_lib('api', ['portfolio',  'realclosure', 'opt', 'extra_cmds'],
-            includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
+            includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h', 'c++/z3++.h'] + API_files)
     add_exe('shell', ['api', 'sat', 'extra_cmds', 'opt'], exe_name='z3')
     add_exe('test', ['api', 'fuzzing', 'simplex', 'sat_smt'], exe_name='test-z3', install=False)
     _libz3Component = add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll',
@@ -125,5 +125,3 @@ def init_project_def():
     add_ml_example('ml_example', 'ml')
     add_z3py_example('py_example', 'python')
     return API_files
-
-
diff --git a/src/shell/tptp_frontend.cpp b/src/shell/tptp_frontend.cpp
index b7dab46fa..90b11fe3b 100644
--- a/src/shell/tptp_frontend.cpp
+++ b/src/shell/tptp_frontend.cpp
@@ -9,7 +9,7 @@
 #include <memory>
 #include <vector>
 
-#include "api/c++/z3++.h"
+#include <api/c++/z3++.h>
 #include "shell/tptp_frontend.h"
 #include "util/error_codes.h"
 
@@ -442,21 +442,6 @@ class tptp_parser {
         return f(static_cast<unsigned>(tmp.size()), tmp.data());
     }
 
-    z3::expr parse_term() {
-        z3::expr e = parse_term_primary();
-        while (accept(token_kind::at_tok)) {
-            z3::expr arg = parse_term_primary();
-            if (!e.is_app() || e.decl().decl_kind() != Z3_OP_UNINTERPRETED)
-                throw parse_error("higher-order application is unsupported");
-            z3::func_decl f = e.decl();
-            std::vector<z3::expr> args;
-            for (unsigned i = 0; i < e.num_args(); ++i) args.push_back(e.arg(i));
-            args.push_back(arg);
-            e = f(static_cast<unsigned>(args.size()), args.data());
-        }
-        return e;
-    }
-
     z3::expr parse_formula();
 
     z3::expr parse_atomic_formula() {
@@ -574,17 +559,6 @@ class tptp_parser {
         return e;
     }
 
-    z3::expr parse_formula() {
-        z3::expr e = parse_implies_formula();
-        while (is(token_kind::iff_tok) || is(token_kind::xor_tok)) {
-            bool is_xor = accept(token_kind::xor_tok);
-            if (!is_xor) expect(token_kind::iff_tok, "'<=>'");
-            z3::expr rhs = parse_implies_formula();
-            e = is_xor ? !(e == rhs) : (e == rhs);
-        }
-        return e;
-    }
-
     void parse_type_decl_formula() {
         while (accept(token_kind::lparen)) {}
         std::string name = parse_name();
@@ -732,6 +706,32 @@ public:
     bool has_conjecture() const { return m_has_conjecture; }
 };
 
+z3::expr tptp_parser::parse_term() {
+    z3::expr e = parse_term_primary();
+    while (accept(token_kind::at_tok)) {
+        z3::expr arg = parse_term_primary();
+        if (!e.is_app() || e.decl().decl_kind() != Z3_OP_UNINTERPRETED)
+            throw parse_error("higher-order application is unsupported");
+        z3::func_decl f = e.decl();
+        std::vector<z3::expr> args;
+        for (unsigned i = 0; i < e.num_args(); ++i) args.push_back(e.arg(i));
+        args.push_back(arg);
+        e = f(static_cast<unsigned>(args.size()), args.data());
+    }
+    return e;
+}
+
+z3::expr tptp_parser::parse_formula() {
+    z3::expr e = parse_implies_formula();
+    while (is(token_kind::iff_tok) || is(token_kind::xor_tok)) {
+        bool is_xor = accept(token_kind::xor_tok);
+        if (!is_xor) expect(token_kind::iff_tok, "'<=>'");
+        z3::expr rhs = parse_implies_formula();
+        e = is_xor ? !(e == rhs) : (e == rhs);
+    }
+    return e;
+}
+
 }
 
 unsigned read_tptp(char const* file_name) {