Struct Cnf 

pub struct Cnf {
    pub num_vars: usize,
    pub clauses: Vec<Vec<SatLit>>,
}

A CNF formula over num_vars variables.

Fields

num_vars: usize

Number of variables; every Var used must be < num_vars.

clauses: Vec<Vec<SatLit>>

The clauses, each a disjunction of literals (the formula is their AND).

Implementations

impl Cnf

pub fn new(num_vars: usize) -> Self

An empty formula over num_vars variables.

pub fn add_clause(&mut self, lits: Vec<SatLit>)

Append one clause (a disjunction of literals).

Trait Implementations

impl Clone for Cnf

fn clone(&self) -> Cnf

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Cnf

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

Formats the value using the given formatter.

impl Default for Cnf

fn default() -> Cnf

Returns the “default value” for a type.