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

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

        File::create(path)?.write_all(pretty_json.as_bytes())?;

    }

    Ok(())

}

pub(crate) fn init_context(

    global_args: &GlobalArgs,

    input_file: PathBuf,

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

    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 global_args.no_use_expand_ac {

        extra_rule_sets.pop_if(|x| x == &"Better_AC_Comprehension_Expansion");

    }

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

    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(family: SolverFamily) -> Solver {

    match family {

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

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

        SolverFamily::Smt(TheoryConfig { ints, matrices }) => Solver::new(Smt::new(ints, matrices)),

}

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

    if global_args.use_native_parser {

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

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

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

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

    let new_model = if global_args.use_optimised_rewriter {

        USE_OPTIMISED_REWRITER_FOR_COMPREHENSIONS.store(true, std::sync::atomic::Ordering::Relaxed);

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

        rewrite_morph(

            model,

            &rule_sets,

            global_args.check_equally_applicable_rules,

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

        if global_args.exit_after_unrolling {

            tracing::info!("Exiting after unrolling");

        }

        rewrite_naive(

            &model,

            &rule_sets,

            global_args.check_equally_applicable_rules,

            global_args.exit_after_unrolling,

        )?

    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,

        Some(pth) => Some(

            File::options()

                .create(true)

                .truncate(true)

                .write(true)

                .open(pth)?,

    let solutions = get_solutions(

        solver,

        model,

        cmd_args.number_of_solutions,

        &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())?;

            println!(

                &cmd_args.output.clone().unwrap().canonicalize()?

    Ok(())

}