[SMT-LIB] get-model

[cok@frontiernet.net]

Cesare, et al.

1) The SMT-LIB v2 document mentions the get-model command, but it does not say what it is supposed to do or in what form to return it.  Is it an accidental left-over, having been replaced by get-assignment?

2) The get-assignment, get-value, get-proof, get-unsat-core all require a corresponding option to be set before the command can be given. When must it be set?  before set-logic? before any declarations or assertions? before any assertions (but not necessarily before declarations)? just before check-sat? just before the corresponding command?

3) The document states that get-value and get-assertions may only be used in interactive mode.  Do you actually mean get-value and get-assignment, since those two commands are closely related? Or perhaps all three -= get-model, get-assignment, get-assertions?


David