From 62f79f8e73d3182485c38204784abc450e899b31 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 4 Feb 2012 22:19:12 +0000 Subject: [PATCH] support for isWellFounded/mkGroundTerm on uninterpretted sorts. cvc4 now assumes uninterpretted sorts are well-founded, allowing datatypes to work with uninterpretted sort subdata --- src/theory/builtin/kinds | 5 +++-- src/theory/builtin/theory_builtin_type_rules.h | 16 ++++++++++++++++ 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: -- 2.30.2