Question: Why is Alt-ergo not answering SAT to trivial questions?

[giltho]

Hello,

Warning: the formulation might be interpreted as criticism of alt-ergo ("why can't alt-ergo solve trivial stuff?", this is not what I mean). It is not, I understand that the choices make sense in the context of verification, I am just curious about other use-cases.

Is there a particular reason why Alt-ergo isn't answering SAT to trivial questions? (Not meaning it can't solve them, it does!)

For instance, alt-ergo will have the following behaviour:

(set-logic ALL)
(check-sat) ; -> unknown

This is surprising, given that we know the answer quite immediately.
I know this is a design choice and not a bug, because on questions like:

(set-logic ALL)
(declare-fun Y () Int)

(assert (<= (- 2147483648) Y))
(assert (<= Y 2147483647))
(assert (not (= Y 0)))

(check-sat)
(get-model)

Alt-ergo returns unknown but (get-model) still shows a correct model, so under the hood, sat-solving is correctly happening. The question is: is Alt-ergo not answering sat because it would require additional effort that is (for verification) not required, or is there a more profound soundness reason?

I am asking because this behaviour makes alt-ergo unfit for under-approximate reasoning, where one needs to know that something is sat, but unknown and unsat collapes into "I don't care" (i.e. opposite of verification tasks).

Thank you!

[bclement-ocp]

Hello! Thank you for your interest in Alt-Ergo.

Currently, if your problem does not include quantifiers and Alt-Ergo produces a model, it should be a valid model and we could answer sat (there's also some issue with user-defined sorts at the moment #1270). The main reason we don't is that people usually use Alt-Ergo through Why3, and Why3 does its own model validation, so it just has not been implemented yet.

We've been having several requests for it (including yours) so it should hopefully be implemented for the next release though :)

In the meantime you could:

• Treat an output of unknown for quantifier-free problems that does successfully produce a model as sat;
• Use an external tool such as dolmen to verify the model

I understand neither of these are probably ideal for your situation, but that's what I can offer for now.

[giltho]

Oh interesting! Thank you for your answer
I'll try this approach!