From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 6 Dec 2019 19:33:51 +0000 (-0800)
Subject: Add lemma for str.to.int/int.to.str (#3541)
X-Git-Tag: cvc5-1.0.0~3787
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=61c78314a1519b5e7be1c45ef9f6cee25b3a10b4;p=cvc5.git

Add lemma for str.to.int/int.to.str (#3541)

This commit adds a lemma to our encoding of `str.to.int` and
`int.to.str` that relates the integer value in the encodings to the
value of partial results.
---

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 8e057a525..dd939e944 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -230,7 +230,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
         nm->mkNode(GEQ, c, nm->mkNode(ITE, leadingZeroPos, d_one, d_zero)),
         nm->mkNode(LT, c, ten));
 
-    lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eqs, eq, cb));
+    Node ux1lem = nm->mkNode(GEQ, n, ux1);
+
+    lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eqs, eq, cb, ux1lem));
     lem = nm->mkNode(FORALL, xbv, lem);
     conc.push_back(lem);
 
@@ -248,11 +250,15 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     //   forall x. (x>=0 ^ x < str.len(itost)) =>
     //     Us( x ) = Ud( x ) ++ Us( x+1 ) ^
     //     U( x+1 ) = (str.code( Ud( x ) )-48) + 10*U( x ) ^
-    //     ite( x=0 AND str.len(itost)>1, 49, 48 ) <= str.code( Ud( x ) ) < 58
+    //     ite( x=0 AND str.len(itost)>1, 49, 48 ) <= str.code( Ud( x ) ) < 58 ^
+    //     n >= U(x + 1)
     // ELSE
     //   itost = ""
     // thus:
     //   int.to.str( n ) = itost
+    //
+    // Note: The conjunct `n >= U(x + 1)` is not needed for correctness but is
+    // just an optimization.
 
     // In the above encoding, we use Us/Ud to introduce a chain of strings
     // that allow us to refer to each character substring of itost. Notice this
@@ -328,7 +334,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node cb =
         nm->mkNode(AND, nm->mkNode(GEQ, c, d_zero), nm->mkNode(LT, c, ten));
 
-    lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eqs, eq, cb));
+    Node ux1lem = nm->mkNode(GEQ, stoit, ux1);
+
+    lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eqs, eq, cb, ux1lem));
     lem = nm->mkNode(FORALL, xbv, lem);
     conc2.push_back(lem);
 
@@ -349,9 +357,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     //   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 )
-    //     48 <= str.code( Ud( x ) ) < 58
+    //     U( x+1 ) = ( str.code( Ud( x ) ) - 48 ) + 10*U( x ) ^
+    //     48 <= str.code( Ud( x ) ) < 58 ^
+    //     stoit >= U( x+1 )
     // Thus, str.to.int( s ) = stoit
+    //
+    // Note: The conjunct `stoit >= U( x+1 )` is not needed for correctness but
+    // is just an optimization.
 
     retNode = stoit;
   }