Struct Cnf

pub struct Cnf { /* private fields */ }

Simple type representing a CNF formula. Other than Instance<VM>, this type only supports clauses and does have an internal variable manager.

Implementations

impl Cnf

pub fn new() -> Cnf

Creates a new Cnf

Examples found in repository

examples/profiling.rs (line 75)

fn build_full_ub<PBE: BoundUpper + FromIterator<(Lit, usize)>>(lits: &[(Lit, usize)]) {
    let mut enc = PBE::from_iter(lits.iter().copied());
    let max_var = lits
        .iter()
        .fold(Var::new(0), |mv, (lit, _)| std::cmp::max(lit.var(), mv));
    let mut var_manager = BasicVarManager::default();
    var_manager.increase_next_free(max_var + 1);
    let mut collector = Cnf::new();
    enc.encode_ub(.., &mut collector, &mut var_manager).unwrap();
}

pub fn with_capacity(capacity: usize) -> Cnf

Creates a new Cnf with a given capacity of clauses

pub fn try_reserve(&mut self, additional: usize) -> Result<(), TryReserveError>

Tries to reserve memory for at least additional new clauses

Errors

If the capacity overflows, or the allocator reports a failure, then an error is returned.

pub fn shrink_to_fit(&mut self)

Shrinks the allocated memory of the Cnf to fit the number of clauses

pub fn capacity(&self) -> usize

Gets the capacity of the Cnf

pub fn is_empty(&self) -> bool

Checks if the CNF is empty

pub fn len(&self) -> usize

Returns the number of clauses in the instance

pub fn clear(&mut self)

Clears the CNF formula

pub fn add_nary(&mut self, lits: &[Lit])

Adds a clause from a slice of literals

pub fn add_lit_impl_lit(&mut self, a: Lit, b: Lit)

See atomics::lit_impl_lit

pub fn add_lit_impl_clause(&mut self, a: Lit, b: &[Lit])

See atomics::lit_impl_clause

pub fn add_lit_impl_cube(&mut self, a: Lit, b: &[Lit])

See atomics::lit_impl_cube

pub fn add_cube_impl_lit(&mut self, a: &[Lit], b: Lit)

See atomics::cube_impl_lit

pub fn add_clause_impl_lit(&mut self, a: &[Lit], b: Lit)

See atomics::clause_impl_lit

pub fn add_cube_impl_clause(&mut self, a: &[Lit], b: &[Lit])

See atomics::cube_impl_clause

pub fn add_clause_impl_clause(&mut self, a: &[Lit], b: &[Lit])

See atomics::clause_impl_clause

pub fn add_clause_impl_cube(&mut self, a: &[Lit], b: &[Lit])

See atomics::clause_impl_cube

pub fn add_cube_impl_cube(&mut self, a: &[Lit], b: &[Lit])

See atomics::cube_impl_cube

pub fn join(self, other: Cnf) -> Cnf

Joins the current CNF with another one. Like Cnf::extend but consumes the object and returns a new object.

pub fn iter(&self) -> Iter<'_, Clause>

Returns an iterator over references to the clauses

pub fn iter_mut(&mut self) -> IterMut<'_, Clause>

Returns an iterator over mutable references to the clauses

pub fn normalize(self) -> Self

Normalizes the CNF. This includes normalizing and sorting the clauses, removing duplicates and tautologies. Comparing two normalized CNFs is equal to comparing sets of sets of literals.

pub fn sanitize(self) -> Self

Sanitizes the CNF by removing tautologies, removing redundant literals, etc.

pub fn shuffle(self) -> Self

Available on crate feature rand only.

Randomly shuffles the order of clauses in the CNF

pub fn add_clause(&mut self, clause: Clause)

Adds a clause to the CNF

pub fn add_unit(&mut self, unit: Lit)

Adds a unit clause to the CNF

pub fn add_binary(&mut self, lit1: Lit, lit2: Lit)

Adds a binary clause to the CNF

pub fn add_ternary(&mut self, lit1: Lit, lit2: Lit, lit3: Lit)

Adds a ternary clause to the CNF

pub fn write_dimacs_path<P: AsRef<Path>>( &self, path: P, n_vars: u32, ) -> Result<(), Error>

Writes the CNF to a DIMACS CNF file at a path

Errors

If the file could not be written to, returns io::Error.

pub fn write_dimacs<W: Write>( &self, writer: &mut W, n_vars: u32, ) -> Result<(), Error>

Writes the CNF to DIMACS CNF

Performance

For performance, consider using a std::io::BufWriter instance.

Errors

If writing fails, returns io::Error.

pub fn evaluate(&self, assign: &Assignment) -> TernaryVal

Checks the value of the CNF under a given assignment

pub fn is_sat(&self, assign: &Assignment) -> bool

👎Deprecated since 0.6.0: use evaluate instead and check against TernaryVal::True

Checks whether the CNF is satisfied by the given assignment

Trait Implementations

impl Clone for Cnf

fn clone(&self) -> Cnf

Returns a copy of the value.

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

Performs copy-assignment from source.

impl CollectClauses for Cnf

fn n_clauses(&self) -> usize

Gets the number of clauses in the collection

fn extend_clauses<T>(&mut self, cl_iter: T) -> Result<(), OutOfMemory>

where T: IntoIterator<Item = Clause>,

Extends the clause collector with an iterator of clauses

fn add_clause(&mut self, cl: Clause) -> Result<(), OutOfMemory>

Adds one clause to the collector

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.

impl<'de> Deserialize<'de> for Cnf

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Extend<Clause> for Cnf

fn extend<Iter: IntoIterator<Item = Clause>>(&mut self, iter: Iter)

Extends a collection with the contents of an iterator.

fn extend_one(&mut self, item: A)

🔬This is a nightly-only experimental API. (extend_one)

Extends a collection with exactly one element.

fn extend_reserve(&mut self, additional: usize)

🔬This is a nightly-only experimental API. (extend_one)

Reserves capacity in a collection for the given number of additional elements.

impl<VM: ManageVars + Default> From<Cnf> for Instance<VM>

fn from(value: Cnf) -> Self

Converts to this type from the input type.

impl FromIterator<Clause> for Cnf

fn from_iter<T: IntoIterator<Item = Clause>>(iter: T) -> Self

Creates a value from an iterator.

impl FromIterator<CnfLine> for Cnf

fn from_iter<T: IntoIterator<Item = CnfLine>>(iter: T) -> Self

Creates a value from an iterator.

impl Index<usize> for Cnf

type Output = Clause

The returned type after indexing.

fn index(&self, index: usize) -> &Self::Output

Performs the indexing (container[index]) operation.

impl<'slf> IntoIterator for &'slf Cnf

type Item = &'slf Clause

The type of the elements being iterated over.

type IntoIter = Iter<'slf, Clause>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl<'slf> IntoIterator for &'slf mut Cnf

type Item = &'slf mut Clause

The type of the elements being iterated over.

type IntoIter = IterMut<'slf, Clause>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl IntoIterator for Cnf

type Item = Clause

The type of the elements being iterated over.

type IntoIter = IntoIter<Clause>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl PartialEq for Cnf

fn eq(&self, other: &Cnf) -> 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 Serialize for Cnf

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for Cnf

impl StructuralPartialEq for Cnf