Struct CongruenceClosure 

pub struct CongruenceClosure<E, S = DefaultHashBuilder> { /* private fields */ }

An implementation of congruence closure, parametric over an arbitrary disjoint set forest implementation.

Based on Nieuwenhuis and Oliveras Proof-producing Congruence Closure, except without the proof production.

Examples

let mut dsf = DisjointSetForest::with_capacity(5);
let mut cc = CongruenceClosure::new();
let mut us = UseSet::new();
let mut st = Pending::default();
let a = 0;
let b = 1;
let c = 2;
let d = 3;
let e = 4;
let f = 5;
// Set a * b = c
cc.equation(Equate((a, b), c), &mut dsf, &mut us, &mut st);
assert!(dsf.is_empty());
// Set d * e = f
cc.equation(Equate((d, e), f), &mut dsf, &mut us, &mut st);
assert!(dsf.is_empty());
// Set a = d
cc.merge(a, d, &mut dsf, &mut us, &mut st);
assert!(!dsf.is_empty());
for i in 0..5 {
    for j in 0..5 {
        assert_eq!(dsf.node_eq(i, j), i == j || (i == a || i == d) && (j == a || j == d))  
    }
}
// Set b = e
cc.merge(b, e, &mut dsf, &mut us, &mut st);
assert!(dsf.node_eq(b, e));
// By congruence, we now have that c = a * b = d * e = f
assert!(dsf.node_eq(c, f));
assert!(dsf.node_eq(a, d));
assert!(!dsf.node_eq(a, b));
assert!(!dsf.node_eq(a, c));
assert!(!dsf.node_eq(a, e));
assert!(!dsf.node_eq(a, f));
assert!(!dsf.node_eq(b, c));
assert!(!dsf.node_eq(b, d));
assert!(!dsf.node_eq(b, f));
assert!(!dsf.node_eq(c, d));
assert!(!dsf.node_eq(c, e));
assert!(!dsf.node_eq(d, e));
assert!(!dsf.node_eq(d, f));
assert!(!dsf.node_eq(e, f));

Implementations

impl<E> CongruenceClosure<E>

pub fn new() -> Self

Create a new, empty congruence closure

Example

let cc = CongruenceClosure::<Equate<(usize, usize), usize>>::new();
assert!(cc.is_empty());

pub fn with_capacity(capacity: usize) -> Self

Create a new, empty congruence closure with the given node and pair capacities

Example

let cc = CongruenceClosure::<Equate<(usize, usize), usize>>::with_capacity(5);
assert!(cc.is_empty());

impl<E, S> CongruenceClosure<E, S>

where S: BuildHasher,

pub fn with_hasher(hasher: S) -> Self

where S: Clone,

Create a new, empty congruence closure with the given hasher

pub fn with_capacity_and_hasher(capacity: usize, hasher: S) -> Self

where S: Clone,

Create a new, empty congruence closure with the given capacity and hasher

pub fn is_empty(&self) -> bool

Whether this congruence closure is empty, i.e. contains no congruence relations

Example

let mut cc = CongruenceClosure::<Equate<(usize, usize), usize>>::new();
let mut dsf = DisjointSetForest::new();
let mut us = UseSet::new();
let mut cs = Pending::new();
assert!(cc.is_empty());

// This operation only adds something to the disjoint set forest, leaving the congruence
// closure itself empty
cc.merge(3, 4, &mut dsf, &mut us, &mut cs);
assert!(cc.is_empty());
assert!(!dsf.is_empty());

// We now actually add something to the congruence closure by equating an *expression*, here
// simply a pair of `usize` indices, to a term
cc.equation(Equate((1, 2), 3), &mut dsf, &mut us, &mut cs);
assert!(!cc.is_empty());
assert!(!dsf.is_empty());

// On the other hand, equating an expression to a term without introducing any new term-level
// equalities only adds things to the congruence closure, leaving the union-find structure
// unchanged:
cc.clear();
dsf.clear();
cc.equation(Equate((1, 2), 3), &mut dsf, &mut us, &mut cs);
assert!(!cc.is_empty());
assert!(dsf.is_empty());

pub fn clear(&mut self)

Clear this congruence closure, maintaining it’s capacity but otherwise resetting it to empty

Example

let mut cc = CongruenceClosure::new();
let mut dsf = DisjointSetForest::new();
let mut us = UseSet::new();
let mut cs = Pending::new();
assert!(cc.is_empty());
cc.equation(Equate((1, 2), 3), &mut dsf, &mut us, &mut cs);
assert!(!cc.is_empty());
cc.clear();
assert!(cc.is_empty());

pub fn lookup<B, U, I>(&self, expr: &B, union_find: &U) -> Option<&E>

where I: Copy + Hash, B: HashMod<U, I>, E: EqMod<U, I, B> + Equation<U, I>,

Get an equation eqn such that eqn.eq_mod(expr, union_find) == true, if one exists.

Example

let mut cc = CongruenceClosure::new();
let mut dsf = DisjointSetForest::new();
let mut us = UseSet::new();
let mut cs = Pending::new();
assert_eq!(cc.lookup(&(1, 2), &dsf), None);
assert_eq!(cc.lookup(&(0, 2), &dsf), None);
assert_eq!(cc.lookup(&(0, 1), &dsf), None);
cc.equation(Equate((1, 2), 3), &mut dsf, &mut us, &mut cs);
assert_eq!(cc.lookup(&(1, 2), &dsf), Some(&Equate((1, 2), 3)));
assert_eq!(cc.lookup(&(0, 2), &dsf), None);
assert_eq!(cc.lookup(&(0, 1), &dsf), None);
cc.merge(0, 1, &mut dsf, &mut us, &mut cs);
let repr = *cc.lookup(&(1, 2), &dsf).unwrap();
assert_eq!(cc.lookup(&(0, 2), &dsf), Some(&repr));
assert!(repr == Equate((1, 2), 3) || repr == Equate((0, 2), 3));
assert_eq!(cc.lookup(&(0, 1), &dsf), None);

pub fn lookup_mut<B, U, I>(&self, expr: &B, union_find: &mut U) -> Option<&E>

where I: Copy + Hash, B: HashMod<U, I>, E: EqMod<U, I, B> + Equation<U, I>,

Get an equation eqn such that eqn.eq_mod(expr, union_find) == true, if one exists.

Always returns the same result as Self::lookup, but may optimize the union-find data structure provided in the process.

pub fn expr_cong<B, U, I>(&self, expr: &B, ix: I, union_find: &U) -> bool

where I: Copy + Hash, B: HashMod<U, I>, E: EqMod<U, I, B> + Equation<U, I>,

Return whether there is an equation eqn such that eqn.eq_mod(expr, union_find) == true and E::node_eq_mut(eqn.ix(), Some(ix), union_find)

Example

let mut cc = CongruenceClosure::new();
let mut dsf = DisjointSetForest::new();
let mut us = UseSet::new();
let mut cs = Pending::new();

assert!(!cc.expr_cong(&(0, 1), 4, &dsf));
assert!(!cc.expr_cong(&(2, 3), 4, &dsf));

cc.merge(0, 2, &mut dsf, &mut us, &mut cs);
cc.merge(1, 3, &mut dsf, &mut us, &mut cs);
assert!(!cc.expr_cong(&(0, 1), 4, &dsf));
assert!(!cc.expr_cong(&(2, 3), 4, &dsf));

// If we set `(0, 1) ~ 4`, we can deduce `(2, 3) ~ 4`, even though we've never inserted the pair `(2, 3)`
cc.equation(Equate((0, 1), 4), &mut dsf, &mut us, &mut cs);
assert!(cc.expr_cong(&(0, 1), 4, &dsf));
assert!(cc.expr_cong(&(2, 3), 4, &dsf));

pub fn expr_cong_mut<B, U, I>( &self, expr: &B, ix: I, union_find: &mut U, ) -> bool

where I: Copy + Hash, B: HashMod<U, I>, E: EqMod<U, I, B> + Equation<U, I>,

Check whether an expression in the equation language is congruent to a given index

Always returns the same result as Self::expr_cong, but may optimize the union-find data structure provided in the process.

pub fn equation<U, I>( &mut self, eqn: E, union_find: &mut U, use_set: &mut UseSet<I>, pending: &mut Pending<I>, )

where I: Copy + Hash + Ord, E: Equation<U, I>,

Register an equation of the form expr = result, where expr is an expression in this congruence closure’s language

Example

let mut cc = CongruenceClosure::new();
let mut dsf = DisjointSetForest::new();
let mut us = UseSet::new();
let mut cs = Pending::new();
// Say 0 ~ 1 and 2 ~ 3
cc.merge(0, 1, &mut dsf, &mut us, &mut cs);
cc.merge(2, 3, &mut dsf, &mut us, &mut cs);
assert!(dsf.node_eq(0, 1));
assert!(dsf.node_eq(2, 3));
assert!(!dsf.node_eq(4, 5));

// If we set (0, 2) ~ 4 and (1, 3) ~ 5, we can then deduce 4 ~ 5
cc.equation(Equate((0, 2), 4), &mut dsf, &mut us, &mut cs);
assert!(dsf.node_eq(0, 1));
assert!(dsf.node_eq(2, 3));
assert!(!dsf.node_eq(4, 5));
cc.equation(Equate((1, 3), 5), &mut dsf, &mut us, &mut cs);
assert!(dsf.node_eq(0, 1));
assert!(dsf.node_eq(2, 3));
assert!(dsf.node_eq(4, 5));

pub fn merge<U, I>( &mut self, a: I, b: I, union_find: &mut U, use_set: &mut UseSet<I>, pending: &mut Pending<I>, )

where I: Copy + Ord + Hash, E: Equation<U, I>,

Merge the equivalence classes of two nodes

Example

let mut cc = CongruenceClosure::new();
let mut dsf = DisjointSetForest::new();
let mut raw_dsf = DisjointSetForest::new();
let mut us = UseSet::new();
let mut cs = Pending::new();

// Calls to `cc.merge` without any equations added to the congruence context are equivalent to calls to `dsf.union`
cc.merge(0, 1, &mut dsf, &mut us, &mut cs);
raw_dsf.union(0, 1);
assert_eq!(dsf, raw_dsf);

cc.merge(2, 3, &mut dsf, &mut us, &mut cs);
raw_dsf.union(2, 3);
assert_eq!(dsf, raw_dsf);

// Similarly, with only one equation in the context, they do not change the union-find ADT,
// though the equation itself may be modified as the union-find is updated:
assert_eq!(cc.lookup(&(4, 5), &dsf), None);
cc.equation(Equate((4, 5), 6), &mut dsf, &mut us, &mut cs);
assert_eq!(dsf, raw_dsf);
assert_eq!(cc.lookup(&(4, 5), &dsf), Some(&Equate((4, 5), 6)));

cc.merge(0, 4, &mut dsf, &mut us, &mut cs);
raw_dsf.union(0, 4);
assert_eq!(dsf, raw_dsf);

// Once we have a set of equations which overlap, however, calling `merge` can trigger multiple `unions` in the DSF,
// implementing congruence closure:
cc.equation(Equate((4, 7), 8), &mut dsf, &mut us, &mut cs);
assert_eq!(dsf, raw_dsf);

cc.merge(7, 5, &mut dsf, &mut us, &mut cs);
raw_dsf.union(7, 5);
assert!(raw_dsf.refines(&dsf));
assert!(!dsf.refines(&raw_dsf));
// In particular:
assert!(!raw_dsf.node_eq(6, 8));
assert!(dsf.node_eq(6, 8));

pub fn update<U, I>( &mut self, node: I, union_find: &mut U, use_set: &mut UseSet<I>, pending: &mut Pending<I>, )

where I: Copy + Ord + Hash, E: Equation<U, I>,

Update the dependencies on a node

Note that, if node is not a representative anymore, only dependencies not yet attached to the new representative will be updated!

pub fn equation_pending<U, I>( &mut self, eqn: E, union_find: &mut U, use_set: &mut UseSet<I>, pending: &mut Pending<I>, )

where I: Copy + Hash + Ord, E: Equation<U, I>,

Register an equation of the form expr = result, placing any additional merges necessary to complete this change into the pending list

pub fn merge_pending<U, I>( &mut self, a: I, b: I, union_find: &mut U, use_set: &mut UseSet<I>, pending: &mut Pending<I>, )

where I: Copy + Ord + Hash, E: Equation<U, I>,

Merge the equivalence classes of two nodes, placing any additional merges necessary to complete this change into the pending list

pub fn update_pending<U, I>( &mut self, node: I, union_find: &mut U, use_set: &mut UseSet<I>, pending: &mut Pending<I>, )

where I: Copy + Ord + Hash, E: Equation<U, I>,

Update the dependencies on a node, placing any additional operations necessary to finish this update into the Pending operation queue.

Note that, if node is not a representative anymore, only dependencies not yet attached to the new representative will be updated!

pub fn do_pending<U, I>( &mut self, union_find: &mut U, use_set: &mut UseSet<I>, pending: &mut Pending<I>, )

where I: Copy + Ord + Hash, E: Equation<U, I>,

Perform all pending operations in a congruence state, leaving it empty

pub fn check_invariants<U, I>( &self, union_find: &U, use_set: &UseSet<I>, ) -> bool

where I: Copy + Hash + Ord, E: Equation<U, I>, U: UnionFind<I>,

Check this data structure’s invariants w.r.t a union-find ADT

Trait Implementations

impl<E: Clone, S: Clone> Clone for CongruenceClosure<E, S>

fn clone(&self) -> CongruenceClosure<E, S>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<E: Debug, S> Debug for CongruenceClosure<E, S>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<E, S: Default + BuildHasher> Default for CongruenceClosure<E, S>

fn default() -> Self

Returns the “default value” for a type.