pub fn try_lower_bool_atom_eq_true(expr: &Expression) -> Option<Expression>Expand description
Rewrites x = true / true = x to x when x is a non-literal boolean atom.
Nested uses such as (x = true) <-> and([y = true, ...]) otherwise force Minion flattening to
introduce aux variables for the left-hand Eq, because both sides of the outer equality are
non-atomic. Lowering the tautological = true first keeps a boolean decision variable atomic
so later equality/reify rules can target it directly.
Literal–literal equalities are left alone for constant folding. Non-boolean atoms are refused.