Skip to content

Commit

Permalink
rename local vars
Browse files Browse the repository at this point in the history
  • Loading branch information
@shnarazk
shnarazk committed Feb 3, 2024
1 parent 62194ce commit c8364b6
Show file tree
Hide file tree
Showing 2 changed files with 52 additions and 85 deletions.
97 changes: 32 additions & 65 deletions src/bdd.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,50 +45,50 @@ impl ReducedDecisionDiagram for BDD<Node> {
// convert tree to BDD
fn reduce(&mut self) {
let root = &self.graph;
let mut to_index: HashMap<Node, usize> = HashMap::new();
let mut from_index: HashMap<usize, Node> = HashMap::new();
from_index.insert(0, Node::new_constant(false));
from_index.insert(1, Node::new_constant(true));
let mut index: HashMap<Node, usize> = HashMap::new();
let mut node: HashMap<usize, Node> = HashMap::new();
node.insert(0, Node::new_constant(false));
node.insert(1, Node::new_constant(true));
let mut vlist: HashMap<usize, Vec<&Node>> = HashMap::new();
// put each vertex u on list vlist[u.var_index]
for n in root.all_nodes().iter().cloned() {
let k = n.unified_key();
to_index.insert(n.clone(), k);
index.insert(n.clone(), k);
if 1 < k {
from_index.insert(k, n.clone());
node.insert(k, n.clone());
vlist.entry(k).or_default().push(n);
}
}
let mut next_id: usize = 2;
for vi in vlist.keys().sorted().rev() {
let lst = &vlist[vi];
let mut q: Vec<((usize, usize), &Node)> = Vec::new();
for node in lst.iter().cloned() {
match **node {
for n in lst.iter().cloned() {
match **n {
Vertex::Bool(_) => (),
Vertex::Var {
ref low, ref high, ..
} => {
if to_index[low] == to_index[high] {
if index[low] == index[high] {
// redundant vertex
to_index.insert(node.clone(), to_index[low]);
index.insert(n.clone(), index[low]);
} else {
q.push(((to_index[low], to_index[high]), node));
q.push(((index[low], index[high]), n));
}
}
}
}
q.sort_unstable_by_key(|(k, _)| *k);
let mut old_key: (usize, usize) = (usize::MAX, usize::MAX);
for (key, node) in q.iter().cloned() {
for (key, n) in q.iter().cloned() {
if key == old_key {
to_index.insert(node.clone(), next_id);
index.insert(n.clone(), next_id);
} else {
next_id += 1;
match **node {
match **n {
Vertex::Bool(_) => {
to_index.insert(node.clone(), next_id);
from_index.insert(next_id, node.clone());
index.insert(n.clone(), next_id);
node.insert(next_id, n.clone());
}
Vertex::Var {
var_index,
Expand All @@ -97,77 +97,44 @@ impl ReducedDecisionDiagram for BDD<Node> {
} => {
let n = Node::new_var(
var_index,
from_index[&to_index[low]].clone(),
from_index[&to_index[high]].clone(),
node[&index[low]].clone(),
node[&index[high]].clone(),
);
to_index.insert(node.clone(), next_id);
to_index.insert(n.clone(), next_id);
from_index.insert(next_id, n);
index.insert(n.clone(), next_id);
index.insert(n.clone(), next_id);
node.insert(next_id, n);
}
}
old_key = key;
}
}
}
// pick up a tree from the hash-table
self.graph = from_index[&to_index[root]].clone();
self.graph = node[&index[root]].clone();
}
fn apply(&self, op: Box<dyn Fn(bool, bool) -> bool>, unit: bool, other: &Self) -> BDD<Node> {
let mut from_index: HashMap<usize, Node> = HashMap::new();
from_index.insert(0, Node::new_constant(false));
from_index.insert(1, Node::new_constant(true));
let mut to_index: HashMap<Node, usize> = HashMap::new();
for (i, node) in self
let mut node: HashMap<usize, Node> = HashMap::new();
node.insert(0, Node::new_constant(false));
node.insert(1, Node::new_constant(true));
let mut index: HashMap<Node, usize> = HashMap::new();
for (i, n) in self
.graph
.all_nodes()
.iter()
.chain(other.graph.all_nodes().iter())
.enumerate()
{
from_index.insert(i + 2, (*node).clone());
if let Some(b) = node.is_constant() {
to_index.insert((*node).clone(), b as usize);
node.insert(i + 2, (*n).clone());
if let Some(b) = n.is_constant() {
index.insert((*n).clone(), b as usize);
} else {
to_index.insert((*node).clone(), i + 2);
index.insert((*n).clone(), i + 2);
}
}
// mapping from index pair to index
let mut merged: HashMap<(usize, usize), Node> = HashMap::new();
// mapping from node to bool
let mut evaluation: HashMap<Node, bool> = HashMap::new();
// | unit hashKey value1 value2 value u |
// hashKey := (to_index at: v1) @ (to_index at: v2).
// merged at: hashKey ifPresent: [ :node | node ifNotNil: [ ^ node "have already evaluated" ] ].
// value1 := evaluation at: v1 ifAbsent: [ nil ].
// value2 := evaluation at: v2 ifAbsent: [ nil ].
// "u.value := v1.value <op> v2.value"
// value := (value1 = unit or: [ value2 = unit ]) ifTrue: [ unit ]
// ifFalse: [
// value1 ifNotNil: [ value2 ifNotNil: [ operator value: value1 value: value2 ] ] ].
// u := value ifNil: [
// | v1Index v2Index vlow1 vlow2 vhigh1 vhigh2 w |
// "create a nonterminal vertex and evaluate further down"
// w := DDNode new.
// evaluation at: w put: value.
// v1Index := v1 isLiteral ifTrue: [ v1 ] ifFalse: [ v1 varIndex ].
// v2Index := v2 isLiteral ifTrue: [ v2 ] ifFalse: [ v2 varIndex ].
// w varIndex: (v1 isLiteral ifTrue: [
// v2 isLiteral ifTrue: [ operator value: v1 value: v2 ] ifFalse: [ v2Index ] ]
// ifFalse: [
// v2 isLiteral ifTrue: [ v1Index ] ifFalse: [ v1 varIndex min: v2 varIndex ] ]).
// vlow1 := v1Index = w varIndex ifTrue: [ v1 low ] ifFalse: [ v1 ].
// vlow2 := v2Index = w varIndex ifTrue: [ v2 low ] ifFalse: [ v2 ].
// vhigh1 := v1Index = w varIndex ifTrue: [ v1 high ] ifFalse: [ v1 ].
// vhigh2 := v2Index = w varIndex ifTrue: [ v2 high ] ifFalse: [ v2 ].
// w low: (self apply: operator
// on: vlow1
// and: vlow2).
// w high: (self apply: operator
// on: vhigh1
// and: vhigh2).
// w ].
// aMapping at: hashKey put: u.
// ^ u
fn aux(
operator @ (op, unit): &BooleanOperator,
(v1, v2): (Node, Node),
Expand Down Expand Up @@ -239,7 +206,7 @@ impl ReducedDecisionDiagram for BDD<Node> {
graph: aux(
&(op, unit),
(self.graph.clone(), other.graph.clone()),
(&mut to_index, &mut from_index),
(&mut index, &mut node),
&mut evaluation,
&mut merged,
),
Expand Down
40 changes: 20 additions & 20 deletions src/zdd.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,17 +45,17 @@ impl<N: DecisionDiagram<N> + DecisionDiagramNode> DecisionDiagram<N> for ZDD<N>
impl ReducedDecisionDiagram for ZDD<Node> {
fn reduce(&mut self) {
let root = &self.graph;
let mut to_index: HashMap<Node, usize> = HashMap::new();
let mut from_index: HashMap<usize, Node> = HashMap::new();
from_index.insert(0, Node::new_constant(false));
from_index.insert(1, Node::new_constant(true));
let mut index: HashMap<Node, usize> = HashMap::new();
let mut node: HashMap<usize, Node> = HashMap::new();
node.insert(0, Node::new_constant(false));
node.insert(1, Node::new_constant(true));
let mut vlist: HashMap<usize, Vec<&Node>> = HashMap::new();
// put each vertex u on list vlist[u.var_index]
for n in root.all_nodes().iter().cloned() {
let k = n.unified_key();
to_index.insert(n.clone(), k);
index.insert(n.clone(), k);
if 1 < k {
from_index.insert(k, n.clone());
node.insert(k, n.clone());
vlist.entry(k).or_default().push(n);
}
}
Expand All @@ -68,26 +68,26 @@ impl ReducedDecisionDiagram for ZDD<Node> {
Vertex::Var {
ref low, ref high, ..
} => {
if to_index[high] == 0 {
if index[high] == 0 {
// redundant vertex
to_index.insert(node.clone(), to_index[low]);
index.insert(node.clone(), index[low]);
} else {
q.push(((to_index[low], to_index[high]), node));
q.push(((index[low], index[high]), node));
}
}
}
}
q.sort_unstable_by_key(|(k, _)| *k);
let mut old_key: (usize, usize) = (usize::MAX, usize::MAX);
for (key, node) in q.iter().cloned() {
for (key, n) in q.iter().cloned() {
if key == old_key {
to_index.insert(node.clone(), next_id);
index.insert(n.clone(), next_id);
} else {
next_id += 1;
match **node {
match **n {
Vertex::Bool(_) => {
to_index.insert(node.clone(), next_id);
from_index.insert(next_id, node.clone());
index.insert(n.clone(), next_id);
node.insert(next_id, n.clone());
}
Vertex::Var {
var_index,
Expand All @@ -96,20 +96,20 @@ impl ReducedDecisionDiagram for ZDD<Node> {
} => {
let n = Node::new_var(
var_index,
from_index[&to_index[low]].clone(),
from_index[&to_index[high]].clone(),
node[&index[low]].clone(),
node[&index[high]].clone(),
);
to_index.insert(node.clone(), next_id);
to_index.insert(n.clone(), next_id);
from_index.insert(next_id, n);
index.insert(n.clone(), next_id);
index.insert(n.clone(), next_id);
node.insert(next_id, n);
}
}
old_key = key;
}
}
}
// pick up a tree from the hash-table
self.graph = from_index[&to_index[root]].clone();
self.graph = node[&index[root]].clone();
}
fn apply(&self, _op: Box<dyn Fn(bool, bool) -> bool>, _unit: bool, _other: &Self) -> Self {
unimplemented!()
Expand Down

0 comments on commit c8364b6

Please sign in to comment.