From 37812f8ad9743b372608e871efe3e336c4ebd631 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 4 Nov 2011 16:52:06 +0000 Subject: [PATCH] STRING_TYPE and CONST_STRING and associate type infrastructure implemented. --- src/expr/expr_manager_template.cpp | 5 ++++ src/expr/expr_manager_template.h | 3 +++ src/expr/node_manager.h | 8 +++++++ src/expr/type.cpp | 18 ++++++++++++++ src/expr/type.h | 24 +++++++++++++++++++ src/expr/type_node.cpp | 5 ++++ src/expr/type_node.h | 3 +++ src/theory/builtin/kinds | 17 +++++++++++++ .../builtin/theory_builtin_type_rules.h | 9 +++++++ src/util/hash.h | 6 +++++ src/util/options.cpp | 2 +- 11 files changed, 99 insertions(+), 1 deletion(-) diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 28f990c98..624fbd9a2 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -125,6 +125,11 @@ BooleanType ExprManager::booleanType() const { return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType()))); } +StringType ExprManager::stringType() const { + NodeManagerScope nms(d_nodeManager); + return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->stringType()))); +} + KindType ExprManager::kindType() const { NodeManagerScope nms(d_nodeManager); return KindType(Type(d_nodeManager, new TypeNode(d_nodeManager->kindType()))); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 77b92c873..184556887 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -120,6 +120,9 @@ public: /** Get the type for booleans */ BooleanType booleanType() const; + /** Get the type for strings. */ + StringType stringType() const; + /** Get the type for sorts. */ KindType kindType() const; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 84ed78662..adba8087c 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -515,6 +515,9 @@ public: /** Get the (singleton) type for pseudobooleans. */ inline TypeNode pseudobooleanType(); + /** Get the (singleton) type for strings. */ + inline TypeNode stringType(); + /** Get the (singleton) type for sorts. */ inline TypeNode kindType(); @@ -780,6 +783,11 @@ inline TypeNode NodeManager::pseudobooleanType() { return TypeNode(mkTypeConst(PSEUDOBOOLEAN_TYPE)); } +/** Get the (singleton) type for strings. */ +inline TypeNode NodeManager::stringType() { + return TypeNode(mkTypeConst(STRING_TYPE)); +} + /** Get the (singleton) type for sorts. */ inline TypeNode NodeManager::kindType() { return TypeNode(mkTypeConst(KIND_TYPE)); diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 77cf97bb1..7e06a05ae 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -227,6 +227,19 @@ Type::operator PseudobooleanType() const throw(AssertionException) { return PseudobooleanType(*this); } +/** Is this the string type? */ +bool Type::isString() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isString(); +} + +/** Cast to a string type */ +Type::operator StringType() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isNull() || isString()); + return StringType(*this); +} + /** Is this the bit-vector type? */ bool Type::isBitVector() const { NodeManagerScope nms(d_nodeManager); @@ -465,6 +478,11 @@ PseudobooleanType::PseudobooleanType(const Type& t) throw(AssertionException) : Assert(isNull() || isPseudoboolean()); } +StringType::StringType(const Type& t) throw(AssertionException) : + Type(t) { + Assert(isNull() || isString()); +} + BitVectorType::BitVectorType(const Type& t) throw(AssertionException) : Type(t) { Assert(isNull() || isBitVector()); diff --git a/src/expr/type.h b/src/expr/type.h index b5aa18262..0b50fbd3c 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -47,6 +47,7 @@ class BooleanType; class IntegerType; class RealType; class PseudobooleanType; +class StringType; class BitVectorType; class ArrayType; class DatatypeType; @@ -253,6 +254,18 @@ public: */ operator PseudobooleanType() const throw(AssertionException); + /** + * Is this the string type? + * @return true if the type is the string type + */ + bool isString() const; + + /** + * Cast this type to a string type + * @return the StringType + */ + operator StringType() const throw(AssertionException); + /** * Is this the bit-vector type? * @return true if the type is a bit-vector type @@ -448,6 +461,17 @@ public: PseudobooleanType(const Type& type) throw(AssertionException); };/* class PseudobooleanType */ +/** + * Singleton class encapsulating the string type. + */ +class CVC4_PUBLIC StringType : public Type { + +public: + + /** Construct from the base type */ + StringType(const Type& type) throw(AssertionException); +};/* class StringType */ + /** * Class encapsulating a function type. */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 51d86904a..77203bbb5 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -95,6 +95,11 @@ bool TypeNode::isPseudoboolean() const { getConst() == PSEUDOBOOLEAN_TYPE; } +bool TypeNode::isString() const { + return getKind() == kind::TYPE_CONSTANT && + getConst() == STRING_TYPE; +} + bool TypeNode::isArray() const { return getKind() == kind::ARRAY_TYPE; } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 966611764..553f83276 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -449,6 +449,9 @@ public: /** Is this the Pseudoboolean type? */ bool isPseudoboolean() const; + /** Is this the String type? */ + bool isString() const; + /** Is this an array type? */ bool isArray() const; 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) { diff --git a/src/util/hash.h b/src/util/hash.h index bd3fee597..6183c5208 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -36,6 +36,12 @@ struct StringHashFunction { } };/* struct StringHashFunction */ +struct StringHashStrategy { + static size_t hash(const std::string& str) { + return std::hash()(str.c_str()); + } +};/* struct StringHashStrategy */ + }/* CVC4 namespace */ #endif /* __CVC4__HASH_H */ diff --git a/src/util/options.cpp b/src/util/options.cpp index 7decc693b..94ddf082f 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -102,7 +102,7 @@ Options::Options() : static const string mostCommonOptionsDescription = "\ Most commonly-used CVC4 options:\n\ --version | -V identify this CVC4 binary\n\ - --help | -h this command line reference\n\ + --help | -h full command line reference\n\ --lang | -L force input language (default is `auto'; see --lang help)\n\ --output-lang force output language (default is `auto'; see --lang help)\n\ --verbose | -v increase verbosity (may be repeated)\n\ -- 2.30.2