[SMT-LIB] get-model

[Cesare Tinelli]

Hi David and all,

On 3 Nov 2010, at 02:33, cok at frontiernet.net wrote:

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

Sorry, I meant all the ones you commented on (:produce-proofs, :produce-unsat-cores, :produce-models, and :produce-assignments). 


>  Others, such as :print-success :verbosity and setting output channels could readily be changed during an interactive session, if we wished to allow that.
> 
That is right. 

That said, I discussed the matter with Aaron and he agreed that it would be more appropriate to come to a clear consensus on this in the API-WORK group first. So he is going to raise the matter there. 

As a consequence, the upcoming new release of the standard document will not contain any fixes related to set-option yet.


Cesare


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