From a440309cdaf18df499283ca1ffab2ef45bd1e3a6 Mon Sep 17 00:00:00 2001 From: Michael Rawson Date: Tue, 31 Oct 2023 12:24:39 +0000 Subject: [PATCH] remove CLASS_NAME, no-op --- Api/Helper_Internal.hpp | 1 - Api/Problem.cpp | 1 - Api/Problem.hpp | 1 - DP/ShortConflictMetaDP.hpp | 1 - DP/SimpleCongruenceClosure.hpp | 1 - Debug/RuntimeStatistics.hpp | 1 - Debug/TimeProfiling.hpp | 2 -- FMB/FiniteModel.hpp | 1 - FMB/FiniteModelBuilder.hpp | 4 --- FMB/FiniteModelMultiSorted.hpp | 1 - FMB/Monotonicity.hpp | 1 - FMB/SortInference.hpp | 2 -- Indexing/AcyclicityIndex.cpp | 2 -- Indexing/AcyclicityIndex.hpp | 2 -- Indexing/ClauseCodeTree.hpp | 3 -- Indexing/ClauseVariantIndex.hpp | 2 -- Indexing/CodeTree.hpp | 3 -- Indexing/CodeTreeInterfaces.cpp | 3 -- Indexing/CodeTreeInterfaces.hpp | 2 -- Indexing/GroundingIndex.hpp | 1 - Indexing/Index.hpp | 2 -- Indexing/IndexManager.hpp | 1 - Indexing/LiteralIndex.hpp | 12 ------- Indexing/LiteralMiniIndex.hpp | 1 - Indexing/LiteralSubstitutionTree.hpp | 1 - Indexing/RequestedIndex.hpp | 1 - Indexing/ResultSubstitution.cpp | 1 - Indexing/SubstitutionTree.hpp | 6 ---- Indexing/SubstitutionTree_FastGen.cpp | 2 -- Indexing/SubstitutionTree_FastInst.cpp | 1 - Indexing/SubstitutionTree_Nodes.cpp | 2 -- Indexing/TermCodeTree.hpp | 2 -- Indexing/TermIndex.hpp | 14 -------- Indexing/TermSharing.hpp | 1 - Indexing/TermSubstitutionTree.hpp | 1 - Inferences/ArgCong.hpp | 1 - .../ArithmeticSubtermGeneralization.hpp | 4 --- Inferences/ArrayTheoryISE.hpp | 1 - Inferences/BackwardDemodulation.hpp | 1 - .../BackwardSubsumptionDemodulation.hpp | 1 - Inferences/BackwardSubsumptionResolution.hpp | 1 - Inferences/BinaryResolution.hpp | 1 - Inferences/BoolEqToDiseq.hpp | 1 - Inferences/BoolSimp.hpp | 1 - Inferences/CNFOnTheFly.hpp | 9 ----- Inferences/Cancellation.hpp | 1 - Inferences/Cases.hpp | 1 - Inferences/CasesSimp.hpp | 1 - Inferences/Choice.hpp | 1 - Inferences/CombinatorDemodISE.hpp | 1 - Inferences/CombinatorNormalisationISE.hpp | 1 - Inferences/Condensation.hpp | 1 - Inferences/DefinitionIntroduction.hpp | 1 - Inferences/DistinctEqualitySimplifier.hpp | 1 - Inferences/ElimLeibniz.hpp | 1 - Inferences/EqualityFactoring.hpp | 1 - Inferences/EqualityResolution.hpp | 1 - Inferences/EquationalTautologyRemoval.hpp | 1 - Inferences/ExtensionalityResolution.hpp | 1 - Inferences/FOOLParamodulation.hpp | 1 - Inferences/Factoring.hpp | 1 - Inferences/FastCondensation.hpp | 1 - Inferences/ForwardDemodulation.hpp | 2 -- Inferences/ForwardLiteralRewriting.hpp | 1 - .../ForwardSubsumptionAndResolution.cpp | 1 - .../ForwardSubsumptionAndResolution.hpp | 1 - Inferences/ForwardSubsumptionDemodulation.hpp | 1 - Inferences/GaussianVariableElimination.hpp | 1 - Inferences/GlobalSubsumption.hpp | 1 - Inferences/Induction.hpp | 2 -- Inferences/InductionHelper.hpp | 1 - Inferences/InferenceEngine.hpp | 10 ------ Inferences/Injectivity.hpp | 1 - Inferences/InnerRewriting.hpp | 1 - Inferences/Instantiation.hpp | 1 - Inferences/InterpretedEvaluation.hpp | 1 - Inferences/InvalidAnswerLiteralRemoval.hpp | 1 - Inferences/LfpRule.hpp | 1 - Inferences/Narrow.hpp | 1 - Inferences/NegativeExt.hpp | 1 - Inferences/PolynomialEvaluation.hpp | 1 - Inferences/PrimitiveInstantiation.hpp | 1 - Inferences/PushUnaryMinus.hpp | 1 - Inferences/RenamingOnTheFly.hpp | 1 - Inferences/SLQueryBackwardSubsumption.hpp | 1 - Inferences/SubVarSup.hpp | 1 - Inferences/SubsumptionDemodulationHelper.hpp | 2 -- Inferences/Superposition.hpp | 1 - Inferences/TautologyDeletionISE.hpp | 1 - Inferences/TermAlgebraReasoning.hpp | 6 ---- Inferences/TheoryInstAndSimp.hpp | 1 - Inferences/URResolution.cpp | 1 - Inferences/URResolution.hpp | 1 - Kernel/BestLiteralSelector.hpp | 2 -- Kernel/ELiteralSelector.hpp | 1 - Kernel/Formula.hpp | 8 ----- Kernel/FormulaUnit.hpp | 1 - Kernel/Grounder.hpp | 3 -- Kernel/Inference.cpp | 1 - Kernel/Inference.hpp | 1 - Kernel/InferenceStore.cpp | 4 --- Kernel/InferenceStore.hpp | 1 - Kernel/InterpretedLiteralEvaluator.cpp | 2 -- Kernel/InterpretedLiteralEvaluator.hpp | 1 - Kernel/KBO.cpp | 1 - Kernel/KBO.hpp | 1 - Kernel/KBOForEPR.hpp | 1 - Kernel/LPO.hpp | 1 - Kernel/LiteralSelector.hpp | 2 -- Kernel/LookaheadLiteralSelector.hpp | 1 - Kernel/MLMatcher.cpp | 1 - Kernel/MLMatcherSD.cpp | 1 - Kernel/MainLoop.hpp | 1 - Kernel/Matcher.hpp | 1 - Kernel/MaximalLiteralSelector.hpp | 1 - Kernel/MismatchHandler.hpp | 2 -- Kernel/OperatorType.hpp | 1 - Kernel/Ordering.hpp | 1 - Kernel/Ordering_Equality.cpp | 1 - Kernel/Polynomial.hpp | 6 ---- Kernel/Problem.hpp | 1 - Kernel/Renaming.hpp | 1 - Kernel/RndLiteralSelector.hpp | 1 - Kernel/RobSubstitution.hpp | 2 -- Kernel/SKIKBO.cpp | 1 - Kernel/SKIKBO.hpp | 1 - Kernel/Signature.hpp | 6 ---- Kernel/SpassLiteralSelector.hpp | 1 - Kernel/SubformulaIterator.cpp | 1 - Kernel/Substitution.hpp | 1 - Kernel/Term.hpp | 1 - Kernel/Theory.hpp | 3 -- Kernel/TypedTermList.hpp | 1 - Lib/Allocator.hpp | 1 - Lib/ArrayMap.hpp | 1 - Lib/BinaryHeap.hpp | 2 -- Lib/Coproduct.hpp | 3 -- Lib/DArray.hpp | 1 - Lib/DHMap.hpp | 1 - Lib/DHMultiset.hpp | 1 - Lib/DHSet.hpp | 1 - Lib/Event.hpp | 4 --- Lib/InverseLookup.hpp | 1 - Lib/List.hpp | 6 ---- Lib/Set.hpp | 1 - Lib/SkipList.hpp | 1 - Lib/SmartPtr.hpp | 1 - Lib/Stack.hpp | 2 -- Lib/Timer.hpp | 1 - Lib/VString.hpp | 3 -- Lib/VirtualIterator.hpp | 5 --- Parse/TPTP.hpp | 5 --- SAT/BufferedSolver.hpp | 1 - SAT/FallbackSolverWrapper.hpp | 1 - SAT/MinimizingSolver.hpp | 1 - SAT/MinisatInterfacing.hpp | 1 - SAT/MinisatInterfacingNewSimp.hpp | 1 - SAT/SATInference.hpp | 3 -- SAT/Z3Interfacing.hpp | 1 - SAT/Z3MainLoop.hpp | 1 - Saturation/AWPassiveClauseContainer.hpp | 1 - Saturation/ClauseContainer.hpp | 6 ---- Saturation/ConsequenceFinder.hpp | 1 - Saturation/Discount.hpp | 1 - Saturation/ExtensionalityClauseContainer.hpp | 1 - Saturation/LRS.hpp | 1 - Saturation/LabelFinder.hpp | 1 - Saturation/ManCSPassiveClauseContainer.cpp | 1 - Saturation/ManCSPassiveClauseContainer.hpp | 1 - Saturation/Otter.hpp | 1 - .../PredicateSplitPassiveClauseContainer.hpp | 1 - Saturation/SaturationAlgorithm.hpp | 1 - Saturation/Splitter.hpp | 2 -- Saturation/SymElOutput.hpp | 1 - Shell/BlockedClauseElimination.hpp | 2 -- Shell/EqualityProxy.hpp | 1 - Shell/EqualityProxyMono.hpp | 1 - Shell/FunctionDefinition.cpp | 1 - Shell/GoalGuessing.hpp | 1 - Shell/InterpretedNormalizer.cpp | 5 --- Shell/LispParser.hpp | 1 - Shell/NewCNF.hpp | 3 -- Shell/Options.hpp | 34 ------------------- Shell/PredicateDefinition.cpp | 1 - Shell/Property.hpp | 1 - Shell/Statistics.hpp | 1 - Shell/SubexpressionIterator.hpp | 1 - Shell/TermAlgebra.hpp | 2 -- 188 files changed, 364 deletions(-) diff --git a/Api/Helper_Internal.hpp b/Api/Helper_Internal.hpp index 5c7123ba9..180820b29 100644 --- 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 index 5ec703a76..ea41bc5ba 100644 --- a/Api/Problem.cpp +++ b/Api/Problem.cpp @@ -300,7 +300,6 @@ typedef List 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 index 6e6a39682..7e3f27699 100644 --- 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 index caff1ae6e..cd8976904 100644 --- 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 index b0e4ee453..13f9b7886 100644 --- 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 index 35689e05e..0f87e9ff9 100644 --- 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 index b67c4e61c..800886e31 100644 --- 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> 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 index 6788bf793..dad5d85dc 100644 --- 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 index c0b435b84..90000e7ab 100644 --- 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& 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 index 4339eb857..ccae8e86e 100644 --- a/FMB/FiniteModelMultiSorted.hpp +++ b/FMB/FiniteModelMultiSorted.hpp @@ -35,7 +35,6 @@ using namespace Kernel; * */ class FiniteModelMultiSorted { - CLASS_NAME(FiniteModelMultiSorted); USE_ALLOCATOR(FiniteModelMultiSorted); DHMap _sizes; diff --git a/FMB/Monotonicity.hpp b/FMB/Monotonicity.hpp index 93eed5e73..7cc8bdb22 100644 --- 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 index 02ada6d1b..4e70f4b13 100644 --- 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 index 8b1b330e9..31b9bbae2 100644 --- 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 index 3d24a19ef..8e5bffe3b 100644 --- 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 index 5faf86c63..cf2603906 100644 --- 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* 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 index 3872ff84e..9d591a98f 100644 --- 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 index 18868c0ab..6bc2e865e 100644 --- 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 index 4c3b26c0a..a5afc7770 100644 --- 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 index 8b62d0b8f..7acb9f071 100644 --- 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 index 08c352d8c..1b55e8d69 100644 --- 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 index d991dbabe..572038dc3 100644 --- a/Indexing/Index.hpp +++ b/Indexing/Index.hpp @@ -129,7 +129,6 @@ typedef VirtualIterator 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 index 2036eb5e3..df00bfd3f 100644 --- 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 index 34cdbc37d..122afeef5 100644 --- 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) diff --git a/Indexing/LiteralMiniIndex.hpp b/Indexing/LiteralMiniIndex.hpp index ecdb69162..95a8b1e85 100644 --- a/Indexing/LiteralMiniIndex.hpp +++ b/Indexing/LiteralMiniIndex.hpp @@ -30,7 +30,6 @@ using namespace Kernel; class LiteralMiniIndex { public: - CLASS_NAME(LiteralMiniIndex); USE_ALLOCATOR(LiteralMiniIndex); LiteralMiniIndex(Clause* cl); diff --git a/Indexing/LiteralSubstitutionTree.hpp b/Indexing/LiteralSubstitutionTree.hpp index 2c8382b4b..c02b7ed62 100644 --- a/Indexing/LiteralSubstitutionTree.hpp +++ b/Indexing/LiteralSubstitutionTree.hpp @@ -36,7 +36,6 @@ class LiteralSubstitutionTree using Leaf = SubstitutionTree::Leaf; public: - CLASS_NAME(LiteralSubstitutionTree); USE_ALLOCATOR(LiteralSubstitutionTree); LiteralSubstitutionTree(bool useC=false); diff --git a/Indexing/RequestedIndex.hpp b/Indexing/RequestedIndex.hpp index 7ffd10dc4..874776fa3 100644 --- a/Indexing/RequestedIndex.hpp +++ b/Indexing/RequestedIndex.hpp @@ -23,7 +23,6 @@ template class RequestedIndex final { public: - CLASS_NAME(RequestedIndex); USE_ALLOCATOR(RequestedIndex); RequestedIndex() diff --git a/Indexing/ResultSubstitution.cpp b/Indexing/ResultSubstitution.cpp index f355ba9cb..eff45ff87 100644 --- a/Indexing/ResultSubstitution.cpp +++ b/Indexing/ResultSubstitution.cpp @@ -26,7 +26,6 @@ class RSProxy : public ResultSubstitution { public: - CLASS_NAME(RSProxy); USE_ALLOCATOR(RSProxy); RSProxy(RobSubstitution* subst, int queryBank, int resultBank) diff --git a/Indexing/SubstitutionTree.hpp b/Indexing/SubstitutionTree.hpp index f7d87ce78..ac9ecb796 100644 --- 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; - CLASS_NAME(SubstitutionTree); USE_ALLOCATOR(SubstitutionTree); SubstitutionTree(bool useC, bool rfSubs); @@ -298,7 +297,6 @@ class SubstitutionTree { public: - CLASS_NAME(SubstitutionTree::ChildBySortHelper); USE_ALLOCATOR(ChildBySortHelper); ChildBySortHelper(IntermediateNode* p): _parent(p) @@ -564,7 +562,6 @@ class SubstitutionTree } #endif - CLASS_NAME(SubstitutionTree::UArrIntermediateNode); USE_ALLOCATOR(UArrIntermediateNode); int _size; @@ -652,7 +649,6 @@ class SubstitutionTree } } - CLASS_NAME(SubstitutionTree::SListIntermediateNode); USE_ALLOCATOR(SListIntermediateNode); class NodePtrComparator @@ -923,7 +919,6 @@ class SubstitutionTree - CLASS_NAME(SubstitutionTree::GenMatcher); USE_ALLOCATOR(GenMatcher); /** @@ -1111,7 +1106,6 @@ class SubstitutionTree _derefBindings.reset(); } - CLASS_NAME(SubstitutionTree::InstMatcher); USE_ALLOCATOR(InstMatcher); struct TermSpec diff --git a/Indexing/SubstitutionTree_FastGen.cpp b/Indexing/SubstitutionTree_FastGen.cpp index fe1ff63bc..93f785a45 100644 --- a/Indexing/SubstitutionTree_FastGen.cpp +++ b/Indexing/SubstitutionTree_FastGen.cpp @@ -80,7 +80,6 @@ struct SubstitutionTree::GenMatcher::Binder struct SubstitutionTree::GenMatcher::Applicator { - CLASS_NAME(SubstitutionTree::GenMatcher::Applicator); USE_ALLOCATOR(SubstitutionTree::GenMatcher::Applicator); inline @@ -107,7 +106,6 @@ class SubstitutionTree::GenMatcher::Substitution : public ResultSubstitution { public: - CLASS_NAME(SubstitutionTree::GenMatcher::Substitution); USE_ALLOCATOR(SubstitutionTree::GenMatcher::Substitution); Substitution(GenMatcher* parent, Renaming* resultNormalizer) diff --git a/Indexing/SubstitutionTree_FastInst.cpp b/Indexing/SubstitutionTree_FastInst.cpp index e3a4a4d38..ad5a7321a 100644 --- a/Indexing/SubstitutionTree_FastInst.cpp +++ b/Indexing/SubstitutionTree_FastInst.cpp @@ -38,7 +38,6 @@ class SubstitutionTree::InstMatcher::Substitution : public ResultSubstitution { public: - CLASS_NAME(SubstitutionTree::InstMatcher::Substitution); USE_ALLOCATOR(SubstitutionTree::InstMatcher::Substitution); Substitution(InstMatcher* parent, Renaming* resultDenormalizer) diff --git a/Indexing/SubstitutionTree_Nodes.cpp b/Indexing/SubstitutionTree_Nodes.cpp index 30fd7488e..7df665db6 100644 --- a/Indexing/SubstitutionTree_Nodes.cpp +++ b/Indexing/SubstitutionTree_Nodes.cpp @@ -66,7 +66,6 @@ class SubstitutionTree::UListLeaf _size--; } - CLASS_NAME(SubstitutionTree::UListLeaf); USE_ALLOCATOR(UListLeaf); private: typedef List LDList; @@ -104,7 +103,6 @@ class SubstitutionTree::SListLeaf _children.remove(ld); } - CLASS_NAME(SubstitutionTree::SListLeaf); USE_ALLOCATOR(SListLeaf); private: typedef SkipList LDSkipList; diff --git a/Indexing/TermCodeTree.hpp b/Indexing/TermCodeTree.hpp index 3b6ef9d9b..8d2547c44 100644 --- a/Indexing/TermCodeTree.hpp +++ b/Indexing/TermCodeTree.hpp @@ -56,7 +56,6 @@ class TermCodeTree : public CodeTree inline bool operator!=(const TermInfo& o) { return !(*this==o); } - CLASS_NAME(TermCodeTree::TermInfo); USE_ALLOCATOR(TermInfo); TermList t; @@ -88,7 +87,6 @@ class TermCodeTree : public CodeTree TermInfo* next(); - CLASS_NAME(TermCodeTree::TermMatcher); USE_ALLOCATOR(TermMatcher); }; diff --git a/Indexing/TermIndex.hpp b/Indexing/TermIndex.hpp index ab478a8f7..5300aaf46 100644 --- a/Indexing/TermIndex.hpp +++ b/Indexing/TermIndex.hpp @@ -28,7 +28,6 @@ class TermIndex : public Index { public: - CLASS_NAME(TermIndex); USE_ALLOCATOR(TermIndex); virtual ~TermIndex(); @@ -47,7 +46,6 @@ class SuperpositionSubtermIndex : public TermIndex { public: - CLASS_NAME(SuperpositionSubtermIndex); USE_ALLOCATOR(SuperpositionSubtermIndex); SuperpositionSubtermIndex(TermIndexingStructure* is, Ordering& ord) @@ -62,7 +60,6 @@ class SuperpositionLHSIndex : public TermIndex { public: - CLASS_NAME(SuperpositionLHSIndex); USE_ALLOCATOR(SuperpositionLHSIndex); SuperpositionLHSIndex(TermSubstitutionTree* is, Ordering& ord, const Options& opt) @@ -95,7 +92,6 @@ class DemodulationSubtermIndexImpl : public DemodulationSubtermIndex { public: - CLASS_NAME(DemodulationSubtermIndexImpl); USE_ALLOCATOR(DemodulationSubtermIndexImpl); DemodulationSubtermIndexImpl(TermIndexingStructure* is) @@ -111,7 +107,6 @@ class DemodulationLHSIndex : public TermIndex { public: - CLASS_NAME(DemodulationLHSIndex); USE_ALLOCATOR(DemodulationLHSIndex); DemodulationLHSIndex(TermIndexingStructure* is, Ordering& ord, const Options& opt) @@ -130,7 +125,6 @@ class InductionTermIndex : public TermIndex { public: - CLASS_NAME(InductionTermIndex); USE_ALLOCATOR(InductionTermIndex); InductionTermIndex(TermIndexingStructure* is) @@ -147,7 +141,6 @@ class StructInductionTermIndex : public TermIndex { public: - CLASS_NAME(StructInductionTermIndex); USE_ALLOCATOR(StructInductionTermIndex); StructInductionTermIndex(TermIndexingStructure* is) @@ -165,7 +158,6 @@ class PrimitiveInstantiationIndex : public TermIndex { public: - CLASS_NAME(PrimitiveInstantiationIndex); USE_ALLOCATOR(PrimitiveInstantiationIndex); PrimitiveInstantiationIndex(TermIndexingStructure* is) : TermIndex(is) @@ -180,7 +172,6 @@ class SubVarSupSubtermIndex : public TermIndex { public: - CLASS_NAME(SubVarSupSubtermIndex); USE_ALLOCATOR(SubVarSupSubtermIndex); SubVarSupSubtermIndex(TermIndexingStructure* is, Ordering& ord) @@ -195,7 +186,6 @@ class SubVarSupLHSIndex : public TermIndex { public: - CLASS_NAME(SubVarSupLHSIndex); USE_ALLOCATOR(SubVarSupLHSIndex); SubVarSupLHSIndex(TermIndexingStructure* is, Ordering& ord, const Options& opt) @@ -213,7 +203,6 @@ class NarrowingIndex : public TermIndex { public: - CLASS_NAME(NarrowingIndex); USE_ALLOCATOR(NarrowingIndex); NarrowingIndex(TermIndexingStructure* is) : TermIndex(is) @@ -229,7 +218,6 @@ class SkolemisingFormulaIndex : public TermIndex { public: - CLASS_NAME(SkolemisingFormulaIndex); USE_ALLOCATOR(SkolemisingFormulaIndex); SkolemisingFormulaIndex(TermIndexingStructure* is) : TermIndex(is) @@ -241,7 +229,6 @@ class SkolemisingFormulaIndex : public TermIndex { public: - CLASS_NAME(HeuristicInstantiationIndex); USE_ALLOCATOR(HeuristicInstantiationIndex); HeuristicInstantiationIndex(TermIndexingStructure* is) : TermIndex(is) @@ -257,7 +244,6 @@ class RenamingFormulaIndex : public TermIndex { public: - CLASS_NAME(RenamingFormulaIndex); USE_ALLOCATOR(RenamingFormulaIndex); RenamingFormulaIndex(TermIndexingStructure* is) : TermIndex(is) diff --git a/Indexing/TermSharing.hpp b/Indexing/TermSharing.hpp index 79790f61d..181d7fb51 100644 --- a/Indexing/TermSharing.hpp +++ b/Indexing/TermSharing.hpp @@ -30,7 +30,6 @@ namespace Indexing { class TermSharing { public: - CLASS_NAME(TermSharing); USE_ALLOCATOR(TermSharing); TermSharing(); diff --git a/Indexing/TermSubstitutionTree.hpp b/Indexing/TermSubstitutionTree.hpp index c578b07da..2cf2079f6 100644 --- a/Indexing/TermSubstitutionTree.hpp +++ b/Indexing/TermSubstitutionTree.hpp @@ -39,7 +39,6 @@ class TermSubstitutionTree : public TermIndexingStructure, SubstitutionTree { public: - CLASS_NAME(TermSubstitutionTree); USE_ALLOCATOR(TermSubstitutionTree); /* diff --git a/Inferences/ArgCong.hpp b/Inferences/ArgCong.hpp index 089072636..9d92658a5 100644 --- a/Inferences/ArgCong.hpp +++ b/Inferences/ArgCong.hpp @@ -31,7 +31,6 @@ class ArgCong : public GeneratingInferenceEngine { public: - CLASS_NAME(ArgCong); USE_ALLOCATOR(ArgCong); ClauseIterator generateClauses(Clause* premise); diff --git a/Inferences/ArithmeticSubtermGeneralization.hpp b/Inferences/ArithmeticSubtermGeneralization.hpp index 256a49ba2..407ffdea1 100644 --- a/Inferences/ArithmeticSubtermGeneralization.hpp +++ b/Inferences/ArithmeticSubtermGeneralization.hpp @@ -23,7 +23,6 @@ class NumeralMultiplicationGeneralization : public SimplifyingGeneratingInference1 { public: - CLASS_NAME(NumeralMultiplicationGeneralization); USE_ALLOCATOR(NumeralMultiplicationGeneralization); virtual ~NumeralMultiplicationGeneralization(); @@ -36,7 +35,6 @@ class VariableMultiplicationGeneralization : public SimplifyingGeneratingInference1 { public: - CLASS_NAME(VariableMultiplicationGeneralization); USE_ALLOCATOR(VariableMultiplicationGeneralization); virtual ~VariableMultiplicationGeneralization(); @@ -49,7 +47,6 @@ class VariablePowerGeneralization : public SimplifyingGeneratingInference1 { public: - CLASS_NAME(VariablePowerGeneralization); USE_ALLOCATOR(VariablePowerGeneralization); virtual ~VariablePowerGeneralization(); @@ -62,7 +59,6 @@ class AdditionGeneralization : public SimplifyingGeneratingInference1 { public: - CLASS_NAME(AdditionGeneralization); USE_ALLOCATOR(AdditionGeneralization); virtual ~AdditionGeneralization(); diff --git a/Inferences/ArrayTheoryISE.hpp b/Inferences/ArrayTheoryISE.hpp index 4d63a622d..62a956f4d 100644 --- a/Inferences/ArrayTheoryISE.hpp +++ b/Inferences/ArrayTheoryISE.hpp @@ -44,7 +44,6 @@ class ArrayTheoryISE : public ImmediateSimplificationEngine { public: - CLASS_NAME(ArrayTheoryISE); USE_ALLOCATOR(ArrayTheoryISE); ArrayTheoryISE(); diff --git a/Inferences/BackwardDemodulation.hpp b/Inferences/BackwardDemodulation.hpp index b83350dab..fd09b5511 100644 --- a/Inferences/BackwardDemodulation.hpp +++ b/Inferences/BackwardDemodulation.hpp @@ -30,7 +30,6 @@ class BackwardDemodulation : public BackwardSimplificationEngine { public: - CLASS_NAME(BackwardDemodulation); USE_ALLOCATOR(BackwardDemodulation); void attach(SaturationAlgorithm* salg); diff --git a/Inferences/BackwardSubsumptionDemodulation.hpp b/Inferences/BackwardSubsumptionDemodulation.hpp index 0d79e359a..b1e0ab93f 100644 --- a/Inferences/BackwardSubsumptionDemodulation.hpp +++ b/Inferences/BackwardSubsumptionDemodulation.hpp @@ -49,7 +49,6 @@ class BackwardSubsumptionDemodulation : public BackwardSimplificationEngine { public: - CLASS_NAME(BackwardSubsumptionDemodulation); USE_ALLOCATOR(BackwardSubsumptionDemodulation); BackwardSubsumptionDemodulation(); diff --git a/Inferences/BackwardSubsumptionResolution.hpp b/Inferences/BackwardSubsumptionResolution.hpp index d5be8b663..281f1e37e 100644 --- a/Inferences/BackwardSubsumptionResolution.hpp +++ b/Inferences/BackwardSubsumptionResolution.hpp @@ -28,7 +28,6 @@ class BackwardSubsumptionResolution : public BackwardSimplificationEngine { public: - CLASS_NAME(BackwardSubsumptionResolution); USE_ALLOCATOR(BackwardSubsumptionResolution); BackwardSubsumptionResolution(bool byUnitsOnly) : _byUnitsOnly(byUnitsOnly) {} diff --git a/Inferences/BinaryResolution.hpp b/Inferences/BinaryResolution.hpp index af6c9583f..ccd12bace 100644 --- a/Inferences/BinaryResolution.hpp +++ b/Inferences/BinaryResolution.hpp @@ -33,7 +33,6 @@ class BinaryResolution : public GeneratingInferenceEngine { public: - CLASS_NAME(BinaryResolution); USE_ALLOCATOR(BinaryResolution); BinaryResolution() diff --git a/Inferences/BoolEqToDiseq.hpp b/Inferences/BoolEqToDiseq.hpp index 36cd9a685..2ec2490d3 100644 --- a/Inferences/BoolEqToDiseq.hpp +++ b/Inferences/BoolEqToDiseq.hpp @@ -24,7 +24,6 @@ namespace Inferences { class BoolEqToDiseq : public GeneratingInferenceEngine { public: - CLASS_NAME(BoolEqToDiseq); USE_ALLOCATOR(BoolEqToDiseq); ClauseIterator generateClauses(Clause* premise); diff --git a/Inferences/BoolSimp.hpp b/Inferences/BoolSimp.hpp index 367bd07b3..1b93458e6 100644 --- a/Inferences/BoolSimp.hpp +++ b/Inferences/BoolSimp.hpp @@ -24,7 +24,6 @@ namespace Inferences { class BoolSimp : public ImmediateSimplificationEngine { public: - CLASS_NAME(BoolSimp); USE_ALLOCATOR(BoolSimp); Clause* simplify(Clause* premise); diff --git a/Inferences/CNFOnTheFly.hpp b/Inferences/CNFOnTheFly.hpp index c6ef4ffa4..a2b22e893 100644 --- a/Inferences/CNFOnTheFly.hpp +++ b/Inferences/CNFOnTheFly.hpp @@ -35,7 +35,6 @@ class IFFXORRewriterISE { public: - CLASS_NAME(IFFXORRewriterISE); USE_ALLOCATOR(IFFXORRewriterISE); Clause* simplify(Clause* c); @@ -46,7 +45,6 @@ class EagerClausificationISE { public: - CLASS_NAME(EagerClausificationISE); USE_ALLOCATOR(EagerClausificationISE); ClauseIterator simplifyMany(Clause* c); @@ -58,7 +56,6 @@ class LazyClausification : public SimplificationEngine { public: - CLASS_NAME(LazyClausification); USE_ALLOCATOR(LazyClausification); LazyClausification(){ @@ -79,7 +76,6 @@ class LazyClausificationGIE { public: - CLASS_NAME(LazyClausificationGIE); USE_ALLOCATOR(LazyClausificationGIE); LazyClausificationGIE(){ @@ -99,7 +95,6 @@ class LazyClausificationGIE : public ImmediateSimplificationEngine { public: - CLASS_NAME(NotProxyISE); USE_ALLOCATOR(NotProxyISE); Kernel::Clause* simplify(Kernel::Clause* c); @@ -111,7 +106,6 @@ class EqualsProxyISE { public: - CLASS_NAME(EqualsProxyISE); USE_ALLOCATOR(EqualsProxyISE); Kernel::Clause* simplify(Kernel::Clause* c); @@ -123,7 +117,6 @@ class OrImpAndProxyISE { public: - CLASS_NAME(OrImpAndProxyISE); USE_ALLOCATOR(OrImpAndProxyISE); Kernel::Clause* simplify(Kernel::Clause* c); @@ -135,7 +128,6 @@ class PiSigmaProxyISE { public: - CLASS_NAME(PiSigmaProxyISE); USE_ALLOCATOR(PiSigmaProxyISE); Kernel::Clause* simplify(Kernel::Clause* c); @@ -145,7 +137,6 @@ class PiSigmaProxyISE class ProxyISE : public ImmediateSimplificationEngine { public: - CLASS_NAME(ProxyISE); USE_ALLOCATOR(ProxyISE); ClauseIterator simplifyMany(Clause* c); Clause* simplify(Clause* c){ NOT_IMPLEMENTED; } diff --git a/Inferences/Cancellation.hpp b/Inferences/Cancellation.hpp index f6e62a4ca..5cf454366 100644 --- a/Inferences/Cancellation.hpp +++ b/Inferences/Cancellation.hpp @@ -20,7 +20,6 @@ class Cancellation : public SimplifyingGeneratingLiteralSimplification { public: - CLASS_NAME(Cancellation); USE_ALLOCATOR(Cancellation); Cancellation(Ordering& ordering); diff --git a/Inferences/Cases.hpp b/Inferences/Cases.hpp index d7f4eef6b..f3336ab3d 100644 --- a/Inferences/Cases.hpp +++ b/Inferences/Cases.hpp @@ -23,7 +23,6 @@ namespace Inferences { class Cases : public GeneratingInferenceEngine { public: - CLASS_NAME(Cases); USE_ALLOCATOR(Cases); Clause* performParamodulation(Clause* cl, Literal* lit, TermList t); diff --git a/Inferences/CasesSimp.hpp b/Inferences/CasesSimp.hpp index c5fbbb490..8de831cb8 100644 --- a/Inferences/CasesSimp.hpp +++ b/Inferences/CasesSimp.hpp @@ -23,7 +23,6 @@ namespace Inferences { class CasesSimp : public ImmediateSimplificationEngine { public: - CLASS_NAME(CasesSimp); USE_ALLOCATOR(CasesSimp); ClauseIterator simplifyMany(Clause* premise); diff --git a/Inferences/Choice.hpp b/Inferences/Choice.hpp index 70bbfb32e..a60cc4289 100644 --- a/Inferences/Choice.hpp +++ b/Inferences/Choice.hpp @@ -24,7 +24,6 @@ namespace Inferences { class Choice : public GeneratingInferenceEngine { public: - CLASS_NAME(Choice); USE_ALLOCATOR(Choice); ClauseIterator generateClauses(Clause* premise); diff --git a/Inferences/CombinatorDemodISE.hpp b/Inferences/CombinatorDemodISE.hpp index a23839428..91de177a8 100644 --- a/Inferences/CombinatorDemodISE.hpp +++ b/Inferences/CombinatorDemodISE.hpp @@ -25,7 +25,6 @@ class CombinatorDemodISE : public ImmediateSimplificationEngine { public: - CLASS_NAME(CombinatorDemodISE); USE_ALLOCATOR(CombinatorDemodISE); CombinatorDemodISE(){} diff --git a/Inferences/CombinatorNormalisationISE.hpp b/Inferences/CombinatorNormalisationISE.hpp index c10b4b998..483d01a11 100644 --- a/Inferences/CombinatorNormalisationISE.hpp +++ b/Inferences/CombinatorNormalisationISE.hpp @@ -40,7 +40,6 @@ class CombinatorNormalisationISE : public ImmediateSimplificationEngine { public: - CLASS_NAME(CombinatorNormalisationISE); USE_ALLOCATOR(CombinatorNormalisationISE); CombinatorNormalisationISE(){} diff --git a/Inferences/Condensation.hpp b/Inferences/Condensation.hpp index 292dd25b2..4f639404a 100644 --- a/Inferences/Condensation.hpp +++ b/Inferences/Condensation.hpp @@ -34,7 +34,6 @@ class Condensation : public ImmediateSimplificationEngine { public: - CLASS_NAME(Condensation); USE_ALLOCATOR(Condensation); Clause* simplify(Clause* cl); diff --git a/Inferences/DefinitionIntroduction.hpp b/Inferences/DefinitionIntroduction.hpp index 290c93cc9..baca76dd7 100644 --- a/Inferences/DefinitionIntroduction.hpp +++ b/Inferences/DefinitionIntroduction.hpp @@ -23,7 +23,6 @@ namespace Inferences class DefinitionIntroduction: public GeneratingInferenceEngine, public Index { public: - CLASS_NAME(DefinitionIntroduction); USE_ALLOCATOR(DefinitionIntroduction); void attach(SaturationAlgorithm *salg) override { diff --git a/Inferences/DistinctEqualitySimplifier.hpp b/Inferences/DistinctEqualitySimplifier.hpp index 58ab24950..5848a5456 100644 --- a/Inferences/DistinctEqualitySimplifier.hpp +++ b/Inferences/DistinctEqualitySimplifier.hpp @@ -24,7 +24,6 @@ class DistinctEqualitySimplifier : public ImmediateSimplificationEngine { public: - CLASS_NAME(DistinctEqualitySimplifier); USE_ALLOCATOR(DistinctEqualitySimplifier); Clause* simplify(Clause* cl); diff --git a/Inferences/ElimLeibniz.hpp b/Inferences/ElimLeibniz.hpp index e5cbb59ba..c0b799c31 100644 --- a/Inferences/ElimLeibniz.hpp +++ b/Inferences/ElimLeibniz.hpp @@ -25,7 +25,6 @@ namespace Inferences { class ElimLeibniz : public GeneratingInferenceEngine { public: - CLASS_NAME(ElimLeibniz); USE_ALLOCATOR(ElimLeibniz); ClauseIterator generateClauses(Clause* premise); diff --git a/Inferences/EqualityFactoring.hpp b/Inferences/EqualityFactoring.hpp index 24f49d48a..410eb94f6 100644 --- a/Inferences/EqualityFactoring.hpp +++ b/Inferences/EqualityFactoring.hpp @@ -31,7 +31,6 @@ class EqualityFactoring : public GeneratingInferenceEngine { public: - CLASS_NAME(EqualityFactoring); USE_ALLOCATOR(EqualityFactoring); ClauseIterator generateClauses(Clause* premise); diff --git a/Inferences/EqualityResolution.hpp b/Inferences/EqualityResolution.hpp index 4a1a91bc6..d2e2ec302 100644 --- a/Inferences/EqualityResolution.hpp +++ b/Inferences/EqualityResolution.hpp @@ -31,7 +31,6 @@ class EqualityResolution : public GeneratingInferenceEngine { public: - CLASS_NAME(EqualityResolution); USE_ALLOCATOR(EqualityResolution); ClauseIterator generateClauses(Clause* premise); diff --git a/Inferences/EquationalTautologyRemoval.hpp b/Inferences/EquationalTautologyRemoval.hpp index b1dff743f..a9caf2bfc 100644 --- a/Inferences/EquationalTautologyRemoval.hpp +++ b/Inferences/EquationalTautologyRemoval.hpp @@ -26,7 +26,6 @@ class EquationalTautologyRemoval : public ImmediateSimplificationEngine { public: - CLASS_NAME(EquationalTautologyRemoval); USE_ALLOCATOR(EquationalTautologyRemoval); EquationalTautologyRemoval() : _cc(nullptr) {} diff --git a/Inferences/ExtensionalityResolution.hpp b/Inferences/ExtensionalityResolution.hpp index 8daad523e..4d03d0921 100644 --- a/Inferences/ExtensionalityResolution.hpp +++ b/Inferences/ExtensionalityResolution.hpp @@ -40,7 +40,6 @@ class ExtensionalityResolution : public GeneratingInferenceEngine { public: - CLASS_NAME(ExtensionalityResolution); USE_ALLOCATOR(ExtensionalityResolution); ExtensionalityResolution() {} diff --git a/Inferences/FOOLParamodulation.hpp b/Inferences/FOOLParamodulation.hpp index a1060fb8d..c2b5166a6 100644 --- a/Inferences/FOOLParamodulation.hpp +++ b/Inferences/FOOLParamodulation.hpp @@ -23,7 +23,6 @@ namespace Inferences { class FOOLParamodulation : public GeneratingInferenceEngine { public: - CLASS_NAME(FOOLParamodulation); USE_ALLOCATOR(FOOLParamodulation); ClauseIterator generateClauses(Clause* premise); }; diff --git a/Inferences/Factoring.hpp b/Inferences/Factoring.hpp index 8f973a4b4..dd64c65a6 100644 --- a/Inferences/Factoring.hpp +++ b/Inferences/Factoring.hpp @@ -30,7 +30,6 @@ class Factoring : public GeneratingInferenceEngine { public: - CLASS_NAME(Factoring); USE_ALLOCATOR(Factoring); ClauseIterator generateClauses(Clause* premise); diff --git a/Inferences/FastCondensation.hpp b/Inferences/FastCondensation.hpp index 429cdddb3..98610c075 100644 --- a/Inferences/FastCondensation.hpp +++ b/Inferences/FastCondensation.hpp @@ -43,7 +43,6 @@ class FastCondensation : public ImmediateSimplificationEngine { public: - CLASS_NAME(FastCondensation); USE_ALLOCATOR(FastCondensation); Clause* simplify(Clause* cl); diff --git a/Inferences/ForwardDemodulation.hpp b/Inferences/ForwardDemodulation.hpp index 0f4ff8c67..918480dce 100644 --- a/Inferences/ForwardDemodulation.hpp +++ b/Inferences/ForwardDemodulation.hpp @@ -32,7 +32,6 @@ class ForwardDemodulation : public ForwardSimplificationEngine { public: - CLASS_NAME(ForwardDemodulation); USE_ALLOCATOR(ForwardDemodulation); void attach(SaturationAlgorithm* salg) override; @@ -50,7 +49,6 @@ class ForwardDemodulationImpl : public ForwardDemodulation { public: - CLASS_NAME(ForwardDemodulationImpl); USE_ALLOCATOR(ForwardDemodulationImpl); bool perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) override; diff --git a/Inferences/ForwardLiteralRewriting.hpp b/Inferences/ForwardLiteralRewriting.hpp index 071a29685..bed1280c9 100644 --- a/Inferences/ForwardLiteralRewriting.hpp +++ b/Inferences/ForwardLiteralRewriting.hpp @@ -31,7 +31,6 @@ class ForwardLiteralRewriting : public ForwardSimplificationEngine { public: - CLASS_NAME(ForwardLiteralRewriting); USE_ALLOCATOR(ForwardLiteralRewriting); void attach(SaturationAlgorithm* salg) override; diff --git a/Inferences/ForwardSubsumptionAndResolution.cpp b/Inferences/ForwardSubsumptionAndResolution.cpp index 57ec4825c..2816c143b 100644 --- a/Inferences/ForwardSubsumptionAndResolution.cpp +++ b/Inferences/ForwardSubsumptionAndResolution.cpp @@ -63,7 +63,6 @@ void ForwardSubsumptionAndResolution::detach() } struct ClauseMatches { - CLASS_NAME(ForwardSubsumptionAndResolution::ClauseMatches); USE_ALLOCATOR(ClauseMatches); private: diff --git a/Inferences/ForwardSubsumptionAndResolution.hpp b/Inferences/ForwardSubsumptionAndResolution.hpp index bab0e28b4..d92e5c971 100644 --- a/Inferences/ForwardSubsumptionAndResolution.hpp +++ b/Inferences/ForwardSubsumptionAndResolution.hpp @@ -30,7 +30,6 @@ class ForwardSubsumptionAndResolution : public ForwardSimplificationEngine { public: - CLASS_NAME(ForwardSubsumptionAndResolution); USE_ALLOCATOR(ForwardSubsumptionAndResolution); ForwardSubsumptionAndResolution(bool subsumptionResolution=true) diff --git a/Inferences/ForwardSubsumptionDemodulation.hpp b/Inferences/ForwardSubsumptionDemodulation.hpp index 7ef26eaaf..59f6be697 100644 --- a/Inferences/ForwardSubsumptionDemodulation.hpp +++ b/Inferences/ForwardSubsumptionDemodulation.hpp @@ -48,7 +48,6 @@ class ForwardSubsumptionDemodulation : public ForwardSimplificationEngine { public: - CLASS_NAME(ForwardSubsumptionDemodulation); USE_ALLOCATOR(ForwardSubsumptionDemodulation); ForwardSubsumptionDemodulation(bool doSubsumption) diff --git a/Inferences/GaussianVariableElimination.hpp b/Inferences/GaussianVariableElimination.hpp index 5823905a8..2a2b4d5c0 100644 --- a/Inferences/GaussianVariableElimination.hpp +++ b/Inferences/GaussianVariableElimination.hpp @@ -18,7 +18,6 @@ class GaussianVariableElimination : public SimplifyingGeneratingInference1 { public: - CLASS_NAME(GaussianVariableElimination); USE_ALLOCATOR(GaussianVariableElimination); SimplifyingGeneratingInference1::Result simplify(Clause *cl, bool doCheckOrdering) override; diff --git a/Inferences/GlobalSubsumption.hpp b/Inferences/GlobalSubsumption.hpp index e81129102..d0ba11a9f 100644 --- a/Inferences/GlobalSubsumption.hpp +++ b/Inferences/GlobalSubsumption.hpp @@ -35,7 +35,6 @@ class GlobalSubsumption : public ForwardSimplificationEngine { public: - CLASS_NAME(GlobalSubsumption); USE_ALLOCATOR(GlobalSubsumption); GlobalSubsumption(const Options& opts) : _index(0), diff --git a/Inferences/Induction.hpp b/Inferences/Induction.hpp index bdfc95af0..c10620e15 100644 --- a/Inferences/Induction.hpp +++ b/Inferences/Induction.hpp @@ -162,7 +162,6 @@ class Induction : public GeneratingInferenceEngine { public: - CLASS_NAME(Induction); USE_ALLOCATOR(Induction); void attach(SaturationAlgorithm* salg) override; @@ -198,7 +197,6 @@ class InductionClauseIterator processClause(premise); } - CLASS_NAME(InductionClauseIterator); USE_ALLOCATOR(InductionClauseIterator); DECL_ELEMENT_TYPE(Clause*); diff --git a/Inferences/InductionHelper.hpp b/Inferences/InductionHelper.hpp index fc0ab6128..82cd8df91 100644 --- a/Inferences/InductionHelper.hpp +++ b/Inferences/InductionHelper.hpp @@ -31,7 +31,6 @@ using namespace Kernel; class InductionHelper { public: - CLASS_NAME(InductionHelper); USE_ALLOCATOR(InductionHelper); InductionHelper(LiteralIndex* comparisonIndex, TermIndex* inductionTermIndex) diff --git a/Inferences/InferenceEngine.hpp b/Inferences/InferenceEngine.hpp index a7bdf17e0..00e648aec 100644 --- a/Inferences/InferenceEngine.hpp +++ b/Inferences/InferenceEngine.hpp @@ -52,7 +52,6 @@ using namespace Shell; class InferenceEngine { public: - CLASS_NAME(InferenceEngine); USE_ALLOCATOR(InferenceEngine); InferenceEngine() : _salg(0) {} @@ -311,7 +310,6 @@ class DummyGIE : public GeneratingInferenceEngine { public: - CLASS_NAME(DummyGIE); USE_ALLOCATOR(DummyGIE); ClauseIterator generateClauses(Clause* premise) @@ -325,7 +323,6 @@ class DummyFSE : public ForwardSimplificationEngine { public: - CLASS_NAME(DummyFSE); USE_ALLOCATOR(DummyFSE); void perform(Clause* cl, bool& keep, ClauseIterator& toAdd, ClauseIterator& premises) @@ -340,7 +337,6 @@ class DummyBSE : public BackwardSimplificationEngine { public: - CLASS_NAME(DummyBSE); USE_ALLOCATOR(DummyBSE); void perform(Clause* premise, BwSimplificationRecordIterator& simplifications) @@ -354,7 +350,6 @@ class CompositeISE : public ImmediateSimplificationEngine { public: - CLASS_NAME(CompositeISE); USE_ALLOCATOR(CompositeISE); CompositeISE() : _inners(0), _innersMany(0) {} @@ -390,7 +385,6 @@ class CompositeGIE : public GeneratingInferenceEngine { public: - CLASS_NAME(CompositeGIE); USE_ALLOCATOR(CompositeGIE); CompositeGIE() : _inners(0) {} @@ -409,7 +403,6 @@ class CompositeSGI : public SimplifyingGeneratingInference { public: - CLASS_NAME(CompositieSGI); USE_ALLOCATOR(CompositeSGI); CompositeSGI() : _simplifiers(), _generators() {} @@ -429,7 +422,6 @@ class ChoiceDefinitionISE : public ImmediateSimplificationEngine { public: - CLASS_NAME(ChoiceDefinitionISE); USE_ALLOCATOR(ChoiceDefinitionISE); Clause* simplify(Clause* cl); @@ -444,7 +436,6 @@ class DuplicateLiteralRemovalISE : public ImmediateSimplificationEngine { public: - CLASS_NAME(DuplicateLiteralRemovalISE); USE_ALLOCATOR(DuplicateLiteralRemovalISE); Clause* simplify(Clause* cl); @@ -454,7 +445,6 @@ class TautologyDeletionISE2 : public ImmediateSimplificationEngine { public: - CLASS_NAME(TautologyDeletionISE2); USE_ALLOCATOR(TautologyDeletionISE2); Clause* simplify(Clause* cl); diff --git a/Inferences/Injectivity.hpp b/Inferences/Injectivity.hpp index 03abcf281..8556811a1 100644 --- a/Inferences/Injectivity.hpp +++ b/Inferences/Injectivity.hpp @@ -23,7 +23,6 @@ namespace Inferences { class Injectivity : public GeneratingInferenceEngine { public: - CLASS_NAME(Injectivity); USE_ALLOCATOR(Injectivity); ClauseIterator generateClauses(Clause* premise); diff --git a/Inferences/InnerRewriting.hpp b/Inferences/InnerRewriting.hpp index 855a263a9..fafe61f15 100644 --- a/Inferences/InnerRewriting.hpp +++ b/Inferences/InnerRewriting.hpp @@ -30,7 +30,6 @@ class InnerRewriting : public ForwardSimplificationEngine { public: - CLASS_NAME(InnerRewriting); USE_ALLOCATOR(InnerRewriting); bool perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) override; diff --git a/Inferences/Instantiation.hpp b/Inferences/Instantiation.hpp index 97ffc15bb..a594c50b2 100644 --- a/Inferences/Instantiation.hpp +++ b/Inferences/Instantiation.hpp @@ -33,7 +33,6 @@ class Instantiation : public GeneratingInferenceEngine { public: - CLASS_NAME(Instantiation); USE_ALLOCATOR(Instantiation); Instantiation() {} diff --git a/Inferences/InterpretedEvaluation.hpp b/Inferences/InterpretedEvaluation.hpp index aba1fb722..e68cfe88a 100644 --- a/Inferences/InterpretedEvaluation.hpp +++ b/Inferences/InterpretedEvaluation.hpp @@ -31,7 +31,6 @@ class InterpretedEvaluation : public ImmediateSimplificationEngine { public: - CLASS_NAME(InterpretedEvaluation); USE_ALLOCATOR(InterpretedEvaluation); InterpretedEvaluation(bool doNormalize, Ordering& ordering); diff --git a/Inferences/InvalidAnswerLiteralRemoval.hpp b/Inferences/InvalidAnswerLiteralRemoval.hpp index 1b58e1ace..c7e9e139e 100644 --- a/Inferences/InvalidAnswerLiteralRemoval.hpp +++ b/Inferences/InvalidAnswerLiteralRemoval.hpp @@ -28,7 +28,6 @@ class InvalidAnswerLiteralRemoval : public ImmediateSimplificationEngine { public: - CLASS_NAME(InvalidAnswerLiteralRemoval); USE_ALLOCATOR(InvalidAnswerLiteralRemoval); Clause* simplify(Clause* cl) override; diff --git a/Inferences/LfpRule.hpp b/Inferences/LfpRule.hpp index 0f30f2a98..409232e53 100644 --- a/Inferences/LfpRule.hpp +++ b/Inferences/LfpRule.hpp @@ -21,7 +21,6 @@ class LfpRule { Rule _inner; public: - CLASS_NAME(LfpRule); USE_ALLOCATOR(LfpRule); LfpRule(Rule rule); diff --git a/Inferences/Narrow.hpp b/Inferences/Narrow.hpp index ec0500ae6..91772e842 100644 --- a/Inferences/Narrow.hpp +++ b/Inferences/Narrow.hpp @@ -31,7 +31,6 @@ class Narrow : public GeneratingInferenceEngine { public: - CLASS_NAME(Narrow); USE_ALLOCATOR(Narrow); ClauseIterator generateClauses(Clause* premise); diff --git a/Inferences/NegativeExt.hpp b/Inferences/NegativeExt.hpp index 58b1f8766..078ff01ee 100644 --- a/Inferences/NegativeExt.hpp +++ b/Inferences/NegativeExt.hpp @@ -31,7 +31,6 @@ class NegativeExt : public GeneratingInferenceEngine { public: - CLASS_NAME(NegativeExt); USE_ALLOCATOR(NegativeExt); ClauseIterator generateClauses(Clause* premise); diff --git a/Inferences/PolynomialEvaluation.hpp b/Inferences/PolynomialEvaluation.hpp index 72db102eb..b6ac82d00 100644 --- a/Inferences/PolynomialEvaluation.hpp +++ b/Inferences/PolynomialEvaluation.hpp @@ -30,7 +30,6 @@ class PolynomialEvaluation : public SimplifyingGeneratingLiteralSimplification { public: - CLASS_NAME(PolynomialEvaluation); USE_ALLOCATOR(PolynomialEvaluation); PolynomialEvaluation(Ordering& ordering); diff --git a/Inferences/PrimitiveInstantiation.hpp b/Inferences/PrimitiveInstantiation.hpp index aec25d1cb..58fc987e4 100644 --- a/Inferences/PrimitiveInstantiation.hpp +++ b/Inferences/PrimitiveInstantiation.hpp @@ -31,7 +31,6 @@ class PrimitiveInstantiation : public GeneratingInferenceEngine { public: - CLASS_NAME(PrimitiveInstantiation); USE_ALLOCATOR(PrimitiveInstantiation); void attach(SaturationAlgorithm* salg); diff --git a/Inferences/PushUnaryMinus.hpp b/Inferences/PushUnaryMinus.hpp index 9df383fbc..4e105b901 100644 --- a/Inferences/PushUnaryMinus.hpp +++ b/Inferences/PushUnaryMinus.hpp @@ -27,7 +27,6 @@ class PushUnaryMinus : public ImmediateSimplificationEngine { public: - CLASS_NAME(PushUnaryMinus); USE_ALLOCATOR(PushUnaryMinus); virtual ~PushUnaryMinus(); diff --git a/Inferences/RenamingOnTheFly.hpp b/Inferences/RenamingOnTheFly.hpp index b4001af13..962736f2b 100644 --- a/Inferences/RenamingOnTheFly.hpp +++ b/Inferences/RenamingOnTheFly.hpp @@ -31,7 +31,6 @@ class RenamingOnTheFly : public SimplificationEngine { public: - CLASS_NAME(RenamingOnTheFly); USE_ALLOCATOR(RenamingOnTheFly); ClauseIterator perform(Clause* c); diff --git a/Inferences/SLQueryBackwardSubsumption.hpp b/Inferences/SLQueryBackwardSubsumption.hpp index d3bd29ea5..01cd9841c 100644 --- a/Inferences/SLQueryBackwardSubsumption.hpp +++ b/Inferences/SLQueryBackwardSubsumption.hpp @@ -26,7 +26,6 @@ class SLQueryBackwardSubsumption : public BackwardSimplificationEngine { public: - CLASS_NAME(SLQueryBackwardSubsumption); USE_ALLOCATOR(SLQueryBackwardSubsumption); SLQueryBackwardSubsumption(bool byUnitsOnly) : _byUnitsOnly(byUnitsOnly), _index(0) {} diff --git a/Inferences/SubVarSup.hpp b/Inferences/SubVarSup.hpp index e9f251633..4fde6f70d 100644 --- a/Inferences/SubVarSup.hpp +++ b/Inferences/SubVarSup.hpp @@ -31,7 +31,6 @@ class SubVarSup : public GeneratingInferenceEngine { public: - CLASS_NAME(SubVarSup); USE_ALLOCATOR(SubVarSup); void attach(SaturationAlgorithm* salg); diff --git a/Inferences/SubsumptionDemodulationHelper.hpp b/Inferences/SubsumptionDemodulationHelper.hpp index ae0e9c9e7..7a0e64494 100644 --- a/Inferences/SubsumptionDemodulationHelper.hpp +++ b/Inferences/SubsumptionDemodulationHelper.hpp @@ -58,7 +58,6 @@ using namespace Lib; */ class OverlayBinder { - CLASS_NAME(OverlayBinder); USE_ALLOCATOR(OverlayBinder); public: @@ -217,7 +216,6 @@ std::ostream& operator<<(std::ostream& o, OverlayBinder const& binder); */ class SDClauseMatches { - CLASS_NAME(SDClauseMatches); USE_ALLOCATOR(SDClauseMatches); public: diff --git a/Inferences/Superposition.hpp b/Inferences/Superposition.hpp index 79a61ff44..46678f78c 100644 --- a/Inferences/Superposition.hpp +++ b/Inferences/Superposition.hpp @@ -31,7 +31,6 @@ class Superposition : public GeneratingInferenceEngine { public: - CLASS_NAME(Superposition); USE_ALLOCATOR(Superposition); void attach(SaturationAlgorithm* salg); diff --git a/Inferences/TautologyDeletionISE.hpp b/Inferences/TautologyDeletionISE.hpp index 6ca205cfe..2b7c8e6b3 100644 --- a/Inferences/TautologyDeletionISE.hpp +++ b/Inferences/TautologyDeletionISE.hpp @@ -25,7 +25,6 @@ class TautologyDeletionISE : public ImmediateSimplificationEngine { public: - CLASS_NAME(TautologyDeletionISE); USE_ALLOCATOR(TautologyDeletionISE); TautologyDeletionISE(bool deleteEqTautologies=true) : _deleteEqTautologies(deleteEqTautologies) {} diff --git a/Inferences/TermAlgebraReasoning.hpp b/Inferences/TermAlgebraReasoning.hpp index aeba6e1b2..ab00ca5e5 100644 --- a/Inferences/TermAlgebraReasoning.hpp +++ b/Inferences/TermAlgebraReasoning.hpp @@ -50,7 +50,6 @@ class DistinctnessISE { public: - CLASS_NAME(DistinctnessISE); USE_ALLOCATOR(DistinctnessISE); Kernel::Clause* simplify(Kernel::Clause* c); @@ -70,7 +69,6 @@ class DistinctnessISE class InjectivityGIE : public GeneratingInferenceEngine { public: - CLASS_NAME(InjectivityGIE); USE_ALLOCATOR(InjectivityGIE); Kernel::ClauseIterator generateClauses(Kernel::Clause* c); @@ -93,7 +91,6 @@ class InjectivityISE : public ImmediateSimplificationEngine { public: - CLASS_NAME(InjectivityISE); USE_ALLOCATOR(InjectivityISE); Kernel::Clause* simplify(Kernel::Clause* c); @@ -103,7 +100,6 @@ class NegativeInjectivityISE : public ImmediateSimplificationEngine { public: - CLASS_NAME(NegativeInjectivityISE); USE_ALLOCATOR(NegativeInjectivityISE); Kernel::Clause* simplify(Kernel::Clause* c); @@ -115,7 +111,6 @@ class NegativeInjectivityISE class AcyclicityGIE : public GeneratingInferenceEngine { public: - CLASS_NAME(AcyclicityGIE); USE_ALLOCATOR(AcyclicityGIE); void attach(Saturation::SaturationAlgorithm* salg); @@ -131,7 +126,6 @@ class AcyclicityGIE class AcyclicityGIE1 : public GeneratingInferenceEngine { public: - CLASS_NAME(AcyclicityGIE1); USE_ALLOCATOR(AcyclicityGIE1); Kernel::ClauseIterator generateClauses(Kernel::Clause* c); diff --git a/Inferences/TheoryInstAndSimp.hpp b/Inferences/TheoryInstAndSimp.hpp index 3b5e07483..de3d14353 100644 --- a/Inferences/TheoryInstAndSimp.hpp +++ b/Inferences/TheoryInstAndSimp.hpp @@ -48,7 +48,6 @@ class TheoryInstAndSimp { public: using SortId = SAT::Z3Interfacing::SortId; - CLASS_NAME(TheoryInstAndSimp); USE_ALLOCATOR(TheoryInstAndSimp); ~TheoryInstAndSimp(); diff --git a/Inferences/URResolution.cpp b/Inferences/URResolution.cpp index 86a22bbb9..51eb742b9 100644 --- a/Inferences/URResolution.cpp +++ b/Inferences/URResolution.cpp @@ -99,7 +99,6 @@ void URResolution::detach() struct URResolution::Item { - CLASS_NAME(URResolution::Item); USE_ALLOCATOR(URResolution::Item); Item(Clause* cl, bool selectedOnly, URResolution& parent, bool mustResolveAll) diff --git a/Inferences/URResolution.hpp b/Inferences/URResolution.hpp index 0e6fa1172..52cd86f62 100644 --- a/Inferences/URResolution.hpp +++ b/Inferences/URResolution.hpp @@ -30,7 +30,6 @@ class URResolution : public GeneratingInferenceEngine { public: - CLASS_NAME(URResolution); USE_ALLOCATOR(URResolution); URResolution(); diff --git a/Kernel/BestLiteralSelector.hpp b/Kernel/BestLiteralSelector.hpp index 72f1cf981..b98ab9695 100644 --- a/Kernel/BestLiteralSelector.hpp +++ b/Kernel/BestLiteralSelector.hpp @@ -54,7 +54,6 @@ class BestLiteralSelector : public LiteralSelector { public: - CLASS_NAME(BestLiteralSelector); USE_ALLOCATOR(BestLiteralSelector); BestLiteralSelector(const Ordering& ordering, const Options& options) : LiteralSelector(ordering, options) @@ -116,7 +115,6 @@ class CompleteBestLiteralSelector : public LiteralSelector { public: - CLASS_NAME(CompleteBestLiteralSelector); USE_ALLOCATOR(CompleteBestLiteralSelector); CompleteBestLiteralSelector(const Ordering& ordering, const Options& options) : LiteralSelector(ordering, options) diff --git a/Kernel/ELiteralSelector.hpp b/Kernel/ELiteralSelector.hpp index 55cae1747..2d150fcd3 100644 --- a/Kernel/ELiteralSelector.hpp +++ b/Kernel/ELiteralSelector.hpp @@ -32,7 +32,6 @@ class ELiteralSelector : public LiteralSelector { public: - CLASS_NAME(ELiteralSelector); USE_ALLOCATOR(ELiteralSelector); enum Values { diff --git a/Kernel/Formula.hpp b/Kernel/Formula.hpp index cbeb48451..2f7080806 100644 --- a/Kernel/Formula.hpp +++ b/Kernel/Formula.hpp @@ -105,7 +105,6 @@ class Formula // use allocator to (de)allocate objects of this class - CLASS_NAME(Formula); USE_ALLOCATOR(Formula); protected: @@ -132,7 +131,6 @@ class NamedFormula public: explicit NamedFormula(vstring name) : Formula(NAME), _name(name) {} - CLASS_NAME(NamedFormula); USE_ALLOCATOR(NamedFormula); vstring name(){ return _name; } @@ -162,7 +160,6 @@ class AtomicFormula Literal* getLiteral() { return _literal; } // use allocator to (de)allocate objects of this class - CLASS_NAME(AtomicFormula); USE_ALLOCATOR(AtomicFormula); protected: /** The literal of this formula */ @@ -206,7 +203,6 @@ class QuantifiedFormula SList** sortListPtr() { return &_sorts; } // use allocator to (de)allocate objects of this class - CLASS_NAME(QuantifiedFormula); USE_ALLOCATOR(QuantifiedFormula); protected: /** list of variables */ @@ -237,7 +233,6 @@ class NegatedFormula Formula* subformula() { return _arg; } // use allocator to (de)allocate objects of this class - CLASS_NAME(NegatedFormula); USE_ALLOCATOR(NegatedFormula); protected: /** The immediate subformula */ @@ -277,7 +272,6 @@ class BinaryFormula } // use allocator to (de)allocate objects of this class - CLASS_NAME(BinaryFormula); USE_ALLOCATOR(BinaryFormula); protected: /** The lhs subformula */ @@ -316,7 +310,6 @@ class JunctionFormula static Formula* generalJunction(Connective c, FormulaList* args); // use allocator to (de)allocate objects of this class - CLASS_NAME(JunctionFormula); USE_ALLOCATOR(JunctionFormula); protected: /** list of immediate subformulas */ @@ -372,7 +365,6 @@ class BoolTermFormula TermList getTerm() { return _ts; } // use allocator to (de)allocate objects of this class - CLASS_NAME(BoolTermFormula); USE_ALLOCATOR(BoolTermFormula); protected: /** boolean term */ diff --git a/Kernel/FormulaUnit.hpp b/Kernel/FormulaUnit.hpp index 5698bac39..0d55762c1 100644 --- a/Kernel/FormulaUnit.hpp +++ b/Kernel/FormulaUnit.hpp @@ -56,7 +56,6 @@ class FormulaUnit Color getColor(); unsigned weight(); - CLASS_NAME(FormulaUnit); USE_ALLOCATOR(FormulaUnit); protected: diff --git a/Kernel/Grounder.hpp b/Kernel/Grounder.hpp index f6919c845..62560fa55 100644 --- a/Kernel/Grounder.hpp +++ b/Kernel/Grounder.hpp @@ -30,7 +30,6 @@ using namespace SAT; class Grounder { public: - CLASS_NAME(Grounder); USE_ALLOCATOR(Grounder); Grounder(SATSolver* satSolver) : _satSolver(satSolver) {} @@ -70,7 +69,6 @@ class GlobalSubsumptionGrounder : public Grounder { bool _doNormalization; public: - CLASS_NAME(GlobalSubsumptionGrounder); USE_ALLOCATOR(GlobalSubsumptionGrounder); GlobalSubsumptionGrounder(SATSolver* satSolver, bool doNormalization=true) @@ -81,7 +79,6 @@ class GlobalSubsumptionGrounder : public Grounder { class IGGrounder : public Grounder { public: - CLASS_NAME(IGGrounder); USE_ALLOCATOR(IGGrounder); IGGrounder(SATSolver* satSolver); diff --git a/Kernel/Inference.cpp b/Kernel/Inference.cpp index 688f0d501..233fa726e 100644 --- a/Kernel/Inference.cpp +++ b/Kernel/Inference.cpp @@ -60,7 +60,6 @@ UnitInputType Kernel::getInputType(UnitList* units) * To be kept around in _ptr2 of INFERENCE_FROM_SAT_REFUTATION **/ struct FromSatRefutationInfo { - CLASS_NAME(FromSatRefutationInfo); USE_ALLOCATOR(FromSatRefutationInfo); FromSatRefutationInfo(const FromSatRefutation& fsr) : _satPremises(fsr._satPremises), _usedAssumptions(fsr._usedAssumptions) diff --git a/Kernel/Inference.hpp b/Kernel/Inference.hpp index 20b50c637..a6c7bc510 100644 --- a/Kernel/Inference.hpp +++ b/Kernel/Inference.hpp @@ -710,7 +710,6 @@ class Inference { private: // don't construct on the heap - CLASS_NAME(Inference); USE_ALLOCATOR(Inference); enum class Kind : unsigned char { diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp index 887c3ac1c..256e5c539 100644 --- a/Kernel/InferenceStore.cpp +++ b/Kernel/InferenceStore.cpp @@ -246,7 +246,6 @@ struct UnitNumberComparator struct InferenceStore::ProofPrinter { - CLASS_NAME(InferenceStore::ProofPrinter); USE_ALLOCATOR(InferenceStore::ProofPrinter); ProofPrinter(ostream& out, InferenceStore* is) @@ -427,7 +426,6 @@ struct InferenceStore::ProofPrinter struct InferenceStore::ProofPropertyPrinter : public InferenceStore::ProofPrinter { - CLASS_NAME(InferenceStore::ProofPropertyPrinter); USE_ALLOCATOR(InferenceStore::ProofPropertyPrinter); ProofPropertyPrinter(ostream& out, InferenceStore* is) : ProofPrinter(out,is) @@ -513,7 +511,6 @@ struct InferenceStore::ProofPropertyPrinter struct InferenceStore::TPTPProofPrinter : public InferenceStore::ProofPrinter { - CLASS_NAME(InferenceStore::TPTPProofPrinter); USE_ALLOCATOR(InferenceStore::TPTPProofPrinter); TPTPProofPrinter(ostream& out, InferenceStore* is) @@ -877,7 +874,6 @@ struct InferenceStore::TPTPProofPrinter struct InferenceStore::ProofCheckPrinter : public InferenceStore::ProofPrinter { - CLASS_NAME(InferenceStore::ProofCheckPrinter); USE_ALLOCATOR(InferenceStore::ProofCheckPrinter); ProofCheckPrinter(ostream& out, InferenceStore* is) diff --git a/Kernel/InferenceStore.hpp b/Kernel/InferenceStore.hpp index f56d871e5..106450656 100644 --- a/Kernel/InferenceStore.hpp +++ b/Kernel/InferenceStore.hpp @@ -38,7 +38,6 @@ using namespace Lib; class InferenceStore { public: - CLASS_NAME(InferenceStore); USE_ALLOCATOR(InferenceStore); static InferenceStore* instance(); diff --git a/Kernel/InterpretedLiteralEvaluator.cpp b/Kernel/InterpretedLiteralEvaluator.cpp index 842dd0af7..856fcf685 100644 --- a/Kernel/InterpretedLiteralEvaluator.cpp +++ b/Kernel/InterpretedLiteralEvaluator.cpp @@ -67,7 +67,6 @@ struct PredEvalResult { class InterpretedLiteralEvaluator::Evaluator { public: - CLASS_NAME(InterpretedLiteralEvaluator::Evaluator); USE_ALLOCATOR(InterpretedLiteralEvaluator::Evaluator); virtual ~Evaluator() {} @@ -131,7 +130,6 @@ template : public Evaluator { public: -CLASS_NAME(InterpretedLiteralEvaluator::ACFunEvaluator); USE_ALLOCATOR(InterpretedLiteralEvaluator::ACFunEvaluator); using ConstantType = typename AbelianGroup::ConstantType; diff --git a/Kernel/InterpretedLiteralEvaluator.hpp b/Kernel/InterpretedLiteralEvaluator.hpp index 764f2ef0f..7e5637963 100644 --- a/Kernel/InterpretedLiteralEvaluator.hpp +++ b/Kernel/InterpretedLiteralEvaluator.hpp @@ -31,7 +31,6 @@ class InterpretedLiteralEvaluator : private BottomUpTermTransformer { public: - CLASS_NAME(InterpretedLiteralEvaluator); USE_ALLOCATOR(InterpretedLiteralEvaluator); InterpretedLiteralEvaluator(bool doNormalize = true); diff --git a/Kernel/KBO.cpp b/Kernel/KBO.cpp index 8439a63c4..283866e7b 100644 --- a/Kernel/KBO.cpp +++ b/Kernel/KBO.cpp @@ -57,7 +57,6 @@ class KBO::State _varDiffs.reset(); } - CLASS_NAME(KBO::State); USE_ALLOCATOR(State); void traverse(Term* t1, Term* t2); diff --git a/Kernel/KBO.hpp b/Kernel/KBO.hpp index b23a28a44..61f7bf20a 100644 --- a/Kernel/KBO.hpp +++ b/Kernel/KBO.hpp @@ -127,7 +127,6 @@ class KBO : public PrecedenceOrdering { public: - CLASS_NAME(KBO); USE_ALLOCATOR(KBO); KBO(Problem& prb, const Options& opt); diff --git a/Kernel/KBOForEPR.hpp b/Kernel/KBOForEPR.hpp index b85c7d5ec..2089f1d5f 100644 --- a/Kernel/KBOForEPR.hpp +++ b/Kernel/KBOForEPR.hpp @@ -31,7 +31,6 @@ class KBOForEPR : public PrecedenceOrdering { public: - CLASS_NAME(KBOForEPR); USE_ALLOCATOR(KBOForEPR); KBOForEPR(Problem& prb, const Options& opt); diff --git a/Kernel/LPO.hpp b/Kernel/LPO.hpp index 4ce00de8a..aa927f85e 100644 --- a/Kernel/LPO.hpp +++ b/Kernel/LPO.hpp @@ -33,7 +33,6 @@ class LPO : public PrecedenceOrdering { public: - CLASS_NAME(LPO); USE_ALLOCATOR(LPO); LPO(Problem& prb, const Options& opt) : diff --git a/Kernel/LiteralSelector.hpp b/Kernel/LiteralSelector.hpp index bab554cb1..7610d7fed 100644 --- a/Kernel/LiteralSelector.hpp +++ b/Kernel/LiteralSelector.hpp @@ -36,7 +36,6 @@ using namespace Shell; class LiteralSelector { public: - CLASS_NAME(LiteralSelector); USE_ALLOCATOR(LiteralSelector); LiteralSelector(const Ordering& ordering, const Options& options) @@ -123,7 +122,6 @@ class TotalLiteralSelector : public LiteralSelector { public: - CLASS_NAME(TotalLiteralSelector); USE_ALLOCATOR(TotalLiteralSelector); TotalLiteralSelector(const Ordering& ordering, const Options& options) diff --git a/Kernel/LookaheadLiteralSelector.hpp b/Kernel/LookaheadLiteralSelector.hpp index a173ec132..5f5f5c2ef 100644 --- a/Kernel/LookaheadLiteralSelector.hpp +++ b/Kernel/LookaheadLiteralSelector.hpp @@ -25,7 +25,6 @@ class LookaheadLiteralSelector : public LiteralSelector { public: - CLASS_NAME(LookaheadLiteralSelector); USE_ALLOCATOR(LookaheadLiteralSelector); LookaheadLiteralSelector(bool completeSelection, const Ordering& ordering, const Options& options) diff --git a/Kernel/MLMatcher.cpp b/Kernel/MLMatcher.cpp index 70e40d0db..e0180abe8 100644 --- a/Kernel/MLMatcher.cpp +++ b/Kernel/MLMatcher.cpp @@ -357,7 +357,6 @@ using namespace Lib; class MLMatcher::Impl final { public: - CLASS_NAME(MLMatcher::Impl); USE_ALLOCATOR(MLMatcher::Impl); Impl(); diff --git a/Kernel/MLMatcherSD.cpp b/Kernel/MLMatcherSD.cpp index 008daffe2..7bb325908 100644 --- a/Kernel/MLMatcherSD.cpp +++ b/Kernel/MLMatcherSD.cpp @@ -701,7 +701,6 @@ using namespace Lib; class MLMatcherSD::Impl final { public: - CLASS_NAME(MLMatcherSD::Impl); USE_ALLOCATOR(MLMatcherSD::Impl); Impl(); diff --git a/Kernel/MainLoop.hpp b/Kernel/MainLoop.hpp index e54147fac..65f789384 100644 --- a/Kernel/MainLoop.hpp +++ b/Kernel/MainLoop.hpp @@ -54,7 +54,6 @@ struct MainLoopResult class MainLoop { public: - CLASS_NAME(MainLoop); USE_ALLOCATOR(MainLoop); MainLoop(Problem& prb, const Options& opt) : _prb(prb), _opt(opt) {} diff --git a/Kernel/Matcher.hpp b/Kernel/Matcher.hpp index 65d5432c4..372995809 100644 --- a/Kernel/Matcher.hpp +++ b/Kernel/Matcher.hpp @@ -266,7 +266,6 @@ class Matcher void backtrack() { ALWAYS(_map->remove(_var)); } - CLASS_NAME(Matcher::MapBinder::BindingBacktrackObject); USE_ALLOCATOR(BindingBacktrackObject); private: BindingMap* _map; diff --git a/Kernel/MaximalLiteralSelector.hpp b/Kernel/MaximalLiteralSelector.hpp index a6aa61c07..d1149d447 100644 --- a/Kernel/MaximalLiteralSelector.hpp +++ b/Kernel/MaximalLiteralSelector.hpp @@ -34,7 +34,6 @@ class MaximalLiteralSelector : public LiteralSelector { public: - CLASS_NAME(MaximalLiteralSelector); USE_ALLOCATOR(MaximalLiteralSelector); MaximalLiteralSelector(const Ordering& ordering, const Options& options) : LiteralSelector(ordering, options) {} diff --git a/Kernel/MismatchHandler.hpp b/Kernel/MismatchHandler.hpp index 369073841..0dffedb3f 100644 --- a/Kernel/MismatchHandler.hpp +++ b/Kernel/MismatchHandler.hpp @@ -35,7 +35,6 @@ class UWAMismatchHandler : public MismatchHandler UWAMismatchHandler(Stack& c) : constraints(c) /*, specialVar(0)*/ {} virtual bool handle(RobSubstitution* sub, TermList t1, unsigned index1, TermList t2, unsigned index2); - CLASS_NAME(UWAMismatchHandler); USE_ALLOCATOR(UWAMismatchHandler); private: @@ -53,7 +52,6 @@ class HOMismatchHandler : public MismatchHandler virtual bool handle(RobSubstitution* sub, TermList t1, unsigned index1, TermList t2, unsigned index2); - CLASS_NAME(HOMismatchHandler); USE_ALLOCATOR(HOMismatchHandler); private: diff --git a/Kernel/OperatorType.hpp b/Kernel/OperatorType.hpp index 82f36895f..4435dacc1 100644 --- a/Kernel/OperatorType.hpp +++ b/Kernel/OperatorType.hpp @@ -55,7 +55,6 @@ namespace Kernel { class OperatorType { public: - CLASS_NAME(OperatorType); USE_ALLOCATOR(OperatorType); class TypeHash { diff --git a/Kernel/Ordering.hpp b/Kernel/Ordering.hpp index 0e9211eef..ee2995a9d 100644 --- a/Kernel/Ordering.hpp +++ b/Kernel/Ordering.hpp @@ -39,7 +39,6 @@ using namespace Shell; class Ordering { public: - CLASS_NAME(Ordering); USE_ALLOCATOR(Ordering); /** diff --git a/Kernel/Ordering_Equality.cpp b/Kernel/Ordering_Equality.cpp index 52c17d7a6..9ddbc2877 100644 --- a/Kernel/Ordering_Equality.cpp +++ b/Kernel/Ordering_Equality.cpp @@ -24,7 +24,6 @@ namespace Kernel class Ordering::EqCmp { public: - CLASS_NAME(EqCmp); USE_ALLOCATOR(EqCmp); EqCmp(Ordering* ordering) : _ordering(ordering) diff --git a/Kernel/Polynomial.hpp b/Kernel/Polynomial.hpp index 4425b6dde..636890622 100644 --- a/Kernel/Polynomial.hpp +++ b/Kernel/Polynomial.hpp @@ -133,7 +133,6 @@ class AnyPoly; template struct Monom { - CLASS_NAME(Monom) USE_ALLOCATOR(Monom) using Numeral = typename Number::ConstantType; @@ -160,7 +159,6 @@ class FuncTerm FuncId _fun; Stack _args; public: - CLASS_NAME(FuncTerm) USE_ALLOCATOR(FuncTerm) FuncTerm(FuncId f, Stack&& args); @@ -230,7 +228,6 @@ using PolyNfSuper = Lib::Coproduct, Variable, AnyPoly>; class PolyNf : public PolyNfSuper { public: - CLASS_NAME(PolyNf) PolyNf(Perfect t); PolyNf(Variable t); @@ -291,7 +288,6 @@ class PolyNf : public PolyNfSuper template struct MonomFactor { - CLASS_NAME(MonomFactor) PolyNf term; int power; @@ -317,7 +313,6 @@ class MonomFactors friend struct std::hash; public: - CLASS_NAME(MonomFactors) USE_ALLOCATOR(MonomFactors) /** @@ -406,7 +401,6 @@ class Polynom public: USE_ALLOCATOR(Polynom) - CLASS_NAME(Polynom) /** * constructs a new Polynom with a list of summands diff --git a/Kernel/Problem.hpp b/Kernel/Problem.hpp index 8f62ca865..62c89deff 100644 --- a/Kernel/Problem.hpp +++ b/Kernel/Problem.hpp @@ -50,7 +50,6 @@ class Problem { Problem& operator=(const Problem&); //private and undefined assignment operator public: - CLASS_NAME(Problem); USE_ALLOCATOR(Problem); explicit Problem(UnitList* units=0); diff --git a/Kernel/Renaming.hpp b/Kernel/Renaming.hpp index 36b2285d5..58975ad3a 100644 --- a/Kernel/Renaming.hpp +++ b/Kernel/Renaming.hpp @@ -33,7 +33,6 @@ using namespace Lib; class Renaming { public: - CLASS_NAME(Renaming); USE_ALLOCATOR(Renaming); Renaming() : diff --git a/Kernel/RndLiteralSelector.hpp b/Kernel/RndLiteralSelector.hpp index 4a7f4335e..729d7435a 100644 --- a/Kernel/RndLiteralSelector.hpp +++ b/Kernel/RndLiteralSelector.hpp @@ -32,7 +32,6 @@ class RndLiteralSelector : public LiteralSelector { public: - CLASS_NAME(RndLiteralSelector); USE_ALLOCATOR(RndLiteralSelector); RndLiteralSelector(const Ordering& ordering, const Options& options, bool complete) : diff --git a/Kernel/RobSubstitution.hpp b/Kernel/RobSubstitution.hpp index 26483cf7c..adb72c19d 100644 --- a/Kernel/RobSubstitution.hpp +++ b/Kernel/RobSubstitution.hpp @@ -37,7 +37,6 @@ class RobSubstitution :public Backtrackable { public: - CLASS_NAME(RobSubstitution); USE_ALLOCATOR(RobSubstitution); RobSubstitution() : _funcSubtermMap(nullptr), _nextUnboundAvailable(0) {} @@ -285,7 +284,6 @@ class RobSubstitution } friend std::ostream& operator<<(std::ostream& out, BindingBacktrackObject const& self) { return out << "(ROB backtrack object for " << self._var << ")"; } - CLASS_NAME(RobSubstitution::BindingBacktrackObject); USE_ALLOCATOR(BindingBacktrackObject); private: RobSubstitution* _subst; diff --git a/Kernel/SKIKBO.cpp b/Kernel/SKIKBO.cpp index 63f53eac6..9bba41347 100644 --- a/Kernel/SKIKBO.cpp +++ b/Kernel/SKIKBO.cpp @@ -58,7 +58,6 @@ class SKIKBO::State _varDiffs.reset(); } - CLASS_NAME(SKIKBO::State); USE_ALLOCATOR(State); void traverse(ArgsIt_ptr aai1, ArgsIt_ptr aai2); diff --git a/Kernel/SKIKBO.hpp b/Kernel/SKIKBO.hpp index 7b260c314..aaa94d2f6 100644 --- a/Kernel/SKIKBO.hpp +++ b/Kernel/SKIKBO.hpp @@ -40,7 +40,6 @@ class SKIKBO : public PrecedenceOrdering { public: - CLASS_NAME(SKIKBO); USE_ALLOCATOR(SKIKBO); SKIKBO(Problem& prb, const Options& opt, bool basic_hol = false); diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp index 894754e21..d1d14c275 100644 --- a/Kernel/Signature.hpp +++ b/Kernel/Signature.hpp @@ -316,7 +316,6 @@ class Signature OperatorType* predType() const; OperatorType* typeConType() const; - CLASS_NAME(Signature::Symbol); USE_ALLOCATOR(Symbol); }; // class Symbol @@ -335,7 +334,6 @@ class Signature { } - CLASS_NAME(Signature::InterpretedSymbol); USE_ALLOCATOR(InterpretedSymbol); /** Return the interpreted function that corresponds to this symbol */ @@ -356,7 +354,6 @@ class Signature { setType(OperatorType::getConstantsType(AtomicSort::intSort())); } - CLASS_NAME(Signature::IntegerSymbol); USE_ALLOCATOR(IntegerSymbol); }; @@ -374,7 +371,6 @@ class Signature { setType(OperatorType::getConstantsType(AtomicSort::rationalSort())); } - CLASS_NAME(Signature::RationalSymbol); USE_ALLOCATOR(RationalSymbol); }; @@ -392,7 +388,6 @@ class Signature { setType(OperatorType::getConstantsType(AtomicSort::realSort())); } - CLASS_NAME(Signature::RealSymbol); USE_ALLOCATOR(RealSymbol); }; @@ -580,7 +575,6 @@ class Signature Signature(); ~Signature(); - CLASS_NAME(Signature); USE_ALLOCATOR(Signature); bool functionExists(const vstring& name,unsigned arity) const; diff --git a/Kernel/SpassLiteralSelector.hpp b/Kernel/SpassLiteralSelector.hpp index f45faf56f..95a1a6fdf 100644 --- a/Kernel/SpassLiteralSelector.hpp +++ b/Kernel/SpassLiteralSelector.hpp @@ -32,7 +32,6 @@ class SpassLiteralSelector : public LiteralSelector { public: - CLASS_NAME(SpassLiteralSelector); USE_ALLOCATOR(SpassLiteralSelector); enum Values { diff --git a/Kernel/SubformulaIterator.cpp b/Kernel/SubformulaIterator.cpp index 2671fc77b..c1aad4bae 100644 --- a/Kernel/SubformulaIterator.cpp +++ b/Kernel/SubformulaIterator.cpp @@ -67,7 +67,6 @@ class SubformulaIterator::Element { int _polarity; Element* _rest; - CLASS_NAME(SubformulaIterator::Element); USE_ALLOCATOR(SubformulaIterator::Element); }; diff --git a/Kernel/Substitution.hpp b/Kernel/Substitution.hpp index 80f60ab13..229a3b09a 100644 --- a/Kernel/Substitution.hpp +++ b/Kernel/Substitution.hpp @@ -38,7 +38,6 @@ using namespace Lib; class Substitution { public: - CLASS_NAME(Substitution); USE_ALLOCATOR(Substitution); Substitution() {} diff --git a/Kernel/Term.hpp b/Kernel/Term.hpp index 775975e31..f60426357 100644 --- a/Kernel/Term.hpp +++ b/Kernel/Term.hpp @@ -90,7 +90,6 @@ bool operator<(const TermList& lhs, const TermList& rhs); */ class TermList { public: - CLASS_NAME(TermList) // divide by 4 because of the tag, by 2 to split the space evenly static const unsigned SPEC_UPPER_BOUND = (UINT_MAX / 4) / 2; /** dummy constructor, does nothing */ diff --git a/Kernel/Theory.hpp b/Kernel/Theory.hpp index d0588905c..f645168ec 100644 --- a/Kernel/Theory.hpp +++ b/Kernel/Theory.hpp @@ -57,7 +57,6 @@ class DivByZeroException : public ArithmeticException class IntegerConstantType { public: - CLASS_NAME(IntegerConstantType) static TermList getSort() { return AtomicSort::intSort(); } typedef int InnerType; @@ -135,7 +134,6 @@ std::ostream& operator<< (std::ostream& out, const IntegerConstantType& val) { */ struct RationalConstantType { typedef IntegerConstantType InnerType; - CLASS_NAME(RationalConstantType) static TermList getSort() { return AtomicSort::rationalSort(); } @@ -208,7 +206,6 @@ std::ostream& operator<< (std::ostream& out, const RationalConstantType& val) { class RealConstantType : public RationalConstantType { public: - CLASS_NAME(RealConstantType) static TermList getSort() { return AtomicSort::realSort(); } RealConstantType() {} diff --git a/Kernel/TypedTermList.hpp b/Kernel/TypedTermList.hpp index ad9af1b3f..245cba167 100644 --- a/Kernel/TypedTermList.hpp +++ b/Kernel/TypedTermList.hpp @@ -20,7 +20,6 @@ class TypedTermList : public TermList { SortId _sort; public: - CLASS_NAME(TypedTermList) TypedTermList(TermList t, SortId sort) : TermList(t), _sort(sort) { ASS_NEQ(sort, AtomicSort::superSort()) } TypedTermList(Term* t) : TypedTermList(TermList(t), SortHelper::getResultSort(t)) {} diff --git a/Lib/Allocator.hpp b/Lib/Allocator.hpp index 7edddb375..a822a2570 100644 --- a/Lib/Allocator.hpp +++ b/Lib/Allocator.hpp @@ -304,7 +304,6 @@ inline void free(void *pointer, size_t size) { #define START_CHECKING_FOR_ALLOCATOR_BYPASSES #define STOP_CHECKING_FOR_ALLOCATOR_BYPASSES #define USE_ALLOCATOR(C) USE_GLOBAL_SMALL_OBJECT_ALLOCATOR(C) -#define CLASS_NAME(className) #define ALLOC_KNOWN(size, className) Lib::alloc(size) #define DEALLOC_KNOWN(ptr, size, className) Lib::free(ptr, size) #define ALLOC_UNKNOWN(size, className) Lib::deprecatedAlloc(size) diff --git a/Lib/ArrayMap.hpp b/Lib/ArrayMap.hpp index 46859d7d4..0d4eaf22e 100644 --- a/Lib/ArrayMap.hpp +++ b/Lib/ArrayMap.hpp @@ -48,7 +48,6 @@ class ArrayMap { typedef ArrayMapEntry Entry; public: - CLASS_NAME(ArrayMap); USE_ALLOCATOR(ArrayMap); /** diff --git a/Lib/BinaryHeap.hpp b/Lib/BinaryHeap.hpp index a341e4cdf..5034f6ce8 100644 --- a/Lib/BinaryHeap.hpp +++ b/Lib/BinaryHeap.hpp @@ -230,7 +230,6 @@ class BinaryHeap { _bh->backtrackPop(_val,_lastBubbleIndex); } - CLASS_NAME(BinaryHeap::BHPopBacktrackObject); USE_ALLOCATOR(BHPopBacktrackObject); private: BinaryHeap* _bh; @@ -248,7 +247,6 @@ class BinaryHeap { _bh->backtrackInsert(_lastBubbleIndex); } - CLASS_NAME(BinaryHeap::BHInsertBacktrackObject); USE_ALLOCATOR(BHInsertBacktrackObject); private: BinaryHeap* _bh; diff --git a/Lib/Coproduct.hpp b/Lib/Coproduct.hpp index 598990f7b..105b5b6ee 100644 --- a/Lib/Coproduct.hpp +++ b/Lib/Coproduct.hpp @@ -48,7 +48,6 @@ namespace CoproductImpl { * data VariadicUnion [] = bottom type */ template<> union VariadicUnion<> { - CLASS_NAME(VariadicUnion) inline void unwrap(unsigned idx) { ASSERTION_VIOLATION_REP(idx) } ~VariadicUnion() {} @@ -76,7 +75,6 @@ namespace CoproductImpl { * data VariadicUnion (a::as) = union {a, Coproduct as} */ template union VariadicUnion { - CLASS_NAME(VariadicUnion) // USE_ALLOCATOR(VariadicUnion) using Ts = TL::List; @@ -278,7 +276,6 @@ class Coproduct Coproduct() : _tag(std::numeric_limits::max()) {} public: - CLASS_NAME(Coproduct) /** a type-level list of all types of this Coproduct */ using Ts = TL::List; diff --git a/Lib/DArray.hpp b/Lib/DArray.hpp index 0b02dac08..19bf6515a 100644 --- a/Lib/DArray.hpp +++ b/Lib/DArray.hpp @@ -42,7 +42,6 @@ class DArray //private and undefined operator= to avoid an implicitly generated one DArray& operator=(const DArray&); public: - CLASS_NAME(DArray); USE_ALLOCATOR(DArray); class Iterator; diff --git a/Lib/DHMap.hpp b/Lib/DHMap.hpp index 06fbe267a..b677cb7f8 100644 --- a/Lib/DHMap.hpp +++ b/Lib/DHMap.hpp @@ -57,7 +57,6 @@ template class DHMap { public: - CLASS_NAME(DHMap); USE_ALLOCATOR(DHMap); /** Create a new DHMap */ diff --git a/Lib/DHMultiset.hpp b/Lib/DHMultiset.hpp index ac3fcf49d..d8b4406ec 100644 --- a/Lib/DHMultiset.hpp +++ b/Lib/DHMultiset.hpp @@ -52,7 +52,6 @@ template class DHMultiset { public: - CLASS_NAME(DHMultiset); USE_ALLOCATOR(DHMultiset); /** Create a new DHMultiset */ diff --git a/Lib/DHSet.hpp b/Lib/DHSet.hpp index 1abfe6058..6570b05f5 100644 --- a/Lib/DHSet.hpp +++ b/Lib/DHSet.hpp @@ -38,7 +38,6 @@ template class DHSet { public: - CLASS_NAME(DHSet); USE_ALLOCATOR(DHSet); /** Empty the DHSet */ diff --git a/Lib/Event.hpp b/Lib/Event.hpp index 9041c5b4f..084d6557a 100644 --- a/Lib/Event.hpp +++ b/Lib/Event.hpp @@ -68,7 +68,6 @@ class SubscriptionObject void unsubscribe(); bool belongsTo(BaseEvent& evt); - CLASS_NAME(SubscriptionObject); USE_ALLOCATOR(SubscriptionObject); private: BaseEvent* event; @@ -111,7 +110,6 @@ class PlainEvent { (pObj->*pMethod)(); } - CLASS_NAME(PlainEvent::MethodSpecificHandlerStruct); USE_ALLOCATOR(MethodSpecificHandlerStruct); }; @@ -162,7 +160,6 @@ class SingleParamEvent (pObj->*pMethod)(t); } - CLASS_NAME(MethodSpecificHandlerStruct); USE_ALLOCATOR(MethodSpecificHandlerStruct); }; @@ -216,7 +213,6 @@ class TwoParamEvent (pObj->*pMethod)(t1, t2); } - CLASS_NAME("TwoParamEvent::MethodSpecificHandlerStruct"); USE_ALLOCATOR(MethodSpecificHandlerStruct); }; diff --git a/Lib/InverseLookup.hpp b/Lib/InverseLookup.hpp index d9a2898c6..9a849321c 100644 --- a/Lib/InverseLookup.hpp +++ b/Lib/InverseLookup.hpp @@ -31,7 +31,6 @@ class InverseLookup InverseLookup(const InverseLookup&); InverseLookup& operator=(const InverseLookup&); public: - CLASS_NAME(InverseLookup); USE_ALLOCATOR(InverseLookup); template diff --git a/Lib/List.hpp b/Lib/List.hpp index 400d629a5..46b4d4445 100644 --- a/Lib/List.hpp +++ b/Lib/List.hpp @@ -468,7 +468,6 @@ class List /** iterator over the list elements */ class Iterator { public: - CLASS_NAME(List::Iterator); USE_ALLOCATOR(List::Iterator); DECL_ELEMENT_TYPE(C); @@ -510,7 +509,6 @@ class List /** iterator over references to list elements */ class RefIterator { public: - CLASS_NAME(List::RefIterator); USE_ALLOCATOR(List::RefIterator); DECL_ELEMENT_TYPE(C&); @@ -541,7 +539,6 @@ class List class PtrIterator { public: - CLASS_NAME(List::PtrIterator); USE_ALLOCATOR(List::PtrIterator); DECL_ELEMENT_TYPE(C*); @@ -563,7 +560,6 @@ class List /** Iterator that allows one to delete the current element */ class DelIterator { public: - CLASS_NAME(List::DelIterator); USE_ALLOCATOR(List::DelIterator); DECL_ELEMENT_TYPE(C); @@ -701,7 +697,6 @@ class List */ class DestructiveIterator { public: - CLASS_NAME(List::DestructiveIterator); USE_ALLOCATOR(List::DestructiveIterator); DECL_ELEMENT_TYPE(C); @@ -729,7 +724,6 @@ class List }; // use allocator to (de)allocate objects of this class - CLASS_NAME(List); USE_ALLOCATOR(List); /** diff --git a/Lib/Set.hpp b/Lib/Set.hpp index 030d1173f..ed8e01bcf 100644 --- a/Lib/Set.hpp +++ b/Lib/Set.hpp @@ -83,7 +83,6 @@ class Set public: // use allocator to (de)allocate objects of this class - CLASS_NAME(Set); USE_ALLOCATOR(Set); /** Create a new Set */ diff --git a/Lib/SkipList.hpp b/Lib/SkipList.hpp index 3aa942352..eac9b161c 100644 --- a/Lib/SkipList.hpp +++ b/Lib/SkipList.hpp @@ -41,7 +41,6 @@ template class SkipList { public: - CLASS_NAME(SkipList); USE_ALLOCATOR(SkipList); class Node { diff --git a/Lib/SmartPtr.hpp b/Lib/SmartPtr.hpp index ad461e59f..9f4cfec83 100644 --- a/Lib/SmartPtr.hpp +++ b/Lib/SmartPtr.hpp @@ -30,7 +30,6 @@ template class SmartPtr { private: struct RefCounter { - CLASS_NAME(SmartPtr::RefCounter); USE_ALLOCATOR(SmartPtr::RefCounter); inline explicit RefCounter(int v) : _val(v) {} diff --git a/Lib/Stack.hpp b/Lib/Stack.hpp index 1aa7c01c4..a3b7a34e7 100644 --- a/Lib/Stack.hpp +++ b/Lib/Stack.hpp @@ -54,7 +54,6 @@ class Stack DECL_ELEMENT_TYPE(C); DECL_ITERATOR_TYPE(Iterator); - CLASS_NAME(Stack); USE_ALLOCATOR(Stack); /** @@ -788,7 +787,6 @@ class Stack { Stack* st; public: - CLASS_NAME(Stack::PushBacktrackObject); USE_ALLOCATOR(Stack::PushBacktrackObject); PushBacktrackObject(Stack* st) : st(st) {} diff --git a/Lib/Timer.hpp b/Lib/Timer.hpp index 31383ee6a..342f43500 100644 --- a/Lib/Timer.hpp +++ b/Lib/Timer.hpp @@ -36,7 +36,6 @@ class Timer ~Timer() { deinitializeTimer(); } public: - CLASS_NAME(Timer); USE_ALLOCATOR(Timer); static Timer* instance(); diff --git a/Lib/VString.hpp b/Lib/VString.hpp index 37234a751..68f252104 100644 --- a/Lib/VString.hpp +++ b/Lib/VString.hpp @@ -31,7 +31,6 @@ namespace Lib { typedef std::basic_ostringstream,STLAllocator > vostringstream_base; struct vostringstream : public vostringstream_base { - CLASS_NAME(vostringstream); USE_ALLOCATOR(vostringstream); // inherit parent's constructors (c++11) @@ -42,7 +41,6 @@ struct vostringstream : public vostringstream_base { typedef std::basic_istringstream,STLAllocator > vistringstream_base; struct vistringstream : public vistringstream_base { - CLASS_NAME(vistringstream); USE_ALLOCATOR(vistringstream); // inherit parent's constructors (c++11) @@ -53,7 +51,6 @@ struct vistringstream : public vistringstream_base { typedef std::basic_stringstream,STLAllocator > vstringstream_base; struct vstringstream : public vstringstream_base { - CLASS_NAME(vstringstream); USE_ALLOCATOR(vstringstream); // inherit parent's constructors (c++11) diff --git a/Lib/VirtualIterator.hpp b/Lib/VirtualIterator.hpp index 3aab65878..712b18358 100644 --- a/Lib/VirtualIterator.hpp +++ b/Lib/VirtualIterator.hpp @@ -81,8 +81,6 @@ class IteratorCore { */ virtual size_t size() const { INVALID_OPERATION("This iterator cannot retrieve its size."); } - CLASS_NAME(IteratorCore); -// CLASS_NAME(typeid(IteratorCore).name()); private: /** * Reference counter field used by the @b VirtualIterator object @@ -101,7 +99,6 @@ class EmptyIterator : public IteratorCore { public: - CLASS_NAME(EmptyIterator); USE_ALLOCATOR(EmptyIterator); EmptyIterator() {} @@ -126,7 +123,6 @@ class EmptyIterator template class VirtualIterator { public: - CLASS_NAME(VirtualIterator); USE_ALLOCATOR(VirtualIterator); DECL_ELEMENT_TYPE(T); @@ -298,7 +294,6 @@ class ProxyIterator : public IteratorCore { public: - CLASS_NAME(ProxyIterator); USE_ALLOCATOR(ProxyIterator); explicit ProxyIterator(Inner inn) : _inn(std::move(inn)) {} diff --git a/Parse/TPTP.hpp b/Parse/TPTP.hpp index 7b308cef8..5c1b33652 100644 --- a/Parse/TPTP.hpp +++ b/Parse/TPTP.hpp @@ -355,7 +355,6 @@ class TPTP */ class Type { public: - CLASS_NAME(Type); USE_ALLOCATOR(Type); explicit Type(TypeTag tag) : _tag(tag) {} /** return the kind of this sort */ @@ -370,7 +369,6 @@ class TPTP : public Type { public: - CLASS_NAME(AtomicType); USE_ALLOCATOR(AtomicType); explicit AtomicType(TermList sort) : Type(TT_ATOMIC), _sort(sort) @@ -387,7 +385,6 @@ class TPTP : public Type { public: - CLASS_NAME(ArrowType); USE_ALLOCATOR(ArrowType); ArrowType(Type* lhs,Type* rhs) : Type(TT_ARROW), _lhs(lhs), _rhs(rhs) @@ -411,7 +408,6 @@ class TPTP : public Type { public: - CLASS_NAME(ProductType); USE_ALLOCATOR(ProductType); ProductType(Type* lhs,Type* rhs) : Type(TT_PRODUCT), _lhs(lhs), _rhs(rhs) @@ -433,7 +429,6 @@ class TPTP : public Type { public: - CLASS_NAME(QuantifiedType); USE_ALLOCATOR(QuantifiedType); QuantifiedType(Type* t, VList* vars) : Type(TT_QUANTIFIED), _type(t), _vars(vars) diff --git a/SAT/BufferedSolver.hpp b/SAT/BufferedSolver.hpp index 620da45f2..cc4d44506 100644 --- a/SAT/BufferedSolver.hpp +++ b/SAT/BufferedSolver.hpp @@ -35,7 +35,6 @@ using namespace Lib; class BufferedSolver : public SATSolver { public: - CLASS_NAME(BufferedSolver); USE_ALLOCATOR(BufferedSolver); BufferedSolver(SATSolver* inner); diff --git a/SAT/FallbackSolverWrapper.hpp b/SAT/FallbackSolverWrapper.hpp index a7980fd21..f169064fe 100644 --- a/SAT/FallbackSolverWrapper.hpp +++ b/SAT/FallbackSolverWrapper.hpp @@ -37,7 +37,6 @@ using namespace Lib; class FallbackSolverWrapper : public SATSolver { public: - CLASS_NAME(FallbackSolverWrapper); USE_ALLOCATOR(FallbackSolverWrapper); FallbackSolverWrapper(SATSolver* inner,SATSolver* fallback); diff --git a/SAT/MinimizingSolver.hpp b/SAT/MinimizingSolver.hpp index fe732aedb..dc9dae40b 100644 --- a/SAT/MinimizingSolver.hpp +++ b/SAT/MinimizingSolver.hpp @@ -36,7 +36,6 @@ using namespace Lib; class MinimizingSolver : public SATSolver { public: - CLASS_NAME(MinimizingSolver); USE_ALLOCATOR(MinimizingSolver); MinimizingSolver(SATSolver* inner); diff --git a/SAT/MinisatInterfacing.hpp b/SAT/MinisatInterfacing.hpp index 98ca9ab77..8af855be1 100644 --- a/SAT/MinisatInterfacing.hpp +++ b/SAT/MinisatInterfacing.hpp @@ -25,7 +25,6 @@ namespace SAT{ class MinisatInterfacing : public PrimitiveProofRecordingSATSolver { public: - CLASS_NAME(MinisatInterfacing); USE_ALLOCATOR(MinisatInterfacing); MinisatInterfacing(const Shell::Options& opts, bool generateProofs=false); diff --git a/SAT/MinisatInterfacingNewSimp.hpp b/SAT/MinisatInterfacingNewSimp.hpp index ffa79ad4b..e04c2e81b 100644 --- a/SAT/MinisatInterfacingNewSimp.hpp +++ b/SAT/MinisatInterfacingNewSimp.hpp @@ -30,7 +30,6 @@ namespace SAT{ class MinisatInterfacingNewSimp : public SATSolverWithAssumptions { public: - CLASS_NAME(MinisatInterfacingNewSimp); USE_ALLOCATOR(MinisatInterfacingNewSimp); static const unsigned VAR_MAX; diff --git a/SAT/SATInference.hpp b/SAT/SATInference.hpp index 0dc0cb773..4e9b59929 100644 --- a/SAT/SATInference.hpp +++ b/SAT/SATInference.hpp @@ -82,7 +82,6 @@ class SATInference class PropInference : public SATInference { public: - CLASS_NAME(PropInference); USE_ALLOCATOR(PropInference); PropInference(SATClauseList* premises) : _premises(premises) {} @@ -111,7 +110,6 @@ class PropInference : public SATInference class FOConversionInference : public SATInference { public: - CLASS_NAME(FOConversionInference); USE_ALLOCATOR(FOConversionInference); FOConversionInference(Unit* origin); @@ -127,7 +125,6 @@ class FOConversionInference : public SATInference class AssumptionInference : public SATInference { public: - CLASS_NAME(AssumptionInference); USE_ALLOCATOR(AssumptionInference); virtual InfType getType() const { return ASSUMPTION; } diff --git a/SAT/Z3Interfacing.hpp b/SAT/Z3Interfacing.hpp index b75c0af3d..dbde6b862 100644 --- a/SAT/Z3Interfacing.hpp +++ b/SAT/Z3Interfacing.hpp @@ -56,7 +56,6 @@ namespace SAT{ class Z3Interfacing : public PrimitiveProofRecordingSATSolver { public: - CLASS_NAME(Z3Interfacing); USE_ALLOCATOR(Z3Interfacing); Z3Interfacing(const Shell::Options& opts, SAT2FO& s2f, bool unsatCoresForAssumptions, vstring const& exportSmtlib); diff --git a/SAT/Z3MainLoop.hpp b/SAT/Z3MainLoop.hpp index ed4ef7d13..c25658500 100644 --- a/SAT/Z3MainLoop.hpp +++ b/SAT/Z3MainLoop.hpp @@ -38,7 +38,6 @@ using namespace Lib; class Z3MainLoop : public MainLoop { public: - CLASS_NAME(Z3MainLoop); USE_ALLOCATOR(Z3MainLoop); Z3MainLoop(Problem& prb, const Options& opt); diff --git a/Saturation/AWPassiveClauseContainer.hpp b/Saturation/AWPassiveClauseContainer.hpp index 8f1829795..ecc265059 100644 --- a/Saturation/AWPassiveClauseContainer.hpp +++ b/Saturation/AWPassiveClauseContainer.hpp @@ -65,7 +65,6 @@ class AWPassiveClauseContainer : public PassiveClauseContainer { public: - CLASS_NAME(AWPassiveClauseContainer); USE_ALLOCATOR(AWPassiveClauseContainer); AWPassiveClauseContainer(bool isOutermost, const Shell::Options& opt, vstring name); diff --git a/Saturation/ClauseContainer.hpp b/Saturation/ClauseContainer.hpp index a172d14c2..484813204 100644 --- a/Saturation/ClauseContainer.hpp +++ b/Saturation/ClauseContainer.hpp @@ -38,7 +38,6 @@ using namespace Shell; class ClauseContainer { public: - CLASS_NAME(ClauseContainer); USE_ALLOCATOR(ClauseContainer); virtual ~ClauseContainer() {} @@ -66,7 +65,6 @@ class RandomAccessClauseContainer : public ClauseContainer { public: - CLASS_NAME(RandomAccessClauseContainer); USE_ALLOCATOR(RandomAccessClauseContainer); virtual void attach(SaturationAlgorithm* salg); @@ -88,7 +86,6 @@ class RandomAccessClauseContainer class PlainClauseContainer : public ClauseContainer { public: - CLASS_NAME(PlainClauseContainer); USE_ALLOCATOR(PlainClauseContainer); void add(Clause* c) override @@ -102,7 +99,6 @@ class UnprocessedClauseContainer : public ClauseContainer { public: - CLASS_NAME(UnprocessedClauseContainer); USE_ALLOCATOR(UnprocessedClauseContainer); virtual ~UnprocessedClauseContainer(); @@ -121,7 +117,6 @@ class PassiveClauseContainer : public RandomAccessClauseContainer { public: - CLASS_NAME(PassiveClauseContainer); USE_ALLOCATOR(PassiveClauseContainer); PassiveClauseContainer(bool isOutermost, const Shell::Options& opt, vstring name = "") : _isOutermost(isOutermost), _opt(opt), _name(name) {} @@ -182,7 +177,6 @@ class ActiveClauseContainer : public RandomAccessClauseContainer { public: - CLASS_NAME(ActiveClauseContainer); USE_ALLOCATOR(ActiveClauseContainer); ActiveClauseContainer(const Shell::Options& opt) {} diff --git a/Saturation/ConsequenceFinder.hpp b/Saturation/ConsequenceFinder.hpp index 38684257c..97e6e3e76 100644 --- a/Saturation/ConsequenceFinder.hpp +++ b/Saturation/ConsequenceFinder.hpp @@ -39,7 +39,6 @@ using namespace Inferences; */ class ConsequenceFinder { public: - CLASS_NAME(ConsequenceFinder); USE_ALLOCATOR(ConsequenceFinder); ~ConsequenceFinder(); diff --git a/Saturation/Discount.hpp b/Saturation/Discount.hpp index 163e7fa7c..b8fa109de 100644 --- a/Saturation/Discount.hpp +++ b/Saturation/Discount.hpp @@ -28,7 +28,6 @@ class Discount : public SaturationAlgorithm { public: - CLASS_NAME(Discount); USE_ALLOCATOR(Discount); Discount(Problem& prb, const Options& opt) diff --git a/Saturation/ExtensionalityClauseContainer.hpp b/Saturation/ExtensionalityClauseContainer.hpp index 3d303c2b6..42783d364 100644 --- a/Saturation/ExtensionalityClauseContainer.hpp +++ b/Saturation/ExtensionalityClauseContainer.hpp @@ -49,7 +49,6 @@ typedef DHMap ClausesBySort; class ExtensionalityClauseContainer { public: - CLASS_NAME(ExtensionalityClauseContainer); USE_ALLOCATOR(ExtensionalityClauseContainer); ExtensionalityClauseContainer(const Options& opt) diff --git a/Saturation/LRS.hpp b/Saturation/LRS.hpp index 7da98b362..e276e61f4 100644 --- a/Saturation/LRS.hpp +++ b/Saturation/LRS.hpp @@ -30,7 +30,6 @@ class LRS : public Otter { public: - CLASS_NAME(LRS); USE_ALLOCATOR(LRS); LRS(Problem& prb, const Options& opt) diff --git a/Saturation/LabelFinder.hpp b/Saturation/LabelFinder.hpp index 46e92a0c5..8316c514a 100644 --- a/Saturation/LabelFinder.hpp +++ b/Saturation/LabelFinder.hpp @@ -32,7 +32,6 @@ using namespace Inferences; class LabelFinder { public: - CLASS_NAME(LabelFinder); USE_ALLOCATOR(LabelFinder); ~LabelFinder(); diff --git a/Saturation/ManCSPassiveClauseContainer.cpp b/Saturation/ManCSPassiveClauseContainer.cpp index 472e7543f..ebf1ccd34 100644 --- a/Saturation/ManCSPassiveClauseContainer.cpp +++ b/Saturation/ManCSPassiveClauseContainer.cpp @@ -27,7 +27,6 @@ using namespace Kernel; class VectorIteratorWrapper : public IteratorCore { public: - CLASS_NAME(VectorIteratorWrapper); USE_ALLOCATOR(VectorIteratorWrapper); explicit VectorIteratorWrapper(const std::vector& v) : curr(v.begin()), end(v.end()) {} diff --git a/Saturation/ManCSPassiveClauseContainer.hpp b/Saturation/ManCSPassiveClauseContainer.hpp index 541dfd3f7..2dc3bb262 100644 --- a/Saturation/ManCSPassiveClauseContainer.hpp +++ b/Saturation/ManCSPassiveClauseContainer.hpp @@ -31,7 +31,6 @@ using namespace Kernel; class ManCSPassiveClauseContainer : public PassiveClauseContainer { public: - CLASS_NAME(ManCSPassiveClauseContainer); USE_ALLOCATOR(ManCSPassiveClauseContainer); ManCSPassiveClauseContainer(bool isOutermost, const Shell::Options& opt) : PassiveClauseContainer(isOutermost, opt) {} diff --git a/Saturation/Otter.hpp b/Saturation/Otter.hpp index 0180ce092..0cac0607e 100644 --- a/Saturation/Otter.hpp +++ b/Saturation/Otter.hpp @@ -28,7 +28,6 @@ class Otter : public SaturationAlgorithm { public: - CLASS_NAME(Otter); USE_ALLOCATOR(Otter); Otter(Problem& prb, const Options& opt); diff --git a/Saturation/PredicateSplitPassiveClauseContainer.hpp b/Saturation/PredicateSplitPassiveClauseContainer.hpp index 794fc00c5..9d479d17a 100644 --- a/Saturation/PredicateSplitPassiveClauseContainer.hpp +++ b/Saturation/PredicateSplitPassiveClauseContainer.hpp @@ -23,7 +23,6 @@ class PredicateSplitPassiveClauseContainer : public PassiveClauseContainer { public: - CLASS_NAME(PredicateSplitPassiveClauseContainer); USE_ALLOCATOR(PredicateSplitPassiveClauseContainer); PredicateSplitPassiveClauseContainer(bool isOutermost, const Shell::Options& opt, vstring name, Lib::vvector> queues, Lib::vvector cutoffs, Lib::vvector ratios, bool layeredArrangement); diff --git a/Saturation/SaturationAlgorithm.hpp b/Saturation/SaturationAlgorithm.hpp index 4af640ae1..43bf36007 100644 --- a/Saturation/SaturationAlgorithm.hpp +++ b/Saturation/SaturationAlgorithm.hpp @@ -57,7 +57,6 @@ class Splitter; class SaturationAlgorithm : public MainLoop { public: - CLASS_NAME(SaturationAlgorithm); USE_ALLOCATOR(SaturationAlgorithm); static SaturationAlgorithm* createFromOptions(Problem& prb, const Options& opt, IndexManager* indexMgr=0); diff --git a/Saturation/Splitter.hpp b/Saturation/Splitter.hpp index 452aef13f..9bfc9ea5f 100644 --- a/Saturation/Splitter.hpp +++ b/Saturation/Splitter.hpp @@ -171,12 +171,10 @@ class Splitter { Stack reduced; bool active; - CLASS_NAME(Splitter::SplitRecord); USE_ALLOCATOR(SplitRecord); }; public: - CLASS_NAME(Splitter); USE_ALLOCATOR(Splitter); Splitter(); diff --git a/Saturation/SymElOutput.hpp b/Saturation/SymElOutput.hpp index c3a726bd5..fe197d5de 100644 --- a/Saturation/SymElOutput.hpp +++ b/Saturation/SymElOutput.hpp @@ -33,7 +33,6 @@ using namespace Shell; */ class SymElOutput { public: - CLASS_NAME(SymElOutput); USE_ALLOCATOR(SymElOutput); SymElOutput(); diff --git a/Shell/BlockedClauseElimination.hpp b/Shell/BlockedClauseElimination.hpp index bcd39fe53..d51a7e0ac 100644 --- a/Shell/BlockedClauseElimination.hpp +++ b/Shell/BlockedClauseElimination.hpp @@ -40,7 +40,6 @@ class BlockedClauseElimination struct ClWrapper; struct Candidate { - CLASS_NAME(BlockedClauseElimination::Candidate); USE_ALLOCATOR(Candidate); ClWrapper* clw; @@ -56,7 +55,6 @@ class BlockedClauseElimination }; struct ClWrapper { - CLASS_NAME(BlockedClauseElimination::ClWrapper); USE_ALLOCATOR(ClWrapper); Clause* cl; // the actual clause diff --git a/Shell/EqualityProxy.hpp b/Shell/EqualityProxy.hpp index ba5123fe7..ad3dbdd62 100644 --- a/Shell/EqualityProxy.hpp +++ b/Shell/EqualityProxy.hpp @@ -56,7 +56,6 @@ using namespace Kernel; class EqualityProxy { public: - CLASS_NAME(EqualityProxy); USE_ALLOCATOR(EqualityProxy); EqualityProxy(Options::EqualityProxy opt); diff --git a/Shell/EqualityProxyMono.hpp b/Shell/EqualityProxyMono.hpp index c940f6670..10311819a 100644 --- a/Shell/EqualityProxyMono.hpp +++ b/Shell/EqualityProxyMono.hpp @@ -55,7 +55,6 @@ using namespace Kernel; class EqualityProxyMono { public: - CLASS_NAME(EqualityProxyMono); USE_ALLOCATOR(EqualityProxyMono); EqualityProxyMono(Options::EqualityProxy opt); diff --git a/Shell/FunctionDefinition.cpp b/Shell/FunctionDefinition.cpp index d3a2bd64b..80bb76ebe 100644 --- a/Shell/FunctionDefinition.cpp +++ b/Shell/FunctionDefinition.cpp @@ -118,7 +118,6 @@ struct FunctionDefinition::Def } } - CLASS_NAME(FunctionDefinition::Def); USE_ALLOCATOR(Def); }; // class FunctionDefintion::Def diff --git a/Shell/GoalGuessing.hpp b/Shell/GoalGuessing.hpp index b4e3ed52d..7c27d37f0 100644 --- a/Shell/GoalGuessing.hpp +++ b/Shell/GoalGuessing.hpp @@ -25,7 +25,6 @@ using namespace Kernel; class GoalGuessing { public: - CLASS_NAME(GoalGuessing); USE_ALLOCATOR(GoalGuessing); void apply(Problem& prb); diff --git a/Shell/InterpretedNormalizer.cpp b/Shell/InterpretedNormalizer.cpp index 00b8c19ac..b73660c44 100644 --- a/Shell/InterpretedNormalizer.cpp +++ b/Shell/InterpretedNormalizer.cpp @@ -50,7 +50,6 @@ class InterpretedNormalizer::FunctionTranslator class InterpretedNormalizer::RoundingFunctionTranslator : public FunctionTranslator { public: - CLASS_NAME(InterpretedNormalizer::RoundingFunctionTranslator); USE_ALLOCATOR(InterpretedNormalizer::RoundingFunctionTranslator); RoundingFunctionTranslator(Interpretation origf, Interpretation newf, Interpretation roundf) @@ -88,7 +87,6 @@ class InterpretedNormalizer::RoundingFunctionTranslator : public FunctionTransla class InterpretedNormalizer::SuccessorTranslator : public FunctionTranslator { public: - CLASS_NAME(InterpretedNormalizer::SuccessorTranslator); USE_ALLOCATOR(InterpretedNormalizer::SuccessorTranslator); SuccessorTranslator() @@ -122,7 +120,6 @@ class InterpretedNormalizer::SuccessorTranslator : public FunctionTranslator class InterpretedNormalizer::BinaryMinusTranslator : public FunctionTranslator { public: - CLASS_NAME(InterpretedNormalizer::BinaryMinusTranslator); USE_ALLOCATOR(InterpretedNormalizer::BinaryMinusTranslator); BinaryMinusTranslator(Interpretation bMinus, Interpretation plus, Interpretation uMinus) @@ -158,7 +155,6 @@ class InterpretedNormalizer::BinaryMinusTranslator : public FunctionTranslator class InterpretedNormalizer::IneqTranslator { public: - CLASS_NAME(InterpretedNormalizer::IneqTranslator); USE_ALLOCATOR(InterpretedNormalizer::IneqTranslator); IneqTranslator(Interpretation src, Interpretation tgt, bool swapArguments, bool reversePolarity) @@ -198,7 +194,6 @@ class InterpretedNormalizer::IneqTranslator class InterpretedNormalizer::NLiteralTransformer : public TermTransformer { public: - CLASS_NAME(InterpretedNormalizer::NLiteralTransformer); USE_ALLOCATOR(InterpretedNormalizer::NLiteralTransformer); NLiteralTransformer() diff --git a/Shell/LispParser.hpp b/Shell/LispParser.hpp index 859c513df..ccb3e1b39 100644 --- a/Shell/LispParser.hpp +++ b/Shell/LispParser.hpp @@ -49,7 +49,6 @@ class LispParser /** expressions */ struct Expression { - CLASS_NAME(LispParser::Expression); USE_ALLOCATOR(Expression); /** type of the expression */ diff --git a/Shell/NewCNF.hpp b/Shell/NewCNF.hpp index b1c0d901d..344cfd42d 100644 --- a/Shell/NewCNF.hpp +++ b/Shell/NewCNF.hpp @@ -136,7 +136,6 @@ class NewCNF // generalized clause struct GenClause { - CLASS_NAME(NewCNF::GenClause); USE_ALLOCATOR(NewCNF::GenClause); GenClause(unsigned size, BindingList* bindings, BindingList* foolBindings) @@ -279,7 +278,6 @@ class NewCNF GenClauses _genClauses; struct Occurrence { - CLASS_NAME(NewCNF::Occurrence); USE_ALLOCATOR(NewCNF::Occurrence); SPGenClause gc; @@ -318,7 +316,6 @@ class NewCNF unsigned _size; public: - CLASS_NAME(NewCNF::Occurrences); USE_ALLOCATOR(NewCNF::Occurrences); Occurrences() : _occurrences(nullptr), _size(0) {} diff --git a/Shell/Options.hpp b/Shell/Options.hpp index c5bd85803..caaa559d1 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -179,7 +179,6 @@ class Options void setInputFile(const vstring& newVal){ _inputFile.set(newVal); } vstring includeFileName (const vstring& relativeName); - CLASS_NAME(Options); USE_ALLOCATOR(Options); // standard ways of creating options @@ -844,7 +843,6 @@ class Options */ struct AbstractOptionValue { - CLASS_NAME(AbstractOptionValue); USE_ALLOCATOR(AbstractOptionValue); AbstractOptionValue(){} @@ -977,7 +975,6 @@ class Options template struct OptionValue : public AbstractOptionValue { - CLASS_NAME(OptionValue); USE_ALLOCATOR(OptionValue); // We need to include an empty constructor as all the OptionValue objects need to be initialized @@ -1078,7 +1075,6 @@ class Options template struct ChoiceOptionValue : public OptionValue { - CLASS_NAME(ChoiceOptionValue); USE_ALLOCATOR(ChoiceOptionValue); ChoiceOptionValue(){} @@ -1211,7 +1207,6 @@ vstring getStringOfValue(float value) const{ return Lib::Int::toString(value); } */ struct RatioOptionValue : public OptionValue { -CLASS_NAME(RatioOptionValue); USE_ALLOCATOR(RatioOptionValue); RatioOptionValue(){} @@ -1257,7 +1252,6 @@ virtual vstring getStringOfActual() const override { */ struct NonGoalWeightOptionValue : public OptionValue{ -CLASS_NAME(NonGoalWeightOptionValue); USE_ALLOCATOR(NonGoalWeightOptionValue); NonGoalWeightOptionValue(){} @@ -1398,7 +1392,6 @@ virtual vstring getStringOfValue(int value) const{ return Lib::Int::toString(val template struct OptionValueConstraint{ -CLASS_NAME(OptionValueConstraint); USE_ALLOCATOR(OptionValueConstraint); OptionValueConstraint() : _hard(false) {} @@ -1425,7 +1418,6 @@ bool _hard; template struct WrappedConstraint : AbstractWrappedConstraint { - CLASS_NAME(WrappedConstraint); USE_ALLOCATOR(WrappedConstraint); WrappedConstraint(const OptionValue& v, OptionValueConstraintUP c) : value(v), con(std::move(c)) {} @@ -1442,7 +1434,6 @@ bool _hard; }; struct WrappedConstraintOrWrapper : public AbstractWrappedConstraint { - CLASS_NAME(WrappedConstraintOrWrapper); USE_ALLOCATOR(WrappedConstraintOrWrapper); WrappedConstraintOrWrapper(AbstractWrappedConstraintUP l, AbstractWrappedConstraintUP r) : left(std::move(l)),right(std::move(r)) {} bool check() override { @@ -1455,7 +1446,6 @@ bool _hard; }; struct WrappedConstraintAndWrapper : public AbstractWrappedConstraint { - CLASS_NAME(WrappedConstraintAndWrapper); USE_ALLOCATOR(WrappedConstraintAndWrapper); WrappedConstraintAndWrapper(AbstractWrappedConstraintUP l, AbstractWrappedConstraintUP r) : left(std::move(l)),right(std::move(r)) {} bool check() override { @@ -1469,7 +1459,6 @@ bool _hard; template struct OptionValueConstraintOrWrapper : public OptionValueConstraint{ - CLASS_NAME(OptionValueConstraintOrWrapper); USE_ALLOCATOR(OptionValueConstraintOrWrapper); OptionValueConstraintOrWrapper(OptionValueConstraintUP l, OptionValueConstraintUP r) : left(std::move(l)),right(std::move(r)) {} bool check(const OptionValue& value){ @@ -1483,7 +1472,6 @@ bool _hard; template struct OptionValueConstraintAndWrapper : public OptionValueConstraint{ - CLASS_NAME(OptionValueConstraintAndWrapper); USE_ALLOCATOR(OptionValueConstraintAndWrapper); OptionValueConstraintAndWrapper(OptionValueConstraintUP l, OptionValueConstraintUP r) : left(std::move(l)),right(std::move(r)) {} bool check(const OptionValue& value){ @@ -1497,7 +1485,6 @@ bool _hard; template struct UnWrappedConstraint : public OptionValueConstraint{ - CLASS_NAME(UnWrappedConstraint); USE_ALLOCATOR(UnWrappedConstraint); UnWrappedConstraint(AbstractWrappedConstraintUP c) : con(std::move(c)) {} @@ -1562,7 +1549,6 @@ bool _hard; template struct Equal : public OptionValueConstraint{ - CLASS_NAME(Equal); USE_ALLOCATOR(Equal); Equal(T gv) : _goodvalue(gv) {} bool check(const OptionValue& value){ @@ -1580,7 +1566,6 @@ bool _hard; template struct NotEqual : public OptionValueConstraint{ - CLASS_NAME(NotEqual); USE_ALLOCATOR(NotEqual); NotEqual(T bv) : _badvalue(bv) {} bool check(const OptionValue& value){ @@ -1598,7 +1583,6 @@ bool _hard; // optionally we can allow it be equal to that value also template struct LessThan : public OptionValueConstraint{ - CLASS_NAME(LessThan); USE_ALLOCATOR(LessThan); LessThan(T gv,bool eq=false) : _goodvalue(gv), _orequal(eq) {} bool check(const OptionValue& value){ @@ -1625,7 +1609,6 @@ bool _hard; // optionally we can allow it be equal to that value also template struct GreaterThan : public OptionValueConstraint{ - CLASS_NAME(GreaterThan); USE_ALLOCATOR(GreaterThan); GreaterThan(T gv,bool eq=false) : _goodvalue(gv), _orequal(eq) {} bool check(const OptionValue& value){ @@ -1653,7 +1636,6 @@ bool _hard; // optionally we can allow it be equal to that value also template struct SmallerThan : public OptionValueConstraint{ - CLASS_NAME(SmallerThan); USE_ALLOCATOR(SmallerThan); SmallerThan(T gv,bool eq=false) : _goodvalue(gv), _orequal(eq) {} bool check(const OptionValue& value){ @@ -1686,7 +1668,6 @@ bool _hard; template struct IfThenConstraint : public OptionValueConstraint{ - CLASS_NAME(IfThenConstraint); USE_ALLOCATOR(IfThenConstraint); IfThenConstraint(OptionValueConstraintUP ic, OptionValueConstraintUP c) : @@ -1707,7 +1688,6 @@ bool _hard; template struct IfConstraint { - CLASS_NAME(IfConstraint); USE_ALLOCATOR(IfConstraint); IfConstraint(OptionValueConstraintUP c) :if_con(std::move(c)) {} @@ -1783,7 +1763,6 @@ bool _hard; } struct isLookAheadSelectionConstraint : public OptionValueConstraint{ - CLASS_NAME(isLookAheadSelectionConstraint); USE_ALLOCATOR(isLookAheadSelectionConstraint); isLookAheadSelectionConstraint() {} bool check(const OptionValue& value){ @@ -1806,7 +1785,6 @@ bool _hard; */ struct OptionProblemConstraint{ - CLASS_NAME(OptionProblemConstraint); USE_ALLOCATOR(OptionProblemConstraint); virtual bool check(Property* p) = 0; @@ -1815,7 +1793,6 @@ bool _hard; }; struct CategoryCondition : OptionProblemConstraint{ - CLASS_NAME(CategoryCondition); USE_ALLOCATOR(CategoryCondition); CategoryCondition(Property::Category c,bool h) : cat(c), has(h) {} @@ -1833,7 +1810,6 @@ bool _hard; }; struct UsesEquality : OptionProblemConstraint{ - CLASS_NAME(UsesEquality); USE_ALLOCATOR(UsesEquality); bool check(Property*p){ @@ -1846,7 +1822,6 @@ bool _hard; }; struct HasHigherOrder : OptionProblemConstraint{ - CLASS_NAME(HasHigherOrder); USE_ALLOCATOR(HasHigherOrder); bool check(Property*p){ @@ -1857,7 +1832,6 @@ bool _hard; }; struct OnlyFirstOrder : OptionProblemConstraint{ - CLASS_NAME(OnlyFirstOrder); USE_ALLOCATOR(OnlyFirstOrder); bool check(Property*p){ @@ -1868,7 +1842,6 @@ bool _hard; }; struct MayHaveNonUnits : OptionProblemConstraint{ - CLASS_NAME(MayHaveNonUnits); USE_ALLOCATOR(MayHaveNonUnits); bool check(Property*p){ @@ -1879,7 +1852,6 @@ bool _hard; }; struct NotJustEquality : OptionProblemConstraint{ - CLASS_NAME(NotJustEquality); USE_ALLOCATOR(NotJustEquality); bool check(Property*p){ @@ -1889,7 +1861,6 @@ bool _hard; }; struct AtomConstraint : OptionProblemConstraint{ - CLASS_NAME(AtomConstraint); USE_ALLOCATOR(AtomConstraint); AtomConstraint(int a,bool g) : atoms(a),greater(g) {} @@ -1907,7 +1878,6 @@ bool _hard; }; struct HasTheories : OptionProblemConstraint { - CLASS_NAME(HasTheories); USE_ALLOCATOR(HasTheories); static bool actualCheck(Property*p); @@ -1917,7 +1887,6 @@ bool _hard; }; struct HasFormulas : OptionProblemConstraint { - CLASS_NAME(HasFormulas); USE_ALLOCATOR(HasFormulas); bool check(Property*p) { @@ -1927,7 +1896,6 @@ bool _hard; }; struct HasGoal : OptionProblemConstraint { - CLASS_NAME(HasGoal); USE_ALLOCATOR(HasGoal); bool check(Property*p){ @@ -1965,7 +1933,6 @@ bool _hard; // set of options will not be randomized and some will be randomized first struct OptionHasValue : OptionProblemConstraint{ - CLASS_NAME(OptionHasValue); USE_ALLOCATOR(OptionHasValue); OptionHasValue(vstring ov,vstring v) : option_value(ov),value(v) {} @@ -1976,7 +1943,6 @@ bool _hard; }; struct ManyOptionProblemConstraints : OptionProblemConstraint { - CLASS_NAME(ManyOptionProblemConstraints); USE_ALLOCATOR(ManyOptionProblemConstraints); ManyOptionProblemConstraints(bool a) : is_and(a) {} diff --git a/Shell/PredicateDefinition.cpp b/Shell/PredicateDefinition.cpp index eece849ee..b9d26783b 100644 --- a/Shell/PredicateDefinition.cpp +++ b/Shell/PredicateDefinition.cpp @@ -144,7 +144,6 @@ struct PredicateDefinition::PredData + ") -(" + Int::toString(nocc) + ") 0(" + Int::toString(docc) + ")"; } - CLASS_NAME(PredicateDefinition::PredData); }; PredicateDefinition::PredicateDefinition() diff --git a/Shell/Property.hpp b/Shell/Property.hpp index 72c799112..67e063e07 100644 --- a/Shell/Property.hpp +++ b/Shell/Property.hpp @@ -152,7 +152,6 @@ class Property static const uint64_t PR_HAS_CDT_CONSTRUCTORS = 2199023255552ul; // 2^41 public: - CLASS_NAME(Property); USE_ALLOCATOR(Property); // constructor, operators new and delete diff --git a/Shell/Statistics.hpp b/Shell/Statistics.hpp index 181d5d717..8393587cc 100644 --- a/Shell/Statistics.hpp +++ b/Shell/Statistics.hpp @@ -43,7 +43,6 @@ using namespace Kernel; class Statistics { public: - CLASS_NAME(Statistics); USE_ALLOCATOR(Statistics); Statistics(); diff --git a/Shell/SubexpressionIterator.hpp b/Shell/SubexpressionIterator.hpp index 63c933e77..60104306c 100644 --- a/Shell/SubexpressionIterator.hpp +++ b/Shell/SubexpressionIterator.hpp @@ -28,7 +28,6 @@ namespace Shell { class SubexpressionIterator { public: - CLASS_NAME(SubexpressionIterator); USE_ALLOCATOR(SubexpressionIterator); /** * SubexpressionIterator::Expression represents an expression, which is diff --git a/Shell/TermAlgebra.hpp b/Shell/TermAlgebra.hpp index 7baf8891e..e508ea367 100644 --- a/Shell/TermAlgebra.hpp +++ b/Shell/TermAlgebra.hpp @@ -25,7 +25,6 @@ using Kernel::TermList; namespace Shell { class TermAlgebraConstructor { public: - CLASS_NAME(TermAlgebraConstructor); USE_ALLOCATOR(TermAlgebraConstructor); /* A term algebra constructor, described by its name, range, @@ -88,7 +87,6 @@ namespace Shell { class TermAlgebra { public: - CLASS_NAME(TermAlgebra); USE_ALLOCATOR(TermAlgebra);