Z3str3: Add consistency checks for string-integer conversion terms in model construction (#4551)

* z3str3: check consistency of str.to_int in fixed length solver

* z3str3: add similar check for int.to_str as well

* z3str3: refactor string-integer conversion check and add post checks for model construction

src/smt/theory_str.cpp

@@ -8134,6 +8134,31 @@ namespace smt {
         return 0;
     }
 
+    // Attempts to convert a string to a non-negative integer.
+    // Returns true if this can be done in a valid way, placing the converted value in the argument.
+    // Otherwise, returns false, if str is empty or contains non-digit characters.
+    bool theory_str::string_integer_conversion_valid(zstring str, rational& converted) const {
+        bool valid = true;
+        converted = rational::zero();
+        rational ten(10);
+        if (str.length() == 0) {
+            return false;
+        } else {
+            for (unsigned i = 0; i < str.length(); ++i) {
+                if (!('0' <= str[i] && str[i] <= '9')) {
+                    return false;
+                } else {
+                    // accumulate
+                    char digit = (int)str[i];
+                    std::string sDigit(1, digit);
+                    int val = atoi(sDigit.c_str());
+                    converted = (ten * converted) + rational(val);
+                }
+            }
+            return true;
+        }
+    }
+
     // Check agreement between integer and string theories for the term a = (str.to-int S).
     // Returns true if axioms were added, and false otherwise.
     bool theory_str::finalcheck_str2int(app * a) {
@@ -8189,27 +8214,9 @@ namespace smt {
         if (S_hasEqcValue) {
             zstring str;
             u.str.is_string(S_str, str);
-            bool valid = true;
             rational convertedRepresentation(0);
-            rational ten(10);
-            if (str.length() == 0) {
-                valid = false;
-            } else {
-                for (unsigned i = 0; i < str.length(); ++i) {
-                    if (!('0' <= str[i] && str[i] <= '9')) {
-                        valid = false;
-                        break;
-                    } else {
-                        // accumulate
-                        char digit = (int)str[i];
-                        std::string sDigit(1, digit);
-                        int val = atoi(sDigit.c_str());
-                        convertedRepresentation = (ten * convertedRepresentation) + rational(val);
-                    }
-                }
-            }
             // TODO this duplicates code a bit, we can simplify the branch on "conclusion" only
-            if (valid) {
+            if (string_integer_conversion_valid(str, convertedRepresentation)) {
                 expr_ref premise(ctx.mk_eq_atom(S, mk_string(str)), m);
                 expr_ref conclusion(ctx.mk_eq_atom(a, m_autil.mk_numeral(convertedRepresentation, true)), m);
                 expr_ref axiom(rewrite_implication(premise, conclusion), m);
@@ -8263,22 +8270,7 @@ namespace smt {
                 }
                 // nonempty string --> convert to correct integer value, or disallow it
                 rational convertedRepresentation(0);
-                rational ten(10);
+                if (string_integer_conversion_valid(Sval, convertedRepresentation)) {
-                bool conversionOK = true;
-                for (unsigned i = 0; i < Sval.length(); ++i) {
-                    char digit = (int)Sval[i];
-                    if (isdigit((int)digit)) {
-                        std::string sDigit(1, digit);
-                        int val = atoi(sDigit.c_str());
-                        convertedRepresentation = (ten * convertedRepresentation) + rational(val);
-                    } else {
-                        // not a digit, invalid
-                        TRACE("str", tout << "str.from-int argument contains non-digit character '" << digit << "'" << std::endl;);
-                        conversionOK = false;
-                        break;
-                    }
-                }
-                if (conversionOK) {
                     expr_ref premise(ctx.mk_eq_atom(a, mk_string(Sval)), m);
                     expr_ref conclusion(ctx.mk_eq_atom(N, m_autil.mk_numeral(convertedRepresentation, true)), m);
                     expr_ref axiom(rewrite_implication(premise, conclusion), m);

src/smt/theory_str.h

@@ -753,6 +753,7 @@ protected:
 
     bool finalcheck_str2int(app * a);
     bool finalcheck_int2str(app * a);
+    bool string_integer_conversion_valid(zstring str, rational& converted) const;
 
     lbool fixed_length_model_construction(expr_ref_vector formulas, expr_ref_vector &precondition,
             expr_ref_vector& free_variables,

src/smt/theory_str_mc.cpp

@@ -1111,6 +1111,92 @@ namespace smt {
             }
         }
 
+        // Check consistency of all string-integer conversion terms wrt. integer theory before we solve,
+        // possibly generating additional constraints for the bit-vector solver.
+        {
+            arith_value v(get_manager());
+            v.init(&get_context());
+            for (auto e : string_int_conversion_terms) {
+                TRACE("str_fl", tout << "pre-run check str-int term " << mk_pp(e, get_manager()) << std::endl;);
+                expr* _arg;
+                if (u.str.is_stoi(e, _arg)) {
+                    expr_ref arg(_arg, m);
+                    rational slen;
+                    if (!fixed_length_get_len_value(arg, slen)) {
+                        expr_ref stoi_cex(m_autil.mk_ge(mk_strlen(arg), mk_int(0)), m);
+                        assert_axiom(stoi_cex);
+                        add_persisted_axiom(stoi_cex);
+                        return l_undef;
+                    }
+                    TRACE("str_fl", tout << "length of term is " << slen << std::endl;);
+
+                    rational ival;
+                    if (v.get_value(e, ival)) {
+                        TRACE("str_fl", tout << "integer theory assigns " << ival << " to " << mk_pp(e, get_manager()) << std::endl;);
+                        // if ival is non-negative, because we know the length of arg, we can add a character constraint for arg
+                        if (ival.is_nonneg()) {
+                            zstring ival_str(ival.to_string().c_str());
+                            zstring padding;
+                            for (rational i = rational::zero(); i < slen - rational(ival_str.length()); ++i) {
+                                padding = padding + zstring("0");
+                            }
+                            zstring arg_val = padding + ival_str;
+                            expr_ref stoi_cex(m);
+                            expr_ref arg_char_expr(mk_string(arg_val), m);
+                            
+                            // Add (e == ival) as a precondition.
+                            precondition.push_back(m.mk_eq(e, mk_int(ival)));
+                            // Assert (arg == arg_chars) in the subsolver.
+                            if (!fixed_length_reduce_eq(subsolver, arg, arg_char_expr, stoi_cex)) {
+                                assert_axiom(stoi_cex);
+                                add_persisted_axiom(stoi_cex);
+                                return l_undef;
+                            }
+                        }
+                    } else {
+                        TRACE("str_fl", tout << "integer theory has no assignment for " << mk_pp(e, get_manager()) << std::endl;);
+                        // consistency needs to be checked after the string is assigned
+                    }
+                } else if (u.str.is_itos(e, _arg)) {
+                    expr_ref arg(_arg, m);
+                    rational slen;
+                    if (!fixed_length_get_len_value(e, slen)) {
+                        expr_ref stoi_cex(m_autil.mk_ge(mk_strlen(e), mk_int(0)), m);
+                        assert_axiom(stoi_cex);
+                        add_persisted_axiom(stoi_cex);
+                        return l_undef;
+                    }
+                    TRACE("str_fl", tout << "length of term is " << slen << std::endl;);
+                    rational ival;
+                    if (v.get_value(arg, ival)) {
+                        TRACE("str_fl", tout << "integer theory assigns " << ival << " to " << mk_pp(arg, get_manager()) << std::endl;);
+                        zstring ival_str;
+                        if (ival.is_neg()) {
+                            // e must be the empty string, i.e. have length 0
+                            ival_str = zstring("");
+                        } else {
+                            // e must be equal to the string representation of ival
+                            ival_str = zstring(ival.to_string().c_str());
+                        }
+                        // Add (arg == ival) as a precondition.
+                        precondition.push_back(m.mk_eq(arg, mk_int(ival)));
+                        // Assert (e == ival_str) in the subsolver.
+                        expr_ref itos_cex(m);
+                        expr_ref _e(e, m);
+                        expr_ref arg_char_expr(mk_string(ival_str), m);
+                        if (!fixed_length_reduce_eq(subsolver, _e, arg_char_expr, itos_cex)) {
+                            assert_axiom(itos_cex);
+                            add_persisted_axiom(itos_cex);
+                            return l_undef;
+                        }
+                    } else {
+                        TRACE("str_fl", tout << "integer theory has no assignment for " << mk_pp(arg, get_manager()) << std::endl;);
+                        // consistency needs to be checked after the string is assigned
+                    }
+                }
+            }
+        }
+
         for (auto e : fixed_length_used_len_terms) {
             expr * var = &e.get_key();
             rational val = e.get_value();
@@ -1188,6 +1274,91 @@ namespace smt {
                 model.insert(var, strValue);
                 subst.insert(var, mk_string(strValue));
             }
+
+            // Check consistency of string-integer conversion terms after the search.
+            {
+                scoped_ptr<expr_replacer> replacer = mk_default_expr_replacer(m, false);
+                replacer->set_substitution(&subst);
+                th_rewriter rw(m);
+                arith_value v(get_manager());
+                v.init(&get_context());
+                for (auto e : string_int_conversion_terms) {
+                    TRACE("str_fl", tout << "post-run check str-int term " << mk_pp(e, get_manager()) << std::endl;);
+                    expr* _arg;
+                    if (u.str.is_stoi(e, _arg)) {
+                        expr_ref arg(_arg, m);
+                        rational ival;
+                        if (v.get_value(e, ival)) {
+                            expr_ref arg_subst(arg, m);
+                            (*replacer)(arg, arg_subst);
+                            rw(arg_subst);
+                            TRACE("str_fl", tout << "ival = " << ival << ", string arg evaluates to " << mk_pp(arg_subst, m) << std::endl;);
+
+                            symbol arg_str;
+                            if (u.str.is_string(arg_subst, arg_str)) {
+                                zstring arg_zstr(arg_str.bare_str());
+                                rational arg_value;
+                                if (string_integer_conversion_valid(arg_zstr, arg_value)) {
+                                    if (ival != arg_value) {
+                                        // contradiction
+                                        expr_ref cex(m.mk_not(m.mk_and(ctx.mk_eq_atom(arg, mk_string(arg_zstr)), ctx.mk_eq_atom(e, mk_int(ival)))), m);
+                                        assert_axiom(cex);
+                                        return l_undef;
+                                    }
+                                } else {
+                                    if (!ival.is_minus_one()) {
+                                        expr_ref cex(m.mk_not(m.mk_and(ctx.mk_eq_atom(arg, mk_string(arg_zstr)), ctx.mk_eq_atom(e, mk_int(ival)))), m);
+                                        assert_axiom(cex);
+                                        return l_undef;
+                                    }
+                                }
+                            }
+                        }
+                    } else if (u.str.is_itos(e, _arg)) {
+                        expr_ref arg(_arg, m);
+                        rational ival;
+                        if (v.get_value(arg, ival)) {
+                            expr_ref e_subst(e, m);
+                            (*replacer)(e, e_subst);
+                            rw(e_subst);
+                            TRACE("str_fl", tout << "ival = " << ival << ", string arg evaluates to " << mk_pp(e_subst, m) << std::endl;);
+
+                            symbol e_str;
+                            if (u.str.is_string(e_subst, e_str)) {
+                                zstring e_zstr(e_str.bare_str());
+                                // if arg is negative, e must be empty
+                                // if arg is non-negative, e must be valid AND cannot contain leading zeroes
+
+                                if (ival.is_neg()) {
+                                    if (!e_zstr.empty()) {
+                                        // contradiction
+                                        expr_ref cex(ctx.mk_eq_atom(m_autil.mk_le(arg, mk_int(-1)), ctx.mk_eq_atom(e, mk_string(""))), m);
+                                        assert_axiom(cex);
+                                        return l_undef;
+                                    }
+                                } else {
+                                    rational e_value;
+                                    if (string_integer_conversion_valid(e_zstr, e_value)) {
+                                        // e contains leading zeroes if its first character is 0 but converted to something other than 0
+                                        if (e_zstr[0] == '0' && !e_value.is_zero()) {
+                                            // contradiction
+                                            expr_ref cex(m.mk_not(m.mk_and(ctx.mk_eq_atom(arg, mk_int(ival)), ctx.mk_eq_atom(e, mk_string(e_zstr)))), m);
+                                            assert_axiom(cex);
+                                            return l_undef;
+                                        }
+                                    } else {
+                                        // contradiction
+                                        expr_ref cex(m.mk_not(m.mk_and(ctx.mk_eq_atom(arg, mk_int(ival)), ctx.mk_eq_atom(e, mk_string(e_zstr)))), m);
+                                        assert_axiom(cex);
+                                        return l_undef;
+                                    }
+                                }
+                            }
+                        }
+                    }
+                }
+            }
+
             // TODO insert length values into substitution table as well?
             if (m_params.m_FixedLengthRefinement) {
                 scoped_ptr<expr_replacer> replacer = mk_default_expr_replacer(m, false);