String const size

[zwimer]

Do String consts have no size? If not, how do you find it?

In the API I can see that BV consts have a given size:

z3/src/api/c++/z3++.h

Line 3582 in ae2672f

inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }

Strings do not seem to have one:

z3/src/api/c++/z3++.h

Line 3581 in ae2672f

inline expr context::string_const(char const * name) { return constant(name, string_sort()); }

String literals have a size, accessible via https://z3prover.github.io/api/html/group__capi.html#ga766dc289b1b9c5884da389291025e6c7
But this function will not work for string constants.

I can, however, make a Z3_mk_seq_length using this as an argument, but that isn't a concrete value but rather just an AST.

If string constants cannot have a size, why not? Or is it just not implemented?

[NikolajBjorner]

There is no specific case for taking the length of a string literal. Everything is an expression, string literals happen to have a size that is determined, but generally string expressions don't have a determined size. For example, if you create a variable s of type String, the length of s can be anything that is consistent with constraints you may set on s.
One thing you can do is to create a string length expression and then call simplify to rewrite it.
The result is an expression that should be an integer constant.

[zwimer]

Is there a way to take the length of a string_const / way to construct a string_const with a length? I know you can specify a length when constructing a bv_const as shown here:

z3/src/api/c++/z3++.h

Line 375 in cbc5b1f

expr bv_const(char const * name, unsigned sz);

[zwimer]

fpa_const specifies a length via the ebits and sbits, and bool_const's length need not be specified since booleans are of a known length. I can find no analogous way to specify the length of a string const though.

[NikolajBjorner]

ebits and sbits are part of the type of a float, similarly, the number of bits in a bit-vector is part of the type.
The lengths are therefore static and the same for all expressions of those types.
This is not the case for string expressions.

[zwimer]

I see; in other words, the only way to constrain the length of a string const is via an external constraint; it is not possible to be have it be part of the type, as one can for a BV?

That is, the closest analogy strings have to z3.BitVec("abc", 64) is the two expressions x=z3.String("abc") and z3.Length(x) == 8 where we require the latter remain true.

Would that be a correct understanding?

[NikolajBjorner]

Sure,

from z3 import *
s = Solver()
s.add(8 == Length(StringVal("abc")))
print(s.check())

this is unsat

from z3 import *
s = Solver()
s.add(8 == Length(String("abc")))
print(s.check())

this is sat.

Here "String("abc")" creates an uninterpreted constant of sort String. The name is "abc".
You can constrain the length of this uninterpreted constant using equations using the Length function.