Enum boogie_backend::options::VectorTheory

pub enum VectorTheory {
    BoogieArray,
    BoogieArrayIntern,
    SmtArray,
    SmtArrayExt,
    SmtSeq,
}

Variants

BoogieArray

BoogieArrayIntern

SmtArray

SmtArrayExt

SmtSeq

Implementations

impl VectorTheory

pub fn is_extensional(&self) -> bool

Trait Implementations

impl Clone for VectorTheory

fn clone(&self) -> VectorTheory

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for VectorTheory

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for VectorTheory

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Serialize for VectorTheory

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Copy for VectorTheory