Implement RecordProperties::mkGroundTerm(). Resolves bug #546.

1 files changed, 12 insertions, 1 deletions

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 09d43b3bc..4d0acccc8 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -477,7 +477,18 @@ struct RecordUpdateTypeRule {
 
 struct RecordProperties {
   inline static Node mkGroundTerm(TypeNode type) {
-    Unimplemented();
+    Assert(type.getKind() == kind::RECORD_TYPE);
+
+    const Record& rec = type.getRecord();
+    std::vector<Node> children;
+    for(Record::iterator i = rec.begin(),
+          i_end = rec.end();
+        i != i_end;
+        ++i) {
+      children.push_back((*i).second.mkGroundTerm());
+    }
+
+    return NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(rec), children);
   }
 
   inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {