I wrote an example collection

I wrote a collection of examples that could help beginners. I wrote those since I could not find the usual "examples" subfolder in the repo.

The output of the last example is more cryptic, since it results in things like "(root-obj (+ (* 64 (^ x 2)) (- 63)) 1)". Any mistake there?

using Z3

function run_model(s)
    res = check(s)
    if res != Z3.sat
        error("Z3.sat ERROR!")
    end

    m = get_model(s)

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

## Example 1
##
function ex1()
    ctx = Context()
    s = Solver(ctx, "QF_NRA")

    x = real_const(ctx, "x")
    y = real_const(ctx, "y")

    add(s, x == y^2)
    add(s, x > 1)

    run_model(s)
end

## Example 2
##
function ex2()
    ctx = Context()
    s = Solver(ctx, "QF_NRA")

    x = real_const(ctx, "x")
    y = real_const(ctx, "y")

    add(s, x > 2)
    add(s, y < 10)
    add(s, x + 2*y == 7)

    run_model(s)
end

## Unclear if this works or not.
## Example 3
##
function ex3()
    print("UNCLEAR IF THIS IS WORKING OR NOT")
    ctx = Context()
    s = Solver(ctx, "QF_NRA")

    x = real_const(ctx, "x")
    y = real_const(ctx, "y")

    add(s, (x^2 + y^2) > 3)
    add(s, (x^3 + y) < 5)
    run_model(s)
end

## Example 4
##
function ex4()
    ctx = Context()
    s = Solver(ctx, "QF_NRA")

    x = real_const(ctx, "x")
    y = real_const(ctx, "y")

    add(s, x + y < 10)
    run_model(s)
end

## Example 5
##
function ex5()
    ctx = Context()
    s = Solver(ctx, "QF_NRA")

    ax = real_const(ctx, "ax")
    ay = real_const(ctx, "ay")

    bx = real_const(ctx, "bx")
    by = real_const(ctx, "by")

    cx = real_const(ctx, "cx")
    cy = real_const(ctx, "cy")

   add(s, ax^2 + ay^2 == 1)
   add(s, ((ax - bx)^2 + (ay - by)^2) == 2)

    add(s, by == 0)
    add(s, cy == 0)
    add(s, (cx - bx) == 1)

    run_model(s)
end

ex1()
ex2()
ex3()
ex4()
ex5()

## Which Solvers can we use instead of "QF_NRA"?
## 
function dangerous_segmentation_fault()
    ctx = Context()
    Solver(ctx, "NON-EXISTING-BOGUS")   # the string could (or should?) be checked in Julia?
end

ahumenberger / Z3.jl

I wrote an example collection #7