Enum splr::solver::Certificate

pub enum Certificate {
    SAT(Vec<i32>),
    UNSAT,
}

Normal results returned by Solver.

Variants

SAT(Vec<i32>)

It is satisfiable; vec is such an assignment sorted by var order.

UNSAT

It is unsatisfiable.

Trait Implementations

impl Debug for Certificate

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

Formats the value using the given formatter.

impl PartialEq for Certificate

fn eq(&self, other: &Certificate) -> bool

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

fn ne(&self, other: &Rhs) -> bool

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<V: AsRef<[i32]>> TryFrom<Vec<V>> for Certificate

Example

 use crate::splr::*;

 let v: Vec<Vec<i32>> = vec![];
 assert!(matches!(
     Certificate::try_from(v),
     Ok(Certificate::SAT(_))
 ));
 assert!(matches!(
     Certificate::try_from(vec![vec![0_i32]]),
     Err(SolverError::InvalidLiteral)
 ));

 // `Solver` has another interface.
 assert!(matches!(
     Solver::try_from((Config::default(), vec![vec![0_i32]].as_ref())),
     Err(Err(SolverError::InvalidLiteral))
 ));

type Error = SolverError

The type returned in the event of a conversion error.

fn try_from(vec: Vec<V>) -> SolverResult

Performs the conversion.

impl Eq for Certificate

impl StructuralPartialEq for Certificate