Removing more miscellaneous throw specifiers. (#1509)

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

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 0ca4b637bff60406391fdde69198f45089807f85..2d6e318f237e12723f50092b3c199fd422430000 100644 (file)
--- 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 b3b792ef595dcc2c64abddf5f9ac535e62bd9736..da4fb4c1663b2de10bc825c74eb8a74d7b28b8b6 100644 (file)
--- 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 2b58f2f1750a96a2ac5aa0d0c10a57a11e478271..b034f846071a4bef2afcc475d195e3c8bf5a7df1 100644 (file)
--- 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 1a56fa141a1caf9c4f5261d37bc78f8b907d4e6f..23f7ea6b5fea6ad2f6d0de9f4a1525cce07861d2 100644 (file)
--- 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 4802ae52c55fd63c45567dcc80bfa96aa644c511..f3a69be9673e92582d7edd1a9d32a9d41bd7ef19 100644 (file)
--- 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 c790f59f60c8a7035c43183e04b81091add807c5..7be5305adb5f4d78b6f189f74bd5297d7b47c911 100644 (file)
--- 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 8f74b716f278969a28653f4d240422ccb4536d81..ae27554f418091bbcee64fc0a402c9b826da874c 100644 (file)
--- 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 67d3b3b7e507317395e64e85acfa3acc9155c6fd..cc89fbdd53c96f1fa540e4ed86d3356ac3e8c0f7 100644 (file)
--- 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 3c4d14693c4b173b0a3d95b19eee9f163d723ef2..b7cfc7ae7dfbd63b69aa084bb3274330e8d84d5a 100644 (file)
--- 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 33dd4387e308dcec59826f1d7e1ad3032d677d43..1dc2d8b1ed05a1953cf8067cdf6653f6cd285d04 100644 (file)
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -137,10 +137,10 @@ class TLazyBitblaster :  public TBitblaster<Node> {
     , 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 d108a37f0477e1430272760ba8b3f6ef37027a7a..33342dc2e7b8f5ed8d53c0418e5b17e9c8f6d3b3 100644 (file)
--- 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 af1dd5331e23ee60f8af7bb045805a46b7bdc7e7..c6f2ec74b40cef5faf4f6951dc1cd85e35571822 100644 (file)
--- 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 a425cbdc887fc37bc0890a0a6680610d85d75e44..8cefe03b2bb13589156f64fedcad47882a3e9ec1 100644 (file)
--- 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 07688a8bbed6b95880e73c59422eea70fae95573..d17f2015275c26b3adb308e0c782e4294fc38116 100644 (file)
--- 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<ExtractSignExtend>::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<ConcatToMult>::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<ConcatToMult>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<ConcatToMult>(" << 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 5956ced7ece2ee427c887740dff861288065b502..067440ee26e5d029810fbdca70dcc66486e4e648 100644 (file)
--- 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<MergeSignExtend>::applies(TNode node) {
 template<> inline
 Node RewriteRule<MergeSignExtend>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<MergeSignExtend>(" << node << ")" << std::endl;
-  unsigned ammount1 = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+  unsigned amount1 =
+      node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
 
   NodeManager* nm = NodeManager::currentNM();
   if (node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND) {
-    unsigned ammount2 = node[0].getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
-    if (ammount2 == 0) {
+    unsigned amount2 =
+        node[0].getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
+    if (amount2 == 0)
+    {
       NodeBuilder<> nb(kind::BITVECTOR_SIGN_EXTEND);
-      Node op = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(ammount1));
+      Node op = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount1));
       nb << op << node[0][0];
       Node res = nb;
       return res;
     }
     NodeBuilder<> nb(kind::BITVECTOR_ZERO_EXTEND);
-    Node op = nm->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(ammount1 + ammount2));
+    Node op = nm->mkConst<BitVectorZeroExtend>(
+        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<BitVectorSignExtend>().signExtendAmount;
-  NodeBuilder<> nb(kind::BITVECTOR_SIGN_EXTEND);
-  Node op = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(ammount1+ ammount2));
-  nb << op << node[0][0];
-  Node res = nb;
-  return res;
+  unsigned amount2 =
+      node[0].getOperator().getConst<BitVectorSignExtend>().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 ecd93cd2cac93f3a9f083836ff7f2ffb1d92d695..e304e48015204d46a6de7b069dc7e7d397678d04 100644 (file)
--- 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>(BitVectorSignExtend(ammount));
+inline Node mkSignExtend(TNode node, unsigned amount)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node signExtendOp =
+      nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount));
   return nm->mkNode(signExtendOp, node); 
 }
 

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index bf1a9bf6524e17186c5ad9d0926196a34b5e3551..a458eec304df96f75d0632f65e042bcb3be8cf77 100644 (file)
--- 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 dc88cc9f4a5eda6a736f2a1ebb15f939767b7753..cbb04604ef2eb2851da552a913d278d8a5925058 100644 (file)
--- 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 ec120ff0c098068457af6df1cfe57bd4ececca5a..60fa3a417dd19c2ebb6e229cf07a3e1d0e71604c 100644 (file)
--- 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 8509e84ab4f5b63145cf44fbe290012a01237e25..069767968a980f6ecf26aede2c93466a4ee724c3 100644 (file)
--- 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 204c514a977bca55ba49b87ec952e1c20a3b57ff..0571a67b7915899ab731be6ebf4056e4a410d0c3 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -177,10 +177,13 @@ private:
    * The pair <id, instance> 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 4e2062c439991fba03b5049722933fca7e3a1d33..435dadce7f2acb6af86b768e54c9b435d829b2f8 100644 (file)
--- 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<bool, Node> 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 f380e86aab29bb579526cd353d7987ebfc91332e..22e2694095ad24678031c85de99feacb6f93122f 100644 (file)
--- 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 5555e29e255095dda84ffb9acc4ff6dd6b1de88b..739925f4fec68737eba9a0b289c91c90187ac9e2 100644 (file)
--- 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 e49b27286024d1b028975ee9180dda939e237963..c84bed38d67087bedc5fdfc08b313397b74575f4 100644 (file)
--- 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;