[−][src]Struct varisat::solver::Solver
A boolean satisfiability solver.
Implementations
impl<'a> Solver<'a>
[src]
pub fn new() -> Solver<'a>
[src]
Create a new solver.
pub fn config(
&mut self,
config_update: &SolverConfigUpdate
) -> Result<(), Error>
[src]
&mut self,
config_update: &SolverConfigUpdate
) -> Result<(), Error>
Change the solver configuration.
pub fn add_formula(&mut self, formula: &CnfFormula)
[src]
Add a formula to the solver.
pub fn add_dimacs_cnf(&mut self, input: impl Read) -> Result<(), Error>
[src]
Reads and adds a formula in DIMACS CNF format.
Using this avoids creating a temporary CnfFormula
.
pub fn witness_var(&mut self, var: Var)
[src]
Sets the "witness" sampling mode for a variable.
pub fn sample_var(&mut self, var: Var)
[src]
Sets the "sample" sampling mode for a variable.
pub fn hide_var(&mut self, var: Var)
[src]
Hide a variable.
Turns a free variable into an existentially quantified variable. If the passed Var
is used
again after this call, it refers to a new variable not the previously hidden variable.
pub fn observe_internal_vars(&mut self) -> Vec<Var>
[src]
Observe solver internal variables.
This turns solver internal variables into witness variables. There is no guarantee that the newly visible variables correspond to previously hidden variables.
Returns a list of newly visible variables.
pub fn solve(&mut self) -> Result<bool, SolverError>
[src]
Check the satisfiability of the current formula.
pub fn assume(&mut self, assumptions: &[Lit])
[src]
Assume given literals for future calls to solve.
This replaces the current set of assumed literals.
pub fn model(&self) -> Option<Vec<Lit>>
[src]
Set of literals that satisfy the formula.
pub fn failed_core(&self) -> Option<&[Lit]>
[src]
Subset of the assumptions that made the formula unsatisfiable.
This is not guaranteed to be minimal and may just return all assumptions every time.
pub fn write_proof(&mut self, target: impl Write + 'a, format: ProofFormat)
[src]
Generate a proof of unsatisfiability during solving.
This needs to be called before any clauses are added.
pub fn close_proof(&mut self) -> Result<(), SolverError>
[src]
Stop generating a proof of unsatisfiability.
This also flushes internal buffers and closes the target file.
pub fn enable_self_checking(&mut self)
[src]
Generate and check a proof on the fly.
This needs to be called before any clauses are added.
pub fn add_proof_processor(&mut self, processor: &'a mut dyn ProofProcessor)
[src]
Generate a proof and process it using a ProofProcessor
.
This implicitly enables self checking.
This needs to be called before any clauses are added.
Trait Implementations
impl<'a> Default for Solver<'a>
[src]
impl<'a> Drop for Solver<'a>
[src]
impl<'a> ExtendFormula for Solver<'a>
[src]
fn add_clause(&mut self, clause: &[Lit])
[src]
Add a clause to the solver.
fn new_var(&mut self) -> Var
[src]
Add a new variable to the solver.
fn new_lit(&mut self) -> Lit
[src]
fn new_var_iter(&mut self, count: usize) -> NewVarIter<'_, Self, Var>ⓘNotable traits for NewVarIter<'a, F, V>
impl<'a, F, V> Iterator for NewVarIter<'a, F, V> where
F: ExtendFormula,
V: From<Var>, type Item = V;
[src]
Notable traits for NewVarIter<'a, F, V>
impl<'a, F, V> Iterator for NewVarIter<'a, F, V> where
F: ExtendFormula,
V: From<Var>, type Item = V;
fn new_lit_iter(&mut self, count: usize) -> NewVarIter<'_, Self, Lit>ⓘNotable traits for NewVarIter<'a, F, V>
impl<'a, F, V> Iterator for NewVarIter<'a, F, V> where
F: ExtendFormula,
V: From<Var>, type Item = V;
[src]
Notable traits for NewVarIter<'a, F, V>
impl<'a, F, V> Iterator for NewVarIter<'a, F, V> where
F: ExtendFormula,
V: From<Var>, type Item = V;
fn new_vars<Vars>(&mut self) -> Vars where
Vars: UniformTuple<Var>,
[src]
Vars: UniformTuple<Var>,
fn new_lits<Lits>(&mut self) -> Lits where
Lits: UniformTuple<Lit>,
[src]
Lits: UniformTuple<Lit>,
Auto Trait Implementations
impl<'a> !RefUnwindSafe for Solver<'a>
impl<'a> !Send for Solver<'a>
impl<'a> !Sync for Solver<'a>
impl<'a> Unpin for Solver<'a>
impl<'a> !UnwindSafe for Solver<'a>
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<Reference, Outer, OuterFieldType, Inner> HasPart<Nested<Outer, Inner>> for Reference where
Inner: Part,
Outer: Part<PartType = Field<OuterFieldType>>,
OuterFieldType: HasPart<Inner, RawTarget = OuterFieldType> + PartialRefTarget + ?Sized,
Reference: HasPart<Outer> + ?Sized,
[src]
Inner: Part,
Outer: Part<PartType = Field<OuterFieldType>>,
OuterFieldType: HasPart<Inner, RawTarget = OuterFieldType> + PartialRefTarget + ?Sized,
Reference: HasPart<Outer> + ?Sized,
unsafe fn part_ptr(
ptr: *const <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::Ptr
[src]
ptr: *const <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::Ptr
unsafe fn part_ptr_mut(
ptr: *mut <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::PtrMut
[src]
ptr: *mut <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::PtrMut
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>,
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<V, T> VZip<V> for T where
V: MultiLane<T>,
V: MultiLane<T>,