Typing allows the invalid expression Int + Bool

[elsoroka]

It's possible to construct an expression of the form BoolExpr + IntExpr which is not valid in Z3, thus it should not be constructable in Satisfiability.jl

[mykelk]

Do other solvers support this? If so, then maybe we might want the API to allow it, but for the solver to raise an exception if it is not supported by that particular solver.

[elsoroka]

This is a good point.
I checked in CVC5 and it appears to be an error there as well. I think more importantly, the specification for the theory of integers (https://smtlib.cs.uiowa.edu/theories-Ints.shtml) says that arithmetic operators (+, -, * etc) only operate on Int expressions, while comparisons (<, > etc) can operate on Int or Bool expressions. So I think it is a bug.

I see how the bug arose -- I implemented the comparison operators first and didn't catch the different typing.

[elsoroka]

PLOT TWIST The bug-ness of this is up for debate because as @mykelk said, other solvers support it -- specifically Z3, where I did most of my testing, allows mixed arithmetic/bool statements (while CVC5 does not).

Minimal example:

(declare-const x Bool)
(declare-const a Int)
(assert (< 1 (+ a x)))
(check-sat)
(get-model)

Z3 outputs

(
  (define-fun a () Int
    2)
  (define-fun x () Bool
    false)
)

Internally, Z3 is replacing x in the arithmetic expression with (ite x 1 0). You can see this using the command (simplify (+ a x)) which outputs (+ a (ite x 1 0)).
CVC5 (and probably others) does NOT allow this.

The same behavior is apparent for mixing Real, Int, and Bool.

(declare-const x Bool)
(declare-const r Real)
(declare-const a Int)
(simplify (+ x a r))

yields (+ (ite x 1.0 0.0) (to_real a) r).

I think for user convenience, the resolution of this "bug" should be to do the Z3 thing:

• Wrap Bool expressions in arithmetic expressions with the if-then-else statement for Int or Real as appropriate.
• Wrap Int expressions in mixed real/int arithmetic with to_real.

The current behavior of Satisfiability.jl yields SMT-LIB statements like the above ((+ x a r)) which work in Z3 but aren't actually correct for the SMT-LIB specification.