diff options
Diffstat (limited to 'src/theory/quantifiers/term_util.cpp')
| -rw-r--r-- | src/theory/quantifiers/term_util.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index de4c56552..cb8bad174 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -283,7 +283,7 @@ bool TermUtil::isAssoc(Kind k, bool reqNAry) { if (reqNAry) { - if (k == SET_UNION || k == SET_INTERSECTION) + if (k == SET_UNION || k == SET_INTER) { return false; } @@ -292,7 +292,7 @@ bool TermUtil::isAssoc(Kind k, bool reqNAry) || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR || k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT || k == STRING_CONCAT - || k == SET_UNION || k == SET_INTERSECTION || k == RELATION_JOIN + || k == SET_UNION || k == SET_INTER || k == RELATION_JOIN || k == RELATION_PRODUCT || k == SEP_STAR; } @@ -300,7 +300,7 @@ bool TermUtil::isComm(Kind k, bool reqNAry) { if (reqNAry) { - if (k == SET_UNION || k == SET_INTERSECTION) + if (k == SET_UNION || k == SET_INTER) { return false; } @@ -308,7 +308,7 @@ bool TermUtil::isComm(Kind k, bool reqNAry) return k == EQUAL || k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR - || k == BITVECTOR_XNOR || k == SET_UNION || k == SET_INTERSECTION + || k == BITVECTOR_XNOR || k == SET_UNION || k == SET_INTER || k == SEP_STAR; } @@ -332,7 +332,7 @@ Node TermUtil::mkTypeValue(TypeNode tn, int32_t val) if (tn.isInteger() || tn.isReal()) { Rational c(val); - n = NodeManager::currentNM()->mkConst(c); + n = NodeManager::currentNM()->mkConst(CONST_RATIONAL, c); } else if (tn.isBitVector()) { |