[SMT-LIB] Use of @ and . in a quoted symbol

[Grant Olney Passmore]

BTW, in Common Lisp, case matters here (abc and |abc| are not the same
symbol, but ABC and abc and |ABC| are):

? (equal 'ABC '|ABC|)
T
? (equal 'abc '|abc|)
NIL
? 'abc
ABC
? 'ABC
ABC
? '|abc|
|abc|
? '|ABC|
ABC

A short overview: http://cliki.net/Case%20sensitivity

Grant

On Sat, Apr 25, 2015 at 6:51 PM Tinelli, Cesare <cesare-tinelli at uiowa.edu>
wrote:

> Dan,
>
> On Page 21 of the SMT-LIB 2.0 document you have
>
> "Following Common Lisp's convention, enclosing a simple symbol in vertical
> bars does not produce a new symbol. This means for instance that abc and
> |abc| are the same symbol."
>
> For the same reasons, |.x| and .x  are the same symbol. That is why CVC4
> rejects |.x| in the declaration below.
>
>
> Cesare
>
>
> On 24 Apr 2015, at 12:32, Delcypher <delcypher at gmail.com> wrote:
>
> > Hi,
> >
> > I know that the ``@`` and ``.`` characters cannot be used as the first
> > character of a symbol but I was wondering if this was the case for
> > quoted symbols?
> >
> > For example
> >
> > ```
> > (set-option :print-success false)
> > (set-info :smt-lib-version 2.0)
> > (declare-fun |.x| () Int)
> > (check-sat)
> > ```
> >
> > CVC4 rejects this
> >
> > ```
> > (error "Parse Error: x.smt2:3.17: cannot declare or define symbol
> > `.x'; symbols starting with . and @ are reserved in SMT-LIB
> >
> >  (declare-fun |.x| () Int)
> >                ^
> > ")
> > ```
> >
> > but Z3 allows this.
> >
> > Could someone clarify if a symbol like ``|.x|`` is legal in SMT-LIB?
> > It isn't clear to me from reading the reference document (section on
> > concrete syntax) if it is legal or not.
> >
> > Thanks,
> > Dan.
> > _______________________________________________
> > SMT-LIB mailing list
> > SMT-LIB at cs.nyu.edu
> > http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>