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 is_concrete(&self) -> bool

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.

impl<T: Types> Constraint<T>

pub fn depth_first_fragments(&self) -> ConstraintFragments<'_, T>

pub fn kvar_deps(&self) -> Vec<T::KVar>

pub fn kvar_mappings( &self, ) -> (HashMap<T::KVar, Vec<Constraint<T>>>, HashMap<T::KVar, Vec<T::KVar>>)

pub fn topo_order_fragments(&self) -> Vec<Self>

pub fn fragment_kvar_head(&self) -> Option<T::KVar>

pub fn sub_all_kvars( &self, assignments: &HashMap<T::KVar, Vec<(&Qualifier<T>, Vec<usize>)>>, ) -> Self

pub fn sub_kvars_except_head( &self, assignments: &HashMap<T::KVar, Vec<(&Qualifier<T>, Vec<usize>)>>, ) -> Self

pub fn sub_head(&self, assignment: &(&Qualifier<T>, Vec<usize>)) -> Self

pub fn scope(&self, var: &T::KVar) -> Self

fn scope_help(&self, var: &T::KVar) -> Option<Constraint<T>>

pub fn sol1(&self, var: &T::KVar) -> Vec<Solution<T>>

pub fn elim(&self, vars: &Vec<T::KVar>) -> Self

pub fn elim1(&self, var: &T::KVar) -> Self

fn do_elim(&self, var: &T::KVar, solution: &Vec<Solution<T>>) -> Self

pub fn is_satisfiable(&self) -> bool

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> 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.