conjure_cp_core/

settings.rs

use std::{
    cell::{Cell, RefCell},
    collections::VecDeque,
    fmt::Display,
    io::{self, BufRead, Write},
    str::FromStr,
};

use schemars::JsonSchema;
use serde::{Deserialize, Serialize};
use strum_macros::{Display as StrumDisplay, EnumIter};

use crate::bug;
use crate::bug_assert;

/// Strategy used when a modelling decision has more than one applicable answer.
#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]
pub enum Heuristic {
    First,
    Random,
    #[default]
    Compact,
    /// Prompt on stdin, or consume values from [`set_heuristic_responses`].
    Interactive,
    /// Enumerate every applicable choice. This is supported by the exhaustive model generator,
    /// but is not accepted by the command-line interface yet.
    All,
}

impl Display for Heuristic {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        f.write_str(match self {
            Self::First => "f",
            Self::Random => "r",
            Self::Compact => "c",
            Self::Interactive => "i",
            Self::All => "x",
        })
    }
}

impl FromStr for Heuristic {
    type Err = String;

    fn from_str(value: &str) -> Result<Self, Self::Err> {
        match value.trim().to_ascii_lowercase().as_str() {
            "f" | "first" => Ok(Self::First),
            "r" | "random" => Ok(Self::Random),
            "c" | "compact" => Ok(Self::Compact),
            "i" | "interactive" => Ok(Self::Interactive),
            "x" | "all" => Ok(Self::All),
            other => Err(format!(
                "unknown heuristic '{other}'; expected one of: f, r, c, i, x"
            )),
        }
    }
}

/// Whether a declaration may have more than one channelled representation.
#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]
pub enum Channelling {
    #[default]
    No,
    Yes,
    /// One representation kind per type family throughout a model, without channelling.
    Uniform,
}

impl Display for Channelling {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        f.write_str(match self {
            Self::No => "no",
            Self::Yes => "yes",
            Self::Uniform => "uniform",
        })
    }
}

impl FromStr for Channelling {
    type Err = String;

    fn from_str(value: &str) -> Result<Self, Self::Err> {
        match value.trim().to_ascii_lowercase().as_str() {
            "no" => Ok(Self::No),
            "yes" => Ok(Self::Yes),
            "uniform" => Ok(Self::Uniform),
            other => Err(format!(
                "unknown channelling setting '{other}'; expected yes, no, or uniform"
            )),
        }
    }
}

pub const DEFAULT_HEURISTIC_SEED: u64 = 0;

thread_local! {
    static ELEMENT_ENCODING: Cell<Option<crate::ast::sat_decision::ElementEncoding>> = const { Cell::new(None) };
    static TABLE_ENCODING: Cell<Option<crate::ast::sat_decision::TableEncoding>> = const { Cell::new(None) };
    static ALLDIFFERENT_ENCODING: Cell<Option<crate::ast::sat_decision::AllDifferentEncoding>> = const { Cell::new(None) };
    static PB_ENCODING: Cell<Option<crate::ast::sat_decision::PbEncoding>> = const { Cell::new(None) };
    static CARDINALITY_ENCODING: Cell<Option<crate::ast::sat_decision::CardinalityEncoding>> = const { Cell::new(None) };
    static AMO_ENCODING: Cell<Option<crate::ast::sat_decision::AmoEncoding>> = const { Cell::new(None) };
    static HEURISTIC: Cell<Heuristic> = const { Cell::new(Heuristic::Compact) };
    static CHANNELLING: Cell<Channelling> = const { Cell::new(Channelling::No) };
    static HEURISTIC_RANDOM_STATE: Cell<u64> = const { Cell::new(DEFAULT_HEURISTIC_SEED) };
    static HEURISTIC_ALL_CHOICES: RefCell<AllChoicesState> =
        const { RefCell::new(AllChoicesState::new()) };
    /// 1-based answers for the interactive heuristic, matching Conjure's `--responses`.
    static HEURISTIC_RESPONSES: RefCell<VecDeque<usize>> = const { RefCell::new(VecDeque::new()) };
}

#[derive(Clone, Debug, PartialEq, Eq)]
pub struct HeuristicChoice {
    pub selected: usize,
    pub options: Vec<String>,
}

#[derive(Debug)]
struct AllChoicesState {
    requested: Vec<usize>,
    decisions: Vec<HeuristicChoice>,
}

impl AllChoicesState {
    const fn new() -> Self {
        Self {
            requested: Vec::new(),
            decisions: Vec::new(),
        }
    }
}

pub fn set_heuristic(heuristic: Heuristic) {
    HEURISTIC.with(|current| current.set(heuristic));
}

pub fn heuristic() -> Heuristic {
    HEURISTIC.with(Cell::get)
}

pub fn set_channelling(channelling: Channelling) {
    CHANNELLING.with(|current| current.set(channelling));
    crate::representation::uniform::reset();
}

pub fn channelling() -> Channelling {
    CHANNELLING.with(Cell::get)
}

pub fn set_heuristic_seed(seed: u64) {
    HEURISTIC_RANDOM_STATE.with(|state| state.set(seed));
}

/// Sets the 1-based answers consumed by the interactive heuristic (`i`).
///
/// When provided (e.g. via `--responses`), these are used instead of prompting on stdin.
/// Values must be in `1..=n` for a decision with `n` options, matching Conjure.
pub fn set_heuristic_responses(responses: Vec<usize>) {
    HEURISTIC_RESPONSES.with(|state| {
        *state.borrow_mut() = VecDeque::from(responses);
    });
}

/// Clears any remaining interactive responses.
pub fn clear_heuristic_responses() {
    HEURISTIC_RESPONSES.with(|state| state.borrow_mut().clear());
}

/// Returns a deterministic pseudo-random index and advances the per-thread heuristic RNG.
pub fn next_heuristic_random_index(upper_bound: usize) -> usize {
    bug_assert!(
        upper_bound > 0,
        "random choice requires at least one candidate"
    );
    HEURISTIC_RANDOM_STATE.with(|state| {
        // SplitMix64: small, reproducible, and sufficient for choice ordering.
        let next = state.get().wrapping_add(0x9e37_79b9_7f4a_7c15);
        state.set(next);
        let mut mixed = next;
        mixed = (mixed ^ (mixed >> 30)).wrapping_mul(0xbf58_476d_1ce4_e5b9);
        mixed = (mixed ^ (mixed >> 27)).wrapping_mul(0x94d0_49bb_1331_11eb);
        mixed ^= mixed >> 31;
        (mixed as usize) % upper_bound
    })
}

/// Starts one replay of the `x` heuristic using the requested branch indices.
pub fn begin_heuristic_all_choices(requested: Vec<usize>) {
    HEURISTIC_ALL_CHOICES.with(|state| {
        *state.borrow_mut() = AllChoicesState {
            requested,
            decisions: Vec::new(),
        };
    });
}

/// Restores the previous heuristic when a scoped override ends.
struct HeuristicGuard(Heuristic);

impl Drop for HeuristicGuard {
    fn drop(&mut self) {
        set_heuristic(self.0);
    }
}

/// Runs `f` with the compact heuristic in force, whatever the configured one is.
///
/// Rewriting a temporary model -- a comprehension generator submodel, say -- picks representations
/// too, but those are not modelling choices about the user's problem: a representation is
/// semantics-preserving, so whichever one a submodel gets, it enumerates the same values. Compact
/// takes the smallest and moves on, leaving the configured heuristic's state for the decisions that
/// do matter: `x` keeps enumerating combinations of the real model only, the random stream is not
/// advanced, and the interactive heuristic does not ask the user about throwaway variables.
///
/// A representation named on the domain itself (`set (representation packed)`) still wins -- representation
/// selection honours that before it consults the heuristic at all.
pub fn with_compact_heuristic<T>(f: impl FnOnce() -> T) -> T {
    let previous = heuristic();
    set_heuristic(Heuristic::Compact);
    let _guard = HeuristicGuard(previous);
    f()
}

/// Selects the requested branch at the next `x` decision and records all available options.
pub fn next_heuristic_all_index(options: &[&str]) -> usize {
    bug_assert!(
        !options.is_empty(),
        "all-choice requires at least one candidate"
    );
    HEURISTIC_ALL_CHOICES.with(|state| {
        let mut state = state.borrow_mut();
        let decision_index = state.decisions.len();
        let selected = state.requested.get(decision_index).copied().unwrap_or(0);
        assert!(
            selected < options.len(),
            "requested heuristic branch {selected} but only {} options exist",
            options.len()
        );
        state.decisions.push(HeuristicChoice {
            selected,
            options: options.iter().map(|option| (*option).to_string()).collect(),
        });
        selected
    })
}

pub fn heuristic_all_choices() -> Vec<HeuristicChoice> {
    HEURISTIC_ALL_CHOICES.with(|state| state.borrow().decisions.clone())
}

/// Selects an option for the interactive heuristic (`i`).
///
/// Options are printed 1-based. Prefers the next value from [`set_heuristic_responses`]; otherwise
/// prompts on stdin (empty input picks option 1), matching Conjure.
pub fn next_heuristic_interactive_index(options: &[&str]) -> usize {
    bug_assert!(
        !options.is_empty(),
        "interactive choice requires at least one candidate"
    );

    for (index, option) in options.iter().enumerate() {
        eprintln!("{}. {}", index + 1, option);
    }

    let recorded = HEURISTIC_RESPONSES.with(|state| state.borrow_mut().pop_front());
    let one_based = match recorded {
        Some(recorded) => {
            eprintln!("Response: {recorded}");
            assert!(
                recorded >= 1 && recorded <= options.len(),
                "recorded response {recorded} out of range; expected a value between 1 and {}",
                options.len()
            );
            recorded
        }
        None => prompt_heuristic_interactive_choice(options.len()),
    };
    one_based - 1
}

fn prompt_heuristic_interactive_choice(option_count: usize) -> usize {
    let stdin = io::stdin();
    let mut stdout = io::stderr();
    loop {
        eprint!("Pick option: ");
        let _ = stdout.flush();
        let mut line = String::new();
        if stdin.lock().read_line(&mut line).is_err() {
            eprintln!("Failed to read interactive heuristic response; defaulting to 1");
            return 1;
        }
        let trimmed = line.trim();
        if trimmed.is_empty() {
            return 1;
        }
        match trimmed.parse::<usize>() {
            Ok(value) if value >= 1 && value <= option_count => return value,
            Ok(_) => {
                eprintln!("Enter a value between 1 and {option_count}");
            }
            Err(_) => {
                eprintln!("Enter an integer value.");
            }
        }
    }
}

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Default)]
pub enum Parser {
    #[default]
    TreeSitter,
    ViaConjure,
}

impl Display for Parser {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Parser::TreeSitter => write!(f, "tree-sitter"),
            Parser::ViaConjure => write!(f, "via-conjure"),
        }
    }
}

impl FromStr for Parser {
    type Err = String;

    fn from_str(s: &str) -> Result<Self, Self::Err> {
        match s.trim().to_ascii_lowercase().as_str() {
            "tree-sitter" => Ok(Parser::TreeSitter),
            "via-conjure" => Ok(Parser::ViaConjure),
            other => Err(format!(
                "unknown parser: {other}; expected one of: tree-sitter, via-conjure"
            )),
        }
    }
}

thread_local! {
    /// Thread-local setting for which parser is currently active.
    ///
    /// Must be explicitly set before use.
    static CURRENT_PARSER: Cell<Option<Parser>> = const { Cell::new(None) };
}

pub fn set_current_parser(parser: Parser) {
    CURRENT_PARSER.with(|current| current.set(Some(parser)));
}

pub fn current_parser() -> Parser {
    CURRENT_PARSER.with(|current| {
        current.get().unwrap_or_else(|| {
            // loud failure on purpose, so we don't end up using the default
            bug!("current parser not set for this thread; call set_current_parser first")
        })
    })
}

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub struct RewriteConfig {
    /// Skip rules whose declared expression discriminants cannot match.
    pub prefilter: bool,
    /// Drive rewriting from persistent dirty node queues instead of repeated full scans.
    pub worklist: bool,
}

impl RewriteConfig {
    pub const fn baseline() -> Self {
        Self {
            prefilter: false,
            worklist: false,
        }
    }

    pub const fn optimised() -> Self {
        Self {
            prefilter: true,
            worklist: true,
        }
    }

    pub const fn is_baseline(self) -> bool {
        !self.prefilter && !self.worklist
    }

    pub const fn is_optimised(self) -> bool {
        self.prefilter && self.worklist
    }
}

impl Default for RewriteConfig {
    fn default() -> Self {
        Self::optimised()
    }
}

impl Display for RewriteConfig {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        if self.is_optimised() {
            write!(f, "optimised")
        } else if self.is_baseline() {
            write!(f, "baseline")
        } else {
            let mut options = vec!["baseline"];
            if self.prefilter {
                options.push("prefilter");
            }
            if self.worklist {
                options.push("worklist");
            }
            write!(f, "{}", options.join("+"))
        }
    }
}

impl FromStr for RewriteConfig {
    type Err = String;

    fn from_str(s: &str) -> Result<Self, Self::Err> {
        let trimmed = s.trim().to_ascii_lowercase();
        match trimmed.as_str() {
            "baseline" => return Ok(Self::baseline()),
            "optimised" => return Ok(Self::optimised()),
            _ => {}
        }

        if !trimmed.starts_with("baseline+") {
            return Err(format!(
                "unknown rewrite config: {trimmed}; expected baseline, optimised, or baseline plus '+' separated prefilter/worklist options"
            ));
        }

        let mut config = Self::baseline();
        let mut baseline_seen = false;
        let mut prefilter_seen = false;
        let mut worklist_seen = false;
        let mut option_seen = false;

        for token in trimmed.split('+') {
            match token {
                "" => {}
                "baseline" => {
                    if baseline_seen {
                        return Err("duplicate rewrite option 'baseline'".to_string());
                    }
                    baseline_seen = true;
                }
                "prefilter" => {
                    if prefilter_seen {
                        return Err("duplicate rewrite option 'prefilter'".to_string());
                    }
                    config.prefilter = true;
                    prefilter_seen = true;
                    option_seen = true;
                }
                "worklist" => {
                    if worklist_seen {
                        return Err("duplicate rewrite option 'worklist'".to_string());
                    }
                    config.worklist = true;
                    worklist_seen = true;
                    option_seen = true;
                }
                other => {
                    return Err(format!(
                        "unknown rewrite option '{other}'; expected baseline, optimised, or a '+' separated combination of: prefilter, worklist"
                    ));
                }
            }
        }

        if !option_seen {
            return Err(
                "rewrite config 'baseline+' must include at least one of: prefilter, worklist"
                    .to_string(),
            );
        }

        Ok(config)
    }
}

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub enum Rewriter {
    Rewrite(RewriteConfig),
}

impl Default for Rewriter {
    fn default() -> Self {
        Self::Rewrite(RewriteConfig::optimised())
    }
}

thread_local! {
    /// Thread-local setting for which rewriter is currently active.
    ///
    /// Must be explicitly set before use.
    static CURRENT_REWRITER: Cell<Option<Rewriter>> = const { Cell::new(None) };
}

impl Display for Rewriter {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Rewriter::Rewrite(config) => write!(f, "{config}"),
        }
    }
}

impl FromStr for Rewriter {
    type Err = String;

    fn from_str(s: &str) -> Result<Self, Self::Err> {
        let trimmed = s.trim().to_ascii_lowercase();
        match trimmed.as_str() {
            "baseline" | "optimised" => Ok(Rewriter::Rewrite(trimmed.parse()?)),
            other => {
                if other.contains('+') {
                    return Ok(Rewriter::Rewrite(other.parse()?));
                }

                Err(format!(
                    "unknown rewriter: {other}; expected baseline, optimised, or baseline plus '+' separated prefilter/worklist options"
                ))
            }
        }
    }
}

pub fn set_current_rewriter(rewriter: Rewriter) {
    CURRENT_REWRITER.with(|current| current.set(Some(rewriter)));
}

pub fn current_rewriter() -> Rewriter {
    CURRENT_REWRITER.with(|current| {
        current.get().unwrap_or_else(|| {
            // loud failure on purpose, so we don't end up using the default
            bug!("current rewriter not set for this thread; call set_current_rewriter first")
        })
    })
}

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub enum QuantifiedExpander {
    Auto,
    Native,
    ViaSolver,
    ViaSolverAc,
}

impl Display for QuantifiedExpander {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            QuantifiedExpander::Auto => write!(f, "auto"),
            QuantifiedExpander::Native => write!(f, "native"),
            QuantifiedExpander::ViaSolver => write!(f, "via-solver"),
            QuantifiedExpander::ViaSolverAc => write!(f, "via-solver-ac"),
        }
    }
}

impl FromStr for QuantifiedExpander {
    type Err = String;

    fn from_str(s: &str) -> Result<Self, Self::Err> {
        match s.trim().to_ascii_lowercase().as_str() {
            "auto" => Ok(QuantifiedExpander::Auto),
            "native" => Ok(QuantifiedExpander::Native),
            "via-solver" => Ok(QuantifiedExpander::ViaSolver),
            "via-solver-ac" => Ok(QuantifiedExpander::ViaSolverAc),
            _ => Err(format!(
                "unknown comprehension expander: {s}; expected one of: \
                 auto, native, via-solver, via-solver-ac"
            )),
        }
    }
}

thread_local! {
    /// Thread-local setting for which comprehension expansion strategy is currently active.
    ///
    /// Must be explicitly set before use.
    static COMPREHENSION_EXPANDER: Cell<Option<QuantifiedExpander>> = const { Cell::new(None) };
}

pub fn set_comprehension_expander(expander: QuantifiedExpander) {
    COMPREHENSION_EXPANDER.with(|current| current.set(Some(expander)));
}

pub fn comprehension_expander() -> QuantifiedExpander {
    COMPREHENSION_EXPANDER.with(|current| {
        current.get().unwrap_or_else(|| {
            // loud failure on purpose, so we don't end up using the default
            bug!(
                "comprehension expander not set for this thread; call set_comprehension_expander first"
            )
        })
    })
}

#[derive(
    Debug,
    EnumIter,
    StrumDisplay,
    PartialEq,
    Eq,
    Hash,
    Clone,
    Copy,
    Serialize,
    Deserialize,
    JsonSchema,
)]
pub enum SolverFamily {
    Minion,
    Sat,
    Z3,
}

thread_local! {
    /// Thread-local setting for which solver family is currently active.
    ///
    /// Must be explicitly set before use.
    static CURRENT_SOLVER_FAMILY: Cell<Option<SolverFamily>> = const { Cell::new(None) };
}

pub const DEFAULT_MINION_DISCRETE_THRESHOLD: usize = 10;

thread_local! {
    /// Thread-local setting controlling when Minion int domains are emitted as `DISCRETE`.
    ///
    /// If an int domain size is <= this threshold, the Minion adaptor uses `DISCRETE`; otherwise
    /// it uses `BOUND`, unless another constraint requires `DISCRETE`.
    static MINION_DISCRETE_THRESHOLD: Cell<Option<usize>> = const { Cell::new(None) };

    /// Thread-local setting controlling whether rule-trace outputs are active in this phase.
    ///
    /// This is intentionally off by default and can be disabled before solver-time rewrites so
    /// follow-up dominance-blocking rewrites do not pollute the initial rewrite trace.
    static RULE_TRACE_ENABLED: Cell<bool> = const { Cell::new(false) };

    /// Thread-local setting controlling whether default rule traces are configured.
    static DEFAULT_RULE_TRACE_ENABLED: Cell<bool> = const { Cell::new(false) };

    /// Thread-local setting controlling whether verbose rule-attempt traces are configured.
    static RULE_ATTEMPT_TRACE_ENABLED: Cell<bool> = const { Cell::new(false) };

    /// Thread-local setting controlling whether aggregate rule-application traces are configured.
    static RULE_TRACE_AGGREGATES_ENABLED: Cell<bool> = const { Cell::new(false) };
}

pub fn set_current_solver_family(solver_family: SolverFamily) {
    CURRENT_SOLVER_FAMILY.with(|current| current.set(Some(solver_family)));
}

/// Restores the previous solver family when a scoped override ends.
struct SolverFamilyGuard(Option<SolverFamily>);

impl Drop for SolverFamilyGuard {
    fn drop(&mut self) {
        CURRENT_SOLVER_FAMILY.with(|current| current.set(self.0));
    }
}

/// Runs `f` as a rewrite for `solver_family`, then restores the surrounding solver context.
///
/// Some rewrites build and solve a temporary model with a different backend from the outer model.
/// Representation applicability must follow the backend that will actually consume that temporary
/// model, not the user's outer solver setting.
pub fn with_solver_family<T>(solver_family: SolverFamily, f: impl FnOnce() -> T) -> T {
    let previous = CURRENT_SOLVER_FAMILY.with(|current| current.replace(Some(solver_family)));
    let _guard = SolverFamilyGuard(previous);
    f()
}

/// The active solver family, or `None` if this thread has not set one.
///
/// Unlike [`current_solver_family`] this does not panic. Solver-family gating asks with this so
/// that unit tests exercising a single component do not have to stand up a solver context.
pub fn try_current_solver_family() -> Option<SolverFamily> {
    CURRENT_SOLVER_FAMILY.with(|current| current.get())
}

pub fn current_solver_family() -> SolverFamily {
    CURRENT_SOLVER_FAMILY.with(|current| {
        current.get().unwrap_or_else(|| {
            // loud failure on purpose, so we don't end up using the default
            bug!(
                "current solver family not set for this thread; call set_current_solver_family first"
            )
        })
    })
}

/// Whether integers carry a representation choice for the solver being targeted.
///
/// SAT has no integers at all: an int variable is encoded as a vector of Booleans, and which
/// encoding it gets is a representation choice like any other. The SMT backend does have integers,
/// but has two ways to express them -- linear arithmetic and bit-vectors -- so the choice is a
/// representation there too. Minion has one native integer and needs none of this. With no solver
/// family set -- a unit test exercising one component, say -- integers stay concrete.
pub fn ints_need_representation() -> bool {
    matches!(
        try_current_solver_family(),
        Some(SolverFamily::Sat | SolverFamily::Z3)
    )
}

/// Pins Minion's domain threshold, or leaves it to the modelling heuristic.
pub fn set_minion_discrete_threshold(threshold: Option<usize>) {
    MINION_DISCRETE_THRESHOLD.with(|current| current.set(threshold));
}

/// Selects one threshold for a Minion model: the default, all bound, or all discrete.
/// Constraints requiring discrete variables still override the threshold.
pub fn select_minion_discrete_threshold() -> usize {
    if let Some(threshold) = MINION_DISCRETE_THRESHOLD.with(Cell::get) {
        return threshold;
    }
    let thresholds = [DEFAULT_MINION_DISCRETE_THRESHOLD, 0, usize::MAX];
    let labels = [
        "minion-discrete-threshold=10",
        "minion-discrete-threshold=0",
        "minion-discrete-threshold=unlimited",
    ];
    let index = match heuristic() {
        Heuristic::First | Heuristic::Compact => 0,
        Heuristic::Random => next_heuristic_random_index(thresholds.len()),
        Heuristic::Interactive => next_heuristic_interactive_index(&labels),
        Heuristic::All => next_heuristic_all_index(&labels),
    };
    thresholds[index]
}

pub fn set_rule_trace_enabled(enabled: bool) {
    RULE_TRACE_ENABLED.with(|current| current.set(enabled));
}

pub fn rule_trace_enabled() -> bool {
    RULE_TRACE_ENABLED.with(|current| current.get())
}

pub fn set_default_rule_trace_enabled(enabled: bool) {
    DEFAULT_RULE_TRACE_ENABLED.with(|current| current.set(enabled));
}

pub fn default_rule_trace_enabled() -> bool {
    DEFAULT_RULE_TRACE_ENABLED.with(|current| current.get())
}

pub fn set_rule_attempt_trace_enabled(enabled: bool) {
    RULE_ATTEMPT_TRACE_ENABLED.with(|current| current.set(enabled));
}

pub fn rule_attempt_trace_enabled() -> bool {
    RULE_ATTEMPT_TRACE_ENABLED.with(|current| current.get())
}

pub fn set_rule_trace_aggregates_enabled(enabled: bool) {
    RULE_TRACE_AGGREGATES_ENABLED.with(|current| current.set(enabled));
}

pub fn rule_trace_aggregates_enabled() -> bool {
    RULE_TRACE_AGGREGATES_ENABLED.with(|current| current.get())
}

pub fn configured_rule_trace_enabled() -> bool {
    default_rule_trace_enabled() || rule_attempt_trace_enabled() || rule_trace_aggregates_enabled()
}

impl FromStr for SolverFamily {
    type Err = String;

    fn from_str(s: &str) -> Result<Self, Self::Err> {
        match s.trim().to_ascii_lowercase().as_str() {
            "minion" => Ok(SolverFamily::Minion),
            "sat" => Ok(SolverFamily::Sat),
            "z3" => Ok(SolverFamily::Z3),
            other => Err(format!(
                "unknown solver '{other}', expected one of: minion, sat, z3"
            )),
        }
    }
}

impl SolverFamily {
    pub fn as_str(&self) -> String {
        match self {
            SolverFamily::Minion => "minion".to_owned(),
            SolverFamily::Sat => "sat".to_owned(),
            SolverFamily::Z3 => "z3".to_owned(),
        }
    }
}

#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]
pub struct SolverArgs {
    pub timeout_ms: Option<u64>,
}

#[cfg(test)]
mod tests {
    use super::{
        Channelling, Heuristic, QuantifiedExpander, RewriteConfig, Rewriter, SolverFamily,
        begin_heuristic_all_choices, clear_heuristic_responses, heuristic_all_choices,
        next_heuristic_all_index, next_heuristic_interactive_index, next_heuristic_random_index,
        set_current_solver_family, set_heuristic_responses, set_heuristic_seed,
        try_current_solver_family, with_solver_family,
    };
    use std::str::FromStr;

    #[test]
    fn compact_is_the_default_heuristic() {
        assert_eq!(Heuristic::default(), Heuristic::Compact);
    }

    #[test]
    fn scoped_solver_family_restores_the_outer_solver() {
        set_current_solver_family(SolverFamily::Z3);

        with_solver_family(SolverFamily::Minion, || {
            assert_eq!(try_current_solver_family(), Some(SolverFamily::Minion));
        });

        assert_eq!(try_current_solver_family(), Some(SolverFamily::Z3));
    }

    #[test]
    fn parses_answer_heuristics_and_channelling() {
        assert_eq!(Heuristic::from_str("f"), Ok(Heuristic::First));
        assert_eq!(Heuristic::from_str("random"), Ok(Heuristic::Random));
        assert_eq!(Heuristic::from_str("c"), Ok(Heuristic::Compact));
        assert_eq!(Heuristic::from_str("i"), Ok(Heuristic::Interactive));
        assert_eq!(
            Heuristic::from_str("interactive"),
            Ok(Heuristic::Interactive)
        );
        assert_eq!(Heuristic::from_str("x"), Ok(Heuristic::All));
        assert_eq!(Channelling::from_str("no"), Ok(Channelling::No));
        assert_eq!(Channelling::from_str("yes"), Ok(Channelling::Yes));
        assert_eq!(Channelling::from_str("uniform"), Ok(Channelling::Uniform));
        assert_eq!(Channelling::Uniform.to_string(), "uniform");
    }

    #[test]
    fn parses_auto_comprehension_expander() {
        assert_eq!(
            QuantifiedExpander::from_str("auto"),
            Ok(QuantifiedExpander::Auto)
        );
        assert_eq!(QuantifiedExpander::Auto.to_string(), "auto");
    }

    #[test]
    fn interactive_heuristic_consumes_one_based_responses() {
        set_heuristic_responses(vec![2, 1]);
        assert_eq!(next_heuristic_interactive_index(&["left", "right"]), 1);
        assert_eq!(next_heuristic_interactive_index(&["a", "b", "c"]), 0);
        clear_heuristic_responses();
    }

    #[test]
    fn random_heuristic_is_reproducible_from_seed() {
        set_heuristic_seed(42);
        let first: Vec<_> = (0..8).map(|_| next_heuristic_random_index(7)).collect();
        set_heuristic_seed(42);
        let second: Vec<_> = (0..8).map(|_| next_heuristic_random_index(7)).collect();
        assert_eq!(first, second);
    }

    #[test]
    fn all_heuristic_replays_and_records_choices() {
        begin_heuristic_all_choices(vec![1]);
        assert_eq!(next_heuristic_all_index(&["left", "right"]), 1);
        assert_eq!(
            heuristic_all_choices()[0].options,
            vec!["left".to_string(), "right".to_string()]
        );
    }

    #[test]
    fn parses_rewrite_option_combinations() {
        assert_eq!(
            RewriteConfig::from_str("baseline").unwrap(),
            RewriteConfig {
                prefilter: false,
                worklist: false,
            }
        );
        assert_eq!(
            RewriteConfig::from_str("baseline+prefilter").unwrap(),
            RewriteConfig {
                prefilter: true,
                worklist: false,
            }
        );
        assert_eq!(
            RewriteConfig::from_str("baseline+worklist").unwrap(),
            RewriteConfig {
                prefilter: false,
                worklist: true,
            }
        );
        assert_eq!(
            RewriteConfig::from_str("baseline+prefilter+worklist").unwrap(),
            RewriteConfig::optimised()
        );
        assert!(RewriteConfig::from_str("+dirty").is_err());
        assert!(RewriteConfig::from_str("baseline+dirty").is_err());
        assert!(RewriteConfig::from_str("baseline+cache").is_err());
        assert!(RewriteConfig::from_str("baseline+rulememo").is_err());
        assert!(RewriteConfig::from_str("baseline+candidateindex").is_err());
        assert!(RewriteConfig::from_str("baseline+dirtyqueues").is_err());
        assert!(RewriteConfig::from_str("baseline+rule-memo").is_err());
        assert!(RewriteConfig::from_str("baseline+candidate-index").is_err());
        assert!(RewriteConfig::from_str("baseline+candidate-node-index").is_err());
        assert!(RewriteConfig::from_str("baseline+dirty-node-queues").is_err());
    }

    #[test]
    fn optimised_rewrite_config_enables_fast_default_options() {
        assert_eq!(
            RewriteConfig::from_str("optimised").unwrap(),
            RewriteConfig {
                prefilter: true,
                worklist: true,
            }
        );
    }

    #[test]
    fn displays_rewrite_option_combinations() {
        assert_eq!(RewriteConfig::baseline().to_string(), "baseline");
        assert_eq!(
            RewriteConfig {
                prefilter: true,
                worklist: false,
            }
            .to_string(),
            "baseline+prefilter"
        );
        assert_eq!(
            RewriteConfig {
                prefilter: false,
                worklist: true,
            }
            .to_string(),
            "baseline+worklist"
        );
        assert_eq!(RewriteConfig::optimised().to_string(), "optimised");
        assert_eq!(
            RewriteConfig::from_str("baseline+prefilter+worklist")
                .unwrap()
                .to_string(),
            "optimised"
        );
    }

    #[test]
    fn parses_rewriter_option_combinations() {
        assert_eq!(
            Rewriter::from_str("baseline+prefilter").unwrap(),
            Rewriter::Rewrite(RewriteConfig {
                prefilter: true,
                worklist: false,
            })
        );
        assert_eq!(
            Rewriter::from_str("baseline+prefilter+worklist").unwrap(),
            Rewriter::Rewrite(RewriteConfig::optimised())
        );
        assert!(Rewriter::from_str("+dirty").is_err());
        assert!(Rewriter::from_str("dirty").is_err());
        assert!(Rewriter::from_str("baseline+dirty").is_err());
    }
}

/// Pin the AMO algorithm, or allow the modelling heuristic to choose.
pub fn set_amo_encoding(encoding: Option<crate::ast::sat_decision::AmoEncoding>) {
    AMO_ENCODING.with(|current| current.set(encoding));
}
/// Explicit AMO algorithm override for this compilation thread.
pub fn amo_encoding() -> Option<crate::ast::sat_decision::AmoEncoding> {
    AMO_ENCODING.with(Cell::get)
}

/// Pin a cardinality provider/algorithm, or let the heuristic select it.
pub fn set_cardinality_encoding(encoding: Option<crate::ast::sat_decision::CardinalityEncoding>) {
    CARDINALITY_ENCODING.with(|current| current.set(encoding));
}
/// Explicit cardinality encoder override for this compilation thread.
pub fn cardinality_encoding() -> Option<crate::ast::sat_decision::CardinalityEncoding> {
    CARDINALITY_ENCODING.with(Cell::get)
}

/// Pin a pseudo-Boolean provider/algorithm, or let the heuristic select it.
pub fn set_pb_encoding(encoding: Option<crate::ast::sat_decision::PbEncoding>) {
    PB_ENCODING.with(|current| current.set(encoding));
}
/// Explicit pseudo-Boolean encoder override for this compilation thread.
pub fn pb_encoding() -> Option<crate::ast::sat_decision::PbEncoding> {
    PB_ENCODING.with(Cell::get)
}

/// Pin the allDifferent strategy, or let the heuristic choose an applicable composition.
pub fn set_alldifferent_encoding(encoding: Option<crate::ast::sat_decision::AllDifferentEncoding>) {
    ALLDIFFERENT_ENCODING.with(|current| current.set(encoding));
}
/// Explicit allDifferent strategy override for this compilation thread.
pub fn alldifferent_encoding() -> Option<crate::ast::sat_decision::AllDifferentEncoding> {
    ALLDIFFERENT_ENCODING.with(Cell::get)
}

/// Pin the table composition, or let the modelling heuristic select it.
pub fn set_table_encoding(encoding: Option<crate::ast::sat_decision::TableEncoding>) {
    TABLE_ENCODING.with(|current| current.set(encoding));
}
/// Explicit table strategy override for this compilation thread.
pub fn table_encoding() -> Option<crate::ast::sat_decision::TableEncoding> {
    TABLE_ENCODING.with(Cell::get)
}

/// Pin the element composition, or let the modelling heuristic select it.
pub fn set_element_encoding(encoding: Option<crate::ast::sat_decision::ElementEncoding>) {
    ELEMENT_ENCODING.with(|current| current.set(encoding));
}
/// Explicit element strategy override for this compilation thread.
pub fn element_encoding() -> Option<crate::ast::sat_decision::ElementEncoding> {
    ELEMENT_ENCODING.with(Cell::get)
}