Builtin evaluation functions for sygus (#1991)

2 files changed, 16 insertions, 0 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index d697a6aaf..f19955d19 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -77,6 +77,11 @@ size_t Datatype::indexOf(Expr item) {
                 item.getType().isSelector(),
                 item,
                 "arg must be a datatype constructor, selector, or tester");
+  return indexOfInternal(item);
+}
+
+size_t Datatype::indexOfInternal(Expr item)
+{
   TNode n = Node::fromExpr(item);
   if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
     return indexOf( item[0] );
@@ -91,6 +96,10 @@ size_t Datatype::cindexOf(Expr item) {
   PrettyCheckArgument(item.getType().isSelector(),
                 item,
                 "arg must be a datatype selector");
+  return cindexOfInternal(item);
+}
+size_t Datatype::cindexOfInternal(Expr item)
+{
   TNode n = Node::fromExpr(item);
   if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
     return cindexOf( item[0] );
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 826711897..990548979 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -615,6 +615,13 @@ public:
    */
   static size_t cindexOf(Expr item) CVC4_PUBLIC;
 
+  /**
+   * Same as above, but without checks. These methods should be used by
+   * internal (Node-level) code.
+   */
+  static size_t indexOfInternal(Expr item);
+  static size_t cindexOfInternal(Expr item);
+
   /** The type for iterators over constructors. */
   typedef DatatypeConstructorIterator iterator;
   /** The (const) type for iterators over constructors. */