vprover · MichaelRawson · Mar 28, 2025
diff --git a/Debug/TimeProfiling.hpp b/Debug/TimeProfiling.hpp
@@ -131,7 +131,6 @@ class TimeTrace
 
 
   struct Node {
-    USE_ALLOCATOR(Node)
     const char* name;
     Lib::Stack<std::unique_ptr<Node>> children;
     Measurements measurements;

diff --git a/Indexing/AcyclicityIndex.cpp b/Indexing/AcyclicityIndex.cpp
@@ -128,7 +128,6 @@ namespace Indexing
       subterms(subterms)
     {}
 
-    USE_ALLOCATOR(AcyclicityIndex::IndexEntry);
 
     Literal* lit;
     Clause* clause;
@@ -173,7 +172,6 @@ namespace Indexing
       return new CycleSearchTreeNode(t, l, c, n, n ? n->depth : 0, substIndex, true);
     }
 
-    USE_ALLOCATOR(AcyclicityIndex::CycleSearchTreeNode);
 
     TypedTermList term;
     Literal *lit;

diff --git a/Indexing/AcyclicityIndex.hpp b/Indexing/AcyclicityIndex.hpp
@@ -40,7 +40,6 @@ struct CycleQueryResult {
     clausesTheta(c)
   {}
 
-  USE_ALLOCATOR(CycleQueryResult);
 
   unsigned totalLengthClauses();
 

diff --git a/Indexing/ClauseCodeTree.hpp b/Indexing/ClauseCodeTree.hpp
@@ -63,7 +63,6 @@ class ClauseCodeTree : public CodeTree
     void init(CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_,
 	ClauseCodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_);
 
-    USE_ALLOCATOR(RemovingLiteralMatcher);
   };
 
   //////// retrieval //////////
@@ -82,7 +81,6 @@ class ClauseCodeTree : public CodeTree
 
     inline ILStruct* getILS() { ASS(matched()); return op->getILS(); }
 
-    USE_ALLOCATOR(LiteralMatcher);
 
   private:
     bool _eagerlyMatched;
@@ -104,7 +102,6 @@ class ClauseCodeTree : public CodeTree
     bool matched() { return lms.isNonEmpty() && lms.top()->success(); }
     CodeOp* getSuccessOp() { ASS(matched()); return lms.top()->op; }
 
-    USE_ALLOCATOR(ClauseMatcher);
 
   private:
     void enterLiteral(CodeOp* entry, bool seekOnlySuccess);

diff --git a/Indexing/CodeTree.hpp b/Indexing/CodeTree.hpp
@@ -117,7 +117,6 @@ class CodeTree
 
     void ensureFreshness(unsigned globalTimestamp);
 
-    USE_ALLOCATOR(ILStruct);
 
     struct GVArrComparator;
 

diff --git a/Indexing/CodeTreeInterfaces.cpp b/Indexing/CodeTreeInterfaces.cpp
@@ -44,7 +44,6 @@ class CodeTreeSubstitution
   : _bindings(bindings), _resultNormalizer(resultNormalizer)
   {}
 
-  USE_ALLOCATOR(CodeTreeSubstitution);
 
   TermList apply(unsigned var)
   {
@@ -109,7 +108,6 @@ class CodeTreeTIS<Data>::ResultIterator
     }
   }
 
-  USE_ALLOCATOR(ResultIterator);
 
   bool hasNext()
   {

diff --git a/Indexing/LiteralMiniIndex.hpp b/Indexing/LiteralMiniIndex.hpp
@@ -30,7 +30,6 @@ using namespace Kernel;
 class LiteralMiniIndex
 {
 public:
-  USE_ALLOCATOR(LiteralMiniIndex);
 
   LiteralMiniIndex() = default;
   void init(Clause* cl);

diff --git a/Indexing/ResultSubstitution.cpp b/Indexing/ResultSubstitution.cpp
@@ -26,7 +26,6 @@ class RSProxy
 : public ResultSubstitution
 {
 public:
-  USE_ALLOCATOR(RSProxy);
 
   RSProxy(RobSubstitution* subst, int queryBank, int resultBank)
   : _subst(subst), _queryBank(queryBank), _resultBank(resultBank) {}

diff --git a/Indexing/SubstitutionTree.hpp b/Indexing/SubstitutionTree.hpp
@@ -454,7 +454,6 @@ class SubstitutionTree final
       virtual Node** childByTop(TermList::Top t, bool canCreate);
       void remove(TermList::Top t);
 
-      USE_ALLOCATOR(UArrIntermediateNode);
 
       int _size;
       Node* _nodes[UARR_INTERMEDIATE_NODE_MAX_SIZE+1];
@@ -517,7 +516,6 @@ class SubstitutionTree final
       inline void remove(TermList::Top t)
       { _nodes.remove(t); }
 
-      USE_ALLOCATOR(SListIntermediateNode);
 
       class NodePtrComparator
       {
@@ -723,7 +721,6 @@ class SubstitutionTree final
       GenMatcher(TermOrLit query, unsigned nextSpecVar)
       { init(query,nextSpecVar); }
 
-      USE_ALLOCATOR(GenMatcher);
 
       /**
        * Bind special variable @b var to @b term. This method
@@ -904,7 +901,6 @@ class SubstitutionTree final
     {
     public:
 
-      USE_ALLOCATOR(InstMatcher);
 
       void reset() {
         _boundVars.reset();

diff --git a/Indexing/SubstitutionTree_FastGen.hpp b/Indexing/SubstitutionTree_FastGen.hpp
@@ -81,7 +81,6 @@ struct SubstitutionTree<LeafData_>::GenMatcher::Binder
 template<class LeafData_>
 struct SubstitutionTree<LeafData_>::GenMatcher::Applicator
 {
-  USE_ALLOCATOR(SubstitutionTree::GenMatcher::Applicator); 
 
   inline
   Applicator(GenMatcher* parent, Renaming* resultNormalizer)
@@ -108,7 +107,6 @@ class SubstitutionTree<LeafData_>::GenMatcher::Substitution
 : public ResultSubstitution
 {
 public:
-  USE_ALLOCATOR(SubstitutionTree::GenMatcher::Substitution);
 
   Substitution(GenMatcher* parent, Renaming* resultNormalizer)
   : _parent(parent), _resultNormalizer(resultNormalizer),

diff --git a/Indexing/SubstitutionTree_FastInst.hpp b/Indexing/SubstitutionTree_FastInst.hpp
@@ -34,7 +34,6 @@ class SubstitutionTree<LeafData_>::InstMatcher::Substitution
 : public ResultSubstitution
 {
 public:
-  USE_ALLOCATOR(SubstitutionTree::InstMatcher::Substitution);
 
   Substitution(InstMatcher* parent, Renaming* resultDenormalizer)
   : _parent(parent), _resultDenormalizer(resultDenormalizer)

diff --git a/Indexing/SubstitutionTree_Nodes.hpp b/Indexing/SubstitutionTree_Nodes.hpp
@@ -68,7 +68,6 @@ class SubstitutionTree<LeafData_>::UListLeaf
     _size--;
   }
 
-  USE_ALLOCATOR(UListLeaf);
 private:
   typedef List<LeafData> LDList;
   LDList* _children;
@@ -100,7 +99,6 @@ class SubstitutionTree<LeafData_>::SListLeaf
   void insert(LeafData ld) override { _children.insert(ld); }
   void remove(LeafData ld) override { _children.remove(ld); }
 
-  USE_ALLOCATOR(SListLeaf);
 private:
   typedef SkipList<LeafData,LDComparator> LDSkipList;
   LDSkipList _children;

diff --git a/Indexing/TermCodeTree.hpp b/Indexing/TermCodeTree.hpp
@@ -70,7 +70,6 @@ class TermCodeTree : public CodeTree
 
     Data* next();
 
-    USE_ALLOCATOR(TermMatcher);
   };
 
 };

diff --git a/Inferences/ALASCA/BinInf.hpp b/Inferences/ALASCA/BinInf.hpp
@@ -54,7 +54,6 @@ struct BinInf
   AlascaIndex<Lhs>* _lhs;
   AlascaIndex<Rhs>* _rhs;
 public:
-  USE_ALLOCATOR(BinInf);
 
   BinInf(BinInf&&) = default;
   BinInf(std::shared_ptr<AlascaState> shared, Rule rule)
@@ -176,7 +175,6 @@ struct TriInf
   AlascaIndex<Premise1>* _prem1;
   AlascaIndex<Premise2>* _prem2;
 public:
-  USE_ALLOCATOR(TriInf);
 
   TriInf(TriInf&&) = default;
   TriInf(std::shared_ptr<AlascaState> shared, Rule rule)

diff --git a/Inferences/ALASCA/BwdDemodulation.hpp b/Inferences/ALASCA/BwdDemodulation.hpp
@@ -29,7 +29,6 @@ class BwdDemodulation
   using Rhs = Demodulation::Rhs;
   using Lhs = Demodulation::Lhs;
 public:
-  USE_ALLOCATOR(BwdDemodulation);
 
   BwdDemodulation(BwdDemodulation&&) = default;
   BwdDemodulation(std::shared_ptr<AlascaState> shared) 

diff --git a/Inferences/ALASCA/Demodulation.hpp b/Inferences/ALASCA/Demodulation.hpp
@@ -32,7 +32,6 @@ using namespace Saturation;
 class Demodulation
 {
 public:
-  USE_ALLOCATOR(Demodulation);
 
   // ±ks + t ≈ 0          C[sσ]
   // ============================

diff --git a/Inferences/ALASCA/EqFactoring.hpp b/Inferences/ALASCA/EqFactoring.hpp
@@ -34,7 +34,6 @@ class EqFactoring
 : public GeneratingInferenceEngine
 {
 public:
-  USE_ALLOCATOR(EqFactoring);
 
   EqFactoring(EqFactoring&&) = default;
   EqFactoring(std::shared_ptr<AlascaState> shared)

diff --git a/Inferences/ALASCA/FloorBounds.hpp b/Inferences/ALASCA/FloorBounds.hpp
@@ -144,7 +144,6 @@ class FloorBounds
   }
 
 public:
-  USE_ALLOCATOR(FloorBounds);
 
   FloorBounds(FloorBounds&&) = default;
   FloorBounds(std::shared_ptr<AlascaState> shared) 

diff --git a/Inferences/ALASCA/FwdDemodulation.hpp b/Inferences/ALASCA/FwdDemodulation.hpp
@@ -35,7 +35,6 @@ class FwdDemodulation
   using Rhs = Demodulation::Rhs;
   using Lhs = Demodulation::Lhs;
 public:
-  USE_ALLOCATOR(FwdDemodulation);
 
   FwdDemodulation(FwdDemodulation&&) = default;
   FwdDemodulation(std::shared_ptr<AlascaState> shared) 

diff --git a/Inferences/ALASCA/InequalityFactoring.hpp b/Inferences/ALASCA/InequalityFactoring.hpp
@@ -34,7 +34,6 @@ class InequalityFactoring
 : public GeneratingInferenceEngine
 {
 public:
-  USE_ALLOCATOR(InequalityFactoring);
 
   InequalityFactoring(InequalityFactoring&&) = default;
   InequalityFactoring(std::shared_ptr<AlascaState> shared)

diff --git a/Inferences/ALASCA/InequalityPredicateNormalization.hpp b/Inferences/ALASCA/InequalityPredicateNormalization.hpp
@@ -36,7 +36,6 @@ class InequalityPredicateNormalization
 : public ImmediateSimplificationEngine
 {
 public:
-  USE_ALLOCATOR(InequalityPredicateNormalization);
 
   InequalityPredicateNormalization(std::shared_ptr<AlascaState> shared) 
     : _shared(std::move(shared)) {}

diff --git a/Inferences/ALASCA/Normalization.hpp b/Inferences/ALASCA/Normalization.hpp
@@ -37,7 +37,6 @@ class Normalization
   std::shared_ptr<AlascaState> _shared;
 public: 
   Normalization(std::shared_ptr<AlascaState> shared) : _shared(std::move(shared)) {}
-  USE_ALLOCATOR(Normalization);
 
   virtual Clause* simplify(Clause* cl) final override;
 };
@@ -72,7 +71,6 @@ class FloorElimination
 
 public: 
   FloorElimination(std::shared_ptr<AlascaState> shared) : _shared(std::move(shared)) {}
-  USE_ALLOCATOR(FloorElimination);
 
   virtual Clause* simplify(Clause* cl) final override {
     auto res = RStack<Literal*>();

diff --git a/Inferences/ALASCA/TautologyDeletion.hpp b/Inferences/ALASCA/TautologyDeletion.hpp
@@ -29,7 +29,6 @@ class TautologyDeletion
 {
   std::shared_ptr<AlascaState> _shared;
 public:
-  USE_ALLOCATOR(TautologyDeletion);
 
   TautologyDeletion(std::shared_ptr<AlascaState> shared) 
     : _shared(std::move(shared)) {}

diff --git a/Inferences/ALASCA/TermFactoring.hpp b/Inferences/ALASCA/TermFactoring.hpp
@@ -38,7 +38,6 @@ class TermFactoring
 : public GeneratingInferenceEngine
 {
 public:
-  USE_ALLOCATOR(TermFactoring);
 
   TermFactoring(TermFactoring&&) = default;
   TermFactoring(std::shared_ptr<AlascaState> shared)

diff --git a/Inferences/ALASCA/VariableElimination.hpp b/Inferences/ALASCA/VariableElimination.hpp
@@ -34,7 +34,6 @@ class VariableElimination
 : public SimplifyingGeneratingInference
 {
 public:
-  USE_ALLOCATOR(VariableElimination);
 
   VariableElimination(VariableElimination&&) = default;
   VariableElimination(std::shared_ptr<AlascaState> shared, bool simplify = true) 

diff --git a/Inferences/Induction.hpp b/Inferences/Induction.hpp
@@ -307,7 +307,6 @@ class InductionClauseIterator
     processClause(premise);
   }
 
-  USE_ALLOCATOR(InductionClauseIterator);
   DECL_ELEMENT_TYPE(Clause*);
 
   inline bool hasNext() { return _clauses.isNonEmpty(); }

diff --git a/Inferences/SubsumptionDemodulationHelper.hpp b/Inferences/SubsumptionDemodulationHelper.hpp
@@ -59,7 +59,6 @@ using namespace Lib;
  */
 class OverlayBinder
 {
-  USE_ALLOCATOR(OverlayBinder);
 
   public:
     using Var = unsigned int;
@@ -217,7 +216,6 @@ std::ostream& operator<<(std::ostream& o, OverlayBinder const& binder);
  */
 class SDClauseMatches
 {
-  USE_ALLOCATOR(SDClauseMatches);
 
   public:
     SDClauseMatches(Clause* base, LiteralMiniIndex const& ixAlts);

diff --git a/Inferences/URResolution.cpp b/Inferences/URResolution.cpp
@@ -99,7 +99,6 @@ void URResolution::detach()
 
 struct URResolution::Item
 {
-  USE_ALLOCATOR(URResolution::Item);
 
   Item(Clause* cl, bool selectedOnly, URResolution& parent, bool mustResolveAll)
   : _orig(cl), _color(cl->color()), _parent(parent)

diff --git a/Kernel/ALASCA/Index.hpp b/Kernel/ALASCA/Index.hpp
@@ -42,7 +42,6 @@ template<class T>
 class AlascaIndex : public Indexing::Index
 {
 public:
-  USE_ALLOCATOR(AlascaIndex);
 
   AlascaIndex()
     : _index()

diff --git a/Kernel/ALASCA/Ordering.hpp b/Kernel/ALASCA/Ordering.hpp
@@ -390,7 +390,6 @@ class LiteralOrdering
   }
 
 public:
-  USE_ALLOCATOR(LiteralOrdering);
 
   LiteralOrdering(LiteralOrdering&& kbo) = default;
   LiteralOrdering& operator=(LiteralOrdering&& kbo) = default;

diff --git a/Kernel/ALASCA/State.hpp b/Kernel/ALASCA/State.hpp
@@ -20,7 +20,6 @@
 namespace Kernel {
   struct AlascaState 
   {
-    USE_ALLOCATOR(AlascaState);
 
     // TODO get rid of this
     static std::shared_ptr<AlascaState> globalState;
-Original file line number
+Diff line change
@@ Expand Up / @@ -40,7 +40,6 @@ struct CycleQueryResult { @@
         clausesTheta(c)
       {}
-      USE_ALLOCATOR(CycleQueryResult);
       unsigned totalLengthClauses();
@@ Expand Down @@
Original file line number	Diff line number	Diff line change
Expand Up		@@ -117,7 +117,6 @@ class CodeTree

		void ensureFreshness(unsigned globalTimestamp);

		USE_ALLOCATOR(ILStruct);

		struct GVArrComparator;

Expand Down