Struct z3::FuncDecl

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

Function declaration. Every constant and function have an associated declaration.

The declaration assigns a name, a sort (i.e., type), and for function the sort (i.e., type) of each of its arguments. Note that, in Z3, a constant is a function with 0 arguments.

Methods

impl<'ctx> FuncDecl<'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 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: &[&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 FuncDecl.

Trait Implementations

impl<'ctx> Drop for FuncDecl<'ctx>

fn drop(&mut self)

Executes the destructor for this type.

impl<'ctx> Display for FuncDecl<'ctx>

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

Formats the value using the given formatter.