# crux v0.1.3 - Table of Contents

> Library for boolean satisfiability solving and expression manipulation.

## Modules

- [Crux](Crux.md): <!--
  SPDX-FileCopyrightText: 2025 crux contributors <https://github.com/ash-project/crux/graphs.contributors>
  SPDX-License-Identifier: MIT
-->
- [Crux.Expression](Crux.Expression.md): Boolean expression representation and manipulation for SAT solving.
- [Crux.Expression.RewriteRule](Crux.Expression.RewriteRule.md): Behaviour for defining expression rewrite rules.
- [Crux.Formula](Crux.Formula.md): A module for representing and manipulating satisfiability formulas in
Conjunctive Normal Form (CNF).

- [Crux.Formula.Tseitin](Crux.Formula.Tseitin.md): Tseitin transformation from a boolean `Crux.Expression` into CNF.
- [Crux.Implementation](Crux.Implementation.md): This module provides an interface to a SAT solver.

- Rewrite Rules
  - [Crux.Expression.RewriteRule.AbsorptionLaw](Crux.Expression.RewriteRule.AbsorptionLaw.md): Rewrite rule that applies absorption laws to simplify expressions.
  - [Crux.Expression.RewriteRule.AnnihilatorLaw](Crux.Expression.RewriteRule.AnnihilatorLaw.md): Rewrite rule that applies boolean annihilator laws.
  - [Crux.Expression.RewriteRule.AssociativityLaw](Crux.Expression.RewriteRule.AssociativityLaw.md): Rewrite rule that applies associativity optimizations to simplify expressions.
  - [Crux.Expression.RewriteRule.CommutativityLaw](Crux.Expression.RewriteRule.CommutativityLaw.md): Rewrite rule that applies commutativity laws to normalize expression order.
  - [Crux.Expression.RewriteRule.ComplementLaw](Crux.Expression.RewriteRule.ComplementLaw.md): Rewrite rule that applies complement laws to simplify expressions.
  - [Crux.Expression.RewriteRule.ConsensusTheorem](Crux.Expression.RewriteRule.ConsensusTheorem.md): Rewrite rule that applies the consensus theorem to eliminate redundant clauses.
  - [Crux.Expression.RewriteRule.DeMorgansLaw](Crux.Expression.RewriteRule.DeMorgansLaw.md): Rewrite rule that applies De Morgan's laws to expressions.
  - [Crux.Expression.RewriteRule.DistributiveLaw](Crux.Expression.RewriteRule.DistributiveLaw.md): Rewrite rule that applies the distributive law to convert expressions to CNF.
  - [Crux.Expression.RewriteRule.DistributivityBasedSimplificationLaw](Crux.Expression.RewriteRule.DistributivityBasedSimplificationLaw.md): Rewrite rule that applies distributivity-based simplifications to expressions.
  - [Crux.Expression.RewriteRule.IdempotentLaw](Crux.Expression.RewriteRule.IdempotentLaw.md): Rewrite rule that applies idempotent laws to simplify expressions.
  - [Crux.Expression.RewriteRule.IdentityLaw](Crux.Expression.RewriteRule.IdentityLaw.md): Rewrite rule that applies boolean identity laws to simplify expressions.
  - [Crux.Expression.RewriteRule.NegationLaw](Crux.Expression.RewriteRule.NegationLaw.md): Rewrite rule that applies negation laws to simplify expressions.
  - [Crux.Expression.RewriteRule.TautologyLaw](Crux.Expression.RewriteRule.TautologyLaw.md): Rewrite rule that detects common tautology patterns.
  - [Crux.Expression.RewriteRule.UnitResolution](Crux.Expression.RewriteRule.UnitResolution.md): Rewrite rule that applies unit resolution to propagate unit clauses.