tessellate-core 0.11.0

//! Optional exact analysis through the embedded Z3 SMT solver.
//!
//! The core evaluator remains the semantic authority. This module only accepts
//! a total, overflow-safe arithmetic fragment, asks Z3 for either a universal
//! violation or an existential witness, and returns concrete SAT models for
//! the evaluator to replay.

use crate::ast::{
    BinaryOp, Cardinality, DeriveBody, Effect, ExpectedValue, Expr, ExprKind, InvariantAssertion,
    InvariantDecl, InvariantQuantifier, Literal, NumericLiteral, TypeRef, UnaryOp,
};
use crate::compiler::{
    CompiledProgram, ValueType, effective_decimal_range_bounds, effective_int_range_bounds,
    normalize_name,
};
use crate::engine::{Input, Query, constant_value, resolve_rule_bindings};
use crate::smtlib::{
    SMTLIB_QUERY_SCHEMA_VERSION, SmtLibExportError, SmtLibMetadata, SmtLibQuery, SmtSourceLocation,
    SmtSymbol, SmtSymbolEncoding,
};
use crate::value::{
    Value, checked_decimal_add, checked_decimal_div, checked_decimal_mul, checked_decimal_sub,
    parse_decimal,
};
use chrono::{Datelike, NaiveDate};
use rust_decimal::Decimal;
use serde::{Deserialize, Serialize};
use std::collections::{BTreeMap, BTreeSet};
use std::fmt::Write as _;
use z3::ast::{Ast, Bool, Int};
use z3::{Params, SatResult, Solver, full_version};

const Z3_TIMEOUT_MS: u32 = 5_000;
const FINITE_ARITHMETIC_VALUE_LIMIT: usize = 256;

/// Controls whether relational assertions may use the optional Z3 backend.
#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
pub enum SolverMode {
    /// Try Z3 when compact exact enumeration is unavailable or too costly.
    #[default]
    Auto,
    /// Never invoke the embedded solver.
    Off,
    /// Try Z3 before concrete strategies; unsupported or unknown results fall back safely.
    Z3,
}

/// Reproducibility metadata for an exact solver result.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct SolverMetadata {
    pub backend: String,
    pub version: String,
    pub logic: String,
}

pub(crate) enum SolverOutcome {
    /// A universal assertion has no violating assignment.
    Proved(SolverMetadata),
    /// A universal assertion has a concrete violating assignment.
    Counterexample {
        input: Input,
        metadata: SolverMetadata,
    },
    /// An existential assertion has a concrete satisfying assignment.
    Witness {
        input: Input,
        metadata: SolverMetadata,
    },
    /// An existential assertion has no satisfying assignment.
    Refuted(SolverMetadata),
    Unavailable(String),
    Unsupported(String),
    Unknown(String),
}

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

#[derive(Clone)]
enum SymbolInfo {
    Presence {
        present: Bool,
    },
    Bool {
        expression: Bool,
        present: Bool,
    },
    Int {
        expression: Int,
        present: Bool,
    },
    Decimal {
        scaled: Int,
        mantissa: Int,
        scale: Int,
        present: Bool,
    },
    Enum {
        expression: Int,
        type_name: String,
        variants: Vec<String>,
        present: Bool,
    },
    Date {
        expression: Int,
        present: Bool,
    },
}

impl SymbolInfo {
    fn present(&self) -> &Bool {
        match self {
            Self::Presence { present }
            | Self::Bool { present, .. }
            | Self::Int { present, .. }
            | Self::Decimal { present, .. }
            | Self::Enum { present, .. }
            | Self::Date { present, .. } => present,
        }
    }
}

#[derive(Clone)]
struct BooleanTerm {
    truth: Bool,
    unknown: Bool,
    conflict: Bool,
}

#[derive(Clone)]
struct ValueStatus {
    unknown: Bool,
    conflict: Bool,
}

struct ScalarArgument {
    parameter_name: String,
    parameter_type: TypeRef,
    expression: Expr,
    strictly_propagated: bool,
}

enum InlinedDeriveBody {
    Expression(Expr),
    Case(Vec<InlinedCaseBranch>),
}

struct InlinedCaseBranch {
    condition: Expr,
    value: Expr,
}

struct InlinedDerive {
    body: InlinedDeriveBody,
    receivers: BTreeMap<String, String>,
    scalar_arguments: Vec<ScalarArgument>,
}

struct CaseSelection {
    active: Vec<Bool>,
    unknown: Bool,
    conflict: Bool,
}

#[derive(Clone)]
struct IntTerm {
    value: Int,
    valid: Bool,
    unknown: Bool,
    bounds: Option<Interval>,
}

#[derive(Clone)]
struct DecimalTerm {
    scaled: Int,
    valid: Bool,
    unknown: Bool,
}

#[derive(Clone)]
struct EnumTerm {
    value: Int,
    valid: Bool,
    unknown: Bool,
}

#[derive(Clone)]
struct DateTerm {
    value: Int,
    valid: Bool,
    unknown: Bool,
}

#[derive(Clone, Copy)]
struct Interval {
    lower: i128,
    upper: i128,
}

impl Interval {
    fn within_i64(self) -> bool {
        self.lower >= i128::from(i64::MIN) && self.upper <= i128::from(i64::MAX)
    }
}

struct CandidateFormula {
    rule: String,
    value: CandidateValueFormula,
    active: Bool,
    unknown: Bool,
    conflict: Bool,
}

struct BlockerFormula {
    rule: String,
    unknown: Bool,
    conflict: Bool,
}

struct UncertainOverrideFormula {
    targets: Vec<String>,
    unknown: Bool,
}

#[derive(Clone)]
enum CandidateValueFormula {
    Concrete(Value),
    Bool(Bool),
    Int(Int),
    Decimal(Int),
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
enum TranslatorCapability {
    Embedded,
    ExternalV2,
}

struct Translator<'a> {
    program: &'a CompiledProgram,
    invariant: &'a InvariantDecl,
    solver: &'a Solver,
    binding_entities: BTreeMap<String, String>,
    symbols: BTreeMap<FieldKey, SymbolInfo>,
    capability: TranslatorCapability,
    uses_nonlinear_arithmetic: bool,
}

impl<'a> Translator<'a> {
    fn new(
        program: &'a CompiledProgram,
        invariant: &'a InvariantDecl,
        solver: &'a Solver,
    ) -> Result<Self, String> {
        Self::new_with_capability(program, invariant, solver, TranslatorCapability::Embedded)
    }

    fn new_for_external_export(
        program: &'a CompiledProgram,
        invariant: &'a InvariantDecl,
        solver: &'a Solver,
    ) -> Result<Self, String> {
        Self::new_with_capability(program, invariant, solver, TranslatorCapability::ExternalV2)
    }

    fn new_with_capability(
        program: &'a CompiledProgram,
        invariant: &'a InvariantDecl,
        solver: &'a Solver,
        capability: TranslatorCapability,
    ) -> Result<Self, String> {
        if capability == TranslatorCapability::ExternalV2 {
            for variable in &invariant.variables {
                if program
                    .entity(&variable.ty.value)
                    .is_some_and(|entity| !entity.choices.is_empty())
                {
                    return Err(format!(
                        "record choice constraints for `{}` cannot yet be represented by the external SMT schema",
                        variable.ty.value
                    ));
                }
            }
        }
        let binding_entities = invariant
            .variables
            .iter()
            .map(|variable| {
                (
                    normalize_name(&variable.name.value),
                    normalize_name(&variable.ty.value),
                )
            })
            .collect::<BTreeMap<_, _>>();
        let mut translator = Self {
            program,
            invariant,
            solver,
            binding_entities,
            symbols: BTreeMap::new(),
            capability,
            uses_nonlinear_arithmetic: false,
        };
        translator.declare_supported_fields()?;
        translator.assert_choice_shapes()?;
        Ok(translator)
    }

    fn declare_supported_fields(&mut self) -> Result<(), String> {
        for variable in &self.invariant.variables {
            let binding = normalize_name(&variable.name.value);
            let entity = self
                .program
                .entity(&variable.ty.value)
                .ok_or_else(|| format!("unknown assertion record `{}`", variable.ty.value))?;
            for field in &entity.fields {
                if self.capability == TranslatorCapability::ExternalV2
                    && (field.optional || matches!(field.ty, TypeRef::Date))
                {
                    continue;
                }
                let key = FieldKey {
                    binding: binding.clone(),
                    field: normalize_name(&field.name.value),
                };
                let symbol_name = format!("v{}", self.symbols.len());
                let present = if field.optional {
                    Bool::new_const(format!("{symbol_name}_present"))
                } else {
                    bool_lit(true)
                };
                let symbol = match &field.ty {
                    TypeRef::Bool => SymbolInfo::Bool {
                        expression: Bool::new_const(symbol_name),
                        present,
                    },
                    TypeRef::Int => SymbolInfo::Int {
                        expression: Int::new_const(symbol_name),
                        present,
                    },
                    TypeRef::Decimal => {
                        let mantissa = Int::new_const(format!("{symbol_name}_mantissa"));
                        let scale = Int::new_const(format!("{symbol_name}_scale"));
                        SymbolInfo::Decimal {
                            scaled: decimal_scaled_expression(&mantissa, &scale),
                            mantissa,
                            scale,
                            present,
                        }
                    }
                    TypeRef::Named(type_name) => {
                        let declaration = self.program.enum_decl(type_name).ok_or_else(|| {
                            format!("field `{binding}.{}` is not an enum", field.name.value)
                        })?;
                        let variants = declaration
                            .variants
                            .iter()
                            .map(|variant| variant.value.clone())
                            .collect::<Vec<_>>();
                        if variants.is_empty() {
                            return Err(format!(
                                "enum field `{binding}.{}` has no values",
                                field.name.value
                            ));
                        }
                        SymbolInfo::Enum {
                            expression: Int::new_const(symbol_name),
                            type_name: type_name.clone(),
                            variants,
                            present,
                        }
                    }
                    TypeRef::Date => SymbolInfo::Date {
                        expression: Int::new_const(symbol_name),
                        present,
                    },
                    TypeRef::String | TypeRef::Duration
                        if self.capability == TranslatorCapability::Embedded =>
                    {
                        // The embedded solver cannot reason about these values,
                        // but a tagged choice still needs their presence bit to
                        // enforce branch shape. SAT model replay fills a present
                        // field with a valid deterministic representative.
                        SymbolInfo::Presence { present }
                    }
                    TypeRef::String | TypeRef::Duration | TypeRef::Unknown => continue,
                };
                match &symbol {
                    SymbolInfo::Presence { .. } => {}
                    SymbolInfo::Bool {
                        expression,
                        present,
                    } => {
                        if let Some(domain) = &field.domain {
                            let allowed = domain
                                .values
                                .iter()
                                .map(|candidate| {
                                    match constant_value(
                                        self.program,
                                        candidate,
                                        Some(&TypeRef::Bool),
                                    )? {
                                        Value::Bool(value) => {
                                            Ok(Ast::eq(expression, Bool::from_bool(value)))
                                        }
                                        _ => Err("Bool domain contains a non-Bool value".into()),
                                    }
                                })
                                .collect::<Result<Vec<_>, String>>()?;
                            self.solver
                                .assert(bool_or(vec![present.clone().not(), bool_or(allowed)]));
                        }
                    }
                    SymbolInfo::Int {
                        expression,
                        present,
                    } => {
                        let (lower, upper) = int_bounds(field)?;
                        self.solver.assert(bool_or(vec![
                            present.clone().not(),
                            expression.ge(Int::from_i64(lower)),
                        ]));
                        self.solver.assert(bool_or(vec![
                            present.clone().not(),
                            expression.le(Int::from_i64(upper)),
                        ]));
                        if let Some(domain) = &field.domain {
                            let allowed = domain
                                .values
                                .iter()
                                .map(|candidate| {
                                    match constant_value(
                                        self.program,
                                        candidate,
                                        Some(&TypeRef::Int),
                                    )? {
                                        Value::Int(value) => {
                                            Ok(Ast::eq(expression, Int::from_i64(value)))
                                        }
                                        _ => Err("Int domain contains a non-Int value".into()),
                                    }
                                })
                                .collect::<Result<Vec<_>, String>>()?;
                            self.solver
                                .assert(bool_or(vec![present.clone().not(), bool_or(allowed)]));
                        }
                    }
                    SymbolInfo::Decimal {
                        scaled,
                        mantissa,
                        scale,
                        present,
                    } => {
                        let maximum = decimal_mantissa_numeral(Decimal::MAX);
                        let minimum = decimal_mantissa_numeral(Decimal::MIN);
                        for constraint in [
                            mantissa.ge(minimum),
                            mantissa.le(maximum),
                            scale.ge(Int::from_i64(0)),
                            scale.le(Int::from_u64(u64::from(Decimal::MAX_SCALE))),
                        ] {
                            self.solver
                                .assert(bool_or(vec![present.clone().not(), constraint]));
                        }
                        if let Some(range) = &field.range {
                            let lower = numeric_decimal(&range.start).ok_or_else(|| {
                                format!("invalid Decimal lower bound for `{}`", field.name.value)
                            })?;
                            let upper = numeric_decimal(&range.end).ok_or_else(|| {
                                format!("invalid Decimal upper bound for `{}`", field.name.value)
                            })?;
                            let lower = decimal_scaled_numeral(lower);
                            let upper = decimal_scaled_numeral(upper);
                            let lower_constraint = if range.start_inclusive {
                                scaled.ge(lower)
                            } else {
                                scaled.gt(lower)
                            };
                            let upper_constraint = if range.end_inclusive {
                                scaled.le(upper)
                            } else {
                                scaled.lt(upper)
                            };
                            self.solver
                                .assert(bool_or(vec![present.clone().not(), lower_constraint]));
                            self.solver
                                .assert(bool_or(vec![present.clone().not(), upper_constraint]));
                        }
                        if let Some(domain) = &field.domain {
                            let allowed = domain
                                .values
                                .iter()
                                .map(|expression| {
                                    constant_value(
                                        self.program,
                                        expression,
                                        Some(&TypeRef::Decimal),
                                    )
                                    .and_then(|value| {
                                        match value {
                                            Value::Decimal(value) => {
                                                Ok(Ast::eq(scaled, decimal_scaled_numeral(value)))
                                            }
                                            Value::Int(value) => Ok(Ast::eq(
                                                scaled,
                                                decimal_scaled_numeral(Decimal::from(value)),
                                            )),
                                            _ => Err("Decimal domain contains a non-number".into()),
                                        }
                                    })
                                })
                                .collect::<Result<Vec<_>, String>>()?;
                            self.solver
                                .assert(bool_or(vec![present.clone().not(), bool_or(allowed)]));
                        }
                    }
                    SymbolInfo::Enum {
                        expression,
                        type_name,
                        variants,
                        present,
                        ..
                    } => {
                        self.solver.assert(bool_or(vec![
                            present.clone().not(),
                            expression.ge(Int::from_i64(0)),
                        ]));
                        self.solver.assert(bool_or(vec![
                            present.clone().not(),
                            expression.lt(Int::from_u64(variants.len() as u64)),
                        ]));
                        if let Some(domain) = &field.domain {
                            let allowed = domain
                                .values
                                .iter()
                                .map(|candidate| {
                                    let value = constant_value(
                                        self.program,
                                        candidate,
                                        Some(&TypeRef::Named(type_name.clone())),
                                    )?;
                                    let Value::Enum { variant, .. } = value else {
                                        return Err("enum domain contains a non-enum value".into());
                                    };
                                    let index = variants
                                        .iter()
                                        .position(|item| {
                                            normalize_name(item) == normalize_name(&variant)
                                        })
                                        .ok_or_else(|| {
                                            format!("unknown `{type_name}` variant `{variant}`")
                                        })?;
                                    Ok(Ast::eq(expression, Int::from_u64(index as u64)))
                                })
                                .collect::<Result<Vec<_>, String>>()?;
                            self.solver
                                .assert(bool_or(vec![present.clone().not(), bool_or(allowed)]));
                        }
                    }
                    SymbolInfo::Date {
                        expression,
                        present,
                    } => {
                        for constraint in [
                            expression
                                .ge(Int::from_i64(i64::from(NaiveDate::MIN.num_days_from_ce()))),
                            expression
                                .le(Int::from_i64(i64::from(NaiveDate::MAX.num_days_from_ce()))),
                        ] {
                            self.solver
                                .assert(bool_or(vec![present.clone().not(), constraint]));
                        }
                        if let Some(domain) = &field.domain {
                            let allowed = domain
                                .values
                                .iter()
                                .map(|candidate| {
                                    match constant_value(
                                        self.program,
                                        candidate,
                                        Some(&TypeRef::Date),
                                    )? {
                                        Value::Date(value) => Ok(Ast::eq(
                                            expression,
                                            Int::from_i64(i64::from(value.num_days_from_ce())),
                                        )),
                                        _ => Err("Date domain contains a non-Date value".into()),
                                    }
                                })
                                .collect::<Result<Vec<_>, String>>()?;
                            self.solver
                                .assert(bool_or(vec![present.clone().not(), bool_or(allowed)]));
                        }
                    }
                }
                self.symbols.insert(key, symbol);
            }
        }
        Ok(())
    }

    fn assert_choice_shapes(&self) -> Result<(), String> {
        for variable in &self.invariant.variables {
            let binding = normalize_name(&variable.name.value);
            let entity = self
                .program
                .entity(&variable.ty.value)
                .ok_or_else(|| format!("unknown assertion record `{}`", variable.ty.value))?;
            for choice in &entity.choices {
                let selector_field = entity.fields.get(choice.selector_field).ok_or_else(|| {
                    format!(
                        "record `{}` has an invalid choice selector",
                        entity.name.value
                    )
                })?;
                let selector_key = FieldKey {
                    binding: binding.clone(),
                    field: normalize_name(&selector_field.name.value),
                };
                let selector_symbol = self.symbols.get(&selector_key).ok_or_else(|| {
                    format!(
                        "choice selector `{}.{}` is outside the embedded solver fragment",
                        binding, selector_field.name.value
                    )
                })?;
                let SymbolInfo::Enum {
                    expression,
                    variants,
                    present: selector_present,
                    ..
                } = selector_symbol
                else {
                    return Err(format!(
                        "choice selector `{}.{}` is not an enum",
                        binding, selector_field.name.value
                    ));
                };

                for branch in &choice.branches {
                    let variant_index = variants
                        .iter()
                        .position(|variant| {
                            normalize_name(variant) == normalize_name(&branch.variant.value)
                        })
                        .ok_or_else(|| {
                            format!(
                                "choice branch `{}` is not a selector enum variant",
                                branch.variant.value
                            )
                        })?;
                    let active = bool_and(
                        selector_present.clone(),
                        Ast::eq(expression, Int::from_u64(variant_index as u64)),
                    );
                    for member in &branch.members {
                        let field = entity.fields.get(member.field).ok_or_else(|| {
                            format!(
                                "choice branch `{}` has an invalid field",
                                branch.variant.value
                            )
                        })?;
                        let key = FieldKey {
                            binding: binding.clone(),
                            field: normalize_name(&field.name.value),
                        };
                        let symbol = self.symbols.get(&key).ok_or_else(|| {
                            format!(
                                "choice field `{}.{}` is outside the embedded solver fragment",
                                binding, field.name.value
                            )
                        })?;
                        let member_present = symbol.present().clone();
                        // A member can only exist in its own active branch.
                        self.solver
                            .assert(bool_or(vec![member_present.clone().not(), active.clone()]));
                        if member.required_when_active {
                            // Surface-required members must exist whenever their
                            // branch is selected.
                            self.solver
                                .assert(bool_or(vec![active.clone().not(), member_present]));
                        }
                    }
                }
            }
        }
        Ok(())
    }

    /// Return the exact quantifier-specific search target.
    ///
    /// A universal assertion searches for one failure. An existential
    /// cardinality assertion searches for a non-failure. For an existential
    /// implication, a vacuously satisfied implication is deliberately not a
    /// witness: both its premise and expected result must hold.
    fn query_formula(&mut self) -> Result<Bool, String> {
        let (decision_name, arguments) = match &self.invariant.assertion {
            InvariantAssertion::Cardinality {
                decision,
                arguments,
                ..
            } => (&decision.value, arguments.as_slice()),
            InvariantAssertion::Implication { expectation, .. } => (
                &expectation.decision.value,
                expectation.arguments.as_slice(),
            ),
        };
        let query = Query {
            decision: normalize_name(decision_name),
            arguments: arguments
                .iter()
                .map(|argument| match &argument.kind {
                    ExprKind::Name(name) => Ok(normalize_name(name)),
                    _ => Err(
                        "the assertion decision must receive record parameters directly".to_owned(),
                    ),
                })
                .collect::<Result<Vec<_>, _>>()?,
        };
        let decision = self
            .program
            .decision(&query.decision)
            .ok_or_else(|| format!("unknown decision `{}`", query.decision))?;
        let candidate_rule_names = self
            .program
            .rules()
            .iter()
            .filter(|(_, rule)| rule_directly_decides(rule, &query.decision))
            .map(|(name, _)| name.clone())
            .collect::<BTreeSet<_>>();
        let relevant_rules = self
            .program
            .rules()
            .iter()
            .filter(|(name, rule)| {
                candidate_rule_names.contains(*name)
                    || rule.override_targets().any(|(target, _)| {
                        candidate_rule_names.contains(&normalize_name(&target.value))
                    })
            })
            .map(|(_, rule)| rule)
            .collect::<Vec<_>>();

        let mut candidates = Vec::new();
        let mut overrides = BTreeMap::<String, Vec<Bool>>::new();
        let mut blockers = Vec::new();
        let mut uncertain_overrides = Vec::new();
        for rule in relevant_rules {
            let parameter_names = rule
                .parameters
                .iter()
                .map(|parameter| normalize_name(&parameter.name.value))
                .collect::<BTreeSet<_>>();
            if let Effect::Decide {
                decision: target,
                arguments,
                ..
            } = &rule.effect
            {
                if normalize_name(&target.value) == query.decision
                    && (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!(
                        "rule `{}` uses a dynamic decision argument",
                        rule.name.value
                    ));
                }
            }
            let Ok(receivers) =
                resolve_rule_bindings(rule, decision, &query, &self.binding_entities)
            else {
                // The runtime skips rules whose parameters cannot bind to this query.
                continue;
            };
            let condition = self.translate_bool(&rule.condition, &receivers)?;
            let active = condition.truth.clone();
            let rule_name = normalize_name(&rule.name.value);
            let override_targets = rule
                .override_targets()
                .map(|(target, _)| normalize_name(&target.value))
                .filter(|target| candidate_rule_names.contains(target))
                .collect::<Vec<_>>();
            for target in &override_targets {
                if candidate_rule_names.contains(target) {
                    overrides
                        .entry(target.clone())
                        .or_default()
                        .push(active.clone());
                }
            }
            let directly_affects = candidate_rule_names.contains(&rule_name);
            if directly_affects || !override_targets.is_empty() {
                blockers.push(BlockerFormula {
                    rule: rule_name.clone(),
                    unknown: if directly_affects {
                        condition.unknown.clone()
                    } else {
                        bool_lit(false)
                    },
                    // Conflicting override conditions are blockers even when
                    // no currently alive candidate happens to be their target.
                    conflict: condition.conflict.clone(),
                });
            }
            if !override_targets.is_empty() {
                uncertain_overrides.push(UncertainOverrideFormula {
                    targets: override_targets,
                    unknown: condition.unknown,
                });
            }
            if let Effect::Decide {
                decision: target,
                arguments,
                value,
                ..
            } = &rule.effect
            {
                if normalize_name(&target.value) == query.decision
                    && effect_matches_query(arguments, &query, &receivers)
                {
                    let (value, unknown, conflict) = self.translate_candidate_value(
                        value,
                        &decision.return_type.value,
                        &receivers,
                    )?;
                    blockers.push(BlockerFormula {
                        rule: rule_name.clone(),
                        unknown: bool_and(active.clone(), unknown.clone()),
                        conflict: bool_and(active.clone(), conflict.clone()),
                    });
                    candidates.push(CandidateFormula {
                        rule: rule_name,
                        value,
                        active: active.clone(),
                        unknown,
                        conflict,
                    });
                }
            }
        }

        let mut present = Vec::new();
        for candidate in candidates {
            let override_active =
                bool_or(overrides.get(&candidate.rule).cloned().unwrap_or_default());
            let valid = bool_or(vec![candidate.unknown, candidate.conflict]).not();
            let alive = bool_and(bool_and(candidate.active, valid), override_active.not());
            present.push((candidate.rule, candidate.value, alive));
        }
        let any_present = bool_or(
            present
                .iter()
                .map(|(_, _, formula)| formula.clone())
                .collect(),
        );
        let gap = any_present.not();
        let mut overlaps = Vec::new();
        for left in 0..present.len() {
            for right in left + 1..present.len() {
                let both_alive = bool_and(present[left].2.clone(), present[right].2.clone());
                let different = candidate_values_equal(&present[left].1, &present[right].1)?.not();
                overlaps.push(bool_and(both_alive, different));
            }
        }
        let overlap = bool_or(overlaps);
        let query_conflict = bool_or(
            blockers
                .iter()
                .map(|blocker| blocker.conflict.clone())
                .collect(),
        );
        let mut query_unknowns = blockers
            .iter()
            .map(|blocker| {
                let override_active =
                    bool_or(overrides.get(&blocker.rule).cloned().unwrap_or_default());
                bool_and(blocker.unknown.clone(), override_active.not())
            })
            .collect::<Vec<_>>();
        query_unknowns.extend(uncertain_overrides.into_iter().map(|uncertain| {
            let target_alive = bool_or(
                present
                    .iter()
                    .filter(|(rule, _, _)| uncertain.targets.contains(rule))
                    .map(|(_, _, alive)| alive.clone())
                    .collect(),
            );
            bool_and(uncertain.unknown, target_alive)
        }));
        let query_unknown = bool_or(query_unknowns);
        let query_invalid = bool_or(vec![query_unknown, query_conflict.clone()]);

        match &self.invariant.assertion {
            InvariantAssertion::Cardinality { cardinality, .. } => {
                let cardinality_failure = match cardinality {
                    Cardinality::ExactlyOne => bool_or(vec![gap, overlap]),
                    Cardinality::Many if decision.cardinality == Cardinality::Many => {
                        bool_lit(false)
                    }
                    Cardinality::ZeroOrOne | Cardinality::Many => overlap.clone(),
                };
                // A universal `d*` over a decision whose provider contract is
                // already `Many` has no upper or lower cardinality bound for a
                // missing fact to violate. The decision query itself remains
                // `unknown`; only this cardinality assertion can prove that
                // every completion still has an allowed number of values.
                //
                // Existential assertions must keep requiring a concrete,
                // resolved witness, and a consumer-side `*` must not erase an
                // exact-one/optional provider's unresolved contract.
                let assertion_invalid = if self.invariant.quantifier == InvariantQuantifier::All
                    && *cardinality == Cardinality::Many
                    && decision.cardinality == Cardinality::Many
                {
                    query_conflict
                } else {
                    query_invalid
                };
                let failure = bool_or(vec![assertion_invalid, cardinality_failure]);
                Ok(match self.invariant.quantifier {
                    InvariantQuantifier::All => failure,
                    InvariantQuantifier::Some => failure.not(),
                })
            }
            InvariantAssertion::Implication {
                condition,
                expectation,
                ..
            } => {
                let invariant_receivers = self
                    .binding_entities
                    .keys()
                    .map(|binding| (binding.clone(), binding.clone()))
                    .collect::<BTreeMap<_, _>>();
                let premise = self.translate_bool(condition, &invariant_receivers)?;
                let ExpectedValue::Scalar(expected_expression) = &expectation.expected else {
                    return Err("set expectations are outside assertion solving".to_owned());
                };
                let expected = constant_value(
                    self.program,
                    expected_expression,
                    Some(&decision.return_type.value),
                )
                .map_err(|error| format!("assertion expectation is not constant: {error}"))?;
                let expected_present = bool_or(
                    present
                        .iter()
                        .map(|(_, value, alive)| {
                            Ok(bool_and(
                                alive.clone(),
                                candidate_equals_value(value, &expected)?,
                            ))
                        })
                        .collect::<Result<Vec<_>, String>>()?,
                );
                let conflict = if decision.cardinality == Cardinality::Many {
                    bool_lit(false)
                } else {
                    overlap.clone()
                };
                // A missing candidate is undefined only for an exactly-one
                // decision. Zero-or-one and many decisions resolve to a valid
                // empty value set, so `!= expected` is true for that result.
                let undefined = if decision.cardinality == Cardinality::ExactlyOne {
                    gap.clone()
                } else {
                    bool_lit(false)
                };
                let relation_failure = match expectation.operator {
                    crate::ast::CompareOp::Equal => expected_present.not(),
                    crate::ast::CompareOp::NotEqual => expected_present,
                };
                let bad_result =
                    bool_or(vec![query_invalid, conflict, undefined, relation_failure]);
                let premise_invalid = bool_or(vec![premise.unknown, premise.conflict]);
                Ok(match self.invariant.quantifier {
                    InvariantQuantifier::All => {
                        bool_or(vec![premise_invalid, bool_and(premise.truth, bad_result)])
                    }
                    InvariantQuantifier::Some => bool_and(
                        bool_and(premise_invalid.not(), premise.truth),
                        bad_result.not(),
                    ),
                })
            }
        }
    }

    fn translate_candidate_value(
        &mut self,
        expression: &Expr,
        expected: &TypeRef,
        receivers: &BTreeMap<String, String>,
    ) -> Result<(CandidateValueFormula, Bool, Bool), String> {
        match expected {
            TypeRef::Bool => {
                let value = self.translate_bool(expression, receivers)?;
                Ok((
                    CandidateValueFormula::Bool(value.truth),
                    value.unknown,
                    value.conflict,
                ))
            }
            TypeRef::Int => {
                let value = self.translate_int(expression, receivers)?;
                let conflict = bool_and(value.valid.clone().not(), value.unknown.clone().not());
                Ok((
                    CandidateValueFormula::Int(value.value),
                    value.unknown,
                    conflict,
                ))
            }
            TypeRef::Decimal => {
                let total_on_finite_domain =
                    self.finite_decimal_values(expression, receivers).is_some();
                let value = self.translate_scaled_numeric(expression, receivers)?;
                let (unknown, conflict) = if total_on_finite_domain {
                    (bool_lit(false), bool_lit(false))
                } else {
                    (
                        value.unknown.clone(),
                        bool_and(value.valid.clone().not(), value.unknown.not()),
                    )
                };
                Ok((
                    CandidateValueFormula::Decimal(value.scaled),
                    unknown,
                    conflict,
                ))
            }
            _ => constant_value(self.program, expression, Some(expected))
                .map(|value| {
                    (
                        CandidateValueFormula::Concrete(value),
                        bool_lit(false),
                        bool_lit(false),
                    )
                })
                .map_err(|error| {
                    format!(
                        "dynamic {expected:?} candidate is outside the solver fragment: {error}"
                    )
                }),
        }
    }

    fn translate_bool(
        &mut self,
        expression: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Result<BooleanTerm, String> {
        match &expression.kind {
            ExprKind::Literal(Literal::Bool(value)) => Ok(boolean_known(bool_lit(*value))),
            ExprKind::Literal(Literal::Unknown) => {
                Err("`unknown` is outside the solver's total Boolean fragment".into())
            }
            ExprKind::Field { .. } => {
                let (key, field) = self.direct_field(expression, receivers)?;
                if field.ty != TypeRef::Bool {
                    return Err(format!("field `{}.{}` is not Bool", key.binding, key.field));
                }
                match self.symbols.get(&key) {
                    Some(SymbolInfo::Bool {
                        expression,
                        present,
                    }) => Ok(BooleanTerm {
                        truth: bool_and(present.clone(), expression.clone()),
                        unknown: present.clone().not(),
                        conflict: bool_lit(false),
                    }),
                    _ => Err(self.missing_symbol_reason(&key, field, "Bool")),
                }
            }
            ExprKind::Unary {
                operator: UnaryOp::Not,
                operand,
            } => {
                let operand = self.translate_bool(operand, receivers)?;
                Ok(boolean_not(operand))
            }
            ExprKind::Binary {
                left,
                operator: BinaryOp::And,
                right,
            } => {
                let left = self.translate_bool(left, receivers)?;
                let right = self.translate_bool(right, receivers)?;
                Ok(boolean_and(left, right))
            }
            ExprKind::Binary {
                left,
                operator: BinaryOp::Or,
                right,
            } => {
                let left = self.translate_bool(left, receivers)?;
                let right = self.translate_bool(right, receivers)?;
                Ok(boolean_or(left, right))
            }
            ExprKind::Binary {
                left,
                operator:
                    operator @ (BinaryOp::Equal
                    | BinaryOp::NotEqual
                    | BinaryOp::Greater
                    | BinaryOp::GreaterEqual
                    | BinaryOp::Less
                    | BinaryOp::LessEqual),
                right,
            } => self.translate_comparison(left, *operator, right, receivers),
            ExprKind::Call {
                callee, arguments, ..
            } => self.translate_bool_derive_call(&callee.value, arguments, receivers),
            ExprKind::Binary { .. }
            | ExprKind::Unary { .. }
            | ExprKind::Literal(_)
            | ExprKind::Name(_) => Err("unsupported Boolean expression in solver fragment".into()),
        }
    }

    fn translate_comparison(
        &mut self,
        left: &Expr,
        operator: BinaryOp,
        right: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Result<BooleanTerm, String> {
        let left_type = self
            .program
            .type_of_span(left.span)
            .ok_or_else(|| "missing compiled type for comparison".to_owned())?;
        let right_type = self
            .program
            .type_of_span(right.span)
            .ok_or_else(|| "missing compiled type for comparison".to_owned())?;
        if matches!(left_type, ValueType::Decimal) || matches!(right_type, ValueType::Decimal) {
            if !matches!(left_type, ValueType::Int | ValueType::Decimal)
                || !matches!(right_type, ValueType::Int | ValueType::Decimal)
            {
                return Err("Decimal comparison requires numeric operands".into());
            }
            let left = self.translate_scaled_numeric(left, receivers)?;
            let right = self.translate_scaled_numeric(right, receivers)?;
            return numeric_comparison(
                operator,
                left.scaled,
                left.valid,
                left.unknown,
                right.scaled,
                right.valid,
                right.unknown,
            );
        }
        match left_type {
            ValueType::Int => {
                if !matches!(right_type, ValueType::Int) {
                    return Err("mixed numeric comparison is outside the solver fragment".into());
                }
                let left = self.translate_int(left, receivers)?;
                let right = self.translate_int(right, receivers)?;
                Ok(numeric_comparison(
                    operator,
                    left.value,
                    left.valid,
                    left.unknown,
                    right.value,
                    right.valid,
                    right.unknown,
                )?)
            }
            ValueType::Bool => {
                if !matches!(operator, BinaryOp::Equal | BinaryOp::NotEqual) {
                    return Err("ordered Bool comparison is not supported".into());
                }
                let left = self.translate_bool(left, receivers)?;
                let right = self.translate_bool(right, receivers)?;
                let (unknown, conflict) = combined_value_status(
                    left.unknown.clone(),
                    left.conflict.clone(),
                    right.unknown.clone(),
                    right.conflict.clone(),
                );
                let valid = bool_or(vec![unknown.clone(), conflict.clone()]).not();
                let equal = Ast::eq(&left.truth, right.truth);
                let truth = if operator == BinaryOp::Equal {
                    equal
                } else {
                    equal.not()
                };
                Ok(BooleanTerm {
                    truth: bool_and(valid.clone(), truth),
                    unknown,
                    conflict,
                })
            }
            ValueType::Enum(type_name) => {
                if !matches!(operator, BinaryOp::Equal | BinaryOp::NotEqual) {
                    return Err("ordered enum comparison is not supported".into());
                }
                let left = self.translate_enum(left, receivers, type_name)?;
                let right = self.translate_enum(right, receivers, type_name)?;
                let left_conflict = bool_and(left.valid.clone().not(), left.unknown.clone().not());
                let right_conflict =
                    bool_and(right.valid.clone().not(), right.unknown.clone().not());
                let (unknown, conflict) = combined_value_status(
                    left.unknown,
                    left_conflict,
                    right.unknown,
                    right_conflict,
                );
                let valid = bool_or(vec![unknown.clone(), conflict.clone()]).not();
                let equal = Ast::eq(&left.value, right.value);
                let truth = if operator == BinaryOp::Equal {
                    equal
                } else {
                    equal.not()
                };
                Ok(BooleanTerm {
                    truth: bool_and(valid.clone(), truth),
                    unknown,
                    conflict,
                })
            }
            ValueType::Date => {
                let left = self.translate_date(left, receivers)?;
                let right = self.translate_date(right, receivers)?;
                numeric_comparison(
                    operator,
                    left.value,
                    left.valid,
                    left.unknown,
                    right.value,
                    right.valid,
                    right.unknown,
                )
            }
            ValueType::Decimal => unreachable!("Decimal comparisons return above"),
            ValueType::String
            | ValueType::Duration
            | ValueType::Entity(_)
            | ValueType::Unknown
            | ValueType::Error => {
                Err("comparison type is outside the solver arithmetic fragment".into())
            }
        }
    }

    /// Prove totality of small finite numeric expressions without asking Z3
    /// to rediscover every exact Decimal operation through nonlinear modular
    /// arithmetic. The sets deliberately over-approximate correlations between
    /// repeated fields; accepting only when every cross-product result is exact
    /// therefore remains sound.
    fn finite_int_values(
        &self,
        expression: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Option<BTreeSet<i64>> {
        if !matches!(
            self.program.type_of_span(expression.span),
            Some(ValueType::Int)
        ) {
            return None;
        }
        match &expression.kind {
            ExprKind::Literal(Literal::Number(NumericLiteral::Int(value))) => {
                Some(BTreeSet::from([*value]))
            }
            ExprKind::Field { .. } => {
                let (_, field) = self.direct_field(expression, receivers).ok()?;
                if field.optional || field.ty != TypeRef::Int {
                    return None;
                }
                if let Some(domain) = &field.domain {
                    let mut values = BTreeSet::new();
                    for expression in &domain.values {
                        let Value::Int(value) =
                            constant_value(self.program, expression, Some(&TypeRef::Int)).ok()?
                        else {
                            return None;
                        };
                        values.insert(value);
                    }
                    return (values.len() <= FINITE_ARITHMETIC_VALUE_LIMIT).then_some(values);
                }
                let (lower, upper) = int_bounds(field).ok()?;
                let count = i128::from(upper)
                    .checked_sub(i128::from(lower))?
                    .checked_add(1)?;
                if count < 0 || usize::try_from(count).ok()? > FINITE_ARITHMETIC_VALUE_LIMIT {
                    return None;
                }
                Some((lower..=upper).collect())
            }
            ExprKind::Unary {
                operator: UnaryOp::Negate,
                operand,
            } => {
                let mut values = BTreeSet::new();
                for value in self.finite_int_values(operand, receivers)? {
                    values.insert(value.checked_neg()?);
                }
                Some(values)
            }
            ExprKind::Binary {
                left,
                operator: operator @ (BinaryOp::Add | BinaryOp::Subtract | BinaryOp::Multiply),
                right,
            } => self.finite_int_binary_values(left, *operator, right, receivers),
            ExprKind::Call {
                callee, arguments, ..
            } => match normalize_name(&callee.value).as_str() {
                "min" | "max" => {
                    let [left, right] = arguments.as_slice() else {
                        return None;
                    };
                    let left_values = self.finite_int_values(left, receivers)?;
                    let right_values = self.finite_int_values(right, receivers)?;
                    if left_values.len().checked_mul(right_values.len())?
                        > FINITE_ARITHMETIC_VALUE_LIMIT
                    {
                        return None;
                    }
                    let is_max = normalize_name(&callee.value) == "max";
                    let mut values = BTreeSet::new();
                    for left in &left_values {
                        for right in &right_values {
                            values.insert(if is_max {
                                (*left).max(*right)
                            } else {
                                (*left).min(*right)
                            });
                        }
                    }
                    Some(values)
                }
                "abs" => {
                    let [argument] = arguments.as_slice() else {
                        return None;
                    };
                    let mut values = BTreeSet::new();
                    for value in self.finite_int_values(argument, receivers)? {
                        values.insert(value.checked_abs()?);
                    }
                    Some(values)
                }
                _ => {
                    let (expression, derive_receivers) = self
                        .inline_entity_derive(&callee.value, arguments, receivers)
                        .ok()?;
                    self.finite_int_values(&expression, &derive_receivers)
                }
            },
            _ => None,
        }
    }

    fn finite_int_binary_values(
        &self,
        left: &Expr,
        operator: BinaryOp,
        right: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Option<BTreeSet<i64>> {
        let left_values = self.finite_int_values(left, receivers)?;
        let right_values = self.finite_int_values(right, receivers)?;
        if left_values.len().checked_mul(right_values.len())? > FINITE_ARITHMETIC_VALUE_LIMIT {
            return None;
        }
        let mut values = BTreeSet::new();
        for left in &left_values {
            for right in &right_values {
                let value = match operator {
                    BinaryOp::Add => left.checked_add(*right),
                    BinaryOp::Subtract => left.checked_sub(*right),
                    BinaryOp::Multiply => left.checked_mul(*right),
                    _ => return None,
                }?;
                values.insert(value);
                if values.len() > FINITE_ARITHMETIC_VALUE_LIMIT {
                    return None;
                }
            }
        }
        Some(values)
    }

    fn finite_decimal_values(
        &self,
        expression: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Option<BTreeSet<Decimal>> {
        if matches!(
            self.program.type_of_span(expression.span),
            Some(ValueType::Int)
        ) {
            return self
                .finite_int_values(expression, receivers)
                .map(|values| values.into_iter().map(Decimal::from).collect());
        }
        if !matches!(
            self.program.type_of_span(expression.span),
            Some(ValueType::Decimal)
        ) {
            return None;
        }
        match &expression.kind {
            ExprKind::Literal(Literal::Number(value)) => {
                Some(BTreeSet::from([numeric_decimal(value)?]))
            }
            ExprKind::Field { .. } => {
                let (_, field) = self.direct_field(expression, receivers).ok()?;
                if field.optional || field.ty != TypeRef::Decimal {
                    return None;
                }
                if let Some(domain) = &field.domain {
                    let mut values = BTreeSet::new();
                    for expression in &domain.values {
                        let value =
                            constant_value(self.program, expression, Some(&TypeRef::Decimal))
                                .ok()?;
                        let value = match value {
                            Value::Decimal(value) => value,
                            Value::Int(value) => Decimal::from(value),
                            _ => return None,
                        };
                        values.insert(value);
                    }
                    return (values.len() <= FINITE_ARITHMETIC_VALUE_LIMIT).then_some(values);
                }
                let range = field.range.as_ref()?;
                let (lower, upper) = effective_decimal_range_bounds(range)?;
                (lower == upper).then(|| BTreeSet::from([lower]))
            }
            ExprKind::Unary {
                operator: UnaryOp::Negate,
                operand,
            } => {
                let mut values = BTreeSet::new();
                for value in self.finite_decimal_values(operand, receivers)? {
                    values.insert(checked_decimal_sub(Decimal::ZERO, value).ok()?);
                }
                Some(values)
            }
            ExprKind::Binary {
                left,
                operator:
                    operator @ (BinaryOp::Add
                    | BinaryOp::Subtract
                    | BinaryOp::Multiply
                    | BinaryOp::Divide),
                right,
            } => self.finite_decimal_binary_values(left, *operator, right, receivers),
            ExprKind::Call {
                callee, arguments, ..
            } => match normalize_name(&callee.value).as_str() {
                "min" | "max" => {
                    let [left, right] = arguments.as_slice() else {
                        return None;
                    };
                    let left_values = self.finite_decimal_values(left, receivers)?;
                    let right_values = self.finite_decimal_values(right, receivers)?;
                    if left_values.len().checked_mul(right_values.len())?
                        > FINITE_ARITHMETIC_VALUE_LIMIT
                    {
                        return None;
                    }
                    let is_max = normalize_name(&callee.value) == "max";
                    let mut values = BTreeSet::new();
                    for left in &left_values {
                        for right in &right_values {
                            values.insert(if is_max {
                                (*left).max(*right)
                            } else {
                                (*left).min(*right)
                            });
                        }
                    }
                    Some(values)
                }
                "abs" => {
                    let [argument] = arguments.as_slice() else {
                        return None;
                    };
                    let mut values = BTreeSet::new();
                    for value in self.finite_decimal_values(argument, receivers)? {
                        values.insert(if value < Decimal::ZERO {
                            checked_decimal_sub(Decimal::ZERO, value).ok()?
                        } else {
                            value
                        });
                    }
                    Some(values)
                }
                _ => {
                    let (expression, derive_receivers) = self
                        .inline_entity_derive(&callee.value, arguments, receivers)
                        .ok()?;
                    self.finite_decimal_values(&expression, &derive_receivers)
                }
            },
            _ => None,
        }
    }

    fn finite_decimal_binary_values(
        &self,
        left: &Expr,
        operator: BinaryOp,
        right: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Option<BTreeSet<Decimal>> {
        let left_values = self.finite_decimal_values(left, receivers)?;
        let right_values = self.finite_decimal_values(right, receivers)?;
        if left_values.len().checked_mul(right_values.len())? > FINITE_ARITHMETIC_VALUE_LIMIT {
            return None;
        }
        let mut values = BTreeSet::new();
        for left in &left_values {
            for right in &right_values {
                let value = match operator {
                    BinaryOp::Add => checked_decimal_add(*left, *right),
                    BinaryOp::Subtract => checked_decimal_sub(*left, *right),
                    BinaryOp::Multiply => checked_decimal_mul(*left, *right),
                    BinaryOp::Divide => checked_decimal_div(*left, *right),
                    _ => return None,
                }
                .ok()?;
                values.insert(value);
                if values.len() > FINITE_ARITHMETIC_VALUE_LIMIT {
                    return None;
                }
            }
        }
        Some(values)
    }

    fn translate_scaled_numeric(
        &mut self,
        expression: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Result<DecimalTerm, String> {
        match self.program.type_of_span(expression.span) {
            Some(ValueType::Int) => {
                let value = self.translate_int(expression, receivers)?;
                let scale = power_of_ten(Decimal::MAX_SCALE);
                Ok(DecimalTerm {
                    scaled: Int::mul(&[&value.value, &scale]),
                    valid: value.valid,
                    unknown: value.unknown,
                })
            }
            Some(ValueType::Decimal) => self.translate_decimal(expression, receivers),
            _ => Err("expected an Int or Decimal expression".into()),
        }
    }

    fn translate_decimal(
        &mut self,
        expression: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Result<DecimalTerm, String> {
        match &expression.kind {
            ExprKind::Literal(Literal::Number(value)) => numeric_decimal(value)
                .map(|value| DecimalTerm {
                    scaled: decimal_scaled_numeral(value),
                    valid: bool_lit(true),
                    unknown: bool_lit(false),
                })
                .ok_or_else(|| "invalid Decimal literal in solver expression".into()),
            ExprKind::Field { .. } => {
                let (key, field) = self.direct_field(expression, receivers)?;
                if field.ty != TypeRef::Decimal {
                    return Err(format!(
                        "field `{}.{}` is not Decimal",
                        key.binding, key.field
                    ));
                }
                match self.symbols.get(&key) {
                    Some(SymbolInfo::Decimal {
                        scaled, present, ..
                    }) => Ok(DecimalTerm {
                        scaled: scaled.clone(),
                        valid: present.clone(),
                        unknown: present.clone().not(),
                    }),
                    _ => Err(self.missing_symbol_reason(&key, field, "Decimal")),
                }
            }
            ExprKind::Unary {
                operator: UnaryOp::Negate,
                operand,
            } => {
                let operand = self.translate_scaled_numeric(operand, receivers)?;
                Ok(DecimalTerm {
                    scaled: operand.scaled.unary_minus(),
                    valid: operand.valid,
                    unknown: operand.unknown,
                })
            }
            ExprKind::Call {
                callee, arguments, ..
            } => match normalize_name(&callee.value).as_str() {
                "min" | "max" => {
                    self.translate_decimal_min_max(&callee.value, arguments, receivers)
                }
                "abs" => self.translate_decimal_abs(arguments, receivers),
                _ => self.translate_decimal_derive_call(&callee.value, arguments, receivers),
            },
            ExprKind::Binary {
                left,
                operator:
                    operator @ (BinaryOp::Add
                    | BinaryOp::Subtract
                    | BinaryOp::Multiply
                    | BinaryOp::Divide),
                right,
            } => self.translate_decimal_arithmetic(left, *operator, right, receivers),
            ExprKind::Binary { .. } => {
                Err("unsupported Decimal expression in solver fragment".into())
            }
            _ => Err("unsupported Decimal expression in solver fragment".into()),
        }
    }

    fn translate_decimal_arithmetic(
        &mut self,
        left: &Expr,
        operator: BinaryOp,
        right: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Result<DecimalTerm, String> {
        let left_term = self.translate_scaled_numeric(left, receivers)?;
        let right_term = self.translate_scaled_numeric(right, receivers)?;
        let operands_valid = bool_and(left_term.valid.clone(), right_term.valid.clone());
        let left_conflict = bool_and(
            left_term.valid.clone().not(),
            left_term.unknown.clone().not(),
        );
        let right_conflict = bool_and(
            right_term.valid.clone().not(),
            right_term.unknown.clone().not(),
        );
        let (unknown, _) = combined_value_status(
            left_term.unknown.clone(),
            left_conflict,
            right_term.unknown.clone(),
            right_conflict,
        );
        let scale = power_of_ten(Decimal::MAX_SCALE);
        let (scaled, operation_valid) = match operator {
            BinaryOp::Add => {
                let scaled = Int::add(&[&left_term.scaled, &right_term.scaled]);
                let valid = decimal_representable(&scaled);
                (scaled, valid)
            }
            BinaryOp::Subtract => {
                let scaled = Int::sub(&[&left_term.scaled, &right_term.scaled]);
                let valid = decimal_representable(&scaled);
                (scaled, valid)
            }
            BinaryOp::Multiply => {
                if depends_on_input(left, receivers) && depends_on_input(right, receivers) {
                    self.uses_nonlinear_arithmetic = true;
                }
                let numerator = Int::mul(&[&left_term.scaled, &right_term.scaled]);
                let divisible = Ast::eq(&numerator.modulo(&scale), Int::from_i64(0));
                let scaled = numerator.div(&scale);
                let valid = bool_and(divisible, decimal_representable(&scaled));
                (scaled, valid)
            }
            BinaryOp::Divide => {
                if depends_on_input(right, receivers) {
                    self.uses_nonlinear_arithmetic = true;
                }
                let numerator = Int::mul(&[&left_term.scaled, &scale]);
                let nonzero = Ast::ne(&right_term.scaled, Int::from_i64(0));
                let divisible = Ast::eq(&numerator.modulo(&right_term.scaled), Int::from_i64(0));
                let scaled = numerator.div(&right_term.scaled);
                let valid = bool_and(nonzero, bool_and(divisible, decimal_representable(&scaled)));
                (scaled, valid)
            }
            _ => return Err("expected Decimal arithmetic".into()),
        };
        Ok(DecimalTerm {
            scaled,
            valid: bool_and(operands_valid, operation_valid),
            unknown,
        })
    }

    fn translate_decimal_min_max(
        &mut self,
        callee: &str,
        arguments: &[Expr],
        receivers: &BTreeMap<String, String>,
    ) -> Result<DecimalTerm, String> {
        let [left_expression, right_expression] = arguments else {
            return Err(format!("builtin `{callee}` expects exactly two arguments"));
        };
        let left = self.translate_scaled_numeric(left_expression, receivers)?;
        let right = self.translate_scaled_numeric(right_expression, receivers)?;
        let left_conflict = bool_and(left.valid.clone().not(), left.unknown.clone().not());
        let right_conflict = bool_and(right.valid.clone().not(), right.unknown.clone().not());
        let (unknown, _) = combined_value_status(
            left.unknown.clone(),
            left_conflict,
            right.unknown.clone(),
            right_conflict,
        );
        let select_left = if normalize_name(callee) == "max" {
            left.scaled.ge(&right.scaled)
        } else {
            left.scaled.le(&right.scaled)
        };
        Ok(DecimalTerm {
            scaled: select_left.ite(&left.scaled, &right.scaled),
            valid: bool_and(left.valid, right.valid),
            unknown,
        })
    }

    fn translate_decimal_abs(
        &mut self,
        arguments: &[Expr],
        receivers: &BTreeMap<String, String>,
    ) -> Result<DecimalTerm, String> {
        let [argument] = arguments else {
            return Err("builtin `abs` expects exactly one argument".into());
        };
        let value = self.translate_scaled_numeric(argument, receivers)?;
        let non_negative = value.scaled.ge(Int::from_i64(0));
        let negated = value.scaled.unary_minus();
        Ok(DecimalTerm {
            scaled: non_negative.ite(&value.scaled, &negated),
            valid: value.valid,
            unknown: value.unknown,
        })
    }

    fn translate_int(
        &mut self,
        expression: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Result<IntTerm, String> {
        match &expression.kind {
            ExprKind::Literal(Literal::Number(NumericLiteral::Int(value))) => Ok(IntTerm {
                value: Int::from_i64(*value),
                valid: bool_lit(true),
                unknown: bool_lit(false),
                bounds: Some(Interval {
                    lower: i128::from(*value),
                    upper: i128::from(*value),
                }),
            }),
            ExprKind::Field { .. } => {
                let (key, field) = self.direct_field(expression, receivers)?;
                if field.ty != TypeRef::Int {
                    return Err(format!("field `{}.{}` is not Int", key.binding, key.field));
                }
                let Some(SymbolInfo::Int {
                    expression: symbol,
                    present,
                }) = self.symbols.get(&key)
                else {
                    return Err(self.missing_symbol_reason(&key, field, "Int"));
                };
                let (lower, upper) = int_bounds(field)?;
                Ok(IntTerm {
                    value: symbol.clone(),
                    valid: present.clone(),
                    unknown: present.clone().not(),
                    bounds: Some(Interval {
                        lower: i128::from(lower),
                        upper: i128::from(upper),
                    }),
                })
            }
            ExprKind::Unary {
                operator: UnaryOp::Negate,
                operand,
            } => {
                let value = self.translate_int(operand, receivers)?;
                let bounds = value.bounds.and_then(interval_negate);
                let operation_valid = int_result_valid(&value.value.unary_minus(), bounds);
                Ok(IntTerm {
                    value: value.value.unary_minus(),
                    valid: bool_and(value.valid, operation_valid),
                    unknown: value.unknown,
                    bounds,
                })
            }
            ExprKind::Binary {
                left,
                operator: BinaryOp::Add,
                right,
            } => {
                let left = self.translate_int(left, receivers)?;
                let right = self.translate_int(right, receivers)?;
                let value = Int::add(&[&left.value, &right.value]);
                let bounds = interval_pair(left.bounds, right.bounds, interval_add);
                let unknown = numeric_terms_unknown(&left, &right);
                Ok(IntTerm {
                    valid: bool_and(
                        bool_and(left.valid, right.valid),
                        int_result_valid(&value, bounds),
                    ),
                    value,
                    unknown,
                    bounds,
                })
            }
            ExprKind::Binary {
                left,
                operator: BinaryOp::Subtract,
                right,
            } => {
                let left = self.translate_int(left, receivers)?;
                let right = self.translate_int(right, receivers)?;
                let value = Int::sub(&[&left.value, &right.value]);
                let bounds = interval_pair(left.bounds, right.bounds, interval_subtract);
                let unknown = numeric_terms_unknown(&left, &right);
                Ok(IntTerm {
                    valid: bool_and(
                        bool_and(left.valid, right.valid),
                        int_result_valid(&value, bounds),
                    ),
                    value,
                    unknown,
                    bounds,
                })
            }
            ExprKind::Binary {
                left,
                operator: BinaryOp::Multiply,
                right,
            } => {
                if depends_on_input(left, receivers) && depends_on_input(right, receivers) {
                    self.uses_nonlinear_arithmetic = true;
                }
                let left = self.translate_int(left, receivers)?;
                let right = self.translate_int(right, receivers)?;
                let value = Int::mul(&[&left.value, &right.value]);
                let bounds = interval_pair(left.bounds, right.bounds, interval_multiply);
                let unknown = numeric_terms_unknown(&left, &right);
                Ok(IntTerm {
                    valid: bool_and(
                        bool_and(left.valid, right.valid),
                        int_result_valid(&value, bounds),
                    ),
                    value,
                    unknown,
                    bounds,
                })
            }
            ExprKind::Binary {
                operator: BinaryOp::Divide,
                ..
            } => Err("integer division is outside the exact solver fragment".into()),
            ExprKind::Call {
                callee, arguments, ..
            } => match normalize_name(&callee.value).as_str() {
                "min" | "max" => self.translate_int_min_max(&callee.value, arguments, receivers),
                "abs" => self.translate_int_abs(arguments, receivers),
                _ => self.translate_int_derive_call(&callee.value, arguments, receivers),
            },
            _ => Err("unsupported integer expression in solver fragment".into()),
        }
    }

    fn translate_int_min_max(
        &mut self,
        callee: &str,
        arguments: &[Expr],
        receivers: &BTreeMap<String, String>,
    ) -> Result<IntTerm, String> {
        let [left_expression, right_expression] = arguments else {
            return Err(format!("builtin `{callee}` expects exactly two arguments"));
        };
        // Tess evaluates both arguments before selecting a result.
        let left = self.translate_int(left_expression, receivers)?;
        let right = self.translate_int(right_expression, receivers)?;
        let unknown = numeric_terms_unknown(&left, &right);
        let is_max = normalize_name(callee) == "max";
        let bounds = interval_min_max(left.bounds, right.bounds, is_max);
        let select_left = if is_max {
            left.value.ge(&right.value)
        } else {
            left.value.le(&right.value)
        };
        Ok(IntTerm {
            value: select_left.ite(&left.value, &right.value),
            valid: bool_and(left.valid, right.valid),
            unknown,
            bounds,
        })
    }

    fn translate_int_abs(
        &mut self,
        arguments: &[Expr],
        receivers: &BTreeMap<String, String>,
    ) -> Result<IntTerm, String> {
        let [argument] = arguments else {
            return Err("builtin `abs` expects exactly one argument".into());
        };
        let value = self.translate_int(argument, receivers)?;
        let non_negative = value.value.ge(Int::from_i64(0));
        let bounds = value.bounds.and_then(interval_abs);
        let operation_valid = if value
            .bounds
            .is_some_and(|bounds| bounds.lower > i128::from(i64::MIN))
        {
            bool_lit(true)
        } else {
            Ast::ne(&value.value, Int::from_i64(i64::MIN))
        };
        let negated = value.value.unary_minus();
        Ok(IntTerm {
            value: non_negative.ite(&value.value, &negated),
            valid: bool_and(value.valid, operation_valid),
            unknown: value.unknown,
            bounds,
        })
    }

    fn translate_enum(
        &mut self,
        expression: &Expr,
        receivers: &BTreeMap<String, String>,
        type_name: &str,
    ) -> Result<EnumTerm, String> {
        if matches!(expression.kind, ExprKind::Field { .. }) {
            let (key, field) = self.direct_field(expression, receivers)?;
            return match self.symbols.get(&key) {
                Some(SymbolInfo::Enum {
                    expression,
                    type_name: actual_type,
                    present,
                    ..
                }) if normalize_name(actual_type) == normalize_name(type_name) => Ok(EnumTerm {
                    value: expression.clone(),
                    valid: present.clone(),
                    unknown: present.clone().not(),
                }),
                _ => Err(self.missing_symbol_reason(&key, field, "enum")),
            };
        }
        let value = constant_value(
            self.program,
            expression,
            Some(&TypeRef::Named(type_name.to_owned())),
        )?;
        let Value::Enum { variant, .. } = value else {
            return Err("expected an enum constant".into());
        };
        let declaration = self
            .program
            .enum_decl(type_name)
            .ok_or_else(|| format!("unknown enum `{type_name}`"))?;
        let index = declaration
            .variants
            .iter()
            .position(|candidate| normalize_name(&candidate.value) == normalize_name(&variant))
            .ok_or_else(|| format!("unknown `{type_name}` variant `{variant}`"))?;
        Ok(EnumTerm {
            value: Int::from_u64(index as u64),
            valid: bool_lit(true),
            unknown: bool_lit(false),
        })
    }

    fn translate_date(
        &mut self,
        expression: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Result<DateTerm, String> {
        if matches!(expression.kind, ExprKind::Field { .. }) {
            let (key, field) = self.direct_field(expression, receivers)?;
            if field.ty != TypeRef::Date {
                return Err(format!("field `{}.{}` is not Date", key.binding, key.field));
            }
            return match self.symbols.get(&key) {
                Some(SymbolInfo::Date {
                    expression,
                    present,
                }) => Ok(DateTerm {
                    value: expression.clone(),
                    valid: present.clone(),
                    unknown: present.clone().not(),
                }),
                _ => Err(self.missing_symbol_reason(&key, field, "Date")),
            };
        }

        if let Ok(Value::Date(value)) =
            constant_value(self.program, expression, Some(&TypeRef::Date))
        {
            return Ok(DateTerm {
                value: Int::from_i64(i64::from(value.num_days_from_ce())),
                valid: bool_lit(true),
                unknown: bool_lit(false),
            });
        }

        if let ExprKind::Call {
            callee, arguments, ..
        } = &expression.kind
        {
            return self.translate_date_derive_call(&callee.value, arguments, receivers);
        }

        Err("unsupported Date expression in solver fragment".into())
    }

    fn direct_field<'b>(
        &self,
        expression: &Expr,
        receivers: &BTreeMap<String, String>,
    ) -> Result<(FieldKey, &'b crate::ast::FieldDecl), String>
    where
        'a: 'b,
    {
        let ExprKind::Field {
            receiver, field, ..
        } = &expression.kind
        else {
            return Err("expected a direct field access".into());
        };
        let ExprKind::Name(receiver_name) = &receiver.kind else {
            return Err("indirect field receivers are outside the solver fragment".into());
        };
        let receiver_name = normalize_name(receiver_name);
        let binding = receivers.get(&receiver_name).ok_or_else(|| {
            format!("receiver `{receiver_name}` is not bound to an assertion record parameter")
        })?;
        let entity = self
            .binding_entities
            .get(binding)
            .ok_or_else(|| format!("binding `{binding}` has no assertion record type"))?;
        let declaration = self
            .program
            .field(entity, &field.value)
            .ok_or_else(|| format!("unknown field `{}`", field.value))?;
        Ok((
            FieldKey {
                binding: binding.clone(),
                field: normalize_name(&field.value),
            },
            declaration,
        ))
    }

    fn missing_symbol_reason(
        &self,
        key: &FieldKey,
        field: &crate::ast::FieldDecl,
        kind: &str,
    ) -> String {
        if self.capability == TranslatorCapability::ExternalV2 {
            if field.optional {
                return format!(
                    "optional field `{}.{}` cannot yet be represented by the external SMT schema",
                    key.binding, key.field
                );
            }
            if matches!(field.ty, TypeRef::Date) {
                return format!(
                    "Date field `{}.{}` cannot yet be represented by the external SMT schema",
                    key.binding, key.field
                );
            }
        }
        format!(
            "missing {kind} solver symbol for `{}.{}`",
            key.binding, key.field
        )
    }

    fn inline_entity_derive(
        &self,
        name: &str,
        arguments: &[Expr],
        receivers: &BTreeMap<String, String>,
    ) -> Result<(Expr, BTreeMap<String, String>), String> {
        let inlined = self.prepare_entity_derive(name, arguments, receivers)?;
        let expression = match inlined.body {
            InlinedDeriveBody::Expression(expression) => expression,
            InlinedDeriveBody::Case(_) => {
                return Err(format!(
                    "fn `{name}` has a case body outside finite-value inlining"
                ));
            }
        };
        for argument in &inlined.scalar_arguments {
            let input_dependent = depends_on_input(&argument.expression, receivers);
            if !input_dependent {
                constant_value(
                    self.program,
                    &argument.expression,
                    Some(&argument.parameter_type),
                )
                .map_err(|error| {
                    format!(
                        "fn `{name}` has an eager scalar argument that is not a known constant: {error}"
                    )
                })?;
            } else if scalar_argument_requires_strict_status(self, &argument.expression, receivers)?
                && !argument.strictly_propagated
            {
                return Err(format!(
                    "fn `{name}` has an input-dependent scalar argument whose eager unknown/conflict status cannot be preserved by finite-value inlining"
                ));
            }
        }
        Ok((expression, inlined.receivers))
    }

    fn prepare_entity_derive(
        &self,
        name: &str,
        arguments: &[Expr],
        receivers: &BTreeMap<String, String>,
    ) -> Result<InlinedDerive, String> {
        let derive = self
            .program
            .derive(name)
            .cloned()
            .ok_or_else(|| format!("function `{name}` is outside the solver fragment"))?;
        if derive.parameters.len() != arguments.len() {
            return Err(format!("fn `{name}` has an incompatible argument count"));
        }
        let mut mapped = receivers.clone();
        let mut scalar_substitutions = BTreeMap::new();
        let mut scalar_arguments = Vec::new();
        for (parameter, argument) in derive.parameters.iter().zip(arguments) {
            if self.program.entity(&parameter.ty.value).is_none() {
                let parameter_name = normalize_name(&parameter.name.value);
                scalar_arguments.push(ScalarArgument {
                    parameter_name: parameter_name.clone(),
                    parameter_type: named_type_ref(&parameter.ty.value),
                    expression: argument.clone(),
                    strictly_propagated: derive.body.expressions().any(|expression| {
                        expression_strictly_propagates_name(expression, &parameter_name)
                    }),
                });
                scalar_substitutions.insert(parameter_name, argument.clone());
                continue;
            }
            let ExprKind::Name(argument_name) = &argument.kind else {
                return Err(format!(
                    "fn `{name}` must receive record parameters directly for solver inlining"
                ));
            };
            let binding = receivers
                .get(&normalize_name(argument_name))
                .ok_or_else(|| format!("fn `{name}` argument is not a bound record"))?;
            mapped.insert(normalize_name(&parameter.name.value), binding.clone());
        }
        let body = match derive.body {
            DeriveBody::Expression(expression) => InlinedDeriveBody::Expression(
                substitute_scalar_arguments(&expression, &scalar_substitutions),
            ),
            DeriveBody::Case(case) => InlinedDeriveBody::Case(
                case.branches
                    .into_iter()
                    .map(|branch| InlinedCaseBranch {
                        condition: substitute_scalar_arguments(
                            &branch.condition,
                            &scalar_substitutions,
                        ),
                        value: substitute_scalar_arguments(&branch.value, &scalar_substitutions),
                    })
                    .collect(),
            ),
        };
        Ok(InlinedDerive {
            body,
            receivers: mapped,
            scalar_arguments,
        })
    }

    fn translate_bool_derive_call(
        &mut self,
        name: &str,
        arguments: &[Expr],
        receivers: &BTreeMap<String, String>,
    ) -> Result<BooleanTerm, String> {
        let inlined = self.prepare_entity_derive(name, arguments, receivers)?;
        let eager = self.translate_eager_scalar_status(&inlined.scalar_arguments, receivers)?;
        let body = match &inlined.body {
            InlinedDeriveBody::Expression(expression) => {
                self.translate_bool(expression, &inlined.receivers)?
            }
            InlinedDeriveBody::Case(branches) => {
                self.translate_bool_case(branches, &inlined.receivers)?
            }
        };
        Ok(apply_eager_boolean_status(body, eager))
    }

    fn translate_int_derive_call(
        &mut self,
        name: &str,
        arguments: &[Expr],
        receivers: &BTreeMap<String, String>,
    ) -> Result<IntTerm, String> {
        let inlined = self.prepare_entity_derive(name, arguments, receivers)?;
        let eager = self.translate_eager_scalar_status(&inlined.scalar_arguments, receivers)?;
        let body = match &inlined.body {
            InlinedDeriveBody::Expression(expression) => {
                self.translate_int(expression, &inlined.receivers)?
            }
            InlinedDeriveBody::Case(branches) => {
                self.translate_int_case(branches, &inlined.receivers)?
            }
        };
        let body_status = numeric_value_status(&body.valid, &body.unknown);
        let status = apply_eager_value_status(body_status, eager);
        Ok(IntTerm {
            value: body.value,
            valid: value_status_is_known(&status),
            unknown: status.unknown,
            bounds: body.bounds,
        })
    }

    fn translate_decimal_derive_call(
        &mut self,
        name: &str,
        arguments: &[Expr],
        receivers: &BTreeMap<String, String>,
    ) -> Result<DecimalTerm, String> {
        let inlined = self.prepare_entity_derive(name, arguments, receivers)?;
        let eager = self.translate_eager_scalar_status(&inlined.scalar_arguments, receivers)?;
        let body = match &inlined.body {
            InlinedDeriveBody::Expression(expression) => {
                self.translate_scaled_numeric(expression, &inlined.receivers)?
            }
            InlinedDeriveBody::Case(branches) => {
                self.translate_decimal_case(branches, &inlined.receivers)?
            }
        };
        let body_status = numeric_value_status(&body.valid, &body.unknown);
        let status = apply_eager_value_status(body_status, eager);
        Ok(DecimalTerm {
            scaled: body.scaled,
            valid: value_status_is_known(&status),
            unknown: status.unknown,
        })
    }

    fn translate_date_derive_call(
        &mut self,
        name: &str,
        arguments: &[Expr],
        receivers: &BTreeMap<String, String>,
    ) -> Result<DateTerm, String> {
        let inlined = self.prepare_entity_derive(name, arguments, receivers)?;
        let eager = self.translate_eager_scalar_status(&inlined.scalar_arguments, receivers)?;
        let body = match &inlined.body {
            InlinedDeriveBody::Expression(expression) => {
                self.translate_date(expression, &inlined.receivers)?
            }
            InlinedDeriveBody::Case(branches) => {
                self.translate_date_case(branches, &inlined.receivers)?
            }
        };
        let body_status = numeric_value_status(&body.valid, &body.unknown);
        let status = apply_eager_value_status(body_status, eager);
        Ok(DateTerm {
            value: body.value,
            valid: value_status_is_known(&status),
            unknown: status.unknown,
        })
    }

    fn translate_case_selection(
        &mut self,
        branches: &[InlinedCaseBranch],
        receivers: &BTreeMap<String, String>,
    ) -> Result<CaseSelection, String> {
        if branches.is_empty() {
            return Err("a case body must contain at least one branch".into());
        }
        let conditions = branches
            .iter()
            .map(|branch| self.translate_bool(&branch.condition, receivers))
            .collect::<Result<Vec<_>, _>>()?;
        let any_true = bool_or(
            conditions
                .iter()
                .map(|condition| condition.truth.clone())
                .collect(),
        );
        let any_unknown = bool_or(
            conditions
                .iter()
                .map(|condition| condition.unknown.clone())
                .collect(),
        );
        let any_condition_conflict = bool_or(
            conditions
                .iter()
                .map(|condition| condition.conflict.clone())
                .collect(),
        );
        let mut overlapping_pairs = Vec::new();
        for (index, left) in conditions.iter().enumerate() {
            for right in &conditions[index + 1..] {
                overlapping_pairs.push(bool_and(left.truth.clone(), right.truth.clone()));
            }
        }
        let multiple_true = bool_or(overlapping_pairs);
        let gap = bool_and(any_true.clone().not(), any_unknown.clone().not());
        let conflict = bool_or(vec![any_condition_conflict, multiple_true, gap]);
        let unknown = bool_and(conflict.clone().not(), any_unknown);
        let known = bool_or(vec![conflict.clone(), unknown.clone()]).not();
        let active = conditions
            .into_iter()
            .map(|condition| bool_and(known.clone(), condition.truth))
            .collect();
        Ok(CaseSelection {
            active,
            unknown,
            conflict,
        })
    }

    fn translate_bool_case(
        &mut self,
        branches: &[InlinedCaseBranch],
        receivers: &BTreeMap<String, String>,
    ) -> Result<BooleanTerm, String> {
        let selection = self.translate_case_selection(branches, receivers)?;
        let values = branches
            .iter()
            .map(|branch| self.translate_bool(&branch.value, receivers))
            .collect::<Result<Vec<_>, _>>()?;
        let truth = bool_or(
            selection
                .active
                .iter()
                .zip(&values)
                .map(|(active, value)| bool_and(active.clone(), value.truth.clone()))
                .collect(),
        );
        let value_unknown = bool_or(
            selection
                .active
                .iter()
                .zip(&values)
                .map(|(active, value)| bool_and(active.clone(), value.unknown.clone()))
                .collect(),
        );
        let value_conflict = bool_or(
            selection
                .active
                .iter()
                .zip(values)
                .map(|(active, value)| bool_and(active.clone(), value.conflict))
                .collect(),
        );
        let conflict = bool_or(vec![selection.conflict, value_conflict]);
        let unknown = bool_and(
            conflict.clone().not(),
            bool_or(vec![selection.unknown, value_unknown]),
        );
        Ok(BooleanTerm {
            truth,
            unknown,
            conflict,
        })
    }

    fn translate_int_case(
        &mut self,
        branches: &[InlinedCaseBranch],
        receivers: &BTreeMap<String, String>,
    ) -> Result<IntTerm, String> {
        let selection = self.translate_case_selection(branches, receivers)?;
        let values = branches
            .iter()
            .map(|branch| self.translate_int(&branch.value, receivers))
            .collect::<Result<Vec<_>, _>>()?;
        let mut value = values
            .first()
            .ok_or_else(|| "a case body must contain at least one branch".to_owned())?
            .value
            .clone();
        let mut value_unknowns = Vec::new();
        let mut value_conflicts = Vec::new();
        for (active, branch) in selection.active.iter().zip(&values) {
            value = active.ite(&branch.value, &value);
            let status = numeric_value_status(&branch.valid, &branch.unknown);
            value_unknowns.push(bool_and(active.clone(), status.unknown));
            value_conflicts.push(bool_and(active.clone(), status.conflict));
        }
        let conflict = bool_or(vec![selection.conflict, bool_or(value_conflicts)]);
        let unknown = bool_and(
            conflict.clone().not(),
            bool_or(vec![selection.unknown, bool_or(value_unknowns)]),
        );
        Ok(IntTerm {
            value,
            valid: bool_or(vec![unknown.clone(), conflict]).not(),
            unknown,
            bounds: None,
        })
    }

    fn translate_decimal_case(
        &mut self,
        branches: &[InlinedCaseBranch],
        receivers: &BTreeMap<String, String>,
    ) -> Result<DecimalTerm, String> {
        let selection = self.translate_case_selection(branches, receivers)?;
        let values = branches
            .iter()
            .map(|branch| self.translate_scaled_numeric(&branch.value, receivers))
            .collect::<Result<Vec<_>, _>>()?;
        let mut scaled = values
            .first()
            .ok_or_else(|| "a case body must contain at least one branch".to_owned())?
            .scaled
            .clone();
        let mut value_unknowns = Vec::new();
        let mut value_conflicts = Vec::new();
        for (active, branch) in selection.active.iter().zip(&values) {
            scaled = active.ite(&branch.scaled, &scaled);
            let status = numeric_value_status(&branch.valid, &branch.unknown);
            value_unknowns.push(bool_and(active.clone(), status.unknown));
            value_conflicts.push(bool_and(active.clone(), status.conflict));
        }
        let conflict = bool_or(vec![selection.conflict, bool_or(value_conflicts)]);
        let unknown = bool_and(
            conflict.clone().not(),
            bool_or(vec![selection.unknown, bool_or(value_unknowns)]),
        );
        Ok(DecimalTerm {
            scaled,
            valid: bool_or(vec![unknown.clone(), conflict]).not(),
            unknown,
        })
    }

    fn translate_date_case(
        &mut self,
        branches: &[InlinedCaseBranch],
        receivers: &BTreeMap<String, String>,
    ) -> Result<DateTerm, String> {
        let selection = self.translate_case_selection(branches, receivers)?;
        let values = branches
            .iter()
            .map(|branch| self.translate_date(&branch.value, receivers))
            .collect::<Result<Vec<_>, _>>()?;
        let mut value = values
            .first()
            .ok_or_else(|| "a case body must contain at least one branch".to_owned())?
            .value
            .clone();
        let mut value_unknowns = Vec::new();
        let mut value_conflicts = Vec::new();
        for (active, branch) in selection.active.iter().zip(&values) {
            value = active.ite(&branch.value, &value);
            let status = numeric_value_status(&branch.valid, &branch.unknown);
            value_unknowns.push(bool_and(active.clone(), status.unknown));
            value_conflicts.push(bool_and(active.clone(), status.conflict));
        }
        let conflict = bool_or(vec![selection.conflict, bool_or(value_conflicts)]);
        let unknown = bool_and(
            conflict.clone().not(),
            bool_or(vec![selection.unknown, bool_or(value_unknowns)]),
        );
        Ok(DateTerm {
            value,
            valid: bool_or(vec![unknown.clone(), conflict]).not(),
            unknown,
        })
    }

    fn translate_eager_scalar_status(
        &mut self,
        arguments: &[ScalarArgument],
        receivers: &BTreeMap<String, String>,
    ) -> Result<ValueStatus, String> {
        let mut reachable = bool_lit(true);
        let mut unknowns = Vec::new();
        let mut conflicts = Vec::new();
        for argument in arguments {
            let status = self.translate_scalar_argument_status(argument, receivers)?;
            unknowns.push(bool_and(reachable.clone(), status.unknown.clone()));
            conflicts.push(bool_and(reachable.clone(), status.conflict.clone()));
            reachable = bool_and(
                reachable,
                bool_or(vec![status.unknown, status.conflict]).not(),
            );
        }
        Ok(ValueStatus {
            unknown: bool_or(unknowns),
            conflict: bool_or(conflicts),
        })
    }

    fn translate_scalar_argument_status(
        &mut self,
        argument: &ScalarArgument,
        receivers: &BTreeMap<String, String>,
    ) -> Result<ValueStatus, String> {
        if matches!(
            argument.expression.kind,
            ExprKind::Literal(Literal::Unknown)
        ) {
            return Ok(ValueStatus {
                unknown: bool_lit(true),
                conflict: bool_lit(false),
            });
        }
        match &argument.parameter_type {
            TypeRef::Bool => {
                let value = self.translate_bool(&argument.expression, receivers)?;
                Ok(ValueStatus {
                    unknown: value.unknown,
                    conflict: value.conflict,
                })
            }
            TypeRef::Int => {
                let value = self.translate_int(&argument.expression, receivers)?;
                Ok(numeric_value_status(&value.valid, &value.unknown))
            }
            TypeRef::Decimal => {
                let value = self.translate_scaled_numeric(&argument.expression, receivers)?;
                Ok(numeric_value_status(&value.valid, &value.unknown))
            }
            TypeRef::Named(type_name) if self.program.enum_decl(type_name).is_some() => {
                let value = self.translate_enum(&argument.expression, receivers, type_name)?;
                Ok(numeric_value_status(&value.valid, &value.unknown))
            }
            TypeRef::Date => {
                let value = self.translate_date(&argument.expression, receivers)?;
                Ok(numeric_value_status(&value.valid, &value.unknown))
            }
            parameter_type => {
                constant_value(self.program, &argument.expression, Some(parameter_type))
                    .map(|_| ValueStatus {
                        unknown: bool_lit(false),
                        conflict: bool_lit(false),
                    })
                    .map_err(|error| {
                        format!(
                            "fn scalar argument `{}` is outside exact eager evaluation: {error}",
                            argument.parameter_name
                        )
                    })
            }
        }
    }

    fn materialize_input(&self) -> Result<Input, String> {
        let solver_model = self
            .solver
            .get_model()
            .ok_or_else(|| "Z3 did not return a model".to_owned())?;
        let mut model = BTreeMap::new();
        for (key, symbol) in &self.symbols {
            let present = solver_model
                .eval(symbol.present(), true)
                .and_then(|value| value.as_bool())
                .ok_or_else(|| "solver returned a non-Bool presence value".to_owned())?;
            if !present {
                continue;
            }
            let value = match symbol {
                SymbolInfo::Presence { .. } => {
                    let entity = self.binding_entities.get(&key.binding).ok_or_else(|| {
                        format!(
                            "solver presence symbol `{}.{}` has no assertion record",
                            key.binding, key.field
                        )
                    })?;
                    let field = self.program.field(entity, &key.field).ok_or_else(|| {
                        format!(
                            "solver presence symbol `{}.{}` has no compiled field",
                            key.binding, key.field
                        )
                    })?;
                    default_field_value(self.program, field)?
                }
                SymbolInfo::Bool { expression, .. } => Value::Bool(
                    solver_model
                        .eval(expression, true)
                        .and_then(|value| value.as_bool())
                        .ok_or_else(|| "solver returned a non-Bool model value".to_owned())?,
                ),
                SymbolInfo::Int { expression, .. } => Value::Int(
                    solver_model
                        .eval(expression, true)
                        .and_then(|value| value.as_i64())
                        .ok_or_else(|| "solver returned an out-of-range Int".to_owned())?,
                ),
                SymbolInfo::Decimal {
                    mantissa, scale, ..
                } => {
                    let mantissa = solver_model
                        .eval(mantissa, true)
                        .ok_or_else(|| "solver omitted a Decimal mantissa".to_owned())?;
                    let mantissa = z3_int_i128(&mantissa)
                        .ok_or_else(|| "solver returned an invalid Decimal mantissa".to_owned())?;
                    let scale = solver_model
                        .eval(scale, true)
                        .and_then(|value| value.as_u64())
                        .and_then(|value| u32::try_from(value).ok())
                        .filter(|value| *value <= Decimal::MAX_SCALE)
                        .ok_or_else(|| "solver returned an invalid Decimal scale".to_owned())?;
                    let value = Decimal::try_from_i128_with_scale(mantissa, scale)
                        .map_err(|error| format!("solver Decimal is not representable: {error}"))?;
                    Value::decimal(value)
                }
                SymbolInfo::Enum {
                    expression,
                    type_name,
                    variants,
                    ..
                } => {
                    let index = solver_model
                        .eval(expression, true)
                        .and_then(|value| value.as_u64())
                        .and_then(|value| usize::try_from(value).ok())
                        .filter(|index| *index < variants.len())
                        .ok_or_else(|| "solver returned an invalid enum index".to_owned())?;
                    Value::Enum {
                        type_name: type_name.clone(),
                        variant: variants[index].clone(),
                    }
                }
                SymbolInfo::Date { expression, .. } => {
                    let days = solver_model
                        .eval(expression, true)
                        .and_then(|value| value.as_i64())
                        .and_then(|value| i32::try_from(value).ok())
                        .ok_or_else(|| "solver returned an invalid Date ordinal".to_owned())?;
                    Value::Date(
                        NaiveDate::from_num_days_from_ce_opt(days)
                            .ok_or_else(|| "solver returned an out-of-range Date".to_owned())?,
                    )
                }
            };
            model.insert(key.clone(), value);
        }

        let mut input = Input::new();
        for variable in &self.invariant.variables {
            let binding = normalize_name(&variable.name.value);
            let entity = self
                .program
                .entity(&variable.ty.value)
                .ok_or_else(|| format!("unknown record `{}`", variable.ty.value))?;
            let mut fields = BTreeMap::new();
            for field in &entity.fields {
                let key = FieldKey {
                    binding: binding.clone(),
                    field: normalize_name(&field.name.value),
                };
                if let Some(value) = model.get(&key) {
                    fields.insert(field.name.value.clone(), value.clone());
                } else if !field.optional {
                    fields.insert(
                        field.name.value.clone(),
                        default_field_value(self.program, field)?,
                    );
                }
            }
            input.insert(&variable.name.value, &variable.ty.value, fields);
        }
        Ok(input)
    }

    fn exported_symbols(&self) -> Result<Vec<SmtSymbol>, String> {
        let mut symbols = self
            .symbols
            .iter()
            .map(|(key, symbol)| {
                let entity = self.binding_entities.get(&key.binding).ok_or_else(|| {
                    format!(
                        "solver symbol `{}.{}` has no assertion record",
                        key.binding, key.field
                    )
                })?;
                let field = self.program.field(entity, &key.field).ok_or_else(|| {
                    format!(
                        "solver symbol `{}.{}` has no compiled field",
                        key.binding, key.field
                    )
                })?;
                if field.optional {
                    return Err(format!(
                        "optional field `{}.{}` cannot yet be represented by the external SMT schema",
                        key.binding, key.field
                    ));
                }
                let encoding = match symbol {
                    SymbolInfo::Presence { .. } => {
                        return Err(format!(
                            "presence-only field `{}.{}` cannot be represented by the external SMT schema",
                            key.binding, key.field
                        ));
                    }
                    SymbolInfo::Bool { expression, .. } => SmtSymbolEncoding::Bool {
                        symbol: expression.to_string(),
                    },
                    SymbolInfo::Int { expression, .. } => SmtSymbolEncoding::Int {
                        symbol: expression.to_string(),
                    },
                    SymbolInfo::Decimal {
                        mantissa, scale, ..
                    } => SmtSymbolEncoding::DecimalMantissaScale {
                        mantissa_symbol: mantissa.to_string(),
                        scale_symbol: scale.to_string(),
                        canonical_scale: Decimal::MAX_SCALE,
                    },
                    SymbolInfo::Enum {
                        expression,
                        type_name,
                        variants,
                        ..
                    } => SmtSymbolEncoding::EnumIndex {
                        symbol: expression.to_string(),
                        type_name: type_name.clone(),
                        variants: variants.clone(),
                    },
                    SymbolInfo::Date { .. } => {
                        return Err(format!(
                            "Date field `{}.{}` cannot yet be represented by the external SMT schema",
                            key.binding, key.field
                        ));
                    }
                };
                Ok(SmtSymbol {
                    binding: key.binding.clone(),
                    entity: entity.clone(),
                    field: key.field.clone(),
                    encoding,
                    source: source_location(self.program, field.span),
                })
            })
            .collect::<Result<Vec<_>, String>>()?;
        symbols.sort_by(|left, right| {
            symbol_ordinal(&left.encoding)
                .cmp(&symbol_ordinal(&right.encoding))
                .then_with(|| left.binding.cmp(&right.binding))
                .then_with(|| left.field.cmp(&right.field))
        });
        Ok(symbols)
    }
}

/// Export one exact assertion query without invoking a solver.
pub(crate) fn export_invariant_smtlib(
    program: &CompiledProgram,
    invariant_name: &str,
) -> Result<SmtLibQuery, SmtLibExportError> {
    let invariant =
        program
            .invariant(invariant_name)
            .ok_or_else(|| SmtLibExportError::UnknownInvariant {
                invariant: invariant_name.to_owned(),
            })?;
    let solver = Solver::new();
    let mut translator =
        Translator::new_for_external_export(program, invariant, &solver).map_err(|reason| {
            SmtLibExportError::Unsupported {
                invariant: invariant.name.value.clone(),
                reason,
            }
        })?;
    let query_formula =
        translator
            .query_formula()
            .map_err(|reason| SmtLibExportError::Unsupported {
                invariant: invariant.name.value.clone(),
                reason,
            })?;
    let logic = if translator.uses_nonlinear_arithmetic {
        "QF_NIA"
    } else {
        "QF_LIA"
    };
    let symbols =
        translator
            .exported_symbols()
            .map_err(|reason| SmtLibExportError::Unsupported {
                invariant: invariant.name.value.clone(),
                reason,
            })?;
    solver.assert(query_formula);
    let serialized = solver.to_smt2();
    if serialized.trim().is_empty() {
        return Err(SmtLibExportError::Unsupported {
            invariant: invariant.name.value.clone(),
            reason: "Z3 could not serialize the translated query as SMT-LIB2".into(),
        });
    }
    let query_kind = match invariant.quantifier {
        InvariantQuantifier::All => "invariant_violation",
        InvariantQuantifier::Some => "invariant_witness",
    };
    let script = render_smtlib_script(
        &invariant.name.value,
        logic,
        query_kind,
        &symbols,
        &serialized,
    );
    Ok(SmtLibQuery {
        invariant: invariant.name.value.clone(),
        source: source_location(program, invariant.span),
        metadata: SmtLibMetadata {
            schema_version: SMTLIB_QUERY_SCHEMA_VERSION.into(),
            generator: "tess".into(),
            generator_version: env!("CARGO_PKG_VERSION").into(),
            logic: logic.into(),
            query: query_kind.into(),
        },
        symbols,
        script,
    })
}

/// Attempt an exact universal proof/counterexample or existential witness/refutation.
pub(crate) fn solve_invariant(
    program: &CompiledProgram,
    invariant: &InvariantDecl,
    mode: SolverMode,
) -> SolverOutcome {
    if mode == SolverMode::Off {
        return SolverOutcome::Unavailable("embedded solver use is disabled".into());
    }
    let solver = Solver::new();
    let mut params = Params::new();
    params.set_u32("timeout", Z3_TIMEOUT_MS);
    solver.set_params(&params);
    let mut translator = match Translator::new(program, invariant, &solver) {
        Ok(translator) => translator,
        Err(error) => return SolverOutcome::Unsupported(error),
    };
    let query_formula = match translator.query_formula() {
        Ok(query_formula) => query_formula,
        Err(error) => return SolverOutcome::Unsupported(error),
    };
    let metadata = SolverMetadata {
        backend: "z3".into(),
        version: full_version().to_owned(),
        logic: if translator.uses_nonlinear_arithmetic {
            "QF_NIA".into()
        } else {
            "QF_LIA".into()
        },
    };
    solver.assert(&query_formula);
    match (invariant.quantifier, solver.check()) {
        (InvariantQuantifier::All, SatResult::Unsat) => SolverOutcome::Proved(metadata),
        (InvariantQuantifier::All, SatResult::Sat) => match translator.materialize_input() {
            Ok(input) => SolverOutcome::Counterexample { input, metadata },
            Err(error) => SolverOutcome::Unknown(error),
        },
        (InvariantQuantifier::Some, SatResult::Unsat) => SolverOutcome::Refuted(metadata),
        (InvariantQuantifier::Some, SatResult::Sat) => match translator.materialize_input() {
            Ok(input) => SolverOutcome::Witness { input, metadata },
            Err(error) => SolverOutcome::Unknown(error),
        },
        (_, SatResult::Unknown) => SolverOutcome::Unknown(
            solver
                .get_reason_unknown()
                .unwrap_or_else(|| "Z3 returned unknown or reached its timeout".to_owned()),
        ),
    }
}

fn render_smtlib_script(
    invariant: &str,
    logic: &str,
    query_kind: &str,
    symbols: &[SmtSymbol],
    body: &str,
) -> String {
    let invariant = smt_comment_value(invariant);
    let body = canonicalize_z3_local_names(body.trim_start());
    let mut output = String::new();
    writeln!(output, "; Tess SMT-LIB query").expect("writing to a String cannot fail");
    writeln!(output, "; schema: {SMTLIB_QUERY_SCHEMA_VERSION}")
        .expect("writing to a String cannot fail");
    writeln!(output, "; generator: tess {}", env!("CARGO_PKG_VERSION"))
        .expect("writing to a String cannot fail");
    writeln!(output, "; assertion: {invariant}").expect("writing to a String cannot fail");
    let semantics = match query_kind {
        "invariant_violation" => "sat means assertion violation",
        "invariant_witness" => "sat means assertion witness",
        _ => "sat means query target is reachable",
    };
    writeln!(output, "; semantics: {semantics}").expect("writing to a String cannot fail");
    for symbol in symbols {
        writeln!(
            output,
            "; symbol: {} -> {}.{} ({}.{}) @ {}:{}:{}",
            encoding_symbol_names(&symbol.encoding),
            smt_comment_value(&symbol.binding),
            smt_comment_value(&symbol.field),
            smt_comment_value(&symbol.entity),
            smt_comment_value(&symbol.field),
            smt_comment_value(&symbol.source.file),
            symbol.source.line,
            symbol.source.column
        )
        .expect("writing to a String cannot fail");
    }
    writeln!(output, "(set-logic {logic})").expect("writing to a String cannot fail");
    output.push_str(&body);
    output
}

fn encoding_symbol_names(encoding: &SmtSymbolEncoding) -> String {
    match encoding {
        SmtSymbolEncoding::Bool { symbol }
        | SmtSymbolEncoding::Int { symbol }
        | SmtSymbolEncoding::EnumIndex { symbol, .. } => symbol.clone(),
        SmtSymbolEncoding::DecimalMantissaScale {
            mantissa_symbol,
            scale_symbol,
            ..
        } => format!("{mantissa_symbol},{scale_symbol}"),
    }
}

/// Z3's serializer names shared local terms from process-global AST ids (for
/// example `$x42`). Renaming those let-bound identifiers in first-use order
/// makes otherwise identical queries byte-for-byte reproducible.
fn canonicalize_z3_local_names(body: &str) -> String {
    let bytes = body.as_bytes();
    let mut names = BTreeMap::<String, String>::new();
    let mut output = String::with_capacity(body.len());
    let mut cursor = 0;
    while cursor < bytes.len() {
        if bytes[cursor] == b'$' && bytes.get(cursor + 1) == Some(&b'x') {
            let mut end = cursor + 2;
            while bytes.get(end).is_some_and(u8::is_ascii_digit) {
                end += 1;
            }
            if end > cursor + 2 {
                let original = &body[cursor..end];
                let next_index = names.len();
                let canonical = names
                    .entry(original.to_owned())
                    .or_insert_with(|| format!("$t{next_index}"));
                output.push_str(canonical);
                cursor = end;
                continue;
            }
        }
        let character = body[cursor..]
            .chars()
            .next()
            .expect("cursor is within the string");
        output.push(character);
        cursor += character.len_utf8();
    }
    output
}

fn smt_comment_value(value: &str) -> String {
    value.replace(['\r', '\n'], " ")
}

fn source_location(program: &CompiledProgram, span: crate::source::Span) -> SmtSourceLocation {
    let source = program.source();
    let (line, column) = source.line_col(span.start);
    SmtSourceLocation {
        file: source.name_at(span.start).to_owned(),
        span: source.local_span(span).unwrap_or(span),
        line,
        column,
    }
}

fn primary_symbol(encoding: &SmtSymbolEncoding) -> &str {
    match encoding {
        SmtSymbolEncoding::Bool { symbol }
        | SmtSymbolEncoding::Int { symbol }
        | SmtSymbolEncoding::EnumIndex { symbol, .. } => symbol,
        SmtSymbolEncoding::DecimalMantissaScale {
            mantissa_symbol, ..
        } => mantissa_symbol,
    }
}

fn symbol_ordinal(encoding: &SmtSymbolEncoding) -> usize {
    let symbol = primary_symbol(encoding);
    let digits = symbol
        .strip_prefix('v')
        .unwrap_or(symbol)
        .chars()
        .take_while(char::is_ascii_digit)
        .collect::<String>();
    digits.parse().unwrap_or(usize::MAX)
}

fn comparison(operator: BinaryOp, left: Int, right: Int) -> Result<Bool, String> {
    Ok(match operator {
        BinaryOp::Equal => Ast::eq(&left, right),
        BinaryOp::NotEqual => Ast::ne(&left, right),
        BinaryOp::Greater => left.gt(right),
        BinaryOp::GreaterEqual => left.ge(right),
        BinaryOp::Less => left.lt(right),
        BinaryOp::LessEqual => left.le(right),
        _ => return Err("expected a comparison operator".into()),
    })
}

fn candidate_values_equal(
    left: &CandidateValueFormula,
    right: &CandidateValueFormula,
) -> Result<Bool, String> {
    match (left, right) {
        (CandidateValueFormula::Concrete(left), CandidateValueFormula::Concrete(right)) => {
            Ok(bool_lit(left == right))
        }
        (CandidateValueFormula::Bool(left), CandidateValueFormula::Bool(right)) => {
            Ok(Ast::eq(left, right))
        }
        (CandidateValueFormula::Int(left), CandidateValueFormula::Int(right))
        | (CandidateValueFormula::Decimal(left), CandidateValueFormula::Decimal(right)) => {
            Ok(Ast::eq(left, right))
        }
        _ => Err("candidate values have incompatible solver representations".into()),
    }
}

fn candidate_equals_value(
    candidate: &CandidateValueFormula,
    expected: &Value,
) -> Result<Bool, String> {
    match (candidate, expected) {
        (CandidateValueFormula::Concrete(candidate), expected) => {
            Ok(bool_lit(candidate == expected))
        }
        (CandidateValueFormula::Bool(candidate), Value::Bool(expected)) => {
            Ok(Ast::eq(candidate, Bool::from_bool(*expected)))
        }
        (CandidateValueFormula::Int(candidate), Value::Int(expected)) => {
            Ok(Ast::eq(candidate, Int::from_i64(*expected)))
        }
        (CandidateValueFormula::Decimal(candidate), Value::Decimal(expected)) => {
            Ok(Ast::eq(candidate, decimal_scaled_numeral(*expected)))
        }
        (CandidateValueFormula::Decimal(candidate), Value::Int(expected)) => Ok(Ast::eq(
            candidate,
            decimal_scaled_numeral(Decimal::from(*expected)),
        )),
        _ => Err("expected value has an incompatible solver representation".into()),
    }
}

fn numeric_comparison(
    operator: BinaryOp,
    left: Int,
    left_valid: Bool,
    left_unknown: Bool,
    right: Int,
    right_valid: Bool,
    right_unknown: Bool,
) -> Result<BooleanTerm, String> {
    let left_conflict = bool_and(left_valid.clone().not(), left_unknown.clone().not());
    let right_conflict = bool_and(right_valid.clone().not(), right_unknown.clone().not());
    let (unknown, conflict) =
        combined_value_status(left_unknown, left_conflict, right_unknown, right_conflict);
    let valid = bool_or(vec![unknown.clone(), conflict.clone()]).not();
    let truth = comparison(operator, left, right)?;
    Ok(BooleanTerm {
        truth: bool_and(valid.clone(), truth),
        unknown,
        conflict,
    })
}

fn boolean_known(truth: Bool) -> BooleanTerm {
    BooleanTerm {
        truth,
        unknown: bool_lit(false),
        conflict: bool_lit(false),
    }
}

fn numeric_value_status(valid: &Bool, unknown: &Bool) -> ValueStatus {
    ValueStatus {
        unknown: unknown.clone(),
        conflict: bool_and(valid.clone().not(), unknown.clone().not()),
    }
}

fn value_status_is_known(status: &ValueStatus) -> Bool {
    bool_or(vec![status.unknown.clone(), status.conflict.clone()]).not()
}

fn apply_eager_value_status(body: ValueStatus, eager: ValueStatus) -> ValueStatus {
    let body_reached = value_status_is_known(&eager);
    ValueStatus {
        unknown: bool_or(vec![
            eager.unknown,
            bool_and(body_reached.clone(), body.unknown),
        ]),
        conflict: bool_or(vec![eager.conflict, bool_and(body_reached, body.conflict)]),
    }
}

fn apply_eager_boolean_status(body: BooleanTerm, eager: ValueStatus) -> BooleanTerm {
    let body_reached = value_status_is_known(&eager);
    let status = apply_eager_value_status(
        ValueStatus {
            unknown: body.unknown,
            conflict: body.conflict,
        },
        eager,
    );
    BooleanTerm {
        truth: bool_and(body_reached, body.truth),
        unknown: status.unknown,
        conflict: status.conflict,
    }
}

fn boolean_not(value: BooleanTerm) -> BooleanTerm {
    let known = bool_or(vec![value.unknown.clone(), value.conflict.clone()]).not();
    BooleanTerm {
        truth: bool_and(known, value.truth.not()),
        unknown: value.unknown,
        conflict: value.conflict,
    }
}

fn boolean_and(left: BooleanTerm, right: BooleanTerm) -> BooleanTerm {
    let left_false = bool_or(vec![
        left.truth.clone(),
        left.unknown.clone(),
        left.conflict.clone(),
    ])
    .not();
    let right_false = bool_or(vec![
        right.truth.clone(),
        right.unknown.clone(),
        right.conflict.clone(),
    ])
    .not();
    let any_false = bool_or(vec![left_false, right_false]);
    let conflict = bool_and(
        any_false.clone().not(),
        bool_or(vec![left.conflict.clone(), right.conflict.clone()]),
    );
    let unknown = bool_and(
        bool_and(any_false.not(), conflict.clone().not()),
        bool_or(vec![left.unknown, right.unknown]),
    );
    BooleanTerm {
        truth: bool_and(left.truth, right.truth),
        unknown,
        conflict,
    }
}

fn boolean_or(left: BooleanTerm, right: BooleanTerm) -> BooleanTerm {
    let any_true = bool_or(vec![left.truth.clone(), right.truth.clone()]);
    let conflict = bool_and(
        any_true.clone().not(),
        bool_or(vec![left.conflict.clone(), right.conflict.clone()]),
    );
    let unknown = bool_and(
        bool_and(any_true.clone().not(), conflict.clone().not()),
        bool_or(vec![left.unknown, right.unknown]),
    );
    BooleanTerm {
        truth: any_true,
        unknown,
        conflict,
    }
}

fn combined_value_status(
    left_unknown: Bool,
    left_conflict: Bool,
    right_unknown: Bool,
    right_conflict: Bool,
) -> (Bool, Bool) {
    let conflict = bool_or(vec![left_conflict, right_conflict]);
    let unknown = bool_and(
        conflict.clone().not(),
        bool_or(vec![left_unknown, right_unknown]),
    );
    (unknown, conflict)
}

fn numeric_terms_unknown(left: &IntTerm, right: &IntTerm) -> Bool {
    let left_conflict = bool_and(left.valid.clone().not(), left.unknown.clone().not());
    let right_conflict = bool_and(right.valid.clone().not(), right.unknown.clone().not());
    combined_value_status(
        left.unknown.clone(),
        left_conflict,
        right.unknown.clone(),
        right_conflict,
    )
    .0
}

fn interval_pair(
    left: Option<Interval>,
    right: Option<Interval>,
    operation: fn(Interval, Interval) -> Option<Interval>,
) -> Option<Interval> {
    operation(left?, right?)
}

fn interval_negate(value: Interval) -> Option<Interval> {
    Some(Interval {
        lower: value.upper.checked_neg()?,
        upper: value.lower.checked_neg()?,
    })
}

fn interval_add(left: Interval, right: Interval) -> Option<Interval> {
    Some(Interval {
        lower: left.lower.checked_add(right.lower)?,
        upper: left.upper.checked_add(right.upper)?,
    })
}

fn interval_subtract(left: Interval, right: Interval) -> Option<Interval> {
    Some(Interval {
        lower: left.lower.checked_sub(right.upper)?,
        upper: left.upper.checked_sub(right.lower)?,
    })
}

fn interval_multiply(left: Interval, right: Interval) -> Option<Interval> {
    let products = [
        left.lower.checked_mul(right.lower)?,
        left.lower.checked_mul(right.upper)?,
        left.upper.checked_mul(right.lower)?,
        left.upper.checked_mul(right.upper)?,
    ];
    Some(Interval {
        lower: *products.iter().min().expect("four products"),
        upper: *products.iter().max().expect("four products"),
    })
}

fn interval_min_max(
    left: Option<Interval>,
    right: Option<Interval>,
    is_max: bool,
) -> Option<Interval> {
    let left = left?;
    let right = right?;
    Some(if is_max {
        Interval {
            lower: left.lower.max(right.lower),
            upper: left.upper.max(right.upper),
        }
    } else {
        Interval {
            lower: left.lower.min(right.lower),
            upper: left.upper.min(right.upper),
        }
    })
}

fn interval_abs(value: Interval) -> Option<Interval> {
    let lower_abs = value.lower.checked_abs()?;
    let upper_abs = value.upper.checked_abs()?;
    Some(Interval {
        lower: if value.lower <= 0 && value.upper >= 0 {
            0
        } else {
            lower_abs.min(upper_abs)
        },
        upper: lower_abs.max(upper_abs),
    })
}

fn int_result_valid(value: &Int, bounds: Option<Interval>) -> Bool {
    if bounds.is_some_and(Interval::within_i64) {
        bool_lit(true)
    } else {
        int_representable(value)
    }
}

fn int_representable(value: &Int) -> Bool {
    bool_and(
        value.ge(Int::from_i64(i64::MIN)),
        value.le(Int::from_i64(i64::MAX)),
    )
}

fn decimal_representable(scaled: &Int) -> Bool {
    let maximum_mantissa = decimal_mantissa_numeral(Decimal::MAX);
    let mut alternatives = Vec::with_capacity((Decimal::MAX_SCALE + 1) as usize);
    for removed_scale in 0..=Decimal::MAX_SCALE {
        let power = power_of_ten(removed_scale);
        let limit = Int::mul(&[&maximum_mantissa, &power]);
        let divisible = Ast::eq(&scaled.modulo(&power), Int::from_i64(0));
        let in_range = bool_and(scaled.ge(limit.unary_minus()), scaled.le(limit));
        alternatives.push(bool_and(divisible, in_range));
    }
    bool_or(alternatives)
}

fn bool_lit(value: bool) -> Bool {
    Bool::from_bool(value)
}

fn bool_and(left: Bool, right: Bool) -> Bool {
    Bool::and(&[left, right])
}

fn bool_or(mut formulas: Vec<Bool>) -> Bool {
    match formulas.len() {
        0 => bool_lit(false),
        1 => formulas.pop().expect("one Boolean formula"),
        _ => Bool::or(&formulas),
    }
}

fn effect_matches_query(
    arguments: &[Expr],
    query: &Query,
    receivers: &BTreeMap<String, String>,
) -> bool {
    arguments.len() == query.arguments.len()
        && arguments
            .iter()
            .zip(&query.arguments)
            .all(|(argument, query_binding)| {
                let ExprKind::Name(parameter) = &argument.kind else {
                    return false;
                };
                receivers.get(&normalize_name(parameter)) == Some(&normalize_name(query_binding))
            })
}

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

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 scalar_argument_requires_strict_status(
    translator: &Translator<'_>,
    expression: &Expr,
    receivers: &BTreeMap<String, String>,
) -> Result<bool, String> {
    Ok(match &expression.kind {
        ExprKind::Literal(Literal::Unknown) => true,
        ExprKind::Literal(_) => false,
        ExprKind::Name(name) => receivers.contains_key(&normalize_name(name)),
        ExprKind::Field { .. } => {
            let (_, field) = translator.direct_field(expression, receivers)?;
            field.optional
        }
        ExprKind::Unary { operator, operand } => {
            scalar_argument_requires_strict_status(translator, operand, receivers)?
                || (*operator == UnaryOp::Negate && depends_on_input(operand, receivers))
        }
        ExprKind::Binary {
            left,
            operator,
            right,
        } => {
            scalar_argument_requires_strict_status(translator, left, receivers)?
                || scalar_argument_requires_strict_status(translator, right, receivers)?
                || (matches!(
                    operator,
                    BinaryOp::Add | BinaryOp::Subtract | BinaryOp::Multiply | BinaryOp::Divide
                ) && (depends_on_input(left, receivers) || depends_on_input(right, receivers)))
        }
        ExprKind::Call { arguments, .. } => {
            // Calls evaluate every argument before entering their body. A
            // nested input-dependent call can therefore fail even when scalar
            // substitution removes its result from the outer derive body.
            let mut strict = depends_on_input(expression, receivers);
            for argument in arguments {
                strict |= scalar_argument_requires_strict_status(translator, argument, receivers)?;
            }
            strict
        }
    })
}

fn expression_strictly_propagates_name(expression: &Expr, name: &str) -> bool {
    match &expression.kind {
        ExprKind::Name(candidate) => normalize_name(candidate) == name,
        ExprKind::Unary { operand, .. } => expression_strictly_propagates_name(operand, name),
        ExprKind::Binary {
            operator: BinaryOp::And | BinaryOp::Or,
            ..
        }
        | ExprKind::Literal(_) => false,
        ExprKind::Binary { left, right, .. } => {
            expression_strictly_propagates_name(left, name)
                || expression_strictly_propagates_name(right, name)
        }
        ExprKind::Call { arguments, .. } => arguments
            .iter()
            .any(|argument| expression_strictly_propagates_name(argument, name)),
        ExprKind::Field { receiver, .. } => expression_strictly_propagates_name(receiver, name),
    }
}

fn substitute_scalar_arguments(expression: &Expr, arguments: &BTreeMap<String, Expr>) -> Expr {
    let argument = match &expression.kind {
        ExprKind::Name(name) => arguments.get(&normalize_name(name)),
        _ => None,
    };
    if let Some(argument) = argument {
        return argument.clone();
    }

    let mut substituted = expression.clone();
    match &mut substituted.kind {
        ExprKind::Field { receiver, .. } => {
            **receiver = substitute_scalar_arguments(receiver, arguments);
        }
        ExprKind::Call {
            arguments: call_arguments,
            ..
        } => {
            for argument in call_arguments {
                *argument = substitute_scalar_arguments(argument, arguments);
            }
        }
        ExprKind::Unary { operand, .. } => {
            **operand = substitute_scalar_arguments(operand, arguments);
        }
        ExprKind::Binary { left, right, .. } => {
            **left = substitute_scalar_arguments(left, arguments);
            **right = substitute_scalar_arguments(right, arguments);
        }
        ExprKind::Literal(_) | ExprKind::Name(_) => {}
    }
    substituted
}

fn int_bounds(field: &crate::ast::FieldDecl) -> Result<(i64, i64), String> {
    let Some(range) = &field.range else {
        return Ok((i64::MIN, i64::MAX));
    };
    effective_int_range_bounds(range).ok_or_else(|| {
        format!(
            "Int field `{}` has invalid or empty bounds",
            field.name.value
        )
    })
}

fn named_type_ref(name: &str) -> TypeRef {
    match normalize_name(name).as_str() {
        "Bool" => TypeRef::Bool,
        "Int" => TypeRef::Int,
        "Decimal" => TypeRef::Decimal,
        "String" => TypeRef::String,
        "Date" => TypeRef::Date,
        "Duration" => TypeRef::Duration,
        _ => TypeRef::Named(name.to_owned()),
    }
}

fn default_field_value(
    program: &CompiledProgram,
    field: &crate::ast::FieldDecl,
) -> Result<Value, String> {
    if let Some(domain) = &field.domain {
        let representative = domain
            .values
            .first()
            .ok_or_else(|| format!("field `{}` has an empty declared domain", field.name.value))?;
        return constant_value(program, representative, Some(&field.ty)).map_err(|error| {
            format!(
                "field `{}` has no valid declared-domain representative: {error}",
                field.name.value
            )
        });
    }
    Ok(match &field.ty {
        TypeRef::Bool => Value::Bool(false),
        TypeRef::Int => {
            let (lower, upper) = int_bounds(field)?;
            Value::Int(lower.max(0).min(upper))
        }
        TypeRef::Decimal => {
            let value = field
                .range
                .as_ref()
                .and_then(effective_decimal_range_bounds)
                .map_or(Decimal::ZERO, |(start, _)| start);
            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(type_name) => {
            let variant = program
                .enum_decl(type_name)
                .and_then(|declaration| declaration.variants.first())
                .ok_or_else(|| format!("field `{}` has no enum values", field.name.value))?;
            Value::Enum {
                type_name: type_name.clone(),
                variant: variant.value.clone(),
            }
        }
        TypeRef::Unknown => {
            return Err(format!(
                "field `{}` has an unresolved type",
                field.name.value
            ));
        }
    })
}

fn power_of_ten(exponent: u32) -> Int {
    let numeral = format!("1{}", "0".repeat(exponent as usize));
    numeral
        .parse()
        .expect("a power of ten is a valid Z3 integer")
}

fn decimal_mantissa_numeral(value: Decimal) -> Int {
    value
        .mantissa()
        .to_string()
        .parse()
        .expect("a Decimal mantissa is a valid Z3 integer")
}

fn decimal_scaled_expression(mantissa: &Int, scale: &Int) -> Int {
    let mut expression = mantissa.clone();
    for candidate_scale in (0..Decimal::MAX_SCALE).rev() {
        let factor = power_of_ten(Decimal::MAX_SCALE - candidate_scale);
        let candidate = Int::mul(&[mantissa, &factor]);
        let selected = Ast::eq(scale, Int::from_u64(u64::from(candidate_scale)));
        expression = selected.ite(&candidate, &expression);
    }
    expression
}

fn decimal_scaled_numeral(value: Decimal) -> Int {
    let value = value.normalize();
    let mantissa = value.mantissa();
    if mantissa == 0 {
        return Int::from_i64(0);
    }
    let mut magnitude = mantissa.unsigned_abs().to_string();
    magnitude.extend(std::iter::repeat_n(
        '0',
        (Decimal::MAX_SCALE - value.scale()) as usize,
    ));
    let numeral = if mantissa.is_negative() {
        format!("-{magnitude}")
    } else {
        magnitude
    };
    numeral
        .parse()
        .expect("a scaled Decimal is a valid Z3 integer")
}

fn z3_int_i128(value: &Int) -> Option<i128> {
    let rendered = value.to_string();
    if let Ok(value) = rendered.parse() {
        return Some(value);
    }
    rendered
        .strip_prefix("(- ")?
        .strip_suffix(')')?
        .parse::<i128>()
        .ok()?
        .checked_neg()
}

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

#[cfg(test)]
mod tests {
    use super::*;
    use crate::SourceFile;
    use crate::analysis::{
        CounterexampleKind, replay_invariant_violation, replay_invariant_witness,
    };

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

    fn solve_and_replay_counterexample(
        program: &CompiledProgram,
        invariant: &str,
    ) -> (Input, CounterexampleKind) {
        let SolverOutcome::Counterexample { input, .. } = solve_invariant(
            program,
            program.invariant(invariant).unwrap(),
            SolverMode::Z3,
        ) else {
            panic!("expected an exact solver counterexample for `{invariant}`")
        };
        let replay = replay_invariant_violation(program, invariant, &input)
            .unwrap()
            .expect("the solver model must replay as a violation");
        (input, replay.kind)
    }

    #[test]
    fn embedded_solver_enforces_choice_tag_and_active_required_members() {
        let program = compile_text(
            r"enum Kind:
    A
    B

record Request:
    choice kind Kind:
        A:
            a: Bool
        B:
            b: Bool

rule selected(request Request):
    request.b: result(request) = O

assert some total(request Request):
    result(request)
",
        );
        let SolverOutcome::Witness { input, .. } = solve_invariant(
            &program,
            program.invariant("total").unwrap(),
            SolverMode::Z3,
        ) else {
            panic!("expected a solver witness");
        };
        let fields = &input.bindings["request"].fields;
        assert!(matches!(
            fields.get("kind"),
            Some(Value::Enum { variant, .. }) if variant == "B"
        ));
        assert_eq!(fields.get("b"), Some(&Value::Bool(true)));
        assert!(!fields.contains_key("a"));
        replay_invariant_witness(&program, "total", &input).unwrap();
    }

    #[test]
    fn embedded_solver_materializes_presence_only_choice_members() {
        let program = compile_text(
            r"enum Kind:
    A
    B

record Request:
    choice kind Kind:
        A:
            note: String
        B:
            delay: Duration?

rule selected(request Request):
    request.kind = A: result(request) = O

assert some total(request Request):
    result(request)
",
        );
        let SolverOutcome::Witness { input, .. } = solve_invariant(
            &program,
            program.invariant("total").unwrap(),
            SolverMode::Z3,
        ) else {
            panic!("expected a solver witness");
        };
        let fields = &input.bindings["request"].fields;
        assert!(matches!(
            fields.get("kind"),
            Some(Value::Enum { variant, .. }) if variant == "A"
        ));
        assert_eq!(fields.get("note"), Some(&Value::String(String::new())));
        assert!(!fields.contains_key("delay"));
        assert!(input.validate(&program).is_empty());
        replay_invariant_witness(&program, "total", &input).unwrap();
    }

    #[test]
    fn external_solver_export_rejects_choice_schema_soundly() {
        let program = compile_text(
            r"enum Kind:
    A

record Request:
    choice kind Kind:
        A:
            value: Bool

rule selected(request Request):
    request.value: result(request) = O

assert total(request Request):
    result(request)
",
        );
        let error = export_invariant_smtlib(&program, "total")
            .expect_err("external schema must not silently drop choice constraints");
        assert!(error.to_string().contains("choice"), "{error}");
    }

    #[test]
    fn embedded_solver_proves_exhaustive_decimal_case_functions_exactly() {
        let program = compile_text(
            r"enum Time:
    Day
    Night

enum Result:
    Yes

record Event:
    time: Time

fn limit(event Event) Decimal:
    case:
        day when event.time = Day: 39.00
        night when event.time = Night: 34.00

rule positive(event Event):
    limit(event) > 0.00: result(event) = Yes

assert total(event Event):
    result(event)
",
        );
        assert!(matches!(
            solve_invariant(
                &program,
                program.invariant("total").unwrap(),
                SolverMode::Z3,
            ),
            SolverOutcome::Proved(_)
        ));
    }

    #[test]
    fn embedded_solver_replays_case_overlap_gap_and_unknown_status() {
        let overlap = compile_text(
            r"enum Result:
    Yes

fn selected Bool:
    case:
        first when O: O
        second when O: O

rule yes:
    selected: result = Yes

assert total:
    result
",
        );
        let (_, kind) = solve_and_replay_counterexample(&overlap, "total");
        assert_eq!(kind, CounterexampleKind::Conflict);

        let gap = compile_text(
            r"enum Result:
    Yes

fn selected Bool:
    case:
        first when X: O
        second when X: O

rule yes:
    selected: result = Yes

assert total:
    result
",
        );
        let (_, kind) = solve_and_replay_counterexample(&gap, "total");
        assert_eq!(kind, CounterexampleKind::Conflict);

        let unknown = compile_text(
            r"enum Result:
    Yes

record Event:
    flag: Bool?

fn selected(event Event) Bool:
    case:
        enabled when event.flag: O
        disabled when event.flag X: O

rule yes(event Event):
    event selected: result(event) = Yes

assert total(event Event):
    result(event)
",
        );
        let (input, kind) = solve_and_replay_counterexample(&unknown, "total");
        assert_eq!(kind, CounterexampleKind::Unknown);
        assert!(!input.bindings["event"].fields.contains_key("flag"));
    }

    #[test]
    fn embedded_solver_keeps_unselected_case_values_lazy() {
        let program = compile_text(
            r"enum Result:
    Yes

fn selected Decimal:
    case:
        live when O: 1.00
        unreachable when X: 1.00 / 0.00

rule yes:
    selected = 1.00: result = Yes

assert total:
    result
",
        );
        assert!(matches!(
            solve_invariant(
                &program,
                program.invariant("total").unwrap(),
                SolverMode::Z3,
            ),
            SolverOutcome::Proved(_)
        ));
    }

    fn intervals() -> Vec<Interval> {
        (-3_i128..=3)
            .flat_map(|lower| (lower..=3).map(move |upper| Interval { lower, upper }))
            .collect()
    }

    #[test]
    fn solver_inlining_preserves_eager_scalar_unknown_and_conflict_status() {
        let program = compile_text(
            r"mod Solver
enum Result:
    Yes
record E:
    flag: Bool?
fn always(value Bool) Bool:
    O
rule yes(e E):
    e.flag always: d(e) = Yes
assert total(e E):
    d(e)
",
        );
        let SolverOutcome::Counterexample { input, .. } = solve_invariant(
            &program,
            program.invariant("total").unwrap(),
            SolverMode::Z3,
        ) else {
            panic!("an eager optional argument must produce an exact unknown counterexample")
        };
        assert!(!input.bindings["e"].fields.contains_key("flag"));

        let date_program = compile_text(
            r"mod Solver
enum Result:
    Yes
record E:
    observed: Date?
fn always(value Date) Bool:
    O
rule yes(e E):
    e.observed always: d(e) = Yes
assert total(e E):
    d(e)
",
        );
        let SolverOutcome::Counterexample { input, .. } = solve_invariant(
            &date_program,
            date_program.invariant("total").unwrap(),
            SolverMode::Z3,
        ) else {
            panic!("an eager optional Date must produce an exact unknown counterexample")
        };
        assert!(!input.bindings["e"].fields.contains_key("observed"));

        let ground_conflict = compile_text(
            r"mod Solver
enum Result:
    Yes
fn always(value Decimal) Bool:
    O
rule yes:
    (1 / 0) always: d = Yes
assert total:
    d
",
        );
        let SolverOutcome::Counterexample { .. } = solve_invariant(
            &ground_conflict,
            ground_conflict.invariant("total").unwrap(),
            SolverMode::Z3,
        ) else {
            panic!("a dropped eager conflict must remain an exact counterexample")
        };
    }

    #[test]
    fn eager_scalar_arguments_preserve_left_to_right_status_priority() {
        let source = |arguments: &str| {
            format!(
                r"mod Solver
enum Result:
    Yes
fn always(first Decimal, second Decimal) Bool:
    O
rule yes:
    always({arguments}): d = Yes
assert total:
    d
"
            )
        };

        let unknown_first = compile_text(&source("unknown, 1 / 0"));
        let (_, kind) = solve_and_replay_counterexample(&unknown_first, "total");
        assert_eq!(kind, CounterexampleKind::Unknown);

        let conflict_first = compile_text(&source("1 / 0, unknown"));
        let (_, kind) = solve_and_replay_counterexample(&conflict_first, "total");
        assert_eq!(kind, CounterexampleKind::Conflict);
    }

    #[test]
    fn nested_scalar_functions_preserve_an_eager_optional_unknown() {
        let program = compile_text(
            r"mod Solver
enum Judgment:
    Accepted
enum Result:
    Yes
record E:
    judgment: Judgment?
fn inner(value Judgment) Bool:
    O
fn outer(value Judgment) Bool:
    value inner
rule yes(e E):
    e.judgment outer: d(e) = Yes
assert total(e E):
    d(e)
",
        );

        let (input, kind) = solve_and_replay_counterexample(&program, "total");
        assert_eq!(kind, CounterexampleKind::Unknown);
        assert!(!input.bindings["e"].fields.contains_key("judgment"));
    }

    #[test]
    fn universal_many_ignores_missing_membership_but_finds_present_arithmetic_conflict() {
        let program = compile_text(
            r"mod Solver
enum Result:
    Yes
record E:
    value: Decimal? [0.00, 1.00]
fn broken(value Decimal) Bool:
    value / 0 > 0
rule invalid(e E):
    e.value broken: d(e) = Yes
assert total(e E):
    d(e)*
",
        );

        let (input, kind) = solve_and_replay_counterexample(&program, "total");
        assert_eq!(kind, CounterexampleKind::Conflict);
        assert!(input.bindings["e"].fields.contains_key("value"));
    }

    #[test]
    fn universal_many_ignores_only_unknown_membership_and_existential_keeps_it() {
        let program = compile_text(
            r"mod Solver
enum Judgment:
    Accepted
    AssumedAccepted
enum Result:
    Yes
record E:
    judgment: Judgment?
fn accepted(value Judgment) Bool:
    value = Accepted | value = AssumedAccepted
rule yes(e E):
    e.judgment accepted: d(e) = Yes
assert many_contract(e E):
    d(e)*
assert some known_witness(e E):
    d(e)*
",
        );

        let SolverOutcome::Proved(_) = solve_invariant(
            &program,
            program.invariant("many_contract").unwrap(),
            SolverMode::Z3,
        ) else {
            panic!("a universal Many contract must ignore unknown set membership")
        };

        let SolverOutcome::Witness { input, .. } = solve_invariant(
            &program,
            program.invariant("known_witness").unwrap(),
            SolverMode::Z3,
        ) else {
            panic!("an existential Many assertion must require a known witness")
        };
        assert!(input.bindings["e"].fields.contains_key("judgment"));
    }

    fn values(interval: Interval) -> impl Iterator<Item = i128> {
        interval.lower..=interval.upper
    }

    #[test]
    fn interval_arithmetic_matches_small_exhaustive_oracles() {
        for left in intervals() {
            let negated = interval_negate(left).unwrap();
            let expected = values(left).map(|value| -value).collect::<Vec<_>>();
            assert_eq!(negated.lower, *expected.iter().min().unwrap());
            assert_eq!(negated.upper, *expected.iter().max().unwrap());

            let absolute = interval_abs(left).unwrap();
            let expected = values(left).map(i128::abs).collect::<Vec<_>>();
            assert_eq!(absolute.lower, *expected.iter().min().unwrap());
            assert_eq!(absolute.upper, *expected.iter().max().unwrap());

            for right in intervals() {
                let pairs = || {
                    values(left).flat_map(move |left| values(right).map(move |right| (left, right)))
                };
                for (actual, expected) in [
                    (
                        interval_add(left, right).unwrap(),
                        pairs()
                            .map(|(left, right)| left + right)
                            .collect::<Vec<_>>(),
                    ),
                    (
                        interval_subtract(left, right).unwrap(),
                        pairs()
                            .map(|(left, right)| left - right)
                            .collect::<Vec<_>>(),
                    ),
                    (
                        interval_multiply(left, right).unwrap(),
                        pairs()
                            .map(|(left, right)| left * right)
                            .collect::<Vec<_>>(),
                    ),
                    (
                        interval_min_max(Some(left), Some(right), false).unwrap(),
                        pairs()
                            .map(|(left, right)| left.min(right))
                            .collect::<Vec<_>>(),
                    ),
                    (
                        interval_min_max(Some(left), Some(right), true).unwrap(),
                        pairs()
                            .map(|(left, right)| left.max(right))
                            .collect::<Vec<_>>(),
                    ),
                ] {
                    assert_eq!(actual.lower, *expected.iter().min().unwrap());
                    assert_eq!(actual.upper, *expected.iter().max().unwrap());
                }
            }
        }
    }

    #[test]
    fn interval_overflow_drops_the_optimization_instead_of_wrapping() {
        let maximum = Interval {
            lower: i128::MAX,
            upper: i128::MAX,
        };
        let minimum = Interval {
            lower: i128::MIN,
            upper: i128::MIN,
        };
        assert!(interval_add(maximum, Interval { lower: 1, upper: 1 }).is_none());
        assert!(interval_subtract(minimum, Interval { lower: 1, upper: 1 }).is_none());
        assert!(interval_multiply(maximum, Interval { lower: 2, upper: 2 }).is_none());
        assert!(interval_negate(minimum).is_none());
        assert!(interval_abs(minimum).is_none());

        assert!(
            Interval {
                lower: i128::from(i64::MIN),
                upper: i128::from(i64::MAX),
            }
            .within_i64()
        );
        assert!(!maximum.within_i64());
        assert!(!minimum.within_i64());
    }

    #[test]
    fn existential_cardinality_returns_a_witness_or_exact_refutation() {
        let satisfiable = compile_text(
            r"mod SomeSolver
enum Result:
    Yes

record E:
    x: Int [0, 2]


policy.yes:
    A value of one produces Yes.

    rule yes(e E):
        e.x = 1: d(e) = Yes

assert some reachable(e E):
    d(e)
",
        );
        let invariant = satisfiable.invariant("reachable").unwrap();
        let SolverOutcome::Witness { input, metadata } =
            solve_invariant(&satisfiable, invariant, SolverMode::Z3)
        else {
            panic!("expected an existential witness")
        };
        assert_eq!(metadata.logic, "QF_LIA");
        assert_eq!(input.bindings["e"].fields["x"], Value::Int(1));

        let impossible = compile_text(
            r"mod SomeSolver
enum Result:
    Yes

record E:
    x: Int [0, 2]

rule unavailable(e E):
    e.x < 0: d(e) = Yes

assert some reachable(e E):
    d(e)
",
        );
        assert!(matches!(
            solve_invariant(
                &impossible,
                impossible.invariant("reachable").unwrap(),
                SolverMode::Z3
            ),
            SolverOutcome::Refuted(_)
        ));
    }

    #[test]
    fn existential_implication_requires_a_true_premise_and_good_result() {
        let impossible = compile_text(
            r"mod SomeSolver
enum Result:
    No

record E:
    x: Int [0, 1]


policy.false_premise:
    Only zero produces No.

    rule only_false_premise(e E):
        e.x = 0: d(e) = No

assert some reachable(e E):
    e.x > 0: d(e) = No
",
        );
        assert!(matches!(
            solve_invariant(
                &impossible,
                impossible.invariant("reachable").unwrap(),
                SolverMode::Z3
            ),
            SolverOutcome::Refuted(_)
        ));

        let satisfiable = compile_text(
            r"mod SomeSolver
enum Result:
    No
    Yes

record E:
    x: Int [0, 2]


policy.result:
    Zero produces No and one produces Yes.

    rule no(e E):
        e.x = 0: d(e) = No

    rule yes(e E):
        e.x = 1: d(e) = Yes

assert some reachable(e E):
    e.x > 0: d(e) = Yes
",
        );
        let SolverOutcome::Witness { input, .. } = solve_invariant(
            &satisfiable,
            satisfiable.invariant("reachable").unwrap(),
            SolverMode::Z3,
        ) else {
            panic!("expected a non-vacuous implication witness")
        };
        assert_eq!(input.bindings["e"].fields["x"], Value::Int(1));
    }

    #[test]
    fn implication_treats_an_empty_optional_decision_as_not_equal() {
        let program = compile_text(
            r"mod Solver
enum Result:
    Yes

record E:
    x: Int [0, 1]

rule no_result(e E):
    e.x < e.x: d(e) = Yes

assert optional_contract(e E):
    d(e)?

assert universal(e E):
    O: d(e) != Yes

assert some existential(e E):
    O: d(e) != Yes
",
        );
        assert!(matches!(
            solve_invariant(
                &program,
                program.invariant("universal").unwrap(),
                SolverMode::Z3
            ),
            SolverOutcome::Proved(_)
        ));
        assert!(matches!(
            solve_invariant(
                &program,
                program.invariant("existential").unwrap(),
                SolverMode::Z3
            ),
            SolverOutcome::Witness { .. }
        ));
    }

    #[test]
    fn finite_decimal_totality_elides_expensive_validity_formula() {
        let exact = compile_text(
            r"mod Solver
record E:
    amount: Decimal {1.0, 2.0}
    rate: Decimal {0.25, 0.50}
    split: Int [1, 2]
    hold: Bool

fn payout(amount Decimal, rate Decimal, split Int) Decimal:
    amount * rate / split


policy.payout:
    Available payouts use the declared formula.

    rule available(e E):
        e.hold X: d(e) = payout(e.amount, e.rate, e.split)

assert safe(e E):
    d(e)?
",
        );
        let query = export_invariant_smtlib(&exact, "safe").unwrap();
        assert_eq!(query.metadata.logic, "QF_NIA");
        assert!(
            !query.script.contains("(mod "),
            "a proved-finite candidate should not retain Decimal validity moduli\n{}",
            query.script
        );
        assert!(matches!(
            solve_invariant(&exact, exact.invariant("safe").unwrap(), SolverMode::Z3),
            SolverOutcome::Proved(_)
        ));

        let inexact = compile_text(
            r"mod Solver
record E:
    amount: Decimal {1.0}
    split: Int [3, 3]
    hold: Bool

fn payout(amount Decimal, split Int) Decimal:
    amount / split


policy.payout:
    Available payouts use division.

    rule available(e E):
        e.hold X: d(e) = payout(e.amount, e.split)

assert safe(e E):
    d(e)?
",
        );
        let query = export_invariant_smtlib(&inexact, "safe").unwrap();
        assert!(query.script.contains("(mod "));
        let SolverOutcome::Counterexample { input, .. } =
            solve_invariant(&inexact, inexact.invariant("safe").unwrap(), SolverMode::Z3)
        else {
            panic!("an inexact finite Decimal combination must remain a conflict")
        };
        assert!(
            crate::analysis::replay_invariant_violation(&inexact, "safe", &input)
                .unwrap()
                .is_some()
        );

        let partially_invalid = compile_text(
            r"mod Solver
record E:
    amount: Decimal {1.0}
    split: Int [0, 1]
    hold: Bool

fn payout(amount Decimal, split Int) Decimal:
    (amount / split) * 0


policy.payout:
    Available payouts may divide by zero.

    rule available(e E):
        e.hold X: d(e) = payout(e.amount, e.split)

assert safe(e E):
    d(e)?
",
        );
        let SolverOutcome::Counterexample { input, .. } = solve_invariant(
            &partially_invalid,
            partially_invalid.invariant("safe").unwrap(),
            SolverMode::Z3,
        ) else {
            panic!("an invalid inner division must not be hidden by multiplication by zero")
        };
        assert!(
            crate::analysis::replay_invariant_violation(&partially_invalid, "safe", &input)
                .unwrap()
                .is_some()
        );

        let over_limit = compile_text(
            r"mod Solver
record E:
    amount: Decimal {1.0}
    offset: Int [0, 256]
    hold: Bool

fn payout(amount Decimal, offset Int) Decimal:
    amount + offset


policy.payout:
    Available payouts add an offset.

    rule available(e E):
        e.hold X: d(e) = payout(e.amount, e.offset)

assert safe(e E):
    d(e)?
",
        );
        let query = export_invariant_smtlib(&over_limit, "safe").unwrap();
        assert!(
            query.script.contains("(mod "),
            "257 finite values must retain the bounded symbolic fallback"
        );
    }

    #[test]
    fn existential_decimal_product_uses_exact_nonlinear_arithmetic() {
        let program = compile_text(
            r"mod SomeSolver
enum Result:
    Yes

record E:
    left: Decimal [0.0, 2.0]
    right: Decimal [0.0, 2.0]


policy.product:
    A product of two produces Yes.

    rule product(e E):
        e.left * e.right = 2.0: d(e) = Yes

assert some reachable(e E):
    d(e)
",
        );
        let SolverOutcome::Witness { input, metadata } = solve_invariant(
            &program,
            program.invariant("reachable").unwrap(),
            SolverMode::Z3,
        ) else {
            panic!("expected a nonlinear Decimal witness")
        };
        assert_eq!(metadata.logic, "QF_NIA");
        let left = input.bindings["e"].fields["left"]
            .as_decimal()
            .expect("Decimal left field");
        let right = input.bindings["e"].fields["right"]
            .as_decimal()
            .expect("Decimal right field");
        assert_eq!(left.checked_mul(right), Some(Decimal::from(2)));
    }

    #[test]
    fn external_export_ignores_unreferenced_optional_and_date_fields() {
        let program = compile_text(
            r"mod Export
enum Result:
    Yes
record E:
    x: Int [0, 1]
    flag: Bool?
    observed: Date
    optional_date: Date?
rule zero(e E):
    e.x = 0: d(e) = Yes
assert total(e E):
    d(e)
",
        );

        let query = export_invariant_smtlib(&program, "total").unwrap();

        assert_eq!(query.metadata.schema_version, SMTLIB_QUERY_SCHEMA_VERSION);
        assert_eq!(query.symbols.len(), 1);
        assert_eq!(query.symbols[0].field, "x");
        assert!(matches!(
            query.symbols[0].encoding,
            SmtSymbolEncoding::Int { .. }
        ));
        assert_eq!(query.script.matches("(declare-fun ").count(), 1);
        assert!(query.script.contains("(declare-fun v0"));
        assert!(!query.script.contains("_present"), "{}", query.script);
        assert!(
            !query.script.contains("(declare-fun v1"),
            "{}",
            query.script
        );
        let solver = Solver::new();
        solver.from_string(query.script);
        assert_eq!(solver.check(), SatResult::Sat);
    }

    #[test]
    fn external_export_still_rejects_referenced_optional_and_date_fields() {
        let optional = compile_text(
            r"mod Export
enum Result:
    Yes
record E:
    flag: Bool?
rule enabled(e E):
    e.flag: d(e) = Yes
assert total(e E):
    d(e)
",
        );
        let error = export_invariant_smtlib(&optional, "total").unwrap_err();
        assert!(matches!(
            error,
            SmtLibExportError::Unsupported { ref reason, .. }
                if reason.contains("optional field `e.flag`")
        ));

        let date = compile_text(
            r#"mod Export
enum Result:
    Yes
record E:
    observed: Date
rule before(e E):
    e.observed < date("2025-01-01"): d(e) = Yes
assert total(e E):
    d(e)
"#,
        );
        let error = export_invariant_smtlib(&date, "total").unwrap_err();
        assert!(matches!(
            error,
            SmtLibExportError::Unsupported { ref reason, .. }
                if reason.contains("Date field `e.observed`")
        ));

        let nested_optional = compile_text(
            r"mod Export
enum Result:
    Yes
record E:
    flag: Bool?
fn inner(e E) Bool:
    e.flag
fn outer(e E) Bool:
    e inner
rule enabled(e E):
    e outer: d(e) = Yes
assert total(e E):
    d(e)
",
        );
        let error = export_invariant_smtlib(&nested_optional, "total").unwrap_err();
        assert!(matches!(
            error,
            SmtLibExportError::Unsupported { ref reason, .. }
                if reason.contains("optional field `e.flag`")
        ));

        let nested_date = compile_text(
            r#"mod Export
enum Result:
    Yes
record E:
    observed: Date
fn inner(e E) Bool:
    e.observed < date("2025-01-01")
fn outer(e E) Bool:
    e inner
rule before(e E):
    e outer: d(e) = Yes
assert total(e E):
    d(e)
"#,
        );
        let error = export_invariant_smtlib(&nested_date, "total").unwrap_err();
        assert!(matches!(
            error,
            SmtLibExportError::Unsupported { ref reason, .. }
                if reason.contains("Date field `e.observed`")
        ));
    }

    #[test]
    fn sat_models_fill_symbol_less_fields_from_their_declared_domain() {
        let universal = compile_text(
            r#"mod Solver
enum Result:
    Yes
record E:
    x: Int [0, 1]
    label: String {"declared"}
rule zero(e E):
    e.x = 0: d(e) = Yes
assert total(e E):
    d(e)
"#,
        );
        let SolverOutcome::Counterexample { input, .. } = solve_invariant(
            &universal,
            universal.invariant("total").unwrap(),
            SolverMode::Z3,
        ) else {
            panic!("expected a universal counterexample")
        };
        assert_eq!(
            input.bindings["e"].fields["label"],
            Value::String("declared".into())
        );
        assert!(input.validate(&universal).is_empty());
        assert!(
            crate::analysis::replay_invariant_violation(&universal, "total", &input)
                .unwrap()
                .is_some()
        );

        let existential = compile_text(
            r#"mod Solver
enum Result:
    Yes
record E:
    x: Int [0, 1]
    label: String {"declared"}
rule one(e E):
    e.x = 1: d(e) = Yes
assert some reachable(e E):
    d(e)
"#,
        );
        let SolverOutcome::Witness { input, .. } = solve_invariant(
            &existential,
            existential.invariant("reachable").unwrap(),
            SolverMode::Z3,
        ) else {
            panic!("expected an existential witness")
        };
        assert_eq!(
            input.bindings["e"].fields["label"],
            Value::String("declared".into())
        );
        assert!(input.validate(&existential).is_empty());
        crate::analysis::replay_invariant_witness(&existential, "reachable", &input).unwrap();
    }
}