Comments (8)
Currently, dolmen
does not check answers from get-value
statements (I haven't tried, but I'd say you'd get either a syntax error or another error), and it's not clear what would be the point: the only thing that dolmen
could check would be that the returned values are coherent with the model previously returned, which might be of interest, but doesn't appear to be that useful right now (but I might be wrong on that point). In any case, if/when dolmen
supports checking get-value
answers, then obviously, it will be in the context of the previous model, which means any abstract values introduced in that model would indeed be in scope.
With that said, I'd propose to close this issue, unless I missed something ?
from dolmen.
As you wish, I opened it only as a remainder but if you believe this feature is unwanted, I agree to close it.
from dolmen.
We don't plan to implement an interactive mode for AE but if we do, we'll need to fix this issue to be
SMT-LIB
compliant.
FWIW Alt-Ergo does have a bare-bones interactive mode for SMT-LIB input (see OCamlPro/alt-ergo#949). Parsing and typing errors make it crash currently but it is still useful for quick tests.
That said, I don't think the issue is really related to checking. Handling this properly (when using dolmen_loop
) requires to introduce new identifiers when (get-model)
or (get-value)
are invoked that should automatically go out of scope when leaving sat
mode, and I think that the only way to do this currently is by abusing Typer.additional_builtins
with ad-hoc state management in user code. Given that the typer already maintains a stack of typer states (for push
/ pop
) it would be useful to be able to somehow hook into that (although I am not sure what the best way to do so would be — it kind of messes up the pipe's flow, so maybe that's not a good idea).
from dolmen.
Ok, so I was really confused for a while and I didn't really understand what feature was being asked, but I see I'm starting to see. If I understand correctly, @Halbaroth is saying that a smt2 file such as the following:
(set-option :produce-models true)
(set-logic ALL)
(declare-const a (Array Int Int))
(check-sat)
(get-value (a))
(get-value ((select @array1 0 0)))
is technically valid if one supposes the answer to the first get-value
(the one for a
), returned
(a (as @array1 (Array Int Int)))
and therefore, @Halbaroth would like it if alt-ergo (when using the dolmen
frontend) would accept such a sequence of declarations, which is not currently the case because dolmen
would complain of an unbound symbol @array1
.
That means different things depending on the use of dolmen
:
- For the binary. This means the validity (i.e. whether a file is conformant to the smtlib specification) of an input file is actually dependent on the answer of the solver being fed the file. Said differently, that means that the validity of the file cannot be checked just by looking at the file. Therefore there is no way for the
dolmen
binary to accept such files if given alone (that is the current behaviour) - For users of the library. First, and as noted in comments above, this is mainly useful in the context of an interactive session. In any case, to properly support such inputs, the user of the
dolmen
library would have to add to the typing env the adequate bindings whenever an abstract value is emitted (as part of a response to a command). I agree that it is not very easy to find out how to do that, but it is possible currently.
In order to add a new term (or type) symbol to the typing env from a loop, the steps would be:
- use the
typing_wrap
function exposed here - this function gives you access to a typing env, which you can manipulate using the module
Dolmen_loop.Typer.T
, which is exposed here, and whose type in particular contains these functions - you can thus use
Dolmen_loop.Typer.T.decl_term_const
on the typing env provided bytyping_wrap
to add the constants that the solver creates, and that should be available. - now comes the problem of the scope of these new constants, as pointed out by @bclement-ocp . To do this, some
push
/pop
operations could indeed solve the problem if inserted correctly. To do this, you can use the function exposed here . Finally, just in case you were wondering, these operation are extremely cheap currently (the typechecker only uses persistent maps, so a push operation just saves the current maps, and pop restores the saved maps).
All that being said, considering the need to maintain a part of the typing env that would be tied to the sat
/unsat
state of the solver, I'd say right now it's probably easier currently to use a dedicated typing builtin. For the future, the typer loop could offer some dedicated support for that kind of situation, but that would require a faire bit of work to find out a nice enough API, and I currently have other relatively pressing things to add in dolmen
, so if you have any concrete suggestion, I'm happy to discuss them.
from dolmen.
Thanks for the detailed explanation! I missed the typing_wrap
function, which does seem to provide what we'd need to implement this on the Alt-Ergo side, so it seems there is indeed nothing more Dolmen can do.
Further thoughts: this would not need to depend on the sat
/unsat
state of the solver per se, but rather on the current mode of the SMT-LIB automaton. We could have an automaton pipe before the typer (either exposing some internals of the Flow module, or a custom one — we already have some logic in Alt-Ergo for this that could be converted to a pipe) that uses typing_wrap
to push
the typer state upon entering sat
or unsat
mode and to pop
it upon leaving. This shouldn't impact the typer logic for push
/ pop
statement because those can't occur in Sat_or_unsat_mode
. Then, when encountering a Get_model
/ Get_value
inside the typer pipe, we could use decl_term_const
without worrying about scoping.
Would that sound like a good way to do this for library users (not asking to implement this in Dolmen, trying to understand how best to implement this in Alt-Ergo)?
from dolmen.
I agree that this depends on the mode of the SMT-LIB automaton, and therefore one could handle that by using appropriate push
/pop
operations in a pipe before the typechecker. That being said, it should be done carefully, because unless I missed something, one can do a push
/pop
operation while in Sat_or_unsat_mode
, and therefore, this new pipe will have to know what other pipes are doing in order to correctly insert additional push
/pop
operations, but it should be doable and a reasonable way to do this.
from dolmen.
@bclement-ocp @Halbaroth any news on that one ?
from dolmen.
The PR OCamlPro/alt-ergo#1032 is stalled until we have a decent incremental mode for Alt-Ergo (which isn't planned for the next release as you know). Besides, the feature isn't crucial, so we can close this issue and open a new one if we need this feature later.
from dolmen.
Related Issues (20)
- Spec errors on the difference logic benchmarks of the SMT-LIB HOT 2
- 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
- Quoted identifiers can be keywords HOT 12
- Warning regarding the `dolmen_type` file HOT 2
- Support non-incremental parsing from stdin HOT 1
- 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
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.