A selected subset of improvements from #1008

Kernel/BottomUpEvaluation.hpp

@@ -327,51 +327,51 @@ class BottomUpEvaluation {
   Result apply(Arg const& toEval) 
   {
     /* recursion state. Contains a stack of items that are being recursed on. */
-    Recycled<Stack<BottomUpChildIter<Arg>>> recState;
-    Recycled<Stack<Result>> recResults;
+    Scratch<std::tuple<Stack<BottomUpChildIter<Arg>>, Stack<Result>>> stacks;
+    auto& [recState, recResults] = *stacks;
 
-    recState->push(BottomUpChildIter<Arg>(toEval, _context));
+    recState.push(BottomUpChildIter<Arg>(toEval, _context));
 
-    while (!recState->isEmpty()) {
-      if (recState->top().hasNext(_context)) {
-        Arg t = recState->top().next(_context);
+    while (!recState.isEmpty()) {
+      if (recState.top().hasNext(_context)) {
+        Arg t = recState.top().next(_context);
 
         Option<Result> nonRec = _evNonRec(t);
         if (nonRec) {
-          recResults->push(move_if_value<Result>(*nonRec));
+          recResults.push(move_if_value<Result>(*nonRec));
 
         } else {
           Option<Result> cached = _memo.get(t);
           if (cached.isSome()) {
-            recResults->push(std::move(cached).unwrap());
+            recResults.push(std::move(cached).unwrap());
           } else {
-            recState->push(BottomUpChildIter<Arg>(t, _context));
+            recState.push(BottomUpChildIter<Arg>(t, _context));
           }
 
         }
 
       } else {
 
-        BottomUpChildIter<Arg> orig = recState->pop();
+        BottomUpChildIter<Arg> orig = recState.pop();
 
         ASS_GE(recResults.size(), orig.nChildren(_context))
         Result* argLst = orig.nChildren(_context) == 0 
           ? nullptr 
-          : static_cast<Result*>(&((*recResults)[recResults->size() - orig.nChildren(_context)]));
+          : static_cast<Result*>(&(recResults[recResults.size() - orig.nChildren(_context)]));
 
         Result eval = _memo.getOrInit(orig.self(), 
                         [&](){ return _function(orig.self(), argLst); });
 
         DEBUG_BOTTOM_UP(0, "evaluated: ", orig.self(), " -> ", eval);
-        recResults->pop(orig.nChildren(_context));
-        recResults->push(std::move(eval));
+        recResults.pop(orig.nChildren(_context));
+        recResults.push(std::move(eval));
       }
     }
-    ASS(recState->isEmpty())
+    ASS(recState.isEmpty())
 
 
-    ASS(recResults->size() == 1);
-    auto result = recResults->pop();
+    ASS(recResults.size() == 1);
+    auto result = recResults.pop();
     DEBUG_BOTTOM_UP(0, "eval result: ", toEval, " -> ", result);
     return result;
   }

Kernel/ClauseQueue.cpp

@@ -33,6 +33,18 @@ ClauseQueue::ClauseQueue()
   _left->nodes()[0] = 0;
 }
 
+/**
+ * Clauses with equal keys go first by input type (a larger one first),
+ * then by number.
+ */
+bool ClauseQueue::tieLessThan(Clause* c1, Clause* c2)
+{
+  if (c1->inputType() != c2->inputType()) {
+    return c2->inputType() < c1->inputType();
+  }
+  return c1->number() < c2->number();
+}
+
 /** Temporary!!! */
 ClauseQueue::~ClauseQueue ()
 {
@@ -62,6 +74,8 @@ void ClauseQueue::insert(Clause* c)
   void* mem = ALLOC_KNOWN(Node::bytesRequiredFor(h + 1), "ClauseQueue::Node");
   Node* newNode = reinterpret_cast<Node*>(mem);
   newNode->clause = c;
+  uint64_t k = key(c);
+  newNode->key = k;
 
   // left is a node with a value smaller than that of newNode and having
   // a large enough height.
@@ -71,7 +85,7 @@ void ClauseQueue::insert(Clause* c)
   unsigned lh = _height;
   for (;;) {
     Node* next = left->nodes()[lh];
-    if (next == 0 || lessThan(c,next->clause)) {
+    if (next == 0 || lessThan(k,c,next)) {
       if (lh <= h) {
 	left->nodes()[lh] = newNode;
 	newNode->nodes()[lh] = next;
@@ -94,6 +108,7 @@ bool ClauseQueue::remove(Clause* c)
 {
   unsigned h = _height;
   Node* left = _left;
+  uint64_t k = key(c);
 
   for (;;) {
     Node* next = left->nodes()[h];
@@ -118,7 +133,7 @@ bool ClauseQueue::remove(Clause* c)
       return true;
     }
 
-    if (next == 0 || lessThan(c,next->clause)) {
+    if (next == 0 || lessThan(k,c,next)) {
       if(h==0) {
 
 #if VDEBUG

Kernel/ClauseQueue.hpp

@@ -17,6 +17,8 @@
 #ifndef __ClauseQueue__
 #define __ClauseQueue__
 
+#include <cstdint>
+
 #if VDEBUG
 #include <ostream>
 #endif
@@ -51,11 +53,14 @@ class ClauseQueue
 
   friend class Iterator;
 protected:
-  /** comparison of clauses */
-  virtual bool lessThan(Clause*,Clause*) = 0;
+  /** primary sort key of a clause, ties are broken by tieLessThan() */
+  virtual uint64_t key(Clause*) = 0;
+  static bool tieLessThan(Clause* c1, Clause* c2);
   /** Nodes in the skip list */
   class Node : public Lib::FlexibleTail<Node, Node *> {
   public:
+    /** key() of the clause */
+    uint64_t key;
     /** Clause at this node */
     Clause* clause;
     /** Links to other nodes on the right, can be of any length */
@@ -66,6 +71,9 @@ class ClauseQueue
   unsigned _height;
   /** the leftmost node with the dummy key and value */
   Node* _left;
+  /** true if the clause with key @b k goes before @b node */
+  static bool lessThan(uint64_t k, Clause* c, const Node* node)
+  { return k < node->key || (k == node->key && tieLessThan(c, node->clause)); }
 
 public:
   /** Iterator over the queue

Kernel/EqHelper.cpp

@@ -109,6 +109,9 @@ Term* EqHelper::replace(Term* trm0, TermList tSrc, TermList tDest)
   modified.push(false);
   toDo.push(trm0->args());
 
+  // subterms no heavier than tSrc (or ground ones, if tSrc is a variable) cannot contain it
+  unsigned srcWeight = tSrc.isVar() ? 1 : tSrc.term()->weight();
+
   for (;;) {
     TermList* tt=toDo.pop();
     if (tt->isEmpty()) {
@@ -148,6 +151,10 @@ Term* EqHelper::replace(Term* trm0, TermList tSrc, TermList tDest)
     }
     ASS(tl.isTerm());
     Term* t=tl.term();
+    if (t->weight() <= srcWeight || (tSrc.isVar() && t->ground())) {
+      args.push(tl);
+      continue;
+    }
     terms.push(t);
     modified.push(false);
     toDo.push(t->args());

Kernel/SubstHelper.hpp

@@ -345,33 +345,31 @@ Term* SubstHelper::applyImpl(Term* trm, Applicator& applicator, bool noSharing)
     ASSERTION_VIOLATION;
   }
 
-  Recycled<Stack<TermList*>> toDo;
-  Recycled<Stack<Term*>> terms;
-  Recycled<Stack<bool>> modified;
-  Recycled<Stack<TermList>> args;
+  Scratch<std::tuple<Stack<TermList*>, Stack<Term*>, Stack<bool>, Stack<TermList>>> stacks;
+  auto& [toDo, terms, modified, args] = *stacks;
 
-  modified->push(false);
-  toDo->push(trm->args());
+  modified.push(false);
+  toDo.push(trm->args());
 
   for(;;) {
-    TermList* tt=toDo->pop();
+    TermList* tt=toDo.pop();
     if(tt->isEmpty()) {
-      if(terms->isEmpty()) {
+      if(terms.isEmpty()) {
         //we're done, args stack contains modified arguments
         //of the topleve term/literal.
-        ASS(toDo->isEmpty());
+        ASS(toDo.isEmpty());
         break;
       }
-      Term* orig=terms->pop();
-      if(!modified->pop()) {
-        args->truncate(args->length() - orig->arity());
-        args->push(TermList(orig));
+      Term* orig=terms.pop();
+      if(!modified.pop()) {
+        args.truncate(args.length() - orig->arity());
+        args.push(TermList(orig));
         continue;
       }
       //here we assume, that stack is an array with
       //second topmost element as &top()-1, third at
       //&top()-2, etc...
-      TermList* argLst=&args->top() - (orig->arity()-1);
+      TermList* argLst=&args.top() - (orig->arity()-1);
 
       bool shouldShare=!noSharing && canBeShared(argLst, orig->arity());
 
@@ -386,61 +384,61 @@ Term* SubstHelper::applyImpl(Term* trm, Applicator& applicator, bool noSharing)
       else {
         newTrm=Term::createNonShared(orig,argLst);
       }
-      args->truncate(args->length() - orig->arity());
-      args->push(TermList(newTrm));
+      args.truncate(args.length() - orig->arity());
+      args.push(TermList(newTrm));
 
-      modified->setTop(true);
+      modified.setTop(true);
       continue;
     }
-    toDo->push(tt->next());
+    toDo.push(tt->next());
 
     TermList tl=*tt;
     if(tl.isOrdinaryVar()) {
       TermList tDest=applicator.apply(tl.var());
-      args->push(tDest);
+      args.push(tDest);
       if(tDest!=tl) {
-        modified->setTop(true);
+        modified.setTop(true);
       }
       continue;
     }
     if(tl.isSpecialVar()) {
       TermList tDest=SpecVarHandler<ProcessSpecVars>::apply(applicator,tl.var());
-      args->push(tDest);
+      args.push(tDest);
       if(tDest!=tl) {
-        modified->setTop(true);
+        modified.setTop(true);
       }
       continue;
     }
     ASS(tl.isTerm());
     if(tl.isVar() || (tl.term()->shared() && tl.term()->ground())) {
-      args->push(tl);
+      args.push(tl);
       continue;
     }
     Term* t = tl.term();
     if(t->isSpecial()) {
       //we handle specal terms at the top level of this function
-      args->push(TermList(applyImpl<ProcessSpecVars>(t, applicator, noSharing)));
+      args.push(TermList(applyImpl<ProcessSpecVars>(t, applicator, noSharing)));
       continue;
     }
-    terms->push(t);
-    modified->push(false);
-    toDo->push(t->args());
+    terms.push(t);
+    modified.push(false);
+    toDo.push(t->args());
   }
-  ASS(toDo->isEmpty());
-  ASS(terms->isEmpty());
-  ASS_EQ(modified->length(),1);
-  ASS_EQ(args->length(),trm->arity());
+  ASS(toDo.isEmpty());
+  ASS(terms.isEmpty());
+  ASS_EQ(modified.length(),1);
+  ASS_EQ(args.length(),trm->arity());
 
   Term* result;
-  if(!modified->pop()) {
+  if(!modified.pop()) {
     result=trm;
   }
   else {
     //here we assume, that stack is an array with
     //second topmost element as &top()-1, third at
     //&top()-2, etc...
-    TermList* argLst=&args->top() - (trm->arity()-1);
-    ASS_EQ(args->size(), trm->arity());
+    TermList* argLst=&args.top() - (trm->arity()-1);
+    ASS_EQ(args.size(), trm->arity());
     if(trm->isLiteral()) {
       ASS(!noSharing);
       Literal* lit = static_cast<Literal*>(trm);

Lib/Map.hpp

@@ -514,6 +514,9 @@ class Map
    */
   void reset()
   {
+    if (_noOfEntries == 0) {
+      return;
+    }
     for (int i = _capacity-1;i >= 0;i--) {
       _entries[i].reset();
     }

Lib/Recycled.hpp

@@ -134,8 +134,8 @@ class Recycled
 {
   using Self = IF_USE_PTRS(std::unique_ptr<T>,T);
   Self _self;
-  Reset _reset;
-  Keep _keep;
+  [[no_unique_address]] Reset _reset;
+  [[no_unique_address]] Keep _keep;
 
   static bool memAlive;
   static Stack<Self>& mem() {
@@ -218,6 +218,34 @@ class Recycled
 template<class T, class Reset, class Keep>
 bool Recycled<T, Reset, Keep>::memAlive = true;
 
+/**
+ * Like Recycled, but cheaper for objects needed on every call of a small,
+ * possibly reentrant function: one object is kept for each nesting depth.
+ * The object is reset when taken.
+ */
+template<class T, class Reset = DefaultReset>
+class Scratch
+{
+  static inline Stack<T*> _all;
+  static inline unsigned _depth = 0;
+  T* _self;
+public:
+  Scratch()
+  {
+    if (_depth == _all.size()) {
+      _all.push(new T());
+    }
+    _self = _all[_depth++];
+    Reset()(*_self);
+  }
+  ~Scratch() { _depth--; }
+  Scratch(Scratch const&) = delete;
+  Scratch& operator=(Scratch const&) = delete;
+
+  T& operator* () { return *_self; }
+  T* operator->() { return _self; }
+};
+
 };
 
 template<class T>