[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