Trait QuantifierVars

pub trait QuantifierVars<'st> {
    // Required method
    fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>];
}

This trait is implemented for types and sequences which can be used as quantified variables in forall and exists.

Required Methods

fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>]

The concrete sequence of variable declaration which should be quantified over.

Implementations on Foreign Types

impl<'st> QuantifierVars<'st> for &'st [SortedVar<'st>]

fn into_vars(self, _st: &'st Storage) -> &'st [SortedVar<'st>]

impl<'st> QuantifierVars<'st> for &'st [Const<'st, Dynamic<'st>>]

fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>]

impl<'st> QuantifierVars<'st> for Vec<Const<'st, Dynamic<'st>>>

fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>]

impl<'st, A, B> QuantifierVars<'st> for (Const<'st, A>, Const<'st, B>)

where A: StaticSorted<'st>, B: StaticSorted<'st>,

fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>]

impl<'st, A, B, C> QuantifierVars<'st> for (Const<'st, A>, Const<'st, B>, Const<'st, C>)

where A: StaticSorted<'st>, B: StaticSorted<'st>, C: StaticSorted<'st>,

fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>]

impl<'st, A, B, C, D> QuantifierVars<'st> for (Const<'st, A>, Const<'st, B>, Const<'st, C>, Const<'st, D>)

where A: StaticSorted<'st>, B: StaticSorted<'st>, C: StaticSorted<'st>, D: StaticSorted<'st>,

fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>]

impl<'st, A, B, C, D, E> QuantifierVars<'st> for (Const<'st, A>, Const<'st, B>, Const<'st, C>, Const<'st, D>, Const<'st, E>)

where A: StaticSorted<'st>, B: StaticSorted<'st>, C: StaticSorted<'st>, D: StaticSorted<'st>, E: StaticSorted<'st>,

fn into_vars(self, st: &'st Storage) -> &'st [SortedVar<'st>]

Implementors

impl<'st, A> QuantifierVars<'st> for Const<'st, A>

where A: StaticSorted<'st>,