use std::sync::{Arc, Mutex};

use conjure_cp::{

    ast::{

        Expression,

        comprehension::{Comprehension, ComprehensionQualifier},

    },

    rule_engine::resolve_rule_sets,

    settings::{SolverFamily, current_rewriter},

    solver::{Solver, SolverError, adaptors::Minion},

};

use super::via_solver_common::{

    detach_symbols, instantiate_return_expressions_from_values, retain_quantified_solution_values,

    rewrite_model_with_configured_rewriter, split_symbolic_guards,

    temporarily_materialise_quantified_vars_as_finds, with_temporary_model,

};

/// Expands the comprehension by solving quantified variables with Minion.

///

/// This returns one expression per assignment to quantified variables that satisfies the static

/// guards of the comprehension. Guards that reference non-quantified decision variables cannot be

/// solved here; they are held back and re-applied to each expanded element under the enclosing AC

/// operator's skip semantics.

    // An empty generator domain -- `int(1..exposedBlock-1)` where an enclosing comprehension has

    // just bound `exposedBlock` to 1 -- yields no elements at all. Building a generator model for

    // it would materialise a find over an empty domain, which Minion cannot hold.

    // The generator model shares the comprehension's symbol table, and rewriting it introduces

    // auxiliary declarations. Detach that table first: the auxiliaries belong to this throwaway

    // model, and leaving them in the comprehension's own scope would put them in the *next*

    // generator model built from the same scope -- as unconstrained finds Minion then branches on,

    // multiplying the assignments and so duplicating the expanded elements. Sibling comprehensions

    // produced by instantiating one return expression share a scope, so this really happens.

    // Quantified variables are shared declarations, so materialise them as finds only for as long

    // as this model needs them.

    let _temp_finds =

    // only branch on the quantified variables.

        target: "rule_engine_rule_trace",

        "Via-solver generator model before rewriting:\n\n{}\n--\n",

    );

    // call rewrite here as well as in expand_via_solver_ac, just to be consistent

    let generator_model =

    // Call the rewriter to rewrite inside the comprehension

    //

    // The original idea was to let the top level rewriter rewrite the return expression model

    // and the generator model. The comprehension wouldn't be expanded until the generator

    // model is in valid minion that can be ran, at which point the return expression model

    // should also be in valid minion.

    //

    // By calling the rewriter inside the rule, we no longer wait for the generator model to be

    // valid Minion, so we don't get the simplified return model either...

    //

    // We need to do this as we want to modify the generator model (add the dummy Z's) then

    // solve and return in one go.

    //

    // Comprehensions need a big rewrite soon, as theres lots of sharp edges such as this in

    // my original implementation, and I don't think we can fit our new optimisation into it.

    // If we wanted to avoid calling the rewriter, we would need to run the first half the rule

    // up to adding the return expr to the generator model, yield, then come back later to

    // actually solve it?

    // Keep return expressions unreduced until quantified assignments are substituted.

    // Rewriting before substitution can change guard structure in ways that are unsafe for

    // constant evaluation after instantiation.

    let return_expression_model =

    let values = {

        tracing::debug!(model=%generator_model,comprehension=%comprehension,"Minion solving comprehension (solver mode)");

            // Only keep quantified assignments; discard solver auxiliaries/locals.

    };

/// Whether any domain generator of `comprehension` ranges over nothing.

        };