remove CLASS_NAME, no-op

vprover · Oct 31, 2023 · a440309 · a440309
1 parent d06e09b
commit a440309
Show file tree

Hide file tree

Showing 188 changed files with 0 additions and 364 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/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.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.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 */

diff --git a/Indexing/LiteralIndex.hpp b/Indexing/LiteralIndex.hpp
@@ -27,7 +27,6 @@ class LiteralIndex
 : public Index
 {
 public:
-  CLASS_NAME(LiteralIndex);
   USE_ALLOCATOR(LiteralIndex);
 
   virtual ~LiteralIndex();
@@ -61,7 +60,6 @@ class BinaryResolutionIndex
 : public LiteralIndex
 {
 public:
-  CLASS_NAME(BinaryResolutionIndex);
   USE_ALLOCATOR(BinaryResolutionIndex);
 
   BinaryResolutionIndex(LiteralIndexingStructure* is)
@@ -74,7 +72,6 @@ class BackwardSubsumptionIndex
 : public LiteralIndex
 {
 public:
-  CLASS_NAME(BackwardSubsumptionIndex);
   USE_ALLOCATOR(BackwardSubsumptionIndex);
 
   BackwardSubsumptionIndex(LiteralIndexingStructure* is)
@@ -87,7 +84,6 @@ class FwSubsSimplifyingLiteralIndex
 : public LiteralIndex
 {
 public:
-  CLASS_NAME(FwSubsSimplifyingLiteralIndex);
   USE_ALLOCATOR(FwSubsSimplifyingLiteralIndex);
 
   FwSubsSimplifyingLiteralIndex(LiteralIndexingStructure* is)
@@ -102,7 +98,6 @@ class FSDLiteralIndex
 : public LiteralIndex
 {
 public:
-  CLASS_NAME(FSDLiteralIndex);
   USE_ALLOCATOR(FSDLiteralIndex);
 
   FSDLiteralIndex(LiteralIndexingStructure* is)
@@ -117,7 +112,6 @@ class UnitClauseLiteralIndex
 : public LiteralIndex
 {
 public:
-  CLASS_NAME(UnitClauseLiteralIndex);
   USE_ALLOCATOR(UnitClauseLiteralIndex);
 
   UnitClauseLiteralIndex(LiteralIndexingStructure* is)
@@ -130,7 +124,6 @@ class UnitClauseWithALLiteralIndex
 : public LiteralIndex
 {
 public:
-  CLASS_NAME(UnitClauseWithALLiteralIndex);
   USE_ALLOCATOR(UnitClauseWithALLiteralIndex);
 
   UnitClauseWithALLiteralIndex(LiteralIndexingStructure* is)
@@ -143,7 +136,6 @@ class NonUnitClauseLiteralIndex
 : public LiteralIndex
 {
 public:
-  CLASS_NAME(NonUnitClauseLiteralIndex);
   USE_ALLOCATOR(NonUnitClauseLiteralIndex);
 
   NonUnitClauseLiteralIndex(LiteralIndexingStructure* is, bool selectedOnly=false)
@@ -158,7 +150,6 @@ class NonUnitClauseWithALLiteralIndex
 : public LiteralIndex
 {
 public:
-  CLASS_NAME(NonUnitClauseWithALLiteralIndex);
   USE_ALLOCATOR(NonUnitClauseWithALLiteralIndex);
 
   NonUnitClauseWithALLiteralIndex(LiteralIndexingStructure* is, bool selectedOnly=false)
@@ -173,7 +164,6 @@ class RewriteRuleIndex
 : public LiteralIndex
 {
 public:
-  CLASS_NAME(RewriteRuleIndex);
   USE_ALLOCATOR(RewriteRuleIndex);
 
   RewriteRuleIndex(LiteralIndexingStructure* is, Ordering& ordering);
@@ -198,7 +188,6 @@ class DismatchingLiteralIndex
 : public LiteralIndex
 {
 public:
-  CLASS_NAME(DismatchingLiteralIndex);
   USE_ALLOCATOR(DismatchingLiteralIndex);
 
   DismatchingLiteralIndex(LiteralIndexingStructure* is)
@@ -211,7 +200,6 @@ class UnitIntegerComparisonLiteralIndex
 : public LiteralIndex
 {
 public:
-  CLASS_NAME(UnitIntegerComparisonLiteralIndex);
   USE_ALLOCATOR(UnitIntegerComparisonLiteralIndex);
 
   UnitIntegerComparisonLiteralIndex(LiteralIndexingStructure* is)
-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 @@