aez
Alt-Ergo Zero is an OCaml library for an SMT solver.
This SMT solver is derived from Alt-Ergo. It uses an efficient SAT solver and supports the following quantifier free theories:
- Equality and uninterpreted functions
- Arithmetic (linear, non-linear, integer, real)
- Enumerated data-types
This API makes heavy use of hash consing, in particular hash-consed strings.
Homepage | http://cubicle.lri.fr/alt-ergo-zero/ |
---|---|
Maintainer | sylvain.conchon [at] lri.fr |
OCaml | >= 3.12 |
Events
Apr 25, 2013
Published version 0.3