Struct mikino_api::prelude::SmtSolver
source · [−]pub struct SmtSolver<Parser> { /* private fields */ }
Expand description
Solver providing most of the SMT-LIB 2.5 commands.
Note the Self::tee
function, which takes a file writer to which it will write
everything sent to the solver.
Check Success
By default, SMT-LIB 2 commands such as declare-...
, define-...
, assert
, etc. are
silent in the sense that, if successful, they do not cause the solver output anything. As a
consequence, rmst2 does not check for errors after these commands are issued: since the command
does not produce anything on success, how long should we wait for an error before deciding the
command seems to have succeeded?
The problem is that when an error-producing command is issued, the actual error will only be
seen by rsmt2 when it parses a result —typically for a later check-sat
or a get-model
.
This can be an issue when debugging, or when passing unchecked expressions or commands from
downstream users.
let mut solver = Solver::default_z3(()).unwrap();
// vvvvvvvvvv~~~~ probably gonna cause an error
solver.assert("(> true 7)").unwrap();
solver.assert("(= 0 1)").unwrap();
solver.assert("(= 0 2)").unwrap();
solver.assert("(= 0 3)").unwrap();
solver.assert("(= 0 4)").unwrap();
solver.assert("(= 0 5)").unwrap();
// zero error so far
let e = solver.check_sat().unwrap_err();
assert_eq!(
&e.to_string(),
"\
solver error: \"line 3 column 13: \
Sort mismatch at argument #1 for function (declare-fun > (Int Int) Bool) \
supplied sort is Bool\"\
",
);
SMT-LIB 2 has a :print-success
option that forces all commands that do not produce a result
to issue success
on the solver’s stdout
when it’s done handling them. This allows rsmt2 to
notice and handle errors as soon as they happen, since it must check for success
every time.
let mut conf = SmtConf::default_z3();
// activates `success`-printing
conf.check_success();
let mut solver = Solver::new(conf, ()).unwrap();
// vvvvvvvvvv~~~~ probably gonna cause an error
let res = solver.assert("(> true 7)");
// did it?
let e = res.unwrap_err();
assert_eq!(
&e.to_string(),
"\
solver error: \"line 4 column 13: \
Sort mismatch at argument #1 for function (declare-fun > (Int Int) Bool) \
supplied sort is Bool\"\
",
);
solver.assert("(= 0 1)").unwrap();
solver.assert("(= 0 2)").unwrap();
solver.assert("(= 0 3)").unwrap();
solver.assert("(= 0 4)").unwrap();
solver.assert("(= 0 5)").unwrap();
let is_sat = solver.check_sat().unwrap();
We can also activate success
-checking at solver level.
let mut solver = Solver::default_z3(()).unwrap();
// activates `success` printing and checking.
solver.print_success().unwrap();
// vvvvvvvvvv~~~~ probably gonna cause an error
let res = solver.assert("(> true 7)");
// did it?
let e = res.unwrap_err();
assert_eq!(
&e.to_string(),
"\
solver error: \"line 4 column 13: \
Sort mismatch at argument #1 for function (declare-fun > (Int Int) Bool) \
supplied sort is Bool\"\
",
);
The downside is that rsmt2 will not parse success
on all commands that do not produce
results. This workflow is usually considered acceptable as parsing success
is expected to be
very, very cheap compared to whatever SMT check(s) the solver performs. This might not apply to
users performing a lot of small, very fast checks; especially if you declare/define/assert a
lot of things, as each declaration/definition/assertion causes to parse success
.
Implementations
sourceimpl<Parser> Solver<Parser>
impl<Parser> Solver<Parser>
sourcepub fn z3(
parser: Parser,
cmd: impl Into<String>
) -> Result<Solver<Parser>, Error>
pub fn z3(
parser: Parser,
cmd: impl Into<String>
) -> Result<Solver<Parser>, Error>
Creates a solver kid with the default z3 configuration.
Mostly used in tests, same as Self::new( SmtConf::z3(), parser )
.
sourcepub fn cvc4(
parser: Parser,
cmd: impl Into<String>
) -> Result<Solver<Parser>, Error>
pub fn cvc4(
parser: Parser,
cmd: impl Into<String>
) -> Result<Solver<Parser>, Error>
Creates a solver kid with the default cvc4 configuration.
Mostly used in tests, same as Self::new( SmtConf::z3(), parser )
.
sourcepub fn yices_2(
parser: Parser,
cmd: impl Into<String>
) -> Result<Solver<Parser>, Error>
pub fn yices_2(
parser: Parser,
cmd: impl Into<String>
) -> Result<Solver<Parser>, Error>
Creates a solver kid with the default yices 2 configuration.
Mostly used in tests, same as Self::new( SmtConf::yices_2(), parser )
.
sourcepub fn default_z3(parser: Parser) -> Result<Solver<Parser>, Error>
pub fn default_z3(parser: Parser) -> Result<Solver<Parser>, Error>
Creates a solver kid with the default z3 configuration and command.
Mostly used in tests, same as Self::new( SmtConf::default_z3(), parser )
.
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.
sourcepub fn default_cvc4(parser: Parser) -> Result<Solver<Parser>, Error>
pub fn default_cvc4(parser: Parser) -> Result<Solver<Parser>, Error>
Creates a solver kid with the default cvc4 configuration and command.
Mostly used in tests, same as Self::new( SmtConf::default_z3(), parser )
.
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.
sourcepub fn default_yices_2(parser: Parser) -> Result<Solver<Parser>, Error>
pub fn default_yices_2(parser: Parser) -> Result<Solver<Parser>, Error>
Creates a solver kid with the default yices 2 configuration and command.
Mostly used in tests, same as Self::new( SmtConf::default_yices_2(), parser )
.
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.
sourcepub fn tee(&mut self, file: File) -> Result<(), Error>
pub fn tee(&mut self, file: File) -> Result<(), Error>
Forces the solver to write all communications to a file.
- fails if the solver is already tee-ed;
- see also
Self::path_tee
.
sourcepub fn path_tee<P>(&mut self, path: P) -> Result<(), Error> where
P: AsRef<Path>,
pub fn path_tee<P>(&mut self, path: P) -> Result<(), Error> where
P: AsRef<Path>,
Forces the solver to write all communications to a file.
- opens
file
withcreate
andwrite
; - fails if the solver is already tee-ed;
- see also
Self::tee
.
sourcepub fn kill(&mut self) -> Result<(), Error>
pub fn kill(&mut self) -> Result<(), Error>
Kills the solver kid.
The windows version just prints (exit)
on the kid’s stdin
. Anything else seems to cause
problems.
This function is automatically called when the solver is dropped.
sourceimpl<Parser> Solver<Parser>
impl<Parser> Solver<Parser>
sourcepub fn produce_unsat_cores(&mut self) -> Result<(), Error>
pub fn produce_unsat_cores(&mut self) -> Result<(), Error>
Activates unsat core production.
sourcepub fn produce_models(&mut self) -> Result<(), Error>
pub fn produce_models(&mut self) -> Result<(), Error>
Activates model production.
sourcepub fn assert(&mut self, expr: impl Expr2Smt<()>) -> Result<(), Error>
pub fn assert(&mut self, expr: impl Expr2Smt<()>) -> Result<(), Error>
Asserts an expression.
Examples
let mut solver = Solver::default_z3(()).unwrap();
solver.assert("(= 0 1)").unwrap();
sourcepub fn check_sat(&mut self) -> Result<bool, Error>
pub fn check_sat(&mut self) -> Result<bool, Error>
Check-sat command, turns unknown
results into errors.
See also
If you want a more natural way to handle unknown results, see parse_check_sat_or_unk
.
Examples
let mut conf = SmtConf::default_z3();
conf.option("-t:10");
let mut solver = Solver::new(conf, ()).unwrap();
solver.declare_const("x", "Int").unwrap();
solver.declare_const("y", "Int").unwrap();
solver.push(1).unwrap();
solver.assert("(= (+ x y) 0)").unwrap();
let maybe_sat = solver.check_sat().unwrap();
assert_eq! { maybe_sat, true }
solver.pop(1).unwrap();
solver.assert("(= (+ (* x x y) (* y y x)) 7654321)").unwrap();
let sat_res = & solver.check_sat();
match * sat_res {
Err(ref e) => match * e.kind() {
::rsmt2::errors::ErrorKind::Unknown => (),
_ => panic!("expected unknown"),
},
Ok(res) => panic!("expected error: {:?}", res),
}
sourcepub fn check_sat_or_unk(&mut self) -> Result<Option<bool>, Error>
pub fn check_sat_or_unk(&mut self) -> Result<Option<bool>, Error>
Check-sat command, turns unknown
results in None
.
See also
Examples
let mut conf = SmtConf::default_z3();
conf.option("-t:10");
solver.declare_const("x", "Int").unwrap();
solver.declare_const("y", "Int").unwrap();
solver.push(1).unwrap();
solver.assert("(= (+ x y) 0)").unwrap();
let maybe_sat = solver.check_sat_or_unk().unwrap();
assert_eq! { maybe_sat, Some(true) }
solver.pop(1).unwrap();
solver.assert("(= (+ (* x x y) (* y y x)) 7654321)").unwrap();
let maybe_sat = solver.check_sat_or_unk().unwrap();
// Unknown ~~~~~~~~~~~~~vvvv
assert_eq! { maybe_sat, None }
sourcepub fn reset(&mut self) -> Result<(), Error>
pub fn reset(&mut self) -> Result<(), Error>
Resets the underlying solver. Restarts the kid process if no reset command is supported.
Examples
let mut solver = Solver::default_z3(()).unwrap();
solver.assert("(= 0 1)").unwrap();
assert!(! solver.check_sat().unwrap());
solver.reset().unwrap();
assert!(solver.check_sat().unwrap());
sourcepub fn declare_const(
&mut self,
symbol: impl Sym2Smt<()>,
out_sort: impl Sort2Smt
) -> Result<(), Error>
pub fn declare_const(
&mut self,
symbol: impl Sym2Smt<()>,
out_sort: impl Sort2Smt
) -> Result<(), Error>
Declares a new constant.
Examples
let mut solver = Solver::default_z3(()).unwrap();
solver.declare_const("x", "Int").unwrap()
sourcepub fn declare_fun<FunSym, Args, OutSort>(
&mut self,
symbol: FunSym,
args: Args,
out: OutSort
) -> Result<(), Error> where
FunSym: Sym2Smt<()>,
OutSort: Sort2Smt,
Args: IntoIterator,
<Args as IntoIterator>::Item: Sort2Smt,
pub fn declare_fun<FunSym, Args, OutSort>(
&mut self,
symbol: FunSym,
args: Args,
out: OutSort
) -> Result<(), Error> where
FunSym: Sym2Smt<()>,
OutSort: Sort2Smt,
Args: IntoIterator,
<Args as IntoIterator>::Item: Sort2Smt,
Declares a new function symbol.
let mut solver = Solver::default_z3(()).unwrap();
solver.declare_fun(
"my_symbol", & [ "Int", "Real", "Bool" ], "Bool"
).unwrap()
sourcepub fn define_const(
&mut self,
symbol: impl Sym2Smt<()>,
out: impl Sort2Smt,
body: impl Expr2Smt<()>
) -> Result<(), Error>
pub fn define_const(
&mut self,
symbol: impl Sym2Smt<()>,
out: impl Sort2Smt,
body: impl Expr2Smt<()>
) -> Result<(), Error>
Defines a new constant function symbol.
Examples
let mut solver = Solver::default_z3(()).unwrap();
solver.define_const(
"seven", "Int", "7"
).unwrap()
sourcepub fn define_fun<Args>(
&mut self,
symbol: impl Sym2Smt<()>,
args: Args,
out: impl Sort2Smt,
body: impl Expr2Smt<()>
) -> Result<(), Error> where
Args: IntoIterator,
<Args as IntoIterator>::Item: SymAndSort<()>,
pub fn define_fun<Args>(
&mut self,
symbol: impl Sym2Smt<()>,
args: Args,
out: impl Sort2Smt,
body: impl Expr2Smt<()>
) -> Result<(), Error> where
Args: IntoIterator,
<Args as IntoIterator>::Item: SymAndSort<()>,
Defines a new function symbol.
Examples
let mut solver = Solver::default_z3(()).unwrap();
solver.define_fun(
"abs", & [ ("n", "Int") ], "Int", "(ite (< x 0) (- x) x)"
).unwrap()
sourcepub fn push(&mut self, n: u8) -> Result<(), Error>
pub fn push(&mut self, n: u8) -> Result<(), Error>
Pushes n
layers on the assertion stack.
- see also
Self::pop
.
Note that using actlits is more efficient than push/pop, and is useable for most push/pop use-cases.
Examples
let mut solver = Solver::default_z3(()).unwrap();
solver.declare_const("x", "Int").unwrap();
solver.declare_const("y", "Int").unwrap();
solver.assert("(= x y)").unwrap();
let sat = solver.check_sat().unwrap();
assert!(sat);
solver.push(1).unwrap();
solver.assert("(= x (+ x 1))").unwrap();
let sat = solver.check_sat().unwrap();
assert!(! sat);
solver.pop(1).unwrap();
let sat = solver.check_sat().unwrap();
assert!(sat);
sourcepub fn pop(&mut self, n: u8) -> Result<(), Error>
pub fn pop(&mut self, n: u8) -> Result<(), Error>
Pops n
layers off the assertion stack.
- see also
Self::push
.
Note that using actlits is more efficient than push/pop, and is useable for most push/pop use-cases.
sourcepub fn check_sat_assuming<Idents>(
&mut self,
idents: Idents
) -> Result<bool, Error> where
Idents: IntoIterator,
<Idents as IntoIterator>::Item: Sym2Smt<()>,
pub fn check_sat_assuming<Idents>(
&mut self,
idents: Idents
) -> Result<bool, Error> where
Idents: IntoIterator,
<Idents as IntoIterator>::Item: Sym2Smt<()>,
Check-sat assuming command, turns unknown
results into errors.
- see also actlits.
sourcepub fn check_sat_assuming_or_unk<Ident, Idents>(
&mut self,
idents: Idents
) -> Result<Option<bool>, Error> where
Idents: IntoIterator,
<Idents as IntoIterator>::Item: Sym2Smt<()>,
pub fn check_sat_assuming_or_unk<Ident, Idents>(
&mut self,
idents: Idents
) -> Result<Option<bool>, Error> where
Idents: IntoIterator,
<Idents as IntoIterator>::Item: Sym2Smt<()>,
Check-sat assuming command, turns unknown
results into None
.
- see also actlits.
sourcepub fn set_logic(&mut self, logic: Logic) -> Result<(), Error>
pub fn set_logic(&mut self, logic: Logic) -> Result<(), Error>
Sets the logic.
Examples
let mut solver = Solver::default_z3(()).unwrap();
solver.set_logic( ::rsmt2::Logic::QF_UF ).unwrap();
sourcepub fn set_custom_logic(&mut self, logic: impl AsRef<str>) -> Result<(), Error>
pub fn set_custom_logic(&mut self, logic: impl AsRef<str>) -> Result<(), Error>
Sets a custom logic.
Examples
let mut solver = Solver::default_z3(()).unwrap();
solver.set_custom_logic("QF_UFBV").unwrap();
sourcepub fn define_fun_rec<Args>(
&mut self,
symbol: impl Sym2Smt<()>,
args: Args,
out: impl Sort2Smt,
body: impl Expr2Smt<()>
) -> Result<(), Error> where
Args: IntoIterator,
<Args as IntoIterator>::Item: SymAndSort<()>,
pub fn define_fun_rec<Args>(
&mut self,
symbol: impl Sym2Smt<()>,
args: Args,
out: impl Sort2Smt,
body: impl Expr2Smt<()>
) -> Result<(), Error> where
Args: IntoIterator,
<Args as IntoIterator>::Item: SymAndSort<()>,
Defines a recursive function.
Examples
let mut solver = Solver::default_z3(()).unwrap();
solver.define_fun_rec(
"abs", & [ ("n", "Int") ], "Int", "(ite (< x 0) (abs (- x)) x)"
).unwrap()
sourcepub fn define_funs_rec<Defs>(&mut self, funs: Defs) -> Result<(), Error> where
Defs: IntoIterator + Clone,
<Defs as IntoIterator>::Item: FunDef<()>,
pub fn define_funs_rec<Defs>(&mut self, funs: Defs) -> Result<(), Error> where
Defs: IntoIterator + Clone,
<Defs as IntoIterator>::Item: FunDef<()>,
Defines some (possibily mutually) recursive functions.
Examples
let mut solver = Solver::default_z3(()).unwrap();
solver.define_funs_rec( & [
("abs_1", [ ("n", "Int") ], "Int", "(ite (< x 0) (abs_2 (- x)) x)"),
("abs_2", [ ("n", "Int") ], "Int", "(ite (< x 0) (abs_3 (- x)) x)"),
("abs_3", [ ("n", "Int") ], "Int", "(ite (< x 0) (abs_1 (- x)) x)"),
] ).unwrap()
sourcepub fn declare_datatypes<Defs>(&mut self, defs: Defs) -> Result<(), Error> where
Defs: IntoIterator + Clone,
<Defs as IntoIterator>::Item: AdtDecl,
pub fn declare_datatypes<Defs>(&mut self, defs: Defs) -> Result<(), Error> where
Defs: IntoIterator + Clone,
<Defs as IntoIterator>::Item: AdtDecl,
Declares mutually recursive datatypes.
A relatively recent version of z3 is recommended. Sort definition is a relatively expert action, this function is a bit complex. The example below goes over how it works.
Examples
use rsmt2::print::{AdtDecl, AdtVariantField, AdtVariant};
// Alright, so we're going to declare two mutually recursive sorts. It is easier to pack the
// sort-declaration data in custom types. If you want to declare a sort, you most likely
// already have a representation for it, so working on custom types is reasonable.
// Notice that the `AdtDecl`, `AdtVariantField` and `AdtVariant` traits from `rsmt2::print::_`
// are in scope. This is what our custom types will need to generate to declare the sort.
// We'll use static string slices for simplicity as `&str` implements all printing traits.
type Sym = &'static str;
type Sort = &'static str;
// Let's start with the top-level sort type.
struct MySort {
// Name of the sort, for instance `List`.
sym: Sym,
// Symbol(s) for the type parameter(s), for instance `T` for `List<T>`. Must be a collection
// of known length, because rsmt2 needs to access the arity (number of type parameters).
args: Vec<Sym>,
// Body of the sort: its variants. For instance the `nil` and `cons` variants for `List<T>`.
variants: Vec<Variant>,
}
impl MySort {
// This thing build the actual definition expected by rsmt2. Its output is something that
// implements `AdtDecl` and can only live as long as the input ref to `self`.
fn as_decl<'me>(&'me self) -> impl AdtDecl + 'me {
// Check out rsmt2's documentation and you'll see that `AdtDecl` is already implemented for
// certain triplets.
(
// Symbol.
&self.sym,
// Sized collection of type-parameter symbols.
&self.args,
// Variant, collection of iterator over `impl AdtVariant` (see below).
self.variants.iter().map(Variant::as_decl),
)
}
fn tree() -> Self {
Self {
sym: "Tree",
args: vec!["T"],
variants: vec![Variant::tree_leaf(), Variant::tree_node()],
}
}
}
// Next up, variants. A variant is a symbol (*e.g.* `nil` or `cons` for `List<T>`) and some
// fields which describe the data stored in the variant.
struct Variant {
sym: Sym,
fields: Vec<Field>,
}
impl Variant {
// Variant declaration; again, `AdtVariant` is implemented for certain types of pairs.
fn as_decl<'me>(&'me self) -> impl AdtVariant + 'me {
(
// Symbol.
self.sym,
// Iterator over field declarations.
self.fields.iter().map(Field::as_decl),
)
}
fn tree_leaf() -> Self {
Self {
sym: "leaf",
fields: vec![],
}
}
fn tree_node() -> Self {
Self {
sym: "node",
fields: vec![Field::tree_node_value(), Field::tree_node_children()],
}
}
}
// A symbol and a sort: describes a piece of data in a variant with a symbol to retrieve it,
// *i.e.* the name of the field.
struct Field {
sym: Sym,
sort: Sort,
}
impl Field {
// As usual, `AdtVariantField` is implemented for certain pairs.
fn as_decl(&self) -> impl AdtVariantField {
(self.sym, self.sort)
}
fn tree_node_value() -> Self {
Self {
sym: "value",
sort: "T",
}
}
fn tree_node_children() -> Self {
Self {
sym: "children",
sort: "(TreeList T)",
}
}
}
let tree = MySort::tree();
// Now this `tree` uses an non-existing `(TreeList T)` sort to store its children, let's declare
// it now.
let nil = Variant {
sym: "nil",
fields: vec![],
};
let cons = Variant {
sym: "cons",
fields: vec![
Field {
sym: "car",
sort: "(Tree T)",
},
Field {
sym: "cdr",
sort: "(TreeList T)",
},
],
};
let tree_list = MySort {
sym: "TreeList",
args: vec!["T"],
variants: vec![nil, cons],
};
let mut solver = rsmt2::Solver::default_z3(()).unwrap();
solver
// These sort are mutually recursive, `Solver::declare_datatypes` needs to declare them at the
// same time.
.declare_datatypes(&[tree.as_decl(), tree_list.as_decl()])
.unwrap();
// That's it! Solver now knows these sorts and we can use them.
solver.declare_const("t1", "(Tree Int)").unwrap();
solver.declare_const("t2", "(Tree Bool)").unwrap();
solver.assert("(> (value t1) 20)").unwrap();
solver.assert("(not (is-leaf t2))").unwrap();
solver.assert("(not (value t2))").unwrap();
let sat = solver.check_sat().unwrap();
assert!(sat);
sourceimpl<Parser> Solver<Parser>
impl<Parser> Solver<Parser>
sourcepub fn get_model<Ident, Type, Value>(
&mut self
) -> Result<Vec<(Ident, Vec<(Ident, Type), Global>, Type, Value), Global>, Error> where
Parser: for<'p> IdentParser<Ident, Type, &'p mut SmtParser<BufReader<ChildStdout>>> + for<'p> ModelParser<Ident, Type, Value, &'p mut SmtParser<BufReader<ChildStdout>>>,
pub fn get_model<Ident, Type, Value>(
&mut self
) -> Result<Vec<(Ident, Vec<(Ident, Type), Global>, Type, Value), Global>, Error> where
Parser: for<'p> IdentParser<Ident, Type, &'p mut SmtParser<BufReader<ChildStdout>>> + for<'p> ModelParser<Ident, Type, Value, &'p mut SmtParser<BufReader<ChildStdout>>>,
Get-model command.
- See also
Self::get_model_const
.
Examples
use rsmt2::Solver;
let mut solver = Solver::default_z3(()).unwrap();
solver.declare_const("x", "Int").unwrap();
solver.declare_const("y", "Int").unwrap();
solver.assert("(= (+ x y) 0)").unwrap();
let is_sat = solver.check_sat().unwrap();
assert!(is_sat);
let model = solver.get_model().unwrap();
let (mut x, mut y) = (None, None);
// `x` and `y` are constants, *i.e.* functions taking no arguments. In general however,
// `get_model` can yield functions. Hence the list of arguments
// vvvv
for (ident, args, sort, value) in model {
assert!(args.is_empty());
if ident == "x" {
x = Some(isize::from_str_radix(&value, 10).expect("while parsing `x` value"))
} else if ident == "y" {
y = Some(isize::from_str_radix(&value, 10).expect("while parsing `y` value"))
} else {
panic!("unexpected ident `{}` in model", ident)
}
}
let (x, y) = (x.expect("`x` not found in model"), y.expect("`y` not found in model"));
assert_eq!(x + y, 0)
sourcepub fn get_model_const<Ident, Type, Value>(
&mut self
) -> Result<Vec<(Ident, Type, Value), Global>, Error> where
Parser: for<'p> IdentParser<Ident, Type, &'p mut SmtParser<BufReader<ChildStdout>>> + for<'p> ModelParser<Ident, Type, Value, &'p mut SmtParser<BufReader<ChildStdout>>>,
pub fn get_model_const<Ident, Type, Value>(
&mut self
) -> Result<Vec<(Ident, Type, Value), Global>, Error> where
Parser: for<'p> IdentParser<Ident, Type, &'p mut SmtParser<BufReader<ChildStdout>>> + for<'p> ModelParser<Ident, Type, Value, &'p mut SmtParser<BufReader<ChildStdout>>>,
Get-model command when all the symbols are nullary.
- See also
Self::get_model
.
Examples
use rsmt2::Solver;
let mut solver = Solver::default_z3(()).unwrap();
solver.declare_const("x", "Int").unwrap();
solver.declare_const("y", "Int").unwrap();
solver.assert("(= (+ x y) 0)").unwrap();
let is_sat = solver.check_sat().unwrap();
assert!(is_sat);
// We only have `x` and `y` which are constant symbols (functions with no arguments).
// Using `get_model_const` instead of `get_model` will generate a model where symbols
// have no arguments.
let model = solver.get_model_const().unwrap();
let (mut x, mut y) = (None, None);
// No list of arguments in the model, as opposed to models from `get_model`.
// vvvvvvvvvvvvvvvvvv
for (ident, sort, value) in model {
if ident == "x" {
x = Some(isize::from_str_radix(&value, 10).expect("while parsing `x` value"))
} else if ident == "y" {
y = Some(isize::from_str_radix(&value, 10).expect("while parsing `y` value"))
} else {
panic!("unexpected ident `{}` in model", ident)
}
}
let (x, y) = (x.expect("`x` not found in model"), y.expect("`y` not found in model"));
assert_eq!(x + y, 0)
sourcepub fn get_values<Exprs, PExpr, PValue>(
&mut self,
exprs: Exprs
) -> Result<Vec<(PExpr, PValue), Global>, Error> where
Parser: for<'p> ExprParser<PExpr, (), &'p mut SmtParser<BufReader<ChildStdout>>> + for<'p> ValueParser<PValue, &'p mut SmtParser<BufReader<ChildStdout>>>,
Exprs: IntoIterator,
<Exprs as IntoIterator>::Item: Expr2Smt<()>,
pub fn get_values<Exprs, PExpr, PValue>(
&mut self,
exprs: Exprs
) -> Result<Vec<(PExpr, PValue), Global>, Error> where
Parser: for<'p> ExprParser<PExpr, (), &'p mut SmtParser<BufReader<ChildStdout>>> + for<'p> ValueParser<PValue, &'p mut SmtParser<BufReader<ChildStdout>>>,
Exprs: IntoIterator,
<Exprs as IntoIterator>::Item: Expr2Smt<()>,
Get-values command.
- See also
Self::get_values_with
.
Notice that the input expression type and the output one have no reason to be the same.
Examples
use rsmt2::Solver;
let mut solver = Solver::default_z3(()).unwrap();
solver.declare_const("x", "Int").unwrap();
solver.declare_const("y", "Int").unwrap();
solver.assert("(= (+ x y) 0)").unwrap();
let is_sat = solver.check_sat().unwrap();
assert!(is_sat);
let vars = ["x", "y"];
let values = solver.get_values(&vars).unwrap();
assert_eq!(vars.len(), values.len());
let mut sum = 0;
let mut values = values.into_iter();
let (var, val) = values.next().unwrap();
assert_eq!(var, "x");
let val = isize::from_str_radix(&val, 10).expect("while parsing `x` value");
sum += val;
let (var, val) = values.next().unwrap();
assert_eq!(var, "y");
let val = isize::from_str_radix(&val, 10).expect("while parsing `y` value");
sum += val;
assert_eq!(values.next(), None);
assert_eq!(sum, 0);
sourcepub fn get_values_with<Exprs, PExpr, PValue, Info>(
&mut self,
exprs: Exprs,
info: Info
) -> Result<Vec<(PExpr, PValue), Global>, Error> where
Info: Copy,
Parser: for<'p> ExprParser<PExpr, Info, &'p mut SmtParser<BufReader<ChildStdout>>> + for<'p> ValueParser<PValue, &'p mut SmtParser<BufReader<ChildStdout>>>,
Exprs: IntoIterator,
<Exprs as IntoIterator>::Item: Expr2Smt<Info>,
pub fn get_values_with<Exprs, PExpr, PValue, Info>(
&mut self,
exprs: Exprs,
info: Info
) -> Result<Vec<(PExpr, PValue), Global>, Error> where
Info: Copy,
Parser: for<'p> ExprParser<PExpr, Info, &'p mut SmtParser<BufReader<ChildStdout>>> + for<'p> ValueParser<PValue, &'p mut SmtParser<BufReader<ChildStdout>>>,
Exprs: IntoIterator,
<Exprs as IntoIterator>::Item: Expr2Smt<Info>,
Get-values command.
- See also
Self::get_values
.
Notice that the input expression type and the output one have no reason to be the same.
sourcepub fn get_unsat_core<Sym>(&mut self) -> Result<Vec<Sym, Global>, Error> where
Parser: for<'p> SymParser<Sym, &'p mut SmtParser<BufReader<ChildStdout>>>,
pub fn get_unsat_core<Sym>(&mut self) -> Result<Vec<Sym, Global>, Error> where
Parser: for<'p> SymParser<Sym, &'p mut SmtParser<BufReader<ChildStdout>>>,
Get-unsat-core command.
See also
NamedExpr
: a convenient wrapper around any expression that gives it a name.
Examples
use rsmt2::prelude::*;
let mut conf = SmtConf::default_z3();
conf.unsat_cores();
let mut solver = Solver::new(conf, ()).unwrap();
solver.declare_const("n", "Int").unwrap();
solver.declare_const("m", "Int").unwrap();
solver.assert("true").unwrap();
let e_1 = "(> n 7)";
let label_e_1 = "e_1";
let named = NamedExpr::new(label_e_1, e_1);
solver.assert(&named).unwrap();
let e_2 = "(> m 0)";
let label_e_2 = "e_2";
let named = NamedExpr::new(label_e_2, e_2);
solver.assert(&named).unwrap();
let e_3 = "(< n 3)";
let label_e_3 = "e_3";
let named = NamedExpr::new(label_e_3, e_3);
solver.assert(&named).unwrap();
assert!(!solver.check_sat().unwrap());
let core: Vec<String> = solver.get_unsat_core().unwrap();
assert_eq!(core, vec![label_e_1, label_e_3]);
sourcepub fn get_interpolant<Expr>(
&mut self,
sym_1: impl Sym2Smt<()>,
sym_2: impl Sym2Smt<()>
) -> Result<Expr, Error> where
Parser: for<'p> ExprParser<Expr, (), &'p mut SmtParser<BufReader<ChildStdout>>>,
pub fn get_interpolant<Expr>(
&mut self,
sym_1: impl Sym2Smt<()>,
sym_2: impl Sym2Smt<()>
) -> Result<Expr, Error> where
Parser: for<'p> ExprParser<Expr, (), &'p mut SmtParser<BufReader<ChildStdout>>>,
Get-interpolant command.
sourcepub fn get_interpolant_with<Info, Expr>(
&mut self,
sym_1: impl Sym2Smt<()>,
sym_2: impl Sym2Smt<()>,
info: Info
) -> Result<Expr, Error> where
Parser: for<'p> ExprParser<Expr, Info, &'p mut SmtParser<BufReader<ChildStdout>>>,
pub fn get_interpolant_with<Info, Expr>(
&mut self,
sym_1: impl Sym2Smt<()>,
sym_2: impl Sym2Smt<()>,
info: Info
) -> Result<Expr, Error> where
Parser: for<'p> ExprParser<Expr, Info, &'p mut SmtParser<BufReader<ChildStdout>>>,
Get-interpolant command.
- See Craig interpolation.
- Only supported by recent versions of Z3.
- This command is only legal after an
unsat
result. - The order of the two inputs symbols matters.
Typically, you should assert two named formulas f_1
and f_2
(example
below). Assuming you issue check-sat
and get unsat
(meaning f_1 ⇒ ¬f_2
),
then get_interpolant(f_1, f_2)
produces a formula I
such that
f_1 ⇒ I
, i.e.f_1 ∧ ¬I
is unsat,I ⇒ ¬f_2
, i.e.I ∧ f_2
is unsat, andI
only mentions variables (constant symbols) that appear in bothf_1
andf_2
.
One way to think about interpolation is that I
captures the reason for f_1 ∧ f_2
being
unsat from the point of view of f_1
, in the sense that I
does not contain variables
that do not appear in f_1
.
Examples
use rsmt2::prelude::*;
let mut solver = Solver::default_z3(()).unwrap();
let (n, m) = ("n", "m");
solver.declare_const(n, "Int").expect("declaring n");
solver.declare_const(m, "Int").expect("declaring m");
let f_1 = "(or (= (mod n 2) 0) (> n 42))";
solver.assert(f_1.to_smt_named("f_1")).expect("assert f_1");
let f_2 = "(and (< n m) (< m 9) (= (mod n 2) 1))";
solver.assert(f_2.to_smt_named("f_2")).expect("assert f_2");
let is_sat = solver.check_sat().unwrap();
assert!(!is_sat);
let interpolant: String = solver.get_interpolant("f_1", "f_2").unwrap();
assert_eq!(&interpolant, "(or (not (<= n 42)) (= (mod n 2) 0))");
// Let's try again, but this time we switch the arguments of `get_interpolant`.
let interpolant: String = solver.get_interpolant("f_2", "f_1").unwrap();
assert_eq!(&interpolant, "(and (= (mod n 2) 1) (<= n 7))");
sourceimpl<Parser> Solver<Parser>
impl<Parser> Solver<Parser>
Actlit-Related Functions.
See the actlit
module for more details.
sourcepub fn get_actlit(&mut self) -> Result<Actlit, Error>
pub fn get_actlit(&mut self) -> Result<Actlit, Error>
Introduces a new actlit.
See the actlit
module for more details.
sourcepub fn de_actlit(&mut self, actlit: Actlit) -> Result<(), Error>
pub fn de_actlit(&mut self, actlit: Actlit) -> Result<(), Error>
Deactivates an activation literal, alias for solver.set_actlit(actlit, false)
.
See the actlit
module for more details.
sourcepub fn set_actlit(&mut self, actlit: Actlit, b: bool) -> Result<(), Error>
pub fn set_actlit(&mut self, actlit: Actlit, b: bool) -> Result<(), Error>
Forces the value of an actlit and consumes it.
See the actlit
module for more details.
sourcepub fn assert_act(
&mut self,
actlit: &Actlit,
expr: impl Expr2Smt<()>
) -> Result<(), Error>
pub fn assert_act(
&mut self,
actlit: &Actlit,
expr: impl Expr2Smt<()>
) -> Result<(), Error>
Asserts an expression without print information, guarded by an activation literal.
See the actlit
module for more details.
sourcepub fn check_sat_act<Actlits>(
&mut self,
actlits: Actlits
) -> Result<bool, Error> where
Actlits: IntoIterator,
<Actlits as IntoIterator>::Item: Sym2Smt<()>,
pub fn check_sat_act<Actlits>(
&mut self,
actlits: Actlits
) -> Result<bool, Error> where
Actlits: IntoIterator,
<Actlits as IntoIterator>::Item: Sym2Smt<()>,
Check-sat command with activation literals, turns unknown
results into
errors.
sourcepub fn check_sat_act_or_unk<Actlits>(
&mut self,
actlits: Actlits
) -> Result<Option<bool>, Error> where
Actlits: IntoIterator,
<Actlits as IntoIterator>::Item: Sym2Smt<()>,
pub fn check_sat_act_or_unk<Actlits>(
&mut self,
actlits: Actlits
) -> Result<Option<bool>, Error> where
Actlits: IntoIterator,
<Actlits as IntoIterator>::Item: Sym2Smt<()>,
Check-sat command with activation literals, turns unknown
results in
None
.
sourceimpl<Parser> Solver<Parser>
impl<Parser> Solver<Parser>
sourcepub fn print_check_sat(&mut self) -> Result<FutureCheckSat, Error>
pub fn print_check_sat(&mut self) -> Result<FutureCheckSat, Error>
Prints a check-sat command.
Allows to print the check-sat
and get the result later, e.g. with
Self::parse_check_sat
.
Examples
use rsmt2::Solver;
let mut solver = Solver::default_z3(()).unwrap();
solver.declare_const("x", "Int").unwrap();
solver.declare_const("y", "Int").unwrap();
solver.assert("(= (+ x y) 0)").unwrap();
let future = solver.print_check_sat().unwrap();
// Do stuff while the solver works.
let sat = solver.parse_check_sat(future).unwrap();
assert!(sat);
sourcepub fn print_check_sat_act<Actlits>(
&mut self,
actlits: Actlits
) -> Result<FutureCheckSat, Error> where
Actlits: IntoIterator,
<Actlits as IntoIterator>::Item: Sym2Smt<()>,
pub fn print_check_sat_act<Actlits>(
&mut self,
actlits: Actlits
) -> Result<FutureCheckSat, Error> where
Actlits: IntoIterator,
<Actlits as IntoIterator>::Item: Sym2Smt<()>,
Check-sat command, with actlits.
See the actlit
module for more details.
sourcepub fn parse_check_sat(&mut self, FutureCheckSat) -> Result<bool, Error>
pub fn parse_check_sat(&mut self, FutureCheckSat) -> Result<bool, Error>
Parse the result of a check-sat, turns unknown
results into errors.
sourcepub fn parse_check_sat_or_unk(
&mut self,
FutureCheckSat
) -> Result<Option<bool>, Error>
pub fn parse_check_sat_or_unk(
&mut self,
FutureCheckSat
) -> Result<Option<bool>, Error>
Parse the result of a check-sat, turns unknown
results into None
.
sourcepub fn print_get_interpolant(
&mut self,
sym_1: impl Sym2Smt<()>,
sym_2: impl Sym2Smt<()>
) -> Result<(), Error>
pub fn print_get_interpolant(
&mut self,
sym_1: impl Sym2Smt<()>,
sym_2: impl Sym2Smt<()>
) -> Result<(), Error>
Get-interpolant command.
At the time of writing, only Z3 supports this command.
sourcepub fn print_check_sat_assuming<Idents>(
&mut self,
bool_vars: Idents
) -> Result<FutureCheckSat, Error> where
Idents: IntoIterator,
<Idents as IntoIterator>::Item: Sym2Smt<()>,
pub fn print_check_sat_assuming<Idents>(
&mut self,
bool_vars: Idents
) -> Result<FutureCheckSat, Error> where
Idents: IntoIterator,
<Idents as IntoIterator>::Item: Sym2Smt<()>,
Check-sat with assumptions command with unit info.
sourcepub fn print_check_sat_assuming_with<Idents, Info>(
&mut self,
bool_vars: Idents,
info: Info
) -> Result<FutureCheckSat, Error> where
Info: Copy,
Idents: IntoIterator,
<Idents as IntoIterator>::Item: Sym2Smt<Info>,
pub fn print_check_sat_assuming_with<Idents, Info>(
&mut self,
bool_vars: Idents,
info: Info
) -> Result<FutureCheckSat, Error> where
Info: Copy,
Idents: IntoIterator,
<Idents as IntoIterator>::Item: Sym2Smt<Info>,
Check-sat with assumptions command.
sourceimpl<Parser> Solver<Parser> where
Parser: 'static + Send,
impl<Parser> Solver<Parser> where
Parser: 'static + Send,
sourcepub unsafe fn async_check_sat_or_unk(&mut self) -> CheckSatFuture<'_, Parser>
pub unsafe fn async_check_sat_or_unk(&mut self) -> CheckSatFuture<'_, Parser>
Asynchronous check-sat, see the asynch
module for details.
This function is not unsafe
in the sense that it cannot create undefined behavior.
However, it is unsafe because the asynchronous check might end up running forever in the
background, burning 100% CPU.
sourceimpl<Parser> Solver<Parser>
impl<Parser> Solver<Parser>
sourcepub fn declare_sort(
&mut self,
sort: impl Sort2Smt,
arity: u8
) -> Result<(), Error>
pub fn declare_sort(
&mut self,
sort: impl Sort2Smt,
arity: u8
) -> Result<(), Error>
Declares a new sort.
Examples
let mut solver = Solver::default_z3(()).unwrap();
solver.declare_sort("A", 0).unwrap();
solver.declare_const("x", "A").unwrap();
solver.declare_const("y", "A").unwrap();
solver.declare_fun("f", & [ "A" ], "A").unwrap();
solver.assert("(= (f (f x)) x)").unwrap();
solver.assert("(= (f x) y)").unwrap();
solver.assert("(not (= x y))").unwrap();
let sat = solver.check_sat().unwrap();
sourcepub fn define_sort<Args>(
&mut self,
sort_sym: impl Sym2Smt<()>,
args: Args,
body: impl Sort2Smt
) -> Result<(), Error> where
Args: IntoIterator,
<Args as IntoIterator>::Item: Sort2Smt,
pub fn define_sort<Args>(
&mut self,
sort_sym: impl Sym2Smt<()>,
args: Args,
body: impl Sort2Smt
) -> Result<(), Error> where
Args: IntoIterator,
<Args as IntoIterator>::Item: Sort2Smt,
Defines a new sort.
Examples
Note the use of Self::define_null_sort
to avoid problems with empty arguments.
let mut solver = Solver::default_z3(()).unwrap();
solver.define_sort("MySet", & ["T"], "(Array T Bool)").unwrap();
solver.define_null_sort("IList", "(List Int)").unwrap();
solver.define_sort(
"List-Set", & ["T"], "(Array (List T) Bool)"
).unwrap();
solver.define_null_sort("I", "Int").unwrap();
solver.declare_const("s1", "(MySet I)").unwrap();
solver.declare_const("s2", "(List-Set Int)").unwrap();
solver.declare_const("a", "I").unwrap();
solver.declare_const("l", "IList").unwrap();
solver.assert("(= (select s1 a) true)").unwrap();
solver.assert("(= (select s2 l) false)").unwrap();
let sat = solver.check_sat().unwrap();
sourcepub fn define_null_sort(
&mut self,
sym: impl Sym2Smt<()>,
body: impl Sort2Smt
) -> Result<(), Error>
pub fn define_null_sort(
&mut self,
sym: impl Sym2Smt<()>,
body: impl Sort2Smt
) -> Result<(), Error>
Defines a new nullary sort.
When using Self::define_sort
with empty args
, rust complains because it does not know
what the Arg
type parameter is. This function addresses this problem by not having
arguments.
sourceimpl<Parser> Solver<Parser>
impl<Parser> Solver<Parser>
sourcepub fn declare_const_with<Info>(
&mut self,
symbol: impl Sym2Smt<Info>,
out_sort: impl Sort2Smt,
info: Info
) -> Result<(), Error> where
Info: Copy,
pub fn declare_const_with<Info>(
&mut self,
symbol: impl Sym2Smt<Info>,
out_sort: impl Sort2Smt,
info: Info
) -> Result<(), Error> where
Info: Copy,
Declares a new constant.
sourcepub fn declare_fun_with<Args, Info>(
&mut self,
symbol: impl Sym2Smt<Info>,
args: Args,
out: impl Sort2Smt,
info: Info
) -> Result<(), Error> where
Info: Copy,
Args: IntoIterator,
<Args as IntoIterator>::Item: Sort2Smt,
pub fn declare_fun_with<Args, Info>(
&mut self,
symbol: impl Sym2Smt<Info>,
args: Args,
out: impl Sort2Smt,
info: Info
) -> Result<(), Error> where
Info: Copy,
Args: IntoIterator,
<Args as IntoIterator>::Item: Sort2Smt,
Declares a new function symbol.
sourcepub fn define_const_with<Info>(
&mut self,
symbol: impl Sym2Smt<Info>,
out_sort: impl Sort2Smt,
body: impl Expr2Smt<Info>,
info: Info
) -> Result<(), Error> where
Info: Copy,
pub fn define_const_with<Info>(
&mut self,
symbol: impl Sym2Smt<Info>,
out_sort: impl Sort2Smt,
body: impl Expr2Smt<Info>,
info: Info
) -> Result<(), Error> where
Info: Copy,
Defines a new constant.
sourcepub fn define_fun_with<Args, Info>(
&mut self,
symbol: impl Sym2Smt<Info>,
args: Args,
out: impl Sort2Smt,
body: impl Expr2Smt<Info>,
info: Info
) -> Result<(), Error> where
Info: Copy,
Args: IntoIterator,
<Args as IntoIterator>::Item: SymAndSort<Info>,
pub fn define_fun_with<Args, Info>(
&mut self,
symbol: impl Sym2Smt<Info>,
args: Args,
out: impl Sort2Smt,
body: impl Expr2Smt<Info>,
info: Info
) -> Result<(), Error> where
Info: Copy,
Args: IntoIterator,
<Args as IntoIterator>::Item: SymAndSort<Info>,
Defines a new function symbol.
sourcepub fn define_funs_rec_with<Defs, Info>(
&mut self,
funs: Defs,
info: Info
) -> Result<(), Error> where
Info: Copy,
Defs: IntoIterator + Clone,
<Defs as IntoIterator>::Item: FunDef<Info>,
pub fn define_funs_rec_with<Defs, Info>(
&mut self,
funs: Defs,
info: Info
) -> Result<(), Error> where
Info: Copy,
Defs: IntoIterator + Clone,
<Defs as IntoIterator>::Item: FunDef<Info>,
Defines some new (possibily mutually) recursive functions.
sourcepub fn define_fun_rec_with<Args, Info>(
&mut self,
symbol: impl Sym2Smt<Info>,
args: Args,
out: impl Sort2Smt,
body: impl Expr2Smt<Info>,
info: Info
) -> Result<(), Error> where
Info: Copy,
Args: IntoIterator,
<Args as IntoIterator>::Item: SymAndSort<Info>,
pub fn define_fun_rec_with<Args, Info>(
&mut self,
symbol: impl Sym2Smt<Info>,
args: Args,
out: impl Sort2Smt,
body: impl Expr2Smt<Info>,
info: Info
) -> Result<(), Error> where
Info: Copy,
Args: IntoIterator,
<Args as IntoIterator>::Item: SymAndSort<Info>,
Defines a new recursive function.
sourcepub fn full_assert<Act, Name, Info>(
&mut self,
actlit: Option<Act>,
name: Option<Name>,
expr: impl Expr2Smt<Info>,
info: Info
) -> Result<(), Error> where
Info: Copy,
Name: Sym2Smt<()>,
Act: Sym2Smt<()>,
pub fn full_assert<Act, Name, Info>(
&mut self,
actlit: Option<Act>,
name: Option<Name>,
expr: impl Expr2Smt<Info>,
info: Info
) -> Result<(), Error> where
Info: Copy,
Name: Sym2Smt<()>,
Act: Sym2Smt<()>,
Asserts an expression with info, optional actlit and optional name.
sourcepub fn named_assert_act_with<Info>(
&mut self,
actlit: &Actlit,
name: impl Sym2Smt<()>,
expr: impl Expr2Smt<Info>,
info: Info
) -> Result<(), Error> where
Info: Copy,
pub fn named_assert_act_with<Info>(
&mut self,
actlit: &Actlit,
name: impl Sym2Smt<()>,
expr: impl Expr2Smt<Info>,
info: Info
) -> Result<(), Error> where
Info: Copy,
Asserts an expression with an activation literal, a name and some print info.
sourcepub fn assert_act_with<Info>(
&mut self,
actlit: &Actlit,
expr: impl Expr2Smt<Info>,
info: Info
) -> Result<(), Error> where
Info: Copy,
pub fn assert_act_with<Info>(
&mut self,
actlit: &Actlit,
expr: impl Expr2Smt<Info>,
info: Info
) -> Result<(), Error> where
Info: Copy,
Asserts an expression with some print information, guarded by an activation literal.
See the actlit
module for more details.
sourcepub fn assert_with<Info, Expr>(
&mut self,
expr: Expr,
info: Info
) -> Result<(), Error> where
Info: Copy,
Expr: Expr2Smt<Info>,
pub fn assert_with<Info, Expr>(
&mut self,
expr: Expr,
info: Info
) -> Result<(), Error> where
Info: Copy,
Expr: Expr2Smt<Info>,
Asserts an expression with some print information.
sourcepub fn named_assert<Expr, Name>(
&mut self,
name: Name,
expr: Expr
) -> Result<(), Error> where
Name: Sym2Smt<()>,
Expr: Expr2Smt<()>,
pub fn named_assert<Expr, Name>(
&mut self,
name: Name,
expr: Expr
) -> Result<(), Error> where
Name: Sym2Smt<()>,
Expr: Expr2Smt<()>,
Asserts a named expression.
sourcepub fn named_assert_with<Name, Info, Expr>(
&mut self,
name: Name,
expr: Expr,
info: Info
) -> Result<(), Error> where
Info: Copy,
Expr: Expr2Smt<Info>,
Name: Sym2Smt<()>,
pub fn named_assert_with<Name, Info, Expr>(
&mut self,
name: Name,
expr: Expr,
info: Info
) -> Result<(), Error> where
Info: Copy,
Expr: Expr2Smt<Info>,
Name: Sym2Smt<()>,
Asserts an expression with a name and some print info.
sourcepub fn check_sat_assuming_with<Info, Syms>(
&mut self,
idents: Syms,
info: Info
) -> Result<bool, Error> where
Info: Copy,
Syms: IntoIterator,
<Syms as IntoIterator>::Item: Sym2Smt<Info>,
pub fn check_sat_assuming_with<Info, Syms>(
&mut self,
idents: Syms,
info: Info
) -> Result<bool, Error> where
Info: Copy,
Syms: IntoIterator,
<Syms as IntoIterator>::Item: Sym2Smt<Info>,
Check-sat assuming command, turns unknown
results into errors.
sourcepub fn check_sat_assuming_or_unk_with<Idents, Info>(
&mut self,
idents: Idents,
info: Info
) -> Result<Option<bool>, Error> where
Info: Copy,
Idents: IntoIterator,
<Idents as IntoIterator>::Item: Sym2Smt<Info>,
pub fn check_sat_assuming_or_unk_with<Idents, Info>(
&mut self,
idents: Idents,
info: Info
) -> Result<Option<bool>, Error> where
Info: Copy,
Idents: IntoIterator,
<Idents as IntoIterator>::Item: Sym2Smt<Info>,
Check-sat assuming command, turns unknown
results into None
.
Trait Implementations
sourceimpl<Parser> Read for Solver<Parser>
impl<Parser> Read for Solver<Parser>
sourcefn read(&mut self, buf: &mut [u8]) -> Result<usize, Error>
fn read(&mut self, buf: &mut [u8]) -> Result<usize, Error>
Pull some bytes from this source into the specified buffer, returning how many bytes were read. Read more
1.36.0 · sourcefn read_vectored(&mut self, bufs: &mut [IoSliceMut<'_>]) -> Result<usize, Error>
fn read_vectored(&mut self, bufs: &mut [IoSliceMut<'_>]) -> Result<usize, Error>
Like read
, except that it reads into a slice of buffers. Read more
sourcefn is_read_vectored(&self) -> bool
fn is_read_vectored(&self) -> bool
can_vector
)Determines if this Read
er has an efficient read_vectored
implementation. Read more
1.0.0 · sourcefn read_to_end(&mut self, buf: &mut Vec<u8, Global>) -> Result<usize, Error>
fn read_to_end(&mut self, buf: &mut Vec<u8, Global>) -> Result<usize, Error>
Read all bytes until EOF in this source, placing them into buf
. Read more
1.0.0 · sourcefn read_to_string(&mut self, buf: &mut String) -> Result<usize, Error>
fn read_to_string(&mut self, buf: &mut String) -> Result<usize, Error>
Read all bytes until EOF in this source, appending them to buf
. Read more
1.6.0 · sourcefn read_exact(&mut self, buf: &mut [u8]) -> Result<(), Error>
fn read_exact(&mut self, buf: &mut [u8]) -> Result<(), Error>
Read the exact number of bytes required to fill buf
. Read more
sourcefn read_buf(&mut self, buf: &mut ReadBuf<'_>) -> Result<(), Error>
fn read_buf(&mut self, buf: &mut ReadBuf<'_>) -> Result<(), Error>
read_buf
)Pull some bytes from this source into the specified buffer. Read more
sourcefn read_buf_exact(&mut self, buf: &mut ReadBuf<'_>) -> Result<(), Error>
fn read_buf_exact(&mut self, buf: &mut ReadBuf<'_>) -> Result<(), Error>
read_buf
)Read the exact number of bytes required to fill buf
. Read more
1.0.0 · sourcefn by_ref(&mut self) -> &mut Self
fn by_ref(&mut self) -> &mut Self
Creates a “by reference” adaptor for this instance of Read
. Read more
sourceimpl<Parser> Write for Solver<Parser>
impl<Parser> Write for Solver<Parser>
sourcefn write(&mut self, buf: &[u8]) -> Result<usize, Error>
fn write(&mut self, buf: &[u8]) -> Result<usize, Error>
Write a buffer into this writer, returning how many bytes were written. Read more
sourcefn flush(&mut self) -> Result<(), Error>
fn flush(&mut self) -> Result<(), Error>
Flush this output stream, ensuring that all intermediately buffered contents reach their destination. Read more
sourcefn is_write_vectored(&self) -> bool
fn is_write_vectored(&self) -> bool
can_vector
)Determines if this Write
r has an efficient write_vectored
implementation. Read more
1.0.0 · sourcefn write_all(&mut self, buf: &[u8]) -> Result<(), Error>
fn write_all(&mut self, buf: &[u8]) -> Result<(), Error>
Attempts to write an entire buffer into this writer. Read more
sourcefn write_all_vectored(&mut self, bufs: &mut [IoSlice<'_>]) -> Result<(), Error>
fn write_all_vectored(&mut self, bufs: &mut [IoSlice<'_>]) -> Result<(), Error>
write_all_vectored
)Attempts to write multiple buffers into this writer. Read more
Auto Trait Implementations
impl<Parser> RefUnwindSafe for Solver<Parser> where
Parser: RefUnwindSafe,
impl<Parser> Send for Solver<Parser> where
Parser: Send,
impl<Parser> Sync for Solver<Parser> where
Parser: Sync,
impl<Parser> Unpin for Solver<Parser> where
Parser: Unpin,
impl<Parser> UnwindSafe for Solver<Parser> where
Parser: UnwindSafe,
Blanket Implementations
sourceimpl<T> BorrowMut<T> for T where
T: ?Sized,
impl<T> BorrowMut<T> for T where
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