taco_smt_encoder/
lib.rs

1//! Interface to interact with SMT solvers
2//!
3//! The module mostly reuses the [easy-smt](https://crates.io/crates/easy-smt)
4//! crate to interact with the SMT solvers. Easy-smt starts SMT solvers by
5//! starting the SMT solver as a subprocess in interactive mode.
6//! This crate provides a higher-level interface to encode boolean expressions
7//! and utility functions to start and configure popular SMT solvers.
8
9use core::{error, fmt};
10use std::{io::Write, process::Command};
11
12use easy_smt::{Context, ContextBuilder};
13use expression_encoding::SMTSolverError;
14use log::{debug, error, trace, warn};
15
16#[cfg(feature = "config_deserialize")]
17use serde::Deserialize;
18
19pub mod expression_encoding;
20
21/// Z3 command
22pub const Z3_PRG: &str = "z3";
23/// Option to set Z3 in SMT-LIB2 language and interactive mode
24pub const Z3_ARGS: [&str; 3] = ["-smt2", "-in", "-v:0"];
25
26/// cvc5 command
27pub const CVC5_PRG: &str = "cvc5";
28/// Option to set CVC5 in quiet mode, use SMT-LIB2 language and force logic to LIA
29pub const CVC5_ARGS: [&str; 3] = ["--quiet", "--lang=smt2", "--incremental"];
30
31/// Interface to interact with SMT solver
32///
33/// This type is an alias for the `easy_smt::Context` type. See
34/// [easy-smt](https://crates.io/crates/easy-smt) for more information.
35pub type SMTSolver = Context;
36
37/// SMT expression
38///
39/// This type is an alias for the [`easy_smt::SExpr`] type.
40pub type SMTExpr = easy_smt::SExpr;
41
42/// Type for functions that check the compatibility of the SMT solver version
43///
44/// This function takes the version of the SMT solver as a tuple of major, minor
45/// and patch version.
46///
47/// The function should take care of warning the user if the version is not
48/// compatible with the current version of the library. Warnings should be
49/// output using the `warn` or `error` macros from the `log` crate.
50type CompatibilityCheck = fn((i32, i32, i32));
51
52/// Configuration for a [`SMTSolverBuilder`]
53#[derive(Debug, Clone)]
54#[cfg_attr(feature = "config_deserialize", derive(Deserialize))]
55pub struct SMTSolverBuilderCfg {
56    /// Command to start the SMT solver
57    command: String,
58    /// Arguments to pass to the SMT solver command
59    #[cfg_attr(feature = "config_deserialize", serde(default))]
60    args: Vec<String>,
61    /// Options to configure in the SMT solver
62    #[cfg_attr(feature = "config_deserialize", serde(default))]
63    opts: Vec<SMTSolverOption>,
64    /// Sets the logic explicitly to `LIA`
65    #[cfg_attr(feature = "config_deserialize", serde(default = "default_set_lia"))]
66    set_lia: bool,
67    /// Function to check version compatibility of the SMT solver
68    #[cfg_attr(feature = "config_deserialize", serde(skip))]
69    check_version: Option<CompatibilityCheck>,
70}
71
72impl PartialEq for SMTSolverBuilderCfg {
73    /// Ignore the concrete function behind check version
74    fn eq(&self, other: &Self) -> bool {
75        self.command == other.command
76            && self.args == other.args
77            && self.opts == other.opts
78            && self.set_lia == other.set_lia
79            && self.check_version.is_some() == other.check_version.is_some()
80    }
81}
82
83/// Function to get the default value for the `set_lia` field
84#[cfg(feature = "config_deserialize")]
85fn default_set_lia() -> bool {
86    false
87}
88
89impl SMTSolverBuilderCfg {
90    /// Create a new SMT solver builder configuration
91    ///
92    /// This function takes the command to start the SMT solver, the arguments
93    /// to pass to the SMT solver, and the options to pass to the SMT solver.
94    ///
95    /// Additionally, it takes a boolean value to set the logic explicitly to
96    /// linear integer arithmetic (LIA).
97    ///
98    /// Note that the SMT solver must be started in interactive
99    /// REPL mode and accept input in the
100    /// [SMT-LIB2](https://smtlib.cs.uiowa.edu) format.
101    pub fn new(
102        command: String,
103        args: Vec<String>,
104        opts: Vec<SMTSolverOption>,
105        set_lia: bool,
106    ) -> Self {
107        Self {
108            command,
109            args,
110            opts,
111            set_lia,
112            check_version: None,
113        }
114    }
115
116    /// Get the default configuration for the Z3 SMT solver
117    pub fn new_z3() -> Self {
118        let opts = Vec::new();
119
120        Self {
121            command: Z3_PRG.to_string(),
122            args: Z3_ARGS.iter().map(|s| s.to_string()).collect(),
123            opts,
124            set_lia: true,
125            check_version: None,
126        }
127    }
128
129    /// Get the default configuration for the CVC5 SMT solver
130    pub fn new_cvc5() -> Self {
131        let check_version = |version: (i32, i32, i32)| {
132            if version.0 <= 1 && version.1 < 1 {
133                warn!(
134                    "Detected cvc5 < v1.1.0 (cvc5 is version {}.{}.{}). This version is not officially supported !",
135                    version.0, version.1, version.2
136                )
137            }
138        };
139
140        Self {
141            command: CVC5_PRG.to_string(),
142            args: CVC5_ARGS.iter().map(|s| s.to_string()).collect(),
143            opts: vec![],
144            set_lia: true,
145            check_version: Some(check_version),
146        }
147    }
148}
149
150/// Error that can occur when creating a new [`SMTSolverBuilder`]
151#[derive(Debug, PartialEq, Clone)]
152pub enum SMTSolverBuilderError {
153    /// The SMT solver seems to not be installed
154    NotInstalled(String),
155}
156
157impl fmt::Display for SMTSolverBuilderError {
158    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> fmt::Result {
159        match self {
160            SMTSolverBuilderError::NotInstalled(s) => {
161                write!(f, "SMT solver {s} is not installed")
162            }
163        }
164    }
165}
166
167impl error::Error for SMTSolverBuilderError {}
168
169/// Trait for types that can provide an [`SMTSolverBuilderCfg`]
170pub trait ProvidesSMTSolverBuilderCfg {
171    /// Get the [`SMTSolverBuilderCfg`]
172    fn get_smt_solver_builder_cfg(&self) -> &SMTSolverBuilderCfg;
173}
174
175impl ProvidesSMTSolverBuilderCfg for SMTSolverBuilderCfg {
176    fn get_smt_solver_builder_cfg(&self) -> &SMTSolverBuilderCfg {
177        self
178    }
179}
180
181/// Builder to create new [`SMTSolver`] instances
182///
183/// This builder can be used to create new SMT solver instances. Each new
184/// instance will be using a separate solver process.
185#[derive(Debug, Clone, PartialEq)]
186pub struct SMTSolverBuilder {
187    command: String,
188    args: Vec<String>,
189    opts: Vec<SMTSolverOption>,
190    set_lia: bool,
191}
192
193impl SMTSolverBuilder {
194    /// Create a new [`SMTSolverBuilder`] with the given configuration
195    pub fn new(cfg: &SMTSolverBuilderCfg) -> Result<Self, SMTSolverBuilderError> {
196        let version = get_smt_solver_version(&cfg.command);
197        match version {
198            Ok(version) => {
199                trace!(
200                    "SMT solver {} version {}.{}.{} found",
201                    cfg.command, version.0, version.1, version.2
202                );
203
204                if let Some(check_version) = cfg.check_version {
205                    check_version(version);
206                }
207            }
208            Err(e) => match e {
209                GetVersionError::NotInstalled(_) => {
210                    return Err(SMTSolverBuilderError::NotInstalled(cfg.command.clone()));
211                }
212                GetVersionError::ParseVersionError => {
213                    warn!("Failed to parse version of SMT solver {}", cfg.command);
214                }
215            },
216        }
217
218        Ok(Self {
219            command: cfg.command.clone(),
220            args: cfg.args.clone(),
221            opts: cfg.opts.clone(),
222            set_lia: cfg.set_lia,
223        })
224    }
225
226    /// Create a new [`SMTSolver`] instance
227    pub fn new_solver(&self) -> SMTSolver {
228        trace!("Creating new solver instance of {}", self.command);
229        let mut builder = ContextBuilder::new();
230
231        if !self.command.is_empty() {
232            builder.solver(&self.command).solver_args(&self.args);
233        }
234
235        let mut solver = builder.build().unwrap_or_else(|_| {
236            panic!(
237                "Failed to start interactive session with SMT solver. Command: {}",
238                self.command
239            )
240        });
241
242        for opt in self.opts.iter() {
243            debug!("Applying SMT solver option {opt}");
244            opt.apply_option(&mut solver);
245        }
246
247        if self.set_lia {
248            debug!("Setting SMT solver logic to quantifier free LIA");
249            solver
250                .set_logic("LIA")
251                .expect("Failed to set logic `LIA` in the SMT solver.");
252        }
253
254        solver
255    }
256
257    /// Create a new [`SMTSolver`] instance with a replay file recoding all
258    /// interactions with the SMT solver
259    pub fn new_solver_with_replay<W>(&mut self, replay_file: W) -> SMTSolver
260    where
261        W: Write + 'static + Send,
262    {
263        trace!("Creating new solver instance of {}", self.command);
264        let mut builder = ContextBuilder::new();
265        builder.replay_file(Some(replay_file));
266        builder.solver(&self.command).solver_args(&self.args);
267
268        let mut solver = builder.build().unwrap_or_else(|_| {
269            panic!(
270                "Failed to start interactive session with SMT solver. Command: {}",
271                self.command
272            )
273        });
274
275        for opt in self.opts.iter() {
276            opt.apply_option(&mut solver);
277        }
278
279        if self.set_lia {
280            debug!("Setting SMT solver logic to LIA");
281            solver
282                .set_logic("LIA")
283                .expect("Failed to set logic `LIA` in the SMT solver.");
284        }
285
286        solver
287    }
288
289    /// Builder to automatically select a supported SMT solver
290    ///
291    /// This builder will try to start the CVC5 solver first, and if that fails, it
292    /// will try to start the Z3 solver. If both fail, it will panic.
293    pub fn new_automatic_selection() -> Result<Self, SMTSolverBuilderError> {
294        if let Ok(z3) = SMTSolverBuilder::new(&SMTSolverBuilderCfg::new_z3()) {
295            Ok(z3)
296        } else if let Ok(cvc5) = SMTSolverBuilder::new(&SMTSolverBuilderCfg::new_cvc5()) {
297            Ok(cvc5)
298        } else {
299            Err(SMTSolverBuilderError::NotInstalled(
300                "No supported SMT solver found".to_string(),
301            ))
302        }
303    }
304}
305
306impl Default for SMTSolverBuilder {
307    /// Create a new [`SMTSolverBuilder`] which will automatically try to select
308    /// a supported SMT solver, if one is installed on the system.
309    fn default() -> Self {
310        SMTSolverBuilder::new_automatic_selection()
311            .expect("Failed to create default SMT solver builder. No SMT solver found.")
312    }
313}
314
315/// Trait for structures provide [`SMTSolverBuilder`]s
316///
317/// This trait should be implemented by any type that can supply a model checker
318/// with a configured SMT solver builder. This is useful for model checking
319/// contexts that hold additional configuration such as for example BDD library
320/// configuration.
321pub trait ProvidesSMTSolverBuilder {
322    /// Get the configured [`SMTSolverBuilder`]
323    fn get_solver_builder(&self) -> SMTSolverBuilder;
324}
325
326impl ProvidesSMTSolverBuilder for SMTSolverBuilder {
327    fn get_solver_builder(&self) -> SMTSolverBuilder {
328        self.clone()
329    }
330}
331
332/// Type for options that can be supplied to an SMT solver
333#[derive(Debug, Clone, PartialEq)]
334#[cfg_attr(feature = "config_deserialize", derive(Deserialize))]
335pub enum SMTSolverOption {
336    /// Option with boolean value
337    BooleanOption {
338        /// Name of the option
339        name: String,
340        /// Value to set the option to
341        value: bool,
342    },
343    /// Option with unsigned integer value
344    UnsignedIntOption {
345        /// Name of the option
346        name: String,
347        /// Value to set the option to
348        value: u32,
349    },
350}
351
352impl SMTSolverOption {
353    /// Create a new boolean [`SMTSolverOption`]
354    pub fn new_boolean_opt(name: String, value: bool) -> Self {
355        Self::BooleanOption { name, value }
356    }
357
358    /// Create a new integer  [`SMTSolverOption`]
359    pub fn new_integer_opt(name: String, value: u32) -> Self {
360        Self::UnsignedIntOption { name, value }
361    }
362
363    /// Apply option to the SMT solver
364    pub fn apply_option(&self, solver: &mut SMTSolver) {
365        match self {
366            SMTSolverOption::BooleanOption { name, value } => {
367                trace!("Setting SMT solver option {name} to {value}");
368                let value = if *value {
369                    solver.true_()
370                } else {
371                    solver.false_()
372                };
373
374                let res = solver.set_option(name, value);
375
376                if let Err(e) = res {
377                    error!("Failed to set option {} in SMT solver ! Error: {}", name, e);
378                }
379            }
380            SMTSolverOption::UnsignedIntOption { name, value } => {
381                trace!("Setting SMT solver option {name} to {value}");
382                let value = solver.numeral(*value);
383                let res = solver.set_option(name, value);
384
385                if let Err(e) = res {
386                    error!("Failed to set option {} in SMT solver ! Error: {}", name, e);
387                }
388            }
389        }
390    }
391}
392
393impl fmt::Display for SMTSolverOption {
394    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
395        match self {
396            SMTSolverOption::BooleanOption { name, value } => write!(f, "{name} : {value}"),
397            SMTSolverOption::UnsignedIntOption { name, value } => write!(f, "{name} : {value}"),
398        }
399    }
400}
401
402/// Trait indicating that the a type holds an [`SMTSolver`]
403///
404/// This trait should be implemented by any type that holds an SMT solver, i.e.
405/// a [`easy_smt::Context`] object. Implementing this trait will enable the type
406/// to encode SMT expressions and check their satisfiability using the SMT
407/// solver.
408pub trait SMTSolverContext {
409    /// Get a mutable reference to the SMT solver associated with this context
410    fn get_smt_solver_mut(&mut self) -> &mut SMTSolver;
411
412    /// Get the SMT solver associated with this context
413    fn get_smt_solver(&self) -> &SMTSolver;
414
415    /// Check the satisfiability of the given [`SMTExpr`]
416    fn assert_and_check_expr(&mut self, expr: SMTExpr) -> Result<SMTSolution, SMTSolverError> {
417        self.get_smt_solver_mut().assert(expr)?;
418        let res = self.get_smt_solver_mut().check()?;
419
420        match res {
421            easy_smt::Response::Sat => Ok(SMTSolution::SAT),
422            easy_smt::Response::Unsat => Ok(SMTSolution::UNSAT),
423            easy_smt::Response::Unknown => Err(SMTSolverError::SolverTimeout),
424        }
425    }
426}
427
428impl SMTSolverContext for SMTSolver {
429    fn get_smt_solver_mut(&mut self) -> &mut SMTSolver {
430        self
431    }
432
433    fn get_smt_solver(&self) -> &SMTSolver {
434        self
435    }
436}
437
438/// Result of an SMT query
439#[derive(Debug, Clone, Copy, PartialEq)]
440pub enum SMTSolution {
441    /// Query was unsatisfiable
442    UNSAT,
443    /// Query was satisfiable
444    SAT,
445}
446
447impl SMTSolution {
448    /// Convert the SMT solution to a boolean
449    pub fn is_sat(&self) -> bool {
450        match self {
451            SMTSolution::SAT => true,
452            SMTSolution::UNSAT => false,
453        }
454    }
455}
456
457impl fmt::Display for SMTSolution {
458    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
459        match self {
460            SMTSolution::UNSAT => write!(f, "UNSAT"),
461            SMTSolution::SAT => write!(f, "SAT"),
462        }
463    }
464}
465
466/// Error that can occur when constructing a new SMT solver builder
467#[derive(Debug, PartialEq)]
468enum GetVersionError {
469    /// Solver does not seem to be installed
470    NotInstalled(String),
471    /// Failed to parse version out of output
472    ParseVersionError,
473}
474
475impl fmt::Display for GetVersionError {
476    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
477        match self {
478            GetVersionError::NotInstalled(s) => write!(
479                f,
480                "Execution of `{s} --version`  failed. This most likely means that the requested SMT solver is not installed."
481            ),
482            GetVersionError::ParseVersionError => write!(
483                f,
484                "Failed to parse version out of the output of `<SMT-SOLVER-COMMAND> --version`"
485            ),
486        }
487    }
488}
489
490impl error::Error for GetVersionError {}
491
492/// Calls solver and attempts to parse the version of the SMT solver that is used
493fn get_smt_solver_version(cmd: &str) -> Result<(i32, i32, i32), GetVersionError> {
494    let out = Command::new(cmd).arg("--version").output();
495    if out.is_err() {
496        return Err(GetVersionError::NotInstalled(cmd.to_owned()));
497    }
498    let out = out.unwrap();
499    if !out.status.success() {
500        return Err(GetVersionError::NotInstalled(cmd.to_owned()));
501    }
502
503    let out_str =
504        std::str::from_utf8(&out.stdout).map_err(|_| GetVersionError::ParseVersionError)?;
505    parse_smt_solver_version(out_str)
506}
507
508/// This function attempts to parse the version number from the output of the
509/// `--version` command.
510///
511/// Note that this function will return a `ParseVersionError` if the output does
512/// not contain the version in the form of "... version x.y.z ..."
513fn parse_smt_solver_version(version_output: &str) -> Result<(i32, i32, i32), GetVersionError> {
514    let version_prefix = "version ";
515    if let Some(start) = version_output.find(version_prefix) {
516        let start = start + version_prefix.len();
517        if let Some(end) = version_output[start..].find([' ', '\n', '\t']) {
518            let version_str = &version_output[start..start + end];
519            let parts: Vec<&str> = version_str.split('.').collect();
520            if parts.len() == 3
521                && let (Ok(major), Ok(minor), Ok(patch)) =
522                    (parts[0].parse(), parts[1].parse(), parts[2].parse())
523            {
524                return Ok((major, minor, patch));
525            }
526        }
527    }
528
529    debug!("Failed to parse SMT solver version from output: {version_output}");
530    Err(GetVersionError::ParseVersionError)
531}
532
533#[cfg(test)]
534mod tests {
535    use std::vec;
536
537    use easy_smt::Response;
538
539    use super::*;
540
541    fn test_solver_interaction(solver: &mut SMTSolver) {
542        let int_sort = solver.int_sort();
543        let x = solver.declare_const("x", int_sort).unwrap();
544
545        let constr = solver.and(
546            solver.lte(x, solver.numeral(2)),
547            solver.gt(x, solver.numeral(1)),
548        );
549        solver.assert(constr).unwrap();
550
551        assert_eq!(solver.check().unwrap(), Response::Sat);
552
553        let solution = solver.get_value(vec![x]).unwrap();
554        assert_eq!(solution.len(), 1);
555        assert_eq!(solution[0].0, x);
556        assert_eq!(solver.get_u64(solution[0].1).unwrap(), 2);
557    }
558
559    // Note: CVC5 smaller than 1.1.0 does not play nice with negative solutions
560    fn test_solver_supports_negative_solutions(solver: &mut SMTSolver) {
561        let int_sort = solver.int_sort();
562        let z = solver.declare_const("z", int_sort).unwrap();
563
564        let constr = solver.and(
565            solver.lte(z, solver.numeral(-1)),
566            solver.gt(z, solver.numeral(-2)),
567        );
568        solver.assert(constr).unwrap();
569
570        assert_eq!(solver.check().unwrap(), Response::Sat);
571
572        let solution = solver.get_value(vec![z]).unwrap();
573        assert_eq!(solution.len(), 1);
574        assert_eq!(solution[0].0, z);
575        assert_eq!(solver.get_i64(solution[0].1).unwrap(), -1);
576    }
577
578    #[test]
579    fn test_z3_solver() {
580        let builder = SMTSolverBuilder::new(&SMTSolverBuilderCfg::new_z3());
581        assert!(builder.is_ok());
582        let builder = builder.unwrap();
583
584        let mut solver = builder.new_solver();
585        test_solver_interaction(&mut solver);
586        test_solver_supports_negative_solutions(&mut solver);
587    }
588
589    #[test]
590    fn test_cvc5_solver() {
591        let builder = SMTSolverBuilder::new(&SMTSolverBuilderCfg::new_cvc5());
592        assert!(builder.is_ok());
593        let builder = builder.unwrap();
594
595        let mut solver = builder.new_solver();
596        test_solver_interaction(&mut solver);
597    }
598
599    #[test]
600    fn test_cvc5_parse_version_1() {
601        let out = "\
602This is cvc5 version 1.1.0 [git tag 1.1.0 branch HEAD]
603compiled with GCC version 11.4.0
604on Dec 21 2023 01:08:41
605
606Copyright (c) 2009-2023 by the authors and their institutional
607affiliations listed at https://cvc5.github.io/people.html
608
609cvc5 is open-source and is covered by the BSD license (modified).
610
611THIS SOFTWARE IS PROVIDED AS-IS, WITHOUT ANY WARRANTIES.
612USE AT YOUR OWN RISK.
613
614This version of cvc5 is linked against the following non-(L)GPL'ed
615third party libraries.
616
617  CaDiCaL - Simplified Satisfiability Solver
618  See https://github.com/arminbiere/cadical for copyright information.
619
620  Editline Library
621  See https://thrysoee.dk/editline
622  for copyright information.
623
624  SymFPU - The Symbolic Floating Point Unit
625  See https://github.com/martin-cs/symfpu/tree/CVC4 for copyright information.
626
627This version of cvc5 is linked against the following third party
628libraries covered by the LGPLv3 license.
629See licenses/lgpl-3.0.txt for more information.
630
631  GMP - Gnu Multi Precision Arithmetic Library
632  See http://gmplib.org for copyright information.
633
634  LibPoly polynomial library
635  See https://github.com/SRI-CSL/libpoly for copyright and
636  licensing information.
637
638cvc5 is statically linked against these libraries. To recompile
639this version of cvc5 with different versions of these libraries
640follow the instructions on https://github.com/cvc5/cvc5/blob/main/INSTALL.md
641
642See the file COPYING (distributed with the source code, and with
643all binaries) for the full cvc5 copyright, licensing, and (lack of)
644warranty information.
645";
646
647        let got = parse_smt_solver_version(out);
648        assert_eq!(got, Ok((1, 1, 0)))
649    }
650
651    #[test]
652    fn test_cvc5_parse_version_2() {
653        let out = "\
654This is cvc5 version 1.2.0
655compiled with GCC version 14.2.1 20240912 (Red Hat 14.2.1-3)
656on Sep 26 2024 00:00:00
657
658Copyright (c) 2009-2023 by the authors and their institutional
659affiliations listed at https://cvc5.github.io/people.html
660
661This build of cvc5 uses GPLed libraries, and is thus covered by
662the GNU General Public License (GPL) version 3.  Versions of cvc5
663are available that are covered by the (modified) BSD license. If
664you want to license cvc5 under this license, please configure cvc5
665with the \"--no-gpl\" option before building from sources.
666
667THIS SOFTWARE IS PROVIDED AS-IS, WITHOUT ANY WARRANTIES.
668USE AT YOUR OWN RISK.
669
670This version of cvc5 is linked against the following non-(L)GPL'ed
671third party libraries.
672
673  CaDiCaL - Simplified Satisfiability Solver
674  See https://github.com/arminbiere/cadical for copyright information.
675
676  CryptoMiniSat - An Advanced SAT Solver
677  See https://github.com/msoos/cryptominisat for copyright information.
678
679  Kissat - Simplified Satisfiability Solver
680  See https://fmv.jku.at/kissat for copyright information.
681
682  Editline Library
683  See https://thrysoee.dk/editline
684  for copyright information.
685
686  SymFPU - The Symbolic Floating Point Unit
687  See https://github.com/martin-cs/symfpu/tree/CVC4 for copyright information.
688
689This version of cvc5 is linked against the following third party
690libraries covered by the LGPLv3 license.
691See licenses/lgpl-3.0.txt for more information.
692
693  GMP - Gnu Multi Precision Arithmetic Library
694  See http://gmplib.org for copyright information.
695
696  LibPoly polynomial library
697  See https://github.com/SRI-CSL/libpoly for copyright and
698  licensing information.
699
700This version of cvc5 is linked against the following third party
701libraries covered by the GPLv3 license.
702See licenses/gpl-3.0.txt for more information.
703
704  CoCoALib - a computer algebra library
705  See https://cocoa.dima.unige.it/cocoa/cocoalib/index.shtml for copyright information
706
707See the file COPYING (distributed with the source code, and with
708all binaries) for the full cvc5 copyright, licensing, and (lack of)
709warranty information.
710";
711
712        let got = parse_smt_solver_version(out);
713        assert_eq!(got, Ok((1, 2, 0)))
714    }
715
716    #[test]
717    fn test_z3_parse_version() {
718        let out = "\
719Z3 version 4.8.12 - 64 bit";
720
721        let got = parse_smt_solver_version(out);
722        assert_eq!(got, Ok((4, 8, 12)))
723    }
724
725    #[test]
726    fn test_z3_get_version() {
727        let version = get_smt_solver_version(Z3_PRG);
728        assert!(version.is_ok());
729    }
730
731    #[test]
732    fn test_cvc5_get_version() {
733        let version = get_smt_solver_version(CVC5_PRG);
734        assert!(version.is_ok());
735    }
736
737    #[test]
738    fn test_automatic_solver_selection() {
739        let builder = SMTSolverBuilder::new_automatic_selection()
740            .expect("Failed to create default SMT solver builder. No SMT solver found.");
741
742        let mut solver = builder.new_solver();
743        test_solver_interaction(&mut solver);
744    }
745
746    #[test]
747    fn test_command_solver() {
748        let cvc5_args: Vec<String> = CVC5_ARGS.iter().map(|&s| s.to_string()).collect();
749
750        let cfg = SMTSolverBuilderCfg::new("cvc5".to_string(), cvc5_args.clone(), vec![], false);
751        let builder = SMTSolverBuilder::new(&cfg).unwrap();
752
753        let mut solver = builder.new_solver();
754        test_solver_interaction(&mut solver);
755
756        let second_builder = builder.clone();
757        assert_eq!(builder, second_builder);
758    }
759
760    #[test]
761    fn test_command_solver_set_lia() {
762        let cvc5_args: Vec<String> = CVC5_ARGS.iter().map(|&s| s.to_string()).collect();
763
764        let cfg = SMTSolverBuilderCfg::new("cvc5".to_string(), cvc5_args.clone(), vec![], true);
765        let builder = SMTSolverBuilder::new(&cfg).unwrap();
766
767        let mut solver = builder.new_solver();
768        test_solver_interaction(&mut solver);
769
770        let second_builder = builder.clone();
771        assert_eq!(builder, second_builder);
772    }
773
774    #[test]
775    #[should_panic]
776    fn test_panic_unknown_solver() {
777        let cfg = SMTSolverBuilderCfg::new("unknown_solver".to_string(), vec![], vec![], false);
778        let _builder = SMTSolverBuilder::new(&cfg).unwrap();
779    }
780
781    #[test]
782    fn display_solution() {
783        assert_eq!(SMTSolution::UNSAT.to_string(), "UNSAT");
784        assert_eq!(SMTSolution::SAT.to_string(), "SAT");
785    }
786
787    #[test]
788    fn test_is_sat() {
789        assert!(!SMTSolution::UNSAT.is_sat());
790        assert!(SMTSolution::SAT.is_sat());
791    }
792
793    #[test]
794    fn test_get_version_error_display() {
795        let err = GetVersionError::NotInstalled("cvc5".to_string());
796        assert_eq!(
797            err.to_string(),
798            "Execution of `cvc5 --version`  failed. This most likely means that the requested SMT solver is not installed."
799        );
800        let err = GetVersionError::ParseVersionError;
801        assert_eq!(
802            err.to_string(),
803            "Failed to parse version out of the output of `<SMT-SOLVER-COMMAND> --version`"
804        );
805        let err = GetVersionError::ParseVersionError;
806        assert_eq!(
807            err.to_string(),
808            "Failed to parse version out of the output of `<SMT-SOLVER-COMMAND> --version`"
809        );
810    }
811
812    #[test]
813    fn test_solver_option_display() {
814        let opt = SMTSolverOption::BooleanOption {
815            name: ":opt".to_string(),
816            value: true,
817        };
818        assert_eq!(opt.to_string(), ":opt : true");
819        let opt = SMTSolverOption::UnsignedIntOption {
820            name: ":opt".to_string(),
821            value: 42,
822        };
823        assert_eq!(opt.to_string(), ":opt : 42");
824    }
825
826    #[test]
827    fn test_new_solver_opt() {
828        let opt = SMTSolverOption::new_boolean_opt(":opt".to_string(), true);
829        assert_eq!(
830            opt,
831            SMTSolverOption::BooleanOption {
832                name: ":opt".to_string(),
833                value: true,
834            }
835        );
836        let opt = SMTSolverOption::new_integer_opt(":opt".to_string(), 42);
837        assert_eq!(
838            opt,
839            SMTSolverOption::UnsignedIntOption {
840                name: ":opt".to_string(),
841                value: 42,
842            }
843        );
844    }
845
846    #[test]
847    fn test_fmt_solver_builder_error() {
848        let err = SMTSolverBuilderError::NotInstalled("cvc5".to_string());
849        assert_eq!(err.to_string(), "SMT solver cvc5 is not installed");
850    }
851
852    #[test]
853    fn test_eq_smt_solver_builder_cfg() {
854        let cfg1 = SMTSolverBuilderCfg::new(
855            "cvc5".to_string(),
856            vec!["--quiet".to_string(), "--lang=smt2".to_string()],
857            vec![],
858            false,
859        );
860        let cfg2 = SMTSolverBuilderCfg::new(
861            "cvc5".to_string(),
862            vec!["--quiet".to_string(), "--lang=smt2".to_string()],
863            vec![],
864            false,
865        );
866        assert_eq!(cfg1, cfg2);
867
868        let cfg3 = SMTSolverBuilderCfg::new(
869            "z3".to_string(),
870            vec!["-smt2".to_string(), "-in".to_string(), "-v:0".to_string()],
871            vec![],
872            false,
873        );
874        assert_ne!(cfg1, cfg3);
875    }
876}
taco_smt_encoder/lib.rs

taco_smt_encoder/
lib.rs
