Enum dimacs::Instance

pub enum Instance {
    Cnf {
        num_vars: u64,
        clauses: Box<[Clause]>,
    },
    Sat {
        num_vars: u64,
        extensions: Extensions,
        formula: Formula,
    },
}

Represents a SAT instance for .cnf or .sat files.

Variants

Cnf

A .cnf SAT instance with clauses.

Fields of Cnf

num_vars: u64	The number of unique variables used within this .cnf SAT instance.
clauses: Box<[Clause]>	The clauses within this .cnf SAT instance formula.

Sat

A .sat SAT instance with an underlying formula and extensions.

Fields of Sat

num_vars: u64	The number of unique variables used within this .sat SAT instance.
extensions: Extensions	Extensions (e.g. XOR or EQ) being used in this SAT instance.
formula: Formula	The underlying formula of this SAT instance.

Methods

impl Instance

fn cnf(num_vars: u64, clauses: Vec<Clause>) -> Instance

Creates a new SAT instance for .cnf files with given clauses.

fn sat(num_vars: u64, extensions: Extensions, formula: Formula) -> Instance

Creates a new SAT instance for .sat files with given extensions and an underlying formula.

Trait Implementations

impl Debug for Instance

fn fmt(&self, __arg_0: &mut Formatter) -> Result

Formats the value using the given formatter.

impl Clone for Instance

fn clone(&self) -> Instance

Returns a copy of the value.

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

Performs copy-assignment from source.

impl PartialEq for Instance

fn eq(&self, __arg_0: &Instance) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, __arg_0: &Instance) -> bool

This method tests for !=.

impl Eq for Instance