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 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, I, Arg, Args: ?Sized, Body>(
&mut self,
sort: &Sort,
args: &'a Args,
body: &Body,
info: &I
) -> SmtRes<()> where
Sort: Sort2Smt,
Arg: Expr2Smt<I> + 'a,
Body: Expr2Smt<I>,
&'a Args: IntoIterator<Item = &'a Arg>,
[src]
&mut self,
sort: &Sort,
args: &'a Args,
body: &Body,
info: &I
) -> SmtRes<()> where
Sort: Sort2Smt,
Arg: Expr2Smt<I> + 'a,
Body: Expr2Smt<I>,
&'a Args: IntoIterator<Item = &'a Arg>,
Defines a new sort.
fn declare_fun<'a, FunSym: ?Sized, ArgSort: ?Sized, Args: ?Sized, I, OutSort: ?Sized>(
&mut self,
symbol: &FunSym,
args: &'a Args,
out: &OutSort,
info: &I
) -> SmtRes<()> where
FunSym: Sym2Smt<I>,
ArgSort: Sort2Smt + 'a,
OutSort: Sort2Smt,
&'a Args: IntoIterator<Item = &'a ArgSort>,
[src]
&mut self,
symbol: &FunSym,
args: &'a Args,
out: &OutSort,
info: &I
) -> SmtRes<()> where
FunSym: Sym2Smt<I>,
ArgSort: Sort2Smt + 'a,
OutSort: Sort2Smt,
&'a Args: IntoIterator<Item = &'a ArgSort>,
Declares a new function symbol.
fn declare_const<Sym: Sym2Smt<I>, Sort: Sort2Smt, I>(
&mut self,
symbol: &Sym,
out_sort: &Sort,
info: &I
) -> SmtRes<()>
[src]
&mut self,
symbol: &Sym,
out_sort: &Sort,
info: &I
) -> SmtRes<()>
Declares a new constant.
fn define_fun<'a, FunSym, ArgSym, ArgSort, Args: ?Sized, OutSort, Body, I>(
&mut self,
symbol: &FunSym,
args: &'a Args,
out: &OutSort,
body: &Body,
info: &I
) -> SmtRes<()> where
ArgSort: Sort2Smt + 'a,
OutSort: Sort2Smt,
FunSym: Sym2Smt<I>,
ArgSym: Sym2Smt<I> + 'a,
Body: Expr2Smt<I>,
&'a Args: IntoIterator<Item = &'a (ArgSym, ArgSort)>,
[src]
&mut self,
symbol: &FunSym,
args: &'a Args,
out: &OutSort,
body: &Body,
info: &I
) -> SmtRes<()> where
ArgSort: Sort2Smt + 'a,
OutSort: Sort2Smt,
FunSym: Sym2Smt<I>,
ArgSym: Sym2Smt<I> + 'a,
Body: Expr2Smt<I>,
&'a Args: IntoIterator<Item = &'a (ArgSym, ArgSort)>,
Defines a new function symbol.
fn define_funs_rec<'a, FunSym, ArgSym, ArgSort, Args, OutSort, Body, Funs: ?Sized, I>(
&mut self,
funs: &'a Funs,
info: &I
) -> SmtRes<()> where
FunSym: Sym2Smt<I> + 'a,
ArgSym: Sym2Smt<I> + 'a,
ArgSort: Sort2Smt + 'a,
OutSort: Sort2Smt + 'a,
Body: Expr2Smt<I> + 'a,
&'a Args: IntoIterator<Item = &'a (ArgSym, ArgSort)> + 'a,
&'a Funs: IntoIterator<Item = &'a (FunSym, Args, OutSort, Body)>,
[src]
&mut self,
funs: &'a Funs,
info: &I
) -> SmtRes<()> where
FunSym: Sym2Smt<I> + 'a,
ArgSym: Sym2Smt<I> + 'a,
ArgSort: Sort2Smt + 'a,
OutSort: Sort2Smt + 'a,
Body: Expr2Smt<I> + 'a,
&'a Args: IntoIterator<Item = &'a (ArgSym, ArgSort)> + 'a,
&'a Funs: IntoIterator<Item = &'a (FunSym, Args, OutSort, Body)>,
Defines some new (possibily mutually) recursive functions.
fn define_fun_rec<'a, FunSym, ArgSym, ArgSort, Args: ?Sized, OutSort, Body, I>(
&mut self,
symbol: &FunSym,
args: &'a Args,
out: &OutSort,
body: &Body,
info: &I
) -> SmtRes<()> where
ArgSort: Sort2Smt + 'a,
OutSort: Sort2Smt,
FunSym: Sym2Smt<I>,
ArgSym: Sym2Smt<I> + 'a,
Body: Expr2Smt<I>,
&'a Args: IntoIterator<Item = &'a (ArgSym, ArgSort)>,
[src]
&mut self,
symbol: &FunSym,
args: &'a Args,
out: &OutSort,
body: &Body,
info: &I
) -> SmtRes<()> where
ArgSort: Sort2Smt + 'a,
OutSort: Sort2Smt,
FunSym: Sym2Smt<I>,
ArgSym: Sym2Smt<I> + 'a,
Body: Expr2Smt<I>,
&'a Args: IntoIterator<Item = &'a (ArgSym, ArgSort)>,
Defines a new recursive function.
fn assert<I, Expr: Expr2Smt<I>>(&mut self, expr: &Expr, info: &I) -> SmtRes<()>
[src]
Asserts an expression with some print information.
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_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<'a, Ident, Type, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<'a, Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
[src]
&mut self
) -> SmtRes<Vec<(Ident, Vec<Type>, Type, Value)>> where
Parser: for<'a> IdentParser<'a, Ident, Type, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<'a, 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<'a, Ident, Type, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<'a, Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
[src]
&mut self
) -> SmtRes<Vec<(Ident, Vec<Type>, Type, Value)>> where
Parser: for<'a> IdentParser<'a, Ident, Type, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<'a, 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<'a, Ident, Type, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<'a, Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
[src]
&mut self
) -> SmtRes<Vec<(Ident, Type, Value)>> where
Parser: for<'a> IdentParser<'a, Ident, Type, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<'a, 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<'a, Ident, Type, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<'a, Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
[src]
&mut self
) -> SmtRes<Vec<(Ident, Type, Value)>> where
Parser: for<'a> IdentParser<'a, Ident, Type, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<'a, 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_or_unknown(&mut self) -> SmtRes<Option<bool>>
[src]
Check-sat command, turns unknown
results in None
.
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, Info, Expr, Exprs: ?Sized>(
&mut self,
exprs: &'a Exprs,
info: &Info
) -> SmtRes<()> where
Expr: Expr2Smt<Info> + 'a,
&'a Exprs: IntoIterator<Item = &'a Expr>,
[src]
&mut self,
exprs: &'a Exprs,
info: &Info
) -> SmtRes<()> where
Expr: Expr2Smt<Info> + 'a,
&'a Exprs: IntoIterator<Item = &'a Expr>,
Get-values command.
fn parse_get_values<Info: Clone, Expr, Value>(
&mut self,
info: Info
) -> SmtRes<Vec<(Expr, Value)>> where
Parser: for<'a> ExprParser<'a, Expr, Info, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<'a, Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
[src]
&mut self,
info: Info
) -> SmtRes<Vec<(Expr, Value)>> where
Parser: for<'a> ExprParser<'a, Expr, Info, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'a> ValueParser<'a, Value, &'a mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
Parse the result of a get-values.
fn get_values<'a, Info: Clone, Expr, Exprs: ?Sized, Value>(
&mut self,
exprs: &'a Exprs,
info: Info
) -> SmtRes<Vec<(Expr, Value)>> where
Parser: for<'b> ExprParser<'b, Expr, Info, &'b mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'b> ValueParser<'b, Value, &'b mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
Expr: Expr2Smt<Info> + 'a,
&'a Exprs: IntoIterator<Item = &'a Expr>,
[src]
&mut self,
exprs: &'a Exprs,
info: Info
) -> SmtRes<Vec<(Expr, Value)>> where
Parser: for<'b> ExprParser<'b, Expr, Info, &'b mut SmtParser<BufReader<&'kid mut ChildStdout>>> + for<'b> ValueParser<'b, Value, &'b mut SmtParser<BufReader<&'kid mut ChildStdout>>>,
Expr: Expr2Smt<Info> + 'a,
&'a Exprs: IntoIterator<Item = &'a Expr>,
Get-values command.
fn print_check_sat_assuming<'a, Info, Ident, Idents: ?Sized>(
&mut self,
bool_vars: &'a Idents,
info: &Info
) -> SmtRes<()> where
Ident: Sym2Smt<Info> + 'a,
&'a Idents: IntoIterator<Item = &'a Ident>,
[src]
&mut self,
bool_vars: &'a Idents,
info: &Info
) -> SmtRes<()> where
Ident: Sym2Smt<Info> + 'a,
&'a Idents: IntoIterator<Item = &'a Ident>,
Check-sat with assumptions command.
fn check_sat_assuming<'a, Info, Ident, Idents: ?Sized>(
&mut self,
idents: &'a Idents,
info: &Info
) -> SmtRes<bool> where
Ident: Sym2Smt<Info> + 'a,
&'a Idents: IntoIterator<Item = &'a Ident>,
[src]
&mut self,
idents: &'a Idents,
info: &Info
) -> SmtRes<bool> where
Ident: Sym2Smt<Info> + 'a,
&'a Idents: IntoIterator<Item = &'a Ident>,
Check-sat assuming command, turns unknown
results into errors.
fn check_sat_assuming_or_unknown<'a, Info, Ident, Idents: ?Sized>(
&mut self,
idents: &'a Idents,
info: &Info
) -> SmtRes<Option<bool>> where
Ident: Sym2Smt<Info> + 'a,
&'a Idents: IntoIterator<Item = &'a Ident>,
[src]
&mut self,
idents: &'a Idents,
info: &Info
) -> SmtRes<Option<bool>> where
Ident: Sym2Smt<Info> + 'a,
&'a Idents: IntoIterator<Item = &'a Ident>,
Check-sat assuming command, turns unknown
results into None
.