Example of getting all solutions

[goretkin]

This is a question, not necessarily specific to the Julia interface to Z3, and a note to others who might need to solve a similar problem of producing all feasible solutions. Is this the recommended way in Z3?

The snippet below produces the indices of all unit square grid cells (pixels) that intersect with a circle of radius 10.

using Z3

ctx = Context()
x = int_const(ctx, "x")
y = int_const(ctx, "y")
dx = real_const(ctx, "dx")
dy = real_const(ctx, "dy")

c = real_const(ctx, "c")
s = real_const(ctx, "s")

solver = Solver(ctx, "QF_NRA")

radius = 10
add(solver, c^2 + s^2 == 1)
add(solver, x + dx == radius * c)
add(solver, y + dy == radius * s)
add(solver, -0.5 <= dx)
add(solver, dx <= 0.5)
add(solver, -0.5 <= dy)
add(solver, dy <= 0.5)

sols = []
while true
    res = check(solver)
    res == Z3.sat || break

    m = get_model(solver)

    x_ = get_numeral_int(Z3.eval(m, x))
    y_ = get_numeral_int(Z3.eval(m, y))
    push!(sols, (x_, y_))
    @show length(sols)
    add(solver, or(x != x_,  y != y_))
end

reference = [(-10, -3), (-10, -2), (-10, -1), (-10, 0), (-10, 1), (-10, 2), (-10, 3), (-9, -5), (-9, -4), (-9, -3), (-9, 3), (-9, 4), (-9, 5), (-8, -7), (-8, -6), (-8, -5), (-8, 5), (-8, 6), (-8, 7), (-7, -8), (-7, -7), (-7, 7), (-7, 8), (-6, -8), (-6, 8), (-5, -9), (-5, -8), (-5, 8), (-5, 9), (-4, -9), (-4, 9), (-3, -10), (-3, -9), (-3, 9), (-3, 10), (-2, -10), (-2, 10), (-1, -10), (-1, 10), (0, -10), (0, 10), (1, -10), (1, 10), (2, -10), (2, 10), (3, -10), (3, -9), (3, 9), (3, 10), (4, -9), (4, 9), (5, -9), (5, -8), (5, 8), (5, 9), (6, -8), (6, 8), (7, -8), (7, -7), (7, 7), (7, 8), (8, -7), (8, -6), (8, -5), (8, 5), (8, 6), (8, 7), (9, -5), (9, -4), (9, -3), (9, 3), (9, 4), (9, 5), (10, -3), (10, -2), (10, -1), (10, 0), (10, 1), (10, 2), (10, 3)]

@assert Set(reference) == Set(sols)

[goretkin]

In particular, I have a question about how to access the assignment to e.g. x without referring to "x", and without using get_numeral_int, since I would the code to be more general.

This is in contrast to the example in the README, which would use "x" instead of x.

for (k, v) in consts(m)
    println("$k = $v")
end