Enum RewriteRule 

pub enum RewriteRule {
    DistributeAndOverOr,
    DistributeOrOverAnd,
    FactorCommonAnd,
    FactorCommonOr,
    PushExistsInward,
    PushForallInward,
    PullExistsOutward,
    PullForallOutward,
    MergeNestedExists,
    MergeNestedForall,
    ReorderConjunctions,
    ReorderDisjunctions,
}

Rewriting rule for generating equivalent expressions.

Variants

DistributeAndOverOr

Distribute conjunction over disjunction: A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C)

DistributeOrOverAnd

Distribute disjunction over conjunction: A ∨ (B ∧ C) → (A ∨ B) ∧ (A ∨ C)

FactorCommonAnd

Factor common terms: (A ∧ B) ∨ (A ∧ C) → A ∧ (B ∨ C)

FactorCommonOr

Factor common terms: (A ∨ B) ∧ (A ∨ C) → A ∨ (B ∧ C)

PushExistsInward

Push quantifiers inward: ∃x. (P ∧ Q) → (∃x. P) ∧ Q (if x not in Q)

PushForallInward

Push quantifiers inward: ∀x. (P ∧ Q) → (∀x. P) ∧ Q (if x not in Q)

PullExistsOutward

Pull quantifiers outward: (∃x. P) ∧ Q → ∃x. (P ∧ Q) (if x not in Q)

PullForallOutward

Pull quantifiers outward: (∀x. P) ∧ Q → ∀x. (P ∧ Q) (if x not in Q)

MergeNestedExists

Convert nested quantifiers: ∃x. ∃y. P → ∃x,y. P

MergeNestedForall

Convert nested quantifiers: ∀x. ∀y. P → ∀x,y. P

ReorderConjunctions

Reorder conjunctions based on selectivity

ReorderDisjunctions

Reorder disjunctions based on short-circuit potential

Trait Implementations

impl Clone for RewriteRule

fn clone(&self) -> RewriteRule

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RewriteRule

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

Formats the value using the given formatter.

impl Eq for RewriteRule

impl Hash for RewriteRule

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, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for RewriteRule

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for RewriteRule