diff options
author | Daniel Baumann <daniel.baumann@progress-linux.org> | 2024-05-18 02:49:50 +0000 |
---|---|---|
committer | Daniel Baumann <daniel.baumann@progress-linux.org> | 2024-05-18 02:49:50 +0000 |
commit | 9835e2ae736235810b4ea1c162ca5e65c547e770 (patch) | |
tree | 3fcebf40ed70e581d776a8a4c65923e8ec20e026 /vendor/varisat/src/variables/data.rs | |
parent | Releasing progress-linux version 1.70.0+dfsg2-1~progress7.99u1. (diff) | |
download | rustc-9835e2ae736235810b4ea1c162ca5e65c547e770.tar.xz rustc-9835e2ae736235810b4ea1c162ca5e65c547e770.zip |
Merging upstream version 1.71.1+dfsg1.
Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>
Diffstat (limited to 'vendor/varisat/src/variables/data.rs')
-rw-r--r-- | vendor/varisat/src/variables/data.rs | 70 |
1 files changed, 70 insertions, 0 deletions
diff --git a/vendor/varisat/src/variables/data.rs b/vendor/varisat/src/variables/data.rs new file mode 100644 index 000000000..ea29e6280 --- /dev/null +++ b/vendor/varisat/src/variables/data.rs @@ -0,0 +1,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() + } + } +} |