From 34eac85599875517732d53a5cc1acd3ab60479d1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 25 Aug 2020 19:04:39 -0500 Subject: Replace Expr-level datatype with Node-level DType (#4875) This PR makes two simultaneous changes: The new API uses Node-level DType instead of Expr-level Datatype. This required converting 2 of the last remaining calls in the parser that used Expr to use the new API. Internally constructed datatypes (e.g. for sygus) use Node-level DType instead of Expr-level Datatype. Note this required moving a block of code for handling a corner case of sygus from Datatype -> DType. This PR removes : ExprManger::mkDatatypeType. The Expr-level datatype itself. This PR removes all references to its include file. It also updates one remaining unit test from Expr -> Node. This PR will enable further removal of other datatype-specific things in the Expr layer. --- src/expr/CMakeLists.txt | 2 -- 1 file changed, 2 deletions(-) (limited to 'src/expr/CMakeLists.txt') diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 0092b78c6..8bc732314 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -73,8 +73,6 @@ libcvc4_add_sources( type_node.cpp type_node.h variable_type_map.h - datatype.h - datatype.cpp datatype_index.h datatype_index.cpp dtype.h -- cgit v1.2.3