ADT constructor for update

[mgudemann]

Is there an equivalent to update (in CVC5) or update-field (in Z3) for ADTs in Princess?

cf. https://github.com/Z3Prover/z3/discussions/5712

[pruemmer]

This is not currently supported, but we could introduce update functions easily.

Is this a question concerning the API or the SMT-LIB interface?

[mgudemann]

Is this a question concerning the API or the SMT-LIB interface?

For the SMT-LIB interface.

[pruemmer]

Thanks for the suggestion, we have now added update functions following the Z3 syntax: (_ update-field X)

[mgudemann]

Great, thanks!