From cea82f89852e3ee2b051627c3402bd23827f6c52 Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Mon, 22 Dec 2014 16:22:42 -0600
Subject: [PATCH] bug fix for constant regular expression model building

---
 src/theory/strings/theory_strings.cpp          |  2 ++
 src/theory/strings/theory_strings_rewriter.cpp | 16 +++++++++++++++-
 src/theory/theory_model.cpp                    | 10 +++++++---
 3 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f394047fa..67b055d33 100644
--- 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 56f6a2ef0..f6c12a2e1 100644
--- 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 1c62717c8..cb50bf355 100644
--- 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;
     }
-- 
2.30.2