use std::{
    collections::{HashMap, HashSet},
    fmt::Display,
};

use itertools::Itertools;

// NOTE: PartialOrd and Ord have no sense, but it is needed to sort them somehow
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
struct Cube {
    t: usize,
    f: usize,
}

impl Cube {
    fn cost(&self) -> usize {
        self.t.count_ones() as usize + self.f.count_ones() as usize
    }

    fn covers(&self, minterm: usize) -> bool {
        let mask = self.t | self.f;
        minterm & mask == self.t && !minterm & mask == self.f
    }

    fn combine(&self, other: &Self) -> Option<Self> {
        let dt = self.t ^ other.t;
        let df = self.f ^ other.f;

        if dt == df && dt.count_ones() == 1 {
            Some(Self {
                t: self.t & other.t,
                f: self.f & other.f,
            })
        } else {
            None
        }
    }
}

fn minimize_prime_implicants(n: usize, minterms: &[usize], maxterms: &[usize]) -> Vec<Cube> {
    let minterms_set: HashSet<_> = minterms.iter().copied().collect();
    let maxterms_set: HashSet<_> = maxterms.iter().copied().collect();

    let mut anyterms_set = HashSet::new();
    for i in 0..2usize.pow(n as u32) {
        if !minterms_set.contains(&i) && !maxterms_set.contains(&i) {
            anyterms_set.insert(i);
        }
    }

    let mask = (1 << n) - 1;
    let initial_cubes: Vec<_> = minterms_set
        .union(&anyterms_set)
        .sorted()
        .map(|&i| Cube { t: i, f: !i & mask })
        .collect();

    let mut covered = vec![vec![false; initial_cubes.len()]];
    let mut cubes = vec![initial_cubes];

    for iteration in 0..n {
        let current_covered = &mut covered[iteration];
        let current_cubes = &cubes[iteration];

        let mut new_cubes = HashSet::new();
        for i in 0..current_cubes.len() {
            for j in i + 1..current_cubes.len() {
                let a = &current_cubes[i];
                let b = &current_cubes[j];

                if let Some(combined_cube) = a.combine(b) {
                    current_covered[i] = true;
                    current_covered[j] = true;
                    new_cubes.insert(combined_cube);
                }
            }
        }

        covered.push(vec![false; new_cubes.len()]);
        cubes.push(new_cubes.into_iter().collect());
    }

    let mut final_cubes = vec![];
    for (iteration, iteration_cubes) in cubes.into_iter().enumerate() {
        for (i, cube) in iteration_cubes.into_iter().enumerate() {
            if !covered[iteration][i] {
                final_cubes.push(cube);
            }
        }
    }

    final_cubes.sort();
    final_cubes
}

fn solve_prime_implicants_table(minterms: &[usize], prime_implicants: &[Cube]) -> Vec<Cube> {
    let mut table: HashSet<(usize, usize)> = (0..prime_implicants.len())
        .cartesian_product(0..minterms.len())
        .filter(|&(i, j)| prime_implicants[i].covers(minterms[j]))
        .collect();

    let mut selected_implicants = vec![false; prime_implicants.len()];
    loop {
        // Select essential minterms
        let mut minterms_freq = vec![0; minterms.len()];
        table.iter().for_each(|&(_, j)| minterms_freq[j] += 1);
        table
            .iter()
            .for_each(|&(i, j)| selected_implicants[i] |= minterms_freq[j] == 1);

        // Check if minterms are fully covered
        let mut covered_minterms = vec![false; minterms.len()];
        table
            .iter()
            .filter(|&&(i, _)| selected_implicants[i])
            .for_each(|&(_, j)| covered_minterms[j] = true);
        if table.is_empty() || covered_minterms.iter().all(|&v| v) {
            break;
        }

        // Removing essential implicants
        let new_table: HashSet<_> = table
            .iter()
            .filter(|&&(i, j)| !selected_implicants[i] && !covered_minterms[j])
            .cloned()
            .collect();
        table = new_table;

        if table.is_empty() {
            // All implicants are used
            break;
        }

        // Finding minterm coverage by implicants
        let mut implicants = HashSet::new();
        let mut covered_by_implicants: HashMap<usize, HashSet<_>> = HashMap::new();
        table.iter().for_each(|&(i, j)| {
            implicants.insert(i);
            covered_by_implicants.entry(i).or_default().insert(j);
        });

        // Removing implicants by cost when essentials are not found
        // NOTE: when checking combinations, implicants must be sorted, to give constant result
        // (If not, it will variate due to order in HashSet)
        let mut removed = false;
        let mut implicants_to_remove = vec![false; prime_implicants.len()];
        for (a, b) in implicants.iter().sorted().tuple_combinations() {
            let a_set = &covered_by_implicants[a];
            let b_set = &covered_by_implicants[b];
            let eq = a_set == b_set;

            let a_cost = prime_implicants[*a].cost();
            let b_cost = prime_implicants[*b].cost();

            if eq && a_cost >= b_cost {
                implicants_to_remove[*a] = true;
                removed = true;
            } else if eq {
                implicants_to_remove[*b] = true;
                removed = true;
            }
        }

        if removed {
            let new_table: HashSet<_> = table
                .iter()
                .filter(|&&(i, _)| !implicants_to_remove[i])
                .cloned()
                .collect();
            table = new_table;
        } else {
            // We can't remove implicants by cost, have to choose by ourselves.
            // NOTE: this leads to non-minimal solution
            // NOTE: this SHOULD NOT happen, as we are filtering equal implicant costs too
            todo!()
        }
    }

    prime_implicants
        .iter()
        .zip(selected_implicants)
        .filter(|&(_, select)| select)
        .map(|(cube, _)| cube)
        .copied()
        .collect()
}

fn minimize(n: usize, minterms: &[usize], maxterms: &[usize]) -> Vec<Cube> {
    let prime_implicants = minimize_prime_implicants(n, minterms, maxterms);
    // print_prime_implicants_table(n, minterms, &prime_implicants);
    solve_prime_implicants_table(minterms, &prime_implicants)
}

#[derive(Clone, Debug, Hash)]
#[allow(dead_code)]
enum Logic {
    Constant(bool),

    Variable(String),
    Not(Box<Logic>),

    And(Vec<Logic>),
    Or(Vec<Logic>),

    Nand(Vec<Logic>),
    Nor(Vec<Logic>),
}

impl Logic {
    fn inverse(&self) -> Self {
        match self {
            Logic::Constant(v) => Logic::Constant(!*v),
            Logic::Variable(name) => Logic::Not(Box::new(Logic::Variable(name.clone()))),
            Logic::Not(logic) => *logic.clone(),

            Logic::And(logics) => Logic::Nand(logics.clone()),
            Logic::Or(logics) => Logic::Nor(logics.clone()),

            Logic::Nand(logics) => Logic::And(logics.clone()),
            Logic::Nor(logics) => Logic::Or(logics.clone()),
        }
    }
}

impl Display for Logic {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Logic::Constant(v) => f.write_str(if *v { "1" } else { "0" }),
            Logic::Variable(name) => f.write_str(name),
            Logic::Not(logic) => f.write_fmt(format_args!("!{}", logic)),

            Logic::And(logics) => {
                let s = logics.iter().map(|logic| logic.to_string()).join(" & ");
                f.write_fmt(format_args!("({s})"))
            }

            Logic::Or(logics) => {
                let s = logics.iter().map(|logic| logic.to_string()).join(" | ");
                f.write_fmt(format_args!("({s})"))
            }

            Logic::Nand(logics) => {
                let s = logics.iter().map(|logic| logic.to_string()).join(" !& ");
                f.write_fmt(format_args!("({s})"))
            }

            Logic::Nor(logics) => {
                let s = logics.iter().map(|logic| logic.to_string()).join(" !| ");
                f.write_fmt(format_args!("({s})"))
            }
        }
    }
}

fn cubes_to_dnf(cubes: &[Cube], vars: &[&str]) -> Logic {
    if cubes.is_empty() {
        return Logic::Constant(false);
    } else if cubes.len() == 1 && cubes[0].t == 0 && cubes[0].f == 0 {
        return Logic::Constant(true);
    }

    let mut dnf = vec![];
    for &Cube { mut t, mut f } in cubes {
        let mut used_vars = Vec::new();

        for i in (0..vars.len()).rev() {
            match (t & 1, f & 1) {
                (1, 0) => used_vars.push(Logic::Variable(vars[i].to_owned())),
                (0, 1) => used_vars.push(Logic::Not(Box::new(Logic::Variable(vars[i].to_owned())))),
                (0, 0) => (),
                _ => unreachable!(),
            }

            t >>= 1;
            f >>= 1;
        }

        if used_vars.len() == 1 {
            dnf.push(used_vars[0].clone());
        } else {
            dnf.push(Logic::And(used_vars));
        }
    }

    if dnf.len() == 1 {
        dnf[0].clone()
    } else {
        Logic::Or(dnf)
    }
}

// NOTE: returns inverted result
fn cubes_to_cnf(cubes: &[Cube], vars: &[&str]) -> Logic {
    if cubes.is_empty() {
        return Logic::Constant(false);
    } else if cubes.len() == 1 && cubes[0].t == 0 && cubes[0].f == 0 {
        return Logic::Constant(true);
    }

    let mut dnf = vec![];
    for &Cube { mut t, mut f } in cubes {
        let mut used_vars = Vec::new();

        for i in (0..vars.len()).rev() {
            match (t & 1, f & 1) {
                (1, 0) => used_vars.push(Logic::Not(Box::new(Logic::Variable(vars[i].to_owned())))),
                (0, 1) => used_vars.push(Logic::Variable(vars[i].to_owned())),
                (0, 0) => (),
                _ => unreachable!(),
            }

            t >>= 1;
            f >>= 1;
        }

        if used_vars.len() == 1 {
            dnf.push(used_vars[0].clone());
        } else {
            dnf.push(Logic::Or(used_vars));
        }
    }

    if dnf.len() == 1 {
        dnf[0].clone()
    } else {
        Logic::And(dnf)
    }
}

fn cubes_to_nand(cubes: &[Cube], vars: &[&str]) -> Logic {
    let dnf = cubes_to_dnf(cubes, vars);
    match dnf {
        Logic::Or(logics) => Logic::Nand(logics.into_iter().map(|logic| logic.inverse()).collect()),
        Logic::And(logics) => Logic::Not(Box::new(Logic::Nand(logics))),
        logic => logic,
    }
}

// NOTE: returns inverted result
fn cubes_to_nor(cubes: &[Cube], vars: &[&str]) -> Logic {
    let cnf = cubes_to_cnf(cubes, vars);
    match cnf {
        Logic::Or(logics) => Logic::Not(Box::new(Logic::Nor(logics))),
        Logic::And(logics) => Logic::Nor(logics.into_iter().map(|logic| logic.inverse()).collect()),
        logic => logic,
    }
}

// NOTE: returns inverted result
// NOTE: returns just inverted DNF, which is enough to understand how to build
fn cubes_to_wired_or(cubes: &[Cube], vars: &[&str]) -> Logic {
    let mut dnf = cubes_to_dnf(cubes, vars);

    // If we have standalone variables, we need to transform them into NAND gates
    if let Logic::Or(logics) = &mut dnf {
        for logic in logics {
            if matches!(logic, Logic::Not(_) | Logic::Variable(_)) {
                *logic = Logic::And(vec![logic.inverse(), logic.inverse()]);
            }
        }
    }

    Logic::Not(Box::new(dnf))
}

fn main() {
    let mut args = std::env::args().skip(1);
    let chip_series_file_path = args.next().unwrap();
    let truth_table_file_path = args.next().unwrap();

    // TODO: make a use of this
    let _chip_series_file = std::fs::read_to_string(chip_series_file_path).unwrap();

    let truth_table_file = std::fs::read_to_string(truth_table_file_path).unwrap();

    // Parsing truth table
    let mut truth_table_lines = truth_table_file.lines();

    let truth_table_inputs = truth_table_lines
        .next()
        .map(|line| line.split_whitespace().collect_vec())
        .unwrap();
    let truth_table_outputs = truth_table_lines
        .next()
        .map(|line| line.split_whitespace().collect_vec())
        .unwrap();

    let mut truth_table_minterms = vec![vec![]; truth_table_outputs.len()];
    let mut truth_table_maxterms = vec![vec![]; truth_table_outputs.len()];
    for line in truth_table_lines {
        let (input, output) = line.split_once(char::is_whitespace).unwrap();
        if input.len() != truth_table_inputs.len() || output.len() != truth_table_outputs.len() {
            panic!("Truth table is incorrect: invalid input/output size");
        }

        let input_term = usize::from_str_radix(input, 2).unwrap();
        for (i, ch) in output.chars().enumerate() {
            match ch {
                '1' => truth_table_minterms[i].push(input_term),
                '0' => truth_table_maxterms[i].push(input_term),
                '-' => (),
                _ => panic!("Truth table is incorrect: invalid char in output section"),
            }
        }
    }

    for (output, (minterms, maxterms)) in truth_table_outputs
        .into_iter()
        .zip(truth_table_minterms.into_iter().zip(truth_table_maxterms))
    {
        let cubes = minimize(truth_table_inputs.len(), &minterms, &maxterms);
        let inv_cubes = minimize(truth_table_inputs.len(), &maxterms, &minterms);

        println!("{output} = {}", cubes_to_dnf(&cubes, &truth_table_inputs));
        println!("{output} = {}", cubes_to_nand(&cubes, &truth_table_inputs));
        println!(
            "{output} = {}",
            cubes_to_cnf(&inv_cubes, &truth_table_inputs)
        );
        println!(
            "{output} = {}",
            cubes_to_nor(&inv_cubes, &truth_table_inputs)
        );
        println!(
            "{output} = {}",
            cubes_to_wired_or(&inv_cubes, &truth_table_inputs)
        );

        println!();
    }
}