From 1af8428755d280d0799320cd9090061fe6769e01 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 11 May 2026 06:56:24 +0000
Subject: [PATCH] Add TPTP regression files and test-z3 tptp test

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/dc1d46fc-4b6c-4f64-91a0-9fb57c73c166

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/test/CMakeLists.txt          |  6 ++--
 src/test/main.cpp                |  1 +
 src/test/tptp.cpp                | 52 ++++++++++++++++++++++++++++++++
 src/test/tptp/agatha-butler.p    | 19 ++++++++++++
 src/test/tptp/simple-sat.p       |  2 ++
 src/test/tptp/socrates-theorem.p |  4 +++
 6 files changed, 81 insertions(+), 3 deletions(-)
 create mode 100644 src/test/tptp.cpp
 create mode 100644 src/test/tptp/agatha-butler.p
 create mode 100644 src/test/tptp/simple-sat.p
 create mode 100644 src/test/tptp/socrates-theorem.p

diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt
index 319cd829b..00d129c0b 100644
--- a/src/test/CMakeLists.txt
+++ b/src/test/CMakeLists.txt
@@ -145,6 +145,7 @@ add_executable(test-z3
   theory_dl.cpp
   theory_pb.cpp
   timeout.cpp
+  tptp.cpp
   total_order.cpp
   totalizer.cpp
   trigo.cpp
@@ -163,12 +164,11 @@ add_executable(test-z3
 z3_add_install_tactic_rule(${z3_test_deps})
 z3_add_memory_initializer_rule(${z3_test_deps})
 z3_add_gparams_register_modules_rule(${z3_test_deps})
-target_compile_definitions(test-z3 PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
+target_compile_definitions(test-z3 PRIVATE ${Z3_COMPONENT_CXX_DEFINES} Z3_TEST_SRC_DIR="${CMAKE_CURRENT_SOURCE_DIR}" Z3_TEST_BIN_DIR="${PROJECT_BINARY_DIR}")
 target_compile_options(test-z3 PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
 target_link_libraries(test-z3 PRIVATE ${Z3_DEPENDENT_LIBS})
 target_include_directories(test-z3 PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
 z3_append_linker_flag_list_to_target(test-z3 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
 z3_add_component_dependencies_to_target(test-z3 ${z3_test_expanded_deps})
-
-
+add_dependencies(test-z3 shell)
 
diff --git a/src/test/main.cpp b/src/test/main.cpp
index f1d874e00..6c0052094 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -120,6 +120,7 @@
     X(model_based_opt) \
     X(factor_rewriter) \
     X(smt2print_parse) \
+    X(tptp) \
     X(substitution) \
     X(polynomial) \
     X(polynomial_factorization) \
diff --git a/src/test/tptp.cpp b/src/test/tptp.cpp
new file mode 100644
index 000000000..a374401db
--- /dev/null
+++ b/src/test/tptp.cpp
@@ -0,0 +1,52 @@
+#include <cstdio>
+#include <sstream>
+#include <string>
+#include <vector>
+#include "util/debug.h"
+
+#ifdef _WINDOWS
+#define Z3_POPEN  _popen
+#define Z3_PCLOSE _pclose
+static char const* z3_bin_name = "z3.exe";
+#else
+#include <sys/wait.h>
+#define Z3_POPEN  popen
+#define Z3_PCLOSE pclose
+static char const* z3_bin_name = "z3";
+#endif
+
+struct tptp_case {
+    char const* file;
+    char const* expected_status;
+};
+
+static std::string run_tptp(char const* file) {
+    std::ostringstream cmd;
+    cmd << "\"" << Z3_TEST_BIN_DIR << "/" << z3_bin_name << "\" -tptp "
+        << "\"" << Z3_TEST_SRC_DIR << "/tptp/" << file << "\" 2>&1";
+    FILE* pipe = Z3_POPEN(cmd.str().c_str(), "r");
+    ENSURE(pipe != nullptr);
+    std::string out;
+    char buffer[4096];
+    while (fgets(buffer, sizeof(buffer), pipe))
+        out += buffer;
+    int code = Z3_PCLOSE(pipe);
+#ifndef _WINDOWS
+    if (WIFEXITED(code))
+        code = WEXITSTATUS(code);
+#endif
+    ENSURE(code == 0);
+    return out;
+}
+
+void tst_tptp() {
+    std::vector<tptp_case> cases = {
+        {"agatha-butler.p", "% SZS status CounterSatisfiable"},
+        {"socrates-theorem.p", "% SZS status Theorem"},
+        {"simple-sat.p", "% SZS status Satisfiable"}
+    };
+    for (auto const& c : cases) {
+        std::string out = run_tptp(c.file);
+        ENSURE(out.find(c.expected_status) != std::string::npos);
+    }
+}
diff --git a/src/test/tptp/agatha-butler.p b/src/test/tptp/agatha-butler.p
new file mode 100644
index 000000000..d5bbded75
--- /dev/null
+++ b/src/test/tptp/agatha-butler.p
@@ -0,0 +1,19 @@
+fof(ax1,axiom, lives(agatha)).
+fof(ax2,axiom, lives(butler)).
+fof(ax3,axiom, lives(charles)).
+
+fof(ax4,axiom, ! [X] : (lives(X) => (X = agatha | X = butler | X = charles))).
+fof(ax5,axiom, ! [X,Y] : (killed(X,Y) => hates(X,Y))).
+fof(ax6,axiom, ! [X,Y] : (killed(X,Y) => ~ richer(X,Y))).
+
+fof(ax7,axiom, ! [X] : (hates(agatha,X) => ~ hates(charles,X))).
+fof(ax8,axiom, ! [X] : (X != butler => hates(agatha,X))).
+fof(ax9,axiom, ! [X] : (~ richer(X,agatha) => hates(butler,X))).
+fof(ax10,axiom, ! [X] : (hates(agatha,X) => hates(butler,X))).
+fof(ax11,axiom, ! [X] : (? [Y] : ~ hates(X,Y))).
+
+fof(ax12,axiom, agatha != butler).
+fof(ax13,axiom, ? [X] : killed(X,agatha)).
+
+fof(conj,conjecture, killed(agatha,agatha)).
+
diff --git a/src/test/tptp/simple-sat.p b/src/test/tptp/simple-sat.p
new file mode 100644
index 000000000..31c59f006
--- /dev/null
+++ b/src/test/tptp/simple-sat.p
@@ -0,0 +1,2 @@
+fof(a1,axiom, p(a)).
+
diff --git a/src/test/tptp/socrates-theorem.p b/src/test/tptp/socrates-theorem.p
new file mode 100644
index 000000000..268b85aec
--- /dev/null
+++ b/src/test/tptp/socrates-theorem.p
@@ -0,0 +1,4 @@
+fof(a1,axiom, ! [X] : (human(X) => mortal(X))).
+fof(a2,axiom, human(socrates)).
+fof(c1,conjecture, mortal(socrates)).
+