Struct rsmt2::prelude::Solver

pub struct Solver<Parser> { /* fields omitted */ }

Solver providing most of the SMT-LIB 2.5 commands.

Note the tee function, which takes a file writer to which it will write everything sent to the solver.

Implementations

impl<Parser> Solver<Parser>

Basic functions, not related to SMT-LIB.

pub fn new(conf: SmtConf, parser: Parser) -> SmtRes<Self>

Constructor.

pub fn z3(parser: Parser, cmd: impl Into<String>) -> SmtRes<Self>

Creates a solver kid with the default z3 configuration.

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

pub fn cvc4(parser: Parser, cmd: impl Into<String>) -> SmtRes<Self>

Creates a solver kid with the default cvc4 configuration.

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

pub fn yices_2(parser: Parser, cmd: impl Into<String>) -> SmtRes<Self>

Creates a solver kid with the default yices 2 configuration.

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

pub fn default_z3(parser: Parser) -> SmtRes<Self>

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.

pub fn default_cvc4(parser: Parser) -> SmtRes<Self>

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.

pub fn default_yices_2(parser: Parser) -> SmtRes<Self>

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.

pub fn conf(&self) -> &SmtConf

Returns the configuration of the solver.

pub fn tee(&mut self, file: File) -> SmtRes<()>

Forces the solver to write all communications to a file.

• fails if the solver is already tee-ed;
• see also path_tee.

pub fn path_tee<P>(&mut self, path: P) -> SmtRes<()> where
    P: AsRef<Path>, 

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

pub fn is_teed(&self) -> bool

True if the solver is tee-ed.

pub fn kill(&mut self) -> SmtRes<()>

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.

pub fn comment_args(&mut self, args: Arguments<'_>) -> SmtRes<()>

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

pub fn comment(&mut self, blah: &str) -> SmtRes<()>

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

impl<Parser> Solver<Parser>

Basic SMT-LIB parser-agnostic commands.

pub fn assert<Expr: ?Sized>(&mut self, expr: &Expr) -> SmtRes<()> where
    Expr: Expr2Smt<()>, 

Asserts an expression.

Examples

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

pub fn check_sat(&mut self) -> SmtRes<bool>

Check-sat command, turns unknown results into errors.

See also

• print_check_sat
• parse_check_sat

If you want a more natural way to handle unknown results, see parse_check_sat_or_unk.

Examples

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

pub fn check_sat_or_unk(&mut self) -> SmtRes<Option<bool>>

Check-sat command, turns unknown results in None.

See also

• parse_check_sat_or_unk

Examples

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 }

pub fn reset(&mut self) -> SmtRes<()>

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

pub fn declare_const<Sym: ?Sized, Sort: ?Sized>(
    &mut self,
    symbol: &Sym,
    out_sort: &Sort
) -> SmtRes<()> where
    Sym: Sym2Smt<()>,
    Sort: Sort2Smt, 

Declares a new constant.

Examples

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

pub fn declare_fun<'a, FunSym: ?Sized, ArgSort: ?Sized, Args, OutSort: ?Sized>(
    &mut self,
    symbol: &FunSym,
    args: Args,
    out: &OutSort
) -> SmtRes<()> where
    FunSym: Sym2Smt<()>,
    ArgSort: Sort2Smt + 'a,
    OutSort: Sort2Smt,
    Args: IntoIterator<Item = &'a ArgSort>, 

Declares a new function symbol.

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

pub fn define_const<FunSym: ?Sized, OutSort: ?Sized, Body: ?Sized>(
    &mut self,
    symbol: &FunSym,
    out: &OutSort,
    body: &Body
) -> SmtRes<()> where
    OutSort: Sort2Smt,
    FunSym: Sym2Smt<()>,
    Body: Expr2Smt<()>, 

Defines a new constant function symbol.

Examples

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

pub fn define_fun<'a, FunSym: ?Sized, ArgSym, ArgSort, Args, OutSort: ?Sized, Body: ?Sized>(
    &mut self,
    symbol: &FunSym,
    args: Args,
    out: &OutSort,
    body: &Body
) -> SmtRes<()> where
    ArgSort: Sort2Smt + 'a,
    OutSort: Sort2Smt,
    FunSym: Sym2Smt<()>,
    ArgSym: Sym2Smt<()> + 'a,
    Body: Expr2Smt<()>,
    Args: IntoIterator<Item = &'a (ArgSym, ArgSort)>, 

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

pub fn push(&mut self, n: u8) -> SmtRes<()>

Pushes n layers on the assertion stack.

• see also pop.

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

pub fn pop(&mut self, n: u8) -> SmtRes<()>

Pops n layers off the assertion stack.

• see also push.

pub fn check_sat_assuming<'a, Ident: ?Sized, Idents>(
    &mut self,
    idents: Idents
) -> SmtRes<bool> where
    Ident: Sym2Smt<()> + 'a,
    Idents: IntoIterator<Item = &'a Ident>, 

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

pub fn check_sat_assuming_or_unk<'a, Ident: ?Sized, Idents>(
    &mut self,
    idents: Idents
) -> SmtRes<Option<bool>> where
    Ident: Sym2Smt<()> + 'a,
    Idents: IntoIterator<Item = &'a Ident>, 

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

pub fn set_logic(&mut self, logic: Logic) -> SmtRes<()>

Sets the logic.

Examples

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

pub fn set_custom_logic<Str>(&mut self, logic: Str) -> SmtRes<()> where
    Str: AsRef<str>, 

Sets a custom logic.

Examples

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

pub fn define_fun_rec<'a, FunSym: ?Sized, ArgSym, ArgSort, Args, OutSort: ?Sized, Body: ?Sized>(
    &mut self,
    symbol: &FunSym,
    args: Args,
    out: &OutSort,
    body: &Body
) -> SmtRes<()> where
    ArgSort: Sort2Smt + 'a,
    OutSort: Sort2Smt,
    FunSym: Sym2Smt<()>,
    ArgSym: Sym2Smt<()> + 'a,
    Body: Expr2Smt<()>,
    Args: IntoIterator<Item = &'a (ArgSym, ArgSort)>, 

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

pub fn define_funs_rec<'a, FunSym, ArgSym, ArgSort, Args, ArgsRef, OutSort, Body, Funs>(
    &mut self,
    funs: Funs
) -> SmtRes<()> where
    FunSym: Sym2Smt<()> + 'a,
    ArgSym: Sym2Smt<()> + 'a,
    ArgSort: Sort2Smt + 'a,
    OutSort: Sort2Smt + 'a,
    Body: Expr2Smt<()> + 'a,
    &'a Args: IntoIterator<Item = &'a (ArgSym, ArgSort)> + 'a,
    Args: ?Sized,
    ArgsRef: 'a + AsRef<Args>,
    Funs: IntoIterator<Item = &'a (FunSym, ArgsRef, OutSort, Body)>,
    Funs::IntoIter: Clone, 

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

pub fn declare_datatypes<'a, Sort, Param, ParamList, Def, DefList, All>(
    &mut self,
    defs: All
) -> SmtRes<()> where
    Sort: Sort2Smt + 'a,
    Param: Sort2Smt + 'a,
    &'a ParamList: IntoIterator<Item = &'a Param> + 'a,
    Def: Sort2Smt + 'a,
    &'a DefList: IntoIterator<Item = &'a Def> + 'a,
    All: IntoIterator<Item = &'a (Sort, usize, ParamList, DefList)> + 'a,
    All::IntoIter: Clone, 

Declares mutually recursive datatypes.

A relatively recent version of z3 is recommended.

Examples

let mut solver = Solver::default_z3(()).unwrap();
solver.declare_datatypes( & [
    ( "Tree", 1, ["T"],
        [ "leaf", "(node (value T) (children (TreeList T)))" ] ),
    ( "TreeList", 1, ["T"],
        [ "nil", "(cons (car (Tree T)) (cdr (TreeList T)))" ]),
] ).unwrap();

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 } panic! { "aaa" }

impl<Parser> Solver<Parser>

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

pub fn get_model<Ident, Type, Value>(
    &mut self
) -> SmtRes<Vec<(Ident, Vec<(Ident, Type)>, Type, Value)>> where
    Parser: for<'a> IdentParser<Ident, Type, &'a mut RSmtParser> + for<'a> ModelParser<Ident, Type, Value, &'a mut RSmtParser>, 

Get-model command.

pub fn get_model_const<Ident, Type, Value>(
    &mut self
) -> SmtRes<Vec<(Ident, Type, Value)>> where
    Parser: for<'a> IdentParser<Ident, Type, &'a mut RSmtParser> + for<'a> ModelParser<Ident, Type, Value, &'a mut RSmtParser>, 

Get-model command when all the symbols are nullary.

pub fn get_values<'a, Expr: ?Sized, Exprs, PExpr, PValue>(
    &mut self,
    exprs: Exprs
) -> SmtRes<Vec<(PExpr, PValue)>> where
    Parser: for<'b> ExprParser<PExpr, (), &'b mut RSmtParser> + for<'b> ValueParser<PValue, &'b mut RSmtParser>,
    Expr: Expr2Smt<()> + 'a,
    Exprs: IntoIterator<Item = &'a Expr>, 

Get-values command.

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

impl<Parser> Solver<Parser>

Actlit-Related Functions.

See the actlit module for more details.

pub fn get_actlit(&mut self) -> SmtRes<Actlit>

Introduces a new actlit.

See the actlit module for more details.

pub fn de_actlit(&mut self, actlit: Actlit) -> SmtRes<()>

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

See the actlit module for more details.

pub fn set_actlit(&mut self, actlit: Actlit, b: bool) -> SmtRes<()>

Forces the value of an actlit and consumes it.

See the actlit module for more details.

pub fn assert_act<Expr: ?Sized>(
    &mut self,
    actlit: &Actlit,
    expr: &Expr
) -> SmtRes<()> where
    Expr: Expr2Smt<()>, 

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

See the actlit module for more details.

pub fn check_sat_act<'a, Actlits>(&mut self, actlits: Actlits) -> SmtRes<bool> where
    Actlits: IntoIterator<Item = &'a Actlit>, 

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

pub fn check_sat_act_or_unk<'a, Actlits>(
    &mut self,
    actlits: Actlits
) -> SmtRes<Option<bool>> where
    Actlits: IntoIterator<Item = &'a Actlit>, 

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

impl<Parser> Solver<Parser>

SMT-LIB asynchronous commands.

pub fn print_check_sat(&mut self) -> SmtRes<FutureCheckSat>

Prints a check-sat command.

Allows to print the check-sat and get the result later, e.g. with 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 }

pub fn print_check_sat_act<'a, Actlits>(
    &mut self,
    actlits: Actlits
) -> SmtRes<FutureCheckSat> where
    Actlits: IntoIterator<Item = &'a Actlit>, 

Check-sat command, with actlits.

See the actlit module for more details.

pub fn parse_check_sat(&mut self, _: FutureCheckSat) -> SmtRes<bool>

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

pub fn parse_check_sat_or_unk(
    &mut self,
    _: FutureCheckSat
) -> SmtRes<Option<bool>>

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

pub fn print_check_sat_assuming<'a, Ident: ?Sized, Idents>(
    &mut self,
    bool_vars: Idents
) -> SmtRes<FutureCheckSat> where
    Ident: Sym2Smt<()> + 'a,
    Idents: IntoIterator<Item = &'a Ident>, 

Check-sat with assumptions command with unit info.

pub fn print_check_sat_assuming_with<'a, Info, Ident: ?Sized, Idents>(
    &mut self,
    bool_vars: Idents,
    info: Info
) -> SmtRes<FutureCheckSat> where
    Info: Copy,
    Ident: Sym2Smt<Info> + 'a,
    Idents: IntoIterator<Item = &'a Ident>, 

Check-sat with assumptions command.

impl<Parser: Send + 'static> Solver<Parser>

Non-blocking commands.

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.

impl<Parser> Solver<Parser>

Sort-related SMT-LIB commands.

pub fn declare_sort<Sort: ?Sized>(
    &mut self,
    sort: &Sort,
    arity: u8
) -> SmtRes<()> where
    Sort: Sort2Smt, 

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

pub fn define_sort<'a, Sort: ?Sized, Arg: ?Sized, Args, Body: ?Sized>(
    &mut self,
    sort: &Sort,
    args: Args,
    body: &Body
) -> SmtRes<()> where
    Sort: Sort2Smt,
    Arg: Sort2Smt + 'a,
    Body: Sort2Smt,
    Args: IntoIterator<Item = &'a Arg>, 

Defines a new sort.

Examples

Note the use of 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();

pub fn define_null_sort<Sort: ?Sized, Body: ?Sized>(
    &mut self,
    sort: &Sort,
    body: &Body
) -> SmtRes<()> where
    Sort: Sort2Smt,
    Body: Sort2Smt, 

Defines a new nullary sort.

When using define_sort, rust complains because it does not know what the Arg type parameter is, since the args parameter is empty. So this function can be useful.

This could be fixed with a default type for Arg, like Body for instance, but this is currently not possible in a function.

impl<Parser> Solver<Parser>

SMT-LIB commands vehiculating user information.

pub fn declare_const_with<Info, Sym: ?Sized, Sort: ?Sized>(
    &mut self,
    symbol: &Sym,
    out_sort: &Sort,
    info: Info
) -> SmtRes<()> where
    Info: Copy,
    Sym: Sym2Smt<Info>,
    Sort: Sort2Smt, 

Declares a new constant.

pub fn declare_fun_with<'a, Info, FunSym: ?Sized, ArgSort: ?Sized, Args, OutSort: ?Sized>(
    &mut self,
    symbol: &FunSym,
    args: Args,
    out: &OutSort,
    info: Info
) -> SmtRes<()> where
    Info: Copy,
    FunSym: Sym2Smt<Info>,
    ArgSort: Sort2Smt + 'a,
    OutSort: Sort2Smt,
    Args: IntoIterator<Item = &'a ArgSort>, 

Declares a new function symbol.

pub fn define_const_with<Info, Sym: ?Sized, Sort: ?Sized, Body: ?Sized>(
    &mut self,
    symbol: &Sym,
    out_sort: &Sort,
    body: &Body,
    info: Info
) -> SmtRes<()> where
    Info: Copy,
    Sym: Sym2Smt<Info>,
    Sort: Sort2Smt,
    Body: Expr2Smt<Info>, 

Defines a new constant.

pub fn define_fun_with<'a, Info, FunSym: ?Sized, ArgSym, ArgSort, Args, OutSort: ?Sized, Body: ?Sized>(
    &mut self,
    symbol: &FunSym,
    args: Args,
    out: &OutSort,
    body: &Body,
    info: Info
) -> SmtRes<()> where
    Info: Copy,
    ArgSort: Sort2Smt + 'a,
    OutSort: Sort2Smt,
    FunSym: Sym2Smt<Info>,
    ArgSym: Sym2Smt<Info> + 'a,
    Body: Expr2Smt<Info>,
    Args: IntoIterator<Item = &'a (ArgSym, ArgSort)>, 

Defines a new function symbol.

pub fn define_funs_rec_with<'a, Info, FunSym, ArgSym, ArgSort, Args, ArgsRef, OutSort, Body, Funs>(
    &mut self,
    funs: Funs,
    info: Info
) -> SmtRes<()> where
    Info: Copy,
    FunSym: Sym2Smt<Info> + 'a,
    ArgSym: Sym2Smt<Info> + 'a,
    ArgSort: Sort2Smt + 'a,
    OutSort: Sort2Smt + 'a,
    Body: Expr2Smt<Info> + 'a,
    &'a Args: IntoIterator<Item = &'a (ArgSym, ArgSort)> + 'a,
    Args: ?Sized,
    ArgsRef: 'a + AsRef<Args>,
    Funs: IntoIterator<Item = &'a (FunSym, ArgsRef, OutSort, Body)>,
    Funs::IntoIter: Clone, 

Defines some new (possibily mutually) recursive functions.

pub fn define_fun_rec_with<'a, Info, FunSym: ?Sized, ArgSym, ArgSort, Args, OutSort: ?Sized, Body: ?Sized>(
    &mut self,
    symbol: &FunSym,
    args: Args,
    out: &OutSort,
    body: &Body,
    info: Info
) -> SmtRes<()> where
    Info: Copy,
    ArgSort: Sort2Smt + 'a,
    OutSort: Sort2Smt,
    FunSym: Sym2Smt<Info>,
    ArgSym: Sym2Smt<Info> + 'a,
    Body: Expr2Smt<Info>,
    Args: IntoIterator<Item = &'a (ArgSym, ArgSort)>, 

Defines a new recursive function.

pub fn assert_act_with<Info, Expr: ?Sized>(
    &mut self,
    actlit: &Actlit,
    expr: &Expr,
    info: Info
) -> SmtRes<()> where
    Info: Copy,
    Expr: Expr2Smt<Info>, 

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

See the actlit module for more details.

pub fn assert_with<Info, Expr: ?Sized>(
    &mut self,
    expr: &Expr,
    info: Info
) -> SmtRes<()> where
    Info: Copy,
    Expr: Expr2Smt<Info>, 

Asserts an expression with some print information.

pub fn check_sat_assuming_with<'a, Info, Ident: ?Sized, Idents>(
    &mut self,
    idents: Idents,
    info: Info
) -> SmtRes<bool> where
    Info: Copy,
    Ident: Sym2Smt<Info> + 'a,
    Idents: IntoIterator<Item = &'a Ident>, 

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

pub fn check_sat_assuming_or_unk_with<'a, Info, Ident: ?Sized, Idents>(
    &mut self,
    idents: Idents,
    info: Info
) -> SmtRes<Option<bool>> where
    Info: Copy,
    Ident: Sym2Smt<Info> + 'a,
    Idents: IntoIterator<Item = &'a Ident>, 

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

impl<Parser> Solver<Parser>

Other commands (either untested or not useful right now).

pub fn set_option<Value: Display>(
    &mut self,
    option: &str,
    value: Value
) -> SmtRes<()>

Set option command.

pub fn produce_unsat_core(&mut self) -> SmtRes<()>

Activates unsat core production.

pub fn reset_assertions(&mut self) -> SmtRes<()>

Resets the assertions in the solver.

pub fn get_info(&mut self, flag: &str) -> SmtRes<()>

Get info command.

pub fn get_option(&mut self, option: &str) -> SmtRes<()>

Get option command.

pub fn set_info(&mut self, attribute: &str) -> SmtRes<()>

Set info command.

pub fn echo(&mut self, text: &str) -> SmtRes<()>

Echo command.

Trait Implementations

impl<Parser> Drop for Solver<Parser>

pub fn drop(&mut self)

Executes the destructor for this type.

impl<Parser> Read for Solver<Parser>

pub fn read(&mut self, buf: &mut [u8]) -> Result<usize>

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

pub fn read_vectored(
    &mut self,
    bufs: &mut [IoSliceMut<'_>]
) -> Result<usize, Error>

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

pub fn is_read_vectored(&self) -> bool

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

Determines if this Reader has an efficient read_vectored implementation.

pub unsafe fn initializer(&self) -> Initializer

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

Determines if this Reader can work with buffers of uninitialized memory.

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

pub fn read_to_string(&mut self, buf: &mut String) -> Result<usize, Error>

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

pub fn read_exact(&mut self, buf: &mut [u8]) -> Result<(), Error>

Read the exact number of bytes required to fill buf.

pub fn by_ref(&mut self) -> &mut Self

Creates a "by reference" adaptor for this instance of Read.

pub fn bytes(self) -> Bytes<Self>

Transforms this Read instance to an Iterator over its bytes.

pub fn chain<R>(self, next: R) -> Chain<Self, R> where
    R: Read, 

Creates an adaptor which will chain this stream with another.

pub fn take(self, limit: u64) -> Take<Self>

Creates an adaptor which will read at most limit bytes from it.

impl<Parser> Write for Solver<Parser>

pub fn write(&mut self, buf: &[u8]) -> Result<usize>

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

pub fn flush(&mut self) -> Result<()>

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

pub fn write_vectored(&mut self, bufs: &[IoSlice<'_>]) -> Result<usize, Error>

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

pub fn is_write_vectored(&self) -> bool

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

Determines if this Writer has an efficient write_vectored implementation.

pub fn write_all(&mut self, buf: &[u8]) -> Result<(), Error>

Attempts to write an entire buffer into this writer.

pub fn write_all_vectored(
    &mut self,
    bufs: &mut [IoSlice<'_>]
) -> Result<(), Error>

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

Attempts to write multiple buffers into this writer.

pub fn write_fmt(&mut self, fmt: Arguments<'_>) -> Result<(), Error>

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

pub fn by_ref(&mut self) -> &mut Self

Creates a "by reference" adaptor for this instance of Write.