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/theory/bv | |
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/theory/bv')
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 19 | ||||
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 10 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 5 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 20 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 23 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 9 |
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); } |