diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-07-15 08:27:13 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-15 10:27:13 -0500 |
commit | 9975291763425e0aba9ae135ccd86d1fbc176d9d (patch) | |
tree | 9d8c1775df573fed99874dbea08273290c31ab35 /src/expr | |
parent | a482635216017b0d558229f2339c663cf58f8d23 (diff) |
Use TypeNode in UninterpretedConstant (#4748)
This commit changes UninterpretedConstant to use TypeNode instead of
Type.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/uninterpreted_constant.cpp | 50 | ||||
-rw-r--r-- | src/expr/uninterpreted_constant.h | 70 |
2 files changed, 77 insertions, 43 deletions
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp index 2b66a3b7a..c9cbcba20 100644 --- a/src/expr/uninterpreted_constant.cpp +++ b/src/expr/uninterpreted_constant.cpp @@ -22,18 +22,57 @@ #include <string> #include "base/check.h" +#include "expr/type_node.h" using namespace std; namespace CVC4 { -UninterpretedConstant::UninterpretedConstant(Type type, Integer index) - : d_type(type), d_index(index) +UninterpretedConstant::UninterpretedConstant(const TypeNode& type, + Integer index) + : d_type(new TypeNode(type)), d_index(index) { //PrettyCheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str()); PrettyCheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str()); } +UninterpretedConstant::~UninterpretedConstant() {} + +UninterpretedConstant::UninterpretedConstant(const UninterpretedConstant& other) + : d_type(new TypeNode(other.getType())), d_index(other.getIndex()) +{ +} + +const TypeNode& UninterpretedConstant::getType() const { return *d_type; } +const Integer& UninterpretedConstant::getIndex() const { return d_index; } +bool UninterpretedConstant::operator==(const UninterpretedConstant& uc) const +{ + return getType() == uc.getType() && d_index == uc.d_index; +} +bool UninterpretedConstant::operator!=(const UninterpretedConstant& uc) const +{ + return !(*this == uc); +} + +bool UninterpretedConstant::operator<(const UninterpretedConstant& uc) const +{ + return getType() < uc.getType() + || (getType() == uc.getType() && d_index < uc.d_index); +} +bool UninterpretedConstant::operator<=(const UninterpretedConstant& uc) const +{ + return getType() < uc.getType() + || (getType() == uc.getType() && d_index <= uc.d_index); +} +bool UninterpretedConstant::operator>(const UninterpretedConstant& uc) const +{ + return !(*this <= uc); +} +bool UninterpretedConstant::operator>=(const UninterpretedConstant& uc) const +{ + return !(*this < uc); +} + std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) { std::stringstream ss; ss << uc.getType(); @@ -49,4 +88,11 @@ std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) { return out << "uc_" << st.c_str() << "_" << uc.getIndex(); } +size_t UninterpretedConstantHashFunction::operator()( + const UninterpretedConstant& uc) const +{ + return TypeNodeHashFunction()(uc.getType()) + * IntegerHashFunction()(uc.getIndex()); +} + }/* CVC4 namespace */ diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h index 46d9a2800..eb6cc203a 100644 --- a/src/expr/uninterpreted_constant.h +++ b/src/expr/uninterpreted_constant.h @@ -16,62 +16,50 @@ #include "cvc4_public.h" -#pragma once +#ifndef CVC4__UNINTERPRETED_CONSTANT_H +#define CVC4__UNINTERPRETED_CONSTANT_H #include <iosfwd> +#include <memory> -#include "expr/type.h" +#include "util/integer.h" namespace CVC4 { -class CVC4_PUBLIC UninterpretedConstant { +class TypeNode; + +class UninterpretedConstant +{ public: - UninterpretedConstant(Type type, Integer index); + UninterpretedConstant(const TypeNode& type, Integer index); + ~UninterpretedConstant(); - Type getType() const { return d_type; } - const Integer& getIndex() const { return d_index; } - bool operator==(const UninterpretedConstant& uc) const - { - return d_type == uc.d_type && d_index == uc.d_index; - } - bool operator!=(const UninterpretedConstant& uc) const - { - return !(*this == uc); - } + UninterpretedConstant(const UninterpretedConstant& other); - bool operator<(const UninterpretedConstant& uc) const - { - return d_type < uc.d_type || - (d_type == uc.d_type && d_index < uc.d_index); - } - bool operator<=(const UninterpretedConstant& uc) const - { - return d_type < uc.d_type || - (d_type == uc.d_type && d_index <= uc.d_index); - } - bool operator>(const UninterpretedConstant& uc) const - { - return !(*this <= uc); - } - bool operator>=(const UninterpretedConstant& uc) const - { - return !(*this < uc); - } + const TypeNode& getType() const; + const Integer& getIndex() const; + bool operator==(const UninterpretedConstant& uc) const; + bool operator!=(const UninterpretedConstant& uc) const; + bool operator<(const UninterpretedConstant& uc) const; + bool operator<=(const UninterpretedConstant& uc) const; + bool operator>(const UninterpretedConstant& uc) const; + bool operator>=(const UninterpretedConstant& uc) const; private: - const Type d_type; + std::unique_ptr<TypeNode> d_type; const Integer d_index; -};/* class UninterpretedConstant */ +}; /* class UninterpretedConstant */ -std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc); /** * Hash function for the BitVector constants. */ -struct CVC4_PUBLIC UninterpretedConstantHashFunction { - inline size_t operator()(const UninterpretedConstant& uc) const { - return TypeHashFunction()(uc.getType()) * IntegerHashFunction()(uc.getIndex()); - } -};/* struct UninterpretedConstantHashFunction */ +struct CVC4_PUBLIC UninterpretedConstantHashFunction +{ + size_t operator()(const UninterpretedConstant& uc) const; +}; /* struct UninterpretedConstantHashFunction */ + +} // namespace CVC4 -}/* CVC4 namespace */ +#endif /* CVC4__UNINTERPRETED_CONSTANT_H */ |