# zee3 v0.3.0 - Table of Contents

Bindings to the Z3 theorem prover.

## Modules

- [Zee3](Zee3.md): Documentation for `Zee3`.

- [Zee3.Defzee3](Zee3.Defzee3.md)
- [Zee3.Interpreter](Zee3.Interpreter.md): Translates Z3 S-Expression ASTs into native Elixir data types,
and compiles Z3 lambdas into executable Elixir anonymous functions.
- [Zee3.Smt2](Zee3.Smt2.md)
- [Zee3.Smt2.BitVec](Zee3.Smt2.BitVec.md): Module to represent Z3 bit vector literals.

- [Zee3.Smt2.Int](Zee3.Smt2.Int.md): Module to represent Z3 integer literals.

- [Zee3.Smt2.List](Zee3.Smt2.List.md): Module to represent Z3 list literals.

- [Zee3.Smt2.Parser](Zee3.Smt2.Parser.md): A NimbleParsec implementation for parsing SMT-LIB2 S-Expressions.
- [Zee3.Smt2.String](Zee3.Smt2.String.md): Module to represent Z3 string literals.

- [Zee3.Smt2.Symbol](Zee3.Smt2.Symbol.md): Module to represent Z3 string literals.

- [Zee3.StdLib](Zee3.StdLib.md): Defines the functions and macros which are available
inside the body of the `Zee3.program/2` macro.
- [Zee3.StdLib.Sort](Zee3.StdLib.Sort.md): Standard SMT-LIB2 Sorts (Types) for the Zee3 DSL.
- [Zee3.StdLib.StdLibBuilder](Zee3.StdLib.StdLibBuilder.md)

## Mix Tasks

- [mix compile.zee3](Mix.Tasks.Compile.Zee3.md)

