Closed Halbaroth closed 4 months ago
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 ?
As you wish, I opened it only as a remainder but if you believe this feature is unwanted, I agree to close it.
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).
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
:
dolmen
binary to accept such files if given alone (that is the current behaviour)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:
typing_wrap
function exposed hereDolmen_loop.Typer.T
, which is exposed here, and whose type in particular contains these functionsDolmen_loop.Typer.T.decl_term_const
on the typing env provided by typing_wrap
to add the constants that the solver creates, and that should be available.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.
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)?
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.
@bclement-ocp @Halbaroth any news on that one ?
The PR https://github.com/OCamlPro/alt-ergo/pull/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.
According to the SMT-LIB standard (see page 49 and 65), we can use abstract values returned by a previous
get-value
statement in a new statement. For instance:Let's imagine the last statement produces the output:
Then the statement:
is valid even if
@array1
isn't a part of signature.Notice that this feature can be used only in an interactive mode. Otherwise, there is no way to predict the abstract value returned by the previous
get-value
.Both
Z3
andcvc5
don't print an abstract value for the arraya
butAlt-Ergo
does.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.