Struct z3::RecFuncDecl

pub struct RecFuncDecl<'ctx> { /* fields omitted */ }

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:

• FuncDecl::add_def

Implementations

impl<'ctx> RecFuncDecl<'ctx>

pub fn new<S: Into<Symbol>>(
    ctx: &'ctx Context,
    name: S,
    domain: &[&Sort<'ctx>],
    range: &Sort<'ctx>
) -> Self

pub unsafe fn from_raw(ctx: &'ctx Context, z3_func_decl: Z3_func_decl) -> Self

pub fn add_def(&self, args: &[&Dynamic<'ctx>], body: &impl Ast<'ctx>)

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.

pub fn arity(&self) -> usize

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

pub fn apply(&self, args: &[&Dynamic<'ctx>]) -> Dynamic<'ctx>

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.

pub fn kind(&self) -> DeclKind

Return the DeclKind of this RecFuncDecl.

pub fn name(&self) -> String

Return the name of this RecFuncDecl.

Strings will return the Symbol. Ints will have a "k!" prepended to the Symbol.

Trait Implementations

impl<'ctx> Debug for RecFuncDecl<'ctx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'ctx> Display for RecFuncDecl<'ctx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'ctx> Drop for RecFuncDecl<'ctx>

fn drop(&mut self)

Executes the destructor for this type.