diff --git a/Api/Helper_Internal.hpp b/Api/Helper_Internal.hpp index 5c7123ba97..180820b294 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 5ec703a766..ea41bc5ba0 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 6e6a396829..7e3f27699f 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/CASC/PortfolioMode.cpp b/CASC/PortfolioMode.cpp index 63075f9150..003093fb73 100644 --- a/CASC/PortfolioMode.cpp +++ b/CASC/PortfolioMode.cpp @@ -501,9 +501,6 @@ bool PortfolioMode::runScheduleAndRecoverProof(Schedule schedule) * the user didn't wish a proof in the file, so we printed it to the secret tmp file * now it's time to restore it. */ - - BYPASSING_ALLOCATOR; - ifstream input(_tmpFileNameForProof); bool openSucceeded = !input.fail(); @@ -692,8 +689,6 @@ void PortfolioMode::runSlice(Options& strategyOpt) fname = _tmpFileNameForProof; } - BYPASSING_ALLOCATOR; - ofstream output(fname.c_str()); if (output.fail()) { // fallback to old printing method @@ -723,7 +718,5 @@ void PortfolioMode::runSlice(Options& strategyOpt) _syncSemaphore.inc(SEM_LOCK); // would be also released after the processes' death, but we are polite and do it already here } - STOP_CHECKING_FOR_ALLOCATOR_BYPASSES; - exit(resultValue); } // runSlice diff --git a/CASC/Schedules.cpp b/CASC/Schedules.cpp index 46a040aadc..d4ef50b2ef 100644 --- a/CASC/Schedules.cpp +++ b/CASC/Schedules.cpp @@ -30,7 +30,6 @@ void Schedules::getScheduleFromFile(const vstring& filename, Schedule& quick) if (filename == "") { USER_ERROR("Schedule file was not set."); } - BYPASSING_ALLOCATOR; ifstream schedule_file (filename.c_str()); if (schedule_file.fail()) { USER_ERROR("Cannot open schedule file: " + filename); diff --git a/DP/ShortConflictMetaDP.hpp b/DP/ShortConflictMetaDP.hpp index caff1ae6e2..cd89769047 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 b0e4ee4533..13f9b7886c 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 35689e05e5..0f87e9ff9d 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.cpp b/Debug/TimeProfiling.cpp index d2da719c0a..a47ddd78c1 100644 --- a/Debug/TimeProfiling.cpp +++ b/Debug/TimeProfiling.cpp @@ -192,7 +192,6 @@ void TimeTrace::Node::printPrettyRec(std::ostream& out, NodeFormatOpts& opts) if (opts.parentDuration.isSome()) { out << "[" << setw(2) << percent(total, opts.parentDuration.unwrap()) << "%] "; } - BYPASSING_ALLOCATOR if (opts.nameWidth.isSome()) { out << msetw(opts.nameWidth.unwrap()) << left; } diff --git a/Debug/TimeProfiling.hpp b/Debug/TimeProfiling.hpp index b67c4e61c5..800886e314 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 6788bf7931..dad5d85dc1 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.cpp b/FMB/FiniteModelBuilder.cpp index b02aef3d77..ea2393e4b9 100644 --- a/FMB/FiniteModelBuilder.cpp +++ b/FMB/FiniteModelBuilder.cpp @@ -132,11 +132,7 @@ FiniteModelBuilder::FiniteModelBuilder(Problem& prb, const Options& opt) break; #if VZ3 case Options::FMBEnumerationStrategy::SMT: - { - BYPASSING_ALLOCATOR; - - _dsaEnumerator = new SmtBasedDSAE(); - } + _dsaEnumerator = new SmtBasedDSAE(); _xmass = false; break; #endif @@ -153,8 +149,6 @@ FiniteModelBuilder::FiniteModelBuilder(Problem& prb, const Options& opt) FiniteModelBuilder::~FiniteModelBuilder() { if(_dsaEnumerator){ - BYPASSING_ALLOCATOR; - delete _dsaEnumerator; } } @@ -2484,8 +2478,6 @@ bool FiniteModelBuilder::SmtBasedDSAE::init(unsigned _startModelSize, DArray 1); - BYPASSING_ALLOCATOR; - try { // initialize the smt solver z3::expr zero = _context.int_val(_startModelSize-1); @@ -2533,8 +2525,6 @@ bool FiniteModelBuilder::SmtBasedDSAE::init(unsigned _startModelSize, DArray& newSortSizes, DArray& sortMaxes) { - BYPASSING_ALLOCATOR; - try { TIME_TRACE("smt search for next domain size assignment"); diff --git a/FMB/FiniteModelBuilder.hpp b/FMB/FiniteModelBuilder.hpp index c0b435b846..90000e7ab6 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 4339eb857d..ccae8e86e1 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 93eed5e733..7cc8bdb228 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 02ada6d1bd..4e70f4b13b 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 8b1b330e99..31b9bbae20 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 3d24a19ef8..8e5bffe3b1 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 5faf86c63a..cf26039069 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 3872ff84e7..9d591a98f3 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 18868c0ab5..6bc2e865e4 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 4c3b26c0a9..a5afc7770a 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 8b62d0b8f9..7acb9f071c 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 08c352d8c7..1b55e8d692 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 d991dbabec..572038dc3c 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 2036eb5e37..df00bfd3f1 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 34cdbc37da..122afeef59 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 ecdb691629..95a8b1e85f 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 2c8382b4bb..c02b7ed628 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 7ffd10dc43..874776fa3c 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 f355ba9cb3..eff45ff873 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 f7d87ce789..ac9ecb796f 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 fe1ff63bcb..93f785a452 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 e3a4a4d38e..ad5a7321ab 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 30fd7488ef..7df665db6d 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 3b6ef9d9b3..8d2547c44c 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 ab478a8f74..5300aaf469 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 79790f61d2..181d7fb51f 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 c578b07da3..2cf2079f6e 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 089072636f..9d92658a50 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 256a49ba21..407ffdea16 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 4d63a622dc..62a956f4d6 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 b83350dab6..fd09b55118 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 0d79e359a2..b1e0ab93f6 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 d5be8b663b..281f1e37e5 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 af6c9583fb..ccd12bace5 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 36cd9a685a..2ec2490d3a 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 367bd07b3f..1b93458e6e 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 c6ef4ffa4a..a2b22e8939 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 f6e62a4ca7..5cf454366e 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 d7f4eef6bd..f3336ab3da 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 c5fbbb4902..8de831cb85 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 70bbfb32e7..a60cc42896 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 a238394287..91de177a8c 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 c10b4b998e..483d01a113 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 292dd25b2e..4f639404af 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 290c93cc92..baca76dd7f 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 58ab249507..5848a54567 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 e5cbb59ba1..c0b799c31f 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 24f49d48a1..410eb94f65 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 4a1a91bc64..d2e2ec302a 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 b1dff743f5..a9caf2bfcd 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 8daad523e3..4d03d09211 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 a1060fb8d9..c2b5166a6a 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 8f973a4b4e..dd64c65a61 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 429cdddb3a..98610c0758 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 0f4ff8c675..918480dce1 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 071a29685d..bed1280c99 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 57ec4825ca..2816c143ba 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 bab0e28b4e..d92e5c9718 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 7ef26eaaf6..59f6be6970 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 5823905a85..2a2b4d5c01 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 e811291028..d0ba11a9f1 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 bdfc95af0b..c10620e15b 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 fc0ab61284..82cd8df91a 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 a7bdf17e0c..00e648aecf 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 03abcf2813..8556811a1a 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 855a263a9b..fafe61f15d 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 97ffc15bb0..a594c50b29 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 aba1fb722f..e68cfe88a2 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 1b58e1ace1..c7e9e139ee 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 0f30f2a988..409232e53d 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 ec0500ae6f..91772e8427 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 58b1f87666..078ff01ee9 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 72db102eb1..b6ac82d000 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 aec25d1cbd..58fc987e44 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 9df383fbc0..4e105b901e 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 b4001af13a..962736f2bd 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 d3bd29ea53..01cd9841cc 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 e9f251633a..4fde6f70dd 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 ae0e9c9e7c..7a0e644948 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 79a61ff44a..46678f78c9 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 6ca205cfe1..2b7c8e6b3e 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 aeba6e1b2a..ab00ca5e5f 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.cpp b/Inferences/TheoryInstAndSimp.cpp index 19a133a695..d312a42767 100644 --- a/Inferences/TheoryInstAndSimp.cpp +++ b/Inferences/TheoryInstAndSimp.cpp @@ -93,10 +93,7 @@ TheoryInstAndSimp::TheoryInstAndSimp(Options::TheoryInstSimp mode, bool thiTauto , _mode(manageDeprecations(mode)) , _thiTautologyDeletion(thiTautologyDeletion) , _naming() - , _solver([&](){ - BYPASSING_ALLOCATOR; - return new Z3Interfacing(_naming, showZ3, /* unsatCoresForAssumptions = */ generalisation, exportSmtlib); - }()) + , _solver(new Z3Interfacing(_naming, showZ3, /* unsatCoresForAssumptions = */ generalisation, exportSmtlib)) , _generalisation(generalisation) , _instantiationConstants ("$inst") , _generalizationConstants("$inst$gen") @@ -604,8 +601,6 @@ Option TheoryInstAndSimp::instantiateWithModel(SkolemizedLiterals template TheoryInstAndSimp::SkolemizedLiterals TheoryInstAndSimp::skolemize(IterLits lits) { - - BYPASSING_ALLOCATOR; // Currently we just get the single solution from Z3 @@ -649,8 +644,6 @@ template TheoryInstAndSimp::SkolemizedLiterals TheoryInstAndSimp VirtualIterator TheoryInstAndSimp::getSolutions(Stack const& theoryLiterals, Stack const& guards, unsigned freshVar) { - BYPASSING_ALLOCATOR; - auto skolemized = skolemize(iterTraits(getConcatenatedIterator( theoryLiterals.iterFifo(), guards.iterFifo() @@ -983,7 +976,6 @@ std::ostream& operator<<(std::ostream& out, Solution const& self) TheoryInstAndSimp::~TheoryInstAndSimp() { - BYPASSING_ALLOCATOR delete _solver; } diff --git a/Inferences/TheoryInstAndSimp.hpp b/Inferences/TheoryInstAndSimp.hpp index 3b5e07483a..de3d14353c 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 86a22bbb9a..51eb742b9e 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 0e6fa1172a..52cd86f625 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 72f1cf981f..b98ab96955 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 55cae17479..2d150fcd33 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 cbeb48451f..2f70808060 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 5698bac39d..0d55762c1b 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 f6919c8453..62560fa55a 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 688f0d5016..233fa726e9 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 20b50c6370..a6c7bc510c 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 887c3ac1ce..256e5c5392 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 f56d871e50..1064506562 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 842dd0af71..856fcf685e 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 764f2ef0fd..7e5637963d 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 8439a63c4f..dcf5622583 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); @@ -395,7 +394,6 @@ template KboWeightMap KBO::weightsFromFile(const Options& opts) const { DArray weights(SigTraits::nSymbols()); - BYPASSING_ALLOCATOR ///////////////////////// parsing helper functions ///////////////////////// diff --git a/Kernel/KBO.hpp b/Kernel/KBO.hpp index b23a28a44c..61f7bf20a0 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 b85c7d5ecd..2089f1d5f2 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 4ce00de8ad..aa927f85e5 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 bab554cb17..7610d7fed3 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 a173ec1326..5f5f5c2efc 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 70e40d0db4..e0180abe89 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 008daffe22..7bb325908e 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 e54147fac5..65f789384a 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 65d5432c43..3729958094 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 a6aa61c07b..d1149d447d 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 3690738417..0dffedb3f6 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 82f36895f8..4435dacc1b 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.cpp b/Kernel/Ordering.cpp index d67f9f9898..f24553ea36 100644 --- a/Kernel/Ordering.cpp +++ b/Kernel/Ordering.cpp @@ -739,8 +739,6 @@ DArray PrecedenceOrdering::typeConPrecFromOpts(Problem& prb, const Options& aux.initFromIterator(getRangeIterator(0u, nTypeCons), nTypeCons); if (!opt.typeConPrecedence().empty()) { - BYPASSING_ALLOCATOR; - vstring precedence; ifstream precedence_file (opt.typeConPrecedence().c_str()); if (precedence_file.is_open() && getline(precedence_file, precedence)) { @@ -767,8 +765,6 @@ DArray PrecedenceOrdering::funcPrecFromOpts(Problem& prb, const Options& op aux.initFromIterator(getRangeIterator(0u, nFunctions), nFunctions); if (!opt.functionPrecedence().empty()) { - BYPASSING_ALLOCATOR; - vstring precedence; ifstream precedence_file (opt.functionPrecedence().c_str()); if (precedence_file.is_open() && getline(precedence_file, precedence)) { @@ -793,8 +789,6 @@ DArray PrecedenceOrdering::predPrecFromOpts(Problem& prb, const Options& op aux.initFromIterator(getRangeIterator(0u, nPredicates), nPredicates); if (!opt.predicatePrecedence().empty()) { - BYPASSING_ALLOCATOR; - vstring precedence; ifstream precedence_file (opt.predicatePrecedence().c_str()); if (precedence_file.is_open() && getline(precedence_file, precedence)) { diff --git a/Kernel/Ordering.hpp b/Kernel/Ordering.hpp index 0e9211eef8..ee2995a9d4 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 52c17d7a6d..9ddbc28773 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 4425b6dde0..6368906222 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 8f62ca8653..62c89deffa 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 36b2285d52..58975ad3af 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 4a7f4335e8..729d7435ad 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 26483cf7c0..adb72c19db 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 63f53eac6b..9bba413475 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 7b260c314f..aaa94d2f6e 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 894754e21f..d1d14c2750 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 f45faf56f0..95a1a6fdfa 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 2671fc77b5..c1aad4bae3 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 80f60ab137..229a3b09ad 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 775975e310..f60426357e 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 d0588905c6..f645168ec1 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 ad9af1b3fa..245cba167e 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.cpp b/Lib/Allocator.cpp index 6ef1a9ab5c..9b57b4345d 100644 --- a/Lib/Allocator.cpp +++ b/Lib/Allocator.cpp @@ -60,26 +60,3 @@ void operator delete(void *ptr) noexcept { Lib::TimeoutProtector tp; std::free(ptr); } - -void *Lib::deprecatedAlloc(size_t size) { - { - TimeoutProtector tp; - if(void *ptr = std::malloc(size)) - return ptr; - } - throw std::bad_alloc(); -} - -void *Lib::deprecatedRealloc(void *ptr, size_t new_size) { - { - TimeoutProtector tp; - if(void *new_ptr = std::realloc(ptr, new_size)) - return new_ptr; - } - throw std::bad_alloc(); -} - -void Lib::deprecatedFree(void *ptr) { - TimeoutProtector tp; - std::free(ptr); -} diff --git a/Lib/Allocator.hpp b/Lib/Allocator.hpp index 7edddb375b..a60b618c68 100644 --- a/Lib/Allocator.hpp +++ b/Lib/Allocator.hpp @@ -43,11 +43,6 @@ size_t getMemoryLimit(); // set the memory limit for global operator new void setMemoryLimit(size_t bytes); -// deprecated functions invoked by *ALLOC_UNKNOWN, should not be used in new code -void *deprecatedAlloc(size_t size); -void *deprecatedRealloc(void *ptr, size_t new_size); -void deprecatedFree(void *ptr); - } #ifdef INDIVIDUAL_ALLOCATIONS @@ -300,16 +295,9 @@ inline void free(void *pointer, size_t size) { #endif // INDIVIDUAL_ALLOCATIONS's else // legacy macros, should be removed eventually -#define BYPASSING_ALLOCATOR -#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) -#define REALLOC_UNKNOWN(ptr, size, className) Lib::deprecatedRealloc(ptr, size) -#define DEALLOC_UNKNOWN(ptr, className) Lib::deprecatedFree(ptr) // TODO dubious: probably a compiler lint these days? /** diff --git a/Lib/ArrayMap.hpp b/Lib/ArrayMap.hpp index 46859d7d4a..0d4eaf22e6 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 a341e4cdf4..5034f6ce81 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 598990f7bb..105b5b6ee6 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 0b02dac086..19bf6515ac 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 06fbe267a1..b677cb7f88 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 ac3fcf49dd..d8b4406ec1 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 1abfe6058b..6570b05f51 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/Environment.cpp b/Lib/Environment.cpp index 13355c0efa..ec6b5dd510 100644 --- a/Lib/Environment.cpp +++ b/Lib/Environment.cpp @@ -51,8 +51,6 @@ Environment::Environment() _pipe(0), _problem(0) { - START_CHECKING_FOR_ALLOCATOR_BYPASSES; - options = new Options; // statistics calls the timer @@ -94,10 +92,7 @@ Environment::~Environment() delete signature; delete statistics; if (predicateSineLevels) delete predicateSineLevels; - { - BYPASSING_ALLOCATOR; // use of std::function in options - delete options; - } + delete options; // #endif } diff --git a/Lib/Event.hpp b/Lib/Event.hpp index 9041c5b4f0..084d6557ac 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 d9a2898c6e..9a849321cc 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 400d629a58..46b4d44450 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 030d1173f6..ed8e01bcf3 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 3aa942352b..eac9b161c4 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 ad461e59f5..9f4cfec839 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 1aa7c01c4b..a3b7a34e74 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/Sys/SyncPipe.cpp b/Lib/Sys/SyncPipe.cpp index fe2a33993a..ef85b7d06e 100644 --- a/Lib/Sys/SyncPipe.cpp +++ b/Lib/Sys/SyncPipe.cpp @@ -49,13 +49,9 @@ SyncPipe::SyncPipe() _readDescriptor=fd[0]; _writeDescriptor=fd[1]; - { - BYPASSING_ALLOCATOR; - - _istream=new fdstream(_readDescriptor); - _ostream=new fdstream(_writeDescriptor); - } - + _istream=new fdstream(_readDescriptor); + _ostream=new fdstream(_writeDescriptor); + _istream->rdbuf()->pubsetbuf(0,0); //add the privileges into the semaphore @@ -137,12 +133,8 @@ void SyncPipe::neverRead() SYSTEM_FAIL("Closing read descriptor of a pipe.", errno); } ASS_EQ(res,0); - { - BYPASSING_ALLOCATOR; - - delete _istream; - _istream=0; - } + delete _istream; + _istream=0; } @@ -187,12 +179,8 @@ void SyncPipe::neverWrite() } ASS_EQ(res,0); - { - BYPASSING_ALLOCATOR; - - delete _ostream; - _ostream=0; - } + delete _ostream; + _ostream=0; } /** * Give up all the privileges of this object diff --git a/Lib/System.cpp b/Lib/System.cpp index 268696e715..1016ccdf9e 100644 --- a/Lib/System.cpp +++ b/Lib/System.cpp @@ -307,8 +307,6 @@ bool System::extractDirNameFromPath(vstring path, vstring& dir) bool System::fileExists(vstring fname) { - BYPASSING_ALLOCATOR; - ifstream ifile(fname.c_str()); return ifile.good(); } diff --git a/Lib/Timer.hpp b/Lib/Timer.hpp index 31383ee6a9..342f43500f 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 37234a7512..68f252104d 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 3aab658787..712b183587 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/Minisat/mtl/Vec.h b/Minisat/mtl/Vec.h index a6c1e5a238..a7fc7dedb5 100644 --- a/Minisat/mtl/Vec.h +++ b/Minisat/mtl/Vec.h @@ -33,7 +33,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Minisat/mtl/IntTypes.h" #include "Minisat/mtl/XAlloc.h" -#include "Lib/Allocator.hpp" +#include "Lib/Timer.hpp" namespace Minisat { @@ -106,9 +106,10 @@ void vec::capacity(Size min_cap) { if (cap >= min_cap) return; Size add = max((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2 const Size size_max = std::numeric_limits::max(); - if ( ((size_max <= std::numeric_limits::max()) && (add > size_max - cap)) - || (((data = (T*) REALLOC_UNKNOWN((void *)data, (cap += add) * sizeof(T),"Minisat::vec")) == NULL) && errno == ENOMEM) ) + if ( ((size_max <= std::numeric_limits::max()) && (add > size_max - cap))) throw OutOfMemoryException(); + + data = (T*) xrealloc((void *)data, (cap += add) * sizeof(T)); } @@ -133,7 +134,7 @@ void vec::clear(bool dealloc) { if (data != NULL){ for (Size i = 0; i < sz; i++) data[i].~T(); sz = 0; - if (dealloc) DEALLOC_UNKNOWN(data,"Minisat::vec"), data = NULL, cap = 0; } } + if (dealloc) xfree(data), data = NULL, cap = 0; } } //================================================================================================= } diff --git a/Minisat/mtl/XAlloc.h b/Minisat/mtl/XAlloc.h index cb64596f2e..6143f534dc 100644 --- a/Minisat/mtl/XAlloc.h +++ b/Minisat/mtl/XAlloc.h @@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include -#include "Lib/Allocator.hpp" +#include "Lib/Timer.hpp" namespace Minisat { @@ -39,7 +39,8 @@ namespace Minisat { class OutOfMemoryException{}; static inline void* xrealloc(void *ptr, size_t size) { - void* mem = REALLOC_UNKNOWN(ptr, size, "Minisat::xrealloc"); + Lib::TimeoutProtector tp; + void* mem = std::realloc(ptr, size); if (mem == NULL && errno == ENOMEM){ throw OutOfMemoryException(); }else @@ -48,7 +49,8 @@ static inline void* xrealloc(void *ptr, size_t size) static inline void xfree (void* ptr) { - DEALLOC_UNKNOWN(ptr,"Minisat::xrealloc"); + Lib::TimeoutProtector tp; + std::free(ptr); } //================================================================================================= diff --git a/Parse/TPTP.cpp b/Parse/TPTP.cpp index 26e4062aea..ab2bad076d 100644 --- a/Parse/TPTP.cpp +++ b/Parse/TPTP.cpp @@ -1220,10 +1220,7 @@ void TPTP::unitList() return; } resetChars(); - { - BYPASSING_ALLOCATOR; // ifstream was allocated by "system new" - delete _in; - } + delete _in; _in = _inputs.pop(); _includeDirectory = _includeDirectories.pop(); delete _allowedNames; @@ -2110,10 +2107,7 @@ void TPTP::include() // the TPTP standard, so far we just set it to "" _includeDirectory = ""; vstring fileName(env.options->includeFileName(relativeName)); - { - BYPASSING_ALLOCATOR; // we cannot make ifstream allocated via Allocator - _in = new ifstream(fileName.c_str()); - } + _in = new ifstream(fileName.c_str()); if (!*_in) { USER_ERROR((vstring)"cannot open file " + fileName); } diff --git a/Parse/TPTP.hpp b/Parse/TPTP.hpp index 7b308cef8f..5c1b336521 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 620da45f23..cc4d44506c 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 a7980fd211..f169064fed 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 fe732aedb8..dc9dae40b4 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 98ca9ab774..8af855be1b 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 ffa79ad4bb..e04c2e81b0 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 0dc0cb7734..4e9b59929d 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.cpp b/SAT/Z3Interfacing.cpp index f5d2518a86..1a6492e1d5 100644 --- a/SAT/Z3Interfacing.cpp +++ b/SAT/Z3Interfacing.cpp @@ -105,8 +105,6 @@ void handleZ3Error(Z3_context ctxt, Z3_error_code code) throw z3::exception(errToString(code)); } -#define STATEMENTS_TO_EXPRESSION(...) [&]() { __VA_ARGS__; return 0; }() - Z3Interfacing::Z3Interfacing(SAT2FO& s2f, bool showZ3, bool unsatCoresForAssumptions, vstring const& exportSmtlib): _hasSeenArrays(false), _varCnt(0), @@ -115,17 +113,12 @@ Z3Interfacing::Z3Interfacing(SAT2FO& s2f, bool showZ3, bool unsatCoresForAssumpt _config(), _context(_config), _solver(_context), - _model((STATEMENTS_TO_EXPRESSION( - BYPASSING_ALLOCATOR; - _solver.check(); - ), - _solver.get_model())), + _model((_solver.check(), _solver.get_model())), _assumptions(), _showZ3(showZ3), _unsatCore(unsatCoresForAssumptions), _out() { - BYPASSING_ALLOCATOR _out = exportSmtlib == "" ? Option() : Option(std::ofstream(exportSmtlib.c_str())) ; if (_out.isSome() && _out.unwrap().fail()) { @@ -176,7 +169,6 @@ unsigned Z3Interfacing::newVar() void Z3Interfacing::addClause(SATClause* cl) { - BYPASSING_ALLOCATOR; ASS(cl); // store to later generate the refutation @@ -251,7 +243,6 @@ Z3Interfacing::Representation Z3Interfacing::getRepresentation(SATClause* cl) SATSolver::Status Z3Interfacing::solve() { - BYPASSING_ALLOCATOR; DEBUG("assumptions: ", _assumptions); output("(check-sat-assuming ("); @@ -329,8 +320,6 @@ SATSolver::Status Z3Interfacing::solveUnderAssumptions(const SATLiteralStack& as SATSolver::VarAssignment Z3Interfacing::getAssignment(unsigned var) { - BYPASSING_ALLOCATOR; - ASS_EQ(_status,SATISFIABLE); bool named = isNamedExpr(var); z3::expr rep = named ? getNameExpr(var) : getRepresentation(SATLiteral(var,1)).expr; @@ -506,7 +495,6 @@ SATClause* Z3Interfacing::getZeroImpliedCertificate(unsigned) z3::sort Z3Interfacing::getz3sort(SortId s) { - BYPASSING_ALLOCATOR; auto srt = _sorts.tryGet(s); if (srt.isSome()) { return srt.unwrap(); @@ -1118,9 +1106,6 @@ Z3Interfacing::Representation Z3Interfacing::getRepresentation(Term* trm) Z3Interfacing::Representation Z3Interfacing::getRepresentation(SATLiteral slit) { - BYPASSING_ALLOCATOR; - - //First, does this represent a ground literal Literal* lit = _sat2fo.toFO(slit); if(lit && lit->ground()){ diff --git a/SAT/Z3Interfacing.hpp b/SAT/Z3Interfacing.hpp index b75c0af3da..dbde6b8628 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 ed4ef7d13a..c25658500e 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 8f18297959..ecc2650598 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 a172d14c28..4848132040 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 38684257c9..97e6e3e763 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 163e7fa7c9..b8fa109de7 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 3d303c2b6c..42783d3640 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 7da98b3628..e276e61f4e 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 46e92a0c57..8316c514ab 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 472e7543fb..ebf1ccd343 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 541dfd3f75..2dc3bb2627 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 0180ce0922..0cac0607e9 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 794fc00c53..9d479d17ae 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 4af640ae1e..43bf36007e 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.cpp b/Saturation/Splitter.cpp index 8bc2fd1736..de938ca5e8 100644 --- a/Saturation/Splitter.cpp +++ b/Saturation/Splitter.cpp @@ -72,14 +72,14 @@ void SplittingBranchSelector::init() break; #if VZ3 case Options::SatSolver::Z3: - { BYPASSING_ALLOCATOR + { _solverIsSMT = true; _solver = new Z3Interfacing(_parent.getOptions(),_parent.satNaming(), /* unsat core */ false, _parent.getOptions().exportAvatarProblem()); if(_parent.getOptions().satFallbackForSMT()){ // TODO make fallback minimizing? SATSolver* fallback = new MinisatInterfacing(_parent.getOptions(),true); _solver = new FallbackSolverWrapper(_solver.release(),fallback); - } + } } break; #endif diff --git a/Saturation/Splitter.hpp b/Saturation/Splitter.hpp index 452aef13fd..013ecff082 100644 --- a/Saturation/Splitter.hpp +++ b/Saturation/Splitter.hpp @@ -59,10 +59,7 @@ class SplittingBranchSelector { SplittingBranchSelector(Splitter& parent) : _ccModel(false), _parent(parent), _solverIsSMT(false) {} ~SplittingBranchSelector(){ #if VZ3 -{ -BYPASSING_ALLOCATOR; _solver=0; -} #endif } @@ -171,12 +168,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 c3a726bd5b..fe197d5def 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 bcd39fe536..d51a7e0ac0 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 ba5123fe73..ad3dbdd62c 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 c940f66704..10311819a8 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 d3a2bd64b6..80bb76ebec 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 b4e3ed52d9..7c27d37f0d 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/InterpolantMinimizer.cpp b/Shell/InterpolantMinimizer.cpp index 4bf93cea27..c6fea9245f 100644 --- a/Shell/InterpolantMinimizer.cpp +++ b/Shell/InterpolantMinimizer.cpp @@ -31,8 +31,6 @@ namespace Shell std::unordered_map InterpolantMinimizer::computeSplittingFunction(Kernel::Unit* refutation, UnitWeight weightFunction) { - BYPASSING_ALLOCATOR; - using namespace z3; context c; optimize solver(c); @@ -194,7 +192,6 @@ namespace Shell void InterpolantMinimizer::analyzeLocalProof(Kernel::Unit *refutation) { - BYPASSING_ALLOCATOR; // print statistics on grey area analyzeGreyAreas(refutation); diff --git a/Shell/Interpolants.cpp b/Shell/Interpolants.cpp index 07113d36d4..fd6c4b4347 100644 --- a/Shell/Interpolants.cpp +++ b/Shell/Interpolants.cpp @@ -71,7 +71,6 @@ namespace Shell void Interpolants::removeTheoryInferences(Unit* refutation) { - BYPASSING_ALLOCATOR; ProofIteratorPostOrder it(refutation); while (it.hasNext()) // traverse the proof in depth-first post order { @@ -141,7 +140,6 @@ namespace Shell */ Formula* Interpolants::getInterpolant(Unit *refutation, UnitWeight weightFunction) { - BYPASSING_ALLOCATOR; /* * compute coloring for the inferences, i.e. compute splitting function in the words of the thesis */ diff --git a/Shell/InterpretedNormalizer.cpp b/Shell/InterpretedNormalizer.cpp index 00b8c19ac1..b73660c44f 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 859c513df4..ccb3e1b39f 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/Naming.cpp b/Shell/Naming.cpp index a02156b2a6..d9740e9e63 100644 --- a/Shell/Naming.cpp +++ b/Shell/Naming.cpp @@ -145,12 +145,10 @@ Formula* Naming::apply_iter(Formula* top_f) { case AND: { FormulaList* fs = tas.f->args(); unsigned length = FormulaList::length(fs); - void* mem = ALLOC_UNKNOWN(length * sizeof(int), "Naming::apply"); - int* cls = array_new(mem, length); + int *cls = new int[length](); int* negCls = 0; if (tas.where == UNDER_IFF) { - mem = ALLOC_UNKNOWN(length * sizeof(int), "Naming::apply"); - negCls = array_new(mem, length); + negCls = new int[length](); } t.fncTag = APPLY_SUB_AND; @@ -167,12 +165,10 @@ Formula* Naming::apply_iter(Formula* top_f) { case OR: { FormulaList* fs = tas.f->args(); unsigned length = FormulaList::length(fs); - void* mem = ALLOC_UNKNOWN(length * sizeof(int), "Naming::apply"); - int* cls = array_new(mem, length); + int *cls = new int[length](); int* negCls = 0; if (tas.where == UNDER_IFF) { - mem = ALLOC_UNKNOWN(length * sizeof(int), "Naming::apply"); - negCls = array_new(mem, length); + negCls = new int[length](); } if (tas.where == ON_TOP) { tas.where = OTHER; @@ -317,14 +313,12 @@ Formula* Naming::apply_iter(Formula* top_f) { FormulaList::push(gs[i], rs); } f = new JunctionFormula(AND, rs); - DEALLOC_UNKNOWN(gs, "Naming::apply"); + delete[] gs; } else if (fs != f->args()) { f = new JunctionFormula(AND, fs); } - DEALLOC_UNKNOWN(sand.cls, "Naming::apply"); - if (sand.negCls) { - DEALLOC_UNKNOWN(sand.negCls, "Naming::apply"); - } + delete[] sand.cls; + delete[] sand.negCls; { Result r; @@ -341,8 +335,7 @@ Formula* Naming::apply_iter(Formula* top_f) { // conjunction under disjunction or IFF, should be split split = true; if (!gs) { - void* mem = ALLOC_UNKNOWN(length * sizeof(Formula*), "Naming::apply"); - gs = array_new(mem, length); + gs = new Formula*[length](); int j = 0; FormulaList::Iterator hs(fs); while (hs.hasNext()) { @@ -439,14 +432,12 @@ Formula* Naming::apply_iter(Formula* top_f) { FormulaList::push(gs[i], rs); } f = new JunctionFormula(OR, rs); - DEALLOC_UNKNOWN(gs, "Naming::apply"); + delete[] gs; } else if (fs != f->args()) { f = new JunctionFormula(OR, fs); } - DEALLOC_UNKNOWN(sor.cls, "Naming::apply"); - if (sor.negCls) { - DEALLOC_UNKNOWN(sor.negCls, "Naming::apply"); - } + delete[] sor.cls; + delete[] sor.negCls; { Result r; @@ -463,8 +454,7 @@ Formula* Naming::apply_iter(Formula* top_f) { // splitWhat != 0 split = true; if (!gs) { - void* mem = ALLOC_UNKNOWN(length * sizeof(Formula*), "Naming::apply"); - gs = array_new(mem, length); + gs = new Formula*[length](); int j = 0; FormulaList::Iterator hs(fs); @@ -756,12 +746,10 @@ Formula* Naming::apply_sub(Formula* f, Where where, int& pos, int& neg) { case AND: { FormulaList* fs = f->args(); unsigned length = FormulaList::length(fs); - void* mem = ALLOC_UNKNOWN(length * sizeof(int), "Naming::apply"); - int* cls = array_new(mem, length); + int *cls = new int[length](); int* negCls = 0; if (where == UNDER_IFF) { - mem = ALLOC_UNKNOWN(length * sizeof(int), "Naming::apply"); - negCls = array_new(mem, length); + negCls = new int[length](); } fs = apply_list(fs, where, cls, negCls); bool split = false; @@ -825,14 +813,12 @@ Formula* Naming::apply_sub(Formula* f, Where where, int& pos, int& neg) { FormulaList::push(gs[i], rs); } f = new JunctionFormula(AND, rs); - DEALLOC_UNKNOWN(gs, "Naming::apply"); + delete[] gs; } else if (fs != f->args()) { f = new JunctionFormula(AND, fs); } - DEALLOC_UNKNOWN(cls, "Naming::apply"); - if (negCls) { - DEALLOC_UNKNOWN(negCls, "Naming::apply"); - } + delete[] cls; + delete[] negCls; neg = product; pos = sum; return f; @@ -841,8 +827,7 @@ Formula* Naming::apply_sub(Formula* f, Where where, int& pos, int& neg) { // conjunction under disjunction or IFF, should be split split = true; if (!gs) { - void* mem = ALLOC_UNKNOWN(length * sizeof(Formula*), "Naming::apply"); - gs = array_new(mem, length); + gs = new Formula *[length](); int j = 0; FormulaList::Iterator hs(fs); while (hs.hasNext()) { @@ -866,12 +851,10 @@ Formula* Naming::apply_sub(Formula* f, Where where, int& pos, int& neg) { case OR: { FormulaList* fs = f->args(); unsigned length = FormulaList::length(fs); - void* mem = ALLOC_UNKNOWN(length * sizeof(int), "Naming::apply"); - int* cls = array_new(mem, length); + int *cls = new int[length](); int* negCls = 0; if (where == UNDER_IFF) { - mem = ALLOC_UNKNOWN(length * sizeof(int), "Naming::apply"); - negCls = array_new(mem, length); + negCls = new int[length](); } if (where == ON_TOP) { where = OTHER; @@ -938,14 +921,12 @@ Formula* Naming::apply_sub(Formula* f, Where where, int& pos, int& neg) { FormulaList::push(gs[i], rs); } f = new JunctionFormula(OR, rs); - DEALLOC_UNKNOWN(gs, "Naming::apply"); + delete[] gs; } else if (fs != f->args()) { f = new JunctionFormula(OR, fs); } - DEALLOC_UNKNOWN(cls, "Naming::apply"); - if (negCls) { - DEALLOC_UNKNOWN(negCls, "Naming::apply"); - } + delete[] cls; + delete[] negCls; neg = sum; pos = product; return f; @@ -954,8 +935,7 @@ Formula* Naming::apply_sub(Formula* f, Where where, int& pos, int& neg) { // splitWhat != 0 split = true; if (!gs) { - void* mem = ALLOC_UNKNOWN(length * sizeof(Formula*), "Naming::apply"); - gs = array_new(mem, length); + gs = new Formula *[length](); int j = 0; FormulaList::Iterator hs(fs); while (hs.hasNext()) { diff --git a/Shell/NewCNF.hpp b/Shell/NewCNF.hpp index b1c0d901dd..344cfd42d0 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.cpp b/Shell/Options.cpp index b4a4568c6a..d7dabf4529 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -2465,10 +2465,6 @@ void Options::output (ostream& str) const } if(!explainOption().empty()){ - - //We bypass the allocator here because of the use of vstringstream - BYPASSING_ALLOCATOR; - AbstractOptionValue* option; vstring name = explainOption(); try{ @@ -2528,10 +2524,6 @@ void Options::output (ostream& str) const bool experimental = showExperimentalOptions(); if(normalshow || experimental) { - - //We bypass the allocator here because of the use of vstringstream - BYPASSING_ALLOCATOR; - Mode this_mode = _mode.actualValue; //str << "=========== Options ==========\n"; @@ -2589,7 +2581,6 @@ void Options::output (ostream& str) const oit.next()->output(str,lineWrapInShowOptions()); } //str << (*groups[i]).str(); - //BYPASSING_ALLOCATOR; //delete groups[i]; } @@ -3277,7 +3268,6 @@ void Options::setForcedOptionValues() */ vstring Options::generateEncodedOptions() const { - BYPASSING_ALLOCATOR; vostringstream res; //saturation algorithm vstring sat; diff --git a/Shell/Options.hpp b/Shell/Options.hpp index c5bd858033..caaa559d18 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 eece849eee..b9d26783b8 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 72c799112e..67e063e073 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 181d5d717b..8393587cc0 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 63c933e770..60104306c6 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 7baf8891e0..e508ea3673 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); diff --git a/Shell/UIHelper.cpp b/Shell/UIHelper.cpp index 3dc7c1e6bc..9110f3ff33 100644 --- a/Shell/UIHelper.cpp +++ b/Shell/UIHelper.cpp @@ -254,7 +254,6 @@ void resetParsing(T exception, vstring inputFile, istream*& input,vstring nowtry env.endOutput(); } - BYPASSING_ALLOCATOR; delete static_cast(input); input=new ifstream(inputFile.c_str()); } @@ -288,9 +287,6 @@ Problem* UIHelper::getInputProblem(const Options& opts) inputSyntax = Options::InputSyntax::TPTP; } } else { - // CAREFUL: this might not be enough if the ifstream (re)allocates while being operated - BYPASSING_ALLOCATOR; - input=new ifstream(inputFile.c_str()); if (input->fail()) { USER_ERROR("Cannot open problem file: "+inputFile); @@ -355,8 +351,6 @@ Problem* UIHelper::getInputProblem(const Options& opts) break; } if (inputFile!="") { - BYPASSING_ALLOCATOR; - delete static_cast(input); input=0; } @@ -441,7 +435,6 @@ void UIHelper::outputResult(ostream& out) } if (env.options->latexOutput() != "off") { - BYPASSING_ALLOCATOR; // for ofstream ofstream latexOut(env.options->latexOutput().c_str()); LaTeX formatter; diff --git a/Test/SyntaxSugar.hpp b/Test/SyntaxSugar.hpp index 23989fec93..0b7cdaa183 100644 --- a/Test/SyntaxSugar.hpp +++ b/Test/SyntaxSugar.hpp @@ -560,7 +560,6 @@ class FuncSugar { template TermSugar operator()(As... args) const { - BYPASSING_ALLOCATOR Stack as { TermSugar(args).sugaredExpr()... }; return TermList(Term::create(_functor, as.size(), @@ -589,10 +588,8 @@ class TypeConSugar { unsigned _functor; public: - TypeConSugar(const char* name, unsigned arity) + TypeConSugar(const char* name, unsigned arity) { - BYPASSING_ALLOCATOR - bool added = false; _functor = env.signature->addTypeCon(name, arity, added); if (added) @@ -628,12 +625,11 @@ class PredSugar { public: PredSugar(const char* name, Stack args, unsigned taArity = 0) { - BYPASSING_ALLOCATOR Stack as; for (auto a : args) { as.push(a.sugaredExpr()); } - + if(taArity){ TermStack vars = {TermList(101, false), TermList(102, false), TermList(103, false)}; SortHelper::normaliseArgSorts(vars, as); diff --git a/vampire.cpp b/vampire.cpp index 600b1650f9..bc6f86b523 100644 --- a/vampire.cpp +++ b/vampire.cpp @@ -204,8 +204,6 @@ void outputClausesToLaTeX(Problem* prb) { ASS(env.options->latexOutput()!="off"); - BYPASSING_ALLOCATOR; // not sure why we need this yet, ofstream? - LaTeX latex; ofstream latexOut(env.options->latexOutput().c_str()); latexOut << latex.header() << endl; @@ -238,8 +236,6 @@ void outputProblemToLaTeX(Problem* prb) { ASS(env.options->latexOutput()!="off"); - BYPASSING_ALLOCATOR; // not sure why we need this yet, ofstream? - LaTeX latex; ofstream latexOut(env.options->latexOutput().c_str()); latexOut << latex.header() << endl; @@ -581,8 +577,6 @@ int main(int argc, char* argv[]) System::registerArgv0(argv[0]); System::setSignalHandlers(); - START_CHECKING_FOR_ALLOCATOR_BYPASSES; - try { // read the command line and interpret it Shell::CommandLine cl(argc, argv); @@ -748,7 +742,6 @@ int main(int argc, char* argv[]) } #if VZ3 catch (z3::exception& exception) { - BYPASSING_ALLOCATOR; vampireReturnValue = VAMP_RESULT_STATUS_UNHANDLED_EXCEPTION; if (outputAllowed()) { cout << "Z3 exception:\n" << exception.msg() << endl;