refactor: binary & gray encoding

src/symbolic_domains/symbolic_domain.rs

@@ -1,7 +1,7 @@
 use std::collections::HashSet;
 
 use biodivine_lib_bdd::{
-    Bdd, BddPartialValuation, BddVariable, BddVariableSet, BddVariableSetBuilder,
+    Bdd, BddPartialValuation, BddValuation, BddVariable, BddVariableSet, BddVariableSetBuilder,
 };
 
 pub trait SymbolicDomain<T> {
@@ -132,7 +132,7 @@ pub trait SymbolicDomain<T> {
 pub trait SymbolicDomainOrd<T>: SymbolicDomain<T> {
     fn new(builder: &mut BddVariableSetBuilder, name: &str, max_value: &T) -> Self;
     /// Encodes the set of values that are strictly less than the given value.
-    fn encode_lt(&self, bdd_variable_set: &BddVariableSet, value: &T) -> Bdd;
+    fn encode_lt(&self, bdd_variable_set: &BddVariableSet, exclusive_upper_bound: &T) -> Bdd;
     /// Encodes the set of values that are less than or equal to the given value.
     fn encode_le(&self, bdd_variable_set: &BddVariableSet, value: &T) -> Bdd {
         self.encode_lt(bdd_variable_set, value)
@@ -354,3 +354,206 @@ impl SymbolicDomainOrd<u8> for PetriNetIntegerDomain {
         lhs.cmp(rhs)
     }
 }
+
+pub struct BinaryIntegerDomain<T> {
+    /// invariant: sorted
+    variables: Vec<BddVariable>,
+    /// in older implementations, this used to be the `max_value`
+    /// since we no longer require ordering, no `max_value` -> Bdd of all the possible values
+    max_value: T, // todo mb, cannot implemnent BinaryIntegerDomain generically -> it must be SymbolicDomainOrd
+}
+
+impl SymbolicDomain<u8> for BinaryIntegerDomain<u8> {
+    fn encode_bits(&self, bdd_valuation: &mut BddPartialValuation, value: &u8) {
+        if value > &(self.max_value) {
+            // this breaks the idea of SymbolicDomain being not bound to the ordering
+            let vars = self
+                .variables
+                .iter()
+                .map(|var| format!("{:?}", var))
+                .collect::<Vec<_>>()
+                .join(", ");
+
+            panic!(
+                "Value is too big for domain {}; value: {}, domain size: {}",
+                vars, value, self.max_value
+            )
+        }
+
+        self.variables.iter().enumerate().for_each(|(idx, var)| {
+            bdd_valuation.set_value(*var, (value & (1 << idx)) != 0);
+        })
+    }
+
+    fn empty_collection(&self, bdd_variable_set: &BddVariableSet) -> Bdd {
+        bdd_variable_set.mk_false()
+    }
+
+    fn unit_collection(&self, bdd_variable_set: &BddVariableSet) -> Bdd {
+        (0..self.max_value).fold(bdd_variable_set.mk_false(), |acc, val| {
+            acc.or(&self.encode_one(bdd_variable_set, &val))
+        })
+    }
+
+    fn raw_bdd_variables(&self) -> Vec<BddVariable> {
+        self.variables.clone() // already sorted
+    }
+
+    fn raw_bdd_variables_unsorted(&self) -> Vec<BddVariable> {
+        self.raw_bdd_variables() // already the optimal performance
+    }
+
+    fn decode_bits(&self, bdd_valuation: &BddPartialValuation) -> u8 {
+        let res = self
+            .variables
+            .iter()
+            .enumerate()
+            .fold(0, |acc, (idx, var)| {
+                let bit = if bdd_valuation
+                    .get_value(*var)
+                    .expect("bits of the value should be in the valuation")
+                {
+                    1
+                } else {
+                    0
+                };
+
+                acc | (bit << idx)
+            });
+
+        if res > self.max_value {
+            panic!(
+                "invalid encoding; should not contain value greater than {}, but contains {}",
+                self.max_value, res
+            )
+        }
+
+        res
+    }
+}
+
+impl SymbolicDomainOrd<u8> for BinaryIntegerDomain<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)
+    }
+}
+
+pub struct GrayCodeIntegerDomain<T> {
+    /// invariant: sorted
+    variables: Vec<BddVariable>,
+    /// in older implementations, this used to be the `max_value`
+    /// since we no longer require ordering, no `max_value` -> Bdd of all the possible values
+    max_value: T, // todo same as in the case of BinaryIntegerDomain
+}
+
+impl GrayCodeIntegerDomain<u8> {
+    fn binary_to_gray_code(n: u8) -> u8 {
+        // magic
+        n ^ (n >> 1)
+    }
+
+    fn gray_code_to_binary(n: u8) -> u8 {
+        // magic II
+        let mut n = n;
+        let mut mask = n >> 1;
+        while mask != 0 {
+            n ^= mask;
+            mask >>= 1;
+        }
+        n
+    }
+}
+
+impl SymbolicDomain<u8> for GrayCodeIntegerDomain<u8> {
+    fn encode_bits(&self, bdd_valuation: &mut BddPartialValuation, value: &u8) {
+        if value > &(self.max_value) {
+            // this breaks the idea of SymbolicDomain being not bound to the ordering
+            let vars = self
+                .variables
+                .iter()
+                .map(|var| format!("{:?}", var))
+                .collect::<Vec<_>>()
+                .join(", ");
+
+            panic!(
+                "Value is too big for domain {}; value: {}, domain size: {}",
+                vars, value, self.max_value
+            )
+        }
+
+        let gray_code = Self::binary_to_gray_code(*value);
+        self.variables.iter().enumerate().for_each(|(idx, var)| {
+            bdd_valuation.set_value(*var, (gray_code & (1 << idx)) != 0);
+        })
+    }
+
+    fn empty_collection(&self, bdd_variable_set: &BddVariableSet) -> Bdd {
+        bdd_variable_set.mk_false()
+    }
+
+    fn unit_collection(&self, bdd_variable_set: &BddVariableSet) -> Bdd {
+        (0..self.max_value).fold(bdd_variable_set.mk_false(), |acc, val| {
+            acc.or(&self.encode_one(bdd_variable_set, &val))
+        })
+    }
+
+    fn raw_bdd_variables(&self) -> Vec<BddVariable> {
+        self.variables.clone() // already sorted
+    }
+
+    fn raw_bdd_variables_unsorted(&self) -> Vec<BddVariable> {
+        self.raw_bdd_variables() // already the optimal performance
+    }
+
+    fn decode_bits(&self, bdd_valuation: &BddPartialValuation) -> u8 {
+        let read_gray_code = self
+            .variables
+            .iter()
+            .enumerate()
+            .fold(0, |acc, (idx, var)| {
+                let bit = if bdd_valuation
+                    .get_value(*var)
+                    .expect("bits of the value should be in the valuation")
+                {
+                    1
+                } else {
+                    0
+                };
+
+                acc | (bit << idx)
+            });
+
+        let res = Self::gray_code_to_binary(read_gray_code);
+
+        if res > self.max_value {
+            panic!(
+                "invalid encoding; should not contain value greater than {}, but contains {}",
+                self.max_value, res
+            )
+        }
+
+        res
+    }
+}

tests/some_test.rs

@@ -3,6 +3,9 @@
 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>;
+
 struct TheFourImpls<D, OD>
 where
     D: bio::symbolic_domain::SymbolicDomainOrd<u8>,
@@ -126,52 +129,37 @@ impl TheFourImplsBdd {
     }
 }
 
-impl
-    TheFourImpls<
-        bio::symbolic_domain::PetriNetIntegerDomain,
-        bio::old_symbolic_domain::PetriNetIntegerDomain,
-    >
-{
+impl TheFourImpls<NewDomain, OldDomain> {
     fn from_path(sbml_path: &str) -> Self {
         let mut xml = xml::reader::EventReader::new(std::io::BufReader::new(
             std::fs::File::open(sbml_path).expect("should be able to open file"),
         ));
         bio::find_start_of(&mut xml, "listOfTransitions").expect("should be able to find");
-        let old_dumb = bio::old_update_fn::SystemUpdateFn::<
-            bio::old_symbolic_domain::PetriNetIntegerDomain,
-            u8,
-        >::try_from_xml(&mut xml)
-        .expect("should be able to parse");
+        let old_dumb = bio::old_update_fn::SystemUpdateFn::<OldDomain, u8>::try_from_xml(&mut xml)
+            .expect("should be able to parse");
 
         let mut xml = xml::reader::EventReader::new(std::io::BufReader::new(
             std::fs::File::open(sbml_path).expect("should be able to open file"),
         ));
         bio::find_start_of(&mut xml, "listOfTransitions").expect("should be able to find");
-        let old_smart = bio::old_update_fn::SmartSystemUpdateFn::<
-            bio::old_symbolic_domain::PetriNetIntegerDomain,
-            u8,
-        >::try_from_xml(&mut xml)
-        .expect("should be able to parse");
+        let old_smart =
+            bio::old_update_fn::SmartSystemUpdateFn::<OldDomain, u8>::try_from_xml(&mut xml)
+                .expect("should be able to parse");
 
         let mut xml = xml::reader::EventReader::new(std::io::BufReader::new(
             std::fs::File::open(sbml_path).expect("should be able to open file"),
         ));
         bio::find_start_of(&mut xml, "listOfTransitions").expect("should be able to find");
-        let new_dumb = bio::update_fn::SystemUpdateFn::<
-            bio::symbolic_domain::PetriNetIntegerDomain,
-            u8,
-        >::try_from_xml(&mut xml)
-        .expect("should be able to parse");
+        let new_dumb = bio::update_fn::SystemUpdateFn::<NewDomain, u8>::try_from_xml(&mut xml)
+            .expect("should be able to parse");
 
         let mut xml = xml::reader::EventReader::new(std::io::BufReader::new(
             std::fs::File::open(sbml_path).expect("should be able to open file"),
         ));
         bio::find_start_of(&mut xml, "listOfTransitions").expect("should be able to find");
-        let new_smart = bio::update_fn::SmartSystemUpdateFn::<
-            bio::symbolic_domain::PetriNetIntegerDomain,
-            u8,
-        >::try_from_xml(&mut xml)
-        .expect("should be able to parse");
+        let new_smart =
+            bio::update_fn::SmartSystemUpdateFn::<NewDomain, u8>::try_from_xml(&mut xml)
+                .expect("should be able to parse");
 
         Self {
             old_dumb,
@@ -330,11 +318,8 @@ fn consistency_check() {
                 // let filepath = "data/manual/basic_transition.sbml".to_string();
                 // let filepath = "data/large/146_BUDDING-YEAST-FAURE-2009.sbml".to_string();
 
-                let the_four = TheFourImpls::<
-                    bio::symbolic_domain::PetriNetIntegerDomain,
-                    bio::old_symbolic_domain::PetriNetIntegerDomain,
-                >::from_path(
-                    filepath.to_str().expect("could not convert to str")
+                let the_four = TheFourImpls::<NewDomain, OldDomain>::from_path(
+                    filepath.to_str().expect("could not convert to str"),
                 );
                 // >::from_path(&filepath);
 
@@ -482,14 +467,14 @@ fn check_specific() {
         let filepath = "data/large/146_BUDDING-YEAST-FAURE-2009.sbml".to_string();
 
         let the_four = TheFourImpls::<
-            bio::symbolic_domain::PetriNetIntegerDomain,
-            bio::old_symbolic_domain::PetriNetIntegerDomain,
+            NewDomain,
+            OldDomain,
             // >::from_path(filepath.to_str().expect("could not convert to str"));
         >::from_path(&filepath);
 
         let the_four_check = TheFourImpls::<
-            bio::symbolic_domain::PetriNetIntegerDomain,
-            bio::old_symbolic_domain::PetriNetIntegerDomain,
+            NewDomain,
+            OldDomain,
             // >::from_path(filepath.to_str().expect("could not convert to str"));
         >::from_path(&filepath);
 
@@ -688,11 +673,8 @@ fn predecessors_consistency_check() {
                 // let filepath = "data/manual/basic_transition.sbml".to_string();
                 // let filepath = "data/large/146_BUDDING-YEAST-FAURE-2009.sbml".to_string();
 
-                let the_four = TheFourImpls::<
-                    bio::symbolic_domain::PetriNetIntegerDomain,
-                    bio::old_symbolic_domain::PetriNetIntegerDomain,
-                >::from_path(
-                    filepath.to_str().expect("could not convert to str")
+                let the_four = TheFourImpls::<NewDomain, OldDomain>::from_path(
+                    filepath.to_str().expect("could not convert to str"),
                 );
                 // >::from_path(&filepath);
 
@@ -717,6 +699,8 @@ fn predecessors_consistency_check() {
                         "the new impls should be the same"
                     );
 
+                    assert!(initial_state.are_same(&the_four), "initial states are same");
+
                     let transitioned = the_four.predecessors_async(variable, initial_state);
 
                     // todo currently, there is a discrepancy between the old and new impls
@@ -761,7 +745,7 @@ fn predecessors_consistency_check() {
 
                     // assert!(transitioned.dumb_are_same(&the_four), "dumb");
 
-                    assert!(transitioned.are_same(&the_four), "all are same");
+                    assert!(transitioned.new_are_same(&the_four), "all are same");
 
                     println!("predecessors count = {} were the same", i);
                     i += 1;