Skip to content

Commit

Permalink
refactor: gray encoding SymbolicDomainOrd impl
Browse files Browse the repository at this point in the history
  • Loading branch information
Lukáš Chudíček committed Dec 12, 2023
1 parent bf50e5b commit be302eb
Show file tree
Hide file tree
Showing 2 changed files with 30 additions and 2 deletions.
28 changes: 28 additions & 0 deletions src/symbolic_domains/symbolic_domain.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}
}
4 changes: 2 additions & 2 deletions tests/some_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit be302eb

Please sign in to comment.