bex/
vhl.rs

1//! (Var, Hi, Lo) triples
2use std::collections::BinaryHeap;
3use std::collections::HashSet;
4use dashmap::DashMap;
5use crate::nid::NID;
6use crate::vid::VID;
7
8type VhlHashMap<K,V> = DashMap<K,V,fxhash::FxBuildHasher>;
9
10#[derive(Debug,Default,Clone)]
11struct VhlVec<T>{ pub vec: boxcar::Vec<T> }
12
13
14/// Simple Hi/Lo pair stored internally when representing nodes.
15/// All nodes with the same branching variable go in the same array, so there's
16/// no point duplicating it.
17#[derive(PartialEq, Eq, Hash, Clone, Copy, Debug, Default)]
18pub struct HiLo {pub hi:NID, pub lo:NID}
19
20impl HiLo {
21  /// constructor
22  pub fn new(hi:NID, lo:NID)->HiLo { HiLo { hi, lo } }
23
24  /// apply the not() operator to both branches
25  #[inline] pub fn invert(self)-> HiLo { HiLo{ hi: !self.hi, lo: !self.lo }}
26
27  pub fn get_part(&self, which:HiLoPart)->NID {
28    if which == HiLoPart::HiPart { self.hi } else { self.lo }} }
29
30impl std::ops::Not for HiLo {
31  type Output = HiLo;
32  fn not(self)-> HiLo {HiLo { hi:!self.hi, lo: !self.lo }}}
33
34
35/// Vhl (for when we really do need the variable)
36#[derive(PartialEq, Eq, PartialOrd, Ord, Hash, Clone, Copy, Debug)]
37pub struct Vhl {pub v:VID, pub hi:NID, pub lo:NID}
38
39impl Vhl {
40  pub fn new(v: VID, hi:NID, lo:NID)->Vhl { Vhl{ v, hi, lo } }
41  pub fn hilo(&self)->HiLo { HiLo{ hi:self.hi, lo: self.lo } }}
42
43impl std::ops::Not for Vhl {
44  type Output = Vhl;
45  fn not(self)->Vhl { Vhl { v:self.v, hi:!self.hi, lo: !self.lo }}}
46
47
48/// Enum for referring to the parts of a HiLo (for WIP).
49#[derive(PartialEq,Debug,Copy,Clone)]
50pub enum HiLoPart { HiPart, LoPart }
51
52/// a deconstructed Vhl (for WIP)
53#[derive(Default,PartialEq,Debug,Copy,Clone)]
54pub struct VhlParts{
55  pub v:VID,
56  pub hi:Option<NID>,
57  pub lo:Option<NID>,
58  pub invert:bool}
59
60  impl VhlParts {
61    pub fn hilo(&self)->Option<HiLo> {
62      if let (Some(hi), Some(lo)) = (self.hi, self.lo) { Some(HiLo{hi,lo}) }
63      else { None }}
64    pub fn set_part(&mut self, part:HiLoPart, v:Option<NID>) {
65      if part == HiLoPart::HiPart { self.hi = v }
66      else { self.lo = v }}}
67
68
69pub trait Walkable {
70
71  /// walk nodes in graph for nid n recursively, without revisiting shared nodes
72  fn step<F>(&self, n:NID, f:&mut F, seen:&mut HashSet<NID>, topdown:bool)
73  where F: FnMut(NID,VID,NID,NID);
74
75  /// iterate through (nid, vid, hi:nid, lo:nid) tuples in the graph.
76  /// visit the parent before visiting the children.
77  fn walk_dn<F>(&self, n:NID, f:&mut F) where F: FnMut(NID,VID,NID,NID) {
78    let mut seen = HashSet::new();
79    self.step(n, f, &mut seen, true)}
80
81  /// same as walk_dn, but visit children before firing the function.
82  /// note that this walks from "left to right" ("lo' to "hi")
83  /// and bottom to top, starting from the leftmost node.
84  /// if you want the bottommost nodes to come first, use self.as_heap(n)
85  fn walk_up<F>(&self, n:NID, f:&mut F) where F: FnMut(NID,VID,NID,NID) {
86    let mut seen = HashSet::new();
87    self.step(n, f, &mut seen, false)}
88
89  /// iterate through (nid, vid, hi:nid, lo:nid) tuples in the graph
90  /// for each nid. visit children before visiting the parent.
91  fn walk_up_each<F>(&self, nids:&[NID], f:&mut F) where F: FnMut(NID,VID,NID,NID) {
92    let mut seen = HashSet::new();
93    for &n in nids { self.step(n, f, &mut seen, false) }}
94
95  /// this is meant for walking nodes ordered by variables from bottom to top.
96  /// it's deprecated because the whole thing ought to be replaced by a nice iterator
97  /// (also, it's not clear to me why the derived Ord for Vhl doesn't require Reverse() here)
98  #[deprecated]
99  fn as_heap(&self, n:NID)->BinaryHeap<(Vhl, NID)> {
100    let mut result = BinaryHeap::new();
101    self.walk_up(n, &mut |nid, v, hi, lo| result.push((Vhl{ v, hi, lo }, nid)));
102    result }}
103
104
105pub trait HiLoBase {
106  fn get_hilo(&self, n:NID)->Option<HiLo>; }
107
108
109#[derive(Debug, Default, Clone)]
110pub struct HiLoCache {
111  /// variable-agnostic hi/lo pairs for individual bdd nodes.
112  hilos: VhlVec<HiLo>,
113  /// reverse map for hilos.
114  index: VhlHashMap<HiLo, usize>}
115
116
117impl HiLoCache {
118
119  pub fn new()->Self { Self::default() }
120
121  pub fn len(&self)->usize { self.hilos.vec.len() }
122  #[must_use] pub fn is_empty(&self) -> bool { self.len() == 0 }
123
124  // TODO: ->Option<HiLo>, and then impl HiLoBase
125  #[inline] pub fn get_hilo(&self, n:NID)->HiLo {
126    assert!(!n.is_lit());
127    let res = self.hilos.vec[n.idx()];
128    if n.is_inv() { res.invert() } else { res }}
129
130  #[inline] pub fn get_node(&self, v:VID, hl0:HiLo)-> Option<NID> {
131    let inv = hl0.lo.is_inv();
132    let hl1 = if inv { hl0.invert() } else { hl0 };
133    if let Some(x) = self.index.get(&hl1) {
134      // !! maybe this should be an assertion, and callers
135      //   should be adjusted to avoid asking for ill-formed Vhl triples?
136      // (without this check, we potentially break the contract of always
137      //  returning a NID that represents a valid Bdd)
138      if hl1.hi.vid().is_below(&v) && hl1.lo.vid().is_below(&v) {
139        let nid = NID::from_vid_idx(v, *x);
140        return Some(if inv { !nid  } else { nid }) }}
141    None }
142
143  #[inline] pub fn insert(&self, v:VID, hl0:HiLo)->NID {
144    let inv = hl0.lo.is_inv();
145    let hilo = if inv { hl0.invert() } else { hl0 };
146    let ix:usize =
147      if let Some(ix) = self.index.get(&hilo) { *ix }
148      else {
149        let ix = self.hilos.vec.push(hilo);
150        self.index.insert(hilo, ix);
151        ix };
152    let res = NID::from_vid_idx(v, ix);
153    if inv { !res } else { res } }}
bex/vhl.rs

bex/
vhl.rs
