From 34fa1b0b05602121a8052324c3e6a9eb4de0a54b Mon Sep 17 00:00:00 2001 From: Michael Rawson Date: Fri, 28 Mar 2025 08:16:58 +0000 Subject: [PATCH] remove USE_ALLOCATOR --- Debug/TimeProfiling.hpp | 1 - Indexing/AcyclicityIndex.cpp | 2 -- Indexing/AcyclicityIndex.hpp | 1 - Indexing/ClauseCodeTree.hpp | 3 --- Indexing/CodeTree.hpp | 1 - Indexing/CodeTreeInterfaces.cpp | 2 -- Indexing/LiteralMiniIndex.hpp | 1 - Indexing/ResultSubstitution.cpp | 1 - Indexing/SubstitutionTree.hpp | 4 ---- Indexing/SubstitutionTree_FastGen.hpp | 2 -- Indexing/SubstitutionTree_FastInst.hpp | 1 - Indexing/SubstitutionTree_Nodes.hpp | 2 -- Indexing/TermCodeTree.hpp | 1 - Inferences/ALASCA/BinInf.hpp | 2 -- Inferences/ALASCA/BwdDemodulation.hpp | 1 - Inferences/ALASCA/Demodulation.hpp | 1 - Inferences/ALASCA/EqFactoring.hpp | 1 - Inferences/ALASCA/FloorBounds.hpp | 1 - Inferences/ALASCA/FwdDemodulation.hpp | 1 - Inferences/ALASCA/InequalityFactoring.hpp | 1 - .../ALASCA/InequalityPredicateNormalization.hpp | 1 - Inferences/ALASCA/Normalization.hpp | 2 -- Inferences/ALASCA/TautologyDeletion.hpp | 1 - Inferences/ALASCA/TermFactoring.hpp | 1 - Inferences/ALASCA/VariableElimination.hpp | 1 - Inferences/Induction.hpp | 1 - Inferences/SubsumptionDemodulationHelper.hpp | 2 -- Inferences/URResolution.cpp | 1 - Kernel/ALASCA/Index.hpp | 1 - Kernel/ALASCA/Ordering.hpp | 1 - Kernel/ALASCA/State.hpp | 1 - Kernel/Formula.hpp | 8 -------- Kernel/FormulaUnit.hpp | 1 - Kernel/Inference.cpp | 1 - Kernel/Inference.hpp | 1 - Kernel/InferenceStore.cpp | 1 - Kernel/MLMatcher.cpp | 1 - Kernel/MLMatcherSD.cpp | 1 - Kernel/Polynomial.hpp | 4 ---- Kernel/QKbo.hpp | 1 - Kernel/RobSubstitution.hpp | 2 -- Kernel/SubformulaIterator.cpp | 1 - Kernel/Substitution.hpp | 1 - Kernel/UnificationWithAbstraction.hpp | 1 - Lib/Allocator.hpp | 11 ----------- Lib/ArrayMap.hpp | 1 - Lib/Backtrackable.hpp | 1 - Lib/BinaryHeap.hpp | 2 -- Lib/DArray.hpp | 1 - Lib/DHMap.hpp | 1 - Lib/DHMultiset.hpp | 1 - Lib/DHSet.hpp | 1 - Lib/InverseLookup.hpp | 1 - Lib/List.hpp | 5 ----- Lib/Set.hpp | 1 - Lib/SkipList.hpp | 1 - Lib/SmartPtr.hpp | 1 - Lib/Stack.hpp | 1 - Lib/VirtualIterator.hpp | 3 --- SAT/SATInference.hpp | 3 --- SATSubsumption/SATSubsumptionAndResolution.hpp | 1 - Saturation/Splitter.hpp | 1 - Shell/BlockedClauseElimination.hpp | 2 -- Shell/FunctionDefinitionHandler.hpp | 2 -- Shell/LispParser.hpp | 1 - Shell/NewCNF.hpp | 3 --- Shell/Options.hpp | 2 -- 67 files changed, 114 deletions(-) diff --git a/Debug/TimeProfiling.hpp b/Debug/TimeProfiling.hpp index 68c819e599..c825148be3 100644 --- a/Debug/TimeProfiling.hpp +++ b/Debug/TimeProfiling.hpp @@ -131,7 +131,6 @@ class TimeTrace struct Node { - USE_ALLOCATOR(Node) const char* name; Lib::Stack> children; Measurements measurements; diff --git a/Indexing/AcyclicityIndex.cpp b/Indexing/AcyclicityIndex.cpp index 1841103b8b..9c96741f45 100644 --- 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 index 775cbb8d7a..bd32b396f5 100644 --- 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 index a7a64daf67..4ef917fd8d 100644 --- 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* 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 index 0f86724071..09c3e99a10 100644 --- 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 index 77c3a0ae5c..a9500f707d 100644 --- 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::ResultIterator } } - USE_ALLOCATOR(ResultIterator); bool hasNext() { diff --git a/Indexing/LiteralMiniIndex.hpp b/Indexing/LiteralMiniIndex.hpp index 0b648f9e96..6fbe6e9d78 100644 --- 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 index 3068e2c677..881ebb4a3e 100644 --- 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 index 22a5fb4476..0b813c9cd6 100644 --- 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 index b925538a95..658075ffb2 100644 --- a/Indexing/SubstitutionTree_FastGen.hpp +++ b/Indexing/SubstitutionTree_FastGen.hpp @@ -81,7 +81,6 @@ struct SubstitutionTree::GenMatcher::Binder template struct SubstitutionTree::GenMatcher::Applicator { - USE_ALLOCATOR(SubstitutionTree::GenMatcher::Applicator); inline Applicator(GenMatcher* parent, Renaming* resultNormalizer) @@ -108,7 +107,6 @@ class SubstitutionTree::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 index 7ea79a5455..33849056c2 100644 --- a/Indexing/SubstitutionTree_FastInst.hpp +++ b/Indexing/SubstitutionTree_FastInst.hpp @@ -34,7 +34,6 @@ class SubstitutionTree::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 index aa3002ccfc..8fab921b1a 100644 --- a/Indexing/SubstitutionTree_Nodes.hpp +++ b/Indexing/SubstitutionTree_Nodes.hpp @@ -68,7 +68,6 @@ class SubstitutionTree::UListLeaf _size--; } - USE_ALLOCATOR(UListLeaf); private: typedef List LDList; LDList* _children; @@ -100,7 +99,6 @@ class SubstitutionTree::SListLeaf void insert(LeafData ld) override { _children.insert(ld); } void remove(LeafData ld) override { _children.remove(ld); } - USE_ALLOCATOR(SListLeaf); private: typedef SkipList LDSkipList; LDSkipList _children; diff --git a/Indexing/TermCodeTree.hpp b/Indexing/TermCodeTree.hpp index 6565c4318c..3de422d795 100644 --- 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 index 13e76d837c..b8880d18c7 100644 --- a/Inferences/ALASCA/BinInf.hpp +++ b/Inferences/ALASCA/BinInf.hpp @@ -54,7 +54,6 @@ struct BinInf AlascaIndex* _lhs; AlascaIndex* _rhs; public: - USE_ALLOCATOR(BinInf); BinInf(BinInf&&) = default; BinInf(std::shared_ptr shared, Rule rule) @@ -176,7 +175,6 @@ struct TriInf AlascaIndex* _prem1; AlascaIndex* _prem2; public: - USE_ALLOCATOR(TriInf); TriInf(TriInf&&) = default; TriInf(std::shared_ptr shared, Rule rule) diff --git a/Inferences/ALASCA/BwdDemodulation.hpp b/Inferences/ALASCA/BwdDemodulation.hpp index e47764b02a..81222ad321 100644 --- 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 shared) diff --git a/Inferences/ALASCA/Demodulation.hpp b/Inferences/ALASCA/Demodulation.hpp index d9fc3a66cd..1cc2acbd10 100644 --- 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 index c0e01c118e..33cfeb7d2f 100644 --- 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 shared) diff --git a/Inferences/ALASCA/FloorBounds.hpp b/Inferences/ALASCA/FloorBounds.hpp index eeb799ff3a..5bc6bb2f0b 100644 --- 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 shared) diff --git a/Inferences/ALASCA/FwdDemodulation.hpp b/Inferences/ALASCA/FwdDemodulation.hpp index 3ec5deed66..8cb322dd1f 100644 --- 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 shared) diff --git a/Inferences/ALASCA/InequalityFactoring.hpp b/Inferences/ALASCA/InequalityFactoring.hpp index 026e54ce2f..2270357145 100644 --- 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 shared) diff --git a/Inferences/ALASCA/InequalityPredicateNormalization.hpp b/Inferences/ALASCA/InequalityPredicateNormalization.hpp index cb3d587f02..05b08641a5 100644 --- 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 shared) : _shared(std::move(shared)) {} diff --git a/Inferences/ALASCA/Normalization.hpp b/Inferences/ALASCA/Normalization.hpp index cd40e10917..f10cdc49fe 100644 --- a/Inferences/ALASCA/Normalization.hpp +++ b/Inferences/ALASCA/Normalization.hpp @@ -37,7 +37,6 @@ class Normalization std::shared_ptr _shared; public: Normalization(std::shared_ptr 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 shared) : _shared(std::move(shared)) {} - USE_ALLOCATOR(FloorElimination); virtual Clause* simplify(Clause* cl) final override { auto res = RStack(); diff --git a/Inferences/ALASCA/TautologyDeletion.hpp b/Inferences/ALASCA/TautologyDeletion.hpp index 92cfa2d2b8..b55ce21c91 100644 --- a/Inferences/ALASCA/TautologyDeletion.hpp +++ b/Inferences/ALASCA/TautologyDeletion.hpp @@ -29,7 +29,6 @@ class TautologyDeletion { std::shared_ptr _shared; public: - USE_ALLOCATOR(TautologyDeletion); TautologyDeletion(std::shared_ptr shared) : _shared(std::move(shared)) {} diff --git a/Inferences/ALASCA/TermFactoring.hpp b/Inferences/ALASCA/TermFactoring.hpp index dd46170f19..9714dcfb56 100644 --- 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 shared) diff --git a/Inferences/ALASCA/VariableElimination.hpp b/Inferences/ALASCA/VariableElimination.hpp index 334d8cb4bc..129c524315 100644 --- 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 shared, bool simplify = true) diff --git a/Inferences/Induction.hpp b/Inferences/Induction.hpp index 8bf07cfd77..971e9f4f61 100644 --- 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 index 48adb4a49e..bd6aee0de9 100644 --- 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 index d3ce81dd8d..275e523910 100644 --- 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 index 3a0764a464..4e824cefc2 100644 --- a/Kernel/ALASCA/Index.hpp +++ b/Kernel/ALASCA/Index.hpp @@ -42,7 +42,6 @@ template class AlascaIndex : public Indexing::Index { public: - USE_ALLOCATOR(AlascaIndex); AlascaIndex() : _index() diff --git a/Kernel/ALASCA/Ordering.hpp b/Kernel/ALASCA/Ordering.hpp index 5926b64687..560c8fe260 100644 --- 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 index 7123a2e987..b2d6bf2e37 100644 --- 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 globalState; diff --git a/Kernel/Formula.hpp b/Kernel/Formula.hpp index 9a250c0901..9a894e397a 100644 --- a/Kernel/Formula.hpp +++ b/Kernel/Formula.hpp @@ -103,7 +103,6 @@ class Formula // use allocator to (de)allocate objects of this class - USE_ALLOCATOR(Formula); protected: /** Create a dummy formula will null content */ @@ -129,7 +128,6 @@ class NamedFormula public: explicit NamedFormula(std::string name) : Formula(NAME), _name(name) {} - USE_ALLOCATOR(NamedFormula); std::string name(){ return _name; } const std::string name() const { return _name;} @@ -164,7 +162,6 @@ class AtomicFormula void setLiteral(Literal* lit) { _literal = lit; } // use allocator to (de)allocate objects of this class - USE_ALLOCATOR(AtomicFormula); protected: /** The literal of this formula */ Literal* _literal; @@ -207,7 +204,6 @@ class QuantifiedFormula SList** sortListPtr() { return &_sorts; } // use allocator to (de)allocate objects of this class - USE_ALLOCATOR(QuantifiedFormula); protected: /** list of variables */ VList* _vars; @@ -237,7 +233,6 @@ class NegatedFormula Formula* subformula() { return _arg; } // use allocator to (de)allocate objects of this class - USE_ALLOCATOR(NegatedFormula); protected: /** The immediate subformula */ Formula* _arg; @@ -276,7 +271,6 @@ class BinaryFormula } // use allocator to (de)allocate objects of this class - USE_ALLOCATOR(BinaryFormula); protected: /** The lhs subformula */ Formula* _left; @@ -314,7 +308,6 @@ class JunctionFormula static Formula* generalJunction(Connective c, FormulaList* args); // use allocator to (de)allocate objects of this class - USE_ALLOCATOR(JunctionFormula); protected: /** list of immediate subformulas */ FormulaList* _args; @@ -369,7 +362,6 @@ class BoolTermFormula TermList getTerm() { return _ts; } // use allocator to (de)allocate objects of this class - USE_ALLOCATOR(BoolTermFormula); protected: /** boolean term */ TermList _ts; diff --git a/Kernel/FormulaUnit.hpp b/Kernel/FormulaUnit.hpp index 41c8372369..0182f10092 100644 --- a/Kernel/FormulaUnit.hpp +++ b/Kernel/FormulaUnit.hpp @@ -56,7 +56,6 @@ class FormulaUnit Color getColor(); unsigned weight(); - USE_ALLOCATOR(FormulaUnit); protected: /** Formula of this unit */ diff --git a/Kernel/Inference.cpp b/Kernel/Inference.cpp index 654df68637..d091e2e0d9 100644 --- a/Kernel/Inference.cpp +++ b/Kernel/Inference.cpp @@ -60,7 +60,6 @@ UnitInputType Kernel::getInputType(UnitList* units) * To be kept around in _ptr2 of INFERENCE_FROM_SAT_REFUTATION **/ struct FromSatRefutationInfo { - USE_ALLOCATOR(FromSatRefutationInfo); FromSatRefutationInfo(const FromSatRefutation& fsr) : _satPremises(fsr._satPremises), _usedAssumptions(fsr._usedAssumptions) { ASS(_satPremises); } diff --git a/Kernel/Inference.hpp b/Kernel/Inference.hpp index bb9c78f5b6..2c425e4cfd 100644 --- a/Kernel/Inference.hpp +++ b/Kernel/Inference.hpp @@ -744,7 +744,6 @@ class Inference { private: // don't construct on the heap - USE_ALLOCATOR(Inference); enum class Kind : unsigned char { INFERENCE_012, diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp index 4ce2200a39..a7390793a9 100644 --- a/Kernel/InferenceStore.cpp +++ b/Kernel/InferenceStore.cpp @@ -837,7 +837,6 @@ struct InferenceStore::ProofCheckPrinter struct InferenceStore::Smt2ProofCheckPrinter : public InferenceStore::ProofPrinter { - USE_ALLOCATOR(InferenceStore::Smt2ProofCheckPrinter); Smt2ProofCheckPrinter(std::ostream& out, InferenceStore* is) : ProofPrinter(out, is) {} diff --git a/Kernel/MLMatcher.cpp b/Kernel/MLMatcher.cpp index 9d502900f6..ea2b985b6f 100644 --- a/Kernel/MLMatcher.cpp +++ b/Kernel/MLMatcher.cpp @@ -356,7 +356,6 @@ using namespace Lib; class MLMatcher::Impl final { public: - USE_ALLOCATOR(MLMatcher::Impl); Impl(); ~Impl() = default; diff --git a/Kernel/MLMatcherSD.cpp b/Kernel/MLMatcherSD.cpp index f77883c480..72ddcbfa7f 100644 --- a/Kernel/MLMatcherSD.cpp +++ b/Kernel/MLMatcherSD.cpp @@ -701,7 +701,6 @@ using namespace Lib; class MLMatcherSD::Impl final { public: - USE_ALLOCATOR(MLMatcherSD::Impl); Impl(); ~Impl() = default; diff --git a/Kernel/Polynomial.hpp b/Kernel/Polynomial.hpp index 2c30ffd63b..2e765a5714 100644 --- a/Kernel/Polynomial.hpp +++ b/Kernel/Polynomial.hpp @@ -159,7 +159,6 @@ class AnyPoly; template struct Monom { - USE_ALLOCATOR(Monom) using Numeral = typename Number::ConstantType; @@ -209,7 +208,6 @@ class FuncTerm FuncId _fun; Stack _args; public: - USE_ALLOCATOR(FuncTerm) FuncTerm(FuncId f, Stack&& args); FuncTerm(FuncId f, PolyNf* args); @@ -427,7 +425,6 @@ class MonomFactors friend struct std::hash; public: - USE_ALLOCATOR(MonomFactors) /** * constructs a new MonomFactors. @@ -521,7 +518,6 @@ class Polynom public: using NumTraits = Number; - USE_ALLOCATOR(Polynom) /** * constructs a new Polynom with a list of summands diff --git a/Kernel/QKbo.hpp b/Kernel/QKbo.hpp index df9c3bbb4a..915bf75dcf 100644 --- a/Kernel/QKbo.hpp +++ b/Kernel/QKbo.hpp @@ -73,7 +73,6 @@ class QKbo std::shared_ptr _norm; KBO _kbo; public: - USE_ALLOCATOR(QKbo); QKbo(QKbo&& kbo) = default; QKbo& operator=(QKbo&& kbo) = default; diff --git a/Kernel/RobSubstitution.hpp b/Kernel/RobSubstitution.hpp index cee0630b7d..32152e4874 100644 --- a/Kernel/RobSubstitution.hpp +++ b/Kernel/RobSubstitution.hpp @@ -260,7 +260,6 @@ class UnificationConstraint TermSpec _sort; public: UnificationConstraint() {} - USE_ALLOCATOR(UnificationConstraint) auto asTuple() const -> decltype(auto) { return std::tie(_t1, _t2, _sort); } IMPL_COMPARISONS_FROM_TUPLE(UnificationConstraint); IMPL_HASH_FROM_TUPLE(UnificationConstraint); @@ -298,7 +297,6 @@ class RobSubstitution mutable OnlyMemorizeNonVar _applyMemo; public: - USE_ALLOCATOR(RobSubstitution); RobSubstitution() : _startedBindingOutputVars(false) diff --git a/Kernel/SubformulaIterator.cpp b/Kernel/SubformulaIterator.cpp index 560cdb64e6..f7caf73463 100644 --- a/Kernel/SubformulaIterator.cpp +++ b/Kernel/SubformulaIterator.cpp @@ -67,7 +67,6 @@ class SubformulaIterator::Element { int _polarity; Element* _rest; - USE_ALLOCATOR(SubformulaIterator::Element); }; diff --git a/Kernel/Substitution.hpp b/Kernel/Substitution.hpp index 5eb10a2068..6bb759e374 100644 --- a/Kernel/Substitution.hpp +++ b/Kernel/Substitution.hpp @@ -37,7 +37,6 @@ using namespace Lib; class Substitution { public: - USE_ALLOCATOR(Substitution); Substitution() {} diff --git a/Kernel/UnificationWithAbstraction.hpp b/Kernel/UnificationWithAbstraction.hpp index 7ea19388b3..48942df870 100644 --- a/Kernel/UnificationWithAbstraction.hpp +++ b/Kernel/UnificationWithAbstraction.hpp @@ -34,7 +34,6 @@ class UnificationConstraintStack { Stack _cont; public: - USE_ALLOCATOR(UnificationConstraintStack) UnificationConstraintStack() : _cont() {} UnificationConstraintStack(UnificationConstraintStack&&) = delete; UnificationConstraintStack& operator=(UnificationConstraintStack&&) = delete; diff --git a/Lib/Allocator.hpp b/Lib/Allocator.hpp index 5f3d02ee1d..1832ca658b 100644 --- a/Lib/Allocator.hpp +++ b/Lib/Allocator.hpp @@ -48,8 +48,6 @@ inline void free(void *pointer, size_t size, size_t align = alignof(std::max_ali ::operator delete(pointer, (std::align_val_t)align); } } // namespace Lib -#define USE_GLOBAL_SMALL_OBJECT_ALLOCATOR(C) - // do some of our own allocation #else // INDIVIDUAL_ALLOCATIONS @@ -275,18 +273,9 @@ inline void free(void *pointer, size_t size) { } } // namespace Lib - -// overload class-specific operator new to call the global small-object allocator -#define USE_GLOBAL_SMALL_OBJECT_ALLOCATOR(C) \ - void *operator new(size_t size) { return Lib::alloc(size, alignof(C)); }\ - void *operator new(size_t size, std::align_val_t align) { return Lib::alloc(size, (size_t)align); }\ - void operator delete(void *ptr, size_t size) { Lib::free(ptr, size, alignof(C)); } \ - void operator delete(void *ptr, size_t size, std::align_val_t align) { Lib::free(ptr, size, (size_t)align); } - #endif // INDIVIDUAL_ALLOCATIONS's else // legacy macros, should be removed eventually -#define USE_ALLOCATOR(C) USE_GLOBAL_SMALL_OBJECT_ALLOCATOR(C) #define ALLOC_KNOWN(size, className) Lib::alloc(size) #define DEALLOC_KNOWN(ptr, size, className) Lib::free(ptr, size) diff --git a/Lib/ArrayMap.hpp b/Lib/ArrayMap.hpp index f756f6c94f..a5204b1e9f 100644 --- a/Lib/ArrayMap.hpp +++ b/Lib/ArrayMap.hpp @@ -48,7 +48,6 @@ class ArrayMap { typedef ArrayMapEntry Entry; public: - USE_ALLOCATOR(ArrayMap); /** * Create the map object diff --git a/Lib/Backtrackable.hpp b/Lib/Backtrackable.hpp index 2ebdb0af47..a70b076939 100644 --- a/Lib/Backtrackable.hpp +++ b/Lib/Backtrackable.hpp @@ -67,7 +67,6 @@ class BacktrackClosure : public BacktrackObject { F _fun; public: - USE_ALLOCATOR(BacktrackClosure); BacktrackClosure(BacktrackClosure&&) = default; BacktrackClosure& operator=(BacktrackClosure&&) = default; diff --git a/Lib/BinaryHeap.hpp b/Lib/BinaryHeap.hpp index 5b1e504cfe..602acf45bc 100644 --- a/Lib/BinaryHeap.hpp +++ b/Lib/BinaryHeap.hpp @@ -241,7 +241,6 @@ class BinaryHeap { _bh->backtrackPop(_val,_lastBubbleIndex); } - USE_ALLOCATOR(BHPopBacktrackObject); private: BinaryHeap* _bh; T _val; @@ -258,7 +257,6 @@ class BinaryHeap { _bh->backtrackInsert(_lastBubbleIndex); } - USE_ALLOCATOR(BHInsertBacktrackObject); private: BinaryHeap* _bh; unsigned _lastBubbleIndex; diff --git a/Lib/DArray.hpp b/Lib/DArray.hpp index 36d44c1b4e..44881669dd 100644 --- a/Lib/DArray.hpp +++ b/Lib/DArray.hpp @@ -39,7 +39,6 @@ template class DArray { public: - USE_ALLOCATOR(DArray); class Iterator; diff --git a/Lib/DHMap.hpp b/Lib/DHMap.hpp index 2477a1c12a..262a4154a1 100644 --- a/Lib/DHMap.hpp +++ b/Lib/DHMap.hpp @@ -57,7 +57,6 @@ template class DHMap { public: - USE_ALLOCATOR(DHMap); /** Create a new DHMap */ DHMap() diff --git a/Lib/DHMultiset.hpp b/Lib/DHMultiset.hpp index d8b4406ec1..ede929e1a1 100644 --- a/Lib/DHMultiset.hpp +++ b/Lib/DHMultiset.hpp @@ -52,7 +52,6 @@ template class DHMultiset { public: - USE_ALLOCATOR(DHMultiset); /** Create a new DHMultiset */ DHMultiset() diff --git a/Lib/DHSet.hpp b/Lib/DHSet.hpp index c03a0c9866..62f1fcf4e0 100644 --- a/Lib/DHSet.hpp +++ b/Lib/DHSet.hpp @@ -38,7 +38,6 @@ template class DHSet { public: - USE_ALLOCATOR(DHSet); /** Empty the DHSet */ void reset() diff --git a/Lib/InverseLookup.hpp b/Lib/InverseLookup.hpp index 9a849321cc..97f1dc37b1 100644 --- a/Lib/InverseLookup.hpp +++ b/Lib/InverseLookup.hpp @@ -31,7 +31,6 @@ class InverseLookup InverseLookup(const InverseLookup&); InverseLookup& operator=(const InverseLookup&); public: - USE_ALLOCATOR(InverseLookup); template InverseLookup(Arr arr, size_t size) diff --git a/Lib/List.hpp b/Lib/List.hpp index a19ce1d403..e79271dad6 100644 --- a/Lib/List.hpp +++ b/Lib/List.hpp @@ -468,7 +468,6 @@ class List /** iterator over the list elements */ class Iterator { public: - USE_ALLOCATOR(List::Iterator); DECL_ELEMENT_TYPE(C); @@ -511,7 +510,6 @@ class List /** iterator over references to list elements */ class RefIterator { public: - USE_ALLOCATOR(List::RefIterator); DECL_ELEMENT_TYPE(C&); @@ -543,7 +541,6 @@ class List /** Iterator that allows one to delete the current element */ class DelIterator { public: - USE_ALLOCATOR(List::DelIterator); DECL_ELEMENT_TYPE(C); DelIterator (List*& l) @@ -690,7 +687,6 @@ class List */ class DestructiveIterator { public: - USE_ALLOCATOR(List::DestructiveIterator); DECL_ELEMENT_TYPE(C); @@ -717,7 +713,6 @@ class List }; // use allocator to (de)allocate objects of this class - USE_ALLOCATOR(List); /** * Class that allows to create a list initially by pushing element both at the beginning (pushFront, the usual push) diff --git a/Lib/Set.hpp b/Lib/Set.hpp index 5fcd86f55f..fd17ff9769 100644 --- a/Lib/Set.hpp +++ b/Lib/Set.hpp @@ -84,7 +84,6 @@ class Set public: // use allocator to (de)allocate objects of this class - USE_ALLOCATOR(Set); /** Create a new Set */ Set() diff --git a/Lib/SkipList.hpp b/Lib/SkipList.hpp index 8b3587f3e0..2f20c2cb76 100644 --- a/Lib/SkipList.hpp +++ b/Lib/SkipList.hpp @@ -42,7 +42,6 @@ template class SkipList { public: - USE_ALLOCATOR(SkipList); class Node { public: diff --git a/Lib/SmartPtr.hpp b/Lib/SmartPtr.hpp index d0f4bae455..62aab77ba5 100644 --- a/Lib/SmartPtr.hpp +++ b/Lib/SmartPtr.hpp @@ -32,7 +32,6 @@ template class SmartPtr { private: struct RefCounter { - USE_ALLOCATOR(SmartPtr::RefCounter); inline explicit RefCounter(int v) : _val(v) {} diff --git a/Lib/Stack.hpp b/Lib/Stack.hpp index 4b56ee3344..60858a3f72 100644 --- a/Lib/Stack.hpp +++ b/Lib/Stack.hpp @@ -57,7 +57,6 @@ class Stack DECL_ELEMENT_TYPE(C); DECL_ITERATOR_TYPE(Iterator); - USE_ALLOCATOR(Stack); /** diff --git a/Lib/VirtualIterator.hpp b/Lib/VirtualIterator.hpp index 8a2c95de0c..14db0f5310 100644 --- a/Lib/VirtualIterator.hpp +++ b/Lib/VirtualIterator.hpp @@ -100,7 +100,6 @@ class EmptyIterator : public IteratorCore { public: - USE_ALLOCATOR(EmptyIterator); EmptyIterator() {} bool hasNext() { return false; }; @@ -124,7 +123,6 @@ class EmptyIterator template class VirtualIterator { public: - USE_ALLOCATOR(VirtualIterator); DECL_ELEMENT_TYPE(T); @@ -298,7 +296,6 @@ class ProxyIterator : public IteratorCore { public: - USE_ALLOCATOR(ProxyIterator); DEFAULT_CONSTRUCTORS(ProxyIterator) virtual ~ProxyIterator() override {} diff --git a/SAT/SATInference.hpp b/SAT/SATInference.hpp index 4e9b59929d..7c642515ff 100644 --- a/SAT/SATInference.hpp +++ b/SAT/SATInference.hpp @@ -82,7 +82,6 @@ class SATInference class PropInference : public SATInference { public: - USE_ALLOCATOR(PropInference); PropInference(SATClauseList* premises) : _premises(premises) {} PropInference(SATClause* prem) : _premises(0) @@ -110,7 +109,6 @@ class PropInference : public SATInference class FOConversionInference : public SATInference { public: - USE_ALLOCATOR(FOConversionInference); FOConversionInference(Unit* origin); FOConversionInference(Clause* cl); @@ -125,7 +123,6 @@ class FOConversionInference : public SATInference class AssumptionInference : public SATInference { public: - USE_ALLOCATOR(AssumptionInference); virtual InfType getType() const { return ASSUMPTION; } }; diff --git a/SATSubsumption/SATSubsumptionAndResolution.hpp b/SATSubsumption/SATSubsumptionAndResolution.hpp index 43d0edb7fb..0bcdde2a78 100644 --- a/SATSubsumption/SATSubsumptionAndResolution.hpp +++ b/SATSubsumption/SATSubsumptionAndResolution.hpp @@ -106,7 +106,6 @@ class SATSubsumptionAndResolution { * The Match set allows to get a line or column of the matrix */ struct MatchSet { - USE_ALLOCATOR(SATSubsumptionAndResolution::MatchSet); friend struct Match; /// @brief Metadata remembering whether some positive match or negative match was found for each literal in M diff --git a/Saturation/Splitter.hpp b/Saturation/Splitter.hpp index 3ac8df5013..e82d88a6e4 100644 --- a/Saturation/Splitter.hpp +++ b/Saturation/Splitter.hpp @@ -184,7 +184,6 @@ class Splitter { Stack partialRedundancyEntries; bool active; - USE_ALLOCATOR(SplitRecord); }; public: diff --git a/Shell/BlockedClauseElimination.hpp b/Shell/BlockedClauseElimination.hpp index 29f62c92b6..59565cd021 100644 --- a/Shell/BlockedClauseElimination.hpp +++ b/Shell/BlockedClauseElimination.hpp @@ -41,7 +41,6 @@ class BlockedClauseElimination struct ClWrapper; struct Candidate { - USE_ALLOCATOR(Candidate); ClWrapper* clw; unsigned litIdx; // index of the potentially blocking literal L @@ -56,7 +55,6 @@ class BlockedClauseElimination }; struct ClWrapper { - USE_ALLOCATOR(ClWrapper); Clause* cl; // the actual clause bool blocked; // if already blocked, don't need to try again diff --git a/Shell/FunctionDefinitionHandler.hpp b/Shell/FunctionDefinitionHandler.hpp index 5165447ba1..864639a0b3 100644 --- a/Shell/FunctionDefinitionHandler.hpp +++ b/Shell/FunctionDefinitionHandler.hpp @@ -32,7 +32,6 @@ using namespace Lib; * which are not variables in some branch. */ struct InductionTemplate { - USE_ALLOCATOR(InductionTemplate); InductionTemplate() = default; InductionTemplate(const Term* t); @@ -79,7 +78,6 @@ struct InductionTemplate { class FunctionDefinitionHandler { public: - USE_ALLOCATOR(FunctionDefinitionHandler); bool static isHandlerEnabled(const Options& opts) { diff --git a/Shell/LispParser.hpp b/Shell/LispParser.hpp index d74ad11eca..abf5dc9522 100644 --- a/Shell/LispParser.hpp +++ b/Shell/LispParser.hpp @@ -48,7 +48,6 @@ class LispParser /** expressions */ struct Expression { - USE_ALLOCATOR(Expression); /** type of the expression */ Tag tag; diff --git a/Shell/NewCNF.hpp b/Shell/NewCNF.hpp index 3768efb087..bea5f99943 100644 --- a/Shell/NewCNF.hpp +++ b/Shell/NewCNF.hpp @@ -135,7 +135,6 @@ class NewCNF // generalized clause struct GenClause { - USE_ALLOCATOR(NewCNF::GenClause); GenClause(unsigned size, BindingList* bindings, BindingList* foolBindings) : valid(true), bindings(bindings), foolBindings(foolBindings), _literals(size), _size(0) {} @@ -277,7 +276,6 @@ class NewCNF GenClauses _genClauses; struct Occurrence { - USE_ALLOCATOR(NewCNF::Occurrence); SPGenClause gc; unsigned position; @@ -315,7 +313,6 @@ class NewCNF unsigned _size; public: - USE_ALLOCATOR(NewCNF::Occurrences); Occurrences() : _occurrences(nullptr), _size(0) {} diff --git a/Shell/Options.hpp b/Shell/Options.hpp index 9526a2ed88..0bd5d2cffd 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -1778,7 +1778,6 @@ bool _hard; struct NegatedOptionProblemConstraint : OptionProblemConstraint { OptionProblemConstraintUP _inner; - USE_ALLOCATOR(NegatedOptionProblemConstraint); bool check(Property*p){ return !_inner->check(p); @@ -1792,7 +1791,6 @@ bool _hard; struct HasPolymorphism : OptionProblemConstraint{ - USE_ALLOCATOR(HasHigherOrder); bool check(Property*p){ ASS(p)