From 072ca08dbbfcef4f36fdebaef1bb12ad46edc3c3 Mon Sep 17 00:00:00 2001
From: Alex Fischman <alexdfischman@gmail.com>
Date: Wed, 2 Aug 2023 11:12:15 -0700
Subject: [PATCH 01/10] Copy old canonical IsoStateSet

Signed-off-by: Alex Fischman <alexdfischman@gmail.com>
---
 bounded/src/set.rs | 312 ++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 292 insertions(+), 20 deletions(-)

diff --git a/bounded/src/set.rs b/bounded/src/set.rs
index 2fb79e0d..33d19893 100644
--- a/bounded/src/set.rs
+++ b/bounded/src/set.rs
@@ -72,7 +72,7 @@ pub fn check(
     print_timing: bool,
 ) -> Result<CheckerAnswer, TranslationError> {
     let (program, context) = translate(module, universe, print_timing)?;
-    match interpret(&program, depth, compress_traces, print_timing) {
+    match interpret(&program, depth, compress_traces, print_timing, &context) {
         InterpreterResult::Unknown => Ok(CheckerAnswer::Unknown),
         InterpreterResult::Convergence => Ok(CheckerAnswer::Convergence),
         InterpreterResult::Counterexample(trace) => {
@@ -1067,17 +1067,19 @@ fn interpret(
     max_depth: Option<usize>,
     compress_traces: TraceCompression,
     print_timing: bool,
+    context: &Context,
 ) -> InterpreterResult {
     // States we have seen so far.
-    let mut seen: HashSet<BoundedState> = program.inits.iter().cloned().collect();
+    let mut seen = IsoStateSet::new(context);
+    for init in &program.inits {
+        seen.insert(init);
+    }
 
     // The BFS queue, i.e., states on the frontier that need to be explored.
     // The queue is always a subset of seen.
-    let mut queue: VecDeque<Trace> = program
-        .inits
-        .iter()
-        .cloned()
-        .map(|state| Trace::new(state, compress_traces))
+    let mut queue: VecDeque<Trace> = seen
+        .states()
+        .map(|state| Trace::new(*state, compress_traces))
         .collect();
 
     let mut transitions = Transitions::new();
@@ -1120,8 +1122,7 @@ fn interpret(
                 tr.updates
                     .iter()
                     .for_each(|update| next.set(update.index, update.formula.evaluate(state)));
-                if !seen.contains(&next) {
-                    seen.insert(next);
+                if seen.insert(&next) {
                     if seen.len() % 1_000_000 == 0 {
                         let elapsed = start_time.elapsed().as_secs_f64();
                         println!(
@@ -1208,6 +1209,133 @@ impl<'a> Transitions<'a> {
     }
 }
 
+/// Can answer the question "have I seen a state that is isomorphic to this one before"?
+struct IsoStateSet {
+    set: HashSet<BoundedState>,
+    max_index: usize,
+    orderings: Vec<Orderings>,
+}
+
+/// A map, where the index is dst and the value is src, of copies from x[src] to y[dst].
+type Ordering = Vec<usize>;
+/// A branch of a trie of orderings
+struct Orderings {
+    src: usize,
+    children: Vec<Orderings>,
+}
+
+impl IsoStateSet {
+    fn new(context: &Context) -> IsoStateSet {
+        fn from_ordering(ordering: &[usize]) -> Vec<Orderings> {
+            match &ordering {
+                [] => vec![],
+                [first, rest @ ..] => vec![Orderings {
+                    src: *first,
+                    children: from_ordering(rest).into_iter().collect(),
+                }],
+            }
+        }
+        fn add_ordering(ordering: &[usize], orderings: &mut Vec<Orderings>) {
+            if ordering.is_empty() || orderings.is_empty() {
+                assert!(
+                    ordering.is_empty() && orderings.is_empty(),
+                    "orderings had different lengths"
+                )
+            }
+            match orderings.iter_mut().find(|o| o.src == ordering[0]) {
+                Some(o) => add_ordering(&ordering[1..], &mut o.children),
+                None => orderings.extend(from_ordering(ordering)),
+            }
+        }
+
+        let sorts: Vec<_> = context.universe.keys().sorted().collect();
+        let mut iter = sorts
+            .iter()
+            .map(|sort| context.universe[sort.as_str()])
+            // the permutations are maps from old to new element values
+            .map(|size| (0..size).permutations(size))
+            // get all combinations of different ways to permute values
+            .multi_cartesian_product_fixed()
+            // reattach sort names onto each ordering
+            .map(|ordering| {
+                assert_eq!(sorts.len(), ordering.len());
+                sorts.iter().map(|s| s.as_str()).zip(ordering).collect()
+            })
+            // convert permutations to copy instructions
+            .map(|permutation: HashMap<&str, Vec<usize>>| {
+                context
+                    .indices
+                    .iter()
+                    .map(|((name, elements), i)| {
+                        let relation = context.signature.relation_decl(name);
+                        assert_eq!(relation.args.len(), elements.len());
+                        // map each old element to a new element
+                        let mut new_elements = elements.clone();
+                        for i in 0..new_elements.len() {
+                            let x = elements[i];
+                            new_elements[i] = match &relation.args[i] {
+                                Sort::Uninterpreted(s) => permutation[s.as_str()][x],
+                                Sort::Bool => x,
+                            };
+                        }
+                        // look up the index to precompute the dst
+                        (context.indices[&(relation.name.as_str(), new_elements)], *i)
+                    })
+                    .sorted()
+                    .map(|(_, v)| v)
+                    .collect()
+            });
+
+        let first: Ordering = iter.next().unwrap();
+        let mut orderings = from_ordering(&first);
+        for ordering in iter {
+            add_ordering(&ordering, orderings.as_mut());
+        }
+
+        IsoStateSet {
+            set: Default::default(),
+            max_index: *context.indices.values().max().unwrap(),
+            orderings,
+        }
+    }
+
+    fn len(&self) -> usize {
+        self.set.len()
+    }
+
+    fn states(&self) -> impl Iterator<Item = &BoundedState> {
+        self.set.iter()
+    }
+
+    fn insert(&mut self, x: &BoundedState) -> bool {
+        self.set.insert(self.canonicalize(x))
+    }
+
+    fn canonicalize(&self, x: &BoundedState) -> BoundedState {
+        let mut orderings: Vec<&Orderings> = self.orderings.iter().collect();
+        let mut y = BoundedState::ZERO;
+        for i in 0..=self.max_index {
+            if i == self.max_index {
+                assert!(orderings.iter().all(|o| o.children.is_empty()));
+            }
+
+            let mut subset: Vec<_> = orderings
+                .iter()
+                .filter(|o| !x.get(o.src))
+                .copied()
+                .collect();
+
+            if subset.is_empty() {
+                y.set(i, true);
+                subset = orderings;
+            }
+
+            orderings = subset.into_iter().flat_map(|o| &o.children).collect();
+        }
+        y
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -1292,6 +1420,18 @@ mod tests {
 
     #[test]
     fn checker_set_basic() {
+        let signature = Signature {
+            sorts: vec![],
+            relations: vec![RelationDecl {
+                args: vec![],
+                sort: Sort::Bool,
+                name: "r".to_string(),
+                mutable: true,
+            }],
+        };
+        let universe = std::collections::HashMap::new();
+        let context = Context::new(&signature, &universe);
+
         let program = BoundedProgram {
             inits: vec![state([0])],
             trs: vec![
@@ -1309,8 +1449,8 @@ mod tests {
                 value: false,
             }),
         };
-        let result0 = interpret(&program, Some(0), TraceCompression::No, false);
-        let result1 = interpret(&program, Some(1), TraceCompression::No, false);
+        let result0 = interpret(&program, Some(0), TraceCompression::No, false, &context);
+        let result1 = interpret(&program, Some(1), TraceCompression::No, false, &context);
         assert_eq!(result0, InterpreterResult::Unknown);
         let mut expected1 = Trace::new(state([0]), TraceCompression::No);
         expected1.push(state([1]));
@@ -1319,6 +1459,38 @@ mod tests {
 
     #[test]
     fn checker_set_cycle() {
+        let signature = Signature {
+            sorts: vec![],
+            relations: vec![
+                RelationDecl {
+                    args: vec![],
+                    sort: Sort::Bool,
+                    name: "0".to_string(),
+                    mutable: true,
+                },
+                RelationDecl {
+                    args: vec![],
+                    sort: Sort::Bool,
+                    name: "1".to_string(),
+                    mutable: true,
+                },
+                RelationDecl {
+                    args: vec![],
+                    sort: Sort::Bool,
+                    name: "2".to_string(),
+                    mutable: true,
+                },
+                RelationDecl {
+                    args: vec![],
+                    sort: Sort::Bool,
+                    name: "3".to_string(),
+                    mutable: true,
+                },
+            ],
+        };
+        let universe = std::collections::HashMap::new();
+        let context = Context::new(&signature, &universe);
+
         let program = BoundedProgram {
             inits: vec![state([1, 0, 0, 0])],
             trs: vec![
@@ -1392,11 +1564,11 @@ mod tests {
                 value: false,
             }),
         };
-        let result1 = interpret(&program, Some(0), TraceCompression::No, false);
-        let result2 = interpret(&program, Some(1), TraceCompression::No, false);
-        let result3 = interpret(&program, Some(2), TraceCompression::No, false);
-        let result4 = interpret(&program, Some(3), TraceCompression::No, false);
-        let result5 = interpret(&program, Some(4), TraceCompression::No, false);
+        let result1 = interpret(&program, Some(0), TraceCompression::No, false, &context);
+        let result2 = interpret(&program, Some(1), TraceCompression::No, false, &context);
+        let result3 = interpret(&program, Some(2), TraceCompression::No, false, &context);
+        let result4 = interpret(&program, Some(3), TraceCompression::No, false, &context);
+        let result5 = interpret(&program, Some(4), TraceCompression::No, false, &context);
         assert_eq!(result1, InterpreterResult::Unknown);
         assert_eq!(result2, InterpreterResult::Unknown);
         assert_eq!(result3, InterpreterResult::Unknown);
@@ -1507,7 +1679,7 @@ mod tests {
             target.trs.iter().sorted().collect::<Vec<_>>(),
         );
 
-        let output = interpret(&target, None, TraceCompression::No, false);
+        let output = interpret(&target, None, TraceCompression::No, false, &context);
         assert_eq!(output, InterpreterResult::Convergence);
 
         Ok(())
@@ -1520,16 +1692,16 @@ mod tests {
         let mut m = fly::parser::parse(source).unwrap();
         sort_check_and_infer(&mut m).unwrap();
         let universe = std::collections::HashMap::from([("node".to_string(), 2)]);
-        let (target, _) = translate(&m, &universe, false)?;
+        let (target, context) = translate(&m, &universe, false)?;
 
-        let bug = interpret(&target, Some(12), TraceCompression::No, false);
+        let bug = interpret(&target, Some(12), TraceCompression::No, false, &context);
         if let InterpreterResult::Counterexample(trace) = &bug {
             assert_eq!(trace.depth(), 12);
         } else {
             assert!(matches!(bug, InterpreterResult::Counterexample(_)));
         }
 
-        let too_short = interpret(&target, Some(11), TraceCompression::No, false);
+        let too_short = interpret(&target, Some(11), TraceCompression::No, false, &context);
         assert_eq!(too_short, InterpreterResult::Unknown);
 
         Ok(())
@@ -1582,4 +1754,104 @@ assume always forall a:x. ((g'(a) <-> f(a)) & (f'(a) <-> f(a)))
         assert_eq!(1, target.trs.len());
         Ok(())
     }
+
+    #[test]
+    fn checker_set_isostateset_correctness() {
+        let source = "
+sort s
+immutable f(s): bool
+        ";
+        let m = fly::parser::parse(source).unwrap();
+        let universe = std::collections::HashMap::from([("s".to_string(), 2)]);
+        let context = Context::new(&m.signature, &universe);
+        let mut set = IsoStateSet::new(&context);
+
+        assert!(set.insert(&state([0, 0])));
+        assert!(!set.insert(&state([0, 0])));
+        assert!(set.insert(&state([0, 1])));
+        assert!(!set.insert(&state([1, 0])));
+        assert!(set.insert(&state([1, 1])));
+
+        let source = "
+sort a
+sort b
+immutable f(a, b): bool
+        ";
+        let m = fly::parser::parse(source).unwrap();
+        let universe =
+            std::collections::HashMap::from([("a".to_string(), 3), ("b".to_string(), 3)]);
+        let context = Context::new(&m.signature, &universe);
+        let mut set = IsoStateSet::new(&context);
+
+        // b: 0 -> 2, 2 -> 1, 1 -> 0
+        assert!(set.insert(&state([1, 1, 1, 0, 0, 1, 0, 1, 1])));
+        assert!(!set.insert(&state([1, 1, 1, 0, 1, 0, 1, 1, 0])));
+
+        let source = "
+sort s
+sort t
+immutable f(s, t, s): bool
+        ";
+        let m = fly::parser::parse(source).unwrap();
+        let universe =
+            std::collections::HashMap::from([("s".to_string(), 3), ("t".to_string(), 2)]);
+        let context = Context::new(&m.signature, &universe);
+        let mut set = IsoStateSet::new(&context);
+        let state = |vec: Vec<(usize, usize, usize)>| -> BoundedState {
+            let mut out = BoundedState::ZERO;
+            for (x, y, z) in vec {
+                out.set(context.indices[&("f", vec![x, y, z])], true);
+            }
+            out
+        };
+
+        assert!(set.insert(&state(vec![(0, 0, 0)])));
+        assert!(!set.insert(&state(vec![(1, 0, 1)])));
+        assert!(!set.insert(&state(vec![(2, 0, 2)])));
+        assert!(!set.insert(&state(vec![(0, 1, 0)])));
+        assert!(!set.insert(&state(vec![(1, 1, 1)])));
+        assert!(!set.insert(&state(vec![(2, 1, 2)])));
+
+        assert!(set.insert(&state(vec![(1, 0, 0)])));
+        assert!(!set.insert(&state(vec![(1, 0, 0)])));
+        assert!(!set.insert(&state(vec![(2, 0, 0)])));
+        assert!(!set.insert(&state(vec![(1, 1, 0)])));
+        assert!(!set.insert(&state(vec![(0, 1, 1)])));
+
+        assert!(set.insert(&state(vec![(0, 0, 0), (0, 1, 0)])));
+        assert!(!set.insert(&state(vec![(1, 0, 1), (1, 1, 1)])));
+        assert!(set.insert(&state(vec![(0, 0, 1), (0, 1, 0)])));
+        assert!(!set.insert(&state(vec![(1, 0, 0), (1, 1, 1)])));
+        assert!(!set.insert(&state(vec![(0, 1, 1), (0, 0, 0)])));
+
+        let source = "
+sort s
+immutable f(s, bool, s): bool
+        ";
+        let m = fly::parser::parse(source).unwrap();
+        let universe = std::collections::HashMap::from([("s".to_string(), 3)]);
+        let context = Context::new(&m.signature, &universe);
+        let mut set = IsoStateSet::new(&context);
+        let state = |vec: Vec<(usize, usize, usize)>| -> BoundedState {
+            let mut out = BoundedState::ZERO;
+            for (x, y, z) in vec {
+                out.set(context.indices[&("f", vec![x, y, z])], true);
+            }
+            out
+        };
+
+        assert!(set.insert(&state(vec![(0, 0, 0)])));
+        assert!(!set.insert(&state(vec![(1, 0, 1)])));
+        assert!(!set.insert(&state(vec![(2, 0, 2)])));
+        assert!(set.insert(&state(vec![(0, 1, 0)])));
+        assert!(!set.insert(&state(vec![(1, 1, 1)])));
+        assert!(!set.insert(&state(vec![(2, 1, 2)])));
+
+        assert!(set.insert(&state(vec![(1, 0, 0)])));
+        assert!(!set.insert(&state(vec![(1, 0, 0)])));
+        assert!(!set.insert(&state(vec![(2, 0, 0)])));
+
+        assert!(set.insert(&state(vec![(1, 1, 0)])));
+        assert!(!set.insert(&state(vec![(0, 1, 1)])));
+    }
 }

From e549b235fef4ead7042114df10536e92f933c144 Mon Sep 17 00:00:00 2001
From: Alex Fischman <alexdfischman@gmail.com>
Date: Wed, 2 Aug 2023 11:15:12 -0700
Subject: [PATCH 02/10] Copy old canonical IsoStateSet

Signed-off-by: Alex Fischman <alexdfischman@gmail.com>
---
 bounded/src/set.rs | 79 +++++++++-------------------------------------
 1 file changed, 15 insertions(+), 64 deletions(-)

diff --git a/bounded/src/set.rs b/bounded/src/set.rs
index 33d19893..d5f5ee36 100644
--- a/bounded/src/set.rs
+++ b/bounded/src/set.rs
@@ -1213,43 +1213,13 @@ impl<'a> Transitions<'a> {
 struct IsoStateSet {
     set: HashSet<BoundedState>,
     max_index: usize,
-    orderings: Vec<Orderings>,
-}
-
-/// A map, where the index is dst and the value is src, of copies from x[src] to y[dst].
-type Ordering = Vec<usize>;
-/// A branch of a trie of orderings
-struct Orderings {
-    src: usize,
-    children: Vec<Orderings>,
+    orderings: Vec<Vec<(usize, usize)>>,
 }
 
 impl IsoStateSet {
     fn new(context: &Context) -> IsoStateSet {
-        fn from_ordering(ordering: &[usize]) -> Vec<Orderings> {
-            match &ordering {
-                [] => vec![],
-                [first, rest @ ..] => vec![Orderings {
-                    src: *first,
-                    children: from_ordering(rest).into_iter().collect(),
-                }],
-            }
-        }
-        fn add_ordering(ordering: &[usize], orderings: &mut Vec<Orderings>) {
-            if ordering.is_empty() || orderings.is_empty() {
-                assert!(
-                    ordering.is_empty() && orderings.is_empty(),
-                    "orderings had different lengths"
-                )
-            }
-            match orderings.iter_mut().find(|o| o.src == ordering[0]) {
-                Some(o) => add_ordering(&ordering[1..], &mut o.children),
-                None => orderings.extend(from_ordering(ordering)),
-            }
-        }
-
         let sorts: Vec<_> = context.universe.keys().sorted().collect();
-        let mut iter = sorts
+        let orderings = sorts
             .iter()
             .map(|sort| context.universe[sort.as_str()])
             // the permutations are maps from old to new element values
@@ -1281,16 +1251,10 @@ impl IsoStateSet {
                         // look up the index to precompute the dst
                         (context.indices[&(relation.name.as_str(), new_elements)], *i)
                     })
-                    .sorted()
-                    .map(|(_, v)| v)
+                    .filter(|(src, dst)| src != dst)
                     .collect()
-            });
-
-        let first: Ordering = iter.next().unwrap();
-        let mut orderings = from_ordering(&first);
-        for ordering in iter {
-            add_ordering(&ordering, orderings.as_mut());
-        }
+            })
+            .collect();
 
         IsoStateSet {
             set: Default::default(),
@@ -1308,31 +1272,18 @@ impl IsoStateSet {
     }
 
     fn insert(&mut self, x: &BoundedState) -> bool {
-        self.set.insert(self.canonicalize(x))
-    }
-
-    fn canonicalize(&self, x: &BoundedState) -> BoundedState {
-        let mut orderings: Vec<&Orderings> = self.orderings.iter().collect();
-        let mut y = BoundedState::ZERO;
-        for i in 0..=self.max_index {
-            if i == self.max_index {
-                assert!(orderings.iter().all(|o| o.children.is_empty()));
-            }
-
-            let mut subset: Vec<_> = orderings
-                .iter()
-                .filter(|o| !x.get(o.src))
-                .copied()
-                .collect();
-
-            if subset.is_empty() {
-                y.set(i, true);
-                subset = orderings;
+        if self.set.contains(x) {
+            false
+        } else {
+            for ordering in &self.orderings {
+                let mut y = x.clone();
+                for (src, dst) in ordering {
+                    y.set(*dst, x.get(*src));
+                }
+                self.set.insert(y);
             }
-
-            orderings = subset.into_iter().flat_map(|o| &o.children).collect();
+            true
         }
-        y
     }
 }
 

From 2cb6cf87fe2a93b5c866b5b0880535934d9ab559 Mon Sep 17 00:00:00 2001
From: Alex Fischman <alexdfischman@gmail.com>
Date: Wed, 2 Aug 2023 11:18:13 -0700
Subject: [PATCH 03/10] Finish add-all version, start testing

Signed-off-by: Alex Fischman <alexdfischman@gmail.com>
---
 bounded/src/set.rs | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/bounded/src/set.rs b/bounded/src/set.rs
index d5f5ee36..1a87ef29 100644
--- a/bounded/src/set.rs
+++ b/bounded/src/set.rs
@@ -1212,7 +1212,6 @@ impl<'a> Transitions<'a> {
 /// Can answer the question "have I seen a state that is isomorphic to this one before"?
 struct IsoStateSet {
     set: HashSet<BoundedState>,
-    max_index: usize,
     orderings: Vec<Vec<(usize, usize)>>,
 }
 
@@ -1257,8 +1256,7 @@ impl IsoStateSet {
             .collect();
 
         IsoStateSet {
-            set: Default::default(),
-            max_index: *context.indices.values().max().unwrap(),
+            set: HashSet::default(),
             orderings,
         }
     }
@@ -1276,7 +1274,7 @@ impl IsoStateSet {
             false
         } else {
             for ordering in &self.orderings {
-                let mut y = x.clone();
+                let mut y = *x;
                 for (src, dst) in ordering {
                     y.set(*dst, x.get(*src));
                 }

From e5afe7fead0c79d0873226f57618edb1b9c26d3e Mon Sep 17 00:00:00 2001
From: Alex Fischman <alexdfischman@gmail.com>
Date: Wed, 2 Aug 2023 11:28:02 -0700
Subject: [PATCH 04/10] Remove print statement

Signed-off-by: Alex Fischman <alexdfischman@gmail.com>
---
 bounded/src/set.rs | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/bounded/src/set.rs b/bounded/src/set.rs
index 1a87ef29..60ff5227 100644
--- a/bounded/src/set.rs
+++ b/bounded/src/set.rs
@@ -1123,15 +1123,6 @@ fn interpret(
                     .iter()
                     .for_each(|update| next.set(update.index, update.formula.evaluate(state)));
                 if seen.insert(&next) {
-                    if seen.len() % 1_000_000 == 0 {
-                        let elapsed = start_time.elapsed().as_secs_f64();
-                        println!(
-                            "progress report: ({elapsed:0.1}s since start) considering depth {current_depth}. \
-                             queue length is {}. visited {} states.",
-                            queue.len(),
-                            seen.len()
-                        );
-                    }
                     let mut trace = trace.clone();
                     trace.push(next);
                     queue.push_back(trace);

From 8d59153c4841f96605876e1e1859bb51a5953399 Mon Sep 17 00:00:00 2001
From: Alex Fischman <alexdfischman@gmail.com>
Date: Wed, 2 Aug 2023 12:02:23 -0700
Subject: [PATCH 05/10] Use bitvec again for slight release mode speedup

Signed-off-by: Alex Fischman <alexdfischman@gmail.com>
---
 Cargo.lock         | 40 ++++++++++++++++++++++++++++++++++++++++
 bounded/Cargo.toml |  1 +
 bounded/src/set.rs | 46 +++++++++++++++++++++-------------------------
 3 files changed, 62 insertions(+), 25 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index 7375530a..453eaa3c 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -104,6 +104,18 @@ dependencies = [
  "typenum",
 ]
 
+[[package]]
+name = "bitvec"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1bc2832c24239b0141d5674bb9174f9d68a8b5b3f2753311927c172ca46f7e9c"
+dependencies = [
+ "funty",
+ "radium",
+ "tap",
+ "wyz",
+]
+
 [[package]]
 name = "block-buffer"
 version = "0.10.4"
@@ -118,6 +130,7 @@ name = "bounded"
 version = "0.1.0"
 dependencies = [
  "biodivine-lib-bdd",
+ "bitvec",
  "cadical",
  "fly",
  "fxhash",
@@ -460,6 +473,12 @@ dependencies = [
  "thiserror",
 ]
 
+[[package]]
+name = "funty"
+version = "2.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6d5a32815ae3f33302d95fdcb2ce17862f8c65363dcfd29360480ba1001fc9c"
+
 [[package]]
 name = "fxhash"
 version = "0.2.1"
@@ -895,6 +914,12 @@ dependencies = [
  "proc-macro2",
 ]
 
+[[package]]
+name = "radium"
+version = "0.7.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dc33ff2d4973d518d823d61aa239014831e521c75da58e3df4840d3f47749d09"
+
 [[package]]
 name = "rand"
 version = "0.8.5"
@@ -1156,6 +1181,12 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "tap"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "55937e1799185b12863d447f42597ed69d9928686b8d88a1df17376a097d8369"
+
 [[package]]
 name = "temporal-verifier"
 version = "0.1.0"
@@ -1568,6 +1599,15 @@ dependencies = [
  "memchr",
 ]
 
+[[package]]
+name = "wyz"
+version = "0.5.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "05f360fc0b24296329c78fda852a1e9ae82de9cf7b27dae4b7f62f118f77b9ed"
+dependencies = [
+ "tap",
+]
+
 [[package]]
 name = "yaml-rust"
 version = "0.4.5"
diff --git a/bounded/Cargo.toml b/bounded/Cargo.toml
index ae42d4fa..7410b0a8 100644
--- a/bounded/Cargo.toml
+++ b/bounded/Cargo.toml
@@ -12,3 +12,4 @@ thiserror = "1.0.40"
 biodivine-lib-bdd = "0.5.1"
 cadical = "0.1.14"
 fxhash = "0.2.1"
+bitvec = "1.0.1"
diff --git a/bounded/src/set.rs b/bounded/src/set.rs
index 60ff5227..0bbac83a 100644
--- a/bounded/src/set.rs
+++ b/bounded/src/set.rs
@@ -4,6 +4,7 @@
 //! A bounded model checker for flyvy programs. Use `translate` to turn a flyvy `Module`
 //! into a `BoundedProgram`, then use `interpret` to evaluate it.
 
+use bitvec::prelude::*;
 use fly::{ouritertools::OurItertools, semantics::*, syntax::*, transitions::*};
 use itertools::Itertools;
 use std::collections::VecDeque;
@@ -157,38 +158,39 @@ impl Context<'_> {
 
 /// Compile-time upper bound on the bounded universe size.
 const STATE_LEN: usize = 128;
-type StateData = u8;
-const STATE_DATA_BITS: usize = std::mem::size_of::<StateData>() * 8;
 
 /// A state in the bounded system. Conceptually, this is an interpretation of the signature on the
 /// bounded universe. We represent states concretely as a bitvector, where each bit represents the
 /// presence of a tuple in a relation. The order of the bits is determined by [Context].
-#[derive(Clone, Copy, PartialEq, Eq, Hash, PartialOrd)]
-struct BoundedState([StateData; STATE_LEN / STATE_DATA_BITS]);
+#[derive(Clone, Copy, Eq, PartialOrd)]
+struct BoundedState(BitArr!(for STATE_LEN));
+
+// Go word by word instead of bit by bit.
+impl std::hash::Hash for BoundedState {
+    fn hash<H>(&self, h: &mut H)
+    where
+        H: std::hash::Hasher,
+    {
+        self.0.as_raw_slice().hash(h)
+    }
+}
+impl PartialEq for BoundedState {
+    fn eq(&self, other: &BoundedState) -> bool {
+        self.0.as_raw_slice().eq(other.0.as_raw_slice())
+    }
+}
 
 impl BoundedState {
-    const ZERO: BoundedState = BoundedState([0; STATE_LEN / STATE_DATA_BITS]);
+    const ZERO: BoundedState = BoundedState(BitArray::ZERO);
 
     fn get(&self, index: usize) -> bool {
         assert!(index < STATE_LEN, "STATE_LEN is too small");
-        let idx = index / STATE_DATA_BITS;
-        // `STATE_DATA_BITS - 1 - ` fixes ordering
-        let bit = STATE_DATA_BITS - 1 - (index % STATE_DATA_BITS);
-
-        ((self.0[idx] >> bit) & 1) != 0
+        self.0[index]
     }
 
     fn set(&mut self, index: usize, value: bool) {
         assert!(index < STATE_LEN, "STATE_LEN is too small");
-        let idx = index / STATE_DATA_BITS;
-        // `STATE_DATA_BITS - 1 - ` fixes ordering
-        let bit = STATE_DATA_BITS - 1 - (index % STATE_DATA_BITS);
-
-        if value {
-            self.0[idx] |= 1 << bit;
-        } else {
-            self.0[idx] &= !(1 << bit);
-        }
+        self.0.set(index, value);
     }
 }
 
@@ -1345,12 +1347,6 @@ mod tests {
         assert!(!s.get(2));
         assert!(!s.get(3));
 
-        let mut a = BoundedState::ZERO;
-        let mut b = BoundedState::ZERO;
-        a.0[1] = 1; // [0, 1, 0, 0, ...]
-        b.0[0] = 1; // [1, 0, 0, 0, ...]
-        assert!(a < b);
-
         assert!(state([0]) < state([1]));
         assert!(state([0, 1, 0, 1]) < state([1, 0, 1, 0]));
         assert!(state([0, 1, 0, 0]) < state([0, 1, 0, 1]));

From f0dc0ee121029bf7a4d93bdceb3d7bf84678225e Mon Sep 17 00:00:00 2001
From: Alex Fischman <alexdfischman@gmail.com>
Date: Wed, 2 Aug 2023 12:41:03 -0700
Subject: [PATCH 06/10] Reduce IsoStateSet API

Signed-off-by: Alex Fischman <alexdfischman@gmail.com>
---
 bounded/src/set.rs | 15 ++++-----------
 1 file changed, 4 insertions(+), 11 deletions(-)

diff --git a/bounded/src/set.rs b/bounded/src/set.rs
index 0bbac83a..a4ae08e3 100644
--- a/bounded/src/set.rs
+++ b/bounded/src/set.rs
@@ -1079,8 +1079,9 @@ fn interpret(
 
     // The BFS queue, i.e., states on the frontier that need to be explored.
     // The queue is always a subset of seen.
-    let mut queue: VecDeque<Trace> = seen
-        .states()
+    let mut queue: VecDeque<Trace> = program
+        .inits
+        .iter()
         .map(|state| Trace::new(*state, compress_traces))
         .collect();
 
@@ -1107,7 +1108,7 @@ fn interpret(
                 "considering new depth: {current_depth}. \
                  queue length is {}. seen {} unique states.",
                 queue.len(),
-                seen.len()
+                seen.set.len()
             );
         }
 
@@ -1254,14 +1255,6 @@ impl IsoStateSet {
         }
     }
 
-    fn len(&self) -> usize {
-        self.set.len()
-    }
-
-    fn states(&self) -> impl Iterator<Item = &BoundedState> {
-        self.set.iter()
-    }
-
     fn insert(&mut self, x: &BoundedState) -> bool {
         if self.set.contains(x) {
             false

From ffa4613c8f4efaca0f16d67f8d3433fe8e17ae2a Mon Sep 17 00:00:00 2001
From: Alex Fischman <alexdfischman@gmail.com>
Date: Wed, 2 Aug 2023 13:43:44 -0700
Subject: [PATCH 07/10] Swap ordering order to match insert()

Signed-off-by: Alex Fischman <alexdfischman@gmail.com>
---
 bounded/src/set.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/bounded/src/set.rs b/bounded/src/set.rs
index a4ae08e3..9803c369 100644
--- a/bounded/src/set.rs
+++ b/bounded/src/set.rs
@@ -1242,7 +1242,7 @@ impl IsoStateSet {
                             };
                         }
                         // look up the index to precompute the dst
-                        (context.indices[&(relation.name.as_str(), new_elements)], *i)
+                        (*i, context.indices[&(relation.name.as_str(), new_elements)])
                     })
                     .filter(|(src, dst)| src != dst)
                     .collect()

From fa6ae1043ecbae44ec8d7751868d0baea7222019 Mon Sep 17 00:00:00 2001
From: Alex Fischman <alexdfischman@gmail.com>
Date: Sun, 6 Aug 2023 10:53:36 -0700
Subject: [PATCH 08/10] Fix queue length printing

Signed-off-by: Alex Fischman <alexdfischman@gmail.com>
---
 bounded/src/set.rs                            |  2 +-
 .../snapshots/lockserver_buggy.fly.2.snap     | 24 +++++++++----------
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/bounded/src/set.rs b/bounded/src/set.rs
index 9803c369..cb8fbf5a 100644
--- a/bounded/src/set.rs
+++ b/bounded/src/set.rs
@@ -1107,7 +1107,7 @@ fn interpret(
             println!(
                 "considering new depth: {current_depth}. \
                  queue length is {}. seen {} unique states.",
-                queue.len(),
+                queue.len() + 1, // include current state
                 seen.set.len()
             );
         }
diff --git a/temporal-verifier/tests/examples/snapshots/lockserver_buggy.fly.2.snap b/temporal-verifier/tests/examples/snapshots/lockserver_buggy.fly.2.snap
index 3151360e..36261e8b 100644
--- a/temporal-verifier/tests/examples/snapshots/lockserver_buggy.fly.2.snap
+++ b/temporal-verifier/tests/examples/snapshots/lockserver_buggy.fly.2.snap
@@ -7,18 +7,18 @@ starting translation...
 enumerating 1 initial states
 enumerating 15 transitions
 starting search from depth 0. there are 1 initial states in the queue.
-considering new depth: 1. queue length is 2. seen 4 unique states.
-considering new depth: 2. queue length is 5. seen 10 unique states.
-considering new depth: 3. queue length is 12. seen 23 unique states.
-considering new depth: 4. queue length is 20. seen 44 unique states.
-considering new depth: 5. queue length is 23. seen 68 unique states.
-considering new depth: 6. queue length is 20. seen 89 unique states.
-considering new depth: 7. queue length is 20. seen 110 unique states.
-considering new depth: 8. queue length is 47. seen 158 unique states.
-considering new depth: 9. queue length is 92. seen 251 unique states.
-considering new depth: 10. queue length is 110. seen 362 unique states.
-considering new depth: 11. queue length is 125. seen 488 unique states.
-considering new depth: 12. queue length is 200. seen 689 unique states.
+considering new depth: 1. queue length is 1. seen 4 unique states.
+considering new depth: 2. queue length is 2. seen 10 unique states.
+considering new depth: 3. queue length is 4. seen 23 unique states.
+considering new depth: 4. queue length is 5. seen 44 unique states.
+considering new depth: 5. queue length is 6. seen 68 unique states.
+considering new depth: 6. queue length is 5. seen 89 unique states.
+considering new depth: 7. queue length is 5. seen 110 unique states.
+considering new depth: 8. queue length is 10. seen 158 unique states.
+considering new depth: 9. queue length is 18. seen 251 unique states.
+considering new depth: 10. queue length is 22. seen 362 unique states.
+considering new depth: 11. queue length is 25. seen 488 unique states.
+considering new depth: 12. queue length is 38. seen 689 unique states.
 found counterexample:
 state 0:
 lock_msg(@node_0) = false

From 26f23cd5a5ed25408611b2481fcd2e1fddd078af Mon Sep 17 00:00:00 2001
From: Alex Fischman <alexdfischman@gmail.com>
Date: Mon, 7 Aug 2023 10:57:31 -0700
Subject: [PATCH 09/10] Do symmetry breaking on initital states as well

Signed-off-by: Alex Fischman <alexdfischman@gmail.com>
---
 bounded/src/set.rs | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

diff --git a/bounded/src/set.rs b/bounded/src/set.rs
index cb8fbf5a..9feb16e5 100644
--- a/bounded/src/set.rs
+++ b/bounded/src/set.rs
@@ -1073,17 +1073,15 @@ fn interpret(
 ) -> InterpreterResult {
     // States we have seen so far.
     let mut seen = IsoStateSet::new(context);
-    for init in &program.inits {
-        seen.insert(init);
-    }
-
     // The BFS queue, i.e., states on the frontier that need to be explored.
     // The queue is always a subset of seen.
-    let mut queue: VecDeque<Trace> = program
-        .inits
-        .iter()
-        .map(|state| Trace::new(*state, compress_traces))
-        .collect();
+    let mut queue: VecDeque<Trace> = VecDeque::new();
+
+    for init in &program.inits {
+        if seen.insert(init) {
+            queue.push_back(Trace::new(*init, compress_traces));
+        }
+    }
 
     let mut transitions = Transitions::new();
     for tr in &program.trs {

From 4ea5960bf00e7b40882497f2856de805c7312e49 Mon Sep 17 00:00:00 2001
From: Alex Fischman <alexdfischman@gmail.com>
Date: Mon, 7 Aug 2023 12:30:06 -0700
Subject: [PATCH 10/10] Implement fingerprinting instead of add-all algorithm

Signed-off-by: Alex Fischman <alexdfischman@gmail.com>
---
 bounded/src/set.rs | 276 ++++++++++++++++++++++++++++++++++++---------
 1 file changed, 222 insertions(+), 54 deletions(-)

diff --git a/bounded/src/set.rs b/bounded/src/set.rs
index 9feb16e5..da45341e 100644
--- a/bounded/src/set.rs
+++ b/bounded/src/set.rs
@@ -1106,7 +1106,7 @@ fn interpret(
                 "considering new depth: {current_depth}. \
                  queue length is {}. seen {} unique states.",
                 queue.len() + 1, // include current state
-                seen.set.len()
+                seen.len()
             );
         }
 
@@ -1202,73 +1202,241 @@ impl<'a> Transitions<'a> {
 }
 
 /// Can answer the question "have I seen a state that is isomorphic to this one before"?
-struct IsoStateSet {
-    set: HashSet<BoundedState>,
-    orderings: Vec<Vec<(usize, usize)>>,
+struct IsoStateSet<'a> {
+    context: &'a Context<'a>,
+    data: HashMap<Fingerprint, Vec<(BoundedState, Partition)>>,
 }
 
-impl IsoStateSet {
-    fn new(context: &Context) -> IsoStateSet {
-        let sorts: Vec<_> = context.universe.keys().sorted().collect();
-        let orderings = sorts
-            .iter()
-            .map(|sort| context.universe[sort.as_str()])
-            // the permutations are maps from old to new element values
-            .map(|size| (0..size).permutations(size))
-            // get all combinations of different ways to permute values
-            .multi_cartesian_product_fixed()
-            // reattach sort names onto each ordering
-            .map(|ordering| {
-                assert_eq!(sorts.len(), ordering.len());
-                sorts.iter().map(|s| s.as_str()).zip(ordering).collect()
-            })
-            // convert permutations to copy instructions
-            .map(|permutation: HashMap<&str, Vec<usize>>| {
-                context
-                    .indices
-                    .iter()
-                    .map(|((name, elements), i)| {
-                        let relation = context.signature.relation_decl(name);
-                        assert_eq!(relation.args.len(), elements.len());
-                        // map each old element to a new element
-                        let mut new_elements = elements.clone();
-                        for i in 0..new_elements.len() {
-                            let x = elements[i];
-                            new_elements[i] = match &relation.args[i] {
-                                Sort::Uninterpreted(s) => permutation[s.as_str()][x],
-                                Sort::Bool => x,
-                            };
-                        }
-                        // look up the index to precompute the dst
-                        (*i, context.indices[&(relation.name.as_str(), new_elements)])
-                    })
-                    .filter(|(src, dst)| src != dst)
-                    .collect()
-            })
-            .collect();
-
+impl<'a> IsoStateSet<'a> {
+    fn new(context: &'a Context) -> IsoStateSet<'a> {
         IsoStateSet {
-            set: HashSet::default(),
-            orderings,
+            context,
+            data: Default::default(),
         }
     }
 
+    fn len(&self) -> usize {
+        self.data.values().map(Vec::len).sum()
+    }
+
+    // true if insertion was successful
+    // false if element was already present
     fn insert(&mut self, x: &BoundedState) -> bool {
-        if self.set.contains(x) {
-            false
+        let (fingerprint, xp) = self.fingerprint(x);
+        if let Some(vec) = self.data.get_mut(&fingerprint) {
+            if vec
+                .iter()
+                .any(|(y, yp)| is_isomorphic(self.context, x, &xp, y, yp))
+            {
+                false
+            } else {
+                vec.push((*x, xp));
+                true
+            }
         } else {
-            for ordering in &self.orderings {
-                let mut y = *x;
-                for (src, dst) in ordering {
-                    y.set(*dst, x.get(*src));
+            self.data.insert(fingerprint.clone(), vec![(*x, xp)]);
+            true
+        }
+    }
+
+    fn fingerprint(&self, state: &BoundedState) -> (Fingerprint, Partition) {
+        let mut previous: HashMap<(&str, usize), usize> = self
+            .context
+            .signature
+            .sorts
+            .iter()
+            .enumerate()
+            .flat_map(|(i, s)| (0..self.context.universe[s]).map(move |e| ((s.as_str(), e), i)))
+            .collect();
+
+        for _ in 0..self.context.universe.values().sum() {
+            use std::collections::BTreeMap;
+            let mut current: HashMap<(&str, usize), BTreeMap<(&str, usize, Vec<Label>), usize>> =
+                previous.keys().map(|k| (*k, Default::default())).collect();
+
+            for ((name, elements), index) in &self.context.indices {
+                if state.get(*index) {
+                    let relation = self.context.signature.relation_decl(name);
+
+                    let labels: Vec<_> = (0..elements.len())
+                        .map(|i| match (&relation.args[i], elements[i]) {
+                            (Sort::Bool, 0) => Label::False,
+                            (Sort::Bool, 1) => Label::True,
+                            (Sort::Bool, _) => unreachable!(),
+                            (Sort::Uninterpreted(s), e) => Label::Other(previous[&(s.as_str(), e)]),
+                        })
+                        .collect();
+
+                    for (i, element) in elements.iter().enumerate() {
+                        if let Sort::Uninterpreted(s) = &relation.args[i] {
+                            *current
+                                .get_mut(&(s, *element))
+                                .unwrap()
+                                .entry((*name, i, labels.clone()))
+                                .or_insert(0) += 1;
+                        }
+                    }
                 }
-                self.set.insert(y);
             }
-            true
+
+            let values_to_indices: HashMap<_, usize> = current
+                .values()
+                .cloned()
+                .sorted()
+                .unique()
+                .enumerate()
+                .map(|(i, x)| (x, i))
+                .collect();
+
+            previous = current
+                .into_iter()
+                .map(|(k, v)| (k, values_to_indices[&v]))
+                .collect();
         }
+
+        let fingerprint: Vec<_> = previous
+            .iter()
+            .map(|((k, _), v)| (k.to_string(), *v))
+            .sorted()
+            .collect();
+
+        let mut classes: HashMap<&str, HashMap<usize, Vec<usize>>> = Default::default();
+        for ((s, e), l) in &previous {
+            classes
+                .entry(s)
+                .or_default()
+                .entry(*l)
+                .or_default()
+                .push(*e);
+        }
+
+        let partition: HashMap<_, Vec<_>> = classes
+            .into_iter()
+            .map(|(k, v)| {
+                (
+                    k.to_string(),
+                    v.into_iter().sorted().map(|(_, v)| v).collect(),
+                )
+            })
+            .collect();
+
+        (fingerprint, partition)
     }
 }
 
+type Fingerprint = Vec<(String, usize)>;
+type Partition = HashMap<String, Vec<Vec<usize>>>;
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
+enum Label {
+    True,
+    False,
+    Other(usize),
+}
+
+fn is_isomorphic(
+    context: &Context,
+    x: &BoundedState,
+    px: &Partition,
+    y: &BoundedState,
+    py: &Partition,
+) -> bool {
+    if x == y {
+        return true;
+    }
+
+    assert_eq!(px.len(), py.len());
+
+    let permutations: Vec<Vec<Vec<usize>>> = px
+        .iter()
+        .sorted()
+        .zip(py.iter().sorted())
+        // the permutations are maps from old to new element values
+        .map(|((sx, vx), (sy, vy))| {
+            assert_eq!(sx, sy);
+            vx.iter()
+                .cloned()
+                .map(|v| {
+                    let l = v.len();
+                    v.into_iter().permutations(l)
+                })
+                .multi_cartesian_product_fixed()
+                .map(|permutation| {
+                    let mut func = vec![0; context.universe[sx]];
+                    assert_eq!(
+                        permutation.iter().map(|v| v.len()).sum::<usize>(),
+                        vy.iter().map(|v| v.len()).sum::<usize>()
+                    );
+                    assert_eq!(permutation.len(), vy.len());
+                    permutation
+                        .iter()
+                        .flatten()
+                        .zip(vy.iter().flatten())
+                        .for_each(|(ax, ay)| func[*ax] = *ay);
+                    func
+                })
+                .collect()
+        })
+        .collect();
+
+    let orderings: Vec<Vec<(usize, usize)>> = permutations
+        .into_iter()
+        // get all combinations of different ways to permute values
+        .multi_cartesian_product_fixed()
+        // reattach sort names onto each ordering
+        .map(|ordering| {
+            assert_eq!(context.signature.sorts.len(), ordering.len());
+            context
+                .signature
+                .sorts
+                .iter()
+                .map(|s| s.as_str())
+                .zip(ordering)
+                .collect()
+        })
+        // convert permutations to copy instructions
+        .map(|permutation: HashMap<&str, Vec<usize>>| {
+            context
+                .indices
+                .iter()
+                .map(|((name, elements), i)| {
+                    let relation = context.signature.relation_decl(name);
+                    assert_eq!(relation.args.len(), elements.len());
+                    // map each old element to a new element
+                    let mut new_elements = elements.clone();
+                    for i in 0..new_elements.len() {
+                        let x = elements[i];
+                        new_elements[i] = match &relation.args[i] {
+                            Sort::Uninterpreted(s) => permutation[s.as_str()][x],
+                            Sort::Bool => x,
+                        };
+                    }
+                    // look up the index to precompute the dst index
+                    (*i, context.indices[&(relation.name.as_str(), new_elements)])
+                })
+                .filter(|(i, j)| i != j)
+                .collect()
+        })
+        .collect();
+
+    'outer: for ordering in &orderings {
+        let mut new_state = *x;
+        for (src, dst) in ordering {
+            let x_bit = x.get(*src);
+            let y_bit = y.get(*dst);
+            if x_bit != y_bit {
+                continue 'outer;
+            }
+            new_state.set(*dst, x_bit);
+        }
+        if new_state == *y {
+            return true;
+        }
+    }
+
+    false
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;