Merge pull request #506 from vprover/michael-judicious-allocation1

remove USE_ALLOCATOR where it very likely makes no difference
vprover · Dec 6, 2023 · 6561205 · 6561205
2 parents c6b72c3 + 42dac07
commit 6561205
Show file tree

Hide file tree

Showing 136 changed files with 1 addition and 514 deletions.
diff --git a/DP/ShortConflictMetaDP.hpp b/DP/ShortConflictMetaDP.hpp
@@ -34,8 +34,6 @@ using namespace SAT;
 
 class ShortConflictMetaDP : public DecisionProcedure {
 public:
-  USE_ALLOCATOR(ShortConflictMetaDP);
-
   /**
    * Create object using @c inner decision procedure. Object takes ownership of the @c inner object.
    */

diff --git a/DP/SimpleCongruenceClosure.hpp b/DP/SimpleCongruenceClosure.hpp
@@ -48,8 +48,6 @@ using namespace Kernel;
 class SimpleCongruenceClosure : public DecisionProcedure
 {
 public:
-  USE_ALLOCATOR(SimpleCongruenceClosure);
-
   SimpleCongruenceClosure(Ordering* ord);
 
   virtual void addLiterals(LiteralIterator lits, bool onlyEqualites) override;

diff --git a/Debug/TimeProfiling.hpp b/Debug/TimeProfiling.hpp
@@ -195,8 +195,6 @@ class TimeTraceOrdering : public Kernel::Ordering
   const char* _nameTerm;
   Ord _ord;
 public:
-  USE_ALLOCATOR(TimeTraceOrdering);
-
   TimeTraceOrdering(const char* nameLit, const char* nameTerm, Ord ord)
   : _nameLit(nameLit)
   , _nameTerm(nameTerm)

diff --git a/FMB/FiniteModel.hpp b/FMB/FiniteModel.hpp
@@ -35,8 +35,6 @@ using namespace Kernel;
  *
  */
 class FiniteModel {
- USE_ALLOCATOR(FiniteModel);
-
 public:
 
  const unsigned _size;

diff --git a/FMB/FiniteModelBuilder.hpp b/FMB/FiniteModelBuilder.hpp
@@ -57,8 +57,6 @@ using namespace SAT;
 
 class FiniteModelBuilder : public MainLoop {
 public:
-  USE_ALLOCATOR(FiniteModelBuilder);    
-
   FiniteModelBuilder(Problem& prb, const Options& opt);
   ~FiniteModelBuilder();
 
@@ -251,8 +249,6 @@ class FiniteModelBuilder : public MainLoop {
 
   class HackyDSAE : public DSAEnumerator {
     struct Constraint_Generator {
-      USE_ALLOCATOR(FiniteModelBuilder::HackyDSAE::Constraint_Generator);
-
       Constraint_Generator_Vals _vals;
       unsigned _weight;
 
@@ -287,8 +283,6 @@ class FiniteModelBuilder : public MainLoop {
     bool checkConstriant(DArray<unsigned>& newSortSizes, Constraint_Generator_Vals& constraint);
 
   public:
-    USE_ALLOCATOR(FiniteModelBuilder::HackyDSAE);
-
     HackyDSAE(bool keepOldGenerators) : _maxWeightSoFar(0), _keepOldGenerators(keepOldGenerators) {}
 
     bool init(unsigned _startSize, DArray<unsigned>&, Stack<std::pair<unsigned,unsigned>>& dsc, Stack<std::pair<unsigned,unsigned>>& sdsc) override {
@@ -314,9 +308,6 @@ class FiniteModelBuilder : public MainLoop {
     unsigned loadSizesFromSmt(DArray<unsigned>& szs);
     void reportZ3OutOfMemory();
   public:
-    // the following is not sufficient, since z3::solver and z3::context allocate internally
-    USE_ALLOCATOR(FiniteModelBuilder::SmtBasedDSAE);
-
     SmtBasedDSAE() : _smtSolver(_context) {}
 
     bool init(unsigned, DArray<unsigned>&, Stack<std::pair<unsigned,unsigned>>&, Stack<std::pair<unsigned,unsigned>>&) override;

diff --git a/FMB/FiniteModelMultiSorted.hpp b/FMB/FiniteModelMultiSorted.hpp
@@ -35,8 +35,6 @@ using namespace Kernel;
  *
  */
 class FiniteModelMultiSorted {
- USE_ALLOCATOR(FiniteModelMultiSorted);
-
  DHMap<unsigned,unsigned> _sizes;
 
 public:

diff --git a/FMB/Monotonicity.hpp b/FMB/Monotonicity.hpp
@@ -40,9 +40,6 @@ namespace FMB {
   using namespace Lib;
 
 class Monotonicity{
-
-  USE_ALLOCATOR(Monotonicity);
-
 public:
   // Assumes clauses are flattened
   Monotonicity(ClauseList* clauses, unsigned srt);

diff --git a/FMB/SortInference.hpp b/FMB/SortInference.hpp
@@ -32,8 +32,6 @@ using namespace Shell;
 using namespace Lib;
 
 struct SortedSignature{
-    USE_ALLOCATOR(SortedSignature);
-
     unsigned sorts;
     DArray<Stack<unsigned>> sortedConstants;
     DArray<Stack<unsigned>> sortedFunctions;
@@ -77,8 +75,6 @@ struct SortedSignature{
 
 class SortInference {
 public:
-  USE_ALLOCATOR(SortInference);    
-
   SortInference(ClauseList* clauses,
                 DArray<unsigned> del_f,
                 DArray<unsigned> del_p,

diff --git a/Indexing/AcyclicityIndex.hpp b/Indexing/AcyclicityIndex.hpp
@@ -66,8 +66,6 @@ class AcyclicityIndex
   void remove(Kernel::Literal *lit, Kernel::Clause *c);
 
   CycleQueryResultsIterator queryCycles(Kernel::Literal *lit, Kernel::Clause *c);
-
-  USE_ALLOCATOR(AcyclicityIndex);
 protected:
   void handleClause(Kernel::Clause* c, bool adding);
 private:

diff --git a/Indexing/ClauseVariantIndex.hpp b/Indexing/ClauseVariantIndex.hpp
@@ -52,8 +52,6 @@ class ClauseVariantIndex
 class SubstitutionTreeClauseVariantIndex : public ClauseVariantIndex
 {
 public:
-  USE_ALLOCATOR(SubstitutionTreeClauseVariantIndex);
-
   SubstitutionTreeClauseVariantIndex() : _emptyClauses(0) {}
   virtual ~SubstitutionTreeClauseVariantIndex() override;
 
@@ -76,8 +74,6 @@ class SubstitutionTreeClauseVariantIndex : public ClauseVariantIndex
 class HashingClauseVariantIndex : public ClauseVariantIndex
 {
 public:
-  USE_ALLOCATOR(HashingClauseVariantIndex);
-
   virtual ~HashingClauseVariantIndex() override;
 
   virtual void insert(Clause* cl) override;

diff --git a/Indexing/CodeTreeInterfaces.hpp b/Indexing/CodeTreeInterfaces.hpp
@@ -40,8 +40,6 @@ using namespace Lib;
 class CodeTreeTIS : public TermIndexingStructure
 {
 public:
-  USE_ALLOCATOR(CodeTreeTIS);
-
   void insert(TypedTermList t, Literal* lit, Clause* cls);
   void remove(TypedTermList t, Literal* lit, Clause* cls);
 
@@ -78,8 +76,6 @@ class CodeTreeSubsumptionIndex
 : public ClauseSubsumptionIndex
 {
 public:
-  USE_ALLOCATOR(CodeTreeSubsumptionIndex);
-
   ClauseSResResultIterator getSubsumingOrSResolvingClauses(Clause* c, bool subsumptionResolution);
 protected:
   //overrides Index::handleClause

diff --git a/Indexing/GroundingIndex.hpp b/Indexing/GroundingIndex.hpp
@@ -31,8 +31,6 @@ using namespace Shell;
 
 class GroundingIndex : public Index {
 public:
-  USE_ALLOCATOR(GroundingIndex);
-
   GroundingIndex(const Options& opt);
 
   SATSolverWithAssumptions& getSolver() { return *_solver; }

diff --git a/Indexing/Index.hpp b/Indexing/Index.hpp
@@ -129,8 +129,6 @@ typedef VirtualIterator<FormulaQueryResult> FormulaQueryResultIterator;
 class Index
 {
 public:
-  USE_ALLOCATOR(Index);
-
   virtual ~Index();
 
   void attachContainer(ClauseContainer* cc);
@@ -157,8 +155,6 @@ class ClauseSubsumptionIndex
 : public Index
 {
 public:
-  USE_ALLOCATOR(ClauseSubsumptionIndex);
-
   virtual ClauseSResResultIterator getSubsumingOrSResolvingClauses(Clause* c, 
     bool subsumptionResolution)
   { NOT_IMPLEMENTED; };

diff --git a/Indexing/IndexManager.hpp b/Indexing/IndexManager.hpp
@@ -72,8 +72,6 @@ enum IndexType {
 class IndexManager
 {
 public:
-  USE_ALLOCATOR(IndexManager);
-
   /** alg can be zero, then it must be set by setSaturationAlgorithm */
   explicit IndexManager(SaturationAlgorithm* alg) : _alg(alg) {}
   void setSaturationAlgorithm(SaturationAlgorithm* alg) 

diff --git a/Indexing/LiteralIndex.hpp b/Indexing/LiteralIndex.hpp
@@ -27,8 +27,6 @@ class LiteralIndex
 : public Index
 {
 public:
-  USE_ALLOCATOR(LiteralIndex);
-
   virtual ~LiteralIndex();
 
   SLQueryResultIterator getAll();
@@ -60,8 +58,6 @@ class BinaryResolutionIndex
 : public LiteralIndex
 {
 public:
-  USE_ALLOCATOR(BinaryResolutionIndex);
-
   BinaryResolutionIndex(LiteralIndexingStructure* is)
   : LiteralIndex(is) {};
 protected:
@@ -72,8 +68,6 @@ class BackwardSubsumptionIndex
 : public LiteralIndex
 {
 public:
-  USE_ALLOCATOR(BackwardSubsumptionIndex);
-
   BackwardSubsumptionIndex(LiteralIndexingStructure* is)
   : LiteralIndex(is) {};
 protected:
@@ -84,8 +78,6 @@ class FwSubsSimplifyingLiteralIndex
 : public LiteralIndex
 {
 public:
-  USE_ALLOCATOR(FwSubsSimplifyingLiteralIndex);
-
   FwSubsSimplifyingLiteralIndex(LiteralIndexingStructure* is)
     : LiteralIndex(is)
   { }
@@ -98,8 +90,6 @@ class FSDLiteralIndex
 : public LiteralIndex
 {
 public:
-  USE_ALLOCATOR(FSDLiteralIndex);
-
   FSDLiteralIndex(LiteralIndexingStructure* is)
     : LiteralIndex(is)
   { }
@@ -112,8 +102,6 @@ class UnitClauseLiteralIndex
 : public LiteralIndex
 {
 public:
-  USE_ALLOCATOR(UnitClauseLiteralIndex);
-
   UnitClauseLiteralIndex(LiteralIndexingStructure* is)
   : LiteralIndex(is) {};
 protected:
@@ -124,8 +112,6 @@ class UnitClauseWithALLiteralIndex
 : public LiteralIndex
 {
 public:
-  USE_ALLOCATOR(UnitClauseWithALLiteralIndex);
-
   UnitClauseWithALLiteralIndex(LiteralIndexingStructure* is)
   : LiteralIndex(is) {};
 protected:
@@ -136,8 +122,6 @@ class NonUnitClauseLiteralIndex
 : public LiteralIndex
 {
 public:
-  USE_ALLOCATOR(NonUnitClauseLiteralIndex);
-
   NonUnitClauseLiteralIndex(LiteralIndexingStructure* is, bool selectedOnly=false)
   : LiteralIndex(is), _selectedOnly(selectedOnly) {};
 protected:
@@ -150,8 +134,6 @@ class NonUnitClauseWithALLiteralIndex
 : public LiteralIndex
 {
 public:
-  USE_ALLOCATOR(NonUnitClauseWithALLiteralIndex);
-
   NonUnitClauseWithALLiteralIndex(LiteralIndexingStructure* is, bool selectedOnly=false)
   : LiteralIndex(is), _selectedOnly(selectedOnly) {};
 protected:
@@ -164,8 +146,6 @@ class RewriteRuleIndex
 : public LiteralIndex
 {
 public:
-  USE_ALLOCATOR(RewriteRuleIndex);
-
   RewriteRuleIndex(LiteralIndexingStructure* is, Ordering& ordering);
   ~RewriteRuleIndex();
 
@@ -188,8 +168,6 @@ class DismatchingLiteralIndex
 : public LiteralIndex
 {
 public:
-  USE_ALLOCATOR(DismatchingLiteralIndex);
-
   DismatchingLiteralIndex(LiteralIndexingStructure* is)
   : LiteralIndex(is) {};
   void handleClause(Clause* c, bool adding);
@@ -200,8 +178,6 @@ class UnitIntegerComparisonLiteralIndex
 : public LiteralIndex
 {
 public:
-  USE_ALLOCATOR(UnitIntegerComparisonLiteralIndex);
-
   UnitIntegerComparisonLiteralIndex(LiteralIndexingStructure* is)
   : LiteralIndex(is) {}
 

diff --git a/Indexing/LiteralSubstitutionTree.hpp b/Indexing/LiteralSubstitutionTree.hpp
@@ -36,8 +36,6 @@ class LiteralSubstitutionTree
   using Leaf = SubstitutionTree::Leaf;
 
 public:
-  USE_ALLOCATOR(LiteralSubstitutionTree);
-
   LiteralSubstitutionTree(bool useC=false);
 
   void insert(Literal* lit, Clause* cls) override { handleLiteral(lit, cls, /* insert */ true); }

diff --git a/Indexing/RequestedIndex.hpp b/Indexing/RequestedIndex.hpp
@@ -23,8 +23,6 @@ template <typename Index>
 class RequestedIndex final
 {
   public:
-    USE_ALLOCATOR(RequestedIndex);
-
     RequestedIndex()
     { }
 

diff --git a/Indexing/SubstitutionTree.hpp b/Indexing/SubstitutionTree.hpp
@@ -119,7 +119,6 @@ class SubstitutionTree
 public:
   static constexpr int QRS_QUERY_BANK = 0;
   static constexpr int QRS_RESULT_BANK = 1;
-  USE_ALLOCATOR(SubstitutionTree);
 
   SubstitutionTree(bool useC, bool rfSubs);