diff options
Diffstat (limited to 'src/expr/uninterpreted_constant.cpp')
-rw-r--r-- | src/expr/uninterpreted_constant.cpp | 50 |
1 files changed, 48 insertions, 2 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 */ |