diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-17 13:07:14 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-17 19:07:14 +0000 |
| commit | d43b252d1c4588c1662811bfe7d7352823aae447 (patch) | |
| tree | 06a9cac3300ef686e944fbef1520e4c372823bc6 /src/theory/quantifiers/term_util.cpp | |
| parent | b203bed15b9b907ea23422417fb0aa4773830483 (diff) | |
Preparations for eliminating arithmetic subtyping (#7637)
Adds TypeNode::isArithmetic, NodeManager::mkConstReal and NodeManager::mkConstInt.
The first method (for now) is equivalent to TypeNode::isReal, and the latter 2 are equivalent to NodeManager::mkConst(CONST_RATIONAL, ...).
This furthermore distinguishes all uses of isReal: all that intend to be isArithmetic are changed in this PR. Redundant uses of isReal() || isInteger() are merged to isArithmetic().
Due to the above, there are no behavior changes in this PR.
Diffstat (limited to 'src/theory/quantifiers/term_util.cpp')
| -rw-r--r-- | src/theory/quantifiers/term_util.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index cb8bad174..beb02c1c5 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -329,7 +329,7 @@ bool TermUtil::isBoolConnectiveTerm( TNode n ) { Node TermUtil::mkTypeValue(TypeNode tn, int32_t val) { Node n; - if (tn.isInteger() || tn.isReal()) + if (tn.isRealOrInt()) { Rational c(val); n = NodeManager::currentNM()->mkConst(CONST_RATIONAL, c); @@ -382,7 +382,7 @@ Node TermUtil::mkTypeValueOffset(TypeNode tn, status = -1; if (!offset_val.isNull()) { - if (tn.isInteger() || tn.isReal()) + if (tn.isRealOrInt()) { val_o = Rewriter::rewrite( NodeManager::currentNM()->mkNode(PLUS, val, offset_val)); @@ -557,7 +557,7 @@ Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg) } else { - if (n.getType().isReal() && n.getConst<Rational>().sgn() < 0) + if (n.getType().isInteger() && n.getConst<Rational>().sgn() < 0) { // negative arguments if (ik == STRING_SUBSTR || ik == STRING_CHARAT) |