Struct z3::RecFuncDecl [−][src]
pub struct RecFuncDecl<'ctx> { /* fields omitted */ }
Expand description
Recursive function declaration. Every function has an associated declaration.
The declaration assigns a name, a return sort (i.e., type), and the sort (i.e., type) of each of its arguments. This is the function declaration type you should use if you want to add a definition to your function, recursive or not.
See also:
Implementations
pub fn new<S: Into<Symbol>>(
ctx: &'ctx Context,
name: S,
domain: &[&Sort<'ctx>],
range: &Sort<'ctx>
) -> Self
Adds the body to a recursive function.
let mut f = RecFuncDecl::new( &ctx, "f", &[&Sort::int(&ctx)], &Sort::int(&ctx)); let n = Int::new_const(&ctx, "n"); f.add_def( &[&n.clone().into()], &Int::add(&ctx, &[&n, &Int::from_i64(&ctx, 1)]) ); let f_of_n = &f.apply(&[&n.clone().into()]); let solver = Solver::new(&ctx); let forall: z3::ast::Bool = z3::ast::forall_const( &ctx, &[&n], &[], &n.lt(&f_of_n.as_int().unwrap()) ).try_into().unwrap(); solver.assert(&forall); let res = solver.check(); assert_eq!(res, SatResult::Sat);
Note that args
should have the types corresponding to the domain
of the RecFuncDecl
.
Return the number of arguments of a function declaration.
If the function declaration is a constant, then the arity is 0
.
let f = RecFuncDecl::new( &ctx, "f", &[&Sort::int(&ctx), &Sort::real(&ctx)], &Sort::int(&ctx)); assert_eq!(f.arity(), 2);
Create a constant (if args
has length 0) or function application (otherwise).
Note that args
should have the types corresponding to the domain
of the RecFuncDecl
.
Trait Implementations
Auto Trait Implementations
impl<'ctx> RefUnwindSafe for RecFuncDecl<'ctx>
impl<'ctx> !Send for RecFuncDecl<'ctx>
impl<'ctx> !Sync for RecFuncDecl<'ctx>
impl<'ctx> Unpin for RecFuncDecl<'ctx>
impl<'ctx> UnwindSafe for RecFuncDecl<'ctx>