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

Update counting function with some adaptions

Browse Source 
Still more changes to come (e.g. interpretation path counting)
This commit is contained in:
Stefan Ellmauthaler 2022-03-31 17:17:52 +02:00
parent 6a47f4db30
commit ccb82318d5
Signed by: ellmau
GPG Key ID: C804A9C1B7AF8256
1 changed files with 30 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
lib/src/adf.rs
View File

@ -404,15 +404,20 @@ impl Adf {
will_be: &[Term], will_be: &[Term],
depth: usize, depth: usize,
) -> Vec<Vec<Term>> { ) -> Vec<Vec<Term>> {
if self.callcache.contains(&interpr.to_vec()) { let cacheitem = interpr
panic!("moo"); .iter()
.enumerate()
.map(|(idx, val)| *val.min(&will_be[idx]))
.collect::<Vec<Term>>();
if !self.callcache.insert(cacheitem) {
panic!("trying to check the same model candidate twice");
return Vec::new();
} }
self.callcache.insert(interpr.to_vec());
log::trace!("two_val_model_counts({:?}) called", interpr); log::trace!("two_val_model_counts({:?}) called", interpr);
log::debug!("two_val_model_recursion_depth: {}/{}", depth, interpr.len()); log::debug!("two_val_model_recursion_depth: {}/{}", depth, interpr.len());
for (idx, &ac) in interpr.iter().enumerate() { //for (idx, &ac) in interpr.iter().enumerate() {
log::trace!("idx{}, ac: Term({}), modelc-/+: {:?}, depth:{}, impact: {}, num_interpr+: {}, num interpr-: {}", idx, ac, self.bdd.models(ac, true), self.bdd.max_depth(ac), self.bdd.var_impact(Var(idx),interpr), self.bdd.interpretations(ac, true, Var(idx), &[], &[]).len(),self.bdd.interpretations(ac, false, Var(idx), &[], &[]).len()); // log::trace!("idx{}, ac: Term({}), modelc-/+: {:?}, depth:{}, impact: {}, num_interpr+: {}, num interpr-: {}", idx, ac, self.bdd.models(ac, true), self.bdd.max_depth(ac), self.bdd.var_impact(Var(idx),interpr), self.bdd.interpretations(ac, true, Var(idx), &[], &[]).len(),self.bdd.interpretations(ac, false, Var(idx), &[], &[]).len());
} //}
if let Some((idx, ac)) = interpr if let Some((idx, ac)) = interpr
.iter() .iter()
.enumerate() .enumerate()
@ -420,15 +425,14 @@ impl Adf {
.min_by(|(idx_a, val_a), (idx_b, val_b)| { .min_by(|(idx_a, val_a), (idx_b, val_b)| {
match self match self
.bdd .bdd
.models(**val_a, true) .var_impact(Var(*idx_b), interpr)
.minimum() .cmp(&self.bdd.var_impact(Var(*idx_a), interpr))
.cmp(&self.bdd.models(**val_b, true).minimum())
{ {
// if the minimal counts are equal, choose the maximal var_impact // if the minimal counts are equal, choose the maximal var_impact
std::cmp::Ordering::Equal => self std::cmp::Ordering::Equal => self
.bdd .bdd
.var_impact(Var(*idx_b), interpr) .max_depth(**val_a)
.cmp(&self.bdd.var_impact(Var(*idx_a), interpr)), .cmp(&self.bdd.max_depth(**val_b)),
value => value, value => value,
} }
}) })
@ -441,7 +445,6 @@ impl Adf {
ac, ac,
check_models check_models
); );
let _ = self // return value can be ignored, but must be catched let _ = self // return value can be ignored, but must be catched
.bdd .bdd
.interpretations(*ac, check_models, Var(idx), &[], &[]) .interpretations(*ac, check_models, Var(idx), &[], &[])
@ -469,7 +472,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_fixpoint(&new_int);
if self.check_consistency(&upd_int, will_be) { if self.check_consistency(&upd_int, will_be) {
result.append(&mut self.two_val_model_counts_logic( result.append(&mut self.two_val_model_counts_logic(
&upd_int, &upd_int,
@ -482,12 +485,12 @@ impl Adf {
}); });
log::trace!("results found so far:{}", result.len()); log::trace!("results found so far:{}", result.len());
// checked one alternative, we can now conclude that only the other option may work // checked one alternative, we can now conclude that only the other option may work
log::trace!("checked one alternative, concluding the other value"); log::debug!("checked one alternative, concluding the other value");
let new_int = interpr let new_int = interpr
.iter() .iter()
.map(|tree| self.bdd.restrict(*tree, Var(idx), !check_models)) .map(|tree| self.bdd.restrict(*tree, Var(idx), !check_models))
.collect::<Vec<Term>>(); .collect::<Vec<Term>>();
let mut upd_int = self.update_interpretation(&new_int); let mut upd_int = self.update_interpretation_fixpoint(&new_int);
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_inconsistency(&upd_int[idx]) { if new_int[idx].no_inf_inconsistency(&upd_int[idx]) {
@ -516,7 +519,6 @@ impl Adf {
} }
}) })
.collect::<Vec<Term>>(); .collect::<Vec<Term>>();
// TODO: Not copletely correct - should be a check if concluded is consistant with ac
let ac = self.ac.clone(); let ac = self.ac.clone();
let result = self.apply_interpretation(&ac, &concluded); let result = self.apply_interpretation(&ac, &concluded);
if self.check_consistency(&result, &concluded) { if self.check_consistency(&result, &concluded) {
@ -527,6 +529,18 @@ impl Adf {
} }
} }
fn update_interpretation_fixpoint(&mut self, interpretation: &[Term]) -> Vec<Term> {
let mut cur_int = interpretation.to_vec();
loop {
let new_int = self.update_interpretation(interpretation);
if cur_int == new_int {
return cur_int;
} else {
cur_int = new_int;
}
}
}
fn update_interpretation(&mut self, interpretation: &[Term]) -> Vec<Term> { fn update_interpretation(&mut self, interpretation: &[Term]) -> Vec<Term> {
self.apply_interpretation(interpretation, interpretation) self.apply_interpretation(interpretation, interpretation)
} }