tessellate-core 0.1.0

use crate::ast::{
    BinaryOp, Declaration, Effect, Expr, ExprKind, FieldDecl, InvariantAssertion, InvariantDecl,
    InvariantQuantifier, Literal, NumericLiteral, RuleDecl, TypeRef,
};
use crate::compiler::{CompiledProgram, normalize_name};
use crate::engine::{
    DecisionStatus, Evaluation, Input, Query, constant_value, evaluate_condition, evaluate_query,
    resolve_rule_bindings,
};
use crate::solver::{SolverMetadata, SolverMode, SolverOutcome, solve_invariant};
use crate::value::{TruthValue, Value, parse_decimal};
use chrono::NaiveDate;
use rust_decimal::Decimal;
use serde::{Deserialize, Serialize};
use std::collections::{BTreeMap, BTreeSet};
use std::fmt::Write;

#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct AnalysisOptions {
    /// Hard cap on concrete inputs or exact representatives evaluated per invariant.
    /// Symbolic solver queries do not consume this budget.
    pub max_evaluations: usize,
    /// Stop concrete exploration after collecting this many counterexamples.
    pub max_counterexamples: usize,
}

impl Default for AnalysisOptions {
    fn default() -> Self {
        Self {
            max_evaluations: 100_000,
            max_counterexamples: 3,
        }
    }
}

#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum Completeness {
    /// Every value in every finite field range was enumerated.
    Exhaustive,
    /// One representative from every exact rule-threshold equivalence region was enumerated.
    ThresholdPartitioned,
    /// The embedded solver decided the exact quantifier-specific query in its supported theory.
    SolverExact,
    /// All generated boundary candidates were enumerated, but the domain was reduced.
    BoundarySampled,
    /// Verification stopped before covering the full plan, possibly after decisive evidence.
    Truncated,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum AnalysisVerdict {
    Passed,
    Failed,
    Inconclusive,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum CounterexampleKind {
    Undefined,
    Overdetermined,
    Unknown,
    Conflict,
    PropertyViolation,
}

#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct Counterexample {
    pub invariant: String,
    pub kind: CounterexampleKind,
    pub input: Input,
    pub reason: String,
    #[serde(skip_serializing_if = "Option::is_none")]
    pub evaluation: Option<Evaluation>,
}

#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct InvariantAnalysis {
    pub invariant: String,
    /// The source-level quantifier whose proof result this record describes.
    #[serde(
        default = "default_invariant_quantifier",
        skip_serializing_if = "is_universal_quantifier"
    )]
    pub quantifier: InvariantQuantifier,
    pub verdict: AnalysisVerdict,
    pub evaluated: usize,
    pub planned_evaluations: usize,
    pub completeness: Completeness,
    #[serde(skip_serializing_if = "Option::is_none")]
    pub solver: Option<SolverMetadata>,
    /// A concrete, evaluator-replayed assignment satisfying `for some`.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub witness: Option<Input>,
    pub counterexamples: Vec<Counterexample>,
    #[serde(default, skip_serializing_if = "Vec::is_empty")]
    pub notes: Vec<String>,
}

const fn default_invariant_quantifier() -> InvariantQuantifier {
    InvariantQuantifier::All
}

// Serde's `skip_serializing_if` contract passes the field by reference even
// though this enum is `Copy`.
#[allow(clippy::trivially_copy_pass_by_ref)]
fn is_universal_quantifier(quantifier: &InvariantQuantifier) -> bool {
    *quantifier == InvariantQuantifier::All
}

#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct StaticFinding {
    pub code: String,
    pub message: String,
}

#[derive(Clone, Debug, Default, Serialize, Deserialize)]
pub struct AnalysisReport {
    pub invariants: Vec<InvariantAnalysis>,
    #[serde(default, skip_serializing_if = "Vec::is_empty")]
    pub traces: Vec<crate::trace::TraceAnalysis>,
    pub findings: Vec<StaticFinding>,
}

impl AnalysisReport {
    #[must_use]
    pub fn success(&self) -> bool {
        (!self.invariants.is_empty() || !self.traces.is_empty())
            && self
                .invariants
                .iter()
                .all(|invariant| invariant.verdict == AnalysisVerdict::Passed)
            && self
                .traces
                .iter()
                .all(|trace| trace.verdict == AnalysisVerdict::Passed)
    }

    /// Render a concise, stable report for humans.
    ///
    /// Machine completeness names, solver metadata, and diagnostic notes remain
    /// available through serialization and the structured fields above.
    #[must_use]
    pub fn render_text(&self) -> String {
        let mut out = String::new();
        for finding in &self.findings {
            let _ = writeln!(out, "! {} · {}", finding.code, finding.message);
        }
        if !self.findings.is_empty() && (!self.invariants.is_empty() || !self.traces.is_empty()) {
            out.push('\n');
        }
        for (invariant_index, invariant) in self.invariants.iter().enumerate() {
            if invariant_index > 0 {
                out.push('\n');
            }
            let (marker, verdict) = match (invariant.quantifier, invariant.verdict) {
                (InvariantQuantifier::All, AnalysisVerdict::Passed) => {
                    ("✓", "proved for all inputs")
                }
                (InvariantQuantifier::Some, AnalysisVerdict::Passed) => {
                    ("✓", "satisfying input found")
                }
                (InvariantQuantifier::Some, AnalysisVerdict::Failed)
                    if invariant.counterexamples.is_empty() =>
                {
                    ("✗", "no satisfying input exists")
                }
                (_, AnalysisVerdict::Failed) if invariant.counterexamples.is_empty() => {
                    ("✗", "failed")
                }
                (_, AnalysisVerdict::Failed) => ("✗", "counterexample found"),
                (_, AnalysisVerdict::Inconclusive) => ("?", "inconclusive"),
            };
            let _ = writeln!(out, "{marker} {}", invariant.invariant);
            let _ = write!(out, "  {verdict}");
            let has_existential_witness = invariant.quantifier == InvariantQuantifier::Some
                && invariant.verdict == AnalysisVerdict::Passed
                && invariant.witness.is_some();
            if has_existential_witness && invariant.completeness != Completeness::SolverExact {
                let evaluations = format_count(invariant.evaluated);
                let noun = pluralized(invariant.evaluated, "evaluation", "evaluations");
                let _ = write!(out, " · after {evaluations} {noun}");
            } else {
                match invariant.completeness {
                    Completeness::Exhaustive => {
                        let combinations = format_count(invariant.planned_evaluations);
                        let noun = pluralized(
                            invariant.planned_evaluations,
                            "combination",
                            "combinations",
                        );
                        let _ = write!(out, " · all {combinations} {noun} checked");
                    }
                    Completeness::ThresholdPartitioned => {
                        let regions = format_count(invariant.evaluated);
                        let noun = pluralized(invariant.evaluated, "exact region", "exact regions");
                        let _ = write!(out, " · {regions} {noun} checked");
                    }
                    Completeness::SolverExact => {
                        out.push_str(" · exact solver");
                        if let Some(solver) = &invariant.solver {
                            let backend = if solver.backend.eq_ignore_ascii_case("z3") {
                                "Z3"
                            } else {
                                &solver.backend
                            };
                            let _ = write!(out, " ({backend})");
                        }
                    }
                    Completeness::BoundarySampled => {
                        let samples = format_count(invariant.evaluated);
                        let noun =
                            pluralized(invariant.evaluated, "boundary sample", "boundary samples");
                        let _ = write!(out, " · {samples} {noun} checked");
                        if invariant.verdict == AnalysisVerdict::Inconclusive {
                            out.push_str(" · not exhaustive");
                        }
                    }
                    Completeness::Truncated => {
                        let evaluated = format_count(invariant.evaluated);
                        if invariant.planned_evaluations == usize::MAX {
                            let _ = write!(out, " · {evaluated} evaluations · truncated");
                        } else {
                            let candidates = format_count(invariant.planned_evaluations);
                            let _ = write!(
                                out,
                                " · {evaluated} of {candidates} evaluations · truncated"
                            );
                        }
                    }
                }
            }
            out.push('\n');

            if invariant.verdict == AnalysisVerdict::Inconclusive
                || (invariant.verdict == AnalysisVerdict::Failed
                    && invariant.counterexamples.is_empty())
            {
                for note in invariant.notes.iter().filter(|note| human_note(note)) {
                    let _ = writeln!(out, "  reason · {note}");
                }
            }

            if let Some(witness) = &invariant.witness {
                out.push_str("\n  witness\n");
                for (binding, entity) in &witness.bindings {
                    let _ = writeln!(out, "    {binding}: {} {{", entity.entity);
                    for (field, value) in &entity.fields {
                        let _ = writeln!(out, "      {field}: {value},");
                    }
                    out.push_str("    }\n");
                }
            }

            for counterexample in &invariant.counterexamples {
                let kind = match counterexample.kind {
                    CounterexampleKind::Undefined => "undefined",
                    CounterexampleKind::Overdetermined => "overdetermined",
                    CounterexampleKind::Unknown => "unknown",
                    CounterexampleKind::Conflict => "conflict",
                    CounterexampleKind::PropertyViolation => "property violation",
                };
                let _ = writeln!(out, "\n  counterexample · {kind}");
                let _ = writeln!(out, "    reason · {}", counterexample.reason);
                for (binding, entity) in &counterexample.input.bindings {
                    let _ = writeln!(out, "    {binding}: {} {{", entity.entity);
                    for (field, value) in &entity.fields {
                        let _ = writeln!(out, "      {field}: {value},");
                    }
                    out.push_str("    }\n");
                }
                if let Some(evaluation) = &counterexample.evaluation {
                    for line in evaluation.render_text().lines() {
                        let _ = writeln!(out, "    {line}");
                    }
                }
            }
        }
        for (trace_index, trace) in self.traces.iter().enumerate() {
            if !self.invariants.is_empty() || trace_index > 0 {
                out.push('\n');
            }
            out.push_str(&trace.render_text());
        }
        out
    }
}

fn pluralized<'a>(count: usize, singular: &'a str, plural: &'a str) -> &'a str {
    if count == 1 { singular } else { plural }
}

fn format_count(count: usize) -> String {
    let digits = count.to_string();
    let mut grouped = String::with_capacity(digits.len() + digits.len() / 3);
    for (index, digit) in digits.chars().enumerate() {
        if index > 0 && (digits.len() - index) % 3 == 0 {
            grouped.push(',');
        }
        grouped.push(digit);
    }
    grouped
}

fn human_note(note: &str) -> bool {
    note != "used an exact threshold partition: every representative stands for a region with identical relevant rule and invariant outcomes"
        && note
            != "integer/decimal domains were reduced to endpoints and comparison boundaries; absence of a counterexample is not a proof"
        && note
            != "integer/decimal domains were reduced to endpoints and comparison boundaries; absence of a satisfying input does not prove that none exists"
        && !note.starts_with("stopped at the configured evaluation limit of ")
}

#[derive(Clone, Debug)]
struct FieldDomain {
    name: String,
    values: Vec<Option<Value>>,
}

#[derive(Clone, Debug)]
struct QuantifiedDomain {
    binding: String,
    entity: String,
    fields: Vec<FieldDomain>,
}

/// Concrete exhaustive fields are stored in `Vec`s. Keep one maliciously large
/// `--max-evaluations` value from turning a valid analysis request into an OOM;
/// larger fields use the exact threshold quotient or the sampled fallback.
const MAX_MATERIALIZED_VALUES_PER_FIELD: usize = 1_000_000;

/// Exact representative enumeration is generally cheaper and more stable than
/// starting the SMT solver at this scale. Larger exact plans are retained as a
/// fallback, but the embedded solver gets the first chance to avoid thousands
/// of evaluator calls.
const EAGER_EXACT_ENUMERATION_LIMIT: usize = 1_024;

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
enum DomainMode {
    Exhaustive,
    ThresholdPartitioned,
    BoundarySampled,
}

impl DomainMode {
    const fn completeness(self) -> Completeness {
        match self {
            Self::Exhaustive => Completeness::Exhaustive,
            Self::ThresholdPartitioned => Completeness::ThresholdPartitioned,
            Self::BoundarySampled => Completeness::BoundarySampled,
        }
    }
}

/// Analyze declared invariants with exact quotient enumeration, the embedded solver,
/// or a conservative deterministic boundary sample.
#[must_use]
pub fn analyze(
    program: &CompiledProgram,
    selected_invariant: Option<&str>,
    options: &AnalysisOptions,
) -> AnalysisReport {
    analyze_with_solver(program, selected_invariant, options, SolverMode::Auto)
}

/// Analyze invariants with compact exact enumeration first, then the embedded
/// solver, and only materialize a larger finite Cartesian product as a fallback.
#[must_use]
pub fn analyze_with_solver(
    program: &CompiledProgram,
    selected_invariant: Option<&str>,
    options: &AnalysisOptions,
    solver_mode: SolverMode,
) -> AnalysisReport {
    let mut invariants = program
        .ast()
        .declarations
        .iter()
        .filter_map(|declaration| match declaration {
            Declaration::Invariant(invariant)
                if selected_invariant.is_none_or(|selected| invariant.name.value == selected) =>
            {
                Some(invariant)
            }
            _ => None,
        })
        .collect::<Vec<_>>();
    invariants.sort_by(|left, right| left.name.value.cmp(&right.name.value));

    AnalysisReport {
        invariants: invariants
            .into_iter()
            .map(|invariant| analyze_invariant(program, invariant, options, solver_mode))
            .collect(),
        traces: if selected_invariant.is_none() {
            crate::trace::analyze_traces(program, None, options)
        } else {
            Vec::new()
        },
        findings: static_findings(program),
    }
}

fn analyze_invariant(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
    options: &AnalysisOptions,
    solver_mode: SolverMode,
) -> InvariantAnalysis {
    if invariant.variables.is_empty() {
        return InvariantAnalysis {
            invariant: invariant.name.value.clone(),
            quantifier: invariant.quantifier,
            verdict: AnalysisVerdict::Failed,
            evaluated: 0,
            planned_evaluations: 0,
            completeness: Completeness::Truncated,
            solver: None,
            witness: None,
            counterexamples: Vec::new(),
            notes: vec!["an invariant must quantify at least one entity variable".into()],
        };
    }
    let mut quantified = Vec::new();
    for variable in &invariant.variables {
        let Some(entity) = program.entity(&variable.ty.value) else {
            return InvariantAnalysis {
                invariant: invariant.name.value.clone(),
                quantifier: invariant.quantifier,
                verdict: AnalysisVerdict::Failed,
                evaluated: 0,
                planned_evaluations: 0,
                completeness: Completeness::Truncated,
                solver: None,
                witness: None,
                counterexamples: Vec::new(),
                notes: vec![format!(
                    "invariant variable type `{}` is not an entity",
                    variable.ty.value
                )],
            };
        };
        quantified.push((variable, entity));
    }

    let exhaustive_size = quantified_domain_size(program, &quantified);
    let fields_materializable = quantified_fields_materializable(program, &quantified);
    let materialization_limited = exhaustive_size
        .is_some_and(|size| size <= options.max_evaluations && !fields_materializable);
    let exhaustive_within_limit = exhaustive_size
        .is_some_and(|size| size <= options.max_evaluations && fields_materializable);
    let eager_limit = options.max_evaluations.min(EAGER_EXACT_ENUMERATION_LIMIT);

    // An explicit `z3` request tries the solver before any concrete strategy.
    // If the exact fragment is unsupported, deterministic exact/sampled
    // fallbacks remain available and retain the reason in their notes.
    let mut requested_solver_note = if solver_mode == SolverMode::Z3 {
        match solver_exact_analysis(program, invariant, solver_mode) {
            Ok(analysis) => return analysis,
            Err(reason) => Some(reason),
        }
    } else {
        None
    };

    // Plan compact exact work before materializing a raw Cartesian product.
    // A compact threshold quotient is preferred in auto mode. If it is unavailable
    // or too large, try the solver before every raw Cartesian product.
    let threshold_plan = threshold_partition_domains(program, invariant);
    let (domains, domain_mode, partition_note) = match threshold_plan {
        Ok(domains) => {
            let threshold_size = planned_evaluation_count(&domains);
            if threshold_size.is_some_and(|size| size <= eager_limit) {
                (
                    domains,
                    DomainMode::ThresholdPartitioned,
                    Some(threshold_partition_note(requested_solver_note.as_deref())),
                )
            } else {
                let solver_note = if requested_solver_note.is_some() {
                    requested_solver_note.take()
                } else if solver_mode == SolverMode::Off {
                    None
                } else {
                    match solver_exact_analysis(program, invariant, solver_mode) {
                        Ok(analysis) => return analysis,
                        Err(reason) => Some(reason),
                    }
                };
                (
                    domains,
                    DomainMode::ThresholdPartitioned,
                    Some(threshold_partition_note(solver_note.as_deref())),
                )
            }
        }
        Err(threshold_reason) => {
            let solver_note = if requested_solver_note.is_some() {
                requested_solver_note.take()
            } else if solver_mode == SolverMode::Off {
                None
            } else {
                match solver_exact_analysis(program, invariant, solver_mode) {
                    Ok(analysis) => return analysis,
                    Err(reason) => Some(reason),
                }
            };
            let mut compact_note =
                format!("exact threshold partitioning was unavailable: {threshold_reason}");
            if let Some(solver_note) = solver_note {
                compact_note.push_str("; ");
                compact_note.push_str(&solver_note);
            }

            if exhaustive_within_limit {
                compact_note.push_str("; enumerated the complete finite domain instead");
                (
                    concrete_domains(program, &quantified, &BTreeSet::new(), true),
                    DomainMode::Exhaustive,
                    Some(compact_note),
                )
            } else {
                let constants = numeric_constants(program);
                (
                    concrete_domains(program, &quantified, &constants, false),
                    DomainMode::BoundarySampled,
                    Some(compact_note),
                )
            }
        }
    };
    let exact_planned_evaluations = planned_evaluation_count(&domains);
    let planned_evaluations = exact_planned_evaluations.unwrap_or(usize::MAX);
    let plan_count_overflowed = exact_planned_evaluations.is_none();
    let limit = planned_evaluations.min(options.max_evaluations);
    let mut evaluated = 0usize;
    let mut counterexamples = Vec::new();
    let mut existential_witness = None;
    let mut stopped_for_counterexamples = false;
    let mut stopped_for_witness = false;

    for ordinal in 0..limit {
        let input = input_at(ordinal, &domains);
        evaluated += 1;
        match invariant.quantifier {
            InvariantQuantifier::All => {
                if let Some(counterexample) = find_invariant_violation(program, invariant, &input) {
                    counterexamples.push(counterexample);
                    if counterexamples.len() >= options.max_counterexamples.max(1) {
                        stopped_for_counterexamples = ordinal + 1 < planned_evaluations;
                        break;
                    }
                }
            }
            InvariantQuantifier::Some => {
                if invariant_has_existential_witness(program, invariant, &input) {
                    stopped_for_witness = ordinal + 1 < planned_evaluations;
                    existential_witness = Some(input);
                    break;
                }
            }
        }
    }

    let completeness = if stopped_for_counterexamples
        || stopped_for_witness
        || plan_count_overflowed
        || planned_evaluations > options.max_evaluations
    {
        Completeness::Truncated
    } else {
        domain_mode.completeness()
    };
    let verdict = match invariant.quantifier {
        InvariantQuantifier::All => {
            if counterexamples.is_empty() {
                if matches!(
                    completeness,
                    Completeness::Exhaustive
                        | Completeness::ThresholdPartitioned
                        | Completeness::SolverExact
                ) {
                    AnalysisVerdict::Passed
                } else {
                    AnalysisVerdict::Inconclusive
                }
            } else {
                AnalysisVerdict::Failed
            }
        }
        InvariantQuantifier::Some if existential_witness.is_some() => AnalysisVerdict::Passed,
        InvariantQuantifier::Some
            if matches!(
                completeness,
                Completeness::Exhaustive | Completeness::ThresholdPartitioned
            ) =>
        {
            AnalysisVerdict::Failed
        }
        InvariantQuantifier::Some => AnalysisVerdict::Inconclusive,
    };
    let mut notes = Vec::new();
    if let Some(note) = partition_note {
        notes.push(note);
    }
    if materialization_limited {
        notes.push(format!(
            "concrete enumeration was not materialized because a field exceeds the internal safety cap of {MAX_MATERIALIZED_VALUES_PER_FIELD} values"
        ));
    }
    if domain_mode == DomainMode::BoundarySampled {
        notes.push(match invariant.quantifier {
            InvariantQuantifier::All => "integer/decimal domains were reduced to endpoints and comparison boundaries; absence of a counterexample is not a proof".into(),
            InvariantQuantifier::Some => "integer/decimal domains were reduced to endpoints and comparison boundaries; absence of a satisfying input does not prove that none exists".into(),
        });
    }
    if planned_evaluations > options.max_evaluations {
        notes.push(format!(
            "stopped at the configured evaluation limit of {}",
            options.max_evaluations
        ));
    }
    if plan_count_overflowed {
        notes.push("the planned evaluation count exceeds this platform's size limit".into());
    }
    if stopped_for_counterexamples {
        notes.push(format!(
            "stopped after {} counterexample(s)",
            options.max_counterexamples.max(1)
        ));
    }
    if stopped_for_witness {
        notes.push("stopped after finding the first satisfying input".into());
    }
    if invariant.quantifier == InvariantQuantifier::Some && verdict == AnalysisVerdict::Failed {
        notes.push(
            "every exact quantified assignment was checked, but none satisfied the assertion"
                .into(),
        );
    }

    InvariantAnalysis {
        invariant: invariant.name.value.clone(),
        quantifier: invariant.quantifier,
        verdict,
        evaluated,
        planned_evaluations,
        completeness,
        solver: None,
        witness: existential_witness,
        counterexamples,
        notes,
    }
}

fn concrete_domains(
    program: &CompiledProgram,
    quantified: &[(&crate::ast::Parameter, &crate::ast::EntityDecl)],
    constants: &BTreeSet<Decimal>,
    exhaustive: bool,
) -> Vec<QuantifiedDomain> {
    quantified
        .iter()
        .map(|(variable, entity)| QuantifiedDomain {
            binding: variable.name.value.clone(),
            entity: variable.ty.value.clone(),
            fields: entity
                .fields
                .iter()
                .map(|field| FieldDomain {
                    name: field.name.value.clone(),
                    values: field_values(program, field, constants, exhaustive),
                })
                .collect(),
        })
        .collect()
}

fn threshold_partition_note(solver_note: Option<&str>) -> String {
    let mut note = "used an exact threshold partition: every representative stands for a region with identical relevant rule and invariant outcomes".to_owned();
    if let Some(solver_note) = solver_note {
        note.push_str("; the solver attempt fell back to this exact partition: ");
        note.push_str(solver_note);
    }
    note
}

fn solver_exact_analysis(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
    solver_mode: SolverMode,
) -> Result<InvariantAnalysis, String> {
    solver_outcome_analysis(
        program,
        invariant,
        solve_invariant(program, invariant, solver_mode),
    )
}

fn solver_outcome_analysis(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
    outcome: SolverOutcome,
) -> Result<InvariantAnalysis, String> {
    match outcome {
        SolverOutcome::Proved(metadata) => {
            if invariant.quantifier != InvariantQuantifier::All {
                return Err("the solver returned a universal proof for `for some`".into());
            }
            Ok(InvariantAnalysis {
                invariant: invariant.name.value.clone(),
                quantifier: invariant.quantifier,
                verdict: AnalysisVerdict::Passed,
                // No concrete input was evaluated. Z3 answered one symbolic query.
                evaluated: 0,
                planned_evaluations: 0,
                completeness: Completeness::SolverExact,
                notes: vec![format!(
                    "the negated property is unsatisfiable in {} via {}",
                    metadata.logic, metadata.version
                )],
                solver: Some(metadata),
                witness: None,
                counterexamples: Vec::new(),
            })
        }
        SolverOutcome::Counterexample { input, metadata } => {
            if invariant.quantifier != InvariantQuantifier::All {
                return Err("the solver returned a universal counterexample for `for some`".into());
            }
            let counterexample = replay_solver_counterexample(program, invariant, &input)?;
            Ok(InvariantAnalysis {
                invariant: invariant.name.value.clone(),
                quantifier: invariant.quantifier,
                verdict: AnalysisVerdict::Failed,
                // One SAT model was replayed, but no Cartesian product was enumerated.
                evaluated: 1,
                planned_evaluations: 0,
                completeness: Completeness::SolverExact,
                notes: vec![format!(
                    "the {} model was replayed by the Tess evaluator",
                    metadata.logic
                )],
                solver: Some(metadata),
                witness: None,
                counterexamples: vec![counterexample],
            })
        }
        SolverOutcome::Witness { input, metadata } => {
            if invariant.quantifier != InvariantQuantifier::Some {
                return Err("the solver returned an existential witness for `for all`".into());
            }
            check_invariant_witness(program, invariant, &input).map_err(|reason| {
                format!("the solver model did not reproduce a satisfying input: {reason}")
            })?;
            Ok(InvariantAnalysis {
                invariant: invariant.name.value.clone(),
                quantifier: invariant.quantifier,
                verdict: AnalysisVerdict::Passed,
                // One SAT model was replayed by the ordinary Tess evaluator.
                evaluated: 1,
                planned_evaluations: 0,
                completeness: Completeness::SolverExact,
                notes: vec![format!(
                    "the satisfying {} model was replayed by the Tess evaluator",
                    metadata.logic
                )],
                solver: Some(metadata),
                witness: Some(input),
                counterexamples: Vec::new(),
            })
        }
        SolverOutcome::Refuted(metadata) => {
            if invariant.quantifier != InvariantQuantifier::Some {
                return Err("the solver returned an existential refutation for `for all`".into());
            }
            Ok(InvariantAnalysis {
                invariant: invariant.name.value.clone(),
                quantifier: invariant.quantifier,
                verdict: AnalysisVerdict::Failed,
                evaluated: 0,
                planned_evaluations: 0,
                completeness: Completeness::SolverExact,
                notes: vec![format!(
                    "no satisfying assignment exists in {} via {}",
                    metadata.logic, metadata.version
                )],
                solver: Some(metadata),
                witness: None,
                counterexamples: Vec::new(),
            })
        }
        SolverOutcome::Unavailable(reason) => Err(format!("embedded solver unavailable: {reason}")),
        SolverOutcome::Unsupported(reason) => {
            Err(format!("solver translation unavailable: {reason}"))
        }
        SolverOutcome::Unknown(reason) => {
            Err(format!("embedded solver was inconclusive: {reason}"))
        }
    }
}

fn replay_solver_counterexample(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
    input: &Input,
) -> Result<Counterexample, String> {
    let Some(counterexample) = find_invariant_violation(program, invariant, input) else {
        return Err("the solver model did not reproduce a violation in the Tess evaluator".into());
    };
    if counterexample.kind == CounterexampleKind::Unknown {
        return Err(format!(
            "the solver model replay needed additional input: {}",
            counterexample.reason
        ));
    }
    Ok(counterexample)
}

fn planned_evaluation_count(domains: &[QuantifiedDomain]) -> Option<usize> {
    domains
        .iter()
        .flat_map(|domain| &domain.fields)
        .try_fold(1usize, |total, field| total.checked_mul(field.values.len()))
}

fn find_invariant_violation(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
    input: &Input,
) -> Option<Counterexample> {
    match &invariant.assertion {
        InvariantAssertion::Cardinality {
            cardinality,
            decision,
            arguments,
            ..
        } => {
            let query = Query {
                decision: decision.value.clone(),
                arguments: arguments
                    .iter()
                    .filter_map(|argument| match &argument.kind {
                        ExprKind::Name(name) => Some(name.clone()),
                        _ => None,
                    })
                    .collect(),
            };
            let evaluation = match evaluate_query(program, input, &query) {
                Ok(evaluation) => evaluation,
                Err(error) => {
                    return Some(Counterexample {
                        invariant: invariant.name.value.clone(),
                        kind: CounterexampleKind::Conflict,
                        input: input.clone(),
                        reason: error.message,
                        evaluation: None,
                    });
                }
            };
            let failure = match (&evaluation.result.status, cardinality) {
                (DecisionStatus::Resolved { values }, crate::ast::Cardinality::ExactlyOne)
                    if values.len() == 1 =>
                {
                    None
                }
                (DecisionStatus::Resolved { values }, crate::ast::Cardinality::ZeroOrOne)
                    if values.len() <= 1 =>
                {
                    None
                }
                (DecisionStatus::Resolved { .. }, crate::ast::Cardinality::Many)
                | (
                    DecisionStatus::Undefined,
                    crate::ast::Cardinality::ZeroOrOne | crate::ast::Cardinality::Many,
                ) => None,
                (DecisionStatus::Undefined, _) => Some((
                    CounterexampleKind::Undefined,
                    "no decision candidate was produced".to_owned(),
                )),
                (DecisionStatus::Unknown { missing }, _) => Some((
                    CounterexampleKind::Unknown,
                    format!(
                        "the decision needs additional input: {}",
                        missing.join(", ")
                    ),
                )),
                (DecisionStatus::Conflict { values, reasons }, _) if values.len() > 1 => Some((
                    CounterexampleKind::Overdetermined,
                    format!(
                        "multiple values remain after explicit overrides: {}{}",
                        values
                            .iter()
                            .map(ToString::to_string)
                            .collect::<Vec<_>>()
                            .join(", "),
                        if reasons.is_empty() {
                            String::new()
                        } else {
                            format!(" ({})", reasons.join("; "))
                        }
                    ),
                )),
                (DecisionStatus::Conflict { reasons, .. }, _) => Some((
                    CounterexampleKind::Conflict,
                    if reasons.is_empty() {
                        "the decision has conflicting support".into()
                    } else {
                        reasons.join("; ")
                    },
                )),
                (DecisionStatus::Resolved { values }, _) if values.is_empty() => Some((
                    CounterexampleKind::Undefined,
                    "no decision candidate was produced".to_owned(),
                )),
                (DecisionStatus::Resolved { values }, _) => Some((
                    CounterexampleKind::Overdetermined,
                    format!("cardinality was violated by {} value(s)", values.len()),
                )),
            };
            failure.map(|(kind, reason)| Counterexample {
                invariant: invariant.name.value.clone(),
                kind,
                input: input.clone(),
                reason,
                evaluation: Some(evaluation),
            })
        }
        InvariantAssertion::Implication {
            condition,
            expectation,
            ..
        } => {
            let condition = evaluate_condition(
                program,
                input,
                invariant
                    .variables
                    .iter()
                    .map(|variable| (variable.name.value.clone(), variable.name.value.clone()))
                    .collect(),
                condition,
            );
            match condition.truth {
                TruthValue::False => return None,
                TruthValue::Unknown => {
                    return Some(Counterexample {
                        invariant: invariant.name.value.clone(),
                        kind: CounterexampleKind::Unknown,
                        input: input.clone(),
                        reason: format!(
                            "property premise is unknown: {}",
                            condition.missing.join(", ")
                        ),
                        evaluation: None,
                    });
                }
                TruthValue::Conflict => {
                    return Some(Counterexample {
                        invariant: invariant.name.value.clone(),
                        kind: CounterexampleKind::Conflict,
                        input: input.clone(),
                        reason: condition.reasons.join("; "),
                        evaluation: None,
                    });
                }
                TruthValue::True => {}
            }
            let query = Query {
                decision: expectation.decision.value.clone(),
                arguments: expectation
                    .arguments
                    .iter()
                    .filter_map(|argument| match &argument.kind {
                        ExprKind::Name(name) => Some(name.clone()),
                        _ => None,
                    })
                    .collect(),
            };
            let evaluation = match evaluate_query(program, input, &query) {
                Ok(evaluation) => evaluation,
                Err(error) => {
                    return Some(Counterexample {
                        invariant: invariant.name.value.clone(),
                        kind: CounterexampleKind::Conflict,
                        input: input.clone(),
                        reason: error.message,
                        evaluation: None,
                    });
                }
            };
            let expected_type = program
                .decision(&expectation.decision.value)
                .map(|decision| &decision.return_type.value);
            let expected = match constant_value(program, &expectation.value, expected_type) {
                Ok(expected) => expected,
                Err(error) => {
                    return Some(Counterexample {
                        invariant: invariant.name.value.clone(),
                        kind: CounterexampleKind::Conflict,
                        input: input.clone(),
                        reason: error,
                        evaluation: Some(evaluation),
                    });
                }
            };
            let failure = match &evaluation.result.status {
                DecisionStatus::Resolved { values } => {
                    let contains = values.contains(&expected);
                    let satisfied = match expectation.operator {
                        crate::ast::CompareOp::Equal => contains,
                        crate::ast::CompareOp::NotEqual => !contains,
                    };
                    (!satisfied).then_some((
                        CounterexampleKind::PropertyViolation,
                        format!(
                            "expected {} to satisfy the declared relation",
                            query.render()
                        ),
                    ))
                }
                DecisionStatus::Undefined => Some((
                    CounterexampleKind::PropertyViolation,
                    format!("{} is undefined", query.render()),
                )),
                DecisionStatus::Unknown { missing } => Some((
                    CounterexampleKind::Unknown,
                    format!(
                        "{} needs additional input: {}",
                        query.render(),
                        missing.join(", ")
                    ),
                )),
                DecisionStatus::Conflict { values, .. } if values.len() > 1 => Some((
                    CounterexampleKind::Overdetermined,
                    format!(
                        "{} has multiple values: {}",
                        query.render(),
                        values
                            .iter()
                            .map(ToString::to_string)
                            .collect::<Vec<_>>()
                            .join(", ")
                    ),
                )),
                DecisionStatus::Conflict { reasons, .. } => Some((
                    CounterexampleKind::Conflict,
                    if reasons.is_empty() {
                        format!("{} has conflicting support", query.render())
                    } else {
                        reasons.join("; ")
                    },
                )),
            };
            failure.map(|(kind, reason)| Counterexample {
                invariant: invariant.name.value.clone(),
                kind,
                input: input.clone(),
                reason,
                evaluation: Some(evaluation),
            })
        }
    }
}

fn invariant_has_existential_witness(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
    input: &Input,
) -> bool {
    check_invariant_witness(program, invariant, input).is_ok()
}

fn check_invariant_witness(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
    input: &Input,
) -> Result<(), String> {
    if let InvariantAssertion::Implication { condition, .. } = &invariant.assertion {
        let premise = evaluate_condition(
            program,
            input,
            invariant
                .variables
                .iter()
                .map(|variable| (variable.name.value.clone(), variable.name.value.clone()))
                .collect(),
            condition,
        );
        match premise.truth {
            TruthValue::True => {}
            TruthValue::False => {
                return Err("the existential property premise is false".into());
            }
            TruthValue::Unknown => {
                return Err(format!(
                    "the existential property premise needs additional input: {}",
                    premise.missing.join(", ")
                ));
            }
            TruthValue::Conflict => {
                return Err(if premise.reasons.is_empty() {
                    "the existential property premise has conflicting support".into()
                } else {
                    premise.reasons.join("; ")
                });
            }
        }
    }

    match find_invariant_violation(program, invariant, input) {
        None => Ok(()),
        Some(non_witness) => Err(non_witness.reason),
    }
}

/// Replay one concrete input against an invariant using the regular Tess
/// evaluator. This is kept crate-private so solver adapters cannot accidentally
/// bypass the evaluator's decision and conflict semantics.
pub(crate) fn replay_invariant_violation(
    program: &CompiledProgram,
    invariant_name: &str,
    input: &Input,
) -> Result<Option<Counterexample>, String> {
    let invariant = program
        .invariant(invariant_name)
        .ok_or_else(|| format!("unknown invariant `{invariant_name}`"))?;
    Ok(find_invariant_violation(program, invariant, input))
}

/// Replay one concrete input as evidence for an existential invariant.
///
/// Unlike ordinary implication, `for some ... if P then Q` requires a case
/// where both the premise and expectation hold. A false or indeterminate
/// premise is therefore not accepted as a vacuous witness.
pub(crate) fn replay_invariant_witness(
    program: &CompiledProgram,
    invariant_name: &str,
    input: &Input,
) -> Result<(), String> {
    let invariant = program
        .invariant(invariant_name)
        .ok_or_else(|| format!("unknown invariant `{invariant_name}`"))?;
    if invariant.quantifier != InvariantQuantifier::Some {
        return Err(format!(
            "invariant `{invariant_name}` does not use the `for some` quantifier"
        ));
    }
    check_invariant_witness(program, invariant, input)
}

#[derive(Clone, Debug)]
enum ThresholdFieldUse {
    Finite,
    Int { transitions: BTreeSet<i128> },
}

#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
struct QuantifiedField {
    binding: String,
    field: String,
}

#[derive(Default)]
struct ThresholdRequirements {
    fields: BTreeMap<QuantifiedField, ThresholdFieldUse>,
}

impl ThresholdRequirements {
    fn mark_finite(&mut self, field: QuantifiedField) {
        self.fields
            .entry(field)
            .or_insert(ThresholdFieldUse::Finite);
    }

    fn mark_int(&mut self, field: QuantifiedField, transitions: impl IntoIterator<Item = i128>) {
        match self
            .fields
            .entry(field)
            .or_insert_with(|| ThresholdFieldUse::Int {
                transitions: BTreeSet::new(),
            }) {
            ThresholdFieldUse::Int {
                transitions: existing,
            } => existing.extend(transitions),
            ThresholdFieldUse::Finite => {
                unreachable!("a compiled field cannot be both Int and finite-valued")
            }
        }
    }
}

struct ThresholdInspector<'a> {
    program: &'a CompiledProgram,
    binding_entities: BTreeMap<String, String>,
    requirements: ThresholdRequirements,
}

impl ThresholdInspector<'_> {
    fn inspect_condition(
        &mut self,
        expression: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Result<(), String> {
        if contains_call(expression) {
            return Err(
                "a relevant condition uses a derive or function call; only direct field predicates are partitionable"
                    .into(),
            );
        }
        if !depends_on_input(expression, receivers) {
            // A ground condition may be true, false, unknown, or conflicting, but its
            // outcome is identical for every input and therefore does not need a cut.
            return Ok(());
        }

        match &expression.kind {
            ExprKind::Field { .. } => {
                let Some((field_key, field_type)) =
                    self.direct_field(expression, receivers)?
                else {
                    return Err("a relevant condition contains an indirect field access".into());
                };
                if field_type != TypeRef::Bool {
                    return Err(format!(
                        "field `{}.{}` is used as a condition but is not Bool",
                        field_key.binding, field_key.field
                    ));
                }
                self.requirements.mark_finite(field_key);
                Ok(())
            }
            ExprKind::Unary {
                operator: crate::ast::UnaryOp::Not,
                operand,
            } => self.inspect_condition(operand, receivers),
            ExprKind::Binary {
                left,
                operator: BinaryOp::And | BinaryOp::Or,
                right,
            } => {
                self.inspect_condition(left, receivers)?;
                self.inspect_condition(right, receivers)
            }
            ExprKind::Binary {
                left,
                operator:
                    operator @ (BinaryOp::Equal
                    | BinaryOp::NotEqual
                    | BinaryOp::Greater
                    | BinaryOp::GreaterEqual
                    | BinaryOp::Less
                    | BinaryOp::LessEqual),
                right,
            } => self.inspect_comparison(left, *operator, right, receivers),
            ExprKind::Binary { .. } | ExprKind::Unary { .. } => Err(
                "a relevant condition applies arithmetic to an input field; only direct Int-field comparisons are partitionable"
                    .into(),
            ),
            ExprKind::Name(_) => Err(
                "a relevant condition depends directly on an entity value instead of one of its fields"
                    .into(),
            ),
            ExprKind::Call { .. } => unreachable!("calls were rejected above"),
            ExprKind::Literal(_) => unreachable!("input-independent literals returned above"),
        }
    }

    fn inspect_comparison(
        &mut self,
        left: &Expr,
        operator: BinaryOp,
        right: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Result<(), String> {
        let left_field = self.direct_field(left, receivers)?;
        let right_field = self.direct_field(right, receivers)?;
        let (field_key, field_type, ground, normalized_operator) = match (left_field, right_field) {
            (Some(_), Some(_)) => {
                return Err(
                    "a relevant condition compares two input fields; cross-field predicates are not partitionable"
                        .into(),
                );
            }
            (Some((name, ty)), None) => (name, ty, right, operator),
            (None, Some((name, ty))) => (name, ty, left, reverse_comparison(operator)),
            (None, None) => {
                if depends_on_input(left, receivers) || depends_on_input(right, receivers) {
                    return Err(
                        "a relevant condition applies arithmetic to an input field; only direct Int-field comparisons are partitionable"
                            .into(),
                    );
                }
                return Ok(());
            }
        };
        if depends_on_input(ground, receivers) {
            return Err(
                "a relevant condition compares an input field with another input-dependent expression"
                    .into(),
            );
        }

        match field_type {
            TypeRef::Int => {
                let constant = ground_numeric_value(self.program, ground)?;
                let transitions = int_comparison_transitions(normalized_operator, constant)?;
                self.requirements.mark_int(field_key, transitions);
                Ok(())
            }
            TypeRef::Bool | TypeRef::Named(_) => {
                if !matches!(normalized_operator, BinaryOp::Equal | BinaryOp::NotEqual) {
                    return Err(format!(
                        "field `{}.{}` uses an unsupported ordered comparison",
                        field_key.binding, field_key.field
                    ));
                }
                constant_value(self.program, ground, Some(&field_type)).map_err(|error| {
                    format!(
                        "comparison with `{}.{}` is not ground: {error}",
                        field_key.binding, field_key.field
                    )
                })?;
                self.requirements.mark_finite(field_key);
                Ok(())
            }
            TypeRef::Decimal | TypeRef::String | TypeRef::Date | TypeRef::Duration => Err(format!(
                "relevant field `{}.{}` has type {}; threshold proofs currently support only Bool, enum, and Int fields",
                field_key.binding,
                field_key.field,
                type_ref_name(&field_type)
            )),
            TypeRef::Unknown => Err(format!(
                "relevant field `{}.{}` has an unresolved type",
                field_key.binding, field_key.field
            )),
        }
    }

    fn direct_field(
        &self,
        expression: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Result<Option<(QuantifiedField, TypeRef)>, String> {
        let ExprKind::Field { receiver, field } = &expression.kind else {
            return Ok(None);
        };
        let ExprKind::Name(receiver_name) = &receiver.kind else {
            return Err("a relevant condition contains an indirect field receiver".into());
        };
        let receiver_name = normalize_name(receiver_name);
        let Some(binding) = receivers.get(&receiver_name) else {
            return Err(format!(
                "field access `{receiver_name}.{}` does not refer to a quantified entity",
                field.value
            ));
        };
        let entity_name = self.binding_entities.get(binding).ok_or_else(|| {
            format!("receiver `{receiver_name}` is not bound to a quantified entity")
        })?;
        let declaration = self
            .program
            .field(entity_name, &field.value)
            .ok_or_else(|| format!("unknown field `{}`", field.value))?;
        Ok(Some((
            QuantifiedField {
                binding: binding.clone(),
                field: normalize_name(&field.value),
            },
            declaration.ty.clone(),
        )))
    }

    fn require_constant(
        &self,
        expression: &Expr,
        expected: &TypeRef,
        receivers: &BTreeMap<String, String>,
        context: &str,
    ) -> Result<(), String> {
        if contains_call(expression) {
            return Err(format!(
                "{context} uses a derive or function call instead of an input-independent constant"
            ));
        }
        if depends_on_input(expression, receivers) {
            return Err(format!("{context} depends on an input value"));
        }
        constant_value(self.program, expression, Some(expected))
            .map(|_| ())
            .map_err(|error| format!("{context} is not a valid constant: {error}"))
    }
}

/// Construct an exact finite quotient of the concrete input domain.
///
/// Eligibility guarantees that every input-dependent atom is either a finite
/// Bool/enum observation or a direct `Int-field op ground-number` comparison.
/// Such an Int atom changes truth value only at the transition cuts recorded
/// below. Relevant effects and expectations are constant, and no relevant rule
/// reads an unused field. Consequently every concrete input maps to exactly one
/// representative whose relevant rule conditions, override activity, candidate
/// values, and invariant premise are identical. Enumerating all representatives is
/// therefore a proof, not boundary sampling.
fn threshold_partition_domains(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
) -> Result<Vec<QuantifiedDomain>, String> {
    let (decision_name, query_arguments) = match &invariant.assertion {
        InvariantAssertion::Cardinality {
            decision,
            arguments,
            ..
        } => (&decision.value, arguments.as_slice()),
        InvariantAssertion::Implication { expectation, .. } => (
            &expectation.decision.value,
            expectation.arguments.as_slice(),
        ),
    };
    let binding_entities = invariant
        .variables
        .iter()
        .map(|variable| {
            (
                normalize_name(&variable.name.value),
                normalize_name(&variable.ty.value),
            )
        })
        .collect::<BTreeMap<_, _>>();
    let query_bindings = query_arguments
        .iter()
        .map(|argument| {
            let ExprKind::Name(name) = &argument.kind else {
                return Err(
                    "the invariant decision must be called directly with quantified entities"
                        .to_owned(),
                );
            };
            let name = normalize_name(name);
            if !binding_entities.contains_key(&name) {
                return Err(format!(
                    "decision argument `{name}` is not a quantified entity"
                ));
            }
            Ok(name)
        })
        .collect::<Result<Vec<_>, String>>()?;
    let decision = program
        .decision(decision_name)
        .ok_or_else(|| format!("unknown decision `{decision_name}`"))?;
    if decision.parameters.len() != query_bindings.len() {
        return Err("the invariant decision argument count is inconsistent".into());
    }
    for (parameter, binding) in decision.parameters.iter().zip(&query_bindings) {
        if binding_entities.get(binding) != Some(&normalize_name(&parameter.ty.value)) {
            return Err(format!(
                "decision argument `{binding}` has an incompatible quantified entity type"
            ));
        }
    }

    let normalized_decision = normalize_name(decision_name);
    let query = Query {
        decision: normalized_decision.clone(),
        arguments: query_bindings,
    };
    let candidate_rule_names = program
        .rules()
        .iter()
        .filter(|(_, rule)| rule_directly_decides(rule, &normalized_decision))
        .map(|(name, _)| name.clone())
        .collect::<BTreeSet<_>>();
    let relevant_rules = program
        .rules()
        .iter()
        .filter(|(name, rule)| {
            candidate_rule_names.contains(*name)
                || rule.effects.iter().any(|effect| {
                    matches!(effect, Effect::Override { rule, .. }
                        if candidate_rule_names.contains(&normalize_name(&rule.value)))
                })
        })
        .map(|(_, rule)| rule)
        .collect::<Vec<_>>();

    let mut inspector = ThresholdInspector {
        program,
        binding_entities: binding_entities.clone(),
        requirements: ThresholdRequirements::default(),
    };
    let invariant_receivers = binding_entities
        .keys()
        .map(|binding| (binding.clone(), binding.clone()))
        .collect::<BTreeMap<_, _>>();
    if let InvariantAssertion::Implication {
        condition,
        expectation,
        ..
    } = &invariant.assertion
    {
        inspector.inspect_condition(condition, &invariant_receivers)?;
        inspector.require_constant(
            &expectation.value,
            &decision.return_type.value,
            &invariant_receivers,
            "the invariant expectation",
        )?;
    }

    for rule in relevant_rules {
        inspect_relevant_rule(&mut inspector, rule, decision, &query, &binding_entities)?;
    }

    build_threshold_domains(program, &invariant.variables, &inspector.requirements)
}

fn inspect_relevant_rule(
    inspector: &mut ThresholdInspector<'_>,
    rule: &RuleDecl,
    decision: &crate::ast::DecisionDecl,
    query: &Query,
    binding_entities: &BTreeMap<String, String>,
) -> Result<(), String> {
    let parameter_names = rule
        .parameters
        .iter()
        .map(|parameter| normalize_name(&parameter.name.value))
        .collect::<BTreeSet<_>>();
    for effect in &rule.effects {
        let Effect::Decide {
            decision: target,
            arguments,
            ..
        } = effect
        else {
            continue;
        };
        if normalize_name(&target.value) != query.decision {
            continue;
        }
        if arguments.len() != query.arguments.len()
            || arguments.iter().any(|argument| {
                !matches!(&argument.kind, ExprKind::Name(name)
                    if parameter_names.contains(&normalize_name(name)))
            })
        {
            return Err(format!(
                "relevant rule `{}` uses a dynamic decision argument",
                rule.name.value
            ));
        }
    }
    let receivers = resolve_rule_bindings(rule, decision, query, binding_entities)
        .map_err(|reason| format!("relevant rule `{}` {reason}", rule.name.value))?;
    inspector.inspect_condition(&rule.condition, &receivers)?;

    for effect in &rule.effects {
        let Effect::Decide {
            decision: target,
            arguments,
            value,
            ..
        } = effect
        else {
            continue;
        };
        if normalize_name(&target.value) != query.decision {
            continue;
        }
        if arguments.len() != decision.parameters.len() {
            return Err(format!(
                "relevant rule `{}` uses a dynamic decision argument",
                rule.name.value
            ));
        }
        inspector.require_constant(
            value,
            &decision.return_type.value,
            &receivers,
            &format!("candidate value in rule `{}`", rule.name.value),
        )?;
    }
    Ok(())
}

fn rule_directly_decides(rule: &RuleDecl, decision: &str) -> bool {
    rule.effects.iter().any(|effect| {
        matches!(effect, Effect::Decide { decision: target, .. }
            if normalize_name(&target.value) == decision)
    })
}

fn contains_call(expression: &Expr) -> bool {
    match &expression.kind {
        ExprKind::Call { .. } => true,
        ExprKind::Field { receiver, .. } => contains_call(receiver),
        ExprKind::Unary { operand, .. } => contains_call(operand),
        ExprKind::Binary { left, right, .. } => contains_call(left) || contains_call(right),
        ExprKind::Literal(_) | ExprKind::Name(_) => false,
    }
}

fn depends_on_input(expression: &Expr, receivers: &BTreeMap<String, String>) -> bool {
    match &expression.kind {
        ExprKind::Field { .. } => true,
        ExprKind::Name(name) => receivers.contains_key(&normalize_name(name)),
        ExprKind::Call { arguments, .. } => arguments
            .iter()
            .any(|argument| depends_on_input(argument, receivers)),
        ExprKind::Unary { operand, .. } => depends_on_input(operand, receivers),
        ExprKind::Binary { left, right, .. } => {
            depends_on_input(left, receivers) || depends_on_input(right, receivers)
        }
        ExprKind::Literal(_) => false,
    }
}

fn ground_numeric_value(program: &CompiledProgram, expression: &Expr) -> Result<Decimal, String> {
    match constant_value(program, expression, Some(&TypeRef::Decimal))? {
        Value::Int(value) => Ok(Decimal::from(value)),
        Value::Decimal(value) => Ok(value),
        value => Err(format!("expected a ground numeric value, found {value}")),
    }
}

const fn reverse_comparison(operator: BinaryOp) -> BinaryOp {
    match operator {
        BinaryOp::Greater => BinaryOp::Less,
        BinaryOp::GreaterEqual => BinaryOp::LessEqual,
        BinaryOp::Less => BinaryOp::Greater,
        BinaryOp::LessEqual => BinaryOp::GreaterEqual,
        BinaryOp::Equal
        | BinaryOp::NotEqual
        | BinaryOp::And
        | BinaryOp::Or
        | BinaryOp::Add
        | BinaryOp::Subtract
        | BinaryOp::Multiply
        | BinaryOp::Divide => operator,
    }
}

fn int_comparison_transitions(operator: BinaryOp, constant: Decimal) -> Result<Vec<i128>, String> {
    let floor = i128::try_from(constant.floor())
        .map_err(|_| format!("numeric threshold `{constant}` is outside the supported range"))?;
    let ceil = i128::try_from(constant.ceil())
        .map_err(|_| format!("numeric threshold `{constant}` is outside the supported range"))?;
    let transitions = match operator {
        BinaryOp::Less | BinaryOp::GreaterEqual => vec![ceil],
        BinaryOp::LessEqual | BinaryOp::Greater => vec![floor + 1],
        BinaryOp::Equal | BinaryOp::NotEqual if constant.fract().is_zero() => {
            vec![floor, floor + 1]
        }
        BinaryOp::Equal | BinaryOp::NotEqual => Vec::new(),
        _ => return Err("expected a comparison operator".into()),
    };
    Ok(transitions)
}

fn build_threshold_domains(
    program: &CompiledProgram,
    variables: &[crate::ast::Parameter],
    requirements: &ThresholdRequirements,
) -> Result<Vec<QuantifiedDomain>, String> {
    variables
        .iter()
        .map(|variable| {
            let binding = normalize_name(&variable.name.value);
            let entity = program
                .entity(&variable.ty.value)
                .ok_or_else(|| format!("unknown quantified entity `{}`", variable.ty.value))?;
            let fields = entity
                .fields
                .iter()
                .map(|field| {
                    let key = QuantifiedField {
                        binding: binding.clone(),
                        field: normalize_name(&field.name.value),
                    };
                    let values = match requirements.fields.get(&key) {
                        Some(ThresholdFieldUse::Finite) => finite_partition_values(program, field)?,
                        Some(ThresholdFieldUse::Int { transitions }) => {
                            int_partition_values(field, transitions)?
                        }
                        None => vec![unused_field_representative(program, field)?],
                    };
                    Ok(FieldDomain {
                        name: field.name.value.clone(),
                        values,
                    })
                })
                .collect::<Result<Vec<_>, String>>()?;
            Ok(QuantifiedDomain {
                binding: variable.name.value.clone(),
                entity: variable.ty.value.clone(),
                fields,
            })
        })
        .collect()
}

fn finite_partition_values(
    program: &CompiledProgram,
    field: &FieldDecl,
) -> Result<Vec<Option<Value>>, String> {
    let values = match &field.ty {
        TypeRef::Bool => vec![Value::Bool(false), Value::Bool(true)],
        TypeRef::Named(name) => program
            .enum_decl(name)
            .map_or_else(Vec::new, |declaration| {
                declaration
                    .variants
                    .iter()
                    .map(|variant| Value::Enum {
                        type_name: name.clone(),
                        variant: variant.value.clone(),
                    })
                    .collect()
            }),
        _ => {
            return Err(format!(
                "field `{}` is not a finite Bool or enum field",
                field.name.value
            ));
        }
    };
    let mut values = values.into_iter().map(Some).collect::<Vec<_>>();
    if field.optional {
        values.insert(0, None);
    }
    if values.is_empty() {
        return Err(format!(
            "field `{}` has no representable values",
            field.name.value
        ));
    }
    Ok(values)
}

fn int_partition_values(
    field: &FieldDecl,
    transitions: &BTreeSet<i128>,
) -> Result<Vec<Option<Value>>, String> {
    let (start, end) = int_field_bounds(field)?;
    let lower = i128::from(start);
    let upper_exclusive = i128::from(end) + 1;
    let mut cuts = BTreeSet::from([lower, upper_exclusive]);
    cuts.extend(
        transitions
            .iter()
            .copied()
            .filter(|cut| lower < *cut && *cut < upper_exclusive),
    );
    let ordered = cuts.into_iter().collect::<Vec<_>>();
    let mut values = ordered
        .windows(2)
        .map(|window| {
            i64::try_from(window[0])
                .map(Value::Int)
                .map(Some)
                .map_err(|_| "integer partition representative is outside i64".to_owned())
        })
        .collect::<Result<Vec<_>, _>>()?;
    if field.optional {
        values.insert(0, None);
    }
    Ok(values)
}

fn int_field_bounds(field: &FieldDecl) -> Result<(i64, i64), String> {
    let Some(range) = &field.range else {
        return Ok((i64::MIN, i64::MAX));
    };
    let (NumericLiteral::Int(start), NumericLiteral::Int(end)) = (&range.start, &range.end) else {
        return Err(format!(
            "Int field `{}` has non-integer range bounds",
            field.name.value
        ));
    };
    Ok((*start, *end))
}

fn unused_field_representative(
    program: &CompiledProgram,
    field: &FieldDecl,
) -> Result<Option<Value>, String> {
    if field.optional {
        return Ok(None);
    }
    let value = match &field.ty {
        TypeRef::Bool => Value::Bool(false),
        TypeRef::Int => Value::Int(
            int_field_bounds(field)?
                .0
                .max(0)
                .min(int_field_bounds(field)?.1),
        ),
        TypeRef::Decimal => {
            let value = field
                .range
                .as_ref()
                .and_then(|range| numeric_decimal(&range.start))
                .unwrap_or(Decimal::ZERO);
            Value::decimal(value)
        }
        TypeRef::String => Value::String(String::new()),
        TypeRef::Date => {
            Value::Date(NaiveDate::from_ymd_opt(1970, 1, 1).expect("valid epoch date"))
        }
        TypeRef::Duration => Value::Duration(0),
        TypeRef::Named(name) => {
            let variant = program
                .enum_decl(name)
                .and_then(|declaration| declaration.variants.first())
                .ok_or_else(|| format!("field `{}` has no enum values", field.name.value))?;
            Value::Enum {
                type_name: name.clone(),
                variant: variant.value.clone(),
            }
        }
        TypeRef::Unknown => {
            return Err(format!(
                "field `{}` has an unresolved type",
                field.name.value
            ));
        }
    };
    Ok(Some(value))
}

const fn type_ref_name(value: &TypeRef) -> &'static str {
    match value {
        TypeRef::Bool => "Bool",
        TypeRef::Int => "Int",
        TypeRef::Decimal => "Decimal",
        TypeRef::String => "String",
        TypeRef::Date => "Date",
        TypeRef::Duration => "Duration",
        TypeRef::Named(_) => "enum",
        TypeRef::Unknown => "unknown",
    }
}

fn input_at(mut ordinal: usize, domains: &[QuantifiedDomain]) -> Input {
    let field_count = domains.iter().map(|domain| domain.fields.len()).sum();
    let mut indices = vec![0; field_count];
    let fields = domains
        .iter()
        .flat_map(|domain| &domain.fields)
        .collect::<Vec<_>>();
    for (index, field) in fields.iter().enumerate().rev() {
        indices[index] = ordinal % field.values.len();
        ordinal /= field.values.len();
    }
    let mut input = Input::new();
    let mut index = 0;
    for domain in domains {
        let mut values = BTreeMap::new();
        for field in &domain.fields {
            if let Some(value) = &field.values[indices[index]] {
                values.insert(field.name.clone(), value.clone());
            }
            index += 1;
        }
        input.insert(&domain.binding, &domain.entity, values);
    }
    input
}

fn quantified_domain_size(
    program: &CompiledProgram,
    quantified: &[(&crate::ast::Parameter, &crate::ast::EntityDecl)],
) -> Option<usize> {
    quantified.iter().try_fold(1usize, |total, (_, entity)| {
        total.checked_mul(finite_domain_size(program, entity)?)
    })
}

fn quantified_fields_materializable(
    program: &CompiledProgram,
    quantified: &[(&crate::ast::Parameter, &crate::ast::EntityDecl)],
) -> bool {
    quantified
        .iter()
        .all(|(_, entity)| concrete_fields_materializable(program, entity))
}

fn finite_domain_size(program: &CompiledProgram, entity: &crate::ast::EntityDecl) -> Option<usize> {
    entity.fields.iter().try_fold(1usize, |total, field| {
        let base = if let Some(values) = declared_domain_values(program, field) {
            values.len()
        } else {
            match &field.ty {
                TypeRef::Bool => 2,
                TypeRef::Int => {
                    let range = field.range.as_ref()?;
                    let (NumericLiteral::Int(start), NumericLiteral::Int(end)) =
                        (&range.start, &range.end)
                    else {
                        return None;
                    };
                    if start > end {
                        return None;
                    }
                    let width = i128::from(*end) - i128::from(*start) + 1;
                    usize::try_from(width).ok()?
                }
                TypeRef::Named(name) => program.enum_decl(name)?.variants.len(),
                TypeRef::Decimal
                | TypeRef::String
                | TypeRef::Date
                | TypeRef::Duration
                | TypeRef::Unknown => return None,
            }
        };
        total.checked_mul(base.checked_add(usize::from(field.optional))?)
    })
}

fn concrete_fields_materializable(
    program: &CompiledProgram,
    entity: &crate::ast::EntityDecl,
) -> bool {
    entity.fields.iter().all(|field| {
        let base = if let Some(values) = declared_domain_values(program, field) {
            values.len()
        } else {
            match &field.ty {
                TypeRef::Bool => 2,
                TypeRef::Int => {
                    let Some(range) = &field.range else {
                        return false;
                    };
                    let (NumericLiteral::Int(start), NumericLiteral::Int(end)) =
                        (&range.start, &range.end)
                    else {
                        return false;
                    };
                    let width = i128::from(*end) - i128::from(*start) + 1;
                    let Ok(width) = usize::try_from(width) else {
                        return false;
                    };
                    width
                }
                TypeRef::Named(name) => {
                    let Some(declaration) = program.enum_decl(name) else {
                        return false;
                    };
                    declaration.variants.len()
                }
                TypeRef::Decimal
                | TypeRef::String
                | TypeRef::Date
                | TypeRef::Duration
                | TypeRef::Unknown => return false,
            }
        };
        base.checked_add(usize::from(field.optional))
            .is_some_and(|size| size <= MAX_MATERIALIZED_VALUES_PER_FIELD)
    })
}

fn field_values(
    program: &CompiledProgram,
    field: &crate::ast::FieldDecl,
    constants: &BTreeSet<Decimal>,
    exhaustive: bool,
) -> Vec<Option<Value>> {
    let mut values = if let Some(values) = declared_domain_values(program, field) {
        values
    } else {
        match &field.ty {
            TypeRef::Bool => vec![Value::Bool(false), Value::Bool(true)],
            TypeRef::Int => integer_values(field, constants, exhaustive),
            TypeRef::Decimal => decimal_values(field, constants),
            TypeRef::String => vec![Value::String(String::new())],
            TypeRef::Date => vec![Value::Date(
                NaiveDate::from_ymd_opt(1970, 1, 1).expect("valid epoch date"),
            )],
            TypeRef::Duration => vec![Value::Duration(0)],
            TypeRef::Named(name) => program.enum_decl(name).map_or_else(Vec::new, |value| {
                value
                    .variants
                    .iter()
                    .map(|variant| Value::Enum {
                        type_name: name.clone(),
                        variant: variant.value.clone(),
                    })
                    .collect()
            }),
            TypeRef::Unknown => Vec::new(),
        }
    };
    let mut seen = BTreeSet::new();
    values.retain(|value| seen.insert(value.clone()));
    let mut optional = values.into_iter().map(Some).collect::<Vec<_>>();
    if field.optional {
        optional.insert(0, None);
    }
    if optional.is_empty() {
        optional.push(None);
    }
    optional
}

fn declared_domain_values(
    program: &CompiledProgram,
    field: &crate::ast::FieldDecl,
) -> Option<Vec<Value>> {
    let domain = field.domain.as_ref()?;
    domain
        .values
        .iter()
        .map(|expression| constant_value(program, expression, Some(&field.ty)).ok())
        .collect()
}

fn integer_values(
    field: &crate::ast::FieldDecl,
    constants: &BTreeSet<Decimal>,
    exhaustive: bool,
) -> Vec<Value> {
    let range = field.range.as_ref().and_then(|range| {
        let (NumericLiteral::Int(start), NumericLiteral::Int(end)) = (&range.start, &range.end)
        else {
            return None;
        };
        Some((*start, *end))
    });
    if exhaustive {
        if let Some((start, end)) = range {
            return (start..=end).map(Value::Int).collect();
        }
    }
    if range.is_none() {
        let mut candidates = BTreeSet::from([-1, 0, 1]);
        for constant in constants {
            if constant.fract().is_zero() {
                if let Ok(value) = i64::try_from(constant.trunc()) {
                    candidates.extend([value.saturating_sub(1), value, value.saturating_add(1)]);
                }
            }
        }
        return candidates.into_iter().map(Value::Int).collect();
    }
    let (start, end) = range.expect("range was checked above");
    let mut candidates = BTreeSet::from([start, end]);
    if start < end {
        candidates.insert(start.saturating_add(1));
        candidates.insert(end.saturating_sub(1));
    }
    for base in [-1, 0, 1] {
        if (start..=end).contains(&base) {
            candidates.insert(base);
        }
    }
    for constant in constants {
        if constant.fract().is_zero() {
            if let Ok(value) = i64::try_from(constant.trunc()) {
                for candidate in [value.saturating_sub(1), value, value.saturating_add(1)] {
                    if (start..=end).contains(&candidate) {
                        candidates.insert(candidate);
                    }
                }
            }
        }
    }
    candidates.into_iter().map(Value::Int).collect()
}

fn decimal_values(field: &crate::ast::FieldDecl, constants: &BTreeSet<Decimal>) -> Vec<Value> {
    let range = field
        .range
        .as_ref()
        .and_then(|range| Some((numeric_decimal(&range.start)?, numeric_decimal(&range.end)?)));
    let epsilon = Decimal::new(1, 3);
    if range.is_none() {
        let mut candidates = BTreeSet::from([Decimal::NEGATIVE_ONE, Decimal::ZERO, Decimal::ONE]);
        for constant in constants {
            candidates.insert(*constant);
            if let Some(value) = constant.checked_sub(epsilon) {
                candidates.insert(value);
            }
            if let Some(value) = constant.checked_add(epsilon) {
                candidates.insert(value);
            }
        }
        return candidates
            .into_iter()
            .map(|value| Value::decimal(value.normalize()))
            .collect();
    }
    let (start, end) = range.expect("range was checked above");
    let mut candidates = BTreeSet::from([start, end]);
    for value in [Decimal::NEGATIVE_ONE, Decimal::ZERO, Decimal::ONE] {
        if value >= start && value <= end {
            candidates.insert(value);
        }
    }
    for constant in constants {
        let neighbors = [
            constant.checked_sub(epsilon),
            Some(*constant),
            constant.checked_add(epsilon),
        ];
        for value in neighbors.into_iter().flatten() {
            if value >= start && value <= end {
                candidates.insert(value.normalize());
            }
        }
    }
    candidates.into_iter().map(Value::decimal).collect()
}

fn numeric_decimal(literal: &NumericLiteral) -> Option<Decimal> {
    match literal {
        NumericLiteral::Int(value) => Some(Decimal::from(*value)),
        NumericLiteral::Decimal(value) => parse_decimal(value).ok(),
    }
}

fn numeric_constants(program: &CompiledProgram) -> BTreeSet<Decimal> {
    let mut constants = BTreeSet::new();
    for declaration in &program.ast().declarations {
        match declaration {
            Declaration::Derive(value) => collect_expr_numbers(&value.expression, &mut constants),
            Declaration::Rule(value) => {
                collect_expr_numbers(&value.condition, &mut constants);
                for effect in &value.effects {
                    if let crate::ast::Effect::Decide {
                        arguments, value, ..
                    } = effect
                    {
                        for argument in arguments {
                            collect_expr_numbers(argument, &mut constants);
                        }
                        collect_expr_numbers(value, &mut constants);
                    }
                }
            }
            // Concrete regression cases must not enlarge the analyzer's abstract
            // domain. Only rule and property boundaries influence exploration.
            Declaration::Case(_)
            | Declaration::Enum(_)
            | Declaration::Entity(_)
            | Declaration::State(_)
            | Declaration::Decision(_)
            | Declaration::Action(_)
            | Declaration::Source(_) => {}
            Declaration::Transition(value) => {
                collect_expr_numbers(&value.condition, &mut constants);
                for update in &value.updates {
                    collect_expr_numbers(&update.value, &mut constants);
                }
            }
            Declaration::Trace(value) => {
                collect_expr_numbers(&value.initial, &mut constants);
                for condition in &value.always {
                    collect_expr_numbers(condition, &mut constants);
                }
                if let Some(condition) = &value.terminal {
                    collect_expr_numbers(condition, &mut constants);
                }
            }
            Declaration::Invariant(value) => match &value.assertion {
                InvariantAssertion::Cardinality { arguments, .. } => {
                    for argument in arguments {
                        collect_expr_numbers(argument, &mut constants);
                    }
                }
                InvariantAssertion::Implication {
                    condition,
                    expectation,
                    ..
                } => {
                    collect_expr_numbers(condition, &mut constants);
                    collect_expr_numbers(&expectation.value, &mut constants);
                }
            },
        }
    }
    constants
}

fn collect_expr_numbers(expression: &Expr, constants: &mut BTreeSet<Decimal>) {
    match &expression.kind {
        ExprKind::Literal(Literal::Number(value)) => {
            if let Some(value) = numeric_decimal(value) {
                constants.insert(value);
            }
        }
        ExprKind::Field { receiver, .. } => collect_expr_numbers(receiver, constants),
        ExprKind::Call { arguments, .. } => {
            for argument in arguments {
                collect_expr_numbers(argument, constants);
            }
        }
        ExprKind::Unary { operand, .. } => collect_expr_numbers(operand, constants),
        ExprKind::Binary { left, right, .. } => {
            collect_expr_numbers(left, constants);
            collect_expr_numbers(right, constants);
        }
        ExprKind::Literal(_) | ExprKind::Name(_) => {}
    }
}

fn static_findings(program: &CompiledProgram) -> Vec<StaticFinding> {
    let mut produced: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();
    let decision_enums = program
        .decisions()
        .values()
        .filter_map(|decision| match &decision.return_type.value {
            TypeRef::Named(name) if program.enum_decl(name).is_some() => Some(name.clone()),
            _ => None,
        })
        .collect::<BTreeSet<_>>();
    let mut dynamic = BTreeSet::new();
    for declaration in &program.ast().declarations {
        let Declaration::Rule(rule) = declaration else {
            continue;
        };
        for effect in &rule.effects {
            let crate::ast::Effect::Decide {
                decision, value, ..
            } = effect
            else {
                continue;
            };
            let Some(decision_decl) = program.decision(&decision.value) else {
                continue;
            };
            let TypeRef::Named(enum_name) = &decision_decl.return_type.value else {
                continue;
            };
            if let ExprKind::Name(variant) = &value.kind {
                produced
                    .entry(enum_name.clone())
                    .or_default()
                    .insert(variant.clone());
            } else {
                dynamic.insert(enum_name.clone());
            }
        }
    }
    let mut findings = Vec::new();
    for name in decision_enums {
        if dynamic.contains(&name) {
            continue;
        }
        let enum_decl = &program.enums()[&name];
        let values = produced.get(&name);
        for variant in &enum_decl.variants {
            if values.is_none_or(|values| !values.contains(&variant.value)) {
                findings.push(StaticFinding {
                    code: "W2001".into(),
                    message: format!(
                        "enum value `{}.{}` is never produced by a decision rule",
                        name, variant.value
                    ),
                });
            }
        }
    }
    findings.sort_by(|left, right| (&left.code, &left.message).cmp(&(&right.code, &right.message)));
    findings
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::ast::{EntityDecl, FieldDecl, RangeConstraint};
    use crate::source::{SourceFile, Span, Spanned};

    fn compile_text(source: &str) -> CompiledProgram {
        let output = crate::compile_source(SourceFile::new("analysis.tes", source));
        assert!(
            !output.has_errors(),
            "{}",
            output
                .diagnostics
                .iter()
                .map(|diagnostic| diagnostic.message.as_str())
                .collect::<Vec<_>>()
                .join("; ")
        );
        output.program.expect("compiled program")
    }

    fn analyze_text(source: &str, max_evaluations: usize) -> InvariantAnalysis {
        let report = analyze_with_solver(
            &compile_text(source),
            Some("total"),
            &AnalysisOptions {
                max_evaluations,
                max_counterexamples: 3,
            },
            SolverMode::Off,
        );
        report
            .invariants
            .into_iter()
            .next()
            .expect("analyzed invariant")
    }

    fn analyze_text_with_solver(source: &str) -> InvariantAnalysis {
        analyze_text_with_solver_limit(source, 100_000)
    }

    fn analyze_text_auto(source: &str) -> InvariantAnalysis {
        let report = analyze(
            &compile_text(source),
            Some("total"),
            &AnalysisOptions::default(),
        );
        report
            .invariants
            .into_iter()
            .next()
            .expect("analyzed invariant")
    }

    fn analyze_text_with_solver_limit(source: &str, max_evaluations: usize) -> InvariantAnalysis {
        let report = analyze_with_solver(
            &compile_text(source),
            Some("total"),
            &AnalysisOptions {
                max_evaluations,
                ..AnalysisOptions::default()
            },
            SolverMode::Z3,
        );
        report
            .invariants
            .into_iter()
            .next()
            .expect("analyzed invariant")
    }

    /// Deliberately bypasses the production planner so compact exact strategies
    /// can be checked against a literal finite-domain oracle.
    fn raw_counterexamples(source: &str) -> Vec<Counterexample> {
        let program = compile_text(source);
        let invariant = program
            .ast()
            .declarations
            .iter()
            .find_map(|declaration| match declaration {
                Declaration::Invariant(invariant) if invariant.name.value == "total" => {
                    Some(invariant)
                }
                _ => None,
            })
            .expect("total invariant");
        let quantified = invariant
            .variables
            .iter()
            .map(|variable| {
                let entity = program
                    .entity(&variable.ty.value)
                    .expect("quantified entity");
                (variable, entity)
            })
            .collect::<Vec<_>>();
        let domains = concrete_domains(&program, &quantified, &BTreeSet::new(), true);
        let combinations = planned_evaluation_count(&domains).expect("finite test domain");

        (0..combinations)
            .filter_map(|ordinal| {
                find_invariant_violation(&program, invariant, &input_at(ordinal, &domains))
            })
            .collect()
    }

    fn input_int(counterexample: &Counterexample, field: &str) -> Option<i64> {
        counterexample
            .input
            .bindings
            .values()
            .next()?
            .fields
            .get(field)?
            .as_int()
    }

    fn binding_int(counterexample: &Counterexample, binding: &str, field: &str) -> Option<i64> {
        counterexample
            .input
            .bindings
            .get(binding)?
            .fields
            .get(field)?
            .as_int()
    }

    fn binding_decimal(
        counterexample: &Counterexample,
        binding: &str,
        field: &str,
    ) -> Option<Decimal> {
        counterexample
            .input
            .bindings
            .get(binding)?
            .fields
            .get(field)?
            .as_decimal()
    }

    fn int_field(optional: bool) -> FieldDecl {
        FieldDecl {
            name: Spanned::new("x".into(), Span::default()),
            ty: TypeRef::Int,
            range: Some(RangeConstraint {
                start: NumericLiteral::Int(0),
                end: NumericLiteral::Int(3),
                span: Span::default(),
            }),
            domain: None,
            optional,
            span: Span::default(),
        }
    }

    #[test]
    fn boundary_values_include_endpoints() {
        let values = integer_values(&int_field(false), &BTreeSet::new(), false);
        assert!(values.contains(&Value::Int(0)));
        assert!(values.contains(&Value::Int(3)));
    }

    #[test]
    fn exhaustive_integer_values_cover_range() {
        let values = integer_values(&int_field(false), &BTreeSet::new(), true);
        assert_eq!(
            values,
            [Value::Int(0), Value::Int(1), Value::Int(2), Value::Int(3)]
        );
    }

    #[test]
    fn threshold_neighbors_are_generated() {
        let values = integer_values(
            &int_field(false),
            &BTreeSet::from([Decimal::from(2)]),
            false,
        );
        assert!(values.contains(&Value::Int(1)));
        assert!(values.contains(&Value::Int(2)));
        assert!(values.contains(&Value::Int(3)));
    }

    #[test]
    fn range_less_numbers_include_rule_boundaries() {
        let mut field = int_field(false);
        field.range = None;
        let values = integer_values(&field, &BTreeSet::from([Decimal::from(100)]), false);
        assert!(values.contains(&Value::Int(99)));
        assert!(values.contains(&Value::Int(100)));
        assert!(values.contains(&Value::Int(101)));
    }

    #[test]
    fn input_enumeration_is_stable() {
        let domains = vec![QuantifiedDomain {
            binding: "s".into(),
            entity: "Student".into(),
            fields: vec![FieldDomain {
                name: "x".into(),
                values: vec![Some(Value::Int(0)), Some(Value::Int(1))],
            }],
        }];
        let first = input_at(0, &domains);
        let second = input_at(1, &domains);
        assert_eq!(first.bindings["s"].fields["x"], Value::Int(0));
        assert_eq!(second.bindings["s"].fields["x"], Value::Int(1));
    }

    #[test]
    fn cartesian_enumeration_is_lexicographic_by_field_order() {
        let domains = vec![QuantifiedDomain {
            binding: "s".into(),
            entity: "E".into(),
            fields: vec![
                FieldDomain {
                    name: "a".into(),
                    values: vec![Some(Value::Int(0)), Some(Value::Int(1))],
                },
                FieldDomain {
                    name: "b".into(),
                    values: vec![Some(Value::Int(0)), Some(Value::Int(1))],
                },
            ],
        }];
        let second = input_at(1, &domains);
        let third = input_at(2, &domains);
        assert_eq!(second.bindings["s"].fields["a"], Value::Int(0));
        assert_eq!(second.bindings["s"].fields["b"], Value::Int(1));
        assert_eq!(third.bindings["s"].fields["a"], Value::Int(1));
        assert_eq!(third.bindings["s"].fields["b"], Value::Int(0));
    }

    #[test]
    fn planned_evaluation_overflow_is_not_saturated_into_an_exact_count() {
        let domains = vec![QuantifiedDomain {
            binding: "s".into(),
            entity: "E".into(),
            fields: (0..usize::BITS)
                .map(|index| FieldDomain {
                    name: format!("f{index}"),
                    values: vec![Some(Value::Bool(false)), Some(Value::Bool(true))],
                })
                .collect(),
        }];
        assert_eq!(planned_evaluation_count(&domains), None);
    }

    #[test]
    fn empty_or_inconclusive_report_is_not_successful() {
        assert!(!AnalysisReport::default().success());
        let report = AnalysisReport {
            invariants: vec![InvariantAnalysis {
                invariant: "c".into(),
                quantifier: InvariantQuantifier::All,
                verdict: AnalysisVerdict::Inconclusive,
                evaluated: 1,
                planned_evaluations: 2,
                completeness: Completeness::Truncated,
                solver: None,
                witness: None,
                counterexamples: Vec::new(),
                notes: Vec::new(),
            }],
            traces: Vec::new(),
            findings: Vec::new(),
        };
        assert!(!report.success());
    }

    #[test]
    fn human_report_summarizes_strategies_without_machine_labels_or_routine_notes() {
        let invariant =
            |name: &str, verdict, evaluated, planned_evaluations, completeness, solver, notes| {
                InvariantAnalysis {
                    invariant: name.into(),
                    quantifier: InvariantQuantifier::All,
                    verdict,
                    evaluated,
                    planned_evaluations,
                    completeness,
                    solver,
                    witness: None,
                    counterexamples: Vec::new(),
                    notes,
                }
            };
        let report = AnalysisReport {
            invariants: vec![
                invariant(
                    "exhaustive",
                    AnalysisVerdict::Passed,
                    40_804,
                    40_804,
                    Completeness::Exhaustive,
                    None,
                    Vec::new(),
                ),
                invariant(
                    "threshold",
                    AnalysisVerdict::Passed,
                    4,
                    4,
                    Completeness::ThresholdPartitioned,
                    None,
                    vec!["used an exact threshold partition: every representative stands for a region with identical relevant rule and invariant outcomes".into()],
                ),
                invariant(
                    "solver",
                    AnalysisVerdict::Passed,
                    0,
                    0,
                    Completeness::SolverExact,
                    Some(SolverMetadata {
                        backend: "z3".into(),
                        version: "Z3 4.15.2.0".into(),
                        logic: "QF_LIA".into(),
                    }),
                    vec!["the negated property is unsatisfiable in QF_LIA via Z3".into()],
                ),
                invariant(
                    "sampled",
                    AnalysisVerdict::Inconclusive,
                    12,
                    12,
                    Completeness::BoundarySampled,
                    None,
                    vec![
                        "integer/decimal domains were reduced to endpoints and comparison boundaries; absence of a counterexample is not a proof".into(),
                        "exact analysis is unavailable for this expression".into(),
                    ],
                ),
                invariant(
                    "truncated",
                    AnalysisVerdict::Inconclusive,
                    100,
                    2_000,
                    Completeness::Truncated,
                    None,
                    vec!["stopped at the configured evaluation limit of 100".into()],
                ),
            ],
            traces: Vec::new(),
            findings: Vec::new(),
        };

        let text = report.render_text();
        assert!(
            text.contains(
                "✓ exhaustive\n  proved for all inputs · all 40,804 combinations checked"
            )
        );
        assert!(text.contains("✓ threshold\n  proved for all inputs · 4 exact regions checked"));
        assert!(text.contains("✓ solver\n  proved for all inputs · exact solver (Z3)"));
        assert!(
            text.contains(
                "? sampled\n  inconclusive · 12 boundary samples checked · not exhaustive"
            )
        );
        assert!(text.contains("  reason · exact analysis is unavailable for this expression"));
        assert!(
            text.contains("? truncated\n  inconclusive · 100 of 2,000 evaluations · truncated")
        );
        for hidden in [
            "solver_exact",
            "threshold_partitioned",
            "negated property",
            "used an exact threshold partition",
            "stopped at the configured evaluation limit",
        ] {
            assert!(!text.contains(hidden), "unexpected `{hidden}` in:\n{text}");
        }
    }

    #[test]
    fn existential_cardinality_passes_when_one_exact_assignment_is_a_witness() {
        let invariant = analyze_text(
            r"module M
enum Result { Yes }
entity E { x: Int range 0..4 }
decision d(E e) -> Result
rule yes(E e):
  when e.x = 2
  then d(e) = Yes
invariant total:
  for some e: E
  exactly one d(e)
",
            100,
        );

        assert_eq!(invariant.quantifier, InvariantQuantifier::Some);
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::Truncated);
        assert!(invariant.evaluated < invariant.planned_evaluations);
        assert!(invariant.counterexamples.is_empty());
        let witness = invariant.witness.as_ref().expect("existential witness");
        assert_eq!(witness.bindings["e"].fields["x"], Value::Int(2));
        let json = serde_json::to_value(&invariant).unwrap();
        assert_eq!(json["quantifier"], "some");
        assert_eq!(json["witness"]["bindings"]["e"]["entity"], "E");
        let report = AnalysisReport {
            invariants: vec![invariant],
            traces: Vec::new(),
            findings: Vec::new(),
        };
        assert!(
            report
                .render_text()
                .contains("✓ total\n  satisfying input found · after 2 evaluations")
        );
        assert!(report.render_text().contains("  witness\n    e: E {"));
    }

    #[test]
    fn existential_exact_exhaustion_without_a_witness_is_conclusively_failed() {
        let invariant = analyze_text(
            r"module M
enum Result { Yes }
entity E { x: Int range 0..4 }
decision d(E e) -> Result
rule impossible(E e):
  when e.x < 0
  then d(e) = Yes
invariant total:
  for some e: E
  exactly one d(e)
",
            100,
        );

        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert!(matches!(
            invariant.completeness,
            Completeness::Exhaustive | Completeness::ThresholdPartitioned
        ));
        assert!(invariant.counterexamples.is_empty());
        assert!(
            invariant
                .notes
                .iter()
                .any(|note| note.contains("none satisfied the assertion"))
        );
        let report = AnalysisReport {
            invariants: vec![invariant],
            traces: Vec::new(),
            findings: Vec::new(),
        };
        assert!(
            report
                .render_text()
                .contains("✗ total\n  no satisfying input exists")
        );
    }

    #[test]
    fn existential_limited_search_without_a_witness_remains_inconclusive() {
        let invariant = analyze_text(
            r"module M
enum Result { Yes }
entity E { x: Int range 0..4 }
decision d(E e) -> Result
rule impossible(E e):
  when e.x < 0
  then d(e) = Yes
invariant total:
  for some e: E
  exactly one d(e)
",
            0,
        );

        assert_eq!(invariant.verdict, AnalysisVerdict::Inconclusive);
        assert_eq!(invariant.completeness, Completeness::Truncated);
        assert_eq!(invariant.evaluated, 0);
        assert!(invariant.planned_evaluations > 0);
        assert!(invariant.counterexamples.is_empty());
    }

    #[test]
    fn existential_search_crosses_multiple_bindings() {
        let invariant = analyze_text(
            r"module M
enum Result { Yes }
entity Left { enabled: Bool }
entity Right { enabled: Bool }
decision d(Left left, Right right) -> Result
rule yes(Left left, Right right):
  when left.enabled and right.enabled
  then d(left, right) = Yes
invariant total:
  for some left: Left, right: Right
  exactly one d(left, right)
",
            100,
        );

        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 4);
        assert_eq!(invariant.evaluated, 4);
    }

    #[test]
    fn existential_implication_requires_a_true_premise_and_satisfied_expectation() {
        let source = r"module M
enum Result { Yes }
entity E { x: Int range 0..1 }
decision d(E e) -> Result
rule yes(E e):
  when e.x = 1
  then d(e) = Yes
invariant total:
  for some e: E
  if e.x = 1
  then d(e) = Yes
";
        let invariant = analyze_text(source, 100);
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);

        let program = compile_text(source);
        let false_premise = Input {
            bindings: BTreeMap::from([(
                "e".into(),
                crate::engine::EntityInput {
                    entity: "E".into(),
                    fields: BTreeMap::from([("x".into(), Value::Int(0))]),
                },
            )]),
        };
        assert_eq!(
            replay_invariant_witness(&program, "total", &false_premise).unwrap_err(),
            "the existential property premise is false"
        );
    }

    #[test]
    fn existential_threshold_partition_proves_a_witness_in_a_huge_domain() {
        let invariant = analyze_text(
            r"module M
enum Result { Exact }
entity E { x: Int range 0..1_000_000_000 }
decision d(E e) -> Result
rule exact(E e):
  when e.x = 50
  then d(e) = Exact
invariant total:
  for some e: E
  exactly one d(e)
",
            100,
        );

        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::Truncated);
        assert_eq!(invariant.planned_evaluations, 3);
        assert_eq!(invariant.evaluated, 2);
        assert_eq!(
            invariant.witness.as_ref().unwrap().bindings["e"].fields["x"],
            Value::Int(50)
        );
    }

    #[test]
    fn existential_boundary_sample_witness_is_conclusive() {
        let invariant = analyze_text(
            r"module M
enum Result { Exact }
entity E { x: Int range 0..1_000_000_000 }
decision d(E e) -> Result
rule exact(E e):
  when e.x + 1 = 50
  then d(e) = Exact
invariant total:
  for some e: E
  exactly one d(e)
",
            100,
        );

        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert!(matches!(
            invariant.completeness,
            Completeness::BoundarySampled | Completeness::Truncated
        ));
        assert!(invariant.evaluated > 0);
        assert!(invariant.witness.is_some());
        assert!(invariant.counterexamples.is_empty());
    }

    #[test]
    fn existential_solver_results_are_replayed_as_witness_or_exact_refutation() {
        let witness = analyze_text_with_solver(
            r"module M
enum Result { Yes }
entity E { x: Int range 0..1_000_000 }
decision d(E e) -> Result
rule yes(E e):
  when e.x = 37
  then d(e) = Yes
invariant total:
  for some e: E
  exactly one d(e)
",
        );
        assert_eq!(witness.verdict, AnalysisVerdict::Passed);
        assert_eq!(witness.completeness, Completeness::SolverExact);
        assert_eq!(witness.evaluated, 1);
        assert_eq!(
            witness.witness.as_ref().unwrap().bindings["e"].fields["x"],
            Value::Int(37)
        );

        let refuted = analyze_text_with_solver(
            r"module M
enum Result { Yes }
entity E { x: Int range 0..1_000_000 }
decision d(E e) -> Result
rule impossible(E e):
  when e.x < 0
  then d(e) = Yes
invariant total:
  for some e: E
  exactly one d(e)
",
        );
        assert_eq!(refuted.verdict, AnalysisVerdict::Failed);
        assert_eq!(refuted.completeness, Completeness::SolverExact);
        assert!(refuted.witness.is_none());
        assert!(refuted.counterexamples.is_empty());
    }

    #[test]
    fn huge_int_range_is_proved_by_three_exact_regions() {
        let invariant = analyze_text(
            r"module M
enum Result { Low, Exact, High }
entity E { x: Int range 0..1_000_000_000 }
decision d(E s) -> Result
rule low(E s):
  when s.x < 50
  then d(s) = Low
rule exact(E s):
  when s.x = 50
  then d(s) = Exact
rule high(E s):
  when s.x > 50
  then d(s) = High
invariant total:
  for all s: E
  exactly one d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.evaluated, 3);
        assert_eq!(invariant.planned_evaluations, 3);
        let report = AnalysisReport {
            invariants: vec![invariant],
            traces: Vec::new(),
            findings: Vec::new(),
        };
        assert!(
            report
                .render_text()
                .contains("proved for all inputs · 3 exact regions checked")
        );
    }

    #[test]
    fn exact_partition_finds_gap_at_threshold() {
        let invariant = analyze_text(
            r"module M
enum Result { Low, High }
entity E { x: Int range 0..1_000_000_000 }
decision d(E s) -> Result
rule low(E s):
  when s.x < 50
  then d(s) = Low
rule high(E s):
  when s.x > 50
  then d(s) = High
invariant total:
  for all s: E
  exactly one d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Undefined
        );
        assert_eq!(input_int(&invariant.counterexamples[0], "x"), Some(50));
    }

    #[test]
    fn exact_partition_finds_distinct_value_overlap_at_threshold() {
        let invariant = analyze_text(
            r"module M
enum Result { Low, High }
entity E { x: Int range 0..1_000_000_000 }
decision d(E s) -> Result
rule low(E s):
  when s.x <= 50
  then d(s) = Low
rule high(E s):
  when s.x >= 50
  then d(s) = High
invariant total:
  for all s: E
  exactly one d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Overdetermined
        );
        assert_eq!(input_int(&invariant.counterexamples[0], "x"), Some(50));
    }

    #[test]
    fn bool_and_enum_fields_are_crossed_exactly_while_unused_fields_are_collapsed() {
        let invariant = analyze_text(
            r"module M
enum Mode { A, B }
enum Result { Yes, No }
entity E { flag: Bool, mode: Mode, unused: String }
decision d(E s) -> Result
rule yes_a(E s):
  when s.flag and s.mode = A
  then d(s) = Yes
rule yes_b(E s):
  when s.flag and s.mode = B
  then d(s) = Yes
rule no_a(E s):
  when not s.flag and s.mode = A
  then d(s) = No
rule no_b(E s):
  when not s.flag and s.mode = B
  then d(s) = No
invariant total:
  for all s: E
  exactly one d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.evaluated, 4);
    }

    #[test]
    fn unsupported_rules_for_another_decision_do_not_disable_exact_partitioning() {
        let invariant = analyze_text(
            r#"module M
enum Result { Low, High }
entity E { x: Int range 0..1_000_000_000, text: String }
decision d(E s) -> Result
decision unrelated(E s) -> Bool
rule low(E s):
  when s.x < 50
  then d(s) = Low
rule high(E s):
  when s.x >= 50
  then d(s) = High
rule string_rule(E s):
  when s.text = "unsupported but irrelevant"
  then unrelated(s) = true
invariant total:
  for all s: E
  exactly one d(s)
"#,
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.evaluated, 2);
    }

    #[test]
    fn direct_override_conditions_participate_in_the_exact_partition() {
        let invariant = analyze_text(
            r"module M
enum Result { Base, Special }
entity E { x: Int range 0..1_000_000_000 }
decision d(E s) -> Result
rule base(E s):
  when true
  then d(s) = Base
rule special(E s):
  when s.x >= 50
  then d(s) = Special
rule prefer_special(E s):
  when s.x >= 50
  then override base
invariant total:
  for all s: E
  exactly one d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.evaluated, 2);
    }

    #[test]
    fn optional_bool_override_keeps_missing_as_an_exact_unknown_region() {
        let invariant = analyze_text(
            r"module M
enum Result { Base, Special }
entity E { special: Bool?, unused: String }
decision d(E s) -> Result
rule base(E s):
  when true
  then d(s) = Base
rule special(E s):
  when s.special
  then d(s) = Special
rule prefer_special(E s):
  when s.special
  then override base
invariant total:
  for all s: E
  exactly one d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 3);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Unknown
        );
        assert!(
            !invariant.counterexamples[0].input.bindings["s"]
                .fields
                .contains_key("special")
        );
    }

    #[test]
    fn repeated_query_binding_supports_rule_parameter_permutation() {
        let invariant = analyze_text(
            r"module M
enum Result { Yes }
entity E { value: Int range 0..1_000_000_000 }
decision d(E first, E second) -> Result
rule yes(E left, E right):
  when left.value < 50 and right.value < 50
  then d(right, left) = Yes
invariant total:
  for all s: E
  exactly one d(s, s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 2);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Undefined
        );
        assert_eq!(input_int(&invariant.counterexamples[0], "value"), Some(50));
    }

    #[test]
    fn shared_binding_resolver_matches_runtime_for_permuted_arguments() {
        let program = compile_text(
            r"module M
enum Result { Yes }
entity E { x: Int range 0..2 }
decision d(E first, E second) -> Result
rule swapped(E left, E right):
  when left.x = 2 and right.x = 1
  then d(right, left) = Yes
",
        );
        let query = Query::parse("d(a, b)").unwrap();
        let bindings = BTreeMap::from([("a".into(), "E".into()), ("b".into(), "E".into())]);
        let mapping = resolve_rule_bindings(
            program.rule("swapped").unwrap(),
            program.decision("d").unwrap(),
            &query,
            &bindings,
        )
        .unwrap();
        assert_eq!(mapping["left"], "b");
        assert_eq!(mapping["right"], "a");

        let mut input = Input::new();
        input.insert("a", "E", BTreeMap::from([("x".into(), Value::Int(1))]));
        input.insert("b", "E", BTreeMap::from([("x".into(), Value::Int(2))]));
        let evaluation = evaluate_query(&program, &input, &query).unwrap();
        assert!(matches!(
            evaluation.result.status,
            DecisionStatus::Resolved { ref values } if values.len() == 1
        ));
    }

    #[test]
    fn two_independent_bindings_of_the_same_entity_are_partitioned_separately() {
        let invariant = analyze_text(
            r"module M
enum Result { LL, LH, HL, HH }
entity E { x: Int range 0..1_000_000_000 }
decision d(E first, E second) -> Result
rule ll(E left, E right):
  when left.x < 50 and right.x < 100
  then d(left, right) = LL
rule lh(E left, E right):
  when left.x < 50 and right.x >= 100
  then d(left, right) = LH
rule hl(E left, E right):
  when left.x >= 50 and right.x < 100
  then d(left, right) = HL
rule hh(E left, E right):
  when left.x >= 50 and right.x >= 100
  then d(left, right) = HH
invariant total:
  for all a: E, b: E
  exactly one d(a, b)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 4);
    }

    #[test]
    fn multi_binding_gap_witness_preserves_each_independent_input() {
        let invariant = analyze_text(
            r"module M
enum Result { LL, LH, HL }
entity E { x: Int range 0..1_000_000_000 }
decision d(E first, E second) -> Result
rule ll(E left, E right):
  when left.x < 50 and right.x < 100
  then d(left, right) = LL
rule lh(E left, E right):
  when left.x < 50 and right.x >= 100
  then d(left, right) = LH
rule hl(E left, E right):
  when left.x >= 50 and right.x < 100
  then d(left, right) = HL
invariant total:
  for all a: E, b: E
  exactly one d(a, b)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Undefined
        );
        assert_eq!(
            binding_int(&invariant.counterexamples[0], "a", "x"),
            Some(50)
        );
        assert_eq!(
            binding_int(&invariant.counterexamples[0], "b", "x"),
            Some(100)
        );
    }

    #[test]
    fn independent_query_argument_permutation_assigns_cuts_to_the_actual_bindings() {
        let invariant = analyze_text(
            r"module M
enum Result { Yes }
entity E { x: Int range 0..1_000_000_000 }
decision d(E first, E second) -> Result
rule yes(E left, E right):
  when left.x < 100 and right.x < 50
  then d(right, left) = Yes
invariant total:
  for all a: E, b: E
  exactly one d(a, b)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 4);
        assert_eq!(
            binding_int(&invariant.counterexamples[0], "a", "x"),
            Some(0)
        );
        assert_eq!(
            binding_int(&invariant.counterexamples[0], "b", "x"),
            Some(100)
        );
    }

    #[test]
    fn different_quantified_entity_types_get_independent_exact_domains() {
        let invariant = analyze_text(
            r"module M
enum Result { Free, Paid }
entity Order { amount: Int range 0..1_000_000_000 }
entity Member { premium: Bool }
decision d(Order order, Member member) -> Result
rule premium(Order order, Member member):
  when member.premium
  then d(order, member) = Free
rule large(Order order, Member member):
  when not member.premium and order.amount >= 50
  then d(order, member) = Free
rule small(Order order, Member member):
  when not member.premium and order.amount < 50
  then d(order, member) = Paid
invariant total:
  for all o: Order, m: Member
  exactly one d(o, m)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 4);
    }

    #[test]
    fn premise_only_quantified_binding_contributes_its_exact_bool_and_int_regions() {
        let invariant = analyze_text(
            r"module M
enum Result { Free }
entity Order { amount: Int range 0..1_000_000_000 }
entity Customer { vip: Bool, score: Int range 0..1_000_000_000 }
decision d(Order order) -> Result
rule free(Order order):
  when true
  then d(order) = Free
invariant total:
  for all o: Order, c: Customer
  if c.vip and c.score >= 100
  then d(o) = Free
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 4);
    }

    #[test]
    fn multi_binding_cross_field_predicate_falls_back_instead_of_claiming_proof() {
        let invariant = analyze_text(
            r"module M
enum Result { Less, NotLess }
entity E { x: Int range 0..1_000_000_000 }
decision d(E first, E second) -> Result
rule less(E left, E right):
  when left.x < right.x
  then d(left, right) = Less
rule not_less(E left, E right):
  when left.x >= right.x
  then d(left, right) = NotLess
invariant total:
  for all a: E, b: E
  exactly one d(a, b)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Inconclusive);
        assert_eq!(invariant.completeness, Completeness::BoundarySampled);
        assert!(
            invariant
                .notes
                .iter()
                .any(|note| note.contains("compares two input fields"))
        );
    }

    #[test]
    fn solver_finds_a_relational_gap_and_replays_the_model() {
        let invariant = analyze_text_with_solver(
            r"module M
enum Result { Free, Paid }
entity Order { amount: Int range 0..100_000 }
entity Coupon { discount: Int range 0..100_000 }
decision d(Order order, Coupon coupon) -> Result
rule free(Order order, Coupon coupon):
  when order.amount - coupon.discount > 50_000
  then d(order, coupon) = Free
rule paid(Order order, Coupon coupon):
  when order.amount - coupon.discount < 50_000
  then d(order, coupon) = Paid
invariant total:
  for all order: Order, coupon: Coupon
  exactly one d(order, coupon)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Undefined
        );
        let amount = binding_int(&invariant.counterexamples[0], "order", "amount").unwrap();
        let discount = binding_int(&invariant.counterexamples[0], "coupon", "discount").unwrap();
        assert_eq!(amount - discount, 50_000);
        assert_eq!(invariant.solver.as_ref().unwrap().logic, "QF_LIA");
    }

    #[test]
    fn solver_proves_relational_totality_without_enumerating_the_raw_product() {
        let invariant = analyze_text_with_solver(
            r"module M
enum Result { Free, Paid }
entity Order { amount: Int range 0..100_000 }
entity Coupon { discount: Int range 0..100_000 }
decision d(Order order, Coupon coupon) -> Result
rule free(Order order, Coupon coupon):
  when order.amount - coupon.discount >= 50_000
  then d(order, coupon) = Free
rule paid(Order order, Coupon coupon):
  when order.amount - coupon.discount < 50_000
  then d(order, coupon) = Paid
invariant total:
  for all order: Order, coupon: Coupon
  exactly one d(order, coupon)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 0);
        assert_eq!(invariant.planned_evaluations, 0);
    }

    #[test]
    fn solver_distinguishes_different_value_overlap_from_same_value_merge() {
        let conflicting = analyze_text_with_solver(
            r"module M
enum Result { Free, Paid }
entity A { x: Int range 0..100_000 }
entity B { y: Int range 0..100_000 }
decision d(A a, B b) -> Result
rule free(A a, B b):
  when a.x - b.y >= 50_000
  then d(a, b) = Free
rule paid(A a, B b):
  when a.x - b.y <= 50_000
  then d(a, b) = Paid
invariant total:
  for all a: A, b: B
  exactly one d(a, b)
",
        );
        assert_eq!(conflicting.verdict, AnalysisVerdict::Failed);
        assert_eq!(conflicting.completeness, Completeness::SolverExact);
        assert_eq!(
            conflicting.counterexamples[0].kind,
            CounterexampleKind::Overdetermined
        );

        let merged = analyze_text_with_solver(
            r"module M
enum Result { Free }
entity A { x: Int range 0..100_000 }
entity B { y: Int range 0..100_000 }
decision d(A a, B b) -> Result
rule upper(A a, B b):
  when a.x - b.y >= 50_000
  then d(a, b) = Free
rule lower(A a, B b):
  when a.x - b.y <= 50_000
  then d(a, b) = Free
invariant total:
  for all a: A, b: B
  exactly one d(a, b)
",
        );
        assert_eq!(merged.verdict, AnalysisVerdict::Passed);
        assert_eq!(merged.completeness, Completeness::SolverExact);
    }

    #[test]
    fn solver_handles_implication_bool_enum_and_constant_scaled_linear_terms() {
        let invariant = analyze_text_with_solver(
            r"module M
enum Result { Free, Paid }
enum Tier { Standard, Preferred }
entity Order { amount: Int range 0..100_000 }
entity Customer { credit: Int range 0..100_000, premium: Bool, tier: Tier }
decision d(Order order, Customer customer) -> Result
rule preferred(Order order, Customer customer):
  when customer.premium and customer.tier = Preferred
  then d(order, customer) = Free
rule amount(Order order, Customer customer):
  when not customer.premium and 2 * order.amount - customer.credit >= 50_000
  then d(order, customer) = Free
rule paid(Order order, Customer customer):
  when not customer.premium and 2 * order.amount - customer.credit < 50_000
  then d(order, customer) = Paid
rule standard_premium(Order order, Customer customer):
  when customer.premium and customer.tier = Standard
  then d(order, customer) = Paid
invariant total:
  for all order: Order, customer: Customer
  if customer.premium and customer.tier = Preferred
  then d(order, customer) = Free
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
    }

    #[test]
    fn solver_proves_direct_decimal_field_relations_without_sampling() {
        let invariant = analyze_text_auto(
            r"module M
enum Result { WithinLimit, Review }
entity Expense {
  claimed: Decimal range 0.00..1_000_000.00,
  approved: Decimal range 0.00..1_000_000.00,
}
derive claimed_amount(Expense e) -> Decimal: e.claimed
decision audit(Expense e) -> Result
rule within(Expense e):
  when claimed_amount(e) <= e.approved
  then audit(e) = WithinLimit
rule review(Expense e):
  when claimed_amount(e) > e.approved
  then audit(e) = Review
invariant total:
  for all e: Expense
  exactly one audit(e)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 0);
        assert_eq!(invariant.planned_evaluations, 0);
        assert_eq!(invariant.solver.as_ref().unwrap().logic, "QF_LIA");
    }

    #[test]
    fn solver_replays_a_decimal_gap_at_equal_field_values() {
        let invariant = analyze_text_auto(
            r"module M
enum Result { Lower, Higher }
entity Quote {
  offered: Decimal range 0.00..1_000_000.00,
  limit: Decimal range 0.00..1_000_000.00,
}
decision classify(Quote q) -> Result
rule lower(Quote q):
  when q.offered < q.limit
  then classify(q) = Lower
rule higher(Quote q):
  when q.offered > q.limit
  then classify(q) = Higher
invariant total:
  for all q: Quote
  exactly one classify(q)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 1);
        let offered = binding_decimal(&invariant.counterexamples[0], "q", "offered").unwrap();
        let limit = binding_decimal(&invariant.counterexamples[0], "q", "limit").unwrap();
        assert_eq!(offered, limit);
    }

    #[test]
    fn solver_handles_mixed_int_decimal_comparisons_and_scale_28_neighbors() {
        let mixed = analyze_text_auto(
            r"module M
enum Result { Below, AtOrAbove }
entity E { amount: Decimal range 0.0..100.0, limit: Int range 0..100 }
decision d(E e) -> Result
rule below(E e):
  when e.amount < e.limit
  then d(e) = Below
rule at_or_above(E e):
  when e.amount >= e.limit
  then d(e) = AtOrAbove
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(mixed.verdict, AnalysisVerdict::Passed);
        assert_eq!(mixed.completeness, Completeness::SolverExact);

        let adjacent = analyze_text_auto(
            r"module M
enum Result { Zero, Quantum }
entity E { amount: Decimal range 0.0..0.0000000000000000000000000001 }
decision d(E e) -> Result
rule at_zero(E e):
  when e.amount = 0
  then d(e) = Zero
rule at_quantum(E e):
  when e.amount = 0.0000000000000000000000000001
  then d(e) = Quantum
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(adjacent.verdict, AnalysisVerdict::Passed);
        assert_eq!(adjacent.completeness, Completeness::SolverExact);
    }

    #[test]
    fn solver_materializes_a_96_bit_decimal_mantissa() {
        let invariant = analyze_text_auto(
            r"module M
enum Result { Below }
entity E {
  amount: Decimal range 7922816251426433759354395033.4..7922816251426433759354395033.5,
}
decision d(E e) -> Result
rule below(E e):
  when e.amount < 7922816251426433759354395033.5
  then d(e) = Below
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(
            binding_decimal(&invariant.counterexamples[0], "e", "amount").unwrap(),
            parse_decimal("7922816251426433759354395033.5").unwrap()
        );
    }

    #[test]
    fn solver_inlines_overflow_safe_entity_derives() {
        let invariant = analyze_text_with_solver(
            r"module M
enum Result { Free, Paid }
entity Order { amount: Int range 0..100_000 }
entity Coupon { discount: Int range 0..100_000 }
derive net(Order order, Coupon coupon) -> Int: order.amount - coupon.discount
decision d(Order order, Coupon coupon) -> Result
rule free(Order order, Coupon coupon):
  when net(order, coupon) >= 50_000
  then d(order, coupon) = Free
rule paid(Order order, Coupon coupon):
  when net(order, coupon) < 50_000
  then d(order, coupon) = Paid
invariant total:
  for all order: Order, coupon: Coupon
  exactly one d(order, coupon)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
    }

    #[test]
    fn solver_proves_exact_input_dependent_decimal_arithmetic() {
        let invariant = analyze_text_with_solver(
            r"module M
enum Result { Any }
entity E {
  left: Decimal range 0.0..1.0,
  right: Decimal range 0.0..1.0,
  unit: Decimal range 1.0..1.0,
}
derive scaled(Decimal value, Decimal factor) -> Decimal: value * factor
derive combined(E e) -> Decimal: scaled(e.left + e.right, e.unit)
decision d(E e) -> Result
rule any(E e):
  when combined(e) >= 0
  then d(e) = Any
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 0);
        assert_eq!(invariant.solver.as_ref().unwrap().logic, "QF_NIA");
    }

    #[test]
    fn solver_replays_inexact_decimal_add_multiply_and_divide() {
        for expression in [
            "e.maximum_tenth + 0.1",
            "e.quantum * 0.1",
            "e.unit / 3",
            "e.unit / e.nothing",
        ] {
            let source = format!(
                r"module M
enum Result {{ Any }}
entity E {{
  maximum_tenth: Decimal range 7922816251426433759354395033.5..7922816251426433759354395033.5,
  quantum: Decimal range 0.0000000000000000000000000001..0.0000000000000000000000000001,
  unit: Decimal range 1.0..1.0,
  nothing: Decimal range 0.0..0.0,
}}
decision d(E e) -> Result
rule any(E e):
  when {expression} >= 0
  then d(e) = Any
invariant total:
  for all e: E
  exactly one d(e)
"
            );
            let invariant = analyze_text_with_solver(&source);
            assert_eq!(
                invariant.verdict,
                AnalysisVerdict::Failed,
                "{expression}: {:?}",
                invariant.notes
            );
            assert_eq!(invariant.completeness, Completeness::SolverExact);
            assert_eq!(
                invariant.counterexamples[0].kind,
                CounterexampleKind::Conflict
            );
        }
    }

    #[test]
    fn solver_matches_boolean_conflict_absorption_and_premise_conflict() {
        let short_circuit = analyze_text_with_solver(
            r"module M
enum Result { Any }
entity E { x: Decimal range 1.0..1.0 }
decision d(E e) -> Result
rule skipped_left_false(E e):
  when false and e.x / 0 > 0
  then d(e) = Any
rule skipped_right_false(E e):
  when e.x / 0 > 0 and false
  then d(e) = Any
rule applied_left_true(E e):
  when true or e.x / 0 > 0
  then d(e) = Any
rule applied_right_true(E e):
  when e.x / 0 > 0 or true
  then d(e) = Any
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(short_circuit.verdict, AnalysisVerdict::Passed);
        assert_eq!(short_circuit.completeness, Completeness::SolverExact);

        let premise = analyze_text_with_solver(
            r"module M
enum Result { Any }
entity E { x: Decimal range 1.0..1.0 }
decision d(E e) -> Result
rule any(E e):
  when true
  then d(e) = Any
invariant total:
  for all e: E
  if e.x / 0 > 0
  then d(e) = Any
",
        );
        assert_eq!(premise.verdict, AnalysisVerdict::Failed);
        assert_eq!(premise.completeness, Completeness::SolverExact);
        assert_eq!(
            premise.counterexamples[0].kind,
            CounterexampleKind::Conflict
        );
    }

    #[test]
    fn solver_handles_dynamic_decimal_candidates_and_same_value_merge() {
        let merged = analyze_text_with_solver(
            r"module M
entity E { amount: Decimal range 0.0..1.0 }
decision d(E e) -> Decimal
rule first(E e):
  when e.amount >= 0
  then d(e) = e.amount + 0
rule second(E e):
  when e.amount <= 1
  then d(e) = e.amount
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(merged.verdict, AnalysisVerdict::Passed);
        assert_eq!(merged.completeness, Completeness::SolverExact);

        let conflicting = analyze_text_with_solver(
            r"module M
entity E { amount: Decimal range 0.0..1.0 }
decision d(E e) -> Decimal
rule first(E e):
  when e.amount >= 0
  then d(e) = e.amount
rule second(E e):
  when e.amount <= 1
  then d(e) = e.amount + 1
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(conflicting.verdict, AnalysisVerdict::Failed);
        assert_eq!(conflicting.completeness, Completeness::SolverExact);
        assert_eq!(
            conflicting.counterexamples[0].kind,
            CounterexampleKind::Overdetermined
        );

        let expected = analyze_text_with_solver(
            r"module M
entity E { amount: Decimal range 0.0..1.0 }
decision d(E e) -> Decimal
rule copy(E e):
  when true
  then d(e) = e.amount + 0
invariant total:
  for all e: E
  if e.amount = 0
  then d(e) = 0
",
        );
        assert_eq!(expected.verdict, AnalysisVerdict::Passed);
        assert_eq!(expected.completeness, Completeness::SolverExact);
    }

    #[test]
    fn solver_handles_dynamic_bool_candidates_and_same_value_merge() {
        let merged = analyze_text_with_solver(
            r"module M
entity E { value: Bool, guard: Bool }
decision d(E e) -> Bool
rule first(E e):
  when e.guard or not e.guard
  then d(e) = e.value
rule second(E e):
  when not e.guard or e.guard
  then d(e) = not not e.value
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(merged.verdict, AnalysisVerdict::Passed);
        assert_eq!(merged.completeness, Completeness::SolverExact);

        let conflicting = analyze_text_with_solver(
            r"module M
entity E { value: Bool, guard: Bool }
decision d(E e) -> Bool
rule first(E e):
  when e.guard or not e.guard
  then d(e) = e.value
rule second(E e):
  when not e.guard or e.guard
  then d(e) = not e.value
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(conflicting.verdict, AnalysisVerdict::Failed);
        assert_eq!(conflicting.completeness, Completeness::SolverExact);
        assert_eq!(
            conflicting.counterexamples[0].kind,
            CounterexampleKind::Overdetermined
        );
    }

    #[test]
    fn solver_handles_dynamic_int_candidates_and_same_value_merge() {
        let merged = analyze_text_with_solver(
            r"module M
entity E { x: Int range 0..10 }
decision d(E e) -> Int
rule first(E e):
  when e.x >= 0
  then d(e) = e.x + 0
rule second(E e):
  when e.x <= 10
  then d(e) = e.x
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(merged.verdict, AnalysisVerdict::Passed);
        assert_eq!(merged.completeness, Completeness::SolverExact);

        let conflicting = analyze_text_with_solver(
            r"module M
entity E { x: Int range 0..10 }
decision d(E e) -> Int
rule first(E e):
  when e.x >= 0
  then d(e) = e.x
rule second(E e):
  when e.x <= 10
  then d(e) = e.x + 1
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(conflicting.verdict, AnalysisVerdict::Failed);
        assert_eq!(conflicting.completeness, Completeness::SolverExact);
        assert_eq!(
            conflicting.counterexamples[0].kind,
            CounterexampleKind::Overdetermined
        );
    }

    #[test]
    fn solver_tracks_dynamic_int_candidate_overflow_only_while_active() {
        let overflowing = analyze_text_with_solver_limit(
            r"module M
entity E { x: Int range 9_223_372_036_854_775_806..9_223_372_036_854_775_807 }
decision d(E e) -> Int
rule increment(E e):
  when true
  then d(e) = e.x + 1
invariant total:
  for all e: E
  exactly one d(e)
",
            1,
        );
        assert_eq!(overflowing.verdict, AnalysisVerdict::Failed);
        assert_eq!(overflowing.completeness, Completeness::SolverExact);
        assert_eq!(
            overflowing.counterexamples[0].kind,
            CounterexampleKind::Conflict
        );
        let x = binding_int(&overflowing.counterexamples[0], "e", "x").unwrap();
        assert!(x.checked_add(1).is_none());

        let inactive_at_maximum = analyze_text_with_solver(
            r"module M
entity E { x: Int range 9_223_372_036_854_775_806..9_223_372_036_854_775_807 }
decision d(E e) -> Int
rule increment(E e):
  when e.x < 9_223_372_036_854_775_807
  then d(e) = e.x + 1
rule maximum(E e):
  when e.x = 9_223_372_036_854_775_807
  then d(e) = e.x
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(inactive_at_maximum.verdict, AnalysisVerdict::Passed);
        assert_eq!(inactive_at_maximum.completeness, Completeness::SolverExact);
    }

    #[test]
    fn solver_exact_many_cardinality_accepts_values_but_rejects_runtime_conflict() {
        let valid = analyze_text_with_solver(
            r"module M
entity E { x: Int range 0..10 }
decision d(E e) -> Int many
rule first(E e):
  when e.x >= 0
  then d(e) = e.x
rule second(E e):
  when e.x <= 10
  then d(e) = e.x + 1
invariant total:
  for all e: E
  many d(e)
",
        );
        assert_eq!(valid.verdict, AnalysisVerdict::Passed);
        assert_eq!(valid.completeness, Completeness::SolverExact);

        let conflicted = analyze_text_with_solver_limit(
            r"module M
entity E { x: Int range 9_223_372_036_854_775_807..9_223_372_036_854_775_807 }
decision d(E e) -> Int many
rule overflow(E e):
  when true
  then d(e) = e.x + 1
invariant total:
  for all e: E
  many d(e)
",
            1,
        );
        assert_eq!(conflicted.verdict, AnalysisVerdict::Failed);
        assert_eq!(conflicted.completeness, Completeness::SolverExact);
        assert_eq!(
            conflicted.counterexamples[0].kind,
            CounterexampleKind::Conflict
        );
    }

    #[test]
    fn solver_materializes_forced_bool_and_enum_sat_witnesses() {
        let invariant = analyze_text_with_solver(
            r"module M
enum Mode { A, B }
enum Result { Covered }
entity E { enabled: Bool, mode: Mode }
decision d(E e) -> Result
rule mode_a(E e):
  when e.mode = A
  then d(e) = Covered
rule disabled_b(E e):
  when not e.enabled and e.mode = B
  then d(e) = Covered
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Undefined
        );
        let fields = &invariant.counterexamples[0].input.bindings["e"].fields;
        assert_eq!(fields["enabled"], Value::Bool(true));
        assert_eq!(
            fields["mode"],
            Value::Enum {
                type_name: "Mode".into(),
                variant: "B".into(),
            }
        );
    }

    #[test]
    fn solver_proves_nested_int_min_max_totality_and_finds_its_boundary_gap() {
        let total = analyze_text_with_solver(
            r"module M
enum Result { Free, Paid }
entity Order { amount: Int range 0..100_000 }
entity Coupon { discount: Int range 0..100_000 }
derive payable(Order order, Coupon coupon) -> Int: max(0, order.amount - coupon.discount)
derive capped(Order order, Coupon coupon) -> Int: min(50_000, payable(order, coupon))
decision d(Order order, Coupon coupon) -> Result
rule free(Order order, Coupon coupon):
  when capped(order, coupon) >= 50_000
  then d(order, coupon) = Free
rule paid(Order order, Coupon coupon):
  when capped(order, coupon) < 50_000
  then d(order, coupon) = Paid
invariant total:
  for all order: Order, coupon: Coupon
  exactly one d(order, coupon)
",
        );
        assert_eq!(total.verdict, AnalysisVerdict::Passed);
        assert_eq!(total.completeness, Completeness::SolverExact);

        let gap = analyze_text_with_solver(
            r"module M
enum Result { Free, Paid }
entity Order { amount: Int range 0..100_000 }
entity Coupon { discount: Int range 0..100_000 }
derive payable(Order order, Coupon coupon) -> Int: max(0, order.amount - coupon.discount)
derive capped(Order order, Coupon coupon) -> Int: min(50_000, payable(order, coupon))
decision d(Order order, Coupon coupon) -> Result
rule free(Order order, Coupon coupon):
  when capped(order, coupon) > 50_000
  then d(order, coupon) = Free
rule paid(Order order, Coupon coupon):
  when capped(order, coupon) < 50_000
  then d(order, coupon) = Paid
invariant total:
  for all order: Order, coupon: Coupon
  exactly one d(order, coupon)
",
        );
        assert_eq!(gap.verdict, AnalysisVerdict::Failed);
        assert_eq!(gap.completeness, Completeness::SolverExact);
        let amount = binding_int(&gap.counterexamples[0], "order", "amount").unwrap();
        let discount = binding_int(&gap.counterexamples[0], "coupon", "discount").unwrap();
        assert_eq!((amount - discount).clamp(0, 50_000), 50_000);
    }

    #[test]
    fn solver_proves_int_abs_totality_and_finds_its_boundary_gap() {
        let total = analyze_text_with_solver(
            r"module M
enum Result { Near, Far }
entity Point { x: Int range 0..100_000 }
derive distance(Point left, Point right) -> Int: abs(left.x - right.x)
decision d(Point left, Point right) -> Result
rule far(Point left, Point right):
  when distance(left, right) >= 50_000
  then d(left, right) = Far
rule near(Point left, Point right):
  when distance(left, right) < 50_000
  then d(left, right) = Near
invariant total:
  for all left: Point, right: Point
  exactly one d(left, right)
",
        );
        assert_eq!(total.verdict, AnalysisVerdict::Passed);
        assert_eq!(total.completeness, Completeness::SolverExact);

        let gap = analyze_text_with_solver(
            r"module M
enum Result { Near, Far }
entity Point { x: Int range 0..100_000 }
derive distance(Point left, Point right) -> Int: abs(left.x - right.x)
decision d(Point left, Point right) -> Result
rule far(Point left, Point right):
  when distance(left, right) > 50_000
  then d(left, right) = Far
rule near(Point left, Point right):
  when distance(left, right) < 50_000
  then d(left, right) = Near
invariant total:
  for all left: Point, right: Point
  exactly one d(left, right)
",
        );
        assert_eq!(gap.verdict, AnalysisVerdict::Failed);
        assert_eq!(gap.completeness, Completeness::SolverExact);
        let left = binding_int(&gap.counterexamples[0], "left", "x").unwrap();
        let right = binding_int(&gap.counterexamples[0], "right", "x").unwrap();
        assert_eq!(left.abs_diff(right), 50_000);
    }

    #[test]
    fn solver_replays_overflowing_min_max_arguments_even_when_they_are_not_selected() {
        for builtin in ["max", "min"] {
            for expression in [
                format!("{builtin}(e.x + 1, 0)"),
                format!("{builtin}(0, e.x + 1)"),
            ] {
                let source = format!(
                    r"module M
enum Result {{ Any }}
entity E {{ x: Int range 0..9_223_372_036_854_775_807 }}
derive selected(E e) -> Int: {expression}
decision d(E e) -> Result
rule any(E e):
  when selected(e) >= 0
  then d(e) = Any
invariant total:
  for all e: E
  exactly one d(e)
"
                );
                let invariant = analyze_text_with_solver_limit(&source, 1);
                assert_eq!(invariant.completeness, Completeness::SolverExact);
                assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
                assert_eq!(
                    binding_int(&invariant.counterexamples[0], "e", "x"),
                    Some(i64::MAX),
                    "{expression}"
                );
            }
        }
    }

    #[test]
    fn solver_replays_abs_overflow_at_i64_min() {
        let invariant = analyze_text_with_solver_limit(
            r"module M
enum Result { Any }
entity E { x: Int range -9_223_372_036_854_775_808..9_223_372_036_854_775_807 }
derive magnitude(E e) -> Int: abs(e.x)
decision d(E e) -> Result
rule any(E e):
  when magnitude(e) >= 0
  then d(e) = Any
invariant total:
  for all e: E
  exactly one d(e)
",
            1,
        );
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(
            binding_int(&invariant.counterexamples[0], "e", "x"),
            Some(i64::MIN)
        );
    }

    #[test]
    fn solver_models_direct_override_activity_exactly() {
        let invariant = analyze_text_with_solver(
            r"module M
enum Result { Free, Paid }
entity A { x: Int range 0..100_000 }
entity B { y: Int range 0..100_000 }
decision d(A a, B b) -> Result
rule base(A a, B b):
  when true
  then d(a, b) = Paid
rule special(A a, B b):
  when a.x >= b.y
  then d(a, b) = Free
rule prefer_special(A a, B b):
  when a.x >= b.y
  then override base
invariant total:
  for all a: A, b: B
  exactly one d(a, b)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
    }

    #[test]
    fn solver_and_exhaustive_modes_agree_on_a_small_relational_gap() {
        let source = r"module M
enum Result { Low, High }
entity E { x: Int range 0..2 }
decision d(E a, E b) -> Result
rule low(E a, E b):
  when a.x + b.x < 0
  then d(a, b) = Low
rule high(E a, E b):
  when a.x + b.x > 0
  then d(a, b) = High
invariant total:
  for all a: E, b: E
  exactly one d(a, b)
";
        let exhaustive = analyze_text(source, 100);
        let automatic = analyze_text_auto(source);
        let solved = analyze_text_with_solver_limit(source, 1);
        assert_eq!(exhaustive.verdict, AnalysisVerdict::Failed);
        assert_eq!(exhaustive.completeness, Completeness::Exhaustive);
        assert_eq!(automatic.verdict, exhaustive.verdict);
        assert_eq!(automatic.completeness, Completeness::SolverExact);
        assert_eq!(automatic.evaluated, 1);
        assert_eq!(automatic.solver.as_ref().unwrap().logic, "QF_LIA");
        assert_eq!(solved.verdict, exhaustive.verdict);
        assert_eq!(solved.completeness, Completeness::SolverExact);
        let sum = binding_int(&solved.counterexamples[0], "a", "x").unwrap()
            + binding_int(&solved.counterexamples[0], "b", "x").unwrap();
        assert_eq!(sum, 0);
    }

    #[test]
    fn embedded_solver_counterexample_is_deterministic_across_repeated_runs() {
        let source = r"module M
enum Result { Low, High }
entity E { x: Int range 0..10 }
decision d(E left, E right) -> Result
rule lower(E left, E right):
  when left.x < right.x
  then d(left, right) = Low
rule higher(E left, E right):
  when left.x > right.x
  then d(left, right) = High
invariant total:
  for all left: E, right: E
  exactly one d(left, right)
";
        let first = analyze_text_with_solver(source);
        assert_eq!(first.verdict, AnalysisVerdict::Failed);
        assert_eq!(first.completeness, Completeness::SolverExact);
        let expected = serde_json::to_value(&first).unwrap();
        for _ in 0..5 {
            assert_eq!(
                serde_json::to_value(analyze_text_with_solver(source)).unwrap(),
                expected
            );
        }
    }

    #[test]
    fn embedded_solver_counterexample_is_stable_under_rule_declaration_order() {
        let first_source = r"module M
enum Result { Low, High }
entity E { x: Int range 0..10 }
decision d(E left, E right) -> Result
rule lower(E left, E right):
  when left.x < right.x
  then d(left, right) = Low
rule higher(E left, E right):
  when left.x > right.x
  then d(left, right) = High
invariant total:
  for all left: E, right: E
  exactly one d(left, right)
";
        let second_source = first_source.replace(
            "rule lower(E left, E right):\n  when left.x < right.x\n  then d(left, right) = Low\nrule higher(E left, E right):\n  when left.x > right.x\n  then d(left, right) = High",
            "rule higher(E left, E right):\n  when left.x > right.x\n  then d(left, right) = High\nrule lower(E left, E right):\n  when left.x < right.x\n  then d(left, right) = Low",
        );
        let first = analyze_text_with_solver(first_source);
        let second = analyze_text_with_solver(&second_source);
        assert_eq!(first.verdict, second.verdict);
        assert_eq!(first.completeness, second.completeness);
        assert_eq!(first.solver, second.solver);
        assert_eq!(
            first.counterexamples[0].kind,
            second.counterexamples[0].kind
        );
        assert_eq!(
            first.counterexamples[0].input,
            second.counterexamples[0].input
        );
    }

    #[test]
    fn solver_outcome_boundary_rejects_unknown_and_incomplete_replay() {
        let program = compile_text(
            r"module M
entity E { maybe: Bool? }
decision d(E e) -> Bool
rule present(E e):
  when e.maybe
  then d(e) = true
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        let invariant = program.invariant("total").unwrap();
        assert_eq!(
            solver_outcome_analysis(
                &program,
                invariant,
                SolverOutcome::Unknown("timeout".into())
            )
            .unwrap_err(),
            "embedded solver was inconclusive: timeout"
        );
        assert_eq!(
            solver_outcome_analysis(
                &program,
                invariant,
                SolverOutcome::Unavailable("disabled".into())
            )
            .unwrap_err(),
            "embedded solver unavailable: disabled"
        );

        let mut input = Input::new();
        input.insert("e", "E", BTreeMap::new());
        let replay_error = solver_outcome_analysis(
            &program,
            invariant,
            SolverOutcome::Counterexample {
                input,
                metadata: SolverMetadata {
                    backend: "test".into(),
                    version: "test".into(),
                    logic: "QF_LIA".into(),
                },
            },
        )
        .unwrap_err();
        assert!(replay_error.contains("replay needed additional input"));
        assert!(replay_error.contains("e.maybe"));
    }

    #[test]
    fn planner_prefers_a_tiny_threshold_quotient_to_small_raw_enumeration() {
        let invariant = analyze_text(
            r"module M
enum Result { Low, High }
entity E { x: Int range 0..100 }
decision d(E e) -> Result
rule low(E e):
  when e.x < 50
  then d(e) = Low
rule high(E e):
  when e.x >= 50
  then d(e) = High
invariant total:
  for all e: E
  exactly one d(e)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.evaluated, 2);
        assert_eq!(invariant.planned_evaluations, 2);
    }

    #[test]
    fn planner_honors_explicit_z3_before_a_compact_threshold_quotient() {
        let invariant = analyze_text_with_solver(
            r"module M
enum Result { Low, High }
entity E { x: Int range 0..100 }
decision d(E e) -> Result
rule low(E e):
  when e.x < 50
  then d(e) = Low
rule high(E e):
  when e.x >= 50
  then d(e) = High
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 0);
        assert_eq!(invariant.planned_evaluations, 0);
    }

    #[test]
    fn planner_uses_solver_before_a_large_supported_cartesian_product() {
        let invariant = analyze_text_auto(
            r"module M
enum Result { Any }
entity E {
  b0: Bool, b1: Bool, b2: Bool, b3: Bool, b4: Bool, b5: Bool,
  b6: Bool, b7: Bool, b8: Bool, b9: Bool, b10: Bool,
}
decision d(E e) -> Result
rule any(E e):
  when (e.b0 or not e.b0) and (e.b1 or not e.b1) and (e.b2 or not e.b2) and (e.b3 or not e.b3) and (e.b4 or not e.b4) and (e.b5 or not e.b5) and (e.b6 or not e.b6) and (e.b7 or not e.b7) and (e.b8 or not e.b8) and (e.b9 or not e.b9) and (e.b10 or not e.b10)
  then d(e) = Any
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 0);
        assert_eq!(invariant.planned_evaluations, 0);
    }

    #[test]
    fn planner_uses_bounded_qf_nia_before_a_finite_exact_product() {
        let invariant = analyze_text_auto(
            r"module M
enum Result { Any }
entity E { x: Int range 0..32, y: Int range 0..32 }
decision d(E e) -> Result
rule any(E e):
  when e.x * e.y >= 0
  then d(e) = Any
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 0);
        assert_eq!(invariant.planned_evaluations, 0);
        assert_eq!(invariant.solver.as_ref().unwrap().logic, "QF_NIA");
    }

    #[test]
    fn planner_solves_exact_decimal_division_before_small_exhaustive() {
        let invariant = analyze_text_auto(
            r"module M
enum Result { Any }
entity E { x: Int range 0..2 }
decision d(E e) -> Result
rule any(E e):
  when e.x / 1 >= 0
  then d(e) = Any
invariant total:
  for all e: E
  exactly one d(e)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 0);
        assert_eq!(invariant.planned_evaluations, 0);
        assert_eq!(invariant.solver.as_ref().unwrap().logic, "QF_LIA");
    }

    #[test]
    fn finite_string_and_decimal_domains_are_exhaustive() {
        let invariant = analyze_text_auto(
            r#"module M
enum Result { Draft, Approved }
entity E {
  status: String domain {"draft", "approved"},
  rate: Decimal domain {0.05, 0.10},
}
decision d(E e) -> Result
rule draft(E e):
  when e.status = "draft" and e.rate >= 0.05
  then d(e) = Draft
rule approved(E e):
  when e.status = "approved" and e.rate >= 0.05
  then d(e) = Approved
invariant total:
  for all e: E
  exactly one d(e)
"#,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::Exhaustive);
        assert_eq!(invariant.evaluated, 4);
        assert_eq!(invariant.planned_evaluations, 4);
    }

    #[test]
    fn solver_replays_symbolic_multiplication_overflow() {
        let invariant = analyze_text_with_solver_limit(
            r"module M
enum Result { Any }
entity E { x: Int range 0..9_223_372_036_854_775_807 }
decision d(E e) -> Result
rule any(E e):
  when e.x * e.x >= 0
  then d(e) = Any
invariant total:
  for all e: E
  exactly one d(e)
",
            1,
        );
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.solver.as_ref().unwrap().logic, "QF_NIA");
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Conflict
        );
        let x = binding_int(&invariant.counterexamples[0], "e", "x").unwrap();
        assert!(x.checked_mul(x).is_none());
    }

    #[test]
    fn planner_solves_shipping_style_max_derive_without_40_804_evaluations() {
        let invariant = analyze_text_auto(
            r"module M
enum Result { Free, Paid }
entity Order {
  amount: Int range 0..100,
  discount: Int range 0..100,
  remote: Bool,
  approved: Bool,
}
derive payable(Order o) -> Int: max(0, o.amount - o.discount)
decision shipping(Order o) -> Result
rule normal_free(Order o):
  when payable(o) >= 50 and not o.remote
  then shipping(o) = Free
rule normal_paid(Order o):
  when payable(o) < 50 and not o.remote
  then shipping(o) = Paid
rule remote_paid(Order o):
  when o.remote
  then shipping(o) = Paid
rule approved_remote(Order o):
  when o.remote and o.approved and payable(o) >= 50
  then shipping(o) = Free
  then override remote_paid
invariant total:
  for all o: Order
  exactly one shipping(o)
",
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.evaluated, 0);
        assert_eq!(invariant.planned_evaluations, 0);
    }

    #[test]
    fn solver_replays_potential_intermediate_i64_overflow() {
        let invariant = analyze_text_with_solver_limit(
            r"module M
enum Result { Less, NotLess }
entity E { x: Int }
decision d(E a, E b) -> Result
rule less(E a, E b):
  when a.x - b.x < 0
  then d(a, b) = Less
rule not_less(E a, E b):
  when a.x - b.x >= 0
  then d(a, b) = NotLess
invariant total:
  for all a: E, b: E
  exactly one d(a, b)
",
            100_000,
        );
        assert_eq!(invariant.completeness, Completeness::SolverExact);
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Conflict
        );
        let left = binding_int(&invariant.counterexamples[0], "a", "x").unwrap();
        let right = binding_int(&invariant.counterexamples[0], "b", "x").unwrap();
        assert!(left.checked_sub(right).is_none());
    }

    #[test]
    fn override_rule_with_ambiguous_same_type_extra_binding_falls_back() {
        let invariant = analyze_text(
            r"module M
enum Result { Base, Target }
entity Query { enabled: Bool }
entity Context { x: Int range 0..1_000_000_000 }
decision d(Query query) -> Result
rule target(Query query, Context context):
  when context.x < 50
  then d(query) = Target
rule suppress_target(Query query, Context context):
  when context.x >= 50
  then override target
rule base(Query query):
  when true
  then d(query) = Base
invariant total:
  for all q: Query, a: Context, b: Context
  exactly one d(q)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Inconclusive);
        assert_eq!(invariant.completeness, Completeness::BoundarySampled);
        assert!(
            invariant
                .notes
                .iter()
                .any(|note| note.contains("ambiguous quantified binding"))
        );
    }

    #[test]
    fn shared_binding_ambiguity_matches_runtime_rule_skipping() {
        let program = compile_text(
            r"module M
enum Result { Base, Target }
entity Query { enabled: Bool }
entity Context { x: Int range 0..100 }
decision d(Query query) -> Result
rule target(Query query, Context context):
  when context.x < 50
  then d(query) = Target
rule suppress_target(Query query, Context context):
  when context.x >= 50
  then override target
rule base(Query query):
  when true
  then d(query) = Base
",
        );
        let query = Query::parse("d(q)").unwrap();
        let bindings = BTreeMap::from([
            ("q".into(), "Query".into()),
            ("a".into(), "Context".into()),
            ("b".into(), "Context".into()),
        ]);
        for rule in ["target", "suppress_target"] {
            let error = resolve_rule_bindings(
                program.rule(rule).unwrap(),
                program.decision("d").unwrap(),
                &query,
                &bindings,
            )
            .unwrap_err();
            assert!(error.contains("ambiguous quantified binding"));
        }

        let mut input = Input::new();
        input.insert(
            "q",
            "Query",
            BTreeMap::from([("enabled".into(), Value::Bool(false))]),
        );
        input.insert(
            "a",
            "Context",
            BTreeMap::from([("x".into(), Value::Int(0))]),
        );
        input.insert(
            "b",
            "Context",
            BTreeMap::from([("x".into(), Value::Int(100))]),
        );
        let evaluation = evaluate_query(&program, &input, &query).unwrap();
        assert!(matches!(
            evaluation.result.status,
            DecisionStatus::Resolved { ref values }
                if values.iter().any(|value| value.to_string() == "Result::Base")
        ));
    }

    #[test]
    fn two_binding_partition_matches_exhaustive_counterexample_on_small_ranges() {
        let source = r"module M
enum Result { Present }
entity E { x: Int range 0..2 }
decision d(E first, E second) -> Result
rule present(E left, E right):
  when left.x != 1 or right.x != 2
  then d(left, right) = Present
invariant total:
  for all a: E, b: E
  exactly one d(a, b)
";
        let exhaustive = raw_counterexamples(source);
        let partitioned = analyze_text(source, 8);
        assert_eq!(partitioned.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(partitioned.verdict, AnalysisVerdict::Failed);
        assert_eq!(exhaustive[0].input, partitioned.counterexamples[0].input);
        assert_eq!(
            binding_int(&partitioned.counterexamples[0], "a", "x"),
            Some(1)
        );
        assert_eq!(
            binding_int(&partitioned.counterexamples[0], "b", "x"),
            Some(2)
        );
    }

    #[test]
    fn implication_premise_thresholds_are_part_of_the_exact_partition() {
        let invariant = analyze_text(
            r"module M
enum Result { Low, High }
entity E { x: Int range 0..1_000_000_000 }
decision d(E s) -> Result
rule low(E s):
  when s.x < 50
  then d(s) = Low
rule high(E s):
  when s.x >= 50
  then d(s) = High
invariant total:
  for all s: E
  if s.x >= 50
  then d(s) = High
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.evaluated, 2);
    }

    #[test]
    fn optional_int_missing_is_an_exact_singleton_region() {
        let invariant = analyze_text(
            r"module M
enum Result { Negative, Nonnegative }
entity E { x: Int? }
decision d(E s) -> Result
rule negative(E s):
  when s.x < 0
  then d(s) = Negative
rule nonnegative(E s):
  when s.x >= 0
  then d(s) = Nonnegative
invariant total:
  for all s: E
  exactly one d(s)
",
            100_000,
        );
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 3);
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Unknown
        );
        assert!(
            !invariant.counterexamples[0].input.bindings["s"]
                .fields
                .contains_key("x")
        );
    }

    #[test]
    fn fractional_thresholds_partition_the_integer_domain_with_floor_and_ceil() {
        let invariant = analyze_text(
            r"module M
enum Result { Low, High }
entity E { x: Int }
decision d(E s) -> Result
rule low(E s):
  when s.x < 2.5
  then d(s) = Low
rule high(E s):
  when s.x >= 2.5
  then d(s) = High
invariant total:
  for all s: E
  exactly one d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 2);
    }

    #[test]
    fn reversed_negative_fractional_thresholds_match_exhaustive_enumeration() {
        let source = r"module M
enum Result { Low, High }
entity E { x: Int range -5..5 }
decision d(E s) -> Result
rule low(E s):
  when -1.5 > s.x
  then d(s) = Low
rule high(E s):
  when -1.5 <= s.x
  then d(s) = High
invariant total:
  for all s: E
  exactly one d(s)
";
        let exhaustive = raw_counterexamples(source);
        let partitioned = analyze_text(source, 10);
        assert!(exhaustive.is_empty());
        assert_eq!(partitioned.verdict, AnalysisVerdict::Passed);
        assert_eq!(partitioned.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(partitioned.planned_evaluations, 2);
    }

    #[test]
    fn arithmetic_input_expression_falls_back_to_inconclusive_sampling() {
        let invariant = analyze_text(
            r"module M
enum Result { Low, High }
entity E { x: Int range 0..1_000_000_000 }
decision d(E s) -> Result
rule low(E s):
  when s.x + 1 < 50
  then d(s) = Low
rule high(E s):
  when s.x + 1 >= 50
  then d(s) = High
invariant total:
  for all s: E
  exactly one d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Inconclusive);
        assert_eq!(invariant.completeness, Completeness::BoundarySampled);
        assert!(
            invariant
                .notes
                .iter()
                .any(|note| note.contains("arithmetic"))
        );
        let report = AnalysisReport {
            invariants: vec![invariant],
            traces: Vec::new(),
            findings: Vec::new(),
        };
        let text = report.render_text();
        assert!(text.contains("? total\n  inconclusive ·"));
        assert!(text.contains("boundary samples checked · not exhaustive"));
        assert!(text.contains("  reason ·"));
    }

    #[test]
    fn derive_condition_falls_back_to_inconclusive_sampling() {
        let invariant = analyze_text(
            r"module M
enum Result { Low, High }
entity E { x: Int range 0..1_000_000_000 }
derive shifted(E s) -> Int: s.x + 1
decision d(E s) -> Result
rule low(E s):
  when shifted(s) < 50
  then d(s) = Low
rule high(E s):
  when shifted(s) >= 50
  then d(s) = High
invariant total:
  for all s: E
  exactly one d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Inconclusive);
        assert_eq!(invariant.completeness, Completeness::BoundarySampled);
        assert!(
            invariant
                .notes
                .iter()
                .any(|note| note.contains("derive or function call"))
        );
    }

    #[test]
    fn representative_region_limit_is_truncated_not_proved() {
        let invariant = analyze_text(
            r"module M
enum Result { Low, Exact, High }
entity E { x: Int range 0..1_000_000_000 }
decision d(E s) -> Result
rule low(E s):
  when s.x < 50
  then d(s) = Low
rule exact(E s):
  when s.x = 50
  then d(s) = Exact
rule high(E s):
  when s.x > 50
  then d(s) = High
invariant total:
  for all s: E
  exactly one d(s)
",
            2,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Inconclusive);
        assert_eq!(invariant.completeness, Completeness::Truncated);
        assert_eq!(invariant.evaluated, 2);
        assert_eq!(invariant.planned_evaluations, 3);
        assert!(
            invariant
                .notes
                .iter()
                .any(|note| note.contains("exact threshold partition"))
        );
    }

    #[test]
    fn counterexample_limit_stops_early_and_reports_truncation() {
        let program = compile_text(
            r"module M
entity E { x: Int range 0..2 }
decision d(E e) -> Bool
invariant total:
  for all e: E
  if e.x = 1 or e.x != 1
  then d(e) = true
",
        );
        let report = analyze_with_solver(
            &program,
            Some("total"),
            &AnalysisOptions {
                max_evaluations: 100,
                max_counterexamples: 1,
            },
            SolverMode::Off,
        );
        let invariant = &report.invariants[0];
        assert_eq!(invariant.verdict, AnalysisVerdict::Failed);
        assert_eq!(invariant.completeness, Completeness::Truncated);
        assert_eq!(invariant.evaluated, 1);
        assert!(invariant.planned_evaluations > invariant.evaluated);
        assert_eq!(invariant.counterexamples.len(), 1);
        assert!(
            invariant
                .notes
                .iter()
                .any(|note| note == "stopped after 1 counterexample(s)")
        );
    }

    #[test]
    fn threshold_partition_matches_exhaustive_gap_witness_on_small_range() {
        let source = r"module M
enum Result { Low, High }
entity E { x: Int range 0..10 }
decision d(E s) -> Result
rule low(E s):
  when s.x < 5
  then d(s) = Low
rule high(E s):
  when s.x > 5
  then d(s) = High
invariant total:
  for all s: E
  exactly one d(s)
";
        let exhaustive = raw_counterexamples(source);
        let partitioned = analyze_text(source, 10);
        assert_eq!(partitioned.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(partitioned.verdict, AnalysisVerdict::Failed);
        assert_eq!(exhaustive[0].input, partitioned.counterexamples[0].input);
    }

    #[test]
    fn empty_resolved_value_set_is_reported_as_undefined() {
        let invariant = analyze_text(
            r"module M
entity E { x: Int range 0..0 }
decision d(E s) -> Bool zero or one
invariant total:
  for all s: E
  exactly one d(s)
",
            100_000,
        );
        assert_eq!(
            invariant.counterexamples[0].kind,
            CounterexampleKind::Undefined
        );
    }

    #[test]
    fn decimal_boundary_sampling_does_not_overflow_at_maximum() {
        let field = FieldDecl {
            name: Spanned::new("x".into(), Span::default()),
            ty: TypeRef::Decimal,
            range: None,
            domain: None,
            optional: false,
            span: Span::default(),
        };
        let values = decimal_values(&field, &BTreeSet::from([Decimal::MAX]));
        assert!(values.contains(&Value::decimal(Decimal::MAX)));
    }

    #[test]
    fn full_i64_range_size_is_not_saturated_into_a_false_finite_size() {
        let entity = EntityDecl {
            name: Spanned::new("E".into(), Span::default()),
            fields: vec![FieldDecl {
                name: Spanned::new("x".into(), Span::default()),
                ty: TypeRef::Int,
                range: Some(RangeConstraint {
                    start: NumericLiteral::Int(i64::MIN),
                    end: NumericLiteral::Int(i64::MAX),
                    span: Span::default(),
                }),
                domain: None,
                optional: false,
                span: Span::default(),
            }],
            span: Span::default(),
        };
        let program = crate::compile_source(SourceFile::new(
            "empty.tes",
            "module M\nentity E { x: Int }\n",
        ))
        .program
        .expect("compiled program");
        assert_eq!(finite_domain_size(&program, &entity), None);
    }

    #[test]
    fn equality_at_i64_max_partitions_the_full_integer_domain_without_overflow() {
        let invariant = analyze_text(
            r"module M
enum Result { Other, Maximum }
entity E { x: Int }
decision d(E s) -> Result
rule maximum(E s):
  when s.x = 9_223_372_036_854_775_807
  then d(s) = Maximum
rule other(E s):
  when s.x != 9_223_372_036_854_775_807
  then d(s) = Other
invariant total:
  for all s: E
  exactly one d(s)
",
            100_000,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.planned_evaluations, 2);
    }

    #[test]
    fn huge_requested_limit_uses_partition_instead_of_materializing_a_huge_int_vec() {
        let invariant = analyze_text(
            r"module M
enum Result { Negative, Nonnegative }
entity E { x: Int range -9_000_000_000_000_000_000..9_000_000_000_000_000_000 }
decision d(E s) -> Result
rule negative(E s):
  when s.x < 0
  then d(s) = Negative
rule nonnegative(E s):
  when s.x >= 0
  then d(s) = Nonnegative
invariant total:
  for all s: E
  exactly one d(s)
",
            usize::MAX,
        );
        assert_eq!(invariant.verdict, AnalysisVerdict::Passed);
        assert_eq!(invariant.completeness, Completeness::ThresholdPartitioned);
        assert_eq!(invariant.evaluated, 2);
        assert!(
            invariant
                .notes
                .iter()
                .any(|note| note.contains("internal safety cap"))
        );
    }

    #[test]
    fn threshold_completeness_has_stable_serde_name() {
        assert_eq!(
            serde_json::to_value(Completeness::ThresholdPartitioned).unwrap(),
            serde_json::json!("threshold_partitioned")
        );
    }
}