get-model command: standard vs. implementations

[Jochen Hoenicke]

While checking some edge case results for get-model against the standard, I noticed that there is a discrepancy between the SMT-LIB standard and what every existing implementation does.

According to the standard, the answer to (get-model) should just be a list of (define-fun...) commands, e.g.

(get-model)

 ; ( (define-fun x () Int 0) (define-fun y () Int 1) )

However, every current solver adds an additional model keyword in the answer:

(get-model)

 ; (model (define-fun x () Int 0) (define-fun y () Int 1) )

The post-processor for the model-validation track in SMT-COMP actually checks that the "model" keyword is present.  Thus it rejects standard conform models.

So should we keep the standard and fix all tools, or should we change the standard?  I personally like the standard better, since it avoids adding another keyword and it follows the pattern of other commands like get-value or get-unsat-core that just print a list.

However, changing all solvers may break existing tools that parse the output of these solvers. To allow a smooth transition, it would be possible to allow an optional "model" in the model parser, so that it works with both current and standard conform solvers.

Cheers,

  Jochen

[Cesare Tinelli]

Jochen,

As I understand it from talking with some of last year's SMT-COMP organizers, since the model validation track was new and the (model ...) format was provided by most if not all solvers, they accepted it.

You are correct though that it is not compliant to the standard. I am not sure which solver introduced that format but I guess the other ones followed its lead. (It must have been one of those very popular SMT solvers.)

For this year's competition I would allow both formats. However, it would be good to resolve this issue for next year.

Personally, I prefer the official format too (without the model  keyword) but if there are enough requests from the community, with a motivation of why adding model is better, we could change the standard.

So it would be good to hear from the community on this.

Cesare

[Clark Barrett]

After some discussion, we are going to propose that we stick with the existing standard.  This means that the result of a get-model command should be a parenthesized list of definitions, *without* the additional "model" keyword.  This is consistent with other commands like get-value, get-assignment, and get-unsat-core, each of which returns a list of objects without any additional keywords.  We recommend that solver developers make this change to conform to the standard.