eflint_json::spec::appendix

Struct EFlintOperator

Source
pub struct EFlintOperator;
Expand description

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§

Source§

impl EFlintOperator

Source

pub const ADD: &str = "ADD"

Arithmetic addition on two numeric values.

Source

pub const AND: &str = "AND"

Conjunction on two boolean values.

Source

pub const COUNT: &str = "COUNT"

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

Source

pub const DIV: &str = "DIV"

Arithmetic division on two numeric values.

Source

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.

Source

pub const EQUALS: &str = "EQ"

Checks if two values are equal.

Source

pub const GREATER: &str = "GT"

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

Source

pub const GREATER_OR_EQUALS: &str = "GE"

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

Source

pub const HOLDS: &str = "HOLDS"

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

Source

pub const LESSER: &str = "LT"

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

Source

pub const LESSER_OR_EQUALS: &str = "LE"

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

Source

pub const MAX: &str = "MAX"

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

Source

pub const MIN: &str = "MIN"

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

Source

pub const MOD: &str = "MOD"

Arithmetic modulo on two numeric values.

Source

pub const MUL: &str = "MUL"

Arithmetic multiplication on two numeric values.

Source

pub const NOT: &str = "NOT"

Negation on one boolean value.

Source

pub const NOT_EQUALS: &str = "NE"

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

Source

pub const OR: &str = "OR"

Disjunction on two boolean values.

Source

pub const SUB: &str = "SUB"

Arithmetic subtraction on two numeric values.

Source

pub const SUM: &str = "SUM"

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

Source

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.

Source

pub const WHEN: &str = "WHEN"

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

Source

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

Returns a list of all the eFLINT operators known.

§Returns

A static slice with all operators.

Source

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.

Source

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.

Source

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.

Source

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.

Source

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.

Source

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.

Source

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§

Source§

impl Clone for EFlintOperator

Source§

fn clone(&self) -> EFlintOperator

Returns a copy of the value. Read more
1.0.0 · Source§

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

Performs copy-assignment from source. Read more
Source§

impl Debug for EFlintOperator

Source§

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

Formats the value using the given formatter. Read more
Source§

impl Copy for EFlintOperator

Auto Trait Implementations§

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> CloneToUninit for T
where T: Clone,

Source§

unsafe fn clone_to_uninit(&self, dst: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)
Performs copy-assignment from self to dst. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<T> ToOwned for T
where T: Clone,

Source§

type Owned = T

The resulting type after obtaining ownership.
Source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
Source§

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more
Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.