fn as_solver_limit(self) -> i32 {

        match self {

            NumberOfSolutions::All => 0,

            NumberOfSolutions::Limit(limit) => limit,

        }

    }

}

fn parse_number_of_solutions(input: &str) -> Result<NumberOfSolutions, String> {

    if input.eq_ignore_ascii_case("all") {

        return Ok(NumberOfSolutions::All);

    }

    let limit = input

        .parse::<i32>()

        .map_err(|_| "expected a positive integer or 'all'".to_string())?;

    if limit <= 0 {

        return Err("expected a positive integer or 'all'".to_string());

    }

    Ok(NumberOfSolutions::Limit(limit))

}

pub fn run_solve_command(global_args: GlobalArgs, solve_args: Args) -> anyhow::Result<()> {

    let input_file = solve_args.input_file.clone();

    let context = init_context(&global_args, input_file)?;

    let model = parse(&global_args, Arc::clone(&context))?;

    let rewritten_model = rewrite(model, &global_args, Arc::clone(&context))?;

    let solver = init_solver(&global_args);

    if solve_args.no_run_solver {

        println!("{}", &rewritten_model);

        if let Some(path) = global_args.save_solver_input_file {

            let solver = solver.load_model(rewritten_model)?;

            eprintln!("Writing solver input file to {}", path.display());

            let mut file: Box<dyn std::io::Write> = Box::new(File::create(path)?);

            solver.write_solver_input_file(&mut file)?;

        }

        run_solver(solver, &global_args, &solve_args, rewritten_model)?

    }

    if let Some(ref path) = solve_args.info_json_path {

        let context_obj = context.read().unwrap().clone();

        let generated_json = &serde_json::to_value(context_obj)?;

        let pretty_json = serde_json::to_string_pretty(&generated_json)?;

    }

    Ok(())

}

pub(crate) fn init_context(

    global_args: &GlobalArgs,

    input_file: PathBuf,

) -> anyhow::Result<Arc<RwLock<Context<'static>>>> {

    set_current_parser(global_args.parser);

    set_current_rewriter(global_args.rewriter);

    set_comprehension_expander(global_args.comprehension_expander);

    set_current_solver_family(global_args.solver);

    set_minion_discrete_threshold(global_args.minion_discrete_threshold);

    let target_family = global_args.solver;

    let mut extra_rule_sets: Vec<&str> = DEFAULT_RULE_SETS.to_vec();

    for rs in &global_args.extra_rule_sets {

        extra_rule_sets.push(rs.as_str());

    if let SolverFamily::Sat(sat_encoding) = target_family {

        extra_rule_sets.push(sat_encoding.as_rule_set());

    }

    let rule_sets = match resolve_rule_sets(target_family, &extra_rule_sets) {

        Ok(rs) => rs,

        Err(e) => {

            tracing::error!("Error resolving rule sets: {}", e);

            exit(1);

    };

    let pretty_rule_sets = rule_sets

        .iter()

        .map(|rule_set| rule_set.name)

        .collect::<Vec<_>>()

        .join(", ");

    tracing::info!("Enabled rule sets: [{}]", pretty_rule_sets);

    tracing::info!(

        target: "file",

        "Rule sets: {}",

        pretty_rule_sets

    );

    let rules = get_rules(&rule_sets)?.into_iter().collect::<Vec<_>>();

    tracing::info!(

        rules.iter().map(|rd| format!("{rd}")).collect::<Vec<_>>().join("\n")

    );

    let context = Context::new_ptr(

        target_family,

        extra_rule_sets.iter().map(|rs| rs.to_string()).collect(),

        rules,

        rule_sets.clone(),

    context.write().unwrap().file_name = Some(input_file.to_str().expect("").into());

    Ok(context)

}

pub(crate) fn init_solver(global_args: &GlobalArgs) -> Solver {

    let family = global_args.solver;

    let timeout_ms = global_args

        .solver_timeout

        .map(|dur| Duration::from(dur).as_millis())

        .map(|timeout_ms| u64::try_from(timeout_ms).expect("Timeout too large"));

    match family {

        SolverFamily::Minion => Solver::new(Minion::default()),

        SolverFamily::Sat(_) => Solver::new(Sat::default()),

}

pub(crate) fn parse(

    global_args: &GlobalArgs,

    context: Arc<RwLock<Context<'static>>>,

) -> anyhow::Result<Model> {

    let input_file: String = context

        .read()

        .unwrap()

        .file_name

        .clone()

        .expect("context should contain the input file");

    tracing::info!(target: "file", "Input file: {}", input_file);

    match global_args.parser {

            parse_essence_file_native(input_file.as_str(), context.clone()).map_err(|e| e.into())

        }

        conjure_cp::settings::Parser::ViaConjure => {

            conjure_executable()

                .map_err(|e| anyhow!("Could not find correct conjure executable: {e}"))?;

            let mut cmd = std::process::Command::new("conjure");

            let output = cmd

                .arg("pretty")

                .arg("--output-format=astjson")

                .arg(input_file)

                .output()?;

            let conjure_stderr = String::from_utf8(output.stderr)?;

            ensure!(conjure_stderr.is_empty(), conjure_stderr);

            let astjson = String::from_utf8(output.stdout)?;

            if cfg!(feature = "extra-rule-checks") {

                tracing::info!("extra-rule-checks: enabled");

            } else {

                tracing::info!("extra-rule-checks: disabled");

            model_from_json(&astjson, context.clone()).map_err(|e| anyhow!(e))

}

pub(crate) fn rewrite(

    model: Model,

    global_args: &GlobalArgs,

    context: Arc<RwLock<Context<'static>>>,

) -> anyhow::Result<Model> {

    tracing::info!("Initial model: \n{}\n", model);

    set_current_rewriter(global_args.rewriter);

    let comprehension_expander = global_args.comprehension_expander;

    set_comprehension_expander(comprehension_expander);

    tracing::info!("Comprehension expander: {}", comprehension_expander);

    let rule_sets = context.read().unwrap().rule_sets.clone();

    let new_model = match global_args.rewriter {

        Rewriter::Morph => {

            tracing::info!("Rewriting the model using the morph rewriter");

                model,

                &rule_sets,

            )

        }

        Rewriter::Naive => {

            tracing::info!("Rewriting the model using the default / naive rewriter");

            rewrite_naive(

                &model,

                &rule_sets,

                global_args.check_equally_applicable_rules,

            )?

    tracing::info!("Rewritten model: \n{}\n", new_model);

    Ok(new_model)

}

fn run_solver(

    solver: Solver,

    global_args: &GlobalArgs,

    cmd_args: &Args,

    model: Model,

) -> anyhow::Result<()> {

    let out_file: Option<File> = match &cmd_args.output {

        None => None,

            File::options()

                .truncate(true)

                .open(pth)?,

        ),

    };

    let solutions = get_solutions(

        solver,

        model,

        cmd_args.number_of_solutions.as_solver_limit(),

        &global_args.save_solver_input_file,

    )?;

    tracing::info!(target: "file", "Solutions: {}", solutions_to_json(&solutions));

    let solutions_json = solutions_to_json(&solutions);

    let solutions_str = to_string_pretty(&solutions_json)?;

    match out_file {

        None => {

            println!("Solutions:");

            println!("{solutions_str}");

        }

        Some(mut outf) => {

            outf.write_all(solutions_str.as_bytes())?;

        }

    }

    Ok(())

}