[SMT-LIB] get-model

[Cesare Tinelli]

Hi David,

Thanks once more for your careful proof reading.

On 31 Oct 2010, at 17:16, cok at frontiernet.net wrote:

> 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?

It is amazing how many things still slip out, despite one's extensive proof-reading. I thought we had removed all references of get-model from the posted version of the document (after we decided that that command was not ready for Version 2.0).
So, yes, it is an accidental left-over (although not because get-model has been replaced by get-assignment, the two commands serve different needs).

In our defense, I should say that Clark, Aaron and I have been editing the document collaboratively with Subversion. After looking at the latex sources I'm starting to suspect that we are screwing up with the merges.


> 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?  

That is a good question, and it is a pretty glaring omission from our document not to specify this. Thanks for pointing that out. There's no blaming Subversion with this one :)

In our intention, all the set-option commands are issued at the very beginning of the script (also before set-logic), and only there. At least as far as the current options are concerned, there is really no point in allowing option changes in mid-script, not to mention that it would be quite difficult to support that.

We'll update the reference document to reflect this restriction.


> 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?
> 
Ops, we meant get-model there (page 62), not get-value. (Typing error I guess.)
However, since get-model is out for now, it should be just get-assertion.
Currently, that is the only interactive-mode command.

As for get-value and get-assignment, the interactive mode is meant for human users. Since get-value and get-assignment are crucial to many applications, they are definitely not restricted to interactive mode.

We'll fix this too.


The new release of the document, including other fixes, should go out in a few days.

Thanks,


Cesare, also for Aaron and Clark
 


> 
> David