Removing more miscellaneous throw specifiers. (#1509)

Removing more miscellaneous throw specifiers. Also fixing the spelling of amount in several places.

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();