remove old allocator macros

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)

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)

Api/Problem.hpp

@@ -146,7 +146,6 @@ class Problem
    */
   struct PreprocessingOptions
   {
-    CLASS_NAME(Problem::PreprocessingOptions);
     USE_ALLOCATOR_ARRAY;    
 
     PreprocessingOptions();

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

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

DP/ShortConflictMetaDP.hpp

@@ -34,7 +34,6 @@ using namespace SAT;
 
 class ShortConflictMetaDP : public DecisionProcedure {
 public:
-  CLASS_NAME(ShortConflictMetaDP);
   USE_ALLOCATOR(ShortConflictMetaDP);
 
   /**

DP/SimpleCongruenceClosure.hpp

@@ -48,7 +48,6 @@ using namespace Kernel;
 class SimpleCongruenceClosure : public DecisionProcedure
 {
 public:
-  CLASS_NAME(SimpleCongruenceClosure);
   USE_ALLOCATOR(SimpleCongruenceClosure);
 
   SimpleCongruenceClosure(Ordering* ord);

Debug/RuntimeStatistics.hpp

@@ -94,7 +94,6 @@ class RSObject
 public:
   virtual ~RSObject() {};
 
-  CLASS_NAME(RSObject);
 
   virtual void print(std::ostream& out) = 0;
 

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

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)

FMB/FiniteModel.hpp

@@ -35,7 +35,6 @@ using namespace Kernel;
  *
  */
 class FiniteModel {
- CLASS_NAME(FiniteModel);
  USE_ALLOCATOR(FiniteModel);
 
 public:

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

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

FMB/FiniteModelMultiSorted.hpp

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

FMB/Monotonicity.hpp

@@ -41,7 +41,6 @@ namespace FMB {
 
 class Monotonicity{
 
-  CLASS_NAME(Monotonicity);
   USE_ALLOCATOR(Monotonicity);
 
 public:

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,

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;

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

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:

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;

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;

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

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

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

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, 

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