conjure_cp_core/
settings.rs

1use std::{fmt::Display, str::FromStr};
2
3use schemars::JsonSchema;
4use serde::{Deserialize, Serialize};
5use strum_macros::{Display as StrumDisplay, EnumIter};
6
7#[cfg(feature = "smt")]
8use crate::solver::adaptors::smt::{IntTheory, MatrixTheory, TheoryConfig};
9
10#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Default)]
11pub enum Parser {
12    #[default]
13    TreeSitter,
14    ViaConjure,
15}
16
17impl Display for Parser {
18    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
19        match self {
20            Parser::TreeSitter => write!(f, "tree-sitter"),
21            Parser::ViaConjure => write!(f, "via-conjure"),
22        }
23    }
24}
25
26impl FromStr for Parser {
27    type Err = String;
28
29    fn from_str(s: &str) -> Result<Self, Self::Err> {
30        match s.trim().to_ascii_lowercase().as_str() {
31            "tree-sitter" => Ok(Parser::TreeSitter),
32            "via-conjure" => Ok(Parser::ViaConjure),
33            other => Err(format!(
34                "unknown parser: {other}; expected one of: tree-sitter, via-conjure"
35            )),
36        }
37    }
38}
39
40#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
41pub enum Rewriter {
42    Naive,
43    Morph,
44}
45
46impl Display for Rewriter {
47    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
48        match self {
49            Rewriter::Naive => write!(f, "naive"),
50            Rewriter::Morph => write!(f, "morph"),
51        }
52    }
53}
54
55impl FromStr for Rewriter {
56    type Err = String;
57
58    fn from_str(s: &str) -> Result<Self, Self::Err> {
59        match s.trim().to_ascii_lowercase().as_str() {
60            "naive" => Ok(Rewriter::Naive),
61            "morph" => Ok(Rewriter::Morph),
62            other => Err(format!(
63                "unknown rewriter: {other}; expected one of: naive, morph"
64            )),
65        }
66    }
67}
68
69#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
70pub enum QuantifiedExpander {
71    Native,
72    ViaSolver,
73    ViaSolverAc,
74}
75
76impl Display for QuantifiedExpander {
77    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
78        match self {
79            QuantifiedExpander::Native => write!(f, "native"),
80            QuantifiedExpander::ViaSolver => write!(f, "via-solver"),
81            QuantifiedExpander::ViaSolverAc => write!(f, "via-solver-ac"),
82        }
83    }
84}
85
86impl FromStr for QuantifiedExpander {
87    type Err = String;
88
89    fn from_str(s: &str) -> Result<Self, Self::Err> {
90        match s.trim().to_ascii_lowercase().as_str() {
91            "native" => Ok(QuantifiedExpander::Native),
92            "via-solver" => Ok(QuantifiedExpander::ViaSolver),
93            "via-solver-ac" => Ok(QuantifiedExpander::ViaSolverAc),
94            _ => Err(format!(
95                "unknown quantified expander: {s}; expected one of: \
96                 native, via-solver, via-solver-ac"
97            )),
98        }
99    }
100}
101
102impl QuantifiedExpander {
103    pub(crate) const fn as_u8(self) -> u8 {
104        match self {
105            QuantifiedExpander::Native => 0,
106            QuantifiedExpander::ViaSolver => 1,
107            QuantifiedExpander::ViaSolverAc => 2,
108        }
109    }
110
111    pub(crate) const fn from_u8(value: u8) -> Self {
112        match value {
113            0 => QuantifiedExpander::Native,
114            1 => QuantifiedExpander::ViaSolver,
115            2 => QuantifiedExpander::ViaSolverAc,
116            _ => QuantifiedExpander::Native,
117        }
118    }
119}
120
121#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Default, Serialize, Deserialize, JsonSchema)]
122pub enum SatEncoding {
123    #[default]
124    Log,
125    Direct,
126    Order,
127}
128
129impl SatEncoding {
130    pub const fn as_rule_set(self) -> &'static str {
131        match self {
132            SatEncoding::Log => "SAT_Log",
133            SatEncoding::Direct => "SAT_Direct",
134            SatEncoding::Order => "SAT_Order",
135        }
136    }
137}
138
139impl Display for SatEncoding {
140    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
141        match self {
142            SatEncoding::Log => write!(f, "log"),
143            SatEncoding::Direct => write!(f, "direct"),
144            SatEncoding::Order => write!(f, "order"),
145        }
146    }
147}
148
149impl FromStr for SatEncoding {
150    type Err = String;
151
152    fn from_str(s: &str) -> Result<Self, Self::Err> {
153        match s.trim().to_ascii_lowercase().as_str() {
154            "log" => Ok(SatEncoding::Log),
155            "direct" => Ok(SatEncoding::Direct),
156            "order" => Ok(SatEncoding::Order),
157            other => Err(format!(
158                "unknown sat-encoding: {other}; expected one of: log, direct, order"
159            )),
160        }
161    }
162}
163
164#[derive(
165    Debug,
166    EnumIter,
167    StrumDisplay,
168    PartialEq,
169    Eq,
170    Hash,
171    Clone,
172    Copy,
173    Serialize,
174    Deserialize,
175    JsonSchema,
176)]
177pub enum SolverFamily {
178    Minion,
179    Sat(SatEncoding),
180    #[cfg(feature = "smt")]
181    Smt(TheoryConfig),
182}
183
184impl FromStr for SolverFamily {
185    type Err = String;
186
187    fn from_str(s: &str) -> Result<Self, Self::Err> {
188        let s = s.trim().to_ascii_lowercase();
189
190        match s.as_str() {
191            "minion" => Ok(SolverFamily::Minion),
192            "sat" | "sat-log" => Ok(SolverFamily::Sat(SatEncoding::Log)),
193            "sat-direct" => Ok(SolverFamily::Sat(SatEncoding::Direct)),
194            "sat-order" => Ok(SolverFamily::Sat(SatEncoding::Order)),
195            #[cfg(feature = "smt")]
196            "smt" => Ok(SolverFamily::Smt(TheoryConfig::default())),
197            other => {
198                // allow forms like `smt-bv-atomic` or `smt-lia-arrays`
199                #[cfg(feature = "smt")]
200                if other.starts_with("smt-") {
201                    let parts = other.split('-').skip(1);
202                    let mut ints = IntTheory::default();
203                    let mut matrices = MatrixTheory::default();
204                    let mut unwrap_alldiff = false;
205
206                    for token in parts {
207                        match token {
208                            "" => {}
209                            "lia" => ints = IntTheory::Lia,
210                            "bv" => ints = IntTheory::Bv,
211                            "arrays" => matrices = MatrixTheory::Arrays,
212                            "atomic" => matrices = MatrixTheory::Atomic,
213                            "nodiscrete" => unwrap_alldiff = true,
214                            other_token => {
215                                return Err(format!(
216                                    "unknown SMT theory option '{other_token}', must be one of bv|lia|arrays|atomic|nodiscrete"
217                                ));
218                            }
219                        }
220                    }
221
222                    return Ok(SolverFamily::Smt(TheoryConfig {
223                        ints,
224                        matrices,
225                        unwrap_alldiff,
226                    }));
227                }
228                Err(format!(
229                    "unknown solver family '{other}', expected one of: minion, sat-log, sat-direct, sat-order, smt[(bv|lia)-(arrays|atomic)][-nodiscrete]"
230                ))
231            }
232        }
233    }
234}
235
236impl SolverFamily {
237    pub const fn as_str(&self) -> &'static str {
238        match self {
239            SolverFamily::Minion => "minion",
240            SolverFamily::Sat(_) => "sat",
241            #[cfg(feature = "smt")]
242            SolverFamily::Smt(_) => "smt",
243        }
244    }
245}
246
247#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]
248pub struct SolverArgs {
249    pub timeout_ms: Option<u64>,
250}
conjure_cp_core/settings.rs

conjure_cp_core/
settings.rs
