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 mut timing = Timing::new();

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

        match command {

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

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

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

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

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

    }

    if cli.timings {

        timing.print();

    }

    print_allocator_metrics();

    Ok(ExitCode::SUCCESS)

}

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

    let mut storage = Storage::new();

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

    match format {

            let lts = timing.measure("read_symbolic_lts", || -> Result<_, MercError> {

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

            })?;

            println!(

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

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

            let lts = timing.measure("read_symbolic_lts", || -> Result<_, MercError> {

                read_symbolic_lts(&mut storage, &mut 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: &mut 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 lts = timing.measure("read_symbolic_lts", || read_sylvan(&mut storage, &mut file))?;

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

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

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

    Ok(())

}

fn explore_impl(

    storage: &mut Storage,

    cli: &Cli,

    args: &ExploreArgs,

    lts: &impl SymbolicLTS,

    timing: &mut 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", || reachability_bdd(

                &manager_ref,

                &lts_bdd,

                args.visualize

            ))?

        println!(

            timing.measure("explore", || reachability(storage, lts))?

    Ok(())

}

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

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

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

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

            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(&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_tool_path {

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

            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 mut order = reorder(&graph)?;

        order.retain(|&x| x != 0);

        println!("Computed variable order: 0, {:?}", order);

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

    Ok(())

}

fn handle_convert(args: &ConvertArgs, _timing: &mut 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: &mut 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)

    })?;

    timing.measure("reduction", || sigref_symbolic(&manager_ref, &lts_bdd, timing, args.visualize))?;

    Ok(())

}