@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]

@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]

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}}}

@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.

@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, :light_theme, :dark_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]

@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

@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

@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.

@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

@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}}

@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

@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}}

@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

@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

@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

@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()"

@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)

@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

@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()"