From: lianah Date: Thu, 21 Mar 2013 16:38:51 +0000 (-0400) Subject: added regression test for constant eval X-Git-Tag: cvc5-1.0.0~7361^2~29 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=020ce7845a6ba4417616eedd072e3b73df3e8b38;p=cvc5.git added regression test for constant eval --- 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); } diff --git a/test/regress/regress0/bv/core/constant_core.smt2 b/test/regress/regress0/bv/core/constant_core.smt2 new file mode 100644 index 000000000..c7a5a605f --- /dev/null +++ b/test/regress/regress0/bv/core/constant_core.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_BV) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun x () (_ BitVec 3)) +(assert (and +(= ((_ extract 1 0) x) (concat ((_ extract 1 1) x) ((_ extract 0 0) x))) +(= ((_ extract 0 0) x) ((_ extract 1 1) x)) +(= ((_ extract 2 2) x) ((_ extract 1 1) x)) +(= (_ bv0 1) ((_ extract 0 0) x)) +(= x (concat ((_ extract 2 2) x) ((_ extract 1 0) x))) +(not (= (_ bv0 3) x)) +)) +(check-sat) +(exit) \ No newline at end of file