diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-03-20 01:41:48 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-03-20 01:41:48 +0000 |
commit | 3af0d6493cdea4be4130076fee93ebbeff669545 (patch) | |
tree | f704b1aa7e7dc5d8d1d23ec8881e4b0a6553bc3a /src/theory | |
parent | af6ac1f03a841a0261190cb7caa15ff1fa1f798c (diff) |
missed one case
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/equality_engine.h | 10 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 3 |
2 files changed, 12 insertions, 1 deletions
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<OwnerClass, NotifyClass, UnionFindPreferences>::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 { |