Struct Parser

pub struct Parser {
    pub redundancy_property: RedundancyProperty,
    pub maxvar: Variable,
    pub clause_pivot: Vector<Literal>,
    pub proof_start: Clause,
    pub proof: Vector<ProofStep>,
    pub max_proof_steps: Option<usize>,
    pub verbose: bool,
    pub clause_db: ClauseDatabase,
    pub witness_db: WitnessDatabase,
}

CNF and DRAT/DPR parser.

Fields

redundancy_property: RedundancyProperty

The redundancy property identifying the proof format.

maxvar: Variable

The highest variable parsed so far

clause_pivot: Vector<Literal>

For RAT, the pivot (first literal) for each clause

It is necessary to store this because the clauses will be sorted (and watches will be shuffled).

proof_start: Clause

The first clause that is part of the proof (and not the input formula)

proof: Vector<ProofStep>

The proof steps

max_proof_steps: Option<usize>

How many proof steps we want to parse

verbose: bool

Print diagnostics and timing information

clause_db: ClauseDatabase

Clause store

witness_db: WitnessDatabase

Witness store

Implementations

impl Parser

pub fn is_pr(&self) -> bool

Returns true if we are parsing a (D)PR proof.

Trait Implementations

impl Debug for Parser

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

Formats the value using the given formatter.

impl Default for Parser

fn default() -> Parser

Create a new parser.

Note: this allocates the static clause and witness databases, so this should only be called once.

impl HeapSpace for Parser

fn heap_space(&self) -> usize

The number of bytes allocated on the heap that this owns.

impl PartialEq for Parser

fn eq(&self, other: &Parser) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for Parser