Lacking string comparison operators

[pjljvandelaar]

As a user I would like to reason lexically over strings, like "Monkey" > "Ashtray".

However,

(get-info :name)
(get-info :version)
(set-logic ALL)
(set-option :produce-models true)
(set-info :smt-lib-version 2.5)

(declare-fun s1() String)
(declare-fun s2() String)
(assert (< s1 s2)
(check-sat)
(get-model)

yields

PS C:\experiments\z3> z3 .\stringCompare.smt2
(:name "Z3")
(:version "4.8.5 - build hashcode b63a0e31d3e2")
(error "line 9 column 16: Sort mismatch at argument #1 for function (declare-fun < (Int Int) Bool) supplied sort is String")

Could support for comparison for strings be added?

At http://cvc4.cs.stanford.edu/wiki/Strings, I read about the str.to.int function: Does this mapping agree with the lexical mapping and should that be used to solve my issue?

See also https://github.com/TorXakis/TorXakis/issues/883

[NikolajBjorner]

The standard proposal lead by Cesare Tinelli includes a lexicographic string comparison method. it also requires unicode support, so both features would require revisiting the available support.

[pjljvandelaar]

Unicode would be nice, but is not needed. Only string comparison is required!

[LeventErkok]

@NikolajBjorner This is something I'm interested in as well. Is the commit operational? Because I'm getting a segfault on <=:

(set-logic ALL)
(declare-fun s0 () String)
(declare-fun s1 () String)
(assert (str.<= s0 s1))
(check-sat)

z3 says:

$ z3 a.smt2
Failed to verify: m_util.str.is_lt(n, e1, e2)
[1]    18261 illegal hardware instruction  z3 a.smt2

[LeventErkok]

By the same token adding support for seq.< and seq.<= would be nice as well.

[LeventErkok]

The segfault is gone, thanks! But something is still quite fishy:

(set-logic ALL)
(declare-fun x () String)
(declare-fun y () String)
(assert (= x "ab"))
(assert (= y "cd"))
(assert (not (str.<= x y)))
(check-sat)

This correctly returns unsat:

$ z3 a.smt2
unsat

But if you swap the first two asserts (lines 4 and 5):

(set-logic ALL)
(declare-fun x () String)
(declare-fun y () String)
(assert (= y "cd"))
(assert (= x "ab"))
(assert (not (str.<= x y)))
(check-sat)

z3 says:

$ z3 a.smt2
sat

[NikolajBjorner]

I believe we can close this now. Support is added for str.< and str.<=.

[LeventErkok]

@NikolajBjorner Would be really nice to have seq.< and seq.<= as well; without those two the sequence logic is lacking access to what you must've already implemented for sure.

[NikolajBjorner]

seq.< and seq.<= are not well defined for all types. Maybe for Int and Real, but what about algebraic data-types, then there should also be <, and <= for ADTs, arrays, user-sorts (and what would that be?).

[LeventErkok]

Great point. I was thinking lexicographic ordering, as given by the order of constructors declared in the data-type itself. (I'm thinking more like deriving Ord in Haskell; i.e., as long as a has comparisons, so does List a; recursively; but perhaps that's a bit too much to ask.)

[NikolajBjorner]

It all depends on whether there are compelling applications that need this. The type system isn't at the level of Haskell and therefore an implementation would not be principled.

[LeventErkok]

That's a fair point. But perhaps Seq Int, Seq (_ BV n), Seq Real and Seq (_ FP n m) are well within reach?

But this is more of a "nice to have" than a "must have" admittedly.

[NikolajBjorner]

All doable, but it is a use-it-or-lose-it question regarding feature addition.

[LeventErkok]

I don't have a compelling use case for the time being.. If I ever have a need, I'll be sure to ping again!