diff options
author | Tim King <taking@cs.nyu.edu> | 2018-01-15 22:47:40 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-01-15 22:47:40 -0800 |
commit | 4538f5fe95758f2507c191ab39175491f24e6f67 (patch) | |
tree | 9b288d3601692488e02c10adebf7f90b227981a0 /src/prop | |
parent | 9ee67c0d1180c7cf85fb648b57bb47100db3d633 (diff) |
Removing more miscellaneous throw specifiers. (#1509)
Removing more miscellaneous throw specifiers. Also fixing the spelling of amount in several places.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 6 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.h | 6 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 5 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 9 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 6 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 4 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 5 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 2 |
8 files changed, 24 insertions, 19 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<Lit>& 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(); |