Merge pull request #499 from vprover/michael-remove-allocator-macros

remove old allocator macros
vprover · Nov 2, 2023 · 1f706eb · 1f706eb
2 parents d06e09b + f6ce7fa
commit 1f706eb
Show file tree

Hide file tree

Showing 210 changed files with 51 additions and 578 deletions.
diff --git a/Api/Helper_Internal.hpp b/Api/Helper_Internal.hpp
@@ -75,7 +75,6 @@ class FBHelperCore
 : public DefaultHelperCore
 {
 public:
-  CLASS_NAME(FBHelperCore);
   USE_ALLOCATOR(FBHelperCore);
 
   FBHelperCore() : nextVar(0), refCtr(0), varFact(*this), _unaryPredicate(0)

diff --git a/Api/Problem.cpp b/Api/Problem.cpp
@@ -300,7 +300,6 @@ typedef List<AnnotatedFormula> AFList;
 class Problem::PData
 {
 public:
-  CLASS_NAME(Problem::PData);
   USE_ALLOCATOR(Problem::PData);
 
   PData() : _size(0), _forms(0), _refCnt(0)

diff --git a/Api/Problem.hpp b/Api/Problem.hpp
@@ -146,7 +146,6 @@ class Problem
    */
   struct PreprocessingOptions
   {
-    CLASS_NAME(Problem::PreprocessingOptions);
     USE_ALLOCATOR_ARRAY;    
 
     PreprocessingOptions();

diff --git a/CASC/PortfolioMode.cpp b/CASC/PortfolioMode.cpp
@@ -501,9 +501,6 @@ bool PortfolioMode::runScheduleAndRecoverProof(Schedule schedule)
      * the user didn't wish a proof in the file, so we printed it to the secret tmp file
      * now it's time to restore it.
      */
-
-    BYPASSING_ALLOCATOR; 
-
     ifstream input(_tmpFileNameForProof);
 
     bool openSucceeded = !input.fail();
@@ -692,8 +689,6 @@ void PortfolioMode::runSlice(Options& strategyOpt)
       fname = _tmpFileNameForProof;
     }
 
-    BYPASSING_ALLOCATOR; 
-
     ofstream output(fname.c_str());
     if (output.fail()) {
       // fallback to old printing method
@@ -723,7 +718,5 @@ void PortfolioMode::runSlice(Options& strategyOpt)
     _syncSemaphore.inc(SEM_LOCK); // would be also released after the processes' death, but we are polite and do it already here
   }
 
-  STOP_CHECKING_FOR_ALLOCATOR_BYPASSES;
-
   exit(resultValue);
 } // runSlice
diff --git a/CASC/Schedules.cpp b/CASC/Schedules.cpp
@@ -30,7 +30,6 @@ void Schedules::getScheduleFromFile(const vstring& filename, Schedule& quick)
   if (filename == "") {
     USER_ERROR("Schedule file was not set.");
   }
-  BYPASSING_ALLOCATOR;
   ifstream schedule_file (filename.c_str());
   if (schedule_file.fail()) {
     USER_ERROR("Cannot open schedule file: " + filename);

diff --git a/DP/ShortConflictMetaDP.hpp b/DP/ShortConflictMetaDP.hpp
@@ -34,7 +34,6 @@ using namespace SAT;
 
 class ShortConflictMetaDP : public DecisionProcedure {
 public:
-  CLASS_NAME(ShortConflictMetaDP);
   USE_ALLOCATOR(ShortConflictMetaDP);
 
   /**

diff --git a/DP/SimpleCongruenceClosure.hpp b/DP/SimpleCongruenceClosure.hpp
@@ -48,7 +48,6 @@ using namespace Kernel;
 class SimpleCongruenceClosure : public DecisionProcedure
 {
 public:
-  CLASS_NAME(SimpleCongruenceClosure);
   USE_ALLOCATOR(SimpleCongruenceClosure);
 
   SimpleCongruenceClosure(Ordering* ord);

diff --git a/Debug/RuntimeStatistics.hpp b/Debug/RuntimeStatistics.hpp
@@ -94,7 +94,6 @@ class RSObject
 public:
   virtual ~RSObject() {};
 
-  CLASS_NAME(RSObject);
 
   virtual void print(std::ostream& out) = 0;
 

diff --git a/Debug/TimeProfiling.cpp b/Debug/TimeProfiling.cpp
@@ -192,7 +192,6 @@ void TimeTrace::Node::printPrettyRec(std::ostream& out, NodeFormatOpts& opts)
   if (opts.parentDuration.isSome()) {
     out << "[" << setw(2) << percent(total, opts.parentDuration.unwrap()) << "%] ";
   }
-  BYPASSING_ALLOCATOR
   if (opts.nameWidth.isSome()) {
     out << msetw(opts.nameWidth.unwrap()) << left;
   }

diff --git a/Debug/TimeProfiling.hpp b/Debug/TimeProfiling.hpp
@@ -132,7 +132,6 @@ class TimeTrace
 
 
   struct Node {
-    CLASS_NAME(Node)
     USE_ALLOCATOR(Node)
     const char* name;
     Lib::Stack<std::unique_ptr<Node>> children;
@@ -196,7 +195,6 @@ class TimeTraceOrdering : public Kernel::Ordering
   const char* _nameTerm;
   Ord _ord;
 public:
-  CLASS_NAME(TimeTraceOrdering);
   USE_ALLOCATOR(TimeTraceOrdering);
 
   TimeTraceOrdering(const char* nameLit, const char* nameTerm, Ord ord)

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

diff --git a/FMB/FiniteModelBuilder.cpp b/FMB/FiniteModelBuilder.cpp
@@ -132,11 +132,7 @@ FiniteModelBuilder::FiniteModelBuilder(Problem& prb, const Options& opt)
       break;
 #if VZ3
     case Options::FMBEnumerationStrategy::SMT:
-      {
-        BYPASSING_ALLOCATOR;
-
-        _dsaEnumerator = new SmtBasedDSAE();
-      }
+      _dsaEnumerator = new SmtBasedDSAE();
       _xmass = false;
       break;
 #endif
@@ -153,8 +149,6 @@ FiniteModelBuilder::FiniteModelBuilder(Problem& prb, const Options& opt)
 FiniteModelBuilder::~FiniteModelBuilder()
 {
   if(_dsaEnumerator){
-    BYPASSING_ALLOCATOR;
-
     delete _dsaEnumerator;
   }
 }
@@ -2484,8 +2478,6 @@ bool FiniteModelBuilder::SmtBasedDSAE::init(unsigned _startModelSize, DArray<uns
 {
   _skippedSomeSizes = (_startModelSize > 1);
 
-  BYPASSING_ALLOCATOR;
-
   try {
     // initialize the smt solver
     z3::expr zero = _context.int_val(_startModelSize-1);
@@ -2533,8 +2525,6 @@ bool FiniteModelBuilder::SmtBasedDSAE::init(unsigned _startModelSize, DArray<uns
 
 void FiniteModelBuilder::SmtBasedDSAE::learnNogood(Constraint_Generator_Vals& nogood, unsigned weight)
 {
-  BYPASSING_ALLOCATOR;
-
   try {
     z3::expr z3clause = _context.bool_val(false);
     // turning a no-good into a clause
@@ -2595,8 +2585,6 @@ void FiniteModelBuilder::SmtBasedDSAE::reportZ3OutOfMemory()
 
 bool FiniteModelBuilder::SmtBasedDSAE::increaseModelSizes(DArray<unsigned>& newSortSizes, DArray<unsigned>& sortMaxes)
 {
-  BYPASSING_ALLOCATOR;
-
   try {
     TIME_TRACE("smt search for next domain size assignment");
 

diff --git a/FMB/FiniteModelBuilder.hpp b/FMB/FiniteModelBuilder.hpp
@@ -57,7 +57,6 @@ using namespace SAT;
 
 class FiniteModelBuilder : public MainLoop {
 public:
-  CLASS_NAME(FiniteModedlBuilder);
   USE_ALLOCATOR(FiniteModelBuilder);    
 
   FiniteModelBuilder(Problem& prb, const Options& opt);
@@ -252,7 +251,6 @@ class FiniteModelBuilder : public MainLoop {
 
   class HackyDSAE : public DSAEnumerator {
     struct Constraint_Generator {
-      CLASS_NAME(FiniteModedlBuilder::HackyDSAE::Constraint_Generator);
       USE_ALLOCATOR(FiniteModelBuilder::HackyDSAE::Constraint_Generator);
 
       Constraint_Generator_Vals _vals;
@@ -289,7 +287,6 @@ class FiniteModelBuilder : public MainLoop {
     bool checkConstriant(DArray<unsigned>& newSortSizes, Constraint_Generator_Vals& constraint);
 
   public:
-    CLASS_NAME(FiniteModedlBuilder::HackyDSAE);
     USE_ALLOCATOR(FiniteModelBuilder::HackyDSAE);
 
     HackyDSAE(bool keepOldGenerators) : _maxWeightSoFar(0), _keepOldGenerators(keepOldGenerators) {}
@@ -318,7 +315,6 @@ class FiniteModelBuilder : public MainLoop {
     void reportZ3OutOfMemory();
   public:
     // the following is not sufficient, since z3::solver and z3::context allocate internally
-    CLASS_NAME(FiniteModedlBuilder::SmtBasedDSAE);
     USE_ALLOCATOR(FiniteModelBuilder::SmtBasedDSAE);
 
     SmtBasedDSAE() : _smtSolver(_context) {}

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

diff --git a/FMB/Monotonicity.hpp b/FMB/Monotonicity.hpp
@@ -41,7 +41,6 @@ namespace FMB {
 
 class Monotonicity{
 
-  CLASS_NAME(Monotonicity);
   USE_ALLOCATOR(Monotonicity);
 
 public:

diff --git a/FMB/SortInference.hpp b/FMB/SortInference.hpp
@@ -32,7 +32,6 @@ using namespace Shell;
 using namespace Lib;
 
 struct SortedSignature{
-    CLASS_NAME(SortedSignature);
     USE_ALLOCATOR(SortedSignature);
 
     unsigned sorts;
@@ -78,7 +77,6 @@ struct SortedSignature{
 
 class SortInference {
 public:
-  CLASS_NAME(SortInference);
   USE_ALLOCATOR(SortInference);    
 
   SortInference(ClauseList* clauses,

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

diff --git a/Indexing/AcyclicityIndex.hpp b/Indexing/AcyclicityIndex.hpp
@@ -40,7 +40,6 @@ struct CycleQueryResult {
     clausesTheta(c)
   {}
 
-  CLASS_NAME(CycleQueryResult);
   USE_ALLOCATOR(CycleQueryResult);
 
   unsigned totalLengthClauses();
@@ -68,7 +67,6 @@ class AcyclicityIndex
 
   CycleQueryResultsIterator queryCycles(Kernel::Literal *lit, Kernel::Clause *c);
 
-  CLASS_NAME(AcyclicityIndex);
   USE_ALLOCATOR(AcyclicityIndex);
 protected:
   void handleClause(Kernel::Clause* c, bool adding);

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_);
 
-    CLASS_NAME(ClauseCodeTree::RemovingLiteralMatcher);
     USE_ALLOCATOR(RemovingLiteralMatcher);
   };
 
@@ -83,7 +82,6 @@ class ClauseCodeTree : public CodeTree
 
     inline ILStruct* getILS() { ASS(matched()); return op->getILS(); }
 
-    CLASS_NAME(ClauseCodeTree::LiteralMatcher);
     USE_ALLOCATOR(LiteralMatcher);
 
   private:
@@ -105,7 +103,6 @@ class ClauseCodeTree : public CodeTree
     bool matched() { return lms.isNonEmpty() && lms.top()->success(); }
     CodeOp* getSuccessOp() { ASS(matched()); return lms.top()->op; }
 
-    CLASS_NAME(ClauseCodeTree::ClauseMatcher);
     USE_ALLOCATOR(ClauseMatcher);
 
   private:

diff --git a/Indexing/ClauseVariantIndex.hpp b/Indexing/ClauseVariantIndex.hpp
@@ -52,7 +52,6 @@ class ClauseVariantIndex
 class SubstitutionTreeClauseVariantIndex : public ClauseVariantIndex
 {
 public:
-  CLASS_NAME(SubstitutionTreeClauseVariantIndex);
   USE_ALLOCATOR(SubstitutionTreeClauseVariantIndex);
 
   SubstitutionTreeClauseVariantIndex() : _emptyClauses(0) {}
@@ -77,7 +76,6 @@ class SubstitutionTreeClauseVariantIndex : public ClauseVariantIndex
 class HashingClauseVariantIndex : public ClauseVariantIndex
 {
 public:
-  CLASS_NAME(HashingClauseVariantIndex);
   USE_ALLOCATOR(HashingClauseVariantIndex);
 
   virtual ~HashingClauseVariantIndex() override;

diff --git a/Indexing/CodeTree.hpp b/Indexing/CodeTree.hpp
@@ -117,7 +117,6 @@ class CodeTree
 
     void ensureFreshness(unsigned globalTimestamp);
 
-    CLASS_NAME(CodeTree::ILStruct);
     USE_ALLOCATOR(ILStruct);
 
     struct GVArrComparator;
@@ -293,7 +292,6 @@ class CodeTree
     ~FnSearchStruct();
     CodeOp*& targetOp(unsigned fn);
 
-    CLASS_NAME(CodeTree::FnSearchStruct);
     USE_ALLOCATOR(FnSearchStruct);
 
     struct OpComparator;
@@ -308,7 +306,6 @@ class CodeTree
     ~GroundTermSearchStruct();
     CodeOp*& targetOp(const Term* trm);
 
-    CLASS_NAME(CodeTree::GroundTermSearchStruct);
     USE_ALLOCATOR(GroundTermSearchStruct);
 
     struct OpComparator;

diff --git a/Indexing/CodeTreeInterfaces.cpp b/Indexing/CodeTreeInterfaces.cpp
@@ -48,7 +48,6 @@ class CodeTreeSubstitution
     }
   }
 
-  CLASS_NAME(CodeTreeSubstitution);
   USE_ALLOCATOR(CodeTreeSubstitution);
 
   TermList applyToBoundResult(TermList t) override
@@ -79,7 +78,6 @@ class CodeTreeSubstitution
       return res;
     }
 
-    CLASS_NAME(CodeTreeSubstitution::Applicator);
     USE_ALLOCATOR(Applicator);
   private:
     CodeTree::BindingArray* _bindings;
@@ -127,7 +125,6 @@ class CodeTreeTIS::ResultIterator
     }
   }
 
-  CLASS_NAME(CodeTreeTIS::ResultIterator);
   USE_ALLOCATOR(ResultIterator);
 
   bool hasNext()

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

diff --git a/Indexing/GroundingIndex.hpp b/Indexing/GroundingIndex.hpp
@@ -31,7 +31,6 @@ using namespace Shell;
 
 class GroundingIndex : public Index {
 public:
-  CLASS_NAME(GroundingIndex);
   USE_ALLOCATOR(GroundingIndex);
 
   GroundingIndex(const Options& opt);

diff --git a/Indexing/Index.hpp b/Indexing/Index.hpp
@@ -129,7 +129,6 @@ typedef VirtualIterator<FormulaQueryResult> FormulaQueryResultIterator;
 class Index
 {
 public:
-  CLASS_NAME(Index);
   USE_ALLOCATOR(Index);
 
   virtual ~Index();
@@ -158,7 +157,6 @@ class ClauseSubsumptionIndex
 : public Index
 {
 public:
-  CLASS_NAME(ClauseSubsumptionIndex);
   USE_ALLOCATOR(ClauseSubsumptionIndex);
 
   virtual ClauseSResResultIterator getSubsumingOrSResolvingClauses(Clause* c, 

diff --git a/Indexing/IndexManager.hpp b/Indexing/IndexManager.hpp
@@ -72,7 +72,6 @@ enum IndexType {
 class IndexManager
 {
 public:
-  CLASS_NAME(IndexManager);
   USE_ALLOCATOR(IndexManager);
 
   /** alg can be zero, then it must be set by setSaturationAlgorithm */
-Original file line number
+Diff line change
@@ Expand Up / @@ -34,7 +34,6 @@ using namespace SAT; @@
     class ShortConflictMetaDP : public DecisionProcedure {
     public:
-      CLASS_NAME(ShortConflictMetaDP);
       USE_ALLOCATOR(ShortConflictMetaDP);
       /**
@@ Expand Down @@