mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-19 09:29:36 +01:00
Fix rustfmt
This commit is contained in:
parent
e78cd57210
commit
e7f38c100b
@ -85,24 +85,28 @@ impl NoGood {
|
|||||||
/// The parameter _update_ is set to [`true`] if there has been an update and to [`false`] otherwise
|
/// The parameter _update_ is set to [`true`] if there has been an update and to [`false`] otherwise
|
||||||
pub fn update_term_vec(&self, term_vec: &[Term], update: &mut bool) -> Vec<Term> {
|
pub fn update_term_vec(&self, term_vec: &[Term], update: &mut bool) -> Vec<Term> {
|
||||||
*update = false;
|
*update = false;
|
||||||
term_vec.iter().enumerate().map(|(idx,val)|{
|
term_vec
|
||||||
|
.iter()
|
||||||
|
.enumerate()
|
||||||
|
.map(|(idx, val)| {
|
||||||
let idx: u32 = idx.try_into().expect(
|
let idx: u32 = idx.try_into().expect(
|
||||||
"no-good learner implementation is based on the assumption \
|
"no-good learner implementation is based on the assumption \
|
||||||
that only u32::MAX-many variables are in place",
|
that only u32::MAX-many variables are in place",
|
||||||
);
|
);
|
||||||
if self.active.contains(idx){
|
if self.active.contains(idx) {
|
||||||
if !val.is_truth_value() {
|
if !val.is_truth_value() {
|
||||||
*update = true;
|
*update = true;
|
||||||
}
|
}
|
||||||
if self.value.contains(idx){
|
if self.value.contains(idx) {
|
||||||
Term::TOP
|
Term::TOP
|
||||||
}else{
|
} else {
|
||||||
Term::BOT
|
Term::BOT
|
||||||
}
|
}
|
||||||
}else{
|
} else {
|
||||||
*val
|
*val
|
||||||
}
|
}
|
||||||
}).collect()
|
})
|
||||||
|
.collect()
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Given a [NoGood] and another one, conclude a non-conflicting value which can be concluded on basis of the given one.
|
/// Given a [NoGood] and another one, conclude a non-conflicting value which can be concluded on basis of the given one.
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user