From 4538f5fe95758f2507c191ab39175491f24e6f67 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 15 Jan 2018 22:47:40 -0800 Subject: [PATCH] Removing more miscellaneous throw specifiers. (#1509) Removing more miscellaneous throw specifiers. Also fixing the spelling of amount in several places. --- src/prop/bvminisat/core/Solver.cc | 6 +-- src/prop/bvminisat/core/Solver.h | 6 +-- src/prop/minisat/core/Solver.cc | 5 +- src/prop/prop_engine.cpp | 9 ++-- src/prop/prop_engine.h | 6 ++- src/prop/sat_solver.h | 4 +- src/prop/theory_proxy.cpp | 5 +- src/prop/theory_proxy.h | 2 +- src/smt/dump.h | 18 ++++---- src/theory/bv/bitblaster_template.h | 19 ++++---- src/theory/bv/lazy_bitblaster.cpp | 10 ++-- src/theory/bv/theory_bv.cpp | 5 +- src/theory/bv/theory_bv.h | 2 +- .../theory_bv_rewrite_rules_normalization.h | 20 ++++---- .../theory_bv_rewrite_rules_simplification.h | 23 +++++----- src/theory/bv/theory_bv_utils.h | 9 ++-- src/theory/logic_info.cpp | 7 +-- src/theory/logic_info.h | 6 +-- src/theory/rewriter_attributes.h | 12 +++-- src/theory/theory.cpp | 46 ++++++++++--------- src/theory/theory.h | 20 ++++---- src/theory/theory_engine.cpp | 10 ++-- src/theory/theory_engine.h | 7 ++- src/theory/theory_model.cpp | 3 +- src/util/resource_manager.h | 4 +- 25 files changed, 139 insertions(+), 125 deletions(-) diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 0ca4b637b..2d6e318f2 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -1469,10 +1469,10 @@ void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::BVProofProxy* p } void Solver::setNotify(Notify* toNotify) { d_notify = toNotify; } - -bool Solver::withinBudget(uint64_t ammount) const { +bool Solver::withinBudget(uint64_t amount) const +{ AlwaysAssert(d_notify); - d_notify->spendResource(ammount); + d_notify->spendResource(amount); d_notify->safePoint(0); return !asynch_interrupt && diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index b3b792ef5..da4fb4c16 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -61,8 +61,8 @@ public: */ virtual void notify(vec& learnt) = 0; - virtual void spendResource(unsigned ammount) = 0; - virtual void safePoint(unsigned ammount) = 0; + virtual void spendResource(unsigned amount) = 0; + virtual void safePoint(unsigned amount) = 0; }; //================================================================================================= @@ -344,7 +344,7 @@ protected: CRef reason (Var x) const; int level (Var x) const; double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... - bool withinBudget (uint64_t ammount) const; + bool withinBudget (uint64_t amount) const; // Static helpers: // diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 2b58f2f17..b034f8460 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -1833,11 +1833,12 @@ void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* else if (to[cr].has_extra()) to[cr].calcAbstraction(); } -inline bool Solver::withinBudget(uint64_t ammount) const { +inline bool Solver::withinBudget(uint64_t amount) const +{ Assert (proxy); // spendResource sets async_interrupt or throws UnsafeInterruptException // depending on whether hard-limit is enabled - proxy->spendResource(ammount); + proxy->spendResource(amount); bool within_budget = !asynch_interrupt && (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) && diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 1a56fa141..23f7ea6b5 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -288,8 +288,8 @@ unsigned PropEngine::getAssertionLevel() const { bool PropEngine::isRunning() const { return d_inCheckSat; } - -void PropEngine::interrupt() throw(ModalException) { +void PropEngine::interrupt() +{ if(! d_inCheckSat) { return; } @@ -299,8 +299,9 @@ void PropEngine::interrupt() throw(ModalException) { Debug("prop") << "interrupt()" << endl; } -void PropEngine::spendResource(unsigned ammount) throw (UnsafeInterruptException) { - d_resourceManager->spendResource(ammount); +void PropEngine::spendResource(unsigned amount) +{ + d_resourceManager->spendResource(amount); } bool PropEngine::properExplanation(TNode node, TNode expl) const { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 4802ae52c..f3a69be96 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -226,14 +226,16 @@ public: /** * Interrupt a running solver (cause a timeout). + * + * Can potentially throw a ModalException. */ - void interrupt() throw(ModalException); + void interrupt(); /** * Informs the ResourceManager that a resource has been spent. If out of * resources, can throw an UnsafeInterruptException exception. */ - void spendResource(unsigned ammount) throw (UnsafeInterruptException); + void spendResource(unsigned amount); /** * For debugging. Return true if "expl" is a well-formed diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index c790f59f6..7be5305ad 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -116,8 +116,8 @@ public: * Notify about a learnt clause. */ virtual void notify(SatClause& clause) = 0; - virtual void spendResource(unsigned ammount) = 0; - virtual void safePoint(unsigned ammount) = 0; + virtual void spendResource(unsigned amount) = 0; + virtual void safePoint(unsigned amount) = 0; };/* class BVSatSolverInterface::Notify */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 8f74b716f..ae27554f4 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -238,8 +238,9 @@ void TheoryProxy::logDecision(SatLiteral lit) { #endif /* CVC4_REPLAY */ } -void TheoryProxy::spendResource(unsigned ammount) { - d_theoryEngine->spendResource(ammount); +void TheoryProxy::spendResource(unsigned amount) +{ + d_theoryEngine->spendResource(amount); } bool TheoryProxy::isDecisionRelevant(SatVariable var) { diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 67d3b3b7e..cc89fbdd5 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -92,7 +92,7 @@ public: void logDecision(SatLiteral lit); - void spendResource(unsigned ammount); + void spendResource(unsigned amount); bool isDecisionEngineDone(); diff --git a/src/smt/dump.h b/src/smt/dump.h index 3c4d14693..b7cfc7ae7 100644 --- a/src/smt/dump.h +++ b/src/smt/dump.h @@ -34,24 +34,24 @@ class CVC4_PUBLIC CVC4dumpstream { CommandSequence* d_commands; #endif /* CVC4_PORTFOLIO */ -public: - CVC4dumpstream() throw() + public: + CVC4dumpstream() #if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO) - : d_os(NULL), d_commands(NULL) + : d_os(NULL), d_commands(NULL) #elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - : d_os(NULL) + : d_os(NULL) #elif defined(CVC4_PORTFOLIO) - : d_commands(NULL) + : d_commands(NULL) #endif /* CVC4_PORTFOLIO */ { } - CVC4dumpstream(std::ostream& os, CommandSequence& commands) throw() + CVC4dumpstream(std::ostream& os, CommandSequence& commands) #if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO) - : d_os(&os), d_commands(&commands) + : d_os(&os), d_commands(&commands) #elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - : d_os(&os) + : d_os(&os) #elif defined(CVC4_PORTFOLIO) - : d_commands(&commands) + : d_commands(&commands) #endif /* CVC4_PORTFOLIO */ { } diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 33dd4387e..1dc2d8b1e 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -137,10 +137,10 @@ class TLazyBitblaster : public TBitblaster { , d_lazyBB(lbv) {} - bool notify(prop::SatLiteral lit); - void notify(prop::SatClause& clause); - void spendResource(unsigned ammount); - void safePoint(unsigned ammount); + bool notify(prop::SatLiteral lit) override; + void notify(prop::SatClause& clause) override; + void spendResource(unsigned amount) override; + void safePoint(unsigned amount) override; }; TheoryBV *d_bv; @@ -249,12 +249,13 @@ public: class MinisatEmptyNotify : public prop::BVSatSolverInterface::Notify { public: MinisatEmptyNotify() {} - bool notify(prop::SatLiteral lit) { return true; } - void notify(prop::SatClause& clause) { } - void spendResource(unsigned ammount) { - NodeManager::currentResourceManager()->spendResource(ammount); + bool notify(prop::SatLiteral lit) override { return true; } + void notify(prop::SatClause& clause) override {} + void spendResource(unsigned amount) override + { + NodeManager::currentResourceManager()->spendResource(amount); } - void safePoint(unsigned ammount) {} + void safePoint(unsigned amount) override {} }; diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index d108a37f0..33342dc2e 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -384,12 +384,14 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) { } } -void TLazyBitblaster::MinisatNotify::spendResource(unsigned ammount) { - d_bv->spendResource(ammount); +void TLazyBitblaster::MinisatNotify::spendResource(unsigned amount) +{ + d_bv->spendResource(amount); } -void TLazyBitblaster::MinisatNotify::safePoint(unsigned ammount) { - d_bv->d_out->safePoint(ammount); +void TLazyBitblaster::MinisatNotify::safePoint(unsigned amount) +{ + d_bv->d_out->safePoint(amount); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index af1dd5331..c6f2ec74b 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -125,8 +125,9 @@ void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { } } -void TheoryBV::spendResource(unsigned ammount) throw(UnsafeInterruptException) { - getOutputChannel().spendResource(ammount); +void TheoryBV::spendResource(unsigned amount) +{ + getOutputChannel().spendResource(amount); } TheoryBV::Statistics::Statistics(const std::string &name): diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index a425cbdc8..8cefe03b2 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -120,7 +120,7 @@ private: Statistics d_statistics; - void spendResource(unsigned ammount) throw(UnsafeInterruptException); + void spendResource(unsigned amount); /** * Return the uninterpreted function symbol corresponding to division-by-zero diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 07688a8bb..d17f20152 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -109,8 +109,8 @@ Node RewriteRule::apply(TNode node) { } else if (low < extendee_size && high >= extendee_size) { // if extract overlaps sign extend and extendee Node low_extract = utils::mkExtract(extendee, extendee_size - 1, low); - unsigned new_ammount = high - extendee_size + 1; - resultNode = utils::mkSignExtend(low_extract, new_ammount); + unsigned new_amount = high - extendee_size + 1; + resultNode = utils::mkSignExtend(low_extract, new_amount); } else { // extract only over sign extend Assert (low >= extendee_size); @@ -529,15 +529,15 @@ bool RewriteRule::applies(TNode node) { if (!node[1].isConst()) return false; TNode extract = node[0]; TNode c = node[1]; - unsigned ammount = utils::getSize(c); - - if (utils::getSize(node) != utils::getSize(extract[0])) return false; - if (c != utils::mkConst(ammount, 0)) return false; + unsigned amount = utils::getSize(c); + + if (utils::getSize(node) != utils::getSize(extract[0])) return false; + if (c != utils::mkZero(amount)) return false; unsigned low = utils::getExtractLow(extract); if (low != 0) return false; unsigned high = utils::getExtractHigh(extract); - if (high + ammount + 1 != utils::getSize(node)) return false; + if (high + amount + 1 != utils::getSize(node)) return false; return true; } @@ -546,9 +546,9 @@ Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; unsigned size = utils::getSize(node); Node factor = node[0][0]; - Assert(utils::getSize(factor) == utils::getSize(node)); - BitVector ammount = BitVector(size, utils::getSize(node[1])); - Node coef = utils::mkConst(BitVector(size, 1u).leftShift(ammount)); + Assert(utils::getSize(factor) == utils::getSize(node)); + BitVector amount = BitVector(size, utils::getSize(node[1])); + Node coef = utils::mkConst(BitVector(size, 1u).leftShift(amount)); return utils::mkNode(kind::BITVECTOR_MULT, factor, coef); } diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 5956ced7e..067440ee2 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -1127,31 +1127,32 @@ bool RewriteRule::applies(TNode node) { template<> inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - unsigned ammount1 = node.getOperator().getConst().signExtendAmount; + unsigned amount1 = + node.getOperator().getConst().signExtendAmount; NodeManager* nm = NodeManager::currentNM(); if (node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND) { - unsigned ammount2 = node[0].getOperator().getConst().zeroExtendAmount; - if (ammount2 == 0) { + unsigned amount2 = + node[0].getOperator().getConst().zeroExtendAmount; + if (amount2 == 0) + { NodeBuilder<> nb(kind::BITVECTOR_SIGN_EXTEND); - Node op = nm->mkConst(BitVectorSignExtend(ammount1)); + Node op = nm->mkConst(BitVectorSignExtend(amount1)); nb << op << node[0][0]; Node res = nb; return res; } NodeBuilder<> nb(kind::BITVECTOR_ZERO_EXTEND); - Node op = nm->mkConst(BitVectorZeroExtend(ammount1 + ammount2)); + Node op = nm->mkConst( + BitVectorZeroExtend(amount1 + amount2)); nb << op << node[0][0]; Node res = nb; return res; } Assert (node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND); - unsigned ammount2 = node[0].getOperator().getConst().signExtendAmount; - NodeBuilder<> nb(kind::BITVECTOR_SIGN_EXTEND); - Node op = nm->mkConst(BitVectorSignExtend(ammount1+ ammount2)); - nb << op << node[0][0]; - Node res = nb; - return res; + unsigned amount2 = + node[0].getOperator().getConst().signExtendAmount; + return utils::mkSignExtend(node[0][0], amount1 + amount2); } /** diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index ecd93cd2c..e304e4801 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -144,10 +144,11 @@ inline Node mkXor(TNode node1, TNode node2) { return NodeManager::currentNM()->mkNode(kind::XOR, node1, node2); } - -inline Node mkSignExtend(TNode node, unsigned ammount) { - NodeManager* nm = NodeManager::currentNM(); - Node signExtendOp = nm->mkConst(BitVectorSignExtend(ammount)); +inline Node mkSignExtend(TNode node, unsigned amount) +{ + NodeManager* nm = NodeManager::currentNM(); + Node signExtendOp = + nm->mkConst(BitVectorSignExtend(amount)); return nm->mkNode(signExtendOp, node); } diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index bf1a9bf65..a458eec30 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -47,7 +47,7 @@ LogicInfo::LogicInfo() } } -LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) +LogicInfo::LogicInfo(std::string logicString) : d_logicString(""), d_theories(THEORY_LAST, false), d_sharingTheories(0), @@ -63,7 +63,7 @@ LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) lock(); } -LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) +LogicInfo::LogicInfo(const char* logicString) : d_logicString(""), d_theories(THEORY_LAST, false), d_sharingTheories(0), @@ -327,7 +327,8 @@ std::string LogicInfo::getLogicString() const { return d_logicString; } -void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) { +void LogicInfo::setLogicString(std::string logicString) +{ PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) { diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index dc88cc9f4..cbb04604e 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -90,14 +90,14 @@ public: * Throws an IllegalArgumentException if the logic string cannot * be interpreted. */ - LogicInfo(std::string logicString) throw(IllegalArgumentException); + LogicInfo(std::string logicString); /** * Construct a LogicInfo from an SMT-LIB-like logic string. * Throws an IllegalArgumentException if the logic string cannot * be interpreted. */ - LogicInfo(const char* logicString) throw(IllegalArgumentException); + LogicInfo(const char* logicString); // ACCESSORS @@ -157,7 +157,7 @@ public: * Throws an IllegalArgumentException if the string can't be * interpreted. */ - void setLogicString(std::string logicString) throw(IllegalArgumentException); + void setLogicString(std::string logicString); /** * Enable all functionality. All theories, plus quantifiers, will be diff --git a/src/theory/rewriter_attributes.h b/src/theory/rewriter_attributes.h index ec120ff0c..60fa3a417 100644 --- a/src/theory/rewriter_attributes.h +++ b/src/theory/rewriter_attributes.h @@ -35,7 +35,8 @@ struct RewriteAttibute { /** * Get the value of the pre-rewrite cache. */ - static Node getPreRewriteCache(TNode node) throw() { + static Node getPreRewriteCache(TNode node) + { Node cache; if (node.hasAttribute(pre_rewrite())) { node.getAttribute(pre_rewrite(), cache); @@ -52,7 +53,8 @@ struct RewriteAttibute { /** * Set the value of the pre-rewrite cache. */ - static void setPreRewriteCache(TNode node, TNode cache) throw() { + static void setPreRewriteCache(TNode node, TNode cache) + { Trace("rewriter") << "setting pre-rewrite of " << node << " to " << cache << std::endl; Assert(!cache.isNull()); if (node == cache) { @@ -66,7 +68,8 @@ struct RewriteAttibute { * Get the value of the post-rewrite cache. * none). */ - static Node getPostRewriteCache(TNode node) throw() { + static Node getPostRewriteCache(TNode node) + { Node cache; if (node.hasAttribute(post_rewrite())) { node.getAttribute(post_rewrite(), cache); @@ -83,7 +86,8 @@ struct RewriteAttibute { /** * Set the value of the post-rewrite cache. v cannot be a null Node. */ - static void setPostRewriteCache(TNode node, TNode cache) throw() { + static void setPostRewriteCache(TNode node, TNode cache) + { Assert(!cache.isNull()); Trace("rewriter") << "setting rewrite of " << node << " to " << cache << std::endl; if (node == cache) { diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 8509e84ab..069767968 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -51,28 +51,30 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ return os; }/* ostream& operator<<(ostream&, Theory::Effort) */ - -Theory::Theory(TheoryId id, context::Context* satContext, - context::UserContext* userContext, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, - std::string name) throw() - : d_id(id) - , d_instanceName(name) - , d_satContext(satContext) - , d_userContext(userContext) - , d_logicInfo(logicInfo) - , d_facts(satContext) - , d_factsHead(satContext, 0) - , d_sharedTermsIndex(satContext, 0) - , d_careGraph(NULL) - , d_quantEngine(NULL) - , d_extTheory(NULL) - , d_checkTime(getFullInstanceName() + "::checkTime") - , d_computeCareGraphTime(getFullInstanceName() + "::computeCareGraphTime") - , d_sharedTerms(satContext) - , d_out(&out) - , d_valuation(valuation) - , d_proofsEnabled(false) +Theory::Theory(TheoryId id, + context::Context* satContext, + context::UserContext* userContext, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + std::string name) + : d_id(id), + d_instanceName(name), + d_satContext(satContext), + d_userContext(userContext), + d_logicInfo(logicInfo), + d_facts(satContext), + d_factsHead(satContext, 0), + d_sharedTermsIndex(satContext, 0), + d_careGraph(NULL), + d_quantEngine(NULL), + d_extTheory(NULL), + d_checkTime(getFullInstanceName() + "::checkTime"), + d_computeCareGraphTime(getFullInstanceName() + "::computeCareGraphTime"), + d_sharedTerms(satContext), + d_out(&out), + d_valuation(valuation), + d_proofsEnabled(false) { smtStatisticsRegistry()->registerStat(&d_checkTime); smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime); diff --git a/src/theory/theory.h b/src/theory/theory.h index 204c514a9..0571a67b7 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -177,10 +177,13 @@ private: * The pair is assumed to uniquely identify this Theory * w.r.t. the SmtEngine. */ - Theory(TheoryId id, context::Context* satContext, - context::UserContext* userContext, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, - std::string instance = "") throw(); // taking : No default. + Theory(TheoryId id, + context::Context* satContext, + context::UserContext* userContext, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + std::string instance = ""); // taking : No default. /** * This is called at shutdown time by the TheoryEngine, just before @@ -289,13 +292,8 @@ public: return node.getNumChildren() == 0 || theoryOf(node) != theoryId; } - /** - * Returns true if the assertFact queue is empty - */ - bool done() const throw() { - return d_factsHead == d_facts.size(); - } - + /** Returns true if the assertFact queue is empty*/ + bool done() const { return d_factsHead == d_facts.size(); } /** * Destructs a Theory. */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 4e2062c43..435dadce7 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -370,10 +370,7 @@ TheoryEngine::~TheoryEngine() { smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded); } -void TheoryEngine::interrupt() throw(ModalException) { - d_interrupted = true; -} - +void TheoryEngine::interrupt() { d_interrupted = true; } void TheoryEngine::preRegister(TNode preprocessed) { Debug("theory") << "TheoryEngine::preRegister( " << preprocessed << ")" << std::endl; @@ -2320,8 +2317,9 @@ std::pair TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, T } } -void TheoryEngine::spendResource(unsigned ammount) { - d_resourceManager->spendResource(ammount); +void TheoryEngine::spendResource(unsigned amount) +{ + d_resourceManager->spendResource(amount); } void TheoryEngine::enableTheoryAlternative(const std::string& name){ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index f380e86aa..22e269409 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -461,10 +461,9 @@ public: /** Destroys a theory engine */ ~TheoryEngine(); - void interrupt() throw(ModalException); - /** - * "Spend" a resource during a search or preprocessing. - */ + void interrupt(); + + /** "Spend" a resource during a search or preprocessing.*/ void spendResource(unsigned amount); /** diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 5555e29e2..739925f4f 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -50,7 +50,8 @@ TheoryModel::TheoryModel(context::Context* c, d_eeContext->push(); } -TheoryModel::~TheoryModel() throw() { +TheoryModel::~TheoryModel() +{ d_eeContext->pop(); delete d_equalityEngine; delete d_eeContext; diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index e49b27286..c84bed38d 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -91,11 +91,11 @@ class CVC4_PUBLIC ResourceManager { /** The amount of resource used. */ uint64_t d_cumulativeResourceUsed; - /** The ammount of resource used during this call. */ + /** The amount of resource used during this call. */ uint64_t d_thisCallResourceUsed; /** - * The ammount of resource budget for this call (min between per call + * The amount of resource budget for this call (min between per call * budget and left-over cumulative budget. */ uint64_t d_thisCallTimeBudget; -- 2.30.2