From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 26 Apr 2021 18:58:53 +0000 (-0500)
Subject: Fix theoryOf for Boolean equalities (#6444)
X-Git-Tag: cvc5-1.0.0~1830
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2bf51317486cfbfc8c19e32256ca9727bfb2e42a;p=cvc5.git

Fix theoryOf for Boolean equalities (#6444)

Required for fixing a bug in CNF stream's ensureLiteral, which was crashing when combined with unsat-cores-mode=assumptions.

With this PR, we assign a formula like (= (= x y) (= z w)) to have theoryOf THEORY_BOOL. Previously, it mistaken was assigned THEORY_UF if e.g. x,y z, w were terms whose type was an uninterpreted sort.

We should retest unsat-cores-mode=assumptions after this PR is merged.
---

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 859356341..5d2128c54 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -214,9 +214,12 @@ TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
           TNode r = node[1];
           TypeNode ltype = l.getType();
           TypeNode rtype = r.getType();
-          if (ltype != rtype)
+          // If the types are different, we must assign based on type due
+          // to handling subtypes (limited to arithmetic). Also, if we are
+          // a Boolean equality, we must assign THEORY_BOOL.
+          if (ltype != rtype || ltype.isBoolean())
           {
-            tid = Theory::theoryOf(l.getType());
+            tid = Theory::theoryOf(ltype);
           }
           else
           {