1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228
use crate::{Bdd, BddNode, BddPointer, BddVariable};
use fxhash::FxBuildHasher;
use std::cmp::{max, min};
use std::collections::HashMap;
impl Bdd {
/// A ternary logical operation on three `Bdd` objects. Works the same as `Bdd::binary_op`,
/// but with three arguments.
///
/// Note that this may not necessarily be faster than performing two (or more) binary
/// operations. However, in some cases it can significantly reduce overhead incurred by
/// creating large intermediate decision diagrams.
pub fn ternary_op<T>(a: &Bdd, b: &Bdd, c: &Bdd, op_function: T) -> Bdd
where
T: Fn(Option<bool>, Option<bool>, Option<bool>) -> Option<bool>,
{
ternary_apply((a, b, c), (None, None, None), None, op_function)
}
/// A ternary version of `Bdd::fused_binary_flip_op` that makes it possible to flip
/// the meaning of a single variable the input and output diagrams.
///
/// Note that this may not necessarily be faster than performing two (or more) binary
/// operations. However, in some cases it can significantly reduce overhead incurred by
/// creating large intermediate decision diagrams.
pub fn fused_ternary_flip_op<T>(
a: (&Bdd, Option<BddVariable>),
b: (&Bdd, Option<BddVariable>),
c: (&Bdd, Option<BddVariable>),
flip_output: Option<BddVariable>,
op_function: T,
) -> Bdd
where
T: Fn(Option<bool>, Option<bool>, Option<bool>) -> Option<bool>,
{
ternary_apply((a.0, b.0, c.0), (a.1, b.1, c.1), flip_output, op_function)
}
}
fn ternary_apply<T>(
args: (&Bdd, &Bdd, &Bdd),
flips: (
Option<BddVariable>,
Option<BddVariable>,
Option<BddVariable>,
),
flip_out_if: Option<BddVariable>,
terminal_lookup: T,
) -> Bdd
where
T: Fn(Option<bool>, Option<bool>, Option<bool>) -> Option<bool>,
{
let (a, b, c) = args;
let (flip_a_if, flip_b_if, flip_c_if) = flips;
let num_vars = a.num_vars();
if a.num_vars() != b.num_vars() || b.num_vars() != c.num_vars() {
panic!(
"Var count mismatch: BDDs are not compatible. {} vs. {} vs. {}",
a.num_vars(),
b.num_vars(),
c.num_vars()
);
}
check_flip_bounds(num_vars, flip_a_if);
check_flip_bounds(num_vars, flip_b_if);
check_flip_bounds(num_vars, flip_c_if);
check_flip_bounds(num_vars, flip_out_if);
// Result holds the new BDD we are computing. Initially, `0` and `1` nodes are present. We
// remember if the result is `false` or not (`is_not_empty`). If it is, we just provide
// a `false` BDD instead of the result. This is easier than explicitly adding `1` later.
let mut result: Bdd = Bdd::mk_true(num_vars);
let mut is_not_empty = false;
// Every node in `result` is inserted into `existing` - this ensures we have no duplicates.
let expected_capacity = max(a.size(), max(b.size(), c.size()));
let mut existing: HashMap<BddNode, BddPointer, FxBuildHasher> =
HashMap::with_capacity_and_hasher(expected_capacity, FxBuildHasher::default());
existing.insert(BddNode::mk_zero(num_vars), BddPointer::zero());
existing.insert(BddNode::mk_one(num_vars), BddPointer::one());
// Task is a triple of pointers into the `a`, `b`, and `c` BDDs.
#[derive(Eq, PartialEq, Hash, Copy, Clone)]
struct Task {
a: BddPointer,
b: BddPointer,
c: BddPointer,
}
// `stack` is used to explore the BDDs "side by side" in DFS-like manner. Each task
// on the stack is a triple of nodes that needs to be fully processed before we are finished.
let mut stack: Vec<Task> = Vec::with_capacity(2 * usize::from(num_vars));
stack.push(Task {
a: a.root_pointer(),
b: b.root_pointer(),
c: c.root_pointer(),
});
// `finished` is a memoization cache of tasks that are already completed, since the same
// combination of nodes can be often explored multiple times.
let mut finished: HashMap<Task, BddPointer, FxBuildHasher> =
HashMap::with_capacity_and_hasher(expected_capacity, FxBuildHasher::default());
while let Some(on_stack) = stack.last() {
if finished.contains_key(on_stack) {
// skip finished tasks
stack.pop();
} else {
let (p_a, p_b, p_c) = (on_stack.a, on_stack.b, on_stack.c);
// Determine which variable we are conditioning on, moving from smallest to largest.
let (v_a, v_b, v_c) = (a.var_of(p_a), b.var_of(p_b), c.var_of(p_c));
let decision_var = min(v_a, min(v_b, v_c));
// If the variable is the same as in the left/right decision node,
// advance the exploration there. Otherwise, keep the pointers the same.
let (low_a, high_a) = if v_a != decision_var {
(p_a, p_a)
} else if Some(v_a) == flip_a_if {
(a.high_link_of(p_a), a.low_link_of(p_a))
} else {
(a.low_link_of(p_a), a.high_link_of(p_a))
};
let (low_b, high_b) = if v_b != decision_var {
(p_b, p_b)
} else if Some(v_b) == flip_b_if {
(b.high_link_of(p_b), b.low_link_of(p_b))
} else {
(b.low_link_of(p_b), b.high_link_of(p_b))
};
let (low_c, high_c) = if v_c != decision_var {
(p_c, p_c)
} else if Some(v_c) == flip_c_if {
(c.high_link_of(p_c), c.low_link_of(p_c))
} else {
(c.low_link_of(p_c), c.high_link_of(p_c))
};
// Two tasks which correspond to the two recursive sub-problems we need to solve.
let comp_low = Task {
a: low_a,
b: low_b,
c: low_c,
};
let comp_high = Task {
a: high_a,
b: high_b,
c: high_c,
};
// Try to solve the tasks using terminal lookup table or from cache.
let new_low = terminal_lookup(low_a.as_bool(), low_b.as_bool(), low_c.as_bool())
.map(BddPointer::from_bool)
.or_else(|| finished.get(&comp_low).cloned());
let new_high = terminal_lookup(high_a.as_bool(), high_b.as_bool(), high_c.as_bool())
.map(BddPointer::from_bool)
.or_else(|| finished.get(&comp_high).cloned());
// If both values are computed, mark this task as resolved.
if let (Some(new_low), Some(new_high)) = (new_low, new_high) {
if new_low.is_one() || new_high.is_one() {
is_not_empty = true
}
if new_low == new_high {
// There is no decision, just skip this node and point to either child.
finished.insert(*on_stack, new_low);
} else {
// There is a decision here.
let node = if flip_out_if == Some(decision_var) {
BddNode::mk_node(decision_var, new_high, new_low)
} else {
BddNode::mk_node(decision_var, new_low, new_high)
};
if let Some(index) = existing.get(&node) {
// Node already exists, just make it a result of this computation.
finished.insert(*on_stack, *index);
} else {
// Node does not exist, it needs to be pushed to result.
result.push_node(node);
existing.insert(node, result.root_pointer());
finished.insert(*on_stack, result.root_pointer());
}
}
stack.pop(); // Mark as resolved.
} else {
// Otherwise, if either value is unknown, push it to the stack.
if flip_out_if == Some(decision_var) {
// If we are flipping output, we have to compute subtasks in the right order.
if new_high.is_none() {
stack.push(comp_high);
}
if new_low.is_none() {
stack.push(comp_low);
}
} else {
if new_low.is_none() {
stack.push(comp_low);
}
if new_high.is_none() {
stack.push(comp_high);
}
}
}
}
}
if is_not_empty {
result
} else {
Bdd::mk_false(num_vars)
}
}
/// **(internal)** A simple utility method for checking bounds of a flip variable.
fn check_flip_bounds(num_vars: u16, var: Option<BddVariable>) {
if let Some(BddVariable(var)) = var {
if var >= num_vars {
panic!(
"Cannot flip variable {} in Bdd with {} variables.",
var, num_vars
);
}
}
}