clean up dsf crate; move IdAlloc to ids crate

dsf/Cargo.toml

@@ -8,7 +8,6 @@ publish = false
 [dependencies]
 imctk-ids = { version = "0.1.0", path = "../ids" }
 imctk-lit = { version = "0.1.0", path = "../lit" }
-bytemuck = "*"
 atomic = "0.6"
 priority-queue = "*"
 

dsf/src/element.rs

@@ -0,0 +1,57 @@
+//! A trait for "elements" that can be split into an "atom" and a "polarity".
+
+use imctk_lit::{Lit, Var};
+
+/// A trait for "elements" that can be split into an "atom" and a "polarity".
+/// 
+/// This lets code generically manipulate variables and literals, and further serves to abstract over their concrete representation.
+/// 
+/// The two most common case this trait is used for are:
+/// 1) The element and the atom are both `Var`. In this case there is only one polarity and the trait implementation is trivial.
+/// 2) The element is `Lit` and the atom is `Var`. Here there are two polarities (`+` and `-`) to keep track of.
+/// 
+/// Mathematically, implementing this trait signifies that elements can be written as pairs `(a, p)` with an atom `a` and a polarity `p`.
+/// The polarities are assumed to form a group `(P, *, 1)`. The trait operations then correspond to:
+/// 1) `from_atom(a) = (a, 1)`
+/// 2) `atom((a, p)) = a`
+/// 3) `apply_pol_of((a, p), (b, q)) = (a, p * q)`
+/// 
+/// Currently, code assumes that `P` is either trivial or isomorphic to `Z_2`.
+/// 
+/// Code using this trait may assume the following axioms to hold:
+/// 1) `from_atom(atom(x)) == x`
+/// 2) `apply_pol_of(atom(x), x) == x`
+/// 3) `apply_pol_of(apply_pol_of(x, y), y) == x`
+// TODO: add missing axioms
+pub trait Element<Atom> {
+    /// Constructs an element from an atom by applying positive polarity.
+    fn from_atom(atom: Atom) -> Self;
+    /// Returns the atom corresponding to an element.
+    fn atom(self) -> Atom;
+    /// Multiplies `self` by the polarity of `other`, i.e. conceptually `apply_pol_of(self, other) = self ^ pol(other)`.
+    fn apply_pol_of(self, other: Self) -> Self;
+}
+
+impl<T> Element<T> for T {
+    fn from_atom(atom: T) -> Self {
+        atom
+    }
+    fn atom(self) -> T {
+        self
+    }
+    fn apply_pol_of(self, _other: T) -> Self {
+        self
+    }
+}
+
+impl Element<Var> for Lit {
+    fn from_atom(atom: Var) -> Self {
+        atom.as_lit()
+    }
+    fn atom(self) -> Var {
+        self.var()
+    }
+    fn apply_pol_of(self, other: Self) -> Self {
+        self ^ other.pol()
+    }
+}

dsf/src/lib.rs

@@ -1,2 +1,13 @@
+//! This crate defines a structure [`UnionFind`] that allows tracking of equivalences between generic elements
+//! and a structure [`TrackedUnionFind`] that provides the same functionality but augmented by change tracking.
+
+#[doc(inline)]
+pub use element::Element;
+#[doc(inline)]
+pub use tracked_union_find::TrackedUnionFind;
+#[doc(inline)]
+pub use union_find::UnionFind;
+
+pub mod element;
+pub mod tracked_union_find;
 pub mod union_find;
-pub mod tracked_union_find;

dsf/src/tests/test_tracked_union_find.rs

@@ -0,0 +1,32 @@
+use super::*;
+use imctk_lit::{Lit, Var};
+
+#[test]
+fn test() {
+    let l = |n| Var::from_index(n).as_lit();
+    let mut tuf = TrackedUnionFind::<Var, Lit>::new();
+    let mut token = tuf.start_observing();
+    tuf.union([l(3), !l(4)]);
+    tuf.union([l(8), l(7)]);
+    let mut token2 = tuf.start_observing();
+    tuf.union([l(4), l(5)]);
+    for change in tuf.drain_changes(&mut token).cloned() {
+        println!("{change:?}");
+    }
+    println!("---");
+    tuf.union([!l(5), l(6)]);
+    tuf.make_repr(l(4).var());
+    let renumber: IdVec<Var, Option<Lit>> =
+        IdVec::from_vec(vec![Some(l(0)), None, None, Some(l(1)), Some(!l(1)), Some(!l(1)), Some(l(1)), Some(l(2)), Some(l(2))]);
+    let reverse = Renumbering::get_reverse(&renumber, &tuf.union_find);
+    dbg!(&renumber, &reverse);
+    tuf.renumber(renumber, reverse);
+    tuf.union([l(0), l(1)]);
+    let mut iter = tuf.drain_changes(&mut token);
+    println!("{:?}", iter.next());
+    iter.stop();
+    println!("---");
+    for change in tuf.drain_changes(&mut token2).cloned() {
+        println!("{change:?}");
+    }
+}

dsf/src/tests/test_union_find.rs

@@ -0,0 +1,176 @@
+#![allow(dead_code, missing_docs)]
+
+use super::*;
+use imctk_lit::{Var, Lit};
+use imctk_ids::id_set_seq::IdSetSeq;
+use rand::prelude::*;
+use std::collections::{HashSet, VecDeque};
+
+#[derive(Default)]
+struct CheckedUnionFind<Atom: Id, Elem> {
+    dut: UnionFind<Atom, Elem>,
+    equivs: IdSetSeq<Atom, Elem>,
+}
+
+impl<Atom: Id, Elem: Id + Element<Atom>> UnionFind<Atom, Elem> {
+    fn debug_print_tree(
+        children: &IdVec<Atom, Vec<Elem>>,
+        atom: Atom,
+        prefix: &str,
+        self_char: &str,
+        further_char: &str,
+        pol: bool,
+    ) {
+        println!(
+            "{prefix}{self_char}{}{:?}",
+            if pol { "!" } else { "" },
+            atom
+        );
+        let my_children = children.get(atom).unwrap();
+        for (index, &child) in my_children.iter().enumerate() {
+            let last = index == my_children.len() - 1;
+            let self_char = if last { "└" } else { "├" };
+            let next_further_char = if last { " " } else { "│" };
+            Self::debug_print_tree(
+                children,
+                child.atom(),
+                &(prefix.to_string() + further_char),
+                self_char,
+                next_further_char,
+                pol ^ (child != Elem::from_atom(child.atom())),
+            );
+        }
+    }
+    fn debug_print(&self) {
+        let mut children: IdVec<Atom, Vec<Elem>> = Default::default();
+        for atom in self.parent.keys() {
+            let parent = self.read_parent(atom);
+            children.grow_for_key(atom);
+            if atom != parent.atom() {
+                children
+                    .grow_for_key(parent.atom())
+                    .push(Elem::from_atom(atom).apply_pol_of(parent));
+            } else {
+                assert!(Elem::from_atom(atom) == parent);
+            }
+        }
+        for atom in self.parent.keys() {
+            if atom == self.read_parent(atom).atom() {
+                Self::debug_print_tree(&children, atom, "", "", " ", false);
+            }
+        }
+    }
+}
+#[derive(Debug, Copy, Clone, PartialOrd, Ord, PartialEq, Eq)]
+enum VarRel {
+    Equiv,
+    AntiEquiv,
+    NotEquiv,
+}
+
+impl<Atom: Id, Elem: Id + Element<Atom>> CheckedUnionFind<Atom, Elem> {
+    fn new() -> Self {
+        CheckedUnionFind {
+            dut: Default::default(),
+            equivs: Default::default(),
+        }
+    }
+    fn ref_equal(&mut self, start: Elem, goal: Elem) -> VarRel {
+        let mut seen: HashSet<Atom> = Default::default();
+        let mut queue: VecDeque<Elem> = [start].into();
+        while let Some(place) = queue.pop_front() {
+            if place.atom() == goal.atom() {
+                if place == goal {
+                    return VarRel::Equiv;
+                } else {
+                    return VarRel::AntiEquiv;
+                }
+            }
+            seen.insert(place.atom());
+            for &next in self.equivs.grow_for(place.atom()).iter() {
+                if !seen.contains(&next.atom()) {
+                    queue.push_back(next.apply_pol_of(place));
+                }
+            }
+        }
+        VarRel::NotEquiv
+    }
+    fn find(&mut self, lit: Elem) -> Elem {
+        let out = self.dut.find(lit);
+        assert!(self.ref_equal(lit, out) == VarRel::Equiv);
+        out
+    }
+    fn union_full(&mut self, lits: [Elem; 2]) -> (bool, [Elem; 2]) {
+        let (ok, [ra, rb]) = self.dut.union_full(lits);
+        assert_eq!(self.ref_equal(lits[0], ra), VarRel::Equiv);
+        assert_eq!(self.ref_equal(lits[1], rb), VarRel::Equiv);
+        assert_eq!(ok, self.ref_equal(lits[0], lits[1]) == VarRel::NotEquiv);
+        assert_eq!(self.dut.find_root(lits[0]), ra);
+        if ok {
+            assert_eq!(self.dut.find_root(lits[1]), ra);
+            self.equivs
+                .grow_for(lits[0].atom())
+                .insert(lits[1].apply_pol_of(lits[0]));
+            self.equivs
+                .grow_for(lits[1].atom())
+                .insert(lits[0].apply_pol_of(lits[1]));
+        } else {
+            assert_eq!(self.dut.find_root(lits[1]).atom(), ra.atom());
+        }
+        (ok, [ra, rb])
+    }
+    fn union(&mut self, lits: [Elem; 2]) -> bool {
+        self.union_full(lits).0
+    }
+    fn make_repr(&mut self, lit: Atom) {
+        self.dut.make_repr(lit);
+        assert_eq!(
+            self.dut.find_root(Elem::from_atom(lit)),
+            Elem::from_atom(lit)
+        );
+        self.check();
+    }
+    fn check(&mut self) {
+        for atom in self.dut.parent.keys() {
+            let parent = self.dut.read_parent(atom);
+            assert_eq!(self.ref_equal(Elem::from_atom(atom), parent), VarRel::Equiv);
+            let root = self.dut.find_root(Elem::from_atom(atom));
+            for &child in self.equivs.grow_for(atom).iter() {
+                assert_eq!(root, self.dut.find_root(child));
+            }
+        }
+    }
+}
+
+#[test]
+fn test() {
+    let mut u: CheckedUnionFind<Var, Lit> = CheckedUnionFind::new();
+    let mut rng = rand_pcg::Pcg64::seed_from_u64(25);
+    let max_var = 2000;
+    for i in 0..2000 {
+        match rng.gen_range(0..10) {
+            0..=4 => {
+                let a = Lit::from_code(rng.gen_range(0..=2 * max_var + 1));
+                let b = Lit::from_code(rng.gen_range(0..=2 * max_var + 1));
+                let result = u.union_full([a, b]);
+                println!("union({a}, {b}) = {result:?}");
+            }
+            5..=7 => {
+                let a = Lit::from_code(rng.gen_range(0..=2 * max_var + 1));
+                let result = u.find(a);
+                println!("find({a}) = {result}");
+            }
+            8 => {
+                u.check();
+            }
+            9 => {
+                let a = Var::from_index(rng.gen_range(0..=max_var));
+                u.make_repr(a);
+                println!("make_repr({a})");
+            }
+            _ => {}
+        }
+    }
+    u.check();
+    //u.dut.debug_print();
+}