Struct rsmt2::conf::SmtConf [−][src]
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 withSelf::models
. To understand why, see https://github.com/SRI-CSL/yices2/issues/162.
Implementations
impl SmtConf
[src]
pub fn z3(cmd: impl Into<String>) -> Self
[src]
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
[src]
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
[src]
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>
[src]
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>
[src]
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>
[src]
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
[src]
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
[src]
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
[src]
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>>
[src]
pub fn desc(&self) -> &str
[src]
Concise description of the underlying solver.
Examples
assert_eq! { SmtConf::default_z3().desc(), "z3" }
pub fn get_models(&self) -> bool
[src]
Model production flag.
pub fn models(&mut self)
[src]
Activates model production.
pub fn get_incremental(&self) -> bool
[src]
Incrementality.
pub fn incremental(&mut self)
[src]
Activates incrementality (push/pop, check-sat-assuming).
pub fn get_cmd(&self) -> &str
[src]
Solver command.
Examples
let conf = SmtConf::default_z3(); assert! { conf.get_cmd() == "z3" || conf.get_cmd() == "z3.exe" }
pub fn get_options(&self) -> &[String]
[src]
Options of the configuration.
Examples
assert_eq! { SmtConf::default_z3().get_options(), & [ "-in", "-smt2" ] }
pub fn get_print_success(&self) -> bool
[src]
Indicates if print success is active.
Examples
assert! { ! SmtConf::default_z3().get_print_success() }
pub fn get_unsat_cores(&self) -> bool
[src]
pub fn get_check_sat_assuming(&self) -> ConfItem
[src]
Keyword for check-sat with assumptions.
Examples
assert_eq! { SmtConf::default_z3().get_check_sat_assuming(), Some("check-sat-assuming") }
pub fn option<S: Into<String>>(&mut self, o: S) -> &mut Self
[src]
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
[src]
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 print_success(&mut self)
[src]
Activates parse sucess.
Examples
let mut conf = SmtConf::default_z3(); conf.print_success(); assert! { conf.get_print_success() }
pub fn unsat_cores(&mut self)
[src]
Activates unsat-core production.
Examples
let mut conf = SmtConf::default_z3(); conf.unsat_cores(); assert! { conf.get_unsat_cores() }
impl SmtConf
[src]
pub fn enrich_get_values_error(&self, e: Error) -> Error
[src]
Adds information to a get-value
error message if needed.
Trait Implementations
Auto Trait Implementations
impl RefUnwindSafe for SmtConf
impl Send for SmtConf
impl Sync for SmtConf
impl Unpin for SmtConf
impl UnwindSafe for SmtConf
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
pub fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
pub fn to_owned(&self) -> T
[src]
pub fn clone_into(&self, target: &mut T)
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
pub fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,