search

flux-rs / flux

Refinement Types for Rust
MIT License
632 stars 17 forks source link

add support for lnot on ints and uints #574

Closed enjhnsn2 closed 8 months ago

enjhnsn2 commented 9 months ago

fixes #571

enjhnsn2 commented 9 months ago

sgtm, I'll add the duplicate signature and test. I'll take a look at the other int -> int functions to try and find a well-formed replacement for E::tt()

enjhnsn2 commented 9 months ago

wait, the shift functions use E::tt() and those are int -> int functions. Why is it right there and wrong here? (note, I don't really understand what E::tt() does lol) 

(Shl, s!(fn(a: Int, b: Int) -> Int{ v: E::tt() })),
enjhnsn2 commented 9 months ago

it was my impression (from context) that E::tt() told Flux to treat the operorator as an uninterpreted function, as in the other bitwise operations:

// BIT
(BitAnd, s!(fn(a: Int, b: Int) -> Int{v: E::tt()})),
(BitOr,  s!(fn(a: Int, b: Int) -> Int{v: E::tt()})),
nilehmann commented 9 months ago

E::tt() means the true formula so you can read Int{v: E::tt()} as Int{v: true}

The problem is not E::tt() but using brackets instead of braces. Using brackets as in Int[E::tt()] would mean Int[true] which is not well-formed because (rust) integers have to be refined by (logical) integers. Instead, Int{v: E::tt()} is an existential type, i.e., the index is existentially quantified and the formula E::tt() is a constraint on the index (a trivial restriction in this case).