diff --git a/DP/ShortConflictMetaDP.hpp b/DP/ShortConflictMetaDP.hpp index cd89769047..dbfd04a75b 100644 --- a/DP/ShortConflictMetaDP.hpp +++ b/DP/ShortConflictMetaDP.hpp @@ -34,8 +34,6 @@ using namespace SAT; class ShortConflictMetaDP : public DecisionProcedure { public: - USE_ALLOCATOR(ShortConflictMetaDP); - /** * Create object using @c inner decision procedure. Object takes ownership of the @c inner object. */ diff --git a/DP/SimpleCongruenceClosure.hpp b/DP/SimpleCongruenceClosure.hpp index 13f9b7886c..aa4330edd2 100644 --- a/DP/SimpleCongruenceClosure.hpp +++ b/DP/SimpleCongruenceClosure.hpp @@ -48,8 +48,6 @@ using namespace Kernel; class SimpleCongruenceClosure : public DecisionProcedure { public: - USE_ALLOCATOR(SimpleCongruenceClosure); - SimpleCongruenceClosure(Ordering* ord); virtual void addLiterals(LiteralIterator lits, bool onlyEqualites) override; diff --git a/Debug/TimeProfiling.hpp b/Debug/TimeProfiling.hpp index 800886e314..4f48d8f9fe 100644 --- a/Debug/TimeProfiling.hpp +++ b/Debug/TimeProfiling.hpp @@ -195,8 +195,6 @@ class TimeTraceOrdering : public Kernel::Ordering const char* _nameTerm; Ord _ord; public: - USE_ALLOCATOR(TimeTraceOrdering); - TimeTraceOrdering(const char* nameLit, const char* nameTerm, Ord ord) : _nameLit(nameLit) , _nameTerm(nameTerm) diff --git a/FMB/FiniteModel.hpp b/FMB/FiniteModel.hpp index dad5d85dc1..1945ec56a6 100644 --- a/FMB/FiniteModel.hpp +++ b/FMB/FiniteModel.hpp @@ -35,8 +35,6 @@ using namespace Kernel; * */ class FiniteModel { - USE_ALLOCATOR(FiniteModel); - public: const unsigned _size; diff --git a/FMB/FiniteModelBuilder.hpp b/FMB/FiniteModelBuilder.hpp index 90000e7ab6..6fcd309db4 100644 --- a/FMB/FiniteModelBuilder.hpp +++ b/FMB/FiniteModelBuilder.hpp @@ -57,8 +57,6 @@ using namespace SAT; class FiniteModelBuilder : public MainLoop { public: - USE_ALLOCATOR(FiniteModelBuilder); - FiniteModelBuilder(Problem& prb, const Options& opt); ~FiniteModelBuilder(); @@ -251,8 +249,6 @@ class FiniteModelBuilder : public MainLoop { class HackyDSAE : public DSAEnumerator { struct Constraint_Generator { - USE_ALLOCATOR(FiniteModelBuilder::HackyDSAE::Constraint_Generator); - Constraint_Generator_Vals _vals; unsigned _weight; @@ -287,8 +283,6 @@ class FiniteModelBuilder : public MainLoop { bool checkConstriant(DArray& newSortSizes, Constraint_Generator_Vals& constraint); public: - USE_ALLOCATOR(FiniteModelBuilder::HackyDSAE); - HackyDSAE(bool keepOldGenerators) : _maxWeightSoFar(0), _keepOldGenerators(keepOldGenerators) {} bool init(unsigned _startSize, DArray&, Stack>& dsc, Stack>& sdsc) override { @@ -314,9 +308,6 @@ class FiniteModelBuilder : public MainLoop { unsigned loadSizesFromSmt(DArray& szs); void reportZ3OutOfMemory(); public: - // the following is not sufficient, since z3::solver and z3::context allocate internally - USE_ALLOCATOR(FiniteModelBuilder::SmtBasedDSAE); - SmtBasedDSAE() : _smtSolver(_context) {} bool init(unsigned, DArray&, Stack>&, Stack>&) override; diff --git a/FMB/FiniteModelMultiSorted.hpp b/FMB/FiniteModelMultiSorted.hpp index ccae8e86e1..10081c1245 100644 --- a/FMB/FiniteModelMultiSorted.hpp +++ b/FMB/FiniteModelMultiSorted.hpp @@ -35,8 +35,6 @@ using namespace Kernel; * */ class FiniteModelMultiSorted { - USE_ALLOCATOR(FiniteModelMultiSorted); - DHMap _sizes; public: diff --git a/FMB/Monotonicity.hpp b/FMB/Monotonicity.hpp index 7cc8bdb228..70eb3a9bf7 100644 --- a/FMB/Monotonicity.hpp +++ b/FMB/Monotonicity.hpp @@ -40,9 +40,6 @@ namespace FMB { using namespace Lib; class Monotonicity{ - - USE_ALLOCATOR(Monotonicity); - public: // Assumes clauses are flattened Monotonicity(ClauseList* clauses, unsigned srt); diff --git a/FMB/SortInference.hpp b/FMB/SortInference.hpp index 4e70f4b13b..89e805f0d1 100644 --- a/FMB/SortInference.hpp +++ b/FMB/SortInference.hpp @@ -32,8 +32,6 @@ using namespace Shell; using namespace Lib; struct SortedSignature{ - USE_ALLOCATOR(SortedSignature); - unsigned sorts; DArray> sortedConstants; DArray> sortedFunctions; @@ -77,8 +75,6 @@ struct SortedSignature{ class SortInference { public: - USE_ALLOCATOR(SortInference); - SortInference(ClauseList* clauses, DArray del_f, DArray del_p, diff --git a/Indexing/AcyclicityIndex.hpp b/Indexing/AcyclicityIndex.hpp index 8e5bffe3b1..52da79b65b 100644 --- a/Indexing/AcyclicityIndex.hpp +++ b/Indexing/AcyclicityIndex.hpp @@ -66,8 +66,6 @@ class AcyclicityIndex void remove(Kernel::Literal *lit, Kernel::Clause *c); CycleQueryResultsIterator queryCycles(Kernel::Literal *lit, Kernel::Clause *c); - - USE_ALLOCATOR(AcyclicityIndex); protected: void handleClause(Kernel::Clause* c, bool adding); private: diff --git a/Indexing/ClauseVariantIndex.hpp b/Indexing/ClauseVariantIndex.hpp index 9d591a98f3..1bda4296f4 100644 --- a/Indexing/ClauseVariantIndex.hpp +++ b/Indexing/ClauseVariantIndex.hpp @@ -52,8 +52,6 @@ class ClauseVariantIndex class SubstitutionTreeClauseVariantIndex : public ClauseVariantIndex { public: - USE_ALLOCATOR(SubstitutionTreeClauseVariantIndex); - SubstitutionTreeClauseVariantIndex() : _emptyClauses(0) {} virtual ~SubstitutionTreeClauseVariantIndex() override; @@ -76,8 +74,6 @@ class SubstitutionTreeClauseVariantIndex : public ClauseVariantIndex class HashingClauseVariantIndex : public ClauseVariantIndex { public: - USE_ALLOCATOR(HashingClauseVariantIndex); - virtual ~HashingClauseVariantIndex() override; virtual void insert(Clause* cl) override; diff --git a/Indexing/CodeTreeInterfaces.hpp b/Indexing/CodeTreeInterfaces.hpp index 7acb9f071c..1090e4a38e 100644 --- a/Indexing/CodeTreeInterfaces.hpp +++ b/Indexing/CodeTreeInterfaces.hpp @@ -40,8 +40,6 @@ using namespace Lib; class CodeTreeTIS : public TermIndexingStructure { public: - USE_ALLOCATOR(CodeTreeTIS); - void insert(TypedTermList t, Literal* lit, Clause* cls); void remove(TypedTermList t, Literal* lit, Clause* cls); @@ -78,8 +76,6 @@ class CodeTreeSubsumptionIndex : public ClauseSubsumptionIndex { public: - USE_ALLOCATOR(CodeTreeSubsumptionIndex); - ClauseSResResultIterator getSubsumingOrSResolvingClauses(Clause* c, bool subsumptionResolution); protected: //overrides Index::handleClause diff --git a/Indexing/GroundingIndex.hpp b/Indexing/GroundingIndex.hpp index 1b55e8d692..9e5c9dfb3c 100644 --- a/Indexing/GroundingIndex.hpp +++ b/Indexing/GroundingIndex.hpp @@ -31,8 +31,6 @@ using namespace Shell; class GroundingIndex : public Index { public: - USE_ALLOCATOR(GroundingIndex); - GroundingIndex(const Options& opt); SATSolverWithAssumptions& getSolver() { return *_solver; } diff --git a/Indexing/Index.hpp b/Indexing/Index.hpp index 572038dc3c..9ae0833439 100644 --- a/Indexing/Index.hpp +++ b/Indexing/Index.hpp @@ -129,8 +129,6 @@ typedef VirtualIterator FormulaQueryResultIterator; class Index { public: - USE_ALLOCATOR(Index); - virtual ~Index(); void attachContainer(ClauseContainer* cc); @@ -157,8 +155,6 @@ class ClauseSubsumptionIndex : public Index { public: - USE_ALLOCATOR(ClauseSubsumptionIndex); - virtual ClauseSResResultIterator getSubsumingOrSResolvingClauses(Clause* c, bool subsumptionResolution) { NOT_IMPLEMENTED; }; diff --git a/Indexing/IndexManager.hpp b/Indexing/IndexManager.hpp index df00bfd3f1..b7c870bfaf 100644 --- a/Indexing/IndexManager.hpp +++ b/Indexing/IndexManager.hpp @@ -72,8 +72,6 @@ enum IndexType { class IndexManager { public: - USE_ALLOCATOR(IndexManager); - /** alg can be zero, then it must be set by setSaturationAlgorithm */ explicit IndexManager(SaturationAlgorithm* alg) : _alg(alg) {} void setSaturationAlgorithm(SaturationAlgorithm* alg) diff --git a/Indexing/LiteralIndex.hpp b/Indexing/LiteralIndex.hpp index 122afeef59..9de1f86c89 100644 --- a/Indexing/LiteralIndex.hpp +++ b/Indexing/LiteralIndex.hpp @@ -27,8 +27,6 @@ class LiteralIndex : public Index { public: - USE_ALLOCATOR(LiteralIndex); - virtual ~LiteralIndex(); SLQueryResultIterator getAll(); @@ -60,8 +58,6 @@ class BinaryResolutionIndex : public LiteralIndex { public: - USE_ALLOCATOR(BinaryResolutionIndex); - BinaryResolutionIndex(LiteralIndexingStructure* is) : LiteralIndex(is) {}; protected: @@ -72,8 +68,6 @@ class BackwardSubsumptionIndex : public LiteralIndex { public: - USE_ALLOCATOR(BackwardSubsumptionIndex); - BackwardSubsumptionIndex(LiteralIndexingStructure* is) : LiteralIndex(is) {}; protected: @@ -84,8 +78,6 @@ class FwSubsSimplifyingLiteralIndex : public LiteralIndex { public: - USE_ALLOCATOR(FwSubsSimplifyingLiteralIndex); - FwSubsSimplifyingLiteralIndex(LiteralIndexingStructure* is) : LiteralIndex(is) { } @@ -98,8 +90,6 @@ class FSDLiteralIndex : public LiteralIndex { public: - USE_ALLOCATOR(FSDLiteralIndex); - FSDLiteralIndex(LiteralIndexingStructure* is) : LiteralIndex(is) { } @@ -112,8 +102,6 @@ class UnitClauseLiteralIndex : public LiteralIndex { public: - USE_ALLOCATOR(UnitClauseLiteralIndex); - UnitClauseLiteralIndex(LiteralIndexingStructure* is) : LiteralIndex(is) {}; protected: @@ -124,8 +112,6 @@ class UnitClauseWithALLiteralIndex : public LiteralIndex { public: - USE_ALLOCATOR(UnitClauseWithALLiteralIndex); - UnitClauseWithALLiteralIndex(LiteralIndexingStructure* is) : LiteralIndex(is) {}; protected: @@ -136,8 +122,6 @@ class NonUnitClauseLiteralIndex : public LiteralIndex { public: - USE_ALLOCATOR(NonUnitClauseLiteralIndex); - NonUnitClauseLiteralIndex(LiteralIndexingStructure* is, bool selectedOnly=false) : LiteralIndex(is), _selectedOnly(selectedOnly) {}; protected: @@ -150,8 +134,6 @@ class NonUnitClauseWithALLiteralIndex : public LiteralIndex { public: - USE_ALLOCATOR(NonUnitClauseWithALLiteralIndex); - NonUnitClauseWithALLiteralIndex(LiteralIndexingStructure* is, bool selectedOnly=false) : LiteralIndex(is), _selectedOnly(selectedOnly) {}; protected: @@ -164,8 +146,6 @@ class RewriteRuleIndex : public LiteralIndex { public: - USE_ALLOCATOR(RewriteRuleIndex); - RewriteRuleIndex(LiteralIndexingStructure* is, Ordering& ordering); ~RewriteRuleIndex(); @@ -188,8 +168,6 @@ class DismatchingLiteralIndex : public LiteralIndex { public: - USE_ALLOCATOR(DismatchingLiteralIndex); - DismatchingLiteralIndex(LiteralIndexingStructure* is) : LiteralIndex(is) {}; void handleClause(Clause* c, bool adding); @@ -200,8 +178,6 @@ class UnitIntegerComparisonLiteralIndex : public LiteralIndex { public: - USE_ALLOCATOR(UnitIntegerComparisonLiteralIndex); - UnitIntegerComparisonLiteralIndex(LiteralIndexingStructure* is) : LiteralIndex(is) {} diff --git a/Indexing/LiteralSubstitutionTree.hpp b/Indexing/LiteralSubstitutionTree.hpp index c02b7ed628..1d78eb0190 100644 --- a/Indexing/LiteralSubstitutionTree.hpp +++ b/Indexing/LiteralSubstitutionTree.hpp @@ -36,8 +36,6 @@ class LiteralSubstitutionTree using Leaf = SubstitutionTree::Leaf; public: - USE_ALLOCATOR(LiteralSubstitutionTree); - LiteralSubstitutionTree(bool useC=false); void insert(Literal* lit, Clause* cls) override { handleLiteral(lit, cls, /* insert */ true); } diff --git a/Indexing/RequestedIndex.hpp b/Indexing/RequestedIndex.hpp index 874776fa3c..569a8589f4 100644 --- a/Indexing/RequestedIndex.hpp +++ b/Indexing/RequestedIndex.hpp @@ -23,8 +23,6 @@ template class RequestedIndex final { public: - USE_ALLOCATOR(RequestedIndex); - RequestedIndex() { } diff --git a/Indexing/SubstitutionTree.hpp b/Indexing/SubstitutionTree.hpp index ac9ecb796f..9a72dbfcbf 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; - USE_ALLOCATOR(SubstitutionTree); SubstitutionTree(bool useC, bool rfSubs); diff --git a/Indexing/TermIndex.hpp b/Indexing/TermIndex.hpp index 5300aaf469..5c9306ff17 100644 --- a/Indexing/TermIndex.hpp +++ b/Indexing/TermIndex.hpp @@ -28,8 +28,6 @@ class TermIndex : public Index { public: - USE_ALLOCATOR(TermIndex); - virtual ~TermIndex(); TermQueryResultIterator getUnifications(TypedTermList t, bool retrieveSubstitutions = true, bool withConstraints = false); @@ -46,8 +44,6 @@ class SuperpositionSubtermIndex : public TermIndex { public: - USE_ALLOCATOR(SuperpositionSubtermIndex); - SuperpositionSubtermIndex(TermIndexingStructure* is, Ordering& ord) : TermIndex(is), _ord(ord) {}; protected: @@ -60,8 +56,6 @@ class SuperpositionLHSIndex : public TermIndex { public: - USE_ALLOCATOR(SuperpositionLHSIndex); - SuperpositionLHSIndex(TermSubstitutionTree* is, Ordering& ord, const Options& opt) : TermIndex(is), _ord(ord), _opt(opt), _tree(is) {}; protected: @@ -92,8 +86,6 @@ class DemodulationSubtermIndexImpl : public DemodulationSubtermIndex { public: - USE_ALLOCATOR(DemodulationSubtermIndexImpl); - DemodulationSubtermIndexImpl(TermIndexingStructure* is) : DemodulationSubtermIndex(is) {}; protected: @@ -107,8 +99,6 @@ class DemodulationLHSIndex : public TermIndex { public: - USE_ALLOCATOR(DemodulationLHSIndex); - DemodulationLHSIndex(TermIndexingStructure* is, Ordering& ord, const Options& opt) : TermIndex(is), _ord(ord), _opt(opt) {}; protected: @@ -125,8 +115,6 @@ class InductionTermIndex : public TermIndex { public: - USE_ALLOCATOR(InductionTermIndex); - InductionTermIndex(TermIndexingStructure* is) : TermIndex(is) {} @@ -141,8 +129,6 @@ class StructInductionTermIndex : public TermIndex { public: - USE_ALLOCATOR(StructInductionTermIndex); - StructInductionTermIndex(TermIndexingStructure* is) : TermIndex(is) {} @@ -158,8 +144,6 @@ class PrimitiveInstantiationIndex : public TermIndex { public: - USE_ALLOCATOR(PrimitiveInstantiationIndex); - PrimitiveInstantiationIndex(TermIndexingStructure* is) : TermIndex(is) { populateIndex(); @@ -172,8 +156,6 @@ class SubVarSupSubtermIndex : public TermIndex { public: - USE_ALLOCATOR(SubVarSupSubtermIndex); - SubVarSupSubtermIndex(TermIndexingStructure* is, Ordering& ord) : TermIndex(is), _ord(ord) {}; protected: @@ -186,8 +168,6 @@ class SubVarSupLHSIndex : public TermIndex { public: - USE_ALLOCATOR(SubVarSupLHSIndex); - SubVarSupLHSIndex(TermIndexingStructure* is, Ordering& ord, const Options& opt) : TermIndex(is), _ord(ord) {}; protected: @@ -203,8 +183,6 @@ class NarrowingIndex : public TermIndex { public: - USE_ALLOCATOR(NarrowingIndex); - NarrowingIndex(TermIndexingStructure* is) : TermIndex(is) { populateIndex(); @@ -218,8 +196,6 @@ class SkolemisingFormulaIndex : public TermIndex { public: - USE_ALLOCATOR(SkolemisingFormulaIndex); - SkolemisingFormulaIndex(TermIndexingStructure* is) : TermIndex(is) {} void insertFormula(TermList formula, TermList skolem); @@ -229,8 +205,6 @@ class SkolemisingFormulaIndex : public TermIndex { public: - USE_ALLOCATOR(HeuristicInstantiationIndex); - HeuristicInstantiationIndex(TermIndexingStructure* is) : TermIndex(is) {} protected: @@ -244,8 +218,6 @@ class RenamingFormulaIndex : public TermIndex { public: - USE_ALLOCATOR(RenamingFormulaIndex); - RenamingFormulaIndex(TermIndexingStructure* is) : TermIndex(is) {} void insertFormula(TermList formula, TermList name, Literal* lit, Clause* cls); diff --git a/Indexing/TermSharing.hpp b/Indexing/TermSharing.hpp index 181d7fb51f..ff01c994ea 100644 --- a/Indexing/TermSharing.hpp +++ b/Indexing/TermSharing.hpp @@ -30,8 +30,6 @@ namespace Indexing { class TermSharing { public: - USE_ALLOCATOR(TermSharing); - TermSharing(); ~TermSharing(); diff --git a/Indexing/TermSubstitutionTree.hpp b/Indexing/TermSubstitutionTree.hpp index 2cf2079f6e..bae5e157e5 100644 --- a/Indexing/TermSubstitutionTree.hpp +++ b/Indexing/TermSubstitutionTree.hpp @@ -39,8 +39,6 @@ class TermSubstitutionTree : public TermIndexingStructure, SubstitutionTree { public: - USE_ALLOCATOR(TermSubstitutionTree); - /* * The extra flag is a higher-order concern. it is set to true when * we require the term query result to include two terms, the result term diff --git a/Inferences/ArgCong.hpp b/Inferences/ArgCong.hpp index 9d92658a50..73ace79f31 100644 --- a/Inferences/ArgCong.hpp +++ b/Inferences/ArgCong.hpp @@ -31,8 +31,6 @@ class ArgCong : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(ArgCong); - ClauseIterator generateClauses(Clause* premise); private: struct ResultFn; diff --git a/Inferences/ArithmeticSubtermGeneralization.hpp b/Inferences/ArithmeticSubtermGeneralization.hpp index 407ffdea16..8f97df7e5d 100644 --- a/Inferences/ArithmeticSubtermGeneralization.hpp +++ b/Inferences/ArithmeticSubtermGeneralization.hpp @@ -23,8 +23,6 @@ class NumeralMultiplicationGeneralization : public SimplifyingGeneratingInference1 { public: - USE_ALLOCATOR(NumeralMultiplicationGeneralization); - virtual ~NumeralMultiplicationGeneralization(); SimplifyingGeneratingInference1::Result simplify(Clause* cl, bool doOrderingCheck); @@ -35,8 +33,6 @@ class VariableMultiplicationGeneralization : public SimplifyingGeneratingInference1 { public: - USE_ALLOCATOR(VariableMultiplicationGeneralization); - virtual ~VariableMultiplicationGeneralization(); SimplifyingGeneratingInference1::Result simplify(Clause* cl, bool doOrderingCheck); @@ -47,8 +43,6 @@ class VariablePowerGeneralization : public SimplifyingGeneratingInference1 { public: - USE_ALLOCATOR(VariablePowerGeneralization); - virtual ~VariablePowerGeneralization(); SimplifyingGeneratingInference1::Result simplify(Clause* cl, bool doOrderingCheck); @@ -59,8 +53,6 @@ class AdditionGeneralization : public SimplifyingGeneratingInference1 { public: - USE_ALLOCATOR(AdditionGeneralization); - virtual ~AdditionGeneralization(); SimplifyingGeneratingInference1::Result simplify(Clause* cl, bool doOrderingCheck); diff --git a/Inferences/BackwardDemodulation.hpp b/Inferences/BackwardDemodulation.hpp index fd09b55118..6a38b19005 100644 --- a/Inferences/BackwardDemodulation.hpp +++ b/Inferences/BackwardDemodulation.hpp @@ -30,8 +30,6 @@ class BackwardDemodulation : public BackwardSimplificationEngine { public: - USE_ALLOCATOR(BackwardDemodulation); - void attach(SaturationAlgorithm* salg); void detach(); diff --git a/Inferences/BackwardSubsumptionDemodulation.hpp b/Inferences/BackwardSubsumptionDemodulation.hpp index b1e0ab93f6..e722bba040 100644 --- a/Inferences/BackwardSubsumptionDemodulation.hpp +++ b/Inferences/BackwardSubsumptionDemodulation.hpp @@ -49,8 +49,6 @@ class BackwardSubsumptionDemodulation : public BackwardSimplificationEngine { public: - USE_ALLOCATOR(BackwardSubsumptionDemodulation); - BackwardSubsumptionDemodulation(); void attach(SaturationAlgorithm* salg) override; diff --git a/Inferences/BackwardSubsumptionResolution.hpp b/Inferences/BackwardSubsumptionResolution.hpp index 281f1e37e5..b278961f48 100644 --- a/Inferences/BackwardSubsumptionResolution.hpp +++ b/Inferences/BackwardSubsumptionResolution.hpp @@ -28,8 +28,6 @@ class BackwardSubsumptionResolution : public BackwardSimplificationEngine { public: - USE_ALLOCATOR(BackwardSubsumptionResolution); - BackwardSubsumptionResolution(bool byUnitsOnly) : _byUnitsOnly(byUnitsOnly) {} void attach(SaturationAlgorithm* salg); diff --git a/Inferences/BinaryResolution.hpp b/Inferences/BinaryResolution.hpp index ccd12bace5..3290ecf625 100644 --- a/Inferences/BinaryResolution.hpp +++ b/Inferences/BinaryResolution.hpp @@ -33,8 +33,6 @@ class BinaryResolution : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(BinaryResolution); - BinaryResolution() : _index(0), _unificationWithAbstraction(false) diff --git a/Inferences/BoolEqToDiseq.hpp b/Inferences/BoolEqToDiseq.hpp index 2ec2490d3a..b09ff16667 100644 --- a/Inferences/BoolEqToDiseq.hpp +++ b/Inferences/BoolEqToDiseq.hpp @@ -24,8 +24,6 @@ namespace Inferences { class BoolEqToDiseq : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(BoolEqToDiseq); - ClauseIterator generateClauses(Clause* premise); }; diff --git a/Inferences/BoolSimp.hpp b/Inferences/BoolSimp.hpp index 1b93458e6e..6aab107c51 100644 --- a/Inferences/BoolSimp.hpp +++ b/Inferences/BoolSimp.hpp @@ -24,7 +24,6 @@ namespace Inferences { class BoolSimp : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(BoolSimp); Clause* simplify(Clause* premise); private: diff --git a/Inferences/CNFOnTheFly.hpp b/Inferences/CNFOnTheFly.hpp index a2b22e8939..9efb8f56ed 100644 --- a/Inferences/CNFOnTheFly.hpp +++ b/Inferences/CNFOnTheFly.hpp @@ -34,9 +34,6 @@ class IFFXORRewriterISE : public ImmediateSimplificationEngine { public: - - USE_ALLOCATOR(IFFXORRewriterISE); - Clause* simplify(Clause* c); }; @@ -44,9 +41,6 @@ class EagerClausificationISE : public ImmediateSimplificationEngine { public: - - USE_ALLOCATOR(EagerClausificationISE); - ClauseIterator simplifyMany(Clause* c); Clause* simplify(Clause* c){ NOT_IMPLEMENTED; } @@ -56,8 +50,6 @@ class LazyClausification : public SimplificationEngine { public: - USE_ALLOCATOR(LazyClausification); - LazyClausification(){ _formulaIndex = 0; } @@ -75,9 +67,6 @@ class LazyClausificationGIE : public GeneratingInferenceEngine { public: - - USE_ALLOCATOR(LazyClausificationGIE); - LazyClausificationGIE(){ _formulaIndex = 0; } @@ -95,8 +84,6 @@ class LazyClausificationGIE : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(NotProxyISE); - Kernel::Clause* simplify(Kernel::Clause* c); }; @@ -106,8 +93,6 @@ class EqualsProxyISE { public: - USE_ALLOCATOR(EqualsProxyISE); - Kernel::Clause* simplify(Kernel::Clause* c); }; @@ -117,8 +102,6 @@ class OrImpAndProxyISE { public: - USE_ALLOCATOR(OrImpAndProxyISE); - Kernel::Clause* simplify(Kernel::Clause* c); }; @@ -128,8 +111,6 @@ class PiSigmaProxyISE { public: - USE_ALLOCATOR(PiSigmaProxyISE); - Kernel::Clause* simplify(Kernel::Clause* c); }; @@ -137,7 +118,6 @@ class PiSigmaProxyISE class ProxyISE : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(ProxyISE); ClauseIterator simplifyMany(Clause* c); Clause* simplify(Clause* c){ NOT_IMPLEMENTED; } };*/ diff --git a/Inferences/Cancellation.hpp b/Inferences/Cancellation.hpp index 5cf454366e..9fb39495ed 100644 --- a/Inferences/Cancellation.hpp +++ b/Inferences/Cancellation.hpp @@ -20,8 +20,6 @@ class Cancellation : public SimplifyingGeneratingLiteralSimplification { public: - USE_ALLOCATOR(Cancellation); - Cancellation(Ordering& ordering); virtual ~Cancellation(); diff --git a/Inferences/Cases.hpp b/Inferences/Cases.hpp index f3336ab3da..434983e32b 100644 --- a/Inferences/Cases.hpp +++ b/Inferences/Cases.hpp @@ -23,8 +23,6 @@ namespace Inferences { class Cases : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(Cases); - Clause* performParamodulation(Clause* cl, Literal* lit, TermList t); ClauseIterator generateClauses(Clause* premise); struct RewriteableSubtermsFn; diff --git a/Inferences/CasesSimp.hpp b/Inferences/CasesSimp.hpp index 8de831cb85..8c4ec6d06e 100644 --- a/Inferences/CasesSimp.hpp +++ b/Inferences/CasesSimp.hpp @@ -23,8 +23,6 @@ namespace Inferences { class CasesSimp : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(CasesSimp); - ClauseIterator simplifyMany(Clause* premise); Clause* simplify(Clause* premise){ NOT_IMPLEMENTED; } diff --git a/Inferences/Choice.hpp b/Inferences/Choice.hpp index a60cc42896..0781dfe549 100644 --- a/Inferences/Choice.hpp +++ b/Inferences/Choice.hpp @@ -24,8 +24,6 @@ namespace Inferences { class Choice : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(Choice); - ClauseIterator generateClauses(Clause* premise); private: diff --git a/Inferences/CombinatorDemodISE.hpp b/Inferences/CombinatorDemodISE.hpp index 91de177a8c..86e4884374 100644 --- a/Inferences/CombinatorDemodISE.hpp +++ b/Inferences/CombinatorDemodISE.hpp @@ -25,8 +25,6 @@ class CombinatorDemodISE : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(CombinatorDemodISE); - CombinatorDemodISE(){} Clause* simplify(Clause* cl); private: diff --git a/Inferences/CombinatorNormalisationISE.hpp b/Inferences/CombinatorNormalisationISE.hpp index 483d01a113..2b3f9e4936 100644 --- a/Inferences/CombinatorNormalisationISE.hpp +++ b/Inferences/CombinatorNormalisationISE.hpp @@ -40,8 +40,6 @@ class CombinatorNormalisationISE : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(CombinatorNormalisationISE); - CombinatorNormalisationISE(){} Clause* simplify(Clause* cl); private: diff --git a/Inferences/Condensation.hpp b/Inferences/Condensation.hpp index 4f639404af..e4277a2ac2 100644 --- a/Inferences/Condensation.hpp +++ b/Inferences/Condensation.hpp @@ -34,8 +34,6 @@ class Condensation : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(Condensation); - Clause* simplify(Clause* cl); }; diff --git a/Inferences/DefinitionIntroduction.hpp b/Inferences/DefinitionIntroduction.hpp index baca76dd7f..64739a32b3 100644 --- a/Inferences/DefinitionIntroduction.hpp +++ b/Inferences/DefinitionIntroduction.hpp @@ -23,8 +23,6 @@ namespace Inferences class DefinitionIntroduction: public GeneratingInferenceEngine, public Index { public: - USE_ALLOCATOR(DefinitionIntroduction); - void attach(SaturationAlgorithm *salg) override { GeneratingInferenceEngine::attach(salg); attachContainer(salg->getPassiveClauseContainer()); diff --git a/Inferences/DistinctEqualitySimplifier.hpp b/Inferences/DistinctEqualitySimplifier.hpp index 5848a54567..eefd32fe1d 100644 --- a/Inferences/DistinctEqualitySimplifier.hpp +++ b/Inferences/DistinctEqualitySimplifier.hpp @@ -24,8 +24,6 @@ class DistinctEqualitySimplifier : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(DistinctEqualitySimplifier); - Clause* simplify(Clause* cl); static bool mustBeDistinct(TermList t1, TermList t2); static bool mustBeDistinct(TermList t1, TermList t2, unsigned& grp); diff --git a/Inferences/ElimLeibniz.hpp b/Inferences/ElimLeibniz.hpp index c0b799c31f..4d3a3c2d0e 100644 --- a/Inferences/ElimLeibniz.hpp +++ b/Inferences/ElimLeibniz.hpp @@ -25,8 +25,6 @@ namespace Inferences { class ElimLeibniz : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(ElimLeibniz); - ClauseIterator generateClauses(Clause* premise); private: diff --git a/Inferences/EqualityFactoring.hpp b/Inferences/EqualityFactoring.hpp index 410eb94f65..288e76af40 100644 --- a/Inferences/EqualityFactoring.hpp +++ b/Inferences/EqualityFactoring.hpp @@ -31,8 +31,6 @@ class EqualityFactoring : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(EqualityFactoring); - ClauseIterator generateClauses(Clause* premise); private: struct IsPositiveEqualityFn; diff --git a/Inferences/EqualityResolution.hpp b/Inferences/EqualityResolution.hpp index d2e2ec302a..328566e8b9 100644 --- a/Inferences/EqualityResolution.hpp +++ b/Inferences/EqualityResolution.hpp @@ -31,8 +31,6 @@ class EqualityResolution : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(EqualityResolution); - ClauseIterator generateClauses(Clause* premise); static Clause* tryResolveEquality(Clause* cl, Literal* toResolve); private: diff --git a/Inferences/EquationalTautologyRemoval.hpp b/Inferences/EquationalTautologyRemoval.hpp index a9caf2bfcd..38dead5650 100644 --- a/Inferences/EquationalTautologyRemoval.hpp +++ b/Inferences/EquationalTautologyRemoval.hpp @@ -26,8 +26,6 @@ class EquationalTautologyRemoval : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(EquationalTautologyRemoval); - EquationalTautologyRemoval() : _cc(nullptr) {} Clause* simplify(Clause* cl) override; diff --git a/Inferences/ExtensionalityResolution.hpp b/Inferences/ExtensionalityResolution.hpp index 4d03d09211..ce758909df 100644 --- a/Inferences/ExtensionalityResolution.hpp +++ b/Inferences/ExtensionalityResolution.hpp @@ -40,8 +40,6 @@ class ExtensionalityResolution : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(ExtensionalityResolution); - ExtensionalityResolution() {} ClauseIterator generateClauses(Clause* premise); diff --git a/Inferences/FOOLParamodulation.hpp b/Inferences/FOOLParamodulation.hpp index c2b5166a6a..0f98facd39 100644 --- a/Inferences/FOOLParamodulation.hpp +++ b/Inferences/FOOLParamodulation.hpp @@ -23,7 +23,6 @@ namespace Inferences { class FOOLParamodulation : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(FOOLParamodulation); ClauseIterator generateClauses(Clause* premise); }; diff --git a/Inferences/Factoring.hpp b/Inferences/Factoring.hpp index dd64c65a61..ce35398d23 100644 --- a/Inferences/Factoring.hpp +++ b/Inferences/Factoring.hpp @@ -30,8 +30,6 @@ class Factoring : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(Factoring); - ClauseIterator generateClauses(Clause* premise); private: class UnificationsOnPositiveFn; diff --git a/Inferences/FastCondensation.hpp b/Inferences/FastCondensation.hpp index 98610c0758..552f2b942c 100644 --- a/Inferences/FastCondensation.hpp +++ b/Inferences/FastCondensation.hpp @@ -43,8 +43,6 @@ class FastCondensation : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(FastCondensation); - Clause* simplify(Clause* cl); private: struct CondensationBinder; diff --git a/Inferences/ForwardDemodulation.hpp b/Inferences/ForwardDemodulation.hpp index 918480dce1..fabdf1a21f 100644 --- a/Inferences/ForwardDemodulation.hpp +++ b/Inferences/ForwardDemodulation.hpp @@ -32,8 +32,6 @@ class ForwardDemodulation : public ForwardSimplificationEngine { public: - USE_ALLOCATOR(ForwardDemodulation); - void attach(SaturationAlgorithm* salg) override; void detach() override; bool perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) override = 0; @@ -49,8 +47,6 @@ class ForwardDemodulationImpl : public ForwardDemodulation { public: - USE_ALLOCATOR(ForwardDemodulationImpl); - bool perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) override; private: }; diff --git a/Inferences/ForwardLiteralRewriting.hpp b/Inferences/ForwardLiteralRewriting.hpp index bed1280c99..9abf914c1c 100644 --- a/Inferences/ForwardLiteralRewriting.hpp +++ b/Inferences/ForwardLiteralRewriting.hpp @@ -31,8 +31,6 @@ class ForwardLiteralRewriting : public ForwardSimplificationEngine { public: - USE_ALLOCATOR(ForwardLiteralRewriting); - void attach(SaturationAlgorithm* salg) override; void detach() override; bool perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) override; diff --git a/Inferences/ForwardSubsumptionAndResolution.hpp b/Inferences/ForwardSubsumptionAndResolution.hpp index d92e5c9718..3d94fd1240 100644 --- a/Inferences/ForwardSubsumptionAndResolution.hpp +++ b/Inferences/ForwardSubsumptionAndResolution.hpp @@ -30,8 +30,6 @@ class ForwardSubsumptionAndResolution : public ForwardSimplificationEngine { public: - USE_ALLOCATOR(ForwardSubsumptionAndResolution); - ForwardSubsumptionAndResolution(bool subsumptionResolution=true) : _subsumptionResolution(subsumptionResolution) {} diff --git a/Inferences/ForwardSubsumptionDemodulation.hpp b/Inferences/ForwardSubsumptionDemodulation.hpp index 59f6be6970..bbcb2037ab 100644 --- a/Inferences/ForwardSubsumptionDemodulation.hpp +++ b/Inferences/ForwardSubsumptionDemodulation.hpp @@ -48,8 +48,6 @@ class ForwardSubsumptionDemodulation : public ForwardSimplificationEngine { public: - USE_ALLOCATOR(ForwardSubsumptionDemodulation); - ForwardSubsumptionDemodulation(bool doSubsumption) : _doSubsumption(doSubsumption) { } diff --git a/Inferences/GaussianVariableElimination.hpp b/Inferences/GaussianVariableElimination.hpp index 2a2b4d5c01..a979d76d79 100644 --- a/Inferences/GaussianVariableElimination.hpp +++ b/Inferences/GaussianVariableElimination.hpp @@ -18,8 +18,6 @@ class GaussianVariableElimination : public SimplifyingGeneratingInference1 { public: - USE_ALLOCATOR(GaussianVariableElimination); - SimplifyingGeneratingInference1::Result simplify(Clause *cl, bool doCheckOrdering) override; private: SimplifyingGeneratingInference1::Result rewrite(Clause &cl, TermList find, TermList replace, diff --git a/Inferences/GlobalSubsumption.hpp b/Inferences/GlobalSubsumption.hpp index d0ba11a9f1..6797ea4a74 100644 --- a/Inferences/GlobalSubsumption.hpp +++ b/Inferences/GlobalSubsumption.hpp @@ -35,8 +35,6 @@ class GlobalSubsumption : public ForwardSimplificationEngine { public: - USE_ALLOCATOR(GlobalSubsumption); - GlobalSubsumption(const Options& opts) : _index(0), _uprOnly(opts.globalSubsumptionSatSolverPower()==Options::GlobalSubsumptionSatSolverPower::PROPAGATION_ONLY), _explicitMinim(opts.globalSubsumptionExplicitMinim()!=Options::GlobalSubsumptionExplicitMinim::OFF), diff --git a/Inferences/Induction.hpp b/Inferences/Induction.hpp index c10620e15b..025d7b5b8d 100644 --- a/Inferences/Induction.hpp +++ b/Inferences/Induction.hpp @@ -162,8 +162,6 @@ class Induction : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(Induction); - void attach(SaturationAlgorithm* salg) override; void detach() override; diff --git a/Inferences/InductionHelper.hpp b/Inferences/InductionHelper.hpp index 82cd8df91a..85e1dfbf24 100644 --- a/Inferences/InductionHelper.hpp +++ b/Inferences/InductionHelper.hpp @@ -31,8 +31,6 @@ using namespace Kernel; class InductionHelper { public: - USE_ALLOCATOR(InductionHelper); - InductionHelper(LiteralIndex* comparisonIndex, TermIndex* inductionTermIndex) : _comparisonIndex(comparisonIndex), _inductionTermIndex(inductionTermIndex) {} diff --git a/Inferences/InferenceEngine.hpp b/Inferences/InferenceEngine.hpp index 00e648aecf..b758d2d82f 100644 --- a/Inferences/InferenceEngine.hpp +++ b/Inferences/InferenceEngine.hpp @@ -52,8 +52,6 @@ using namespace Shell; class InferenceEngine { public: - USE_ALLOCATOR(InferenceEngine); - InferenceEngine() : _salg(0) {} virtual ~InferenceEngine() { @@ -310,8 +308,6 @@ class DummyGIE : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(DummyGIE); - ClauseIterator generateClauses(Clause* premise) { return ClauseIterator::getEmpty(); @@ -323,8 +319,6 @@ class DummyFSE : public ForwardSimplificationEngine { public: - USE_ALLOCATOR(DummyFSE); - void perform(Clause* cl, bool& keep, ClauseIterator& toAdd, ClauseIterator& premises) { keep=true; @@ -337,8 +331,6 @@ class DummyBSE : public BackwardSimplificationEngine { public: - USE_ALLOCATOR(DummyBSE); - void perform(Clause* premise, BwSimplificationRecordIterator& simplifications) { simplifications=BwSimplificationRecordIterator::getEmpty(); @@ -350,8 +342,6 @@ class CompositeISE : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(CompositeISE); - CompositeISE() : _inners(0), _innersMany(0) {} virtual ~CompositeISE(); void addFront(ImmediateSimplificationEngine* fse); @@ -385,8 +375,6 @@ class CompositeGIE : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(CompositeGIE); - CompositeGIE() : _inners(0) {} virtual ~CompositeGIE(); void addFront(GeneratingInferenceEngine* fse); @@ -403,8 +391,6 @@ class CompositeSGI : public SimplifyingGeneratingInference { public: - USE_ALLOCATOR(CompositeSGI); - CompositeSGI() : _simplifiers(), _generators() {} virtual ~CompositeSGI(); void push(SimplifyingGeneratingInference*); @@ -422,8 +408,6 @@ class ChoiceDefinitionISE : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(ChoiceDefinitionISE); - Clause* simplify(Clause* cl); bool isPositive(Literal* lit); @@ -436,8 +420,6 @@ class DuplicateLiteralRemovalISE : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(DuplicateLiteralRemovalISE); - Clause* simplify(Clause* cl); }; @@ -445,8 +427,6 @@ class TautologyDeletionISE2 : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(TautologyDeletionISE2); - Clause* simplify(Clause* cl); }; diff --git a/Inferences/Injectivity.hpp b/Inferences/Injectivity.hpp index 8556811a1a..d714caa4f4 100644 --- a/Inferences/Injectivity.hpp +++ b/Inferences/Injectivity.hpp @@ -23,7 +23,6 @@ namespace Inferences { class Injectivity : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(Injectivity); ClauseIterator generateClauses(Clause* premise); private: diff --git a/Inferences/InnerRewriting.hpp b/Inferences/InnerRewriting.hpp index fafe61f15d..1f163e0a61 100644 --- a/Inferences/InnerRewriting.hpp +++ b/Inferences/InnerRewriting.hpp @@ -30,8 +30,6 @@ class InnerRewriting : public ForwardSimplificationEngine { public: - USE_ALLOCATOR(InnerRewriting); - bool perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) override; }; diff --git a/Inferences/Instantiation.hpp b/Inferences/Instantiation.hpp index a594c50b29..a7f15d10d3 100644 --- a/Inferences/Instantiation.hpp +++ b/Inferences/Instantiation.hpp @@ -33,8 +33,6 @@ class Instantiation : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(Instantiation); - Instantiation() {} //void init(); diff --git a/Inferences/InterpretedEvaluation.hpp b/Inferences/InterpretedEvaluation.hpp index e68cfe88a2..20e009cae1 100644 --- a/Inferences/InterpretedEvaluation.hpp +++ b/Inferences/InterpretedEvaluation.hpp @@ -31,8 +31,6 @@ class InterpretedEvaluation : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(InterpretedEvaluation); - InterpretedEvaluation(bool doNormalize, Ordering& ordering); virtual ~InterpretedEvaluation(); diff --git a/Inferences/InvalidAnswerLiteralRemoval.hpp b/Inferences/InvalidAnswerLiteralRemoval.hpp index c7e9e139ee..167582ddd4 100644 --- a/Inferences/InvalidAnswerLiteralRemoval.hpp +++ b/Inferences/InvalidAnswerLiteralRemoval.hpp @@ -28,8 +28,6 @@ class InvalidAnswerLiteralRemoval : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(InvalidAnswerLiteralRemoval); - Clause* simplify(Clause* cl) override; }; diff --git a/Inferences/LfpRule.hpp b/Inferences/LfpRule.hpp index 409232e53d..e603c90eaf 100644 --- a/Inferences/LfpRule.hpp +++ b/Inferences/LfpRule.hpp @@ -21,8 +21,6 @@ class LfpRule { Rule _inner; public: - USE_ALLOCATOR(LfpRule); - LfpRule(Rule rule); LfpRule(); SimplifyingGeneratingInference1::Result simplify(Clause *cl, bool doCheckOrdering) override; diff --git a/Inferences/Narrow.hpp b/Inferences/Narrow.hpp index 91772e8427..ccc0d66ae6 100644 --- a/Inferences/Narrow.hpp +++ b/Inferences/Narrow.hpp @@ -31,8 +31,6 @@ class Narrow : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(Narrow); - ClauseIterator generateClauses(Clause* premise); void attach(SaturationAlgorithm* salg); diff --git a/Inferences/NegativeExt.hpp b/Inferences/NegativeExt.hpp index 078ff01ee9..e46258b8dc 100644 --- a/Inferences/NegativeExt.hpp +++ b/Inferences/NegativeExt.hpp @@ -31,8 +31,6 @@ class NegativeExt : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(NegativeExt); - ClauseIterator generateClauses(Clause* premise); private: struct ResultFn; diff --git a/Inferences/PolynomialEvaluation.hpp b/Inferences/PolynomialEvaluation.hpp index b6ac82d000..8a40178520 100644 --- a/Inferences/PolynomialEvaluation.hpp +++ b/Inferences/PolynomialEvaluation.hpp @@ -30,8 +30,6 @@ class PolynomialEvaluation : public SimplifyingGeneratingLiteralSimplification { public: - USE_ALLOCATOR(PolynomialEvaluation); - PolynomialEvaluation(Ordering& ordering); virtual ~PolynomialEvaluation(); diff --git a/Inferences/PrimitiveInstantiation.hpp b/Inferences/PrimitiveInstantiation.hpp index 58fc987e44..75aa3b5774 100644 --- a/Inferences/PrimitiveInstantiation.hpp +++ b/Inferences/PrimitiveInstantiation.hpp @@ -31,8 +31,6 @@ class PrimitiveInstantiation : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(PrimitiveInstantiation); - void attach(SaturationAlgorithm* salg); void detach(); diff --git a/Inferences/PushUnaryMinus.hpp b/Inferences/PushUnaryMinus.hpp index 4e105b901e..a4e4c62cde 100644 --- a/Inferences/PushUnaryMinus.hpp +++ b/Inferences/PushUnaryMinus.hpp @@ -27,8 +27,6 @@ class PushUnaryMinus : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(PushUnaryMinus); - virtual ~PushUnaryMinus(); Clause* simplify(Clause* cl); diff --git a/Inferences/RenamingOnTheFly.hpp b/Inferences/RenamingOnTheFly.hpp index 962736f2bd..a095875d28 100644 --- a/Inferences/RenamingOnTheFly.hpp +++ b/Inferences/RenamingOnTheFly.hpp @@ -31,8 +31,6 @@ class RenamingOnTheFly : public SimplificationEngine { public: - USE_ALLOCATOR(RenamingOnTheFly); - ClauseIterator perform(Clause* c); void attach(SaturationAlgorithm* salg) override; diff --git a/Inferences/SLQueryBackwardSubsumption.hpp b/Inferences/SLQueryBackwardSubsumption.hpp index 01cd9841cc..da7de2a5bc 100644 --- a/Inferences/SLQueryBackwardSubsumption.hpp +++ b/Inferences/SLQueryBackwardSubsumption.hpp @@ -26,8 +26,6 @@ class SLQueryBackwardSubsumption : public BackwardSimplificationEngine { public: - USE_ALLOCATOR(SLQueryBackwardSubsumption); - SLQueryBackwardSubsumption(bool byUnitsOnly) : _byUnitsOnly(byUnitsOnly), _index(0) {} /** diff --git a/Inferences/SubVarSup.hpp b/Inferences/SubVarSup.hpp index 4fde6f70dd..8c1d6f5642 100644 --- a/Inferences/SubVarSup.hpp +++ b/Inferences/SubVarSup.hpp @@ -31,8 +31,6 @@ class SubVarSup : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(SubVarSup); - void attach(SaturationAlgorithm* salg); void detach(); diff --git a/Inferences/Superposition.hpp b/Inferences/Superposition.hpp index 46678f78c9..de6efe38c1 100644 --- a/Inferences/Superposition.hpp +++ b/Inferences/Superposition.hpp @@ -31,8 +31,6 @@ class Superposition : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(Superposition); - void attach(SaturationAlgorithm* salg); void detach(); diff --git a/Inferences/TautologyDeletionISE.hpp b/Inferences/TautologyDeletionISE.hpp index 2b7c8e6b3e..3ceec54cc8 100644 --- a/Inferences/TautologyDeletionISE.hpp +++ b/Inferences/TautologyDeletionISE.hpp @@ -25,8 +25,6 @@ class TautologyDeletionISE : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(TautologyDeletionISE); - TautologyDeletionISE(bool deleteEqTautologies=true) : _deleteEqTautologies(deleteEqTautologies) {} Clause* simplify(Clause* cl); private: diff --git a/Inferences/TermAlgebraReasoning.hpp b/Inferences/TermAlgebraReasoning.hpp index ab00ca5e5f..9088427aba 100644 --- a/Inferences/TermAlgebraReasoning.hpp +++ b/Inferences/TermAlgebraReasoning.hpp @@ -50,8 +50,6 @@ class DistinctnessISE { public: - USE_ALLOCATOR(DistinctnessISE); - Kernel::Clause* simplify(Kernel::Clause* c); }; @@ -69,8 +67,6 @@ class DistinctnessISE class InjectivityGIE : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(InjectivityGIE); - Kernel::ClauseIterator generateClauses(Kernel::Clause* c); private: @@ -91,8 +87,6 @@ class InjectivityISE : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(InjectivityISE); - Kernel::Clause* simplify(Kernel::Clause* c); }; @@ -100,8 +94,6 @@ class NegativeInjectivityISE : public ImmediateSimplificationEngine { public: - USE_ALLOCATOR(NegativeInjectivityISE); - Kernel::Clause* simplify(Kernel::Clause* c); private: @@ -111,8 +103,6 @@ class NegativeInjectivityISE class AcyclicityGIE : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(AcyclicityGIE); - void attach(Saturation::SaturationAlgorithm* salg); void detach(); Kernel::ClauseIterator generateClauses(Kernel::Clause *c); @@ -126,8 +116,6 @@ class AcyclicityGIE class AcyclicityGIE1 : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(AcyclicityGIE1); - Kernel::ClauseIterator generateClauses(Kernel::Clause* c); private: diff --git a/Inferences/TheoryInstAndSimp.hpp b/Inferences/TheoryInstAndSimp.hpp index de3d14353c..19a632220e 100644 --- a/Inferences/TheoryInstAndSimp.hpp +++ b/Inferences/TheoryInstAndSimp.hpp @@ -48,8 +48,6 @@ class TheoryInstAndSimp { public: using SortId = SAT::Z3Interfacing::SortId; - USE_ALLOCATOR(TheoryInstAndSimp); - ~TheoryInstAndSimp(); TheoryInstAndSimp() : TheoryInstAndSimp(*env.options) {} diff --git a/Inferences/URResolution.hpp b/Inferences/URResolution.hpp index 52cd86f625..aee40695f8 100644 --- a/Inferences/URResolution.hpp +++ b/Inferences/URResolution.hpp @@ -30,8 +30,6 @@ class URResolution : public GeneratingInferenceEngine { public: - USE_ALLOCATOR(URResolution); - URResolution(); URResolution(bool selectedOnly, UnitClauseLiteralIndex* unitIndex, NonUnitClauseLiteralIndex* nonUnitIndex); diff --git a/Kernel/BestLiteralSelector.hpp b/Kernel/BestLiteralSelector.hpp index b98ab96955..447ee06c1a 100644 --- a/Kernel/BestLiteralSelector.hpp +++ b/Kernel/BestLiteralSelector.hpp @@ -54,8 +54,6 @@ class BestLiteralSelector : public LiteralSelector { public: - USE_ALLOCATOR(BestLiteralSelector); - BestLiteralSelector(const Ordering& ordering, const Options& options) : LiteralSelector(ordering, options) { _comp.attachSelector(this); @@ -115,8 +113,6 @@ class CompleteBestLiteralSelector : public LiteralSelector { public: - USE_ALLOCATOR(CompleteBestLiteralSelector); - CompleteBestLiteralSelector(const Ordering& ordering, const Options& options) : LiteralSelector(ordering, options) { _comp.attachSelector(this); diff --git a/Kernel/ELiteralSelector.hpp b/Kernel/ELiteralSelector.hpp index 2d150fcd33..7ced1dcaad 100644 --- a/Kernel/ELiteralSelector.hpp +++ b/Kernel/ELiteralSelector.hpp @@ -32,8 +32,6 @@ class ELiteralSelector : public LiteralSelector { public: - USE_ALLOCATOR(ELiteralSelector); - enum Values { // NoSelection, -- not implemented, this would be the same as spass's OFF SelectNegativeLiterals = 0, diff --git a/Kernel/Grounder.hpp b/Kernel/Grounder.hpp index 62560fa55a..666107043a 100644 --- a/Kernel/Grounder.hpp +++ b/Kernel/Grounder.hpp @@ -30,8 +30,6 @@ using namespace SAT; class Grounder { public: - USE_ALLOCATOR(Grounder); - Grounder(SATSolver* satSolver) : _satSolver(satSolver) {} virtual ~Grounder() {} @@ -69,8 +67,6 @@ class GlobalSubsumptionGrounder : public Grounder { bool _doNormalization; public: - USE_ALLOCATOR(GlobalSubsumptionGrounder); - GlobalSubsumptionGrounder(SATSolver* satSolver, bool doNormalization=true) : Grounder(satSolver), _doNormalization(doNormalization) {} protected: @@ -79,8 +75,6 @@ class GlobalSubsumptionGrounder : public Grounder { class IGGrounder : public Grounder { public: - USE_ALLOCATOR(IGGrounder); - IGGrounder(SATSolver* satSolver); private: TermList _tgtTerm; diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp index 256e5c5392..b56593fd94 100644 --- a/Kernel/InferenceStore.cpp +++ b/Kernel/InferenceStore.cpp @@ -246,8 +246,6 @@ struct UnitNumberComparator struct InferenceStore::ProofPrinter { - USE_ALLOCATOR(InferenceStore::ProofPrinter); - ProofPrinter(ostream& out, InferenceStore* is) : _is(is), out(out) { @@ -426,8 +424,6 @@ struct InferenceStore::ProofPrinter struct InferenceStore::ProofPropertyPrinter : public InferenceStore::ProofPrinter { - USE_ALLOCATOR(InferenceStore::ProofPropertyPrinter); - ProofPropertyPrinter(ostream& out, InferenceStore* is) : ProofPrinter(out,is) { max_theory_clause_depth = 0; @@ -511,8 +507,6 @@ struct InferenceStore::ProofPropertyPrinter struct InferenceStore::TPTPProofPrinter : public InferenceStore::ProofPrinter { - USE_ALLOCATOR(InferenceStore::TPTPProofPrinter); - TPTPProofPrinter(ostream& out, InferenceStore* is) : ProofPrinter(out, is) { splitPrefix = Saturation::Splitter::splPrefix; @@ -874,8 +868,6 @@ struct InferenceStore::TPTPProofPrinter struct InferenceStore::ProofCheckPrinter : public InferenceStore::ProofPrinter { - USE_ALLOCATOR(InferenceStore::ProofCheckPrinter); - ProofCheckPrinter(ostream& out, InferenceStore* is) : ProofPrinter(out, is) {} diff --git a/Kernel/InferenceStore.hpp b/Kernel/InferenceStore.hpp index 1064506562..4f6af86c27 100644 --- a/Kernel/InferenceStore.hpp +++ b/Kernel/InferenceStore.hpp @@ -38,8 +38,6 @@ using namespace Lib; class InferenceStore { public: - USE_ALLOCATOR(InferenceStore); - static InferenceStore* instance(); typedef List IntList; diff --git a/Kernel/InterpretedLiteralEvaluator.cpp b/Kernel/InterpretedLiteralEvaluator.cpp index 856fcf685e..fda6dae45f 100644 --- a/Kernel/InterpretedLiteralEvaluator.cpp +++ b/Kernel/InterpretedLiteralEvaluator.cpp @@ -67,8 +67,6 @@ struct PredEvalResult { class InterpretedLiteralEvaluator::Evaluator { public: - USE_ALLOCATOR(InterpretedLiteralEvaluator::Evaluator); - virtual ~Evaluator() {} virtual bool canEvaluateFunc(unsigned func) { return false; } @@ -130,8 +128,6 @@ template : public Evaluator { public: - USE_ALLOCATOR(InterpretedLiteralEvaluator::ACFunEvaluator); - using ConstantType = typename AbelianGroup::ConstantType; ACFunEvaluator() : _fun(env.signature->getInterpretingSymbol(AbelianGroup::interpreation)) { } diff --git a/Kernel/InterpretedLiteralEvaluator.hpp b/Kernel/InterpretedLiteralEvaluator.hpp index 7e5637963d..d71f37a957 100644 --- a/Kernel/InterpretedLiteralEvaluator.hpp +++ b/Kernel/InterpretedLiteralEvaluator.hpp @@ -31,8 +31,6 @@ class InterpretedLiteralEvaluator : private BottomUpTermTransformer { public: - USE_ALLOCATOR(InterpretedLiteralEvaluator); - InterpretedLiteralEvaluator(bool doNormalize = true); ~InterpretedLiteralEvaluator(); diff --git a/Kernel/KBO.cpp b/Kernel/KBO.cpp index dcf5622583..6a520a1cb2 100644 --- a/Kernel/KBO.cpp +++ b/Kernel/KBO.cpp @@ -57,8 +57,6 @@ class KBO::State _varDiffs.reset(); } - USE_ALLOCATOR(State); - void traverse(Term* t1, Term* t2); void traverse(TermList tl,int coefficient); Result result(Term* t1, Term* t2); diff --git a/Kernel/KBO.hpp b/Kernel/KBO.hpp index 61f7bf20a0..0f7ae0cca5 100644 --- a/Kernel/KBO.hpp +++ b/Kernel/KBO.hpp @@ -127,8 +127,6 @@ class KBO : public PrecedenceOrdering { public: - USE_ALLOCATOR(KBO); - KBO(Problem& prb, const Options& opt); KBO( // KBO params diff --git a/Kernel/KBOForEPR.hpp b/Kernel/KBOForEPR.hpp index 2089f1d5f2..e17b2c0266 100644 --- a/Kernel/KBOForEPR.hpp +++ b/Kernel/KBOForEPR.hpp @@ -31,8 +31,6 @@ class KBOForEPR : public PrecedenceOrdering { public: - USE_ALLOCATOR(KBOForEPR); - KBOForEPR(Problem& prb, const Options& opt); using PrecedenceOrdering::compare; diff --git a/Kernel/LPO.hpp b/Kernel/LPO.hpp index aa927f85e5..83433a355b 100644 --- a/Kernel/LPO.hpp +++ b/Kernel/LPO.hpp @@ -33,8 +33,6 @@ class LPO : public PrecedenceOrdering { public: - USE_ALLOCATOR(LPO); - LPO(Problem& prb, const Options& opt) : PrecedenceOrdering(prb, opt) {} diff --git a/Kernel/LiteralSelector.hpp b/Kernel/LiteralSelector.hpp index 7610d7fed3..2871caa584 100644 --- a/Kernel/LiteralSelector.hpp +++ b/Kernel/LiteralSelector.hpp @@ -36,8 +36,6 @@ using namespace Shell; class LiteralSelector { public: - USE_ALLOCATOR(LiteralSelector); - LiteralSelector(const Ordering& ordering, const Options& options) : _ord(ordering), _opt(options), _reversePolarity(false) { @@ -122,8 +120,6 @@ class TotalLiteralSelector : public LiteralSelector { public: - USE_ALLOCATOR(TotalLiteralSelector); - TotalLiteralSelector(const Ordering& ordering, const Options& options) : LiteralSelector(ordering, options) {} diff --git a/Kernel/LookaheadLiteralSelector.hpp b/Kernel/LookaheadLiteralSelector.hpp index 5f5f5c2efc..98f3471e56 100644 --- a/Kernel/LookaheadLiteralSelector.hpp +++ b/Kernel/LookaheadLiteralSelector.hpp @@ -25,8 +25,6 @@ class LookaheadLiteralSelector : public LiteralSelector { public: - USE_ALLOCATOR(LookaheadLiteralSelector); - LookaheadLiteralSelector(bool completeSelection, const Ordering& ordering, const Options& options) : LiteralSelector(ordering, options), _completeSelection(completeSelection) { diff --git a/Kernel/MainLoop.hpp b/Kernel/MainLoop.hpp index 65f789384a..2f2683a2fd 100644 --- a/Kernel/MainLoop.hpp +++ b/Kernel/MainLoop.hpp @@ -53,9 +53,7 @@ struct MainLoopResult class MainLoop { -public: - USE_ALLOCATOR(MainLoop); - +public: MainLoop(Problem& prb, const Options& opt) : _prb(prb), _opt(opt) {} virtual ~MainLoop() {} diff --git a/Kernel/MaximalLiteralSelector.hpp b/Kernel/MaximalLiteralSelector.hpp index d1149d447d..183ea1123d 100644 --- a/Kernel/MaximalLiteralSelector.hpp +++ b/Kernel/MaximalLiteralSelector.hpp @@ -34,8 +34,6 @@ class MaximalLiteralSelector : public LiteralSelector { public: - USE_ALLOCATOR(MaximalLiteralSelector); - MaximalLiteralSelector(const Ordering& ordering, const Options& options) : LiteralSelector(ordering, options) {} bool isBGComplete() const override { return true; } diff --git a/Kernel/MismatchHandler.hpp b/Kernel/MismatchHandler.hpp index 0dffedb3f6..793c3ac36a 100644 --- a/Kernel/MismatchHandler.hpp +++ b/Kernel/MismatchHandler.hpp @@ -35,8 +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); - USE_ALLOCATOR(UWAMismatchHandler); - private: bool checkUWA(TermList t1, TermList t2); virtual bool introduceConstraint(TermList t1,unsigned index1, TermList t2, unsigned index2); @@ -52,8 +50,6 @@ class HOMismatchHandler : public MismatchHandler virtual bool handle(RobSubstitution* sub, TermList t1, unsigned index1, TermList t2, unsigned index2); - USE_ALLOCATOR(HOMismatchHandler); - private: Stack& constraints; diff --git a/Kernel/OperatorType.hpp b/Kernel/OperatorType.hpp index 4435dacc1b..856f7bb7aa 100644 --- a/Kernel/OperatorType.hpp +++ b/Kernel/OperatorType.hpp @@ -55,8 +55,6 @@ namespace Kernel { class OperatorType { public: - USE_ALLOCATOR(OperatorType); - class TypeHash { public: static bool equals(OperatorType* t1, OperatorType* t2) diff --git a/Kernel/Ordering.hpp b/Kernel/Ordering.hpp index ee2995a9d4..d8a11ec75f 100644 --- a/Kernel/Ordering.hpp +++ b/Kernel/Ordering.hpp @@ -39,8 +39,6 @@ using namespace Shell; class Ordering { public: - USE_ALLOCATOR(Ordering); - /** * Represents the results of ordering comparisons * diff --git a/Kernel/Ordering_Equality.cpp b/Kernel/Ordering_Equality.cpp index 9ddbc28773..0307f93c62 100644 --- a/Kernel/Ordering_Equality.cpp +++ b/Kernel/Ordering_Equality.cpp @@ -24,8 +24,6 @@ namespace Kernel class Ordering::EqCmp { public: - USE_ALLOCATOR(EqCmp); - EqCmp(Ordering* ordering) : _ordering(ordering) { #if VDEBUG diff --git a/Kernel/Problem.hpp b/Kernel/Problem.hpp index 62c89deffa..e333d5954d 100644 --- a/Kernel/Problem.hpp +++ b/Kernel/Problem.hpp @@ -49,9 +49,6 @@ class Problem { Problem(const Problem&); //private and undefined copy constructor Problem& operator=(const Problem&); //private and undefined assignment operator public: - - USE_ALLOCATOR(Problem); - explicit Problem(UnitList* units=0); explicit Problem(ClauseIterator clauses, bool copy); ~Problem(); diff --git a/Kernel/Renaming.hpp b/Kernel/Renaming.hpp index 58975ad3af..4bc9982806 100644 --- a/Kernel/Renaming.hpp +++ b/Kernel/Renaming.hpp @@ -33,8 +33,6 @@ using namespace Lib; class Renaming { public: - USE_ALLOCATOR(Renaming); - Renaming() : _nextVar(0), _identity(true) { } diff --git a/Kernel/RndLiteralSelector.hpp b/Kernel/RndLiteralSelector.hpp index 729d7435ad..b54529893b 100644 --- a/Kernel/RndLiteralSelector.hpp +++ b/Kernel/RndLiteralSelector.hpp @@ -32,8 +32,6 @@ class RndLiteralSelector : public LiteralSelector { public: - USE_ALLOCATOR(RndLiteralSelector); - RndLiteralSelector(const Ordering& ordering, const Options& options, bool complete) : LiteralSelector(ordering, options), _complete(complete) {} diff --git a/Kernel/SKIKBO.cpp b/Kernel/SKIKBO.cpp index 9bba413475..1416cac622 100644 --- a/Kernel/SKIKBO.cpp +++ b/Kernel/SKIKBO.cpp @@ -58,8 +58,6 @@ class SKIKBO::State _varDiffs.reset(); } - USE_ALLOCATOR(State); - void traverse(ArgsIt_ptr aai1, ArgsIt_ptr aai2); void traverse(ArgsIt_ptr aai, int coefficient); Result result(ArgsIt_ptr aai1, ArgsIt_ptr aai2); diff --git a/Kernel/SKIKBO.hpp b/Kernel/SKIKBO.hpp index aaa94d2f6e..72bc8b4744 100644 --- a/Kernel/SKIKBO.hpp +++ b/Kernel/SKIKBO.hpp @@ -40,8 +40,6 @@ class SKIKBO : public PrecedenceOrdering { public: - USE_ALLOCATOR(SKIKBO); - SKIKBO(Problem& prb, const Options& opt, bool basic_hol = false); SKIKBO( // KBO params diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp index d1d14c2750..307aa7469c 100644 --- a/Kernel/Signature.hpp +++ b/Kernel/Signature.hpp @@ -315,8 +315,6 @@ class Signature OperatorType* fnType() const; OperatorType* predType() const; OperatorType* typeConType() const; - - USE_ALLOCATOR(Symbol); }; // class Symbol class InterpretedSymbol @@ -334,8 +332,6 @@ class Signature { } - USE_ALLOCATOR(InterpretedSymbol); - /** Return the interpreted function that corresponds to this symbol */ inline Interpretation getInterpretation() const { ASS_REP(interpreted(), _name); return _interp; } }; @@ -354,7 +350,6 @@ class Signature { setType(OperatorType::getConstantsType(AtomicSort::intSort())); } - USE_ALLOCATOR(IntegerSymbol); }; class RationalSymbol @@ -371,7 +366,6 @@ class Signature { setType(OperatorType::getConstantsType(AtomicSort::rationalSort())); } - USE_ALLOCATOR(RationalSymbol); }; class RealSymbol @@ -388,7 +382,6 @@ class Signature { setType(OperatorType::getConstantsType(AtomicSort::realSort())); } - USE_ALLOCATOR(RealSymbol); }; ////////////////////////////////////// @@ -575,8 +568,6 @@ class Signature Signature(); ~Signature(); - USE_ALLOCATOR(Signature); - bool functionExists(const vstring& name,unsigned arity) const; bool predicateExists(const vstring& name,unsigned arity) const; bool typeConExists(const vstring& name,unsigned arity) const; diff --git a/Kernel/SpassLiteralSelector.hpp b/Kernel/SpassLiteralSelector.hpp index 95a1a6fdfa..59e379508e 100644 --- a/Kernel/SpassLiteralSelector.hpp +++ b/Kernel/SpassLiteralSelector.hpp @@ -32,8 +32,6 @@ class SpassLiteralSelector : public LiteralSelector { public: - USE_ALLOCATOR(SpassLiteralSelector); - enum Values { OFF = 0, IFSEVERALMAXIMAL = 1, diff --git a/Lib/Coproduct.hpp b/Lib/Coproduct.hpp index 105b5b6ee6..8957abe47f 100644 --- a/Lib/Coproduct.hpp +++ b/Lib/Coproduct.hpp @@ -75,7 +75,6 @@ namespace CoproductImpl { * data VariadicUnion (a::as) = union {a, Coproduct as} */ template union VariadicUnion { - // USE_ALLOCATOR(VariadicUnion) using Ts = TL::List; A _head; diff --git a/Lib/Event.hpp b/Lib/Event.hpp index 084d6557ac..37e2112998 100644 --- a/Lib/Event.hpp +++ b/Lib/Event.hpp @@ -67,8 +67,6 @@ class SubscriptionObject ~SubscriptionObject(); void unsubscribe(); bool belongsTo(BaseEvent& evt); - - USE_ALLOCATOR(SubscriptionObject); private: BaseEvent* event; BaseEvent::HandlerStruct* hs; @@ -110,7 +108,6 @@ class PlainEvent { (pObj->*pMethod)(); } - USE_ALLOCATOR(MethodSpecificHandlerStruct); }; template @@ -159,8 +156,6 @@ class SingleParamEvent { (pObj->*pMethod)(t); } - - USE_ALLOCATOR(MethodSpecificHandlerStruct); }; template @@ -212,8 +207,6 @@ class TwoParamEvent { (pObj->*pMethod)(t1, t2); } - - USE_ALLOCATOR(MethodSpecificHandlerStruct); }; template diff --git a/Lib/Timer.hpp b/Lib/Timer.hpp index 342f43500f..a11609da65 100644 --- a/Lib/Timer.hpp +++ b/Lib/Timer.hpp @@ -36,8 +36,6 @@ class Timer ~Timer() { deinitializeTimer(); } public: - USE_ALLOCATOR(Timer); - static Timer* instance(); /** stop the timer and reset the clock */ diff --git a/Parse/TPTP.hpp b/Parse/TPTP.hpp index 5c1b336521..c03beed698 100644 --- a/Parse/TPTP.hpp +++ b/Parse/TPTP.hpp @@ -355,7 +355,6 @@ class TPTP */ class Type { public: - USE_ALLOCATOR(Type); explicit Type(TypeTag tag) : _tag(tag) {} /** return the kind of this sort */ TypeTag tag() const {return _tag;} @@ -369,7 +368,6 @@ class TPTP : public Type { public: - USE_ALLOCATOR(AtomicType); explicit AtomicType(TermList sort) : Type(TT_ATOMIC), _sort(sort) {} @@ -385,7 +383,6 @@ class TPTP : public Type { public: - USE_ALLOCATOR(ArrowType); ArrowType(Type* lhs,Type* rhs) : Type(TT_ARROW), _lhs(lhs), _rhs(rhs) {} @@ -408,7 +405,6 @@ class TPTP : public Type { public: - USE_ALLOCATOR(ProductType); ProductType(Type* lhs,Type* rhs) : Type(TT_PRODUCT), _lhs(lhs), _rhs(rhs) {} @@ -429,7 +425,6 @@ class TPTP : public Type { public: - 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 cc4d44506c..690f54caac 100644 --- a/SAT/BufferedSolver.hpp +++ b/SAT/BufferedSolver.hpp @@ -35,8 +35,6 @@ using namespace Lib; class BufferedSolver : public SATSolver { public: - USE_ALLOCATOR(BufferedSolver); - BufferedSolver(SATSolver* inner); virtual SATClause* getRefutation() override { return _inner->getRefutation(); } diff --git a/SAT/FallbackSolverWrapper.hpp b/SAT/FallbackSolverWrapper.hpp index f169064fed..dc697faf99 100644 --- a/SAT/FallbackSolverWrapper.hpp +++ b/SAT/FallbackSolverWrapper.hpp @@ -37,8 +37,6 @@ using namespace Lib; class FallbackSolverWrapper : public SATSolver { public: - USE_ALLOCATOR(FallbackSolverWrapper); - FallbackSolverWrapper(SATSolver* inner,SATSolver* fallback); virtual SATClause* getRefutation() override { diff --git a/SAT/MinimizingSolver.hpp b/SAT/MinimizingSolver.hpp index dc9dae40b4..47e903b2c9 100644 --- a/SAT/MinimizingSolver.hpp +++ b/SAT/MinimizingSolver.hpp @@ -36,8 +36,6 @@ using namespace Lib; class MinimizingSolver : public SATSolver { public: - USE_ALLOCATOR(MinimizingSolver); - MinimizingSolver(SATSolver* inner); virtual SATClause* getRefutation() override { return _inner->getRefutation(); } diff --git a/SAT/MinisatInterfacing.hpp b/SAT/MinisatInterfacing.hpp index 8af855be1b..cc6f6519f8 100644 --- a/SAT/MinisatInterfacing.hpp +++ b/SAT/MinisatInterfacing.hpp @@ -25,8 +25,6 @@ namespace SAT{ class MinisatInterfacing : public PrimitiveProofRecordingSATSolver { public: - USE_ALLOCATOR(MinisatInterfacing); - MinisatInterfacing(const Shell::Options& opts, bool generateProofs=false); /** diff --git a/SAT/MinisatInterfacingNewSimp.hpp b/SAT/MinisatInterfacingNewSimp.hpp index e04c2e81b0..24c97b4d85 100644 --- a/SAT/MinisatInterfacingNewSimp.hpp +++ b/SAT/MinisatInterfacingNewSimp.hpp @@ -30,8 +30,6 @@ namespace SAT{ class MinisatInterfacingNewSimp : public SATSolverWithAssumptions { public: - USE_ALLOCATOR(MinisatInterfacingNewSimp); - static const unsigned VAR_MAX; MinisatInterfacingNewSimp(const Shell::Options& opts, bool generateProofs=false); diff --git a/SAT/Z3Interfacing.hpp b/SAT/Z3Interfacing.hpp index dbde6b8628..2943154234 100644 --- a/SAT/Z3Interfacing.hpp +++ b/SAT/Z3Interfacing.hpp @@ -56,8 +56,6 @@ namespace SAT{ class Z3Interfacing : public PrimitiveProofRecordingSATSolver { public: - USE_ALLOCATOR(Z3Interfacing); - Z3Interfacing(const Shell::Options& opts, SAT2FO& s2f, bool unsatCoresForAssumptions, vstring const& exportSmtlib); Z3Interfacing(SAT2FO& s2f, bool showZ3, bool unsatCoresForAssumptions, vstring const& exportSmtlib); ~Z3Interfacing(); diff --git a/SAT/Z3MainLoop.hpp b/SAT/Z3MainLoop.hpp index c25658500e..00562c8b31 100644 --- a/SAT/Z3MainLoop.hpp +++ b/SAT/Z3MainLoop.hpp @@ -38,8 +38,6 @@ using namespace Lib; class Z3MainLoop : public MainLoop { public: - USE_ALLOCATOR(Z3MainLoop); - Z3MainLoop(Problem& prb, const Options& opt); ~Z3MainLoop(){}; diff --git a/Saturation/AWPassiveClauseContainer.hpp b/Saturation/AWPassiveClauseContainer.hpp index ecc2650598..d6b6a6738d 100644 --- a/Saturation/AWPassiveClauseContainer.hpp +++ b/Saturation/AWPassiveClauseContainer.hpp @@ -65,8 +65,6 @@ class AWPassiveClauseContainer : public PassiveClauseContainer { public: - USE_ALLOCATOR(AWPassiveClauseContainer); - AWPassiveClauseContainer(bool isOutermost, const Shell::Options& opt, vstring name); ~AWPassiveClauseContainer(); void add(Clause* cl) override; diff --git a/Saturation/ClauseContainer.hpp b/Saturation/ClauseContainer.hpp index 4848132040..cf9102c0de 100644 --- a/Saturation/ClauseContainer.hpp +++ b/Saturation/ClauseContainer.hpp @@ -38,8 +38,6 @@ using namespace Shell; class ClauseContainer { public: - USE_ALLOCATOR(ClauseContainer); - virtual ~ClauseContainer() {} ClauseEvent addedEvent; /** @@ -65,8 +63,6 @@ class RandomAccessClauseContainer : public ClauseContainer { public: - USE_ALLOCATOR(RandomAccessClauseContainer); - virtual void attach(SaturationAlgorithm* salg); virtual void detach(); @@ -86,8 +82,6 @@ class RandomAccessClauseContainer class PlainClauseContainer : public ClauseContainer { public: - USE_ALLOCATOR(PlainClauseContainer); - void add(Clause* c) override { addedEvent.fire(c); @@ -99,8 +93,6 @@ class UnprocessedClauseContainer : public ClauseContainer { public: - USE_ALLOCATOR(UnprocessedClauseContainer); - virtual ~UnprocessedClauseContainer(); UnprocessedClauseContainer() : _data(64) {} void add(Clause* c) override; @@ -117,8 +109,6 @@ class PassiveClauseContainer : public RandomAccessClauseContainer { public: - USE_ALLOCATOR(PassiveClauseContainer); - PassiveClauseContainer(bool isOutermost, const Shell::Options& opt, vstring name = "") : _isOutermost(isOutermost), _opt(opt), _name(name) {} virtual ~PassiveClauseContainer(){}; @@ -177,8 +167,6 @@ class ActiveClauseContainer : public RandomAccessClauseContainer { public: - USE_ALLOCATOR(ActiveClauseContainer); - ActiveClauseContainer(const Shell::Options& opt) {} void add(Clause* c) override; diff --git a/Saturation/ConsequenceFinder.hpp b/Saturation/ConsequenceFinder.hpp index 97e6e3e763..8467f612b4 100644 --- a/Saturation/ConsequenceFinder.hpp +++ b/Saturation/ConsequenceFinder.hpp @@ -39,8 +39,6 @@ using namespace Inferences; */ class ConsequenceFinder { public: - USE_ALLOCATOR(ConsequenceFinder); - ~ConsequenceFinder(); void init(SaturationAlgorithm* sa); diff --git a/Saturation/Discount.hpp b/Saturation/Discount.hpp index b8fa109de7..86e0fb64a6 100644 --- a/Saturation/Discount.hpp +++ b/Saturation/Discount.hpp @@ -28,8 +28,6 @@ class Discount : public SaturationAlgorithm { public: - USE_ALLOCATOR(Discount); - Discount(Problem& prb, const Options& opt) : SaturationAlgorithm(prb, opt) {} diff --git a/Saturation/ExtensionalityClauseContainer.hpp b/Saturation/ExtensionalityClauseContainer.hpp index 42783d3640..49a873460d 100644 --- a/Saturation/ExtensionalityClauseContainer.hpp +++ b/Saturation/ExtensionalityClauseContainer.hpp @@ -49,8 +49,6 @@ typedef DHMap ClausesBySort; class ExtensionalityClauseContainer { public: - USE_ALLOCATOR(ExtensionalityClauseContainer); - ExtensionalityClauseContainer(const Options& opt) : _size(0), _maxLen(opt.extensionalityMaxLength()), diff --git a/Saturation/LRS.hpp b/Saturation/LRS.hpp index e276e61f4e..2431c92402 100644 --- a/Saturation/LRS.hpp +++ b/Saturation/LRS.hpp @@ -30,8 +30,6 @@ class LRS : public Otter { public: - USE_ALLOCATOR(LRS); - LRS(Problem& prb, const Options& opt) : Otter(prb, opt), _limitsEverActive(false) {} diff --git a/Saturation/LabelFinder.hpp b/Saturation/LabelFinder.hpp index 8316c514ab..86950ec19b 100644 --- a/Saturation/LabelFinder.hpp +++ b/Saturation/LabelFinder.hpp @@ -32,8 +32,6 @@ using namespace Inferences; class LabelFinder { public: - USE_ALLOCATOR(LabelFinder); - ~LabelFinder(); void onNewPropositionalClause(Clause* cl); diff --git a/Saturation/ManCSPassiveClauseContainer.cpp b/Saturation/ManCSPassiveClauseContainer.cpp index ebf1ccd343..b680203aab 100644 --- a/Saturation/ManCSPassiveClauseContainer.cpp +++ b/Saturation/ManCSPassiveClauseContainer.cpp @@ -21,23 +21,6 @@ namespace Saturation using namespace Lib; using namespace Kernel; -/* - * this class wraps the iterator of std::vector into IteratorCore required by Vampire. - */ -class VectorIteratorWrapper : public IteratorCore -{ -public: - USE_ALLOCATOR(VectorIteratorWrapper); - - explicit VectorIteratorWrapper(const std::vector& v) : curr(v.begin()), end(v.end()) {} - bool hasNext() { return curr != end; }; - Clause* next() { auto cl = *curr; curr = std::next(curr); return cl;}; - -private: - std::vector::const_iterator curr; - const std::vector::const_iterator end; -}; - void ManCSPassiveClauseContainer::add(Clause* cl) { clauses.push_back(cl); diff --git a/Saturation/ManCSPassiveClauseContainer.hpp b/Saturation/ManCSPassiveClauseContainer.hpp index 2dc3bb2627..80c8d78bcc 100644 --- a/Saturation/ManCSPassiveClauseContainer.hpp +++ b/Saturation/ManCSPassiveClauseContainer.hpp @@ -31,8 +31,6 @@ using namespace Kernel; class ManCSPassiveClauseContainer : public PassiveClauseContainer { public: - USE_ALLOCATOR(ManCSPassiveClauseContainer); - ManCSPassiveClauseContainer(bool isOutermost, const Shell::Options& opt) : PassiveClauseContainer(isOutermost, opt) {} virtual ~ManCSPassiveClauseContainer(){} diff --git a/Saturation/Otter.hpp b/Saturation/Otter.hpp index 0cac0607e9..148a2256f8 100644 --- a/Saturation/Otter.hpp +++ b/Saturation/Otter.hpp @@ -28,8 +28,6 @@ class Otter : public SaturationAlgorithm { public: - USE_ALLOCATOR(Otter); - Otter(Problem& prb, const Options& opt); ClauseContainer* getSimplifyingClauseContainer() override; diff --git a/Saturation/PredicateSplitPassiveClauseContainer.hpp b/Saturation/PredicateSplitPassiveClauseContainer.hpp index 9d479d17ae..5d761d1641 100644 --- a/Saturation/PredicateSplitPassiveClauseContainer.hpp +++ b/Saturation/PredicateSplitPassiveClauseContainer.hpp @@ -23,8 +23,6 @@ class PredicateSplitPassiveClauseContainer : public PassiveClauseContainer { public: - USE_ALLOCATOR(PredicateSplitPassiveClauseContainer); - PredicateSplitPassiveClauseContainer(bool isOutermost, const Shell::Options& opt, vstring name, Lib::vvector> queues, Lib::vvector cutoffs, Lib::vvector ratios, bool layeredArrangement); virtual ~PredicateSplitPassiveClauseContainer(); diff --git a/Saturation/SaturationAlgorithm.hpp b/Saturation/SaturationAlgorithm.hpp index 43bf36007e..85541dd64f 100644 --- a/Saturation/SaturationAlgorithm.hpp +++ b/Saturation/SaturationAlgorithm.hpp @@ -57,8 +57,6 @@ class Splitter; class SaturationAlgorithm : public MainLoop { public: - USE_ALLOCATOR(SaturationAlgorithm); - static SaturationAlgorithm* createFromOptions(Problem& prb, const Options& opt, IndexManager* indexMgr=0); SaturationAlgorithm(Problem& prb, const Options& opt); diff --git a/Saturation/Splitter.hpp b/Saturation/Splitter.hpp index 013ecff082..1361c1c0d9 100644 --- a/Saturation/Splitter.hpp +++ b/Saturation/Splitter.hpp @@ -172,8 +172,6 @@ class Splitter { }; public: - USE_ALLOCATOR(Splitter); - Splitter(); ~Splitter(); diff --git a/Saturation/SymElOutput.hpp b/Saturation/SymElOutput.hpp index fe197d5def..26fee03020 100644 --- a/Saturation/SymElOutput.hpp +++ b/Saturation/SymElOutput.hpp @@ -33,8 +33,6 @@ using namespace Shell; */ class SymElOutput { public: - USE_ALLOCATOR(SymElOutput); - SymElOutput(); void init(SaturationAlgorithm* sa); diff --git a/Shell/EqualityProxy.hpp b/Shell/EqualityProxy.hpp index ad3dbdd62c..1af04dd1c1 100644 --- a/Shell/EqualityProxy.hpp +++ b/Shell/EqualityProxy.hpp @@ -56,8 +56,6 @@ using namespace Kernel; class EqualityProxy { public: - USE_ALLOCATOR(EqualityProxy); - EqualityProxy(Options::EqualityProxy opt); void apply(Problem& prb); diff --git a/Shell/EqualityProxyMono.hpp b/Shell/EqualityProxyMono.hpp index 10311819a8..16b65f47f6 100644 --- a/Shell/EqualityProxyMono.hpp +++ b/Shell/EqualityProxyMono.hpp @@ -55,8 +55,6 @@ using namespace Kernel; class EqualityProxyMono { public: - USE_ALLOCATOR(EqualityProxyMono); - EqualityProxyMono(Options::EqualityProxy opt); void apply(Problem& prb); diff --git a/Shell/FunctionDefinition.cpp b/Shell/FunctionDefinition.cpp index 80bb76ebec..078934a516 100644 --- a/Shell/FunctionDefinition.cpp +++ b/Shell/FunctionDefinition.cpp @@ -117,8 +117,6 @@ struct FunctionDefinition::Def DEALLOC_KNOWN(argOccurs, lhs->arity()*sizeof(bool), "FunctionDefinition::Def::argOccurs"); } } - - USE_ALLOCATOR(Def); }; // class FunctionDefintion::Def diff --git a/Shell/GoalGuessing.hpp b/Shell/GoalGuessing.hpp index 7c27d37f0d..e605b97e41 100644 --- a/Shell/GoalGuessing.hpp +++ b/Shell/GoalGuessing.hpp @@ -25,8 +25,6 @@ using namespace Kernel; class GoalGuessing { public: - USE_ALLOCATOR(GoalGuessing); - void apply(Problem& prb); private: bool apply(UnitList*& units); diff --git a/Shell/InterpretedNormalizer.cpp b/Shell/InterpretedNormalizer.cpp index b73660c44f..b42fb03780 100644 --- a/Shell/InterpretedNormalizer.cpp +++ b/Shell/InterpretedNormalizer.cpp @@ -50,8 +50,6 @@ class InterpretedNormalizer::FunctionTranslator class InterpretedNormalizer::RoundingFunctionTranslator : public FunctionTranslator { public: - USE_ALLOCATOR(InterpretedNormalizer::RoundingFunctionTranslator); - RoundingFunctionTranslator(Interpretation origf, Interpretation newf, Interpretation roundf) { _origFun = env.signature->getInterpretingSymbol(origf); @@ -87,8 +85,6 @@ class InterpretedNormalizer::RoundingFunctionTranslator : public FunctionTransla class InterpretedNormalizer::SuccessorTranslator : public FunctionTranslator { public: - USE_ALLOCATOR(InterpretedNormalizer::SuccessorTranslator); - SuccessorTranslator() { _succFun = env.signature->getInterpretingSymbol(Theory::INT_SUCCESSOR); @@ -120,8 +116,6 @@ class InterpretedNormalizer::SuccessorTranslator : public FunctionTranslator class InterpretedNormalizer::BinaryMinusTranslator : public FunctionTranslator { public: - USE_ALLOCATOR(InterpretedNormalizer::BinaryMinusTranslator); - BinaryMinusTranslator(Interpretation bMinus, Interpretation plus, Interpretation uMinus) { _bMinusFun = env.signature->getInterpretingSymbol(bMinus); @@ -155,8 +149,6 @@ class InterpretedNormalizer::BinaryMinusTranslator : public FunctionTranslator class InterpretedNormalizer::IneqTranslator { public: - USE_ALLOCATOR(InterpretedNormalizer::IneqTranslator); - IneqTranslator(Interpretation src, Interpretation tgt, bool swapArguments, bool reversePolarity) : _swapArguments(swapArguments), _reversePolarity(reversePolarity) { @@ -194,8 +186,6 @@ class InterpretedNormalizer::IneqTranslator class InterpretedNormalizer::NLiteralTransformer : public TermTransformer { public: - USE_ALLOCATOR(InterpretedNormalizer::NLiteralTransformer); - NLiteralTransformer() : _ineqTransls(env.signature->predicates()), _fnTransfs(env.signature->functions()) diff --git a/Shell/Options.hpp b/Shell/Options.hpp index caaa559d18..ad2eb6f14c 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -179,8 +179,6 @@ class Options void setInputFile(const vstring& newVal){ _inputFile.set(newVal); } vstring includeFileName (const vstring& relativeName); - USE_ALLOCATOR(Options); - // standard ways of creating options void set(const vstring& name, const vstring& value); // implicitly the long version used here void set(const char* name, const char* value, bool longOpt); @@ -842,9 +840,6 @@ class Options * @author Giles */ struct AbstractOptionValue { - - USE_ALLOCATOR(AbstractOptionValue); - AbstractOptionValue(){} AbstractOptionValue(vstring l,vstring s) : longName(l), shortName(s), experimental(false), is_set(false),_should_copy(true), _tag(OptionTag::LAST_TAG), supress_problemconstraints(false) {} @@ -974,9 +969,6 @@ class Options */ template struct OptionValue : public AbstractOptionValue { - - USE_ALLOCATOR(OptionValue); - // We need to include an empty constructor as all the OptionValue objects need to be initialized // with something when the Options object is created. They should then all be reconstructed // This is annoying but preferable to the alternative in my opinion @@ -1074,9 +1066,6 @@ class Options */ template struct ChoiceOptionValue : public OptionValue { - - USE_ALLOCATOR(ChoiceOptionValue); - ChoiceOptionValue(){} ChoiceOptionValue(vstring l, vstring s,T def,OptionChoiceValues c) : OptionValue(l,s,def), choices(c) {} @@ -1206,9 +1195,6 @@ vstring getStringOfValue(float value) const{ return Lib::Int::toString(value); } * @author Giles */ struct RatioOptionValue : public OptionValue { - -USE_ALLOCATOR(RatioOptionValue); - RatioOptionValue(){} RatioOptionValue(vstring l, vstring s, int def, int other, char sp=':') : OptionValue(l,s,def), sep(sp), defaultOtherValue(other), otherValue(other) {}; @@ -1251,9 +1237,6 @@ virtual vstring getStringOfActual() const override { * @author Giles */ struct NonGoalWeightOptionValue : public OptionValue{ - -USE_ALLOCATOR(NonGoalWeightOptionValue); - NonGoalWeightOptionValue(){} NonGoalWeightOptionValue(vstring l, vstring s, float def) : OptionValue(l,s,def), numerator(1), denominator(1) {}; @@ -1392,7 +1375,6 @@ virtual vstring getStringOfValue(int value) const{ return Lib::Int::toString(val template struct OptionValueConstraint{ -USE_ALLOCATOR(OptionValueConstraint); OptionValueConstraint() : _hard(false) {} virtual ~OptionValueConstraint() {} // virtual methods present -> there should be virtual destructor @@ -1418,8 +1400,6 @@ bool _hard; template struct WrappedConstraint : AbstractWrappedConstraint { - USE_ALLOCATOR(WrappedConstraint); - WrappedConstraint(const OptionValue& v, OptionValueConstraintUP c) : value(v), con(std::move(c)) {} bool check() override { @@ -1434,7 +1414,6 @@ bool _hard; }; struct WrappedConstraintOrWrapper : public AbstractWrappedConstraint { - USE_ALLOCATOR(WrappedConstraintOrWrapper); WrappedConstraintOrWrapper(AbstractWrappedConstraintUP l, AbstractWrappedConstraintUP r) : left(std::move(l)),right(std::move(r)) {} bool check() override { return left->check() || right->check(); @@ -1446,7 +1425,6 @@ bool _hard; }; struct WrappedConstraintAndWrapper : public AbstractWrappedConstraint { - USE_ALLOCATOR(WrappedConstraintAndWrapper); WrappedConstraintAndWrapper(AbstractWrappedConstraintUP l, AbstractWrappedConstraintUP r) : left(std::move(l)),right(std::move(r)) {} bool check() override { return left->check() && right->check(); @@ -1459,7 +1437,6 @@ bool _hard; template struct OptionValueConstraintOrWrapper : public OptionValueConstraint{ - USE_ALLOCATOR(OptionValueConstraintOrWrapper); OptionValueConstraintOrWrapper(OptionValueConstraintUP l, OptionValueConstraintUP r) : left(std::move(l)),right(std::move(r)) {} bool check(const OptionValue& value){ return left->check(value) || right->check(value); @@ -1472,7 +1449,6 @@ bool _hard; template struct OptionValueConstraintAndWrapper : public OptionValueConstraint{ - USE_ALLOCATOR(OptionValueConstraintAndWrapper); OptionValueConstraintAndWrapper(OptionValueConstraintUP l, OptionValueConstraintUP r) : left(std::move(l)),right(std::move(r)) {} bool check(const OptionValue& value){ return left->check(value) && right->check(value); @@ -1485,8 +1461,6 @@ bool _hard; template struct UnWrappedConstraint : public OptionValueConstraint{ - USE_ALLOCATOR(UnWrappedConstraint); - UnWrappedConstraint(AbstractWrappedConstraintUP c) : con(std::move(c)) {} bool check(const OptionValue&){ return con->check(); } @@ -1549,7 +1523,6 @@ bool _hard; template struct Equal : public OptionValueConstraint{ - USE_ALLOCATOR(Equal); Equal(T gv) : _goodvalue(gv) {} bool check(const OptionValue& value){ return value.actualValue == _goodvalue; @@ -1566,7 +1539,6 @@ bool _hard; template struct NotEqual : public OptionValueConstraint{ - USE_ALLOCATOR(NotEqual); NotEqual(T bv) : _badvalue(bv) {} bool check(const OptionValue& value){ return value.actualValue != _badvalue; @@ -1583,7 +1555,6 @@ bool _hard; // optionally we can allow it be equal to that value also template struct LessThan : public OptionValueConstraint{ - USE_ALLOCATOR(LessThan); LessThan(T gv,bool eq=false) : _goodvalue(gv), _orequal(eq) {} bool check(const OptionValue& value){ return (value.actualValue < _goodvalue || (_orequal && value.actualValue==_goodvalue)); @@ -1609,7 +1580,6 @@ bool _hard; // optionally we can allow it be equal to that value also template struct GreaterThan : public OptionValueConstraint{ - USE_ALLOCATOR(GreaterThan); GreaterThan(T gv,bool eq=false) : _goodvalue(gv), _orequal(eq) {} bool check(const OptionValue& value){ return (value.actualValue > _goodvalue || (_orequal && value.actualValue==_goodvalue)); @@ -1636,7 +1606,6 @@ bool _hard; // optionally we can allow it be equal to that value also template struct SmallerThan : public OptionValueConstraint{ - USE_ALLOCATOR(SmallerThan); SmallerThan(T gv,bool eq=false) : _goodvalue(gv), _orequal(eq) {} bool check(const OptionValue& value){ return (value.actualValue < _goodvalue || (_orequal && value.actualValue==_goodvalue)); @@ -1668,8 +1637,6 @@ bool _hard; template struct IfThenConstraint : public OptionValueConstraint{ - USE_ALLOCATOR(IfThenConstraint); - IfThenConstraint(OptionValueConstraintUP ic, OptionValueConstraintUP c) : if_con(std::move(ic)), then_con(std::move(c)) {} @@ -1688,7 +1655,6 @@ bool _hard; template struct IfConstraint { - USE_ALLOCATOR(IfConstraint); IfConstraint(OptionValueConstraintUP c) :if_con(std::move(c)) {} OptionValueConstraintUP then(OptionValueConstraintUP c){ @@ -1763,7 +1729,6 @@ bool _hard; } struct isLookAheadSelectionConstraint : public OptionValueConstraint{ - USE_ALLOCATOR(isLookAheadSelectionConstraint); isLookAheadSelectionConstraint() {} bool check(const OptionValue& value){ return value.actualValue == 11 || value.actualValue == 1011 || value.actualValue == -11 || value.actualValue == -1011; @@ -1785,16 +1750,12 @@ bool _hard; */ struct OptionProblemConstraint{ - USE_ALLOCATOR(OptionProblemConstraint); - virtual bool check(Property* p) = 0; virtual vstring msg() = 0; virtual ~OptionProblemConstraint() {}; }; struct CategoryCondition : OptionProblemConstraint{ - USE_ALLOCATOR(CategoryCondition); - CategoryCondition(Property::Category c,bool h) : cat(c), has(h) {} bool check(Property*p){ ASS(p); @@ -1810,8 +1771,6 @@ bool _hard; }; struct UsesEquality : OptionProblemConstraint{ - USE_ALLOCATOR(UsesEquality); - bool check(Property*p){ ASS(p) return (p->equalityAtoms() != 0) || @@ -1822,8 +1781,6 @@ bool _hard; }; struct HasHigherOrder : OptionProblemConstraint{ - USE_ALLOCATOR(HasHigherOrder); - bool check(Property*p){ ASS(p) return (p->higherOrder()); @@ -1832,8 +1789,6 @@ bool _hard; }; struct OnlyFirstOrder : OptionProblemConstraint{ - USE_ALLOCATOR(OnlyFirstOrder); - bool check(Property*p){ ASS(p) return (!p->higherOrder()); @@ -1842,8 +1797,6 @@ bool _hard; }; struct MayHaveNonUnits : OptionProblemConstraint{ - USE_ALLOCATOR(MayHaveNonUnits); - bool check(Property*p){ return (p->formulas() > 0) // let's not try to guess what kind of clauses these will give rise to || (p->clauses() > p->unitClauses()); @@ -1852,8 +1805,6 @@ bool _hard; }; struct NotJustEquality : OptionProblemConstraint{ - USE_ALLOCATOR(NotJustEquality); - bool check(Property*p){ return (p->category()!=Property::PEQ || p->category()!=Property::UEQ); } @@ -1861,8 +1812,6 @@ bool _hard; }; struct AtomConstraint : OptionProblemConstraint{ - USE_ALLOCATOR(AtomConstraint); - AtomConstraint(int a,bool g) : atoms(a),greater(g) {} int atoms; bool greater; @@ -1878,8 +1827,6 @@ bool _hard; }; struct HasTheories : OptionProblemConstraint { - USE_ALLOCATOR(HasTheories); - static bool actualCheck(Property*p); bool check(Property*p); @@ -1887,8 +1834,6 @@ bool _hard; }; struct HasFormulas : OptionProblemConstraint { - USE_ALLOCATOR(HasFormulas); - bool check(Property*p) { return p->hasFormulas(); } @@ -1896,8 +1841,6 @@ bool _hard; }; struct HasGoal : OptionProblemConstraint { - USE_ALLOCATOR(HasGoal); - bool check(Property*p){ return p->hasGoal(); } @@ -1933,8 +1876,6 @@ bool _hard; // set of options will not be randomized and some will be randomized first struct OptionHasValue : OptionProblemConstraint{ - USE_ALLOCATOR(OptionHasValue); - OptionHasValue(vstring ov,vstring v) : option_value(ov),value(v) {} bool check(Property*p); vstring msg(){ return option_value+" has value "+value; } @@ -1943,8 +1884,6 @@ bool _hard; }; struct ManyOptionProblemConstraints : OptionProblemConstraint { - USE_ALLOCATOR(ManyOptionProblemConstraints); - ManyOptionProblemConstraints(bool a) : is_and(a) {} bool check(Property*p){ diff --git a/Shell/Property.hpp b/Shell/Property.hpp index 67e063e073..bb717fa712 100644 --- a/Shell/Property.hpp +++ b/Shell/Property.hpp @@ -152,8 +152,6 @@ class Property static const uint64_t PR_HAS_CDT_CONSTRUCTORS = 2199023255552ul; // 2^41 public: - USE_ALLOCATOR(Property); - // constructor, operators new and delete explicit Property(); static Property* scan(UnitList*); diff --git a/Shell/Statistics.hpp b/Shell/Statistics.hpp index 8393587cc0..405bdd2b61 100644 --- a/Shell/Statistics.hpp +++ b/Shell/Statistics.hpp @@ -43,8 +43,6 @@ using namespace Kernel; class Statistics { public: - USE_ALLOCATOR(Statistics); - Statistics(); void print(std::ostream& out); diff --git a/Shell/SubexpressionIterator.hpp b/Shell/SubexpressionIterator.hpp index 60104306c6..432e4e6953 100644 --- a/Shell/SubexpressionIterator.hpp +++ b/Shell/SubexpressionIterator.hpp @@ -28,7 +28,6 @@ namespace Shell { class SubexpressionIterator { public: - USE_ALLOCATOR(SubexpressionIterator); /** * SubexpressionIterator::Expression represents an expression, which is * either a term or a formula. Terms are stored as objects of TermList, diff --git a/Shell/TermAlgebra.hpp b/Shell/TermAlgebra.hpp index e508ea3673..b9f112a9a5 100644 --- a/Shell/TermAlgebra.hpp +++ b/Shell/TermAlgebra.hpp @@ -25,8 +25,6 @@ using Kernel::TermList; namespace Shell { class TermAlgebraConstructor { public: - USE_ALLOCATOR(TermAlgebraConstructor); - /* A term algebra constructor, described by its name, range, arity, and for each argument: the name of its destructor and its sort*/ @@ -87,9 +85,6 @@ namespace Shell { class TermAlgebra { public: - USE_ALLOCATOR(TermAlgebra); - - /* An algebra described by its name, sort, number of constructors, the constructors themselves (whose range must be the algebra sort), and their cyclicity. If allowsCyclicTerms is false, and