diff --git a/bin/bottomup_cnf_to_bdd.rs b/bin/bottomup_cnf_to_bdd.rs index ec7c5027..dc78267d 100644 --- a/bin/bottomup_cnf_to_bdd.rs +++ b/bin/bottomup_cnf_to_bdd.rs @@ -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, }; @@ -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`", diff --git a/examples/one_shot_benchmark.rs b/examples/one_shot_benchmark.rs index df607be3..c30e1d77 100644 --- a/examples/one_shot_benchmark.rs +++ b/examples/one_shot_benchmark.rs @@ -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; @@ -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::>::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 { diff --git a/src/builder/bdd/builder.rs b/src/builder/bdd/builder.rs index c9c9c8a6..30936939 100644 --- a/src/builder/bdd/builder.rs +++ b/src/builder/bdd/builder.rs @@ -1,6 +1,6 @@ use crate::{ builder::{bdd::CompiledCNF, BottomUpBuilder}, - plan::bdd_plan::BddPlan, + plan::BottomUpPlan, repr::{ bdd::{BddNode, BddPtr}, cnf::Cnf, @@ -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(), } } } diff --git a/src/plan/bdd_plan.rs b/src/plan/bottom_up_plan.rs similarity index 70% rename from src/plan/bdd_plan.rs rename to src/plan/bottom_up_plan.rs index db59883c..4f86479f 100644 --- a/src/plan/bdd_plan.rs +++ b/src/plan/bottom_up_plan.rs @@ -4,36 +4,38 @@ use crate::repr::{dtree::DTree, var_label::VarLabel}; #[derive(Debug, Clone)] -pub enum BddPlan { - And(Box, Box), - Or(Box, Box), - Iff(Box, Box), - Ite(Box, Box, Box), - Not(Box), +pub enum BottomUpPlan { + And(Box, Box), + Or(Box, Box), + Iff(Box, Box), + Ite(Box, Box, Box), + Not(Box), 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)) } @@ -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, diff --git a/src/plan/mod.rs b/src/plan/mod.rs index f1984430..71f9b38a 100644 --- a/src/plan/mod.rs +++ b/src/plan/mod.rs @@ -1 +1,3 @@ -pub mod bdd_plan; +mod bottom_up_plan; + +pub use self::bottom_up_plan::*;