Struct SMTSolverBuilderCfg 

pub struct SMTSolverBuilderCfg {
    pub(crate) command: String,
    pub(crate) args: Vec<String>,
    pub(crate) opts: Vec<SMTSolverOption>,
    pub(crate) set_lia: bool,
    pub(crate) check_version: Option<fn((i32, i32, i32))>,
}

Configuration for a SMTSolverBuilder

Fields

command: String

Command to start the SMT solver

args: Vec<String>

Arguments to pass to the SMT solver command

opts: Vec<SMTSolverOption>

Options to configure in the SMT solver

set_lia: bool

Sets the logic explicitly to LIA

check_version: Option<fn((i32, i32, i32))>

Function to check version compatibility of the SMT solver

Implementations

impl SMTSolverBuilderCfg

pub fn new( command: String, args: Vec<String>, opts: Vec<SMTSolverOption>, set_lia: bool, ) -> Self

Create a new SMT solver builder configuration

This function takes the command to start the SMT solver, the arguments to pass to the SMT solver, and the options to pass to the SMT solver.

Additionally, it takes a boolean value to set the logic explicitly to linear integer arithmetic (LIA).

Note that the SMT solver must be started in interactive REPL mode and accept input in the SMT-LIB2 format.

pub fn new_z3() -> Self

Get the default configuration for the Z3 SMT solver

pub fn new_cvc5() -> Self

Get the default configuration for the CVC5 SMT solver

Trait Implementations

impl Clone for SMTSolverBuilderCfg

fn clone(&self) -> SMTSolverBuilderCfg

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SMTSolverBuilderCfg

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for SMTSolverBuilderCfg

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for SMTSolverBuilderCfg

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

Ignore the concrete function behind check version

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 ProvidesSMTSolverBuilderCfg for SMTSolverBuilderCfg

fn get_smt_solver_builder_cfg(&self) -> &SMTSolverBuilderCfg

Get the SMTSolverBuilderCfg