Struct Solver

pub struct Solver { /* private fields */ }

Solver object representing an instance of the boolean satisfiability problem.

Implementations

impl Solver

pub fn new() -> Self

Create a new SAT solver instance.

pub fn new_lit(&mut self) -> Bool

Create a fresh boolean variable.

pub fn add_clause<I: IntoIterator<Item = Bool>>(&mut self, lits: I)

Add a clause to the SAT instance (assert the disjunction of the given literals).

pub fn solve<'a>(&'a mut self) -> Result<Model<'a>, ()>

Solve the SAT instance, returning a solution (Model) if the instance is satisfiable, or returning an Err(()) if the problem is unsatisfiable.

pub fn solve_under_assumptions<'a, I: IntoIterator<Item = Bool>>( &'a mut self, lits: I, ) -> Result<Model<'a>, ()>

Solve the SAT instance under given assumptions, returning a solution (Model) if the instance is satisfiable, or returning an Err(()) if the problem is unsatisfiable.

The conjunction of the given literals are temporarily added to the SAT instance, so the result is the same as if each literal was added as a clause, but the solver object can be re-used afterwards and does then not contain these assumptions. This interface can be used to build SAT instances incrementally.

pub fn and_literal<I: IntoIterator<Item = Bool>>(&mut self, xs: I) -> Bool

Return a literal representing the conjunction of the given booleans.

pub fn or_literal<I: IntoIterator<Item = Bool>>(&mut self, xs: I) -> Bool

Return a literal representing the disjunctino of the given booleans.

pub fn assert_at_most_one(&mut self, xs: impl Iterator<Item = Bool>)

Assert that at most one of the given booleans can be true.

pub fn assert_exactly_one<I: IntoIterator<Item = Bool>>(&mut self, xs: I)

Assert that exactly one of the given booleans is set to true.

pub fn implies(&mut self, a: Bool, b: Bool) -> Bool

Returns a literal representing the truth value of the implication a -> b.

pub fn equiv(&mut self, a: Bool, b: Bool) -> Bool

Returns a literal representing whether the two given booleans have the same value.

pub fn assert_parity<I: IntoIterator<Item = Bool>>(&mut self, xs: I, x: bool)

Assert that the odd parity bit of the given list of booleans has the given value.

pub fn assert_parity_or<I: IntoIterator<Item = Bool>, J: IntoIterator<Item = Bool>>( &mut self, prefix: I, xs: J, c: bool, )

Assert that the odd parity bit of the given list of booleans has the given value, except if any of the values in prefix are true.

pub fn xor_literal<I: IntoIterator<Item = Bool>>(&mut self, xs: I) -> Bool

Returns a Bool which represents the odd parity bit for the given sequence of Bool values.

pub fn equal<T: ModelEq>(&mut self, a: &T, b: &T)

Assert the equality of the given objects.

pub fn not_equal<T: ModelEq>(&mut self, a: &T, b: &T)

Assert the non-equality of the given objects.

pub fn greater_than<T: ModelOrd>(&mut self, a: &T, b: &T)

Assert a > b.

pub fn greater_than_equal<T: ModelOrd>(&mut self, a: &T, b: &T)

Assert a >= b.

pub fn less_than<T: ModelOrd>(&mut self, a: &T, b: &T)

Assert a < b.

pub fn less_than_equal<T: ModelOrd>(&mut self, a: &T, b: &T)

Assert a <= b.

pub fn greater_than_or<T: ModelOrd, I: IntoIterator<Item = Bool>>( &mut self, prefix: I, a: &T, b: &T, )

Assert a > b unless any of the booleans in the given prefix are true.

pub fn greater_than_equal_or<T: ModelOrd, I: IntoIterator<Item = Bool>>( &mut self, prefix: I, a: &T, b: &T, )

Assert a >= b unless any of the booleans in the given prefix are true.

pub fn less_than_or<T: ModelOrd, I: IntoIterator<Item = Bool>>( &mut self, prefix: I, a: &T, b: &T, )

Assert a < b unless any of the booleans in the given prefix are true.

pub fn less_than_equal_or<T: ModelOrd, I: IntoIterator<Item = Bool>>( &mut self, prefix: I, a: &T, b: &T, )

Assert a <= b unless any of the booleans in the given prefix are true.

pub fn num_assigns(&self) -> isize

Return the number of assignments to variables made in the solver instance.

pub fn num_clauses(&self) -> isize

Return the number of clauses in the solver instance.

pub fn num_learnts(&self) -> isize

Return the number of learnt clauses in the solver instance.

pub fn num_vars(&self) -> isize

Return the number of variables in the solver instance.

pub fn num_free_vars(&self) -> isize

Return the number of free variables in the solver instance.

pub fn solver_name(&self) -> &'static str

Name and version of SAT solver.

Trait Implementations

impl Debug for Solver

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

Formats the value using the given formatter.

impl Drop for Solver

fn drop(&mut self)

Executes the destructor for this type.