diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-10-04 16:47:43 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-04 16:47:43 -0700 |
commit | 682a9ad81e7819a391b6eac49ea989d75c9774cc (patch) | |
tree | 2fc80d937f89e9b015c274a5083b567b7f77e1b2 /src/expr | |
parent | 13758686d92eb5a6cfb30d830a35b20c14213717 (diff) |
New C++ API: Add checks for Sorts. (#2519)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/type.cpp | 12 | ||||
-rw-r--r-- | src/expr/type.h | 27 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 2 |
3 files changed, 41 insertions, 0 deletions
diff --git a/src/expr/type.cpp b/src/expr/type.cpp index a3e35e91f..fe8cc097b 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -72,6 +72,18 @@ bool Type::isWellFounded() const { return d_typeNode->isWellFounded(); } +bool Type::isFirstClass() const +{ + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isFirstClass(); +} + +bool Type::isFunctionLike() const +{ + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isFunctionLike(); +} + Expr Type::mkGroundTerm() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->mkGroundTerm().toExpr(); diff --git a/src/expr/type.h b/src/expr/type.h index b2ec1b024..4d22f1538 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -145,6 +145,33 @@ protected: bool isWellFounded() 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; + + /** + * Is this a function-LIKE type? + * + * Anything function-like except arrays (e.g., datatype selectors) is + * considered a function here. Function-like terms can not be the argument + * or return value for any term that is function-like. + * This is mainly to avoid higher order. + * + * Note that arrays are explicitly not considered function-like here. + * + * @return true if this is a function-like type + */ + bool isFunctionLike() const; + + /** * Construct and return a ground term for this Type. Throws an * exception if this type is not well-founded. */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index b54290612..fd65f96b9 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -20,6 +20,7 @@ #include "expr/node_manager_attributes.h" #include "expr/type_properties.h" #include "options/base_options.h" +#include "options/bv_options.h" #include "options/expr_options.h" #include "options/quantifiers_options.h" #include "options/uf_options.h" @@ -222,6 +223,7 @@ bool TypeNode::isClosedEnumerable() } bool TypeNode::isFirstClass() const { + (void)options::bitblastMode(); return ( getKind() != kind::FUNCTION_TYPE || options::ufHo() ) && getKind() != kind::CONSTRUCTOR_TYPE && getKind() != kind::SELECTOR_TYPE && |