[−][src]Trait batsat::interface::SolverInterface

pub trait SolverInterface {
    fn num_vars(&self) -> u32;

    fn num_clauses(&self) -> u64;

    fn num_conflicts(&self) -> u64;

    fn num_propagations(&self) -> u64;

    fn num_decisions(&self) -> u64;

    fn num_restarts(&self) -> u64;

    fn is_ok(&self) -> bool;

    fn print_stats(&self);

    fn new_var(&mut self, upol: lbool, dvar: bool) -> Var;

    fn new_var_default(&mut self) -> Var;

    fn var_of_int(&mut self, i: u32) -> Var;

    fn add_clause_reuse(&mut self, clause: &mut Vec<Lit>) -> bool;

    fn simplify_th<Th: Theory>(&mut self, th: &mut Th) -> bool;

    fn solve_limited_th<Th: Theory>(
        &mut self, 
        th: &mut Th, 
        assumps: &[Lit]
    ) -> lbool;

    fn proved_at_lvl_0(&self) -> &[Lit];

    fn get_model(&self) -> &[lbool];

    fn value_var(&self, v: Var) -> lbool;

    fn value_lit(&self, lit: Lit) -> lbool;

    fn value_lvl_0(&self, lit: Lit) -> lbool;

    fn unsat_core(&self) -> &[Lit];

    fn unsat_core_contains_lit(&self, lit: Lit) -> bool;

    fn unsat_core_contains_var(&self, v: Var) -> bool;

    fn simplify(&mut self) -> bool { ... }

    fn solve_limited(&mut self, assumps: &[Lit]) -> lbool { ... }
}

Main interface for a solver: it makes it possible to add clauses, allocate variables, and check for satisfiability

Some functions take a parameter Th:Theory, for SMT solving.

Required methods

fn num_vars(&self) -> u32

fn num_clauses(&self) -> u64

fn num_conflicts(&self) -> u64

fn num_propagations(&self) -> u64

fn num_decisions(&self) -> u64

fn num_restarts(&self) -> u64

fn is_ok(&self) -> bool

fn print_stats(&self)

Print some current statistics to standard output.

fn new_var(&mut self, upol: lbool, dvar: bool) -> Var

Creates a new SAT variable in the solver. If 'decision' is cleared, variable will not be used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).

fn new_var_default(&mut self) -> Var

Create a new variable with the default polarity

fn var_of_int(&mut self, i: u32) -> Var

Get the i-th variable, possibly creating it if it doesn't already exist.

fn add_clause_reuse(&mut self, clause: &mut Vec<Lit>) -> bool

Add a clause to the solver. Returns false if the solver is in an UNSAT state.

fn simplify_th<Th: Theory>(&mut self, th: &mut Th) -> bool

Simplify using the given theory.

fn solve_limited_th<Th: Theory>(
    &mut self,
    th: &mut Th,
    assumps: &[Lit]
) -> lbool

Solve using the given theory.

  • th is the theory.

fn proved_at_lvl_0(&self) -> &[Lit]

Obtain the slice of literals that are proved at level 0.

These literals will keep this value from now on.

fn get_model(&self) -> &[lbool]

Query whole model

Precondition: last result was Sat (ie lbool::TRUE)

fn value_var(&self, v: Var) -> lbool

Query model for var

Precondition: last result was Sat (ie lbool::TRUE)

fn value_lit(&self, lit: Lit) -> lbool

Query model for lit

fn value_lvl_0(&self, lit: Lit) -> lbool

Value of this literal if it's assigned at level 0, or UNDEF otherwise

fn unsat_core(&self) -> &[Lit]

Return unsat core (as a subset of assumptions).

Precondition: last result was Unsat

fn unsat_core_contains_lit(&self, lit: Lit) -> bool

Does this literal occur in the unsat-core?

Precondition: last result was Unsat

fn unsat_core_contains_var(&self, v: Var) -> bool

Does this variable occur in the unsat-core?

Precondition: last result was Unsat

Loading content...

Provided methods

fn simplify(&mut self) -> bool

Simplify the clause database according to the current top-level assigment. Currently, the only thing done here is the removal of satisfied clauses, but more things can be put here.

fn solve_limited(&mut self, assumps: &[Lit]) -> lbool

Search for a model that respects a given set of assumptions (with resource constraints).

  • assumps is the list of assumptions to use (the literals that can be part of the unsat core)
Loading content...

Implementors

impl<Cb: Callbacks> SolverInterface for Solver<Cb>[src]

Loading content...