From: Tianyi Liang Date: Sat, 1 Mar 2014 04:56:45 +0000 (-0600) Subject: add re.nostr for the empty regular expression; add re.allchar for the regular express... X-Git-Tag: cvc5-1.0.0~7052 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0e7bfa71e7bea8b832df00d00332b42bf8bca60b;p=cvc5.git add re.nostr for the empty regular expression; add re.allchar for the regular expresssion containing all charactors --- 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 */