Skip to content

Commit

Permalink
Disentangles VarOrder and BddPtr with new PartialVariableOrder
Browse files Browse the repository at this point in the history
…trait, fixes ref/lifetimes

Two problems:

1. `VarOrder`'s `first`, `first_essential`, and `sort` methods rely
   on the input type being a `BddPtr`, which causes problems for
   #163. So, I've instead abstracted the idea of a partial variable order,
   i.e. that structs may or may not have a sortable variable,
   to a trait; `BddPtr` (and soon, `SemanticBddPtr`) implements
   this trait. This caused minimal code impact.
2. `first`, `first_essential`, and `sort` shouldn't consume their
   inputs, so I've changed these to just be refs. Required lifetime
   annotations.

Then, added doctests for these methods!
  • Loading branch information
mattxwang committed Jul 27, 2023
1 parent af20185 commit 707062a
Show file tree
Hide file tree
Showing 3 changed files with 96 additions and 36 deletions.
2 changes: 1 addition & 1 deletion src/builder/bdd/robdd.rs
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ impl<'a, T: IteTable<'a, BddPtr<'a>> + Default> BddBuilder<'a> for RobddBuilder<

// ok the work!
// find the first essential variable for f, g, or h
let lbl = self.order.borrow().first_essential(f, g, h);
let lbl = self.order.borrow().first_essential(&f, &g, &h);
let fx = self.condition_essential(f, lbl, true);
let gx = self.condition_essential(g, lbl, true);
let hx = self.condition_essential(h, lbl, true);
Expand Down
11 changes: 11 additions & 0 deletions src/repr/bdd.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,8 @@ use std::{
};
use BddPtr::*;

use super::var_order::PartialVariableOrder;

/// Core BDD pointer datatype
#[derive(Debug, Clone, Eq, Copy, PartialOrd, Ord)]
pub enum BddPtr<'a> {
Expand Down Expand Up @@ -50,6 +52,15 @@ impl<'a> Hash for BddPtr<'a> {
}
}

impl<'a> PartialVariableOrder for BddPtr<'a> {
fn var(&self) -> Option<VarLabel> {
match self {
Compl(n) | Reg(n) => Some(n.var),
PtrTrue | PtrFalse => None,
}
}
}

/// The intermediate representation for a BddPtr that is being folded in a
/// [`Fold`] computation.
///
Expand Down
119 changes: 84 additions & 35 deletions src/repr/var_order.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,8 @@
//! in the order occur first in the BDD, starting from the root.
//! Lower numbers occur first in the order (i.e., closer to the root)

use crate::{
repr::{bdd::BddPtr, var_label::VarLabel},
util,
};
use std::fmt::Display;
use crate::{repr::var_label::VarLabel, util};
use std::fmt::{Debug, Display};

#[derive(Debug, Clone)]
pub struct VarOrder {
Expand Down Expand Up @@ -97,18 +94,31 @@ impl VarOrder {
self.var_to_pos[a.value() as usize] <= self.var_to_pos[b.value() as usize]
}

/// Returns the BddPtr whose top variable occurs first in a given
/// ordering (ties broken by returning `a`)
pub fn first<'a>(&self, a: BddPtr<'a>, b: BddPtr<'a>) -> BddPtr<'a> {
match (a, b) {
(BddPtr::PtrTrue, _) | (BddPtr::PtrFalse, _) => b,
(_, BddPtr::PtrTrue) | (_, BddPtr::PtrFalse) => a,
(
BddPtr::Reg(node_a) | BddPtr::Compl(node_a),
BddPtr::Reg(node_b) | BddPtr::Compl(node_b),
) => {
let pa = self.get(node_a.var);
let pb = self.get(node_b.var);
/// Returns the item (with a partial label) whose top variable
/// occurs first in a given ordering (ties broken by returning `a`)
/// ```
/// # use rsdd::repr::bdd::{BddNode, BddPtr};
/// # use rsdd::repr::var_order::VarOrder;
/// # use rsdd::repr::var_label::VarLabel;
/// let o = VarOrder::linear_order(2);
/// let n1 = BddNode::new(VarLabel::new(0), BddPtr::PtrTrue, BddPtr::PtrFalse);
/// let n2 = BddNode::new(VarLabel::new(1), BddPtr::PtrFalse, BddPtr::PtrTrue);
///
/// let v1 = BddPtr::Reg(&n1);
/// let v2 = BddPtr::Reg(&n2);
///
/// assert_eq!(o.first(&v1, &v2), &v1);
///
/// assert_eq!(o.first(&BddPtr::PtrTrue, &v2), &v2);
/// assert_eq!(o.first(&v1, &BddPtr::PtrFalse), &v1);
/// ```
pub fn first<'a, T: PartialVariableOrder>(&self, a: &'a T, b: &'a T) -> &'a T {
match (a.var(), b.var()) {
(None, _) => b,
(_, None) => a,
(Some(va), Some(vb)) => {
let pa = self.get(va);
let pb = self.get(vb);
if pa < pb {
a
} else {
Expand All @@ -118,18 +128,28 @@ impl VarOrder {
}
}

/// Returns a sorted pair where the BddPtr whose top variable is first
/// occurs first in the pair.
pub fn sort<'a>(&self, a: BddPtr<'a>, b: BddPtr<'a>) -> (BddPtr<'a>, BddPtr<'a>) {
match (a, b) {
(BddPtr::PtrTrue, _) | (BddPtr::PtrFalse, _) => (b, a),
(_, BddPtr::PtrTrue) | (_, BddPtr::PtrFalse) => (a, b),
(
BddPtr::Reg(node_a) | BddPtr::Compl(node_a),
BddPtr::Reg(node_b) | BddPtr::Compl(node_b),
) => {
let pa = self.get(node_a.var);
let pb = self.get(node_b.var);
/// Returns a sorted pair where the item (with a partial label) whose top variable
/// is first occurs first in the pair.
/// ```
/// # use rsdd::repr::bdd::{BddNode, BddPtr};
/// # use rsdd::repr::var_order::VarOrder;
/// # use rsdd::repr::var_label::VarLabel;
/// let o = VarOrder::linear_order(2);
/// let n1 = BddNode::new(VarLabel::new(0), BddPtr::PtrTrue, BddPtr::PtrFalse);
/// let n2 = BddNode::new(VarLabel::new(1), BddPtr::PtrFalse, BddPtr::PtrTrue);
///
/// let v1 = BddPtr::Reg(&n1);
/// let v2 = BddPtr::Reg(&n2);
///
/// assert_eq!(o.sort(&v2, &v1), (&v1, &v2));
/// ```
pub fn sort<'a, T: PartialVariableOrder>(&self, a: &'a T, b: &'a T) -> (&'a T, &'a T) {
match (a.var(), b.var()) {
(None, _) => (b, a),
(_, None) => (a, b),
(Some(va), Some(vb)) => {
let pa = self.get(va);
let pb = self.get(vb);
if pa < pb {
(a, b)
} else {
Expand Down Expand Up @@ -175,14 +195,34 @@ impl VarOrder {
}
}

/// get the first essential variable (i.e., the variable that comes first in
/// the order) among `a`, `b`, `c`
pub fn first_essential(&self, a: BddPtr, b: BddPtr, c: BddPtr) -> VarLabel {
/// get the first essential variable
/// (i.e., the variable that comes first in the order) among `a`, `b`, `c`
/// ```
/// # use rsdd::repr::bdd::{BddNode, BddPtr};
/// # use rsdd::repr::var_order::VarOrder;
/// # use rsdd::repr::var_label::VarLabel;
/// let o = VarOrder::linear_order(3);
/// let n1 = BddNode::new(VarLabel::new(0), BddPtr::PtrTrue, BddPtr::PtrFalse);
/// let n2 = BddNode::new(VarLabel::new(1), BddPtr::PtrFalse, BddPtr::PtrTrue);
/// let n3 = BddNode::new(VarLabel::new(2), BddPtr::PtrFalse, BddPtr::PtrTrue);
///
/// let v1 = BddPtr::Reg(&n1);
/// let v2 = BddPtr::Reg(&n2);
/// let v3 = BddPtr::Reg(&n3);
///
/// assert_eq!(o.first_essential(&v2, &v3, &v1), VarLabel::new(0));
/// ```
pub fn first_essential<T: PartialVariableOrder + Debug>(
&self,
a: &T,
b: &T,
c: &T,
) -> VarLabel {
let f1 = self.first(a, b);
let f2 = self.first(f1, c);
match f2 {
BddPtr::Reg(n) | BddPtr::Compl(n) => n.var,
BddPtr::PtrTrue | BddPtr::PtrFalse => panic!(
match f2.var() {
Some(v) => v,
None => panic!(
"Could not find a valid first variable among a: {:?}, b: {:?}, c: {:?}",
a, b, c
),
Expand Down Expand Up @@ -236,6 +276,15 @@ impl Display for VarOrder {
}
}

/// Structs that implement this trait expose an optional VarLabel
/// with each item. These are then used for sorting and other
/// ordering operations; None (typically reserved for constants)
/// is considered to be "greater than" other objects (i.e. comes last),
/// and no guaranteed ordering exists between None objects.
pub trait PartialVariableOrder {
fn var(&self) -> Option<VarLabel>;
}

#[test]
fn var_order_basics() {
let order = VarOrder::linear_order(10);
Expand Down

0 comments on commit 707062a

Please sign in to comment.