Add simplification rules (#1243)

facebookexperimental · Oct 16, 2023 · 9b2ceeb · 9b2ceeb
1 parent bff6070
commit 9b2ceeb
Show file tree

Hide file tree

Showing 4 changed files with 99 additions and 29 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/binaries/summary_store.tar b/binaries/summary_store.tar
diff --git a/checker/src/abstract_value.rs b/checker/src/abstract_value.rs
@@ -649,8 +649,7 @@ impl AbstractValue {
     pub fn make_from(expression: Expression, expression_size: u64) -> Rc<AbstractValue> {
         if expression_size > k_limits::MAX_EXPRESSION_SIZE {
             if expression_size < u64::MAX {
-                trace!("expression {:?}", expression);
-                debug!("expression abstracted");
+                debug!("expression abstracted:  {:?}", expression);
             }
             // If the expression gets too large, refining it gets expensive and composing it
             // into other expressions leads to exponential growth. We therefore need to abstract
@@ -1256,6 +1255,22 @@ impl AbstractValueTrait for Rc<AbstractValue> {
                         }
                     }
                 }
+                // [if c { a } else { b } && c] -> a
+                Expression::ConditionalExpression {
+                    condition,
+                    consequent,
+                    ..
+                } if condition.eq(&other) => {
+                    return consequent.clone();
+                }
+                // [if c { a } else { b } && !c] -> b
+                Expression::ConditionalExpression {
+                    condition,
+                    alternate,
+                    ..
+                } if condition.eq(&other.logical_not()) => {
+                    return alternate.clone();
+                }
                 _ => (),
             }
             match &other.expression {
@@ -2133,6 +2148,26 @@ impl AbstractValueTrait for Rc<AbstractValue> {
                 }
             }
         }
+        // [if c {d} else { (if c {e} else {f}) join (if c {g} else {h}) }] -> if c {d} else { (f join h)}
+        if let Expression::Join { left, right } = &alternate.expression {
+            match (&left.expression, &right.expression) {
+                (
+                    Expression::ConditionalExpression {
+                        condition: c1,
+                        alternate: g,
+                        ..
+                    },
+                    Expression::ConditionalExpression {
+                        condition: c2,
+                        alternate: h,
+                        ..
+                    },
+                ) if c1.eq(c2) && c1.eq(self) => {
+                    return self.conditional_expression(consequent.clone(), g.join(h.clone()));
+                }
+                _ => {}
+            }
+        }
 
         // [if (if c { x } else { y }) { if c { a } else { b }} else { d }] ->
         // if c { if x { a } else { d } } else { if y { b } else { d } }
@@ -2159,6 +2194,28 @@ impl AbstractValueTrait for Rc<AbstractValue> {
             }
         }
 
+        // [if c { if (if c { a } else { b }) { x } else { y } } else { z }] -> if c { if a { x } else { y }} else {z}
+        if let Expression::ConditionalExpression {
+            condition: cab,
+            consequent: x,
+            alternate: y,
+        } = &consequent.expression
+        {
+            if let Expression::ConditionalExpression {
+                condition: c2,
+                consequent: a,
+                ..
+            } = &cab.expression
+            {
+                if self.eq(c2) {
+                    return self.conditional_expression(
+                        a.conditional_expression(x.clone(), y.clone()),
+                        alternate,
+                    );
+                }
+            }
+        }
+
         // if self { consequent } else { alternate } implies self in the consequent and !self in the alternate
         if !matches!(self.expression, Expression::Or { .. }) {
             if consequent.expression_size <= k_limits::MAX_EXPRESSION_SIZE / 10 {
@@ -4172,6 +4229,11 @@ impl AbstractValueTrait for Rc<AbstractValue> {
                 return self.clone();
             }
 
+            // [(x && y) || x] -> x
+            if other.inverse_implies_not(self) {
+                return other.clone();
+            }
+
             // [x || !(x && y)] -> true, etc.
             if self.inverse_implies(&other) {
                 return Rc::new(TRUE);
@@ -4527,6 +4589,14 @@ impl AbstractValueTrait for Rc<AbstractValue> {
                     return other;
                 }
 
+                // [(x && y) || !x] -> x && y
+                // [(x && y) || !y] -> x && y
+                (Expression::And { left: x, right: y }, Expression::LogicalNot { operand: xy })
+                    if x.eq(xy) || y.eq(xy) =>
+                {
+                    return self.clone();
+                }
+
                 // [x || (x && y)] -> x
                 // [y || (x && y)] -> y
                 (_, Expression::And { left: x, right: y }) if x.eq(self) || y.eq(self) => {

diff --git a/checker/src/environment.rs b/checker/src/environment.rs
@@ -353,7 +353,7 @@ impl Environment {
                                 // conditional on index == i
                                 let conditional_value = indices_are_equal
                                     .conditional_expression(value.clone(), v.clone());
-                                debug!("conditional_value {:?}", conditional_value);
+                                //debug!("conditional_value {:?}", conditional_value);
                                 self.strong_update_value_at(p.clone(), conditional_value);
                             }
                         }