From f37411e40673b07e8fe7d20ed9b6c5be98f3b8ae Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 20 Jun 2014 22:25:21 -0400 Subject: [PATCH] Implement RecordProperties::mkGroundTerm(). Resolves bug #546. --- src/theory/datatypes/theory_datatypes_type_rules.h | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) 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 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) { -- 2.30.2