[SAL] Re: question about Yices

[Bruno Dutertre]

Maria Paola Bonacina wrote:
> Dear Bruno or Leonardo,
> 
> for the attached input file ex3.ys, Yices generates the model
> 
> x = -2
> y = 2
> f(0) = 1
> f(1) = 3
> 
> Why does it generate precisely this model and not another one?
> 
> Thank you very much for any hint you can provide.
> 
> Cheers,
> Maria Paola
> 
> 

Maria Paola,

Yices builds an E-graph to represent the constraints. It puts
equal terms into equivalence classes. When you ask for a model,
Yices assigns an integer value to each class by taking them in
order and using a counter. The first class is given value 0,
if possible, then the counter is incremented and the second class
is given value 1 if possible, and so forth. So the exact model you
get depends on which order the classes are considered. The actual
procedure used is slightly more complicated but that's the general
idea.

Bruno