Mismatch between hasInstance and simplestValue

[jad-hamza]

There are some mismatches between hasInstance and simplestValue

inox/src/main/scala/inox/ast/SymbolOps.scala

Line 906 in 7752948

def hasInstance(tpe: Type): Option[Boolean] = tpe match {

• hasInstance returns true on types defined outside of Inox (such as ArrayType)
• they don't seem to behave the same for ADTType, as hasInstance doesn't visit constructor fields?
• they're different for TypeParameter, I guess that's expected?

Should we make them just one function (returning an Option), or is the distinction necessary?
And we should override these functions in Stainless for ArrayType? (always true?)

[jad-hamza]

For context, I'm looking at this because I got a crash on simplestValue here for nested arrays/ADTs:
https://github.com/epfl-lara/stainless/blob/1fa4365e71fc4ad054ea051a0a1d09f1027a3480/core/src/main/scala/stainless/solvers/InoxEncoder.scala#L132

[samarion]

hasInstance returns true on types defined outside of Inox (such as ArrayType)

I thought the ArrayType encoding added an ADT invariant. I would expect hasInstance to return None in that case.

they don't seem to behave the same for ADTType, as hasInstance doesn't visit constructor fields?

That looks like a bug to me.

they're different for TypeParameter, I guess that's expected?

I believe hasInstance is expected to be more conservative than simplestValue (e.g. for type parameters which might correspond to empty types in general, but do have simplest values).

Should we make them just one function (returning an Option), or is the distinction necessary?

You can probably merge the two functions, but you would still need to add an extra parameter which controls how conservative the behavior should be.

Note that the current hasInstance API allows it to return Some(false) when we're sure no instance exists, which won't be possible from the Option[Expr] interface. However, this feature doesn't seem to actually be used anywhere in the Inox codebase so it's probably fine to drop it.

And we should override these functions in Stainless for ArrayType? (always true?)

You can try, but it might not help. It depends on whether the simplestValue is called on the encoded Inox type or the Stainless one. What is your use case?

[samarion]

One issue I noticed with simplestValue is that we optimistically select the ADT constructor with fewest parameters when creating an instance, which might lead to loops. I believe we should instead select the constructor which has the fewest mutually recursive types in its signature. We might even want to write a custom type traversal to ignore recursive types under function types.

[jad-hamza]

You can try, but it might not help. It depends on whether the simplestValue is called on the encoded Inox type or the Stainless one. What is your use case?

It's for the crash described in my reply (where we call simplestValue on Stainless trees), sorry I should have added that to the original post.

[samarion]

It's for the crash described in my reply (where we call simplestValue on Stainless trees), sorry I should have added that to the original post.

Ah yes, then overriding both methods would indeed help (and make a lot of sense) here.

[samarion]

Fixed by @jad-hamza in #151