[−][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
SolverVarName
Update the global to solver var mapping.
For proof checking, the solver variable names are only used for hash computations.
Fields of SolverVarName
UserVarName
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).
Fields of UserVarName
DeleteVar
Delete a variable.
This is only allowed for variables that are isolated and hidden.
Fields of DeleteVar
var: Var
ChangeSamplingMode
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.
Fields of ChangeSamplingMode
AddClause
Add a new input clause.
This is only emitted for clauses added incrementally after an initial solve call.
Fields of AddClause
AtClause
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.
Fields of AtClause
UnitClauses
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.
Fields of UnitClauses
DeleteClause
Delete a clause consisting of the given literals.
Fields of DeleteClause
clause: &'a [Lit]
proof: DeleteClauseProof
ChangeHashBits
Change the number of clause hash bits used
Fields of ChangeHashBits
bits: u32
Model
A (partial) assignment that satisfies all clauses and assumptions.
Fields of Model
Assumptions
Change the active set of assumptions.
This is checked against future model or failed assumptions steps.
Fields of Assumptions
FailedAssumptions
A subset of the assumptions that make the formula unsat.
Fields of FailedAssumptions
End
Signals the end of a proof.
A varisat proof must end with this command or else the checker will complain about an incomplete proof.
Methods
impl<'a> ProofStep<'a>
[src]
pub fn contains_hashes(&self) -> bool
[src]
Does this proof step use clause hashes?
Trait Implementations
impl<'a> Copy for ProofStep<'a>
[src]
impl<'a> Clone for ProofStep<'a>
[src]
fn clone(&self) -> ProofStep<'a>
[src]
fn clone_from(&mut self, source: &Self)
1.0.0[src]
Performs copy-assignment from source
. Read more
impl<'a> Debug for ProofStep<'a>
[src]
Auto Trait Implementations
Blanket Implementations
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> 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,