machine_check_common/property/
closed_form.rs

1use crate::{check::Property, property::PropertyType};
2
3impl Property {
4    /*
5     * Returns whether the property is a closed-form formula, i.e. contains no free variables.
6     *
7     * This can be used for efficient computation: a closed-form formula does not change with respect to outside,
8     * so its valuation can be computed only once.
9     */
10    pub fn is_closed_form(&self) -> bool {
11        self.is_closed_form_inner(0, &mut Vec::new())
12    }
13
14    /*
15     * Returns whether the subproperty at a given index is a closed-form formula, i.e. contains no free variables.
16     *
17     * This can be used for efficient computation: a closed-form formula does not change with respect to outside,
18     * so its valuation can be computed only once.
19     *
20     * Panics if the subproperty index is invalid.
21     */
22    pub fn is_subproperty_closed_form(&self, subproperty_index: usize) -> bool {
23        self.is_closed_form_inner(subproperty_index, &mut Vec::new())
24    }
25
26    fn is_closed_form_inner(
27        &self,
28        subproperty_index: usize,
29        inner_fixed_points: &mut Vec<usize>,
30    ) -> bool {
31        let subproperty_entry = self.subproperty_entry(subproperty_index);
32
33        match &subproperty_entry.ty {
34            PropertyType::Const(_) | PropertyType::Atomic(_) => true,
35            PropertyType::Negation(inner) => self.is_closed_form_inner(*inner, inner_fixed_points),
36            PropertyType::BiLogic(bi_logic_operator) => {
37                self.is_closed_form_inner(bi_logic_operator.a, inner_fixed_points)
38                    && self.is_closed_form_inner(bi_logic_operator.b, inner_fixed_points)
39            }
40            PropertyType::Next(next_operator) => {
41                self.is_closed_form_inner(next_operator.inner, inner_fixed_points)
42            }
43            PropertyType::FixedPoint(fixed_point_operator) => {
44                inner_fixed_points.push(subproperty_index);
45                let result =
46                    self.is_closed_form_inner(fixed_point_operator.inner, inner_fixed_points);
47                inner_fixed_points.pop();
48                result
49            }
50            PropertyType::FixedVariable(fixed_point_index) => {
51                inner_fixed_points.contains(fixed_point_index)
52            }
53        }
54    }
55}
machine_check_common/property/closed_form.rs

machine_check_common/property/
closed_form.rs
