Issues with substr

[jawline]

Hi,

I'm having some trouble with string support in Z3. Giving the following program

(declare-const a String) (define-const c String "abc")

(assert (= (str.substr a 1 4) c))

(check-sat) (get-model)

I would expect a to be _abc, however when I run Z3 it gives me the output

sat (model (define-fun a () String "") )

which maps a to the empty string. Is this correct behaviour/me misunderstanding how substr should work, or am I getting a strange model.

Note: if I change the program to be substr a 1 1 == abc it still says the program is satisfiable, which I find very strange.

Thanks, Blake Loring

[NikolajBjorner]

substr is under-specified when the intervals don't match up with the string length, so if a is not constrained it is possible to supply a value for a that doesn't match up to the boundaries specified by the integers.

[jawline]

Ah ok, do you have any recommendations on working if I was trying to use Z3 to model string behaviours for charAt and substr in a language.

Would doing a length check before any at or substr resolve it.

Something like x.charAt(5) == 5 generated the SMT x.length > 5 && (= (at x 5))

Thank you for the help.

[NikolajBjorner]

You could assert an equality that constrains x to be a concatenation of sub-strings, and then constrain the length of the substrings the way your model prescribes.

As a disclaimer, note that string and sequence support in Z3 is still a relatively new feature. It is tested on a relatively limited set of problems so far. It attempts to follow an ongoing standardization effort, which is also a work in progress.

[jawline]

Thank you for your quick response.

Could you give a short example of what you mean by constraining x to be a concatenation of sub-strings.

Additionally, do you think the substr definition will change later, or is this constraint likely to persist. I love the new strings support and we really need it - but if these models are likely to change a lot going forward it may be putting it on the back burner for a while.

Thanks, Blake Loring

[NikolajBjorner]

Seems it is a bug relative to the tentative spec:

 o (str.substr String Int Int String)

[[str.substr]](w, m, n) is the (unique) word w2 such that
for some words w1 and w3
- w = w1w2w3     - |w1| = m
- |w2| = min(n, |w| - m)     if 0 <= m < |w| and 0 < n

[[str.substr]](w, m, n) is the empty word if m < 0, m >= |w|, or n <= 0

Note that the second part of the definition makes [[str.substr]]     a total function.

[NikolajBjorner]

The result should now be along the lines you would like and the upcoming standardization describes.