summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/datatype.cpp21
-rw-r--r--src/util/datatype.h26
-rw-r--r--src/util/regexp.cpp80
-rw-r--r--src/util/regexp.h74
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) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback