Enum Constraint 

pub enum Constraint<T: Types> {
    Pred(Pred<T>, Option<T::Tag>),
    Conj(Vec<Self>),
    ForAll(Bind<T>, Box<Self>),
}

Variants

Pred(Pred<T>, Option<T::Tag>)

Conj(Vec<Self>)

ForAll(Bind<T>, Box<Self>)

Implementations

impl<T: Types> Constraint<T>

pub const TRUE: Self

pub fn foralls(bindings: Vec<Bind<T>>, c: Self) -> Self

pub fn conj(cstrs: Vec<Self>) -> Self

pub fn concrete_head_count(&self) -> usize

Returns true if the constraint has at least one concrete RHS (“head”) predicates. If !c.is_concrete then c is trivially satisfiable and we can avoid calling fixpoint. Returns the number of concrete, non-trivial head predicates in the constraint.

pub fn flatten<F1>(&self, is_underscore: F1) -> Vec<FlatConstraint<T>>

where F1: Copy + Fn(&T::Var) -> bool,

Flattens a single constraint into a list of individual constraints which may be checked for satisfiability.

NOTE: Assumes and requires that all binder names are unique, i.e. there is no shadowing (it is OK to have multiple binders of the same name so long as they never are used, e.g. UNDERSCORE).

Trait Implementations

impl<T: Types> Clone for Constraint<T>

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<T: Types> Debug for Constraint<T>

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

Formats the value using the given formatter.

impl<T: Types> Display for Constraint<T>

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

Formats the value using the given formatter.

impl<T: Types> Hash for Constraint<T>

fn hash<__H: Hasher>(&self, __state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.