bug fix for constant regular expression model building

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f394047fafffb462c9b2f5530063d444b09f7699..67b055d33cc18dd403c52a1f498ca5e60ee8f992 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -479,6 +479,8 @@ void TheoryStrings::preRegisterTerm(TNode n) {
       case kind::STRING_IN_REGEXP: {
         d_out->requirePhase(n, true);
         d_equalityEngine.addTriggerPredicate(n);
+        d_equalityEngine.addTerm(n[0]);
+        d_equalityEngine.addTerm(n[1]);
         break;
       }
       //case kind::STRING_SUBSTR_TOTAL:

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 56f6a2ef0a27ac39af83aa0c8eb5e229b0f0107d..f6c12a2e1e2872ea611597513e2f40c450adfb0e 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -395,6 +395,20 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
     retNode = one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x));
   } else if(node[1].getKind() == kind::REGEXP_STAR && node[1][0].getKind() == kind::REGEXP_SIGMA) {
     retNode = NodeManager::currentNM()->mkConst( true );
+  } else if(node[1].getKind() == kind::REGEXP_CONCAT) {
+    //opt
+    bool flag = true;
+    for(unsigned i=0; i<node[1].getNumChildren(); i++) {
+      if(node[1][i].getKind() != kind::REGEXP_SIGMA) {
+        flag = false;
+        break;
+      }
+    }
+    if(flag) {
+      Node num = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[1].getNumChildren() ) );
+      retNode = num.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x));
+    }
+    //
   } else if(node[1].getKind() == kind::STRING_TO_REGEXP) {
     retNode = x.eqNode(node[1][0]);
   } else if(x != node[0]) {
@@ -702,7 +716,7 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
     retNode = prerewriteConcatRegExp(node);
   } else if(node.getKind() == kind::REGEXP_UNION) {
     retNode = prerewriteOrRegExp(node);
-  }else if(node.getKind() == kind::REGEXP_INTER) {
+  } else if(node.getKind() == kind::REGEXP_INTER) {
     retNode = prerewriteAndRegExp(node);
   } else if(node.getKind() == kind::REGEXP_STAR) {
     if(node[0].getKind() == kind::REGEXP_STAR) {

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 1c62717c8fb494e1df4541403334260022694cdf..cb50bf355ce78a812de20359891aa969e406f71c 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -198,9 +198,13 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
     }
 
     if (!d_equalityEngine->hasTerm(n)) {
-      // Unknown term - return first enumerated value for this type
-      TypeEnumerator te(n.getType());
-      ret = *te;
+      if(n.getType().isRegExp()) { 
+        ret = Rewriter::rewrite(ret);
+      } else {
+        // Unknown term - return first enumerated value for this type
+        TypeEnumerator te(n.getType());
+        ret = *te;
+      }
       d_modelCache[n] = ret;
       return ret;
     }