Method mkString

src/api/java/Context.java:2162–2173

Create a string constant.

(String s)

     * Create a string constant.
     */
    public SeqExpr<CharSort> mkString(String s)
    {
        StringBuilder buf = new StringBuilder();
        for (int i = 0; i < s.length(); i += Character.charCount(s.codePointAt(i))) {
            int code = s.codePointAt(i);
            if (code <= 32 || 127 < code) 
                buf.append(String.format("\\u{%x}", code));
            else
                buf.append(s.charAt(i));
        }
        return (SeqExpr<CharSort>) Expr.create(this, Native.mkString(nCtx(), buf.toString()));
    }

    /**
     * Convert an integer expression to a string.