z3_decl_kind and str.</str.<=?

[evmaus]

Hey:

So it looks like although the Z3 C++ API exposes both str.< and str.<= from the SMT standard as lexicographic comparison via the following methods: Z3_ast Z3_API Z3_mk_str_lt(Z3_context c, Z3_ast prefix, Z3_ast s); Z3_ast Z3_API Z3_mk_str_le(Z3_context c, Z3_ast prefix, Z3_ast s);

However, it seems like the enumeration for different interpreted function types (Z3_decl_kind) doesn't include a (SEQ/STR) LT/LE: https://github.com/Z3Prover/z3/blob/367e5fdd5258eacfc18e1089b305d9004382578d/src/api/z3_api.h#L1192

Is this intentional? What's the level of support for the lexicographic string comparison functions?

Thanks, Everett

(Possibly related: It also seems like str.</str.<= isn't recognized by whatever version of Z3 is backing rise4fun. No idea if that's just that it's an older version or something else, and I didn't have time today to build a recent Z3 version & try it on my own machine.)

[LeventErkok]

I believe these are handled via:

https://github.com/Z3Prover/z3/blob/6cc52e04c3ea7e2534644a285d231bdaaafd8714/src/ast/seq_decl_plugin.h#L87-L88

(Only < and <= is supported; if you need > or >=, then you flip the arguments.)

[evmaus]

So, yes--it seems like the feature is present in the AST if you're interacting via SMTLib commands; that'd imply that my issue with rise4fun was just that it was backed by an older version of Z3. :) There's also a lot of places in the codebase, including the API, that imply that they are supported & exist.

Our use case, though, is only interacting with Z3 via the C/C++ APIs. From the comments in the API, the z3_func_decl enum seems like it's supposed to be a list the types of interpreted functions supported by Z3, but I may be misunderstanding its purpose. My observation was that although many of the interpreted functions for sequences and strings are present, some appear to be missing. My question was mostly "is there a reason for that, or is that just an oversight?"

Thanks!

[NikolajBjorner]

Call it an oversight. There is bound to be other functions that don't have their op-codes exposed. The workarounds is to use string matching or contribute to Z3 as it is open source.

[evmaus]

Makes sense--we wanted to make sure we weren't using internal/unreleased methods.

Happy to contribute patches if we encounter this in the future! Thanks!