Wrong model in the non-regression tests

[Halbaroth]

Alt-Ergo outputs a wrong model on this SMTLIB input:

(set-logic QF_UF)
(set-option :produce-models true) ; enable model generation
(declare-const p Bool)
(declare-const q Bool)
(assert (=> (not p) (not q)))
(check-sat)
(get-model)

The output:

unknown
(
)

and the command : dune exec -- alt-ergo --frontend dolmen --produce-models

[bclement-ocp]

This is a dupe of #777, no? We probably should have a single issue for model unsoundness (although in this case the model is not unsound, it is incomplete).

Should we postpone these to 2.6.0? Although these are unfortunate, we don't claim anything on the soundness (or absence thereof) of models in 2.5.0, and the release is already way past due.

[Halbaroth]

I don't think so. I guess AE failed to produce a complete model because functions returning boolean values are converted into predicates.

[bclement-ocp]

I am not saying the cause is the same in both cases, but that I think it would make more sense to consolidate all the incorrect models into a single issue rather than having one issue for each possible cause. Since the outcomes are related, it would be easier to have a single place to go to for all the info/insight/etc. we have on this rather than have it be scattered.

[Halbaroth]

After investigating more, I think I found the origin of the bug. The problem comes from case-splits. Consider this very simple problem:

(set-logic QF_UF)
(set-option :produce-models true) ; enable model generation
(declare-const p Bool)
(declare-const q Bool)
(assert (or p q))
(check-sat)
(get-model)

Alt-Ergo produces the partial model { p = true } but we expect something as { p = true; q = whatever }. While reasoning on p, AE found that true satisfies this formula and it didn't explore at all the other branch, which means it didn't add the q in the UF and AE ignores that the term q exists during the model generation phase.

If we permute p an q in the above problem, we got the partial model { q = true } and replacing the or gate by an and gate produces a complete model.

[Halbaroth]

I wrote a fix for this issue that is not completely satisfactory. The idea is really simple:

• The frontend has to remember which terms have been declared by the user. Notice that a term cannot be both declared and defined in the SMT standard or the native language. I create a separate hash table to collect declared terms in d_cnf.
• I converted this table into a list and feeds output_concrete_model with it.
• I iterate on this list in Models.output_concrete_model after producing all the terms from the union-find.
• If the declared term is not in the model yet, I produce a dummy value for it and print it.

This solution is not satisfactory for many reasons:

• First of all, we iterate twice on the list of declared terms.
• We have to transmit these terms while printing the model.
• The missing terms are not in the map of the model.

I have a better solution that requires substantially more work.

Besides, saving the declared terms in the frontend fixes another issue caused by the preprocess phase of AE. Consider the input:

(set-logic ALL)
(set-option :produce-models true)
(declare-const p Bool)
(declare-const q Bool)
(assert (and (or p (not p)) q))
(check-sat)
(get-model)

Alt-Ergo will not produce a value for p as the tautology or p (not p) is wiped out by the preprocess phase.

[bclement-ocp]

That sounds right, we do need to collect the defined stuff in the frontend because we lose that information later.

The hash table shouldn't be necessary, collecting the Term_decl in a list should be enough (although there is probably some shenanigans wrt push/pop commands that must be taken care of -- but that is also true for the hash table).

Instead of iterating on the list in Models.output_concrete_model with custom printing code, why not use it to fill in default values in Uf.compute_concrete_model, instead of using empty initial maps for fprofs / cprofs / carrays? These should then get overwritten by Uf.compute_concrete_model as appropriate.