New C++ API: Add checks for Sorts. (#2519)

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 &&