diff --git a/crates/oxidd-cli/src/main.rs b/crates/oxidd-cli/src/main.rs index 8f1745b..8cab4b9 100644 --- a/crates/oxidd-cli/src/main.rs +++ b/crates/oxidd-cli/src/main.rs @@ -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; @@ -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 @@ -259,20 +260,39 @@ where } } + fn balanced_reduce( + iter: impl IntoIterator, + mut f: impl for<'a> FnMut(&'a T, &'a T) -> T, + ) -> Option { + let mut buf: Vec = 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( clauses: &[B], clause_order: &ClauseOrderTree, report: impl Fn(&B) + Copy, - ) -> B { + ) -> Option { 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 + }, + ), } } @@ -280,18 +300,19 @@ where clauses: &[B], clause_order: &ClauseOrderTree, report: impl Fn(&B) + Copy + Send + Sync, - ) -> B { + ) -> Option { 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, rhs: Option| { + let conj = lhs?.and(&rhs?).expect(OOM_MSG); + report(&conj); + Some(conj) + }, + ), } } @@ -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, rhs: Option| { + 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() } } } diff --git a/crates/oxidd-parser/src/dimacs.rs b/crates/oxidd-parser/src/dimacs.rs index 7cb4d67..7fcad73 100644 --- a/crates/oxidd-parser/src/dimacs.rs +++ b/crates/oxidd-parser/src/dimacs.rs @@ -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> @@ -65,13 +65,12 @@ where fn rec<'a, E: ParseError<&'a [u8]> + ContextError<&'a [u8]>>( input: &'a [u8], inserted: &mut BitVec, + buffer: &mut Vec, ) -> 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"); @@ -86,28 +85,49 @@ where return Ok((input, (ClauseOrderTree::Clause(n), (span, n)))); } - if let Ok((input, (left, (max1_span, max1)))) = rec::(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, diff --git a/crates/oxidd-parser/src/lib.rs b/crates/oxidd-parser/src/lib.rs index f56d70c..a6ec544 100644 --- a/crates/oxidd-parser/src/lib.rs +++ b/crates/oxidd-parser/src/lib.rs @@ -208,7 +208,7 @@ impl PropProblem { #[derive(Clone, PartialEq, Eq, Debug)] pub enum ClauseOrderTree { /// Conjunction - Conj(Box, Box), + Conj(Box<[ClauseOrderTree]>), /// Clause index (starting from 0) Clause(usize), }