[RFC] Input AST of the SAT API

[Halbaroth]

I open this issue because I was trying to solve properly the issue #778 yesterday and I got stuck with the SAT solver API. We know that Alt-Ergo produces partial models because of preprocessing and optimizations in the SAT solvers. In #778, we was agreed that a good solution is to collect in d_cnf all the declared symbols and feed the get_model method with them. This solution will work, and actually I wrote the PR already but I wasn't very pleased with it. This solution doesn't solve the issue if you use the SAT API directly. A library's user should expect to get a complete model if he/she calls the get_model method of the SAT API.

After thinking about it, I think that the core issue is the fact we used a preprocessed AST for the input expressions of the SAT API.
The current Expr AST assumes three roles:

1. The parsed (and typed) AST.
2. A preprocessed AST.
3. A CNF AST for the formulas.

I think we should use three different ASTs here:

1. A subset of the Dolmen AST as input of the SAT API.
2. For the preprocessed AST, we may use again the Dolmen one but we have to perform the preprocessing phase in the SAT solver at the very beginning of assume. So basically, we could create a new module Preprocess that takes a Dolmen AST and returned a preprocessed one. We may add some memoization here.
3. We have already a CNF AST for SatML and actually we translate the CNF AST of FunSAT to the CNF AST of SatML. We should push the CNF AST from Expr into FunSAT and use directly the CNF AST of SatML into SatML. Again the transformation of formulas into CNF formulas has to be performed in assume.

A possible roadmap to do this work could be:

• Remove the legacy parser and perform some clean-ups.
• Move the CNF AST from Expr into FunSAT and remove the translation performed in satml_frontend. The CNF transformation is performed in the SAT solvers.
• Create a preprocess module which transforms a Expr AST into a Expr AST.
• Use this preprocess at the very beginning of the assume (before the CNF transformation).
• Replace Expr by a subset of the Dolmen AST.

[bclement-ocp]

Assuming that by "the SAT API" you mean the Frontend / Sat_solver_sig API, they don't currently have a concept of symbols being declared; switching to using the Dolmen AST instead will not change that.

Long-term pushing the Dolmen AST downwards is probably the move (although we do need to be careful about hash-consing), but I'd say we should wait until we remove the legacy frontend to do so. Could we instead have an API to explicitly declare symbols to the solver, which would be used by d_cnf? The user would then only be guaranteed to have values in the models for the symbols that have been explicitly declared.

We can then revisit that design and come up with a better solution (probably centered around the Dolmen AST as you suggest) once we drop the legacy frontend and the related constraints.

[Halbaroth]

Ok, I reword what I mean in this issue. The main problem is the fact some preprocessing computations are performed in the Expr AST before feeding the SAT solver with these expressions.

If we don't do that before giving a formula to assume, it's almost solved the issue with incomplete models because we can scan the formula in assume to collect declared symbols and we don't need to add an ugly declaration primitive to our SAT API. There is only one case where the model is still incomplete with this solution: if you don't use at all the symbol in any asserted formulas. For instance:

(set-option :produce-models true)
(set-logic ALL)
(declare-const x Int)
(check-sat)
(get-model)

I suggest to use a subset of the Dolmen AST because we could simplify a lot D_cnf. Nevertheless, there are some stumbling blocks as the purification or the skolemization of formulas.

Of course, this refactoring requires a lot of work and I don't plan do it for a specific release.

[bclement-ocp]

I am not sure we should be inspecting the formulas for this; it'd be better to have some sort of context object (see e.g. Z3's API) to keep track of declared symbols (to be clear, this context object should have an equivalent of Expr.mk_name that tracks the created identifiers with type context -> string -> symbol, not a context -> symbol -> unit function to use after the fact). This would avoid needing a separate mechanism for the declared-but-unused symbols (which we do need to support for SMT-LIB compliance).