mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 23:25:36 +00:00
Code Activity

Use read_tptp API directly in tptp unit test

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/f07170c1-549a-464c-89f8-fee973f9790f

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-11 16:49:56 +00:00 • committed by GitHub
parent 61ed3ae6c8
commit 4350d8f29d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 14 additions and 63 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/test/CMakeLists.txt
View file

@ -146,6 +146,7 @@ add_executable(test-z3
theory_pb.cpp
timeout.cpp
tptp.cpp
../shell/tptp_frontend.cpp
total_order.cpp
totalizer.cpp
trigo.cpp
@ -167,11 +168,9 @@ z3_add_gparams_register_modules_rule(${z3_test_deps})
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)

74
src/test/tptp.cpp
View file

@ -1,77 +1,29 @@
#include <cstdio>
#include <sstream>
#include <string>
#include <vector>
#include <cctype>
#include <iostream>
#include <sstream>
#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
#include "shell/tptp_frontend.h"
struct tptp_case {
char const* file;
char const* expected_status;
};
constexpr unsigned command_output_buffer_size = 4096;
static bool is_safe_file_name(char const* s) {
if (!s || !*s)
return false;
if (s[0] == '-' || s[0] == '.')
return false;
if (std::string(s).find('/') != std::string::npos || std::string(s).find('\\') != std::string::npos)
return false;
if (std::string(s).find("..") != std::string::npos)
return false;
while (*s) {
unsigned char c = static_cast<unsigned char>(*s);
if (!(std::isalnum(c) || c == '.' || c == '-' || c == '_'))
return false;
++s;
}
return true;
}
static std::string run_tptp(char const* file) {
if (!is_safe_file_name(file)) {
std::cerr << "Unsafe TPTP test filename: " << file << "\n";
ENSURE(false);
}
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");
if (!pipe) {
std::cerr << "Failed to execute command: " << cmd.str() << "\n";
ENSURE(false);
}
std::string out;
char buffer[command_output_buffer_size];
while (fgets(buffer, sizeof(buffer), pipe))
out += buffer;
int code = Z3_PCLOSE(pipe);
#ifndef _WINDOWS
if (WIFEXITED(code))
code = WEXITSTATUS(code);
#endif
if (code != 0) {
std::cerr << "TPTP command failed for file '" << file << "' with exit code " << code << "\n";
std::cerr << out << "\n";
ENSURE(false);
}
return out;
std::string path = std::string(Z3_TEST_SRC_DIR) + "/tptp/" + file;
std::streambuf* old_out = std::cout.rdbuf();
std::ostringstream out;
std::cout.rdbuf(out.rdbuf());
unsigned code = read_tptp(path.c_str());
std::cout.rdbuf(old_out);
ENSURE(code == 0);
return out.str();
}
bool g_display_statistics = false;
bool g_display_model = false;
void tst_tptp() {
std::vector<tptp_case> cases = {
{"agatha-butler.p", "% SZS status Theorem"},