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

[Tinelli, Cesare]

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