Enum varisat::variables::data::SamplingMode

pub enum SamplingMode {
    Sample,
    Witness,
    Hide,
}

Variable sampling mode.

This partitions all variables into three sets. Using these partitions it is possible to specify equivalence vs. equisatisfiability per variable. Let V be the set of all variables, S, W and H the sets of Sampling, Witness and Hidden variables. Let F be the input formula and G be the current formula. The following invariants are upheld:

• The formulas are always equisatisfiable: (∃ V) G ⇔ (∃ V) F
• Restricted to the sampling variables they are equivalent: (∀ S) ((∃ V∖S) G ⇔ (∃ V∖S) F)
• Restricted to the non-hidden variables the input formula is implied: (∀ V∖H) ((∃ H) G ⇒ (∃ H) F)

This ensures that the solver will be able to find and extend each satisfiable assignment of the sampling variables to an assignment that covers the witness variables.

Variants

SampleWitnessHide

Trait Implementations

impl Eq for SamplingMode

fn assert_receiver_is_total_eq(&self)

impl PartialEq<SamplingMode> for SamplingMode

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

This method tests for self and other values to be equal, and is used by ==.

#[must_use]

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

This method tests for !=.

impl Copy for SamplingMode

impl Clone for SamplingMode

fn clone(&self) -> SamplingMode

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for SamplingMode

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

Formats the value using the given formatter.