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

use conjure_cp::{

    ast::{

        DecisionVariable, DeclarationKind, Expression, Model, Name, comprehension::Comprehension,

    },

    rule_engine::resolve_rule_sets,

    settings::{SolverFamily, current_rewriter},

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

};

use super::via_solver_common::{

    instantiate_return_expressions_from_values, retain_quantified_solution_values,

    rewrite_model_with_configured_rewriter, 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.

    // only branch on the quantified variables.

        target: "rule_engine_human",

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

        generator_model

    );

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

    // 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.

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

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

            ));

    };

        };

        };

    }