[−][src]Enum varisat::checker::CheckedProofStep
A single step of a proof.
Clauses are identified by a unique increasing id assigned by the checker. Whenever the literals of a clause are included in a step, they are sorted and free of duplicates.
Variants
UserVar
Updates the corresponding user variable for a proof variable.
Fields of UserVar
var: Var
user_var: Option<CheckedUserVar>
AddClause
A clause of the input formula.
Fields of AddClause
DuplicatedClause
A duplicated clause of the input formula.
The checker detects duplicated clauses and will use the same id for all copies. This also applies to clauses of the input formula. This step allows proof processors to identify the input formula's clauses by consecutive ids. When a duplicate clause is found, an id is allocated and this step is emitted. The duplicated clause is not considered part of the formula and the allocated id will not be used in any other steps.
Fields of DuplicatedClause
TautologicalClause
A tautological clause of the input formula.
Tautological clauses can be completely ignored. This step is only used to give an id to a tautological input clause.
Fields of TautologicalClause
AtClause
Addition of an asymmetric tautology (AT).
A clause C is an asymmetric tautology wrt. a formula F, iff unit propagation in F with the
negated literals of C as unit clauses leads to a conflict. The propagations
field contains
clauses in the order they became unit and as last element the clause that caused a conflict.
Fields of AtClause
DeleteClause
Deletion of a redundant clause.
Fields of DeleteClause
DeleteAtClause
Deletion of a clause that is an asymmetric tautology w.r.t the remaining irredundant clauses.
Fields of DeleteAtClause
DeleteRatClause
Deletion of a resolution asymmetric tautology w.r.t the remaining irredundant caluses.
The pivot is always a hidden variable.
Fields of DeleteRatClause
MakeIrredundant
Make a redundant clause irredundant.
Fields of MakeIrredundant
Model
A (partial) assignment that satisfies all clauses and assumptions.
Fields of Model
Assumptions
Change the active set of assumptions.
Fields of Assumptions
FailedAssumptions
Subset of assumptions incompatible with the formula.
The proof consists of showing that the negation of the assumptions is an AT wrt. the formula.
Fields of FailedAssumptions
Trait Implementations
impl<'a> Debug for CheckedProofStep<'a>
[src]
Auto Trait Implementations
impl<'a> Send for CheckedProofStep<'a>
impl<'a> Sync for CheckedProofStep<'a>
Blanket Implementations
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> From<T> for T
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<Reference, Outer, OuterFieldType, Inner> HasPart<Nested<Outer, Inner>> for Reference where
Inner: Part,
Outer: Part<PartType = Field<OuterFieldType>>,
OuterFieldType: HasPart<Inner, RawTarget = OuterFieldType> + PartialRefTarget + ?Sized,
Reference: HasPart<Outer> + ?Sized,
Inner: Part,
Outer: Part<PartType = Field<OuterFieldType>>,
OuterFieldType: HasPart<Inner, RawTarget = OuterFieldType> + PartialRefTarget + ?Sized,
Reference: HasPart<Outer> + ?Sized,
unsafe fn part_ptr(
ptr: *const <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::Ptr
ptr: *const <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::Ptr
unsafe fn part_ptr_mut(
ptr: *mut <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::PtrMut
ptr: *mut <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::PtrMut