Crash when using & instead of && for Booleans

[jad-hamza]

The & operator produces a crash with an exception

Exception in thread "main" inox.ast.TypeOps$TypeErrorException: Type error

object Untyped {
  def untyped(a: Boolean) = {
    require(a & a)    
    assert(true)
  }
}

[mantognini]

Currently Inox doesn't support & | ^ on Boolean, but it should. I'll add support for that as well in epfl-lara/inox#26.

[samarion]

Hmm, I'm not sure we actually need these within Inox. The operators are easy to encode using let bindings, && and ||. In general, I'd prefer Inox to stay as simple as possible and handle such encoding / extraction issues within Stainless itself.

[mantognini]

The issue I see with mapping it to && and || is that those don't have the same semantics (short-circuit doesn't apply on & and |). As for ^, we could use != but it wouldn't have the same operator precedence. Wouldn't that create more issues in the long term? (The way I planned to modify inox was limited to BV* operators.)

[samarion]

If you use

val a = b1
val b = b2
a && b

you get the same semantics as & (and similar encodings for the other ones).

About operator precedence, I don't mean we should not support these operators in the frontend (namely Stainless), but I don't think they are required in the solving backend (namely Inox). Operator precedence isn't really an issue in Inox since we aren't going to be parsing anything.

If you meant that you would only be adding support for these within the Stainless PR linked to https://github.com/epfl-lara/inox/pull/26, then I completely agree :)

[mantognini]

I now see your point. Patch will be available through stainless only.

[mantognini]

Support for this is included in #33.

[jad-hamza]

The original example is now emitting this exception:

[Internal] java.util.NoSuchElementException: key not found: class stainless.extraction.imperative.Trees$BoolBitwiseAnd

[samarion]

Re-fixed in https://github.com/epfl-lara/stainless/commit/d322b4a6792cc30516b79948e70669219c9e14a8