Enum ExtensionType 

pub enum ExtensionType {
    And(Lit, Lit),
    Or(Lit, Lit),
    Xor(Lit, Lit),
    Ite {
        cond: Lit,
        then_lit: Lit,
        else_lit: Lit,
    },
    Equiv(Lit, Lit),
    General {
        positive: Vec<Lit>,
        negative: Vec<Lit>,
    },
}

Types of extension variable definitions

Variants

And(Lit, Lit)

AND: z ↔ (x ∧ y)

Or(Lit, Lit)

OR: z ↔ (x ∨ y)

Xor(Lit, Lit)

XOR: z ↔ (x ⊕ y)

Ite

ITE: z ↔ (if c then t else e)

Fields

cond: Lit

Condition literal

then_lit: Lit

Then branch literal

else_lit: Lit

Else branch literal

Equiv(Lit, Lit)

Equivalence: z ↔ (x ↔ y)

General

General definition from conjunction/disjunction

Fields

positive: Vec<Lit>

Positive literals in the definition

negative: Vec<Lit>

Negative literals in the definition

Trait Implementations

impl Clone for ExtensionType

fn clone(&self) -> ExtensionType

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ExtensionType

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

Formats the value using the given formatter.