Feedback on smtlibv2.6 syntax and arithmetic typing rules
Guillaume Bury
https://asciinema.org/a/325668
That being said, and considering the ongoing discussions about smtlibv3, I wanted to share some feedback about the various problems, or rather interesting particularities of the SMTLIBv2.6 standard when compared to other formats. Note that of course, dolmen was written from scratch very recently and only performs type-checking, so it might be a bit unfair comparing to provers written some time ago which have evolved together with the SMTLIB (and thus bound by legacy implementations and/or backwards compatibility).
<info_flag>::= :all-statistics | :assertion-stack-levels | :authors | :error-behavior | :name | :reason-unknown | :version | <keyword>
<b_value> ::= true | false
<option> ::= :diagnostic-output-channel <string> | :global-declarations <b_value> | :interactive-mode <b_value> | :print-success <b_value> | :produce-assertions <b_value> | :produce-assignments <b_value> | :produce-models <b_value> | :produce-proofs <b_value> | :produce-unsat-assumptions <b_value> | :produce-unsat-cores <b_value> | :random-seed <numeral> | :regular-output-channel <string> | :reproducible-resource-limit <numeral> | :verbosity <numeral> | <attribute>
Lastly, the real problem occurs in the last instance of this kind of specification with the `prop_literal` production:
<prop_literal> ::= <symbol> | ( not <symbol> )
Firstly is the definition of arithmetic linearity in the SMTLIB. Currently, linearity is specified as a restriction specified in the `:language` field of each logic that need it. As known (and fixed in smtlibv3 if I understand correctly), this is a problem because it duplicates the definition of linearity. But if one read carefully, there are actually two different definitions of linearity in SMTLIBv2.6. Most of the linear arithmetic logics (e.g. AUFLIRA, LIA, LRA, QF_LIA, QF_UFLIA, QF_UFLRA, QF_LRA, UFLRA) specify linear terms as including terms of the form c, ( * x c), ( * c x) where:
While on the topic of arithmetic restrictions, it seems that at least some problems in difference logic have a somewhat liberal interpretation of the spec. The difference logic spec looks like this:
"Closed quantifier-free formulas with atoms of the form: - q - (op (- x y) n), - (op (- x y) (- n)), or - (op x y) where - q is a variable or free constant symbol of sort Bool, - op is <, <=, >, >=, =, or distinct, - x, y are free constant symbols of sort Int, - n is a numeral.
Guillaume Bury
Jochen Hoenicke
Another example of the same kind of problem appears with the Command options productions, which use the following declaration:<b_value> ::= true | false<option> ::= :diagnostic-output-channel <string> | :global-declarations <b_value> | :interactive-mode <b_value> | :print-success <b_value> | :produce-assertions <b_value> | :produce-assignments <b_value> | :produce-models <b_value> | :produce-proofs <b_value> | :produce-unsat-assumptions <b_value> | :produce-unsat-cores <b_value> | :random-seed <numeral> | :regular-output-channel <string> | :reproducible-resource-limit <numeral> | :verbosity <numeral> | <attribute>Same as before, the last case allowing any `<attribute>` subsumes all other cases. Fortunately, this makes the rule <b_value> useless, which is good because since `true` and `false` are not reserved keywords, it would be extremely annoying to specify in a parser generator.
keywordAttr ::= CPATTERN | CNAMED;
keywordTheory ::= CSORTSDESCRIPTION | CSORTS |
CFUNS | CFUNSDESCRIPTION | CDEFINITION;
...
keyword ::= KEYWORD | keywordAttr | keywordTheoryLogic | keywordOption;
Let's now talk about typing arithmetic in smtlib, and I'll here make a list of the surprising quirks that one can spot when trying to strictly follow the specification for arithmetic.
Firstly is the definition of arithmetic linearity in the SMTLIB. Currently, linearity is specified as a restriction specified in the `:language` field of each logic that need it. As known (and fixed in smtlibv3 if I understand correctly), this is a problem because it duplicates the definition of linearity. But if one read carefully, there are actually two different definitions of linearity in SMTLIBv2.6. Most of the linear arithmetic logics (e.g. AUFLIRA, LIA, LRA, QF_LIA, QF_UFLIA, QF_UFLRA, QF_LRA, UFLRA) specify linear terms as including terms of the form c, ( * x c), ( * c x) where:- x is a free constant of sort Int or Real and- c is an integer or rational coefficient, respectively.Whereas some logics (e.g. AUFLIA, QF_AUFLIA), use the following:- x is a free constant or a term with top symbol not in Ints, and- c is a term of the form n or (- n) for some numeral n.The difference is in whether expression whose top symbol are not an arithmetic builtin can be mutliplied by a constant. While for a few logics this is not a big problem, as soon as UF or Arrays are included in the logic, this makes a non trivial difference. Additionally, since not all logics are specified on http://smtlib.cs.uiowa.edu/logics-all.shtml , it's not clear which definition some logics use. For instance ALIA (and QF_ALIA) is not specified, however trial and error seems to indicate it should belong to the more lenient case.
While on the topic of arithmetic restrictions, it seems that at least some problems in difference logic have a somewhat liberal interpretation of the spec. The difference logic spec looks like this:"Closed quantifier-free formulas with atoms of the form: - q - (op (- x y) n), - (op (- x y) (- n)), or - (op x y) where - q is a variable or free constant symbol of sort Bool, - op is <, <=, >, >=, =, or distinct, - x, y are free constant symbols of sort Int, - n is a numeral.However, I have seen problems which use addition in let-bound variables. I don't have an example on hand (I'll try and find a precise example of this), but basically a variable `x` was let-bound to some other variable added to a constant (e.g. `y + c`), and then later compared to a single variable (e.g. `(< x z)`). While this can be normalized into one of the accepted form (because it normalizes to `(< (- y z) (- c))` ), I think it's not conforming to the spec as currently written.
Cesare Tinelli
Hi Guillame,
Many thanks for your feedback. Please see our inlined replies below.
On 8 Jul 2020, at 4:06, Guillaume Bury wrote:
Hi, as announced a bit earlier this year, I've been working on a library to
parse and type languages used in automated deduction, this include of
course SMTLIB (v2.6), but also TPTP, dimacs, iCNF, zipperposition's format,
and alt-ergo's format (the aim is to cover most if not all languages used
by automated theorem provers, so don't hesitate to propose new format to
add, ^^). One main feature of dolmen is that it now provides a LSP
(Language server protocol) that you can use in your editor to get instant
feedback when editing files,a s can be seen in the following demo:
<a href="https://asciinema.org/a/325668" target="_blank"><img
src="https://asciinema.org/a/325668.svg" /></a>
Thanks again for working on this library. It could be an extremely useful tool for the entire AR community.
[...]
First of all, a very quick remark about the syntax of smtlib v2.6 (as
defined in page 95 and onwards in
http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf ),
the `info-flag` production is declared as follows in the standard
<info_flag>::= :all-statistics | :assertion-stack-levels | :authors |
:error-behavior | :name | :reason-unknown | :version | <keyword>which is somewhat redundant given that `<keyword>` includes all the
previous cases.
The redundancy was intentional, to list in a single place in the formal document all the predefined flags.
Additionally, if i'm not mistaken, the previous cases
cannot be reasonably expressed in a production for LR(2) or LALR(1)
parsers, since they are instance of the `<keyword>` production and not
declared as distinct token (contrary to reserved words).
Maybe we should have stressed in the document that the grammar itself is not prescriptive. The document's goal is to define the SMT-LIB language as a standard, not the grammar itself. So the grammar presented there is designed along the needs of clarifying the various aspects of the language. It was not meant to be a reference grammar. We had an implicit understanding that implementors would design their grammar rules while accepting the same language.
In particular, in the case above one could definitely just use the rule
<info_flag> ::= <keyword>
or, in fact, eliminate the <info_flag> non-terminal altogether and replace it by <keyword>.
That said, it might be useful to implementer to see a grammar in the reference document that they could use as is in actual parser generators, without having to design their own and convince themselves that it recognizes the same language. We will keep this in mind for Version 3 of the standard.
However in that
example, there is no problem as all but the last case can be omitted in the
parser.
Another example of the same kind of problem appears with the Command
options productions, which use the following declaration:
<b_value> ::= true | false
<option> ::= :diagnostic-output-channel <string> | :global-declarations
<b_value> | :interactive-mode <b_value> | :print-success <b_value> |
:produce-assertions <b_value> | :produce-assignments <b_value> |
:produce-models <b_value> | :produce-proofs <b_value> |
:produce-unsat-assumptions <b_value> | :produce-unsat-cores <b_value> |
:random-seed <numeral> | :regular-output-channel <string> |
:reproducible-resource-limit <numeral> | :verbosity <numeral> | <attribute>Same as before, the last case allowing any `<attribute>` subsumes all other
cases.
Yes, the same reply applies here.
Fortunately, this makes the rule <b_value> useless, which is good
because since `true` and `false` are not reserved keywords, it would be
extremely annoying to specify in a parser generator.
I do not quite see the problem for parser generators with true and false not being reserved words. What is annoying exactly?
Lastly, the real problem occurs in the last instance of this kind of
specification with the `prop_literal` production:
<prop_literal> ::= <symbol> | ( not <symbol> )
This time again, the use of `not` is problematic because `not` is not a
reserved word, and actually belong to the `<symbol>` tokens, but in this
case, it is not subsumed by any other case, and requires a bit of a hack to
correctly parse. Hopefully, there won't be any such case in the smtlibv3
syntax, ^^
The main issue here is that not, true and false play double duty: they are both predefined symbols of the attribute sublanguage and symbols of the Core theory.
What would you suggest to fix the problem you point out?
The lack of definitions for many logics is indeed problematic. It is one of the issues we hope to address in SMT-LIB 3 (although we do not expect we will be able to solve it completely).
The linearity restriction in the proposed Version 3 is addressed differently by introducing a new "linear multiplication" symbol. However, for backward compatibility the old syntax will be still allowed, at least for a while, so the quirks you mention above will not go away unfortunately.
Now some of the duplication of the linearity definition is avoided by some
logics which simply refers to their QF_ counterpart (e.g. AUFLIA), by
specifying that they have the same extensions. However, it is never
explicitly specified that in the spec above, 'x' is also allowed to be a
quantified variable in logics which allow quantifiers. Hence a strict
reading and interpretation of the specification of AUFLIA would forbid
terms such as `(* 3 x)` where `x` is a quantified variable, which I assume
was not the intent.
You are correct. We missed this and it should indeed be clarified.
While on the topic of arithmetic restrictions, it seems that at least some
problems in difference logic have a somewhat liberal interpretation of the
spec. The difference logic spec looks like this:
"Closed quantifier-free formulas with atoms of the form: - q - (op (- x y)
n), - (op (- x y) (- n)), or - (op x y) where - q is a variable or free
constant symbol of sort Bool, - op is <, <=, >, >=, =, or distinct, - x, y
are free constant symbols of sort Int, - n is a numeral.However, I have seen problems which use addition in let-bound variables. I
don't have an example on hand (I'll try and find a precise example of
this), but basically a variable `x` was let-bound to some other variable
added to a constant (e.g. `y + c`), and then later compared to a single
variable (e.g. `(< x z)`). While this can be normalized into one of the
accepted form (because it normalizes to `(< (- y z) (- c))` ), I think it's
not conforming to the spec as currently written.
You are correct here as well. Exactly because we do not have a reference parser/checker for SMT-LIB, sometimes submitted benchmarks end up being accepted in the SMT-LIB repository that do not strictly conform to the prescribed syntax of the claimed logic.
Perhaps once you have your library up and running, if you are willing to, we could collaborate with you on building a reference conformance checker for SMT-LIB 2.6 and use it to validate current and future benchmarks in the official distribution.
Please contact us directly by email to discuss this if you are interested.
Best,
Cesare, also for Clark and Pascal
--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/534cc5f0-850f-4577-8668-490b5104f8cco%40googlegroups.com.
Cesare Tinelli
Hi Jochen,
Thanks for your comments. Please see below.
On 8 Jul 2020, at 11:13, Jochen Hoenicke wrote:
On Wed, 8 Jul 2020 at 11:41, Guillaume Bury <guillau...@gmail.com>
wrote:
Another example of the same kind of problem appears with the Command
options productions, which use the following declaration:
<b_value> ::= true | false
<option> ::= :diagnostic-output-channel <string> | :global-declarations
<b_value> | :interactive-mode <b_value> | :print-success <b_value> |
:produce-assertions <b_value> | :produce-assignments <b_value> |
:produce-models <b_value> | :produce-proofs <b_value> |
:produce-unsat-assumptions <b_value> | :produce-unsat-cores <b_value> |
:random-seed <numeral> | :regular-output-channel <string> |
:reproducible-resource-limit <numeral> | :verbosity <numeral> | <attribute>Same as before, the last case allowing any `<attribute>` subsumes all
other cases. Fortunately, this makes the rule <b_value> useless, which is
good because since `true` and `false` are not reserved keywords, it would
be extremely annoying to specify in a parser generator.
I interpret these as restricting the option values for boolean options to
true|false, while other options can have arbitrary values.
That was indeed the intention.
So attribute
should match every attribute except for the ones listed in this rule.
That is one way to do it. Another alternative for a solver is to have a simpler grammar with a rule that defines <option> as <attribute>, and then checking separately that the parsed attribute is a supported one.
To allow true and false as both symbols and special terminals in the
grammar, we use non-terminals for symbols that are defined as the terminal
SYMBOL or any of the other non-reserved special symbols (all
reserved/non-reserved symbols take their name as string value).
Likewise for keywords, where we have a non-terminal also for keywords that
are not special keywords for set-option. Here's an excerpt from our
smtlib2 grammar:
symbol ::= SYMBOL | CONTINUEDEXECUTION | ERRORSYM | FALSE | ...;
keywordAttr ::= CPATTERN | CNAMED;
keywordTheory ::= CSORTSDESCRIPTION | CSORTS |
CFUNS | CFUNSDESCRIPTION | CDEFINITION;
...
keywordNoOption ::= KEYWORD | keywordAttr | keywordTheoryLogic;
keyword ::= KEYWORD | keywordAttr | keywordTheoryLogic | keywordOption;
That seems like a reasonable solution to me. Again, the reference document is not meant to dictate the actual grammar to use.
BTW, the current standard specifies that s-expression is a syntactic
superset of term, but that would require allowing reserved symbols in
s-expression, which the grammar currently doesn't reflect. So a quantified
or annotated term currently should be an <s_expr> but that requires to
allow reserved symbols like 'forall' and '!' in the s_expr rule. Since it
would be useful to use all terms as s_expressions when annotating terms
(e.g. for :pattern annotation), reserved symbols should really be allowed
there.
Good point. We will fix this in Version 3 and possibly in Version 2.6 too, or perhaps in a new Version 2.7 meant to be the last one before the move to Version 3.
[...]
Firstly is the definition of arithmetic linearity in the SMTLIB.
Currently, linearity is specified as a restriction specified in the
`:language` field of each logic that need it.
[...]
That's a problem I wasn't aware of. It would be good to just allow all
terms for x whose top symbol is not arithmetic (select/uninterpreted
functions/variables/constants, also str.len in SLIA) as long as the term is
allowed in the respective logic. Maybe it's simpler to drop the
restriction completely and allow every term for x. After all, multiplying
a linear term with a constant always gives a linear term.
There is also the problem that c is sometimes a bit weirdly defined,
especially in LRA logics, e.g., (/ 1 3), or 0.5 are allowed but not (/ 1.0
3.0) or (/ 1.0 2.0), which in LIRA avoid the implicit cast from int to
real.
OK. We will consider that.
[...]
Another strange restriction is the array sorts allowed in different
logics. AUFLIRA is the only logic that supports two-dimensional arrays
(Array Int (Array Int Real)), but it doesn't support integer arrays (Array
Int Int). AUFLIA supports only one-dimensional integer arrays. ABV
supports only one-dimensional arrays between bit vector types,
It is true that it looks strange but please keep in mind that many of these restrictions are historical and motivated by the fact that they enable more efficient implementations (for instance, is easier to provide support for flat arrays that it is for nested ones.)
The move to Version 3 is a good occasion to reevaluate some of these restrictions and see if they are worth keeping.
and for FP
logics nobody defined what arrays are supported, because the logic
definitions are missing. So what should we assume for ABVFPLIA?
This is a legitimate questions of course. The truth is that the set of logics has exploded because of the huge number of benchmarks from various sources we have collected during the years. We, the SMT-LIB coordinators, simply do not have the time and patience to provide a definition to all of them as this is a time-consuming, tedious and error-prone work.
The intention of the import construct in Version 3 is to specify the particular combination of theories explicitly at the cost some loss in precision.
Eventually abandoning logics will create the problem of how to classify benchmarks, for voting purposes in the library itself (now each logic has its own git repo) and for SMT-COMP (whose divisions map one-to-one to the logics). But this is a problem we will deal with separately.
Cesare
Jochen
--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CANYHNmJvthsG2qqGZeb66GcNj_WYte5LDNGdJTKRwOLXtk-8qg%40mail.gmail.com.