cvlr_nondet/
core.rs

1/// A trait for giving a type a non-deterministic value
2pub trait Nondet: Sized {
3    fn nondet() -> Self;
4
5    fn nondet_with<F>(func: F) -> Self
6    where
7        F: FnOnce(&Self) -> bool,
8    {
9        let val = Self::nondet();
10        cvlr_asserts::cvlr_assume!(func(&val));
11        val
12    }
13}
14
15/// Return a nondet value of type according to the Nondet trait
16pub fn nondet<T: Nondet>() -> T {
17    Nondet::nondet()
18}
19
20pub fn nondet_with<T: Nondet, F>(func: F) -> T
21where
22    F: FnOnce(&T) -> bool,
23{
24    Nondet::nondet_with(func)
25}
26
27#[macro_export]
28macro_rules! nondet_impl {
29    ($t:ty, $v:expr, $doc:tt) => {
30        impl Nondet for $t {
31            #[inline]
32            #[doc = $doc]
33            fn nondet() -> $t {
34                $v
35            }
36        }
37    };
38}