use std::{

    collections::{HashMap, VecDeque},

    sync::{Arc, Mutex, RwLock, atomic::Ordering},

};

use conjure_cp::{

    ast::{

        Atom, DecisionVariable, DeclarationKind, DeclarationPtr, Expression, Metadata, Model, Moo,

        Name, ReturnType, SubModel, SymbolTable, Typeable as _,

        ac_operators::ACOperatorKind,

        comprehension::{Comprehension, USE_OPTIMISED_REWRITER_FOR_COMPREHENSIONS},

        serde::{HasId as _, ObjId},

    },

    bug,

    context::Context,

    rule_engine::{resolve_rule_sets, rewrite_morph, rewrite_naive},

    settings::SolverFamily,

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

};

use tracing::warn;

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

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

///

/// If successful, this modifies the symbol table given to add aux-variables needed inside the

/// expanded expressions.

    // ADD RETURN EXPRESSION TO GENERATOR MODEL AS CONSTRAINT

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

    // References to quantified variables in the return expression point to entries in the

    // return_expression symbol table.

    //

    // Change these to point to the corresponding entry in the generator symbol table instead.

    //

    // In the generator symbol-table, quantified variables are decision variables (as we are

    // solving for them), but in the return expression symbol table they are givens.

                // if this variable is a quantified var...

                    // ... use the generator symbol tables version of it

                } else {

                }

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

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

    // only branch on the quantified variables.

    // Minion unrolling expects quantified variables in the generator model as find declarations.

    // Keep this conversion local to the temporary model used for solving.

    );

    } else {

    };

        }

    };

    // REWRITE RETURN EXPRESSION

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

        } else {

        };

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

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

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

        // TODO: deal with represented names if quantified variables are abslits.

        // convert back to an expression

        // we only want to substitute quantified variables.

        // (definitely not machine names, as they mean something different in this scope!)

        // substitute in the values for the quantified variables

            };

            // is this referencing a quantified var?

            };

        // Copy the return expression's symbols into parent scope.

        // For variables in the return expression with machine names, create new declarations

        // for them in the parent symbol table, so that the machine names used are unique.

        //

        // Store the declaration translations in `machine_name_translations`.

        // These are stored as a map of (old declaration id) -> (new declaration ptr), as

        // declaration pointers do not implement hash.

        //

        // Populate `machine_name_translations`

            // do not add quantified declarations for quantified vars to the parent symbol table.

                    DeclarationKind::Given(_) | DeclarationKind::Quantified(_)

                )

            {

                bug!(

                    "the symbol table of the return expression of a comprehension should only contain machine names"

                );

            };

        }

        // Update references to use the new delcarations.

        #[allow(clippy::arc_with_non_send_sync)]

            {

            } else {

            }

    }

/// Guard that temporarily converts quantified declarations to find declarations.

struct TempQuantifiedFindGuard {

    originals: Vec<(DeclarationPtr, DeclarationKind)>,

}

impl Drop for TempQuantifiedFindGuard {

}

/// Converts quantified declarations in `submodel` to temporary find declarations.

        };

        };

    }

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

    );

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