Skip to content

Commit

Permalink
Rename projection to project (matches pick/select).
Browse files Browse the repository at this point in the history
  • Loading branch information
daemontus committed Dec 15, 2020
1 parent d8e51b1 commit 49a65b4
Show file tree
Hide file tree
Showing 2 changed files with 15 additions and 18 deletions.
8 changes: 4 additions & 4 deletions src/_impl_bdd/_impl_relation_ops.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ impl Bdd {
///
/// If we see the Bdd as a set of bitvectors, this is essentially existential quantification:
/// $\exists x_i : (x_1, ..., x_i, ..., x_n) \in BDD$.
pub fn var_projection(&self, variable: BddVariable) -> Bdd {
pub fn var_project(&self, variable: BddVariable) -> Bdd {
Bdd::fused_binary_flip_op(
(self, None),
(self, Some(variable)),
Expand All @@ -20,13 +20,13 @@ impl Bdd {
///
/// This can be used to implement operations like `domain` and `range` of
/// a certain relation.
pub fn projection(&self, variables: &[BddVariable]) -> Bdd {
pub fn project(&self, variables: &[BddVariable]) -> Bdd {
// Starting from the last Bdd variables is more efficient, we therefore enforce it.
// (variables vector is always very small anyway)
sorted(variables)
.into_iter()
.rev()
.fold(self.clone(), |result, v| result.var_projection(v))
.fold(self.clone(), |result, v| result.var_project(v))
}

/// Picks one valuation for the given `BddVariable`.
Expand Down Expand Up @@ -60,7 +60,7 @@ impl Bdd {
pub fn pick(&self, variables: &[BddVariable]) -> Bdd {
fn r_pick(set: &Bdd, variables: &[BddVariable]) -> Bdd {
if let Some((last_var, rest)) = variables.split_last() {
let picked = r_pick(&set.var_projection(*last_var), rest);
let picked = r_pick(&set.var_project(*last_var), rest);
picked.and(&set.var_pick(*last_var))
} else {
set.clone()
Expand Down
25 changes: 11 additions & 14 deletions src/_test_bdd/_test_bdd_relation_ops.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ fn bdd_var_projection() {
let bdd = variables.eval_expression_string("(v1 => (v2 <=> v3)) & (!v1 => !(v2 <=> v5))");
let v1 = BddVariable(0);
assert_eq!(
bdd.var_projection(v1),
bdd.var_project(v1),
variables.eval_expression_string("(v2 <=> v3) | !(v2 <=> v5)")
);
}
Expand Down Expand Up @@ -64,12 +64,12 @@ fn bdd_projection_trivial() {

let vars = (0..5).map(BddVariable).collect::<Vec<_>>();
for k in 0..5 {
assert_eq!(ff, ff.projection(&vars[0..k]));
assert_eq!(tt, tt.projection(&vars[0..k]));
assert_eq!(ff, ff.project(&vars[0..k]));
assert_eq!(tt, tt.project(&vars[0..k]));
}

assert_eq!(bdd, bdd.projection(&Vec::new()));
assert_eq!(tt, bdd.projection(&vars));
assert_eq!(bdd, bdd.project(&Vec::new()));
assert_eq!(tt, bdd.project(&vars));
}

#[test]
Expand All @@ -79,20 +79,17 @@ fn bdd_projection_simple() {
{
let bdd = variables.eval_expression_string("(v1 <=> v2) & (v4 <=> v5)");
let projected = variables.eval_expression_string("(v1 <=> v2)");
assert_eq!(projected, bdd.projection(&vec![v4, v5]));
assert_eq!(
bdd.projection(&vec![v3, v4, v5]),
bdd.projection(&vec![v4, v5])
);
assert_eq!(projected, bdd.project(&vec![v4, v5]));
assert_eq!(bdd.project(&vec![v3, v4, v5]), bdd.project(&vec![v4, v5]));
}
{
let bdd = variables.eval_expression_string("(v4 => (v1 & v2)) & (!v4 => (!v1 & v3))");
let projected_3 = variables.eval_expression_string("(v1 & v2) | (!v1 & v3)");
let projected_2 = variables.eval_expression_string("(v1 & v2) | !v1");
assert_eq!(bdd, bdd.projection(&vec![v5]));
assert_eq!(projected_3, bdd.projection(&vec![v4]));
assert_eq!(projected_2, bdd.projection(&vec![v3, v4]));
assert_eq!(variables.mk_true(), bdd.projection(&vec![v2, v3, v4]));
assert_eq!(bdd, bdd.project(&vec![v5]));
assert_eq!(projected_3, bdd.project(&vec![v4]));
assert_eq!(projected_2, bdd.project(&vec![v3, v4]));
assert_eq!(variables.mk_true(), bdd.project(&vec![v2, v3, v4]));
}
}

Expand Down

0 comments on commit 49a65b4

Please sign in to comment.