Add support for chaining
Opened this issue · 1 comments
mykelk commented
This does not currently work:
@satvariable(alpha, Real)
sat!(0 ≤ alpha ≤ 1)
It results in:
TypeError: non-boolean (BoolExpr) used in boolean context
elsoroka commented
This is interesting because in the context of SMT, we expect 0 ≤ alpha ≤ 1
to be semantically equivalent to (0 ≤ alpha) ∧ (alpha ≤ 1)
. In Satisfiability.jl, (0 ≤ alpha) ∧ (alpha ≤ 1)
constructs a BoolExpr
object, since the value of alpha
isn't known.
This will shortly become relevant:
- Operators such as Base.:+ and Base.:& can be extended. However, there isn't a Base.:&& because && is control flow, not a function.
- So
(0 ≤ alpha) && (alpha ≤ 1)
(using the control-flow "and" instead of the logical∧
) doesn't work, which makes sense.- As a side note,
(0 ≤ alpha) & (alpha ≤ 1)
is possible to define, although it is not currently defined in Satisfiability.jl.
- As a side note,
Why this is relevant:
Based on an inspection with InteractiveUtils.code_llvm
, I think 0 ≤ alpha ≤ 1
is equivalent to (0 ≤ alpha) && (alpha ≤ 1)
.
Experiment setup:
using Satisfiability
import Base.&
Base.:&(a::BoolExpr, b::BoolExpr) = a ∧ b
@satvariable(alpha, Real)
a = 0.5
f(a) = (0 < a) && (a < 1)
g(a) = 0 < a < 1
h(a) = (0 < a) & (a < 1)
Now, if we test these we see:
- f(a), g(a) and h(a) are all true
- f(alpha) and g(alpha) yield the same error @mykelk reported
- BECAUSE we extended Base.:&, h(alpha) yields the BoolExpr (0 < a) ∧(a < 1)
But what is0 < a < 1
?
# The output of f and g for a Float64 variable `a` have identical LLVM code on my machine, and h has very similar code.
println(InteractiveUtils.code_llvm(f, Tuple{Float64}))
println(InteractiveUtils.code_llvm(g, Tuple{Float64}))
println(InteractiveUtils.code_llvm(h, Tuple{Float64}))
# code_llvm for f(alpha) and g(alpha) calls `ijl_type_error`
println(InteractiveUtils.code_llvm(f, Tuple{RealExpr}))
println(InteractiveUtils.code_llvm(g, Tuple{RealExpr}))
# code_llvm for h(alpha) is obviously very different from the others
# println(InteractiveUtils.code_llvm(h, Tuple{RealExpr}))
I think chained comparisons are rewritten using &&. So it may not be possible to support chaining Satisfiability.jl expressions.