Merge branch 'master' into kbo-move-semantics

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

FMB/FiniteModelBuilder.cpp

@@ -168,7 +168,7 @@ bool FiniteModelBuilder::reset(){
     cout << "offset for " << f << " is " << offsets << " (arity is " << env.signature->functionArity(f) << ") " << endl;
 #endif
 
-    DArray<unsigned> f_signature = _sortedSignature->functionSignatures[f];
+    auto const& f_signature = _sortedSignature->functionSignatures[f];
     ASS(f_signature.size() == env.signature->functionArity(f)+1);
 
     unsigned add = _sortModelSizes[f_signature[0]];
@@ -195,7 +195,7 @@ bool FiniteModelBuilder::reset(){
 
 #endif
 
-    DArray<unsigned> p_signature = _sortedSignature->predicateSignatures[p];
+    auto const& p_signature = _sortedSignature->predicateSignatures[p];
     ASS(p_signature.size()==env.signature->predicateArity(p));
     unsigned add=1;
     for(unsigned i=0;i<p_signature.size();i++){
@@ -1912,7 +1912,8 @@ void FiniteModelBuilder::onModelFound()
     vampireSortSizes[vSort] = size;
   }
 
-  FiniteModelMultiSorted model(vampireSortSizes);
+  // TODO can we get rid of this clone() and pass a reference instead(?)
+  FiniteModelMultiSorted model(vampireSortSizes.clone());
 
   //Record interpretation of constants and functions
   for(unsigned f=0;f<env.signature->functions();f++){

FMB/FiniteModelMultiSorted.cpp

@@ -532,15 +532,11 @@ void FiniteModelMultiSorted::eliminateSortFunctionsAndPredicates(const Stack<uns
     // we will need to reencode everything
 
     // save the old stuff
-    DArray<unsigned> old_f_offsets;
-    _f_offsets.swap(old_f_offsets);
-    DArray<unsigned> old_f_interpretation;
-    _f_interpretation.swap(old_f_interpretation);
-    DArray<unsigned> old_p_offsets;
-    _p_offsets.swap(old_p_offsets);
-    DArray<char> old_p_interpretation;
-    _p_interpretation.swap(old_p_interpretation);
-    DArray<unsigned> old_sizes = _sizes; // this is a copy, not a swap
+    auto old_f_offsets        = std::move(_f_offsets);
+    auto old_f_interpretation = std::move(_f_interpretation);
+    auto old_p_offsets        = std::move(_p_offsets);
+    auto old_p_interpretation = std::move(_p_interpretation);
+    auto old_sizes = _sizes.clone();
 
     // update size of the affected sort
     _sizes[srt] = newSize;
@@ -683,15 +679,11 @@ void FiniteModelMultiSorted::eliminateSortFunctionsAndPredicates(const Stack<uns
     // we will need to reencode everything
 
     // save the old stuff
-    DArray<unsigned> old_f_offsets;
-    _f_offsets.swap(old_f_offsets);
-    DArray<unsigned> old_f_interpretation;
-    _f_interpretation.swap(old_f_interpretation);
-    DArray<unsigned> old_p_offsets;
-    _p_offsets.swap(old_p_offsets);
-    DArray<char> old_p_interpretation;
-    _p_interpretation.swap(old_p_interpretation);
-    DArray<unsigned> old_sizes = _sizes; // this is a copy, not a swap
+    auto old_f_offsets        = std::move(_f_offsets);
+    auto old_f_interpretation = std::move(_f_interpretation);
+    auto old_p_offsets        = std::move(_p_offsets);
+    auto old_p_interpretation = std::move(_p_interpretation);
+    auto old_sizes = _sizes.clone();
 
     // update size of the affected sort
     _sizes[srt] = newSize;

FMB/ModelCheck.hpp

@@ -108,7 +108,8 @@ static void doCheck(UnitList* units)
       sortSizesArray[sort] = curModelSize;
     }
   }
-  FiniteModelMultiSorted model(sortSizesArray);
+  // TODO can we pass a reference here instead of clone()ing?
+  FiniteModelMultiSorted model(sortSizesArray.clone());
 
   Set<Term*> domainConstants; // union of all the perSort ones
   DHMap<Term*,unsigned> domainConstantNumber;

Kernel/KBO.cpp

@@ -553,7 +553,7 @@ KboWeightMap<SigTraits> KBO::weightsFromFile(const Options& opts) const
   }
 
   return KboWeightMap<SigTraits> {
-    ._weights                = weights,
+    ._weights                = weights.clone(),
     ._introducedSymbolWeight = introducedWeight,
     ._specialWeights         = specialWeights,
   };
@@ -975,7 +975,7 @@ KboWeightMap<SigTraits> KboWeightMap<SigTraits>::fromSomeUnsigned(Extractor ex,
   }
 
   return KboWeightMap {
-    ._weights                = weights,
+    ._weights                = weights.clone(),
     ._introducedSymbolWeight = 1,
     ._specialWeights         = KboSpecialWeights<SigTraits>::dflt(),
   };
@@ -1008,7 +1008,7 @@ KboWeightMap<FuncSigTraits> KboWeightMap<FuncSigTraits>::randomized(unsigned max
   }
 
   return KboWeightMap {
-    ._weights                = weights,
+    ._weights                = weights.clone(),
     ._introducedSymbolWeight = introducedWeight,
     ._specialWeights         = KboSpecialWeights<FuncSigTraits> {
       ._variableWeight = variableWeight,

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

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

Lib/DArray.hpp

@@ -61,7 +61,7 @@ class DArray
     }
   }
 
-  DArray(const DArray& o)
+  explicit DArray(const DArray& o)
     : _size(o.size()), _capacity(o.size())
   {
     if(_size==0) {
@@ -75,6 +75,8 @@ class DArray
     }
   }
 
+  DArray clone() const { return DArray(*this); }
+
   void swap(DArray& other) {
     std::swap(other._size, _size);
     std::swap(other._capacity, _capacity);

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);
   });

UnitTests/tKBO.hpp

@@ -22,7 +22,7 @@ inline KboWeightMap<SigTraits> toWeightMap(unsigned introducedSymbolWeight, KboS
     out[i] = w == NULL ? df.symbolWeight(i) : *w;
   }
   return  {
-    ._weights = out,
+    ._weights = out.clone(),
     ._introducedSymbolWeight = introducedSymbolWeight,
     ._specialWeights         = ws,
   };