diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-26 11:44:23 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-26 14:44:23 -0300 |
commit | cc052e096323a193b52a05c2400c0c4639ada5de (patch) | |
tree | 7df1a434c075a4359bca3b1378447017791982e4 /src | |
parent | 55fd45841d2f51c5194b710d8d99ad43c2315c08 (diff) |
Optionally permit creation of non-flat function types (#6010)
This is required for creating the representation of closues in LFSC, which are of the form ((forall x T) P) where notice that forall has non-flat function type (-> Int Sort (-> Bool Bool)).
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/node_manager.cpp | 20 | ||||
-rw-r--r-- | src/expr/node_manager.h | 22 |
2 files changed, 30 insertions, 12 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 59afec4a6..883febd6f 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -769,40 +769,44 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor nm, rec, index + 1); } -TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) +TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts, + bool reqFlat) { Assert(sorts.size() >= 2); - CheckArgument(!sorts[sorts.size() - 1].isFunction(), + CheckArgument(!reqFlat || !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) +TypeNode NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts, + bool reqFlat) { Assert(sorts.size() >= 1); std::vector<TypeNode> sortNodes; sortNodes.insert(sortNodes.end(), sorts.begin(), sorts.end()); sortNodes.push_back(booleanType()); - return mkFunctionType(sortNodes); + return mkFunctionType(sortNodes, reqFlat); } TypeNode NodeManager::mkFunctionType(const TypeNode& domain, - const TypeNode& range) + const TypeNode& range, + bool reqFlat) { std::vector<TypeNode> sorts; sorts.push_back(domain); sorts.push_back(range); - return mkFunctionType(sorts); + return mkFunctionType(sorts, reqFlat); } TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes, - const TypeNode& range) + const TypeNode& range, + bool reqFlat) { Assert(argTypes.size() >= 1); std::vector<TypeNode> sorts(argTypes); sorts.push_back(range); - return mkFunctionType(sorts); + return mkFunctionType(sorts, reqFlat); } TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 89cd61e09..076b6d164 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -886,9 +886,15 @@ class NodeManager { * * @param domain the domain type * @param range the range type + * @param reqFlat If true, we require flat function types, e.g. the + * range type cannot be a function. User-generated function types and those + * used in solving must be flat, although some use cases (e.g. LFSC proof + * conversion) require non-flat function types. * @returns the functional type domain -> range */ - TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range); + TypeNode mkFunctionType(const TypeNode& domain, + const TypeNode& range, + bool reqFlat = true); /** * Make a function type with input types from @@ -896,18 +902,25 @@ class NodeManager { * * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n]) * @param range the range type + * @param reqFlat Same as above * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range */ TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes, - const TypeNode& range); + const TypeNode& range, + bool reqFlat = true); /** * Make a function type with input types from * <code>sorts[0..sorts.size()-2]</code> and result type * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have * at least 2 elements. + * + * @param sorts The argument and range sort of the function type, where the + * range type is the last in this vector. + * @param reqFlat Same as above */ - TypeNode mkFunctionType(const std::vector<TypeNode>& sorts); + TypeNode mkFunctionType(const std::vector<TypeNode>& sorts, + bool reqFlat = true); /** * Make a predicate type with input types from @@ -915,7 +928,8 @@ class NodeManager { * <code>BOOLEAN</code>. <code>sorts</code> must have at least one * element. */ - TypeNode mkPredicateType(const std::vector<TypeNode>& sorts); + TypeNode mkPredicateType(const std::vector<TypeNode>& sorts, + bool reqFlat = true); /** * Make a tuple type with types from |