Skip to content

Commit

Permalink
Expose Substitution and Subst in oxidd
Browse files Browse the repository at this point in the history
  • Loading branch information
nhusung committed Jun 24, 2024
1 parent 23129e0 commit 9c20f3d
Show file tree
Hide file tree
Showing 3 changed files with 24 additions and 13 deletions.
34 changes: 22 additions & 12 deletions crates/oxidd-core/src/util/substitution.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
use std::marker::PhantomData;
use std::sync::atomic;
use std::sync::atomic::AtomicU64;

Expand Down Expand Up @@ -75,21 +76,29 @@ impl<T: Substitution> Substitution for &T {

/// Substitution mapping variables to replacement functions, created from slices
/// of functions
///
/// `S` is the storage type, and can, e.g., be a `Vec<S>`
#[derive(Debug)]
pub struct Subst<'a, F> {
pub struct Subst<F, S = Vec<F>> {
id: u32,
vars: &'a [F],
replacements: &'a [F],
vars: S,
replacements: S,
phantom: PhantomData<fn(&F)>,
}

impl<F> Copy for Subst<'_, F> {}
impl<F> Clone for Subst<'_, F> {
impl<F, S: Copy> Copy for Subst<F, S> {}
impl<F, S: Clone> Clone for Subst<F, S> {
fn clone(&self) -> Self {
*self
Self {
id: self.id,
vars: self.vars.clone(),
replacements: self.replacements.clone(),
phantom: PhantomData,
}
}
}

impl<'a, F> Substitution for Subst<'a, F> {
impl<'a, F, S: AsRef<[F]>> Substitution for &'a Subst<F, S> {
type Var = &'a F;
type Replacement = &'a F;

Expand All @@ -100,11 +109,11 @@ impl<'a, F> Substitution for Subst<'a, F> {

#[inline]
fn pairs(&self) -> impl ExactSizeIterator<Item = (Self::Var, Self::Replacement)> {
self.vars.iter().zip(self.replacements)
self.vars.as_ref().iter().zip(self.replacements.as_ref())
}
}

impl<'a, F> Subst<'a, F> {
impl<F, S: AsRef<[F]>> Subst<F, S> {
/// Create a new substitution to replace the i-th variable of `vars` by the
/// i-th function in replacement
///
Expand All @@ -114,17 +123,18 @@ impl<'a, F> Subst<'a, F> {
///
/// Panics if `vars` and `replacements` have different length
#[track_caller]
pub fn new(vars: &'a [F], replacements: &'a [F]) -> Self {
pub fn new(vars: S, replacements: S) -> Self {
assert_eq!(
vars.len(),
replacements.len(),
vars.as_ref().len(),
replacements.as_ref().len(),
"`vars` and `replacements` must have the same length"
);

Self {
id: new_substitution_id(),
vars,
replacements,
phantom: PhantomData,
}
}
}
Expand Down
1 change: 1 addition & 0 deletions crates/oxidd/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ pub use oxidd_core::function::FunctionSubst;
pub use oxidd_core::function::NumberBase;
pub use oxidd_core::function::PseudoBooleanFunction;
pub use oxidd_core::function::TVLFunction;
pub use oxidd_core::util::{Subst, Substitution};
pub use oxidd_core::Edge;
pub use oxidd_core::InnerNode;
pub use oxidd_core::LevelNo;
Expand Down
2 changes: 1 addition & 1 deletion crates/oxidd/tests/boolean_function.rs
Original file line number Diff line number Diff line change
Expand Up @@ -635,7 +635,7 @@ impl<'a, B: BooleanFunction + FunctionSubst> TestAllBooleanFunctions<'a, B> {
expected |= ((f_explicit >> mapped_assignment) & 1) << assignment;
}

let actual = self.dd_to_boolean_func[&f.substitute(subst).unwrap()];
let actual = self.dd_to_boolean_func[&f.substitute(&subst).unwrap()];
assert_eq!(actual, expected);
}
}
Expand Down

0 comments on commit 9c20f3d

Please sign in to comment.