diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 02:02:06 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 02:02:06 +0000 |
commit | 52d6dc20c61007a5c066590aa1fd0b95ed3c2527 (patch) | |
tree | 040efec36cde7775b5c19eb43fcdd60cbeb61f9e /src/theory/bv/theory_bv.cpp | |
parent | 4fa8c7d1a0654e7780fd485c51463c06b34379b5 (diff) |
* added propagation as lemmas to TheoryBV:
* modified BVMinisat to work incrementally
* added more bv regressions
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 109 |
1 files changed, 83 insertions, 26 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 45d99f9c9..e8e1aead6 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -32,12 +32,13 @@ using namespace std; using namespace CVC4::theory::bv::utils; TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) - : Theory(THEORY_BV, c, u, out, valuation), + : Theory(THEORY_BV, c, u, out, valuation), d_context(c), d_assertions(c), d_bitblaster(new Bitblaster(c) ), - d_statistics() - { + d_statistics(), + d_alreadyPropagatedSet(c) + { d_true = utils::mkTrue(); } TheoryBV::~TheoryBV() { @@ -61,35 +62,54 @@ TheoryBV::Statistics::~Statistics() { void TheoryBV::preRegisterTerm(TNode node) { BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl; - //marker literal: bitblast all terms before we start - //d_bitblaster->bitblast(node); + if (node.getKind() == kind::EQUAL || + node.getKind() == kind::BITVECTOR_ULT || + node.getKind() == kind::BITVECTOR_ULE || + node.getKind() == kind::BITVECTOR_SLT || + node.getKind() == kind::BITVECTOR_SLE) { + d_bitblaster->bitblast(node); + d_bitblaster->addAtom(node); + } } void TheoryBV::check(Effort e) { - if (fullEffort(e) && !done()) { - Trace("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl; - std::vector<TNode> assertions; - + if (e == EFFORT_STANDARD) { + BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; + BVDebug("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl; while (!done()) { TNode assertion = get(); - Trace("bitvector-assertions") << "TheoryBV::check assertion " << assertion << "\n"; - d_bitblaster->bitblast(assertion); - d_bitblaster->assertToSat(assertion); + // make sure we do not assert things we propagated + if (!hasBeenPropagated(assertion)) { + BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << assertion << "\n"; + bool ok = d_bitblaster->assertToSat(assertion, true); + if (!ok) { + std::vector<TNode> conflictAtoms; + d_bitblaster->getConflict(conflictAtoms); + d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size()); + Node conflict = mkConjunction(conflictAtoms); + d_out->conflict(conflict); + BVDebug("bitvector") << "TheoryBV::check returns conflict: " <<conflict <<" \n "; + return; + } + } } + } - TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer); - bool res = d_bitblaster->solve(); - if (res == false) { + if (e == EFFORT_FULL) { + BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; + // in standard effort we only do boolean constraint propagation + bool ok = d_bitblaster->solve(false); + if (!ok) { std::vector<TNode> conflictAtoms; d_bitblaster->getConflict(conflictAtoms); d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size()); - Node conflict = mkConjunction(conflictAtoms); d_out->conflict(conflict); - Trace("bitvector") << "TheoryBV::check returns conflict. \n "; + BVDebug("bitvector") << "TheoryBV::check returns conflict: " <<conflict <<" \n "; return; } } + } @@ -109,19 +129,56 @@ Node TheoryBV::getValue(TNode n) { } } -Node TheoryBV::explain(TNode node) { - BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl; +bool TheoryBV::hasBeenPropagated(TNode node) { + return d_alreadyPropagatedSet.count(node); +} - TNode equality = node.getKind() == kind::NOT ? node[0] : node; - Assert(equality.getKind() == kind::EQUAL); - Assert(0); - return node; +void TheoryBV::propagate(Effort e) { + BVDebug("bitvector") << "TheoryBV::propagate() \n"; + + // get new propagations from the sat solver + std::vector<TNode> propagations; + d_bitblaster->getPropagations(propagations); + + // propagate the facts on the propagation queue + for (unsigned i = 0; i < propagations.size(); ++ i) { + TNode node = propagations[i]; + BVDebug("bitvector") << "TheoryBV::propagate " << node <<" \n"; + if (d_valuation.getSatValue(node) == Node::null()) { + vector<Node> explanation; + d_bitblaster->explainPropagation(node, explanation); + if (explanation.size() == 0) { + d_out->lemma(node); + } else { + NodeBuilder<> nb(kind::OR); + nb << node; + for (unsigned i = 0; i < explanation.size(); ++ i) { + nb << explanation[i].notNode(); + } + Node lemma = nb; + d_out->lemma(lemma); + } + d_alreadyPropagatedSet.insert(node); + } + } } -// Node TheoryBV::preprocessTerm(TNode term) { -// return term; //d_staticEqManager.find(term); -// } +Node TheoryBV::explain(TNode n) { + BVDebug("bitvector") << "TheoryBV::explain node " << n <<"\n"; + std::vector<Node> explanation; + d_bitblaster->explainPropagation(n, explanation); + Node exp; + + if (explanation.size() == 0) { + return utils::mkTrue(); + } + + exp = utils::mkAnd(explanation); + + BVDebug("bitvector") << "TheoryBV::explain with " << exp <<"\n"; + return exp; +} Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { switch(in.getKind()) { |