Handling abstract values in (get-value) statements

[Halbaroth]

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:

(set-option :produce-models true)
(set-logic ALL)
(declare-const a (Array Int Int))
(check-sat)
(get-value (a))

Let's imagine the last statement produces the output:

(a (as @array1 (Array Int Int)))

Then the statement:

(get-value ((select @array1 0 0)))

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 and cvc5 don't print an abstract value for the array a but Alt-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.

[Gbury]

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 ?

[Halbaroth]

As you wish, I opened it only as a remainder but if you believe this feature is unwanted, I agree to close it.

[bclement-ocp]

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).

[Gbury]

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 by typing_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.

[bclement-ocp]

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)?

[Gbury]

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.

[Gbury]

@bclement-ocp @Halbaroth any news on that one ?

[Halbaroth]

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.