diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-11-12 06:14:49 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-11-12 08:14:49 -0600 |
commit | ad340126a7adbb9840cca1d082c57b43995987a4 (patch) | |
tree | da06599c2691f063b770b2b1ba7e2ccf87f26cc6 /src/expr/node_manager.h | |
parent | 5cfbb67e228daf76835b7fd0a95d214859be030e (diff) |
Remove `ConstantMap<Rational>` (#7635)
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/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 28 |
1 files changed, 20 insertions, 8 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 1208a0e03..d301c857c 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -522,11 +522,17 @@ class NodeManager template <class T> Node mkConst(const T&); + /** + * Create a constant of type `T` with an explicit kind `k`. + */ + template <class T> + Node mkConst(Kind k, const T&); + template <class T> TypeNode mkTypeConst(const T&); template <class NodeClass, class T> - NodeClass mkConstInternal(const T&); + NodeClass mkConstInternal(Kind k, const T&); /** Create a node with children. */ TypeNode mkTypeNode(Kind kind, TypeNode child1); @@ -1187,22 +1193,29 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind, template <class T> Node NodeManager::mkConst(const T& val) { - return mkConstInternal<Node, T>(val); + return mkConstInternal<Node, T>(kind::metakind::ConstantMap<T>::kind, val); +} + +template <class T> +Node NodeManager::mkConst(Kind k, const T& val) +{ + return mkConstInternal<Node, T>(k, val); } template <class T> TypeNode NodeManager::mkTypeConst(const T& val) { - return mkConstInternal<TypeNode, T>(val); + return mkConstInternal<TypeNode, T>(kind::metakind::ConstantMap<T>::kind, + val); } template <class NodeClass, class T> -NodeClass NodeManager::mkConstInternal(const T& val) { - // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t; +NodeClass NodeManager::mkConstInternal(Kind k, const T& val) +{ NVStorage<1> nvStorage; expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage); nvStack.d_id = 0; - nvStack.d_kind = kind::metakind::ConstantMap<T>::kind; + nvStack.d_kind = k; nvStack.d_rc = 0; nvStack.d_nchildren = 1; @@ -1230,11 +1243,10 @@ NodeClass NodeManager::mkConstInternal(const T& val) { } nv->d_nchildren = 0; - nv->d_kind = kind::metakind::ConstantMap<T>::kind; + nv->d_kind = k; nv->d_id = next_id++;// FIXME multithreading nv->d_rc = 0; - //OwningTheory::mkConst(val); new (&nv->d_children) T(val); poolInsert(nv); |