Enum varisat_internal_proof::ProofStep

pub enum ProofStep<'a> {
    SolverVarName {
        global: Var,
        solver: Option<Var>,
    },
    UserVarName {
        global: Var,
        user: Option<Var>,
    },
    DeleteVar {
        var: Var,
    },
    ChangeSamplingMode {
        var: Var,
        sample: bool,
    },
    AddClause {
        clause: &'a [Lit],
    },
    AtClause {
        redundant: bool,
        clause: &'a [Lit],
        propagation_hashes: &'a [ClauseHash],
    },
    UnitClauses {
        units: &'a [(Lit, ClauseHash)],
    },
    DeleteClause {
        clause: &'a [Lit],
        proof: DeleteClauseProof,
    },
    ChangeHashBits {
        bits: u32,
    },
    Model {
        assignment: &'a [Lit],
    },
    Assumptions {
        assumptions: &'a [Lit],
    },
    FailedAssumptions {
        failed_core: &'a [Lit],
        propagation_hashes: &'a [ClauseHash],
    },
    End,
}

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

global: Varsolver: Option<Var>

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

global: Varuser: Option<Var>

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

var: Varsample: bool

AddClause

Add a new input clause.

This is only emitted for clauses added incrementally after an initial solve call.

Fields of AddClause

clause: &'a [Lit]

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

redundant: boolclause: &'a [Lit]propagation_hashes: &'a [ClauseHash]

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

units: &'a [(Lit, ClauseHash)]

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

assignment: &'a [Lit]

Assumptions

Change the active set of assumptions.

This is checked against future model or failed assumptions steps.

Fields of Assumptions

assumptions: &'a [Lit]

FailedAssumptions

A subset of the assumptions that make the formula unsat.

Fields of FailedAssumptions

failed_core: &'a [Lit]propagation_hashes: &'a [ClauseHash]

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.

Implementations

impl<'a> ProofStep<'a>

pub fn contains_hashes(&self) -> bool

Does this proof step use clause hashes?

Trait Implementations

impl<'a> Clone for ProofStep<'a>

fn clone(&self) -> ProofStep<'a>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'a> Copy for ProofStep<'a>

impl<'a> Debug for ProofStep<'a>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.