vj_sim/constraints/
func_order.rs

1//! The implicit solve order of function arguments (task C13; IEEE 1800-2023
2//! 18.5.11).
3//!
4//! "Random variables used as function arguments get solved first": a call's
5//! return value is a state variable, so every random variable the call's
6//! arguments mention must have its value before the constraint holding the call
7//! can be solved. The LRM puts it as an implicit variable ordering: the
8//! argument variables have priority over the other random variables of the
9//! constraint, constraints over only higher-priority variables are solved
10//! first, and a circular ordering is an error.
11//!
12//! [`stages`] computes that order as a level per variable: stage 0 has no
13//! argument obligation, a variable constrained together with a call over `a`
14//! sits one stage after `a` (the longest chain decides). The registry solves
15//! stage by stage, the values of earlier stages being constants (state) for
16//! the later ones.
17//!
18//! Only the *outermost* call of an expression yields edges: the variables of its
19//! whole argument tree (nested calls included) precede the conjunct's other
20//! variables. A variable that is an argument of any call of the conjunct is not
21//! "other" for any of them, so `F(a) == G(b)` puts `a` and `b` in one stage (the
22//! equation between two return values is then a check on a drawn pair, not a
23//! circular order). The `dist` selector variables (numbered at or after
24//! `n_vars`) take no part: they are not random variables of the class.
25
26use super::dist::SELECTOR_BASE;
27use super::ir::{ArrayNode, Expr, VarId};
28use std::collections::BTreeSet;
29
30/// The implicit order is circular (LRM 18.5.11).
31#[derive(Clone, Copy, Debug, PartialEq, Eq)]
32pub struct Cycle;
33
34/// The variables of `e` outside any call, and of the argument trees of its
35/// outermost calls.
36fn split(e: &Expr, others: &mut BTreeSet<VarId>, args: &mut BTreeSet<VarId>) {
37    match e {
38        Expr::Array(ArrayNode::Call { args: a, .. }) => {
39            for x in a {
40                x.for_each_var(&mut |v, _| {
41                    args.insert(v);
42                });
43            }
44        }
45        Expr::Var(v, _) => {
46            others.insert(*v);
47        }
48        other => {
49            let _ = other.try_map_children::<()>(&mut |c| {
50                split(c, others, args);
51                Ok(c.clone())
52            });
53        }
54    }
55}
56
57/// The stage of each of the `n_vars` random variables (module docs). A
58/// conjunct set with no call over a random variable puts everything in stage 0.
59pub fn stages(n_vars: usize, conjuncts: &[Expr]) -> Result<Vec<u32>, Cycle> {
60    let mut edges: BTreeSet<(usize, usize)> = BTreeSet::new();
61    for c in conjuncts {
62        let (mut others, mut args) = (BTreeSet::new(), BTreeSet::new());
63        split(c, &mut others, &mut args);
64        let real =
65            |v: &VarId| (*v < SELECTOR_BASE && (*v as usize) < n_vars).then_some(*v as usize);
66        let args: Vec<usize> = args.iter().filter_map(real).collect();
67        for o in others.iter().filter_map(real) {
68            if args.contains(&o) {
69                continue;
70            }
71            for &a in &args {
72                edges.insert((a, o));
73            }
74        }
75    }
76    // Longest path by Kahn's algorithm.
77    let mut indeg = vec![0usize; n_vars];
78    let mut succ: Vec<Vec<usize>> = vec![Vec::new(); n_vars];
79    for &(a, b) in &edges {
80        indeg[b] += 1;
81        succ[a].push(b);
82    }
83    let mut stage = vec![0u32; n_vars];
84    let mut ready: Vec<usize> = (0..n_vars).filter(|&v| indeg[v] == 0).collect();
85    let mut done = 0;
86    while let Some(v) = ready.pop() {
87        done += 1;
88        for &w in &succ[v] {
89            stage[w] = stage[w].max(stage[v] + 1);
90            indeg[w] -= 1;
91            if indeg[w] == 0 {
92                ready.push(w);
93            }
94        }
95    }
96    if done != n_vars {
97        return Err(Cycle);
98    }
99    Ok(stage)
100}
101
102#[cfg(test)]
103mod tests {
104    use super::*;
105    use crate::constraints::ir::{BinOp, Ty};
106
107    fn s32() -> Ty {
108        Ty::signed(32)
109    }
110    fn var(i: u32) -> Expr {
111        Expr::Var(i, s32())
112    }
113    fn call(args: Vec<Expr>) -> Expr {
114        Expr::Array(ArrayNode::Call {
115            func: 0,
116            args,
117            ty: s32(),
118        })
119    }
120    fn eq(a: Expr, b: Expr) -> Expr {
121        Expr::Binary(BinOp::Eq, Box::new(a), Box::new(b), Ty::BIT)
122    }
123
124    #[test]
125    fn no_call_means_one_stage() {
126        assert_eq!(stages(3, &[eq(var(0), var(1))]), Ok(vec![0, 0, 0]));
127    }
128
129    #[test]
130    fn an_argument_is_solved_before_the_other_variables_of_its_constraint() {
131        // x(0) <= F(y(1)): y first.
132        let c = eq(var(0), call(vec![var(1)]));
133        assert_eq!(stages(2, &[c]), Ok(vec![1, 0]));
134    }
135
136    #[test]
137    fn chains_take_the_longest_path() {
138        // x == F(y), y == F(z): z, y, x.
139        let cs = [
140            eq(var(0), call(vec![var(1)])),
141            eq(var(1), call(vec![var(2)])),
142        ];
143        assert_eq!(stages(3, &cs), Ok(vec![2, 1, 0]));
144    }
145
146    #[test]
147    fn two_arguments_of_one_constraint_share_a_stage() {
148        // F(a) == G(b): no order between a and b (a check on the pair).
149        let c = eq(call(vec![var(0)]), call(vec![var(1)]));
150        assert_eq!(stages(2, &[c]), Ok(vec![0, 0]));
151        // x == F(x): a variable that is also an argument is not "other".
152        assert_eq!(stages(1, &[eq(var(0), call(vec![var(0)]))]), Ok(vec![0]));
153    }
154
155    #[test]
156    fn nested_calls_put_every_inner_variable_before_the_rest() {
157        // x == F(G(a, b)): a and b first.
158        let c = eq(var(0), call(vec![call(vec![var(1), var(2)])]));
159        assert_eq!(stages(3, &[c]), Ok(vec![1, 0, 0]));
160    }
161
162    #[test]
163    fn a_circular_order_is_an_error() {
164        // x == F(y) and y == F(x): LRM 18.5.11 says circular is an error.
165        let cs = [
166            eq(var(0), call(vec![var(1)])),
167            eq(var(1), call(vec![var(0)])),
168        ];
169        assert_eq!(stages(2, &cs), Err(Cycle));
170    }
171
172    #[test]
173    fn selector_variables_take_no_part() {
174        let c = eq(var(SELECTOR_BASE), call(vec![var(0)]));
175        assert_eq!(stages(1, &[c]), Ok(vec![0]));
176    }
177}
vj_sim/constraints/func_order.rs

vj_sim/constraints/
func_order.rs
