Re:Programming in Z3 by learning to think like a compiler
by csb6 on Monday May 03, 2021 @01:52PM
(#27028335)
Here [1] is a cool project that uses Z3 to make graphics specified by constraints.
I remember reading an article about someone using Z3 to optimize the placement of cutout drawings on a piece of paper (kind of like a spritesheet) and optimizing for the smallest possible area in order to reduce the use of paper/materials. However, I can't seem to find the article anywhere.
One more use of z3 is as one of the available solvers for a tool called gnatprove [2], which is used to prove/verify the correctness of programs written in the SPARK subset of the Ada programming language. SPARK is used to program safety-critical aeronautical/military projects.
I remember reading an article about someone using Z3 to optimize the placement of cutout drawings on a piece of paper (kind of like a spritesheet) and optimizing for the smallest possible area in order to reduce the use of paper/materials. However, I can't seem to find the article anywhere.
One more use of z3 is as one of the available solvers for a tool called gnatprove [2], which is used to prove/verify the correctness of programs written in the SPARK subset of the Ada programming language. SPARK is used to program safety-critical aeronautical/military projects.
[1] https://www.anishathalye.com/2019/12/12/constraint-based-gra...
[2] https://docs.adacore.com/spark2014-docs/html/ug/en/gnatprove...