Comments (12)
I think that's correct, i'll fix that.
from dolmen.
That being said, after a bit more thinking, this is really weird, and maybe should not be done. Using reserved words as identifiers, even quoted, just seems prone to confusion, and doesn't seem to be supported in a consistent way by existing solvers.
For instance, Z3 supports (declare-const |forall| Int)
but CVC5 doesn't; on the other hand CVC5 supports (declare-const |_| Int)
while Z3 doesn't, and both support (declare-const |!| Int)
. All of these are part of the set of reserved words.
It is probably fine to take the lax interpretation of "Following Common Lisp’s conventions, enclosing
a simple symbol in vertical bars does not produce a new symbol." as implying that assert
and |assert|
are the same "pseudo-symbol" and hence neither is valid as a symbol.
from dolmen.
It's not easy to determine indeed, but first let me state that for most things related to the spec, the behaviour of solvers is not really a good indication (sadly enough). Basically, the problem boils down to the following two choices:
- quoted symbols allow to quote reserved words and turn them into symbols, allowing for instance the following statement
(declare-fun |assert| () Bool)
- on the other hand, if the quoting mechanism is completely transparent, and quoted reserved words behave as reserved words, then the following statement should be legal:
(|assert| false)
So basically, this is the choice we have: exactly one of the two statements above should be legal (and the other not). I would say that for now my reading of the specification would make me go towards the first solution (i.e. quoting allows to use usually reserved names as symbol names), but I agree it's not really clear.
from dolmen.
I think there is a third reading, which is the one I was going for: quoted reserved words behave as reserved words in contexts where a quoted symbol is allowed by the grammar.
(declare-fun |assert| () Bool)
is rejected, because(declare-fun <symbol> () Bool)
is allowed and the symbol isassert
, which is a reserved word;(|assert| false)
is accepted, because the syntax is(assert <term>)
, not(<symbol> <term>)
from dolmen.
In fact there is a weird discrepancy in the way that the standard excludes reserved words versus symbols starting with @
or .
from being used. From a strict reading of the spec:
- Reserved words are not simple symbols;
- Simple symbols starting with
@
or.
are "reserved for solver use"; - "Enclosing a simple symbol in vertical bars does not produce a new symbol" (emphasis mine)
So |assert|
is OK, even though assert
is a reserved word, because assert
is not a simple symbol, |assert|
is not "enclosing a simple symbol in vertical bars"; but |@assert|
is reserved, because @assert
is a simple symbol, and so |@assert|
and @assert
are the same symbol.
On the other hand, |@é|
is technically allowed, since it is not a "simple symbol starting with @
or .
" (and yet I believe it is rejected after #185 ).
from dolmen.
Your understanding is probably the one that matches the (quite fuzzy) specification of the smtlib spec. That being said, I'd argue for a slightly different semantics for a few reasons.
So first, my proposition:
- in my proposed semantics:
|assert|
would act as a symbol (and not a reserved word), so you can define/declare/let-bind it - any symbol (whether it be quoted or simple in the source) would be reserved if it starts with an
@
or a.
Now for a few reasons:
- first: simplicity. At least for the aspects of the spec that are not specific enough, I'd argue that the simpler and most intuitive/coherent behaviour should be used
- second: usability/intent. At least in my opinion quoting is there to.. well quote things, so my interpretation of quoted symbols is to allow users to quote symbols that otherwise may not be accepted as simple symbols. Reasons for not being accepted as simple symbols are mainly tied to the syntax, so these reasons can be for instance whitespace-related (as the examples in the spec show), but it can also be that the symbol that one wanted to use is a reserved word. In that case, it makes sens to me to allow users to not have to rename their symbols, and therefore to allow quoted reserved word as symbols.
- lastly, about
|@é|
and the like, here I'd argue for simplicity and predictability of the syntax, as well as separation of the syntax and typing/name resolving parts of the language: quoting is a syntax mechanism to overcome some difficulty related to the syntax of symbols/identifiers, as well as the usefullness of reserved word for parsing (which would make it extremely annoying/complex to try and supportassert
as both a reserved word or a symbol depending on its position in the source). On the other hand symbols reserved for solver use is a typing/name resolution thing: the restriction is not enforced during parsing, and the rules that drives it are more closely related to name resolution, and name shadowing than, the syntax.
That way quoting is only relevant in the parser, and the information of what was quoted disappears afterwards, and not used during typing, because it makes more sense for quoting to be a syntax solution to a syntax problem, and typing can then simply not care about the syntax.
from dolmen.
Yeah, I also think that this is the most reasonable implementation.
That said, if quoted keywords are allowed, it would be really useful for Dolmen to provide quoting printers so that users don't have to manage the list of keywords on their own when printing models.
from dolmen.
Yup, such functions will be part of the printing functionality of Dolmen (which I should really get to soon..).
from dolmen.
My point is that even without the full printing functionality having only these functions would be very helpful, and probably easier to implement than the full printing functionality (but maybe not that much?).
from dolmen.
Well, it's more that these functions solve one very particular problem, which is to ensure that what you print is likely to be parseable, however, it doesn't ensure that what is parsed is what you want (e.g. that you didn't accidentally shadow some variables or definitions).
from dolmen.
True, but for my specific use case (which is model printing in Alt-Ergo), having just those functions should be enough :)
from dolmen.
Hm.. right, I'll add those functions as soon as I have the time.
from dolmen.
Related Issues (20)
- Reject names starting with `@` and `.` outside of models
- Handling of `set-option :global-declarations`
- Handling of named terms HOT 2
- Check sat assuming HOT 2
- DIMACS variables do not appear as decls HOT 1
- Uncaught exception on buggy file
- 4.08 support broken (`List.concat_map`) HOT 10
- Warning regarding the `dolmen_type` file HOT 2
- Support non-incremental parsing from stdin HOT 1
- Handling abstract values in `(get-value)` statements HOT 8
- Supporting evaluation for custom functions HOT 5
- Question regarding BV logic in SMT files HOT 14
- Support `bv2nat` as a "relaxed mode" HOT 2
- Attributes in nested quantifiers HOT 2
- RDL check is a bit too lenient HOT 1
- Can we get a formal 1.0 release please HOT 4
- Confusing error message with pattern matching on polymorphic type in ae's native language
- Support for `get-assignment` HOT 2
- Support for custom attributes
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from dolmen.