[SMT-LIB] Comments to the new SMT-LIB standard

[Jochen Hoenicke]

Hello,

I am currently reading the SMT-LIB standard v2.0 and have some
remarks/questions.

Is define-fun the new way of avoiding nested let's?
Many benchmarks currently have a lot of nested flet to assign formulas
to names.  This can be either translated by define-fun or by nested
let terms.  The latter needs deep nesting (danger of stack-overflow
not only in the parser but also in every code that processes the AST)
and does not work across assert statements.  define-fun seems to be a
good way to avoid nested lets and if I understand correctly from a
previous mail, this is its purpose.

Do solvers still have to work around stack-overflows for nested lets,
and, or?  If nested lets can be replaced by define-fun and nested and
by a multi-argument and, there is no need to support deep nestings.  I
would do the transformation myself in the parser, but unfortunately
there is the get-assertion function that forbids simplifying the AST.
Writing a non-recursive AST to string conversion function for deeply
nested terms seems to be no fun at all.

Grammar issues
-----------------

Although I cannot find it explicitly mentioned in the standard, the
nonterminal <symbol> should obviously also match predefined symbols.
This is necessary, e.g. to allow the terms true and false, or to allow
every syntactic construct to match <s_expr>.  Then, the grammar as
defined in the standard is ambiguous.

First, why is Bool a predefined symbol?  and, or, not etc. are not. I
would suggest to remove Bool as predefined symbol.
Also, one could have defined "distinct" as a function in the Core
theory by adding an attribute :pairwise similar to :chainable.

If symbols include predefined symbols, what symbols are forbidden for
identifiers?
The following identifiers give ambiguities in the grammar:
  _ (ambiguity in identifier)
  ! as distinct let forall exists  (ambiguity in term)
  par NUMERAL DECIMAL STRING  (ambiguity in function declaration in a theory)
  Bool (ambiguity in sort)
If I do not have a typo in my grammar, this list is exhaustive.
My suggestion is to remove Bool from predefined symbols and disallow
at least the symbols
  _ ! as distinct let forall exists
in most places.  All other symbols, e.g. push, pop, true, false, sat,
unsat, error, can be allowed.

To be precise, the function names "forall", "exists", "!", and "let"
would not lead to any ambiguity, also "as", "distinct", and "_" could
be used as variable names, but it would be a nightmare to write a
parser that can distinguish a function call
 (forall ((as foo Int) (g int)) (= (f a) g))
from a quantifier
 (forall ((as Int) (g Int)) (= (f as) g))

By the way, is the symbol |xy| different from the symbol xy?

Are predefined keywords also keywords?
This leads to ambiguous grammar, but probably we don't want to forbid,
e.g., the user defined annotation :notes for a term.
If one takes the grammar literally, then all predefined attributes
could be removed without changing the language.  I think the intention
is, that <keyword> in attribute should not match those predefined
keywords that appear in a production of the parent non-terminal.

Currently, I have 37 shift-reduce and reduce-reduce conflicts, or I
use a complicated grammar (with four different attribute
non-terminals) to avoid the conflicts and still allow, e.g., the
:authors keyword in theories.

minor typos in the standard:
------------------------------

spec_constant sometimes spelled as spec_const.
attribute_value is unused; probably the rule for attribute should be
  attribute ::= keyword | keyword attribute_value
:author (predefined keyword) versus :authors (info_flags)
get-option is currently not a predefined symbol
the predefined keywords :axioms :family :logic :script  should be removed.
page 22: A sort parameter can be any <symbol>:  replace <symbol> with <sort>
page 23: description still mentions "=", grammar does not.
page 57: preorder enumeration should be postorder enumeration:
(! (+ (! (x :named f)) f) :named g)  should first define f, then define g.
page 70: DECIMAL is sorted as if it would start with R


Regards,
  Jochen Hoenicke