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
Public Member Functions inherited from ast
	ast (context &c)
	ast (context &c, Z3_ast n)
	ast (ast const &s)
	~ast ()
	operator Z3_ast () const
	operator bool () const
ast &	operator= (ast const &s)
Z3_ast_kind	kind () const
unsigned	hash () const
Public Member Functions inherited from object
	object (context &c)
	object (object const &s)
context &	ctx () const
void	check_error () const

Additional Inherited Members
Protected Attributes inherited from ast
Z3_ast	m_ast
Protected Attributes inherited from object
context *	m_ctx

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 527 of file z3++.h.

Constructor & Destructor Documentation

func_decl() [1/3]

func_decl ( context &  c )

inline

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

:ast(c) {}

func_decl() [2/3]

func_decl ( context &  c, Z3_func_decl  n  )

inline

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

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

func_decl() [3/3]

func_decl ( func_decl const &  s )

inline

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

:ast(s) {}

Member Function Documentation

arity()

unsigned arity ( ) const

inline

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

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

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

decl_kind()

Z3_decl_kind decl_kind ( ) const

inline

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

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

domain()

sort domain ( unsigned  i ) const

inline

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

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

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

is_const()

bool is_const ( ) const

inline

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

{ return arity() == 0; }

name()

symbol name ( ) const

inline

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

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

operator Z3_func_decl()

operator Z3_func_decl ( ) const

inline

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

{ return reinterpret_cast<Z3_func_decl>(m_ast); }

operator()() [1/11]

expr operator() ( ) const

inline

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

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

operator()() [2/11]

expr operator() ( unsigned  n, expr const *  args  ) const

inline

Definition at line 2223 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);

    }

operator()() [3/11]

expr operator() ( expr_vector const &  v ) const

inline

Definition at line 2234 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);
    }

operator()() [4/11]

expr operator() ( expr const &  a ) const

inline

Definition at line 2249 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);
    }

operator()() [5/11]

expr operator() ( int  a ) const

inline

Definition at line 2256 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);
    }

operator()() [6/11]

expr operator() ( expr const &  a1, expr const &  a2  ) const

inline

Definition at line 2262 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);
    }

operator()() [7/11]

expr operator() ( expr const &  a1, int  a2  ) const

inline

Definition at line 2269 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);
    }

operator()() [8/11]

expr operator() ( int  a1, expr const &  a2  ) const

inline

Definition at line 2276 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);
    }

operator()() [9/11]

expr operator() ( expr const &  a1, expr const &  a2, expr const &  a3  ) const

inline

Definition at line 2283 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);
    }

operator()() [10/11]

expr operator() ( expr const &  a1, expr const &  a2, expr const &  a3, expr const &  a4  ) const

inline

Definition at line 2290 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);
    }

operator()() [11/11]

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

inline

Definition at line 2297 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);
    }

operator=()

func_decl& operator= ( func_decl const &  s )

inline

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

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

range()

sort range ( ) const

inline

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

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