fn main() -> ExitCode {

    let cli = Cli::parse();

    let mut timing = Timing::new();

    env_logger::Builder::new()

        .filter_level(cli.verbosity.log_level_filter())

        .format_key_values(|formatter, source| format_key_values_json(formatter, source))

        .parse_default_env()

        .init();

    if cli.version.into() {

        eprintln!("{}", Version);

        return ExitCode::SUCCESS;

    }

    let result = handle_command(&cli, &mut timing);

    if cli.timings {

        timing.print();

    }

    print_allocator_metrics();

    if cfg!(feature = "merc_metrics") {

        oxidd::bdd::print_stats();

    }

    report_error(result)

}

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

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

        match command {

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

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

            Commands::Project(args) => handle_project_fts(cli, args, timing)?,

            Commands::ProjectVpg(args) => handle_project_vpg(cli, args, timing)?,

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

            Commands::TranslateVpg(args) => handle_translate_vpg(cli, args)?,

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

    }

    Ok(())

}

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_else(|| format!("Unknown parity game file format for '{}", path.display()))?;

    if format == ParityGameFormat::PG {

        let game = timing.measure("read_pg", || read_pg(&mut file))?;

        let (solution, strategy) = timing.measure("solve_zielonka", || match args.solver {

            Solver::Zielonka => solve_zielonka(&game, args.verify_solution),

            Solver::PriorityPromotion => solve_priority_promotion(&game, args.verify_solution),

        });

        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())

        if let Some(strategy) = strategy

            && args.verify_solution

        {

            verify_solution(&game, &solution, &strategy);

        }

        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 game = timing.measure("read_vpg", || -> Result<_, MercError> {

            read_vpg(&manager_ref, &mut file)

        })?;

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

            info!("Making the VPG total...");

            make_vpg_total(&manager_ref, &game)?

            game

        timing.measure("solve_variability_zielonka", || -> Result<_, MercError> {

            if args.vpg_solver == VpgSolver::Product {

                let solver = args.solver;

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

                for result in solve_variability_product_zielonka(&game, solver, timing) {

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

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

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

                    }

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

                    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, args.vpg_solver, false)?;

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

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

                        let config = entry?;

                        let config_function = bits_to_bdd(&manager_ref, game.variables(), &config)?;

                        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, timing)?;

                }

            Ok(())

        })?;

    Ok(())

}

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

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

    let format = guess_format_from_extension(path, args.format)

        .ok_or_else(|| format!("Unknown parity game file format for '{}", path.display()))?;

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

    match format {

            let game = timing.measure("read_pg", || read_pg(&mut file))?;

            let (reachable_game, mapping) = timing.measure("compute_reachable", || compute_reachable(&game));

            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 game = timing.measure("read_vpg", || read_vpg(&manager_ref, &mut file))?;

            let (reachable_game, mapping) = timing.measure("compute_reachable_vpg", || compute_reachable(&game));

            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_fts(cli: &Cli, args: &ProjectArgs, timing: &mut Timing) -> Result<(), MercError> {

    let format = guess_lts_format_from_extension(&args.filename, args.format).ok_or_else(|| {

        format!(

            args.filename.display()

    })?;

    if format != LtsFormat::Aut {

        return Err(MercError::from(

            "The project command only works for featured transition systems in the .aut format.",

        ));

    }

    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.display(),

    })?;

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

    debug!("Feature diagram {:?}", feature_diagram);

    let mut fts_file = File::open(&args.filename)?;

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

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

    for result in project_feature_transition_system_iter(&fts, &feature_diagram, timing) {

        let (ProjectedLts { bits, bdd: _, lts }, _) = 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(&bits)

            .with_added_extension(extension);

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

        write_aut(&mut output_file, &lts)?;

    Ok(())

}

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

    let format = guess_format_from_extension(&args.filename, args.format)

        .ok_or_else(|| format!("Unknown parity game file format for '{}'.", args.filename.display()))?;

    let mut file = File::open(&args.filename)?;

    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 vpg = timing.measure("read_vpg", || read_vpg(&manager_ref, &mut file))?;

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

    for result in project_variability_parity_games_iter(&vpg, timing) {

        let (Projected { bits, bdd: _, game }, _) = 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(&bits)

            .with_added_extension(extension);

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

        if args.reachable {

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

            write_pg(&mut output_file, &reachable_pg)?;

            write_pg(&mut output_file, &game)?;

    Ok(())

}

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

    let format = guess_lts_format_from_extension(&args.labelled_transition_system, args.format).ok_or_else(|| {

        format!(

            args.labelled_transition_system.display()

    })?;

    if format != LtsFormat::Aut {

        return Err(MercError::from(

            "The translate command only works for labelled transition systems in the .aut format.",

        ));

    }

    let mut lts_file = File::open(&args.labelled_transition_system).map_err(|e| {

        MercError::from(format!(

            &args.labelled_transition_system.display(),

    })?;

    let lts = read_aut(&mut lts_file)?;

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

        MercError::from(format!(

            &args.formula_filename.display(),

    })?)?;

    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(&lts, &formula_spec.formula)?;

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

    write_pg(&mut output_file, &vpg)?;

    Ok(())

}

fn handle_translate_vpg(cli: &Cli, args: &TranslateVpgArgs) -> 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.display(),

    })?;

    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.display(),

    })?;

    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.display(),

    })?)?;

    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_vpg(

        &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_else(|| format!("Unknown parity game file format for '{}'.", path.display()))?;

    if format == ParityGameFormat::PG {

        let game = timing.measure("read_pg", || read_pg(&mut file))?;

        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 game = timing.measure("read_vpg", || read_vpg(&manager_ref, &mut file))?;

        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(())

}