From be302eb99a4dedda301ea013915920f4910e5829 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Luk=C3=A1=C5=A1=20Chud=C3=AD=C4=8Dek?= <xchudic1@fi.muni.cz>
Date: Tue, 12 Dec 2023 15:55:11 +0100
Subject: [PATCH] refactor: gray encoding SymbolicDomainOrd impl

---
 src/symbolic_domains/symbolic_domain.rs | 28 +++++++++++++++++++++++++
 tests/some_test.rs                      |  4 ++--
 2 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/src/symbolic_domains/symbolic_domain.rs b/src/symbolic_domains/symbolic_domain.rs
index a8f8f96..03ecbfe 100644
--- a/src/symbolic_domains/symbolic_domain.rs
+++ b/src/symbolic_domains/symbolic_domain.rs
@@ -557,3 +557,31 @@ impl SymbolicDomain<u8> for GrayCodeIntegerDomain<u8> {
         res
     }
 }
+
+impl SymbolicDomainOrd<u8> for GrayCodeIntegerDomain<u8> {
+    fn new(builder: &mut BddVariableSetBuilder, name: &str, max_value: &u8) -> Self {
+        let bit_count = 8 - max_value.leading_zeros();
+
+        let variables = (0..bit_count)
+            .map(|it| {
+                let name = format!("{name}_v{}", it + 1);
+                builder.make_variable(name.as_str())
+            })
+            .collect();
+
+        Self {
+            variables,
+            max_value: *max_value,
+        }
+    }
+
+    fn encode_lt(&self, bdd_variable_set: &BddVariableSet, exclusive_upper_bound: &u8) -> Bdd {
+        (0..*exclusive_upper_bound).fold(self.empty_collection(bdd_variable_set), |acc, val| {
+            acc.or(&self.encode_one(bdd_variable_set, &val))
+        })
+    }
+
+    fn cmp(lhs: &u8, rhs: &u8) -> std::cmp::Ordering {
+        lhs.cmp(rhs)
+    }
+}
diff --git a/tests/some_test.rs b/tests/some_test.rs
index b252a1a..7fc7cab 100644
--- a/tests/some_test.rs
+++ b/tests/some_test.rs
@@ -3,8 +3,8 @@
 use biodivine_lib_bdd::Bdd;
 use biodivine_lib_logical_models::prelude as bio;
 
-type OldDomain = bio::old_symbolic_domain::BinaryIntegerDomain<u8>;
-type NewDomain = bio::symbolic_domain::BinaryIntegerDomain<u8>;
+type OldDomain = bio::old_symbolic_domain::GrayCodeIntegerDomain<u8>;
+type NewDomain = bio::symbolic_domain::GrayCodeIntegerDomain<u8>;
 
 struct TheFourImpls<D, OD>
 where