remove USE_ALLOCATOR where it very likely makes no difference

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.
    */

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;

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)

FMB/FiniteModel.hpp

@@ -35,8 +35,6 @@ using namespace Kernel;
  *
  */
 class FiniteModel {
- USE_ALLOCATOR(FiniteModel);
-
 public:
 
  const unsigned _size;

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;

FMB/FiniteModelMultiSorted.hpp

@@ -35,8 +35,6 @@ using namespace Kernel;
  *
  */
 class FiniteModelMultiSorted {
- USE_ALLOCATOR(FiniteModelMultiSorted);
-
  DHMap<unsigned,unsigned> _sizes;
 
 public:

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

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,

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:

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;

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

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

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

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) 

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

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

Indexing/RequestedIndex.hpp

@@ -23,8 +23,6 @@ template <typename Index>
 class RequestedIndex final
 {
   public:
-    USE_ALLOCATOR(RequestedIndex);
-
     RequestedIndex()
     { }
 

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