Trait rsmt2::Solver
[−]
[src]
pub trait Solver<'kid, Parser: Copy>: SolverBasic<'kid, Parser> { fn reset(&mut self) -> SmtRes<()> { ... } fn set_logic(&mut self, logic: Logic) -> SmtRes<()> { ... } fn set_option<Value: Display>(
&mut self,
option: &str,
value: Value
) -> SmtRes<()> { ... } fn interactive_mode(&mut self) -> SmtRes<()> { ... } fn print_success(&mut self) -> SmtRes<()> { ... } fn produce_unsat_core(&mut self) -> SmtRes<()> { ... } fn exit(&mut self) -> SmtRes<()> { ... } fn push(&mut self, n: u8) -> SmtRes<()> { ... } fn pop(&mut self, n: u8) -> SmtRes<()> { ... } fn reset_assertions(&mut self) -> SmtRes<()> { ... } fn get_actlit(&mut self) -> SmtRes<Actlit> { ... } fn de_actlit(&mut self, actlit: Actlit) -> SmtRes<()> { ... } fn set_actlit(&mut self, actlit: Actlit, b: bool) -> SmtRes<()> { ... } fn declare_sort<Sort: Sort2Smt>(
&mut self,
sort: &Sort,
arity: &u8
) -> SmtRes<()> { ... } 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>, { ... } 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>, { ... } 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>, { ... } 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>, { ... } fn declare_const<Sym: ?Sized, Sort: ?Sized>(
&mut self,
symbol: &Sym,
out_sort: &Sort
) -> SmtRes<()>
where
Sym: Sym2Smt<()>,
Sort: Sort2Smt, { ... } 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, { ... } 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)>, { ... } 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)>, { ... } 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)>, { ... } 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)>, { ... } 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)>, { ... } 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)>, { ... } fn assert<Expr: ?Sized>(&mut self, expr: &Expr) -> SmtRes<()>
where
Expr: Expr2Smt<()>, { ... } fn assert_act<Expr: ?Sized>(
&mut self,
actlit: &Actlit,
expr: &Expr
) -> SmtRes<()>
where
Expr: Expr2Smt<()>, { ... } fn assert_with<Info, Expr: ?Sized>(
&mut self,
expr: &Expr,
info: Info
) -> SmtRes<()>
where
Info: Copy,
Expr: Expr2Smt<Info>, { ... } fn assert_act_with<Info, Expr: ?Sized>(
&mut self,
actlit: &Actlit,
expr: &Expr,
info: Info
) -> SmtRes<()>
where
Info: Copy,
Expr: Expr2Smt<Info>, { ... } fn get_info(&mut self, flag: &str) -> SmtRes<()> { ... } fn get_option(&mut self, option: &str) -> SmtRes<()> { ... } fn set_info(&mut self, attribute: &str) -> SmtRes<()> { ... } fn echo(&mut self, text: &str) -> SmtRes<()> { ... } fn print_check_sat(&mut self) -> SmtRes<()> { ... } fn print_check_sat_act<'a, Actlits>(
&mut self,
actlits: Actlits
) -> SmtRes<()>
where
Actlits: Copy + IntoIterator<Item = &'a Actlit>, { ... } fn print_get_model(&mut self) -> SmtRes<()> { ... } 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>>>, { ... } 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>>>, { ... } 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>>>, { ... } 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>>>, { ... } fn parse_success(&mut self) -> SmtRes<()> { ... } fn parse_check_sat(&mut self) -> SmtRes<bool> { ... } fn parse_check_sat_or_unknown(&mut self) -> SmtRes<Option<bool>> { ... } fn check_sat(&mut self) -> SmtRes<bool> { ... } fn check_sat_act<'a, Actlits>(&mut self, actlits: Actlits) -> SmtRes<bool>
where
Actlits: Copy + IntoIterator<Item = &'a Actlit>, { ... } fn check_sat_or_unknown(&mut self) -> SmtRes<Option<bool>> { ... } fn check_sat_act_or_unknown<'a, Actlits>(
&mut self,
actlits: Actlits
) -> SmtRes<Option<bool>>
where
Actlits: Copy + IntoIterator<Item = &'a Actlit>, { ... } fn print_get_assertions(&mut self) -> SmtRes<()> { ... } fn print_get_assignment(&mut self) -> SmtRes<()> { ... } fn print_get_unsat_assumptions(&mut self) -> SmtRes<()> { ... } fn print_get_proof(&mut self) -> SmtRes<()> { ... } fn print_get_unsat_core(&mut self) -> SmtRes<()> { ... } fn print_get_values<'a, Expr: ?Sized, Exprs>(
&mut self,
exprs: Exprs
) -> SmtRes<()>
where
Expr: Expr2Smt<()> + 'a,
Exprs: Clone + IntoIterator<Item = &'a Expr>, { ... } 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>, { ... } 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>>>, { ... } 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>>>, { ... } 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>, { ... } 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>, { ... } 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>, { ... } 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>, { ... } fn check_sat_assuming<'a, Ident: ?Sized, Idents>(
&mut self,
idents: Idents
) -> SmtRes<bool>
where
Ident: Sym2Smt<()> + 'a,
Idents: Copy + IntoIterator<Item = &'a Ident>, { ... } 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>, { ... } 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>, { ... } 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>, { ... } }
Provides SMT-LIB commands.
Provided Methods
fn reset(&mut self) -> SmtRes<()>
Resets the underlying solver. Restarts the kid process if no reset command is supported.
fn set_logic(&mut self, logic: Logic) -> SmtRes<()>
Sets the logic.
fn set_option<Value: Display>(
&mut self,
option: &str,
value: Value
) -> SmtRes<()>
&mut self,
option: &str,
value: Value
) -> SmtRes<()>
Set option command.
fn interactive_mode(&mut self) -> SmtRes<()>
Activates interactive mode.
fn print_success(&mut self) -> SmtRes<()>
Activates print success.
fn produce_unsat_core(&mut self) -> SmtRes<()>
Activates unsat core production.
fn exit(&mut self) -> SmtRes<()>
Shuts the solver down.
fn push(&mut self, n: u8) -> SmtRes<()>
Pushes n
layers on the assertion stack.
fn pop(&mut self, n: u8) -> SmtRes<()>
Pops n
layers off the assertion stack.
fn reset_assertions(&mut self) -> SmtRes<()>
Resets the assertions in the solver.
fn get_actlit(&mut self) -> SmtRes<Actlit>
Introduces a new actlit.
fn de_actlit(&mut self, actlit: Actlit) -> SmtRes<()>
Deactivates an activation literal, alias for
solver.set_actlit(actlit, false)
.
fn set_actlit(&mut self, actlit: Actlit, b: bool) -> SmtRes<()>
Forces the value of an actlit and consumes it.
fn declare_sort<Sort: Sort2Smt>(
&mut self,
sort: &Sort,
arity: &u8
) -> SmtRes<()>
&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>,
&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>,
&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>,
&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>,
&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,
&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,
&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)>,
&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)>,
&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)>,
&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)>,
&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)>,
&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)>,
&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<()>,
Expr: Expr2Smt<()>,
Asserts an expression without print information.
fn assert_act<Expr: ?Sized>(
&mut self,
actlit: &Actlit,
expr: &Expr
) -> SmtRes<()> where
Expr: Expr2Smt<()>,
&mut self,
actlit: &Actlit,
expr: &Expr
) -> SmtRes<()> where
Expr: Expr2Smt<()>,
Asserts an expression without print information, guarded by an activation literal.
fn assert_with<Info, Expr: ?Sized>(
&mut self,
expr: &Expr,
info: Info
) -> SmtRes<()> where
Info: Copy,
Expr: Expr2Smt<Info>,
&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>,
&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.
fn get_info(&mut self, flag: &str) -> SmtRes<()>
Get info command.
fn get_option(&mut self, option: &str) -> SmtRes<()>
Get option command.
fn set_info(&mut self, attribute: &str) -> SmtRes<()>
Set info command.
fn echo(&mut self, text: &str) -> SmtRes<()>
Echo command.
fn print_check_sat(&mut self) -> SmtRes<()>
Check-sat command.
fn print_check_sat_act<'a, Actlits>(&mut self, actlits: Actlits) -> SmtRes<()> where
Actlits: Copy + IntoIterator<Item = &'a Actlit>,
Actlits: Copy + IntoIterator<Item = &'a Actlit>,
Check-sat command, with actlits.
fn print_get_model(&mut self) -> SmtRes<()>
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>>>,
&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>>>,
&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>>>,
&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>>>,
&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<()>
Parse success.
fn parse_check_sat(&mut self) -> SmtRes<bool>
Parse the result of a check-sat, turns unknown
results into errors.
fn parse_check_sat_or_unknown(&mut self) -> SmtRes<Option<bool>>
Parse the result of a check-sat, turns unknown
results into None
.
fn check_sat(&mut self) -> SmtRes<bool>
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>,
Actlits: Copy + IntoIterator<Item = &'a Actlit>,
Check-sat command with activation literals, turns unknown
results into
errors.
fn check_sat_or_unknown(&mut self) -> SmtRes<Option<bool>>
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>,
&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
.
fn print_get_assertions(&mut self) -> SmtRes<()>
Get-assertions command.
fn print_get_assignment(&mut self) -> SmtRes<()>
Get-assignment command.
fn print_get_unsat_assumptions(&mut self) -> SmtRes<()>
Get-unsat-assumptions command.
fn print_get_proof(&mut self) -> SmtRes<()>
Get-proof command.
fn print_get_unsat_core(&mut self) -> SmtRes<()>
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>,
&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>,
&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>>>,
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>>>,
&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>,
&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.
Notice that the input expression type and the output one have no reason to be the same.
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>,
&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.
Notice that the input expression type and the output one have no reason to be the same.
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>,
&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>,
&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>,
&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>,
&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>,
&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>,
&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
.
Implementors
impl<'kid, Parser: Copy> Solver<'kid, Parser> for PlainSolver<'kid, Parser>
impl<'kid, Parser: Copy> Solver<'kid, Parser> for TeeSolver<'kid, Parser>