Struct rsmt2::TeeSolver

pub struct TeeSolver<'kid, Parser: Copy> { /* fields omitted */ }

Wrapper around a PlainSolver logging IOs to a file.

Methods

impl<'kid, Parser: Copy> TeeSolver<'kid, Parser>

fn conf(&self) -> &SolverConf

Configuration of the solver.

Trait Implementations

impl<'kid, Parser: Copy> Solver<'kid, Parser> for TeeSolver<'kid, Parser>

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

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

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

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

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

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

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, 

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, 

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

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

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

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

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

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

Defines a new recursive function.

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

Asserts an expression without print information.

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.

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.

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.

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

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

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

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

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

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

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

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

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

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

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

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

Get-values command.

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

Get-values command.

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

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

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

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

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

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

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