Struct varisat::clause::header::ClauseHeader

#[repr(transparent)]
pub struct ClauseHeader {
    pub(super) data: [LitIdx; 3],
}

Metadata for a clause.

This is stored in a ClauseAlloc and thus must have a representation compatible with slice of LitIdx values.

Fields

data: [LitIdx; 3]

Methods

impl ClauseHeader

pub fn new() -> ClauseHeader

Create a new clause header with default entries.

pub fn len(&self) -> usize

Length of the clause.

pub fn set_len(&mut self, length: usize)

Set the length of the clause.

Must be <= Var::max_count() as each variable may only be present once per clause.

pub fn deleted(&self) -> bool

Whether the clause is marked as deleted.

pub fn set_deleted(&mut self, deleted: bool)

Mark the clause as deleted.

pub fn tier(&self) -> Tier

Current Tier of the clause.

pub fn set_tier(&mut self, tier: Tier)

Set the current Tier of the clause.

pub fn redundant(&self) -> bool

Whether the clause is redundant.

pub fn mark(&self) -> bool

Whether the clause is marked.

The mark is a temporary bit that can be set by various routines, but should always be reset to false.

pub fn set_mark(&mut self, mark: bool)

Mark or unmark the clause.

Make sure to clear the mark after use.

pub fn active(&self) -> bool

The clause's active flag

This is set when a clause was involved in conflict analysis and periodically reset.

pub fn set_active(&mut self, active: bool)

Set or reset the clause's active flag.

pub fn glue(&self) -> usize

The glue level.

pub fn set_glue(&mut self, glue: usize)

Update the glue level.

pub fn activity(&self) -> f32

Clause activity.

pub fn set_activity(&mut self, activity: f32)

Update clause activity.

Trait Implementations

impl Copy for ClauseHeader

impl Clone for ClauseHeader

fn clone(&self) -> ClauseHeader

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Default for ClauseHeader

fn default() -> ClauseHeader

Returns the "default value" for a type.