From 762129d4c7df6563cca451f3d33210cc094bae3d Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 12 Feb 2018 17:45:07 -0500
Subject: [PATCH] fixups to theory_str for regex

---
 src/smt/theory_str.cpp | 18 +++++++++++++-----
 src/smt/theory_str.h   |  1 +
 2 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 8157ceea9..e68a7fa8a 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -6571,7 +6571,7 @@ namespace smt {
             SASSERT(str1.length() == 1);
             SASSERT(str2.length() == 1);
             return 1 + str2[0] - str1[0];
-        } else if (u.re.is_full(re)) {
+        } else if (u.re.is_full_char(re) || u.re.is_full_seq(re)) {
             return 1;
         } else {
             TRACE("str", tout << "WARNING: unknown regex term " << mk_pp(re, get_manager()) << std::endl;);
@@ -6613,7 +6613,7 @@ namespace smt {
             SASSERT(str1.length() == 1);
             SASSERT(str2.length() == 1);
             return 1 + str2[0] - str1[0];
-        } else if (u.re.is_full(re)) {
+        } else if (u.re.is_full_char(re) || u.re.is_full_seq(re)) {
             return 1;
         } else {
             TRACE("str", tout << "WARNING: unknown regex term " << mk_pp(re, get_manager()) << std::endl;);
@@ -6649,8 +6649,10 @@ namespace smt {
             }
         } else if (u.re.is_range(re)) {
             return true;
-        } else if (u.re.is_full(re)) {
+        } else if (u.re.is_full_char(re)) {
             return true;
+        } else if (u.re.is_full_seq(re)) {
+            return false; // generally unbounded
         } else if (u.re.is_complement(re)) {
             // TODO can we do better?
             return false;
@@ -6712,8 +6714,10 @@ namespace smt {
             SASSERT(str1.length() == 1);
             SASSERT(str2.length() == 1);
             lens.insert(1);
-        } else if (u.re.is_full(re)) {
+        } else if (u.re.is_full_char(re)) {
             lens.insert(1);
+        } else if (u.re.is_full_seq(re)) {
+            lens.reset();
         } else if (u.re.is_complement(re)) {
             lens.reset();
         } else {
@@ -6828,9 +6832,13 @@ namespace smt {
             SASSERT(str2.length() == 1);
             expr_ref retval(ctx.mk_eq_atom(lenVar, m_autil.mk_numeral(rational::one(), true)), m);
             return retval;
-        } else if (u.re.is_full(re)) {
+        } else if (u.re.is_full_char(re)) {
             expr_ref retval(ctx.mk_eq_atom(lenVar, m_autil.mk_numeral(rational::one(), true)), m);
             return retval;
+        } else if (u.re.is_full_seq(re)) {
+            // match any unbounded string
+            expr_ref retval(m_autil.mk_ge(lenVar, m_autil.mk_numeral(rational::zero(), true)), m);
+            return retval;
         } else if (u.re.is_complement(re)) {
             // skip complement for now, in general this is difficult to predict
             expr_ref retval(m_autil.mk_ge(lenVar, m_autil.mk_numeral(rational::zero(), true)), m);
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index ef0bbf0ee..506726bc6 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -745,6 +745,7 @@ protected:
     void new_diseq_eh(theory_var, theory_var) override;
 
     theory* mk_fresh(context*) override { return alloc(theory_str, get_manager(), m_params); }
+    void init(context * ctx) override;
     void init_search_eh() override;
     void add_theory_assumptions(expr_ref_vector & assumptions) override;
     lbool validate_unsat_core(expr_ref_vector & unsat_core) override;