diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-11-04 16:52:06 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-11-04 16:52:06 +0000 |
commit | 37812f8ad9743b372608e871efe3e336c4ebd631 (patch) | |
tree | 704591a3151169ed998956cbe4b85be8725941c2 /src/theory/builtin | |
parent | b5fd5b61a9f0f993703497fb1c8d678cf2d8bb01 (diff) |
STRING_TYPE and CONST_STRING and associate type infrastructure implemented.
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/kinds | 17 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 9 |
2 files changed, 26 insertions, 0 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 83a372726..50e4d53bb 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -301,6 +301,23 @@ well-founded TUPLE_TYPE \ "::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" +# These will eventually move to a theory of strings. +# +# For now these are unbounded strings over a fixed, finite alphabet +# (this may change). +sort STRING_TYPE \ + Cardinality::INTEGERS \ + well-founded \ + "NodeManager::currentNM()->mkConst(::std::string())" \ + "string" \ + "String type" +constant CONST_STRING \ + ::std::string \ + ::CVC4::StringHashStrategy \ + "util/hash.h" \ + "a string of characters" +typerule CONST_STRING ::CVC4::theory::builtin::StringConstantTypeRule + typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index ce06b4259..48a5d475d 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -130,6 +130,15 @@ public: } };/* class TupleTypeRule */ +class StringConstantTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + Assert(n.getKind() == kind::CONST_STRING); + return nodeManager->stringType(); + } +};/* class StringConstantTypeRule */ + + class FunctionProperties { public: inline static Cardinality computeCardinality(TypeNode type) { |