oxidd_core/util/
substitution.rs

1use std::marker::PhantomData;
2use std::sync::atomic;
3use std::sync::atomic::AtomicU64;
4
5/// Generate a new, globally unique substitution ID
6pub fn new_substitution_id() -> u32 {
7    static ID: AtomicU64 = AtomicU64::new(0);
8    let id = ID.fetch_add(1, atomic::Ordering::Relaxed);
9    if id > u32::MAX as u64 {
10        panic!(
11            "Too many `Substitution` structs\n\
12            \n\
13            To allow caching across multiple results, we assign each \
14            substitution a unique 32 bit integer. Now, so many substitutions \
15            have been created that we cannot guarantee uniqueness anymore."
16        );
17    }
18
19    id as u32
20}
21
22/// Substitution mapping variables to replacement functions
23///
24/// The intent behind substitution structs is to optimize the case where the
25/// same substitution is applied multiple times. We would like to re-use apply
26/// cache entries across these operations, and therefore, we need a compact
27/// identifier for the substitution (provided by [`Self::id()`] here).
28///
29/// To create a substitution, you'll probably want to use [`Subst::new()`].
30pub trait Substitution {
31    /// Variable type
32    type Var;
33    /// Replacement type
34    type Replacement;
35
36    /// Get the ID of this substitution
37    ///
38    /// This unique identifier may safely be used as part of a cache key, i.e.,
39    /// two different substitutions to be used with one manager must not have
40    /// the same ID. (That two equal substitutions have the same ID would be
41    /// ideal but is not required for correctness.)
42    fn id(&self) -> u32;
43
44    /// Iterate over pairs of variable and replacement
45    fn pairs(&self) -> impl ExactSizeIterator<Item = (Self::Var, Self::Replacement)>;
46
47    /// Map the substitution, e.g., to use different variable and replacement
48    /// types
49    ///
50    /// `f` should be injective with respect to variables (the first component),
51    /// i.e., two different variables should not be mapped to one. This is
52    /// required to preserve that the substitution is a mapping from variables
53    /// to replacement functions.
54    #[inline]
55    fn map<V, R, F>(&self, f: F) -> MapSubst<Self, F>
56    where
57        F: Fn((Self::Var, Self::Replacement)) -> (V, R),
58    {
59        MapSubst { inner: self, f }
60    }
61}
62
63impl<T: Substitution> Substitution for &T {
64    type Var = T::Var;
65    type Replacement = T::Replacement;
66
67    #[inline]
68    fn id(&self) -> u32 {
69        (*self).id()
70    }
71    #[inline]
72    fn pairs(&self) -> impl ExactSizeIterator<Item = (Self::Var, Self::Replacement)> {
73        (*self).pairs()
74    }
75}
76
77/// Substitution mapping variables to replacement functions, created from slices
78/// of functions
79///
80/// `S` is the storage type, and can, e.g., be `Vec<F>` or `&[F]`.
81#[derive(Debug)]
82pub struct Subst<F, S = Vec<F>> {
83    id: u32,
84    vars: S,
85    replacements: S,
86    phantom: PhantomData<fn(&F)>,
87}
88
89impl<F, S: Copy> Copy for Subst<F, S> {}
90impl<F, S: Clone> Clone for Subst<F, S> {
91    fn clone(&self) -> Self {
92        Self {
93            id: self.id,
94            vars: self.vars.clone(),
95            replacements: self.replacements.clone(),
96            phantom: PhantomData,
97        }
98    }
99}
100
101impl<'a, F, S: AsRef<[F]>> Substitution for &'a Subst<F, S> {
102    type Var = &'a F;
103    type Replacement = &'a F;
104
105    #[inline]
106    fn id(&self) -> u32 {
107        self.id
108    }
109
110    #[inline]
111    fn pairs(&self) -> impl ExactSizeIterator<Item = (Self::Var, Self::Replacement)> {
112        self.vars.as_ref().iter().zip(self.replacements.as_ref())
113    }
114}
115
116impl<F, S: AsRef<[F]>> Subst<F, S> {
117    /// Create a new substitution to replace the i-th variable of `vars` by the
118    /// i-th function in replacement
119    ///
120    /// All variables of `vars` should be distinct. Furthermore, variables must
121    /// be handles for the respective decision diagram levels, e.g., the
122    /// respective Boolean function for B(C)DDs, and a singleton set for ZBDDs.
123    ///
124    /// Panics if `vars` and `replacements` have different length
125    #[track_caller]
126    pub fn new(vars: S, replacements: S) -> Self {
127        assert_eq!(
128            vars.as_ref().len(),
129            replacements.as_ref().len(),
130            "`vars` and `replacements` must have the same length"
131        );
132
133        Self {
134            id: new_substitution_id(),
135            vars,
136            replacements,
137            phantom: PhantomData,
138        }
139    }
140}
141
142/// Substitution mapping variables to replacement functions, created via
143/// [`Substitution::map()`]
144#[derive(Clone, Copy, Debug)]
145pub struct MapSubst<'a, S: ?Sized, F> {
146    inner: &'a S,
147    f: F,
148}
149
150impl<V, R, S: Substitution + ?Sized, F: Fn((S::Var, S::Replacement)) -> (V, R)> Substitution
151    for MapSubst<'_, S, F>
152{
153    type Var = V;
154    type Replacement = R;
155
156    #[inline]
157    fn id(&self) -> u32 {
158        self.inner.id()
159    }
160
161    #[inline]
162    fn pairs(&self) -> impl ExactSizeIterator<Item = (Self::Var, Self::Replacement)> {
163        self.inner.pairs().map(&self.f)
164    }
165}
oxidd_core/util/substitution.rs

oxidd_core/util/
substitution.rs
