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

Resets the underlying solver. Restarts the kid process if no reset command is supported.

Sets the logic.

Set option command.

Activates interactive mode.

Activates print success.

Activates unsat core production.

Shuts the solver down.

Pushes n layers on the assertion stack.

Pops n layers off the assertion stack.

Resets the assertions in the solver.

Introduces a new actlit.

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

Forces the value of an actlit and consumes it.

Declares a new sort.

Defines a new sort.

Defines a new sort.

Declares a new function symbol.

Declares a new function symbol.

Declares a new constant.

Declares a new constant.

Defines a new function symbol.

Defines a new function symbol.

Defines some new (possibily mutually) recursive functions.

Defines some new (possibily mutually) recursive functions.

Defines a new recursive function.

Defines a new recursive function.

Asserts an expression without print information.

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

Asserts an expression with some print information.

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

Get info command.

Get option command.

Set info command.

Echo command.

Check-sat command.

Check-sat command, with actlits.

Get-model command.

Parse the result of a get-model.

Get-model command.

Parse the result of a get-model where all the symbols are nullary.

Get-model command when all the symbols are nullary.

Parse success.

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

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

Check-sat command, turns unknown results into errors.

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

Check-sat command, turns unknown results in None.

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

Get-assertions command.

Get-assignment command.

Get-unsat-assumptions command.

Get-proof command.

Get-unsat-core command.

Get-values command.

Get-values command.

Parse the result of a get-values.

Parse the result of a get-values.

Get-values command.

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

Get-values command.

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

Check-sat with assumptions command with unit info.

Check-sat with assumptions command.

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

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

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

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

Implementors