From 33663c4d51f7934d0d5e89eb087fdd23b1fdbea3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Jul 2026 10:49:00 -0700 Subject: [PATCH] Replace TPTP frontend env vars with tptp config module 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 --- src/cmd_context/tptp_frontend.cpp | 18 ++++++++++-------- src/params/CMakeLists.txt | 1 + src/params/tptp.pyg | 6 ++++++ 3 files changed, 17 insertions(+), 8 deletions(-) create mode 100644 src/params/tptp.pyg diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index 0149de1128..c8dbf561fd 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -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: " diff --git a/src/params/CMakeLists.txt b/src/params/CMakeLists.txt index 9aea5b9187..05fad60866 100644 --- a/src/params/CMakeLists.txt +++ b/src/params/CMakeLists.txt @@ -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 ) diff --git a/src/params/tptp.pyg b/src/params/tptp.pyg new file mode 100644 index 0000000000..dfb510b153 --- /dev/null +++ b/src/params/tptp.pyg @@ -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)')))