No value printed in models for declared constants without constraint

[Halbaroth]

Consider the input file

(set-logic ALL)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)

(assert (distinct a b))
(check-sat)
(get-model)

Calling AE with the command $ alt-ergo --produce-models input.smt2 outputs

unknown
(
  (define-fun a () Int 2)
  (define-fun b () Int 0)
)

According to the SMT-LIB, models have to contain definitions for all declared constants.

[bclement-ocp]

I think that this is because we never call Uf.make on unused symbols, and we probably don't want to do that so as to avoid overloading the data structure.

Ideally we would have access to the actual list of declared symbols somewhere, but I don't think we have that currently, and from my understanding we would have to dig a bit into the guts of how model generation works to fix this. We are trying to avoid doing that until #553 is merged so I don't know if it's worth fixing for 2.5.0 ?

[Halbaroth]

I think that this is because we never call Uf.make on unused symbols, and we probably don't want to do that so as to avoid overloading the data structure.

This was my insight of the root of the problem. I agree we cannot change this quickly. I postponed it for the next release.

[bclement-ocp]

Another thing we need to be careful about: currently we create the Expr.t only when the symbols are used. Changing it to creating the Expr.t at declaration time would have implications for the weak table & the expression's ID :(

[Halbaroth]

Exactly! We have to clean up the way we use ID in the UF before fixing this issue.

[bclement-ocp]

I think maintaining a separate list of declared symbols (as Symbols.t, not Expr.t) and inspecting that list at model generation time as I described above would also work without impacting the weak table?

[bclement-ocp]

The code in the issue now prints the following (with --produce-models):

unknown
(
  (define-fun a () Int 1)
  (define-fun b () Int 0)
  (define-fun c () Int (as @a0 Int))
)