From 5531eb1e728fa0309e9e04e5b129598848771b16 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 29 Jun 2026 10:30:08 -0700 Subject: [PATCH] fix path --- src/cmd_context/tptp_frontend.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index c2b2c4fc3f..6c8258ad75 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -1792,6 +1792,18 @@ class tptp_parser { std::string env = normalize_path(std::string(root) + "/" + name); if (file_exists(env)) return env; } + // Walk up ancestor directories of the current file. TPTP include paths are + // relative to the TPTP root directory (e.g. "Axioms/BOO001-0.ax"), while the + // problem file typically lives in a subdirectory such as "Problems/BOO/". + std::string dir = dirname(curr_file); + for (;;) { + size_t idx = dir.find_last_of("/\\"); + if (idx == std::string::npos) break; + dir = dir.substr(0, idx); + if (dir.empty()) break; + std::string candidate = normalize_path(dir + "/" + name); + if (file_exists(candidate)) return candidate; + } // Try relative to current working directory (common when running from TPTP root) std::string cwd_relative = normalize_path(name); if (file_exists(cwd_relative)) return cwd_relative;