use std::sync::OnceLock;
use super::{Fin, PassKind, Runner, Step, Stop, finish, worth_building};
use crate::engine::budget::Counter;
use crate::expr::{Context, OpCode};
use crate::ops::{BinOp, UnOp};
const VARS: [u8; 3] = [0xAA, 0xCC, 0xF0];
#[derive(Copy, Clone, Debug, PartialEq, Eq)]
pub(crate) enum T {
Var(u8),
Zero,
Ones,
Not(u16),
Bin(BinOp, u16, u16),
}
pub(crate) struct MinForms {
pub(crate) forms: Vec<(Vec<T>, u8)>,
#[cfg_attr(not(feature = "mba"), allow(dead_code))]
pub(crate) alts: Vec<Vec<Vec<T>>>,
}
pub(crate) const ALTERNATIVES: usize = 8;
pub(crate) fn min_forms() -> &'static MinForms {
static FORMS: OnceLock<MinForms> = OnceLock::new();
FORMS.get_or_init(search)
}
fn search() -> MinForms {
let mut best: Vec<Option<(Vec<T>, u8)>> = vec![None; 256];
let mut alts: Vec<Vec<Vec<T>>> = vec![Vec::new(); 256];
let mut covered: Vec<Vec<u8>> = vec![Vec::new(); 256];
best[0x00] = Some((vec![T::Zero], 0));
best[0xFF] = Some((vec![T::Ones], 0));
for (k, &v) in VARS.iter().enumerate() {
best[v as usize] = Some((vec![T::Var(k as u8)], 0));
}
let concat = |a: &[T], b: &[T], op: BinOp| -> Vec<T> {
let off = a.len() as u16;
let mut out = a.to_vec();
out.extend(b.iter().map(|t| match *t {
T::Not(x) => T::Not(x + off),
T::Bin(o, x, y) => T::Bin(o, x + off, y + off),
other => other,
}));
out.push(T::Bin(op, off - 1, out.len() as u16 - 1));
out
};
let mut size = 1u8;
while best.iter().any(Option::is_none) {
let mut found: Vec<(usize, Vec<T>)> = Vec::new();
for f in 0..256usize {
let Some((tf, sf)) = &best[f] else { continue };
if *sf + 1 == size {
let mut t = tf.clone();
t.push(T::Not(t.len() as u16 - 1));
found.push((!(f as u8) as usize, t));
}
for (g, bg) in best.iter().enumerate().skip(f) {
let Some((tg, sg)) = bg else { continue };
if sf + sg + 1 != size {
continue;
}
for (op, v) in [(BinOp::And, f & g), (BinOp::Or, f | g), (BinOp::Xor, f ^ g)] {
found.push((v, concat(tf, tg, op)));
}
}
}
let fresh: Vec<bool> = best.iter().map(Option::is_none).collect();
let all = |f: usize| -> Vec<&Vec<T>> {
best[f]
.iter()
.map(|(t, _)| t)
.chain(alts[f].iter())
.collect()
};
let mut more: Vec<(usize, Vec<T>)> = Vec::new();
for f in 0..256usize {
let Some((_, sf)) = &best[f] else { continue };
if *sf + 1 == size && fresh[usize::from(!(f as u8))] {
for tf in all(f).into_iter().skip(1) {
let mut t = tf.clone();
t.push(T::Not(t.len() as u16 - 1));
more.push((usize::from(!(f as u8)), t));
}
}
for (g, bg) in best.iter().enumerate().skip(f) {
let Some((_, sg)) = bg else { continue };
if sf + sg + 1 != size {
continue;
}
for (op, v) in [(BinOp::And, f & g), (BinOp::Or, f | g), (BinOp::Xor, f ^ g)] {
if !fresh[v] {
continue;
}
for (i, tf) in all(f).into_iter().enumerate() {
for (j, tg) in all(g).into_iter().enumerate() {
if i > 0 || j > 0 {
more.push((v, concat(tf, tg, op)));
}
}
}
}
}
}
found.extend(more);
for (v, t) in found {
if best[v].is_none() {
covered[v] = subtables(&t);
best[v] = Some((t, size));
} else if fresh[v] && alts[v].len() < 2 * ALTERNATIVES && !alts[v].contains(&t) {
let subs = subtables(&t);
let new = subs.iter().any(|s| !covered[v].contains(s));
if alts[v].len() < ALTERNATIVES && best[v].as_ref().is_some_and(|(b, _)| *b != t)
|| new
{
covered[v].extend(subs);
alts[v].push(t);
}
}
}
size += 1;
}
MinForms {
forms: best
.into_iter()
.map(|b| b.unwrap_or((vec![T::Zero], 0)))
.collect(),
alts,
}
}
pub(crate) fn subtables(t: &[T]) -> Vec<u8> {
let mut vals: Vec<u8> = Vec::with_capacity(t.len());
for n in t {
vals.push(match *n {
T::Var(k) => VARS[usize::from(k)],
T::Zero => 0,
T::Ones => 0xFF,
T::Not(a) => !vals[usize::from(a)],
T::Bin(op, a, b) => {
let (x, y) = (vals[usize::from(a)], vals[usize::from(b)]);
match op {
BinOp::And => x & y,
BinOp::Or => x | y,
_ => x ^ y,
}
}
});
}
let mut out: Vec<u8> = t
.iter()
.zip(&vals)
.take(t.len().saturating_sub(1))
.filter(|(n, _)| matches!(n, T::Not(_) | T::Bin(..)))
.map(|(_, &v)| v)
.collect();
out.sort_unstable();
out.dedup();
out
}
pub(crate) type Info = Option<(Vec<u32>, u8)>;
fn prune(atoms: Vec<u32>, tt: u8) -> (Vec<u32>, u8) {
let mut keep: Vec<u32> = Vec::new();
for (k, &a) in atoms.iter().enumerate() {
let flip = |i: usize| (tt >> (i ^ (1 << k))) & 1 != (tt >> i) & 1;
if (0..8).any(flip) {
keep.push(a);
}
}
let tt = remap_down(tt, &atoms, &keep);
(keep, tt)
}
fn remap_down(tt: u8, from: &[u32], to: &[u32]) -> u8 {
let mut out = 0u8;
for i in 0..8usize {
let mut j = 0usize;
for (k, a) in to.iter().enumerate() {
let p = from.iter().position(|b| b == a).unwrap_or(0);
j |= ((i >> k) & 1) << p;
}
out |= ((tt >> j) & 1) << i;
}
out
}
fn remap(tt: u8, from: &[u32], to: &[u32]) -> u8 {
let pos: Vec<usize> = from
.iter()
.map(|a| to.iter().position(|b| b == a).unwrap_or(0))
.collect();
let mut out = 0u8;
for i in 0..8usize {
let mut j = 0usize;
for (k, &p) in pos.iter().enumerate() {
j |= ((i >> p) & 1) << k;
}
out |= ((tt >> j) & 1) << i;
}
out
}
fn bitwise_op(op: OpCode) -> bool {
matches!(op, OpCode::And | OpCode::Or | OpCode::Xor | OpCode::Not)
}
fn info_of(r: &mut Runner<'_, '_>, cx: &Context, root: u32) -> Result<Info, Stop> {
let mut stack: Vec<(u32, bool)> = vec![(root, false)];
while let Some((i, expanded)) = stack.pop() {
if r.bitwise.contains_key(&i) {
continue;
}
let node = cx.node(i);
let leaf = |i: u32| -> Info {
match cx.const_val(i) {
Some(v) if v.is_zero() => Some((Vec::new(), 0x00)),
Some(v) if v.is_ones() => Some((Vec::new(), 0xFF)),
_ => Some((vec![i], VARS[0])),
}
};
if !bitwise_op(node.op) {
r.bitwise.insert(i, leaf(i));
continue;
}
if !expanded {
stack.push((i, true));
for c in node.children() {
if !r.bitwise.contains_key(&c) {
stack.push((c, false));
}
}
continue;
}
r.meter.charge(Counter::PassWork, 1)?;
let kids: Vec<Info> = node.children().map(|c| r.bitwise[&c].clone()).collect();
let info = if kids.iter().any(Option::is_none) {
None
} else {
let mut atoms: Vec<u32> = kids
.iter()
.flat_map(|k| k.as_ref().map_or(Vec::new(), |k| k.0.clone()))
.collect();
atoms.sort_unstable();
atoms.dedup();
if atoms.len() > 3 {
None
} else {
let t: Vec<u8> = kids
.iter()
.map(|k| {
let (a, tt) = k.as_ref().map_or((&[][..], 0), |k| (&k.0[..], k.1));
remap(tt, a, &atoms)
})
.collect();
let tt = match node.op {
OpCode::Not => !t[0],
OpCode::And => t[0] & t[1],
OpCode::Or => t[0] | t[1],
_ => t[0] ^ t[1],
};
Some(prune(atoms, tt))
}
};
let info = if info.is_none() {
r.stats.passes.entry("bitwise").or_default().atomized += 1;
leaf(i)
} else {
info
};
r.bitwise.insert(i, info);
}
Ok(r.bitwise[&root].clone())
}
pub(super) fn emit(
r: &mut Runner<'_, '_>,
cx: &mut Context,
tt: u8,
atoms: &[u32],
) -> Result<u32, Stop> {
let (tmpl, _) = &min_forms().forms[tt as usize];
let w = cx.width_of(atoms.first().copied().unwrap_or(0));
let mut built: Vec<u32> = Vec::with_capacity(tmpl.len());
for t in tmpl {
r.meter.charge(Counter::PassWork, 1)?;
let id = match *t {
T::Var(k) => atoms[k as usize],
T::Zero => r.build(cx, |cx| cx.mk_const(&crate::BitVec::zero(w)))?,
T::Ones => r.build(cx, |cx| cx.mk_const(&crate::BitVec::ones(w)))?,
T::Not(a) => {
let a = built[a as usize];
r.build(cx, |cx| cx.c_un(UnOp::Not, a))?
}
T::Bin(op, a, b) => {
let (a, b) = (built[a as usize], built[b as usize]);
r.build(cx, |cx| cx.c_bin(op, a, b))?
}
};
built.push(id);
}
r.meter.check()?;
Ok(*built.last().unwrap_or(&atoms[0]))
}
pub(super) fn step(r: &mut Runner<'_, '_>, cx: &mut Context, n: u32) -> Result<Step, Stop> {
if !bitwise_op(cx.node(n).op) {
return Ok(Step::Normal(Fin::FINAL));
}
let Some((atoms, tt)) = info_of(r, cx, n)? else {
return Ok(Step::Normal(Fin::FINAL));
};
if atoms == [n] {
return Ok(Step::Normal(Fin::FINAL));
}
let mut canon = atoms.clone();
canon.sort_by(|a, b| cx.order(*a, *b));
let tt_c = remap(tt, &atoms, &canon);
let estimate = min_forms().forms[tt_c as usize]
.0
.iter()
.filter(|t| !matches!(t, T::Var(_)))
.count() as u32;
if let Some(f) = worth_building(r, cx, n, &atoms, estimate)? {
r.stats.passes.entry("bitwise").or_default().rejected_cost += 1;
return Ok(Step::Normal(Fin::FINAL.and(f)));
}
let before = cx.len() as u32;
let e = if canon.is_empty() {
let w = cx.width_of(n);
let v = if tt == 0 {
crate::BitVec::zero(w)
} else {
crate::BitVec::ones(w)
};
r.build(cx, |cx| cx.mk_const(&v))?
} else {
emit(r, cx, tt_c, &canon)?
};
finish(r, cx, PassKind::Bitwise, n, e, before, &atoms, Fin::FINAL)
}