From 17234d14972ca476f9f490a20354c2feebf5ccf1 Mon Sep 17 00:00:00 2001
From: joe-hauns <joe-hauns@protonmail.com>
Date: Tue, 10 Dec 2024 15:40:15 +0100
Subject: [PATCH 1/2] using relative file names in Debug/Tracer

---
 CMakeLists.txt   |  3 +++
 Debug/Tracer.hpp | 15 ++++++++++++---
 2 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 854c31f5b..41b52f175 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -14,6 +14,9 @@ set(CMAKE_CXX_STANDARD 17)
 set(CMAKE_CXX_STANDARD_REQUIRED ON)
 set(CMAKE_CXX_EXTENSIONS OFF)
 
+# make __FILENAME__ macro as relative path used instead of absoulte source path __FILE__
+set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D__FILENAME__='\"$(subst ${CMAKE_SOURCE_DIR}/,,$(abspath $<))\"'")
+
 # configure compilers
 if(CMAKE_CXX_COMPILER_ID STREQUAL GNU OR CMAKE_CXX_COMPILER_ID MATCHES Clang$)
   add_compile_options(-Wall)
diff --git a/Debug/Tracer.hpp b/Debug/Tracer.hpp
index d83291a9c..6c5373640 100644
--- a/Debug/Tracer.hpp
+++ b/Debug/Tracer.hpp
@@ -49,12 +49,12 @@ template<class A, class... As> struct _printDbg<A, As...>{
 
 template<class... A> void printDbg(const char* file, int line, const A&... msg)
 {
-  int width = 60;
+  unsigned width = 60;
   std::cout << "[ debug ] ";
   for (const char* c = file; *c != 0 && width > 0; c++, width--) {
     std::cout << *c;
   }
-  for (int i = 0; i < width; i++) {
+  for (unsigned i = 0; i < width; i++) {
     std::cout << ' ';
   }
   std::cout <<  "@" << std::setw(5) << line << ":";
@@ -65,9 +65,18 @@ template<class... A> void printDbg(const char* file, int line, const A&... msg)
 } // namespace Debug
 
 #if VDEBUG
-#  define DBG(...) { Debug::printDbg(__FILE__, __LINE__, __VA_ARGS__); }
+
+#ifdef ABSOLUTE_SOURCE_DIR
+#define __REL_FILE__  (&__FILE__[sizeof(ABSOLUTE_SOURCE_DIR) / sizeof(ABSOLUTE_SOURCE_DIR[0])])
+#else
+#define __REL_FILE__  __FILE__
+#endif
+
+#  define DBG(...) { Debug::printDbg(__REL_FILE__, __LINE__, __VA_ARGS__); }
+#  define WARN(...) { DBG("WARNING: ", __VA_ARGS__); }
 #  define DBGE(x) DBG(#x, " = ", x)
 #else // ! VDEBUG
+#  define WARN(...) {}
 #  define DBG(...) {}
 #  define DBGE(x) {}
 #endif

From 36d99187496318bcef479acee3d9e05801ff5b09 Mon Sep 17 00:00:00 2001
From: Martin Suda <martin.suda@cvut.cz>
Date: Tue, 10 Dec 2024 21:17:14 +0100
Subject: [PATCH 2/2] stick with the name from the header

---
 Kernel/Theory.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Kernel/Theory.cpp b/Kernel/Theory.cpp
index 5d416cb31..6375d677a 100644
--- a/Kernel/Theory.cpp
+++ b/Kernel/Theory.cpp
@@ -1625,9 +1625,9 @@ bool Theory::isInterpretedFunction(Term* t)
   return isInterpretedFunction(t->functor());
 }
 
-bool Theory::isInterpretedPredicate(unsigned lit, Interpretation itp)
+bool Theory::isInterpretedPredicate(unsigned f, Interpretation itp)
 {
-  return isInterpretedPredicate(lit) && interpretPredicate(lit)==itp;
+  return isInterpretedPredicate(f) && interpretPredicate(f)==itp;
 }
 
 /**