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/util | |
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/util')
-rw-r--r-- | src/util/CMakeLists.txt | 1 | ||||
-rw-r--r-- | src/util/tuple.h | 53 |
2 files changed, 0 insertions, 54 deletions
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 79a44f426..5fd0003bf 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -77,7 +77,6 @@ libcvc5_add_sources( statistics_value.h string.cpp string.h - tuple.h unsafe_interrupt_exception.h utility.cpp utility.h diff --git a/src/util/tuple.h b/src/util/tuple.h deleted file mode 100644 index 733ecf189..000000000 --- a/src/util/tuple.h +++ /dev/null @@ -1,53 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Mathias Preiner, 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. - * **************************************************************************** - * - * Tuple operators. - */ - -#include "cvc5_public.h" - -#ifndef CVC5__TUPLE_H -#define CVC5__TUPLE_H - -#include <iostream> -#include <vector> -#include <utility> - -namespace cvc5 { - -class TupleUpdate -{ - unsigned d_index; - - public: - TupleUpdate(unsigned index) : d_index(index) {} - unsigned getIndex() const { return d_index; } - bool operator==(const TupleUpdate& t) const { return d_index == t.d_index; } - bool operator!=(const TupleUpdate& t) const { return d_index != t.d_index; } -}; /* class TupleUpdate */ - -struct TupleUpdateHashFunction -{ - inline size_t operator()(const TupleUpdate& t) const { - return t.getIndex(); - } -}; /* struct TupleUpdateHashFunction */ - -std::ostream& operator<<(std::ostream& out, const TupleUpdate& t); - -inline std::ostream& operator<<(std::ostream& out, const TupleUpdate& t) { - return out << "[" << t.getIndex() << "]"; -} - -} // namespace cvc5 - -#endif /* CVC5__TUPLE_H */ |