diff options
Diffstat (limited to 'src/theory/sets/rels_utils.h')
| -rw-r--r-- | src/theory/sets/rels_utils.h | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h index 8ce314c94..79757d311 100644 --- a/src/theory/sets/rels_utils.h +++ b/src/theory/sets/rels_utils.h @@ -17,6 +17,9 @@ #ifndef SRC_THEORY_SETS_RELS_UTILS_H_ #define SRC_THEORY_SETS_RELS_UTILS_H_ +#include "expr/dtype.h" +#include "expr/node.h" + namespace CVC4 { namespace theory { namespace sets { @@ -67,8 +70,9 @@ public: return tuple[n_th]; } TypeNode tn = tuple.getType(); - const Datatype& dt = tn.getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal( tn.toType(), n_th ), tuple); + const DType& dt = tn.getDType(); + return NodeManager::currentNM()->mkNode( + kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, n_th), tuple); } static Node reverseTuple( Node tuple ) { @@ -77,16 +81,17 @@ public: std::vector<TypeNode> tuple_types = tuple.getType().getTupleTypes(); std::reverse( tuple_types.begin(), tuple_types.end() ); TypeNode tn = NodeManager::currentNM()->mkTupleType( tuple_types ); - const Datatype& dt = tn.getDatatype(); - elements.push_back( Node::fromExpr(dt[0].getConstructor() ) ); + const DType& dt = tn.getDType(); + elements.push_back(dt[0].getConstructor()); for(int i = tuple_types.size() - 1; i >= 0; --i) { elements.push_back( nthElementOfTuple(tuple, i) ); } return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, elements ); } static Node constructPair(Node rel, Node a, Node b) { - const Datatype& dt = rel.getType().getSetElementType().getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), a, b); + const DType& dt = rel.getType().getSetElementType().getDType(); + return NodeManager::currentNM()->mkNode( + kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), a, b); } }; |