diff options
author | lianah <lianahady@gmail.com> | 2013-03-25 20:37:31 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-25 20:37:31 -0400 |
commit | e69531ce6cefe15dcc7afe9b79d2b36c778148fa (patch) | |
tree | 06f773744af58fcb4552bba66cb2da708e21eed6 /src/theory/bv/theory_bv.cpp | |
parent | 7f9b419adf3e45ce12ab9fb9b2d1afa076110e7d (diff) |
cleaned up the bv subtheory interface; added check for inequality theory completeness
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 128 |
1 files changed, 74 insertions, 54 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index bdf93eadc..a62324946 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -22,6 +22,9 @@ #include "theory/bv/bitblaster.h" #include "theory/bv/options.h" #include "theory/bv/theory_bv_rewrite_rules_normalization.h" +#include "theory/bv/bv_subtheory_core.h" +#include "theory/bv/bv_subtheory_inequality.h" +#include "theory/bv/bv_subtheory_bitblast.h" #include "theory/model.h" using namespace CVC4; @@ -37,37 +40,57 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_context(c), d_alreadyPropagatedSet(c), d_sharedTermsSet(c), - d_coreSolver(c, this), - d_inequalitySolver(c, this), - d_bitblastSolver(c, this), + d_subtheories(), + d_subtheoryMap(), d_statistics(), d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), d_propagatedBy(c) - {} - -TheoryBV::~TheoryBV() {} + { + SubtheorySolver* core_solver = new CoreSolver(c, this); + d_subtheories.push_back(core_solver); + d_subtheoryMap[SUB_CORE] = core_solver; + + SubtheorySolver* ineq_solver = new InequalitySolver(c, this); + d_subtheories.push_back(ineq_solver); + d_subtheoryMap[SUB_INEQUALITY] = ineq_solver; + + SubtheorySolver* bb_solver = new BitblastSolver(c, this); + d_subtheories.push_back(bb_solver); + d_subtheoryMap[SUB_BITBLAST] = bb_solver; + } +TheoryBV::~TheoryBV() { + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + delete d_subtheories[i]; + } +} void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { - d_coreSolver.setMasterEqualityEngine(eq); + dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq); } TheoryBV::Statistics::Statistics(): d_avgConflictSize("theory::bv::AvgBVConflictSize"), d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0), - d_solveTimer("theory::bv::solveTimer") + d_solveTimer("theory::bv::solveTimer"), + d_numCallsToCheckFullEffort("theory::bv::NumberOfFullCheckCalls", 0), + d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0) { StatisticsRegistry::registerStat(&d_avgConflictSize); StatisticsRegistry::registerStat(&d_solveSubstitutions); StatisticsRegistry::registerStat(&d_solveTimer); + StatisticsRegistry::registerStat(&d_numCallsToCheckFullEffort); + StatisticsRegistry::registerStat(&d_numCallsToCheckStandardEffort); } TheoryBV::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_avgConflictSize); StatisticsRegistry::unregisterStat(&d_solveSubstitutions); StatisticsRegistry::unregisterStat(&d_solveTimer); + StatisticsRegistry::unregisterStat(&d_numCallsToCheckFullEffort); + StatisticsRegistry::unregisterStat(&d_numCallsToCheckStandardEffort); } @@ -79,9 +102,9 @@ void TheoryBV::preRegisterTerm(TNode node) { // don't use the equality engine in the eager bit-blasting return; } - - d_bitblastSolver.preRegister(node); - d_coreSolver.preRegister(node); + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + d_subtheories[i]->preRegister(node); + } } void TheoryBV::sendConflict() { @@ -99,7 +122,11 @@ void TheoryBV::sendConflict() { void TheoryBV::check(Effort e) { Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; - + if (Theory::fullEffort(e)) { + ++(d_statistics.d_numCallsToCheckFullEffort); + } else { + ++(d_statistics.d_numCallsToCheckStandardEffort); + } // if we are already in conflict just return the conflict if (inConflict()) { sendConflict(); @@ -108,38 +135,37 @@ void TheoryBV::check(Effort e) while (!done()) { TNode fact = get().assertion; - d_coreSolver.assertFact(fact); - d_inequalitySolver.assertFact(fact); - d_bitblastSolver.assertFact(fact); - } - - bool ok = true; - if (!inConflict()) { - ok = d_coreSolver.check(e); + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + d_subtheories[i]->assertFact(fact); + } } - Assert (!ok == inConflict()); - if (!inConflict() && !d_coreSolver.isComplete()) { - ok = d_inequalitySolver.check(e); - } + bool ok = true; + bool complete = false; + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + Assert (!inConflict()); + ok = d_subtheories[i]->check(e); + complete = d_subtheories[i]->isComplete(); - // Assert (!ok == inConflict()); - // if (!inConflict() && !d_coreSolver.isCoreTheory()) { - // if (!inConflict() && !d_inequalitySolver.isInequalityTheory()) { - // ok = d_bitblastSolver.check(e); - // } - - Assert (!ok == inConflict()); - if (inConflict()) { - sendConflict(); + if (!ok) { + // if we are in a conflict no need to check with other theories + Assert (inConflict()); + sendConflict(); + return; + } + if (complete) { + // if the last subtheory was complete we stop + return; + } } } void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){ Assert(!inConflict()); // Assert (fullModel); // can only query full model - d_coreSolver.collectModelInfo(m); - d_bitblastSolver.collectModelInfo(m); + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + d_subtheories[i]->collectModelInfo(m); + } } void TheoryBV::propagate(Effort e) { @@ -255,15 +281,9 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) { - // Ask the appropriate subtheory for the explanation - if (propagatedBy(literal, SUB_CORE)) { - Debug("bitvector::explain") << "TheoryBV::explain(" << literal << "): CORE" << std::endl; - d_coreSolver.explain(literal, assumptions); - } else { - Assert(propagatedBy(literal, SUB_BITBLAST)); - Debug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl; - d_bitblastSolver.explain(literal, assumptions); - } + Assert (wasPropagatedBySubtheory(literal)); + SubTheory sub = getPropagatingSubtheory(literal); + d_subtheoryMap[sub]->explain(literal, assumptions); } @@ -288,7 +308,9 @@ void TheoryBV::addSharedTerm(TNode t) { Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; d_sharedTermsSet.insert(t); if (!options::bitvectorEagerBitblast() && d_useEqualityEngine) { - d_coreSolver.addSharedTerm(t); + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + d_subtheories[i]->addSharedTerm(t); + } } } @@ -298,15 +320,13 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) if (options::bitvectorEagerBitblast()) { return EQUALITY_UNKNOWN; } - - EqualityStatus status = d_coreSolver.getEqualityStatus(a, b); - if (status == EQUALITY_UNKNOWN) { - status = d_inequalitySolver.getEqualityStatus(a, b); - } - if (status == EQUALITY_UNKNOWN) { - status = d_bitblastSolver.getEqualityStatus(a, b); + + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b); + if (status != EQUALITY_UNKNOWN) { + return status; + } } - - return status; + return EQUALITY_UNKNOWN; ; } |