[−][src]Struct minisat::Solver
Solver object representing an instance of the boolean satisfiability problem.
Methods
impl Solver
[src]
pub fn new() -> Self
[src]
Create a new SAT solver instance.
pub fn new_lit(&mut self) -> Bool
[src]
Create a fresh boolean variable.
pub fn add_clause<I: IntoIterator<Item = Bool>>(&mut self, lits: I)
[src]
Add a clause to the SAT instance (assert the disjunction of the given literals).
pub fn solve<'a>(&'a mut self) -> Result<Model<'a>, ()>
[src]
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>, ()>
[src]
&'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
[src]
Return a literal representing the conjunction of the given booleans.
pub fn or_literal<I: IntoIterator<Item = Bool>>(&mut self, xs: I) -> Bool
[src]
Return a literal representing the disjunctino of the given booleans.
pub fn assert_at_most_one(&mut self, xs: impl Iterator<Item = Bool>)
[src]
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)
[src]
Assert that exactly one of the given booleans is set to true.
pub fn implies(&mut self, a: Bool, b: Bool) -> Bool
[src]
Returns a literal representing the truth value of the implication a -> b
.
pub fn equiv(&mut self, a: Bool, b: Bool) -> Bool
[src]
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)
[src]
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
)
[src]
&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
[src]
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)
[src]
Assert the equality of the given objects.
pub fn not_equal<T: ModelEq>(&mut self, a: &T, b: &T)
[src]
Assert the non-equality of the given objects.
pub fn greater_than<T: ModelOrd>(&mut self, a: &T, b: &T)
[src]
Assert a > b
.
pub fn greater_than_equal<T: ModelOrd>(&mut self, a: &T, b: &T)
[src]
Assert a >= b
.
pub fn less_than<T: ModelOrd>(&mut self, a: &T, b: &T)
[src]
Assert a < b
.
pub fn less_than_equal<T: ModelOrd>(&mut self, a: &T, b: &T)
[src]
Assert a <= b
.
pub fn greater_than_or<T: ModelOrd, I: IntoIterator<Item = Bool>>(
&mut self,
prefix: I,
a: &T,
b: &T
)
[src]
&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
)
[src]
&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
)
[src]
&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
)
[src]
&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
[src]
Return the number of assignments to variables made in the solver instance.
pub fn num_clauses(&self) -> isize
[src]
Return the number of clauses in the solver instance.
pub fn num_learnts(&self) -> isize
[src]
Return the number of learnt clauses in the solver instance.
pub fn num_vars(&self) -> isize
[src]
Return the number of variables in the solver instance.
pub fn num_free_vars(&self) -> isize
[src]
Return the number of free variables in the solver instance.
pub fn solver_name(&self) -> &'static str
[src]
Name and version of SAT solver.
Trait Implementations
Auto Trait Implementations
impl !Send for Solver
impl !Sync for Solver
impl Unpin for Solver
impl UnwindSafe for Solver
impl RefUnwindSafe for Solver
Blanket Implementations
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> From<T> for T
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,