1 files changed, 46 insertions, 0 deletions
diff --git a/vendor/varisat-checker/src/context.rs b/vendor/varisat-checker/src/context.rs
new file mode 100644
index 000000000..5cd7e807b
--- /dev/null
+++ b/vendor/varisat-checker/src/context.rs
@@ -0,0 +1,46 @@
+//! Central checker data structure.
+use partial_ref::{part, PartialRefTarget};
+
+use crate::{
+    clauses::Clauses, hash::ClauseHasher, processing::Processing, rup::RupCheck,
+    state::CheckerState, tmp::TmpData, variables::Variables,
+};
+
+/// Part declarations for the [`Context`] struct.
+pub mod parts {
+    use super::*;
+
+    part!(pub CheckerStateP: CheckerState);
+    part!(pub ClauseHasherP: ClauseHasher);
+    part!(pub ClausesP: Clauses);
+    part!(pub ProcessingP<'a>: Processing<'a>);
+    part!(pub RupCheckP: RupCheck);
+    part!(pub TmpDataP: TmpData);
+    part!(pub VariablesP: Variables);
+}
+
+use parts::*;
+
+/// Central checker data structure.
+///
+/// This struct contains all data kept by the checker. Most functions operating on multiple fields
+/// of the context use partial references provided by the `partial_ref` crate. This documents the
+/// data dependencies and makes the borrow checker happy without the overhead of passing individual
+/// references.
+#[derive(PartialRefTarget, Default)]
+pub struct Context<'a> {
+    #[part(CheckerStateP)]
+    pub checker_state: CheckerState,
+    #[part(ClauseHasherP)]
+    pub clause_hasher: ClauseHasher,
+    #[part(ClausesP)]
+    pub clauses: Clauses,
+    #[part(ProcessingP<'a>)]
+    pub processing: Processing<'a>,
+    #[part(RupCheckP)]
+    pub rup_check: RupCheck,
+    #[part(TmpDataP)]
+    pub tmp_data: TmpData,
+    #[part(VariablesP)]
+    pub variables: Variables,
+}