Merge branch 'master' into gmp

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)

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

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__

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) {

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,
@@ -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<std::string>();
   });
 

Kernel/TermIterators.hpp

@@ -36,32 +36,46 @@ 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<TermList>
 {
 public:
   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]);
     std::swap(_aux[1], other._aux[1]);
     if (_stack.size() >= 1 && _stack[0] == &other._aux[1]) {
-      // fix pointer pointing into this object
+      // see #hack 1
       ASS(_aux[0].isEmpty())
       _stack[0] = &_aux[1];
     }
   }
 
+  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<const Literal*>(term)->isTwoVarEquality()){
+      // see #hack 1
       _aux[0] = TermList::empty();
       _aux[1]=static_cast<const Literal*>(term)->twoVarEqSort();
       _stack.push(&_aux[1]);      
@@ -74,6 +88,7 @@ class VariableIterator
   VariableIterator(TermList t) : _stack(8), _used(false)
   {
     if(t.isVar()) {
+      // see #hack 1
       _aux[0] = TermList::empty();
       _aux[1]=t;
       _stack.push(&_aux[1]);
@@ -91,6 +106,7 @@ class VariableIterator
     _stack.reset();
     _used = false;
     if(term->isLiteral() && static_cast<const Literal*>(term)->isTwoVarEquality()){
+      // see #hack 1
       _aux[0] = TermList::empty();
       _aux[1]=static_cast<const Literal*>(term)->twoVarEqSort();
       _stack.push(&_aux[1]);      
@@ -105,6 +121,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]);
@@ -131,6 +148,7 @@ class VariableIterator
 private:
   Stack<const TermList*> _stack;
   bool _used;
+  // see #hack 1
   TermList _aux[2];
 };
 

Kernel/Theory.cpp

@@ -1385,9 +1385,7 @@ bool Theory::isInterpretedNumber(TermList t)
  * Return true iff @b pred is an interpreted predicate
  */
 bool Theory::isInterpretedPredicate(unsigned pred)
-{
-  return env.signature->getPredicate(pred)->interpreted();
-}
+{ return env.signature->getPredicate(pred)->interpreted(); }
 
 /**
  * Return true iff @b lit has an interpreted predicate
@@ -1413,9 +1411,9 @@ bool Theory::isInterpretedPredicate(Literal* lit)
 }
 
 
-bool Theory::isInterpretedPredicate(unsigned lit, Interpretation itp)
+bool Theory::isInterpretedPredicate(unsigned pred, Interpretation itp)
 {
-  return isInterpretedPredicate(lit) && interpretPredicate(lit)==itp;
+  return isInterpretedPredicate(pred) && interpretPredicate(pred) == itp;
 }
 
 /**

Kernel/Theory.hpp

@@ -568,7 +568,7 @@ class Theory
       other interpreted predicate.
    */
   bool isInterpretedPredicate(unsigned pred);
-
+    
   bool isInterpretedEquality(Literal* lit);
   bool isInterpretedPredicate(Literal* lit, Interpretation itp);
   bool isInterpretedPredicate(unsigned pred, Interpretation itp);

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<unsigned> const& perm) {
+  return anyPerm(vl.size(), [&](auto const& perm) {
     AcRectComp c {vl, vr, perm};
     return eqModAC_(lhs, rhs, c);
   });