I wrote an example collection #7
Description
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