Unsupported operations on `Z3.ExprAllocated`

[goretkin]

I wanted to leverage the fallback definition of matrix multiplication in Julia's Base:

using Z3
ctx = Context()

# rotation, (cosine and sine representation)
c = real_const(ctx, "c")
s = real_const(ctx, "s")
R = [
    c s;
    -s c
]

but there are some missing definitions:

julia> R * [1, 2]
ERROR: MethodError: no method matching zero(::Z3.ExprAllocated)

I can define:

Base.zero(e::Z3.ExprAllocated) = Z3.int_val(ctx, 0) # TODO ctx should come from `e`, or not be used

And it works, however I suspect there is a better definition.

I also wanted unary +, just for symmetry. I've defined for that:

Base.:+(e::Z3.ExprAllocated) = e

[goretkin]

I came across https://github.com/ahumenberger/Z3.jl/blob/c280b1cda96a0bb774adc226f9295b64462de44d/src/Z3.jl#L71 and perhaps a reasonable definition is:

Base.zero(e::Z3.ExprAllocated) = Z3.num_val(Z3.ctx(x), 0, Z3.get_sort(x))

or perhaps

Base.zero(e::Z3.ExprAllocated) = Z3.num_val(Z3.ctx(x), false, Z3.get_sort(x))

If the expression is of sort bool, it probably makes sense for this to error in some way, since booleans behave differently in Z3 than in julia:

julia> tf = Z3.bool_const(ctx, "tf")
tf

julia> tf * tf
null

julia> tf + tf
null

julia> true * true
true

julia> true + true
2