Removing more miscellaneous throw specifiers. (#1509)

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

7 files changed, 47 insertions, 41 deletions

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