Returns an element that is "self || other".
(&self, other: Rc<SymbolicValue>)
| 1127 | |
| 1128 | /// Returns an element that is "self || other". |
| 1129 | fn or(&self, other: Rc<SymbolicValue>) -> Rc<SymbolicValue> { |
| 1130 | fn unsimplified(x: &Rc<SymbolicValue>, y: Rc<SymbolicValue>) -> Rc<SymbolicValue> { |
| 1131 | SymbolicValue::make_binary(x.clone(), y, |left, right| Expression::Or { left, right }) |
| 1132 | } |
| 1133 | fn is_contained_in(x: &Rc<SymbolicValue>, y: &Rc<SymbolicValue>) -> bool { |
| 1134 | if *x == *y { |
| 1135 | return true; |
| 1136 | } |
| 1137 | if let Expression::Or { left, right } = &y.expression { |
| 1138 | is_contained_in(x, left) || is_contained_in(x, right) |
| 1139 | } else { |
| 1140 | false |
| 1141 | } |
| 1142 | } |
| 1143 | |
| 1144 | let self_as_bool = self.as_bool_if_known(); |
| 1145 | if !self_as_bool.unwrap_or(true) { |
| 1146 | // [false || y] -> y |
| 1147 | other |
| 1148 | } else if self_as_bool.unwrap_or(false) || other.as_bool_if_known().unwrap_or(false) { |
| 1149 | // [x || true] -> true |
| 1150 | // [true || y] -> true |
| 1151 | Rc::new(SymbolicValue::new_true()) |
| 1152 | } else if other.is_top() || other.is_bottom() || !self.as_bool_if_known().unwrap_or(true) { |
| 1153 | // [self || TOP] -> TOP |
| 1154 | // [self || BOTTOM] -> BOTTOM |
| 1155 | // [false || other] -> other |
| 1156 | other |
| 1157 | } else if self.is_top() || self.is_bottom() || !other.as_bool_if_known().unwrap_or(true) { |
| 1158 | // [TOP || other] -> TOP |
| 1159 | // [BOTTOM || other] -> BOTTOM |
| 1160 | // [self || false] -> self |
| 1161 | self.clone() |
| 1162 | } else { |
| 1163 | // [x || x] -> x |
| 1164 | if self.expression == other.expression { |
| 1165 | return other; |
| 1166 | } |
| 1167 | |
| 1168 | // [!x || x] -> true |
| 1169 | if let Expression::LogicalNot { operand } = &self.expression { |
| 1170 | if is_contained_in(operand, &other) { |
| 1171 | return Rc::new(SymbolicValue::new_true()); |
| 1172 | } |
| 1173 | } |
| 1174 | |
| 1175 | // [x || !x] -> true |
| 1176 | if let Expression::LogicalNot { operand } = &other.expression { |
| 1177 | if is_contained_in(operand, &self) { |
| 1178 | return Rc::new(SymbolicValue::new_true()); |
| 1179 | } |
| 1180 | } |
| 1181 | |
| 1182 | // [x || (x || y)] -> x || y |
| 1183 | // [x || (y || x)] -> x || y |
| 1184 | // [(x || y) || y] -> x || y |
| 1185 | // [(x || y) || x] -> x || y |
| 1186 | if is_contained_in(self, &other) { |
no test coverage detected