Enum varisat_checker::CheckedProofStep

pub enum CheckedProofStep<'a> {
    UserVar {
        var: Var,
        user_var: Option<CheckedUserVar>,
    },
    AddClause {
        id: u64,
        clause: &'a [Lit],
    },
    DuplicatedClause {
        id: u64,
        same_as_id: u64,
        clause: &'a [Lit],
    },
    TautologicalClause {
        id: u64,
        clause: &'a [Lit],
    },
    AtClause {
        id: u64,
        redundant: bool,
        clause: &'a [Lit],
        propagations: &'a [u64],
    },
    DeleteClause {
        id: u64,
        clause: &'a [Lit],
    },
    DeleteAtClause {
        id: u64,
        keep_as_redundant: bool,
        clause: &'a [Lit],
        propagations: &'a [u64],
    },
    DeleteRatClause {
        id: u64,
        keep_as_redundant: bool,
        clause: &'a [Lit],
        pivot: Lit,
        propagations: &'a ResolutionPropagations,
    },
    MakeIrredundant {
        id: u64,
        clause: &'a [Lit],
    },
    Model {
        assignment: &'a [Lit],
    },
    Assumptions {
        assumptions: &'a [Lit],
    },
    FailedAssumptions {
        failed_core: &'a [Lit],
        propagations: &'a [u64],
    },
}

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: Varuser_var: Option<CheckedUserVar>

AddClause

A clause of the input formula.

Fields of AddClause

id: u64clause: &'a [Lit]

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

id: u64same_as_id: u64clause: &'a [Lit]

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

id: u64clause: &'a [Lit]

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

id: u64redundant: boolclause: &'a [Lit]propagations: &'a [u64]

DeleteClause

Deletion of a redundant clause.

Fields of DeleteClause

id: u64clause: &'a [Lit]

DeleteAtClause

Deletion of a clause that is an asymmetric tautology w.r.t the remaining irredundant clauses.

Fields of DeleteAtClause

id: u64keep_as_redundant: boolclause: &'a [Lit]propagations: &'a [u64]

DeleteRatClause

Deletion of a resolution asymmetric tautology w.r.t the remaining irredundant caluses.

The pivot is always a hidden variable.

Fields of DeleteRatClause

id: u64keep_as_redundant: boolclause: &'a [Lit]pivot: Litpropagations: &'a ResolutionPropagations

MakeIrredundant

Make a redundant clause irredundant.

Fields of MakeIrredundant

id: u64clause: &'a [Lit]

Model

A (partial) assignment that satisfies all clauses and assumptions.

Fields of Model

assignment: &'a [Lit]

Assumptions

Change the active set of assumptions.

Fields of Assumptions

assumptions: &'a [Lit]

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

failed_core: &'a [Lit]propagations: &'a [u64]

Trait Implementations

impl<'a> Debug for CheckedProofStep<'a>

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

Formats the value using the given formatter.