use std::fmt::{self, Write};
use rustc_hash::FxHashSet;
use crate::{CfgAtom, CfgDiff, CfgExpr, CfgOptions, InactiveReason};
pub struct DnfExpr {
conjunctions: Vec<Conjunction>,
}
struct Conjunction {
literals: Vec<Literal>,
}
struct Literal {
negate: bool,
var: Option<CfgAtom>, }
impl DnfExpr {
pub fn new(expr: &CfgExpr) -> Self {
let builder = Builder { expr: DnfExpr { conjunctions: Vec::new() } };
builder.lower(expr)
}
pub fn why_inactive(&self, opts: &CfgOptions) -> Option<InactiveReason> {
let mut res = InactiveReason { enabled: Vec::new(), disabled: Vec::new() };
for conj in &self.conjunctions {
let mut conj_is_true = true;
for lit in &conj.literals {
let atom = lit.var.as_ref()?;
let enabled = opts.enabled.contains(atom);
if lit.negate == enabled {
conj_is_true = false;
if enabled {
res.enabled.push(atom.clone());
} else {
res.disabled.push(atom.clone());
}
}
}
if conj_is_true {
return None;
}
}
res.enabled.sort_unstable_by(compare);
res.enabled.dedup();
res.disabled.sort_unstable_by(compare);
res.disabled.dedup();
Some(res)
}
pub fn compute_enable_hints<'a>(
&'a self,
opts: &'a CfgOptions,
) -> impl Iterator<Item = CfgDiff> + 'a {
self.conjunctions.iter().filter_map(move |conj| {
let mut enable = FxHashSet::default();
let mut disable = FxHashSet::default();
for lit in &conj.literals {
let atom = lit.var.as_ref()?;
let enabled = opts.enabled.contains(atom);
if lit.negate && enabled {
disable.insert(atom.clone());
}
if !lit.negate && !enabled {
enable.insert(atom.clone());
}
}
for lit in &conj.literals {
let atom = lit.var.as_ref()?;
let enabled = enable.contains(atom)
|| (opts.enabled.contains(atom) && !disable.contains(atom));
if enabled == lit.negate {
return None;
}
}
if enable.is_empty() && disable.is_empty() {
return None;
}
let mut diff = CfgDiff {
enable: enable.into_iter().collect(),
disable: disable.into_iter().collect(),
};
diff.enable.sort_unstable_by(compare);
diff.disable.sort_unstable_by(compare);
Some(diff)
})
}
}
fn compare(a: &CfgAtom, b: &CfgAtom) -> std::cmp::Ordering {
match (a, b) {
(CfgAtom::Flag(a), CfgAtom::Flag(b)) => a.as_str().cmp(b.as_str()),
(CfgAtom::Flag(_), CfgAtom::KeyValue { .. }) => std::cmp::Ordering::Less,
(CfgAtom::KeyValue { .. }, CfgAtom::Flag(_)) => std::cmp::Ordering::Greater,
(CfgAtom::KeyValue { key, value }, CfgAtom::KeyValue { key: key2, value: value2 }) => {
key.as_str().cmp(key2.as_str()).then(value.as_str().cmp(value2.as_str()))
}
}
}
impl fmt::Display for DnfExpr {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
if self.conjunctions.len() != 1 {
f.write_str("any(")?;
}
for (i, conj) in self.conjunctions.iter().enumerate() {
if i != 0 {
f.write_str(", ")?;
}
conj.fmt(f)?;
}
if self.conjunctions.len() != 1 {
f.write_char(')')?;
}
Ok(())
}
}
impl Conjunction {
fn new(parts: Box<[CfgExpr]>) -> Self {
let mut literals = Vec::new();
for part in parts.into_vec() {
match part {
CfgExpr::Invalid | CfgExpr::Atom(_) | CfgExpr::Not(_) => {
literals.push(Literal::new(part));
}
CfgExpr::All(conj) => {
literals.extend(Conjunction::new(conj).literals);
}
CfgExpr::Any(_) => unreachable!("disjunction in conjunction"),
}
}
Self { literals }
}
}
impl fmt::Display for Conjunction {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
if self.literals.len() != 1 {
f.write_str("all(")?;
}
for (i, lit) in self.literals.iter().enumerate() {
if i != 0 {
f.write_str(", ")?;
}
lit.fmt(f)?;
}
if self.literals.len() != 1 {
f.write_str(")")?;
}
Ok(())
}
}
impl Literal {
fn new(expr: CfgExpr) -> Self {
match expr {
CfgExpr::Invalid => Self { negate: false, var: None },
CfgExpr::Atom(atom) => Self { negate: false, var: Some(atom) },
CfgExpr::Not(expr) => match *expr {
CfgExpr::Invalid => Self { negate: true, var: None },
CfgExpr::Atom(atom) => Self { negate: true, var: Some(atom) },
_ => unreachable!("non-atom {:?}", expr),
},
CfgExpr::Any(_) | CfgExpr::All(_) => unreachable!("non-literal {:?}", expr),
}
}
}
impl fmt::Display for Literal {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
if self.negate {
write!(f, "not(")?;
}
match &self.var {
Some(var) => var.fmt(f)?,
None => f.write_str("<invalid>")?,
}
if self.negate {
f.write_char(')')?;
}
Ok(())
}
}
struct Builder {
expr: DnfExpr,
}
impl Builder {
fn lower(mut self, expr: &CfgExpr) -> DnfExpr {
let expr = make_nnf(expr);
let expr = make_dnf(expr);
match expr {
CfgExpr::Invalid | CfgExpr::Atom(_) | CfgExpr::Not(_) => {
self.expr.conjunctions.push(Conjunction::new(Box::new([expr])));
}
CfgExpr::All(conj) => {
self.expr.conjunctions.push(Conjunction::new(conj));
}
CfgExpr::Any(disj) => {
let mut disj = disj.into_vec();
disj.reverse();
while let Some(conj) = disj.pop() {
match conj {
CfgExpr::Invalid | CfgExpr::Atom(_) | CfgExpr::All(_) | CfgExpr::Not(_) => {
self.expr.conjunctions.push(Conjunction::new(Box::new([conj])));
}
CfgExpr::Any(inner_disj) => {
disj.extend(inner_disj.into_vec().into_iter().rev());
}
}
}
}
}
self.expr
}
}
fn make_dnf(expr: CfgExpr) -> CfgExpr {
match expr {
CfgExpr::Invalid | CfgExpr::Atom(_) | CfgExpr::Not(_) => expr,
CfgExpr::Any(e) => flatten(CfgExpr::Any(e.into_vec().into_iter().map(make_dnf).collect())),
CfgExpr::All(e) => {
let e = e.into_vec().into_iter().map(make_dnf).collect::<Vec<_>>();
flatten(CfgExpr::Any(distribute_conj(&e).into_boxed_slice()))
}
}
}
fn distribute_conj(conj: &[CfgExpr]) -> Vec<CfgExpr> {
fn go(out: &mut Vec<CfgExpr>, with: &mut Vec<CfgExpr>, rest: &[CfgExpr]) {
match rest {
[head, tail @ ..] => match head {
CfgExpr::Any(disj) => {
for part in disj.iter() {
with.push(part.clone());
go(out, with, tail);
with.pop();
}
}
_ => {
with.push(head.clone());
go(out, with, tail);
with.pop();
}
},
_ => {
out.push(CfgExpr::All(with.clone().into_boxed_slice()));
}
}
}
let mut out = Vec::new(); let mut with = Vec::new();
go(&mut out, &mut with, conj);
out
}
fn make_nnf(expr: &CfgExpr) -> CfgExpr {
match expr {
CfgExpr::Invalid | CfgExpr::Atom(_) => expr.clone(),
CfgExpr::Any(expr) => CfgExpr::Any(expr.iter().map(make_nnf).collect()),
CfgExpr::All(expr) => CfgExpr::All(expr.iter().map(make_nnf).collect()),
CfgExpr::Not(operand) => make_nnf_neg(operand),
}
}
fn make_nnf_neg(operand: &CfgExpr) -> CfgExpr {
match operand {
CfgExpr::Invalid => CfgExpr::Not(Box::new(CfgExpr::Invalid)), CfgExpr::Atom(atom) => CfgExpr::Not(Box::new(CfgExpr::Atom(atom.clone()))),
CfgExpr::Not(expr) => make_nnf(expr),
CfgExpr::Any(inner) => CfgExpr::All(inner.iter().map(make_nnf_neg).collect()),
CfgExpr::All(inner) => CfgExpr::Any(inner.iter().map(make_nnf_neg).collect()),
}
}
fn flatten(expr: CfgExpr) -> CfgExpr {
match expr {
CfgExpr::All(inner) => CfgExpr::All(
inner
.iter()
.flat_map(|e| match e {
CfgExpr::All(inner) => inner.as_ref(),
_ => std::slice::from_ref(e),
})
.cloned()
.collect(),
),
CfgExpr::Any(inner) => CfgExpr::Any(
inner
.iter()
.flat_map(|e| match e {
CfgExpr::Any(inner) => inner.as_ref(),
_ => std::slice::from_ref(e),
})
.cloned()
.collect(),
),
_ => expr,
}
}