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 | |
parent | a482635216017b0d558229f2339c663cf58f8d23 (diff) |
Use TypeNode in UninterpretedConstant (#4748)
This commit changes UninterpretedConstant to use TypeNode instead of
Type.
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 2 | ||||
-rw-r--r-- | src/expr/uninterpreted_constant.cpp | 50 | ||||
-rw-r--r-- | src/expr/uninterpreted_constant.h | 70 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 2 | ||||
-rw-r--r-- | src/theory/builtin/type_enumerator.h | 3 | ||||
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.cpp | 2 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 3 | ||||
-rw-r--r-- | src/theory/datatypes/type_enumerator.cpp | 2 | ||||
-rw-r--r-- | src/theory/rewriter.cpp | 3 |
9 files changed, 87 insertions, 50 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index fcf0c028e..c4ba701b9 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3596,7 +3596,7 @@ Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const CVC4_API_SOLVER_CHECK_SORT(sort); return mkValHelper<CVC4::UninterpretedConstant>( - CVC4::UninterpretedConstant(*sort.d_type, index)); + CVC4::UninterpretedConstant(TypeNode::fromType(*sort.d_type), index)); CVC4_API_SOLVER_TRY_CATCH_END; } 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 */ diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 3a6b9bfff..29ac4f2d1 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -96,7 +96,7 @@ class SExprTypeRule { class UninterpretedConstantTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - return TypeNode::fromType(n.getConst<UninterpretedConstant>().getType()); + return n.getConst<UninterpretedConstant>().getType(); } };/* class UninterpretedConstantTypeRule */ diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h index edac15d86..18dcf4521 100644 --- a/src/theory/builtin/type_enumerator.h +++ b/src/theory/builtin/type_enumerator.h @@ -60,7 +60,8 @@ class UninterpretedSortEnumerator : public TypeEnumeratorBase<UninterpretedSortE if(isFinished()) { throw NoMoreValuesException(getType()); } - return NodeManager::currentNM()->mkConst(UninterpretedConstant(getType().toType(), d_count)); + return NodeManager::currentNM()->mkConst( + UninterpretedConstant(getType(), d_count)); } UninterpretedSortEnumerator& operator++() override diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 699e26d21..450a0fd37 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -720,7 +720,7 @@ Node DatatypesRewriter::normalizeCodatatypeConstantEqc( { int debruijn = depth - it->second - 1; return NodeManager::currentNM()->mkConst( - UninterpretedConstant(n.getType().toType(), debruijn)); + UninterpretedConstant(n.getType(), debruijn)); } std::vector<Node> children; bool childChanged = false; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index d6cb3b37e..505d08c38 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1642,7 +1642,8 @@ Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_c std::map< Node, int >::iterator itv = vmap.find( n ); if( itv!=vmap.end() ){ int debruijn = depth - 1 - itv->second; - return NodeManager::currentNM()->mkConst(UninterpretedConstant(n.getType().toType(), debruijn)); + return NodeManager::currentNM()->mkConst( + UninterpretedConstant(n.getType(), debruijn)); }else if( n.getType().isDatatype() ){ Node nc = eqc_cons[n]; if( !nc.isNull() ){ diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index ccaba009d..3dca74b19 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -107,7 +107,7 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ if (d_child_enum) { ret = NodeManager::currentNM()->mkConst( - UninterpretedConstant(d_type.toType(), d_size_limit)); + UninterpretedConstant(d_type, d_size_limit)); } else { diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index d77f6fe83..f2e13d1e0 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -333,7 +333,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, #ifdef CVC4_ASSERTIONS RewriteResponse r2 = d_theoryRewriters[newTheoryId]->postRewrite(response.d_node); - Assert(r2.d_node == response.d_node); + Assert(r2.d_node == response.d_node) + << r2.d_node << " != " << response.d_node; #endif rewriteStackTop.d_node = response.d_node; break; |