diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-07 19:25:27 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-07 19:25:27 -0500 |
commit | 8e5aba973b06fb581221a82aacdf7d3ca7938a22 (patch) | |
tree | ea5db058d5991ec44ca1f0c47054c3f0d733f367 /src/expr | |
parent | 080f0de4379c4e1fe5a016e40c7852a3abb52760 (diff) |
Add support for datatype update (#6449)
This removes the special case of TUPLE_UPDATE and RECORD_UPDATE in favor of the more general datatype update.
Datatype update is handled analogously to APPLY_SELECTOR / APPLY_TESTER.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/expr/dtype.cpp | 4 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 2 | ||||
-rw-r--r-- | src/expr/node_manager.h | 2 | ||||
-rw-r--r-- | src/expr/record.cpp | 27 | ||||
-rw-r--r-- | src/expr/record.h | 60 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 7 | ||||
-rw-r--r-- | src/expr/type_node.h | 2 |
8 files changed, 8 insertions, 98 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 28cf23f57..9bf63dcfc 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -112,8 +112,6 @@ libcvc5_add_sources( dtype_cons.cpp dtype_selector.h dtype_selector.cpp - record.cpp - record.h sequence.cpp sequence.h subs.cpp diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 07b8aa5f1..c1893d3f4 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -109,7 +109,7 @@ const DType& DType::datatypeOf(Node item) size_t DType::indexOf(Node item) { Assert(item.getType().isConstructor() || item.getType().isTester() - || item.getType().isSelector()); + || item.getType().isSelector() || item.getType().isUpdater()); return indexOfInternal(item); } @@ -125,7 +125,7 @@ size_t DType::indexOfInternal(Node item) size_t DType::cindexOf(Node item) { - Assert(item.getType().isSelector()); + Assert(item.getType().isSelector() || item.getType().isUpdater()); return cindexOfInternal(item); } size_t DType::cindexOfInternal(Node item) diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 0a0781819..780fda9ab 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -724,7 +724,7 @@ TypeNode NodeManager::mkDatatypeUpdateType(TypeNode domain, TypeNode range) domain.isDatatype(), domain, "cannot create non-datatype upater type"); // It is a function type domain x range -> domain, we store only the // arguments - return mkTypeNode(kind::DT_UPDATE_TYPE, domain, range); + return mkTypeNode(kind::UPDATER_TYPE, domain, range); } TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 8b99f5743..9952baf89 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -34,6 +34,8 @@ namespace cvc5 { +using Record = std::vector<std::pair<std::string, TypeNode>>; + namespace api { class Solver; } diff --git a/src/expr/record.cpp b/src/expr/record.cpp deleted file mode 100644 index 0792de20c..000000000 --- a/src/expr/record.cpp +++ /dev/null @@ -1,27 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * A class representing a record definition. - */ - -#include "expr/record.h" - -#include "base/check.h" -#include "base/output.h" - -namespace cvc5 { - -std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) { - return out << "[" << t.getField() << "]"; -} - -} // namespace cvc5 diff --git a/src/expr/record.h b/src/expr/record.h deleted file mode 100644 index ecf6c8d32..000000000 --- a/src/expr/record.h +++ /dev/null @@ -1,60 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Tim King, Mathias Preiner, Morgan Deters - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * A class representing a Record definition. - */ - -#include "cvc5_public.h" - -#ifndef CVC5__RECORD_H -#define CVC5__RECORD_H - -#include <iostream> -#include <string> -#include <vector> -#include <utility> - -// Forward Declarations -namespace cvc5 { -// This forward delcartion is required to resolve a cicular dependency with -// Record which is a referenced in a Kind file. -class TypeNode; -} // namespace cvc5 - -namespace cvc5 { - -// operators for record update -class RecordUpdate -{ - std::string d_field; - - public: - RecordUpdate(const std::string& field) : d_field(field) {} - std::string getField() const { return d_field; } - bool operator==(const RecordUpdate& t) const { return d_field == t.d_field; } - bool operator!=(const RecordUpdate& t) const { return d_field != t.d_field; } -}; /* class RecordUpdate */ - -struct RecordUpdateHashFunction -{ - inline size_t operator()(const RecordUpdate& t) const { - return std::hash<std::string>()(t.getField()); - } -}; /* struct RecordUpdateHashFunction */ - -std::ostream& operator<<(std::ostream& out, const RecordUpdate& t); - -using Record = std::vector<std::pair<std::string, TypeNode>>; - -} // namespace cvc5 - -#endif /* CVC5__RECORD_H */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 483983e6e..bd435a392 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -249,7 +249,7 @@ bool TypeNode::isClosedEnumerable() bool TypeNode::isFirstClass() const { return getKind() != kind::CONSTRUCTOR_TYPE && getKind() != kind::SELECTOR_TYPE - && getKind() != kind::TESTER_TYPE && getKind() != kind::DT_UPDATE_TYPE + && getKind() != kind::TESTER_TYPE && getKind() != kind::UPDATER_TYPE && (getKind() != kind::TYPE_CONSTANT || (getConst<TypeConstant>() != REGEXP_TYPE && getConst<TypeConstant>() != SEXPR_TYPE)); @@ -633,10 +633,7 @@ bool TypeNode::isSelector() const { return getKind() == kind::SELECTOR_TYPE; } bool TypeNode::isTester() const { return getKind() == kind::TESTER_TYPE; } -bool TypeNode::isDatatypeUpdater() const -{ - return getKind() == kind::DT_UPDATE_TYPE; -} +bool TypeNode::isUpdater() const { return getKind() == kind::UPDATER_TYPE; } bool TypeNode::isCodatatype() const { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index d73d64b43..0ab1d0217 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -652,7 +652,7 @@ public: bool isTester() const; /** Is this a datatype updater type */ - bool isDatatypeUpdater() const; + bool isUpdater() const; /** Get the internal Datatype specification from a datatype type */ const DType& getDType() const; |