# `Crux.Expression`
[🔗](https://github.com/ash-project/crux/blob/v0.1.3/lib/crux/expression.ex#L6)

Boolean expression representation and manipulation for SAT solving.

Provides a DSL for creating boolean expressions with the `b/1` macro, plus functions
for traversal, evaluation, simplification, and CNF conversion.

# `cnf`

```elixir
@type cnf(variable) :: cnf_conjunction(variable)
```

Conjunctive Normal Form (CNF) expression.

CNF is a conjunction (AND) of clauses, where each clause is a
disjunction (OR) of literals. A literal is either a variable,
a negated variable, or a boolean constant.

Examples:
- `a` (single literal)
- `a OR b` (single clause)
- `(a OR b) AND c` (two clauses)
- `(a OR NOT b) AND (c OR d)` (two clauses with negation)

# `cnf_clause`

```elixir
@type cnf_clause(variable) ::
  {:or, cnf_clause(variable), cnf_clause(variable)} | cnf_literal(variable)
```

A clause in CNF - a disjunction (OR) of literals.

Can be either a single literal or multiple literals joined by OR.

# `cnf_conjunction`

```elixir
@type cnf_conjunction(variable) ::
  {:and, cnf_conjunction(variable), cnf_conjunction(variable)}
  | cnf_clause(variable)
```

A conjunction (AND) of clauses in CNF.

Can be either a single clause or multiple clauses joined by AND.

# `cnf_literal`

```elixir
@type cnf_literal(variable) :: variable | {:not, variable} | boolean()
```

A literal in CNF.

Can be:
- A variable
- A negated variable
- A boolean constant

# `t`

```elixir
@type t() :: t(term())
```

See `t/1`.

# `t`

```elixir
@type t(variable) ::
  {:and, t(variable), t(variable)}
  | {:or, t(variable), t(variable)}
  | {:not, t(variable)}
  | true
  | false
  | variable
```

Represents an expression.

# `walker`

```elixir
@type walker(variable, acc) ::
  walker_stateless(variable) | walker_stateful(variable, acc)
```

A walker function that can be either stateless or stateful.

# `walker_stateful`

```elixir
@type walker_stateful(variable, acc) :: (t(variable), acc -> {t(variable), acc})
```

A stateful walker function that operates on expressions with an accumulator.

Takes an expression and an accumulator, returns a transformed expression
and updated accumulator.

# `walker_stateless`

```elixir
@type walker_stateless(variable) :: (t(variable) -> t(variable))
```

A stateless walker function that operates on expressions.

Takes an expression and returns a transformed expression.

# `all_or_none`

```elixir
@spec all_or_none([variable]) :: t(variable) when variable: term()
```

Returns an expression that ensures all variables have the same truth value.

This function creates constraints where either all variables are true together,
or all are false together (also known as "mutually inclusive" or "biconditional"
constraints). It's useful for modeling linked states like database transactions,
feature flags, or cache coherency where states must be synchronized.

## Examples

    iex> # Database transaction - both happen or neither
    ...> all_or_none([:begin_transaction, :commit_transaction])
    {:not,
     {:and, {:or, :begin_transaction, :commit_transaction},
      {:not, {:and, :begin_transaction, :commit_transaction}}}}

    iex> # Feature flags - UI and API dark mode go together
    ...> all_or_none([:dark_mode_ui, :dark_mode_api])
    {:not,
     {:and, {:or, :dark_mode_api, :dark_mode_ui}, {:not, {:and, :dark_mode_api, :dark_mode_ui}}}}

    iex> # Empty list always satisfied
    ...> all_or_none([])
    true

    iex> # Single variable always satisfied
    ...> all_or_none([:single])
    true

## Truth Table for [:a, :b, :c]

| :a | :b | :c | Valid? |
|----|----|----|--------|
| F  | F  | F  | ✓      |
| T  | T  | T  | ✓      |
| T  | F  | F  | ✗      |
| F  | T  | F  | ✗      |
| F  | F  | T  | ✗      |
| T  | T  | F  | ✗      |
| T  | F  | T  | ✗      |
| F  | T  | T  | ✗      |

# `at_most_one`

```elixir
@spec at_most_one([variable]) :: t(variable) when variable: term()
```

Returns an expression that ensures at most one of the given variables can be true.

This function creates constraints where any two variables cannot both be true
simultaneously (also known as "mutually exclusive" constraints). It's useful for
modeling scenarios like user roles, payment methods, or file states where only
one option should be active at a time.

## Examples

    iex> # User roles - person can have at most one role
    ...> at_most_one([:admin, :user, :guest])
    {:and, {:and, {:not, {:and, :admin, :user}}, {:not, {:and, :admin, :guest}}},
     {:not, {:and, :guest, :user}}}

    iex> # Payment methods - choose at most one option
    ...> at_most_one([:credit_card, :paypal])
    {:not, {:and, :credit_card, :paypal}}

    iex> # Empty list always satisfied
    ...> at_most_one([])
    true

    iex> # Single variable always satisfied
    ...> at_most_one([:single])
    true

## Truth Table for [:a, :b, :c]

| :a | :b | :c | Valid? |
|----|----|----|--------|
| F  | F  | F  | ✓      |
| T  | F  | F  | ✓      |
| F  | T  | F  | ✓      |
| F  | F  | T  | ✓      |
| T  | T  | F  | ✗      |
| T  | F  | T  | ✗      |
| F  | T  | T  | ✗      |
| T  | T  | T  | ✗      |

# `b`
*macro* 

Creates tuples of a boolean statement.

Supports basic boolean operations (`and`, `or`, `not`) as well as higher-order
boolean operators for common logical patterns.

## Examples

    iex> # Complex expression using basic operators
    ...> b((:a and not :b) or (not :c and :d))
    {:or, {:and, :a, {:not, :b}}, {:and, {:not, :c}, :d}}

    iex> # NAND (Not AND) - "not both"
    ...> b(nand(:a, :b))
    {:not, {:and, :a, :b}}

    iex> # NOR (Not OR) - "neither"
    ...> b(nor(:a, :b))
    {:not, {:or, :a, :b}}

    iex> # XOR (Exclusive OR) - "exactly one"
    ...> b(xor(:a, :b))
    {:and, {:or, :a, :b}, {:not, {:and, :a, :b}}}

    iex> # XNOR (Not Exclusive OR) - "both or neither"
    ...> b(xnor(:a, :b))
    {:not, {:and, {:or, :a, :b}, {:not, {:and, :a, :b}}}}

    iex> # IMPLIES - "if A then B"
    ...> b(implies(:a, :b))
    {:not, {:and, :a, {:not, :b}}}

    iex> # IMPLIED_BY - "A if B"
    ...> b(implied_by(:a, :b))
    {:not, {:and, :b, {:not, :a}}}

# `balance`

```elixir
@spec balance(expression :: t(variable)) :: t(variable) when variable: term()
```

Balances a boolean expression by normalizing operand order.

This function sorts operands in AND and OR expressions to create a canonical
form that makes expressions easier to compare and reason about.

# `exactly_one`

```elixir
@spec exactly_one([variable]) :: t(variable) when variable: term()
```

Returns an expression that ensures exactly one of the given variables is true.

This function combines `at_most_one/1` with additional constraints ensuring that
at least one variable must be true (also known as "mutually exclusive and
collectively exhaustive" constraints). It's useful for modeling radio button
scenarios like order status, user preferences, or permission levels where exactly
one option must be selected.

## Examples

    iex> # User preference - must pick exactly one theme
    ...> exactly_one([:light_theme, :dark_theme])
    {:and, {:or, :light_theme, :dark_theme}, {:not, {:and, :dark_theme, :light_theme}}}

    iex> # Empty list can never satisfy exactly one
    ...> exactly_one([])
    false

    iex> # Single variable must be true
    ...> exactly_one([:single])
    :single

## Truth Table for [:a, :b, :c]

| :a | :b | :c | Valid? |
|----|----|----|--------|
| F  | F  | F  | ✗      |
| T  | F  | F  | ✓      |
| F  | T  | F  | ✓      |
| F  | F  | T  | ✓      |
| T  | T  | F  | ✗      |
| T  | F  | T  | ✗      |
| F  | T  | T  | ✗      |
| T  | T  | T  | ✗      |

# `expand`

```elixir
@spec expand(expression :: t(variable), callback :: (t(variable) -> t(variable))) ::
  t(variable)
when variable: term()
```

Expands a boolean expression using a callback function without accumulator.

Convenience function for when no accumulator state is needed.

## Examples

    iex> expand(b(:a and true), fn
    ...>   var when is_variable(var) -> var
    ...>   other -> other
    ...> end)
    :a

# `expand`

```elixir
@spec expand(
  expression :: t(variable),
  acc,
  callback :: (t(variable), acc -> {t(variable), acc})
) :: {t(variable), acc}
when variable: term(), acc: term()
```

Expands a boolean expression using a callback function with accumulator.

Similar to `run/2` but exposes the accumulator and uses a callback for expansion
rather than just variable evaluation. This allows for more complex transformations
that need to maintain state across the traversal.

## Examples

    iex> expand(b(:a and :b), [], fn
    ...>   var, acc when is_variable(var) -> {var, [var | acc]}
    ...>   other, acc -> {other, acc}
    ...> end)
    {b(:a and :b), [:b, :a]}

    iex> expand(b(true or :a), [], fn
    ...>   var, acc when is_variable(var) -> {var, [var | acc]}
    ...>   other, acc -> {other, acc}
    ...> end)
    {true, []}
    # Note: :a is not visited due to short-circuiting

# `generate_expression`

```elixir
@spec generate_expression(StreamData.t(variable)) :: StreamData.t(t(variable))
when variable: term()
```

Generates random boolean expressions for property-based testing.

Uses StreamData.tree to create recursive boolean expressions with the provided
leaf generator for terminal values. Automatically includes booleans alongside
the provided inner generator.

# `in_cnf?`

```elixir
@spec in_cnf?(expression :: t(variable)) :: boolean() when variable: term()
```

Checks if an expression is in Conjunctive Normal Form (CNF).

CNF is a conjunction (AND) of clauses, where each clause is a
disjunction (OR) of literals. A literal is either a variable,
a negated variable, or a boolean constant.

## Examples

    iex> in_cnf?(b(:a and :b))
    true

    iex> in_cnf?(b(:a or :b))
    true

    iex> in_cnf?(b((:a or :b) and :c))
    true

    iex> in_cnf?(b(:a or (:b and :c)))
    false

    iex> in_cnf?(b(not (:a and :b)))
    false

    iex> in_cnf?(b(not :a))
    true

# `is_literal`
*macro* 

# `is_operation`
*macro* 

# `is_variable`
*macro* 

# `postwalk`

```elixir
@spec postwalk(expression :: t(variable), fun :: walker_stateless(variable)) ::
  t(variable)
when variable: term()
```

Performs a depth-first, post-order traversal of the expression.

## Examples

    iex> postwalk(b(:a and :b), fn
    ...>   {:and, left, right} -> {:or, left, right}
    ...>   other -> other
    ...> end)
    {:or, :a, :b}

    iex> postwalk(b(:a and (:b or :c)), fn
    ...>   {:and, left, right} -> {:or, left, right}
    ...>   {:or, left, right} -> {:and, left, right}
    ...>   other -> other
    ...> end)
    {:or, :a, {:and, :b, :c}}

# `postwalk`

```elixir
@spec postwalk(
  expression :: t(variable),
  acc,
  fun :: walker_stateful(variable, acc)
) :: {t(variable), acc}
when variable: term(), acc: term()
```

Performs a depth-first, post-order traversal of the expression using an accumulator.

## Examples

    iex> {_result, acc} =
    ...>   postwalk(b(:a and :b), [], fn
    ...>     {:and, _, _} = expr, acc -> {expr, [:and | acc]}
    ...>     other, acc -> {other, acc}
    ...>   end)
    ...>
    ...> acc
    [:and]

    iex> {_result, count} =
    ...>   postwalk(b(:a and (:b or :c)), 0, fn
    ...>     {:and, _, _} = expr, acc -> {expr, acc + 1}
    ...>     {:or, _, _} = expr, acc -> {expr, acc + 1}
    ...>     other, acc -> {other, acc}
    ...>   end)
    ...>
    ...> count
    2

# `prewalk`

```elixir
@spec prewalk(expression :: t(variable), fun :: walker_stateless(variable)) ::
  t(variable)
when variable: term()
```

Performs a depth-first, pre-order traversal of the expression.

## Examples

    iex> prewalk(b(:a and :b), fn
    ...>   {:and, left, right} -> {:or, left, right}
    ...>   other -> other
    ...> end)
    {:or, :a, :b}

    iex> prewalk(b(:a and (:b or :c)), fn
    ...>   {:and, left, right} -> {:or, left, right}
    ...>   {:or, left, right} -> {:and, left, right}
    ...>   other -> other
    ...> end)
    {:or, :a, {:and, :b, :c}}

# `prewalk`

```elixir
@spec prewalk(
  expression :: t(variable),
  acc,
  fun :: walker_stateful(variable, acc)
) :: {t(variable), acc}
when variable: term(), acc: term()
```

Performs a depth-first, pre-order traversal of the expression using an accumulator.

## Examples

    iex> {_result, acc} =
    ...>   prewalk(b(:a and :b), [], fn
    ...>     {:and, _, _} = expr, acc -> {expr, [:and | acc]}
    ...>     other, acc -> {other, acc}
    ...>   end)
    ...>
    ...> acc
    [:and]

    iex> {_result, count} =
    ...>   prewalk(b(:a and (:b or :c)), 0, fn
    ...>     {:and, _, _} = expr, acc -> {expr, acc + 1}
    ...>     {:or, _, _} = expr, acc -> {expr, acc + 1}
    ...>     other, acc -> {other, acc}
    ...>   end)
    ...>
    ...> count
    2

# `run`

```elixir
@spec run(expression :: t(variable), eval_fn :: (variable -> result)) :: t(result)
when variable: term(), result: term()
```

Evaluates a boolean expression using a variable evaluation callback.

## Examples

    iex> run(b(:a and :b), fn
    ...>   :a -> true
    ...>   :b -> false
    ...> end)
    false

    iex> run(b(:a or :b), fn
    ...>   :a -> true
    ...>   :b -> false
    ...> end)
    true

    iex> run(b(not :a), fn :a -> true end)
    false

    iex> run(b(:a and (true or :a)), & &1)
    :a

# `simplify`

```elixir
@spec simplify(expression :: t(variable)) :: t(variable) when variable: term()
```

Simplifies a boolean expression using all available simplification laws.

Applies all boolean laws except De Morgan's and Distributive laws, which are
reserved for CNF conversion. This provides general-purpose simplification
that preserves logical equivalence while reducing expression complexity.

## Examples

    iex> simplify(b(not not :a and (:a and :a)))
    :a

    iex> simplify(b(true and (:x or false)))
    :x

    iex> simplify(b(:a or (not :a or :b)))
    true

# `to_algebra`

```elixir
@spec to_algebra(
  expression :: t(variable),
  algebra_opts :: keyword(),
  variable_ast_callback :: (variable -> Macro.t())
) :: Inspect.Algebra.t()
when variable: term()
```

Converts an expression to an `Inspect.Algebra` document.

See `Code.quoted_to_algebra/2` for formatting options.

## Examples

    iex> b(:a and not :b)
    ...> |> to_algebra()
    ...> |> Inspect.Algebra.format(80)
    ...> |> IO.iodata_to_binary()
    ":a and not :b"

    # You can customize how variables are represented:
    iex> b(:a and not :b)
    ...> |> to_algebra([], fn var -> quote do: unquote(var)() end)
    ...> |> Inspect.Algebra.format(80)
    ...> |> IO.iodata_to_binary()
    "a() and not b()"

# `to_ast`

```elixir
@spec to_ast(
  expression :: t(variable),
  variable_ast_callback :: (variable -> Macro.t())
) :: Macro.t()
when variable: term()
```

Converts an expression to an AST.

You can pass a callback to convert variables to AST nodes.
By default, it uses `Macro.escape/1`.

## Examples

    iex> {:and, _meta, [:a, :b]} = to_ast(b(:a and :b))

    # You can customize how variables are represented:
    iex> {:and, _, [{:a, _, []}, {:b, _, []}]} =
    ...>   to_ast(b(:a and :b), fn var -> quote do: unquote(var)() end)

# `to_cnf`

```elixir
@spec to_cnf(expression :: t(variable)) :: cnf(variable) when variable: term()
```

Converts an expression to conjunctive normal form (CNF).

Applies the following transformations:
- Negation Law
- De Morgan's laws (which may create new double negations)
- Negation Law again
- Distributive law

# `to_string`

```elixir
@spec to_string(
  expression :: t(variable),
  variable_ast_callback :: (variable -> Macro.t())
) ::
  String.t()
when variable: term()
```

Converts an expression to a string.

For more control over formatting, use `to_algebra/3` and `Inspect.Algebra.format/2`.

## Examples

    iex> Elixir.Crux.Expression.to_string(b(:a and not :b))
    ":a and not :b"

    # You can customize how variables are represented:
    iex> Elixir.Crux.Expression.to_string(b(:a and not :b), fn var -> quote do: unquote(var)() end)
    "a() and not b()"

---

*Consult [api-reference.md](api-reference.md) for complete listing*