fn init_bdd_manager(cli: &Cli) -> oxidd::bdd::BDDManagerRef {

    oxidd::bdd::new_manager(

        cli.oxidd_node_capacity,

        cli.oxidd_cache_capacity.unwrap_or(cli.oxidd_node_capacity),

        cli.oxidd_workers,

}

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

    let cli = Cli::parse();

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

    }

    let timing = Timing::new();

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

        match command {

            Commands::Info(args) => handle_info(args, &timing)?,

            Commands::Explore(args) => handle_explore(&cli, args, &timing)?,

            Commands::Reorder(args) => handle_reorder(args, &timing)?,

            Commands::Convert(args) => handle_convert(args, &timing)?,

            Commands::Reduce(args) => handle_reduce(&cli, args, &timing)?,

    }

    if cli.timings {

        timing.print();

    }

    print_allocator_metrics();

    Ok(ExitCode::SUCCESS)

}

fn handle_info(args: &InfoArgs, timing: &Timing) -> Result<(), MercError> {

    let mut storage = Storage::new();

    let format =

        guess_format_from_extension(&args.filename, args.format).ok_or("Cannot determine input symbolic LTS format")?;

    if format != SymFormat::Sym {

        return Err("Currently only the .sym format is supported for info".into());

    }

    let lts = timing.measure("read_symbolic_lts", || {

        read_symbolic_lts(&mut storage, File::open(&args.filename)?)

    })?;

    println!(

        LargeFormatter(merc_ldd::len(&mut storage, lts.states()))

    println!("Number of summand groups: {}", lts.transition_groups().len());

    Ok(())

}

fn handle_explore(cli: &Cli, args: &ExploreArgs, timing: &Timing) -> Result<(), MercError> {

    let mut storage = Storage::new();

    let format = guess_format_from_extension(&args.filename, args.format).ok_or("Cannot determine input format")?;

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

    match format {

            let mut lts = timing.measure("read_symbolic_lts", || read_sylvan(&mut storage, &mut file))?;

            explore_impl(&mut storage, cli, args, &mut lts, timing)?;

            let mut lts = timing.measure("read_symbolic_lts", || read_symbolic_lts(&mut storage, &mut file))?;

            explore_impl(&mut storage, cli, args, &mut lts, timing)?;

    Ok(())

}

fn explore_impl<L: SymbolicLTS>(

    storage: &mut Storage,

    cli: &Cli,

    args: &ExploreArgs,

    lts: &mut L,

    timing: &Timing,

) -> Result<(), MercError> {

    if args.use_bdd {

        let manager_ref = init_bdd_manager(cli);

        let lts_bdd = timing.measure("convert_bdd", || {

            SymbolicLtsBdd::from_symbolic_lts(storage, &manager_ref, lts)

        })?;

        println!(

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

                let reachable_states_bdd = reachability_bdd(&manager_ref, &lts_bdd, args.visualize)?;

                let num_reachable_states_bdd = reachable_states_bdd.sat_count::<u64, FxBuildHasher>(

                    lts_bdd.state_variables().len() as u32,

                    &mut SatCountCache::default(),

                ) as usize;

                Ok(num_reachable_states_bdd)

            })?

        println!(

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

                let states = reachability(storage, lts, timing)?;

                Ok(len(storage, &states))

            })?

    Ok(())

}

fn handle_reorder(args: &ReorderArgs, _timing: &Timing) -> Result<(), MercError> {

    let kahypar_path = if let Some(path) = &args.kahypar_path {

        which_in("KaHyPar", Some(path), std::env::current_dir()?).map_err(|_e| "Cannot find KaHyPar")?

        which::which("KaHyPar").map_err(|_e| "Cannot find KaHyPar in PATH")?

    let kahypar_ini_path = if let Some(path) = &args.kahypar_ini_path {

        if !path.is_file() {

            return Err(format!(

                "The specified kahypar.ini path '{}' does not exist or is not a file.",

                path.display()

            )

            .into());

        }

        path.clone()

        let mut default_kahypar_ini_path = std::env::current_exe()?;

        default_kahypar_ini_path.pop(); // remove the executable filename

        default_kahypar_ini_path.push("kahypar.ini");

        if !default_kahypar_ini_path.is_file() {

            return Err(format!(

                "Could not find '{}'. The 'kahypar.ini' file must be present next to the executable, or passed via --kahypar-ini-path.",

                default_kahypar_ini_path.display()

            )

            .into());

        }

        default_kahypar_ini_path

    if args.filename.extension() == Some(OsStr::new("lps")) {

        let lpsreach_path = if let Some(path) = &args.mcrl2_path {

            which_in("lpsreach", Some(path), std::env::current_dir()?).map_err(|_e| "Cannot find lpsreach")?

            which::which("lpsreach").map_err(|_e| "Cannot find lpsreach in PATH")?

        let proc = duct::cmd!(lpsreach_path, "--info", &args.filename)

            .stdout_capture()

            .run()

            .map_err(|e| e.to_string())?;

        let graph = parse_compacted_dependency_graph(str::from_utf8(&proc.stdout)?);

        let order = reorder(&kahypar_path, &kahypar_ini_path, &graph)?;

        println!("Computed variable order: {}", order.iter().format(" "));

    } else if args.filename.extension() == Some(OsStr::new("pbes")) {

        let pbessolvesymbolic = if let Some(path) = &args.mcrl2_path {

            which_in("pbessolvesymbolic", Some(path), std::env::current_dir()?)

                .map_err(|_e| "Cannot find pbessolvesymbolic")?

            which::which("pbessolvesymbolic").map_err(|_e| "Cannot find pbessolvesymbolic in PATH")?

        let proc = duct::cmd!(pbessolvesymbolic, "--info", &args.filename)

            .stdout_capture()

            .run()

            .map_err(|e| e.to_string())?;

        let graph = parse_compacted_dependency_graph(str::from_utf8(&proc.stdout)?);

        let order = reorder(&kahypar_path, &kahypar_ini_path, &graph)?;

        println!(

            order.iter().filter(|&x| *x != 0).format(" ")

        return Err("Input file must be either a .lps or .pbes file".into());

    Ok(())

}

fn handle_convert(args: &ConvertArgs, _timing: &Timing) -> Result<(), MercError> {

    let mut storage = Storage::new();

    let format =

        guess_format_from_extension(&args.filename, args.format).ok_or("Cannot determine input symbolic LTS format")?;

    if format != SymFormat::Sym {

        return Err("Currently only the .sym format is supported for conversion".into());

    }

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

    let lts = read_symbolic_lts(&mut storage, &mut file)?;

    let output_format = guess_lts_format_from_extension(&args.output, args.output_format)

        .ok_or("Cannot determine output LTS format")?;

    match output_format {

            unimplemented!("Writing LTS format is not yet implemented");

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

            let mut stream = AutStream::new(&mut output);

            convert_symbolic_lts(&mut storage, &mut stream, &lts)?;

            let explicit_lts =

                convert_symbolic_lts(&mut storage, &mut LtsBuilderMem::new(Vec::new(), Vec::new()), &lts)?;

            write_bcg(&explicit_lts, &args.output)?;

    Ok(())

}

fn handle_reduce(cli: &Cli, args: &ReduceArgs, timing: &Timing) -> Result<(), MercError> {

    let format =

        guess_format_from_extension(&args.filename, args.format).ok_or("Cannot determine input symbolic LTS format")?;

    if format != SymFormat::Sym {

        return Err("Currently only the .sym format is supported for conversion".into());

    }

    let mut storage = Storage::new();

    let manager_ref = init_bdd_manager(cli);

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

    let lts = read_symbolic_lts(&mut storage, &mut file)?;

    let lts_bdd = timing.measure("convert_bdd", || {

        SymbolicLtsBdd::from_symbolic_lts(&mut storage, &manager_ref, &lts)

    })?;

    let _quotient = timing.measure("reduction", || -> Result<BDDFunction, MercError> {

        match args.equivalence {

            Equivalence::StrongBisimSigref => sigref_symbolic(

                &manager_ref,

                &lts_bdd,

                timing,

                args.split_signature,

                args.extend_relation,

                args.merge_transitions,

                args.visualize,

            .map(|(quotient, _, _)| quotient),

            Equivalence::StrongBisim => refine_bisimulation(&manager_ref, &lts_bdd),

    })?;

    Ok(())

}