lemma/inversion/
boolean.rs

1//! Boolean expression simplification using BDDs
2
3use crate::{Expression, ExpressionId, ExpressionKind, LiteralValue};
4
5/// Simplify a boolean expression using BDD-based simplification
6pub fn simplify_boolean<F>(
7    expr: &Expression,
8    try_fold: &F,
9    expr_eq: &impl Fn(&Expression, &Expression) -> bool,
10) -> crate::LemmaResult<Expression>
11where
12    F: Fn(&Expression) -> Option<Expression>,
13{
14    let folded = try_fold(expr).unwrap_or_else(|| expr.clone());
15
16    let mut atoms: Vec<Expression> = Vec::new();
17    if let Some(bexpr) = to_bool_expr(&folded, &mut atoms, expr_eq) {
18        const MAX_ATOMS: usize = 64;
19        if atoms.len() <= MAX_ATOMS {
20            let simplified = bexpr.simplify_via_bdd();
21            let rebuilt = from_bool_expr(&simplified, &atoms);
22            return Ok(try_fold(&rebuilt).unwrap_or(rebuilt));
23        }
24    }
25
26    Ok(folded)
27}
28
29/// Simplify OR expressions using BDD
30pub fn simplify_or_expression<F>(
31    expr: &Expression,
32    try_fold: &F,
33    expr_eq: &impl Fn(&Expression, &Expression) -> bool,
34) -> Expression
35where
36    F: Fn(&Expression) -> Option<Expression>,
37{
38    let folded = try_fold(expr).unwrap_or_else(|| expr.clone());
39
40    let mut atoms: Vec<Expression> = Vec::new();
41    if let Some(bexpr) = to_bool_expr(&folded, &mut atoms, expr_eq) {
42        const MAX_ATOMS: usize = 64;
43        if atoms.len() <= MAX_ATOMS {
44            let simplified = bexpr.simplify_via_bdd();
45            let rebuilt = from_bool_expr(&simplified, &atoms);
46            return try_fold(&rebuilt).unwrap_or(rebuilt);
47        }
48    }
49
50    folded
51}
52
53fn to_bool_expr(
54    expr: &Expression,
55    atoms: &mut Vec<Expression>,
56    expr_eq: &impl Fn(&Expression, &Expression) -> bool,
57) -> Option<boolean_expression::Expr<usize>> {
58    use boolean_expression::Expr as BExpr;
59    use ExpressionKind as EK;
60
61    match &expr.kind {
62        EK::Literal(LiteralValue::Boolean(b)) => Some(BExpr::Const(*b)),
63        EK::LogicalAnd(l, r) => {
64            let lbe = to_bool_expr(l, atoms, expr_eq)?;
65            let rbe = to_bool_expr(r, atoms, expr_eq)?;
66            Some(BExpr::and(lbe, rbe))
67        }
68        EK::LogicalOr(l, r) => {
69            let lbe = to_bool_expr(l, atoms, expr_eq)?;
70            let rbe = to_bool_expr(r, atoms, expr_eq)?;
71            Some(BExpr::or(lbe, rbe))
72        }
73        EK::LogicalNegation(inner, _) => {
74            let ibe = to_bool_expr(inner, atoms, expr_eq)?;
75            Some(BExpr::not(ibe))
76        }
77        EK::Comparison(_, _, _) | EK::FactHasAnyValue(_) => {
78            let mut idx_opt = None;
79            for (i, a) in atoms.iter().enumerate() {
80                if expr_eq(a, expr) {
81                    idx_opt = Some(i);
82                    break;
83                }
84            }
85            let idx = match idx_opt {
86                Some(i) => i,
87                None => {
88                    atoms.push(expr.clone());
89                    atoms.len() - 1
90                }
91            };
92            Some(BExpr::Terminal(idx))
93        }
94        EK::Literal(_)
95        | EK::Arithmetic(_, _, _)
96        | EK::UnitConversion(_, _)
97        | EK::MathematicalOperator(_, _)
98        | EK::FactReference(_)
99        | EK::RuleReference(_)
100        | EK::Veto(_) => None,
101    }
102}
103
104fn from_bool_expr(be: &boolean_expression::Expr<usize>, atoms: &[Expression]) -> Expression {
105    use boolean_expression::Expr as BExpr;
106    use ExpressionKind as EK;
107
108    match be {
109        BExpr::Const(b) => Expression::new(
110            EK::Literal(LiteralValue::Boolean(*b)),
111            None,
112            ExpressionId::new(0),
113        ),
114        BExpr::Terminal(i) => atoms.get(*i).cloned().unwrap_or_else(|| {
115            Expression::new(
116                EK::Literal(LiteralValue::Boolean(false)),
117                None,
118                ExpressionId::new(0),
119            )
120        }),
121        BExpr::Not(inner) => {
122            let inner_expr = from_bool_expr(inner, atoms);
123            Expression::new(
124                EK::LogicalNegation(Box::new(inner_expr), crate::NegationType::Not),
125                None,
126                ExpressionId::new(0),
127            )
128        }
129        BExpr::And(l, r) => {
130            let l_expr = from_bool_expr(l, atoms);
131            let r_expr = from_bool_expr(r, atoms);
132            Expression::new(
133                EK::LogicalAnd(Box::new(l_expr), Box::new(r_expr)),
134                None,
135                ExpressionId::new(0),
136            )
137        }
138        BExpr::Or(l, r) => {
139            let l_expr = from_bool_expr(l, atoms);
140            let r_expr = from_bool_expr(r, atoms);
141            Expression::new(
142                EK::LogicalOr(Box::new(l_expr), Box::new(r_expr)),
143                None,
144                ExpressionId::new(0),
145            )
146        }
147    }
148}
lemma/inversion/boolean.rs

lemma/inversion/
boolean.rs
