sv_sim_sim/constraints/
priority.rs

1//! Soft constraints and their priorities (Task C15; IEEE 1800-2023 18.5.13,
2//! 18.5.13.1, 18.5.13.2).
3//!
4//! # Representation
5//!
6//! A soft constraint is an ordinary boolean conjunct wrapped as
7//! `Var(SOFT_BASE + k) || body`: the hidden variable `k` is the soft's *discard
8//! flag*. Resolving a call replaces every flag by a constant
9//! ([`resolve_softs`]): a discarded soft becomes `true` ("treated as if
10//! replaced by the value 1", 18.5.13) and a kept one is its body, so the
11//! solver never sees a soft constraint, only the hard problem one choice of
12//! flags describes. The wrapper may sit anywhere in a conjunct, so `p -> soft
13//! q` and `if (c) soft q; else soft r;` need nothing more.
14//!
15//! # Priorities (18.5.13.1)
16//!
17//! [`Priority`] orders the soft constraints of a program: the object (an
18//! object contained through a `rand` handle ranks below its container), then
19//! the class level (a derived class above its bases, an inline constraint
20//! above all), then the declaration order. [`object_order`] is the rule for
21//! contained objects: the container above every contained object, a later
22//! handle above an earlier one, and an object held through several handles at
23//! the rank of the last of them. The class-level and declaration-order rules
24//! are what the builder's `Builder::set_priority_scope` and its running
25//! sequence number implement.
26//!
27//! # Solving (18.5.13's conceptual model)
28//!
29//! [`solve_relaxing`] is the staged relaxation: try every soft constraint; if
30//! that has no solution, try the hard constraints alone (their failure is an
31//! ordinary failure) and then take the soft constraints in priority order,
32//! keeping each one only if it can be satisfied together with the hard
33//! constraints and the higher-priority softs already kept. This is the "c1
34//! and c2, else c1, else c2, else neither" model applied recursively, and
35//! it needs nothing of the solver but a feasibility answer.
36//!
37//! # `disable soft` (18.5.13.2)
38//!
39//! A [`Disable`] discards every *lower*-priority soft constraint that directly
40//! names the same random variable ([`SoftKey`]), unconditionally;
41//! [`apply_disables`] does it once, statically, because priorities and the
42//! variables a constraint names are static.
43
44use super::dist::{Dist, SELECTOR_BASE};
45use super::ir::{ArrayId, ArrayNode, BinOp, Expr, Ty, VarId};
46use num_bigint::BigUint;
47use num_traits::One;
48
49/// The first discard-flag id: soft `k`'s flag is `Var(SOFT_BASE + k)`. Above
50/// [`SELECTOR_BASE`] so no pass that already skips selector variables can
51/// mistake it for a field.
52pub const SOFT_BASE: VarId = 1 << 31;
53
54/// The rank of one soft constraint (or `disable soft`); larger is stronger.
55/// Ordered by object, then class level, then declaration order.
56#[derive(
57    Clone,
58    Copy,
59    Debug,
60    Default,
61    PartialEq,
62    Eq,
63    PartialOrd,
64    Ord,
65    Hash,
66    serde::Serialize,
67    serde::Deserialize,
68)]
69pub struct Priority {
70    /// The rank of the object the constraint belongs to: contained objects
71    /// rank below their container ([`object_order`]).
72    pub object: u32,
73    /// The class level within the object: a derived class's constraints rank
74    /// above its base classes'; an inline constraint above every class level.
75    pub level: u32,
76    /// The declaration sequence: later is higher.
77    pub seq: u32,
78}
79
80/// A random variable a `disable soft` can name, or a soft constraint can
81/// directly mention (18.5.13.2: "including `array.size`").
82#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
83pub enum SoftKey {
84    /// A scalar random variable (or one element of a fixed array).
85    Var(VarId),
86    /// Some element of a dynamic array or queue, or the array as a whole when
87    /// it is a `disable soft` target.
88    Array(ArrayId),
89    /// The size of a dynamic array or queue.
90    ArraySize(ArrayId),
91}
92
93impl SoftKey {
94    /// Whether a `disable soft` on `self` reaches a soft constraint that
95    /// mentions `mention` (18.5.13.2: only where the variable *directly*
96    /// appears). Naming a whole array reaches its elements and its size;
97    /// naming `A.size` only the size.
98    pub fn disables(self, mention: SoftKey) -> bool {
99        match (self, mention) {
100            (SoftKey::Var(a), SoftKey::Var(b)) => a == b,
101            (SoftKey::Array(a), SoftKey::Array(b) | SoftKey::ArraySize(b)) => a == b,
102            (SoftKey::ArraySize(a), SoftKey::ArraySize(b)) => a == b,
103            _ => false,
104        }
105    }
106}
107
108/// One soft constraint of a program.
109#[derive(Clone, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
110pub struct Soft {
111    /// Its priority.
112    pub priority: Priority,
113    /// The [`Dist`]s (indices into the program's dist table) it contains.
114    pub dists: Vec<u32>,
115    /// The random variables it directly mentions.
116    pub keys: Vec<SoftKey>,
117    /// Discarded for every call by a higher-priority `disable soft`
118    /// ([`apply_disables`]).
119    pub disabled: bool,
120    /// The `disable soft`s ([`Disable`]s, by their index in the program's
121    /// table) that reach it: [`Self::disabled`] is whether any is in force. A
122    /// `disable soft` in a constraint block `constraint_mode(0)` switched off
123    /// is not (LRM 18.9), so a call recomputes the flag from this list.
124    pub disabled_by: Vec<u32>,
125}
126
127/// One `disable soft x;` constraint.
128#[derive(Clone, Copy, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
129pub struct Disable {
130    /// Its priority: only softs below it are discarded.
131    pub priority: Priority,
132    /// The variable it names.
133    pub key: SoftKey,
134}
135
136/// Marks every soft constraint a `disable soft` of higher priority reaches.
137pub fn apply_disables(softs: &mut [Soft], disables: &[Disable]) {
138    for s in softs {
139        s.disabled_by = disables
140            .iter()
141            .enumerate()
142            .filter(|(_, d)| d.priority > s.priority && s.keys.iter().any(|&k| d.key.disables(k)))
143            .map(|(i, _)| i as u32)
144            .collect();
145        s.disabled = !s.disabled_by.is_empty();
146    }
147}
148
149/// The random variables `e` (and the `dists` it holds) directly mention.
150pub fn keys_of(e: &Expr, dists: &[&Dist]) -> Vec<SoftKey> {
151    let mut keys: Vec<SoftKey> = Vec::new();
152    let mut add = |k: SoftKey| {
153        if !keys.contains(&k) {
154            keys.push(k);
155        }
156    };
157    e.for_each_var(&mut |v, _| {
158        if v < SELECTOR_BASE {
159            add(SoftKey::Var(v));
160        }
161    });
162    e.any_node(&mut |n| {
163        if let Expr::Array(a) = n {
164            match a {
165                ArrayNode::Size(id) => add(SoftKey::ArraySize(*id)),
166                ArrayNode::Elem { array, .. }
167                | ArrayNode::Foreach { array, .. }
168                | ArrayNode::Reduce { array, .. } => add(SoftKey::Array(*array)),
169                ArrayNode::Distinct { arrays, .. } => {
170                    arrays.iter().for_each(|a| add(SoftKey::Array(*a)));
171                }
172                // A pick's elements are plain variables and states, found above.
173                ArrayNode::Loop(..) | ArrayNode::Call { .. } | ArrayNode::Pick { .. } => {}
174            }
175        }
176        false
177    });
178    for d in dists {
179        for &v in &d.vars {
180            add(SoftKey::Var(v));
181        }
182    }
183    keys
184}
185
186/// The soft constraint with discard flag `id` wrapped around `body`.
187pub fn wrap_soft(id: u32, body: Expr) -> Expr {
188    Expr::Binary(
189        BinOp::LogOr,
190        Box::new(Expr::Var(SOFT_BASE + id, Ty::BIT)),
191        Box::new(body),
192        Ty::BIT,
193    )
194}
195
196/// `e` with every soft wrapper resolved: `discard[k]` replaces soft `k` by
197/// `true`, a kept soft by its body. `Err(k)` names a flag outside `discard`.
198pub fn resolve_softs(e: &Expr, discard: &[bool]) -> Result<Expr, u32> {
199    let mapped = e.try_map_children(&mut |c| resolve_softs(c, discard))?;
200    if let Expr::Binary(BinOp::LogOr, a, b, _) = &mapped
201        && let Expr::Var(v, _) = **a
202        && v >= SOFT_BASE
203    {
204        let k = v - SOFT_BASE;
205        return match discard.get(k as usize) {
206            Some(true) => Ok(Expr::Const(Ty::BIT, BigUint::one())),
207            Some(false) => Ok((**b).clone()),
208            None => Err(k),
209        };
210    }
211    Ok(mapped)
212}
213
214/// Whether `e` holds a soft wrapper.
215pub fn has_soft(e: &Expr) -> bool {
216    e.any_node(&mut |n| matches!(n, Expr::Var(v, _) if *v >= SOFT_BASE))
217}
218
219/// Solves a problem with `softs`: `attempt(discard, seed)` solves it with the
220/// soft constraints flagged in `discard` replaced by `true` and returns its
221/// solution (it must not have any effect but advancing `seed`);
222/// `relaxable(err)` says whether an error means "no solution for this choice
223/// of softs" and not a failure of the call.
224///
225/// Every soft first; if there is no solution, the hard constraints alone (a
226/// failure there is the call's), then each soft by priority, kept when it fits
227/// with everything kept so far (module docs). Each attempt starts from the
228/// call's seed, so the result is exactly the draw a program with only the kept
229/// constraints would make, and with no contradiction it is the draw of the
230/// all-hard program.
231pub fn solve_relaxing<T, E>(
232    softs: &[Soft],
233    seed: &mut u64,
234    mut attempt: impl FnMut(&[bool], &mut u64) -> Result<T, E>,
235    relaxable: impl Fn(&E) -> bool,
236) -> Result<T, E> {
237    let seed0 = *seed;
238    let initial: Vec<bool> = softs.iter().map(|s| s.disabled).collect();
239    let mut s = seed0;
240    match attempt(&initial, &mut s) {
241        Ok(t) => {
242            *seed = s;
243            return Ok(t);
244        }
245        Err(e) if !relaxable(&e) => return Err(e),
246        Err(_) => {}
247    }
248    // Hard constraints alone: no solution here is the call's failure.
249    let mut best_seed = seed0;
250    let mut best = attempt(&vec![true; softs.len()], &mut best_seed)?;
251    let mut order: Vec<usize> = (0..softs.len()).filter(|&k| !softs[k].disabled).collect();
252    order.sort_by(|&a, &b| softs[b].priority.cmp(&softs[a].priority).then(b.cmp(&a)));
253    let mut keep = vec![false; softs.len()];
254    for k in order {
255        keep[k] = true;
256        let discard: Vec<bool> = keep.iter().map(|&b| !b).collect();
257        let mut s = seed0;
258        match attempt(&discard, &mut s) {
259            Ok(t) => {
260                best = t;
261                best_seed = s;
262            }
263            Err(e) if relaxable(&e) => keep[k] = false,
264            Err(e) => return Err(e),
265        }
266    }
267    *seed = best_seed;
268    Ok(best)
269}
270
271/// The objects reached from `root` through `contained` (its `rand` object
272/// handles in declaration order), lowest priority first and `root` last
273/// (18.5.13.1): every container above the objects it contains, a later handle
274/// above an earlier one, and an object contained several times at the rank of
275/// the highest, i.e. last, occurrence. An object graph can be cyclic, so an
276/// object is not entered again while it is being expanded.
277pub fn object_order<K: Clone + PartialEq>(root: &K, contained: &impl Fn(&K) -> Vec<K>) -> Vec<K> {
278    fn walk<K: Clone + PartialEq>(
279        o: &K,
280        path: &mut Vec<K>,
281        contained: &impl Fn(&K) -> Vec<K>,
282        out: &mut Vec<K>,
283    ) {
284        if path.contains(o) {
285            return;
286        }
287        path.push(o.clone());
288        for c in contained(o) {
289            walk(&c, path, contained, out);
290        }
291        path.pop();
292        out.push(o.clone());
293    }
294    let mut all = Vec::new();
295    walk(root, &mut Vec::new(), contained, &mut all);
296    let mut kept: Vec<K> = Vec::new();
297    for o in all.into_iter().rev() {
298        if !kept.contains(&o) {
299            kept.push(o);
300        }
301    }
302    kept.reverse();
303    kept
304}
305
306#[cfg(test)]
307mod tests {
308    use super::*;
309    use crate::constraints::ir::BinOp;
310
311    fn s(object: u32, level: u32, seq: u32) -> Priority {
312        Priority { object, level, seq }
313    }
314
315    fn soft(priority: Priority, keys: Vec<SoftKey>) -> Soft {
316        Soft {
317            priority,
318            dists: Vec::new(),
319            keys,
320            disabled: false,
321            disabled_by: Vec::new(),
322        }
323    }
324
325    // ---- 18.5.13.1's worked example -------------------------------------
326
327    /// A class of the example: its base, and per class level its soft
328    /// constraints in declaration order.
329    struct Class {
330        base: Option<&'static Class>,
331        /// This level's constraint blocks in the order that fixes their
332        /// priority (an `extern` block at its prototype), each with the
333        /// labels of its soft constraints in order.
334        blocks: &'static [&'static [&'static str]],
335        /// `rand` handle members: (name, class).
336        handles: &'static [(&'static str, &'static Class)],
337    }
338
339    static B1: Class = Class {
340        base: None,
341        blocks: &[&["a1", "a2"]],
342        handles: &[],
343    };
344    static D1: Class = Class {
345        base: Some(&B1),
346        blocks: &[&["b1"]],
347        handles: &[],
348    };
349    static B2: Class = Class {
350        base: None,
351        blocks: &[&["c1"]],
352        handles: &[],
353    };
354    static D2: Class = Class {
355        base: Some(&B2),
356        // d, the extern block e (at its prototype, so before f), then f
357        blocks: &[&["d1"], &["e1"], &["f1"]],
358        handles: &[("p1", &D1), ("p2", &B1), ("p3", &D1)],
359    };
360
361    /// An object of the example: its class and a name for its identity.
362    #[derive(Clone, Copy)]
363    struct Obj {
364        class: &'static Class,
365        id: u32,
366    }
367
368    /// Objects are the same when their ids are.
369    impl PartialEq for Obj {
370        fn eq(&self, other: &Obj) -> bool {
371            self.id == other.id
372        }
373    }
374
375    /// The soft constraints of one object with their priorities: base levels
376    /// first (lower), then the class's, blocks and constraints in order.
377    fn object_softs(o: Obj, rank: u32, prefix: &str) -> Vec<(Priority, String)> {
378        let mut chain: Vec<&'static Class> = Vec::new();
379        let mut c = Some(o.class);
380        while let Some(k) = c {
381            chain.push(k);
382            c = k.base;
383        }
384        chain.reverse(); // root base first
385        let mut seq = 0;
386        let mut out = Vec::new();
387        for (level, class) in chain.iter().enumerate() {
388            for block in class.blocks {
389                for label in *block {
390                    out.push((s(rank, level as u32, seq), format!("{prefix}{label}")));
391                    seq += 1;
392                }
393            }
394        }
395        out
396    }
397
398    /// Objects of the example: id 0 is `d`; `p1`, `p2`, `p3` are 1, 2, 3 (or
399    /// `p3` is `p1` itself when `same`).
400    fn contained(same: bool) -> impl Fn(&Obj) -> Vec<Obj> {
401        move |o: &Obj| {
402            o.class
403                .handles
404                .iter()
405                .enumerate()
406                .map(|(i, (_, class))| Obj {
407                    class,
408                    id: if same && i == 2 { 1 } else { i as u32 + 1 },
409                })
410                .collect()
411        }
412    }
413
414    /// The whole call's soft constraints, highest priority first, as the
415    /// subclause writes them: the inline constraints on top.
416    fn chain(same: bool) -> String {
417        let root = Obj { class: &D2, id: 0 };
418        let objects = object_order(&root, &contained(same));
419        let mut all: Vec<(Priority, String)> = Vec::new();
420        for (rank, o) in objects.iter().enumerate() {
421            let prefix = match (o.class as *const Class, o.id) {
422                (_, 0) => String::new(),
423                (_, 1) if same => "p3.".to_string(),
424                (_, 1) => "p1.".to_string(),
425                (_, 2) => "p2.".to_string(),
426                _ => "p3.".to_string(),
427            };
428            all.extend(object_softs(*o, rank as u32, &prefix));
429        }
430        // inline constraints: above every class level of every object
431        all.push((s(u32::MAX, u32::MAX, 0), "i1".to_string()));
432        all.push((s(u32::MAX, u32::MAX, 1), "i2".to_string()));
433        all.sort_by_key(|b| std::cmp::Reverse(b.0));
434        all.into_iter()
435            .map(|(_, l)| l)
436            .collect::<Vec<_>>()
437            .join(" ")
438    }
439
440    #[test]
441    fn the_priority_chain_is_the_one_18_5_13_1_gives() {
442        assert_eq!(
443            chain(false),
444            "i2 i1 f1 e1 d1 c1 p3.b1 p3.a2 p3.a1 p2.a2 p2.a1 p1.b1 p1.a2 p1.a1"
445        );
446    }
447
448    #[test]
449    fn the_same_object_through_two_handles_takes_the_higher_rank() {
450        assert_eq!(
451            chain(true),
452            "i2 i1 f1 e1 d1 c1 p3.b1 p3.a2 p3.a1 p2.a2 p2.a1"
453        );
454    }
455
456    #[test]
457    fn object_order_expands_nested_objects_and_survives_cycles() {
458        // 0 holds 1 then 2; 1 holds 3; 3 holds 0 again (a cycle).
459        let contained = |o: &u32| match *o {
460            0 => vec![1, 2],
461            1 => vec![3],
462            3 => vec![0],
463            _ => Vec::new(),
464        };
465        // 3 is contained in 1, 1 before 2; the cycle back to 0 is not entered.
466        assert_eq!(object_order(&0, &contained), vec![3, 1, 2, 0]);
467        // An object reached again later takes the later rank.
468        let again = |o: &u32| match *o {
469            0 => vec![1, 2, 1],
470            _ => Vec::new(),
471        };
472        assert_eq!(object_order(&0, &again), vec![2, 1, 0]);
473    }
474
475    // ---- disable soft ---------------------------------------------------
476
477    #[test]
478    fn a_disable_discards_only_lower_priority_softs_that_mention_the_variable() {
479        let x = SoftKey::Var(0);
480        let y = SoftKey::Var(1);
481        let mut softs = vec![
482            soft(s(0, 0, 0), vec![x]),    // A1: below the disable
483            soft(s(0, 0, 2), vec![x]),    // A3: above it
484            soft(s(0, 0, 0), vec![y]),    // another variable
485            soft(s(0, 0, 0), vec![x, y]), // mentions x directly
486        ];
487        let disables = [Disable {
488            priority: s(0, 0, 1),
489            key: x,
490        }];
491        apply_disables(&mut softs, &disables);
492        let flags: Vec<bool> = softs.iter().map(|s| s.disabled).collect();
493        assert_eq!(flags, vec![true, false, false, true]);
494    }
495
496    #[test]
497    fn a_disable_on_a_whole_array_reaches_its_size_and_a_size_disable_only_the_size() {
498        let size = SoftKey::ArraySize(3);
499        let elem = SoftKey::Array(3);
500        assert!(elem.disables(size) && elem.disables(elem));
501        assert!(size.disables(size) && !size.disables(elem));
502        assert!(!SoftKey::Array(4).disables(size));
503        assert!(!SoftKey::Var(3).disables(elem));
504    }
505
506    // ---- resolve_softs ---------------------------------------------------
507
508    fn var(v: u32) -> Expr {
509        Expr::Var(v, Ty::unsigned(8))
510    }
511
512    fn lt(a: Expr, b: Expr) -> Expr {
513        Expr::Binary(BinOp::Lt, Box::new(a), Box::new(b), Ty::BIT)
514    }
515
516    #[test]
517    fn a_discarded_soft_is_true_and_a_kept_one_is_its_body() {
518        let body = lt(var(0), Expr::Const(Ty::unsigned(8), BigUint::from(3u32)));
519        let e = Expr::Binary(
520            BinOp::LogAnd,
521            Box::new(wrap_soft(0, body.clone())),
522            Box::new(wrap_soft(1, body.clone())),
523            Ty::BIT,
524        );
525        assert!(has_soft(&e));
526        let one = Expr::Const(Ty::BIT, BigUint::one());
527        let r = resolve_softs(&e, &[false, true]).unwrap();
528        assert_eq!(
529            r,
530            Expr::Binary(BinOp::LogAnd, Box::new(body), Box::new(one), Ty::BIT)
531        );
532        assert!(!has_soft(&r));
533        assert_eq!(resolve_softs(&e, &[false]), Err(1));
534    }
535
536    #[test]
537    fn the_variables_a_soft_mentions_exclude_the_flags_and_selectors() {
538        let e = wrap_soft(0, lt(var(2), var(5)));
539        assert_eq!(
540            keys_of(&e, &[]),
541            vec![SoftKey::Var(2), SoftKey::Var(5)],
542            "the discard flag is not a mention"
543        );
544        let arr = Expr::Array(ArrayNode::Size(7));
545        assert_eq!(keys_of(&arr, &[]), vec![SoftKey::ArraySize(7)]);
546    }
547
548    // ---- solve_relaxing --------------------------------------------------
549
550    /// A toy problem: a solution is a set of kept softs; softs `a` and `b`
551    /// conflict. `Err(())` when the kept set contains both.
552    fn toy(
553        softs: &[Soft],
554        conflict: (usize, usize),
555        hard_fails: bool,
556    ) -> Result<Vec<usize>, &'static str> {
557        let mut seed = 5u64;
558        let mut calls = 0;
559        let r = solve_relaxing(
560            softs,
561            &mut seed,
562            |discard, s| {
563                calls += 1;
564                *s += 1;
565                if hard_fails {
566                    return Err("unsat");
567                }
568                let kept: Vec<usize> = (0..discard.len()).filter(|&k| !discard[k]).collect();
569                if kept.contains(&conflict.0) && kept.contains(&conflict.1) {
570                    return Err("unsat");
571                }
572                Ok(kept)
573            },
574            |e| *e == "unsat",
575        );
576        let _ = calls;
577        r
578    }
579
580    #[test]
581    fn without_a_contradiction_every_soft_is_kept() {
582        let softs = vec![soft(s(0, 0, 0), vec![]), soft(s(0, 0, 1), vec![])];
583        assert_eq!(toy(&softs, (7, 8), false), Ok(vec![0, 1]));
584    }
585
586    #[test]
587    fn the_higher_priority_of_two_conflicting_softs_wins() {
588        let softs = vec![
589            soft(s(0, 0, 0), vec![]),
590            soft(s(0, 0, 1), vec![]),
591            soft(s(0, 0, 2), vec![]),
592        ];
593        // 0 and 2 conflict: 2 is later, so higher; 0 is dropped, 1 stays.
594        assert_eq!(toy(&softs, (0, 2), false), Ok(vec![1, 2]));
595        // 1 and 2 conflict: 1 is dropped.
596        assert_eq!(toy(&softs, (1, 2), false), Ok(vec![0, 2]));
597    }
598
599    #[test]
600    fn a_higher_derived_level_beats_a_later_base_declaration() {
601        // soft 0 is in the derived class (level 1) though declared first.
602        let softs = vec![soft(s(0, 1, 0), vec![]), soft(s(0, 0, 1), vec![])];
603        assert_eq!(toy(&softs, (0, 1), false), Ok(vec![0]));
604    }
605
606    #[test]
607    fn a_hard_failure_is_reported_and_disabled_softs_never_return() {
608        let softs = vec![soft(s(0, 0, 0), vec![])];
609        assert_eq!(toy(&softs, (7, 8), true), Err("unsat"));
610        let mut d = soft(s(0, 0, 1), vec![]);
611        d.disabled = true;
612        let softs = vec![soft(s(0, 0, 0), vec![]), d];
613        assert_eq!(toy(&softs, (0, 1), false), Ok(vec![0]));
614    }
615
616    #[test]
617    fn the_seed_is_the_kept_attempts_not_the_probes() {
618        let softs = vec![soft(s(0, 0, 0), vec![]), soft(s(0, 0, 1), vec![])];
619        let mut seed = 100u64;
620        let r = solve_relaxing(
621            &softs,
622            &mut seed,
623            |discard, s| {
624                *s += 1;
625                if discard.iter().all(|d| !d) {
626                    Err("unsat")
627                } else {
628                    Ok(discard.to_vec())
629                }
630            },
631            |e: &&str| *e == "unsat",
632        );
633        assert_eq!(r, Ok(vec![true, false]));
634        assert_eq!(seed, 101, "one draw on top of the call's own seed");
635    }
636}
sv_sim_sim/constraints/priority.rs

sv_sim_sim/constraints/
priority.rs
