[SMT-LIB] SMT-LIB logic and language Version 2 draft

[Cesare Tinelli]

Dear Tjark,

thanks for your immediate feedback.

On Aug 1, 2009, at 2:38 AM, Tjark Weber wrote:


> On Fri, 2009-07-31 at 00:16 -0500, Cesare Tinelli wrote:
>
>> the draft below defines Version 2 of SMT-LIB's underlying logic and
>> the language for specifying theories, sublogics and benchmarks.
>>
>
>
>> Again, your feedback is highly welcome.
>>
>
> A nice piece of work!  I believe it's very much going into the right
> direction.
>
>
Thanks, that was our intention :)


> I only have very minor remarks for the time being.
>
>
>>    <hex> ::= a non empty sequence of digits and the letters
>>              from a to f, capitalized or not
>>
>>    <hexadecimal> ::= #h<hex>
>> ------------------------------
>> Ex: #h0  #hA04  #h01AB #h61ff
>> ------------------------------
>>
>
> I suggest at least one mixed-case example, e.g., #h01Ab, just to point
> out that's valid.
>
>
Done.


>>    <bin> ::= a non-empty sequence of 0s and 1s
>>    <binary> ::= #bin<bin>
>> ------------------------------
>> Ex: #b0  #b001 #b101011
>> ------------------------------
>>
>
> #bin should be #b.
>
>
Fixed.


>>    <symbol> ::= any sequence of letters, digits and the characters
>>                 + - / * = ~ ? ! . _ $ % & ^ < > @ :
>>                 that does not start with a digit
>>              |  any sequence of printable ASCII characters that  
>> starts
>>                 and ends with | and does not otherwise contain |
>>
>
> I suggest inserting "non-empty" or "(possibly empty)" before  
> "sequence"
> as appropriate.
>
>
Changed "any sequence of letters ..." to "any non-empty sequence of  
letters ..."

The other is fine (|| is an allowed symbol).



>> Then (f t_1 ... t_n) is syntactic sugar respectively for:
>>
>> i)   (f ... (f (f t_1 t_2) t_3) ... t_n)
>> ii)  (f t_1 (f t_2 ... (f t_{n-1} t_n) ...)
>> iii) (and (f t_1 t_2) ... (f t_1 t_2))
>>       [with 'and' itself assumed to be declared as :left_assoc]
>>
>
> iii) should probably read "(and (f t_1 t_2) ... (f t_1 t_n))".
>
>
Actually, it was meant to be "(and (f t_1 t_2) ... (f t_{n-1} t_n))"

[e.g., (< x1 x2 x3 x4) stands for (and (< x1 x2) (< x2 x3) (< x3 x4))]


Cesare


>
> Regards,
> Tjark
>
>