Trait Satif

Source

pub trait Satif {
Show 13 methods    // Required methods
    fn new_var(&mut self) -> Var;
    fn num_var(&self) -> usize;
    fn add_clause(&mut self, clause: &[Lit]);
    fn solve(&mut self, assumps: &[Lit]) -> bool;
    fn sat_value(&self, lit: Lit) -> Option<bool>;

    // Provided methods
    fn new_var_to(&mut self, var: Var) { ... }
    fn max_var(&self) -> Var { ... }
    fn solve_with_constraint(
        &mut self,
        _assumps: &[Lit],
        _constraint: Vec<LitVec>,
    ) -> bool { ... }
    fn solve_with_limit(
        &mut self,
        _assumps: &[Lit],
        _constraint: Vec<LitVec>,
        _limit: Duration,
    ) -> Option<bool> { ... }
    fn unsat_has(&self, _lit: Lit) -> bool { ... }
    fn simplify(&mut self) -> Option<bool> { ... }
    fn set_frozen(&mut self, _var: Var, _frozen: bool) { ... }
    fn clauses(&self) -> Vec<LitVec> { ... }
}