Struct SmtConf

pub struct SmtConf { /* private fields */ }

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 with conf.models(). To understand why, see https://github.com/SRI-CSL/yices2/issues/162.

Implementations

impl SmtConf

pub fn z3() -> Self

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

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

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>>

Spawns the solver.

Examples

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

pub fn desc(&self) -> &str

Concise description of the underlying solver.

Examples

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

pub fn get_models(&self) -> bool

Model production flag.

pub fn models(&mut self)

Activates model production.

pub fn get_incremental(&self) -> bool

Incrementality.

pub fn incremental(&mut self)

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

pub fn get_cmd(&self) -> &str

Solver command.

Examples

let conf = SmtConf::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::z3().get_options(), & [ "-in", "-smt2" ]
}

pub fn get_print_success(&self) -> bool

Indicates if print success is active.

Examples

assert! { ! SmtConf::z3().get_print_success() }

pub fn get_unsat_cores(&self) -> bool

Indicates if unsat cores is active.

Examples

assert! { ! SmtConf::z3().get_unsat_cores() }

pub fn get_check_sat_assuming(&self) -> Option<&'static str>

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

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

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)

Activates parse sucess.

Examples

let mut conf = SmtConf::z3() ;
conf.print_success() ;
assert! { conf.get_print_success() }

pub fn unsat_cores(&mut self)

Activates unsat-core production.

Examples

let mut conf = SmtConf::z3() ;
conf.unsat_cores() ;
assert! { conf.get_unsat_cores() }

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 duplicate 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.