ADT constructor for update

[mgudemann]

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

cf. Z3Prover/z3#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!