Struct RecFuncDecl 

pub struct RecFuncDecl { /* 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 RecFuncDecl

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

pub fn add_def(&self, args: &[&dyn Ast], body: &dyn Ast)

Adds the body to a recursive function.

let mut f = RecFuncDecl::new(
    "f",
    &[&Sort::int()],
    &Sort::int());
let n = Int::new_const("n");
f.add_def(
    &[&n],
    &Int::add(&[&n, &Int::from_i64(1)])
);

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

let solver = Solver::new();
let forall: z3::ast::Bool = z3::ast::forall_const(
        &[&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>

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

pub fn apply(&self, args: &[&dyn Ast]) -> Dynamic

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.

pub fn domain(&self, i: usize) -> Option<SortKind>

Returns the kind of the i-th domain (parameter) of this FuncDecl.

Returns None if i >= |domain|.

pub fn range(&self) -> SortKind

Returns the kind of range (output) of this FuncDecl.

Trait Implementations

impl Debug for RecFuncDecl

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

Formats the value using the given formatter.

impl Deref for RecFuncDecl

type Target = FuncDecl

The resulting type after dereferencing.

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

Dereferences the value.

impl Display for RecFuncDecl

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

Formats the value using the given formatter.

impl Drop for RecFuncDecl

fn drop(&mut self)

Executes the destructor for this type.