NaCLZ3
X
–
Menu
this.z3.initialize()
bbb.defaultSolver = this.z3
this.a = pt(0,0)
this.b = pt(1,1)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
always: { this.a.dist(this.b) == 200 }; [this.a, this.b, this.a.dist(this.b)]
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
// Afterwards, print this, the async assignment should have happened by now (unless Z3 crashed)
[this.a, this.b, this.a.dist(this.b)]
this.a.x = 10
[this.a, this.b, this.a.dist(this.b)]
this.b = pt(20,20)
[this.a, this.b, this.a.dist(this.b)]
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
You must have enabled Native Client in Chrome's about:flags! Check the output of the console. Then run the following statements.
NaCl is async-only. If you print the following line entirely, the constraints will not be solved when printing the array.
After a browser loop, the constraints are solved and these have the right values. You can go on and change parts of a or b, or replace this.a and this.b with new points. The constraints will be re-satisfied.