Enum SMTSolverOption 

pub enum SMTSolverOption {
    BooleanOption {
        name: String,
        value: bool,
    },
    UnsignedIntOption {
        name: String,
        value: u32,
    },
}

Type for options that can be supplied to an SMT solver

Variants

BooleanOption

Option with boolean value

Fields

name: String

Name of the option

value: bool

Value to set the option to

UnsignedIntOption

Option with unsigned integer value

Fields

name: String

Name of the option

value: u32

Value to set the option to

Implementations

impl SMTSolverOption

pub fn new_boolean_opt(name: String, value: bool) -> Self

Create a new boolean SMTSolverOption

pub fn new_integer_opt(name: String, value: u32) -> Self

Create a new integer SMTSolverOption

pub fn apply_option(&self, solver: &mut SMTSolver)

Apply option to the SMT solver

Trait Implementations

impl Clone for SMTSolverOption

fn clone(&self) -> SMTSolverOption

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SMTSolverOption

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for SMTSolverOption

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Display for SMTSolverOption

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

Formats the value using the given formatter.

impl PartialEq for SMTSolverOption

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for SMTSolverOption