Struct rsmt2::PlainSolver
[−]
[src]
pub struct PlainSolver<'kid, Parser: Copy> { /* fields omitted */ }
Plain solver, as opposed to TeeSolver
which logs IOs.
Methods
impl<'kid, Parser: Copy> PlainSolver<'kid, Parser>
[src]
fn new(kid: &'kid mut Kid, parser: Parser) -> SmtRes<Self>
[src]
Creates a plain solver.
fn tee(self, file: File) -> TeeSolver<'kid, Parser>
[src]
Wraps a solver to log IOs to a file.
fn conf(&self) -> &SolverConf
[src]
Configuration of the solver.
Trait Implementations
impl<'kid, Parser: Copy> Solver<'kid, Parser> for PlainSolver<'kid, Parser>
[src]
fn reset(&mut self) -> SmtRes<()>
[src]
Resets the underlying solver. Restarts the kid process if no reset command is supported. Read more
fn set_logic(&mut self, logic: Logic) -> SmtRes<()>
[src]
Sets the logic.
fn set_option<Value: Display>(
&mut self,
option: &str,
value: Value
) -> SmtRes<()>
[src]
&mut self,
option: &str,
value: Value
) -> SmtRes<()>
Set option command.
fn interactive_mode(&mut self) -> SmtRes<()>
[src]
Activates interactive mode.
fn print_success(&mut self) -> SmtRes<()>
[src]
Activates print success.
fn produce_unsat_core(&mut self) -> SmtRes<()>
[src]
Activates unsat core production.
fn exit(&mut self) -> SmtRes<()>
[src]
Shuts the solver down.
fn push(&mut self, n: u8) -> SmtRes<()>
[src]
Pushes n
layers on the assertion stack.
fn pop(&mut self, n: u8) -> SmtRes<()>
[src]
Pops n
layers off the assertion stack.
fn reset_assertions(&mut self) -> SmtRes<()>
[src]
Resets the assertions in the solver.
fn get_actlit(&mut self) -> SmtRes<Actlit>
[src]
Introduces a new actlit.
fn de_actlit(&mut self, actlit: Actlit) -> SmtRes<()>
[src]
Deactivates an activation literal, alias for solver.set_actlit(actlit, false)
. Read more
fn set_actlit(&mut self, actlit: Actlit, b: bool) -> SmtRes<()>
[src]
Forces the value of an actlit and consumes it.
fn declare_sort<Sort: Sort2Smt>(
&mut self,
sort: &Sort,
arity: &u8
) -> SmtRes<()>
[src]
&mut self,
sort: &Sort,
arity: &u8
) -> SmtRes<()>
Declares a new sort.
fn define_sort<'a, Sort, Arg, Args, Body>(
&mut self,
sort: &Sort,
args: Args,
body: &Body
) -> SmtRes<()> where
Sort: Sort2Smt,
Arg: Expr2Smt<()> + 'a,
Body: Expr2Smt<()>,
Args: Copy + IntoIterator<Item = &'a Arg>,
[src]
&mut self,
sort: &Sort,
args: Args,
body: &Body
) -> SmtRes<()> where
Sort: Sort2Smt,
Arg: Expr2Smt<()> + 'a,
Body: Expr2Smt<()>,
Args: Copy + IntoIterator<Item = &'a Arg>,
Defines a new sort.
fn define_sort_with<'a, Sort, Info, Arg, Args, Body>(
&mut self,
sort: &Sort,
args: Args,
body: &Body,
info: Info
) -> SmtRes<()> where
Info: Copy,
Sort: Sort2Smt,
Arg: Expr2Smt<Info> + 'a,
Body: Expr2Smt<Info>,
Args: Copy + IntoIterator<Item = &'a Arg>,
[src]
&mut self,
sort: &Sort,
args: Args,
body: &Body,
info: Info
) -> SmtRes<()> where
Info: Copy,
Sort: Sort2Smt,
Arg: Expr2Smt<Info> + 'a,
Body: Expr2Smt<Info>,
Args: Copy + IntoIterator<Item = &'a Arg>,
Defines a new sort.
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: Copy + IntoIterator<Item = &'a ArgSort>,
[src]
&mut self,
symbol: &FunSym,
args: Args,
out: &OutSort
) -> SmtRes<()> where
FunSym: Sym2Smt<()>,
ArgSort: Sort2Smt + 'a,
OutSort: Sort2Smt,
Args: Copy + IntoIterator<Item = &'a ArgSort>,
Declares a new function symbol.
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: Copy + IntoIterator<Item = &'a ArgSort>,
[src]
&mut self,
symbol: &FunSym,
args: Args,
out: &OutSort,
info: Info
) -> SmtRes<()> where
Info: Copy,
FunSym: Sym2Smt<Info>,
ArgSort: Sort2Smt + 'a,
OutSort: Sort2Smt,
Args: Copy + IntoIterator<Item = &'a ArgSort>,
Declares a new function symbol.
fn declare_const<Sym: ?Sized, Sort: ?Sized>(
&mut self,
symbol: &Sym,
out_sort: &Sort
) -> SmtRes<()> where
Sym: Sym2Smt<()>,
Sort: Sort2Smt,
[src]
&mut self,
symbol: &Sym,
out_sort: &Sort
) -> SmtRes<()> where
Sym: Sym2Smt<()>,
Sort: Sort2Smt,
Declares a new constant.
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,
[src]
&mut self,
symbol: &Sym,
out_sort: &Sort,
info: Info
) -> SmtRes<()> where
Info: Copy,
Sym: Sym2Smt<Info>,
Sort: Sort2Smt,
Declares a new constant.
fn define_fun<'a, FunSym, ArgSym, ArgSort, Args, OutSort, Body>(
&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: Copy + IntoIterator<Item = &'a (ArgSym, ArgSort)>,
[src]
&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: Copy + IntoIterator<Item = &'a (ArgSym, ArgSort)>,
Defines a new function symbol.
fn define_fun_with<'a, Info, FunSym, ArgSym, ArgSort, Args, OutSort, Body>(
&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: Copy + IntoIterator<Item = &'a (ArgSym, ArgSort)>,
[src]
&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: Copy + IntoIterator<Item = &'a (ArgSym, ArgSort)>,
Defines a new function symbol.
fn define_funs_rec<'a, FunSym, ArgSym, ArgSort, Args, 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,
Funs: Copy + IntoIterator<Item = &'a (FunSym, Args, OutSort, Body)>,
[src]
&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,
Funs: Copy + IntoIterator<Item = &'a (FunSym, Args, OutSort, Body)>,
Defines some new (possibily mutually) recursive functions.
fn define_funs_rec_with<'a, Info, FunSym, ArgSym, ArgSort, Args, 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,
Funs: Copy + IntoIterator<Item = &'a (FunSym, Args, OutSort, Body)>,
[src]
&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,
Funs: Copy + IntoIterator<Item = &'a (FunSym, Args, OutSort, Body)>,
Defines some new (possibily mutually) recursive functions.
fn define_fun_rec<'a, FunSym, ArgSym, ArgSort, Args, OutSort, Body>(
&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: Copy + IntoIterator<Item = &'a (ArgSym, ArgSort)>,
[src]
&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: Copy + IntoIterator<Item = &'a (ArgSym, ArgSort)>,
Defines a new recursive function.
fn define_fun_rec_with<'a, Info, FunSym, ArgSym, ArgSort, Args, OutSort, Body>(
&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: Copy + IntoIterator<Item = &'a (ArgSym, ArgSort)>,
[src]
&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: Copy + IntoIterator<Item = &'a (ArgSym, ArgSort)>,
Defines a new recursive function.
fn assert<Expr: ?Sized>(&mut self, expr: &Expr) -> SmtRes<()> where
Expr: Expr2Smt<()>,
[src]
Expr: Expr2Smt<()>,
Asserts an expression without print information.
fn assert_act<Expr: ?Sized>(
&mut self,
actlit: &Actlit,
expr: &Expr
) -> SmtRes<()> where
Expr: Expr2Smt<()>,
[src]
&mut self,
actlit: &Actlit,
expr: &Expr
) -> SmtRes<()> where
Expr: Expr2Smt<()>,
Asserts an expression without print information, guarded by an activation literal. Read more
fn assert_with<Info, Expr: ?Sized>(
&mut self,
expr: &Expr,
info: Info
) -> SmtRes<()> where
Info: Copy,
Expr: Expr2Smt<Info>,
[src]
&mut self,
expr: &Expr,
info: Info
) -> SmtRes<()> where
Info: Copy,
Expr: Expr2Smt<Info>,
Asserts an expression with some print information.
fn assert_act_with<Info, Expr: ?Sized>(
&mut self,
actlit: &Actlit,
expr: &Expr,
info: Info
) -> SmtRes<()> where
Info: Copy,
Expr: Expr2Smt<Info>,
[src]
&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. Read more
fn get_info(&mut self, flag: &str) -> SmtRes<()>
[src]
Get info command.
fn get_option(&mut self, option: &str) -> SmtRes<()>
[src]
Get option command.
fn set_info(&mut self, attribute: &str) -> SmtRes<()>
[src]
Set info command.
fn echo(&mut self, text: &str) -> SmtRes<()>
[src]
Echo command.
fn print_check_sat(&mut self) -> SmtRes<()>
[src]
Check-sat command.
fn print_check_sat_act<'a, Actlits>(&mut self, actlits: Actlits) -> SmtRes<()> where
Actlits: Copy + IntoIterator<Item = &'a Actlit>,
[src]
Actlits: Copy + IntoIterator<Item = &'a Actlit>,
Check-sat command, with actlits.
fn print_get_model(&mut self) -> SmtRes<()>
[src]
Get-model command.
fn parse_get_model<Ident, Type, Value>(
&mut self
) -> SmtRes<Vec<(Ident, Vec<Type>, Type, Value)>> where
Parser: for<'a> IdentParser<Ident, Type, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
[src]
&mut self
) -> SmtRes<Vec<(Ident, Vec<Type>, Type, Value)>> where
Parser: for<'a> IdentParser<Ident, Type, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
Parse the result of a get-model.
fn get_model<Ident, Type, Value>(
&mut self
) -> SmtRes<Vec<(Ident, Vec<Type>, Type, Value)>> where
Parser: for<'a> IdentParser<Ident, Type, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
[src]
&mut self
) -> SmtRes<Vec<(Ident, Vec<Type>, Type, Value)>> where
Parser: for<'a> IdentParser<Ident, Type, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
Get-model command.
fn parse_get_model_const<Ident, Type, Value>(
&mut self
) -> SmtRes<Vec<(Ident, Type, Value)>> where
Parser: for<'a> IdentParser<Ident, Type, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
[src]
&mut self
) -> SmtRes<Vec<(Ident, Type, Value)>> where
Parser: for<'a> IdentParser<Ident, Type, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
Parse the result of a get-model where all the symbols are nullary.
fn get_model_const<Ident, Type, Value>(
&mut self
) -> SmtRes<Vec<(Ident, Type, Value)>> where
Parser: for<'a> IdentParser<Ident, Type, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
[src]
&mut self
) -> SmtRes<Vec<(Ident, Type, Value)>> where
Parser: for<'a> IdentParser<Ident, Type, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
Get-model command when all the symbols are nullary.
fn parse_success(&mut self) -> SmtRes<()>
[src]
Parse success.
fn parse_check_sat(&mut self) -> SmtRes<bool>
[src]
Parse the result of a check-sat, turns unknown
results into errors.
fn parse_check_sat_or_unknown(&mut self) -> SmtRes<Option<bool>>
[src]
Parse the result of a check-sat, turns unknown
results into None
.
fn check_sat(&mut self) -> SmtRes<bool>
[src]
Check-sat command, turns unknown
results into errors.
fn check_sat_act<'a, Actlits>(&mut self, actlits: Actlits) -> SmtRes<bool> where
Actlits: Copy + IntoIterator<Item = &'a Actlit>,
[src]
Actlits: Copy + IntoIterator<Item = &'a Actlit>,
Check-sat command with activation literals, turns unknown
results into errors. Read more
fn check_sat_or_unknown(&mut self) -> SmtRes<Option<bool>>
[src]
Check-sat command, turns unknown
results in None
.
fn check_sat_act_or_unknown<'a, Actlits>(
&mut self,
actlits: Actlits
) -> SmtRes<Option<bool>> where
Actlits: Copy + IntoIterator<Item = &'a Actlit>,
[src]
&mut self,
actlits: Actlits
) -> SmtRes<Option<bool>> where
Actlits: Copy + IntoIterator<Item = &'a Actlit>,
Check-sat command with activation literals, turns unknown
results in None
. Read more
fn print_get_assertions(&mut self) -> SmtRes<()>
[src]
Get-assertions command.
fn print_get_assignment(&mut self) -> SmtRes<()>
[src]
Get-assignment command.
fn print_get_unsat_assumptions(&mut self) -> SmtRes<()>
[src]
Get-unsat-assumptions command.
fn print_get_proof(&mut self) -> SmtRes<()>
[src]
Get-proof command.
fn print_get_unsat_core(&mut self) -> SmtRes<()>
[src]
Get-unsat-core command.
fn print_get_values<'a, Expr: ?Sized, Exprs>(
&mut self,
exprs: Exprs
) -> SmtRes<()> where
Expr: Expr2Smt<()> + 'a,
Exprs: Clone + IntoIterator<Item = &'a Expr>,
[src]
&mut self,
exprs: Exprs
) -> SmtRes<()> where
Expr: Expr2Smt<()> + 'a,
Exprs: Clone + IntoIterator<Item = &'a Expr>,
Get-values command.
fn print_get_values_with<'a, Info, Expr: ?Sized, Exprs>(
&mut self,
exprs: Exprs,
info: Info
) -> SmtRes<()> where
Info: Copy,
Expr: Expr2Smt<Info> + 'a,
Exprs: Clone + IntoIterator<Item = &'a Expr>,
[src]
&mut self,
exprs: Exprs,
info: Info
) -> SmtRes<()> where
Info: Copy,
Expr: Expr2Smt<Info> + 'a,
Exprs: Clone + IntoIterator<Item = &'a Expr>,
Get-values command.
fn parse_get_values<Expr, Value>(&mut self) -> SmtRes<Vec<(Expr, Value)>> where
Parser: for<'a> ExprParser<Expr, (), &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
[src]
Parser: for<'a> ExprParser<Expr, (), &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
Parse the result of a get-values.
fn parse_get_values_with<Info, Expr, Value>(
&mut self,
info: Info
) -> SmtRes<Vec<(Expr, Value)>> where
Info: Copy,
Parser: for<'a> ExprParser<Expr, Info, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
[src]
&mut self,
info: Info
) -> SmtRes<Vec<(Expr, Value)>> where
Info: Copy,
Parser: for<'a> ExprParser<Expr, Info, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
Parse the result of a get-values.
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 SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'b> ValueParser<PValue, &'b mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
Expr: Expr2Smt<()> + 'a,
Exprs: Copy + IntoIterator<Item = &'a Expr>,
[src]
&mut self,
exprs: Exprs
) -> SmtRes<Vec<(PExpr, PValue)>> where
Parser: for<'b> ExprParser<PExpr, (), &'b mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'b> ValueParser<PValue, &'b mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
Expr: Expr2Smt<()> + 'a,
Exprs: Copy + IntoIterator<Item = &'a Expr>,
Get-values command. Read more
fn get_values_with<'a, Info, Expr: ?Sized, Exprs, PExpr, PValue>(
&mut self,
exprs: Exprs,
info: Info
) -> SmtRes<Vec<(PExpr, PValue)>> where
Info: Copy,
Parser: for<'b> ExprParser<PExpr, Info, &'b mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'b> ValueParser<PValue, &'b mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
Expr: Expr2Smt<Info> + 'a,
Exprs: Copy + IntoIterator<Item = &'a Expr>,
[src]
&mut self,
exprs: Exprs,
info: Info
) -> SmtRes<Vec<(PExpr, PValue)>> where
Info: Copy,
Parser: for<'b> ExprParser<PExpr, Info, &'b mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'b> ValueParser<PValue, &'b mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
Expr: Expr2Smt<Info> + 'a,
Exprs: Copy + IntoIterator<Item = &'a Expr>,
Get-values command. Read more
fn print_check_sat_assuming<'a, Ident: ?Sized, Idents>(
&mut self,
bool_vars: Idents
) -> SmtRes<()> where
Ident: Sym2Smt<()> + 'a,
Idents: Copy + IntoIterator<Item = &'a Ident>,
[src]
&mut self,
bool_vars: Idents
) -> SmtRes<()> where
Ident: Sym2Smt<()> + 'a,
Idents: Copy + IntoIterator<Item = &'a Ident>,
Check-sat with assumptions command with unit info.
fn print_check_sat_assuming_with<'a, Info, Ident: ?Sized, Idents>(
&mut self,
bool_vars: Idents,
info: Info
) -> SmtRes<()> where
Info: Copy,
Ident: Sym2Smt<Info> + 'a,
Idents: Copy + IntoIterator<Item = &'a Ident>,
[src]
&mut self,
bool_vars: Idents,
info: Info
) -> SmtRes<()> where
Info: Copy,
Ident: Sym2Smt<Info> + 'a,
Idents: Copy + IntoIterator<Item = &'a Ident>,
Check-sat with assumptions command.
fn check_sat_assuming<'a, Ident: ?Sized, Idents>(
&mut self,
idents: Idents
) -> SmtRes<bool> where
Ident: Sym2Smt<()> + 'a,
Idents: Copy + IntoIterator<Item = &'a Ident>,
[src]
&mut self,
idents: Idents
) -> SmtRes<bool> where
Ident: Sym2Smt<()> + 'a,
Idents: Copy + IntoIterator<Item = &'a Ident>,
Check-sat assuming command, turns unknown
results into errors.
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: Copy + IntoIterator<Item = &'a Ident>,
[src]
&mut self,
idents: Idents,
info: Info
) -> SmtRes<bool> where
Info: Copy,
Ident: Sym2Smt<Info> + 'a,
Idents: Copy + IntoIterator<Item = &'a Ident>,
Check-sat assuming command, turns unknown
results into errors.
fn check_sat_assuming_or_unknown_u<'a, Ident: ?Sized, Idents>(
&mut self,
idents: Idents
) -> SmtRes<Option<bool>> where
Ident: Sym2Smt<()> + 'a,
Idents: Copy + IntoIterator<Item = &'a Ident>,
[src]
&mut self,
idents: Idents
) -> SmtRes<Option<bool>> where
Ident: Sym2Smt<()> + 'a,
Idents: Copy + IntoIterator<Item = &'a Ident>,
Check-sat assuming command, turns unknown
results into None
.
fn check_sat_assuming_or_unknown<'a, Info, Ident: ?Sized, Idents>(
&mut self,
idents: Idents,
info: Info
) -> SmtRes<Option<bool>> where
Info: Copy,
Ident: Sym2Smt<Info> + 'a,
Idents: Copy + IntoIterator<Item = &'a Ident>,
[src]
&mut self,
idents: Idents,
info: Info
) -> SmtRes<Option<bool>> where
Info: Copy,
Ident: Sym2Smt<Info> + 'a,
Idents: Copy + IntoIterator<Item = &'a Ident>,
Check-sat assuming command, turns unknown
results into None
.