Unknown syntax in model produced by Alt-Ergo 2.6.0

[manmatteo]

Since Alt-Ergo 2.6.0, we are getting literals starting with . in the produced models, and I am not sure how they should be interpreted (currently Why3 considers them invalid syntax). For example in this file:

(set-logic ALL)
(set-option :produce-models true)
(declare-sort t 0)
(declare-fun q (t) Int)
(declare-fun o (Int) t)
(assert (forall ((i Int)) (or (> 0 0) (= i (q (o i))))))
(check-sat)
(get-model)

I obtain the model

unknown
(
  (define-fun q ((arg_0 t)) Int
   (ite (= arg_0 .k1) 1 (ite (= arg_0 .k0) 0 (- 1))))
  (define-fun o ((arg_0 Int)) t
   (ite (= arg_0 1) (as @a2 t) (ite (= arg_0 0) (as @a3 t) (as @a4 t))))
)

The definition of o contains things like (as @a2 t), that I expect. The definition of q contains .k0 instead, which seem to play a similar role but, for instance, skips the type annotation.

[Gbury]

In the SMT-LIB standard, identifiers starting with either a . or a @ are reserved for use by solvers in models (or more generally in the output produced by solvers). This helps solvers more easily generate names with the guarantee they they do not clash with existing names from the input. So from the point of view of why3, these should be regular identifiers. That being said, in the output you showed, the identifiers that start with a dot appear to not be bound or defined, so that looks like an internal error of alt-ergo (probably a missing substitution before printing a model).

[manmatteo]

I see. It is strange that we only started observing this problem with Alt-Ergo 2.6.0 then. As for the fact that they are not bound, isn't it the same also for the @ identifiers in the output above? I am used to seeing them appear without being declared, and I think the model parser in Why3 already deals with this.

[Gbury]

Right, so there is a difference between identifiers starting with a . and those starting with @: identifiers with a dot should be regular identifiers, the dot is only there to prevent conflicts with names from the input problem, so in particular these identifiers should be defined.

On the other hand, identifiers starting with an @ are called "abstract values", and are meant to not be defined, and instead represent some arbitrary value of their type (on that topic, abstract values should always be used enclosed by a type annotation, i.e. in the form (as @foo some_type)). They are useful in a few cases, most notably for arrays, since the SMT-LIb theory of arrays do not give any function to create an array (i.e. all functions that return an array also take an array as argument), so abstract values are the only way to have some kind of base value for arrays in models (though that may change in future versions with the addition of a const function).

[manmatteo]

Ok, thank you for the explanation! So it seems that there is really an issue in Alt-Ergo, since some . identifiers we see are not defined. At the same time, Why3 is not complaining about unbound symbols, but really about unparsed symbols, so there might be a problem in Why3 as well.

[bclement-ocp]

That's not good, we are supposed to make all of those disappear and are replaced with abstract values (using @) prior to printing. Thanks for the report — I will look into it.