Struct varisat::context::Context

pub struct Context<'a> {
    pub analyze_conflict: AnalyzeConflict,
    pub assignment: Assignment,
    pub binary_clauses: BinaryClauses,
    pub clause_activity: ClauseActivity,
    pub clause_alloc: ClauseAlloc,
    pub clause_db: ClauseDb,
    pub impl_graph: ImplGraph,
    pub assumptions: Assumptions,
    pub model: Model,
    pub proof: Proof<'a>,
    pub schedule: Schedule,
    pub solver_config: SolverConfig,
    pub solver_state: SolverState,
    pub tmp_data: TmpData,
    pub tmp_flags: TmpFlags,
    pub trail: Trail,
    pub variables: Variables,
    pub vsids: Vsids,
    pub watchlists: Watchlists,
}

Central solver data structure.

This struct contains all data kept by the solver. 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

analyze_conflict: AnalyzeConflict

assignment: Assignment

binary_clauses: BinaryClauses

clause_activity: ClauseActivity

clause_alloc: ClauseAlloc

clause_db: ClauseDb

impl_graph: ImplGraph

assumptions: Assumptions

model: Model

proof: Proof<'a>

schedule: Schedule

solver_config: SolverConfig

solver_state: SolverState

tmp_data: TmpData

tmp_flags: TmpFlags

trail: Trail

variables: Variables

vsids: Vsids

watchlists: Watchlists

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<WatchlistsP, Const<VsidsP, Const<VariablesP, Const<TrailP, Const<TmpFlagsP, Const<TmpDataP, Const<SolverStateP, Const<SolverConfigP, Const<ScheduleP, Const<ProofP<'a>, Const<ModelP, Const<AssumptionsP, Const<ImplGraphP, Const<ClauseDbP, Const<ClauseAllocP, Const<ClauseActivityP, Const<BinaryClausesP, Const<AssignmentP, Const<AnalyzeConflictP, 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<WatchlistsP, Mut<VsidsP, Mut<VariablesP, Mut<TrailP, Mut<TmpFlagsP, Mut<TmpDataP, Mut<SolverStateP, Mut<SolverConfigP, Mut<ScheduleP, Mut<ProofP<'a>, Mut<ModelP, Mut<AssumptionsP, Mut<ImplGraphP, Mut<ClauseDbP, Mut<ClauseAllocP, Mut<ClauseActivityP, Mut<BinaryClausesP, Mut<AssignmentP, Mut<AnalyzeConflictP, 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, WatchlistsP>, Const<Nested<ContainingPart, VsidsP>, Const<Nested<ContainingPart, VariablesP>, Const<Nested<ContainingPart, TrailP>, Const<Nested<ContainingPart, TmpFlagsP>, Const<Nested<ContainingPart, TmpDataP>, Const<Nested<ContainingPart, SolverStateP>, Const<Nested<ContainingPart, SolverConfigP>, Const<Nested<ContainingPart, ScheduleP>, Const<Nested<ContainingPart, ProofP<'a>>, Const<Nested<ContainingPart, ModelP>, Const<Nested<ContainingPart, AssumptionsP>, Const<Nested<ContainingPart, ImplGraphP>, Const<Nested<ContainingPart, ClauseDbP>, Const<Nested<ContainingPart, ClauseAllocP>, Const<Nested<ContainingPart, ClauseActivityP>, Const<Nested<ContainingPart, BinaryClausesP>, Const<Nested<ContainingPart, AssignmentP>, Const<Nested<ContainingPart, AnalyzeConflictP>, 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, WatchlistsP>, Mut<Nested<ContainingPart, VsidsP>, Mut<Nested<ContainingPart, VariablesP>, Mut<Nested<ContainingPart, TrailP>, Mut<Nested<ContainingPart, TmpFlagsP>, Mut<Nested<ContainingPart, TmpDataP>, Mut<Nested<ContainingPart, SolverStateP>, Mut<Nested<ContainingPart, SolverConfigP>, Mut<Nested<ContainingPart, ScheduleP>, Mut<Nested<ContainingPart, ProofP<'a>>, Mut<Nested<ContainingPart, ModelP>, Mut<Nested<ContainingPart, AssumptionsP>, Mut<Nested<ContainingPart, ImplGraphP>, Mut<Nested<ContainingPart, ClauseDbP>, Mut<Nested<ContainingPart, ClauseAllocP>, Mut<Nested<ContainingPart, ClauseActivityP>, Mut<Nested<ContainingPart, BinaryClausesP>, Mut<Nested<ContainingPart, AssignmentP>, Mut<Nested<ContainingPart, AnalyzeConflictP>, Reference>>>>>>>>>>>>>>>>>>>

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

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

unsafe fn part_ptr(
    ptr: *const Self
) -> <<AnalyzeConflictP 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
) -> <<AnalyzeConflictP 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<AssignmentP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<AssignmentP 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
) -> <<AssignmentP 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<BinaryClausesP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<BinaryClausesP 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
) -> <<BinaryClausesP 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<ClauseActivityP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<ClauseActivityP 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
) -> <<ClauseActivityP 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<ClauseAllocP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<ClauseAllocP 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
) -> <<ClauseAllocP 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<ClauseDbP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<ClauseDbP 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
) -> <<ClauseDbP 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<ImplGraphP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<ImplGraphP 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
) -> <<ImplGraphP 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<AssumptionsP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<AssumptionsP 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
) -> <<AssumptionsP 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<ModelP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<ModelP 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
) -> <<ModelP 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<ProofP<'a>> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<ProofP<'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
) -> <<ProofP<'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<ScheduleP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<ScheduleP 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
) -> <<ScheduleP 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<SolverConfigP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<SolverConfigP 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
) -> <<SolverConfigP 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<SolverStateP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<SolverStateP 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
) -> <<SolverStateP 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<TmpFlagsP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<TmpFlagsP 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
) -> <<TmpFlagsP 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<TrailP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<TrailP 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
) -> <<TrailP 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.

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

unsafe fn part_ptr(
    ptr: *const Self
) -> <<VsidsP 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
) -> <<VsidsP 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<WatchlistsP> for Context<'a>

unsafe fn part_ptr(
    ptr: *const Self
) -> <<WatchlistsP 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
) -> <<WatchlistsP as Part>::PartType as PartType>::PtrMut

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