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/clause.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/clause.rs')
-rw-r--r-- | vendor/varisat/src/clause.rs | 67 |
1 files changed, 67 insertions, 0 deletions
diff --git a/vendor/varisat/src/clause.rs b/vendor/varisat/src/clause.rs new file mode 100644 index 000000000..0d3591858 --- /dev/null +++ b/vendor/varisat/src/clause.rs @@ -0,0 +1,67 @@ +//! Clause storage. +use std::slice; + +use varisat_formula::{lit::LitIdx, Lit}; + +pub mod activity; +pub mod alloc; +pub mod assess; +pub mod db; +pub mod gc; +pub mod header; +pub mod reduce; + +pub use activity::{bump_clause_activity, decay_clause_activities, ClauseActivity}; +pub use alloc::{ClauseAlloc, ClauseRef}; +pub use assess::{assess_learned_clause, bump_clause}; +pub use db::{ClauseDb, Tier}; +pub use gc::collect_garbage; +pub use header::ClauseHeader; + +use header::HEADER_LEN; + +/// A clause. +/// +/// This is stoed in a [`ClauseAlloc`] and thus must have a representation compatible with slice of +/// [`LitIdx`] values. +/// +/// It would be nicer to use a DST struct with two members and `repr(C)`, but while that can be +/// declared in stable rust, it's almost impossible to work with. +#[repr(transparent)] +pub struct Clause { + data: [LitIdx], +} + +impl Clause { + /// The clause's header + pub fn header(&self) -> &ClauseHeader { + unsafe { + let header_ptr = self.data.as_ptr() as *const ClauseHeader; + &*header_ptr + } + } + + /// Mutable reference to the clause's header + pub fn header_mut(&mut self) -> &mut ClauseHeader { + unsafe { + let header_ptr = self.data.as_mut_ptr() as *mut ClauseHeader; + &mut *header_ptr + } + } + + /// The clause's literals + pub fn lits(&self) -> &[Lit] { + unsafe { + let lit_ptr = self.data.as_ptr().add(HEADER_LEN) as *const Lit; + slice::from_raw_parts(lit_ptr, self.data.len() - HEADER_LEN) + } + } + + /// Mutable slice of the clause's literals + pub fn lits_mut(&mut self) -> &mut [Lit] { + unsafe { + let lit_ptr = self.data.as_mut_ptr().add(HEADER_LEN) as *mut Lit; + slice::from_raw_parts_mut(lit_ptr, self.data.len() - HEADER_LEN) + } + } +} |