From 17234d14972ca476f9f490a20354c2feebf5ccf1 Mon Sep 17 00:00:00 2001 From: joe-hauns Date: Tue, 10 Dec 2024 15:40:15 +0100 Subject: [PATCH 1/9] 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 struct _printDbg{ template 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 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 Date: Tue, 10 Dec 2024 21:17:14 +0100 Subject: [PATCH 2/9] 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; } /** From 1625f16da507ad206fb94eb4185b94228b9a89cf Mon Sep 17 00:00:00 2001 From: joe-hauns Date: Thu, 12 Dec 2024 11:13:36 +0100 Subject: [PATCH 3/9] tidy --- Kernel/NumTraits.hpp | 5 ----- 1 file changed, 5 deletions(-) diff --git a/Kernel/NumTraits.hpp b/Kernel/NumTraits.hpp index d73e2c90f..ef1d6d6eb 100644 --- a/Kernel/NumTraits.hpp +++ b/Kernel/NumTraits.hpp @@ -293,11 +293,6 @@ struct NumTraits; static const char* name() {return #CamelCase;} \ }; \ -#define __INSTANTIATE_NUM_TRAITS_ALL \ - __INSTANTIATE_NUM_TRAITS(Rational) \ - __INSTANTIATE_NUM_TRAITS(Real ) \ - __INSTANTIATE_NUM_TRAITS(Integer ) \ - #define __NUM_TRAITS_IF_FRAC(sort, ...) __NUM_TRAITS_IF_FRAC_ ## sort (__VA_ARGS__) #define __NUM_TRAITS_IF_FRAC_INT(...) #define __NUM_TRAITS_IF_FRAC_REAL(...) __VA_ARGS__ From f0dad5e96b03b699c56e47dfd4bfeb763e055b3a Mon Sep 17 00:00:00 2001 From: joe-hauns Date: Thu, 12 Dec 2024 11:16:08 +0100 Subject: [PATCH 4/9] fixed output formatting --- Kernel/OperatorType.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Kernel/OperatorType.cpp b/Kernel/OperatorType.cpp index 6125fe26b..b573903a7 100644 --- a/Kernel/OperatorType.cpp +++ b/Kernel/OperatorType.cpp @@ -137,7 +137,7 @@ std::string OperatorType::argsToString() const { unsigned ar = arity(); ASS(ar); - std::string res = ar != 1 ? "(" : ""; + std::string res = ar > 1 ? "(" : ""; for (unsigned i = _typeArgsArity; i < ar; i++) { res += arg(i).toString(); if (i != ar-1) { From 1ed353a86d4c41769d5732166842868096a6de33 Mon Sep 17 00:00:00 2001 From: joe-hauns Date: Thu, 12 Dec 2024 11:18:05 +0100 Subject: [PATCH 5/9] clarifying comment --- Kernel/Term.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/Kernel/Term.cpp b/Kernel/Term.cpp index cc2ca1c04..948091be6 100644 --- a/Kernel/Term.cpp +++ b/Kernel/Term.cpp @@ -727,6 +727,7 @@ std::string Term::toString(bool topLevel) const return uminus(); } } + /* this means we have an uninterpteted term which will be formatted as usual */ return Option(); }); From 37fae7d3202ed298d91338564d0ecc0fb2c6a312 Mon Sep 17 00:00:00 2001 From: joe-hauns Date: Thu, 12 Dec 2024 11:30:58 +0100 Subject: [PATCH 6/9] fixed move assignment for VariableIterator --- Kernel/Term.cpp | 2 +- Kernel/TermIterators.hpp | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Kernel/Term.cpp b/Kernel/Term.cpp index 948091be6..b9fd07bed 100644 --- a/Kernel/Term.cpp +++ b/Kernel/Term.cpp @@ -121,7 +121,7 @@ bool TermList::isSafe() const } bool TermList::ground() const -{ return !isVar() && term()->ground(); } +{ return isTerm() && term()->ground(); } /** * Return true if @b ss and @b tt have the same top symbols, that is, diff --git a/Kernel/TermIterators.hpp b/Kernel/TermIterators.hpp index 0c664ef30..ec6e6a78a 100644 --- a/Kernel/TermIterators.hpp +++ b/Kernel/TermIterators.hpp @@ -44,10 +44,7 @@ class VariableIterator DECL_ELEMENT_TYPE(TermList); VariableIterator() : _stack(8), _used(false) {} - VariableIterator& operator=(VariableIterator&&) = default; - VariableIterator(VariableIterator&& other) - : VariableIterator() - { + void swap(VariableIterator& other) { std::swap(_stack, other._stack); std::swap(_used, other._used); std::swap(_aux[0], other._aux[0]); @@ -59,6 +56,9 @@ class VariableIterator } } + VariableIterator& operator=(VariableIterator&& other) { swap(other); return *this; } + VariableIterator(VariableIterator&& other) : VariableIterator() { swap(other); } + VariableIterator(const Term* term) : _stack(8), _used(false) { if(term->isLiteral() && static_cast(term)->isTwoVarEquality()){ From 30ac5129bb2e4825cfd9b4c3ccf0da6608bd7b3e Mon Sep 17 00:00:00 2001 From: joe-hauns Date: Thu, 12 Dec 2024 11:36:10 +0100 Subject: [PATCH 7/9] clarifying comments --- Kernel/TermIterators.hpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Kernel/TermIterators.hpp b/Kernel/TermIterators.hpp index ec6e6a78a..636e41405 100644 --- a/Kernel/TermIterators.hpp +++ b/Kernel/TermIterators.hpp @@ -50,7 +50,8 @@ class VariableIterator std::swap(_aux[0], other._aux[0]); std::swap(_aux[1], other._aux[1]); if (_stack.size() >= 1 && _stack[0] == &other._aux[1]) { - // fix pointer pointing into this object + // other->_stack[0] might contain a reference to other->_aux[1] (an efficiency hack you can see being used in the constructors) + // So in order to perform proper move semantics and not tun into use after free issues, we need to make the pointer point into this->_aux[1] ASS(_aux[0].isEmpty()) _stack[0] = &_aux[1]; } @@ -62,6 +63,7 @@ class VariableIterator VariableIterator(const Term* term) : _stack(8), _used(false) { if(term->isLiteral() && static_cast(term)->isTwoVarEquality()){ + /* a hack to make iteration faster (?) */ _aux[0] = TermList::empty(); _aux[1]=static_cast(term)->twoVarEqSort(); _stack.push(&_aux[1]); @@ -74,6 +76,7 @@ class VariableIterator VariableIterator(TermList t) : _stack(8), _used(false) { if(t.isVar()) { + /* a hack to make iteration faster (?) */ _aux[0] = TermList::empty(); _aux[1]=t; _stack.push(&_aux[1]); @@ -105,6 +108,7 @@ class VariableIterator _stack.reset(); _used = false; if(t.isVar()) { + /* a hack to make iteration faster (?) */ _aux[0] = TermList::empty(); _aux[1]=t; _stack.push(&_aux[1]); From 19e03e303a404abacd87c3d5d03ea3529357babc Mon Sep 17 00:00:00 2001 From: joe-hauns Date: Thu, 12 Dec 2024 11:47:01 +0100 Subject: [PATCH 8/9] comment --- Kernel/TermIterators.hpp | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/Kernel/TermIterators.hpp b/Kernel/TermIterators.hpp index 636e41405..37f23dd97 100644 --- a/Kernel/TermIterators.hpp +++ b/Kernel/TermIterators.hpp @@ -36,7 +36,20 @@ namespace Kernel { * - This iterator returns sort variables * - If the sort of the returned variables is required, please * use VariableIterator2 below, having read its documentation. - */ + * + * #hack 1: + * A comment on the implementation and the member _aux: + * iteration is done dfs using a _stack of TermList* which can all be iterated using TermList::next. + * This is all fine and easy as long as we want to iterate the arguments of some Term* or Literal*. + * But if we want to iterate some `TermList` that is not an argument of a Term* we need to somehow make + * it still conform with the invariants expected by `TermList::next` (i.e. it being a pointer with + * an adress where all the adresses before being TermList s as well and the list of TermLists before + * the current adress is terminated by an empty TermList). + * In order to achieve this the stack _aux is used, which is populated with whatever thing we want to + * iterate that is not an argument to a Term*, and then a pointer to that thing is passed pushed onto + * the _stack. This means though that stack might contain pointers to TermList s that do not live on + * heap but within this object. Thus we need to account for this in our move constructors. + */ class VariableIterator : public IteratorCore { @@ -50,8 +63,7 @@ class VariableIterator std::swap(_aux[0], other._aux[0]); std::swap(_aux[1], other._aux[1]); if (_stack.size() >= 1 && _stack[0] == &other._aux[1]) { - // other->_stack[0] might contain a reference to other->_aux[1] (an efficiency hack you can see being used in the constructors) - // So in order to perform proper move semantics and not tun into use after free issues, we need to make the pointer point into this->_aux[1] + // see #hack 1 ASS(_aux[0].isEmpty()) _stack[0] = &_aux[1]; } @@ -63,7 +75,7 @@ class VariableIterator VariableIterator(const Term* term) : _stack(8), _used(false) { if(term->isLiteral() && static_cast(term)->isTwoVarEquality()){ - /* a hack to make iteration faster (?) */ + // see #hack 1 _aux[0] = TermList::empty(); _aux[1]=static_cast(term)->twoVarEqSort(); _stack.push(&_aux[1]); @@ -76,7 +88,7 @@ class VariableIterator VariableIterator(TermList t) : _stack(8), _used(false) { if(t.isVar()) { - /* a hack to make iteration faster (?) */ + // see #hack 1 _aux[0] = TermList::empty(); _aux[1]=t; _stack.push(&_aux[1]); @@ -94,6 +106,7 @@ class VariableIterator _stack.reset(); _used = false; if(term->isLiteral() && static_cast(term)->isTwoVarEquality()){ + // see #hack 1 _aux[0] = TermList::empty(); _aux[1]=static_cast(term)->twoVarEqSort(); _stack.push(&_aux[1]); @@ -135,6 +148,7 @@ class VariableIterator private: Stack _stack; bool _used; + // see #hack 1 TermList _aux[2]; }; From fa64d607596f417bf5ae2c5192f80e06b991999b Mon Sep 17 00:00:00 2001 From: joe-hauns Date: Thu, 12 Dec 2024 12:45:25 +0100 Subject: [PATCH 9/9] fix after merge --- Test/TestUtils.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/TestUtils.cpp b/Test/TestUtils.cpp index 123ad4ed3..320ed9515 100644 --- a/Test/TestUtils.cpp +++ b/Test/TestUtils.cpp @@ -278,7 +278,7 @@ bool TestUtils::eqModACRect(Kernel::TermList lhs, Kernel::TermList rhs) if (vl.size() != vr.size()) return false; - return anyPerm(vl.size(), [&](DArray perm) { + return anyPerm(vl.size(), [&](auto& perm) { AcRectComp c {vl, vr, perm}; return eqModAC_(lhs, rhs, c); });