use std::collections::HashSet;
use base::{Base};
use {nid, nid::{NID,I,O}};
use vid::{VID,VidOrdering};
use cur::{Cursor, CursorPlan};
use reg::Reg;
use vhl::{HiLo, HiLoBase, Walkable};
use hashbrown::HashMap;
use bdd::{BDDBase}; #[cfg(test)] use vid::{topmost, botmost};
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
struct ANF {
v: VID,
hi: NID,
lo: NID }
pub struct ANFBase {
nvars:usize,
nodes:Vec<ANF>,
cache:HashMap<ANF,NID>,
tags:HashMap<String,NID>}
impl Walkable for ANFBase {
fn step<F>(&self, n:NID, f:&mut F, seen:&mut HashSet<NID>, topdown: bool)
where F: FnMut(NID,VID,NID,NID) {
if !seen.contains(&n) {
seen.insert(n); let ANF{ v, hi, lo, } = self.fetch(n);
if topdown { f(n,v,hi,lo) }
if !nid::is_const(hi) { self.step(hi, f, seen, topdown) }
if !nid::is_const(lo) { self.step(lo, f, seen, topdown) }
if !topdown { f(n,v,hi,lo) }}}}
impl Base for ANFBase {
fn new(n:usize)->Self {
ANFBase { nvars: n, nodes:vec![], cache: HashMap::new(), tags:HashMap::new() }}
fn num_vars(&self)->usize { self.nvars }
fn dot(&self, n:NID, wr: &mut dyn std::fmt::Write) {
macro_rules! w {
($x:expr $(,$xs:expr)*) => { writeln!(wr, $x $(,$xs)*).unwrap(); }}
w!("digraph anf {{");
w!("subgraph head {{ h1[shape=plaintext; label=\"ANF\"] }}");
w!(" I[label=⊤; shape=square];");
w!(" O[label=⊥; shape=square];");
w!("{{rank = same; I; O;}}");
w!("node[shape=circle];");
self.walk(n, &mut |n,_,_h,_l| w!(" \"{}\"[label=\"{:?}\"];", n, n.vid()));
w!("edge[style=solid];");
self.walk(n, &mut |n,_,hi,_l| w!(" \"{:?}\"->\"{:?}\";", n, hi));
w!("edge[style=dashed];");
self.walk(n, &mut |n,_,__,lo| w!(" \"{:?}\"->\"{:?}\";", n, lo));
w!("}}"); }
fn def(&mut self, _s:String, _v:VID)->NID { todo!("anf::def"); }
fn tag(&mut self, n:NID, s:String)->NID { self.tags.insert(s, n); n }
fn get(&self, s:&str)->Option<NID> { Some(*self.tags.get(s)?) }
fn when_lo(&mut self, v:VID, n:NID)->NID {
let nv = n.vid();
match v.cmp_depth(&nv) {
VidOrdering::Above => n, VidOrdering::Level => self.fetch(n).lo,
VidOrdering::Below => {
let ANF{ v:_, hi, lo } = self.fetch(nid::raw(n));
let hi1 = self.when_lo(v, hi);
let lo1 = self.when_lo(v, lo);
let mut res = self.vhl(nv, hi1, lo1);
if nid::is_inv(n) != nid::is_inv(res) { res = !res }
res }}}
fn when_hi(&mut self, v:VID, n:NID)->NID {
let nv = n.vid();
match v.cmp_depth(&nv) {
VidOrdering::Above => n, VidOrdering::Level => self.fetch(n).hi,
VidOrdering::Below => {
let ANF{ v:_, hi, lo } = self.fetch(nid::raw(n));
let hi1 = self.when_hi(v, hi);
let lo1 = self.when_hi(v, lo);
let mut res = self.vhl(nv, hi1, lo1);
if nid::is_inv(n) != nid::is_inv(res) { res = !res }
res }}}
fn and(&mut self, x:NID, y:NID)->NID {
if x == O || y == O { O }
else if x == I || x == y { y }
else if y == I { x }
else if x == !y { O }
else {
let (a,b) = (nid::raw(x), nid::raw(y)); if nid::is_inv(x) {
if nid::is_inv(y) { expr![ self, (I ^ (a ^ ((a & b) ^ b)))] }
else { expr![ self, ((a & b) ^ b)] }}
else if nid::is_inv(y) { expr![ self, ((a & b) ^ a)] }
else { self.calc_and(x, y) }}}
fn xor(&mut self, x:NID, y:NID)->NID {
if x == y { O }
else if x == O { y }
else if y == O { x }
else if x == I { !y }
else if y == I { !x }
else if x == !y { I }
else {
let (a, b) = (nid::raw(x), nid::raw(y));
let res = self.calc_xor(a, b);
if nid::is_inv(x) == nid::is_inv(y) { res }
else { !res }}}
fn or(&mut self, x:NID, y:NID)->NID { expr![self, ((x & y) ^ (x ^ y))] }
fn sub(&mut self, v:VID, n:NID, ctx:NID)->NID {
let cv = ctx.vid();
if ctx.might_depend_on(v) {
let x = self.fetch(ctx);
let (hi, lo) = (x.hi, x.lo);
if v == cv { expr![self, ((n & hi) ^ lo)] }
else {
let rhi = self.sub(v,n,hi);
let rlo = self.sub(v,n,lo);
let top = NID::from_vid(cv);
expr![self, ((top & rhi) ^ rlo)] }}
else { ctx }}
fn save(&self, _path:&str)->::std::io::Result<()> { todo!("anf::save") }
fn solution_set(&self, n: NID, nvars: usize)->hashbrown::HashSet<Reg> {
self.solutions_trunc(n, nvars).collect() }
}
impl ANFBase {
fn fetch(&self, n:NID)->ANF {
if nid::is_var(n) { ANF{v:n.vid(), hi:I, lo: if nid::is_inv(n) { I } else { O } }}
else {
let mut anf = self.nodes[nid::idx(n)];
if nid::is_inv(n) { anf.lo = !anf.lo }
anf }}
fn vhl(&mut self, v:VID, hi0:NID, lo0:NID)->NID {
if hi0 == I && lo0 == O { return NID::from_vid(v) }
let (hi,lo) = (hi0, nid::raw(lo0));
let res =
if let Some(&nid) = self.cache.get(&ANF{v, hi, lo}) { nid }
else {
let anf = ANF{ v, hi, lo };
let nid = NID::from_vid_idx(v, self.nodes.len() as u32);
self.cache.insert(anf, nid);
self.nodes.push(anf);
nid };
if nid::is_inv(lo) { !res } else { res }}
fn calc_and(&mut self, x:NID, y:NID)->NID {
let (xv, yv) = (x.vid(), y.vid());
match xv.cmp_depth(&yv) {
VidOrdering::Above =>
if nid::is_var(x) { self.vhl(x.vid(), y, O) }
else {
let ANF{v:a, hi:b, lo:c } = self.fetch(x);
let hi = self.and(b, y);
let lo = self.and(c, y);
self.vhl(a, hi, lo)},
VidOrdering::Below => self.and(y, x),
VidOrdering::Level => {
let ANF{ v:a, hi:b, lo:c } = self.fetch(x);
let ANF{ v:p, hi:q, lo:r } = self.fetch(y);
assert_eq!(a,p);
let cr = self.and(c,r);
let cq = self.and(c,q);
let qxr = self.xor(q,r);
let n = NID::from_vid(a);
expr![self, ((n & ((b & qxr) ^ cq)) ^ cr)] }}}
fn calc_xor(&mut self, x:NID, y:NID)->NID {
let (xv, yv) = (x.vid(), y.vid());
match xv.cmp_depth(&yv) {
VidOrdering::Above => {
let ANF{v, hi, lo} = self.fetch(x);
let lo = self.xor(lo, y);
self.vhl(v, hi, lo)},
VidOrdering::Below => self.xor(y, x),
VidOrdering::Level => {
let ANF{v:a, hi:b, lo:c} = self.fetch(x);
let ANF{v:p, hi:q, lo:r} = self.fetch(y);
assert_eq!(a,p);
let hi = self.xor(b, q);
let lo = self.xor(c, r);
self.vhl(a, hi, lo)}}}
pub fn solutions(&mut self, n:NID)->ANFSolIterator {
self.solutions_trunc(n, self.num_vars())}
pub fn solutions_trunc(&self, n:NID, nvars:usize)->ANFSolIterator {
assert!(nvars <= self.num_vars(), "nvars arg to solutions_trunc must be <= self.nvars");
ANFSolIterator::from_anf_base(self, n, nvars)}
}
impl HiLoBase for ANFBase {
fn get_hilo(&self, nid:NID)->Option<HiLo> {
let ANF { v:_, hi, lo } = self.fetch(nid);
Some(HiLo { hi, lo }) }}
impl CursorPlan for ANFBase {}
impl ANFBase {
fn log(&self, _cur:&Cursor, _msg: &str) {
#[cfg(test)] {
print!("{:>10}", format!("{}", _cur.node));
print!(" {:?}", _cur.scope);
let s = format!("{}", _msg);
println!(" {:50} {:?}", s, _cur.nstack); }}
pub fn first_term(&self, nvars:usize, n:NID)->Option<Cursor> {
if n == O { return None } let mut cur = Cursor::new(nvars, n); cur.descend(self); Some(cur) }
pub fn next_term(&self, mut cur:Cursor)->Option<Cursor> {
self.log(&cur,"== next_term()");
if !nid::is_const(cur.node) {
println!("warning: ANFBase::next_term should be called on cursor pointing at a leaf.");
cur.descend(self); }
loop {
cur.step_up(); self.log(&cur,"step up");
cur.go_next_lo_var(); self.log(&cur,"next lo");
if cur.at_top() && cur.var_get() { self.log(&cur, "@end"); return None }
cur.clear_trailing_bits(); self.log(&cur, "cleared trailing");
cur.put_step(self, true);
if cur.node == I { self.log(&cur, "<-- answer (lo)"); return Some(cur) }
cur.descend(self); self.log(&cur, "descend");
if cur.node == I { self.log(&cur, "<-- answer (lo)"); return Some(cur) }}}
pub fn terms_trunc(&self, n:NID, nvars:usize)->ANFTermIterator {
ANFTermIterator::from_anf_base(&self, n, nvars)}
pub fn terms(&self, n:NID)->ANFTermIterator {
ANFTermIterator::from_anf_base(&self, n, self.nvars) }}
pub struct ANFTermIterator<'a> {
base: &'a ANFBase,
next: Option<Cursor> }
impl<'a> ANFTermIterator<'a> {
pub fn from_anf_base(base: &'a ANFBase, nid:NID, nvars:usize)->Self {
if let Some(next) = base.first_term(nvars, nid) {
ANFTermIterator{ base, next:Some(next) }}
else {
ANFTermIterator{ base, next:None }}}}
impl<'a> Iterator for ANFTermIterator<'a> {
type Item = Reg;
fn next(&mut self)->Option<Self::Item> {
if let Some(cur) = self.next.take() {
let reg = cur.scope.clone();
self.next = self.base.next_term(cur);
Some(reg) }
else { None }}}
pub struct ANFSolIterator<'a> {
_anf: &'a ANFBase,
bdd: BDDBase,
bcur: Option<Cursor>}
impl<'a> ANFSolIterator<'a> {
pub fn from_anf_base(anf: &'a ANFBase, nid:NID, nvars:usize)->Self {
let mut bdd = BDDBase::new(nvars);
let bnid = anf.to_base_trunc(nid, &mut bdd, nvars);
let bcur = bdd.first_solution(bnid, nvars);
ANFSolIterator{ _anf:anf, bdd, bcur } }}
impl<'a> Iterator for ANFSolIterator<'a> {
type Item = Reg;
fn next(&mut self)->Option<Self::Item> {
if let Some(cur) = self.bcur.take() {
let res = Some(cur.scope.clone());
self.bcur = self.bdd.next_solution(cur);
res }
else { None } }}
impl ANFBase {
pub fn to_base(&self, n:NID, dest: &mut dyn Base)->NID {
self.to_base_trunc(n, dest, self.nvars)}
pub fn to_base_trunc(&self, n:NID, dest: &mut dyn Base, nvars:usize)-> NID {
let mut sum = nid::O;
if nid::is_inv(n) { sum = nid::I }
for t in self.terms_trunc(nid::raw(n), nvars) {
let mut term = I;
for v in t.hi_bits() {
term = dest.and(term, NID::var(v as u32));
println!("term: {}", term) }
sum = dest.xor(sum, term);
println!("sum: {}", sum) }
sum }}
test_base_consts!(ANFBase);
test_base_when!(ANFBase);
#[test] fn test_anf_hilo() {
let base = ANFBase::new(1);
let a = NID::var(0);
let ANF{ v, hi, lo } = base.fetch(a);
assert_eq!(v, a.vid());
assert_eq!(hi, I);
assert_eq!(lo, O); }
#[test] fn test_anf_hilo_not() {
let base = ANFBase::new(1);
let a = NID::var(0);
let ANF{ v, hi, lo } = base.fetch(!a);
assert_eq!(v, a.vid());
assert_eq!(hi, I);
assert_eq!(lo, I); }
#[test] fn test_anf_xor() {
let mut base = ANFBase::new(2);
let a = NID::var(0); let b = NID::var(1);
let (axb, bxa) = (base.xor(a,b), base.xor(b,a));
assert_eq!(O, base.xor(a,a), "a xor a should be 0");
assert_eq!(!a, base.xor(I,a), "a xor 1 should be ~a");
assert_eq!(axb, bxa, "xor should be order-independent");
let ANF{ v, hi, lo } = base.fetch(axb);
let topv = topmost(a.vid(), b.vid());
let botv = botmost(a.vid(), b.vid());
assert_eq!(v, topv);
assert_eq!(hi, I);
assert_eq!(lo, NID::from_vid(botv)); }
#[test] fn test_anf_xor_inv() {
let mut base = ANFBase::new(2);
let a = NID::var(0); let b = NID::var(1);
let axb = base.xor(a, b);
let naxb = base.xor(!a, b);
let axnb = base.xor(a, !b);
let naxnb = base.xor(!a, !b);
assert_eq!(naxnb, axb, "expect ~a ^ ~b == a^b");
assert_eq!(axnb, naxb, "expect a ^ ~b == ~a ^ b");
assert_eq!(axb, !naxb, "expect a ^ b == ~(~a ^ b)"); }
#[test] fn test_anf_xor3() {
let mut base = ANFBase::new(4);
let a = NID::var(0); let b = NID::var(1); let c = NID::var(2);
assert_eq!(expr![base, ((a ^ b) ^ c)],
expr![base, (a ^ (b ^ c))]); }
#[test] fn test_anf_and() {
let mut base = ANFBase::new(2);
let a = NID::var(0); let b = NID::var(1);
let ab = base.and(a, b);
let ANF{v, hi, lo} = base.fetch(ab);
let topv = topmost(a.vid(), b.vid());
let botv = botmost(a.vid(), b.vid());
assert_eq!(v, topv);
assert_eq!(hi, NID::from_vid(botv));
assert_eq!(lo, O);}
#[test] fn test_anf_xtb() {
let mut base = ANFBase::new(2);
let (x0, x1) = (VID::var(0), VID::var(1));
let t = NID::from_vid(topmost(x0,x1));
let b = NID::from_vid(botmost(x0,x1));
let tb = base.and(b,t);
let bxtb = base.xor(b, tb); let txtb = base.xor(t, tb);
let (bv, tv) = (b.vid(), t.vid());
assert_eq!(base.fetch(b), ANF{ v:bv, hi:I, lo:nid::O}, "b = b(1)+0");
assert_eq!(base.fetch(t), ANF{ v:tv, hi:I, lo:nid::O}, "t = t(1)+0");
assert_eq!(base.fetch(tb), ANF{ v:tv, hi:b, lo:nid::O}, "tb = t(b)+0");
assert_eq!(base.fetch(bxtb), ANF{ v:tv, hi:b, lo:b}, "b + tb = t(b)+b");
assert_eq!(base.fetch(txtb), ANF{ v:tv, hi:!b, lo:nid::O}, "t+tb = t(b+1)+0");
}
#[test] fn test_anf_and3() {
let mut base = ANFBase::new(4);
let a = NID::var(0); let b = NID::var(1); let c = NID::var(2);
assert_eq!(expr![base, ((a & b) & c)],
expr![base, (a & (b & c))]); }
#[test] fn test_anf_and_big() {
let mut base = ANFBase::new(4);
let a = NID::var(0); let b = NID::var(1); let c = NID::var(2);
let p = NID::var(3); let q = NID::var(4); let r = NID::var(5);
let ab = base.and(a,b); let pq = base.and(p,q);
let actual = expr![base, ((ab ^ c) & (pq ^ r))];
let expected = expr![base, ((ab & (pq ^ r)) ^ (c & (pq ^ r)))];
assert_eq!(expected, actual); }
#[test] fn test_anf_and_same_head() {
let mut base = ANFBase::new(5);
let a = NID::var(0); let b = NID::var(1); let c = NID::var(2);
let q = NID::var(3); let r = NID::var(4);
let ab = base.and(a,b); let aq = base.and(a,q);
let actual = expr![base, ((ab ^ c) & (aq ^ r))];
let expected = expr![base, ((a & ((b & (q ^ r)) ^ (c&q)))^(c&r))];
assert_eq!(expected, actual); }
#[test] fn test_anf_sub() {
let mut base = ANFBase::new(6);
let a = NID::var(0); let b = NID::var(1); let c = NID::var(2);
let x = NID::var(3); let y = NID::var(4); let z = NID::var(5);
let ctx = expr![base, ((a & b) ^ c) ];
let xyz = expr![base, ((x & y) ^ z) ];
assert_eq!(base.sub(a.vid(), xyz, ctx), expr![base, ((xyz & b) ^ c)]);
assert_eq!(base.sub(b.vid(), xyz, ctx), expr![base, ((a & xyz) ^ c)]);}
#[test] fn test_anf_sub_inv() {
let mut base = ANFBase::new(7); let nv = |x|NID::var(x);
let (v1,v2,v4,v6) = (nv(1), nv(2), nv(4), nv(6));
let ctx = expr![base, (v1 & v6) ];
let top = expr![base, ((I^v4) & v2)];
assert_eq!(top, base.and(!v4, v2), "sanity check");
let expect = expr![base, ((v2 & (v4 & v6)) ^ (v2 & v6))];
let actual = base.sub(v1.vid(), top, ctx);
assert_eq!(expect, actual);}
#[test] fn test_anf_terms() {
let mut base = ANFBase::new(3); let nv = |x|NID::var(x);
let (x,y,z) = (nv(0), nv(1), nv(2));
let n = expr![base, ((z^(z&y))^((y&x)^x))];
let terms:Vec<_> = base.terms(n).map(|t| t.as_usize()).collect();
assert_eq!(terms, [0b001, 0b011, 0b100, 0b110]);}
#[test] fn test_anf_terms_not() {
let mut anf = ANFBase::new(3);
let (a,_,c) = (NID::var(0), NID::var(1), NID::var(2));
let anc = expr![anf, (a & (c^I))];
let res:Vec<_> = anf.terms(anc).map(|reg|reg.as_usize()).collect();
assert_eq!(res, vec![0b001,0b101]); }
#[test] fn test_anf_terms_bug() {
let mut anf = ANFBase::new(3);
let (a,b,c) = (NID::var(0), NID::var(1), NID::var(2));
let x = expr![anf, ((a & (b^c)) ^ (b & (c^I)))]; let t:Vec<_> = anf.terms(x).map(|r|r.as_usize()).collect();
assert_eq!(t, vec![0b010,0b011,0b101,0b110]); }
#[test] fn test_anf_to_base() {
use bdd::BDDBase;
let mut anf = ANFBase::new(3);
let mut bdd = BDDBase::new(3);
let (a,b,c) = (NID::var(0), NID::var(1), NID::var(2));
let initial = expr![anf, (a & (c^I))];
let expect = expr![bdd, (a & (c^I))];
let actual = anf.to_base(initial, &mut bdd);
assert_eq!(expect, actual, "anf-> bdd should get same answer as pure bdd (1).");
let initial = expr![anf, (a & (b^c))];
let expect = expr![bdd, (a & (b^c))];
let actual = anf.to_base(initial, &mut bdd);
assert_eq!(expect, actual, "anf-> bdd should get same answer as pure bdd (2).");
let initial = expr![anf, ((a & (b^c)) ^ (b & (c^I)))];
let expect = expr![bdd, ((a & (b^c)) ^ (b & (c^I)))];
let actual = anf.to_base(initial, &mut bdd);
assert_eq!(expect, actual, "anf-> bdd should get same answer as pure bdd (3).");}