use std::{

    cell::RefCell,

    collections::{HashMap, VecDeque},

    sync::{Arc, Mutex},

};

use conjure_cp::{

    ast::{

        Atom, DeclarationPtr, Expression, Metadata, Model, Moo, Name, Reference, ReturnType,

        SymbolTable, Typeable as _,

        ac_operators::ACOperatorKind,

        comprehension::{Comprehension, ComprehensionQualifier},

        serde::HasId as _,

    },

    rule_engine::resolve_rule_sets,

    settings::{SolverFamily, current_rewriter},

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

};

use tracing::warn;

use uniplate::{Biplate, Uniplate as _, zipper::Zipper};

use super::via_solver_common::{

    instantiate_return_expressions_from_values, retain_quantified_solution_values,

    rewrite_model_with_configured_rewriter, temporarily_materialise_quantified_vars_as_finds,

    with_temporary_model,

};

/// Expands the comprehension using Minion, returning the resulting expressions.

///

/// This method is only suitable for comprehensions inside an AC operator. The AC operator that

/// contains this comprehension should be passed into the `ac_operator` argument.

///

/// This method performs additional pruning of "uninteresting" values, only possible when the

/// comprehension is inside an AC operator.

    // ADD RETURN EXPRESSION TO GENERATOR MODEL AS CONSTRAINT

    // ======================================================

    // Replace all boolean expressions referencing non-quantified variables in the return

    // expression with dummy variables. This allows us to add it as a constraint to the

    // generator model.

    );

    // REWRITE GENERATOR MODEL AND PASS TO MINION

    // ==========================================

    // REWRITE RETURN EXPRESSION

    // =========================

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

    // Rewriting before substitution can introduce index auxiliaries that remain symbolic and may

    // produce unsupported Minion shapes after expansion.

        // Minion expects quantified variables in the temporary generator model as find

        // declarations. Keep this conversion scoped to solver-backed expansion.

        // Rewrite with quantified vars materialised as finds so Minion flattening can

        // introduce auxiliaries for constraints involving quantified variables.

            }

        };

        // SOLVE FOR THE QUANTIFIED VARIABLES, AND SUBSTITUTE INTO THE RETURN EXPRESSION

        // ============================================================================

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

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

            ));

    };

/// Eliminate all references to non-quantified variables by introducing dummy variables to the

/// return expression. This modified return expression is added to the generator model, which is

/// returned.

///

/// Dummy variables must be the same type as the AC operators identity value.

///

/// To reduce the number of dummy variables, we turn the largest expression containing only

/// non-quantified variables and of the correct type into a dummy variable.

///

/// If there is no such expression, (e.g. and[(a<i) | i: int(1..10)]) , we use the smallest

/// expression of the correct type that contains a non-quantified variable. This ensures that

/// we lose as few references to quantified variables as possible.

    // for sum/product we want to put integer expressions into dummy variables,

    // for and/or we want to put boolean expressions into dummy variables.

    'outer: loop {

        // an expression or its descendants needs to be turned into a dummy variable if it

        // contains non-quantified variables.

        // does this expression contain quantified variables?

        // can this expression be turned into a dummy variable?

        // The expression and its descendants don't need a dummy variables, so we don't

        // need to descend into its children.

            // go to next node or quit

                    // visited all nodes

                };

            }

        // The expression contains non-quantified variables:

        // does this expression have any children that can be turned into dummy variables?

            // eligible if it can be turned into a dummy variable, and turning it into a

            // dummy variable removes a non-quantified variable from the model.

        // This expression has no child that can be turned into a dummy variable, but can

        // be a dummy variable => turn it into a dummy variable and continue.

            // introduce dummy var and continue

            // go to next node

                    // visited all nodes

                };

            }

        }

        // This expression has no child that can be turned into a dummy variable, and

        // cannot be a dummy variable => backtrack upwards to find a parent that can be a

        // dummy variable, and make it a dummy variable.

            // TODO: remove this case, make has_eligible_child check better?

            // go upwards until we find something that can be a dummy variable, make it

            // a dummy variable, then continue.

                    // TODO: this expression we are rewritng might already contain

                    // dummy vars - we might need a pass to get rid of the unused

                    // ones!

                    //

                    // introduce dummy var and continue

                    // go to next node

                            // visited all nodes

                        };

                    }

            }

        }

        // If the expression contains quantified variables as well as non-quantified

        // variables, try to retain the quantified variables by finding a child that can be

        // made a dummy variable which has only non-quantified variables.

        // This expression contains no quantified variables, so no point trying to turn a

        // child into a dummy variable.

            // introduce dummy var and continue

            // go to next node

                    // visited all nodes

                };

            }

        } else {

        }

    }

    // double check that the above transformation didn't miss any stray non-quantified vars

        "generator model should only contain references to variables in its symbol table."

    );

/// Replaces references to declarations outside `symtab` with local dummy declarations.

///

/// This preserves locality by construction for temporary generator models passed to Minion.

/// All rewrites then operate purely on local references and cannot reintroduce parent-scope vars.

        {

            );

            }

        }

        };

        // Already local to this temporary generator model.

        } else {

                });

            };

        };

/// Returns a tuple of non-quantified decision variables and quantified variables inside the expression.

///

/// As lettings, givens, etc. will eventually be subsituted for constants, this only returns

/// non-quantified _decision_ variables.

#[inline]

    // doing this as two functions non_quantified_variables and quantified_variables might've been

    // easier to read.

    //

    // However, doing this in one function avoids an extra universe call...

/// Returns `true` if `expr` can be turned into a dummy variable.

#[inline]

    // do not put root expression in a dummy variable or things go wrong.

    // is the expression the same type as the dummy variable?

/// Returns `true` if `expr` or its descendants contains non-quantified variables.

#[inline]

    // a name is a non-quantified variable if its definition is not in the local scope of the

    // comprehension's generators.