Struct rsmt2::Solver

source · [−]
pub struct Solver<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();
//               vvvvvvvvvvvvvvvvvvvvvv~~~~ probably gonna cause an error
solver.assert(r#"(> "not an integer" 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 25: \
        Sort mismatch at argument #1 for function (declare-fun > (Int Int) Bool) \
        supplied sort is String\"\
    ",
);

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();

//                         vvvvvvvvvvvvvvvvvvvvvv~~~~ probably gonna cause an error
let res = solver.assert(r#"(> "not an integer" 7)"#);
// did it?
let e = res.unwrap_err();
assert_eq!(
    &e.to_string(),
    "\
        solver error: \"line 4 column 25: \
        Sort mismatch at argument #1 for function (declare-fun > (Int Int) Bool) \
        supplied sort is String\"\
    ",
);
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();

//                         vvvvvvvvvvvvvvvvvvvvvv~~~~ probably gonna cause an error
let res = solver.assert(r#"(> "not an integer" 7)"#);
// did it?
let e = res.unwrap_err();
assert_eq!(
    &e.to_string(),
    "\
        solver error: \"line 4 column 25: \
        Sort mismatch at argument #1 for function (declare-fun > (Int Int) Bool) \
        supplied sort is String\"\
    ",
);

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

Constructor.

Creates a solver kid with the default z3 configuration.

Mostly used in tests, same as Self::new( SmtConf::z3(), parser ).

Creates a solver kid with the default cvc4 configuration.

Mostly used in tests, same as Self::new( SmtConf::z3(), parser ).

Creates a solver kid with the default yices 2 configuration.

Mostly used in tests, same as Self::new( SmtConf::yices_2(), parser ).

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.

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.

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.

Returns the configuration of the solver.

Forces the solver to write all communications to a file.

Forces the solver to write all communications to a file.

  • opens file with create and write;
  • fails if the solver is already tee-ed;
  • see also Self::tee.

True if the solver is tee-ed.

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.

Prints a comment in the tee-ed file, if any.

Prints a comment in the tee-ed file, if any (string version).

Basic SMT-LIB parser-agnostic commands.

Activates print-success, see here.

Parses a success, see here.

Activates unsat core production.

Activates model production.

Asserts an expression.

Examples
let mut solver = Solver::default_z3(()).unwrap();
solver.assert("(= 0 1)").unwrap();

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),
}

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 }

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());

Declares a new constant.

Examples
let mut solver = Solver::default_z3(()).unwrap();
solver.declare_const("x", "Int").unwrap()

Declares a new function symbol.

let mut solver = Solver::default_z3(()).unwrap();
solver.declare_fun(
    "my_symbol", & [ "Int", "Real", "Bool" ], "Bool"
).unwrap()

Defines a new constant function symbol.

Examples
let mut solver = Solver::default_z3(()).unwrap();
solver.define_const(
    "seven", "Int", "7"
).unwrap()

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

Pushes n layers on the assertion stack.

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

Pops n layers off the assertion stack.

Note that using actlits is more efficient than push/pop, and is useable for most push/pop use-cases.

Check-sat assuming command, turns unknown results into errors.

Check-sat assuming command, turns unknown results into None.

Sets the logic.

Examples
let mut solver = Solver::default_z3(()).unwrap();
solver.set_logic( ::rsmt2::Logic::QF_UF ).unwrap();

Sets a custom logic.

Examples
let mut solver = Solver::default_z3(()).unwrap();
solver.set_custom_logic("QF_UFBV").unwrap();

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

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

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

Basic SMT-LIB commands using the user’s parser.

Get-model command.

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)

Get-model command when all the symbols are nullary.

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)

Get-values command.

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

Get-values command.

Notice that the input expression type and the output one have no reason to be the same.

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]);

Get-interpolant command.

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, and
  • I only mentions variables (constant symbols) that appear in both f_1 and f_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 0) 2) 1) (<= n 7))");

See the actlit module for more details.

Introduces a new actlit.

See the actlit module for more details.

Deactivates an activation literal, alias for solver.set_actlit(actlit, false).

See the actlit module for more details.

Forces the value of an actlit and consumes it.

See the actlit module for more details.

Asserts an expression without print information, guarded by an activation literal.

See the actlit module for more details.

Check-sat command with activation literals, turns unknown results into errors.

Check-sat command with activation literals, turns unknown results in None.

SMT-LIB asynchronous commands.

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

Check-sat command, with actlits.

See the actlit module for more details.

Parse the result of a check-sat, turns unknown results into errors.

Parse the result of a check-sat, turns unknown results into None.

Get-interpolant command.

At the time of writing, only Z3 supports this command.

Check-sat with assumptions command with unit info.

Check-sat with assumptions command.

Non-blocking commands.

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.

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();

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();

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.

SMT-LIB commands vehiculating user information.

Declares a new constant.

Declares a new function symbol.

Defines a new constant.

Defines a new function symbol.

Defines some new (possibily mutually) recursive functions.

Defines a new recursive function.

Asserts an expression with info, optional actlit and optional name.

Asserts an expression with an activation literal, a name and some print info.

Asserts an expression with some print information, guarded by an activation literal.

See the actlit module for more details.

Asserts an expression with some print information.

Asserts a named expression.

Asserts an expression with a name and some print info.

Check-sat assuming command, turns unknown results into errors.

Check-sat assuming command, turns unknown results into None.

Other commands.

Set option command.

Resets the assertions in the solver.

Get info command.

Get option command.

Set info command.

Echo command.

Trait Implementations

Executes the destructor for this type. Read more

Pull some bytes from this source into the specified buffer, returning how many bytes were read. Read more

Like read, except that it reads into a slice of buffers. Read more

🔬This is a nightly-only experimental API. (can_vector)

Determines if this Reader has an efficient read_vectored implementation. Read more

Read all bytes until EOF in this source, placing them into buf. Read more

Read all bytes until EOF in this source, appending them to buf. Read more

Read the exact number of bytes required to fill buf. Read more

🔬This is a nightly-only experimental API. (read_buf)

Pull some bytes from this source into the specified buffer. Read more

🔬This is a nightly-only experimental API. (read_buf)

Read the exact number of bytes required to fill cursor. Read more

Creates a “by reference” adaptor for this instance of Read. Read more

Transforms this Read instance to an Iterator over its bytes. Read more

Creates an adapter which will chain this stream with another. Read more

Creates an adapter which will read at most limit bytes from it. Read more

Write a buffer into this writer, returning how many bytes were written. Read more

Flush this output stream, ensuring that all intermediately buffered contents reach their destination. Read more

Like write, except that it writes from a slice of buffers. Read more

🔬This is a nightly-only experimental API. (can_vector)

Determines if this Writer has an efficient write_vectored implementation. Read more

Attempts to write an entire buffer into this writer. Read more

🔬This is a nightly-only experimental API. (write_all_vectored)

Attempts to write multiple buffers into this writer. Read more

Writes a formatted string into this writer, returning any error encountered. Read more

Creates a “by reference” adapter for this instance of Write. Read more

Auto Trait Implementations

Blanket Implementations

Gets the TypeId of self. Read more

Immutably borrows from an owned value. Read more

Mutably borrows from an owned value. Read more

Returns the argument unchanged.

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

The type returned in the event of a conversion error.

Performs the conversion.

The type returned in the event of a conversion error.

Performs the conversion.