libprop_sat_solver/tableaux_solver/
tableau.rs

1//! A `Tableau` is a collection of `Theory`-ies. This corresponds to the entire propositional
2//! tableau tree, where each `Theory` is a branch (from the root node to each leaf).
3
4use std::collections::VecDeque;
5
6use crate::formula::PropositionalFormula;
7
8use super::Theory;
9
10/// A `Tableau` is a collection of `Theory`-ies. This corresponds to the entire propositional
11/// tableau tree, where each `Theory` is a branch (from the root node to each leaf).
12///
13/// For example, given the tableau (tree)
14///
15/// ```text
16///     (a^b)
17///     /   \
18///    a     b
19/// ```
20///
21/// There are two branches (hence two `Theory`-ies):
22///
23/// 1. `{ (a^b), a }`
24/// 2. `{ (a^b), b }`
25#[derive(Debug, Clone, PartialEq)]
26pub struct Tableau {
27    theories: VecDeque<Theory>,
28}
29
30impl Tableau {
31    /// Construct a new `Tableau` with no theories.
32    pub fn new() -> Self {
33        Self {
34            theories: VecDeque::new(),
35        }
36    }
37
38    /// Construct a `Tableau` with the starting root node being the given propositional formula.
39    pub fn from_starting_propositional_formula(formula: PropositionalFormula) -> Self {
40        let mut theories = VecDeque::new();
41        theories.push_back(Theory::from_propositional_formula(formula));
42        Self { theories }
43    }
44
45    /// Check if the `Tableau` contains no `Theory`-ies.
46    pub fn is_empty(&self) -> bool {
47        self.theories.is_empty()
48    }
49
50    /// Retrieve a `Theory` from the `Tableau`.
51    pub fn pop_theory(&mut self) -> Option<Theory> {
52        self.theories.pop_front()
53    }
54
55    /// Add a `Theory` to the `Tableau`.
56    pub fn push_theory(&mut self, theory: Theory) {
57        self.theories.push_back(theory)
58    }
59
60    /// Check if the `Tableau` already contains the `Theory`.
61    pub fn contains(&self, theory: &Theory) -> bool {
62        self.theories.contains(theory)
63    }
64}
65
66#[cfg(test)]
67mod tests {
68    use super::*;
69    use crate::formula::Variable;
70    use assert2::check;
71
72    #[test]
73    fn test_empty_construction() {
74        let empty_tab = Tableau::new();
75        check!(empty_tab.is_empty());
76    }
77
78    #[test]
79    fn test_single_construction() {
80        let mut single_tab = Tableau::from_starting_propositional_formula(
81            PropositionalFormula::variable(Variable::new("a")),
82        );
83
84        check!(!single_tab.is_empty());
85        check!(single_tab.pop_theory().unwrap().formulas().count() == 1);
86    }
87
88    #[test]
89    fn test_push_theory() {
90        let mut tab = Tableau::new();
91        check!(tab.is_empty());
92
93        tab.push_theory(Theory::from_propositional_formula(
94            PropositionalFormula::variable(Variable::new("a")),
95        ));
96
97        check!(!tab.is_empty());
98
99        let theory = tab.pop_theory().unwrap();
100
101        check!(
102            &PropositionalFormula::variable(Variable::new("a"))
103                == theory.formulas().next().unwrap()
104        );
105    }
106
107    #[test]
108    fn test_pop_theory() {
109        let mut tab = Tableau::from_starting_propositional_formula(PropositionalFormula::variable(
110            Variable::new("a"),
111        ));
112        check!(!tab.is_empty());
113
114        let theory = tab.pop_theory().unwrap();
115
116        check!(
117            &PropositionalFormula::variable(Variable::new("a"))
118                == theory.formulas().next().unwrap()
119        );
120    }
121
122    #[test]
123    fn test_push_pop_theory() {
124        let mut tab = Tableau::new();
125
126        tab.push_theory(Theory::from_propositional_formula(
127            PropositionalFormula::variable(Variable::new("a")),
128        ));
129        let _ = tab.pop_theory();
130
131        check!(tab.is_empty());
132    }
133
134    #[test]
135    fn test_contains_theory() {
136        let tab = Tableau::from_starting_propositional_formula(PropositionalFormula::variable(
137            Variable::new("a"),
138        ));
139
140        check!(tab.contains(&Theory::from_propositional_formula(
141            PropositionalFormula::variable(Variable::new("a"))
142        )));
143    }
144
145    #[test]
146    fn test_does_not_contain_theory() {
147        let tab = Tableau::from_starting_propositional_formula(PropositionalFormula::variable(
148            Variable::new("a"),
149        ));
150
151        check!(!tab.contains(&Theory::from_propositional_formula(
152            PropositionalFormula::variable(Variable::new("b"))
153        )));
154    }
155}
libprop_sat_solver/tableaux_solver/tableau.rs

libprop_sat_solver/tableaux_solver/
tableau.rs
