//! The two ways to give Z3 an `allDifferent`.

//!

//! Both rules sit in the `Smt` rule set at the same priority, so they are equally applicable to any

//! `allDifferent` and the heuristic picks between them: `-h i` asks, `-h x` enumerates both, and

//! `-h c`/`-h f` take the first. Whichever wins rewrites the expression, so the choice is recorded

//! in the model and is not asked again on the next visit.

//!

//! `distinct` is usually the better of the two, but not always -- Z3 sometimes does better with the

//! counting encoding, which is why this is a choice rather than a fixed lowering.

use conjure_cp::ast::matrix::safe_index_optimised;

use conjure_cp::ast::{

    AbstractLiteral, Expression as Expr, GroundDomain, Metadata, Moo, SymbolTable,

};

use conjure_cp::essence_expr;

use conjure_cp::rule_engine::{

    ApplicationError::{DomainError, RuleNotApplicable},

    ApplicationResult, RuleEffect, register_rule,

};

/// Hand `allDifferent` to Z3 as its native `distinct`.

#[register_rule("Smt", 4000, [AllDiff])]

    };

/// Encode `allDifferent` as "no value occurs more than once" instead of using `distinct`.

#[register_rule("Smt", 4000, [AllDiff])]

    };

    let Ok(GroundDomain::Matrix(val_domain, index_domains, _)) =

    else {

    };

    };

    // Counting occurrences means enumerating the element domain and testing each entry against

    // every value in it. That only reads as `allDifferent` when the entries are scalars: for a

    // matrix of matrices the "values" are whole rows, and the encoding would compare a row against

    // whatever the chosen layout left each entry as. `distinct` handles those natively.