Struct Config 

pub struct Config {
    pub logic: Option<Identifier<'static>>,
    pub produce_models: bool,
}

Configuration for SMT solvers.

This is a simple struct holding some parameters used to instantiate SMT solvers. Config instances are usually constructed from the default one by changing the desired parameters and then passed to Solver::new() and related constructors. Fields are public and can be set arbitrarily but a builder method for each parameter is also provided, for convenience.

Example:

let config =
    Config::default()
        .logic("LIA")
        .produce_models(true);

let solver = Solver::new(&config)?;
// ...

Fields

logic: Option<Identifier<'static>>

The name of the logic to instantiate the solver for.

A None value is the default, which means a logic is not selected and the solver will accept symbols from all the known theories, as if “ALL” had been specified (such as with the (set-logic ALL) command in SMT-LIBv2).

Note that the "ALL" string itself has no special meaning, but is looked up as any other logic name (and probably not found).

produce_models: bool

Whether the solver has to activate the machinery for generating models for satisfiable instances.

Implementations

impl Config

pub fn new() -> Config

Create a new Config object with default values.

pub fn logic<'a>(self, logic: impl Into<Identifier<'a>>) -> Config

Set the logic fied.

pub fn produce_models(self, produce_models: bool) -> Config

Set the produce_models fied.

Trait Implementations

impl Clone for Config

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Config

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

Formats the value using the given formatter.

impl Default for Config

fn default() -> Self

Returns the “default value” for a type.