diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-27 10:23:42 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-27 10:23:42 -0500 |
commit | a64866663f10db4ffadd2d48500cda05c4831f0e (patch) | |
tree | 34c95678bf117cda2818a201250354b7601f6545 | |
parent | 27ac2ce712b0bcfdef83e2d44dd210f667ab7959 (diff) |
Do not require that function sorts are first class internally (#4128)
This PR removes the requirement in the NodeManager that argument types to the function sort are first class.
Notice that the new API does this check (as it should): https://github.com/CVC4/CVC4/blob/master/src/api/cvc4cpp.cpp#L2633
Moreover, SyGuS v2 internally requires constructing function types having arguments that are not first class (e.g. regular expression type). This is required to update the regression https://github.com/CVC4/CVC4/blob/master/test/regress/regress1/sygus/re-concat.sy to SyGuS v2.
FYI @abdoo8080 .
-rw-r--r-- | src/expr/node_manager.cpp | 36 | ||||
-rw-r--r-- | src/expr/node_manager.h | 56 |
2 files changed, 41 insertions, 51 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 5d409f748..16ffd8306 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -575,6 +575,42 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor } } +TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) +{ + Assert(sorts.size() >= 2); + CheckArgument(!sorts[sorts.size() - 1].isFunction(), + sorts[sorts.size() - 1], + "must flatten function types"); + return mkTypeNode(kind::FUNCTION_TYPE, sorts); +} + +TypeNode NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) +{ + Assert(sorts.size() >= 1); + std::vector<TypeNode> sortNodes; + sortNodes.insert(sortNodes.end(), sorts.begin(), sorts.end()); + sortNodes.push_back(booleanType()); + return mkFunctionType(sortNodes); +} + +TypeNode NodeManager::mkFunctionType(const TypeNode& domain, + const TypeNode& range) +{ + std::vector<TypeNode> sorts; + sorts.push_back(domain); + sorts.push_back(range); + return mkFunctionType(sorts); +} + +TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes, + const TypeNode& range) +{ + Assert(argTypes.size() >= 1); + std::vector<TypeNode> sorts(argTypes); + sorts.push_back(range); + return mkFunctionType(sorts); +} + TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { std::vector< TypeNode > ts; Debug("tuprec-debug") << "Make tuple type : "; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index eced00c48..2e8f40fff 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -807,7 +807,7 @@ public: * @param range the range type * @returns the functional type domain -> range */ - inline TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range); + TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range); /** * Make a function type with input types from @@ -817,8 +817,8 @@ public: * @param range the range type * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range */ - inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes, - const TypeNode& range); + TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes, + const TypeNode& range); /** * Make a function type with input types from @@ -826,7 +826,7 @@ public: * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have * at least 2 elements. */ - inline TypeNode mkFunctionType(const std::vector<TypeNode>& sorts); + TypeNode mkFunctionType(const std::vector<TypeNode>& sorts); /** * Make a predicate type with input types from @@ -834,7 +834,7 @@ public: * <code>BOOLEAN</code>. <code>sorts</code> must have at least one * element. */ - inline TypeNode mkPredicateType(const std::vector<TypeNode>& sorts); + TypeNode mkPredicateType(const std::vector<TypeNode>& sorts); /** * Make a tuple type with types from @@ -1086,52 +1086,6 @@ inline TypeNode NodeManager::builtinOperatorType() { return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE)); } -/** Make a function type from domain to range. */ -inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) { - std::vector<TypeNode> sorts; - sorts.push_back(domain); - sorts.push_back(range); - return mkFunctionType(sorts); -} - -inline TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range) { - Assert(argTypes.size() >= 1); - std::vector<TypeNode> sorts(argTypes); - sorts.push_back(range); - return mkFunctionType(sorts); -} - -inline TypeNode -NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) { - Assert(sorts.size() >= 2); - std::vector<TypeNode> sortNodes; - for (unsigned i = 0; i < sorts.size(); ++ i) { - CheckArgument(sorts[i].isFirstClass(), - sorts, - "cannot create function types for argument types that are " - "not first-class. Try option --uf-ho."); - 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); -} - -inline TypeNode -NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) { - Assert(sorts.size() >= 1); - std::vector<TypeNode> sortNodes; - for (unsigned i = 0; i < sorts.size(); ++ i) { - CheckArgument(sorts[i].isFirstClass(), - sorts, - "cannot create predicate types for argument types that are " - "not first-class. Try option --uf-ho."); - sortNodes.push_back(sorts[i]); - } - sortNodes.push_back(booleanType()); - return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); -} - inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) { std::vector<TypeNode> typeNodes; for (unsigned i = 0; i < types.size(); ++ i) { |