Module expr

The expr module provides functionality for working with Boolean expressions, including parsing and manipulation. Defines an arbitrary boolean expression type and functions for its manipulation.

This module provides an Expr enum to represent boolean expressions involving variables, logical NOT, AND, OR, and constant boolean values (true/false). It includes helper methods for checking expression types, unwrapping values, and constructing complex expressions from slices.

Furthermore, it implements several logical transformation functions:

• demorgans_laws: Applies De Morgan’s laws to push negations inwards.
• distributive_laws: Applies distributive laws (e.g. AND over OR) to transform expressions towards a conjunctive or disjunctive normal form.
• apply_laws: A higher-level function that repeatedly applies De Morgan’s and distributive laws until the expression stabilizes, aiming to convert it into a form suitable for CNF conversion (though full CNF conversion often requires more, like Tseytin transformation for non-exponential results).

Enums

Expr

Represents a boolean expression.

Functions

apply_laws

Applies De Morgan’s laws and then distributive laws repeatedly to an expression until it no longer changes (reaches a fixed point).

demorgans_laws

Applies De Morgan’s laws to an expression to push negations (Not) inwards.

distributive_laws

Applies distributive laws to an expression, primarily A AND (B OR C) -> (A AND B) OR (A AND C) and (B OR C) AND A -> (B AND A) OR (C AND A).