Struct EFlintOperator

pub struct EFlintOperator;

Defines identifiers for eFLINT operators, as well as the number of operands they require.

Note that iterator operators (FORALL, FOREACH, EXISTS) are defined separately in EFlintIteratorOperator.

Implementations

impl EFlintOperator

pub const ADD: &str = "ADD"

Arithmetic addition on two numeric values.

pub const AND: &str = "AND"

Conjunction on two boolean values.

pub const COUNT: &str = "COUNT"

Counts the number of instances generated by a single instance value.

pub const DIV: &str = "DIV"

Arithmetic division on two numeric values.

pub const ENABLED: &str = "ENABLED"

Takes a single instance value and checks if that instance can be derived by the current rules. Essentially is EFlintOperator::HOLDS but without considering postulation.

pub const EQUALS: &str = "EQ"

Checks if two values are equal.

pub const GREATER: &str = "GT"

Compares two numeric values to examine if the first is stricly greater than the second.

pub const GREATER_OR_EQUALS: &str = "GE"

Compares two numeric values to examine if the first is greater than- or equal to the second.

pub const HOLDS: &str = "HOLDS"

Essentially inline boolean query, i.e., takes a single instance value and checks if that instance is true.

pub const LESSER: &str = "LT"

Compares two numeric values to examine if the first is stricly smaller than the second.

pub const LESSER_OR_EQUALS: &str = "LE"

Compares two numeric values to examine if the first is smaller than- or equal to the second.

pub const MAX: &str = "MAX"

Returns the maximum value from the instances generated by a single instance value.

pub const MIN: &str = "MIN"

Returns the minimum value from the instances generated by a single instance value.

pub const MOD: &str = "MOD"

Arithmetic modulo on two numeric values.

pub const MUL: &str = "MUL"

Arithmetic multiplication on two numeric values.

pub const NOT: &str = "NOT"

Negation on one boolean value.

pub const NOT_EQUALS: &str = "NE"

Checks if two values are not equal (inverse of EFlintOperator::EQUALS).

pub const OR: &str = "OR"

Disjunction on two boolean values.

pub const SUB: &str = "SUB"

Arithmetic subtraction on two numeric values.

pub const SUM: &str = "SUM"

Sums the instances generated by a single instance value together to a numeric value.

pub const VIOLATED: &str = "VIOLATED"

Takes a single instance value and checks if, if that instantiation were to be added to the knowledge base, it would trigger any violations.

pub const WHEN: &str = "WHEN"

Filters an instance expression with a boolean expression to keep only the ones that evaluate to true.

pub const fn all() -> &'static [&'static str]

Returns a list of all the eFLINT operators known.

Returns

A static slice with all operators.

pub const fn logical() -> &'static [&'static str]

Returns a list of all the logic operators in eFLINT.

Returns

A static slice with all logic operators.

pub const fn comparison() -> &'static [&'static str]

Returns a list of all the comparison operators in eFLINT.

Returns

A static slice with all comparison operators.

pub const fn arithmetic() -> &'static [&'static str]

Returns a list of all the arithmetic operators in eFLINT.

Returns

A static slice with all arithmetic operators.

pub const fn iterator() -> &'static [&'static str]

Returns a list of all the iterator operators in eFLINT.

Returns

A static slice with all iterator operators.

pub const fn miscellaneous() -> &'static [&'static str]

Returns a list of all the miscellaneous operators in eFLINT.

Returns

A static slice with all miscellaneous operators.

pub fn kind(op: &str) -> ExpressionKind

Returns the expression kind (boolean or instance) to which the given operator evaluates.

Arguments

• op: The eFLINT operator to return the expression kind for.

Returns

An auxillary::ExpressionKind what denotes which of the two kinds it is.

Panics

This function panics if the given string is not one of the eFLINT operators.

pub fn n_operators(op: &str) -> usize

Returns the number of operators required by the given eFLINT operator.

Arguments

• op: The eFLINT operator to return the number of operators for.

Returns

The number of operators.

Panics

This function panics if the given string is not one of the eFLINT operators.

Trait Implementations

impl Clone for EFlintOperator

fn clone(&self) -> EFlintOperator

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for EFlintOperator

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

Formats the value using the given formatter.

impl Copy for EFlintOperator