use std::collections::{HashSet, VecDeque};

use std::fmt::{Display, Formatter};

use std::hash::{DefaultHasher, Hash, Hasher};

use std::sync::atomic::{AtomicU64, Ordering};

static HASH_HITS: AtomicU64 = AtomicU64::new(0);

static HASH_MISSES: AtomicU64 = AtomicU64::new(0);

        "Expression hash stats: hits={}, misses={}",

    );

use tracing::trace;

use conjure_cp_enum_compatibility_macro::{document_compatibility, generate_discriminants};

use itertools::Itertools;

use serde::{Deserialize, Serialize};

use tree_morph::cache::CacheHashable;

use ustr::Ustr;

use polyquine::Quine;

use uniplate::{Biplate, Uniplate};

use crate::ast::metadata::NO_HASH;

use crate::bug;

use super::abstract_comprehension::AbstractComprehension;

use super::ac_operators::ACOperatorKind;

use super::categories::{Category, CategoryOf};

use super::comprehension::Comprehension;

use super::domains::HasDomain as _;

use super::pretty::{pretty_expressions_as_top_level, pretty_vec};

use super::records::RecordValue;

use super::sat_encoding::SATIntEncoding;

use super::{

    AbstractLiteral, Atom, DeclarationPtr, Domain, DomainPtr, GroundDomain, IntVal, Literal,

    Metadata, Model, Moo, Name, Range, Reference, ReturnType, SetAttr, SymbolTable, SymbolTablePtr,

    Typeable, UnresolvedDomain, matrix,

};

// Ensure that this type doesn't get too big

//

// If you triggered this assertion, you either made a variant of this enum that is too big, or you

// made Name,Literal,AbstractLiteral,Atom bigger, which made this bigger! To fix this, put some

// stuff in boxes.

//

// Enums take the size of their largest variant, so an enum with mostly small variants and a few

// large ones wastes memory... A larger Expression type also slows down Oxide.

//

// For more information, and more details on type sizes and how to measure them, see the commit

// message for 6012de809 (perf: reduce size of AST types, 2025-06-18).

//

// You can also see type sizes in the rustdoc documentation, generated by ./tools/gen_docs.sh

//

// https://github.com/conjure-cp/conjure-oxide/commit/6012de8096ca491ded91ecec61352fdf4e994f2e

// TODO: box all usages of Metadata to bring this down a bit more - I have added variants to

// ReturnType, and Metadata contains ReturnType, so Metadata has got bigger. Metadata will get a

// lot bigger still when we start using it for memoisation, so it should really be

// boxed ~niklasdewally

// expect size of Expression to be 112 bytes

static_assertions::assert_eq_size!([u8; 112], Expression);

/// Represents different types of expressions used to define rules and constraints in the model.

///

/// The `Expression` enum includes operations, constants, and variable references

/// used to build rules and conditions for the model.

#[generate_discriminants]

#[document_compatibility]

#[derive(Clone, Debug, Hash, PartialEq, Eq, Serialize, Deserialize, Uniplate, Quine)]

#[biplate(to=AbstractComprehension)]

#[biplate(to=AbstractLiteral<Expression>)]

#[biplate(to=AbstractLiteral<Literal>)]

#[biplate(to=Atom)]

#[biplate(to=Comprehension)]

#[biplate(to=DeclarationPtr)]

#[biplate(to=DomainPtr)]

#[biplate(to=Literal)]

#[biplate(to=Metadata)]

#[biplate(to=Name)]

#[biplate(to=Option<Expression>)]

#[biplate(to=RecordValue<Expression>)]

#[biplate(to=RecordValue<Literal>)]

#[biplate(to=Reference)]

#[biplate(to=Model)]

#[biplate(to=SymbolTable)]

#[biplate(to=SymbolTablePtr)]

#[biplate(to=Vec<Expression>)]

#[path_prefix(conjure_cp::ast)]

pub enum Expression {

    AbstractLiteral(Metadata, AbstractLiteral<Expression>),

    /// The top of the model

    Root(Metadata, Vec<Expression>),

    /// An expression representing "A is valid as long as B is true"

    /// Turns into a conjunction when it reaches a boolean context

    Bubble(Metadata, Moo<Expression>, Moo<Expression>),

    /// A comprehension.

    ///

    /// The inside of the comprehension opens a new scope.

    // todo (gskorokhod): Comprehension contains a symbol table which contains a bunch of pointers.

    // This makes implementing Quine tricky (it doesnt support Rc, by design). Skip it for now.

    #[polyquine_skip]

    Comprehension(Metadata, Moo<Comprehension>),

    /// Higher-level abstract comprehension

    #[polyquine_skip] // no idea what this is lol but it stops rustc screaming at me

    AbstractComprehension(Metadata, Moo<AbstractComprehension>),

    /// Defines dominance ("Solution A is preferred over Solution B")

    DominanceRelation(Metadata, Moo<Expression>),

    /// `fromSolution(name)` - Used in dominance relation definitions

    FromSolution(Metadata, Moo<Atom>),

    #[polyquine_with(arm = (_, name) => {

        let ident = proc_macro2::Ident::new(name.as_str(), proc_macro2::Span::call_site());

        quote::quote! { #ident.clone().into() }

    })]

    Metavar(Metadata, Ustr),

    Atomic(Metadata, Atom),

    /// A matrix index.

    ///

    /// Defined iff the indices are within their respective index domains.

    #[compatible(JsonInput)]

    UnsafeIndex(Metadata, Moo<Expression>, Vec<Expression>),

    /// A safe matrix index.

    ///

    /// See [`Expression::UnsafeIndex`]

    #[compatible(SMT)]

    SafeIndex(Metadata, Moo<Expression>, Vec<Expression>),

    /// A matrix slice: `a[indices]`.

    ///

    /// One of the indicies may be `None`, representing the dimension of the matrix we want to take

    /// a slice of. For example, for some 3d matrix a, `a[1,..,2]` has the indices

    /// `Some(1),None,Some(2)`.

    ///

    /// It is assumed that the slice only has one "wild-card" dimension and thus is 1 dimensional.

    ///

    /// Defined iff the defined indices are within their respective index domains.

    #[compatible(JsonInput)]

    UnsafeSlice(Metadata, Moo<Expression>, Vec<Option<Expression>>),

    /// A safe matrix slice: `a[indices]`.

    ///

    /// See [`Expression::UnsafeSlice`].

    SafeSlice(Metadata, Moo<Expression>, Vec<Option<Expression>>),

    /// `inDomain(x,domain)` iff `x` is in the domain `domain`.

    ///

    /// This cannot be constructed from Essence input, nor passed to a solver: this expression is

    /// mainly used during the conversion of `UnsafeIndex` and `UnsafeSlice` to `SafeIndex` and

    /// `SafeSlice` respectively.

    InDomain(Metadata, Moo<Expression>, DomainPtr),

    /// `toInt(b)` casts boolean expression b to an integer.

    ///

    /// - If b is false, then `toInt(b) == 0`

    ///

    /// - If b is true, then `toInt(b) == 1`

    #[compatible(SMT)]

    ToInt(Metadata, Moo<Expression>),

    /// `|x|` - absolute value of `x`

    #[compatible(JsonInput, SMT)]

    Abs(Metadata, Moo<Expression>),

    /// `sum(<vec_expr>)`

    #[compatible(JsonInput, SMT)]

    Sum(Metadata, Moo<Expression>),

    /// `a * b * c * ...`

    #[compatible(JsonInput, SMT)]

    Product(Metadata, Moo<Expression>),

    /// `min(<vec_expr>)`

    #[compatible(JsonInput, SMT)]

    Min(Metadata, Moo<Expression>),

    /// `max(<vec_expr>)`

    #[compatible(JsonInput, SMT)]

    Max(Metadata, Moo<Expression>),

    /// `not(a)`

    #[compatible(JsonInput, SAT, SMT)]

    Not(Metadata, Moo<Expression>),

    /// `or(<vec_expr>)`

    #[compatible(JsonInput, SAT, SMT)]

    Or(Metadata, Moo<Expression>),

    /// `and(<vec_expr>)`

    #[compatible(JsonInput, SAT, SMT)]

    And(Metadata, Moo<Expression>),

    /// Ensures that `a->b` (material implication).

    #[compatible(JsonInput, SMT)]

    Imply(Metadata, Moo<Expression>, Moo<Expression>),

    /// `iff(a, b)` a <-> b

    #[compatible(JsonInput, SMT)]

    Iff(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput)]

    Union(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput)]

    In(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput)]

    Intersect(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput)]

    Supset(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput)]

    SupsetEq(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput)]

    Subset(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput)]

    SubsetEq(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput, SMT)]

    Eq(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput, SMT)]

    Neq(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput, SMT)]

    Geq(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput, SMT)]

    Leq(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput, SMT)]

    Gt(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput, SMT)]

    Lt(Metadata, Moo<Expression>, Moo<Expression>),

    /// Division after preventing division by zero, usually with a bubble

    #[compatible(SMT)]

    SafeDiv(Metadata, Moo<Expression>, Moo<Expression>),

    /// Division with a possibly undefined value (division by 0)

    #[compatible(JsonInput)]

    UnsafeDiv(Metadata, Moo<Expression>, Moo<Expression>),

    /// Modulo after preventing mod 0, usually with a bubble

    #[compatible(SMT)]

    SafeMod(Metadata, Moo<Expression>, Moo<Expression>),

    /// Modulo with a possibly undefined value (mod 0)

    #[compatible(JsonInput)]

    UnsafeMod(Metadata, Moo<Expression>, Moo<Expression>),

    /// Negation: `-x`

    #[compatible(JsonInput, SMT)]

    Neg(Metadata, Moo<Expression>),

    /// Factorial: `x!` or 'factorial(x)`

    #[compatible(JsonInput)]

    Factorial(Metadata, Moo<Expression>),

    /// Set of domain values function is defined for

    #[compatible(JsonInput)]

    Defined(Metadata, Moo<Expression>),

    /// Set of codomain values function is defined for

    #[compatible(JsonInput)]

    Range(Metadata, Moo<Expression>),

    /// Unsafe power`x**y` (possibly undefined)

    ///

    /// Defined when (X!=0 \\/ Y!=0) /\ Y>=0

    #[compatible(JsonInput)]

    UnsafePow(Metadata, Moo<Expression>, Moo<Expression>),

    /// `UnsafePow` after preventing undefinedness

    SafePow(Metadata, Moo<Expression>, Moo<Expression>),

    /// Flatten matrix operator

    /// `flatten(M)` or `flatten(n, M)`

    /// where M is a matrix and n is an optional integer argument indicating depth of flattening

    Flatten(Metadata, Option<Moo<Expression>>, Moo<Expression>),

    /// `allDiff(<vec_expr>)`

    #[compatible(JsonInput)]

    AllDiff(Metadata, Moo<Expression>),

    /// `table([x1, x2, ...], [[r11, r12, ...], [r21, r22, ...], ...])`

    ///

    /// Represents a positive table constraint: the tuple `[x1, x2, ...]` must match one of the

    /// allowed rows.

    #[compatible(JsonInput)]

    Table(Metadata, Moo<Expression>, Moo<Expression>),

    /// `negativeTable([x1, x2, ...], [[r11, r12, ...], [r21, r22, ...], ...])`

    ///

    /// Represents a negative table constraint: the tuple `[x1, x2, ...]` must NOT match any of the

    /// forbidden rows.

    #[compatible(JsonInput)]

    NegativeTable(Metadata, Moo<Expression>, Moo<Expression>),

    /// Binary subtraction operator

    ///

    /// This is a parser-level construct, and is immediately normalised to `Sum([a,-b])`.

    /// TODO: make this compatible with Set Difference calculations - need to change return type and domain for this expression and write a set comprehension rule.

    /// have already edited minus_to_sum to prevent this from applying to sets

    #[compatible(JsonInput)]

    Minus(Metadata, Moo<Expression>, Moo<Expression>),

    /// Ensures that x=|y| i.e. x is the absolute value of y.

    ///

    /// Low-level Minion constraint.

    ///

    /// # See also

    ///

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#abs)

    #[compatible(Minion)]

    FlatAbsEq(Metadata, Moo<Atom>, Moo<Atom>),

    /// Ensures that `alldiff([a,b,...])`.

    ///

    /// Low-level Minion constraint.

    ///

    /// # See also

    ///

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#alldiff)

    #[compatible(Minion)]

    FlatAllDiff(Metadata, Vec<Atom>),

    /// Ensures that sum(vec) >= x.

    ///

    /// Low-level Minion constraint.

    ///

    /// # See also

    ///

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#sumgeq)

    #[compatible(Minion)]

    FlatSumGeq(Metadata, Vec<Atom>, Atom),

    /// Ensures that sum(vec) <= x.

    ///

    /// Low-level Minion constraint.

    ///

    /// # See also

    ///

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#sumleq)

    #[compatible(Minion)]

    FlatSumLeq(Metadata, Vec<Atom>, Atom),

    /// `ineq(x,y,k)` ensures that x <= y + k.

    ///

    /// Low-level Minion constraint.

    ///

    /// # See also

    ///

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#ineq)

    #[compatible(Minion)]

    FlatIneq(Metadata, Moo<Atom>, Moo<Atom>, Box<Literal>),

    /// `w-literal(x,k)` ensures that x == k, where x is a variable and k a constant.

    ///

    /// Low-level Minion constraint.

    ///

    /// This is a low-level Minion constraint and you should probably use Eq instead. The main use

    /// of w-literal is to convert boolean variables to constraints so that they can be used inside

    /// watched-and and watched-or.

    ///

    /// # See also

    ///

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#minuseq)

    /// + `rules::minion::boolean_literal_to_wliteral`.

    #[compatible(Minion)]

    #[polyquine_skip]

    FlatWatchedLiteral(Metadata, Reference, Literal),

    /// `weightedsumleq(cs,xs,total)` ensures that cs.xs <= total, where cs.xs is the scalar dot

    /// product of cs and xs.

    ///

    /// Low-level Minion constraint.

    ///

    /// Represents a weighted sum of the form `ax + by + cz + ...`

    ///

    /// # See also

    ///

    /// + [Minion

    /// documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#weightedsumleq)

    FlatWeightedSumLeq(Metadata, Vec<Literal>, Vec<Atom>, Moo<Atom>),

    /// `weightedsumgeq(cs,xs,total)` ensures that cs.xs >= total, where cs.xs is the scalar dot

    /// product of cs and xs.

    ///

    /// Low-level Minion constraint.

    ///

    /// Represents a weighted sum of the form `ax + by + cz + ...`

    ///

    /// # See also

    ///

    /// + [Minion

    /// documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#weightedsumleq)

    FlatWeightedSumGeq(Metadata, Vec<Literal>, Vec<Atom>, Moo<Atom>),

    /// Ensures that x =-y, where x and y are atoms.

    ///

    /// Low-level Minion constraint.

    ///

    /// # See also

    ///

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#minuseq)

    #[compatible(Minion)]

    FlatMinusEq(Metadata, Moo<Atom>, Moo<Atom>),

    /// Ensures that x*y=z.

    ///

    /// Low-level Minion constraint.

    ///

    /// # See also

    ///

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#product)

    #[compatible(Minion)]

    FlatProductEq(Metadata, Moo<Atom>, Moo<Atom>, Moo<Atom>),

    /// Ensures that floor(x/y)=z. Always true when y=0.

    ///

    /// Low-level Minion constraint.

    ///

    /// # See also

    ///

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#div_undefzero)

    #[compatible(Minion)]

    MinionDivEqUndefZero(Metadata, Moo<Atom>, Moo<Atom>, Moo<Atom>),

    /// Ensures that x%y=z. Always true when y=0.

    ///

    /// Low-level Minion constraint.

    ///

    /// # See also

    ///

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#mod_undefzero)

    #[compatible(Minion)]

    MinionModuloEqUndefZero(Metadata, Moo<Atom>, Moo<Atom>, Moo<Atom>),

    /// Ensures that `x**y = z`.

    ///

    /// Low-level Minion constraint.

    ///

    /// This constraint is false when `y<0` except for `1**y=1` and `(-1)**y=z` (where z is 1 if y

    /// is odd and z is -1 if y is even).

    ///

    /// # See also

    ///

    /// + [Github comment about `pow` semantics](https://github.com/minion/minion/issues/40#issuecomment-2595914891)

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#pow)

    MinionPow(Metadata, Moo<Atom>, Moo<Atom>, Moo<Atom>),

    /// `reify(constraint,r)` ensures that r=1 iff `constraint` is satisfied, where r is a 0/1

    /// variable.

    ///

    /// Low-level Minion constraint.

    ///

    /// # See also

    ///

    ///  + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#reify)

    #[compatible(Minion)]

    MinionReify(Metadata, Moo<Expression>, Atom),

    /// `reifyimply(constraint,r)` ensures that `r->constraint`, where r is a 0/1 variable.

    /// variable.

    ///

    /// Low-level Minion constraint.

    ///

    /// # See also

    ///

    ///  + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#reifyimply)

    #[compatible(Minion)]

    MinionReifyImply(Metadata, Moo<Expression>, Atom),

    /// `w-inintervalset(x, [a1,a2, b1,b2, … ])` ensures that the value of x belongs to one of the

    /// intervals {a1,…,a2}, {b1,…,b2} etc.

    ///

    /// The list of intervals must be given in numerical order.

    ///

    /// Low-level Minion constraint.

    ///

    /// # See also

    ///>

    ///  + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#w-inintervalset)

    #[compatible(Minion)]

    MinionWInIntervalSet(Metadata, Atom, Vec<i32>),

    /// `w-inset(x, [v1, v2, … ])` ensures that the value of `x` is one of the explicitly given values `v1`, `v2`, etc.

    ///

    /// This constraint enforces membership in a specific set of discrete values rather than intervals.

    ///

    /// The list of values must be given in numerical order.

    ///

    /// Low-level Minion constraint.

    ///

    /// # See also

    ///

    ///  + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#w-inset)

    #[compatible(Minion)]

    MinionWInSet(Metadata, Atom, Vec<i32>),

    /// `element_one(vec, i, e)` specifies that `vec[i] = e`. This implies that i is

    /// in the range `[1..len(vec)]`.

    ///

    /// Low-level Minion constraint.

    ///

    /// # See also

    ///

    ///  + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#element_one)

    #[compatible(Minion)]

    MinionElementOne(Metadata, Vec<Atom>, Moo<Atom>, Moo<Atom>),

    /// Declaration of an auxiliary variable.

    ///

    /// As with Savile Row, we semantically distinguish this from `Eq`.

    #[compatible(Minion)]

    #[polyquine_skip]

    AuxDeclaration(Metadata, Reference, Moo<Expression>),

    /// This expression is for encoding ints for the SAT solver, it stores the encoding type, the vector of booleans and the min/max for the int.

    #[compatible(SAT)]

    SATInt(Metadata, SATIntEncoding, Moo<Expression>, (i32, i32)),

    /// Addition over a pair of expressions (i.e. a + b) rather than a vec-expr like Expression::Sum.

    /// This is for compatibility with backends that do not support addition over vectors.

    #[compatible(SMT)]

    PairwiseSum(Metadata, Moo<Expression>, Moo<Expression>),

    /// Multiplication over a pair of expressions (i.e. a * b) rather than a vec-expr like Expression::Product.

    /// This is for compatibility with backends that do not support multiplication over vectors.

    #[compatible(SMT)]

    PairwiseProduct(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput)]

    Image(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput)]

    ImageSet(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput)]

    PreImage(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput)]

    Inverse(Metadata, Moo<Expression>, Moo<Expression>),

    #[compatible(JsonInput)]

    Restrict(Metadata, Moo<Expression>, Moo<Expression>),

    /// Lexicographical < between two matrices.

    ///

    /// A <lex B iff: A[i] < B[i] for some i /\ (A[j] > B[j] for some j -> i < j)

    /// I.e. A must be less than B at some index i, and if it is greater than B at another index j,

    /// then j comes after i.

    /// I.e. A must be greater than B at the first index where they differ.

    ///

    /// E.g. [1, 1] <lex [2, 1] and [1, 1] <lex [1, 2]

    LexLt(Metadata, Moo<Expression>, Moo<Expression>),

    /// Lexicographical <= between two matrices

    LexLeq(Metadata, Moo<Expression>, Moo<Expression>),

    /// Lexicographical > between two matrices

    /// This is a parser-level construct, and is immediately normalised to LexLt(b, a)

    LexGt(Metadata, Moo<Expression>, Moo<Expression>),

    /// Lexicographical >= between two matrices

    /// This is a parser-level construct, and is immediately normalised to LexLeq(b, a)

    LexGeq(Metadata, Moo<Expression>, Moo<Expression>),

    /// Low-level minion constraint. See Expression::LexLt

    FlatLexLt(Metadata, Vec<Atom>, Vec<Atom>),

    /// Low-level minion constraint. See Expression::LexLeq

    FlatLexLeq(Metadata, Vec<Atom>, Vec<Atom>),

}

// for the given matrix literal, return a bounded domain from the min to max of applying op to each

// child expression.

//

// Op must be monotonic.

//

// Returns none if unbounded

    // only care about the elements, not the indices

    // fold each element's domain into one using op.

    //

    // here, I assume that op is monotone. This means that the bounds of op([a1,a2],[b1,b2])  for

    // the ranges [a1,a2], [b1,b2] will be

    // [min(op(a1,b1),op(a2,b1),op(a1,b2),op(a2,b2)),max(op(a1,b1),op(a2,b1),op(a1,b2),op(a2,b2))].

    //

    // We used to not assume this, and work out the bounds by applying op on the Cartesian product

    // of A and B; however, this caused a combinatorial explosion and my computer to run out of

    // memory (on the hakank_eprime_xkcd test)...

    //Int

    // For example, to find the bounds of the intervals [1,4], [1,5] combined using op, we used to do

    //  [min(op(1,1), op(1,2),op(1,3),op(1,4),op(1,5),op(2,1)..

    //

    // +,-,/,* are all monotone, so this assumption should be fine for now...

    };

        };

        // all the possible new values for current_min / current_max

    }

    } else {

    }

// Returns none if unbounded

            }

            }

        }

    }

impl Expression {

    /// Returns the possible values of the expression, recursing to leaf expressions

            )),

            )),

                // may actually use the value in the future

                #[allow(clippy::redundant_pattern_matching)]

                    // TODO: We can implement proper indexing for tuples

                // may actually use the value in the future

                #[allow(clippy::redundant_pattern_matching)]

                    // TODO: We can implement proper indexing for records

                bug!("subject of an index operation should support indexing")

            }

                    bug!("subject of an index operation should be a matrix");

                };

                    // same as index

                }

            }

            }

            }

                    // rust integer division is truncating; however, we want to always round down,

                    // including for negative numbers.

                        } else {

                        }

                )

                // rust integer division is truncating; however, we want to always round down

                // including for negative numbers.

                            } else {

                            }

                    )

                    .unwrap_or_else(|err| bug!("Got {err} when computing domain of {self}"));

                } else {

                    bug!("Domain of {self} was not integer")

                }

            }

                )

                    )

                    .unwrap_or_else(|err| bug!("Got {err} when computing domain of {self}"));

                } else {

                    bug!("Domain of {self} was not integer")

                }

            }

                        } else {

                        }

                )

                        // TODO: handle flatten with depth argument

                } else {

                    // TODO: currently only works for matrices

                    };

                }

            }

            }

            }

            }

        }

    /// Returns a reference to this expression's metadata without cloning.

        macro_rules! match_meta_ref {

            ($($variant:ident),* $(,)?) => {

                match self {

                    $(Expression::$variant(meta, ..) => meta,)*

                }

            };

        }

            AbstractLiteral,

            Root,

            Bubble,

            Comprehension,

            AbstractComprehension,

            DominanceRelation,

            FromSolution,

            Metavar,

            Atomic,

            UnsafeIndex,

            SafeIndex,

            UnsafeSlice,

            SafeSlice,

            InDomain,

            ToInt,

            Abs,

            Sum,

            Product,

            Min,

            Max,

            Not,

            Or,

            And,

            Imply,

            Iff,

            Union,

            In,

            Intersect,

            Supset,

            SupsetEq,

            Subset,

            SubsetEq,

            Eq,

            Neq,

            Geq,

            Leq,

            Gt,

            Lt,

            SafeDiv,

            UnsafeDiv,

            SafeMod,

            UnsafeMod,

            Neg,

            Defined,

            Range,

            UnsafePow,

            SafePow,

            Flatten,

            AllDiff,

            Minus,

            Factorial,

            FlatAbsEq,

            FlatAllDiff,

            FlatSumGeq,

            FlatSumLeq,

            FlatIneq,

            FlatWatchedLiteral,

            FlatWeightedSumLeq,

            FlatWeightedSumGeq,

            FlatMinusEq,

            FlatProductEq,

            MinionDivEqUndefZero,

            MinionModuloEqUndefZero,

            MinionPow,

            MinionReify,

            MinionReifyImply,

            MinionWInIntervalSet,

            MinionWInSet,

            MinionElementOne,

            AuxDeclaration,

            SATInt,

            PairwiseSum,

            PairwiseProduct,

            Image,

            ImageSet,

            PreImage,

            Inverse,

            Restrict,

            LexLt,

            LexLeq,

            LexGt,

            LexGeq,

            FlatLexLt,

            FlatLexLeq,

            NegativeTable,

            Table

        )

    /// Checks whether this expression is safe.

    ///

    /// An expression is unsafe if can be undefined, or if any of its children can be undefined.

    ///

    /// Unsafe expressions are (typically) prefixed with Unsafe in our AST, and can be made

    /// safe through the use of bubble rules.

        // TODO: memoise in Metadata

                Expression::UnsafeDiv(_, _, _)

                | Expression::UnsafeMod(_, _, _)

                | Expression::UnsafePow(_, _, _)

                | Expression::UnsafeIndex(_, _, _)

                | Expression::Bubble(_, _, _)

                | Expression::UnsafeSlice(_, _, _) => {

                }

            }

        }

    /// True if the expression is an associative and commutative operator

    /// True if the expression is a matrix literal.

    ///

    /// This is true for both forms of matrix literals: those with elements of type [`Literal`] and

    /// [`Expression`].

            Expression::AbstractLiteral(_, AbstractLiteral::Matrix(_, _))

                | Expression::Atomic(

                    _,

                    Atom::Literal(Literal::AbstractLiteral(AbstractLiteral::Matrix(_, _))),

                )

        )

    /// True iff self and other are both atomic and identical.

    ///

    /// This method is useful to cheaply check equivalence. Assuming CSE is enabled, any unifiable

    /// expressions will be rewritten to a common variable. This is much cheaper than checking the

    /// entire subtrees of `self` and `other`.

        } else {

        }

    /// If the expression is a list, returns a *copied* vector of the inner expressions.

    ///

    /// A list is any a matrix with the domain `int(1..)`. This includes matrix literals without

    /// any explicitly specified domain.

            }

            Expression::Atomic(

                _,

        }

    /// If the expression is a matrix, gets it elements and index domain.

    ///

    /// **Consider using the safer [`Expression::unwrap_list`] instead.**

    ///

    /// It is generally undefined to edit the length of a matrix unless it is a list (as defined by

    /// [`Expression::unwrap_list`]). Users of this function should ensure that, if the matrix is

    /// reconstructed, the index domain and the number of elements in the matrix remain the same.

            }

            Expression::Atomic(

                _,

            ) => Some((

            )),

        }

    /// For a Root expression, extends the inner vec with the given vec.

    ///

    /// # Panics

    /// Panics if the expression is not Root.

            }

        }

    /// Converts the expression to a literal, if possible.

            }

                    bug!("negated literal should be an int");

                };

            }

        }

    /// If this expression is an associative-commutative operator, return its [ACOperatorKind].

    /// Returns the categories of all sub-expressions of self.

}

                // Not defined for anything other than a function

            }

        }

        None => {

                // Not defined for anything other than a function

            }

        }

    }

                // Not defined for anything other than a function

            }

        }

        None => {

                // Not defined for anything other than a function

            }

        }

    }

impl TryFrom<&Expression> for i32 {

    type Error = ();

        };

        };

        };

}

impl TryFrom<Expression> for i32 {

    type Error = ();

}

impl From<i32> for Expression {

}

impl From<bool> for Expression {

}

impl From<Atom> for Expression {

}