From b045d1d06f2d28957ccca6ed7d9e6458b4a96b79 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 10 May 2017 10:35:38 -0500
Subject: [PATCH] Do not split on cardinality for string equivalence classes
 with non-constant lengths if disequalities already imply sufficient lower
 bound. Fixes bug 799.

---
 src/theory/strings/theory_strings.cpp         | 31 ++++++++++++++++---
 test/regress/regress0/strings/Makefile.am     |  3 +-
 test/regress/regress0/strings/bug799-min.smt2 | 18 +++++++++++
 3 files changed, 47 insertions(+), 5 deletions(-)
 create mode 100644 test/regress/regress0/strings/bug799-min.smt2

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 42e43b543..6526b68cf 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2212,7 +2212,7 @@ void TheoryStrings::getNormalForms( Node &eqc, std::vector< std::vector< Node >
     normal_forms_exp_depend.push_back( std::map< Node, std::map< bool, int > >() );
   }else{
     if(Trace.isOn("strings-solve")) {
-      Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl;
+      Trace("strings-solve") << "--- Normal forms for equivalance class " << eqc << " : " << std::endl;
       for( unsigned i=0; i<normal_forms.size(); i++ ) {
         Trace("strings-solve") << "#" << i << " (from " << normal_form_src[i] << ") : ";
         for( unsigned j=0; j<normal_forms[i].size(); j++ ) {
@@ -3725,9 +3725,32 @@ void TheoryStrings::checkCardinality() {
         card_need++;
       }
       Trace("strings-card") << "Need length " << card_need << " for this number of strings (where alphabet size is " << d_card_size << ")." << std::endl;
-      Node cmp = NodeManager::currentNM()->mkNode( kind::GEQ, lr, NodeManager::currentNM()->mkConst( Rational( card_need ) ) );
-      cmp = Rewriter::rewrite( cmp );
-      if( cmp!=d_true ){
+      //check if we need to split
+      bool needsSplit = true;
+      if( lr.isConst() ){
+        // if constant, compare
+        Node cmp = NodeManager::currentNM()->mkNode( kind::GEQ, lr, NodeManager::currentNM()->mkConst( Rational( card_need ) ) );
+        cmp = Rewriter::rewrite( cmp );
+        needsSplit = cmp!=d_true;
+      }else{
+        // find the minimimum constant that we are unknown to be disequal from, or otherwise stop if we increment such that cardinality does not apply
+        unsigned r=0; 
+        bool success = true;
+        while( r<card_need && success ){
+          Node rr = NodeManager::currentNM()->mkConst<Rational>( Rational(r) );
+          if( areDisequal( rr, lr ) ){
+            r++;
+          }else{
+            success = false;
+          }
+        }
+        if( r>0 ){
+          Trace("strings-card") << "Symbolic length " << lr << " must be at least " << r << " due to constant disequalities." << std::endl;
+        }
+        needsSplit = r<card_need;
+      }
+
+      if( needsSplit ){
         unsigned int int_k = (unsigned int)card_need;
         for( std::vector< Node >::iterator itr1 = cols[i].begin();
             itr1 != cols[i].end(); ++itr1) {
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 41c500170..5c89c8472 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -87,7 +87,8 @@ TESTS = \
   strings-index-empty.smt2 \
   bug768.smt2 \
   username_checker_min.smt2 \
-  repl-empty-sem.smt2
+  repl-empty-sem.smt2 \
+  bug799-min.smt2
 
 FAILING_TESTS =
 
diff --git a/test/regress/regress0/strings/bug799-min.smt2 b/test/regress/regress0/strings/bug799-min.smt2
new file mode 100644
index 000000000..06acffc97
--- /dev/null
+++ b/test/regress/regress0/strings/bug799-min.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --incremental --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+
+(declare-fun u () String)
+(declare-fun s () String)
+
+(assert (= (str.len u) 9))
+(assert (= (str.at u 1) s))
+(assert (= (str.at u 2) "4"))
+(assert (= (str.at u 7) "5"))
+(assert (= (str.at u 8) "6"))
+
+(push 1)
+(assert (str.in.re s (re.range "0" "3")))
+
+(check-sat)
-- 
2.30.2