vj_sim/constraints/
guard.rs

1//! Constraint guards (LRM 1800-2023 18.5.12): the 4-valued `FALSE`/`TRUE`/
2//! `ERROR`/`RANDOM` evaluator run on an implication's or `if`'s predicate
3//! before the constraint reaches the solver (plan section 1.7).
4//!
5//! # What a guard is
6//!
7//! The predicate of a constraint-level `->` or `if` is a *guard*, not a
8//! relation for the solver to satisfy: it is evaluated first, over constants,
9//! state variables and object handles, and only what it cannot decide (it
10//! reads a random variable) becomes a conditional constraint. Evaluating it
11//! yields one of four values ([`GuardValue`]) by Figure 18-3's three truth
12//! tables, applied bottom-up over the predicate's `&&`/`||`/`!` tree:
13//!
14//! | final value | outcome |
15//! | ----------- | ------- |
16//! | `TRUE`      | the body is an unconditional constraint |
17//! | `FALSE`     | the constraint is eliminated, and "can generate no error" |
18//! | `ERROR`     | `randomize()` fails with an error ([`GuardError`]) |
19//! | `RANDOM`    | a conditional constraint: the guard stays in the IR |
20//!
21//! The tables are *not* Rust's short-circuit semantics. `FALSE` dominates
22//! `ERROR` under `&&` in either order (`E && 0` is `0`), and `TRUE` dominates
23//! it under `||`, so `a.x == 5 || b.x > 0` with a null `b` and `a.x == 5` is
24//! an unconditional constraint and not an error (LRM 18.5.12 Example 1,
25//! Case 1), while `ERROR` dominates `RANDOM` (`R && E` is `E`). The guard's
26//! sub-expressions are "evaluated in an arbitrary order", so the result may
27//! not depend on operand order, and the tables here are symmetric.
28//!
29//! # Leaves
30//!
31//! Only `&&`, `||` and `!` are structural. Every other node is a *leaf*:
32//!
33//! * a leaf that reads a state variable whose value cannot be read (a null
34//!   handle on the way to it, a deleted object, an X/Z value) is `ERROR`,
35//!   even when it also reads a random variable: dereferencing a null handle
36//!   is the error the guard exists to prevent;
37//! * otherwise a leaf that reads a random variable is `RANDOM`;
38//! * otherwise the leaf is evaluated ([`super::ir::eval`]) and is `TRUE` or
39//!   `FALSE` by its truthiness, or `ERROR` if its evaluation fails (a
40//!   division by zero).
41//!
42//! # Resolving a program
43//!
44//! [`resolve`] rewrites a conjunct's [`Expr::Guard`] nodes under the state
45//! values read for one `randomize()` call. A `RANDOM` predicate is rewritten
46//! too: each maximal sub-tree that is decided (`TRUE`/`FALSE`, which also
47//! drops an `ERROR` it dominates) becomes a constant, so what reaches the
48//! solver reads only random variables and readable state, and a state read
49//! the predicate dodges (`R || (T || E)`) can never make the BDD fail. That
50//! is exact: a node whose final value is `RANDOM` has only `TRUE`/`RANDOM`
51//! children under `&&` and only `FALSE`/`RANDOM` under `||`, so a decided
52//! child is the identity of its operator.
53
54use super::ir::{Assignment, BinOp, ConstraintEvalError, Expr, StateId, Ty, UnOp, eval};
55use core::fmt;
56use num_bigint::BigUint;
57use num_traits::{One, Zero};
58
59/// The value of a guard (sub-)expression (LRM 18.5.12).
60#[derive(Clone, Copy, Debug, PartialEq, Eq)]
61pub enum GuardValue {
62    /// `0`: the sub-expression is false.
63    False,
64    /// `1`: the sub-expression is true.
65    True,
66    /// `E`: the sub-expression causes an evaluation error.
67    Error,
68    /// `R`: the sub-expression reads a random variable and cannot be
69    /// evaluated yet.
70    Random,
71}
72
73impl GuardValue {
74    /// Conjunction, Figure 18-3 (left table): `FALSE` dominates, then
75    /// `ERROR`, then `RANDOM`.
76    pub fn and(self, other: GuardValue) -> GuardValue {
77        use GuardValue::{Error as E, False as F, Random as R, True as T};
78        match (self, other) {
79            (F, _) | (_, F) => F,
80            (E, _) | (_, E) => E,
81            (R, _) | (_, R) => R,
82            (T, T) => T,
83        }
84    }
85
86    /// Disjunction, Figure 18-3 (middle table): `TRUE` dominates, then
87    /// `ERROR`, then `RANDOM`.
88    pub fn or(self, other: GuardValue) -> GuardValue {
89        use GuardValue::{Error as E, False as F, Random as R, True as T};
90        match (self, other) {
91            (T, _) | (_, T) => T,
92            (E, _) | (_, E) => E,
93            (R, _) | (_, R) => R,
94            (F, F) => F,
95        }
96    }
97
98    /// Negation, Figure 18-3 (right table): swaps `TRUE` and `FALSE`, keeps
99    /// `ERROR` and `RANDOM`.
100    #[allow(clippy::should_implement_trait)]
101    pub fn not(self) -> GuardValue {
102        match self {
103            GuardValue::False => GuardValue::True,
104            GuardValue::True => GuardValue::False,
105            GuardValue::Error => GuardValue::Error,
106            GuardValue::Random => GuardValue::Random,
107        }
108    }
109}
110
111/// Why a guard evaluated to `ERROR`.
112#[derive(Clone, Debug, PartialEq, Eq)]
113pub enum GuardCause {
114    /// A leaf reads a state variable that has no value: a null or deleted
115    /// object on the way to it, or an X/Z value.
116    UnreadableState(StateId),
117    /// A leaf failed to evaluate (a division by zero).
118    Eval(ConstraintEvalError),
119}
120
121/// A guard whose final value is `ERROR`: `randomize()` fails (LRM 18.5.12).
122#[derive(Clone, Debug, PartialEq, Eq)]
123pub struct GuardError {
124    /// The first erroring leaf.
125    pub cause: GuardCause,
126}
127
128impl fmt::Display for GuardError {
129    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
130        match &self.cause {
131            GuardCause::UnreadableState(s) => write!(
132                f,
133                "constraint guard error: state variable #{s} cannot be read (a null or deleted \
134                 object handle, or an X/Z value)"
135            ),
136            GuardCause::Eval(e) => write!(f, "constraint guard error: {e}"),
137        }
138    }
139}
140
141impl std::error::Error for GuardError {}
142
143/// Whether `e` reads any random variable.
144fn reads_var(e: &Expr) -> bool {
145    let mut any = false;
146    e.for_each_var(&mut |_, _| any = true);
147    any
148}
149
150/// The first state variable `e` reads that has no value under `a`.
151fn unreadable_state(e: &Expr, a: &Assignment) -> Option<StateId> {
152    let mut bad = None;
153    e.for_each_state(&mut |s| {
154        if bad.is_none() && !matches!(a.states.get(s as usize), Some(Some(_))) {
155            bad = Some(s);
156        }
157    });
158    bad
159}
160
161/// The value of one leaf (module docs), or why it is `ERROR`.
162fn leaf(e: &Expr, a: &Assignment) -> Result<GuardValue, GuardCause> {
163    if let Some(s) = unreadable_state(e, a) {
164        return Err(GuardCause::UnreadableState(s));
165    }
166    if reads_var(e) {
167        return Ok(GuardValue::Random);
168    }
169    match eval(e, a) {
170        Ok(v) if v.is_zero() => Ok(GuardValue::False),
171        Ok(_) => Ok(GuardValue::True),
172        Err(e) => Err(GuardCause::Eval(e)),
173    }
174}
175
176/// The value of the predicate `pred` under `a` (only `a.states` is read; a
177/// state of `None` is unreadable), by Figure 18-3 applied recursively.
178pub fn value(pred: &Expr, a: &Assignment) -> GuardValue {
179    match pred {
180        Expr::Binary(BinOp::LogAnd, l, r, _) => value(l, a).and(value(r, a)),
181        Expr::Binary(BinOp::LogOr, l, r, _) => value(l, a).or(value(r, a)),
182        Expr::Unary(UnOp::LogNot, x, _) => value(x, a).not(),
183        other => leaf(other, a).unwrap_or(GuardValue::Error),
184    }
185}
186
187/// The first leaf that makes the `ERROR` predicate `pred` an error. `pred`
188/// must have [`value`] `Error`.
189fn cause(pred: &Expr, a: &Assignment) -> GuardError {
190    let erroring = |e: &Expr| value(e, a) == GuardValue::Error;
191    let inner = match pred {
192        Expr::Binary(BinOp::LogAnd | BinOp::LogOr, l, r, _) => {
193            if erroring(l) {
194                Some(&**l)
195            } else if erroring(r) {
196                Some(&**r)
197            } else {
198                None
199            }
200        }
201        Expr::Unary(UnOp::LogNot, x, _) if erroring(x) => Some(&**x),
202        _ => None,
203    };
204    match inner {
205        Some(i) => cause(i, a),
206        None => GuardError {
207            cause: match leaf(pred, a) {
208                Err(c) => c,
209                Ok(_) => unreachable!("`cause` is only asked of an erroring predicate"),
210            },
211        },
212    }
213}
214
215fn constant(b: bool) -> Expr {
216    Expr::Const(Ty::BIT, if b { BigUint::one() } else { BigUint::zero() })
217}
218
219/// The `RANDOM` predicate `pred` with every decided sub-tree replaced by a
220/// constant (module docs).
221fn simplify(pred: &Expr, a: &Assignment) -> Result<Expr, GuardError> {
222    match value(pred, a) {
223        GuardValue::True => Ok(constant(true)),
224        GuardValue::False => Ok(constant(false)),
225        GuardValue::Error => Err(cause(pred, a)),
226        GuardValue::Random => Ok(match pred {
227            Expr::Binary(op @ (BinOp::LogAnd | BinOp::LogOr), l, r, t) => Expr::Binary(
228                *op,
229                Box::new(simplify(l, a)?),
230                Box::new(simplify(r, a)?),
231                *t,
232            ),
233            Expr::Unary(UnOp::LogNot, x, t) => {
234                Expr::Unary(UnOp::LogNot, Box::new(simplify(x, a)?), *t)
235            }
236            leaf => leaf.clone(),
237        }),
238    }
239}
240
241/// `e` with every [`Expr::Guard`] resolved under the state values of `a`
242/// (module docs): a `FALSE` guard becomes its else arm, a `TRUE` guard its
243/// body, a `RANDOM` guard a guard over the simplified predicate, and an
244/// `ERROR` guard is the call's failure. An arm that is not selected is
245/// dropped unexamined, so a guard inside it cannot raise an error ("the
246/// constraint is eliminated and can generate no error").
247pub fn resolve(e: &Expr, a: &Assignment) -> Result<Expr, GuardError> {
248    Ok(match e {
249        Expr::Const(..) | Expr::Var(..) | Expr::State(..) => e.clone(),
250        Expr::Guard(p, then, otherwise, t) => match value(p, a) {
251            GuardValue::True => resolve(then, a)?,
252            GuardValue::False => resolve(otherwise, a)?,
253            GuardValue::Error => return Err(cause(p, a)),
254            GuardValue::Random => Expr::Guard(
255                Box::new(simplify(p, a)?),
256                Box::new(resolve(then, a)?),
257                Box::new(resolve(otherwise, a)?),
258                *t,
259            ),
260        },
261        Expr::Unary(op, x, t) => Expr::Unary(*op, Box::new(resolve(x, a)?), *t),
262        Expr::Binary(op, l, r, t) => {
263            Expr::Binary(*op, Box::new(resolve(l, a)?), Box::new(resolve(r, a)?), *t)
264        }
265        Expr::Ite(c, x, y, t) => Expr::Ite(
266            Box::new(resolve(c, a)?),
267            Box::new(resolve(x, a)?),
268            Box::new(resolve(y, a)?),
269            *t,
270        ),
271        Expr::Resize(x, t) => Expr::Resize(Box::new(resolve(x, a)?), *t),
272        Expr::Concat(parts, t) => Expr::Concat(
273            parts
274                .iter()
275                .map(|p| resolve(p, a))
276                .collect::<Result<_, _>>()?,
277            *t,
278        ),
279        Expr::Slice(x, lo, t) => Expr::Slice(Box::new(resolve(x, a)?), *lo, *t),
280        Expr::AllDistinct(members) => Expr::AllDistinct(
281            members
282                .iter()
283                .map(|m| resolve(m, a))
284                .collect::<Result<_, _>>()?,
285        ),
286        Expr::Array(n) => {
287            let mut err = None;
288            let r = n.map_children(&mut |c| match resolve(c, a) {
289                Ok(x) => x,
290                Err(e) => {
291                    err.get_or_insert(e);
292                    c.clone()
293                }
294            });
295            if let Some(e) = err {
296                return Err(e);
297            }
298            Expr::Array(r)
299        }
300    })
301}
302
303#[cfg(test)]
304mod tests {
305    use super::GuardValue::{Error as E, False as F, Random as R, True as T};
306    use super::*;
307
308    const ALL: [GuardValue; 4] = [F, T, E, R];
309
310    /// Figure 18-3 transcribed: rows and columns in the figure's order
311    /// `0 1 E R`.
312    const AND: [[GuardValue; 4]; 4] = [
313        [F, F, F, F], // 0
314        [F, T, E, R], // 1
315        [F, E, E, E], // E
316        [F, R, E, R], // R
317    ];
318    const OR: [[GuardValue; 4]; 4] = [
319        [F, T, E, R], // 0
320        [T, T, T, T], // 1
321        [E, T, E, E], // E
322        [R, T, E, R], // R
323    ];
324    const NOT: [GuardValue; 4] = [T, F, E, R];
325
326    #[test]
327    fn conjunction_matches_figure_18_3_in_every_cell() {
328        for (i, a) in ALL.iter().enumerate() {
329            for (j, b) in ALL.iter().enumerate() {
330                assert_eq!(a.and(*b), AND[i][j], "{a:?} && {b:?}");
331            }
332        }
333    }
334
335    #[test]
336    fn disjunction_matches_figure_18_3_in_every_cell() {
337        for (i, a) in ALL.iter().enumerate() {
338            for (j, b) in ALL.iter().enumerate() {
339                assert_eq!(a.or(*b), OR[i][j], "{a:?} || {b:?}");
340            }
341        }
342    }
343
344    #[test]
345    fn negation_matches_figure_18_3() {
346        for (i, a) in ALL.iter().enumerate() {
347            assert_eq!(a.not(), NOT[i], "!{a:?}");
348        }
349    }
350
351    #[test]
352    fn the_tables_do_not_depend_on_operand_order() {
353        // "The subexpressions are evaluated in an arbitrary order."
354        for a in ALL {
355            for b in ALL {
356                assert_eq!(a.and(b), b.and(a));
357                assert_eq!(a.or(b), b.or(a));
358            }
359        }
360    }
361
362    fn u8t() -> Ty {
363        Ty::unsigned(8)
364    }
365    fn st(i: u32) -> Expr {
366        Expr::State(i, u8t())
367    }
368    fn var(i: u32) -> Expr {
369        Expr::Var(i, u8t())
370    }
371    fn k(v: u64) -> Expr {
372        Expr::constant(u8t(), v)
373    }
374    fn bin(op: BinOp, l: Expr, r: Expr) -> Expr {
375        let t = match op {
376            BinOp::Eq
377            | BinOp::Ne
378            | BinOp::Lt
379            | BinOp::Gt
380            | BinOp::LogAnd
381            | BinOp::LogOr
382            | BinOp::LogImpl => Ty::BIT,
383            _ => l.ty(),
384        };
385        Expr::Binary(op, Box::new(l), Box::new(r), t)
386    }
387    fn not(x: Expr) -> Expr {
388        Expr::Unary(UnOp::LogNot, Box::new(x), Ty::BIT)
389    }
390    fn guard(p: Expr, then: Expr, otherwise: Expr) -> Expr {
391        Expr::Guard(Box::new(p), Box::new(then), Box::new(otherwise), Ty::BIT)
392    }
393    fn states(v: &[Option<u64>]) -> Assignment {
394        Assignment {
395            vars: vec![],
396            states: v.iter().map(|x| x.map(BigUint::from)).collect(),
397        }
398    }
399
400    /// A leaf with each of the four values: `s0 == 1` is `TRUE` and
401    /// `s0 == 2` `FALSE` under `s0 = 1`, `s1 == 0` reads the unreadable
402    /// `s1` (`ERROR`) and `v0 == 3` reads a random variable (`RANDOM`).
403    fn leaf_of(v: GuardValue) -> Expr {
404        match v {
405            T => bin(BinOp::Eq, st(0), k(1)),
406            F => bin(BinOp::Eq, st(0), k(2)),
407            E => bin(BinOp::Eq, st(1), k(0)),
408            R => bin(BinOp::Eq, var(0), k(3)),
409        }
410    }
411    fn env() -> Assignment {
412        states(&[Some(1), None])
413    }
414
415    #[test]
416    fn leaves_are_classified_by_what_they_read() {
417        let a = env();
418        for v in ALL {
419            assert_eq!(value(&leaf_of(v), &a), v, "leaf for {v:?}");
420        }
421        // A leaf reading both a random variable and an unreadable state is
422        // an error: the dereference is the error, whatever else it reads.
423        let both = bin(BinOp::Lt, var(0), st(1));
424        assert_eq!(value(&both, &a), E);
425        // A state-only leaf whose evaluation fails is an error too.
426        let div = bin(BinOp::Div, st(0), k(0));
427        let div = bin(BinOp::Eq, div, k(0));
428        assert_eq!(value(&div, &a), E);
429        // Truthiness: a non-bit leaf is true when nonzero.
430        assert_eq!(value(&st(0), &a), T);
431        assert_eq!(value(&k(0), &a), F);
432    }
433
434    #[test]
435    fn predicates_combine_by_the_tables_for_every_pair() {
436        let a = env();
437        for (i, x) in ALL.iter().enumerate() {
438            for (j, y) in ALL.iter().enumerate() {
439                let and = bin(BinOp::LogAnd, leaf_of(*x), leaf_of(*y));
440                let or = bin(BinOp::LogOr, leaf_of(*x), leaf_of(*y));
441                assert_eq!(value(&and, &a), AND[i][j], "{x:?} && {y:?}");
442                assert_eq!(value(&or, &a), OR[i][j], "{x:?} || {y:?}");
443            }
444            assert_eq!(value(&not(leaf_of(*x)), &a), NOT[i], "!{x:?}");
445        }
446    }
447
448    #[test]
449    fn false_dominates_error_and_true_dominates_error_unlike_left_to_right() {
450        let a = env();
451        // E && 0: a left-to-right evaluator would already have failed.
452        let e_and_f = bin(BinOp::LogAnd, leaf_of(E), leaf_of(F));
453        assert_eq!(value(&e_and_f, &a), F);
454        let e_or_t = bin(BinOp::LogOr, leaf_of(E), leaf_of(T));
455        assert_eq!(value(&e_or_t, &a), T);
456        // 1 && E: the error survives.
457        let t_and_e = bin(BinOp::LogAnd, leaf_of(T), leaf_of(E));
458        assert_eq!(value(&t_and_e, &a), E);
459    }
460
461    #[test]
462    fn a_false_guard_takes_the_else_arm_and_drops_an_erroring_then_arm() {
463        let a = env();
464        // if (s0 == 2) <guard that errors> else v0 == 5
465        let bad_then = guard(leaf_of(E), k_bit(1), k_bit(1));
466        let else_arm = bin(BinOp::Eq, var(0), k(5));
467        let g = guard(leaf_of(F), bad_then, else_arm.clone());
468        assert_eq!(resolve(&g, &a), Ok(else_arm));
469        // `a -> b` is a guard whose else arm is the constant 1: eliminated.
470        let imp = guard(leaf_of(F), bin(BinOp::Eq, var(0), k(5)), k_bit(1));
471        assert_eq!(resolve(&imp, &a), Ok(k_bit(1)));
472    }
473
474    fn k_bit(v: u64) -> Expr {
475        Expr::constant(Ty::BIT, v)
476    }
477
478    #[test]
479    fn a_true_guard_is_its_body_unconditionally() {
480        let a = env();
481        let body = bin(BinOp::Eq, var(0), k(5));
482        let g = guard(leaf_of(T), body.clone(), k_bit(1));
483        assert_eq!(resolve(&g, &a), Ok(body));
484    }
485
486    #[test]
487    fn an_error_guard_fails_with_the_erroring_leaf() {
488        let a = env();
489        let g = guard(leaf_of(E), k_bit(1), k_bit(1));
490        assert_eq!(
491            resolve(&g, &a),
492            Err(GuardError {
493                cause: GuardCause::UnreadableState(1)
494            })
495        );
496        // The cause is the leaf that decides the value, not one the tables
497        // dominated: (E && 0) || E fails on the second E (state #1 both
498        // times here, so use an eval error for the dominated one).
499        let div = bin(BinOp::Eq, bin(BinOp::Div, st(0), k(0)), k(0));
500        let p = bin(
501            BinOp::LogOr,
502            bin(BinOp::LogAnd, div, leaf_of(F)),
503            leaf_of(E),
504        );
505        let g = guard(p, k_bit(1), k_bit(1));
506        assert_eq!(
507            resolve(&g, &a),
508            Err(GuardError {
509                cause: GuardCause::UnreadableState(1)
510            })
511        );
512    }
513
514    #[test]
515    fn a_random_guard_stays_with_its_decided_subtrees_folded() {
516        let a = env();
517        // (v0 == 3 || s0 == 2 || (s1 == 0 && s0 == 2)) -> body: the second
518        // and third disjuncts are FALSE (the third drops its ERROR), so the
519        // conditional constraint is `(v0 == 3 || 0 || 0) -> body`.
520        let p = bin(
521            BinOp::LogOr,
522            bin(BinOp::LogOr, leaf_of(R), leaf_of(F)),
523            bin(BinOp::LogAnd, leaf_of(E), leaf_of(F)),
524        );
525        let body = bin(BinOp::Eq, var(1), k(7));
526        let g = guard(p, body.clone(), k_bit(1));
527        let want_p = bin(
528            BinOp::LogOr,
529            bin(BinOp::LogOr, leaf_of(R), k_bit(0)),
530            k_bit(0),
531        );
532        assert_eq!(resolve(&g, &a), Ok(guard(want_p, body, k_bit(1))));
533    }
534
535    #[test]
536    fn a_random_guard_with_an_error_disjunct_fails() {
537        let a = env();
538        // R || E is E: the guard cannot be left conditional.
539        let p = bin(BinOp::LogOr, leaf_of(R), leaf_of(E));
540        let g = guard(p, k_bit(1), k_bit(1));
541        assert!(resolve(&g, &a).is_err());
542    }
543
544    #[test]
545    fn guards_nest_and_resolve_inside_other_nodes() {
546        let a = env();
547        // (if (s0==1) (if (s0==2) X else Y)) && Z resolves to Y && Z.
548        let y = bin(BinOp::Eq, var(0), k(1));
549        let z = bin(BinOp::Eq, var(0), k(2));
550        let x = bin(BinOp::Eq, var(0), k(9));
551        let inner = guard(leaf_of(F), x, y.clone());
552        let outer = guard(leaf_of(T), inner, k_bit(1));
553        let all = bin(BinOp::LogAnd, outer, z.clone());
554        assert_eq!(resolve(&all, &a), Ok(bin(BinOp::LogAnd, y, z)));
555    }
556
557    #[test]
558    fn a_uniqueness_group_is_resolved_through_its_guards() {
559        let a = env();
560        let group = |m: Vec<Expr>| Expr::AllDistinct(m);
561        // The taken arm of a decided guard is the group itself.
562        let g = guard(
563            leaf_of(T),
564            group(vec![var(0), var(1), st(0)]),
565            group(vec![var(0), var(1)]),
566        );
567        assert_eq!(resolve(&g, &a), Ok(group(vec![var(0), var(1), st(0)])));
568        let g = guard(
569            leaf_of(F),
570            group(vec![var(0), var(1), st(0)]),
571            group(vec![var(0), var(1)]),
572        );
573        assert_eq!(resolve(&g, &a), Ok(group(vec![var(0), var(1)])));
574        // A random guard keeps the group as its body.
575        let g = guard(leaf_of(R), group(vec![var(0), var(1)]), k_bit(1));
576        assert_eq!(
577            resolve(&g, &a),
578            Ok(guard(leaf_of(R), group(vec![var(0), var(1)]), k_bit(1)))
579        );
580        // A guard inside a member is resolved in place, in member order.
581        let member = bin(BinOp::Add, var(1), k(1));
582        let wrapped = guard(leaf_of(T), member.clone(), k_bit(1));
583        let g = group(vec![var(0), wrapped]);
584        assert_eq!(resolve(&g, &a), Ok(group(vec![var(0), member])));
585        // An unreadable state in a taken guard is still the loud error.
586        let g = group(vec![var(0), guard(leaf_of(E), var(1), var(0))]);
587        assert!(resolve(&g, &a).is_err());
588    }
589
590    #[test]
591    fn an_expression_without_guards_resolves_to_itself() {
592        let a = env();
593        let e = bin(
594            BinOp::LogImpl,
595            bin(BinOp::Lt, var(0), st(0)),
596            bin(BinOp::Eq, var(1), k(4)),
597        );
598        assert_eq!(resolve(&e, &a), Ok(e));
599    }
600}
vj_sim/constraints/guard.rs

vj_sim/constraints/
guard.rs
