diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-11-11 16:03:12 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2021-11-11 19:19:10 -0800 |
| commit | 01cc6aab4031f633bdf6cb41a0a8aa6345bb24eb (patch) | |
| tree | 55c33c54d8f3be5f5b4835be6b48d13d63f0c079 /src/theory/quantifiers/extended_rewrite.cpp | |
| parent | f826638031ae919a03bd48c2003eed82cea7279a (diff) | |
Remove `ConstantMap<Rational>`
This is in preparation of having two different kinds (`CONST_RATIONAL`
and `CONST_INT`) share the same payload. To do so, we cannot rely on
`ConstantMap<Rational>` anymore to map the payload type to a kind. This
commit extends support in the `mkmetakind` script to deal with such
payloads by adding a `+` suffix to the type. The commit also does some
minor refactoring of `NodeManager::mkConst()` and
`NodeManager::mkConstInternal()` to support setting the kind explicitly.
Finally, the commit addresses all instances where `mkConst<Rational>()`
is used, including the API.
Diffstat (limited to 'src/theory/quantifiers/extended_rewrite.cpp')
| -rw-r--r-- | src/theory/quantifiers/extended_rewrite.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 3d20f66b3..5aab618c0 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -49,7 +49,7 @@ ExtendedRewriter::ExtendedRewriter(Rewriter& rew, bool aggr) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); - d_zero = NodeManager::currentNM()->mkConst(Rational(0)); + d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); } void ExtendedRewriter::setCache(Node n, Node ret) const |