diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 10 | ||||
-rw-r--r-- | src/theory/bv/bv_eager_solver.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 3 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.cpp | 3 | ||||
-rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 10 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 2 |
9 files changed, 20 insertions, 18 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index d4d7bc04c..4d953b03c 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(); - void safePoint(); + void spendResource(uint64_t ammount); + void safePoint(uint64_t ammount); }; TheoryBV *d_bv; @@ -240,10 +240,10 @@ public: MinisatEmptyNotify() {} bool notify(prop::SatLiteral lit) { return true; } void notify(prop::SatClause& clause) { } - void spendResource() { - NodeManager::currentResourceManager()->spendResource(); + void spendResource(uint64_t ammount) { + NodeManager::currentResourceManager()->spendResource(ammount); } - void safePoint() {} + void safePoint(uint64_t ammount) {} }; diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index 57a635c20..0c087ddb9 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -67,7 +67,7 @@ bool EagerBitblastSolver::isInitialized() { } void EagerBitblastSolver::assertFormula(TNode formula) { - d_bv->spendResource(); + d_bv->spendResource(1); Assert (isInitialized()); Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula "<< formula <<"\n"; d_assertionSet.insert(formula); diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index c86572ead..7e3ed46c8 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -152,7 +152,7 @@ bool BitblastSolver::check(Theory::Effort e) { // We need to ensure we are fully propagated, so propagate now if (d_useSatPropagation) { - d_bv->spendResource(); + d_bv->spendResource(1); bool ok = d_bitblaster->propagate(); if (!ok) { std::vector<TNode> conflictAtoms; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 9481b9894..13c31463b 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -21,6 +21,7 @@ #include "theory/bv/slicer.h" #include "theory/theory_model.h" #include "theory/bv/options.h" +#include "smt/options.h" using namespace std; using namespace CVC4; @@ -167,7 +168,7 @@ bool CoreSolver::decomposeFact(TNode fact) { bool CoreSolver::check(Theory::Effort e) { Trace("bitvector::core") << "CoreSolver::check \n"; - d_bv->spendResource(); + d_bv->spendResource(options::theoryCheckStep()); d_checkCalled = true; Assert (!d_bv->inConflict()); diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 660551fe2..55dcbb03a 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -18,6 +18,7 @@ #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" +#include "smt/options.h" using namespace std; using namespace CVC4; @@ -29,7 +30,7 @@ using namespace CVC4::theory::bv::utils; bool InequalitySolver::check(Theory::Effort e) { Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n"; ++(d_statistics.d_numCallstoCheck); - d_bv->spendResource(); + d_bv->spendResource(options::theoryCheckStep()); bool ok = true; while (!done() && ok) { diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 065d5d5ef..eca9f12ab 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -103,7 +103,7 @@ void EagerBitblaster::bbTerm(TNode node, Bits& bits) { return; } - d_bv->spendResource(); + d_bv->spendResource(options::bitblastStep()); Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; d_termBBStrategies[node.getKind()] (node, bits, this); diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index 080f23143..61472fd79 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -170,7 +170,7 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) { return; } - d_bv->spendResource(); + d_bv->spendResource(options::bitblastStep()); Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; ++d_statistics.d_numTerms; @@ -356,12 +356,12 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) { } } -void TLazyBitblaster::MinisatNotify::spendResource() { - d_bv->spendResource(); +void TLazyBitblaster::MinisatNotify::spendResource(uint64_t ammount) { + d_bv->spendResource(ammount); } -void TLazyBitblaster::MinisatNotify::safePoint() { - d_bv->d_out->safePoint(); +void TLazyBitblaster::MinisatNotify::safePoint(uint64_t ammount) { + d_bv->d_out->safePoint(ammount); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 9dcd5ac62..6f399cb7a 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -107,8 +107,8 @@ void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { } } -void TheoryBV::spendResource() throw(UnsafeInterruptException) { - getOutputChannel().spendResource(); +void TheoryBV::spendResource(uint64_t ammount) throw(UnsafeInterruptException) { + getOutputChannel().spendResource(ammount); } TheoryBV::Statistics::Statistics(): diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 11d8cb895..3317d1b01 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() throw(UnsafeInterruptException); + void spendResource(uint64_t ammount) throw(UnsafeInterruptException); /** * Return the uninterpreted function symbol corresponding to division-by-zero |