fn main() -> Result<ExitCode, MercError> {

    let cli = Cli::parse();

    let mut timing = Timing::new();

    env_logger::Builder::new()

        .filter_level(cli.verbosity.log_level_filter())

        .parse_default_env()

        .init();

    if cli.version.into() {

        eprintln!("{}", Version);

        return Ok(ExitCode::SUCCESS);

    }

    if let Some(command) = &cli.commands {

        match command {

            Commands::Solve(args) => handle_solve(&cli, args, &mut timing)?,

            Commands::Reachable(args) => handle_reachable(&cli, args, &mut timing)?,

            Commands::Project(args) => handle_project(&cli, args, &mut timing)?,

            Commands::Translate(args) => handle_translate(&cli, args)?,

            Commands::Display(args) => handle_display(&cli, args, &mut timing)?,

    }

    if cli.timings {

        timing.print();

    }

    print_allocator_metrics();

    if cfg!(feature = "merc_metrics") {

        oxidd::bdd::print_stats();

    }

    Ok(ExitCode::SUCCESS)

}

fn handle_solve(cli: &Cli, args: &SolveArgs, timing: &mut Timing) -> Result<(), MercError> {

    let path = Path::new(&args.filename);

    let mut file = File::open(path)?;

    let format = guess_format_from_extension(path, args.format).ok_or("Unknown parity game file format.")?;

    if format == ParityGameFormat::PG {

        let mut time_read = timing.start("read_pg");

        let game = read_pg(&mut file)?;

        time_read.finish();

        let mut time_solve = timing.start("solve_zielonka");

        let solution = solve_zielonka(&game);

        if args.full_solution {

            for (index, player_set) in solution.iter().enumerate() {

                println!("W{index}: {}", player_set.iter_ones().format(", "));

            }

        } else if solution[0][0] {

            println!("{}", Player::Even.solution())

            println!("{}", Player::Odd.solution())

        time_solve.finish();

        let solve_variant = args

            .solve_variant

            .ok_or("For variability parity game solving a solving strategy should be selected")?;

        let manager_ref = oxidd::bdd::new_manager(

            cli.oxidd_node_capacity,

            cli.oxidd_cache_capacity.unwrap_or(cli.oxidd_node_capacity),

            cli.oxidd_workers,

        let mut time_read = timing.start("read_vpg");

        let game = read_vpg(&manager_ref, &mut file)?;

        time_read.finish();

        let game = if !game.is_total(&manager_ref)? {

            make_vpg_total(&manager_ref, &game)?

            game

        let mut time_solve = timing.start("solve_variability_zielonka");

        if solve_variant == ZielonkaVariant::Product {

            let mut results = [Vec::new(), Vec::new()];

            for (cube, _bdd, solution) in solve_variability_product_zielonka(&game) {

                for (index, w) in solution.iter().enumerate() {

                    results[index].push((cube.clone(), w.clone()));

                }

            for (index, w) in results.iter().enumerate() {

                println!("W{index}: ");

                for (cube, vertices) in w {

                    println!(

                        FormatConfig(cube),

                        vertices

                            .iter_ones()

                            .filter(|v| if args.full_solution { true } else { *v == 0 })

                            .format(", ")

            let solutions = solve_variability_zielonka(&manager_ref, &game, solve_variant, false)?;

            for (index, w) in solutions.iter().enumerate() {

                println!("W{index}: ");

                for entry in CubeIterAll::new(game.variables(), game.configuration()) {

                    let (config, config_function) = entry?;

                    println!(

                        FormatConfig(&config),

                        w.iter() // Do not use iter_vertices because the first one is the initial vertex only

                            .take(if args.full_solution { usize::MAX } else { 1 }) // Take only first if we don't want full solution

                            .filter(|(_v, config)| { config.and(&config_function).unwrap().satisfiable() })

                            .map(|(v, _)| v)

                            .format(", ")

            if args.verify_solution {

                verify_variability_product_zielonka_solution(&game, &solutions)?;

            }

        time_solve.finish();

    Ok(())

}

fn handle_reachable(cli: &Cli, args: &ReachableArgs, timing: &mut Timing) -> Result<(), MercError> {

    let path = Path::new(&args.filename);

    let mut file = File::open(path)?;

    let format = guess_format_from_extension(path, args.format).ok_or("Unknown parity game file format.")?;

    match format {

            let mut time_read = timing.start("read_pg");

            let game = read_pg(&mut file)?;

            time_read.finish();

            let mut time_reachable = timing.start("compute_reachable");

            let (reachable_game, mapping) = compute_reachable(&game);

            time_reachable.finish();

            for (old_index, new_index) in mapping.iter().enumerate() {

                debug!("{} -> {:?}", old_index, new_index);

            let mut output_file = File::create(&args.output)?;

            write_pg(&mut output_file, &reachable_game)?;

            let manager_ref = oxidd::bdd::new_manager(

                cli.oxidd_node_capacity,

                cli.oxidd_cache_capacity.unwrap_or(cli.oxidd_node_capacity),

                cli.oxidd_workers,

            let mut time_read = timing.start("read_vpg");

            let game = read_vpg(&manager_ref, &mut file)?;

            time_read.finish();

            let mut time_reachable = timing.start("compute_reachable_vpg");

            let (reachable_game, mapping) = compute_reachable(&game);

            time_reachable.finish();

            for (old_index, new_index) in mapping.iter().enumerate() {

                debug!("{} -> {:?}", old_index, new_index);

            let mut output_file = File::create(&args.output)?;

            write_pg(&mut output_file, &reachable_game)?;

    Ok(())

}

fn handle_project(cli: &Cli, args: &ProjectArgs, timing: &mut Timing) -> Result<(), MercError> {

    let path = Path::new(&args.filename);

    let mut file = File::open(path)?;

    let format = guess_format_from_extension(path, args.format).ok_or("Unknown parity game file format.")?;

    if format != ParityGameFormat::VPG {

        return Err(MercError::from(

            "The project command only works for variability parity games.",

        ));

    }

    let manager_ref = oxidd::bdd::new_manager(

        cli.oxidd_node_capacity,

        cli.oxidd_cache_capacity.unwrap_or(cli.oxidd_node_capacity),

        cli.oxidd_workers,

    let mut time_read = timing.start("read_vpg");

    let vpg = read_vpg(&manager_ref, &mut file)?;

    time_read.finish();

    let output_path = Path::new(&args.output);

    for result in project_variability_parity_games_iter(&vpg) {

        let (cube, _bdd, pg) = result?;

        let extension = output_path.extension().ok_or("Missing extension on output file")?;

        let new_path = output_path

            .with_file_name(format!(

                output_path

                    .file_stem()

                    .ok_or("Missing filename on output")?

                    .to_string_lossy(),

                FormatConfig(&cube)

            .with_extension(extension);

        let mut output_file = File::create(new_path)?;

        if args.reachable {

            let (reachable_pg, _projection) = compute_reachable(&pg);

            write_pg(&mut output_file, &reachable_pg)?;

            write_pg(&mut output_file, &pg)?;

    Ok(())

}

fn handle_translate(cli: &Cli, args: &TranslateArgs) -> Result<(), MercError> {

    let manager_ref = oxidd::bdd::new_manager(

        cli.oxidd_node_capacity,

        cli.oxidd_cache_capacity.unwrap_or(cli.oxidd_node_capacity),

        cli.oxidd_workers,

    let mut feature_diagram_file = File::open(&args.feature_diagram_filename).map_err(|e| {

        MercError::from(format!(

            &args.feature_diagram_filename, e

    })?;

    let feature_diagram = FeatureDiagram::from_reader(&manager_ref, &mut feature_diagram_file)?;

    let mut fts_file = File::open(&args.fts_filename).map_err(|e| {

        MercError::from(format!(

            &args.fts_filename, e

    })?;

    let fts = read_fts(&manager_ref, &mut fts_file, feature_diagram.features().clone())?;

    let formula_spec = UntypedStateFrmSpec::parse(&read_to_string(&args.formula_filename).map_err(|e| {

        MercError::from(format!(

            &args.formula_filename, e

    })?)?;

    if !formula_spec.action_declarations.is_empty() {

        return Err(MercError::from("We do not support formulas with action declarations."));

    }

    if !formula_spec.data_specification.is_empty() {

        return Err(MercError::from("The formula must not contain a data specification."));

    }

    let vpg = translate(

        &manager_ref,

        &fts,

        feature_diagram.configuration().clone(),

        &formula_spec.formula,

    )?;

    let mut output_file = File::create(&args.output)?;

    write_vpg(&mut output_file, &vpg)?;

    Ok(())

}

fn handle_display(cli: &Cli, args: &DisplayArgs, timing: &mut Timing) -> Result<(), MercError> {

    let path = Path::new(&args.filename);

    let mut file = File::open(path)?;

    let format = guess_format_from_extension(path, args.format).ok_or("Unknown parity game file format.")?;

    if format == ParityGameFormat::PG {

        let mut time_read = timing.start("read_pg");

        let game = read_pg(&mut file)?;

        time_read.finish();

        let mut output_file = File::create(&args.output)?;

        write!(&mut output_file, "{}", PgDot::new(&game))?;

        let manager_ref = oxidd::bdd::new_manager(

            cli.oxidd_node_capacity,

            cli.oxidd_cache_capacity.unwrap_or(cli.oxidd_node_capacity),

            cli.oxidd_workers,

        let mut time_read = timing.start("read_vpg");

        let game = read_vpg(&manager_ref, &mut file)?;

        time_read.finish();

        let mut output_file = File::create(&args.output)?;

        write!(&mut output_file, "{}", VpgDot::new(&game))?;

    if let Ok(dot_path) = which::which("dot") {

        info!("Generating PDF using dot...");

        cmd!(dot_path, "-Tpdf", &args.output, "-O").run()?;

    }

    Ok(())

}