Open
Description
cl-z3 provides Common Lisp bindings for the Z3 Satisfiability Modulo Theories solver. In short, this interface allows one to leverage Z3's ability to solve constraints involving variables over numbers, strings, bitvectors, uninterpreted functions, and more, including optimization problems.
Author: Andrew Walter
License: MIT
Repo: https://github.com/mister-walter/cl-z3
Thanks, and let me know if you have any questions or concerns!