diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-04-06 19:01:25 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-04-06 19:01:25 +0000 |
commit | bc63c26f48851a79d21139f32f2c57daeb47f49d (patch) | |
tree | 2ea7c3c7d51cda62f153f4371440984b789479c6 /src/theory/bv | |
parent | f42542012fa0e59bdcca2b3f4c39b1a575d62140 (diff) |
processing assertions in bit-vectors even when in fullcheck (needed for sharing)
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 34 |
1 files changed, 16 insertions, 18 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index e8e1aead6..429e5ff19 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -73,24 +73,22 @@ void TheoryBV::preRegisterTerm(TNode node) { } void TheoryBV::check(Effort e) { - if (e == EFFORT_STANDARD) { - BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; - BVDebug("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl; - while (!done()) { - TNode assertion = get(); - // 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; - } + BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; + BVDebug("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl; + while (!done()) { + TNode assertion = get(); + // 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; } } } |