1
2
3
4
5
6
7
8
9
10
11
12
13
14
// first, run the following statements
z3
=
this
.
get
(
"Z3Module"
)
.
module
z3
.
initialize
(
)
bbb
.
defaultSolver
=
z3
a
=
pt
(
0
,
0
)
b
=
pt
(
1
,
1
)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
Just a small Demo of NaCl Z3 with Babelsberg.
1
// print this next line entirely. It will have the old values, because NaCLZ3 is async and had no time
solving the system
always
:
{
a
.
dist
(
b
)
==
200
}
;
[
a
,
b
,
a
.
dist
(
b
)]
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
1
// Afterwards, print this, the async assignment should have happened by now (unless Z3 crashed)
[
a
,
b
,
a
.
dist
(
b
)]
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
World successfully saved
✗