Enum SmtSolver

pub enum SmtSolver {
    Z3,
    CVC5,
}

Variants

Z3

CVC5

Trait Implementations

impl Clone for SmtSolver

fn clone(&self) -> SmtSolver

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for SmtSolver

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

Formats the value using the given formatter.

impl Default for SmtSolver

fn default() -> SmtSolver

Returns the “default value” for a type.

impl<'de> Deserialize<'de> for SmtSolver

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl FromStr for SmtSolver

type Err = &'static str

The associated error which can be returned from parsing.

fn from_str(s: &str) -> Result<Self, Self::Err>

Parses a string s to return a value of this type.

impl TryFrom<String> for SmtSolver

type Error = &'static str

The type returned in the event of a conversion error.

fn try_from(value: String) -> Result<Self, Self::Error>

Performs the conversion.

impl Copy for SmtSolver