Enum rsmt2::conf::SmtStyle

pub enum SmtStyle {
    Z3,
    CVC4,
    Yices2,
}

Solver styles.

• z3: full support
• cvc4: full support in theory, but only partially tested. Note that get-value is known to crash some versions of CVC4.
• yices 2: full support in theory, but only partially tested. Command get-model will only work on Yices 2 > 2.6.1, and needs to be activated in SmtConf with SmtConf::models. To understand why, see https://github.com/SRI-CSL/yices2/issues/162.

Variants

Z3

Z3-style smt solver.

CVC4

CVC4-style smt solver.

NB: CVC4 has only been partially tested at this point.

Yices2

Yices-2-style smt solver.

NB: Yices 2 has only been partially tested at this point.

Implementations

impl SmtStyle

pub fn new(self, cmd: impl Into<String>) -> SmtConf

Configuration constructor.

pub fn default(self) -> SmtConf

Default configuration for a solver style.

Warning

The command used to run a particular solver is up to the end-user. As such, it does not make sense to use default commands for anything else than local testing. You should explicitely pass the command to use with Self::new instead.

pub fn of_str(s: &str) -> Option<Self>

A solver style from a string.

pub fn str_keys() -> Vec<&'static str>

Legal string representations of solver styles.

pub fn env_cmd(self) -> SmtRes<Option<String>>

Solver style command from the corresponding environment variable.

The environement variables scanned are Z3_ENV_VAR, CVC4_ENV_VAR and YICES_2_ENV_VAR.

pub fn cmd(self) -> &'static str

Default command for a solver style.

pub fn is_z3(self) -> bool

True if self is Self::Z3.

Trait Implementations

impl Clone for SmtStyle

fn clone(&self) -> SmtStyle

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for SmtStyle

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for SmtStyle

fn fmt(&self, fmt: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq<SmtStyle> for SmtStyle

fn eq(&self, other: &SmtStyle) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=.

impl Copy for SmtStyle

impl Eq for SmtStyle

impl StructuralEq for SmtStyle

impl StructuralPartialEq for SmtStyle