Struct varisat_checker::context::Context

pub struct Context<'a> {
    pub checker_state: CheckerState,
    pub clause_hasher: ClauseHasher,
    pub clauses: Clauses,
    pub processing: Processing<'a>,
    pub rup_check: RupCheck,
    pub tmp_data: TmpData,
    pub variables: Variables,
}

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.

Fields

checker_state: CheckerState

clause_hasher: ClauseHasher

clauses: Clauses

processing: Processing<'a>

rup_check: RupCheck

tmp_data: TmpData

variables: Variables

Trait Implementations

impl<'a> Default for Context<'a>

fn default() -> Context<'a>

Returns the "default value" for a type.

impl<'a> PartialRefTarget for Context<'a>

type RawTarget = Self

A partial reference will be represented by a pointer to this associated type.

impl<'a1, 'a> IntoPartialRef<'a1> for &'a1 Context<'a>

type Ref = Const<VariablesP, Const<TmpDataP, Const<RupCheckP, Const<ProcessingP<'a>, Const<ClausesP, Const<ClauseHasherP, Const<CheckerStateP, Ref<'a1, Context<'a>>>>>>>>>

fn into_partial_ref(self) -> Self::Ref

Convert a mutable or immutable reference into a partial reference.

impl<'a1, 'a> IntoPartialRef<'a1> for &'a1 mut Context<'a>

type Ref = Mut<VariablesP, Mut<TmpDataP, Mut<RupCheckP, Mut<ProcessingP<'a>, Mut<ClausesP, Mut<ClauseHasherP, Mut<CheckerStateP, Ref<'a1, Context<'a>>>>>>>>>

fn into_partial_ref(self) -> Self::Ref

Convert a mutable or immutable reference into a partial reference.

impl<'a1, 'a, ContainingPart, Reference> SplitIntoParts<'a1, ContainingPart, Reference> for Context<'a> where
    ContainingPart: Part<PartType = Field<Self>>,
    Reference: PartialRef<'a1>,
    Reference::Target: HasPart<ContainingPart>, 

type Result = Const<Nested<ContainingPart, VariablesP>, Const<Nested<ContainingPart, TmpDataP>, Const<Nested<ContainingPart, RupCheckP>, Const<Nested<ContainingPart, ProcessingP<'a>>, Const<Nested<ContainingPart, ClausesP>, Const<Nested<ContainingPart, ClauseHasherP>, Const<Nested<ContainingPart, CheckerStateP>, Reference>>>>>>>

A partial reference that has all the parts Reference and all parts of Self nested in ContainingPart as constant parts.

type ResultMut = Mut<Nested<ContainingPart, VariablesP>, Mut<Nested<ContainingPart, TmpDataP>, Mut<Nested<ContainingPart, RupCheckP>, Mut<Nested<ContainingPart, ProcessingP<'a>>, Mut<Nested<ContainingPart, ClausesP>, Mut<Nested<ContainingPart, ClauseHasherP>, Mut<Nested<ContainingPart, CheckerStateP>, Reference>>>>>>>

A partial reference that has all the parts Reference and all parts of Self nested in ContainingPart as mutable parts.

impl<'a> HasPart<CheckerStateP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<CheckerStateP as Part>::PartType as PartType>::Ptr

Given a constant pointer to a target, produce a constant pointer to a part of it.

unsafe fn part_ptr_mut(
    ptr: *mut Self
) -> <<CheckerStateP as Part>::PartType as PartType>::PtrMut

Given a mutable pointer to a target, produce a mutable pointer to a part of it.

impl<'a> HasPart<ClauseHasherP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<ClauseHasherP as Part>::PartType as PartType>::Ptr

Given a constant pointer to a target, produce a constant pointer to a part of it.

unsafe fn part_ptr_mut(
    ptr: *mut Self
) -> <<ClauseHasherP as Part>::PartType as PartType>::PtrMut

Given a mutable pointer to a target, produce a mutable pointer to a part of it.

impl<'a> HasPart<ClausesP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<ClausesP as Part>::PartType as PartType>::Ptr

Given a constant pointer to a target, produce a constant pointer to a part of it.

unsafe fn part_ptr_mut(
    ptr: *mut Self
) -> <<ClausesP as Part>::PartType as PartType>::PtrMut

Given a mutable pointer to a target, produce a mutable pointer to a part of it.

impl<'a> HasPart<ProcessingP<'a>> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<ProcessingP<'a> as Part>::PartType as PartType>::Ptr

Given a constant pointer to a target, produce a constant pointer to a part of it.

unsafe fn part_ptr_mut(
    ptr: *mut Self
) -> <<ProcessingP<'a> as Part>::PartType as PartType>::PtrMut

Given a mutable pointer to a target, produce a mutable pointer to a part of it.

impl<'a> HasPart<RupCheckP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<RupCheckP as Part>::PartType as PartType>::Ptr

Given a constant pointer to a target, produce a constant pointer to a part of it.

unsafe fn part_ptr_mut(
    ptr: *mut Self
) -> <<RupCheckP as Part>::PartType as PartType>::PtrMut

Given a mutable pointer to a target, produce a mutable pointer to a part of it.

impl<'a> HasPart<TmpDataP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<TmpDataP as Part>::PartType as PartType>::Ptr

Given a constant pointer to a target, produce a constant pointer to a part of it.

unsafe fn part_ptr_mut(
    ptr: *mut Self
) -> <<TmpDataP as Part>::PartType as PartType>::PtrMut

Given a mutable pointer to a target, produce a mutable pointer to a part of it.

impl<'a> HasPart<VariablesP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<VariablesP as Part>::PartType as PartType>::Ptr

Given a constant pointer to a target, produce a constant pointer to a part of it.

unsafe fn part_ptr_mut(
    ptr: *mut Self
) -> <<VariablesP as Part>::PartType as PartType>::PtrMut

Given a mutable pointer to a target, produce a mutable pointer to a part of it.