[−][src]Struct rsmt2_zz::SmtConf
Configuration and solver specific info.
- [z3][z3]: full support
- [cvc4][cvc4]: full support in theory, but only partially tested. Note that
get-value
is known to crash some versions of CVC4. - [yices 2][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 in SmtConf withconf.models()
. To understand why, see https://github.com/SRI-CSL/yices2/issues/162.
Methods
impl SmtConf
[src]
pub fn z3() -> Self
[src]
Creates a new z3-like solver configuration.
Examples
let conf = SmtConf::z3() ; assert! { conf.get_cmd() == "z3" || conf.get_cmd() == "z3.exe" }
pub fn cvc4() -> Self
[src]
Creates a new cvc4-like solver configuration.
Examples
let conf = SmtConf::cvc4() ; assert! { conf.get_cmd() == "cvc4" || conf.get_cmd() == "cvc4.exe" }
pub fn yices_2() -> Self
[src]
Creates a new yices-2-like solver configuration.
Examples
let conf = SmtConf::yices_2() ; assert! { conf.get_cmd() == "yices-smt2" || conf.get_cmd() == "yices-smt2.exe" }
pub fn spawn<Parser>(self, parser: Parser) -> SmtRes<Solver<Parser>>
[src]
pub fn desc(&self) -> &str
[src]
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::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::z3().get_options(), & [ "-in", "-smt2" ] }
pub fn get_print_success(&self) -> bool
[src]
pub fn get_unsat_cores(&self) -> bool
[src]
pub fn get_check_sat_assuming(&self) -> Option<&'static str>
[src]
Keyword for check-sat with assumptions.
Examples
assert_eq! { SmtConf::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::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::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::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::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,
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.
fn to_owned(&self) -> T
[src]
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.
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>,