Struct z3::RecFuncDecl

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

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.

This struct can dereference into a FuncDecl to access its methods.

See also:

• RecFuncDecl::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 fn add_def(&self, args: &[&dyn Ast<'ctx>], body: &dyn 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],
    &Int::add(&ctx, &[&n, &Int::from_i64(&ctx, 1)])
);

let f_of_n = &f.apply(&[&n.clone()]);

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.

Methods from Deref<Target = FuncDecl<'ctx>>

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 = FuncDecl::new(
    &ctx,
    "f",
    &[&Sort::int(&ctx), &Sort::real(&ctx)],
    &Sort::int(&ctx));
assert_eq!(f.arity(), 2);

pub fn apply(&self, args: &[&dyn Ast<'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 FuncDecl.

pub fn kind(&self) -> DeclKind

Return the DeclKind of this FuncDecl.

pub fn name(&self) -> String

Return the name of this FuncDecl.

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> Deref for RecFuncDecl<'ctx>

type Target = FuncDecl<'ctx>

The resulting type after dereferencing.

fn deref(&self) -> &Self::Target

Dereferences the value.

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.