diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/datatype.cpp | 21 | ||||
-rw-r--r-- | src/util/datatype.h | 26 | ||||
-rw-r--r-- | src/util/regexp.cpp | 80 | ||||
-rw-r--r-- | src/util/regexp.h | 74 |
4 files changed, 130 insertions, 71 deletions
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 8d70e4ffc..4d45d9148 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -36,6 +36,7 @@ namespace CVC4 { namespace expr { namespace attr { struct DatatypeIndexTag {}; + struct DatatypeConsIndexTag {}; struct DatatypeFiniteTag {}; struct DatatypeWellFoundedTag {}; struct DatatypeFiniteComputedTag {}; @@ -45,6 +46,7 @@ namespace expr { }/* CVC4::expr namespace */ typedef expr::Attribute<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAttr; +typedef expr::Attribute<expr::attr::DatatypeConsIndexTag, uint64_t> DatatypeConsIndexAttr; typedef expr::Attribute<expr::attr::DatatypeFiniteTag, bool> DatatypeFiniteAttr; typedef expr::Attribute<expr::attr::DatatypeWellFoundedTag, bool> DatatypeWellFoundedAttr; typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFiniteComputedAttr; @@ -81,6 +83,20 @@ size_t Datatype::indexOf(Expr item) { } } +size_t Datatype::cindexOf(Expr item) { + ExprManagerScope ems(item); + CheckArgument(item.getType().isSelector(), + item, + "arg must be a datatype selector"); + TNode n = Node::fromExpr(item); + if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){ + return cindexOf( item[0] ); + }else{ + Assert(n.hasAttribute(DatatypeConsIndexAttr())); + return n.getAttribute(DatatypeConsIndexAttr()); + } +} + void Datatype::resolve(ExprManager* em, const std::map<std::string, DatatypeType>& resolutions, const std::vector<Type>& placeholders, @@ -103,7 +119,7 @@ void Datatype::resolve(ExprManager* em, d_resolved = true; size_t index = 0; for(std::vector<DatatypeConstructor>::iterator i = d_constructors.begin(), i_end = d_constructors.end(); i != i_end; ++i) { - (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements); + (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements, index); Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index); Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++); } @@ -401,7 +417,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, const std::vector<Type>& placeholders, const std::vector<Type>& replacements, const std::vector< SortConstructorType >& paramTypes, - const std::vector< DatatypeType >& paramReplacements) + const std::vector< DatatypeType >& paramReplacements, size_t cindex) throw(IllegalArgumentException, DatatypeResolutionException) { CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager"); @@ -447,6 +463,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, } (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr(); } + Node::fromExpr((*i).d_selector).setAttribute(DatatypeConsIndexAttr(), cindex); Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++); (*i).d_resolved = true; } diff --git a/src/util/datatype.h b/src/util/datatype.h index 99a303950..a8f3b404a 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -191,7 +191,7 @@ private: const std::vector<Type>& placeholders, const std::vector<Type>& replacements, const std::vector< SortConstructorType >& paramTypes, - const std::vector< DatatypeType >& paramReplacements) + const std::vector< DatatypeType >& paramReplacements, size_t cindex) throw(IllegalArgumentException, DatatypeResolutionException); friend class Datatype; @@ -434,6 +434,12 @@ public: */ static size_t indexOf(Expr item) CVC4_PUBLIC; + /** + * Get the index of constructor corresponding to selector. (Zero is + * always the first index.) + */ + static size_t cindexOf(Expr item) CVC4_PUBLIC; + /** The type for iterators over constructors. */ typedef DatatypeConstructorIterator iterator; /** The (const) type for iterators over constructors. */ @@ -442,6 +448,7 @@ public: private: std::string d_name; std::vector<Type> d_params; + bool d_isCo; std::vector<DatatypeConstructor> d_constructors; bool d_resolved; Type d_self; @@ -488,13 +495,13 @@ private: public: /** Create a new Datatype of the given name. */ - inline explicit Datatype(std::string name); + inline explicit Datatype(std::string name, bool isCo = false); /** * Create a new Datatype of the given name, with the given * parameterization. */ - inline Datatype(std::string name, const std::vector<Type>& params); + inline Datatype(std::string name, const std::vector<Type>& params, bool isCo = false); /** * Add a constructor to this Datatype. Constructor names need not @@ -520,6 +527,9 @@ public: /** Get parameters */ inline std::vector<Type> getParameters() const; + /** is this a co-datatype? */ + inline bool isCodatatype() const; + /** * Return the cardinality of this datatype (the sum of the * cardinalities of its constructors). The Datatype must be @@ -656,18 +666,20 @@ inline std::string DatatypeUnresolvedType::getName() const throw() { return d_name; } -inline Datatype::Datatype(std::string name) : +inline Datatype::Datatype(std::string name, bool isCo) : d_name(name), d_params(), + d_isCo(isCo), d_constructors(), d_resolved(false), d_self(), d_card(CardinalityUnknown()) { } -inline Datatype::Datatype(std::string name, const std::vector<Type>& params) : +inline Datatype::Datatype(std::string name, const std::vector<Type>& params, bool isCo) : d_name(name), d_params(params), + d_isCo(isCo), d_constructors(), d_resolved(false), d_self(), @@ -701,6 +713,10 @@ inline std::vector<Type> Datatype::getParameters() const { return d_params; } +inline bool Datatype::isCodatatype() const { + return d_isCo; +} + inline bool Datatype::operator!=(const Datatype& other) const throw() { return !(*this == other); } diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index b6db624d5..3bc17b050 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -23,6 +23,71 @@ using namespace std; namespace CVC4 {
+void String::toInternal(const std::string &s) {
+ d_str.clear();
+ unsigned i=0;
+ while(i < s.size()) {
+ if(s[i] == '\\') {
+ i++;
+ if(i < s.size()) {
+ switch(s[i]) {
+ case 'n': {d_str.push_back( convertCharToUnsignedInt('\n') );i++;} break;
+ case 't': {d_str.push_back( convertCharToUnsignedInt('\t') );i++;} break;
+ case 'v': {d_str.push_back( convertCharToUnsignedInt('\v') );i++;} break;
+ case 'b': {d_str.push_back( convertCharToUnsignedInt('\b') );i++;} break;
+ case 'r': {d_str.push_back( convertCharToUnsignedInt('\r') );i++;} break;
+ case 'f': {d_str.push_back( convertCharToUnsignedInt('\f') );i++;} break;
+ case 'a': {d_str.push_back( convertCharToUnsignedInt('\a') );i++;} break;
+ case '\\': {d_str.push_back( convertCharToUnsignedInt('\\') );i++;} break;
+ case 'x': {
+ if(i + 2 < s.size()) {
+ if((isdigit(s[i+1]) || (s[i+1] >= 'a' && s[i+1] >= 'f') || (s[i+1] >= 'A' && s[i+1] >= 'F')) &&
+ (isdigit(s[i+2]) || (s[i+2] >= 'a' && s[i+2] >= 'f') || (s[i+2] >= 'A' && s[i+2] >= 'F'))) {
+ d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) );
+ i += 3;
+ } else {
+ throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );
+ }
+ } else {
+ throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );
+ }
+ }
+ break;
+ default: {
+ if(isdigit(s[i])) {
+ int num = (int)s[i] - (int)'0';
+ bool flag = num < 4;
+ if(i+1 < s.size() && num < 8 && isdigit(s[i+1]) && s[i+1] < '8') {
+ num = num * 8 + (int)s[i+1] - (int)'0';
+ if(flag && i+2 < s.size() && isdigit(s[i+2]) && s[i+2] < '8') {
+ num = num * 8 + (int)s[i+2] - (int)'0';
+ d_str.push_back( convertCharToUnsignedInt((char)num) );
+ i += 3;
+ } else {
+ d_str.push_back( convertCharToUnsignedInt((char)num) );
+ i += 2;
+ }
+ } else {
+ d_str.push_back( convertCharToUnsignedInt((char)num) );
+ i++;
+ }
+ } else {
+ d_str.push_back( convertCharToUnsignedInt(s[i]) );
+ i++;
+ }
+ }
+ }
+ } else {
+ throw CVC4::Exception( "should be handled by lexer: \"" + s + "\"" );
+ //d_str.push_back( convertCharToUnsignedInt('\\') );
+ }
+ } else {
+ d_str.push_back( convertCharToUnsignedInt(s[i]) );
+ i++;
+ }
+ }
+}
+
void String::getCharSet(std::set<unsigned int> &cset) const {
for(std::vector<unsigned int>::const_iterator itr = d_str.begin();
itr != d_str.end(); itr++) {
@@ -30,6 +95,21 @@ void String::getCharSet(std::set<unsigned int> &cset) const { }
}
+bool String::overlap(String &y) const {
+ unsigned n = y.size();
+ if(d_str.size() < y.size()) {
+ n = d_str.size();
+ }
+ for(unsigned i=1; i<n; i++) {
+ String s = suffix(i);
+ String p = y.prefix(i);
+ if(s == p) {
+ return true;
+ }
+ }
+ return false;
+}
+
std::string String::toString() const {
std::string str;
for(unsigned int i=0; i<d_str.size(); ++i) {
diff --git a/src/util/regexp.h b/src/util/regexp.h index 8c4a3922d..2bb2b5c4c 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -70,70 +70,7 @@ private: } } - void toInternal(const std::string &s) { - d_str.clear(); - unsigned i=0; - while(i < s.size()) { - if(s[i] == '\\') { - i++; - if(i < s.size()) { - switch(s[i]) { - case 'n': {d_str.push_back( convertCharToUnsignedInt('\n') );i++;} break; - case 't': {d_str.push_back( convertCharToUnsignedInt('\t') );i++;} break; - case 'v': {d_str.push_back( convertCharToUnsignedInt('\v') );i++;} break; - case 'b': {d_str.push_back( convertCharToUnsignedInt('\b') );i++;} break; - case 'r': {d_str.push_back( convertCharToUnsignedInt('\r') );i++;} break; - case 'f': {d_str.push_back( convertCharToUnsignedInt('\f') );i++;} break; - case 'a': {d_str.push_back( convertCharToUnsignedInt('\a') );i++;} break; - case '\\': {d_str.push_back( convertCharToUnsignedInt('\\') );i++;} break; - case 'x': { - if(i + 2 < s.size()) { - if((isdigit(s[i+1]) || (s[i+1] >= 'a' && s[i+1] >= 'f') || (s[i+1] >= 'A' && s[i+1] >= 'F')) && - (isdigit(s[i+2]) || (s[i+2] >= 'a' && s[i+2] >= 'f') || (s[i+2] >= 'A' && s[i+2] >= 'F'))) { - d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) ); - i += 3; - } else { - throw CVC4::Exception( "Error String Literal: \"" + s + "\"" ); - } - } else { - throw CVC4::Exception( "Error String Literal: \"" + s + "\"" ); - } - } - break; - default: { - if(isdigit(s[i])) { - int num = (int)s[i] - (int)'0'; - bool flag = num < 4; - if(i+1 < s.size() && num < 8 && isdigit(s[i+1]) && s[i+1] < '8') { - num = num * 8 + (int)s[i+1] - (int)'0'; - if(flag && i+2 < s.size() && isdigit(s[i+2]) && s[i+2] < '8') { - num = num * 8 + (int)s[i+2] - (int)'0'; - d_str.push_back( convertCharToUnsignedInt((char)num) ); - i += 3; - } else { - d_str.push_back( convertCharToUnsignedInt((char)num) ); - i += 2; - } - } else { - d_str.push_back( convertCharToUnsignedInt((char)num) ); - i++; - } - } else { - d_str.push_back( convertCharToUnsignedInt(s[i]) ); - i++; - } - } - } - } else { - throw CVC4::Exception( "should be handled by lexer: \"" + s + "\"" ); - //d_str.push_back( convertCharToUnsignedInt('\\') ); - } - } else { - d_str.push_back( convertCharToUnsignedInt(s[i]) ); - i++; - } - } - } + void toInternal(const std::string &s); public: String() {} @@ -316,6 +253,15 @@ public: ret_vec.insert( ret_vec.end(), itr, itr + j ); return String(ret_vec); } + + String prefix(unsigned i) const { + return substr(0, i); + } + String suffix(unsigned i) const { + return substr(d_str.size() - i, i); + } + bool overlap(String &y) const; + bool isNumber() const { if(d_str.size() == 0) return false; for(unsigned int i=0; i<d_str.size(); ++i) { |