Skip to main content

mago_codex/
assertion.rs

1use std::borrow::Cow;
2use std::hash::BuildHasher;
3use std::hash::Hash;
4
5use foldhash::fast::FixedState;
6
7use mago_word::Word;
8use mago_word::concat_word;
9use mago_word::i64_word;
10use mago_word::usize_word;
11use mago_word::word;
12
13use crate::metadata::CodebaseMetadata;
14use crate::ttype::TType;
15use crate::ttype::atomic::TAtomic;
16use crate::ttype::atomic::array::key::ArrayKey;
17use crate::ttype::template::TemplateResult;
18use crate::ttype::template::inferred_type_replacer;
19use crate::ttype::union::TUnion;
20
21#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
22#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
23pub enum Assertion {
24    Any,
25    IsType(TAtomic),
26    IsNotType(TAtomic),
27    Falsy,
28    Truthy,
29    IsIdentical(TAtomic),
30    IsNotIdentical(TAtomic),
31    IsEqual(TAtomic),
32    IsNotEqual(TAtomic),
33    IsEqualIsset,
34    IsIsset,
35    IsNotIsset,
36    HasStringArrayAccess,
37    HasIntOrStringArrayAccess,
38    ArrayKeyExists,
39    ArrayKeyDoesNotExist,
40    InArray(TUnion),
41    NotInArray(TUnion),
42    HasArrayKey(ArrayKey),
43    DoesNotHaveArrayKey(ArrayKey),
44    HasNonnullEntryForKey(ArrayKey),
45    DoesNotHaveNonnullEntryForKey(ArrayKey),
46    Empty,
47    NonEmpty,
48    NonEmptyCountable(bool),
49    EmptyCountable,
50    HasExactCount(usize),
51    HasAtLeastCount(usize),
52    DoesNotHaveExactCount(usize),
53    DoesNotHasAtLeastCount(usize),
54    IsLessThan(i64),
55    IsLessThanOrEqual(i64),
56    IsGreaterThan(i64),
57    IsGreaterThanOrEqual(i64),
58    /// A range fact implied by a comparison with a non-literal bound.
59    ///
60    /// For example, `$a > $b` with `int<0, max> $b` implies `$a > 0`
61    /// in the true branch, but its negation does not imply `$a <= 0`.
62    /// These assertions therefore deliberately negate to `Any`.
63    IsLessThanFromBound(i64),
64    IsLessThanOrEqualFromBound(i64),
65    IsGreaterThanFromBound(i64),
66    IsGreaterThanOrEqualFromBound(i64),
67    /// An exact comparison with another tracked expression.
68    ///
69    /// Unlike bound-derived facts, these retain the relationship so consumers
70    /// can reason about arithmetic such as `$limit - $length` after
71    /// `$length < $limit`.
72    IsLessThanVariable(Word),
73    IsLessThanOrEqualVariable(Word),
74    IsGreaterThanVariable(Word),
75    IsGreaterThanOrEqualVariable(Word),
76    Countable,
77    NotCountable(bool),
78}
79
80impl Assertion {
81    #[must_use]
82    pub fn to_atom(&self) -> Word {
83        match self {
84            Assertion::Any => word("any"),
85            Assertion::Falsy => word("falsy"),
86            Assertion::Truthy => word("truthy"),
87            Assertion::IsEqualIsset => word("=isset"),
88            Assertion::IsIsset => word("isset"),
89            Assertion::IsNotIsset => word("!isset"),
90            Assertion::HasStringArrayAccess => word("=string-array-access"),
91            Assertion::HasIntOrStringArrayAccess => word("=int-or-string-array-access"),
92            Assertion::ArrayKeyExists => word("array-key-exists"),
93            Assertion::ArrayKeyDoesNotExist => word("!array-key-exists"),
94            Assertion::EmptyCountable => word("empty-countable"),
95            Assertion::Empty => word("empty"),
96            Assertion::NonEmpty => word("non-empty"),
97            Assertion::Countable => word("countable"),
98            Assertion::NotCountable(_) => word("!countable"),
99            Assertion::IsType(atomic) => atomic.get_id(),
100            Assertion::IsNotType(atomic) => concat_word!(b"!", atomic.get_id()),
101            Assertion::IsIdentical(atomic) => concat_word!(b"=", atomic.get_id()),
102            Assertion::IsNotIdentical(atomic) => concat_word!(b"!=", atomic.get_id()),
103            Assertion::IsEqual(atomic) => concat_word!(b"~", atomic.get_id()),
104            Assertion::IsNotEqual(atomic) => concat_word!(b"!~", atomic.get_id()),
105            Assertion::InArray(union) => concat_word!(b"=in-array-", union.get_id()),
106            Assertion::NotInArray(union) => concat_word!(b"!=in-array-", union.get_id()),
107            Assertion::HasArrayKey(key) => concat_word!(b"=has-array-key-", key.to_atom()),
108            Assertion::DoesNotHaveArrayKey(key) => concat_word!(b"!=has-array-key-", key.to_atom()),
109            Assertion::HasNonnullEntryForKey(key) => concat_word!(b"=has-nonnull-entry-for-", key.to_atom()),
110            Assertion::DoesNotHaveNonnullEntryForKey(key) => {
111                concat_word!(b"!=has-nonnull-entry-for-", key.to_atom())
112            }
113            Assertion::HasExactCount(number) => concat_word!(b"has-exactly-", usize_word(*number)),
114            Assertion::HasAtLeastCount(number) => concat_word!(b"has-at-least-", usize_word(*number)),
115            Assertion::DoesNotHaveExactCount(number) => concat_word!(b"!has-exactly-", usize_word(*number)),
116            Assertion::DoesNotHasAtLeastCount(number) => concat_word!(b"has-at-most-", usize_word(*number)),
117            Assertion::IsLessThan(number) => concat_word!(b"is-less-than-", i64_word(*number)),
118            Assertion::IsLessThanOrEqual(number) => concat_word!(b"is-less-than-or-equal-", i64_word(*number)),
119            Assertion::IsGreaterThan(number) => concat_word!(b"is-greater-than-", i64_word(*number)),
120            Assertion::IsGreaterThanOrEqual(number) => concat_word!(b"is-greater-than-or-equal-", i64_word(*number)),
121            Assertion::IsLessThanFromBound(number) => concat_word!(b"is-less-than-from-bound-", i64_word(*number)),
122            Assertion::IsLessThanOrEqualFromBound(number) => {
123                concat_word!(b"is-less-than-or-equal-from-bound-", i64_word(*number))
124            }
125            Assertion::IsGreaterThanFromBound(number) => {
126                concat_word!(b"is-greater-than-from-bound-", i64_word(*number))
127            }
128            Assertion::IsGreaterThanOrEqualFromBound(number) => {
129                concat_word!(b"is-greater-than-or-equal-from-bound-", i64_word(*number))
130            }
131            Assertion::IsLessThanVariable(variable) => concat_word!(b"is-less-than-variable-", variable),
132            Assertion::IsLessThanOrEqualVariable(variable) => {
133                concat_word!(b"is-less-than-or-equal-variable-", variable)
134            }
135            Assertion::IsGreaterThanVariable(variable) => {
136                concat_word!(b"is-greater-than-variable-", variable)
137            }
138            Assertion::IsGreaterThanOrEqualVariable(variable) => {
139                concat_word!(b"is-greater-than-or-equal-variable-", variable)
140            }
141            Assertion::NonEmptyCountable(negatable) => {
142                if *negatable {
143                    word("non-empty-countable")
144                } else {
145                    word("=non-empty-countable")
146                }
147            }
148        }
149    }
150
151    #[must_use]
152    pub fn to_hash(&self) -> u64 {
153        FixedState::default().hash_one(self.to_atom())
154    }
155
156    #[must_use]
157    pub fn is_negation(&self) -> bool {
158        matches!(
159            self,
160            Assertion::Falsy
161                | Assertion::IsNotType(_)
162                | Assertion::IsNotEqual(_)
163                | Assertion::IsNotIdentical(_)
164                | Assertion::IsNotIsset
165                | Assertion::NotInArray(..)
166                | Assertion::ArrayKeyDoesNotExist
167                | Assertion::DoesNotHaveArrayKey(_)
168                | Assertion::DoesNotHaveExactCount(_)
169                | Assertion::DoesNotHaveNonnullEntryForKey(_)
170                | Assertion::DoesNotHasAtLeastCount(_)
171                | Assertion::EmptyCountable
172                | Assertion::Empty
173                | Assertion::NotCountable(_)
174        )
175    }
176
177    #[must_use]
178    pub fn has_isset(&self) -> bool {
179        matches!(
180            self,
181            Assertion::IsIsset | Assertion::ArrayKeyExists | Assertion::HasStringArrayAccess | Assertion::IsEqualIsset
182        )
183    }
184
185    #[must_use]
186    pub fn has_non_isset_equality(&self) -> bool {
187        matches!(
188            self,
189            Assertion::InArray(_)
190                | Assertion::HasIntOrStringArrayAccess
191                | Assertion::HasStringArrayAccess
192                | Assertion::IsIdentical(_)
193                | Assertion::IsEqual(_)
194        )
195    }
196
197    #[must_use]
198    pub fn has_equality(&self) -> bool {
199        matches!(
200            self,
201            Assertion::InArray(_)
202                | Assertion::HasIntOrStringArrayAccess
203                | Assertion::HasStringArrayAccess
204                | Assertion::IsEqualIsset
205                | Assertion::IsIdentical(_)
206                | Assertion::IsNotIdentical(_)
207                | Assertion::IsEqual(_)
208                | Assertion::IsNotEqual(_)
209                | Assertion::HasExactCount(_)
210        )
211    }
212
213    #[must_use]
214    pub fn has_literal_value(&self) -> bool {
215        match self {
216            Assertion::IsIdentical(atomic)
217            | Assertion::IsNotIdentical(atomic)
218            | Assertion::IsType(atomic)
219            | Assertion::IsNotType(atomic)
220            | Assertion::IsEqual(atomic)
221            | Assertion::IsNotEqual(atomic) => {
222                atomic.is_literal_int()
223                    || atomic.is_literal_float()
224                    || atomic.is_known_literal_string()
225                    || atomic.is_literal_class_string()
226            }
227
228            _ => false,
229        }
230    }
231
232    #[must_use]
233    pub fn has_integer(&self) -> bool {
234        match self {
235            Assertion::IsIdentical(atomic)
236            | Assertion::IsNotIdentical(atomic)
237            | Assertion::IsType(atomic)
238            | Assertion::IsNotType(atomic)
239            | Assertion::IsEqual(atomic)
240            | Assertion::IsNotEqual(atomic) => atomic.is_int(),
241            _ => false,
242        }
243    }
244
245    #[must_use]
246    pub fn has_literal_string(&self) -> bool {
247        match self {
248            Assertion::IsIdentical(atomic)
249            | Assertion::IsNotIdentical(atomic)
250            | Assertion::IsType(atomic)
251            | Assertion::IsNotType(atomic)
252            | Assertion::IsEqual(atomic)
253            | Assertion::IsNotEqual(atomic) => atomic.is_known_literal_string(),
254
255            _ => false,
256        }
257    }
258
259    #[must_use]
260    pub fn has_literal_int(&self) -> bool {
261        match self {
262            Assertion::IsIdentical(atomic)
263            | Assertion::IsNotIdentical(atomic)
264            | Assertion::IsType(atomic)
265            | Assertion::IsNotType(atomic)
266            | Assertion::IsEqual(atomic)
267            | Assertion::IsNotEqual(atomic) => atomic.is_literal_int(),
268
269            _ => false,
270        }
271    }
272
273    #[must_use]
274    pub fn has_literal_float(&self) -> bool {
275        match self {
276            Assertion::IsIdentical(atomic)
277            | Assertion::IsNotIdentical(atomic)
278            | Assertion::IsType(atomic)
279            | Assertion::IsNotType(atomic)
280            | Assertion::IsEqual(atomic)
281            | Assertion::IsNotEqual(atomic) => atomic.is_literal_float(),
282
283            _ => false,
284        }
285    }
286
287    #[must_use]
288    pub fn with_type(&self, atomic: TAtomic) -> Self {
289        match self {
290            Assertion::IsType(_) => Assertion::IsType(atomic),
291            Assertion::IsNotType(_) => Assertion::IsNotType(atomic),
292            Assertion::IsIdentical(_) => Assertion::IsIdentical(atomic),
293            Assertion::IsNotIdentical(_) => Assertion::IsNotIdentical(atomic),
294            Assertion::IsEqual(_) => Assertion::IsEqual(atomic),
295            Assertion::IsNotEqual(_) => Assertion::IsNotEqual(atomic),
296            _ => self.clone(),
297        }
298    }
299
300    #[must_use]
301    pub fn get_type(&self) -> Option<&TAtomic> {
302        match self {
303            Assertion::IsIdentical(atomic)
304            | Assertion::IsNotIdentical(atomic)
305            | Assertion::IsType(atomic)
306            | Assertion::IsNotType(atomic)
307            | Assertion::IsEqual(atomic)
308            | Assertion::IsNotEqual(atomic) => Some(atomic),
309            _ => None,
310        }
311    }
312
313    pub fn get_type_mut(&mut self) -> Option<&mut TAtomic> {
314        match self {
315            Assertion::IsIdentical(atomic)
316            | Assertion::IsNotIdentical(atomic)
317            | Assertion::IsType(atomic)
318            | Assertion::IsNotType(atomic)
319            | Assertion::IsEqual(atomic)
320            | Assertion::IsNotEqual(atomic) => Some(atomic),
321            _ => None,
322        }
323    }
324
325    #[must_use]
326    pub fn resolve_templates(&self, codebase: &CodebaseMetadata, template_result: &TemplateResult) -> Vec<Self> {
327        match self {
328            Assertion::IsType(atomic) => {
329                let union = TUnion::from_single(Cow::Owned(atomic.clone()));
330                let resolved_union = inferred_type_replacer::replace(&union, template_result, codebase);
331
332                let mut result = vec![];
333                for resolved_atomic in resolved_union.types.into_owned() {
334                    result.push(Assertion::IsType(resolved_atomic));
335                }
336
337                if result.is_empty() {
338                    result.push(Assertion::IsType(TAtomic::Never));
339                }
340
341                result
342            }
343            Assertion::IsNotType(atomic) => {
344                let union = TUnion::from_single(Cow::Owned(atomic.clone()));
345                let resolved_union = inferred_type_replacer::replace(&union, template_result, codebase);
346
347                let mut result = vec![];
348                for resolved_atomic in resolved_union.types.into_owned() {
349                    result.push(Assertion::IsNotType(resolved_atomic));
350                }
351
352                if result.is_empty() {
353                    result.push(Assertion::IsNotType(TAtomic::Never));
354                }
355
356                result
357            }
358            Assertion::InArray(union) => {
359                let resolved_union = inferred_type_replacer::replace(union, template_result, codebase);
360
361                vec![Assertion::InArray(resolved_union)]
362            }
363            Assertion::NotInArray(union) => {
364                let resolved_union = inferred_type_replacer::replace(union, template_result, codebase);
365
366                vec![Assertion::NotInArray(resolved_union)]
367            }
368            _ => {
369                vec![self.clone()]
370            }
371        }
372    }
373
374    #[must_use]
375    pub fn is_negation_of(&self, other: &Assertion) -> bool {
376        match self {
377            Assertion::Any => false,
378            Assertion::Falsy => matches!(other, Assertion::Truthy),
379            Assertion::Truthy => matches!(other, Assertion::Falsy),
380            Assertion::IsType(atomic) => match other {
381                Assertion::IsNotType(other_atomic) => other_atomic == atomic,
382                _ => false,
383            },
384            Assertion::IsNotType(atomic) => match other {
385                Assertion::IsType(other_atomic) => other_atomic == atomic,
386                _ => false,
387            },
388            Assertion::IsIdentical(atomic) => match other {
389                Assertion::IsNotIdentical(other_atomic) => other_atomic == atomic,
390                _ => false,
391            },
392            Assertion::IsNotIdentical(atomic) => match other {
393                Assertion::IsIdentical(other_atomic) => other_atomic == atomic,
394                _ => false,
395            },
396            Assertion::IsEqual(atomic) => match other {
397                Assertion::IsNotEqual(other_atomic) => other_atomic == atomic,
398                _ => false,
399            },
400            Assertion::IsNotEqual(atomic) => match other {
401                Assertion::IsEqual(other_atomic) => other_atomic == atomic,
402                _ => false,
403            },
404            Assertion::IsEqualIsset => false,
405            Assertion::IsIsset => matches!(other, Assertion::IsNotIsset),
406            Assertion::IsNotIsset => matches!(other, Assertion::IsIsset),
407            Assertion::HasStringArrayAccess => false,
408            Assertion::HasIntOrStringArrayAccess => false,
409            Assertion::ArrayKeyExists => matches!(other, Assertion::ArrayKeyDoesNotExist),
410            Assertion::ArrayKeyDoesNotExist => matches!(other, Assertion::ArrayKeyExists),
411            Assertion::HasArrayKey(str) => match other {
412                Assertion::DoesNotHaveArrayKey(other_str) => other_str == str,
413                _ => false,
414            },
415            Assertion::DoesNotHaveArrayKey(str) => match other {
416                Assertion::HasArrayKey(other_str) => other_str == str,
417                _ => false,
418            },
419            Assertion::HasNonnullEntryForKey(str) => match other {
420                Assertion::DoesNotHaveNonnullEntryForKey(other_str) => other_str == str,
421                _ => false,
422            },
423            Assertion::DoesNotHaveNonnullEntryForKey(str) => match other {
424                Assertion::HasNonnullEntryForKey(other_str) => other_str == str,
425                _ => false,
426            },
427            Assertion::InArray(union) => match other {
428                Assertion::NotInArray(other_union) => other_union == union,
429                _ => false,
430            },
431            Assertion::NotInArray(union) => match other {
432                Assertion::InArray(other_union) => other_union == union,
433                _ => false,
434            },
435            Assertion::Empty => matches!(other, Assertion::NonEmpty),
436            Assertion::NonEmpty => matches!(other, Assertion::Empty),
437            Assertion::NonEmptyCountable(negatable) => {
438                if *negatable {
439                    matches!(other, Assertion::EmptyCountable)
440                } else {
441                    false
442                }
443            }
444            Assertion::EmptyCountable => matches!(other, Assertion::NonEmptyCountable(true)),
445            Assertion::HasExactCount(number) => match other {
446                Assertion::DoesNotHaveExactCount(other_number) => other_number == number,
447                _ => false,
448            },
449            Assertion::DoesNotHaveExactCount(number) => match other {
450                Assertion::HasExactCount(other_number) => other_number == number,
451                _ => false,
452            },
453            Assertion::HasAtLeastCount(number) => match other {
454                Assertion::DoesNotHasAtLeastCount(other_number) => other_number == number,
455                _ => false,
456            },
457            Assertion::DoesNotHasAtLeastCount(number) => match other {
458                Assertion::HasAtLeastCount(other_number) => other_number == number,
459                _ => false,
460            },
461            Assertion::IsLessThan(number) => match other {
462                Assertion::IsGreaterThanOrEqual(other_number) => other_number == number,
463                _ => false,
464            },
465            Assertion::IsLessThanOrEqual(number) => match other {
466                Assertion::IsGreaterThan(other_number) => other_number == number,
467                _ => false,
468            },
469            Assertion::IsGreaterThan(number) => match other {
470                Assertion::IsLessThanOrEqual(other_number) => other_number == number,
471                _ => false,
472            },
473            Assertion::IsGreaterThanOrEqual(number) => match other {
474                Assertion::IsLessThan(other_number) => other_number == number,
475                _ => false,
476            },
477            Assertion::IsLessThanFromBound(_)
478            | Assertion::IsLessThanOrEqualFromBound(_)
479            | Assertion::IsGreaterThanFromBound(_)
480            | Assertion::IsGreaterThanOrEqualFromBound(_) => false,
481            Assertion::IsLessThanVariable(variable) => match other {
482                Assertion::IsGreaterThanOrEqualVariable(other_variable) => other_variable == variable,
483                _ => false,
484            },
485            Assertion::IsLessThanOrEqualVariable(variable) => match other {
486                Assertion::IsGreaterThanVariable(other_variable) => other_variable == variable,
487                _ => false,
488            },
489            Assertion::IsGreaterThanVariable(variable) => match other {
490                Assertion::IsLessThanOrEqualVariable(other_variable) => other_variable == variable,
491                _ => false,
492            },
493            Assertion::IsGreaterThanOrEqualVariable(variable) => match other {
494                Assertion::IsLessThanVariable(other_variable) => other_variable == variable,
495                _ => false,
496            },
497            Assertion::Countable => matches!(other, Assertion::NotCountable(negatable) if *negatable),
498            Assertion::NotCountable(_) => matches!(other, Assertion::Countable),
499        }
500    }
501
502    #[must_use]
503    pub fn get_negation(&self) -> Self {
504        match self {
505            Assertion::Any => Assertion::Any,
506            Assertion::Falsy => Assertion::Truthy,
507            Assertion::IsType(atomic) => Assertion::IsNotType(atomic.clone()),
508            Assertion::IsNotType(atomic) => Assertion::IsType(atomic.clone()),
509            Assertion::Truthy => Assertion::Falsy,
510            Assertion::IsIdentical(atomic) => Assertion::IsNotIdentical(atomic.clone()),
511            Assertion::IsNotIdentical(atomic) => Assertion::IsIdentical(atomic.clone()),
512            Assertion::IsEqual(atomic) => Assertion::IsNotEqual(atomic.clone()),
513            Assertion::IsNotEqual(atomic) => Assertion::IsEqual(atomic.clone()),
514            Assertion::IsIsset => Assertion::IsNotIsset,
515            Assertion::IsNotIsset => Assertion::IsIsset,
516            Assertion::Empty => Assertion::NonEmpty,
517            Assertion::NonEmpty => Assertion::Empty,
518            Assertion::NonEmptyCountable(negatable) => {
519                if *negatable {
520                    Assertion::EmptyCountable
521                } else {
522                    Assertion::Any
523                }
524            }
525            Assertion::EmptyCountable => Assertion::NonEmptyCountable(true),
526            Assertion::ArrayKeyExists => Assertion::ArrayKeyDoesNotExist,
527            Assertion::ArrayKeyDoesNotExist => Assertion::ArrayKeyExists,
528            Assertion::InArray(union) => Assertion::NotInArray(union.clone()),
529            Assertion::NotInArray(union) => Assertion::InArray(union.clone()),
530            Assertion::HasExactCount(size) => Assertion::DoesNotHaveExactCount(*size),
531            Assertion::DoesNotHaveExactCount(size) => Assertion::HasExactCount(*size),
532            Assertion::HasAtLeastCount(size) => Assertion::DoesNotHasAtLeastCount(*size),
533            Assertion::DoesNotHasAtLeastCount(size) => Assertion::HasAtLeastCount(*size),
534            Assertion::HasArrayKey(str) => Assertion::DoesNotHaveArrayKey(*str),
535            Assertion::DoesNotHaveArrayKey(str) => Assertion::HasArrayKey(*str),
536            Assertion::HasNonnullEntryForKey(str) => Assertion::DoesNotHaveNonnullEntryForKey(*str),
537            Assertion::DoesNotHaveNonnullEntryForKey(str) => Assertion::HasNonnullEntryForKey(*str),
538            Assertion::HasStringArrayAccess => Assertion::Any,
539            Assertion::HasIntOrStringArrayAccess => Assertion::Any,
540            Assertion::IsEqualIsset => Assertion::Any,
541            Assertion::IsLessThan(number) => Assertion::IsGreaterThanOrEqual(*number),
542            Assertion::IsLessThanOrEqual(number) => Assertion::IsGreaterThan(*number),
543            Assertion::IsGreaterThan(number) => Assertion::IsLessThanOrEqual(*number),
544            Assertion::IsGreaterThanOrEqual(number) => Assertion::IsLessThan(*number),
545            Assertion::IsLessThanFromBound(_)
546            | Assertion::IsLessThanOrEqualFromBound(_)
547            | Assertion::IsGreaterThanFromBound(_)
548            | Assertion::IsGreaterThanOrEqualFromBound(_) => Assertion::Any,
549            Assertion::IsLessThanVariable(variable) => Assertion::IsGreaterThanOrEqualVariable(*variable),
550            Assertion::IsLessThanOrEqualVariable(variable) => Assertion::IsGreaterThanVariable(*variable),
551            Assertion::IsGreaterThanVariable(variable) => Assertion::IsLessThanOrEqualVariable(*variable),
552            Assertion::IsGreaterThanOrEqualVariable(variable) => Assertion::IsLessThanVariable(*variable),
553            Assertion::Countable => Assertion::NotCountable(true),
554            Assertion::NotCountable(_) => Assertion::Countable,
555        }
556    }
557
558    /// Whether this assertion represents the condition itself and can be used
559    /// while constructing the opposite branch.
560    ///
561    /// Facts inferred from a non-literal range bound are only consequences of
562    /// a condition. They are useful in the true branch but are not logically
563    /// equivalent to that condition, so negating them would be unsound.
564    #[inline]
565    #[must_use]
566    pub const fn is_negatable(&self) -> bool {
567        !matches!(
568            self,
569            Self::IsLessThanFromBound(_)
570                | Self::IsLessThanOrEqualFromBound(_)
571                | Self::IsGreaterThanFromBound(_)
572                | Self::IsGreaterThanOrEqualFromBound(_)
573        )
574    }
575
576    /// Returns the expression referenced by a relational assertion.
577    #[inline]
578    #[must_use]
579    pub const fn referenced_variable(&self) -> Option<Word> {
580        match self {
581            Self::IsLessThanVariable(variable)
582            | Self::IsLessThanOrEqualVariable(variable)
583            | Self::IsGreaterThanVariable(variable)
584            | Self::IsGreaterThanOrEqualVariable(variable) => Some(*variable),
585            _ => None,
586        }
587    }
588}