Lines
69.8 %
Functions
27.22 %
use std::{cell::Cell, fmt::Display, str::FromStr};
use schemars::JsonSchema;
use serde::{Deserialize, Serialize};
use strum_macros::{Display as StrumDisplay, EnumIter};
use crate::bug;
use crate::solver::adaptors::smt::{IntTheory, MatrixTheory, TheoryConfig};
#[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 enum Rewriter {
Naive,
Morph,
/// Thread-local setting for which rewriter is currently active.
static CURRENT_REWRITER: Cell<Option<Rewriter>> = const { Cell::new(None) };
impl Display for Rewriter {
Rewriter::Naive => write!(f, "naive"),
Rewriter::Morph => write!(f, "morph"),
impl FromStr for Rewriter {
"naive" => Ok(Rewriter::Naive),
"morph" => Ok(Rewriter::Morph),
"unknown rewriter: {other}; expected one of: naive, morph"
pub fn set_current_rewriter(rewriter: Rewriter) {
CURRENT_REWRITER.with(|current| current.set(Some(rewriter)));
pub fn current_rewriter() -> Rewriter {
CURRENT_REWRITER.with(|current| {
bug!("current rewriter not set for this thread; call set_current_rewriter first")
pub enum QuantifiedExpander {
Native,
ViaSolver,
ViaSolverAc,
impl Display for QuantifiedExpander {
QuantifiedExpander::Native => write!(f, "native"),
QuantifiedExpander::ViaSolver => write!(f, "via-solver"),
QuantifiedExpander::ViaSolverAc => write!(f, "via-solver-ac"),
impl FromStr for QuantifiedExpander {
"native" => Ok(QuantifiedExpander::Native),
"via-solver" => Ok(QuantifiedExpander::ViaSolver),
"via-solver-ac" => Ok(QuantifiedExpander::ViaSolverAc),
_ => Err(format!(
"unknown comprehension expander: {s}; expected one of: \
native, via-solver, via-solver-ac"
/// Thread-local setting for which comprehension expansion strategy is currently active.
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| {
bug!(
"comprehension expander not set for this thread; call set_comprehension_expander first"
)
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Default, Serialize, Deserialize, JsonSchema)]
pub enum SatEncoding {
Log,
Direct,
Order,
impl SatEncoding {
pub const fn as_str(self) -> &'static str {
SatEncoding::Log => "log",
SatEncoding::Direct => "direct",
SatEncoding::Order => "order",
pub const fn as_rule_set(self) -> &'static str {
SatEncoding::Log => "SAT_Log",
SatEncoding::Direct => "SAT_Direct",
SatEncoding::Order => "SAT_Order",
impl Display for SatEncoding {
SatEncoding::Log => write!(f, "log"),
SatEncoding::Direct => write!(f, "direct"),
SatEncoding::Order => write!(f, "order"),
impl FromStr for SatEncoding {
"log" => Ok(SatEncoding::Log),
"direct" => Ok(SatEncoding::Direct),
"order" => Ok(SatEncoding::Order),
"unknown sat-encoding: {other}; expected one of: log, direct, order"
#[derive(
Debug,
EnumIter,
StrumDisplay,
PartialEq,
Eq,
Hash,
Clone,
Copy,
Serialize,
Deserialize,
JsonSchema,
)]
pub enum SolverFamily {
Minion,
Sat(SatEncoding),
Smt(TheoryConfig),
/// Thread-local setting for which solver family is currently active.
static CURRENT_SOLVER_FAMILY: Cell<Option<SolverFamily>> = const { Cell::new(None) };
pub const DEFAULT_MINION_DISCRETE_THRESHOLD: usize = 10;
/// 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<usize> =
const { Cell::new(DEFAULT_MINION_DISCRETE_THRESHOLD) };
pub fn set_current_solver_family(solver_family: SolverFamily) {
CURRENT_SOLVER_FAMILY.with(|current| current.set(Some(solver_family)));
pub fn current_solver_family() -> SolverFamily {
CURRENT_SOLVER_FAMILY.with(|current| {
"current solver family not set for this thread; call set_current_solver_family first"
pub fn set_minion_discrete_threshold(threshold: usize) {
MINION_DISCRETE_THRESHOLD.with(|current| current.set(threshold));
pub fn minion_discrete_threshold() -> usize {
MINION_DISCRETE_THRESHOLD.with(|current| current.get())
impl FromStr for SolverFamily {
let s = s.trim().to_ascii_lowercase();
match s.as_str() {
"minion" => Ok(SolverFamily::Minion),
"sat" | "sat-log" => Ok(SolverFamily::Sat(SatEncoding::Log)),
"sat-direct" => Ok(SolverFamily::Sat(SatEncoding::Direct)),
"sat-order" => Ok(SolverFamily::Sat(SatEncoding::Order)),
"smt" => Ok(SolverFamily::Smt(TheoryConfig::default())),
other => {
// allow forms like `smt-bv-atomic` or `smt-lia-arrays`
if other.starts_with("smt-") {
let parts = other.split('-').skip(1);
let mut ints = IntTheory::default();
let mut matrices = MatrixTheory::default();
let mut unwrap_alldiff = false;
for token in parts {
match token {
"" => {}
"lia" => ints = IntTheory::Lia,
"bv" => ints = IntTheory::Bv,
"arrays" => matrices = MatrixTheory::Arrays,
"atomic" => matrices = MatrixTheory::Atomic,
"nodiscrete" => unwrap_alldiff = true,
other_token => {
return Err(format!(
"unknown SMT theory option '{other_token}', must be one of bv|lia|arrays|atomic|nodiscrete"
));
return Ok(SolverFamily::Smt(TheoryConfig {
ints,
matrices,
unwrap_alldiff,
}));
Err(format!(
"unknown solver family '{other}', expected one of: minion, sat-log, sat-direct, sat-order, smt[(bv|lia)-(arrays|atomic)][-nodiscrete]"
))
impl SolverFamily {
pub fn as_str(&self) -> String {
SolverFamily::Minion => "minion".to_owned(),
SolverFamily::Sat(encoding) => format!("sat-{}", encoding.as_str()),
SolverFamily::Smt(theory_config) => format!("smt-{}", theory_config.as_str()),
#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]
pub struct SolverArgs {
pub timeout_ms: Option<u64>,