[−][src]Struct cadical::Solver
The CaDiCaL incremental SAT solver. The literals are unwrapped positive and negative integers, exactly as in the DIMACS format. The common IPASIR operations are presented in a safe Rust interface.
Examples
let mut sat: cadical::Solver = Default::default(); sat.add_clause([1, 2].iter().copied()); sat.add_clause([-1, 2].iter().copied()); assert_eq!(sat.solve(), Some(true)); assert_eq!(sat.value(2), Some(true));
Implementations
impl<C: Callbacks> Solver<C>
[src]
pub fn new() -> Self
[src]
Constructs a new solver instance.
pub fn with_config(config: &str) -> Result<Self, Error>
[src]
Constructs a new solver with one of the following pre-defined configurations of advanced internal options:
default
: set default advanced internal optionsplain
: disable all internal preprocessing optionssat
: set internal options to target satisfiable instancesunsat
: set internal options to target unsatisfiable instances
pub fn signature(&self) -> &str
[src]
Returns the name and version of the CaDiCaL library.
pub fn add_clause<I>(&mut self, clause: I) where
I: Iterator<Item = i32>,
[src]
I: Iterator<Item = i32>,
Adds the given clause to the solver. Negated literals are negative
integers, positive literals are positive ones. All literals must be
non-zero and different from i32::MIN
.
pub fn solve(&mut self) -> Option<bool>
[src]
Solves the formula defined by the added clauses. If the formula is
satisfiable, then Some(true)
is returned. If the formula is
unsatisfiable, then Some(false)
is returned. If the solver runs out
of resources or was terminated, then None
is returned.
pub fn solve_with<I>(&mut self, assumptions: I) -> Option<bool> where
I: Iterator<Item = i32>,
[src]
I: Iterator<Item = i32>,
Solves the formula defined by the set of clauses under the given assumptions.
pub fn status(&self) -> Option<bool>
[src]
Returns the status of the solver as returned by the last call to
solve
or solve_with
. The state becomes None
if a new clause
is added.
pub fn value(&self, lit: i32) -> Option<bool>
[src]
Returns the value of the given literal in the last solution. The
state of the solver must be Some(true)
. The returned value is
None
if the formula is satisfied regardless of the value of the
literal.
pub fn failed(&self, lit: i32) -> bool
[src]
Checks if the given assumed literal (passed to solve_with
) was used
in the proof of the unsatisfiability of the formula. The state of the
solver must be Some(false)
.
pub fn max_variable(&self) -> i32
[src]
Returns the maximum variable index in the problem as maintained by the solver.
Examples
let mut sat: cadical::Solver = Default::default(); sat.add_clause([1, 3].iter().copied()); assert_eq!(sat.max_variable(), 3); assert_eq!(sat.num_variables(), 2); assert_eq!(sat.num_clauses(), 1);
pub fn num_variables(&self) -> i32
[src]
Returns the number of active variables in the problem. Variables become active if a clause is added with it. They become inactive, if they are eliminated or become fixed at the root level.
pub fn num_clauses(&self) -> usize
[src]
Returns the number of active irredundant clauses. Clauses become inactive if they are satisfied, subsumed or eliminated.
pub fn set_callbacks(&mut self, cbs: Option<C>)
[src]
Sets the callbacks to be called while the solver is running.
Examples
let mut sat: cadical::Solver = Default::default(); sat.add_clause([1, 2].iter().copied()); sat.set_callbacks(Some(cadical::Timeout::new(0.0))); assert_eq!(sat.solve(), None);
pub fn get_callbacks(&mut self) -> Option<&mut C>
[src]
Returns a mutable reference to the callbacks.
pub fn write_dimacs(&mut self, path: &Path) -> Result<(), Error>
[src]
Writes the problem in DIMACS format to the given file.
pub fn read_dimacs(&mut self, path: &Path) -> Result<i32, Error>
[src]
Reads a problem in DIMACS format from the given file. You must call this function during configuration time, before adding any clauses. Returns the number of variables as reported by the loader.
Trait Implementations
impl<C: Callbacks> Default for Solver<C>
[src]
impl<C: Callbacks> Drop for Solver<C>
[src]
impl<C: Callbacks + Send> Send for Solver<C>
[src]
CaDiCaL does not use thread local variables, so it is possible to
move it between threads. However it cannot be used queried concurrently
(for example getting the value from multiple threads at once), so we
do not implement Sync
.
Auto Trait Implementations
impl<C> RefUnwindSafe for Solver<C> where
C: RefUnwindSafe,
C: RefUnwindSafe,
impl<C = Timeout> !Sync for Solver<C>
impl<C> Unpin for Solver<C>
impl<C> UnwindSafe for Solver<C> where
C: UnwindSafe,
C: UnwindSafe,
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
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> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
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>,