[SMT-LIB] Version 2.0 of SMT-LIB is finally here!

[Cesare Tinelli]

Dear Anders and Alberto,

thanks a lot for your thoughtful feedback. Our reply follows below.


On 23 Feb 2010, at 09:22, Alberto Griggio wrote:

>> We encourage interested people in this wider list to take a look at the
>> document and give us their feedback **by the end of this month.**
> 
> Dear Clark, Aaron, Cesare and all,
> 
> we hope we are still on time for some feedback for the SMT-LIB v2
> draft. We have gone through it, and it generally looks quite fine
> (definitely an improvement wrt. v1.2!),

Good to hear that :)

> however there are some points
> that we didn't understand properly. Here's a list of them (in no
> particular order):
> 
> - The restrictions on the set-logic command are not 100% clear to
>  us. In particular, is it allowed to declare sorts/functions before
>  setting a logic? What about push (or pop)? The description of
>  set-logic on p.55 doesn't say anything about this, could you
>  clarify? Also, has something like this to be considered legitimate?
> 
>  (declare-sort Int 0)
>  (declare-fun + (Int Int) Int)
>  (declare-fun < (Int Int) Bool)
>  (declare-fun x () Int)
>  (declare-fun y () Int)
>  (set-logic QF_UF)
>  (assert (= x y))
>  (assert (< x y))
>  (check-sat)
> 
>  We think this would confuse more than one solver... (since we expect
>  many SMT solvers to have a built-in notion of "Int", "+", "<")
> 
You are completely right. This is an oversight on our part. Our intention was to require the set-logic command to come before any assertion-set commands (which means that the script above would not be legal). We'll modify the description of the command accordingly.


> 
> - As it is, it seems that the get-model command is not easily
>  implementable. On p.59, it's written that get-model should return
>  values for "all closed quantifier-free (sub)terms occurring in the
>  current set of assertions", which might be *many*. Example:
> 
>  (assert (and (and (and (and (and P Q))))))
>  (check-sat)
>  (get-model)
>  ; (assert (= P true))
>  ; (assert (= Q true))
>  ; (assert (= (and P Q) true))
>  ; (assert (= (and (and P Q)) true))
>  ; (assert (= (and (and (and P Q))) true))
>  ; (assert (= (and (and (and (and P Q)))) true))
>  ; (assert (= (and (and (and (and (and P Q))))) true))
> 
>  Or did we get it wrong?
> 
No, you did not. 

That definition of get-model is definitely too general and onerous, and unnecessarily so. Since the posting of the draft we have been working internally on defining a more reasonable one. The challenge was to produce a more restricted definition what was at the same time: useful to interactive users, precisely specifiable, and not to difficult to understand. We have settled on the following one, which seems to strike the right balance: 

(get-model) has the same semantics as (get-value (t1 ... tn)) where t1,...,tn are all the closed quantifier-free (sub)terms occurring in the current set of assertions and having a *user-defined* top symbol. (The top symbol of a term (f t1 ... tn) is f; the top symbol of a term (t alpha_1 ... alpha_n) or (let x = t′ in t) is the top symbol of t.)

In your example, assuming that P and Q are user-defined, you would get only 

 ((assert (= P true))
  (assert (= Q true))
 )

as expected, we suppose.

There is a caveat with this definition. Suppose one of the (sub)terms in the assertions is (using abstract syntax, for legibility)

let x = t in (f x (g x))

say, where f and g are user-defined and t is closed. You will get back a value for the whole term, which has the same value as (f t (g t)), but you will not get back a value for  let x = t in (g x).

If you really want to see that value you have two options:
instead of  let x = t in (f x (g x)), in your assertion you use
- (f t (g t)) or, 
- you first define a constant c with value t, with define-fun, and then use (f c (g c)).

Considering that get-model is meant only for the interactive mode, this looks like a reasonable compromise.

Note that with get-value we do not have this problem because if you want to know the value of  let x = t in (g x)  you explicitly ask for it. 


> 
> - The semantics for (set-option :timeout) is a bit unclear. What is
>  the timeout supposed to affect? Only (check-sat) commands, or all
>  the commands? When does the clock start ticking? Right after the
>  (set-option :timeout) command, or at the beginning of every
>  individual command? Also, is the timeout on wall-clock time or on
>  CPU time?

All legitimate questions (that option should not have gone into the posted draft yet).  We have been debating those questions too. Unfortunately, there is still no clear consensus on the most useful definition. One could make a convincing case for the timeout to apply to the whole script or to individual commands such as check-sat. A new discussion in the API work group is needed to get the opinions of a larger set of people (of course, comments from this forum are also welcome).
This means though that this option will not make it to Version 2.0.


> Finally, the document mentions both 
>  (set-option :timeout -1) and (set-option :timeout none): what's the
>  difference (if any) between the two?
> 
That is not intended. '-1' should be 'none'. The error has been fixed.


> 
> - It seems there is currently no (standard) way of disabling support
>  for model generation, proof and unsat core computation. In general,
>  such features might come with a non-negligible overhead, so it could
>  be useful to have a way of disabling them if they are not needed. At
>  the moment, either a solver fully supports them, or it always says
>  "unsupported" (or it has to use non-standard extensions to
>  enable/disable them).
> 
This is a very good suggestion. We'll modify the specs to make those commands disabled by default and to allow their individual enabling and disabling. The error response will be modified accordingly so that the solver reports 'disabled' if one calls the commands when it is disabled.
 
Incidentally, we have been also working at a reasonable definition of get-assignment, a command that did not make to the draft because of disagreements in the API working group on its semantics. We are going to propose that get-assignment return the truth value of every (sub)formula in the assertions that has been explicitly annotated for consideration by the command.
The get-assignment command should be to be a lot less heavy than the ones above. Perhaps we do not need enabling and disabling for it? What do you think?


> 
> - It would be nice to have a translator from the old format to the new
>  one, but also from the new one to the old one (when possible). 
> 
Yes. We are going to build an old-to-new translator into CVC3, which we will use to upgrade the library to Version 2.0.
It would not difficult to add the inverse translator as well, so we intend to do so, and make the translation functionalities available as new options in a public release of CVC3. 

 
> The
>  latter would allow anyone to compete in the forthcoming competition
>  without too much effort, and it would also allow to run last year's
>  winners as reference points.

This is something to relay to the SMT-COMP discussion list. Providing a translator for the benefit of the community is one thing. Proving one for the competition is another (involving potentially delicate correctness and fairness issues). The best way for SMT-COMP'10 to deal with the transition should be discussed in that forum.


> 
> - There are several new commands that might be non-trivial to support,
>  especially for solvers that currently support only a small fraction
>  of SMT-LIB's logics and features (like non-zero-arity sorts and
>  function definitions). We think that it would be nice (especially
>  for not "scaring away" potential new competitors) to have a sort of
>  "grace period" in which it is guaranteed that such new commands
>  won't be used for the competition. This would make - we think - the
>  transition smoother for everybody.
> 
Sure. That is the intention of the SMT-COMP organizers. But again, this is out of the jurisdiction of this discussion list :)


> 
> Thanks again for your work on the new SMT-LIB standard,
> we are looking forward to hear from you,
> 
Thank you for your support and feedback. We greatly appreciate it. 

Best,


Cesare, also for Aaron and Clark


> Best,
> Anders and Alberto
> 
>