From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 21 Jun 2014 02:25:21 +0000 (-0400)
Subject: Implement RecordProperties::mkGroundTerm().  Resolves bug #546.
X-Git-Tag: cvc5-1.0.0~6757
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f37411e40673b07e8fe7d20ed9b6c5be98f3b8ae;p=cvc5.git

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

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) {