diff options
Diffstat (limited to 'src')
| -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 { |