diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-12-11 16:10:02 -0500 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-12-11 16:10:02 -0500 |
commit | e5c363fe467c0a29df2c36da74a27413103d584a (patch) | |
tree | a66b10598212e54bb5da624f2d9962229a87ed03 /src/theory/bv/theory_bv.cpp | |
parent | 67af0bb961e42ab84c5f82245809ea12e2c12758 (diff) |
fixed some slicer bugs; set up bv theory to run bit-blaster to check for correctness
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index c4e16545f..d537b8e60 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -126,13 +126,24 @@ void TheoryBV::check(Effort e) } // FIXME: this is not quite correct as it does not take into account cardinality constraints - if (!d_coreSolver.isCoreTheory()) { + + if (d_coreSolver.isCoreTheory()) { + // paranoid check to make sure results of bit-blaster agree with slicer for core theory + if (inConflict()) { + d_conflict = false; + d_bitblastSolver.addAssertions(new_assertions, Theory::EFFORT_FULL); + Assert (inConflict()); + } else { + d_bitblastSolver.addAssertions(new_assertions, Theory::EFFORT_FULL); + Assert (!inConflict()); + } + } + else { if (!inConflict()) { // sending assertions to the bitblast solver d_bitblastSolver.addAssertions(new_assertions, e); } - } - + } if (inConflict()) { sendConflict(); } @@ -252,7 +263,7 @@ 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 << "): EQUALITY" << std::endl; + Debug("bitvector::explain") << "TheoryBV::explain(" << literal << "): CORE" << std::endl; d_coreSolver.explain(literal, assumptions); } else { Assert(propagatedBy(literal, SUB_BITBLAST)); |