diff options
author | lianah <lianahady@gmail.com> | 2013-01-14 21:13:10 -0500 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-01-14 21:13:10 -0500 |
commit | 990073166e45c76bad5119d77a9c964ae2deee1f (patch) | |
tree | 90b2b640dbd4c2919448db1d174d4e9c3603c9b1 /src | |
parent | f8c88fa4b7b9b2d59f48d0e33f1344196a06f5da (diff) |
fixed more minor bugs
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/bv/slicer.cpp | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 17 |
2 files changed, 6 insertions, 17 deletions
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index 1dbb48eed..e67c0b827 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -354,7 +354,7 @@ void Slicer::registerSimpleEquality(TNode eq) { Splinter* s = new Splinter(low -1 , 0); slice->addSplinter(0, s); } - if (high + granularity < size) { + if (high != size - 1) { Splinter* s = new Splinter(size - 1, high + 1); slice->addSplinter(high+1, s); } @@ -427,7 +427,9 @@ bool Slicer::isCoreTerm(TNode node) { Kind kind = node.getKind(); if (kind != kind::BITVECTOR_EXTRACT && kind != kind::BITVECTOR_CONCAT && - kind != kind::EQUAL && kind != kind::NOT) { + kind != kind::EQUAL && kind != kind::NOT && + node.getMetaKind() != kind::metakind::VARIABLE && + kind != kind::CONST_BITVECTOR) { d_coreTermCache[node] = false; return false; } else { diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 5af5b2d23..1c746fafa 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -125,23 +125,10 @@ void TheoryBV::check(Effort e) d_coreSolver.addAssertions(new_assertions, e); } - // FIXME: this is not quite correct as it does not take into account cardinality constraints - - //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() && !d_coreSolver.isCoreTheory()) { // sending assertions to the bitblast solver if it's not just core theory + Assert (false); + std::cout << "Using bitblaster \n"; d_bitblastSolver.addAssertions(new_assertions, e); } |