mirror of
https://github.com/Z3Prover/z3
synced 2026-05-16 23:25:36 +00:00
21b3f72b36
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/dc1d46fc-4b6c-4f64-91a0-9fb57c73c166 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
54 lines
1.4 KiB
C++
54 lines
1.4 KiB
C++
#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;
|
|
};
|
|
|
|
constexpr unsigned tptp_buf_sz = 4096;
|
|
|
|
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[tptp_buf_sz];
|
|
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 Theorem"},
|
|
{"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);
|
|
}
|
|
}
|