From 2bf51317486cfbfc8c19e32256ca9727bfb2e42a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 26 Apr 2021 13:58:53 -0500 Subject: [PATCH] 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. --- src/theory/theory.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) 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 { -- 2.30.2