# Z3 Theorem Prover

## Docs

- [Parameters](https://mintlify.wiki/Z3Prover/z3/api/advanced/parameters.md): Configure Z3 solver behavior with parameters
- [Proofs](https://mintlify.wiki/Z3Prover/z3/api/advanced/proofs.md): Generate and work with proof objects and unsat cores
- [Simplifiers](https://mintlify.wiki/Z3Prover/z3/api/advanced/simplifiers.md): Simplify formulas before solving with Z3 simplifiers
- [Statistics](https://mintlify.wiki/Z3Prover/z3/api/advanced/statistics.md): Collect and analyze Z3 solver performance metrics
- [Context API](https://mintlify.wiki/Z3Prover/z3/api/context.md): Z3 context and configuration management functions
- [Expression API](https://mintlify.wiki/Z3Prover/z3/api/expressions.md): Creating and manipulating Z3 expressions (ASTs)
- [Fixedpoint API](https://mintlify.wiki/Z3Prover/z3/api/fixedpoint.md): Recursive predicate solving and Datalog queries
- [Model API](https://mintlify.wiki/Z3Prover/z3/api/model.md): Extracting and interpreting satisfying assignments
- [Optimization API](https://mintlify.wiki/Z3Prover/z3/api/optimize.md): MaxSMT and optimization queries
- [Solver API](https://mintlify.wiki/Z3Prover/z3/api/solver.md): Incremental SMT solver interface
- [Sort API](https://mintlify.wiki/Z3Prover/z3/api/sorts.md): Type system and sort constructors in Z3
- [Tactics API](https://mintlify.wiki/Z3Prover/z3/api/tactics.md): Goal transformation and solving strategies
- [Arithmetic Theory](https://mintlify.wiki/Z3Prover/z3/api/theories/arithmetic.md): Integer and real arithmetic operations in Z3
- [Array Theory](https://mintlify.wiki/Z3Prover/z3/api/theories/arrays.md): Extensional array theory with select and store operations
- [Bit-Vector Theory](https://mintlify.wiki/Z3Prover/z3/api/theories/bitvectors.md): Fixed-size bit-vector operations in Z3
- [Algebraic Datatypes](https://mintlify.wiki/Z3Prover/z3/api/theories/datatypes.md): User-defined recursive and non-recursive datatypes in Z3
- [Finite Sets](https://mintlify.wiki/Z3Prover/z3/api/theories/finite-sets.md): Finite set theory with cardinality constraints
- [Floating-Point Arithmetic](https://mintlify.wiki/Z3Prover/z3/api/theories/floating-point.md): IEEE 754 floating-point arithmetic in Z3
- [Sequences and Strings](https://mintlify.wiki/Z3Prover/z3/api/theories/sequences.md): String and sequence operations including regular expressions
- [C API Reference](https://mintlify.wiki/Z3Prover/z3/bindings/c/api-reference.md): Complete reference for the Z3 C API
- [C API Getting Started](https://mintlify.wiki/Z3Prover/z3/bindings/c/getting-started.md): Learn the basics of using Z3 from C
- [C API Installation](https://mintlify.wiki/Z3Prover/z3/bindings/c/installation.md): Install and configure the Z3 C API
- [C++ API Reference](https://mintlify.wiki/Z3Prover/z3/bindings/cpp/api-reference.md): Complete reference for Z3 C++ API classes and methods
- [C++ API Getting Started](https://mintlify.wiki/Z3Prover/z3/bindings/cpp/getting-started.md): Learn the basics of using Z3 from C++
- [C++ API Installation](https://mintlify.wiki/Z3Prover/z3/bindings/cpp/installation.md): Building and linking Z3 with C++ projects
- [.NET API Reference](https://mintlify.wiki/Z3Prover/z3/bindings/dotnet/api-reference.md): Complete reference for the Z3 .NET API
- [.NET API Getting Started](https://mintlify.wiki/Z3Prover/z3/bindings/dotnet/getting-started.md): Learn the basics of using Z3 from .NET
- [.NET API Installation](https://mintlify.wiki/Z3Prover/z3/bindings/dotnet/installation.md): Install and configure Z3 for .NET applications
- [API Reference](https://mintlify.wiki/Z3Prover/z3/bindings/go/api-reference.md): Complete API reference for Z3 Go bindings
- [Getting Started](https://mintlify.wiki/Z3Prover/z3/bindings/go/getting-started.md): Quick start guide for Z3 Go bindings
- [Installation](https://mintlify.wiki/Z3Prover/z3/bindings/go/installation.md): Install and build Z3 Go bindings
- [Java API Reference](https://mintlify.wiki/Z3Prover/z3/bindings/java/api-reference.md): Complete reference for the Z3 Java API
- [Java API Getting Started](https://mintlify.wiki/Z3Prover/z3/bindings/java/getting-started.md): Learn the basics of using Z3 from Java
- [Java API Installation](https://mintlify.wiki/Z3Prover/z3/bindings/java/installation.md): Install and configure Z3 for Java
- [API Reference](https://mintlify.wiki/Z3Prover/z3/bindings/javascript/api-reference.md): Complete reference for Z3 JavaScript/TypeScript bindings
- [Getting Started](https://mintlify.wiki/Z3Prover/z3/bindings/javascript/getting-started.md): Quick start guide for Z3 JavaScript/TypeScript bindings
- [Installation](https://mintlify.wiki/Z3Prover/z3/bindings/javascript/installation.md): Install Z3 JavaScript/TypeScript bindings via npm
- [Getting Started](https://mintlify.wiki/Z3Prover/z3/bindings/ocaml/getting-started.md): Quick start guide for Z3 OCaml bindings
- [Installation](https://mintlify.wiki/Z3Prover/z3/bindings/ocaml/installation.md): Install Z3 OCaml bindings
- [Python API Reference](https://mintlify.wiki/Z3Prover/z3/bindings/python/api-reference.md): Complete reference for Z3 Python bindings
- [Getting Started with Z3 Python](https://mintlify.wiki/Z3Prover/z3/bindings/python/getting-started.md): Learn the basics of using Z3 in Python with examples
- [Python Installation](https://mintlify.wiki/Z3Prover/z3/bindings/python/installation.md): Install and configure Z3 Python bindings
- [Building with Bazel](https://mintlify.wiki/Z3Prover/z3/building/bazel.md): Build Z3 using Bazel for scalable, reproducible builds
- [Building with CMake](https://mintlify.wiki/Z3Prover/z3/building/cmake.md): Build Z3 using CMake for cross-platform development
- [Building with Make](https://mintlify.wiki/Z3Prover/z3/building/make.md): Build Z3 using Make and the Python configuration script
- [Building with Visual Studio](https://mintlify.wiki/Z3Prover/z3/building/visual-studio.md): Build Z3 on Windows using Visual Studio and MSVC
- [Expressions](https://mintlify.wiki/Z3Prover/z3/concepts/expressions.md): Understanding Z3's Abstract Syntax Trees and expression system
- [Models](https://mintlify.wiki/Z3Prover/z3/concepts/models.md): Understanding and working with satisfying assignments in Z3
- [Quantifiers](https://mintlify.wiki/Z3Prover/z3/concepts/quantifiers.md): Understanding quantified formulas, patterns, and instantiation in Z3
- [SMT Solving](https://mintlify.wiki/Z3Prover/z3/concepts/smt-solving.md): Understanding Satisfiability Modulo Theories in Z3
- [Solvers](https://mintlify.wiki/Z3Prover/z3/concepts/solvers.md): Using Z3's incremental solver interface
- [Tactics](https://mintlify.wiki/Z3Prover/z3/concepts/tactics.md): Building custom solvers with Z3's tactic framework
- [Automated Testing](https://mintlify.wiki/Z3Prover/z3/examples/automated-testing.md): Generating test inputs and finding edge cases with Z3
- [Basic Constraint Solving](https://mintlify.wiki/Z3Prover/z3/examples/basic-solving.md): Learn the fundamentals of Z3 with simple constraint solving examples
- [Constraint Solving](https://mintlify.wiki/Z3Prover/z3/examples/constraint-solving.md): Using Z3 for scheduling, planning, and configuration problems
- [Model Checking](https://mintlify.wiki/Z3Prover/z3/examples/model-checking.md): Verifying temporal properties and system invariants with Z3
- [Optimization Problems](https://mintlify.wiki/Z3Prover/z3/examples/optimization-problems.md): Learn to find optimal solutions using Z3 Optimize for MaxSMT and optimization
- [Program Verification](https://mintlify.wiki/Z3Prover/z3/examples/program-verification.md): Use Z3 to verify correctness of algorithms and find bugs automatically
- [Sudoku Solver](https://mintlify.wiki/Z3Prover/z3/examples/sudoku-solver.md): Build a complete Sudoku solver using Z3 constraint programming
- [Symbolic Execution](https://mintlify.wiki/Z3Prover/z3/examples/symbolic-execution.md): Path exploration and bug finding using symbolic execution with Z3
- [Finite Sets](https://mintlify.wiki/Z3Prover/z3/guides/finite-sets.md): Use Z3's FiniteSets theory for reasoning about finite set operations, membership, and cardinality
- [Fixedpoint and Datalog](https://mintlify.wiki/Z3Prover/z3/guides/fixedpoint.md): Use Z3's fixedpoint engine for Datalog queries, Horn clauses, and program verification with PDR/IC3
- [Floating-Point Arithmetic](https://mintlify.wiki/Z3Prover/z3/guides/floating-point.md): Work with IEEE 754 floating-point numbers in Z3, including rounding modes, special values, and conversions
- [Optimization](https://mintlify.wiki/Z3Prover/z3/guides/optimization.md): Learn how to use Z3's optimization features including MaxSMT, weighted constraints, and multi-objective optimization
- [Sequences and Strings](https://mintlify.wiki/Z3Prover/z3/guides/sequences-strings.md): Work with strings and sequences in Z3, including concatenation, length, substrings, regular expressions, and string constraints
- [Installation](https://mintlify.wiki/Z3Prover/z3/installation.md): Install Z3 on your system using pre-built binaries or build from source
- [Introduction to Z3](https://mintlify.wiki/Z3Prover/z3/introduction.md): Learn what Z3 is and how it can help you solve complex constraint problems
- [Quickstart](https://mintlify.wiki/Z3Prover/z3/quickstart.md): Get started with Z3 in under 5 minutes