ellmau/adf-obdd
1
0
Fork 0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-19 09:29:36 +01:00
Code Issues Projects Releases Wiki Activity

Add more efficient construction of 2-val models with counting

Browse Source 
wip commit; considering variable impact on other bdds should be
implemented next
This commit is contained in:
Stefan Ellmauthaler 2022-03-24 16:57:18 +01:00
parent 0d4f9ff195
commit 39379d9e3d
Failed to extract signature
2 changed files with 33 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
lib/src/adf.rs
View File

@ -388,11 +388,15 @@ impl Adf {
} }
fn two_val_model_counts(&mut self, interpr: &[Term]) -> Vec<Vec<Term>> { fn two_val_model_counts(&mut self, interpr: &[Term]) -> Vec<Vec<Term>> {
self.two_val_model_counts_logic(interpr, &vec![Term::UND; interpr.len()])
}
fn two_val_model_counts_logic(&mut self, interpr: &[Term], must_be: &[Term]) -> Vec<Vec<Term>> {
log::trace!("two_val_model_counts({:?}) called ", interpr); log::trace!("two_val_model_counts({:?}) called ", interpr);
if let Some((idx, ac)) = interpr if let Some((idx, ac)) = interpr
.iter() .iter()
.enumerate() .enumerate()
.filter(|(_idx, val)| !val.is_truth_value()) .filter(|(idx, val)| !(val.is_truth_value() || must_be[*idx].is_truth_value()))
.min_by(|(_idx_a, val_a), (_idx_b, val_b)| { .min_by(|(_idx_a, val_a), (_idx_b, val_b)| {
self.bdd self.bdd
.models(**val_a, true) .models(**val_a, true)
@ -417,15 +421,16 @@ impl Adf {
let res = negative let res = negative
.iter() .iter()
.try_for_each(|var| { .try_for_each(|var| {
if new_int[var.value()].is_true() { if new_int[var.value()].is_true() || must_be[var.value()] == Term::TOP {
return Err(()); return Err(());
} }
new_int[var.value()] = Term::BOT; new_int[var.value()] = Term::BOT;
Ok(()) Ok(())
}) })
.and(positive.iter().try_for_each(|var| { .and(positive.iter().try_for_each(|var| {
if new_int[var.value()].is_truth_value() if (new_int[var.value()].is_truth_value()
&& !new_int[var.value()].is_true() && !new_int[var.value()].is_true())
|| must_be[var.value()] == Term::BOT
{ {
return Err(()); return Err(());
} }
@ -435,7 +440,7 @@ impl Adf {
if res.is_ok() { if res.is_ok() {
new_int[idx] = if check_models { Term::TOP } else { Term::BOT }; new_int[idx] = if check_models { Term::TOP } else { Term::BOT };
let upd_int = self.update_interpretation(&new_int); let upd_int = self.update_interpretation(&new_int);
result.append(&mut self.two_val_model_counts(&upd_int)); result.append(&mut self.two_val_model_counts_logic(&upd_int, must_be));
} }
res res
}); });
@ -449,16 +454,34 @@ impl Adf {
// TODO: should be "must be true/false" instead of setting it to TOP/BOT and will need sanity checks at every iteration // TODO: should be "must be true/false" instead of setting it to TOP/BOT and will need sanity checks at every iteration
log::trace!("\nnew_int {new_int:?}\nupd_int {upd_int:?}"); log::trace!("\nnew_int {new_int:?}\nupd_int {upd_int:?}");
if new_int[idx].no_inf_decrease(&upd_int[idx]) { if new_int[idx].no_inf_inconsistency(&upd_int[idx]) {
upd_int[idx] = if check_models { Term::BOT } else { Term::TOP }; upd_int[idx] = if check_models { Term::BOT } else { Term::TOP };
if new_int[idx].no_inf_decrease(&upd_int[idx]) { if new_int[idx].no_inf_inconsistency(&upd_int[idx]) {
result.append(&mut self.two_val_model_counts(&upd_int)); let mut must_be_new = must_be.to_vec();
must_be_new[idx] = new_int[idx];
result.append(&mut self.two_val_model_counts_logic(&upd_int, &must_be_new));
} }
} }
result result
} else { } else {
// filter has created empty iterator // filter has created empty iterator
vec![interpr.to_vec()] let concluded = interpr
.iter()
.enumerate()
.map(|(idx, val)| {
if !val.is_truth_value() {
must_be[idx]
} else {
*val
}
})
.collect::<Vec<Term>>();
// TODO: Not copletely correct - should be a check if concluded is consistant with ac
if concluded == self.update_interpretation(&concluded) {
vec![concluded]
} else {
vec![interpr.to_vec()]
}
} }
} }

2
lib/src/datatypes/bdd.rs
View File

@ -73,7 +73,7 @@ impl Term {
} }
/// Returns true if the information of *other* does not decrease and it is not inconsistent. /// Returns true if the information of *other* does not decrease and it is not inconsistent.
pub fn no_inf_decrease(&self, other: &Self) -> bool { pub fn no_inf_inconsistency(&self, other: &Self) -> bool {
if self.compare_inf(other) { if self.compare_inf(other) {
return true; return true;
} }