Add support for chaining

[mykelk]

This does not currently work:

@satvariable(alpha, Real)
sat!(0 ≤ alpha ≤ 1)

It results in:

TypeError: non-boolean (BoolExpr) used in boolean context

[elsoroka]

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.