2 files changed, 29 insertions, 1 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index c90419def..4d5e95119 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -309,7 +309,10 @@ operator FUNCTION_TYPE 2: "a function type"
 cardinality FUNCTION_TYPE \
     "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
-well-founded FUNCTION_TYPE false
+well-founded FUNCTION_TYPE \
+    "::CVC4::theory::builtin::FunctionProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::builtin::FunctionProperties::mkGroundTerm(%TYPE%)" \
+    "theory/builtin/theory_builtin_type_rules.h"
 enumerator FUNCTION_TYPE \
     ::CVC4::theory::builtin::FunctionEnumerator \
     "theory/builtin/type_enumerator.h"
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index d49edbc8c..a3d1776e1 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -223,6 +223,31 @@ class FunctionProperties {
 
     return valueCard ^ argsCard;
   }
+  /** Function type is well-founded if its component sorts are */
+  static bool isWellFounded(TypeNode type)
+  {
+    for (TypeNode::iterator i = type.begin(), i_end = type.end(); i != i_end;
+         ++i)
+    {
+      if (!(*i).isWellFounded())
+      {
+        return false;
+      }
+    }
+    return true;
+  }
+  /**
+   * Ground term for function sorts is (lambda x. t) where x is the
+   * canonical variable list for its type and t is the canonical ground term of
+   * its range.
+   */
+  static Node mkGroundTerm(TypeNode type)
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    Node bvl = nm->getBoundVarListForFunctionType(type);
+    Node ret = type.getRangeType().mkGroundTerm();
+    return nm->mkNode(kind::LAMBDA, bvl, ret);
+  }
 };/* class FuctionProperties */
 
 class SExprProperties {