diff options
author | lianah <lianahady@gmail.com> | 2013-03-21 12:38:51 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-21 12:38:51 -0400 |
commit | 020ce7845a6ba4417616eedd072e3b73df3e8b38 (patch) | |
tree | 42e925680f64095bc848c809c2ec91f88b9521a1 /src | |
parent | 80697ed7280ac2462ec05e29754a0a563f19de44 (diff) |
added regression test for constant eval
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 7 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 10 |
2 files changed, 8 insertions, 9 deletions
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 01378da56..85ae64d05 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -123,7 +123,7 @@ bool CoreSolver::decomposeFact(TNode fact) { Node new_b = getBaseDecomposition(b, explanation); explanation.push_back(fact); - TNode reason = utils::mkAnd(explanation); + Node reason = utils::mkAnd(explanation); Assert (utils::getSize(new_a) == utils::getSize(new_b) && utils::getSize(new_a) == utils::getSize(a)); @@ -197,11 +197,10 @@ bool CoreSolver::check(Theory::Effort e) { } bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) { - Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl; - Debug("bv-slicer-eq") << " reason=" << reason << endl; // Notify the equality engine if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_CORE) ) { - Trace("bitvector::core") << " (assert " << fact << ")\n"; + Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl; + // Debug("bv-slicer-eq") << " reason=" << reason << endl; bool negated = fact.getKind() == kind::NOT; TNode predicate = negated ? fact[0] : fact; if (predicate.getKind() == kind::EQUAL) { diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 135b944ad..2d390b7b9 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -122,13 +122,13 @@ void TheoryBV::check(Effort e) } Assert (!ok == inConflict()); - if (!inConflict() && !d_coreSolver.isCoreTheory()) { - ok = d_inequalitySolver.check(e); - } + // if (!inConflict() && !d_coreSolver.isCoreTheory()) { + // ok = d_inequalitySolver.check(e); + // } Assert (!ok == inConflict()); - // if (!inConflict() && !d_coreSolver.isCoreTheory()) { - if (!inConflict() && !d_inequalitySolver.isInequalityTheory()) { + if (!inConflict() && !d_coreSolver.isCoreTheory()) { + //if (!inConflict() && !d_inequalitySolver.isInequalityTheory()) { ok = d_bitblastSolver.check(e); } |