Product Description
Z3 is a state-of-the art theorem prover from Microsoft Research.
Includes many efficient custom solvers for data-type theories that are common in program testing, verification, synthesis, and analysis. Z3 integrates efficient constraint solving technologies for propositional satisfiability, free functions, linear arithmetic over the reals and integers, bit-vectors, algebraic data-types, and applicative arrays. It can be used for checking satisfiability of logical formulas with quantifiers, as well by leveraging quantifier instantiation procedures, saturation, and quantifier-elimation procedures for reals, integers, and algebraic datatypes. Besides supporting a rich base of theories, Z3 is also highly customizable with an extensive API and support for custom theories.