You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
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 is 0 < 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.
This does not currently work:
It results in:
The text was updated successfully, but these errors were encountered: