[SMT-LIB] user_value vs. string

[Joseph Kiniry]

Hi Christoph et al,

On 4 Dec, 2006, at 17:39, Christoph M. Wintersteiger wrote:

> Hi all!
>
> just a short suggestion: Currently the rule for an annotation in  
> smt-lib
> format is
>
> annotation ::= <attribute> | <attribute> <user_value>
>
> while a user_value is of the form {...}.
>
> However, some theory-files (e.g. BitVecter32.smt) have annotation in
> string form "...".
>
> So, maybe it would be a good idea to update the standard to an
> annotation rule like
>
> annotation ::= <attribute> | <attribute> <user_value> | <attribute>
> <string>
>
> or maybe get rid of the user_value at all?

I strongly support keeping user_value.  We use them for VC  
generation, debugging, and generating program traces in other SMT- 
like languages and plan on doing the same for our SMT-backend.

As far as the syntax goes, so long as it does not introduce  
ambiguity, I don't mind what type of terminals are used.

Joe
---
Joseph Kiniry
School of Computer Science and Informatics
University College Dublin
http://secure.ucd.ie/
http://srg.cs.ucd.ie/