feat: check-all-sat support

[Halbaroth]

This PR adds the support for the check-all-sat support. I think we can merge the PR without clean-up its implementation as the feature doesn't break the classical model generation. Please see #847 for a clean-up roadmap of this feature.

The PR includes two ways to use this new feature:

• using the new CLI option --all-sat (or --all-models), AE produces all the possible propositional models after each check-sat. For instance using the input file:

(set-logic ALL)
(declare-const x Bool)
(declare-const y Bool)
(declare-const z Bool)
(assert (or x y))
(assert (or (not y) z))
(check-sat)

and the command dune exec -- alt-ergo --all-sat --produce-models --sat-solver CDCL test.smt2, we got the output:

output of the command

                                
; File "test.smt2", line 7, characters 1-12: I don't know (0.4635) (7 steps) (goal g_1)
unknown
; Returned timeout reason = NoTimeout
(
(define-fun x () Bool true)
(define-fun y () Bool false)
(define-fun z () Bool false)
)
; File "test.smt2", line 7, characters 1-12: I don't know (0.4636) (13 steps) (goal g_1)
unknown
; Returned timeout reason = NoTimeout
(
(define-fun x () Bool false)
(define-fun y () Bool true)
(define-fun z () Bool true)
)
; File "test.smt2", line 7, characters 1-12: I don't know (0.4637) (17 steps) (goal g_1)
unknown
; Returned timeout reason = NoTimeout
(
(define-fun x () Bool true)
(define-fun y () Bool false)
(define-fun z () Bool true)
)
; File "test.smt2", line 7, characters 1-12: I don't know (0.4638) (23 steps) (goal g_1)
unknown
; Returned timeout reason = NoTimeout
(
(define-fun x () Bool true)
(define-fun y () Bool true)
(define-fun z () Bool true)
)
; File "test.smt2", line 7, characters 1-12: Valid (0.4638) (23 steps) (goal g_1)
unsat

• A new keyword check-all-sat is available in the SMT-LIB input language only. For instance

(set-logic ALL)
(declare-const x Bool)
(declare-const y Bool)
(declare-const z Bool)
(assert (or x y))
(assert (or (not y) z))
(check-all-sat x y)

with the command dune exec -- alt-ergo --produce-models --sat-solver CDCL --frontend legacy test.smt2 outputs

output of the commad

; File "test.smt2", line 7, characters 1-20: I don't know (0.0003) (7 steps) (goal g_1)
unknown
; Returned timeout reason = NoTimeout
(
(define-fun x () Bool true)
(define-fun y () Bool false)
(define-fun z () Bool false)
)
; File "test.smt2", line 7, characters 1-20: I don't know (0.0005) (14 steps) (goal g_1)
unknown
; Returned timeout reason = NoTimeout
(
(define-fun x () Bool false)
(define-fun y () Bool true)
(define-fun z () Bool true)
)
; File "test.smt2", line 7, characters 1-20: I don't know (0.0005) (16 steps) (goal g_1)
unknown
; Returned timeout reason = NoTimeout
(
(define-fun x () Bool true)
(define-fun y () Bool true)
(define-fun z () Bool true)
)
; File "test.smt2", line 7, characters 1-20: Valid (0.0006) (16 steps) (goal g_1)
unsat

This feature is clearly more interesting as you can choose for which literals you want all the boolean models.

The PR includes also another option to print a boolean model while printing the first-order model. The feature is broken but I can restore it easily. I'm not sure if the option is really useful, at least while using the SMT-LIB input language, as there is a standard way to obtain this feature (in fact a more general feature), see #844. We should deprecate the option or reserve it for the native input language.

Some important remarks about the feature:

• The feature doesn't work properly with the tableaux solver. The reason is simple and I actually ran into this issue while testing outputted models with the Tableaux solver. I have a solution that I will explain in details in an appropriate issue.
• The solver outputs unsat at the end because it exhausted all the possible boolean models. This answer leaks the way AE works under the hood. I guess the best solution consists to print a comment telling we have exhausted all the boolean models. But fixing this issue will be easier after fixing #833.

[bclement-ocp]

Before reviewing the code in detail, I want to better understand what we are trying to achieve with that feature, so I will only make high-level remarks here.

It was my understanding that this feature was required for OptimAE. After looking at the code, it doesn't appear to be the case, as OptimAE uses a different mechanism to iterate over the propositional models for optimization (in fact, in the OptimAE branch, the all-models feature has been implemented after the rest of the optimization work). Given that OptimAE does not need this feature, and that it is actually fairly small and self-contained (all changes but those in frontend.ml seem to be trivial plumbing), we can evaluate the feature on its own merit without rushing to merge the implementation as-is.

As an aside, this feature was initially implemented for an unnamed intern project in 2011, dropped during the development of OptimAE (the removal was merged in #530) and then re-implemented later --- but if I had to wager, without that one-day hack in 2011, it would not have been implemented in OptimAE.

With that out of the way, I am not sure we want to merge this at all. I don't think there is much value in enumerating propositional models rather than actual models in general (in part because having a propositional model does not guarantee that a corresponding model of the input formula exists), and if we care about models, then model enumeration can be implemented outside the solver.

The typical way to implement model enumeration uses incremental solving: first get a model using (check-sat), get the value of the propositional term(s) you are interested in with (get-assignment) (see #844), assert that one of them should be false, then call (check-sat) again and repeat until you get unsat. Replace (check-sat) and (get-assignment) by the appropriate (incremental) API calls if not using SMT-LIB input.

I agree that providing this loop in a built-in way would be useful (in fact, the current implementation uses the exact loop I described above), but given that there is no rush for the feature I think it would be better to first clean up the interface to be able to do proper incremental solving (rather than giving a single list of commands and we're done, as we discussed) and to implement this feature on top of the incremental solving API once it exists (I think the relevant issue is #382 ).

Edit: as a side note, we should all this check-allsat rather than check-all-sat when using SMT-LIB to be compatible with MathSat5, see bottom of https://mathsat.fbk.eu/smt2examples.html

[Halbaroth]

I agree to postpone this feature until we have a sufficient support for incremental mode.