Struct FlatConstraint 

pub struct FlatConstraint<T: Types> {
    pub binders: Vec<(T::Var, Sort<T>)>,
    pub assumptions: FxIndexSet<Pred<T>>,
    pub head: Pred<T>,
    pub tag: Option<T::Tag>,
}

Fields

binders: Vec<(T::Var, Sort<T>)>

All of the binders that come before the head.

NOTE: There should be no duplicates among the binders which are used (so e.g. UNDERSCORE appearing multiple times is OK).

assumptions: FxIndexSet<Pred<T>>

All of the assumptions (i.e. a flattened conjunction of predicates from all of the binders)

head: Pred<T>

tag: Option<T::Tag>

Implementations

impl<T: Types> FlatConstraint<T>

pub fn remove_binders( &self, vars: &HashSet<T::Var>, ) -> (Vec<ConstDecl<T>>, FlatConstraint<T>)

Removes any binder corresponding to a given var. Returns the new constraint along with the removed binders and their sorts.

NOTE: Assumes that all binders are unique and therefore there are no name clashes.

pub fn add_assumption(&mut self, assumption: Pred<T>)

pub fn preconditions(&self) -> FxIndexSet<Pred<T>>

pub fn wkvars_and_constrs( &self, ) -> Vec<(WKVar<T>, FlatConstraint<T>, Vec<FlatConstraint<T>>)>

Each element of the output is a wkvar, the constraint it corresponds to, and the other constraints which must also hold.

We essentially “decompose” each assumption which contains a wkvar in order to transform the constraint into one in which that wkvar is exposed.

These decompositions are of two forms.

1. Hoisting existentials to the top level.
2. Splitting disjuncts using the below property. When we split a disjunct, we generate other constraints. A more sophisticated analysis might try and solve multiple constraints simultaneously; if we were to do this, we would probably want to change how this algorithm works to avoid redundancy, e.g. by instead of generating ((wkvar, constr, other_constrs) outputs generating (all_constrs) outputs and letting consumers choose which wkvars to solve in each constr.

(p || q) => c
==
(p => c) && (q => c)

Trait Implementations

impl<T: Types> Clone for FlatConstraint<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 FlatConstraint<T>

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

Formats the value using the given formatter.