1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70

//! Data associated with variables.

/// 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.

#[derive(Copy, Clone, PartialEq, Eq, Debug)]
pub enum SamplingMode {
    Sample,
    Witness,
    Hide,
}

/// Data associated with variables.
///
/// This is available for each _global_ variable, even if eliminated within the solver.
#[derive(Clone)]
pub struct VarData {
    /// The variable's sampling mode.
    pub sampling_mode: SamplingMode,
    /// Whether the variable is forced by a unit clause.
    ///
    /// This is used to remember unit clauses after they are removed from the solver.
    pub unit: Option<bool>,
    /// True if there are no clauses containing this variable and other variables.
    ///
    /// This is the case if there are no clauses containing this variable or just a unit clause with
    /// this variable.
    pub isolated: bool,
    /// True if this variable is part of the current assumptions.
    pub assumed: bool,
    /// Whether the global variable was deleted.
    pub deleted: bool,
}

impl Default for VarData {
    fn default() -> VarData {
        VarData {
            sampling_mode: SamplingMode::Hide,
            unit: None,
            isolated: true,
            assumed: false,
            deleted: true,
        }
    }
}

impl VarData {
    /// Default variable data for a new user variable.
    pub fn user_default() -> VarData {
        VarData {
            sampling_mode: SamplingMode::Sample,
            deleted: false,
            ..VarData::default()
        }
    }
}