Struct gf::smt::Expr

pub struct Expr { /* fields omitted */ }

🟢 Expression.

Expressions are reference-counted: the Clone implementation increments the counter, and the Drop implementation decrements it, freeing the expression when it is no longer used.

Simplification

Expressions are automatically simplified when built, unless you explicitly opt out, which is never a good idea because non-simplified expressions are often too difficult for an SMT solver even if the actual code is small.

See the simplifier module for the list of transformations.

Implementations

impl Expr

pub fn new_bit_vec(bv: BitVec) -> Self

Construct a bit vector constant.

pub fn new_bit_vec_op<I>(
    op: BitVecOp,
    operands: I
) -> Result<Self, BitVecOpError> where
    I: IntoIterator<Item = Expr>, 

Construct a bit vector operator application with simplification.

pub fn new_bit_vec_op_non_simplified<I>(
    op: BitVecOp,
    operands: I
) -> Result<Self, BitVecOpError> where
    I: IntoIterator<Item = Expr>, 

Construct a bit vector operator application without simplification.

pub fn new_concat_cascade<I>(operands: I) -> Result<Self, BitVecOpError> where
    I: IntoIterator<Item = Expr>, 

Construct a concatenation cascade.

pub fn new_var(sort: Sort, id: String) -> Self

Construct a free variable of given sort.

pub fn from_value(value: ExprValue) -> Self

Wrap a value.

pub fn kind(&self) -> &ExprKind

Return the expression kind.

pub fn sort(&self) -> &Sort

Return the expression sort.

pub fn is_bit_vec(&self) -> bool

Return whether the expression is a bit vector constant.

pub fn is_bit_vec_op(&self) -> bool

Return whether the expression is a bit vector operator application.

pub fn is_var(&self) -> bool

Return whether the expression is a free variable.

pub fn bit_vec(&self) -> &BitVec

Return bit vector value.

Errors

• Panics if the expression is not a bit vector constant.

pub fn bit_vec_op_operands(&self) -> &[Expr]

Return bit vector operator application operands.

Errors

• Panics if the expression is not a bit vector operator application.

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

Return identifier of a variable.

Errors

• Panics if the expression is not a variable.

Trait Implementations

impl Clone for Expr

fn clone(&self) -> Expr

Returns a copy 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 Eq for Expr

impl Hash for Expr

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, 

Feeds a slice of this type into the given Hasher.

impl PartialEq<Expr> for Expr

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

This method tests for self and other values to be equal, and is used by ==.

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

This method tests for !=.

impl StructuralEq for Expr

impl StructuralPartialEq for Expr