Struct SMTSolverBuilder 

pub struct SMTSolverBuilder {
    pub(crate) command: String,
    pub(crate) args: Vec<String>,
    pub(crate) opts: Vec<SMTSolverOption>,
    pub(crate) set_lia: bool,
}

Builder to create new SMTSolver instances

This builder can be used to create new SMT solver instances. Each new instance will be using a separate solver process.

Fields

command: String

args: Vec<String>

opts: Vec<SMTSolverOption>

set_lia: bool

Implementations

impl SMTSolverBuilder

pub fn new(cfg: &SMTSolverBuilderCfg) -> Result<Self, SMTSolverBuilderError>

Create a new SMTSolverBuilder with the given configuration

pub fn new_solver(&self) -> SMTSolver

Create a new SMTSolver instance

pub fn new_solver_with_replay<W>(&mut self, replay_file: W) -> SMTSolver

where W: Write + 'static + Send,

Create a new SMTSolver instance with a replay file recoding all interactions with the SMT solver

pub fn new_automatic_selection() -> Result<Self, SMTSolverBuilderError>

Builder to automatically select a supported SMT solver

This builder will try to start the CVC5 solver first, and if that fails, it will try to start the Z3 solver. If both fail, it will panic.

Trait Implementations

impl Clone for SMTSolverBuilder

fn clone(&self) -> SMTSolverBuilder

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SMTSolverBuilder

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for SMTSolverBuilder

fn default() -> Self

Create a new SMTSolverBuilder which will automatically try to select a supported SMT solver, if one is installed on the system.

impl PartialEq for SMTSolverBuilder

fn eq(&self, other: &SMTSolverBuilder) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl ProvidesSMTSolverBuilder for SMTSolverBuilder

fn get_solver_builder(&self) -> SMTSolverBuilder

Get the configured SMTSolverBuilder

impl StructuralPartialEq for SMTSolverBuilder