Fix str to int reduction (#3358)

This fixes a corner case of the str-to-int reduction for the case where the argument is the empty string.

This fixes #3357.

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index d1eef656b6307ab7c61f50096f45e2add2ba05cc..8e057a525d2d5147b3e635e78c3d5394d6a423f1 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -309,6 +309,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     lem = s.eqNode(nm->mkNode(APPLY_UF, us, d_zero));
     conc2.push_back(lem);
 
+    lem = nm->mkNode(GT, lens, d_zero);
+    conc2.push_back(lem);
+
     Node x = nm->mkBoundVar(nm->integerType());
     Node xbv = nm->mkNode(BOUND_VAR_LIST, x);
     Node g =
@@ -343,6 +346,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     // ELSE:
     //   stoit = U( len( s ) ) ^ U( 0 ) = 0 ^
     //   "" = Us( len( s ) ) ^ s = Us( 0 ) ^
+    //   str.len( s ) > 0 ^
     //   forall x. (x>=0 ^ x < str.len(s)) =>
     //     Us( x ) = Ud( x ) ++ Us( x+1 ) ^
     //     U( x+1 ) = ( str.code( Ud( x ) ) - 48 ) + 10*U( x )

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a3ee076898e447e7a7929a73e2c83d993171d28e..3045ea35e208764477a6465d53075ddef137f8fd 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1576,6 +1576,7 @@ set(regress_1_tests
   regress1/strings/issue3090.smt2
   regress1/strings/issue3217.smt2
   regress1/strings/issue3272.smt2
+  regress1/strings/issue3357.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/regress1/strings/issue3357.smt2 b/test/regress/regress1/strings/issue3357.smt2
new file mode 100644 (file)
index 0000000..940245c
--- /dev/null
+++ b/test/regress/regress1/strings/issue3357.smt2
@@ -0,0 +1,18 @@
+(set-logic ALL_SUPPORTED)
+(set-option :strings-exp true)
+(set-info :status unsat)
+(declare-fun a () String)
+(declare-fun b () String)
+(declare-const c String)
+(declare-const d String)
+(declare-const g String)
+(declare-const e String)
+(declare-const f String)
+(assert (or  
+            (and (= d (str.++ e g)) (str.in.re e (re.* (str.to.re "HG4"))) (> 0 (str.to.int g)) (= 1 (str.len e)) (= 2 (str.len (str.substr b 0 (str.len d)))))  
+            (and 
+                (str.in.re (str.replace (str.replace a c "") "T" "") (re.* (re.union (str.to.re "a") (str.to.re "")))) 
+                (= 0 (str.to.int (str.replace (str.replace a c "") "T" "")))))
+)
+(assert (= b (str.++ d f)))
+(check-sat