diff options
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 78 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.h | 3 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 50 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 5 |
4 files changed, 121 insertions, 15 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index a3921bb42..f26037cf0 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -30,6 +30,14 @@ RegExpOpr::RegExpOpr() { d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma );
}
+int RegExpOpr::gcd ( int a, int b ) {
+ int c;
+ while ( a != 0 ) {
+ c = a; a = b%a; b = c;
+ }
+ return b;
+}
+
bool RegExpOpr::checkConstRegExp( Node r ) {
Trace("strings-regexp-cstre") << "RegExp-CheckConstRegExp starts with " << mkString( r ) << std::endl;
bool ret = true;
@@ -325,6 +333,76 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { return retNode;
}
+//TODO:
+bool RegExpOpr::guessLength( Node r, int &co ) {
+ int k = r.getKind();
+ switch( k ) {
+ case kind::STRING_TO_REGEXP:
+ {
+ if(r[0].isConst()) {
+ co += r[0].getConst< CVC4::String >().size();
+ return true;
+ } else {
+ return false;
+ }
+ }
+ break;
+ case kind::REGEXP_CONCAT:
+ {
+ for(unsigned i=0; i<r.getNumChildren(); ++i) {
+ if(!guessLength( r[i], co)) {
+ return false;
+ }
+ }
+ return true;
+ }
+ break;
+ case kind::REGEXP_OR:
+ {
+ int g_co;
+ for(unsigned i=0; i<r.getNumChildren(); ++i) {
+ int cop = 0;
+ if(!guessLength( r[i], cop)) {
+ return false;
+ }
+ if(i == 0) {
+ g_co = cop;
+ } else {
+ g_co = gcd(g_co, cop);
+ }
+ }
+ return true;
+ }
+ break;
+ case kind::REGEXP_INTER:
+ {
+ int g_co;
+ for(unsigned i=0; i<r.getNumChildren(); ++i) {
+ int cop = 0;
+ if(!guessLength( r[i], cop)) {
+ return false;
+ }
+ if(i == 0) {
+ g_co = cop;
+ } else {
+ g_co = gcd(g_co, cop);
+ }
+ }
+ return true;
+ }
+ break;
+ case kind::REGEXP_STAR:
+ {
+ co = 0;
+ return true;
+ }
+ break;
+ default:
+ Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in membership of RegExp." << std::endl;
+ return false;
+ }
+}
+
void RegExpOpr::firstChar( Node r ) {
Trace("strings-regexp-firstchar") << "Head characters: ";
for(char ch = d_char_start; ch <= d_char_end; ++ch) {
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 5f0eab2e0..702e5ba84 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -45,6 +45,8 @@ private: //void simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn );
//Node simplify( Node t, std::vector< Node > &new_nodes );
std::string niceChar( Node r );
+ int gcd ( int a, int b );
+
public:
RegExpOpr();
bool checkConstRegExp( Node r );
@@ -53,6 +55,7 @@ public: Node complement( Node r );
int delta( Node r );
Node derivativeSingle( Node r, CVC4::String c );
+ bool guessLength( Node r, int &co );
void firstChar( Node r );
bool follow( Node r, CVC4::String c, std::vector< char > &vec_chars );
std::string mkString( Node r );
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 66cc2a434..b8f3f496f 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -57,6 +57,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_false = NodeManager::currentNM()->mkConst( false ); d_regexp_incomplete = false; + d_opt_regexp_gcd = true; } TheoryStrings::~TheoryStrings() { @@ -1818,14 +1819,6 @@ bool TheoryStrings::checkCardinality() { return false; } -int TheoryStrings::gcd ( int a, int b ) { - int c; - while ( a != 0 ) { - c = a; a = b%a; b = c; - } - return b; -} - void TheoryStrings::getEquivalenceClasses( std::vector< Node >& eqcs ) { eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ) { @@ -2009,6 +2002,14 @@ bool TheoryStrings::checkMemberships() { Node r = atom[1]; Assert( r.getKind()==kind::REGEXP_STAR ); if( !areEqual( x, d_emptyString ) ) { + /*if(d_opt_regexp_gcd) { + if(d_membership_length.find(atom) == d_membership_length.end()) { + addedLemma = addMembershipLength(atom); + d_membership_length[atom] = true; + } else { + Trace("strings-regexp") << "Membership length is already added." << std::endl; + } + }*/ bool flag = true; if( d_reg_exp_deriv.find(atom)==d_reg_exp_deriv.end() ) { if(splitRegExp( x, r, atom )) { @@ -2020,12 +2021,12 @@ bool TheoryStrings::checkMemberships() { Trace("strings-regexp-derivative") << "... is processed by deriv." << std::endl; } if( flag && d_reg_exp_unroll.find(atom)==d_reg_exp_unroll.end() ) { - if( unrollStar( atom ) ) { - addedLemma = true; - } else { - Trace("strings-regexp") << "RegExp is incomplete due to " << assertion << ", depth = " << d_regexp_unroll_depth << std::endl; - is_unk = true; - } + if( unrollStar( atom ) ) { + addedLemma = true; + } else { + Trace("strings-regexp") << "RegExp is incomplete due to " << assertion << ", depth = " << d_regexp_unroll_depth << std::endl; + is_unk = true; + } } else { Trace("strings-regexp") << "...is already unrolled or splitted." << std::endl; } @@ -2097,6 +2098,27 @@ CVC4::String TheoryStrings::getHeadConst( Node x ) { } } +bool TheoryStrings::addMembershipLength(Node atom) { + Node x = atom[0]; + Node r = atom[1]; + + /*std::vector< int > co; + co.push_back(0); + for(unsigned int k=0; k<lts.size(); ++k) { + if(lts[k].isConst() && lts[k].getType().isInteger()) { + int len = lts[k].getConst<Rational>().getNumerator().toUnsignedInt(); + co[0] += cols[k].size() * len; + } else { + co.push_back( cols[k].size() ); + } + } + int g_co = co[0]; + for(unsigned k=1; k<co.size(); ++k) { + g_co = gcd(g_co, co[k]); + }*/ + return false; +} + bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) { // TODO cstr in vre Assert(x != d_emptyString); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 6ac8cf995..fb6599919 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -116,6 +116,7 @@ private: Node d_zero; // Options bool d_opt_fmf; + bool d_opt_regexp_gcd; // Helper functions Node getRepresentative( Node t ); bool hasTerm( Node a ); @@ -202,7 +203,6 @@ private: bool checkCardinality(); bool checkInductiveEquations(); bool checkMemberships(); - int gcd(int a, int b); public: void preRegisterTerm(TNode n); @@ -267,6 +267,8 @@ private: bool d_regexp_incomplete; int d_regexp_unroll_depth; int d_regexp_max_depth; + // membership length + std::map< Node, bool > d_membership_length; // regular expression derivative std::map< Node, bool > d_reg_exp_deriv; // regular expression operations @@ -274,6 +276,7 @@ private: CVC4::String getHeadConst( Node x ); bool splitRegExp( Node x, Node r, Node ant ); + bool addMembershipLength(Node atom); // Finite Model Finding |