[−][src]Struct rsmt2_zz::Solver
Solver providing most of the SMT-LIB 2.5 commands.
Note the tee
function, which takes a file writer to which it will write everything
sent to the solver.
Methods
impl<Parser> Solver<Parser>
[src]
pub fn new(conf: SmtConf, parser: Parser) -> SmtRes<Self>
[src]
Constructor.
pub fn default(parser: Parser) -> SmtRes<Self>
[src]
Creates a solver kid with the default configuration.
Mostly used in tests, same as Self::new( SmtConf::z3(), parser )
.
pub fn default_z3(parser: Parser) -> SmtRes<Self>
[src]
Creates a solver kid with the default z3 configuration.
Mostly used in tests, same as Self::new( SmtConf::z3(), parser )
.
pub fn default_cvc4(parser: Parser) -> SmtRes<Self>
[src]
Creates a solver kid with the default cvc4 configuration.
Mostly used in tests, same as Self::new( SmtConf::z3(), parser )
.
pub fn default_yices_2(parser: Parser) -> SmtRes<Self>
[src]
Creates a solver kid with the default yices 2 configuration.
Mostly used in tests, same as Self::new( SmtConf::yices_2(), parser )
.
pub fn conf(&self) -> &SmtConf
[src]
Returns the configuration of the solver.
pub fn tee(&mut self, file: File) -> SmtRes<()>
[src]
Forces the solver to write all communications to a file.
Errors if the solver was already tee-ed.
pub fn path_tee<P>(&mut self, path: P) -> SmtRes<()> where
P: AsRef<Path>,
[src]
P: AsRef<Path>,
Forces the solver to write all communications to a file.
Opens file
with create
and write
.
pub fn is_teed(&self) -> bool
[src]
True if the solver is tee-ed.
pub fn kill(&mut self) -> SmtRes<()>
[src]
Kills the solver kid.
The windows version just prints (exit)
on the kid's stdin
. Anything else seems to cause
problems.
This function is automatically called when the solver is dropped.
pub fn comment_args(&mut self, args: Arguments) -> SmtRes<()>
[src]
Prints a comment in the tee-ed file if any.
pub fn comment(&mut self, blah: &str) -> SmtRes<()>
[src]
Prints a comment in the tee-ed file if any. String version.
impl<Parser> Solver<Parser>
[src]
pub fn assert<Expr: ?Sized>(&mut self, expr: &Expr) -> SmtRes<()> where
Expr: Expr2Smt<()>,
[src]
Expr: Expr2Smt<()>,
Asserts an expression.
Examples
let mut solver = Solver::default(()).unwrap() ; solver.assert("(= 0 1)").unwrap() ;
pub fn check_sat(&mut self) -> SmtRes<bool>
[src]
Check-sat command, turns unknown
results into errors.
See also
If you want a more natural way to handle unknown results, see parse_check_sat_or_unk
.
Examples
solver.declare_const("x", "Int").unwrap() ; solver.declare_const("y", "Int").unwrap() ; solver.push(1).unwrap() ; solver.assert("(= (+ x y) 0)").unwrap() ; let maybe_sat = solver.check_sat().unwrap() ; assert_eq! { maybe_sat, true } solver.pop(1).unwrap() ; solver.assert("(= (+ (* x x y) (* y y x)) 7654321)").unwrap() ; let sat_res = & solver.check_sat() ; match * sat_res { Err(ref e) => match * e.kind() { ::rsmt2::errors::ErrorKind::Unknown => (), _ => panic!("expected unknown"), }, Ok(res) => panic!("expected error: {:?}", res), }
pub fn check_sat_or_unk(&mut self) -> SmtRes<Option<bool>>
[src]
Check-sat command, turns unknown
results in None
.
See also
Examples
solver.declare_const("x", "Int").unwrap() ; solver.declare_const("y", "Int").unwrap() ; solver.push(1).unwrap() ; solver.assert("(= (+ x y) 0)").unwrap() ; let maybe_sat = solver.check_sat_or_unk().unwrap() ; assert_eq! { maybe_sat, Some(true) } solver.pop(1).unwrap() ; solver.assert("(= (+ (* x x y) (* y y x)) 7654321)").unwrap() ; let maybe_sat = solver.check_sat_or_unk().unwrap() ; // Unknown ~~~~~~~~~~~~~vvvv assert_eq! { maybe_sat, None }
pub fn reset(&mut self) -> SmtRes<()>
[src]
Resets the underlying solver. Restarts the kid process if no reset command is supported.
Examples
let mut solver = Solver::default(()).unwrap() ; solver.assert("(= 0 1)").unwrap() ; assert! { ! solver.check_sat().unwrap() } solver.reset().unwrap() ; assert! { solver.check_sat().unwrap() }
pub 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.
Examples
let mut solver = Solver::default(()).unwrap() ; solver.declare_const("x", "Int").unwrap()
pub 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: IntoIterator<Item = &'a ArgSort>,
[src]
&mut self,
symbol: &FunSym,
args: Args,
out: &OutSort
) -> SmtRes<()> where
FunSym: Sym2Smt<()>,
ArgSort: Sort2Smt + 'a,
OutSort: Sort2Smt,
Args: IntoIterator<Item = &'a ArgSort>,
Declares a new function symbol.
let mut solver = Solver::default(()).unwrap() ; solver.declare_fun( "my_symbol", & [ "Int", "Real", "Bool" ], "Bool" ).unwrap()
pub fn define_const<FunSym: ?Sized, OutSort: ?Sized, Body: ?Sized>(
&mut self,
symbol: &FunSym,
out: &OutSort,
body: &Body
) -> SmtRes<()> where
OutSort: Sort2Smt,
FunSym: Sym2Smt<()>,
Body: Expr2Smt<()>,
[src]
&mut self,
symbol: &FunSym,
out: &OutSort,
body: &Body
) -> SmtRes<()> where
OutSort: Sort2Smt,
FunSym: Sym2Smt<()>,
Body: Expr2Smt<()>,
Defines a new constant function symbol.
Examples
let mut solver = Solver::default(()).unwrap() ; solver.define_const( "seven", "Int", "7" ).unwrap()
pub fn define_fun<'a, FunSym: ?Sized, ArgSym, ArgSort, Args, OutSort: ?Sized, Body: ?Sized>(
&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: 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: IntoIterator<Item = &'a (ArgSym, ArgSort)>,
Defines a new function symbol.
Examples
let mut solver = Solver::default(()).unwrap() ; solver.define_fun( "abs", & [ ("n", "Int") ], "Int", "(ite (< x 0) (- x) x)" ).unwrap()
pub fn push(&mut self, n: u8) -> SmtRes<()>
[src]
Pushes n
layers on the assertion stack.
Examples
let mut solver = Solver::default(()).unwrap() ; solver.declare_const("x", "Int").unwrap() ; solver.declare_const("y", "Int").unwrap() ; solver.assert("(= x y)").unwrap() ; let sat = solver.check_sat().unwrap() ; assert!(sat) ; solver.push(1).unwrap() ; solver.assert("(= x (+ x 1))").unwrap() ; let sat = solver.check_sat().unwrap() ; assert!(! sat) ; solver.pop(1).unwrap() ; let sat = solver.check_sat().unwrap() ; assert!(sat) ;
pub fn pop(&mut self, n: u8) -> SmtRes<()>
[src]
Pops n
layers off the assertion stack.
See push
for examples.
pub fn check_sat_assuming<'a, Ident: ?Sized, Idents>(
&mut self,
idents: Idents
) -> SmtRes<bool> where
Ident: Sym2Smt<()> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
[src]
&mut self,
idents: Idents
) -> SmtRes<bool> where
Ident: Sym2Smt<()> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
Check-sat assuming command, turns unknown
results into errors.
pub fn check_sat_assuming_or_unk<'a, Ident: ?Sized, Idents>(
&mut self,
idents: Idents
) -> SmtRes<Option<bool>> where
Ident: Sym2Smt<()> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
[src]
&mut self,
idents: Idents
) -> SmtRes<Option<bool>> where
Ident: Sym2Smt<()> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
Check-sat assuming command, turns unknown
results into None
.
pub fn set_logic(&mut self, logic: Logic) -> SmtRes<()>
[src]
Sets the logic.
Examples
let mut solver = Solver::default(()).unwrap() ; solver.set_logic( ::rsmt2::Logic::QF_UF ).unwrap() ;
pub fn define_fun_rec<'a, FunSym: ?Sized, ArgSym, ArgSort, Args, OutSort: ?Sized, Body: ?Sized>(
&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: 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: IntoIterator<Item = &'a (ArgSym, ArgSort)>,
Defines a recursive function.
Examples
let mut solver = Solver::default(()).unwrap() ; solver.define_fun_rec( "abs", & [ ("n", "Int") ], "Int", "(ite (< x 0) (abs (- x)) x)" ).unwrap()
pub fn define_funs_rec<'a, FunSym, ArgSym, ArgSort, Args, ArgsRef, 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,
Args: ?Sized,
ArgsRef: 'a + AsRef<Args>,
Funs: IntoIterator<Item = &'a (FunSym, ArgsRef, OutSort, Body)>,
Funs::IntoIter: Clone,
[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,
Args: ?Sized,
ArgsRef: 'a + AsRef<Args>,
Funs: IntoIterator<Item = &'a (FunSym, ArgsRef, OutSort, Body)>,
Funs::IntoIter: Clone,
Defines some (possibily mutually) recursive functions.
Examples
let mut solver = Solver::default(()).unwrap() ; solver.define_funs_rec( & [ ("abs_1", & [ ("n", "Int") ], "Int", "(ite (< x 0) (abs_2 (- x)) x)"), ("abs_2", & [ ("n", "Int") ], "Int", "(ite (< x 0) (abs_3 (- x)) x)"), ("abs_3", & [ ("n", "Int") ], "Int", "(ite (< x 0) (abs_1 (- x)) x)"), ] ).unwrap()
pub fn declare_datatypes<'a, Sort, Param, ParamList, Def, DefList, All>(
&mut self,
defs: All
) -> SmtRes<()> where
Sort: Sort2Smt + 'a,
Param: Sort2Smt + 'a,
&'a ParamList: IntoIterator<Item = &'a Param> + 'a,
Def: Sort2Smt + 'a,
&'a DefList: IntoIterator<Item = &'a Def> + 'a,
All: IntoIterator<Item = &'a (Sort, usize, ParamList, DefList)> + 'a,
All::IntoIter: Clone,
[src]
&mut self,
defs: All
) -> SmtRes<()> where
Sort: Sort2Smt + 'a,
Param: Sort2Smt + 'a,
&'a ParamList: IntoIterator<Item = &'a Param> + 'a,
Def: Sort2Smt + 'a,
&'a DefList: IntoIterator<Item = &'a Def> + 'a,
All: IntoIterator<Item = &'a (Sort, usize, ParamList, DefList)> + 'a,
All::IntoIter: Clone,
Declares mutually recursive datatypes.
A relatively recent version of z3 is recommended.
Examples
# use rsmt2::Solver ;
let mut solver = Solver::default(()).unwrap() ;
solver.declare_datatypes( & [
( "Tree", 1, ["T"],
[ "leaf", "(node (value T) (children (TreeList T)))" ] ),
( "TreeList", 1, ["T"],
[ "nil", "(cons (car (Tree T)) (cdr (TreeList T)))" ]),
] ).unwrap() ;
solver.declare_const( "t1", "(Tree Int)" ).unwrap() ;
solver.declare_const( "t2", "(Tree Bool)" ).unwrap() ;
solver.assert("(> (value t1) 20)").unwrap() ;
solver.assert("(not (is-leaf t2))").unwrap() ;
solver.assert("(not (value t2))").unwrap() ;
let sat = solver.check_sat().unwrap() ;
assert! { sat } panic! { "aaa" }
impl<Parser> Solver<Parser>
[src]
pub fn get_model<Ident, Type, Value>(
&mut self
) -> SmtRes<Vec<(Ident, Vec<(Ident, Type)>, Type, Value)>> where
Parser: for<'a> IdentParser<Ident, Type, &'a mut RSmtParser> + for<'a> ModelParser<Ident, Type, Value, &'a mut RSmtParser>,
[src]
&mut self
) -> SmtRes<Vec<(Ident, Vec<(Ident, Type)>, Type, Value)>> where
Parser: for<'a> IdentParser<Ident, Type, &'a mut RSmtParser> + for<'a> ModelParser<Ident, Type, Value, &'a mut RSmtParser>,
Get-model command.
pub fn get_model_const<Ident, Type, Value>(
&mut self
) -> SmtRes<Vec<(Ident, Type, Value)>> where
Parser: for<'a> IdentParser<Ident, Type, &'a mut RSmtParser> + for<'a> ModelParser<Ident, Type, Value, &'a mut RSmtParser>,
[src]
&mut self
) -> SmtRes<Vec<(Ident, Type, Value)>> where
Parser: for<'a> IdentParser<Ident, Type, &'a mut RSmtParser> + for<'a> ModelParser<Ident, Type, Value, &'a mut RSmtParser>,
Get-model command when all the symbols are nullary.
pub 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 RSmtParser> + for<'b> ValueParser<PValue, &'b mut RSmtParser>,
Expr: Expr2Smt<()> + 'a,
Exprs: IntoIterator<Item = &'a Expr>,
[src]
&mut self,
exprs: Exprs
) -> SmtRes<Vec<(PExpr, PValue)>> where
Parser: for<'b> ExprParser<PExpr, (), &'b mut RSmtParser> + for<'b> ValueParser<PValue, &'b mut RSmtParser>,
Expr: Expr2Smt<()> + 'a,
Exprs: IntoIterator<Item = &'a Expr>,
Get-values command.
Notice that the input expression type and the output one have no reason to be the same.
impl<Parser> Solver<Parser>
[src]
Actlit-related functions.
See the actlit
's module doc for more details.
pub fn get_actlit(&mut self) -> SmtRes<Actlit>
[src]
Introduces a new actlit.
See the actlit
's module doc for more details.
pub fn de_actlit(&mut self, actlit: Actlit) -> SmtRes<()>
[src]
Deactivates an activation literal, alias for solver.set_actlit(actlit, false)
.
See the actlit
's module doc for more details.
pub fn set_actlit(&mut self, actlit: Actlit, b: bool) -> SmtRes<()>
[src]
Forces the value of an actlit and consumes it.
See the actlit
's module doc for more details.
pub 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.
See the actlit
's module doc for more details.
pub fn check_sat_act<'a, Actlits>(&mut self, actlits: Actlits) -> SmtRes<bool> where
Actlits: IntoIterator<Item = &'a Actlit>,
[src]
Actlits: IntoIterator<Item = &'a Actlit>,
Check-sat command with activation literals, turns unknown
results into
errors.
pub fn check_sat_act_or_unk<'a, Actlits>(
&mut self,
actlits: Actlits
) -> SmtRes<Option<bool>> where
Actlits: IntoIterator<Item = &'a Actlit>,
[src]
&mut self,
actlits: Actlits
) -> SmtRes<Option<bool>> where
Actlits: IntoIterator<Item = &'a Actlit>,
Check-sat command with activation literals, turns unknown
results in
None
.
impl<Parser> Solver<Parser>
[src]
pub fn print_check_sat(&mut self) -> SmtRes<FutureCheckSat>
[src]
Prints a check-sat command.
Allows to print the check-sat
and get the result later, e.g. with
parse_check_sat
.
Examples
use rsmt2::Solver ; let mut solver = Solver::default(()).unwrap() ; solver.declare_const("x", "Int").unwrap() ; solver.declare_const("y", "Int").unwrap() ; solver.assert("(= (+ x y) 0)").unwrap() ; let future = solver.print_check_sat().unwrap() ; // Do stuff while the solver works. let sat = solver.parse_check_sat(future).unwrap() ; assert! { sat }
pub fn print_check_sat_act<'a, Actlits>(
&mut self,
actlits: Actlits
) -> SmtRes<FutureCheckSat> where
Actlits: IntoIterator<Item = &'a Actlit>,
[src]
&mut self,
actlits: Actlits
) -> SmtRes<FutureCheckSat> where
Actlits: IntoIterator<Item = &'a Actlit>,
Check-sat command, with actlits.
See the actlit
's module doc for more details.
pub fn parse_check_sat(&mut self, _: FutureCheckSat) -> SmtRes<bool>
[src]
Parse the result of a check-sat, turns unknown
results into errors.
pub fn parse_check_sat_or_unk(
&mut self,
_: FutureCheckSat
) -> SmtRes<Option<bool>>
[src]
&mut self,
_: FutureCheckSat
) -> SmtRes<Option<bool>>
Parse the result of a check-sat, turns unknown
results into None
.
pub fn print_check_sat_assuming<'a, Ident: ?Sized, Idents>(
&mut self,
bool_vars: Idents
) -> SmtRes<FutureCheckSat> where
Ident: Sym2Smt<()> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
[src]
&mut self,
bool_vars: Idents
) -> SmtRes<FutureCheckSat> where
Ident: Sym2Smt<()> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
Check-sat with assumptions command with unit info.
pub fn print_check_sat_assuming_with<'a, Info, Ident: ?Sized, Idents>(
&mut self,
bool_vars: Idents,
info: Info
) -> SmtRes<FutureCheckSat> where
Info: Copy,
Ident: Sym2Smt<Info> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
[src]
&mut self,
bool_vars: Idents,
info: Info
) -> SmtRes<FutureCheckSat> where
Info: Copy,
Ident: Sym2Smt<Info> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
Check-sat with assumptions command.
impl<Parser> Solver<Parser>
[src]
pub fn declare_sort<Sort: ?Sized>(
&mut self,
sort: &Sort,
arity: u8
) -> SmtRes<()> where
Sort: Sort2Smt,
[src]
&mut self,
sort: &Sort,
arity: u8
) -> SmtRes<()> where
Sort: Sort2Smt,
Declares a new sort.
Examples
let mut solver = Solver::default(()).unwrap() ; solver.declare_sort("A", 0).unwrap() ; solver.declare_const("x", "A").unwrap() ; solver.declare_const("y", "A").unwrap() ; solver.declare_fun("f", & [ "A" ], "A").unwrap() ; solver.assert("(= (f (f x)) x)").unwrap() ; solver.assert("(= (f x) y)").unwrap() ; solver.assert("(not (= x y))").unwrap() ; let sat = solver.check_sat().unwrap() ;
pub fn define_sort<'a, Sort: ?Sized, Arg: ?Sized, Args, Body: ?Sized>(
&mut self,
sort: &Sort,
args: Args,
body: &Body
) -> SmtRes<()> where
Sort: Sort2Smt,
Arg: Sort2Smt + 'a,
Body: Sort2Smt,
Args: IntoIterator<Item = &'a Arg>,
[src]
&mut self,
sort: &Sort,
args: Args,
body: &Body
) -> SmtRes<()> where
Sort: Sort2Smt,
Arg: Sort2Smt + 'a,
Body: Sort2Smt,
Args: IntoIterator<Item = &'a Arg>,
Defines a new sort.
Examples
Note the use of define_null_sort
to avoid problems with empty
arguments.
let mut solver = Solver::default(()).unwrap() ; solver.define_sort("MySet", & ["T"], "(Array T Bool)").unwrap() ; solver.define_null_sort("IList", "(List Int)").unwrap() ; solver.define_sort( "List-Set", & ["T"], "(Array (List T) Bool)" ).unwrap() ; solver.define_null_sort("I", "Int").unwrap() ; solver.declare_const("s1", "(MySet I)").unwrap() ; solver.declare_const("s2", "(List-Set Int)").unwrap() ; solver.declare_const("a", "I").unwrap() ; solver.declare_const("l", "IList").unwrap() ; solver.assert("(= (select s1 a) true)").unwrap() ; solver.assert("(= (select s2 l) false)").unwrap() ; let sat = solver.check_sat().unwrap() ;
pub fn define_null_sort<Sort: ?Sized, Body: ?Sized>(
&mut self,
sort: &Sort,
body: &Body
) -> SmtRes<()> where
Sort: Sort2Smt,
Body: Sort2Smt,
[src]
&mut self,
sort: &Sort,
body: &Body
) -> SmtRes<()> where
Sort: Sort2Smt,
Body: Sort2Smt,
Defines a new nullary sort.
When using define_sort
, rust complains because it does not know what the Arg
type
parameter is, since the args
parameter is empty. So this function can be useful.
This could be fixed with a default type for Arg
, like Body
for instance, but this is
currently not possible in a function.
impl<Parser> Solver<Parser>
[src]
pub 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.
pub 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: 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: IntoIterator<Item = &'a ArgSort>,
Declares a new function symbol.
pub fn define_const_with<Info, Sym: ?Sized, Sort: ?Sized, Body: ?Sized>(
&mut self,
symbol: &Sym,
out_sort: &Sort,
body: &Body,
info: Info
) -> SmtRes<()> where
Info: Copy,
Sym: Sym2Smt<Info>,
Sort: Sort2Smt,
Body: Expr2Smt<Info>,
[src]
&mut self,
symbol: &Sym,
out_sort: &Sort,
body: &Body,
info: Info
) -> SmtRes<()> where
Info: Copy,
Sym: Sym2Smt<Info>,
Sort: Sort2Smt,
Body: Expr2Smt<Info>,
Defines a new constant.
pub fn define_fun_with<'a, Info, FunSym: ?Sized, ArgSym, ArgSort, Args, OutSort: ?Sized, Body: ?Sized>(
&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: 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: IntoIterator<Item = &'a (ArgSym, ArgSort)>,
Defines a new function symbol.
pub fn define_funs_rec_with<'a, Info, FunSym, ArgSym, ArgSort, Args, ArgsRef, 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,
Args: ?Sized,
ArgsRef: 'a + AsRef<Args>,
Funs: IntoIterator<Item = &'a (FunSym, ArgsRef, OutSort, Body)>,
Funs::IntoIter: Clone,
[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,
Args: ?Sized,
ArgsRef: 'a + AsRef<Args>,
Funs: IntoIterator<Item = &'a (FunSym, ArgsRef, OutSort, Body)>,
Funs::IntoIter: Clone,
Defines some new (possibily mutually) recursive functions.
pub fn define_fun_rec_with<'a, Info, FunSym: ?Sized, ArgSym, ArgSort, Args, OutSort: ?Sized, Body: ?Sized>(
&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: 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: IntoIterator<Item = &'a (ArgSym, ArgSort)>,
Defines a new recursive function.
pub 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.
See the actlit
's module doc for more details.
pub 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.
pub 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: IntoIterator<Item = &'a Ident>,
[src]
&mut self,
idents: Idents,
info: Info
) -> SmtRes<bool> where
Info: Copy,
Ident: Sym2Smt<Info> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
Check-sat assuming command, turns unknown
results into errors.
pub fn check_sat_assuming_or_unk_with<'a, Info, Ident: ?Sized, Idents>(
&mut self,
idents: Idents,
info: Info
) -> SmtRes<Option<bool>> where
Info: Copy,
Ident: Sym2Smt<Info> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
[src]
&mut self,
idents: Idents,
info: Info
) -> SmtRes<Option<bool>> where
Info: Copy,
Ident: Sym2Smt<Info> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
Check-sat assuming command, turns unknown
results into None
.
impl<Parser> Solver<Parser>
[src]
pub fn set_option<Value: Display>(
&mut self,
option: &str,
value: Value
) -> SmtRes<()>
[src]
&mut self,
option: &str,
value: Value
) -> SmtRes<()>
Set option command.
pub fn produce_unsat_core(&mut self) -> SmtRes<()>
[src]
Activates unsat core production.
pub fn reset_assertions(&mut self) -> SmtRes<()>
[src]
Resets the assertions in the solver.
pub fn get_info(&mut self, flag: &str) -> SmtRes<()>
[src]
Get info command.
pub fn get_option(&mut self, option: &str) -> SmtRes<()>
[src]
Get option command.
pub fn set_info(&mut self, attribute: &str) -> SmtRes<()>
[src]
Set info command.
pub fn echo(&mut self, text: &str) -> SmtRes<()>
[src]
Echo command.
Trait Implementations
impl<Parser> Drop for Solver<Parser>
[src]
impl<Parser> Write for Solver<Parser>
[src]
fn write(&mut self, buf: &[u8]) -> Result<usize>
[src]
fn flush(&mut self) -> Result<()>
[src]
fn write_vectored(&mut self, bufs: &[IoSlice]) -> Result<usize, Error>
1.36.0[src]
fn write_all(&mut self, buf: &[u8]) -> Result<(), Error>
1.0.0[src]
fn write_fmt(&mut self, fmt: Arguments) -> Result<(), Error>
1.0.0[src]
fn by_ref(&mut self) -> &mut Self
1.0.0[src]
Auto Trait Implementations
impl<Parser> RefUnwindSafe for Solver<Parser> where
Parser: RefUnwindSafe,
Parser: RefUnwindSafe,
impl<Parser> Send for Solver<Parser> where
Parser: Send,
Parser: Send,
impl<Parser> Sync for Solver<Parser> where
Parser: Sync,
Parser: Sync,
impl<Parser> Unpin for Solver<Parser> where
Parser: Unpin,
Parser: Unpin,
impl<Parser> UnwindSafe for Solver<Parser> where
Parser: UnwindSafe,
Parser: UnwindSafe,
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,