Trait satoxid::Backend [−][src]
pub trait Backend {
fn add_clause<I>(&mut self, lits: I)
where
I: Iterator<Item = i32>;
fn add_debug_info<D: Debug>(&mut self, _debug: D) { ... }
fn append_debug_info<D: Debug>(&mut self, _debug: D) { ... }
}Expand description
Backend abstraction trait.
Required methods
fn add_clause<I>(&mut self, lits: I) where
I: Iterator<Item = i32>, [src]
fn add_clause<I>(&mut self, lits: I) where
I: Iterator<Item = i32>, [src]Add raw clause as integer SAT variable.
These are usually determined using VarMap.
Provided methods
fn add_debug_info<D: Debug>(&mut self, _debug: D)[src]
fn add_debug_info<D: Debug>(&mut self, _debug: D)[src]This function is used every time a constraint is encoded,
when the debug flag of Encoder is enabled.
fn append_debug_info<D: Debug>(&mut self, _debug: D)[src]
fn append_debug_info<D: Debug>(&mut self, _debug: D)[src]Implementations on Foreign Types
impl Backend for Solver[src]
impl Backend for Solver[src]fn add_clause<I>(&mut self, lits: I) where
I: Iterator<Item = i32>, [src]
I: Iterator<Item = i32>,
fn add_debug_info<D: Debug>(&mut self, debug: D)[src]
fn append_debug_info<D: Debug>(&mut self, debug: D)[src]
Implementors
impl Backend for DimacsWriter[src]
impl Backend for DimacsWriter[src]fn add_clause<I>(&mut self, lits: I) where
I: Iterator<Item = i32>, [src]
I: Iterator<Item = i32>,