oxidd_core/util/
substitution.rs

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

oxidd_core/util/
substitution.rs
