Trait splr::types::Instantiate

pub trait Instantiate {
    fn instantiate(conf: &Config, cnf: &CNFDescription) -> Self;

    fn handle(&mut self, _e: SolverEvent) { ... }
}

API for object instantiation based on Configuration and CNFDescription. This is implemented by all the Splr modules except Configuration and CNFDescription.

Example

use crate::{splr::config::Config, splr::types::*};
use splr::{cdb::ClauseDB, solver::Solver};
let _ = ClauseDB::instantiate(&Config::default(), &CNFDescription::default());
let _ = Solver::instantiate(&Config::default(), &CNFDescription::default());

Required methods

fn instantiate(conf: &Config, cnf: &CNFDescription) -> Self

make and return an object from Config and CNFDescription.

Loading content...

Provided methods

fn handle(&mut self, _e: SolverEvent)

update by a solver event.

Loading content...

Implementors

impl Instantiate for AssignStack

fn instantiate(config: &Config, cnf: &CNFDescription) -> AssignStack

fn handle(&mut self, e: SolverEvent)

impl Instantiate for ClauseDB

fn instantiate(config: &Config, cnf: &CNFDescription) -> ClauseDB

fn handle(&mut self, e: SolverEvent)

impl Instantiate for Eliminator

fn instantiate(config: &Config, cnf: &CNFDescription) -> Eliminator

fn handle(&mut self, e: SolverEvent)

impl Instantiate for Restarter

fn instantiate(config: &Config, cnf: &CNFDescription) -> Self

fn handle(&mut self, e: SolverEvent)

impl Instantiate for Solver

fn instantiate(config: &Config, cnf: &CNFDescription) -> Solver

use crate::{splr::config::Config, splr::types::*};
use splr::solver::Solver;
let s = Solver::instantiate(&Config::default(), &CNFDescription::default());

impl Instantiate for State

fn instantiate(config: &Config, cnf: &CNFDescription) -> State

fn handle(&mut self, e: SolverEvent)

Loading content...