diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-28 22:56:45 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-28 22:59:00 -0600 |
commit | 0e7bfa71e7bea8b832df00d00332b42bf8bca60b (patch) | |
tree | ce0ac17a6c67030f36b1fa662535a0e84233da29 | |
parent | fb4104e7c5a88741f9ffd55384198af31435df9e (diff) |
add re.nostr for the empty regular expression; add re.allchar for the regular expresssion containing all charactors
-rw-r--r-- | src/parser/smt2/Smt2.g | 14 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 2 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 10 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.h | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 4 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 4 | ||||
-rw-r--r-- | src/util/regexp.h | 10 |
7 files changed, 23 insertions, 23 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 873f3dce6..6e9f04ce9 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1032,6 +1032,12 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | str[s,false] { expr = MK_CONST( ::CVC4::String(s) ); } + | RENOSTR_TOK + { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_EMPTY, nvec ); } + + | REALLCHAR_TOK + { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_SIGMA, nvec ); } + | EMPTYSET_TOK { expr = MK_CONST( ::CVC4::EmptySet()); } @@ -1294,12 +1300,12 @@ builtinOp[CVC4::Kind& kind] | STRREPL_TOK { $kind = CVC4::kind::STRING_STRREPL; } | STRPREF_TOK { $kind = CVC4::kind::STRING_PREFIX; } | STRSUFF_TOK { $kind = CVC4::kind::STRING_SUFFIX; } - | STRITOS_TOK { $kind = CVC4::kind::STRING_ITOS; } - | STRSTOI_TOK { $kind = CVC4::kind::STRING_STOI; } + | STRITOS_TOK { $kind = CVC4::kind::STRING_ITOS; } + | STRSTOI_TOK { $kind = CVC4::kind::STRING_STOI; } | STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; } | STRTORE_TOK { $kind = CVC4::kind::STRING_TO_REGEXP; } | RECON_TOK { $kind = CVC4::kind::REGEXP_CONCAT; } - | REUNION_TOK { $kind = CVC4::kind::REGEXP_UNION; } + | REUNION_TOK { $kind = CVC4::kind::REGEXP_UNION; } | REINTER_TOK { $kind = CVC4::kind::REGEXP_INTER; } | RESTAR_TOK { $kind = CVC4::kind::REGEXP_STAR; } | REPLUS_TOK { $kind = CVC4::kind::REGEXP_PLUS; } @@ -1705,6 +1711,8 @@ RESTAR_TOK : 're.*'; REPLUS_TOK : 're.+'; REOPT_TOK : 're.opt'; RERANGE_TOK : 're.range'; +RENOSTR_TOK : 're.nostr'; +REALLCHAR_TOK : 're.allchar'; SETUNION_TOK: 'union'; SETINT_TOK: 'intersection'; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index b709d7f80..dd6eac0ff 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -346,6 +346,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::REGEXP_PLUS: out << "re.+ "; break; case kind::REGEXP_OPT: out << "re.opt "; break; case kind::REGEXP_RANGE: out << "re.range "; break; + case kind::REGEXP_EMPTY: out << "re.nostr "; break; + case kind::REGEXP_SIGMA: out << "re.allchar "; break; // bv theory case kind::BITVECTOR_CONCAT: out << "concat "; break; diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 7f6893d7f..573aabe81 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -173,7 +173,7 @@ int RegExpOpr::delta( Node r ) { }
default: {
Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in delta of RegExp." << std::endl;
- AlwaysAssert( false );
+ Assert( false );
//return Node::null();
}
}
@@ -526,12 +526,12 @@ bool RegExpOpr::follow( Node r, CVC4::String c, std::vector< char > &vec_chars ) ret = 2;
}
break;*/
- default:
- //TODO: special sym: sigma, none, all
+ default: {
Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in delta of RegExp." << std::endl;
//AlwaysAssert( false );
//return Node::null();
return false;
+ }
}
}
@@ -791,7 +791,7 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes }
default: {
Trace("strings-regexp") << "Unsupported term: " << r << " in simplifyNRegExp." << std::endl;
- AlwaysAssert( false, "Unsupported Term" );
+ Assert( false, "Unsupported Term" );
}
}
conc = Rewriter::rewrite( conc );
@@ -907,7 +907,7 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes }
default: {
Trace("strings-regexp") << "Unsupported term: " << r << " in simplifyPRegExp." << std::endl;
- AlwaysAssert( false, "Unsupported Term" );
+ Assert( false, "Unsupported Term" );
}
}
conc = Rewriter::rewrite( conc );
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 32bfb2b3d..f9ae0a0ca 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -54,12 +54,12 @@ private: void simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes );
std::string niceChar( Node r );
int gcd ( int a, int b );
+ Node mkAllExceptOne( char c );
public:
RegExpOpr();
bool checkConstRegExp( Node r );
void simplify(Node t, std::vector< Node > &new_nodes, bool polarity);
- Node mkAllExceptOne( char c );
Node complement( Node r );
int delta( Node r );
Node derivativeSingle( Node r, CVC4::String c );
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index bb79f337b..15958def8 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -99,8 +99,8 @@ void StringsPreprocess::processRegExp( Node s, Node r, std::vector< Node > &ret break; } default: { - Trace("strings-preprocess") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl; - AlwaysAssert( false, "Unsupported Term" ); + Trace("strings-error") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl; + Assert( false, "Unsupported Term" ); } } } diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index c35e2b5c2..7196dc8f2 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -284,8 +284,8 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i } } default: { - Trace("strings-postrewrite") << "Unsupported term: " << r << " in testConstStringInRegExp." << std::endl; - AlwaysAssert( false, "Unsupported Term" ); + Trace("strings-error") << "Unsupported term: " << r << " in testConstStringInRegExp." << std::endl; + Assert( false, "Unsupported Term" ); return false; } } diff --git a/src/util/regexp.h b/src/util/regexp.h index dadc5996c..7985f4072 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -404,16 +404,6 @@ struct CVC4_PUBLIC RegExpHashFunction { std::ostream& operator <<(std::ostream& os, const RegExp& s) CVC4_PUBLIC; -class CVC4_PUBLIC RegExpEmpty : public RegExp { -public: - RegExpEmpty() : RegExp(0) {} -}; - -class CVC4_PUBLIC RegExpSigma : public RegExp { -public: - RegExpSigma() : RegExp(2) {} -}; - }/* CVC4 namespace */ #endif /* __CVC4__REGEXP_H */ |