Enum SatEncodingDecision 

pub enum SatEncodingDecision {
    Assert(Expression),
    AtMostOne {
        inputs: Vec<Expression>,
        encoding: Option<EncodingSelection<AmoEncoding>>,
    },
    Cardinality {
        inputs: Vec<Expression>,
        relation: CardinalityRelation,
        bound: i64,
        encoding: Option<EncodingSelection<CardinalityEncoding>>,
    },
    CountRelation {
        output: Expression,
        inputs: Vec<Expression>,
        relation: IntegerRelation,
        bound: i64,
        encoding: Option<EncodingSelection<CardinalityEncoding>>,
        amo_encoding: Option<EncodingSelection<AmoEncoding>>,
    },
    PseudoBoolean {
        terms: Vec<(i64, Expression)>,
        groups: Vec<PbTermGroup>,
        relation: CardinalityRelation,
        bound: i64,
        encoding: Option<EncodingSelection<PbEncoding>>,
    },
    IntegerRelation {
        output: Expression,
        terms: Vec<(i64, Expression)>,
        groups: Vec<PbTermGroup>,
        relation: IntegerRelation,
        bound: i64,
        encoding: Option<EncodingSelection<PbEncoding>>,
    },
    Objective {
        minimise: bool,
        value: SatIntegerView,
        encoding: Option<EncodingSelection<PbEncoding>>,
    },
    AllDifferent {
        output: Expression,
        inputs: Vec<SatIntegerView>,
        comparisons: Option<Vec<Expression>>,
        except: Option<SatIntegerView>,
        encoding: Option<EncodingSelection<AllDifferentEncoding>>,
        amo_encoding: Option<EncodingSelection<AmoEncoding>>,
        pb_encoding: Option<EncodingSelection<PbEncoding>>,
    },
    Table {
        output: Expression,
        inputs: Vec<SatIntegerView>,
        rows: Vec<Vec<i64>>,
        row_views: Option<Vec<Vec<SatIntegerView>>>,
        negative: bool,
        encoding: Option<EncodingSelection<TableEncoding>>,
        pb_encoding: Option<EncodingSelection<PbEncoding>>,
    },
    Element {
        index_view: SatIntegerView,
        value: SatIntegerView,
        entries: Vec<(i64, SatIntegerView)>,
        encoding: Option<EncodingSelection<ElementEncoding>>,
        pb_encoding: Option<EncodingSelection<PbEncoding>>,
    },
    Boolean {
        output: Expression,
        expression: Expression,
    },
}

A Boolean operation whose truth is asserted or bound to a named output.

Variants

Assert(Expression)

Assert the semantic Boolean expression; the adaptor chooses clauses and witnesses.

AtMostOne

At most one input may be true; the selected library algorithm is recorded explicitly.

Fields

inputs: Vec<Expression>

encoding: Option<EncodingSelection<AmoEncoding>>

Cardinality

Compare the number of true operands with a mathematical integer bound.

Fields

inputs: Vec<Expression>

relation: CardinalityRelation

bound: i64

encoding: Option<EncodingSelection<CardinalityEncoding>>

CountRelation

Define the truth of a Boolean count comparison using cardinality and AMO providers.

Fields

output: Expression

inputs: Vec<Expression>

relation: IntegerRelation

bound: i64

encoding: Option<EncodingSelection<CardinalityEncoding>>

amo_encoding: Option<EncodingSelection<AmoEncoding>>

Selected when either implication includes an at-most-one threshold.

PseudoBoolean

Compare a signed weighted Boolean sum with an integer bound.

Fields

terms: Vec<(i64, Expression)>

groups: Vec<PbTermGroup>

Relationships already guaranteed by the integer representation constraints.

relation: CardinalityRelation

bound: i64

encoding: Option<EncodingSelection<PbEncoding>>

IntegerRelation

Define an integer relation over a signed weighted view of the numeric operands.

Fields

output: Expression

terms: Vec<(i64, Expression)>

groups: Vec<PbTermGroup>

relation: IntegerRelation

bound: i64

encoding: Option<EncodingSelection<PbEncoding>>

Objective

Minimise or maximise an actual-value integer view using the selected PB provider.

Fields

minimise: bool

value: SatIntegerView

encoding: Option<EncodingSelection<PbEncoding>>

AllDifferent

Define scalar or whole-value distinctness, with an optional repeated exception value.

Fields

output: Expression

inputs: Vec<SatIntegerView>

comparisons: Option<Vec<Expression>>

Pair conditions for compound values, lowered through the existing equality rules.

except: Option<SatIntegerView>

This value may occur repeatedly.

encoding: Option<EncodingSelection<AllDifferentEncoding>>

amo_encoding: Option<EncodingSelection<AmoEncoding>>

pb_encoding: Option<EncodingSelection<PbEncoding>>

Table

Define membership in an integer/Boolean relation.

Fields

output: Expression

inputs: Vec<SatIntegerView>

rows: Vec<Vec<i64>>

row_views: Option<Vec<Vec<SatIntegerView>>>

Non-constant relation cells retain their numeric representation views.

negative: bool

encoding: Option<EncodingSelection<TableEncoding>>

pb_encoding: Option<EncodingSelection<PbEncoding>>

Element

Define a selected scalar value; out-of-domain indices leave it unconstrained.

Fields

index_view: SatIntegerView

value: SatIntegerView

entries: Vec<(i64, SatIntegerView)>

encoding: Option<EncodingSelection<ElementEncoding>>

pb_encoding: Option<EncodingSelection<PbEncoding>>

Boolean

Define an output as equivalent to a semantic Boolean expression.

Fields

output: Expression

expression: Expression

Implementations

impl SatEncodingDecision

pub fn expressions(&self) -> Vec<&Expression>

Semantic expressions held by this decision.

Trait Implementations

impl Biplate<DeclarationPtr> for SatEncodingDecision

fn biplate( &self, ) -> (Tree<DeclarationPtr>, Box<dyn Fn(Tree<DeclarationPtr>) -> SatEncodingDecision>)

Definition of a Biplate.

fn with_children_bi(&self, children: VecDeque<To>) -> Self

Reconstructs the node with the given children.

fn descend_bi(&self, op: &impl Fn(To) -> To) -> Self

Biplate variant of [Uniplate::descend]

fn universe_bi(&self) -> VecDeque<To>

Gets all children of a node, including itself and all children.

fn children_bi(&self) -> VecDeque<To>

Returns the children of a type. If to == from then it returns the original element (in contrast to children).

fn children_bi_count(&self) -> usize

Number of children that would be returned by children_bi.

fn try_replace_child_at_bi(&mut self, index: usize, child: To) -> bool

Replaces the indexth child of type To within self.

fn transform_bi(&self, op: &impl Fn(To) -> To) -> Self

Applies the given function to all nodes bottom up.

fn holes_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>

Returns an iterator over all direct children of the input, paired with a function that “fills the hole” where the child was with a new value.

fn contexts_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>

Returns an iterator over the universe of the input, paired with a function that “fills the hole” where the child was with a new value.

impl Biplate<Expression> for SatEncodingDecision

fn biplate( &self, ) -> (Tree<Expression>, Box<dyn Fn(Tree<Expression>) -> SatEncodingDecision>)

Definition of a Biplate.

fn with_children_bi(&self, children: VecDeque<To>) -> Self

Reconstructs the node with the given children.

fn descend_bi(&self, op: &impl Fn(To) -> To) -> Self

Biplate variant of [Uniplate::descend]

fn universe_bi(&self) -> VecDeque<To>

Gets all children of a node, including itself and all children.

fn children_bi(&self) -> VecDeque<To>

Returns the children of a type. If to == from then it returns the original element (in contrast to children).

fn children_bi_count(&self) -> usize

Number of children that would be returned by children_bi.

fn try_replace_child_at_bi(&mut self, index: usize, child: To) -> bool

Replaces the indexth child of type To within self.

fn transform_bi(&self, op: &impl Fn(To) -> To) -> Self

Applies the given function to all nodes bottom up.

fn holes_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>

Returns an iterator over all direct children of the input, paired with a function that “fills the hole” where the child was with a new value.

fn contexts_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>

Returns an iterator over the universe of the input, paired with a function that “fills the hole” where the child was with a new value.

impl Biplate<SatEncodingDecision> for SatEncodingDecision

fn biplate( &self, ) -> (Tree<SatEncodingDecision>, Box<dyn Fn(Tree<SatEncodingDecision>) -> SatEncodingDecision>)

Definition of a Biplate.

fn children_bi_count(&self) -> usize

Number of children that would be returned by children_bi.

fn try_replace_child_at_bi( &mut self, index: usize, child: SatEncodingDecision, ) -> bool

Replaces the indexth child of type To within self.

fn with_children_bi(&self, children: VecDeque<To>) -> Self

Reconstructs the node with the given children.

fn descend_bi(&self, op: &impl Fn(To) -> To) -> Self

Biplate variant of [Uniplate::descend]

fn universe_bi(&self) -> VecDeque<To>

Gets all children of a node, including itself and all children.

fn children_bi(&self) -> VecDeque<To>

Returns the children of a type. If to == from then it returns the original element (in contrast to children).

fn transform_bi(&self, op: &impl Fn(To) -> To) -> Self

Applies the given function to all nodes bottom up.

fn holes_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>

Returns an iterator over all direct children of the input, paired with a function that “fills the hole” where the child was with a new value.

fn contexts_bi(&self) -> impl Iterator<Item = (To, impl Fn(To))>

Returns an iterator over the universe of the input, paired with a function that “fills the hole” where the child was with a new value.

impl Clone for SatEncodingDecision

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SatEncodingDecision

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for SatEncodingDecision

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Display for SatEncodingDecision

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

Formats the value using the given formatter.

impl Eq for SatEncodingDecision

impl Hash for SatEncodingDecision

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 SatEncodingDecision

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

Equality operator ==.

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

Inequality operator !=.

impl Serialize for SatEncodingDecision

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

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for SatEncodingDecision

impl Uniplate for SatEncodingDecision

fn uniplate( &self, ) -> (Tree<SatEncodingDecision>, Box<dyn Fn(Tree<SatEncodingDecision>) -> SatEncodingDecision>)

Definition of a Uniplate.

fn try_replace_child_at( &mut self, index: usize, child: SatEncodingDecision, ) -> bool

Replaces the indexth direct child of self.

fn descend(&self, op: &impl Fn(Self) -> Self) -> Self

Applies a function to all direct children of this

fn universe(&self) -> VecDeque<Self>

Gets all children of a node, including itself and all children.

fn children(&self) -> VecDeque<Self>

Gets the direct children (maximal substructures) of a node.

fn with_children(&self, children: VecDeque<Self>) -> Self

Reconstructs the node with the given children.

fn transform(&self, f: &impl Fn(Self) -> Self) -> Self

Applies the given function to all nodes bottom up.

fn rewrite(&self, f: &impl Fn(Self) -> Option<Self>) -> Self

Rewrites by applying a rule everywhere it can.

fn cata<T>(&self, op: &impl Fn(Self, VecDeque<T>) -> T) -> T

Performs a fold-like computation on each value.

fn holes(&self) -> impl Iterator<Item = (Self, impl Fn(Self))>

Returns an iterator over all direct children of the input, paired with a function that “fills the hole” where the child was with a new value.

fn contexts(&self) -> impl Iterator<Item = (Self, impl Fn(Self))>

Returns an iterator over the universe of the input, paired with a function that “fills the hole” where the child was with a new value.

Layout

Note: Most layout information is completely unstable and may even differ between compilations. The only exception is types with certain repr(...) attributes. Please see the Rust Reference's “Type Layout” chapter for details on type layout guarantees.

Size: 288 bytes

Size for each variant:

• Assert: 152 bytes
• AtMostOne: 40 bytes
• Cardinality: 48 bytes
• CountRelation: 192 bytes
• PseudoBoolean: 72 bytes
• IntegerRelation: 216 bytes
• Objective: 96 bytes
• AllDifferent: 288 bytes
• Table: 232 bytes
• Element: 200 bytes
• Boolean: 288 bytes