func_decl Class Reference

Function declaration (aka function definition). It is the signature of interpreted and uninterpreted functions in Z3. The basic building block in Z3 is the function application. More...

Inheritance diagram for func_decl:

Public Member Functions
	func_decl (context &c)
	func_decl (context &c, Z3_func_decl n)
	func_decl (func_decl const &s)
	operator Z3_func_decl () const
func_decl &	operator= (func_decl const &s)
unsigned	arity () const
sort	domain (unsigned i) const
sort	range () const
symbol	name () const
Z3_decl_kind	decl_kind () const
bool	is_const () const
expr	operator() () const
expr	operator() (unsigned n, expr const *args) const
expr	operator() (expr_vector const &v) const
expr	operator() (expr const &a) const
expr	operator() (int a) const
expr	operator() (expr const &a1, expr const &a2) const
expr	operator() (expr const &a1, int a2) const
expr	operator() (int a1, expr const &a2) const
expr	operator() (expr const &a1, expr const &a2, expr const &a3) const
expr	operator() (expr const &a1, expr const &a2, expr const &a3, expr const &a4) const
expr	operator() (expr const &a1, expr const &a2, expr const &a3, expr const &a4, expr const &a5) const

---

Detailed Description

Function declaration (aka function definition). It is the signature of interpreted and uninterpreted functions in Z3. The basic building block in Z3 is the function application.

Definition at line 427 of file z3++.h.

---

Constructor & Destructor Documentation

func_decl

(

context &

c

)

[inline]

Definition at line 429 of file z3++.h.

:ast(c) {}

func_decl	(	context &	c,
		Z3_func_decl	n
	)		[inline]

Definition at line 430 of file z3++.h.

:ast(c, reinterpret_cast<Z3_ast>(n)) {}

func_decl

(

func_decl const &

s

)

[inline]

Definition at line 431 of file z3++.h.

:ast(s) {}

---

Member Function Documentation

unsigned arity

(

)

const [inline]

Definition at line 435 of file z3++.h.

Referenced by FuncDeclRef::__call__(), func_decl::domain(), FuncDeclRef::domain(), and func_decl::is_const().

{ return Z3_get_arity(ctx(), *this); }

Z3_decl_kind decl_kind

(

)

const [inline]

Definition at line 439 of file z3++.h.

{ return Z3_get_decl_kind(ctx(), *this); }

sort domain

(

unsigned

i

)

const [inline]

Definition at line 436 of file z3++.h.

Referenced by FuncDeclRef::__call__(), and func_decl::operator()().

{ assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }

bool is_const

(

)

const [inline]

Definition at line 441 of file z3++.h.

{ return arity() == 0; }

symbol name

(

)

const [inline]

Definition at line 438 of file z3++.h.

{ Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }

operator Z3_func_decl

(

)

const [inline]

Definition at line 432 of file z3++.h.

{ return reinterpret_cast<Z3_func_decl>(m_ast); }

expr operator()

(

)

const [inline]

Definition at line 1680 of file z3++.h.

                                            {
        Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
        ctx().check_error();
        return expr(ctx(), r);
    }

expr operator()	(	unsigned	n,
		expr const *	args
	)		const [inline]

Definition at line 1659 of file z3++.h.

                                                                         {
        array<Z3_ast> _args(n);
        for (unsigned i = 0; i < n; i++) {
            check_context(*this, args[i]);
            _args[i] = args[i];
        }
        Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
        check_error();
        return expr(ctx(), r);
    
    }

expr operator()

(

expr_vector const &

v

)

const [inline]

Definition at line 1670 of file z3++.h.

                                                                   {
        array<Z3_ast> _args(args.size());
        for (unsigned i = 0; i < args.size(); i++) {
            check_context(*this, args[i]);
            _args[i] = args[i];
        }
        Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
        check_error();
        return expr(ctx(), r);    
    }

expr operator()

(

expr const &

a

)

const [inline]

Definition at line 1685 of file z3++.h.

                                                          {
        check_context(*this, a);
        Z3_ast args[1] = { a };
        Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
        ctx().check_error();
        return expr(ctx(), r);
    }

expr operator()

(

int

a

)

const [inline]

Definition at line 1692 of file z3++.h.

                                                 {
        Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
        Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
        ctx().check_error();
        return expr(ctx(), r);
    }

expr operator()	(	expr const &	a1,
		expr const &	a2
	)		const [inline]

Definition at line 1698 of file z3++.h.

                                                                            {
        check_context(*this, a1); check_context(*this, a2);
        Z3_ast args[2] = { a1, a2 };
        Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
        ctx().check_error();
        return expr(ctx(), r);
    }

expr operator()	(	expr const &	a1,
		int	a2
	)		const [inline]

Definition at line 1705 of file z3++.h.

                                                                   {
        check_context(*this, a1); 
        Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
        Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
        ctx().check_error();
        return expr(ctx(), r);
    }

expr operator()	(	int	a1,
		expr const &	a2
	)		const [inline]

Definition at line 1712 of file z3++.h.

                                                                   {
        check_context(*this, a2);
        Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
        Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
        ctx().check_error();
        return expr(ctx(), r);
    }

expr operator()	(	expr const &	a1,
		expr const &	a2,
		expr const &	a3
	)		const [inline]

Definition at line 1719 of file z3++.h.

                                                                                             {
        check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
        Z3_ast args[3] = { a1, a2, a3 };
        Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
        ctx().check_error();
        return expr(ctx(), r);
    }

expr operator()	(	expr const &	a1,
		expr const &	a2,
		expr const &	a3,
		expr const &	a4
	)		const [inline]

Definition at line 1726 of file z3++.h.

                                                                                                              {
        check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
        Z3_ast args[4] = { a1, a2, a3, a4 };
        Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
        ctx().check_error();
        return expr(ctx(), r);
    }

expr operator()	(	expr const &	a1,
		expr const &	a2,
		expr const &	a3,
		expr const &	a4,
		expr const &	a5
	)		const [inline]

Definition at line 1733 of file z3++.h.

                                                                                                                               {
        check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
        Z3_ast args[5] = { a1, a2, a3, a4, a5 };
        Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
        ctx().check_error();
        return expr(ctx(), r);
    }

func_decl& operator=

(

func_decl const &

s

)

[inline]

Definition at line 433 of file z3++.h.

{ return static_cast<func_decl&>(ast::operator=(s)); }

sort range

(

)

const [inline]

Definition at line 437 of file z3++.h.

{ Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }