diff options
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 257 |
1 files changed, 83 insertions, 174 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index c977435ec..79c065d7e 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -19,196 +19,82 @@ #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" - #include "theory/valuation.h" +#include "theory/bv/bv_sat.h" + using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; -using namespace CVC4::theory::bv::utils; +using namespace CVC4::context; using namespace std; +using namespace CVC4::theory::bv::utils; -void TheoryBV::preRegisterTerm(TNode node) { +TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) + : Theory(THEORY_BV, c, u, out, valuation), + d_context(c), + d_assertions(c), + d_bitblaster(new Bitblaster(c) ), + d_statistics() + { + d_true = utils::mkTrue(); + } +TheoryBV::~TheoryBV() { + delete d_bitblaster; +} +TheoryBV::Statistics::Statistics(): + d_avgConflictSize("theory::bv::AvgBVConflictSize"), + d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0) +{ + StatisticsRegistry::registerStat(&d_avgConflictSize); + StatisticsRegistry::registerStat(&d_solveSubstitutions); +} - BVDebug("bitvector") << "TheoryBV::preRegister(" << node << ")" << std::endl; +TheoryBV::Statistics::~Statistics() { + StatisticsRegistry::unregisterStat(&d_avgConflictSize); + StatisticsRegistry::unregisterStat(&d_solveSubstitutions); +} - if (node.getKind() == kind::EQUAL) { - d_eqEngine.addTerm(node[0]); - if (node[0].getKind() == kind::BITVECTOR_CONCAT) { - for (unsigned i = 0, i_end = node[0].getNumChildren(); i < i_end; ++ i) { - d_eqEngine.addTerm(node[0][i]); - } - } - d_eqEngine.addTerm(node[1]); - if (node[1].getKind() == kind::BITVECTOR_CONCAT) { - for (unsigned i = 0, i_end = node[1].getNumChildren(); i < i_end; ++ i) { - d_eqEngine.addTerm(node[1][i]); - } - } +void TheoryBV::preRegisterTerm(TNode node) { - d_normalization[node] = new Normalization(d_context, node); - } + BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl; + //marker literal: bitblast all terms before we start + d_bitblaster->bitblast(node); } void TheoryBV::check(Effort e) { - BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; - - // Normalization iterators - NormalizationMap::iterator it = d_normalization.begin(); - NormalizationMap::iterator it_end = d_normalization.end(); - - // Get all the assertions - std::vector<TNode> assertionsList; - while (!done()) { - // Get the assertion - TNode assertion = get(); - d_assertions.insert(assertion); - assertionsList.push_back(assertion); - } - - bool normalizeEqualities = false; - - for (unsigned i = 0; i < assertionsList.size(); ++ i) { - - TNode assertion = assertionsList[i]; - - BVDebug("bitvector") << "TheoryBV::check(" << e << "): asserting: " << assertion << std::endl; - - // Do the right stuff - switch (assertion.getKind()) { - case kind::EQUAL: { - // Slice and solve the equality - bool ok = d_sliceManager.solveEquality(assertion[0], assertion[1]); - if (!ok) return; - // Normalize all equalities - normalizeEqualities = true; - it = d_normalization.begin(); - it = d_normalization.end(); - break; + if (fullEffort(e)) { + std::vector<TNode> assertions; + while (!done()) { + TNode assertion = get(); + Debug("bitvector") << "assertion " << assertion << "\n"; + assertions.push_back(assertion); + d_bitblaster->bitblast(assertion); } - case kind::NOT: { - if (!normalizeEqualities) { - // We still need to check this dis-equality, as it might have been pre-registered just now - // so we didn't have a chance to propagate - it = d_normalization.find(assertion[0]); - if (it->second->assumptions.size() == 1) { - // Just normalize this equality - normalizeEqualities = true; - it_end = it; - it_end ++; - } - } - break; + + std::vector<TNode>::const_iterator it = assertions.begin(); + for (; it != assertions.end(); ++it) { + d_bitblaster->assertToSat(*it); } - default: - Unhandled(assertion.getKind()); - } - } - - if (normalizeEqualities) { + bool res = d_bitblaster->solve(); + if (res == false) { + std::vector<TNode> conflictAtoms; + d_bitblaster->getConflict(conflictAtoms); - BVDebug("bitvector") << "Checking for propagations" << std::endl; - - NormalizationMap::iterator it = d_normalization.begin(); - NormalizationMap::iterator it_end = d_normalization.end(); - for(; it != it_end; ++ it) { - - TNode equality = it->first; - BVDebug("bitvector") << "Checking " << equality << std::endl; - Normalization& normalization = *it->second; + d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size()); - // If asserted, we don't care - if (d_assertions.find(equality) != d_assertions.end()) continue; - - // Assumptions - std::set<TNode> assumptions; - TNode lhs = normalization.equalities.back()[0]; - TNode rhs = normalization.equalities.back()[1]; - // If already satisfied, do nothing - if (lhs == rhs) continue; - - Node lhsNormalized = d_eqEngine.normalize(lhs, assumptions); - Node rhsNormalized = d_eqEngine.normalize(rhs, assumptions); - - if (lhsNormalized == lhs && rhsNormalized == rhs) continue; - - normalization.equalities.push_back(lhsNormalized.eqNode(rhsNormalized)); - normalization.assumptions.push_back(assumptions); - - BVDebug("bitvector") << "Adding normalization " << lhsNormalized.eqNode(rhsNormalized) << std::endl; - BVDebug("bitvector") << " assumptions " << utils::setToString(assumptions) << std::endl; - - - BVDebug("bitvector") << "TheoryBV::check(" << e << "): normalizes to " << lhsNormalized << " = " << rhsNormalized << std::endl; - - // If both are equal we can propagate - bool propagate = lhsNormalized == rhsNormalized; - // otherwise if both are constants, we propagate negation (if not already there) - bool propagateNegation = !propagate && - lhsNormalized.getKind() == kind::CONST_BITVECTOR && rhsNormalized.getKind() == kind::CONST_BITVECTOR - && d_assertions.find(equality.notNode()) == d_assertions.end(); - ; - if (propagate || propagateNegation) { - Node implied = propagate ? Node(equality) : equality.notNode() ; - Node impliedNegated = propagate ? equality.notNode() : Node(equality) ; - // If the negation of what's implied has been asserted, we are in conflict - if (d_assertions.find(impliedNegated) != d_assertions.end()) { - BVDebug("bitvector") << "TheoryBV::check(" << e << "): conflict with " << utils::setToString(assumptions) << std::endl; - // Construct the assumptions - for (unsigned i = 0; i < normalization.assumptions.size(); ++ i) { - assumptions.insert(normalization.assumptions[i].begin(), normalization.assumptions[i].end()); - } - // Make the conflict - assumptions.insert(impliedNegated); - d_out->conflict(mkConjunction(assumptions)); - return; - } - // Otherwise we propagate the implication - else { - BVDebug("bitvector") << "TheoryBV::check(" << e << "): propagating " << implied << std::endl; - d_out->propagate(implied); - d_assertions.insert(implied); - } - } + Node conflict = mkConjunction(conflictAtoms); + d_out->conflict(conflict); + return; } } } -bool TheoryBV::triggerEquality(size_t triggerId) { - BVDebug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << ")" << std::endl; - Assert(triggerId < d_triggers.size()); - BVDebug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << "): " << d_triggers[triggerId] << std::endl; - - return true; - - TNode equality = d_triggers[triggerId]; - - // If we have just asserted this equality ignore it - if (d_assertions.contains(equality)) return true; - - // If we have a negation asserted, we have a confict - if (d_assertions.contains(equality.notNode())) { - - std::vector<TNode> explanation; - d_eqEngine.getExplanation(equality[0], equality[1], explanation); - std::set<TNode> assumptions; - assumptions.insert(equality.notNode()); - utils::getConjuncts(explanation, assumptions); - d_out->conflict(utils::mkConjunction(assumptions)); - - return false; - } - - // Otherwise we propagate this equality - d_out->propagate(equality); - - return true; -} Node TheoryBV::getValue(TNode n) { - NodeManager* nodeManager = NodeManager::currentNM(); + //NodeManager* nodeManager = NodeManager::currentNM(); switch(n.getKind()) { @@ -216,8 +102,7 @@ Node TheoryBV::getValue(TNode n) { Unhandled(kind::VARIABLE); case kind::EQUAL: // 2 args - return nodeManager-> - mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) ); + Unhandled(kind::VARIABLE); default: Unhandled(n.getKind()); @@ -229,13 +114,37 @@ Node TheoryBV::explain(TNode node) { TNode equality = node.getKind() == kind::NOT ? node[0] : node; Assert(equality.getKind() == kind::EQUAL); + Assert(0); + return node; + +} - context::CDList< set<TNode> >& vec = d_normalization[equality]->assumptions; - std::set<TNode> assumptions; - for (unsigned i = 0; i < vec.size(); ++ i) { - BVDebug("bitvector") << "Adding normalization " << d_normalization[equality]->equalities[i] << std::endl; - BVDebug("bitvector") << " assumptions " << utils::setToString(d_normalization[equality]->assumptions[i]) << std::endl; - assumptions.insert(vec[i].begin(), vec[i].end()); +// Node TheoryBV::preprocessTerm(TNode term) { +// return term; //d_staticEqManager.find(term); +// } + +Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { + switch(in.getKind()) { + case kind::EQUAL: + + if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) { + ++(d_statistics.d_solveSubstitutions); + outSubstitutions.addSubstitution(in[0], in[1]); + return PP_ASSERT_STATUS_SOLVED; + } + if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) { + ++(d_statistics.d_solveSubstitutions); + outSubstitutions.addSubstitution(in[1], in[0]); + return PP_ASSERT_STATUS_SOLVED; + } + // to do constant propagations + + break; + case kind::NOT: + break; + default: + // TODO other predicates + break; } - return utils::mkConjunction(assumptions); + return PP_ASSERT_STATUS_UNSOLVED; } |