From c3a959b3112af83492694b8f0919381b1c467fb8 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 11 Sep 2013 11:23:19 -0400 Subject: Theory of strings. Signed-off-by: Morgan Deters --- src/util/regexp.h | 336 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 336 insertions(+) create mode 100644 src/util/regexp.h (limited to 'src/util/regexp.h') diff --git a/src/util/regexp.h b/src/util/regexp.h new file mode 100644 index 000000000..debb57e4c --- /dev/null +++ b/src/util/regexp.h @@ -0,0 +1,336 @@ +/********************* */ +/*! \file regexp.h + ** \verbatim + ** Original author: Tianyi Liang + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__REGEXP_H +#define __CVC4__REGEXP_H + +#include +#include +//#include "util/exception.h" +//#include "util/integer.h" +#include "util/hash.h" + +namespace CVC4 { + +class CVC4_PUBLIC Char { + +private: + unsigned int d_char; + +public: + Char() {} + + Char(const unsigned int c) + : d_char(c) {} + + ~Char() {} + + Char& operator =(const Char& y) { + if(this != &y) d_char = y.d_char; + return *this; + } + + bool operator ==(const Char& y) const { + return d_char == y.d_char ; + } + + bool operator !=(const Char& y) const { + return d_char != y.d_char ; + } + + bool operator <(const Char& y) const { + return d_char < y.d_char; + } + + bool operator >(const Char& y) const { + return d_char > y.d_char ; + } + + bool operator <=(const Char& y) const { + return d_char <= y.d_char; + } + + bool operator >=(const Char& y) const { + return d_char >= y.d_char ; + } + + /* + * Convenience functions + */ + std::string toString() const { + std::string str = "1"; + str[0] = (char) d_char; + return str; + } + + unsigned size() const { + return 1; + } + + const char* c_str() const { + return toString().c_str(); + } +};/* class Char */ + +namespace strings { + +struct CharHashFunction { + size_t operator()(const ::CVC4::Char& c) const { + return __gnu_cxx::hash()(c.toString().c_str()); + } +};/* struct CharHashFunction */ + +} + +inline std::ostream& operator <<(std::ostream& os, const Char& c) CVC4_PUBLIC; +inline std::ostream& operator <<(std::ostream& os, const Char& c) { + return os << "\"" << c.toString() << "\""; +} + +class CVC4_PUBLIC String { + +private: + std::vector d_str; + + bool isVecSame(const std::vector &a, const std::vector &b) const { + if(a.size() != b.size()) return false; + else { + for(unsigned int i=0; i &s) : d_str(s) { } + + ~String() {} + + String& operator =(const String& y) { + if(this != &y) d_str = y.d_str; + return *this; + } + + bool operator ==(const String& y) const { + return isVecSame(d_str, y.d_str); + } + + bool operator !=(const String& y) const { + return ! ( isVecSame(d_str, y.d_str) ); + } + + String concat (const String& other) const { + std::vector ret_vec(d_str); + ret_vec.insert( ret_vec.end(), other.d_str.begin(), other.d_str.end() ); + return String(ret_vec); + } + + bool operator <(const String& y) const { + if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size(); + else { + for(unsigned int i=0; i(const String& y) const { + if(d_str.size() != y.d_str.size()) return d_str.size() > y.d_str.size(); + else { + for(unsigned int i=0; i y.d_str[i]; + + return false; + } + } + + bool operator <=(const String& y) const { + if(d_str.size() != y.d_str.size()) return d_str.size() < y.d_str.size(); + else { + for(unsigned int i=0; i=(const String& y) const { + if(d_str.size() != y.d_str.size()) return d_str.size() > y.d_str.size(); + else { + for(unsigned int i=0; i y.d_str[i]; + + return true; + } + } + + bool strncmp(const String &y, unsigned int n) const { + for(unsigned int i=0; i ret_vec; + std::vector::const_iterator itr = d_str.begin() + i; + //for(unsigned k=0; k ret_vec; + std::vector::const_iterator itr = d_str.begin() + i; + //for(unsigned k=0; k::const_iterator itr2 = itr; + //for(unsigned k=0; k()(s.toString().c_str()); + } +};/* struct StringHashFunction */ + +} + +inline std::ostream& operator <<(std::ostream& os, const String& s) CVC4_PUBLIC; +inline std::ostream& operator <<(std::ostream& os, const String& s) { + return os << "\"" << s.toString() << "\""; +} + +class CVC4_PUBLIC RegExp { + +private: + std::string d_str; + +public: + RegExp() {} + + RegExp(const std::string s) + : d_str(s) {} + + ~RegExp() {} + + RegExp& operator =(const RegExp& y) { + if(this != &y) d_str = y.d_str; + return *this; + } + + bool operator ==(const RegExp& y) const { + return d_str == y.d_str ; + } + + bool operator !=(const RegExp& y) const { + return d_str != y.d_str ; + } + + String concat (const RegExp& other) const { + return String(d_str + other.d_str); + } + + bool operator <(const RegExp& y) const { + return d_str < y.d_str; + } + + bool operator >(const RegExp& y) const { + return d_str > y.d_str ; + } + + bool operator <=(const RegExp& y) const { + return d_str <= y.d_str; + } + + bool operator >=(const RegExp& y) const { + return d_str >= y.d_str ; + } + + /* + * Convenience functions + */ + + size_t hash() const { + unsigned int h = 1; + + for (size_t i = 0; i < d_str.length(); ++i) { + h = (h << 5) + d_str[i]; + } + + return h; + } + + std::string toString() const { + return d_str; + } + + unsigned size() const { + return d_str.size(); + } +};/* class String */ + +/** + * Hash function for the RegExp constants. + */ +struct CVC4_PUBLIC RegExpHashFunction { + inline size_t operator()(const RegExp& s) const { + return s.hash(); + } +};/* struct RegExpHashFunction */ + +inline std::ostream& operator <<(std::ostream& os, const RegExp& s) CVC4_PUBLIC; +inline std::ostream& operator <<(std::ostream& os, const RegExp& s) { + return os << s.toString(); +} +}/* CVC4 namespace */ + +#endif /* __CVC4__STRING_H */ -- cgit v1.2.3