From 3af0d6493cdea4be4130076fee93ebbeff669545 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Sun, 20 Mar 2011 01:41:48 +0000 Subject: [PATCH] missed one case --- src/theory/bv/equality_engine.h | 10 +++++++++- src/theory/bv/theory_bv.h | 3 +++ test/regress/regress0/bv/core/Makefile.am | 1 + test/regress/regress0/bv/core/equality-05.cvc | 6 ++++++ test/regress/regress0/bv/core/equality-05.smt | 11 +++++++++++ test/regress/regress0/bv/core/slice-20.smt | 16 ++++++++++++++++ 6 files changed, 46 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/bv/core/equality-05.cvc create mode 100644 test/regress/regress0/bv/core/equality-05.smt create mode 100644 test/regress/regress0/bv/core/slice-20.smt diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h index 53c44bed0..954253269 100644 --- a/src/theory/bv/equality_engine.h +++ b/src/theory/bv/equality_engine.h @@ -321,7 +321,8 @@ public: inline bool hasTerm(TNode t) const; /** - * Adds an equality t1 = t2 to the database. Returns false if any of the triggers failed. + * Adds an equality t1 = t2 to the database. Returns false if any of the triggers failed, or a + * conflict was introduced. */ bool addEquality(TNode t1, TNode t2, Node reason); @@ -437,6 +438,13 @@ bool EqualityEngine::addEquality( // If already the same, we're done if (t1classId == t2classId) return true; + // Check for constants + if (d_nodes[t1classId].getMetaKind() == kind::metakind::CONSTANT && + d_nodes[t2classId].getMetaKind() == kind::metakind::CONSTANT) { + d_notify.conflict(reason); + return false; + } + // Get the nodes of the representatives EqualityNode& node1 = getEqualityNode(t1classId); EqualityNode& node2 = getEqualityNode(t2classId); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index fa9762cb7..8eaa332eb 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -44,6 +44,9 @@ public: bool operator () (size_t triggerId) { return d_theoryBV.triggerEquality(triggerId); } + void conflict(Node explanation) { + d_theoryBV.d_out->conflict(explanation); + } }; struct BVEqualitySettings { diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am index 947dc65ad..0e559f6f2 100644 --- a/test/regress/regress0/bv/core/Makefile.am +++ b/test/regress/regress0/bv/core/Makefile.am @@ -41,6 +41,7 @@ TESTS = \ equality-00.smt \ equality-01.smt \ equality-02.smt \ + equality-05.smt \ bv_eq_diamond10.smt \ slice-01.smt \ slice-02.smt \ diff --git a/test/regress/regress0/bv/core/equality-05.cvc b/test/regress/regress0/bv/core/equality-05.cvc new file mode 100644 index 000000000..93bef502d --- /dev/null +++ b/test/regress/regress0/bv/core/equality-05.cvc @@ -0,0 +1,6 @@ +x,y:BITVECTOR(1); +ASSERT(x = 0bin0); +ASSERT(y = 0bin1); +ASSERT(x = y); +CHECKSAT; + diff --git a/test/regress/regress0/bv/core/equality-05.smt b/test/regress/regress0/bv/core/equality-05.smt new file mode 100644 index 000000000..a7b9f6185 --- /dev/null +++ b/test/regress/regress0/bv/core/equality-05.smt @@ -0,0 +1,11 @@ +(benchmark equality + :status unsat + :logic QF_BV + :extrafuns ((x BitVec[1])) + :extrafuns ((y BitVec[1])) + :assumption (= x bv0[1]) + :assumption (= y bv1[1]) + :assumption (= x y) + :formula +true +) diff --git a/test/regress/regress0/bv/core/slice-20.smt b/test/regress/regress0/bv/core/slice-20.smt new file mode 100644 index 000000000..66fac573b --- /dev/null +++ b/test/regress/regress0/bv/core/slice-20.smt @@ -0,0 +1,16 @@ +(benchmark slice + :status unsat + :logic QF_BV + :extrafuns ((x1 BitVec[4])) + :extrafuns ((y1 BitVec[4])) + :extrafuns ((x2 BitVec[2])) + :extrafuns ((y2 BitVec[2])) + :extrafuns ((x3 BitVec[1])) + :extrafuns ((y3 BitVec[1])) + :assumption (= x1 y1) + :assumption (= x1 (concat x2 x2)) + :assumption (= x2 (concat x3 x3)) + :assumption (= y1 (concat y2 y2)) + :assumption (= y2 (concat y3 y3)) + :formula (not (= x3 y3)) +) -- 2.30.2