Struct Kissat

pub struct Kissat { /* private fields */ }

A SolverAdaptor for interacting with the Kissat SAT solver.

Implementations

impl Kissat

pub fn new() -> Kissat

Trait Implementations

impl Default for Kissat

fn default() -> Kissat

Returns the “default value” for a type.

impl SolverAdaptor for Kissat

fn solve( &mut self, callback: Box<dyn Fn(HashMap<Name, Literal>) -> bool + Send>, _: Internal, ) -> Result<SolveSuccess, SolverError>

Runs the solver on the given model.

fn solve_mut( &mut self, callback: Box<dyn Fn(HashMap<Name, Literal>, Box<dyn ModelModifier>) -> bool + Send>, _: Internal, ) -> Result<SolveSuccess, SolverError>

Runs the solver on the given model, allowing modification of the model through a ModelModifier.

fn load_model(&mut self, model: Model, _: Internal) -> Result<(), SolverError>

fn get_family(&self) -> SolverFamily

Get the solver family that this solver adaptor belongs to

fn init_solver(&mut self, _: Internal)

fn get_name(&self) -> Option<String>

Gets the name of the solver adaptor for pretty printing.

fn add_adaptor_info_to_stats(&self, stats: SolverStats) -> SolverStats

Adds the solver adaptor name and family (if they exist) to the given stats object.