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 fine-grained heuristics

Browse Source 
considering max-depth too
This commit is contained in:
Stefan Ellmauthaler 2022-04-04 13:04:11 +02:00
parent 8d9e7f09e1
commit 3feeb1343b
Failed to extract signature
1 changed files with 11 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
lib/src/adf.rs
View File

@ -1,12 +1,10 @@
/*! /*!
This module describes the abstract dialectical framework This module describes the abstract dialectical framework
- computing interpretations - computing interpretations and models
- computing fixpoints - computing fixpoints
*/ */
use std::collections::HashSet;
use serde::{Deserialize, Serialize}; use serde::{Deserialize, Serialize};
use crate::{ use crate::{
@ -29,8 +27,6 @@ pub struct Adf {
ordering: VarContainer, ordering: VarContainer,
bdd: Bdd, bdd: Bdd,
ac: Vec<Term>, ac: Vec<Term>,
#[serde(skip)]
callcache: HashSet<Vec<Term>>,
} }
impl Default for Adf { impl Default for Adf {
@ -39,7 +35,6 @@ impl Default for Adf {
ordering: VarContainer::default(), ordering: VarContainer::default(),
bdd: Bdd::new(), bdd: Bdd::new(),
ac: Vec::new(), ac: Vec::new(),
callcache: HashSet::new(),
} }
} }
} }
@ -55,7 +50,6 @@ impl Adf {
), ),
bdd: Bdd::new(), bdd: Bdd::new(),
ac: vec![Term(0); parser.namelist_rc_refcell().as_ref().borrow().len()], ac: vec![Term(0); parser.namelist_rc_refcell().as_ref().borrow().len()],
callcache: HashSet::new(),
}; };
(0..parser.namelist_rc_refcell().borrow().len()) (0..parser.namelist_rc_refcell().borrow().len())
.into_iter() .into_iter()
@ -93,7 +87,6 @@ impl Adf {
ordering: VarContainer::copy(ordering), ordering: VarContainer::copy(ordering),
bdd: Bdd::new(), bdd: Bdd::new(),
ac: vec![Term(0); bio_ac.len()], ac: vec![Term(0); bio_ac.len()],
callcache: HashSet::new(),
}; };
result result
.ac .ac
@ -417,10 +410,18 @@ impl Adf {
.cmp(&self.bdd.paths(**val_b, true).minimum()) .cmp(&self.bdd.paths(**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 => match self
.bdd .bdd
.var_impact(Var(*idx_b), interpr) .var_impact(Var(*idx_b), interpr)
.cmp(&self.bdd.var_impact(Var(*idx_a), interpr)), .cmp(&self.bdd.var_impact(Var(*idx_a), interpr))
{
// If it is still equal, choose the one with the maximal depth (i.e. the most applied changes)
std::cmp::Ordering::Equal => self
.bdd
.max_depth(**val_b)
.cmp(&self.bdd.max_depth(**val_a)),
value => value,
},
value => value, value => value,
} }
}) })