pub enum SmtStyle {
Z3,
CVC4,
Yices2,
}
Expand description
Solver styles.
- 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 inSmtConf
withSmtConf::models
. To understand why, see https://github.com/SRI-CSL/yices2/issues/162.
Variants
Z3
Z3-style smt solver.
CVC4
CVC4-style smt solver.
NB: CVC4 has only been partially tested at this point.
Yices2
Yices-2-style smt solver.
NB: Yices 2 has only been partially tested at this point.
Implementations
sourceimpl SmtStyle
impl SmtStyle
sourcepub fn env_cmd(self) -> SmtRes<Option<String>>
pub fn env_cmd(self) -> SmtRes<Option<String>>
Solver style command from the corresponding environment variable.
The environement variables scanned are Z3_ENV_VAR
, CVC4_ENV_VAR
and
YICES_2_ENV_VAR
.
Trait Implementations
sourceimpl PartialEq<SmtStyle> for SmtStyle
impl PartialEq<SmtStyle> for SmtStyle
impl Copy for SmtStyle
impl Eq for SmtStyle
impl StructuralEq for SmtStyle
impl StructuralPartialEq for SmtStyle
Auto Trait Implementations
impl RefUnwindSafe for SmtStyle
impl Send for SmtStyle
impl Sync for SmtStyle
impl Unpin for SmtStyle
impl UnwindSafe for SmtStyle
Blanket Implementations
sourceimpl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more