diff options
author | lianah <lianahady@gmail.com> | 2015-05-29 10:18:36 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2015-05-29 10:18:36 -0400 |
commit | 331f8cccb1f5fc8806774652deb71f23c7572772 (patch) | |
tree | 1cf4b0d6356840f0543b301f8e90544f5ca3dbe3 /src/theory/bv | |
parent | b4aaa40ca834958130a8ee5a922ac45c6de84ce1 (diff) |
changed resource step options to unsigned
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 8 | ||||
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 2 |
4 files changed, 8 insertions, 8 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 4d953b03c..d42c4a8c9 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -135,8 +135,8 @@ class TLazyBitblaster : public TBitblaster<Node> { {} bool notify(prop::SatLiteral lit); void notify(prop::SatClause& clause); - void spendResource(uint64_t ammount); - void safePoint(uint64_t ammount); + void spendResource(unsigned ammount); + void safePoint(unsigned ammount); }; TheoryBV *d_bv; @@ -240,10 +240,10 @@ public: MinisatEmptyNotify() {} bool notify(prop::SatLiteral lit) { return true; } void notify(prop::SatClause& clause) { } - void spendResource(uint64_t ammount) { + void spendResource(unsigned ammount) { NodeManager::currentResourceManager()->spendResource(ammount); } - void safePoint(uint64_t ammount) {} + void safePoint(unsigned ammount) {} }; diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index 61472fd79..59ecc7385 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -356,11 +356,11 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) { } } -void TLazyBitblaster::MinisatNotify::spendResource(uint64_t ammount) { +void TLazyBitblaster::MinisatNotify::spendResource(unsigned ammount) { d_bv->spendResource(ammount); } -void TLazyBitblaster::MinisatNotify::safePoint(uint64_t ammount) { +void TLazyBitblaster::MinisatNotify::safePoint(unsigned ammount) { d_bv->d_out->safePoint(ammount); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 6f399cb7a..95a483d34 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -107,7 +107,7 @@ void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { } } -void TheoryBV::spendResource(uint64_t ammount) throw(UnsafeInterruptException) { +void TheoryBV::spendResource(unsigned ammount) throw(UnsafeInterruptException) { getOutputChannel().spendResource(ammount); } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 3317d1b01..193de55db 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -103,7 +103,7 @@ private: Statistics d_statistics; - void spendResource(uint64_t ammount) throw(UnsafeInterruptException); + void spendResource(unsigned ammount) throw(UnsafeInterruptException); /** * Return the uninterpreted function symbol corresponding to division-by-zero |