Comments on the recent email of Harald

[Silvio Ranise]

Dear Harald,

thanks a lot for your contribution to the discussion
on the common format of SMT-LIB.  Our reactions to
your comments follow below.

 We urge the other members of this list to express their
opinion as well on the issues raises by Harald.

Best regards,

Cesare and Silvio.

----------------------------------------


 > 1. No sort system! Our aim here is to exchange benchmark
 > examples, not to do language design
 >
We do agree that this should not be a forum for discussing the
relative benefits of sorted vs. unsorted languages.
It is a fact though that quite a lot of applications have benchmarks
and background theories which are more natural expressed in a sorted
framework. So sorts are in a sense unavoidable.
Our latest proposal tries to strike a balance by adopting an unsorted
underlying framework and allowing sorts in benchmarks and background
theories, provided that sorts are understood as syntactic sugar.
 From this, it obviously follows that we should provide a sensible way
to translate sorted stuff into the basic unsorted framework. The
relativization process we described in a previous email is a stardard
way to do that.


 > 2. No explicit language for syntactic restrictions.
 >
We are glad you agree with us on this, but we are not sure of what
you mean with your elaboration of this point.
The restriction field in a benchmark specification is meant to allow
one to document that the benchmarks fall into a certain subclass of
formulae. The reason to document this is that that subclass might allow
more efficient decision procedures. That's it. Whether the user of
the benchmarks decides to exploit this fact and build an a hoc tool
for that class (as Ofer for instance has done for the "difference
logic" class, or you have done for the class of qffs accepted by ICS)
or decides to develop a more general tool, it is not our business.


 > 3. There should be a base logic, which includes a reasoble number
 > of different theories.  [...]
 >
We all agree that there should be a base logic. We do not think,
however, that it is a good idea to include any specific theory into
the logic itself. Background theories can be specified separately,
in each benchmark class.
Of course, we can agree on the specification of a small number of
popular background theories such as LA over the rationals and so on.
But we do not see the need to embed these theories into the base logic.
(And note again that this is independent on whether the benchmark
user decides to build-in those theories into his solver or not.)


 > 4. The base logic already includes lets (they are useful and
 >   harmless), but no propositional connectives or explicit
quantification.
 >
We do not understand the need for such a restriction.
We suggest the base logic to be simply unsorted first-order logic with
equality, thereby considering also quantifiers and the usual
connectives,
possibly extended with some syntactic constructs which---everybody
agrees---are very useful, such as if-the-else's and let's.  Then, it is
up to the benchmark provider to specify to which fragment of this base
logic the benchmarks belong to: equational, quantifier-free, guarded,
whatever. This is done in the input language restriction field discussed

earlier. This way, no particular fragment of FOL-EQ has special status,
making SMT-LIB open to a vast array of benchmark classes.


 > Another extension could be along the dimension of various type
systems
 > (cmp 1.), but then the benchmark infrastructure should support
 > translations (tools) into an untyped fragment.
 >
We of course agree on this. That is why we proposed to have a sorted
language for benchmarks and for background theories, and an associated
translation process into unsorted FOL.


 > 5. No need for declaring function symbols, [...]
 > Mechanism for declaring function symbols should allow for infinite
 > families of function symbols (is indexing with respect to a Cartesian

 > product of naturals enough?).
 >
We are not sure what you mean by that. If you mean syntactical
conventions such as f_2_1, say, for denoting the first function symbol
of arity 2 in the family, then we agree.


 > There might even be the possibility to declare a function symbol
 > to be AC etc.
 >
Strictly speaking this is not necessary. If a function symbol in a
benchmark is AC it is because its background theory says so. Hence
it should be enough to look at the specification of the background
theory.
For example, some equational theorem provers look for axioms
characterizing
commutativity and associativity in order to infer that a certain symbol
is AC
and treat it in a special way.


 > 6. Distiction between machine-readable [...]
 >
We agree on this point. At least to start with, the only part
that needs to be machine-readable is the one that contains
the benchmarks. Everything else, whether it is written in a formal
language or not, is meant to be documentation for the benchmark
user, and so need not be machine-readable.


 > 7. Include constructs for specifying expected return values.
 > Should we also have standard formats for proof objects?
 > Probably not in the initial phase.
 >
We agree that there should be constructs to specify whether
a formula is satisfiable/un-satisfiable w.r.t. the background theory.
On the other hand, we think that arriving to a common standard for
proof objects would be too a difficult task, at least for now.


 > 8. Altoghether, a small example...
 >
At the moment, we too have no particular suggestions or
requirements on the concrete syntax of the benchmarks.
But we too agree that it should be easily parseable.
Your example syntax is fine, with the necessary adjustments
implied by our proposal (and ignoring for now some unimportat
details).
In our proposal, your example would look like this
(note how the first fields contain just English text):


(:benchmark-set "0"

  :signature      ; may be left empty
  " ... "

  :language
  "Conjunctions of equations and negated equations"

  :theory
  "The union of LA and U" ; where LA and U are defined
                          ; somewhere else in the library

  :semantics
  "a formula is satisfiable iff there is any model of
   the background theory that makes the formula true"

  :benchmarks
  (:formula
   (:turnstyle
    (:conjunction
     (:equal z (:f_1_1 (:minus x y)))  ; f_1_1 is the first
uninterpreted
     (:equal x (:plus z y))            ; function symbol of arity 1
     (:diseq (:neg y)                  ; :neg is unary minus (no
oveloading)
            (:neg (:minus x (:f_1_1 (:f_1_1 z))))))
    :value :unsat)
   :formula
    (...)))