Struct Assignment 

pub struct Assignment { /* private fields */ }

Type representing an assignment of variables.

Implementations

impl Assignment

pub fn len(&self) -> usize

Gets the length of the assignment

pub fn is_empty(&self) -> bool

Checks whether the assignment is empty

pub fn var_value(&self, var: Var) -> TernaryVal

Get the value that the solution assigns to a variable. If the variable is not included in the solution, will return TernaryVal::DontCare.

pub fn lit_value(&self, lit: Lit) -> TernaryVal

Same as Assignment::var_value, but for literals.

pub fn replace_dont_care(&mut self, def: bool)

Replaces unassigned variables in the assignment with a default value

pub fn assign_var(&mut self, variable: Var, value: TernaryVal)

Assigns a variable in the assignment

pub fn assign_lit(&mut self, lit: Lit)

Assigns a literal to true

pub fn truncate(self, max_var: Var) -> Self

Truncates a solution to only include assignments up to a maximum variable

pub fn max_var(&self) -> Option<Var>

Get the maximum variable in the assignment

Panics

If the assignment contains more then u32::MAX variables.

pub fn from_solver_output_path<P: AsRef<Path>>(path: P) -> Result<Self>

Reads a solution from SAT solver output given the path

If it is unclear whether the SAT solver indicated satisfiability, use fio::parse_sat_solver_output instead.

Errors

• IO error: std::io::Error
• Invalid solver output: fio::SatSolverOutputError
• Invalid v line: InvalidVLine

pub fn from_vline(line: &str) -> Result<Self>

Creates an assignment from a SAT solver value line

Errors

InvalidVLine or parsing error, or nom::error::Error

pub fn extend_from_vline(&mut self, lines: &str) -> Result<()>

Parses an assignment from a value line returned by a solver

The following value line formats are supported:

• SAT Competition: v 1 -2 -3 4 0
• MaxSAT Evaluation: v 1001
• PB Competition: v x1 -x2 -x3 x4

Errors

Can return various parsing errors

Examples found in repository

examples/check-solution.rs (line 76)

fn main() -> anyhow::Result<()> {
    let args = Args::parse();
    let opb_opts = OpbOptions {
        first_var_idx: args.opb_first_var_idx,
        ..OpbOptions::default()
    };
    let (constrs, objs) = parse_instance(args.instance, args.file_format, opb_opts)?.decompose();

    let mut reader = if let Some(solution) = args.solution {
        fio::open_compressed_uncompressed_read(solution)?
    } else {
        Box::new(io::BufReader::new(io::stdin()))
    };

    let mut sol = Assignment::default();
    loop {
        let mut buf = String::new();
        let read = reader.read_line(&mut buf)?;
        if read == 0 {
            break;
        }
        if buf.starts_with('v') {
            sol.extend_from_vline(&buf)?;
        }
    }

    if let Some(constr) = constrs.unsat_constraint(&sol) {
        println!("unsatisfied constraint: {constr}");
        std::process::exit(1);
    }
    print!("objective values: ");
    for i in 0..objs.len() {
        if i < objs.len() - 1 {
            print!("{}, ", objs[i].evaluate(&sol))
        } else {
            print!("{}", objs[i].evaluate(&sol));
        }
    }
    println!();
    Ok(())
}

pub fn iter(&self) -> impl Iterator<Item = Lit> + '_

Gets an iterator over literals assigned to true

Trait Implementations

impl Clone for Assignment

fn clone(&self) -> Assignment

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Assignment

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

Formats the value using the given formatter.

impl Default for Assignment

fn default() -> Assignment

Returns the “default value” for a type.

impl<'de> Deserialize<'de> for Assignment

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Display for Assignment

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

Formats the value using the given formatter.

impl From<Vec<TernaryVal>> for Assignment

fn from(assignment: Vec<TernaryVal>) -> Self

Converts to this type from the input type.

impl FromIterator<Lit> for Assignment

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

Creates a value from an iterator.

impl FromIterator<TernaryVal> for Assignment

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

Creates a value from an iterator.

impl FromIterator<bool> for Assignment

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

Creates a value from an iterator.

impl Index<Var> for Assignment

type Output = TernaryVal

The returned type after indexing.

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

Performs the indexing (container[index]) operation.

impl IndexMut<Var> for Assignment

fn index_mut(&mut self, index: Var) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.

impl<'a> IntoIterator for &'a Assignment

Turns the assignment reference into an iterator over all true literals

type Item = Lit

The type of the elements being iterated over.

type IntoIter = FilterMap<Enumerate<Iter<'a, TernaryVal>>, fn((usize, &TernaryVal)) -> Option<Lit>>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl IntoIterator for Assignment

Turns the assignment into an iterator over all true literals

type Item = Lit

The type of the elements being iterated over.

type IntoIter = FilterMap<Enumerate<IntoIter<TernaryVal>>, fn((usize, TernaryVal)) -> Option<Lit>>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl PartialEq for Assignment

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

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 Assignment

impl StructuralPartialEq for Assignment