diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-10 20:24:34 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-10 20:24:34 -0500 |
commit | e5d09628376cc101cbd3646dd64041170dacb402 (patch) | |
tree | 6a08f0ac7d28c348947c1ae085b11fed3f5103ad /src/expr | |
parent | f1d4d477d7cbfb6c8ba79232986a4135c5647e4a (diff) |
Properly implement function extensionality based on cardinality (#1765)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/type_node.cpp | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 9e61e713b..e7775cf7f 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -82,6 +82,22 @@ bool TypeNode::isInterpretedFinite() const { }else if( isSet() ) { return getSetElementType().isInterpretedFinite(); } + else if (isFunction()) + { + if (!getRangeType().isInterpretedFinite()) + { + return false; + } + std::vector<TypeNode> argTypes = getArgTypes(); + for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++) + { + if (!argTypes[i].isInterpretedFinite()) + { + return false; + } + } + return true; + } } return false; } |