Struct Expr 

#[non_exhaustive]
pub struct Expr {
    pub span: Span,
    pub kind: ExprKind,
    pub ty: Type,
}

Fields (Non-exhaustive)

Non-exhaustive structs could have additional fields added in future. Therefore, non-exhaustive structs cannot be constructed in external crates using the traditional Struct { .. } syntax; cannot be matched against without a wildcard ..; and struct update syntax will not work.

span: Span

kind: ExprKind

ty: Type

Implementations

impl Expr

pub fn error() -> Expr

impl Expr

pub fn add(&self, other: &Expr) -> Expr

impl Expr

pub fn sub(&self, other: &Expr) -> Expr

impl Expr

pub fn mul(&self, other: &Expr) -> Expr

impl Expr

pub fn div(&self, other: &Expr) -> Expr

impl Expr

pub fn and(&self, other: &Expr) -> Expr

impl Expr

pub fn or(&self, other: &Expr) -> Expr

impl Expr

pub fn new_typed(kind: ExprKind, ty: Type) -> Expr

pub fn result(ty: &Type) -> Expr

pub fn broke() -> Expr

pub fn op(&self, op: Op, rhs: &Expr) -> Expr

pub fn prefix(&self, op: PrefixOp) -> Expr

pub fn num(value: i64) -> Expr

pub fn bool(value: bool) -> Expr

pub fn ident(ident: &str, ty: &Type) -> Expr

pub fn imp(&self, other: &Expr) -> Expr

pub fn ite(&self, then: &Expr, otherwise: &Expr) -> Expr

pub fn quantifier(q: Quantifier, vars: &[Var], body: &Expr) -> Expr

pub fn call(name: Name, args: Vec<Expr>, fun_ref: FunctionRef) -> Expr

pub fn lt(&self, other: &Expr) -> Expr

Create self < other.

pub fn le(&self, other: &Expr) -> Expr

Create self <= other.

pub fn gt(&self, other: &Expr) -> Expr

Create self > other.

pub fn ge(&self, other: &Expr) -> Expr

Create self >= other.

pub fn eq(&self, other: &Expr) -> Expr

Create self == other.

pub fn ne(&self, other: &Expr) -> Expr

Create self != other.

pub fn subst(&self, f: impl FnMut(&Expr) -> bool, to: &Expr) -> Expr

Substitute all sub-expressions for which f returns true with to.

pub fn subst_ident(&self, from: &str, to: &Expr) -> Expr

Substitute all occurrences of from with to.

pub fn subst_old_ident(&self, from: &str, to: &Expr) -> Expr

Substitute all occurrences of old(from) with to.

pub fn subst_result(&self, to: &Expr) -> Expr

Substitute all occurrences of result with to.

pub fn pre_order_map(&self, f: impl FnMut(&Expr) -> Option<Expr>) -> Expr

pub fn post_order_map(&self, f: impl FnMut(&Expr) -> Option<Expr>) -> Expr

pub fn with_span(&self, span: Span) -> Expr

impl Expr

pub fn as_ident(&self) -> Option<&str>

pub fn is_result(&self) -> bool

pub fn is_ident(&self, i: &str) -> bool

impl Expr

pub fn smt<'st>(&self, st: &'st Storage) -> Result<Dynamic<'st>, SmtError>

Trait Implementations

impl Add<&Expr> for &Expr

type Output = Expr

The resulting type after applying the + operator.

fn add(self, rhs: &Expr) -> Self::Output

Performs the + operation.

impl Add<&Expr> for Expr

type Output = Expr

The resulting type after applying the + operator.

fn add(self, rhs: &Expr) -> Self::Output

Performs the + operation.

impl Add<Expr> for &Expr

type Output = Expr

The resulting type after applying the + operator.

fn add(self, rhs: Expr) -> Self::Output

Performs the + operation.

impl Add for Expr

type Output = Expr

The resulting type after applying the + operator.

fn add(self, rhs: Expr) -> Self::Output

Performs the + operation.

impl BitAnd<&Expr> for &Expr

type Output = Expr

The resulting type after applying the & operator.

fn bitand(self, rhs: &Expr) -> Self::Output

Performs the & operation.

impl BitAnd<&Expr> for Expr

type Output = Expr

The resulting type after applying the & operator.

fn bitand(self, rhs: &Expr) -> Self::Output

Performs the & operation.

impl BitAnd<Expr> for &Expr

type Output = Expr

The resulting type after applying the & operator.

fn bitand(self, rhs: Expr) -> Self::Output

Performs the & operation.

impl BitAnd for Expr

type Output = Expr

The resulting type after applying the & operator.

fn bitand(self, rhs: Expr) -> Self::Output

Performs the & operation.

impl BitOr<&Expr> for &Expr

type Output = Expr

The resulting type after applying the | operator.

fn bitor(self, rhs: &Expr) -> Self::Output

Performs the | operation.

impl BitOr<&Expr> for Expr

type Output = Expr

The resulting type after applying the | operator.

fn bitor(self, rhs: &Expr) -> Self::Output

Performs the | operation.

impl BitOr<Expr> for &Expr

type Output = Expr

The resulting type after applying the | operator.

fn bitor(self, rhs: Expr) -> Self::Output

Performs the | operation.

impl BitOr for Expr

type Output = Expr

The resulting type after applying the | operator.

fn bitor(self, rhs: Expr) -> Self::Output

Performs the | operation.

impl Clone for Expr

fn clone(&self) -> Expr

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Expr

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

Formats the value using the given formatter.

impl Display for Expr

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

Formats the value using the given formatter.

impl Div<&Expr> for &Expr

type Output = Expr

The resulting type after applying the / operator.

fn div(self, rhs: &Expr) -> Self::Output

Performs the / operation.

impl Div<&Expr> for Expr

type Output = Expr

The resulting type after applying the / operator.

fn div(self, rhs: &Expr) -> Self::Output

Performs the / operation.

impl Div<Expr> for &Expr

type Output = Expr

The resulting type after applying the / operator.

fn div(self, rhs: Expr) -> Self::Output

Performs the / operation.

impl Div for Expr

type Output = Expr

The resulting type after applying the / operator.

fn div(self, rhs: Expr) -> Self::Output

Performs the / operation.

impl Mul<&Expr> for &Expr

type Output = Expr

The resulting type after applying the * operator.

fn mul(self, rhs: &Expr) -> Self::Output

Performs the * operation.

impl Mul<&Expr> for Expr

type Output = Expr

The resulting type after applying the * operator.

fn mul(self, rhs: &Expr) -> Self::Output

Performs the * operation.

impl Mul<Expr> for &Expr

type Output = Expr

The resulting type after applying the * operator.

fn mul(self, rhs: Expr) -> Self::Output

Performs the * operation.

impl Mul for Expr

type Output = Expr

The resulting type after applying the * operator.

fn mul(self, rhs: Expr) -> Self::Output

Performs the * operation.

impl Neg for Expr

type Output = Expr

The resulting type after applying the - operator.

fn neg(self) -> Self::Output

Performs the unary - operation.

impl Not for Expr

type Output = Expr

The resulting type after applying the ! operator.

fn not(self) -> Self::Output

Performs the unary ! operation.

impl Sub<&Expr> for &Expr

type Output = Expr

The resulting type after applying the - operator.

fn sub(self, rhs: &Expr) -> Self::Output

Performs the - operation.

impl Sub<&Expr> for Expr

type Output = Expr

The resulting type after applying the - operator.

fn sub(self, rhs: &Expr) -> Self::Output

Performs the - operation.

impl Sub<Expr> for &Expr

type Output = Expr

The resulting type after applying the - operator.

fn sub(self, rhs: Expr) -> Self::Output

Performs the - operation.

impl Sub for Expr

type Output = Expr

The resulting type after applying the - operator.

fn sub(self, rhs: Expr) -> Self::Output

Performs the - operation.