Struct Formula

pub struct Formula { /* private fields */ }

Represents a formula in propositional logic

Implementations

impl Formula

pub fn new() -> Self

Create a new empty formula

pub fn add_clause(&mut self, literals: Vec<i32>)

Add a clause to the formula

pub fn set_num_variables(&mut self, num_vars: usize)

Set the number of variables directly

pub fn reserve_clauses(&mut self, num_clauses: usize)

Pre-allocate space for the expected number of clauses

pub fn translate_to_implication_form(&mut self)

Translate to implication form

pub fn get_implication_form(&self) -> Option<&ImplicationFormula>

Get the stored implication form

pub fn encode_formula_to_triplets(&mut self)

Encode the formula into triplets

pub fn get_triplets(&self) -> Option<&TripletFormula>

Get the triplets representation

pub fn num_variables(&self) -> usize

Get the number of variables in the formula

pub fn num_clauses(&self) -> usize

Get the number of clauses in the formula

pub fn get_clauses(&self) -> &[Vec<i32>]

Get the clauses

Trait Implementations

impl Clone for Formula

fn clone(&self) -> Formula

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Formula

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

Formats the value using the given formatter.

impl Default for Formula

fn default() -> Formula

Returns the “default value” for a type.