str.to_code function

[Avgor46]

Hi!

It seems that CVC5 supports str.to_code function, but I cannot find such method in any StringFormulaManager (CVC5 and other). Why is this function not being processed at the moment?

[kfriedberger]

It looks like nobody has yet requested support for string::to_code from JavaSMT. We could add this in the next release, if required.

[kfriedberger]

Links to solver documentation:

• Z3: https://z3prover.github.io/api/html/group__capi.html#gaf7f1141487f7fb41beca2d469e9d633f
• CVC5: https://cvc5.github.io/docs/cvc5-1.1.1/api/cpp/kind.html#_CPPv4N4cvc54Kind14STRING_TO_CODEE

With string::to_code we should also add string::from_code.

[Avgor46]

That would be very helpful!

[kfriedberger]

Work in progress: #422

[kfriedberger]

#422 was merged and will be part of the next release.