Z3 is a Satisfiability Modulo Theories (SMT) solver. It is an automated satisfiability checker for many-typed first-order logic with built-in theories, including support for quantifiers. The currently supported theories are:
- equality over free (aka uninterpreted) function and predicate symbols
- real and integer arithmetic
- bit-vectors and arrays
- tuple/records/enumeration types and algebraic (recursive) data-types.
Z3 checks whether a set of formulas is satisfiable in the built-in theories. When the set of formulas is existential then Z3 is a decision procedure: it is
always guaranteed to return a correct answer.
- If a set of formulas F is satisfiable, Z3 can produce a model for F.
- If a set of formulas contains universal quantifiers, then the model produced by Z3 should be viewed as a potential model, since Z3 is incomplete in this case.
No comments:
Post a Comment