conjure_cp_core/
settings.rs

1use std::{cell::Cell, fmt::Display, str::FromStr};
2
3use schemars::JsonSchema;
4use serde::{Deserialize, Serialize};
5use strum_macros::{Display as StrumDisplay, EnumIter};
6
7use crate::bug;
8
9use crate::solver::adaptors::smt::{IntTheory, MatrixTheory, TheoryConfig};
10
11#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Default)]
12pub enum Parser {
13    #[default]
14    TreeSitter,
15    ViaConjure,
16}
17
18impl Display for Parser {
19    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
20        match self {
21            Parser::TreeSitter => write!(f, "tree-sitter"),
22            Parser::ViaConjure => write!(f, "via-conjure"),
23        }
24    }
25}
26
27impl FromStr for Parser {
28    type Err = String;
29
30    fn from_str(s: &str) -> Result<Self, Self::Err> {
31        match s.trim().to_ascii_lowercase().as_str() {
32            "tree-sitter" => Ok(Parser::TreeSitter),
33            "via-conjure" => Ok(Parser::ViaConjure),
34            other => Err(format!(
35                "unknown parser: {other}; expected one of: tree-sitter, via-conjure"
36            )),
37        }
38    }
39}
40
41thread_local! {
42    /// Thread-local setting for which parser is currently active.
43    ///
44    /// Must be explicitly set before use.
45    static CURRENT_PARSER: Cell<Option<Parser>> = const { Cell::new(None) };
46}
47
48pub fn set_current_parser(parser: Parser) {
49    CURRENT_PARSER.with(|current| current.set(Some(parser)));
50}
51
52pub fn current_parser() -> Parser {
53    CURRENT_PARSER.with(|current| {
54        current.get().unwrap_or_else(|| {
55            // loud failure on purpose, so we don't end up using the default
56            bug!("current parser not set for this thread; call set_current_parser first")
57        })
58    })
59}
60
61#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
62pub struct MorphConfig {
63    pub cache: MorphCachingStrategy,
64    pub prefilter: bool,
65    /// Use naive (no-levels) traversal (`morph_naive`). Enabled with `levelsoff`, disabled with `levelson`.
66    pub naive: bool,
67    pub fixedpoint: bool,
68}
69
70impl Default for MorphConfig {
71    fn default() -> Self {
72        Self {
73            cache: MorphCachingStrategy::NoCache,
74            prefilter: false,
75            naive: true,
76            fixedpoint: false,
77        }
78    }
79}
80
81impl Display for MorphConfig {
82    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
83        write!(f, "morph")?;
84
85        let mut features = Vec::new();
86        if !self.naive {
87            features.push("levelson");
88        }
89        match self.cache {
90            MorphCachingStrategy::NoCache => {}
91            MorphCachingStrategy::Cache => features.push("cache"),
92            MorphCachingStrategy::IncrementalCache => features.push("inccache"),
93        }
94        if self.prefilter {
95            features.push("prefilteron");
96        }
97        if self.fixedpoint {
98            features.push("fixedpoint");
99        }
100
101        if !features.is_empty() {
102            write!(f, "-{}", features.join("-"))?;
103        }
104
105        Ok(())
106    }
107}
108
109#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]
110pub enum MorphCachingStrategy {
111    NoCache,
112    Cache,
113    #[default]
114    IncrementalCache,
115}
116
117impl FromStr for MorphCachingStrategy {
118    type Err = String;
119
120    fn from_str(s: &str) -> Result<Self, Self::Err> {
121        match s.trim().to_ascii_lowercase().as_str() {
122            "no-cache" => Ok(Self::NoCache),
123            "cache" => Ok(Self::Cache),
124            "inc-cache" => Ok(Self::IncrementalCache),
125            other => Err(format!(
126                "unknown cache strategy: {other}; expected one of: no-cache, cahce, inc-cache"
127            )),
128        }
129    }
130}
131
132impl Display for MorphCachingStrategy {
133    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
134        match self {
135            MorphCachingStrategy::NoCache => write!(f, "nocache"),
136            MorphCachingStrategy::Cache => write!(f, "cache"),
137            MorphCachingStrategy::IncrementalCache => write!(f, "inccache"),
138        }
139    }
140}
141
142#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
143pub enum Rewriter {
144    Naive,
145    Morph(MorphConfig),
146}
147
148thread_local! {
149    /// Thread-local setting for which rewriter is currently active.
150    ///
151    /// Must be explicitly set before use.
152    static CURRENT_REWRITER: Cell<Option<Rewriter>> = const { Cell::new(None) };
153}
154
155impl Display for Rewriter {
156    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
157        match self {
158            Rewriter::Naive => write!(f, "naive"),
159            Rewriter::Morph(config) => write!(f, "{config}"),
160        }
161    }
162}
163
164impl FromStr for Rewriter {
165    type Err = String;
166
167    fn from_str(s: &str) -> Result<Self, Self::Err> {
168        let trimmed = s.trim().to_ascii_lowercase();
169        match trimmed.as_str() {
170            "naive" => Ok(Rewriter::Naive),
171            "morph" => Ok(Rewriter::Morph(MorphConfig::default())),
172            other => {
173                if !other.starts_with("morph-") {
174                    return Err(format!(
175                        "unknown rewriter: {other}; expected one of: naive, morph, morph-[levelson]-[cache|inccache]-[prefilteron]-[fixedpoint]"
176                    ));
177                }
178
179                let parts = other.split('-').skip(1);
180                Ok(Rewriter::Morph(parse_morph_config_tokens(parts)?))
181            }
182        }
183    }
184}
185
186fn parse_morph_config_tokens<'a>(
187    tokens: impl IntoIterator<Item = &'a str>,
188) -> Result<MorphConfig, String> {
189    let mut config = MorphConfig::default();
190    let mut cache_set = false;
191    let mut levels_set = false;
192    let mut prefilter_set = false;
193
194    for token in tokens {
195        match token {
196            "" => (),
197            "levelson" => {
198                if levels_set {
199                    return Err(
200                        "conflicting levels options: only one levels setting is allowed"
201                            .to_string(),
202                    );
203                }
204                config.naive = false;
205                levels_set = true;
206            }
207            "cache" | "inccache" => {
208                if cache_set {
209                    return Err(
210                        "conflicting cache options: only one of cache|inccache is allowed"
211                            .to_string(),
212                    );
213                }
214                config.cache = match token {
215                    "cache" => MorphCachingStrategy::Cache,
216                    "inccache" => MorphCachingStrategy::IncrementalCache,
217                    _ => unreachable!(),
218                };
219                cache_set = true;
220            }
221            "prefilteron" => {
222                if prefilter_set {
223                    return Err(
224                        "conflicting prefilter options: only one prefilter setting is allowed"
225                            .to_string(),
226                    );
227                }
228                config.prefilter = true;
229                prefilter_set = true;
230            }
231            "fixedpoint" => {
232                config.fixedpoint = true;
233            }
234            other_token => {
235                return Err(format!(
236                    "unknown morph option '{other_token}', must be one of levelson|cache|inccache|prefilteron|fixedpoint"
237                ));
238            }
239        }
240    }
241
242    Ok(config)
243}
244
245pub fn set_current_rewriter(rewriter: Rewriter) {
246    CURRENT_REWRITER.with(|current| current.set(Some(rewriter)));
247}
248
249pub fn current_rewriter() -> Rewriter {
250    CURRENT_REWRITER.with(|current| {
251        current.get().unwrap_or_else(|| {
252            // loud failure on purpose, so we don't end up using the default
253            bug!("current rewriter not set for this thread; call set_current_rewriter first")
254        })
255    })
256}
257
258#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
259pub enum QuantifiedExpander {
260    Native,
261    ViaSolver,
262    ViaSolverAc,
263}
264
265impl Display for QuantifiedExpander {
266    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
267        match self {
268            QuantifiedExpander::Native => write!(f, "native"),
269            QuantifiedExpander::ViaSolver => write!(f, "via-solver"),
270            QuantifiedExpander::ViaSolverAc => write!(f, "via-solver-ac"),
271        }
272    }
273}
274
275impl FromStr for QuantifiedExpander {
276    type Err = String;
277
278    fn from_str(s: &str) -> Result<Self, Self::Err> {
279        match s.trim().to_ascii_lowercase().as_str() {
280            "native" => Ok(QuantifiedExpander::Native),
281            "via-solver" => Ok(QuantifiedExpander::ViaSolver),
282            "via-solver-ac" => Ok(QuantifiedExpander::ViaSolverAc),
283            _ => Err(format!(
284                "unknown comprehension expander: {s}; expected one of: \
285                 native, via-solver, via-solver-ac"
286            )),
287        }
288    }
289}
290
291thread_local! {
292    /// Thread-local setting for which comprehension expansion strategy is currently active.
293    ///
294    /// Must be explicitly set before use.
295    static COMPREHENSION_EXPANDER: Cell<Option<QuantifiedExpander>> = const { Cell::new(None) };
296}
297
298pub fn set_comprehension_expander(expander: QuantifiedExpander) {
299    COMPREHENSION_EXPANDER.with(|current| current.set(Some(expander)));
300}
301
302pub fn comprehension_expander() -> QuantifiedExpander {
303    COMPREHENSION_EXPANDER.with(|current| {
304        current.get().unwrap_or_else(|| {
305            // loud failure on purpose, so we don't end up using the default
306            bug!(
307                "comprehension expander not set for this thread; call set_comprehension_expander first"
308            )
309        })
310    })
311}
312
313#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Default, Serialize, Deserialize, JsonSchema)]
314pub enum SatEncoding {
315    #[default]
316    Log,
317    Direct,
318    Order,
319}
320
321impl SatEncoding {
322    pub const fn as_str(self) -> &'static str {
323        match self {
324            SatEncoding::Log => "log",
325            SatEncoding::Direct => "direct",
326            SatEncoding::Order => "order",
327        }
328    }
329
330    pub const fn as_rule_set(self) -> &'static str {
331        match self {
332            SatEncoding::Log => "SAT_Log",
333            SatEncoding::Direct => "SAT_Direct",
334            SatEncoding::Order => "SAT_Order",
335        }
336    }
337}
338
339impl Display for SatEncoding {
340    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
341        match self {
342            SatEncoding::Log => write!(f, "log"),
343            SatEncoding::Direct => write!(f, "direct"),
344            SatEncoding::Order => write!(f, "order"),
345        }
346    }
347}
348
349impl FromStr for SatEncoding {
350    type Err = String;
351
352    fn from_str(s: &str) -> Result<Self, Self::Err> {
353        match s.trim().to_ascii_lowercase().as_str() {
354            "log" => Ok(SatEncoding::Log),
355            "direct" => Ok(SatEncoding::Direct),
356            "order" => Ok(SatEncoding::Order),
357            other => Err(format!(
358                "unknown sat-encoding: {other}; expected one of: log, direct, order"
359            )),
360        }
361    }
362}
363
364#[derive(
365    Debug,
366    EnumIter,
367    StrumDisplay,
368    PartialEq,
369    Eq,
370    Hash,
371    Clone,
372    Copy,
373    Serialize,
374    Deserialize,
375    JsonSchema,
376)]
377pub enum SolverFamily {
378    Minion,
379    Sat(SatEncoding),
380    Smt(TheoryConfig),
381}
382
383thread_local! {
384    /// Thread-local setting for which solver family is currently active.
385    ///
386    /// Must be explicitly set before use.
387    static CURRENT_SOLVER_FAMILY: Cell<Option<SolverFamily>> = const { Cell::new(None) };
388}
389
390pub const DEFAULT_MINION_DISCRETE_THRESHOLD: usize = 10;
391
392thread_local! {
393    /// Thread-local setting controlling when Minion int domains are emitted as `DISCRETE`.
394    ///
395    /// If an int domain size is <= this threshold, the Minion adaptor uses `DISCRETE`; otherwise
396    /// it uses `BOUND`, unless another constraint requires `DISCRETE`.
397    static MINION_DISCRETE_THRESHOLD: Cell<usize> =
398        const { Cell::new(DEFAULT_MINION_DISCRETE_THRESHOLD) };
399
400    /// Thread-local setting controlling whether rule-trace outputs are active in this phase.
401    ///
402    /// This is intentionally off by default and can be disabled before solver-time rewrites so
403    /// follow-up dominance-blocking rewrites do not pollute the initial rewrite trace.
404    static RULE_TRACE_ENABLED: Cell<bool> = const { Cell::new(false) };
405
406    /// Thread-local setting controlling whether default rule traces are configured.
407    static DEFAULT_RULE_TRACE_ENABLED: Cell<bool> = const { Cell::new(false) };
408
409    /// Thread-local setting controlling whether verbose rule-attempt traces are configured.
410    static RULE_TRACE_VERBOSE_ENABLED: Cell<bool> = const { Cell::new(false) };
411
412    /// Thread-local setting controlling whether aggregate rule-application traces are configured.
413    static RULE_TRACE_AGGREGATES_ENABLED: Cell<bool> = const { Cell::new(false) };
414}
415
416pub fn set_current_solver_family(solver_family: SolverFamily) {
417    CURRENT_SOLVER_FAMILY.with(|current| current.set(Some(solver_family)));
418}
419
420pub fn current_solver_family() -> SolverFamily {
421    CURRENT_SOLVER_FAMILY.with(|current| {
422        current.get().unwrap_or_else(|| {
423            // loud failure on purpose, so we don't end up using the default
424            bug!(
425                "current solver family not set for this thread; call set_current_solver_family first"
426            )
427        })
428    })
429}
430
431pub fn set_minion_discrete_threshold(threshold: usize) {
432    MINION_DISCRETE_THRESHOLD.with(|current| current.set(threshold));
433}
434
435pub fn minion_discrete_threshold() -> usize {
436    MINION_DISCRETE_THRESHOLD.with(|current| current.get())
437}
438
439pub fn set_rule_trace_enabled(enabled: bool) {
440    RULE_TRACE_ENABLED.with(|current| current.set(enabled));
441}
442
443pub fn rule_trace_enabled() -> bool {
444    RULE_TRACE_ENABLED.with(|current| current.get())
445}
446
447pub fn set_default_rule_trace_enabled(enabled: bool) {
448    DEFAULT_RULE_TRACE_ENABLED.with(|current| current.set(enabled));
449}
450
451pub fn default_rule_trace_enabled() -> bool {
452    DEFAULT_RULE_TRACE_ENABLED.with(|current| current.get())
453}
454
455pub fn set_rule_trace_verbose_enabled(enabled: bool) {
456    RULE_TRACE_VERBOSE_ENABLED.with(|current| current.set(enabled));
457}
458
459pub fn rule_trace_verbose_enabled() -> bool {
460    RULE_TRACE_VERBOSE_ENABLED.with(|current| current.get())
461}
462
463pub fn set_rule_trace_aggregates_enabled(enabled: bool) {
464    RULE_TRACE_AGGREGATES_ENABLED.with(|current| current.set(enabled));
465}
466
467pub fn rule_trace_aggregates_enabled() -> bool {
468    RULE_TRACE_AGGREGATES_ENABLED.with(|current| current.get())
469}
470
471pub fn configured_rule_trace_enabled() -> bool {
472    default_rule_trace_enabled() || rule_trace_verbose_enabled() || rule_trace_aggregates_enabled()
473}
474
475impl FromStr for SolverFamily {
476    type Err = String;
477
478    fn from_str(s: &str) -> Result<Self, Self::Err> {
479        let s = s.trim().to_ascii_lowercase();
480
481        match s.as_str() {
482            "minion" => Ok(SolverFamily::Minion),
483            "sat" | "sat-log" => Ok(SolverFamily::Sat(SatEncoding::Log)),
484            "sat-direct" => Ok(SolverFamily::Sat(SatEncoding::Direct)),
485            "sat-order" => Ok(SolverFamily::Sat(SatEncoding::Order)),
486            "smt" => Ok(SolverFamily::Smt(TheoryConfig::default())),
487            other => {
488                // allow forms like `smt-bv-atomic` or `smt-lia-arrays`
489                if other.starts_with("smt-") {
490                    let parts = other.split('-').skip(1);
491                    let mut ints = IntTheory::default();
492                    let mut matrices = MatrixTheory::default();
493                    let mut unwrap_alldiff = false;
494
495                    for token in parts {
496                        match token {
497                            "" => {}
498                            "lia" => ints = IntTheory::Lia,
499                            "bv" => ints = IntTheory::Bv,
500                            "arrays" => matrices = MatrixTheory::Arrays,
501                            "atomic" => matrices = MatrixTheory::Atomic,
502                            "nodiscrete" => unwrap_alldiff = true,
503                            other_token => {
504                                return Err(format!(
505                                    "unknown SMT theory option '{other_token}', must be one of bv|lia|arrays|atomic|nodiscrete"
506                                ));
507                            }
508                        }
509                    }
510
511                    return Ok(SolverFamily::Smt(TheoryConfig {
512                        ints,
513                        matrices,
514                        unwrap_alldiff,
515                    }));
516                }
517                Err(format!(
518                    "unknown solver family '{other}', expected one of: minion, sat-log, sat-direct, sat-order, smt[(bv|lia)-(arrays|atomic)][-nodiscrete]"
519                ))
520            }
521        }
522    }
523}
524
525impl SolverFamily {
526    pub fn as_str(&self) -> String {
527        match self {
528            SolverFamily::Minion => "minion".to_owned(),
529            SolverFamily::Sat(encoding) => format!("sat-{}", encoding.as_str()),
530            SolverFamily::Smt(theory_config) => format!("smt-{}", theory_config.as_str()),
531        }
532    }
533}
534
535#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]
536pub struct SolverArgs {
537    pub timeout_ms: Option<u64>,
538}
conjure_cp_core/settings.rs

conjure_cp_core/
settings.rs
