Struct ConstraintWithEnv 

pub struct ConstraintWithEnv<T: Types> {
    pub kvar_decls: Vec<KVarDecl<T>>,
    pub qualifiers: Vec<Qualifier<T>>,
    pub constraint: Constraint<T>,
}

Fields

kvar_decls: Vec<KVarDecl<T>>

qualifiers: Vec<Qualifier<T>>

constraint: Constraint<T>

Implementations

impl ConstraintWithEnv<ParsingTypes>

pub fn is_satisfiable(&self) -> bool

pub fn uniquify(&mut self)

pub fn solve_by_fusion(&self) -> bool

pub fn solve_by_predicate_abstraction(&self) -> bool

pub fn compute_initial_assignments<'a>( &'a self, qualifiers: &'a Vec<Qualifier<ParsingTypes>>, ) -> HashMap<String, Vec<(&'a Qualifier<ParsingTypes>, Vec<usize>)>>

pub fn solve_for_kvars<'a>( &'a self, qualifiers: &'a Vec<Qualifier<ParsingTypes>>, ) -> HashMap<String, Vec<(&'a Qualifier<ParsingTypes>, Vec<usize>)>>

Trait Implementations

impl<T: Types> Hash for ConstraintWithEnv<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.