[−][src]Enum varisat_internal_proof::ProofStep
A single proof step.
Represents a mutation of the current formula and a justification for the mutation's validity.
Variants
Update the global to solver var mapping.
For proof checking, the solver variable names are only used for hash computations.
Update the global to user var mapping.
A variable without user mapping is considered hidden by the checker. When a variable without user mapping gets a user mapping, the sampling mode is initialized to witness.
It's not allowed to change a variable from one user name to another when the variable is in use.
Clause additions and assumptions are only allowed to use variables with user mappings (and a non-witness sampling mode).
Delete a variable.
This is only allowed for variables that are isolated and hidden.
Fields of DeleteVar
var: Var
Changes the sampling mode of a variable.
This is only used to change between Sample and Witness. Hidden is managed by adding or removing a user var name.
Add a new input clause.
This is only emitted for clauses added incrementally after an initial solve call.
Add a clause that is an asymmetric tautoligy (AT).
Assuming the negation of the clause's literals leads to a unit propagation conflict.
The second slice contains the hashes of all clauses involved in the resulting conflict. The order of hashes is the order in which the clauses propagate when all literals of the clause are set false.
When generating DRAT proofs the second slice is ignored and may be empty.
Unit clauses found by top-level unit-propagation.
Pairs of unit clauses and the original clause that became unit. Clauses are in chronological
order. This is equivalent to multiple AtClause
steps where the clause is unit and the
propagation_hashes field contains just one hash, with the difference that this is not output
for DRAT proofs.
Ignored when generating DRAT proofs.
Delete a clause consisting of the given literals.
Fields of DeleteClause
clause: &'a [Lit]
proof: DeleteClauseProof
Change the number of clause hash bits used
Fields of ChangeHashBits
bits: u32
A (partial) assignment that satisfies all clauses and assumptions.
Change the active set of assumptions.
This is checked against future model or failed assumptions steps.
A subset of the assumptions that make the formula unsat.
Signals the end of a proof.
A varisat proof must end with this command or else the checker will complain about an incomplete proof.
Implementations
impl<'a> ProofStep<'a>
[src]
pub fn contains_hashes(&self) -> bool
[src]
Does this proof step use clause hashes?
Trait Implementations
impl<'a> Clone for ProofStep<'a>
[src]
impl<'a> Copy for ProofStep<'a>
[src]
impl<'a> Debug for ProofStep<'a>
[src]
Auto Trait Implementations
impl<'a> RefUnwindSafe for ProofStep<'a>
impl<'a> Send for ProofStep<'a>
impl<'a> Sync for ProofStep<'a>
impl<'a> Unpin for ProofStep<'a>
impl<'a> UnwindSafe for ProofStep<'a>
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut 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>,