Struct rsmt2::SolverConf

pub struct SolverConf { /* fields omitted */ }

Configuration and solver specific info.

Methods

impl SolverConf

fn z3() -> Self

Creates a new z3-like solver configuration.

fn cvc4() -> Self

Creates a new CVC4-like solver configuration.

fn style(&self) -> &SolverStyle

Solver style.

fn get_cmd(&self) -> &str

Solver command.

fn get_options(&self) -> &[&'static str]

Options of the configuration.

fn get_parse_success(&self) -> bool

Indicates if parse success is active.

fn get_check_sat_assuming(&self) -> &ConfItem

Keyword for check-sat with assumptions.

fn option(self, o: &'static str) -> Self

Adds an option to the configuration.

fn cmd(self, cmd: String) -> Self

Sets the command for the solver.

fn print_success(self) -> Self

Activates parse sucess.

fn unsat_cores(self) -> Self

Activates unsat-core production.

Trait Implementations

impl Debug for SolverConf

fn fmt(&self, __arg_0: &mut Formatter) -> Result

Formats the value using the given formatter.

impl Clone for SolverConf

fn clone(&self) -> SolverConf

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.