smt2: lower empty_string and decimal of_int to SMT-LIB

src/solvers/smt2/smt2_conv.cpp

@@ -2786,6 +2786,23 @@ void smt2_convt::convert_expr(const exprt &expr)
     //   is_prefix(prefix, s)       -> (str.prefixof prefix s)
     //   is_suffix(suffix, s)       -> (str.suffixof suffix s)
     //   replace(s, old, new)       -> (str.replace s old new) : first match
+    //                                 only; note that symex constant
+    //                                 propagation and the SAT string solver
+    //                                 give replace replace-every-match
+    //                                 semantics
+    //   replace_all(s, old, new)   -> (str.replace_all s old new) : every
+    //                                 match; s unchanged if old is ""
+    //   from_code(i)               -> (str.from_code i) : Int operand; ""
+    //                                 unless 0 <= i <= 196607
+    //   to_code(s)                 -> (str.to_code s)   : Int result; -1
+    //                                 unless |s| = 1
+    //   from_int(n)                -> (str.from_int n)  : Int operand; ""
+    //                                 for n < 0 (unlike of_int, which
+    //                                 produces a leading '-')
+    //   of_int(n[, 10])            -> (ite (>= n 0) (str.from_int n)
+    //                                   (str.++ "-" (str.from_int (- n))))
+    //                                 : Int operand, decimal only
+    //   empty_string()             -> ""
     //   equal(s, t)                -> (= s t)
     //   index_of(s, sub[, off])    -> (str.indexof s sub off) : off defaults 0
     //   startswith(s, prefix)      -> (str.prefixof prefix s)
@@ -2794,9 +2811,11 @@ void smt2_convt::convert_expr(const exprt &expr)
     // and the regex operators map to str.to_re / str.in_re and the re.* family
     // (re.range, re.++, re.*, re.+, re.opt, re.loop, re.union, re.inter,
     // re.comp, re.diff, re.all, re.allchar, re.none). Built-ins without an
-    // exact SMT-LIB theory-of-strings counterpart (e.g. compare_to, of_int,
-    // parse_int, format, case folding, trim) are intentionally not lowered and
-    // fall through to the generic function-application handling below.
+    // exact SMT-LIB theory-of-strings counterpart (e.g. compare_to, of_int with
+    // a radix other than 10, parse_int, format, case folding, trim) are
+    // intentionally not lowered and fall through to the generic
+    // function-application handling below, which makes them uninterpreted
+    // functions.
     //
     // Note: this lowering is specific to the (non-incremental) smt2_convt
     // back-end. The incremental SMT back-end uses a separate converter
@@ -2826,6 +2845,10 @@ void smt2_convt::convert_expr(const exprt &expr)
       {ID_cprover_string_is_prefix_func, "str.prefixof"},
       {ID_cprover_string_is_suffix_func, "str.suffixof"},
       {ID_cprover_string_replace_func, "str.replace"},
+      {ID_cprover_string_replace_all_func, "str.replace_all"},
+      {ID_cprover_string_from_code_func, "str.from_code"},
+      {ID_cprover_string_to_code_func, "str.to_code"},
+      {ID_cprover_string_from_int_func, "str.from_int"},
       {ID_cprover_string_equal_func, "="},
       // regex operators
       {ID_cprover_string_to_regex_func, "str.to_re"},
@@ -2853,10 +2876,17 @@ void smt2_convt::convert_expr(const exprt &expr)
     const bool is_endswith = fn_id == ID_cprover_string_endswith_func;
     const bool is_is_empty = fn_id == ID_cprover_string_is_empty_func;
     const bool is_regex_loop = fn_id == ID_cprover_regex_loop_func;
+    const bool is_empty_string = fn_id == ID_cprover_string_empty_string_func;
+    // of_int with a radix other than 10 has no SMT-LIB counterpart.
+    const bool is_of_int =
+      fn_id == ID_cprover_string_of_int_func &&
+      (args.size() == 1 ||
+       (args.size() == 2 && args[1].is_constant() &&
+        numeric_cast<mp_integer>(to_constant_expr(args[1])) == mp_integer{10}));
 
     if(
       !smt_name.empty() || is_index_of || is_startswith || is_endswith ||
-      is_is_empty || is_regex_loop)
+      is_is_empty || is_regex_loop || is_empty_string || is_of_int)
     {
       // Soundness guard: this native lowering expects SMT-LIB-native operands.
       // The same cprover_string_*_func ids are also used with the
@@ -2876,6 +2906,25 @@ void smt2_convt::convert_expr(const exprt &expr)
         }
       }
 
+      // The code-point and integer conversions are Int-sorted in SMT-LIB;
+      // reject operands or results of any other sort (e.g. bit-vectors)
+      // instead of emitting SMT-LIB that the solver rejects.
+      const bool int_operand = fn_id == ID_cprover_string_from_code_func ||
+                               fn_id == ID_cprover_string_from_int_func ||
+                               is_of_int;
+      const bool int_result = fn_id == ID_cprover_string_to_code_func;
+      if(
+        (int_operand || int_result) &&
+        ((!is_of_int && args.size() != 1) ||
+         (int_operand && args[0].type().id() != ID_integer) ||
+         (int_result && expr.type().id() != ID_integer)))
+      {
+        throw unsupported_operation_exceptiont{
+          "string built-in '" + id2string(fn_id) +
+          "' expects a single Int-sorted (integer) operand or an "
+          "Int-sorted result in the SMT-LIB string lowering"};
+      }
+
       if(is_index_of)
       {
         // str.indexof requires three operands; default the start offset to the
@@ -2903,6 +2952,30 @@ void smt2_convt::convert_expr(const exprt &expr)
         convert_expr(args[0]);
         out << ')';
       }
+      else if(is_empty_string)
+      {
+        // empty_string() -> ""
+        if(!args.empty() || expr.type().id() != ID_string)
+        {
+          throw unsupported_operation_exceptiont{
+            "string built-in '" + id2string(fn_id) +
+            "' expects no operands and a String result in the SMT-LIB "
+            "string lowering"};
+        }
+        out << "\"\"";
+      }
+      else if(is_of_int)
+      {
+        // of_int(n[, 10]): the decimal representation of n, with a leading
+        // '-' for negative n, whereas str.from_int yields "" for n < 0.
+        out << "(ite (>= ";
+        convert_expr(args[0]);
+        out << " 0) (str.from_int ";
+        convert_expr(args[0]);
+        out << ") (str.++ \"-\" (str.from_int (- ";
+        convert_expr(args[0]);
+        out << "))))";
+      }
       else if(is_is_empty)
       {
         // is_empty(s) -> (= s "")

src/util/irep_ids.def

@@ -656,6 +656,10 @@ IREP_ID_ONE(cprover_string_parse_int_func)
 IREP_ID_ONE(cprover_string_is_valid_int_func)
 IREP_ID_ONE(cprover_string_is_valid_long_func)
 IREP_ID_ONE(cprover_string_replace_func)
+IREP_ID_ONE(cprover_string_replace_all_func)
+IREP_ID_ONE(cprover_string_from_code_func)
+IREP_ID_ONE(cprover_string_to_code_func)
+IREP_ID_ONE(cprover_string_from_int_func)
 IREP_ID_ONE(cprover_string_set_length_func)
 IREP_ID_ONE(cprover_string_startswith_func)
 IREP_ID_ONE(cprover_string_substring_func)

unit/solvers/smt2/smt2_conv.cpp

@@ -535,6 +535,56 @@ TEST_CASE(
     REQUIRE(get_assert(eq) == "(assert (= s1 s2))");
   }
 
+  SECTION("string operators replace_all/from_code/to_code/from_int")
+  {
+    const typet int_type{ID_integer};
+
+    // replace_all replaces every occurrence (str.replace_all), unlike
+    // replace (str.replace, first occurrence only).
+    const auto repl_all = string_builtin_app(
+      ID_cprover_string_replace_all_func, {s1, s2, s1}, string_type);
+    const auto c_repl_all = string_builtin_app(
+      ID_cprover_string_contains_func, {repl_all, s2}, bool_typet{});
+    REQUIRE(
+      get_assert(c_repl_all) ==
+      "(assert (str.contains (str.replace_all s1 s2 s1) s2))");
+
+    // from_code: the single-char string for a code point (str.from_code).
+    const auto fc = string_builtin_app(
+      ID_cprover_string_from_code_func,
+      {from_integer(102, int_type)},
+      string_type);
+    const auto c_fc = string_builtin_app(
+      ID_cprover_string_contains_func, {fc, s1}, bool_typet{});
+    REQUIRE(
+      get_assert(c_fc) == "(assert (str.contains (str.from_code 102) s1))");
+
+    // to_code: the code point of a single-char string, an Int result
+    // (str.to_code; -1 unless the string has length 1). Composed under an
+    // Int operand here to exercise nesting.
+    const auto tc =
+      string_builtin_app(ID_cprover_string_to_code_func, {s2}, int_type);
+    const auto at_tc =
+      string_builtin_app(ID_cprover_string_char_at_func, {s1, tc}, string_type);
+    const auto c_tc = string_builtin_app(
+      ID_cprover_string_contains_func, {at_tc, s1}, bool_typet{});
+    REQUIRE(
+      get_assert(c_tc) ==
+      "(assert (str.contains (str.at s1 (str.to_code s2)) s1))");
+
+    // from_int: the decimal string of a non-negative integer (str.from_int;
+    // SMT-LIB defines it for naturals only -- negative values yield "" and a
+    // front-end needing sign support composes it, e.g.
+    // ite(n < 0, "-" ++ from_int(-n), from_int(n))).
+    const auto fi =
+      string_builtin_app(ID_cprover_string_from_int_func, {tc}, string_type);
+    const auto c_fi = string_builtin_app(
+      ID_cprover_string_contains_func, {fi, s1}, bool_typet{});
+    REQUIRE(
+      get_assert(c_fi) ==
+      "(assert (str.contains (str.from_int (str.to_code s2)) s1))");
+  }
+
   SECTION("regex range/concat/plus/union/inter/comp operators")
   {
     const auto re1 =
@@ -619,6 +669,149 @@ TEST_CASE(
       ID_cprover_string_contains_func, {arr, s2}, bool_typet{});
     REQUIRE_THROWS(get_assert(contains));
   }
+
+  SECTION("Int-sorted string conversions reject other sorts and arities")
+  {
+    const signedbv_typet s32{32};
+    const auto fc_bv = string_builtin_app(
+      ID_cprover_string_from_code_func, {from_integer(102, s32)}, string_type);
+    REQUIRE_THROWS(get_assert(equal_exprt{fc_bv, s1}));
+
+    const auto fc_two = string_builtin_app(
+      ID_cprover_string_from_code_func,
+      {from_integer(102, integer_typet{}), from_integer(102, integer_typet{})},
+      string_type);
+    REQUIRE_THROWS(get_assert(equal_exprt{fc_two, s1}));
+
+    const auto tc_bv =
+      string_builtin_app(ID_cprover_string_to_code_func, {s2}, s32);
+    REQUIRE_THROWS(get_assert(equal_exprt{tc_bv, from_integer(102, s32)}));
+
+    const auto oi_bv = string_builtin_app(
+      ID_cprover_string_of_int_func, {from_integer(102, s32)}, string_type);
+    REQUIRE_THROWS(get_assert(equal_exprt{oi_bv, s1}));
+
+    const auto es_arg = string_builtin_app(
+      ID_cprover_string_empty_string_func, {s1}, string_type);
+    REQUIRE_THROWS(get_assert(equal_exprt{es_arg, s1}));
+  }
+
+  SECTION("of_int with a radix other than 10 is not lowered")
+  {
+    const auto oi_hex = string_builtin_app(
+      ID_cprover_string_of_int_func,
+      {from_integer(102, integer_typet{}), from_integer(16, integer_typet{})},
+      string_type);
+    REQUIRE(
+      get_assert(equal_exprt{oi_hex, s1}) ==
+      "(assert (= (cprover_string_of_int_func 102 16) s1))");
+  }
+}
+
+/// Decide `lhs != expected` with Z3; UNSAT shows that the lowering of `lhs`
+/// evaluates to `expected`.
+static decision_proceduret::resultt
+z3_disproves(const exprt &lhs, const exprt &expected)
+{
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+  null_message_handlert message_handler;
+  smt2_dect smt2_dec{
+    ns, "unit test", "", "ALL", smt2_dect::solvert::Z3, "", message_handler};
+  smt2_dec << notequal_exprt{lhs, expected};
+  return smt2_dec();
+}
+
+TEST_CASE(
+  "smt2_convt string conversions evaluated by Z3",
+  "[core][solvers][smt2]")
+{
+  const typet string_type{ID_string};
+  const integer_typet int_type;
+  const auto str = [&](const char *v)
+  { return constant_exprt{v, string_type}; };
+  const auto num = [&](long v) { return from_integer(v, int_type); };
+  const auto unsat = decision_proceduret::resultt::D_UNSATISFIABLE;
+
+  // replace_all replaces every match; replace only the first one.
+  REQUIRE(
+    z3_disproves(
+      string_builtin_app(
+        ID_cprover_string_replace_all_func,
+        {str("aXaXa"), str("X"), str("Y")},
+        string_type),
+      str("aYaYa")) == unsat);
+  REQUIRE(
+    z3_disproves(
+      string_builtin_app(
+        ID_cprover_string_replace_func,
+        {str("aXaXa"), str("X"), str("Y")},
+        string_type),
+      str("aYaXa")) == unsat);
+  // An empty pattern leaves the string unchanged (unlike Java and Python).
+  REQUIRE(
+    z3_disproves(
+      string_builtin_app(
+        ID_cprover_string_replace_all_func,
+        {str("abc"), str(""), str("x")},
+        string_type),
+      str("abc")) == unsat);
+
+  // from_code: "" outside [0, 196607].
+  REQUIRE(
+    z3_disproves(
+      string_builtin_app(
+        ID_cprover_string_from_code_func, {num(102)}, string_type),
+      str("f")) == unsat);
+  REQUIRE(
+    z3_disproves(
+      string_builtin_app(
+        ID_cprover_string_from_code_func, {num(196608)}, string_type),
+      str("")) == unsat);
+
+  // to_code: -1 unless the string has length 1.
+  REQUIRE(
+    z3_disproves(
+      string_builtin_app(ID_cprover_string_to_code_func, {str("f")}, int_type),
+      num(102)) == unsat);
+  REQUIRE(
+    z3_disproves(
+      string_builtin_app(ID_cprover_string_to_code_func, {str("ab")}, int_type),
+      num(-1)) == unsat);
+
+  // from_int: decimal digits, "" for negative values.
+  REQUIRE(
+    z3_disproves(
+      string_builtin_app(
+        ID_cprover_string_from_int_func, {num(42)}, string_type),
+      str("42")) == unsat);
+  REQUIRE(
+    z3_disproves(
+      string_builtin_app(
+        ID_cprover_string_from_int_func, {num(-5)}, string_type),
+      str("")) == unsat);
+
+  // of_int: decimal digits, with a leading '-' for negative values.
+  for(const auto &[n, digits] : std::vector<std::pair<long, const char *>>{
+        {42, "42"}, {0, "0"}, {-5, "-5"}, {-120, "-120"}})
+  {
+    REQUIRE(
+      z3_disproves(
+        string_builtin_app(
+          ID_cprover_string_of_int_func, {num(n)}, string_type),
+        str(digits)) == unsat);
+    REQUIRE(
+      z3_disproves(
+        string_builtin_app(
+          ID_cprover_string_of_int_func, {num(n), num(10)}, string_type),
+        str(digits)) == unsat);
+  }
+
+  // empty_string is ""
+  REQUIRE(
+    z3_disproves(
+      string_builtin_app(ID_cprover_string_empty_string_func, {}, string_type),
+      str("")) == unsat);
 }
 
 TEST_CASE(