Enum Expression

pub enum Expression {
    Primitive(ExpressionPrimitive),
    VarRef(ExpressionVarRef),
    ConstructorApp(ExpressionConstructorApp),
    Operator(ExpressionOperator),
    Iterator(ExpressionIterator),
    Projection(ExpressionProjection),
}

Defines an eFLINT expression that evaluates to a value.

There are multiple variants of this:

• Primitives: Constants/Literals;
• Variable references: References to quantified variables;
• Construction applications: Instantiation of a type of some kind;
• Operators: Addition, substraction, multiplication, etc.;
• Iterators: Foreach, forall, exists, etc.; and
• Projections: Field accessing of some type.

Variants

Primitive(ExpressionPrimitive)

eFLINT primitives, i.e., literal values:

"Amy"
42
42.0
true

VarRef(ExpressionVarRef)

eFLINT variable references:

citizen
// As in second occurance in:
Foreach citizen: citizen

ConstructorApp(ExpressionConstructorApp)

Constructor applications, i.e., instantiating facts:

citizen("Amy")

Operator(ExpressionOperator)

Operators (addition, multiplication, Holds, Violated, etc):

1 + 2
Holds("Amy")

Iterator(ExpressionIterator)

Iterators that do inherent quantification.

Note that this is different from operators like Count, which do not quantify themselves but rather process an already produced instance expression.

For example:

Foreach citizen : citizen.
Forall citizen : citizen.
Exists citizen : citizen.

Projection(ExpressionProjection)

Projection:

citizen.string

Implementations

impl Expression

pub fn kind(&self) -> Option<ExpressionKind>

Returns the kind of this expression, whether it’s a boolean or instance expression.

Returns

An auxillary::ExpressionKind denoting which of the two kinds it is. If None is returned, then this is not statically determinable (this is the case for Operators and Iterators).

Trait Implementations

impl Clone for Expression

fn clone(&self) -> Expression

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Expression

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Expression

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl EnumDebug for Expression

fn type_name() -> &'static str

Returns the static name of the type used for EnumDebug-printing.

fn variant_names() -> &'static [&'static str]

Returns all variants in the trait as a list of names.

fn variant_name(&self) -> &'static str

Returns the static name of the variant.

fn variant(&self) -> EnumDebugFormatter<'_, Self>

Returns a formatter for this enum that writes its variant name.

fn variants() -> Copied<Iter<'static, &'static str>>

Returns an iterator over all variants in this enum.

impl Serialize for Expression

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.