[−][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
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
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
Auto Trait Implementations
impl<'a> Send for CheckedProofStep<'a>
impl<'a> Sync for CheckedProofStep<'a>
Blanket Implementations
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
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,