string fmf changes

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index a3921bb428fb0554ac55bb1a78d9f9d1b78f9bf6..f26037cf050b676ab77be5a0504e0dffbb73e7c2 100644 (file)
--- 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 );\r
 }\r
 \r
+int RegExpOpr::gcd ( int a, int b ) {\r
+  int c;\r
+  while ( a != 0 ) {\r
+     c = a; a = b%a;  b = c;\r
+  }\r
+  return b;\r
+}\r
+\r
 bool RegExpOpr::checkConstRegExp( Node r ) {\r
        Trace("strings-regexp-cstre") << "RegExp-CheckConstRegExp starts with " << mkString( r ) << std::endl;\r
        bool ret = true;\r
@@ -325,6 +333,76 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
        return retNode;\r
 }\r
 \r
+//TODO:\r
+bool RegExpOpr::guessLength( Node r, int &co ) {\r
+       int k = r.getKind();\r
+       switch( k ) {\r
+               case kind::STRING_TO_REGEXP:\r
+               {\r
+                       if(r[0].isConst()) {\r
+                               co += r[0].getConst< CVC4::String >().size();\r
+                               return true;\r
+                       } else {\r
+                               return false;\r
+                       }\r
+               }\r
+                       break;\r
+               case kind::REGEXP_CONCAT:\r
+               {\r
+                       for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
+                               if(!guessLength( r[i], co)) {\r
+                                       return false;\r
+                               }\r
+                       }\r
+                       return true;\r
+               }\r
+                       break;\r
+               case kind::REGEXP_OR:\r
+               {\r
+                       int g_co;\r
+                       for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
+                               int cop = 0;\r
+                               if(!guessLength( r[i], cop)) {\r
+                                       return false;\r
+                               }\r
+                               if(i == 0) {\r
+                                       g_co = cop;\r
+                               } else {\r
+                                       g_co = gcd(g_co, cop);\r
+                               }\r
+                       }\r
+                       return true;\r
+               }\r
+                       break;\r
+               case kind::REGEXP_INTER:\r
+               {\r
+                       int g_co;\r
+                       for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
+                               int cop = 0;\r
+                               if(!guessLength( r[i], cop)) {\r
+                                       return false;\r
+                               }\r
+                               if(i == 0) {\r
+                                       g_co = cop;\r
+                               } else {\r
+                                       g_co = gcd(g_co, cop);\r
+                               }\r
+                       }\r
+                       return true;\r
+               }\r
+                       break;\r
+               case kind::REGEXP_STAR:\r
+               {\r
+                       co = 0;\r
+                       return true;\r
+               }\r
+                       break;\r
+               default:\r
+                       Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in membership of RegExp." << std::endl;\r
+                       return false;\r
+       }\r
+}\r
+\r
 void RegExpOpr::firstChar( Node r ) {\r
        Trace("strings-regexp-firstchar") << "Head characters: ";\r
        for(char ch = d_char_start; ch <= d_char_end; ++ch) {\r

diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 5f0eab2e00f36a53fc9c2e1b438324f0cc990a29..702e5ba84d6f39b136a370a801f968c29da31bfb 100644 (file)
--- 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 );\r
        //Node simplify( Node t, std::vector< Node > &new_nodes );\r
        std::string niceChar( Node r );\r
+       int gcd ( int a, int b );\r
+\r
 public:\r
        RegExpOpr();\r
        bool checkConstRegExp( Node r );\r
@@ -53,6 +55,7 @@ public:
        Node complement( Node r );\r
        int delta( Node r );\r
        Node derivativeSingle( Node r, CVC4::String c );\r
+       bool guessLength( Node r, int &co );\r
        void firstChar( Node r );\r
        bool follow( Node r, CVC4::String c, std::vector< char > &vec_chars );\r
        std::string mkString( Node r );\r

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index b7576659aed81748a4ec32a7a75389a995936e70..4e20ac248363cc668a4fd95594a15b9bc95a39f7 100644 (file)
--- 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 6ac8cf99592d5fcbd6c6f4aa9af3b13e01ab6760..fb65999198b1595dcf795091ad786500860cf078 100644 (file)
--- 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