Answers for get-model does not respect SMT-LIB 2 standard

[AdrienChampion]

When asked for a model, yices 2 (2.6.1) produces definitions as

(
    (= <ident> <value>)
    ...
)

But according to SMT-LIB 2.6 (page 47), models should look function symbol definitions, i.e.

(
    (define-fun <ident> ( <args_list> ) <sort> <value>)
    ...
)

Is this on purpose? Do you plan to produce models SMT-LIB-style in the future?

I am asking this as I am adding support for Yices 2 in the Rust SMT-LIB 2 crate rsmt2, where this discrepancy causes (relatively minor) problems.

[BrunoDutertre]

Get the latest version from gitub then try command-line option --smt2-model-format.

[BrunoDutertre]

And yes. It is on purpose. The yices format is much simpler, more compact,
less verbose, and easier to parse. The yices format also predates the 2.6 standard.

[AdrienChampion]

I see, thank you :)

I'm curious how you print models for non-nullary function symbols though, do you use some kind of closure notation?

In any case, let me go ahead and close this.

[BrunoDutertre]

That's documented in the Yices manual: https://yices.csl.sri.com/papers/manual.pdf