From: Andrew Reynolds Date: Wed, 11 Oct 2017 02:07:14 +0000 (-0500) Subject: Ho node manager types (#1203) X-Git-Tag: cvc5-1.0.0~5567 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5e2c7c3a25d334c0068b423225f8ff7793260069;p=cvc5.git Ho node manager types (#1203) * Remove restrictions about function types * Introduce notion of first-class type, improve assertions, add comment on equality type rule. * Update comment --- diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index d5d296579..0b1773114 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1075,10 +1075,12 @@ NodeManager::mkFunctionType(const std::vector& sorts) { Assert(sorts.size() >= 2); std::vector sortNodes; for (unsigned i = 0; i < sorts.size(); ++ i) { - CheckArgument(!sorts[i].isFunctionLike(), sorts, - "cannot create higher-order function types"); + CheckArgument(sorts[i].isFirstClass(), sorts, + "cannot create function types for argument types that are not first-class"); sortNodes.push_back(sorts[i]); } + CheckArgument(!sorts[sorts.size()-1].isFunction(), sorts[sorts.size()-1], + "must flatten function types"); return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); } @@ -1087,8 +1089,8 @@ NodeManager::mkPredicateType(const std::vector& sorts) { Assert(sorts.size() >= 1); std::vector sortNodes; for (unsigned i = 0; i < sorts.size(); ++ i) { - CheckArgument(!sorts[i].isFunctionLike(), sorts, - "cannot create higher-order function types"); + CheckArgument(sorts[i].isFirstClass(), sorts, + "cannot create predicate types for argument types that are not first-class"); sortNodes.push_back(sorts[i]); } sortNodes.push_back(booleanType()); @@ -1121,10 +1123,10 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType, "unexpected NULL index type"); CheckArgument(!constituentType.isNull(), constituentType, "unexpected NULL constituent type"); - CheckArgument(!indexType.isFunctionLike(), indexType, - "cannot index arrays by a function-like type"); - CheckArgument(!constituentType.isFunctionLike(), constituentType, - "cannot store function-like types in arrays"); + CheckArgument(indexType.isFirstClass(), indexType, + "cannot index arrays by types that are not first-class"); + CheckArgument(constituentType.isFirstClass(), constituentType, + "cannot store types that are not first-class in arrays"); Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl; return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); @@ -1133,24 +1135,23 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType, inline TypeNode NodeManager::mkSetType(TypeNode elementType) { CheckArgument(!elementType.isNull(), elementType, "unexpected NULL element type"); - // TODO: Confirm meaning of isFunctionLike(). --K - CheckArgument(!elementType.isFunctionLike(), elementType, - "cannot store function-like types in sets"); + CheckArgument(elementType.isFirstClass(), elementType, + "cannot store types that are not first-class in sets"); Debug("sets") << "making sets type " << elementType << std::endl; return mkTypeNode(kind::SET_TYPE, elementType); } inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) { - CheckArgument(!domain.isFunctionLike(), domain, - "cannot create higher-order function types"); - CheckArgument(!range.isFunctionLike(), range, - "cannot create higher-order function types"); + CheckArgument(domain.isDatatype(), domain, + "cannot create non-datatype selector type"); + CheckArgument(range.isFirstClass(), range, + "cannot have selector fields that are not first-class types"); return mkTypeNode(kind::SELECTOR_TYPE, domain, range); } inline TypeNode NodeManager::mkTesterType(TypeNode domain) { - CheckArgument(!domain.isFunctionLike(), domain, - "cannot create higher-order function types"); + CheckArgument(domain.isDatatype(), domain, + "cannot create non-datatype tester"); return mkTypeNode(kind::TESTER_TYPE, domain ); } diff --git a/src/expr/type.h b/src/expr/type.h index dfab42dad..f52658a03 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -59,9 +59,6 @@ class FunctionType; class SExprType; class SortType; class SortConstructorType; -// not in release 1.0 -//class PredicateSubtype; -class SubrangeType; class Type; /** Hash function for Types */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index c06691d08..8001ca3df 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -22,6 +22,7 @@ #include "options/base_options.h" #include "options/expr_options.h" #include "options/quantifiers_options.h" +#include "options/uf_options.h" using namespace std; @@ -86,6 +87,16 @@ bool TypeNode::isInterpretedFinite() const { } } +bool TypeNode::isFirstClass() const { + return ( getKind() != kind::FUNCTION_TYPE || options::ufHo() ) && + getKind() != kind::CONSTRUCTOR_TYPE && + getKind() != kind::SELECTOR_TYPE && + getKind() != kind::TESTER_TYPE && + getKind() != kind::SEXPR_TYPE && + ( getKind() != kind::TYPE_CONSTANT || + getConst() != REGEXP_TYPE ); +} + bool TypeNode::isWellFounded() const { return kind::isWellFounded(*this); } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 65b422a53..72d00a5a2 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -429,6 +429,18 @@ public: */ bool isInterpretedFinite() const; + + /** + * Is this a first-class type? + * First-class types are types for which: + * (1) we handle equalities between terms of that type, and + * (2) they are allowed to be parameters of parametric types (e.g. index or element types of arrays). + * + * Examples of types that are not first-class include constructor types, + * selector types, tester types, regular expressions and SExprs. + */ + bool isFirstClass() const; + /** * Returns whether this type is well-founded. * diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 370e5d348..777f6e57f 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -77,10 +77,7 @@ class EqualityTypeRule { if( check ) { TypeNode lhsType = n[0].getType(check); TypeNode rhsType = n[1].getType(check); - - // TODO : we may want to limit cases where we have equalities between terms of different types - // equalities between (Set Int) and (Set Real) already cause strange issues in theory solver for sets - // one possibility is to only allow this for Int/Real + if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) { std::stringstream ss; ss << "Subexpressions must have a common base type:" << std::endl; @@ -90,6 +87,7 @@ class EqualityTypeRule { throw TypeCheckingExceptionPrivate(n, ss.str()); } + // TODO : check isFirstClass for these types? (github issue #1202) } return booleanType; }