[SMT-LIB] get-model

[cok@frontiernet.net]

Thanks for the clarifications.  Just to be pedantically precise - in (2) below you intend that ALL options be set before set-logic, not just the ones about which I commented?  Others, such as :print-success :verbosity and setting output channels could readily be changed during an interactive session, if we wished to allow that.

- David

 
----- "Cesare Tinelli" <tinelli at cs.uiowa.edu> wrote:

> 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