Struct Cnf 

pub struct Cnf { /* private fields */ }

A CNF formula under construction: a variable table (atoms canonicalised so a = b and b = a share a variable) plus the accumulating clause set. Clone so a prepared premise CNF can be reused per goal — the of-pair Tseitin work is done once, then each cell only adds its ¬goal unit (incremental solving, the IPASIR pattern).

Implementations

impl Cnf

pub fn new() -> Self

pub fn from_premises(premises: &[ProofExpr]) -> Option<Cnf>

Clausify a fixed premise set ONCE (the expensive of-pair Tseitin work), so many goals can be checked against it by cloning + adding ¬goal. None if any premise is not encodable. This is the incremental entry for solving a whole puzzle (16+ cells) without re-grounding or re-clausifying the shared premises every time.

pub fn num_vars(&self) -> usize

Number of CDCL variables allocated (atoms + Tseitin auxiliaries).

pub fn num_atoms(&self) -> usize

Number of distinct ATOM variables (the rest are Tseitin auxiliaries).

pub fn clauses(&self) -> &[Vec<Lit>]

The accumulated clauses.

pub fn atom_value(&self, e: &ProofExpr, model: &[bool]) -> Option<bool>

The Boolean value of atom e under a SAT model (a crate::cdcl::SolveResult::Sat assignment, indexed by variable), or None if e is not a recognised atom or was never encoded into this CNF. This decodes a model back to source atoms (e.g. signal@t), skipping the Tseitin auxiliaries that carry no source meaning.

pub fn encode(&mut self, e: &ProofExpr) -> Option<Lit>

Tseitin-encode e, returning a literal whose truth equals e’s, and emitting the defining clauses for any auxiliary variables. Returns None if e is not a quantifier-free propositional formula over recognisable atoms (so the caller can fall back to another engine rather than silently mis-encode).

pub fn assert(&mut self, e: &ProofExpr) -> Option<()>

Assert e as CNF, introducing auxiliary variables ONLY for genuinely non-clausal structure (a disjunct that is itself a conjunction — e.g. an of-pair disjunct). A top-level conjunction splits into separate clauses; a disjunction or implication flattens into ONE clause; a literal stays a literal. So a closure A∨B∨C∨D becomes a single clause with ZERO aux variables instead of a Tseitin spine. This structure-aware clausification (Plaisted & Greenbaum, 1986) is what keeps the CNF — and therefore the solve and the RUP replay — small. None if e is not encodable.

pub fn assert_neg(&mut self, e: &ProofExpr) -> Option<()>

Assert the NEGATION of e (used to refute the goal). A literal goal becomes a unit clause; a compound goal asserts its De-Morgan dual, clause by clause.

pub fn into_solver(self) -> Solver

Hand the accumulated CNF to a fresh CDCL solver.

pub fn into_solver_with_atoms(self) -> (Solver, HashMap<String, Var>)

Like into_solver but also hands back the atom→variable map (moved, not cloned). Callers that need to decode a SAT model can do so from this small map instead of cloning the entire clause database just to keep the table alive.

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 Default for Cnf

fn default() -> Cnf

Returns the “default value” for a type.