Struct rsmt2::conf::SmtConf

pub struct SmtConf { /* private fields */ }

Configuration and solver specific info.

• z3: full support
• cvc4: full support in theory, but only partially tested. Note that get-value is known to crash some versions of CVC4.
• yices 2: full support in theory, but only partially tested. Command get-model will only work on Yices 2 > 2.6.1, and needs to be activated with Self::models. To understand why, see https://github.com/SRI-CSL/yices2/issues/162.

Implementations

impl SmtConf

pub fn style(&self) -> SmtStyle

Solver style accessor.

pub fn z3(cmd: impl Into<String>) -> Self

Creates a new z3-like solver configuration.

Examples

let conf = SmtConf::z3("my_z3_command");
assert!(conf.get_cmd() == "my_z3_command")

pub fn cvc4(cmd: impl Into<String>) -> Self

Creates a new cvc4-like solver configuration.

Examples

let conf = SmtConf::cvc4("my_cvc4_command");
assert!(conf.get_cmd() == "my_cvc4_command")

pub fn yices_2(cmd: impl Into<String>) -> Self

Creates a new yices-2-like solver configuration.

Examples

let conf = SmtConf::yices_2("my_yices_2_command");
assert!(conf.get_cmd() == "my_yices_2_command")

pub fn z3_or_env(cmd: Option<String>) -> SmtRes<Self>

Creates a z3-like solver configuration from an optional, or the value of the Z3_ENV_VAR environment variable.

Fails if cmd.is_none() and Z3_ENV_VAR is not set.

use rsmt2::conf::{SmtConf, Z3_ENV_VAR};
use std::env::{set_var, var_os};

// Passes the command directly.
let cmd = "z3_explicit";
let explicit_cmd = SmtConf::z3_or_env(Some(cmd.into())).expect("explicit");
assert_eq!(explicit_cmd.get_cmd(), cmd);

// Error if no command + environment variable not set.
assert_eq!(var_os(Z3_ENV_VAR), None);
let error = SmtConf::z3_or_env(None);
match error {
    Ok(_) => panic!("expected error, got an SMT style"),
    Err(e) => assert_eq!(
        &e.to_string(),
        "no command for z3 provided, \
        and `RSMT2_Z3_CMD` environment variable not set; \
        cannot spawn z3 solver"
    ),
}

// Retrieves the command from the environment.
let cmd = "z3_implicit";
assert_eq!(Z3_ENV_VAR, "RSMT2_Z3_CMD");
set_var(Z3_ENV_VAR, cmd);
let implicit_cmd = SmtConf::z3_or_env(None).expect("implicit");
assert_eq!(implicit_cmd.get_cmd(), cmd);

pub fn cvc4_or_env(cmd: Option<String>) -> SmtRes<Self>

Creates a CVC4-like solver configuration from an optional, or the value of the CVC4_ENV_VAR environment variable.

Fails if cmd.is_none() and CVC4_ENV_VAR is not set.

use rsmt2::conf::{SmtConf, CVC4_ENV_VAR};
use std::env::{set_var, var_os};

// Passes the command directly.
let cmd = "cvc4_explicit";
let explicit_cmd = SmtConf::cvc4_or_env(Some(cmd.into())).expect("explicit");
assert_eq!(explicit_cmd.get_cmd(), cmd);

// Error if no command + environment variable not set.
assert_eq!(var_os(CVC4_ENV_VAR), None);
let error = SmtConf::cvc4_or_env(None);
match error {
    Ok(_) => panic!("expected error, got an SMT style"),
    Err(e) => assert_eq!(
        &e.to_string(),
        "no command for CVC4 provided, \
        and `RSMT2_CVC4_CMD` environment variable not set; \
        cannot spawn CVC4 solver"
    ),
}

// Retrieves the command from the environment.
let cmd = "cvc4_implicit";
assert_eq!(CVC4_ENV_VAR, "RSMT2_CVC4_CMD");
set_var(CVC4_ENV_VAR, cmd);
let implicit_cmd = SmtConf::cvc4_or_env(None).expect("implicit");
assert_eq!(implicit_cmd.get_cmd(), cmd);

pub fn yices_2_or_env(cmd: Option<String>) -> SmtRes<Self>

Creates a Yices-2-like solver configuration from an optional, or the value of the YICES_2_ENV_VAR environment variable.

Fails if cmd.is_none() and YICES_2_ENV_VAR is not set.

use rsmt2::conf::{SmtConf, YICES_2_ENV_VAR};
use std::env::{set_var, var_os};

// Passes the command directly.
let cmd = "yices_2_explicit";
let explicit_cmd = SmtConf::yices_2_or_env(Some(cmd.into())).expect("explicit");
assert_eq!(explicit_cmd.get_cmd(), cmd);

// Error if no command + environment variable not set.
assert_eq!(var_os(YICES_2_ENV_VAR), None);
let error = SmtConf::yices_2_or_env(None);
match error {
    Ok(_) => panic!("expected error, got an SMT style"),
    Err(e) => assert_eq!(
        &e.to_string(),
        "no command for Yices 2 provided, \
        and `RSMT2_YICES_2_CMD` environment variable not set; \
        cannot spawn Yices 2 solver"
    ),
}

// Retrieves the command from the environment.
let cmd = "yices_2_implicit";
assert_eq!(YICES_2_ENV_VAR, "RSMT2_YICES_2_CMD");
set_var(YICES_2_ENV_VAR, cmd);
let implicit_cmd = SmtConf::yices_2_or_env(None).expect("implicit");
assert_eq!(implicit_cmd.get_cmd(), cmd);

pub fn default_z3() -> Self

Creates a new z3-like solver configuration and command.

Warning

The command used to run a particular solver is up to the end-user. As such, it does not make sense to use default commands for anything else than local testing. You should explicitely pass the command to use with Self::z3 instead.

Examples

let conf = SmtConf::default_z3();
assert! {
    conf.get_cmd() == "z3" || conf.get_cmd() == "z3.exe"
}

pub fn default_cvc4() -> Self

Creates a new cvc4-like solver configuration and command.

Warning

The command used to run a particular solver is up to the end-user. As such, it does not make sense to use default commands for anything else than local testing. You should explicitely pass the command to use with Self::cvc4 instead.

Examples

let conf = SmtConf::default_cvc4();
assert! {
    conf.get_cmd() == "cvc4" || conf.get_cmd() == "cvc4.exe"
}

pub fn default_yices_2() -> Self

Creates a new yices-2-like solver configuration and command.

Warning

The command used to run a particular solver is up to the end-user. As such, it does not make sense to use default commands for anything else than local testing. You should explicitely pass the command to use with Self::yices_2 instead.

Examples

let conf = SmtConf::default_yices_2();
assert! {
    conf.get_cmd() == "yices" || conf.get_cmd() == "yices.exe"
}

pub fn spawn<Parser>(self, parser: Parser) -> SmtRes<Solver<Parser>>

Spawns the solver.

Examples

let _solver = SmtConf::default_z3().spawn(()).unwrap();

pub fn desc(&self) -> &str

Concise description of the underlying solver.

Examples

assert_eq! { SmtConf::default_z3().desc(), "z3" }

pub fn get_cmd(&self) -> &str

Solver command.

Examples

let conf = SmtConf::default_z3();
assert! {
    conf.get_cmd() == "z3" || conf.get_cmd() == "z3.exe"
}

pub fn get_options(&self) -> &[String]

Options of the configuration.

Examples

assert_eq! {
    SmtConf::default_z3().get_options(), & [ "-in", "-smt2" ]
}

pub fn option<S: Into<String>>(&mut self, o: S) -> &mut Self

Adds an option to the configuration.

Examples

let mut conf = SmtConf::default_z3();
conf.option("arith.euclidean_solver=true");
assert_eq! {
    conf.get_options(),
    & [ "-in", "-smt2", "arith.euclidean_solver=true" ]
}

pub fn cmd<S: Into<String>>(&mut self, cmd: S) -> &mut Self

Sets the command for the solver.

Examples

let mut conf = SmtConf::default_z3();
conf.cmd("my_custom_z3_command");
assert_eq! { conf.get_cmd(), "my_custom_z3_command" }

pub fn get_models(&self) -> bool

Model production flag.

Examples

assert!(SmtConf::default_z3().get_models());

pub fn models(&mut self)

Activates model production.

Examples

let mut conf = SmtConf::default_z3();
conf.models();
assert!(conf.get_models());

pub fn set_models(&mut self, val: bool)

(De)activates model production.

Examples

let mut conf = SmtConf::default_z3();
conf.set_models(false);
assert!(!conf.get_models());

pub fn get_incremental(&self) -> bool

Incrementality.

Examples

let mut conf = SmtConf::default_z3();
assert!(conf.get_incremental());

pub fn incremental(&mut self)

Activates incrementality (push/pop, check-sat-assuming).

Examples

let mut conf = SmtConf::default_z3();
conf.incremental();
assert!(conf.get_incremental());

pub fn set_incremental(&mut self, val: bool)

Activates incrementality (push/pop, check-sat-assuming).

Examples

let mut conf = SmtConf::default_z3();
conf.incremental();
assert!(conf.get_incremental());

pub fn get_unsat_cores(&self) -> bool

Indicates if unsat core production is active.

Examples

assert!(! SmtConf::default_z3().get_unsat_cores());

pub fn unsat_cores(&mut self)

Activates unsat core production.

Examples

let mut conf = SmtConf::default_z3();
conf.unsat_cores();
assert!(conf.get_unsat_cores());

pub fn set_unsat_cores(&mut self, val: bool)

(De)activates unsat core production.

Examples

let mut conf = SmtConf::default_z3();
conf.set_unsat_cores(false);
assert!(!conf.get_unsat_cores());

pub fn get_check_sat_assuming(&self) -> ConfItem

Keyword for check-sat with assumptions.

Examples

assert_eq! {
    SmtConf::default_z3().get_check_sat_assuming(), Some("check-sat-assuming")
}

pub fn get_check_success(&self) -> bool

Indicates if success-checking is active, see Solver.

Examples

assert!(! SmtConf::default_z3().get_check_success());

pub fn check_success(&mut self)

Activates success-checking, see Solver.

Examples

let mut conf = SmtConf::default_z3();
conf.check_success();
assert!(conf.get_check_success());

pub fn set_check_success(&mut self, val: bool)

(De)activates sucess-checking, see Solver.

Examples

let mut conf = SmtConf::default_z3();
conf.set_check_success(true);
assert!(conf.get_check_success());

pub fn get_interpolants(&self) -> bool

Indicates if interpolant production is active.

Examples

assert!(SmtConf::default_z3().get_interpolants());

pub fn interpolants(&mut self) -> SmtRes<()>

Activates interpolant production.

Examples

let mut conf = SmtConf::default_z3();
conf.interpolants();
assert!(conf.get_interpolants());

pub fn set_interpolants(&mut self, val: bool) -> SmtRes<()>

(De)activates interpolant production.

Examples

let mut conf = SmtConf::default_z3();
conf.set_interpolants(false);
assert!(!conf.get_interpolants());

impl SmtConf

Solver-specific error-handling

pub fn enrich_get_values_error(&self, e: Error) -> Error

Adds information to a get-value error message if needed.

Trait Implementations

impl Clone for SmtConf

fn clone(&self) -> SmtConf

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for SmtConf

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

Formats the value using the given formatter.