I wrote an example collection

[SteveElp]

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]

(root-obj (+ (* 64 (^ x 2)) (- 63)) 1) is an algebraic number representing the first root of the polynomial 64*x^2 - 63. You can get a real approximation via Expr::get_decimal_string.

https://github.com/Z3Prover/z3/blob/6f0a3673574932e5105a5c136bafc148b25fe03c/src/solver/smt_logics.cpp#L24 contains a list of logics for which it is possible to create a solver.

Regarding the segmentation fault: This should be catched in the Z3 C++ API and turned into a C++ exception which can be caught on the Julia side.