[SMT-LIB] Use of @ and . in a quoted symbol
Delcypher
delcypher at gmail.com
Fri Apr 24 13:32:12 EDT 2015
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.
More information about the SMT-LIB
mailing list