Relaxed the constant requirement for regular expression loop;

Added "ignoring negative membership" option (fragment checking is not provided,
and users must make sure the constraint is in the fragment;
otherwise, the solution may not be correct).

diff --git a/src/theory/strings/options b/src/theory/strings/options
index 10f22b05a8a7a6c8d7c6bb361f5738eaaedb5457..dc8c50966af531fb8b672a3d37683da3313ea67e 100644 (file)
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -23,6 +23,9 @@ option stringOpt1 strings-opt1 --strings-opt1 bool :default true
 option stringOpt2 strings-opt2 --strings-opt2 bool :default false
  internal option2 for strings: constant regexp splitting
 
+option stringIgnNegMembership strings-inm --strings-inm bool :default false
+ internal for strings: ignore negative membership constraints (fragment checking is needed, left to users for now)
+
 expert-option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int16_t :default 256 :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
  the cardinality of the characters used by the theory of strings, default 256
 

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 765fb586e9c9ba86498e3b447a4c2e709ff5460f..2347af3e60ef1575c7b31e8cada839efd97d2e3e 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -716,12 +716,17 @@ void RegExpOpr::firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset )
     std::pair< std::set<unsigned>, SetNodes > p(cset, vset);
     d_fset_cache[r] = p;
 
-    Trace("regexp-fset") << "FSET( " << mkString(r) << " ) = { ";
-    for(std::set<unsigned>::const_iterator itr = cset.begin();
-      itr != cset.end(); itr++) {
-        Trace("regexp-fset") << CVC4::String::convertUnsignedIntToChar(*itr) << ",";
-      }
-    Trace("regexp-fset") << " }" << std::endl;
+    if(Trace.isOn("regexp-fset")) {
+      Trace("regexp-fset") << "FSET(" << mkString(r) << ") = {";
+      for(std::set<unsigned>::const_iterator itr = cset.begin();
+        itr != cset.end(); itr++) {
+          if(itr != cset.begin()) {
+            Trace("regexp-fset") << ",";
+          }
+          Trace("regexp-fset") << CVC4::String::convertUnsignedIntToChar(*itr);
+        }
+      Trace("regexp-fset") << "}" << std::endl;
+    }
   }
 }
 
@@ -1319,7 +1324,7 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node >
     r1 = r2;
     r2 = tmpNode;
   }
-  Trace("regexp-intersect") << "Starting INTERSECT(" << cnt << "):\n  "<< mkString(r1) << ",\n  " << mkString(r2) << std::endl;
+  Trace("regexp-int") << "Starting INTERSECT(" << cnt << "):\n  "<< mkString(r1) << ",\n  " << mkString(r2) << std::endl;
   //if(Trace.isOn("regexp-debug")) {
   //  Trace("regexp-debug") << "... with cache:\n";
   //  for(std::map< PairNodes, Node >::const_iterator itr=cache.begin();
@@ -1372,21 +1377,27 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node >
             Unreachable();
           }
         }
-        if(Trace.isOn("regexp-debug")) {
-          Trace("regexp-debug") << "Try CSET( " << cset.size() << " ) = ";
+        if(Trace.isOn("regexp-int-debug")) {
+          Trace("regexp-int-debug") << "Try CSET(" << cset.size() << ") = {";
           for(std::vector<unsigned>::const_iterator itr = cset.begin();
             itr != cset.end(); itr++) {
             CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) );
-            Trace("regexp-debug") << c << ", ";
+            if(itr != cset.begin()) {
+              Trace("regexp-int-debug") << ", ";
+            }
+            Trace("regexp-int-debug") << c;
           }
-          Trace("regexp-debug") << std::endl;
+          Trace("regexp-int-debug") << std::endl;
         }
         std::map< PairNodes, Node > cacheX;
         for(std::vector<unsigned>::const_iterator itr = cset.begin();
           itr != cset.end(); itr++) {
           CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) );
+          Trace("regexp-int-debug") << "Try character " << c << " ... " << std::endl;
           Node r1l = derivativeSingle(r1, c);
           Node r2l = derivativeSingle(r2, c);
+          Trace("regexp-int-debug") << "  ... got partial(r1,c) = " << mkString(r1l) << std::endl;
+          Trace("regexp-int-debug") << "  ... got partial(r2,c) = " << mkString(r2l) << std::endl;
           Node rt;
           
           if(r1l > r2l) {
@@ -1401,11 +1412,13 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node >
             std::map< PairNodes, Node > cache2(cache);
             cache2[ p ] = NodeManager::currentNM()->mkNode(kind::REGEXP_RV, NodeManager::currentNM()->mkConst(CVC4::Rational(cnt)));
             rt = intersectInternal(r1l, r2l, cache2, cnt+1);
-
-            rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT,
-              NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) );
             cacheX[ pp ] = rt;
           }
+
+          rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT,
+            NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) );
+
+          Trace("regexp-int-debug") << "  ... got p(r1,c) && p(r2,c) = " << mkString(rt) << std::endl;
           vec_nodes.push_back(rt);
         }
         rNode = Rewriter::rewrite( vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] :
@@ -1418,7 +1431,7 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node >
       d_inter_cache[p] = rNode;
     }
   }
-  Trace("regexp-intersect") << "End(" << cnt << ") of INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl;
+  Trace("regexp-int") << "End(" << cnt << ") of INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl;
   return rNode;
 }
 

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 0df551847c0266f8ab021d5a98641e621194e9de..384d4567b4f37f5df7642b08a7bd52045a5bd3b0 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -589,7 +589,9 @@ void TheoryStrings::check(Effort e) {
     //must record string in regular expressions
     if ( atom.getKind() == kind::STRING_IN_REGEXP ) {
       addMembership(assertion);
-      d_equalityEngine.assertPredicate(atom, polarity, fact);
+      //if(polarity || !options::stringIgnNegMembership()) {
+        d_equalityEngine.assertPredicate(atom, polarity, fact);
+      //}
     } else if (atom.getKind() == kind::STRING_STRCTN) {
       if(polarity) {
         d_str_pos_ctn.push_back( atom );
@@ -3460,7 +3462,7 @@ void TheoryStrings::addMembership(Node assertion) {
       }
     }
     lst->push_back( r );
-  } else {
+  } else if(!options::stringIgnNegMembership()) {
     /*if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) {
       int rt;
       Node r2 = d_regexp_opr.complement(r, rt);
@@ -3483,7 +3485,10 @@ void TheoryStrings::addMembership(Node assertion) {
     }
     lst->push_back( r );
   }
-  d_regexp_memberships.push_back( assertion );
+  // old
+  if(polarity || !options::stringIgnNegMembership()) {
+    d_regexp_memberships.push_back( assertion );
+  }
 }
 
 Node TheoryStrings::getNormalString(Node x, std::vector<Node> &nf_exp) {

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index dfec0a7957a8271f2c862f86416c498790730ef3..6fcbdfff332097efd1f0001bcc4cef69076c1f86 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -748,18 +748,26 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
     if(r.getKind() == kind::REGEXP_STAR) {
       retNode = r;
     } else {
+      TNode n1 = Rewriter::rewrite( node[1] );
+      if(!n1.isConst()) {
+        throw LogicException("re.loop contains non-constant integer (1).");
+      }
       CVC4::Rational RMAXINT(LONG_MAX);
-      Assert(node[1].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (1)");
-      unsigned l = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
+      Assert(n1.getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (1)");
+      unsigned l = n1.getConst<Rational>().getNumerator().toUnsignedInt();
       std::vector< Node > vec_nodes;
       for(unsigned i=0; i<l; i++) {
         vec_nodes.push_back(r);
       }
       if(node.getNumChildren() == 3) {
+        TNode n2 = Rewriter::rewrite( node[2] );
+        if(!n2.isConst()) {
+          throw LogicException("re.loop contains non-constant integer (2).");
+        }
         Node n = vec_nodes.size()==0 ? NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(CVC4::String("")))
           : vec_nodes.size()==1 ? r : prerewriteConcatRegExp(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes));
-        Assert(node[2].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (2)");
-        unsigned u = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
+        Assert(n2.getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (2)");
+        unsigned u = n2.getConst<Rational>().getNumerator().toUnsignedInt();
         if(u <= l) {
           retNode = n;
         } else {

diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 8a51ea36ca85c79c56a8769dff3a4a0c08539c55..55059fa77decabafcb86fff232e1a0d96e8f3701 100644 (file)
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -388,18 +388,18 @@ public:
       if (!t.isInteger()) {
         throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 2");
       }
-      if(!(*it).isConst()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 2");
-      }
+      //if(!(*it).isConst()) {
+        //throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 2");
+      //}
       ++it;
       if(it != it_end) {
         t = (*it).getType(check);
         if (!t.isInteger()) {
           throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 3");
         }
-        if(!(*it).isConst()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 3");
-        }
+        //if(!(*it).isConst()) {
+          //throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 3");
+        //}
         //if(++it != it_end) {
         //  throw TypeCheckingExceptionPrivate(n, "too many regexp");
         //}

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 865d05cd2036cabaae8ba2711ffe3604a28a59b2..8a2674ceebe960121a6f65d01721c75b2c6bb3a6 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -37,6 +37,7 @@ TESTS =       \
   model001.smt2 \
   substr001.smt2 \
   regexp001.smt2 \
+  regexp002.smt2 \
   regexp003.smt2 \
   leadingzero001.smt2 \
   loop001.smt2 \
@@ -53,8 +54,8 @@ TESTS =       \
 FAILING_TESTS =
 
 EXTRA_DIST = $(TESTS) \
+  artemis-0512-nonterm.smt2 \
   fmf001.smt2 \
-  regexp002.smt2 \
   type002.smt2
 
 #   slow after changes on Nov 20 : artemis-0512-nonterm.smt2

diff --git a/test/regress/regress0/strings/regexp002.smt2 b/test/regress/regress0/strings/regexp002.smt2
index 18541af4e455b3cbef6fbdc946d63364b5e059b4..8c29ccb3825bff957ee1c0be334f8727eb6de86a 100644 (file)
--- a/test/regress/regress0/strings/regexp002.smt2
+++ b/test/regress/regress0/strings/regexp002.smt2
@@ -1,6 +1,10 @@
 (set-logic QF_S)\r
 (set-info :status sat)\r
 (set-option :strings-exp true)\r
+; this option requires user to check whether the constraint is in the fragment\r
+; currently we do not provide only positive membership constraint checking\r
+; if users use this option but the constraint is not in this fragment, the result will fail\r
+(set-option :strings-inm true)\r
 \r
 (declare-fun x () String)\r
 (declare-fun y () String)\r