diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-26 13:58:53 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-26 13:58:53 -0500 |
| commit | 2bf51317486cfbfc8c19e32256ca9727bfb2e42a (patch) | |
| tree | a05f035ff50ec261eaf4ae890af8a246c550e386 /src | |
| parent | 7e85adc022bc10e2a2b95bd42e216ddddd51e03e (diff) | |
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.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/theory.cpp | 7 |
1 files 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 { |