1use serde::{Deserialize, Serialize};
21
22#[derive(Debug, Clone, PartialEq, Eq, thiserror::Error)]
24pub enum VarNameError {
25 #[error("变量名不能为空")]
27 Empty,
28 #[error("变量名 {0:?} 不是合法标识符")]
30 Invalid(String),
31 #[error("变量名 {0:?} 是保留常量 token")]
33 Reserved(String),
34}
35
36pub fn is_identifier(name: &str) -> bool {
38 let mut chars = name.chars();
39 let Some(first) = chars.next() else {
40 return false;
41 };
42 (first.is_alphabetic() || first == '_') && chars.all(|c| c.is_alphanumeric() || c == '_')
43}
44
45pub fn is_reserved_token(name: &str) -> bool {
47 matches!(
48 name,
49 "0" | "False"
50 | "false"
51 | "FALSE"
52 | "1"
53 | "True"
54 | "true"
55 | "TRUE"
56 | "X"
57 | "x"
58 | "?"
59 | "Unknown"
60 | "unknown"
61 )
62}
63
64#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
66pub enum Expr {
67 Const(crate::value::Ternary),
69 Var(String),
71 Not(Box<Expr>),
73 And(Box<Expr>, Box<Expr>),
75 Or(Box<Expr>, Box<Expr>),
77 Xor(Box<Expr>, Box<Expr>),
79 Implies(Box<Expr>, Box<Expr>),
81 Equiv(Box<Expr>, Box<Expr>),
83}
84
85impl Expr {
86 pub fn and(a: Expr, b: Expr) -> Self {
88 Self::And(Box::new(a), Box::new(b))
89 }
90 pub fn or(a: Expr, b: Expr) -> Self {
92 Self::Or(Box::new(a), Box::new(b))
93 }
94 pub fn logical_not(a: Expr) -> Self {
98 Self::Not(Box::new(a))
99 }
100 pub fn xor(a: Expr, b: Expr) -> Self {
102 Self::Xor(Box::new(a), Box::new(b))
103 }
104 pub fn implies(a: Expr, b: Expr) -> Self {
106 Self::Implies(Box::new(a), Box::new(b))
107 }
108 pub fn equiv(a: Expr, b: Expr) -> Self {
110 Self::Equiv(Box::new(a), Box::new(b))
111 }
112
113 pub fn try_var(name: impl Into<String>) -> Result<Self, VarNameError> {
119 let name = name.into();
120 if name.is_empty() {
121 return Err(VarNameError::Empty);
122 }
123 if is_reserved_token(&name) {
124 return Err(VarNameError::Reserved(name));
125 }
126 if !is_identifier(&name) {
127 return Err(VarNameError::Invalid(name));
128 }
129 Ok(Self::Var(name))
130 }
131
132 pub const fn is_unknown_const(&self) -> bool {
134 matches!(self, Self::Const(crate::value::Ternary::Unknown))
135 }
136
137 pub fn variables(&self) -> Vec<String> {
141 let mut out = Vec::new();
142 let mut seen = std::collections::HashSet::new();
143 let mut stack = vec![self];
144 while let Some(node) = stack.pop() {
145 match node {
146 Self::Const(_) => {}
147 Self::Var(name) => {
148 if seen.insert(name.clone()) {
149 out.push(name.clone());
150 }
151 }
152 Self::Not(a) => stack.push(a),
153 Self::And(a, b)
154 | Self::Or(a, b)
155 | Self::Xor(a, b)
156 | Self::Implies(a, b)
157 | Self::Equiv(a, b) => {
158 stack.push(b);
159 stack.push(a);
160 }
161 }
162 }
163 out
164 }
165
166 pub fn node_count(&self) -> usize {
168 let mut count = 0usize;
169 let mut stack = vec![self];
170 while let Some(node) = stack.pop() {
171 count += 1;
172 match node {
173 Self::Const(_) | Self::Var(_) => {}
174 Self::Not(a) => stack.push(a),
175 Self::And(a, b)
176 | Self::Or(a, b)
177 | Self::Xor(a, b)
178 | Self::Implies(a, b)
179 | Self::Equiv(a, b) => {
180 stack.push(a);
181 stack.push(b);
182 }
183 }
184 }
185 count
186 }
187
188 pub fn depth(&self) -> usize {
190 let mut max = 0usize;
191 let mut stack = vec![(self, 1usize)];
192 while let Some((node, depth)) = stack.pop() {
193 max = max.max(depth);
194 match node {
195 Self::Const(_) | Self::Var(_) => {}
196 Self::Not(a) => stack.push((a, depth + 1)),
197 Self::And(a, b)
198 | Self::Or(a, b)
199 | Self::Xor(a, b)
200 | Self::Implies(a, b)
201 | Self::Equiv(a, b) => {
202 stack.push((a, depth + 1));
203 stack.push((b, depth + 1));
204 }
205 }
206 }
207 max
208 }
209
210 pub fn to_infix(&self) -> String {
216 match self {
217 Self::Const(v) => v.to_string(),
218 Self::Var(name) => name.clone(),
219 Self::Not(a) => format!("¬({})", a.to_infix()),
220 Self::And(a, b) => format!("({} ∧ {})", a.to_infix(), b.to_infix()),
221 Self::Or(a, b) => format!("({} ∨ {})", a.to_infix(), b.to_infix()),
222 Self::Xor(a, b) => format!("({} ⊕ {})", a.to_infix(), b.to_infix()),
223 Self::Implies(a, b) => format!("({} ⇒ {})", a.to_infix(), b.to_infix()),
224 Self::Equiv(a, b) => format!("({} ≡ {})", a.to_infix(), b.to_infix()),
225 }
226 }
227}
228
229impl std::fmt::Display for Expr {
230 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
231 f.write_str(&self.to_infix())
232 }
233}
234
235#[cfg(test)]
236mod tests {
237 use super::*;
238 use crate::value::Ternary;
239
240 #[test]
241 fn collects_variables_in_order() {
242 let e = Expr::and(
243 Expr::Var("a".into()),
244 Expr::or(Expr::Var("b".into()), Expr::Var("a".into())),
245 );
246 assert_eq!(e.variables(), vec!["a".to_string(), "b".to_string()]);
247 }
248
249 #[test]
250 fn node_count_and_depth() {
251 let e = Expr::and(Expr::Var("a".into()), Expr::Var("b".into()));
252 assert_eq!(e.node_count(), 3);
253 assert_eq!(e.depth(), 2);
254 }
255
256 #[test]
257 fn infix_rendering() {
258 let e = Expr::logical_not(Expr::Var("a".into()));
259 assert_eq!(e.to_infix(), "¬(a)");
260 let e2 = Expr::equiv(Expr::Const(Ternary::True), Expr::Var("x".into()));
261 assert_eq!(e2.to_infix(), "(1 ≡ x)");
262 }
263
264 #[test]
265 fn try_var_rejects_reserved_and_malformed_names() {
266 assert_eq!(Expr::try_var("a_1").unwrap(), Expr::Var("a_1".into()));
267 assert!(matches!(
268 Expr::try_var("X").unwrap_err(),
269 VarNameError::Reserved(_)
270 ));
271 assert!(matches!(
272 Expr::try_var("a b").unwrap_err(),
273 VarNameError::Invalid(_)
274 ));
275 assert!(matches!(
276 Expr::try_var("").unwrap_err(),
277 VarNameError::Empty
278 ));
279 }
280
281 #[test]
282 fn display_does_not_round_trip_arbitrary_vars() {
283 let e = Expr::Var("X".into());
285 assert_eq!(e.to_string(), "X");
286 assert!(matches!(
287 crate::parser::Parser::parse(&e.to_string()).unwrap(),
288 Expr::Const(Ternary::Unknown)
289 ));
290 }
291
292 #[test]
293 fn iterative_metrics_match_hand_computed_values() {
294 let e = Expr::and(
295 Expr::Var("a".into()),
296 Expr::implies(Expr::Var("b".into()), Expr::Var("c".into())),
297 );
298 assert_eq!(e.node_count(), 5);
299 assert_eq!(e.depth(), 3);
300 assert_eq!(e.variables(), vec!["a", "b", "c"]);
301 }
302}