support for isWellFounded/mkGroundTerm on uninterpretted sorts. cvc4 now assumes uninterpretted sorts are well-founded, allowing datatypes to work with uninterpretted sort subdata

2 files changed, 19 insertions, 2 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 50e4d53bb..b7329cb3a 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -260,8 +260,9 @@ parameterized SORT_TYPE SORT_TAG 0: "sort type"
 # enough (for now) ?  Once we support quantifiers, maybe reconsider
 # this..
 cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)"
-well-founded SORT_TYPE false
-
+well-founded SORT_TYPE \
+    "::CVC4::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)"
 
 # A kind representing "inlined" operators defined with OPERATOR
 # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 48a5d475d..86603f004 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -138,6 +138,22 @@ public:
   }
 };/* class StringConstantTypeRule */
 
+class SortProperties {
+//private:  //FIXME?
+//  static std::map< TypeNode, TNode > d_groundTerms;
+public:
+  inline static bool isWellFounded(TypeNode type) {
+    return true;
+  }
+  inline static Node mkGroundTerm(TypeNode type) {
+    Assert(type.getKind() == kind::SORT_TYPE);
+    //if( d_groundTerms.find( type )==d_groundTerms.end() ){
+    //  d_groundTerms[type] = NodeManager::currentNM()->mkVar( type );
+    //}
+    //return d_groundTerms[type];
+    return NodeManager::currentNM()->mkVar( type );
+  }
+};
 
 class FunctionProperties {
 public: