distributive_laws

sat_solver::sat::expr

Function distributive_laws 

Source 
pub fn distributive_laws(expr: &Expr) -> Expr
Expand description

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

This function aims to transform expressions towards a disjunctive normal form (DNF) if applied to distribute AND over OR.

It recursively applies these transformations.

§Arguments

  • expr: The expression to transform.

§Panics

Panics if it encounters an Expr::Not(_) variant directly during distribution, as it expects negations to have been pushed to the literal level (NNF) by demorgans_laws before distribution is applied for typical CNF/DNF conversion steps.