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/bitblaster_template.h | |
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/bitblaster_template.h')
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 19 |
1 files changed, 10 insertions, 9 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 {} }; |