mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-02 12:13:25 +00:00
Code Activity

Replace TPTP frontend env vars with tptp config module

Browse source 
Replace the TPTP and Z3_TPTP_DUMP_SMT2 environment variables in
tptp_frontend.cpp with a new 'tptp' configuration module (src/params/tptp.pyg)
exposing tptp.root and tptp.dump_smt2 parameters.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
This commit is contained in:
Nikolaj Bjorner 2026-07-31 10:49:00 -07:00
parent 683cb4ec03
commit 33663c4d51
3 changed files with 17 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/cmd_context/tptp_frontend.cpp
View file

@ -23,6 +23,7 @@
#include "solver/solver.h"
#include "cmd_context/cmd_context.h"
#include "cmd_context/tptp_frontend.h"
#include "params/tptp.hpp"
@ -2375,13 +2376,13 @@ class tptp_parser {
// Try relative to current file's directory
std::string local = normalize_path(dirname(curr_file) + "/" + name);
if (file_exists(local)) return local;
// Try TPTP environment variable (standard TPTP convention): includes such as
// Try the tptp.root parameter (standard TPTP convention): includes such as
// "Axioms/MAT001^0.ax" are resolved relative to the TPTP root directory named
// by $TPTP. This is required when a problem is run from a directory that does
// not contain the Axioms/ tree (e.g. an isolated benchmark harness workspace).
char const* root = std::getenv("TPTP");
if (root) {
std::string env = normalize_path(std::string(root) + "/" + name);
// by the parameter. This is required when a problem is run from a directory that
// does not contain the Axioms/ tree (e.g. an isolated benchmark harness workspace).
std::string root = tptp().root().str();
if (!root.empty()) {
std::string env = normalize_path(root + "/" + name);
if (file_exists(env)) return env;
}
// Walk up ancestor directories of the current file. TPTP include paths are
@ -2947,9 +2948,10 @@ static unsigned read_tptp_stream(std::istream& in, char const* current_file) {
solver_params.set_bool("pi.avoid_skolems", false);
ctx.get_solver()->updt_params(solver_params);
// Optional: dump the parsed goal as an SMT-LIB2 benchmark (env Z3_TPTP_DUMP_SMT2
// Optional: dump the parsed goal as an SMT-LIB2 benchmark (parameter tptp.dump_smt2
// gives the output file path). Used to produce SMTLIB versions of TPTP instances.
if (char const* dump_path = getenv("Z3_TPTP_DUMP_SMT2")) {
std::string dump_path = tptp().dump_smt2().str();
if (!dump_path.empty()) {
std::ofstream dout(dump_path);
if (dout) {
dout << "; Auto-generated from TPTP input: "

1
src/params/CMakeLists.txt
View file

@ -30,6 +30,7 @@ z3_add_component(params
smt_params_helper.pyg
solver_params.pyg
tactic_params.pyg
tptp.pyg
EXTRA_REGISTER_MODULE_HEADERS
context_params.h
)

6
src/params/tptp.pyg Normal file
View file

@ -0,0 +1,6 @@
def_module_params('tptp',
description='TPTP frontend parameters',
class_name='tptp',
export=True,
params=(('root', SYMBOL, '', 'root directory for resolving TPTP include() axiom paths (replaces the TPTP environment variable)'),
('dump_smt2', SYMBOL, '', 'if non-empty, file path to dump the parsed TPTP goal as an SMT-LIB2 benchmark (replaces the Z3_TPTP_DUMP_SMT2 environment variable)')))