Struct ExpressionIterator

pub struct ExpressionIterator {
    pub iterator: String,
    pub binds: Vec<String>,
    pub expression: Box<Expression>,
}

Defines an iterator expression in eFLINT.

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.

Fields

iterator: String

The iterator operator to execute. See appendix::EFlintIteratorOperator for a list of known eFLINT operators.

binds: Vec<String>

The list of variables bound by this iterator. Basically the first occurrence of citizen in:

Foreach citizen : citizen.

expression: Box<Expression>

The expression that is repeated for every quantified combination of bound variables.

For Foreach, this is an instance expressions. For Exists and Forall, these are boolean expressions.

Trait Implementations

impl Clone for ExpressionIterator

fn clone(&self) -> ExpressionIterator

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for ExpressionIterator

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for ExpressionIterator

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Serialize for ExpressionIterator

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

where __S: Serializer,

Serialize this value into the given Serde serializer.