rsmt2_zz/
conf.rs

1//! Solver configuration, contains backend-solver-specific info.
2//!
3//! Do **NOT** use wildcards when matching over `SmtStyle`. We want the code to fail to compile
4//! whenever we add a solver. Likewise, do not use `if let` with `SmtStyle`.
5
6use std::fmt;
7
8use crate::{SmtRes, Solver};
9
10use self::SmtStyle::*;
11
12/// A configuration item is either a keyword or unsupported.
13pub type ConfItem = Option<&'static str>;
14
15/// Value of an unsupported configuration item.
16#[inline]
17fn unsupported() -> ConfItem {
18    None
19}
20/// Keyword for a configuration item.
21#[inline]
22fn supported(keyword: &'static str) -> ConfItem {
23    Some(keyword)
24}
25
26/// Solver styles.
27///
28/// - [z3][z3]: full support
29/// - [cvc4][cvc4]: full support in theory, but only partially tested. Note that `get-value` is
30///   known to crash some versions of CVC4.
31/// - [yices 2][yices 2]: full support in theory, but only partially tested. Command `get-model`
32///   will only work on Yices 2 > `2.6.1`, and needs to be activated in [SmtConf][SmtConf] with
33///   [`conf.models()`](struct.SmtConf.html#method.models). To understand why, see
34///   <https://github.com/SRI-CSL/yices2/issues/162>.
35#[derive(Debug, Clone, Copy)]
36#[allow(dead_code)]
37pub enum SmtStyle {
38    /// Z3-style smt solver.
39    Z3,
40    /// CVC4-style smt solver.
41    ///
42    /// **NB**: CVC4 has only been partially tested at this point.
43    CVC4,
44    /// Yices-2-style smt solver.
45    ///
46    /// Yices 2 has only been partially tested at this point.
47    Yices2,
48}
49
50impl SmtStyle {
51    /// Default configuration for a solver style.
52    pub fn default(self) -> SmtConf {
53        let cmd = self.cmd();
54        match self {
55            Z3 => SmtConf {
56                style: self,
57                cmd,
58                options: vec!["-in".into(), "-smt2".into()],
59                models: true,
60                incremental: true,
61                parse_success: false,
62                unsat_cores: false,
63                check_sat_assuming: supported("check-sat-assuming"),
64            },
65            CVC4 => SmtConf {
66                style: self,
67                cmd,
68                options: vec![
69                    "-q".into(),
70                    "--interactive".into(),
71                    "--lang".into(),
72                    "smt2".into(),
73                ],
74                models: false,
75                incremental: false,
76                parse_success: false,
77                unsat_cores: false,
78                check_sat_assuming: unsupported(),
79            },
80            Yices2 => SmtConf {
81                style: self,
82                cmd,
83                options: vec![
84                    "--incremental".into(),
85                ],
86                models: false,
87                incremental: true,
88                parse_success: false,
89                unsat_cores: false,
90                check_sat_assuming: supported("check-sat-assuming"),
91            },
92        }
93    }
94
95    /// A solver style from a string.
96    #[allow(dead_code)]
97    pub fn of_str(s: &str) -> Option<Self> {
98        match s {
99            "z3" | "Z3" => Some(Z3),
100            "cvc4" | "CVC4" => Some(CVC4),
101            "Yices2" | "yices2" | "YICES2" | "Yices 2" | "yices 2" | "YICES 2" => Some(CVC4),
102            _ => None,
103        }
104    }
105    /// Legal string representations of solver styles.
106    #[allow(dead_code)]
107    pub fn str_keys() -> Vec<&'static str> {
108        vec![
109            "z3", "Z3", "cvc4", "CVC4", "Yices2", "yices2", "YICES2", "Yices 2", "yices 2",
110            "YICES 2",
111        ]
112    }
113
114    /// Default command for a solver style.
115    #[cfg(not(windows))]
116    pub fn cmd(self) -> String {
117        match self {
118            Z3 => "z3".to_string(),
119            CVC4 => "cvc4".to_string(),
120            Yices2 => "yices-smt2".to_string(),
121        }
122    }
123    /// Default command for a solver style.
124    #[cfg(windows)]
125    pub fn cmd(self) -> String {
126        match self {
127            Z3 => "z3.exe".to_string(),
128            CVC4 => "cvc4.exe".to_string(),
129            Yices2 => "yices-smt2.exe".to_string(),
130        }
131    }
132}
133
134impl fmt::Display for SmtStyle {
135    fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
136        match *self {
137            Z3 => write!(fmt, "z3"),
138            CVC4 => write!(fmt, "cvc4"),
139            Yices2 => write!(fmt, "yices2"),
140        }
141    }
142}
143
144/// Configuration and solver specific info.
145///
146/// - [z3][z3]: full support
147/// - [cvc4][cvc4]: full support in theory, but only partially tested. Note that `get-value` is
148///   known to crash some versions of CVC4.
149/// - [yices 2][yices 2]: full support in theory, but only partially tested. Command `get-model`
150///   will only work on Yices 2 > `2.6.1`, and needs to be activated in [SmtConf][SmtConf] with
151///   [`conf.models()`](struct.SmtConf.html#method.models). To understand why, see
152///   <https://github.com/SRI-CSL/yices2/issues/162>.
153#[derive(Debug, Clone)]
154pub struct SmtConf {
155    /// Solver style.
156    style: SmtStyle,
157    /// Solver command.
158    cmd: String,
159    /// Options to call the solver with.
160    options: Vec<String>,
161    /// Model production.
162    models: bool,
163    /// Incrementality.
164    incremental: bool,
165    /// Parse success.
166    parse_success: bool,
167    /// Triggers unsat-core production.
168    unsat_cores: bool,
169    /// Keyword for check-sat with assumptions.
170    check_sat_assuming: ConfItem,
171}
172
173impl SmtConf {
174    /// Creates a new z3-like solver configuration.
175    ///
176    /// # Examples
177    ///
178    /// ```rust
179    /// # use rsmt2::SmtConf ;
180    /// let conf = SmtConf::z3() ;
181    /// assert! {
182    ///     conf.get_cmd() == "z3" || conf.get_cmd() == "z3.exe"
183    /// }
184    /// ```
185    #[inline]
186    pub fn z3() -> Self {
187        Z3.default()
188    }
189
190    /// Creates a new cvc4-like solver configuration.
191    ///
192    /// # Examples
193    ///
194    /// ```rust
195    /// # use rsmt2::SmtConf ;
196    /// let conf = SmtConf::cvc4() ;
197    /// assert! {
198    ///     conf.get_cmd() == "cvc4" || conf.get_cmd() == "cvc4.exe"
199    /// }
200    /// ```
201    #[inline]
202    pub fn cvc4() -> Self {
203        CVC4.default()
204    }
205
206    /// Creates a new yices-2-like solver configuration.
207    ///
208    /// # Examples
209    ///
210    /// ```rust
211    /// # use rsmt2::SmtConf ;
212    /// let conf = SmtConf::yices_2() ;
213    /// assert! {
214    ///     conf.get_cmd() == "yices-smt2" || conf.get_cmd() == "yices-smt2.exe"
215    /// }
216    /// ```
217    #[inline]
218    pub fn yices_2() -> Self {
219        Yices2.default()
220    }
221
222    /// Spawns the solver.
223    ///
224    /// # Examples
225    ///
226    /// ```rust
227    /// # use rsmt2::SmtConf ;
228    /// let _solver = SmtConf::z3().spawn(()).unwrap() ;
229    /// ```
230    #[inline]
231    pub fn spawn<Parser>(self, parser: Parser) -> SmtRes<Solver<Parser>> {
232        Solver::new(self, parser)
233    }
234
235    /// Concise description of the underlying solver.
236    ///
237    /// # Examples
238    ///
239    /// ```rust
240    /// # use rsmt2::SmtConf ;
241    /// assert_eq! { SmtConf::z3().desc(), "z3" }
242    /// ```
243    #[inline]
244    pub fn desc(&self) -> &str {
245        match self.style {
246            Z3 => "z3",
247            CVC4 => "cvc4",
248            Yices2 => "yices2",
249        }
250    }
251
252    /// Model production flag.
253    pub fn get_models(&self) -> bool {
254        self.models
255    }
256    /// Activates model production.
257    pub fn models(&mut self) {
258        if self.models {
259            return ();
260        } else {
261            self.models = true
262        }
263        match self.style {
264            CVC4 => self.options.push("--produce-models".into()),
265            Yices2 => self.options.push("--smt2-model-format".into()),
266            Z3 => (),
267        }
268    }
269
270    /// Incrementality.
271    pub fn get_incremental(&self) -> bool {
272        self.incremental
273    }
274    /// Activates incrementality (push/pop, check-sat-assuming).
275    pub fn incremental(&mut self) {
276        if self.incremental {
277            return ();
278        } else {
279            self.incremental = true
280        }
281        match self.style {
282            CVC4 | Yices2 => self.options.push("--incremental".into()),
283            Z3 => (),
284        }
285    }
286
287    /// Solver command.
288    ///
289    /// # Examples
290    ///
291    /// ```rust
292    /// # use rsmt2::SmtConf ;
293    /// let conf = SmtConf::z3() ;
294    /// assert! {
295    ///     conf.get_cmd() == "z3" || conf.get_cmd() == "z3.exe"
296    /// }
297    /// ```
298    #[inline]
299    pub fn get_cmd(&self) -> &str {
300        &self.cmd
301    }
302
303    /// Options of the configuration.
304    ///
305    /// # Examples
306    ///
307    /// ```rust
308    /// # use rsmt2::SmtConf ;
309    /// assert_eq! {
310    ///     SmtConf::z3().get_options(), & [ "-in", "-smt2" ]
311    /// }
312    /// ```
313    #[inline]
314    pub fn get_options(&self) -> &[String] {
315        &self.options
316    }
317
318    /// Indicates if print success is active.
319    ///
320    /// # Examples
321    ///
322    /// ```rust
323    /// # use rsmt2::SmtConf ;
324    /// assert! { ! SmtConf::z3().get_print_success() }
325    /// ```
326    #[inline]
327    pub fn get_print_success(&self) -> bool {
328        self.parse_success
329    }
330
331    /// Indicates if unsat cores is active.
332    ///
333    /// # Examples
334    ///
335    /// ```rust
336    /// # use rsmt2::SmtConf ;
337    /// assert! { ! SmtConf::z3().get_unsat_cores() }
338    /// ```
339    #[inline]
340    pub fn get_unsat_cores(&self) -> bool {
341        self.unsat_cores
342    }
343
344    /// Keyword for check-sat with assumptions.
345    ///
346    /// # Examples
347    ///
348    /// ```rust
349    /// # use rsmt2::SmtConf ;
350    /// assert_eq! {
351    ///     SmtConf::z3().get_check_sat_assuming(), Some("check-sat-assuming")
352    /// }
353    /// ```
354    #[inline]
355    pub fn get_check_sat_assuming(&self) -> ConfItem {
356        self.check_sat_assuming.as_ref().map(|s| *s)
357    }
358
359    /// Adds an option to the configuration.
360    ///
361    /// # Examples
362    ///
363    /// ```rust
364    /// # use rsmt2::SmtConf ;
365    /// let mut conf = SmtConf::z3() ;
366    /// conf.option("arith.euclidean_solver=true") ;
367    /// assert_eq! {
368    ///     conf.get_options(),
369    ///     & [ "-in", "-smt2", "arith.euclidean_solver=true" ]
370    /// }
371    /// ```
372    #[inline]
373    pub fn option<S: Into<String>>(&mut self, o: S) -> &mut Self {
374        self.options.push(o.into());
375        self
376    }
377
378    /// Sets the command for the solver.
379    ///
380    /// # Examples
381    ///
382    /// ```rust
383    /// # use rsmt2::SmtConf ;
384    /// let mut conf = SmtConf::z3() ;
385    /// conf.cmd("my_custom_z3_command") ;
386    /// assert_eq! { conf.get_cmd(), "my_custom_z3_command" }
387    /// ```
388    #[inline]
389    pub fn cmd<S: Into<String>>(&mut self, cmd: S) -> &mut Self {
390        let cmd = cmd.into();
391        let mut iter = cmd.split(' ');
392
393        'set_cmd: while let Some(cmd) = iter.next() {
394            if !cmd.is_empty() {
395                self.cmd = cmd.into();
396                break 'set_cmd;
397            }
398        }
399
400        for option in iter {
401            if !option.is_empty() {
402                self.options.push(option.into())
403            }
404        }
405
406        self
407    }
408
409    /// Activates parse sucess.
410    ///
411    /// # Examples
412    ///
413    /// ```rust
414    /// # use rsmt2::SmtConf ;
415    /// let mut conf = SmtConf::z3() ;
416    /// conf.print_success() ;
417    /// assert! { conf.get_print_success() }
418    /// ```
419    #[inline]
420    #[cfg(not(no_parse_success))]
421    pub fn print_success(&mut self) {
422        self.parse_success = true
423    }
424
425    /// Activates unsat-core production.
426    ///
427    /// # Examples
428    ///
429    /// ```rust
430    /// # use rsmt2::SmtConf ;
431    /// let mut conf = SmtConf::z3() ;
432    /// conf.unsat_cores() ;
433    /// assert! { conf.get_unsat_cores() }
434    /// ```
435    #[inline]
436    pub fn unsat_cores(&mut self) {
437        self.unsat_cores = true
438    }
439}
440
441/// ## Solver-specific error-handling
442impl SmtConf {
443    /// Adds information to a `get-value` error message if needed.
444    pub fn enrich_get_values_error(&self, e: crate::errors::Error) -> crate::errors::Error {
445        match self.style {
446            SmtStyle::CVC4 => e.chain_err(|| {
447                "some versions of CVC4 produce errors on `get-value` commands, \
448                 consider using `get-model` instead"
449            }),
450            SmtStyle::Z3 | SmtStyle::Yices2 => e,
451        }
452    }
453}
rsmt2_zz/conf.rs

rsmt2_zz/
conf.rs
