Skip to content

Commit

Permalink
Allow arbitrary arity trees when specifying the clause order
Browse files Browse the repository at this point in the history
  • Loading branch information
@nhusung
nhusung committed Jul 2, 2024
1 parent 8a74879 commit 75d8e04
Show file tree
Hide file tree
Showing 3 changed files with 100 additions and 69 deletions.
107 changes: 59 additions & 48 deletions crates/oxidd-cli/src/main.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ use oxidd_parser::Problem;
use oxidd_parser::Prop;
use oxidd_parser::Var;
use rayon::iter::IntoParallelIterator;
use rayon::iter::ParallelIterator;
use rustc_hash::FxHashMap;
use rustc_hash::FxHasher;

Expand Down Expand Up @@ -88,7 +89,7 @@ struct Cli {
read_var_order: bool,

/// Order in which to apply operations when building a CNF
#[arg(value_enum, long, default_value_t = CNFBuildOrder::LeftDeep)]
#[arg(value_enum, long, default_value_t = CNFBuildOrder::Balanced)]
cnf_build_order: CNFBuildOrder,

/// For every conjunction operation in a CNF, compute and print the DD's
Expand Down Expand Up @@ -259,39 +260,59 @@ where
}
}

fn balanced_reduce<T>(
iter: impl IntoIterator<Item = T>,
mut f: impl for<'a> FnMut(&'a T, &'a T) -> T,
) -> Option<T> {
let mut buf: Vec<T> = iter.into_iter().collect();
let mut step = 1;
while step < buf.len() {
let mut i = 0;
while i + step < buf.len() {
buf[i] = f(&buf[i], &buf[i + step]);
i += 2 * step;
}
step *= 2;
}
buf.into_iter().next()
}

fn clause_tree_rec<B: BooleanFunction>(
clauses: &[B],
clause_order: &ClauseOrderTree,
report: impl Fn(&B) + Copy,
) -> B {
) -> Option<B> {
match clause_order {
ClauseOrderTree::Clause(n) => clauses[*n].clone(),
ClauseOrderTree::Conj(lhs, rhs) => {
let lhs = clause_tree_rec(clauses, lhs, report);
let rhs = clause_tree_rec(clauses, rhs, report);
let conj = lhs.and(&rhs).expect(OOM_MSG);
report(&conj);
conj
}
ClauseOrderTree::Clause(n) => Some(clauses[*n].clone()),
ClauseOrderTree::Conj(sub) => balanced_reduce(
sub.iter()
.filter_map(|t| clause_tree_rec(clauses, t, report)),
|lhs: &B, rhs: &B| {
let conj = lhs.and(rhs).expect(OOM_MSG);
report(&conj);
conj
},
),
}
}

fn clause_tree_par_rec<B: BooleanFunction + Send + Sync>(
clauses: &[B],
clause_order: &ClauseOrderTree,
report: impl Fn(&B) + Copy + Send + Sync,
) -> B {
) -> Option<B> {
match clause_order {
ClauseOrderTree::Clause(n) => clauses[*n].clone(),
ClauseOrderTree::Conj(lhs, rhs) => {
let (lhs, rhs) = rayon::join(
|| clause_tree_rec(clauses, lhs, report),
|| clause_tree_rec(clauses, rhs, report),
);
let conj = lhs.and(&rhs).expect(OOM_MSG);
report(&conj);
conj
}
ClauseOrderTree::Clause(n) => Some(clauses[*n].clone()),
ClauseOrderTree::Conj(sub) => ParallelIterator::reduce(
sub.into_par_iter()
.map(|t| clause_tree_rec(clauses, t, report)),
|| None,
|lhs: Option<B>, rhs: Option<B>| {
let conj = lhs?.and(&rhs?).expect(OOM_MSG);
report(&conj);
Some(conj)
},
),
}
}

Expand Down Expand Up @@ -394,38 +415,28 @@ where
res
})
}
CNFBuildOrder::Balanced => {
let mut clauses = clauses;
let mut step = 1;
while step < clauses.len() {
let mut i = 0;
while i + step < clauses.len() {
clauses[i] = clauses[i].and(&clauses[i + step]).expect(OOM_MSG);
report(&clauses[i]);
i += 2 * step;
}
step *= 2;
}
clauses.into_iter().next().unwrap()
}
CNFBuildOrder::WorkStealing => rayon::iter::ParallelIterator::reduce(
clauses.into_par_iter(),
|| B::t(manager),
|acc, f| {
if acc.valid() {
f
} else {
let res = acc.and(&f).expect(OOM_MSG);
report(&res);
res
}
CNFBuildOrder::Balanced => balanced_reduce(clauses, |lhs: &B, rhs: &B| {
let conj = lhs.and(rhs).expect(OOM_MSG);
report(&conj);
conj
})
.unwrap(),
CNFBuildOrder::WorkStealing => ParallelIterator::reduce(
clauses.into_par_iter().map(|c| Some(c)),
|| None,
|lhs: Option<B>, rhs: Option<B>| {
let res = lhs?.and(&rhs?).expect(OOM_MSG);
report(&res);
Some(res)
},
),
)
.unwrap(),
CNFBuildOrder::Tree => {
clause_tree_rec(&clauses, cnf.clause_order().unwrap(), report)
clause_tree_rec(&clauses, cnf.clause_order().unwrap(), report).unwrap()
}
CNFBuildOrder::TreeParallel => {
clause_tree_par_rec(&clauses, cnf.clause_order().unwrap(), report)
.unwrap()
}
}
}
Expand Down
60 changes: 40 additions & 20 deletions crates/oxidd-parser/src/dimacs.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,10 +52,10 @@ fn comment<'a, E: ParseError<&'a [u8]>>(input: &'a [u8]) -> IResult<&'a [u8], ()

/// Parse a clause order, e.g.:
///
/// `[0, [2, 3]]`
/// `[0, [2, 3, 1]]`
///
/// Returns a pre-linearized clause order (tree), as well as the maximal clause
/// number and its span.
/// Returns clause order (tree), as well as the maximal clause number and its
/// span.
fn clause_order<'a, E>(
input: &'a [u8],
) -> IResult<&'a [u8], (ClauseOrderTree, (&'a [u8], usize)), E>
Expand All @@ -65,13 +65,12 @@ where
fn rec<'a, E: ParseError<&'a [u8]> + ContextError<&'a [u8]>>(
input: &'a [u8],
inserted: &mut BitVec,
buffer: &mut Vec<ClauseOrderTree>,
) -> IResult<&'a [u8], (ClauseOrderTree, (&'a [u8], usize)), E> {
let (input, _) = space0(input)?;
let (input, _) = char('[')(input)?;
let (input, _) = space0(input)?;
debug_assert!(space0::<_, E>(input).is_err());

if let Ok((input, (span, n))) = consumed(u64::<_, E>)(input) {
let (input, _) = space0(input)?;
let (input, _) = char(']')(input)?;

if n > MAX_CAPACITY {
return fail(span, "clause number too large");
Expand All @@ -86,28 +85,49 @@ where
return Ok((input, (ClauseOrderTree::Clause(n), (span, n))));
}

if let Ok((input, (left, (max1_span, max1)))) = rec::<E>(input, inserted) {
let (input, _) = space0(input)?;
let (input, _) = char(',')(input)?;
let (input, _) = space0(input)?;
let (input, (right, (max2_span, max2))) = rec(input, inserted)?;
let (input, _) = space0(input)?;
let (input, _) = char(']')(input)?;
if let Ok((mut input, _)) = char::<_, E>('[')(input) {
(input, _) = space0(input)?;
let buffer_pos = buffer.len();
let mut max_span = [].as_slice();
let mut max = 0;

let input = loop {
(input, _) = space0(input)?;
if let [b']', r @ ..] = input {
break r;
}
let (i, (sub, (sub_max_span, sub_max))) = rec(input, inserted, buffer)?;
buffer.push(sub);
if sub_max >= max {
max = sub_max;
max_span = sub_max_span;
}

(input, _) = space0(i)?;
match input {
[b']', r @ ..] => break r,
[b',', r @ ..] => input = r,
_ => return fail(input, "expected ',' or ']'"),
}
};

let conj = ClauseOrderTree::Conj(Box::new(left), Box::new(right));
let max = if max1 >= max2 {
(max1_span, max1)
let t = if buffer.len() == buffer_pos + 1 {
// flatten `[42]` into `42`
buffer.pop().unwrap()
} else {
(max2_span, max2)
ClauseOrderTree::Conj(buffer.split_off(buffer_pos).into_boxed_slice())
};
return Ok((input, (conj, max)));
return Ok((input, (t, (max_span, max))));
}

fail(word_span(input), "expected '[' or a clause number")
}

let mut inserted = BitVec::new();
let (input, (span, res)) = cut(consumed(|input| rec(input, &mut inserted)))(input)?;
let (input, _) = space0(input)?;
let (input, (span, res)) = cut(consumed(|input| {
rec(input, &mut inserted, &mut Vec::with_capacity(65536))
}))(input)?;
if let Some(n) = inserted.first_zero() {
return Err(Err::Failure(E::from_external_error(
span,
Expand Down
2 changes: 1 addition & 1 deletion crates/oxidd-parser/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -208,7 +208,7 @@ impl PropProblem {
#[derive(Clone, PartialEq, Eq, Debug)]
pub enum ClauseOrderTree {
/// Conjunction
Conj(Box<ClauseOrderTree>, Box<ClauseOrderTree>),
Conj(Box<[ClauseOrderTree]>),
/// Clause index (starting from 0)
Clause(usize),
}
Expand Down

0 comments on commit 75d8e04

Please sign in to comment.