diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-02-04 22:19:12 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-02-04 22:19:12 +0000 |
commit | 62f79f8e73d3182485c38204784abc450e899b31 (patch) | |
tree | bc18b3239c628ae399e9c61417d536607b63e9e9 /src | |
parent | 57f2a8e9215daf83616bb05b3b134e5544f7d808 (diff) |
support for isWellFounded/mkGroundTerm on uninterpretted sorts. cvc4 now assumes uninterpretted sorts are well-founded, allowing datatypes to work with uninterpretted sort subdata
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/builtin/kinds | 5 | ||||
-rw-r--r-- | 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: |