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/// The version is the first whitespace-separated token of the form "x.y.z".
512/// Returns a `ParseVersionError` if no such token exists.
513fn parse_smt_solver_version(version_output: &str) -> Result<(i32, i32, i32), GetVersionError> {
514    for token in version_output.split_whitespace() {
515        let parts: Vec<&str> = token.split('.').collect();
516        if parts.len() == 3
517            && let (Ok(major), Ok(minor), Ok(patch)) =
518                (parts[0].parse(), parts[1].parse(), parts[2].parse())
519        {
520            return Ok((major, minor, patch));
521        }
522    }
523
524    debug!("Failed to parse SMT solver version from output: {version_output}");
525    Err(GetVersionError::ParseVersionError)
526}
527
528#[cfg(test)]
529mod tests {
530    use std::vec;
531
532    use easy_smt::Response;
533
534    use super::*;
535
536    fn test_solver_interaction(solver: &mut SMTSolver) {
537        let int_sort = solver.int_sort();
538        let x = solver.declare_const("x", int_sort).unwrap();
539
540        let constr = solver.and(
541            solver.lte(x, solver.numeral(2)),
542            solver.gt(x, solver.numeral(1)),
543        );
544        solver.assert(constr).unwrap();
545
546        assert_eq!(solver.check().unwrap(), Response::Sat);
547
548        let solution = solver.get_value(vec![x]).unwrap();
549        assert_eq!(solution.len(), 1);
550        assert_eq!(solution[0].0, x);
551        assert_eq!(solver.get_u64(solution[0].1).unwrap(), 2);
552    }
553
554    // Note: CVC5 smaller than 1.1.0 does not play nice with negative solutions
555    fn test_solver_supports_negative_solutions(solver: &mut SMTSolver) {
556        let int_sort = solver.int_sort();
557        let z = solver.declare_const("z", int_sort).unwrap();
558
559        let constr = solver.and(
560            solver.lte(z, solver.numeral(-1)),
561            solver.gt(z, solver.numeral(-2)),
562        );
563        solver.assert(constr).unwrap();
564
565        assert_eq!(solver.check().unwrap(), Response::Sat);
566
567        let solution = solver.get_value(vec![z]).unwrap();
568        assert_eq!(solution.len(), 1);
569        assert_eq!(solution[0].0, z);
570        assert_eq!(solver.get_i64(solution[0].1).unwrap(), -1);
571    }
572
573    #[test]
574    fn test_z3_solver() {
575        let builder = SMTSolverBuilder::new(&SMTSolverBuilderCfg::new_z3());
576        assert!(builder.is_ok());
577        let builder = builder.unwrap();
578
579        let mut solver = builder.new_solver();
580        test_solver_interaction(&mut solver);
581        test_solver_supports_negative_solutions(&mut solver);
582    }
583
584    #[test]
585    fn test_cvc5_solver() {
586        let builder = SMTSolverBuilder::new(&SMTSolverBuilderCfg::new_cvc5());
587        assert!(builder.is_ok());
588        let builder = builder.unwrap();
589
590        let mut solver = builder.new_solver();
591        test_solver_interaction(&mut solver);
592    }
593
594    #[test]
595    fn test_cvc5_parse_version_1() {
596        let out = "\
597This is cvc5 version 1.1.0 [git tag 1.1.0 branch HEAD]
598compiled with GCC version 11.4.0
599on Dec 21 2023 01:08:41
600
601Copyright (c) 2009-2023 by the authors and their institutional
602affiliations listed at https://cvc5.github.io/people.html
603
604cvc5 is open-source and is covered by the BSD license (modified).
605
606THIS SOFTWARE IS PROVIDED AS-IS, WITHOUT ANY WARRANTIES.
607USE AT YOUR OWN RISK.
608
609This version of cvc5 is linked against the following non-(L)GPL'ed
610third party libraries.
611
612  CaDiCaL - Simplified Satisfiability Solver
613  See https://github.com/arminbiere/cadical for copyright information.
614
615  Editline Library
616  See https://thrysoee.dk/editline
617  for copyright information.
618
619  SymFPU - The Symbolic Floating Point Unit
620  See https://github.com/martin-cs/symfpu/tree/CVC4 for copyright information.
621
622This version of cvc5 is linked against the following third party
623libraries covered by the LGPLv3 license.
624See licenses/lgpl-3.0.txt for more information.
625
626  GMP - Gnu Multi Precision Arithmetic Library
627  See http://gmplib.org for copyright information.
628
629  LibPoly polynomial library
630  See https://github.com/SRI-CSL/libpoly for copyright and
631  licensing information.
632
633cvc5 is statically linked against these libraries. To recompile
634this version of cvc5 with different versions of these libraries
635follow the instructions on https://github.com/cvc5/cvc5/blob/main/INSTALL.md
636
637See the file COPYING (distributed with the source code, and with
638all binaries) for the full cvc5 copyright, licensing, and (lack of)
639warranty information.
640";
641
642        let got = parse_smt_solver_version(out);
643        assert_eq!(got, Ok((1, 1, 0)))
644    }
645
646    #[test]
647    fn test_cvc5_parse_version_2() {
648        let out = "\
649This is cvc5 version 1.2.0
650compiled with GCC version 14.2.1 20240912 (Red Hat 14.2.1-3)
651on Sep 26 2024 00:00:00
652
653Copyright (c) 2009-2023 by the authors and their institutional
654affiliations listed at https://cvc5.github.io/people.html
655
656This build of cvc5 uses GPLed libraries, and is thus covered by
657the GNU General Public License (GPL) version 3.  Versions of cvc5
658are available that are covered by the (modified) BSD license. If
659you want to license cvc5 under this license, please configure cvc5
660with the \"--no-gpl\" option before building from sources.
661
662THIS SOFTWARE IS PROVIDED AS-IS, WITHOUT ANY WARRANTIES.
663USE AT YOUR OWN RISK.
664
665This version of cvc5 is linked against the following non-(L)GPL'ed
666third party libraries.
667
668  CaDiCaL - Simplified Satisfiability Solver
669  See https://github.com/arminbiere/cadical for copyright information.
670
671  CryptoMiniSat - An Advanced SAT Solver
672  See https://github.com/msoos/cryptominisat for copyright information.
673
674  Kissat - Simplified Satisfiability Solver
675  See https://fmv.jku.at/kissat for copyright information.
676
677  Editline Library
678  See https://thrysoee.dk/editline
679  for copyright information.
680
681  SymFPU - The Symbolic Floating Point Unit
682  See https://github.com/martin-cs/symfpu/tree/CVC4 for copyright information.
683
684This version of cvc5 is linked against the following third party
685libraries covered by the LGPLv3 license.
686See licenses/lgpl-3.0.txt for more information.
687
688  GMP - Gnu Multi Precision Arithmetic Library
689  See http://gmplib.org for copyright information.
690
691  LibPoly polynomial library
692  See https://github.com/SRI-CSL/libpoly for copyright and
693  licensing information.
694
695This version of cvc5 is linked against the following third party
696libraries covered by the GPLv3 license.
697See licenses/gpl-3.0.txt for more information.
698
699  CoCoALib - a computer algebra library
700  See https://cocoa.dima.unige.it/cocoa/cocoalib/index.shtml for copyright information
701
702See the file COPYING (distributed with the source code, and with
703all binaries) for the full cvc5 copyright, licensing, and (lack of)
704warranty information.
705";
706
707        let got = parse_smt_solver_version(out);
708        assert_eq!(got, Ok((1, 2, 0)))
709    }
710
711    #[test]
712    fn test_cvc5_parse_version_3() {
713        let out = "\
714Could not read history from /root/.cvc5_history_smtlib2: No such file or directory
715cvc5 1.4.0 [git b432cd7 on branch HEAD]
716compiled as a unrestricted build with GCC version 11.4.0 on Sep 17 2026 21:14:31
717
718Copyright (c) 2009-2026 by the authors and their institutional
719affiliations listed at https://cvc5.github.io/people.html
720
721cvc5 is open-source and is covered by the BSD license (modified).
722
723THIS SOFTWARE IS PROVIDED AS-IS, WITHOUT ANY WARRANTIES.
724USE AT YOUR OWN RISK.
725
726This version of cvc5 is linked against the following non-(L)GPL'ed
727third party libraries.
728
729  CaDiCaL - Simplified Satisfiability Solver
730  See https://github.com/arminbiere/cadical for copyright information.
731
732  Editline Library
733  See https://thrysoee.dk/editline
734  for copyright information.
735
736  SymFPU - The Symbolic Floating Point Unit
737  See https://github.com/martin-cs/symfpu/tree/main for copyright information.
738
739This version of cvc5 is linked against the following third party
740libraries covered by the LGPLv3 license.
741See licenses/lgpl-3.0.txt for more information.
742
743  GMP - Gnu Multi Precision Arithmetic Library
744  See http://gmplib.org for copyright information.
745
746  LibPoly polynomial library
747  See https://github.com/SRI-CSL/libpoly for copyright and
748  licensing information.
749
750cvc5 is statically linked against these libraries. To recompile
751this version of cvc5 with different versions of these libraries
752follow the instructions on https://github.com/cvc5/cvc5/blob/main/INSTALL.md
753
754See the file COPYING (distributed with the source code, and with
755all binaries) for the full cvc5 copyright, licensing, and (lack of)
756warranty information.
757";
758
759        let got = parse_smt_solver_version(out);
760        assert_eq!(got, Ok((1, 4, 0)))
761    }
762
763    #[test]
764    fn test_z3_parse_version() {
765        let out = "\
766Z3 version 4.8.12 - 64 bit";
767
768        let got = parse_smt_solver_version(out);
769        assert_eq!(got, Ok((4, 8, 12)))
770    }
771
772    #[test]
773    fn test_z3_get_version() {
774        let version = get_smt_solver_version(Z3_PRG);
775        assert!(version.is_ok());
776    }
777
778    #[test]
779    fn test_cvc5_get_version() {
780        let version = get_smt_solver_version(CVC5_PRG);
781        assert!(version.is_ok());
782    }
783
784    #[test]
785    fn test_automatic_solver_selection() {
786        let builder = SMTSolverBuilder::new_automatic_selection()
787            .expect("Failed to create default SMT solver builder. No SMT solver found.");
788
789        let mut solver = builder.new_solver();
790        test_solver_interaction(&mut solver);
791    }
792
793    #[test]
794    fn test_command_solver() {
795        let cvc5_args: Vec<String> = CVC5_ARGS.iter().map(|&s| s.to_string()).collect();
796
797        let cfg = SMTSolverBuilderCfg::new("cvc5".to_string(), cvc5_args.clone(), vec![], false);
798        let builder = SMTSolverBuilder::new(&cfg).unwrap();
799
800        let mut solver = builder.new_solver();
801        test_solver_interaction(&mut solver);
802
803        let second_builder = builder.clone();
804        assert_eq!(builder, second_builder);
805    }
806
807    #[test]
808    fn test_command_solver_set_lia() {
809        let cvc5_args: Vec<String> = CVC5_ARGS.iter().map(|&s| s.to_string()).collect();
810
811        let cfg = SMTSolverBuilderCfg::new("cvc5".to_string(), cvc5_args.clone(), vec![], true);
812        let builder = SMTSolverBuilder::new(&cfg).unwrap();
813
814        let mut solver = builder.new_solver();
815        test_solver_interaction(&mut solver);
816
817        let second_builder = builder.clone();
818        assert_eq!(builder, second_builder);
819    }
820
821    #[test]
822    #[should_panic]
823    fn test_panic_unknown_solver() {
824        let cfg = SMTSolverBuilderCfg::new("unknown_solver".to_string(), vec![], vec![], false);
825        let _builder = SMTSolverBuilder::new(&cfg).unwrap();
826    }
827
828    #[test]
829    fn display_solution() {
830        assert_eq!(SMTSolution::UNSAT.to_string(), "UNSAT");
831        assert_eq!(SMTSolution::SAT.to_string(), "SAT");
832    }
833
834    #[test]
835    fn test_is_sat() {
836        assert!(!SMTSolution::UNSAT.is_sat());
837        assert!(SMTSolution::SAT.is_sat());
838    }
839
840    #[test]
841    fn test_get_version_error_display() {
842        let err = GetVersionError::NotInstalled("cvc5".to_string());
843        assert_eq!(
844            err.to_string(),
845            "Execution of `cvc5 --version`  failed. This most likely means that the requested SMT solver is not installed."
846        );
847        let err = GetVersionError::ParseVersionError;
848        assert_eq!(
849            err.to_string(),
850            "Failed to parse version out of the output of `<SMT-SOLVER-COMMAND> --version`"
851        );
852        let err = GetVersionError::ParseVersionError;
853        assert_eq!(
854            err.to_string(),
855            "Failed to parse version out of the output of `<SMT-SOLVER-COMMAND> --version`"
856        );
857    }
858
859    #[test]
860    fn test_solver_option_display() {
861        let opt = SMTSolverOption::BooleanOption {
862            name: ":opt".to_string(),
863            value: true,
864        };
865        assert_eq!(opt.to_string(), ":opt : true");
866        let opt = SMTSolverOption::UnsignedIntOption {
867            name: ":opt".to_string(),
868            value: 42,
869        };
870        assert_eq!(opt.to_string(), ":opt : 42");
871    }
872
873    #[test]
874    fn test_new_solver_opt() {
875        let opt = SMTSolverOption::new_boolean_opt(":opt".to_string(), true);
876        assert_eq!(
877            opt,
878            SMTSolverOption::BooleanOption {
879                name: ":opt".to_string(),
880                value: true,
881            }
882        );
883        let opt = SMTSolverOption::new_integer_opt(":opt".to_string(), 42);
884        assert_eq!(
885            opt,
886            SMTSolverOption::UnsignedIntOption {
887                name: ":opt".to_string(),
888                value: 42,
889            }
890        );
891    }
892
893    #[test]
894    fn test_fmt_solver_builder_error() {
895        let err = SMTSolverBuilderError::NotInstalled("cvc5".to_string());
896        assert_eq!(err.to_string(), "SMT solver cvc5 is not installed");
897    }
898
899    #[test]
900    fn test_eq_smt_solver_builder_cfg() {
901        let cfg1 = SMTSolverBuilderCfg::new(
902            "cvc5".to_string(),
903            vec!["--quiet".to_string(), "--lang=smt2".to_string()],
904            vec![],
905            false,
906        );
907        let cfg2 = SMTSolverBuilderCfg::new(
908            "cvc5".to_string(),
909            vec!["--quiet".to_string(), "--lang=smt2".to_string()],
910            vec![],
911            false,
912        );
913        assert_eq!(cfg1, cfg2);
914
915        let cfg3 = SMTSolverBuilderCfg::new(
916            "z3".to_string(),
917            vec!["-smt2".to_string(), "-in".to_string(), "-v:0".to_string()],
918            vec![],
919            false,
920        );
921        assert_ne!(cfg1, cfg3);
922    }
923}
taco_smt_encoder/lib.rs

taco_smt_encoder/
lib.rs
