Skip to content

Commit

Permalink
Move shared compile_* to BottomUpBuilder (#158)
Browse files Browse the repository at this point in the history 
Now, the SDD builder gets quite a bit of behaviour for free!

(also, renames `from_boolexpr` to `from_logical_expr` for consistency)
  • Loading branch information
@mattxwang
mattxwang authored Jul 24, 2023
1 parent 97532c5 commit e364f2f
Show file tree
Hide file tree
Showing 9 changed files with 211 additions and 251 deletions.
5 changes: 1 addition & 4 deletions bin/bottomup_cnf_to_bdd.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,7 @@ use std::{fs, time::Instant};

use clap::Parser;
use rsdd::{
builder::{
bdd::{BddBuilder, RobddBuilder},
cache::LruIteTable,
},
builder::{bdd::RobddBuilder, cache::LruIteTable, BottomUpBuilder},
plan::BottomUpPlan,
repr::{bdd::BddPtr, cnf::Cnf, dtree::DTree},
serialize::BDDSerializer,
Expand Down
5 changes: 1 addition & 4 deletions examples/marginal_map_experiment.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,7 @@ use std::{collections::HashMap, fs};
use clap::Parser;
use rand::Rng;
use rsdd::{
builder::{
bdd::{BddBuilder, RobddBuilder},
cache::AllIteTable,
},
builder::{bdd::RobddBuilder, cache::AllIteTable, BottomUpBuilder},
repr::{bdd::BddPtr, cnf::Cnf, var_label::VarLabel, wmc::WmcParams},
util::semirings::RealSemiring,
};
Expand Down
2 changes: 1 addition & 1 deletion examples/one_shot_benchmark.rs
View file
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
use clap::Parser;
use rsdd::builder::bdd::BddBuilder;
use rsdd::builder::bdd::RobddBuilder;
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::builder::BottomUpBuilder;
use rsdd::plan::BottomUpPlan;
use rsdd::repr::bdd::BddPtr;
use rsdd::repr::cnf::Cnf;
Expand Down
192 changes: 60 additions & 132 deletions src/builder/bdd/builder.rs
View file
Original file line number Diff line number Diff line change
@@ -1,11 +1,9 @@
use crate::{
builder::{bdd::CompiledCNF, BottomUpBuilder},
plan::BottomUpPlan,
repr::{
bdd::{BddNode, BddPtr},
cnf::Cnf,
ddnnf::DDNNFPtr,
logical_expr::LogicalExpr,
model::PartialModel,
var_label::VarLabel,
},
Expand Down Expand Up @@ -81,66 +79,6 @@ pub trait BddBuilder<'a>: BottomUpBuilder<'a, BddPtr<'a>> {
ptr
}

/// Compile a BDD from a CNF
fn compile_cnf(&'a self, cnf: &Cnf) -> BddPtr<'a> {
let mut cvec: Vec<BddPtr> = Vec::with_capacity(cnf.clauses().len());
if cnf.clauses().is_empty() {
return BddPtr::true_ptr();
}
// check if there is an empty clause -- if so, UNSAT
if cnf.clauses().iter().any(|x| x.is_empty()) {
return BddPtr::false_ptr();
}

// sort the clauses based on a best-effort bottom-up ordering of clauses
let mut cnf_sorted = cnf.clauses().to_vec();
cnf_sorted.sort_by(|c1, c2| {
// order the clause with the first-most variable last
let fst1 = c1
.iter()
.max_by(|l1, l2| {
if self.less_than(l1.label(), l2.label()) {
Ordering::Less
} else {
Ordering::Equal
}
})
.unwrap();
let fst2 = c2
.iter()
.max_by(|l1, l2| {
if self.less_than(l1.label(), l2.label()) {
Ordering::Less
} else {
Ordering::Equal
}
})
.unwrap();
if self.less_than(fst1.label(), fst2.label()) {
Ordering::Less
} else {
Ordering::Equal
}
});

for lit_vec in cnf_sorted.iter() {
let (vlabel, val) = (lit_vec[0].label(), lit_vec[0].polarity());
let mut bdd = self.var(vlabel, val);
for lit in lit_vec {
let (vlabel, val) = (lit.label(), lit.polarity());
let var = self.var(vlabel, val);
bdd = self.or(bdd, var);
}
cvec.push(bdd);
}
// now cvec has a list of all the clauses; collapse it down
let r = self.collapse_clauses(&cvec);
match r {
None => BddPtr::true_ptr(),
Some(x) => x,
}
}

fn collapse_clauses(&'a self, vec: &[BddPtr<'a>]) -> Option<BddPtr<'a>> {
if vec.is_empty() {
None
Expand All @@ -157,76 +95,6 @@ pub trait BddBuilder<'a>: BottomUpBuilder<'a, BddPtr<'a>> {
}
}
}
fn compile_boolexpr(&'a self, expr: &LogicalExpr) -> BddPtr<'a> {
match &expr {
LogicalExpr::Literal(lbl, polarity) => self.var(VarLabel::new(*lbl as u64), *polarity),
LogicalExpr::And(ref l, ref r) => {
let r1 = self.compile_boolexpr(l);
let r2 = self.compile_boolexpr(r);
self.and(r1, r2)
}
LogicalExpr::Or(ref l, ref r) => {
let r1 = self.compile_boolexpr(l);
let r2 = self.compile_boolexpr(r);
self.or(r1, r2)
}
LogicalExpr::Not(ref e) => self.compile_boolexpr(e).neg(),
LogicalExpr::Iff(ref l, ref r) => {
let r1 = self.compile_boolexpr(l);
let r2 = self.compile_boolexpr(r);
self.iff(r1, r2)
}
LogicalExpr::Xor(ref l, ref r) => {
let r1 = self.compile_boolexpr(l);
let r2 = self.compile_boolexpr(r);
self.xor(r1, r2)
}
LogicalExpr::Ite {
ref guard,
ref thn,
ref els,
} => {
let g = self.compile_boolexpr(guard);
let t = self.compile_boolexpr(thn);
let e = self.compile_boolexpr(els);
self.ite(g, t, e)
}
}
}

/// Compiles a plan into a BDD
fn compile_plan(&'a self, expr: &BottomUpPlan) -> BddPtr<'a> {
match &expr {
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)
}
BottomUpPlan::Or(ref l, ref r) => {
let r1 = self.compile_plan(l);
let r2 = self.compile_plan(r);
self.or(r1, r2)
}
BottomUpPlan::Iff(ref l, ref r) => {
let r1 = self.compile_plan(l);
let r2 = self.compile_plan(r);
self.iff(r1, r2)
}
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)
}
BottomUpPlan::Not(ref f) => {
let f = self.compile_plan(f);
f.neg()
}
BottomUpPlan::ConstTrue => BddPtr::true_ptr(),
BottomUpPlan::ConstFalse => BddPtr::false_ptr(),
}
}
}

impl<'a, T> BottomUpBuilder<'a, BddPtr<'a>> for T
Expand Down Expand Up @@ -317,4 +185,64 @@ where

self.exists(a, lbl)
}

/// Compile a BDD from a CNF
fn compile_cnf(&'a self, cnf: &Cnf) -> BddPtr<'a> {
let mut cvec: Vec<BddPtr> = Vec::with_capacity(cnf.clauses().len());
if cnf.clauses().is_empty() {
return BddPtr::true_ptr();
}
// check if there is an empty clause -- if so, UNSAT
if cnf.clauses().iter().any(|x| x.is_empty()) {
return BddPtr::false_ptr();
}

// sort the clauses based on a best-effort bottom-up ordering of clauses
let mut cnf_sorted = cnf.clauses().to_vec();
cnf_sorted.sort_by(|c1, c2| {
// order the clause with the first-most variable last
let fst1 = c1
.iter()
.max_by(|l1, l2| {
if self.less_than(l1.label(), l2.label()) {
Ordering::Less
} else {
Ordering::Equal
}
})
.unwrap();
let fst2 = c2
.iter()
.max_by(|l1, l2| {
if self.less_than(l1.label(), l2.label()) {
Ordering::Less
} else {
Ordering::Equal
}
})
.unwrap();
if self.less_than(fst1.label(), fst2.label()) {
Ordering::Less
} else {
Ordering::Equal
}
});

for lit_vec in cnf_sorted.iter() {
let (vlabel, val) = (lit_vec[0].label(), lit_vec[0].polarity());
let mut bdd = self.var(vlabel, val);
for lit in lit_vec {
let (vlabel, val) = (lit.label(), lit.polarity());
let var = self.var(vlabel, val);
bdd = self.or(bdd, var);
}
cvec.push(bdd);
}
// now cvec has a list of all the clauses; collapse it down
let r = self.collapse_clauses(&cvec);
match r {
None => BddPtr::true_ptr(),
Some(x) => x,
}
}
}
1 change: 0 additions & 1 deletion src/builder/bdd/robdd.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -318,7 +318,6 @@ mod tests {
use std::borrow::Borrow;
use std::collections::HashMap;

use crate::builder::bdd::builder::BddBuilder;
use crate::builder::BottomUpBuilder;
use crate::repr::wmc::WmcParams;
use crate::util::semirings::{FiniteField, RealSemiring};
Expand Down
82 changes: 81 additions & 1 deletion src/builder/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,10 @@ pub mod bdd;
pub mod decision_nnf;
pub mod sdd;

use crate::repr::var_label::VarLabel;
use crate::{
plan::BottomUpPlan,
repr::{cnf::Cnf, logical_expr::LogicalExpr, var_label::VarLabel},
};

pub trait BottomUpBuilder<'a, Ptr> {
// constants --- can elide the input lifetimes
Expand Down Expand Up @@ -48,6 +51,83 @@ pub trait BottomUpBuilder<'a, Ptr> {
/// compose g into f for variable v
/// I.e., computes the logical function (exists v. (g <=> v) /\ f).
fn compose(&'a self, f: Ptr, lbl: VarLabel, g: Ptr) -> Ptr;

// compilation

/// directly compile a CNF
fn compile_cnf(&'a self, cnf: &Cnf) -> Ptr;

/// directly compile a logical expression
fn compile_logical_expr(&'a self, expr: &LogicalExpr) -> Ptr {
match &expr {
LogicalExpr::Literal(lbl, polarity) => self.var(VarLabel::new(*lbl as u64), *polarity),
LogicalExpr::And(ref l, ref r) => {
let r1 = self.compile_logical_expr(l);
let r2 = self.compile_logical_expr(r);
self.and(r1, r2)
}
LogicalExpr::Or(ref l, ref r) => {
let r1 = self.compile_logical_expr(l);
let r2 = self.compile_logical_expr(r);
self.or(r1, r2)
}
LogicalExpr::Not(ref e) => self.negate(self.compile_logical_expr(e)),
LogicalExpr::Iff(ref l, ref r) => {
let r1 = self.compile_logical_expr(l);
let r2 = self.compile_logical_expr(r);
self.iff(r1, r2)
}
LogicalExpr::Xor(ref l, ref r) => {
let r1 = self.compile_logical_expr(l);
let r2 = self.compile_logical_expr(r);
self.xor(r1, r2)
}
LogicalExpr::Ite {
ref guard,
ref thn,
ref els,
} => {
let g = self.compile_logical_expr(guard);
let t = self.compile_logical_expr(thn);
let e = self.compile_logical_expr(els);
self.ite(g, t, e)
}
}
}

/// Compiles from a BottomUpPlan, which represents a deferred computation
fn compile_plan(&'a self, expr: &BottomUpPlan) -> Ptr {
match &expr {
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)
}
BottomUpPlan::Or(ref l, ref r) => {
let r1 = self.compile_plan(l);
let r2 = self.compile_plan(r);
self.or(r1, r2)
}
BottomUpPlan::Iff(ref l, ref r) => {
let r1 = self.compile_plan(l);
let r2 = self.compile_plan(r);
self.iff(r1, r2)
}
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)
}
BottomUpPlan::Not(ref f) => {
let f = self.compile_plan(f);
self.negate(f)
}
BottomUpPlan::ConstTrue => self.true_ptr(),
BottomUpPlan::ConstFalse => self.false_ptr(),
}
}
}

pub trait TopDownBuilder<'a, Ptr> {
Expand Down
Loading

0 comments on commit e364f2f

Please sign in to comment.