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

@@ -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)
 

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) \

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);
+    }
+}

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)).
+

src/test/tptp/simple-sat.p

@@ -0,0 +1,2 @@
+fof(a1,axiom, p(a)).
+

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)).
+