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.

See also:

• RecFuncDecl

Implementations

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

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

Formats the value using the given formatter.

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

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

Formats the value using the given formatter.

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

fn drop(&mut self)

Executes the destructor for this type.