Skip to content

Commit

Permalink
Rename BddPlan -> BottomUpPlan and flatten module (#157)
Browse files Browse the repository at this point in the history
Prereq for #155.
  • Loading branch information
mattxwang committed Jul 24, 2023
1 parent 974fb6a commit 97532c5
Show file tree
Hide file tree
Showing 5 changed files with 33 additions and 29 deletions.
4 changes: 2 additions & 2 deletions bin/bottomup_cnf_to_bdd.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ use rsdd::{
bdd::{BddBuilder, RobddBuilder},
cache::LruIteTable,
},
plan::bdd_plan::BddPlan,
plan::BottomUpPlan,
repr::{bdd::BddPtr, cnf::Cnf, dtree::DTree},
serialize::BDDSerializer,
};
Expand Down Expand Up @@ -55,7 +55,7 @@ fn main() {
let plan = match args.strategy.as_str() {
"dtree" => {
let dtree = DTree::from_cnf(&cnf, &order);
BddPlan::from_dtree(&dtree)
BottomUpPlan::from_dtree(&dtree)
}
_ => panic!(
"Unknown strategy {} provided, expected one of: `dtree`",
Expand Down
4 changes: 2 additions & 2 deletions examples/one_shot_benchmark.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ use rsdd::builder::cache::LruIteTable;
use rsdd::builder::decision_nnf::DecisionNNFBuilder;
use rsdd::builder::decision_nnf::StandardDecisionNNFBuilder;
use rsdd::builder::sdd::{CompressionSddBuilder, SddBuilder};
use rsdd::plan::bdd_plan::BddPlan;
use rsdd::plan::BottomUpPlan;
use rsdd::repr::bdd::BddPtr;
use rsdd::repr::cnf::Cnf;
use rsdd::repr::ddnnf::DDNNFPtr;
Expand Down Expand Up @@ -170,7 +170,7 @@ fn compile_bdd_dtree(str: String, _args: &Args) -> BenchResult {
let order = cnf.min_fill_order();
let dtree = DTree::from_cnf(&cnf, &order);
let builder = RobddBuilder::<LruIteTable<BddPtr>>::new(order);
let plan = BddPlan::from_dtree(&dtree);
let plan = BottomUpPlan::from_dtree(&dtree);
let bdd = builder.compile_plan(&plan);

if let Some(path) = &_args.dump_bdd {
Expand Down
20 changes: 10 additions & 10 deletions src/builder/bdd/builder.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
use crate::{
builder::{bdd::CompiledCNF, BottomUpBuilder},
plan::bdd_plan::BddPlan,
plan::BottomUpPlan,
repr::{
bdd::{BddNode, BddPtr},
cnf::Cnf,
Expand Down Expand Up @@ -195,36 +195,36 @@ pub trait BddBuilder<'a>: BottomUpBuilder<'a, BddPtr<'a>> {
}

/// Compiles a plan into a BDD
fn compile_plan(&'a self, expr: &BddPlan) -> BddPtr<'a> {
fn compile_plan(&'a self, expr: &BottomUpPlan) -> BddPtr<'a> {
match &expr {
BddPlan::Literal(var, polarity) => self.var(*var, *polarity),
BddPlan::And(ref l, ref r) => {
BottomUpPlan::Literal(var, polarity) => self.var(*var, *polarity),
BottomUpPlan::And(ref l, ref r) => {
let r1 = self.compile_plan(l);
let r2 = self.compile_plan(r);
self.and(r1, r2)
}
BddPlan::Or(ref l, ref r) => {
BottomUpPlan::Or(ref l, ref r) => {
let r1 = self.compile_plan(l);
let r2 = self.compile_plan(r);
self.or(r1, r2)
}
BddPlan::Iff(ref l, ref r) => {
BottomUpPlan::Iff(ref l, ref r) => {
let r1 = self.compile_plan(l);
let r2 = self.compile_plan(r);
self.iff(r1, r2)
}
BddPlan::Ite(ref f, ref g, ref h) => {
BottomUpPlan::Ite(ref f, ref g, ref h) => {
let f = self.compile_plan(f);
let g = self.compile_plan(g);
let h = self.compile_plan(h);
self.ite(f, g, h)
}
BddPlan::Not(ref f) => {
BottomUpPlan::Not(ref f) => {
let f = self.compile_plan(f);
f.neg()
}
BddPlan::ConstTrue => BddPtr::true_ptr(),
BddPlan::ConstFalse => BddPtr::false_ptr(),
BottomUpPlan::ConstTrue => BddPtr::true_ptr(),
BottomUpPlan::ConstFalse => BddPtr::false_ptr(),
}
}
}
Expand Down
30 changes: 16 additions & 14 deletions src/plan/bdd_plan.rs → src/plan/bottom_up_plan.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,36 +4,38 @@
use crate::repr::{dtree::DTree, var_label::VarLabel};

#[derive(Debug, Clone)]
pub enum BddPlan {
And(Box<BddPlan>, Box<BddPlan>),
Or(Box<BddPlan>, Box<BddPlan>),
Iff(Box<BddPlan>, Box<BddPlan>),
Ite(Box<BddPlan>, Box<BddPlan>, Box<BddPlan>),
Not(Box<BddPlan>),
pub enum BottomUpPlan {
And(Box<BottomUpPlan>, Box<BottomUpPlan>),
Or(Box<BottomUpPlan>, Box<BottomUpPlan>),
Iff(Box<BottomUpPlan>, Box<BottomUpPlan>),
Ite(Box<BottomUpPlan>, Box<BottomUpPlan>, Box<BottomUpPlan>),
Not(Box<BottomUpPlan>),
ConstTrue,
ConstFalse,
Literal(VarLabel, bool),
}

impl BddPlan {
#[allow(clippy::should_implement_trait)] // this is a naming thing; perhaps consider renaming this in the future?
pub fn not(p: BddPlan) -> Self {
impl BottomUpPlan {
// this is a naming thing; perhaps consider renaming this in the future?
// (but, both not and neg are std::ops, so you'll hit this clippy with both natural choices)
#[allow(clippy::should_implement_trait)]
pub fn not(p: BottomUpPlan) -> Self {
Self::Not(Box::new(p))
}

pub fn and(p1: BddPlan, p2: BddPlan) -> Self {
pub fn and(p1: BottomUpPlan, p2: BottomUpPlan) -> Self {
Self::And(Box::new(p1), Box::new(p2))
}

pub fn or(p1: BddPlan, p2: BddPlan) -> Self {
pub fn or(p1: BottomUpPlan, p2: BottomUpPlan) -> Self {
Self::Or(Box::new(p1), Box::new(p2))
}

pub fn iff(p1: BddPlan, p2: BddPlan) -> Self {
pub fn iff(p1: BottomUpPlan, p2: BottomUpPlan) -> Self {
Self::Iff(Box::new(p1), Box::new(p2))
}

pub fn ite(pc: BddPlan, pt: BddPlan, pf: BddPlan) -> Self {
pub fn ite(pc: BottomUpPlan, pt: BottomUpPlan, pf: BottomUpPlan) -> Self {
Self::Ite(Box::new(pc), Box::new(pt), Box::new(pf))
}

Expand All @@ -58,7 +60,7 @@ impl BddPlan {
/// &&
/// / \
/// (A ∨ B) (B ∨ C)
pub fn from_dtree(dtree: &DTree) -> BddPlan {
pub fn from_dtree(dtree: &DTree) -> BottomUpPlan {
match dtree {
DTree::Node {
l,
Expand Down
4 changes: 3 additions & 1 deletion src/plan/mod.rs
Original file line number Diff line number Diff line change
@@ -1 +1,3 @@
pub mod bdd_plan;
mod bottom_up_plan;

pub use self::bottom_up_plan::*;

0 comments on commit 97532c5

Please sign in to comment.