[SMT-LIB] Grammar ambiguity for v2 attributes

[Cesare Tinelli]

Chris,

On 16 Jun 2010, at 17:33, Christopher L Conway wrote:

> There appears to be an ambiguity in the grammar for v2 attributes:
> 
>    <attribute> ::= <keyword> | <keyword> <sexpr>
>    <sexpr> ::= ... | <keyword> | ...
> 
Yes, but this one is simply because of a typo, already pointed by Jochen in a previous message. As the text in the second paragraph of Section 3.4 implies, the intended definition of attribute is 

<attribute> ::= <keyword> | <keyword> <attribute_value>
                                      ^^^^^^^^^^^^^^^^^

So, no attribute value can look like a keyword. I believe this should clarify your doubts below.

This error too will be fixed in the next release.


Cesare




> The input ":a :b :c" can be parsed as [hint: view in a fixed width font]
> 
>       :a        :b        :c
>        |         |         |
>    <keyword> <keyword> <keyword>
>         \        |         |
>          \    <sexpr>      |
>           \     /          |
>         <attribute>   <attribute>
>                \       /
>               <attribute>*
> 
> or
> 
>        :a        :b        :c
>         |         |         |
>     <keyword> <keyword> <keyword>
>         |          \        |
>         |           \    <sexpr>
>         |            \     /
>    <attribute>     <attribute>
>             \       /
>            <attribute>*
> 
> or
> 
>       :a           :b          :c
>        |            |           |
>     <keyword>   <keyword>   <keyword>
>        |            |           |
>    <attribute> <attribute> <attribute>
>              \      |      /
>               \     |     /
>                <attribute>*
> 
> Is it the intention that set of attribute keywords will be well known,
> as will their number and kind of values, and parser will be able to
> handle them using context-sensitive rules? If so, what attributes are
> included in the current SMT-LIB v2 benchmarks and what are their value
> types?
> 
> Alternatively, are attributes allowed to have keyword values? Is it
> the case that any existing attributes use keyword values?
> 
> Regards,
> Chris
> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib