Enum Expr 

pub enum Expr<T: Types> {
    Constant(Constant<T>),
    Var(T::Var),
    App(Box<Self>, Option<Vec<Sort<T>>>, Vec<Self>, Option<Sort<T>>),
    Neg(Box<Self>),
    BinaryOp(BinOp, Box<[Self; 2]>),
    IfThenElse(Box<[Self; 3]>),
    And(Vec<Self>),
    Or(Vec<Self>),
    Not(Box<Self>),
    Imp(Box<[Self; 2]>),
    Iff(Box<[Self; 2]>),
    Atom(BinRel, Box<[Self; 2]>),
    Let(T::Var, Box<[Self; 2]>),
    ThyFunc(ThyFunc),
    IsCtor(T::Var, Box<Self>),
    Quantifier(Quantifier, Vec<(T::Var, Sort<T>)>, Box<Self>),
    WKVar(WKVar<T>),
}

Variants

Constant(Constant<T>)

Var(T::Var)

App(Box<Self>, Option<Vec<Sort<T>>>, Vec<Self>, Option<Sort<T>>)

Neg(Box<Self>)

BinaryOp(BinOp, Box<[Self; 2]>)

IfThenElse(Box<[Self; 3]>)

And(Vec<Self>)

Or(Vec<Self>)

Not(Box<Self>)

Imp(Box<[Self; 2]>)

Iff(Box<[Self; 2]>)

Atom(BinRel, Box<[Self; 2]>)

Let(T::Var, Box<[Self; 2]>)

ThyFunc(ThyFunc)

IsCtor(T::Var, Box<Self>)

Quantifier(Quantifier, Vec<(T::Var, Sort<T>)>, Box<Self>)

WKVar(WKVar<T>)

NOTE: WKVars are for internal use and we serialize them as UIFs using the var argument. We also don’t emit WKVars that are in head position when translating to fixpoint.

In an ideal world fixpoint would deal with weak kvars itself.

Implementations

impl<T: Types> Expr<T>

pub const FALSE: Self

pub const TRUE: Self

pub const fn int(val: u128) -> Expr<T>

pub fn eq(self, other: Self) -> Self

pub fn and(exprs: Vec<Self>) -> Self

pub fn var_sorts_to_int(&mut self)

pub fn free_vars(&self) -> FxIndexSet<T::Var>

pub fn is_trivially_true(&self) -> bool

pub fn substitute(&self, subst: &FxIndexMap<T::Var, Self>) -> Self

pub fn wkvars_in_conj(&self) -> Vec<WKVar<T>>

pub fn uncurry(&self) -> Self

pub fn has_wkvar_reachable_by_split(&self) -> bool

pub fn hoist_exists(&self) -> (Vec<(<T as Types>::Var, Sort<T>)>, Expr<T>)

pub fn as_conjunction(self) -> Vec<Self>

pub fn strip_wkvars(&self) -> Self

pub fn total_num_disjuncts(&self) -> usize

Trait Implementations

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

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

Formats the value using the given formatter.

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

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

Formats the value using the given formatter.

impl<T: Types> From<Constant<T>> for Expr<T>

fn from(v: Constant<T>) -> Self

Converts to this type from the input type.

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

impl<T: Types> PartialEq for Expr<T>

fn eq(&self, __other: &Self) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<T: Types> Eq for Expr<T>