Merge pull request #630 from vprover/tracer-output

Tracer Output
vprover · Dec 12, 2024 · 24f1ae3 · 24f1ae3
2 parents 5dbcc50 + 17cc956
commit 24f1ae3
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 5 deletions.
diff --git 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
@@ -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

diff --git 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;
 }
 
 /**