From 61c78314a1519b5e7be1c45ef9f6cee25b3a10b4 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 6 Dec 2019 11:33:51 -0800 Subject: [PATCH] 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. --- .../strings/theory_strings_preprocess.cpp | 22 ++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) 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; } -- 2.30.2