Skip to content

Commit

Permalink
Better (more correct) implementation of extend and prune.
Browse files Browse the repository at this point in the history
  • Loading branch information
daemontus committed May 14, 2024
1 parent 392c762 commit b59ce38
Show file tree
Hide file tree
Showing 3 changed files with 139 additions and 114 deletions.
216 changes: 112 additions & 104 deletions src/bdd/traits/boolean_function.rs
Original file line number Diff line number Diff line change
Expand Up @@ -407,55 +407,59 @@ mod tests {
assert_eq!(actual.degree(), expected.degree());
}

// #[test]
// fn test_substitute_variables_same_substituted_ok() {
// let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
// .expect("Should not panic here");
//
// let new_value = var("a") | !var("b");
// let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
// let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
//
// // cannot use `var("a") | !var("b") | var("b")` for defining expected here
// // since that collapses Or(Or(a, !b), b), which substitute doesn't do
// let expected = Bdd::try_from(
// Expression::n_ary_or(&[new_value.clone(), var("b")])
// & var("c")
// & !new_value.clone()
// & bool(true),
// )
// .expect("Should not panic here");
// let actual = input.substitute(&mapping);
//
// assert_eq!(expected, actual);
// assert!(expected.is_equivalent(&actual));
// assert_eq!(actual.degree(), expected.degree());
// }
//
// #[test]
// fn test_substitute_variables_same_unsubstituted_ok() {
// let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
// .expect("Should not panic here");
//
// let new_value = var("c") | !var("b");
// let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
// let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
//
// // cannot use `var("a") | !var("b") | var("b")` for defining expected here
// // since that collapses Or(Or(a, !b), b), which substitute doesn't do
// let expected = Bdd::try_from(
// Expression::n_ary_or(&[new_value.clone(), var("b")])
// & var("c")
// & !new_value.clone()
// & bool(true),
// )
// .expect("Should not panic here");
// let actual = input.substitute(&mapping);
//
// assert_eq!(expected, actual);
// assert!(expected.is_equivalent(&actual));
// assert_eq!(actual.degree(), expected.degree());
// }
#[test]
#[should_panic]
fn test_substitute_variables_same_substituted_ok() {
let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
.expect("Should not panic here");

let new_value = var("a") | !var("b");
let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);

// cannot use `var("a") | !var("b") | var("b")` for defining expected here
// since that collapses Or(Or(a, !b), b), which substitute doesn't do
let expected = Bdd::try_from(
Expression::n_ary_or(&[new_value.clone(), var("b")])
& var("c")
& !new_value.clone()
& bool(true),
)
.expect("Should not panic here");
let actual = input.substitute(&mapping);

assert_eq!(expected, actual);
assert!(expected.is_equivalent(&actual));
assert_eq!(actual.degree(), expected.degree());
}

#[test]
fn test_substitute_variables_same_unsubstituted_ok() {
// (a | b) & c & !a & 1
let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
.expect("Should not panic here");

// c | !b
let new_value = var("c") | !var("b");
let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);

// cannot use `var("a") | !var("b") | var("b")` for defining expected here
// since that collapses Or(Or(a, !b), b), which substitute doesn't do
// ((c | !b) | b) & c & !(c | !b) & 1
let expected = Bdd::try_from(
Expression::n_ary_or(&[new_value.clone(), var("b")])
& var("c")
& !new_value.clone()
& bool(true),
)
.expect("Should not panic here");
let actual = input.substitute(&mapping);

assert_eq!(expected, actual);
assert!(expected.is_equivalent(&actual));
assert_eq!(actual.degree(), expected.degree());
}

#[test]
fn test_substitute_variables_added_only_ok() {
Expand Down Expand Up @@ -485,61 +489,65 @@ mod tests {
assert_eq!(actual.degree(), expected.degree());
}

// #[test]
// fn test_substitute_variables_added_and_substituted_ok() {
// let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
// .expect("Should not panic here");
//
// let new_value = var("ddd") & (bool(false) | var("a"));
// let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
// let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
//
// // cannot use bitwise operators for defining expected here
// // since that collapses Or(Or(a, !b), b), which substitute doesn't do
// let expected = Bdd::try_from(
// Expression::n_ary_or(&[new_value.clone(), var("b")])
// & var("c")
// & !new_value.clone()
// & bool(true),
// )
// .expect("Should not panic here");
// let actual = input.substitute(&mapping);
//
// assert_eq!(expected, actual);
// assert!(expected.is_equivalent(&actual));
//
// assert_eq!(input.degree(), 3);
// assert_eq!(actual.degree(), 4);
// assert_eq!(expected.degree(), 4);
// }
//
// #[test]
// fn test_substitute_variables_added_and_unsubstituted_ok() {
// let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
// .expect("Should not panic here");
//
// let new_value = var("ddd") & (bool(false) | var("b"));
// let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
// let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
//
// // cannot use bitwise operators for defining expected here
// // since that collapses Or(Or(a, !b), b), which substitute doesn't do
// let expected = Bdd::try_from(
// Expression::n_ary_or(&[new_value.clone(), var("b")])
// & var("c")
// & !new_value.clone()
// & bool(true),
// )
// .expect("Should not panic here");
// let actual = input.substitute(&mapping);
//
// assert_eq!(expected, actual);
// assert!(expected.is_equivalent(&actual));
//
// assert_eq!(input.degree(), 3);
// assert_eq!(actual.degree(), 3);
// assert_eq!(expected.degree(), 3);
// }
#[test]
#[should_panic]
fn test_substitute_variables_added_and_substituted_ok() {
let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
.expect("Should not panic here");

let new_value = var("ddd") & (bool(false) | var("a"));
let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);

// cannot use bitwise operators for defining expected here
// since that collapses Or(Or(a, !b), b), which substitute doesn't do
let expected = Bdd::try_from(
Expression::n_ary_or(&[new_value.clone(), var("b")])
& var("c")
& !new_value.clone()
& bool(true),
)
.expect("Should not panic here");
let actual = input.substitute(&mapping);

assert_eq!(expected, actual);
assert!(expected.is_equivalent(&actual));

assert_eq!(input.degree(), 3);
assert_eq!(actual.degree(), 4);
assert_eq!(expected.degree(), 4);
}

#[test]
fn test_substitute_variables_added_and_unsubstituted_ok() {
// (a | b) & c & !a & 1
let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
.expect("Should not panic here");

// ddd & (0 | b)
let new_value = var("ddd") & (bool(false) | var("b"));
let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);

// cannot use bitwise operators for defining expected here
// since that collapses Or(Or(a, !b), b), which substitute doesn't do
// ((ddd & (0 | b)) | b) & c & !(ddd & (0 | b)) & 1
let expected = Bdd::try_from(
Expression::n_ary_or(&[new_value.clone(), var("b")])
& var("c")
& !new_value.clone()
& bool(true),
)
.expect("Should not panic here");
let actual = input.substitute(&mapping);

assert_eq!(expected, actual);
assert!(expected.is_equivalent(&actual));

assert_eq!(input.degree(), 3);
assert_eq!(actual.degree(), 3);
assert_eq!(expected.degree(), 3);
}

#[test]
fn test_substitute_variables_removed_ok() {
Expand Down
18 changes: 13 additions & 5 deletions src/bdd/utils/extend_variables.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,10 @@ pub fn extend_bdd_variables<TLiteral: Debug + Clone + Eq + Ord>(
bdd: &Bdd<TLiteral>,
new_inputs: &[TLiteral],
) -> Bdd<TLiteral> {
if bdd.inputs == new_inputs {
return bdd.clone();
}

// Test pre-condition.
debug_assert!(bdd.inputs.iter().all(|it| new_inputs.contains(it)));

Expand All @@ -23,14 +27,16 @@ pub fn extend_bdd_variables<TLiteral: Debug + Clone + Eq + Ord>(
// Also, since `bdd.inputs` is a subset of `new_inputs`, we know that every
// `bdd.inputs[old_i]` must (eventually) appear in the `new_inputs` iterator, we just
// need to skip enough of the new variables.
let mut old_i = 0;
for (new_i, var) in new_inputs.iter().enumerate() {
if new_i < bdd.inputs.len() && &bdd.inputs[old_i] == var {
for (old_i, var) in bdd.inputs.iter().enumerate() {
let new_i = new_inputs
.binary_search(var)
.expect("Collection `new_inputs` is not a superset of `bdd.inputs`.");

if new_i != old_i {
permutation.insert(
BddVariable::from_index(old_i),
BddVariable::from_index(new_i),
);
old_i += 1;
}
}

Expand All @@ -39,7 +45,9 @@ pub fn extend_bdd_variables<TLiteral: Debug + Clone + Eq + Ord>(
// These operations are not memory-unsafe, they can just break the BDD
// in weird ways if you don't know what you are doing.
new_bdd.set_num_vars(u16::try_from(new_inputs.len()).unwrap());
new_bdd.rename_variables(&permutation);
if !permutation.is_empty() {
new_bdd.rename_variables(&permutation);
}
}

Bdd::new(new_bdd, new_inputs.to_owned())
Expand Down
19 changes: 14 additions & 5 deletions src/bdd/utils/prune_variables.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,10 @@ pub fn prune_bdd_variables<TLiteral: Debug + Clone + Eq + Ord>(
bdd: &Bdd<TLiteral>,
new_inputs: &[TLiteral],
) -> Bdd<TLiteral> {
if bdd.inputs == new_inputs {
return bdd.clone();
}

// Test pre-condition.
debug_assert!(bdd
.essential_inputs()
Expand All @@ -22,22 +26,27 @@ pub fn prune_bdd_variables<TLiteral: Debug + Clone + Eq + Ord>(

// "Inverse" of `expand_bdd_variables`. This works because both input lists are sorted
// and the `new_inputs` is a subset of `bdd.inputs`.
let mut new_i = 0usize;
for (old_i, var) in bdd.inputs.iter().enumerate() {
if new_i < new_inputs.len() && &new_inputs[new_i] == var {
for (new_i, var) in new_inputs.iter().enumerate() {
let old_i = bdd
.inputs
.binary_search(var)
.expect("Collection `new_inputs` is not a subset of `bdd.inputs`.");

if new_i != old_i {
permutation.insert(
BddVariable::from_index(old_i),
BddVariable::from_index(new_i),
);
new_i += 1;
}
}

let mut new_bdd = bdd.bdd.clone();
unsafe {
// These operations are not memory-unsafe, they can just break the BDD
// in weird ways if you don't know what you are doing.
new_bdd.rename_variables(&permutation);
if !permutation.is_empty() {
new_bdd.rename_variables(&permutation);
}
new_bdd.set_num_vars(u16::try_from(new_inputs.len()).unwrap());
// Also, notice that here, we are setting the variable count *after*
// the permutation, not before, because it is actually decreasing, not
Expand Down

0 comments on commit b59ce38

Please sign in to comment.