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)

	operator Z3_func_decl () const

unsigned	id () const
	retrieve unique identifier for func_decl. More...

unsigned	arity () const

sort	domain (unsigned i) const

sort	range () const

symbol	name () const

Z3_decl_kind	decl_kind () const

func_decl	transitive_closure (func_decl 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

std::string	to_string () const

Public Member Functions inherited from object
	object (context &c)

context &	ctx () const

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

Constructor & Destructor Documentation

func_decl ( context & c )

inline

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

Referenced by func_decl::transitive_closure().

711 :ast(c) {}

z3::ast::ast

ast(context &c)

Definition: z3++.h:508

func_decl	(	context &	c,
		Z3_func_decl	n
	)

inline

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

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

z3::ast::ast

ast(context &c)

Definition: z3++.h:508

Member Function Documentation

unsigned arity ( ) const

inline

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

Referenced by fixedpoint::add_fact(), func_decl::domain(), and func_decl::is_const().

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

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

Z3_get_arity

unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)

Alias for Z3_get_domain_size.

Z3_decl_kind decl_kind ( ) const

inline

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

Referenced by expr::is_and(), expr::is_distinct(), expr::is_eq(), expr::is_false(), expr::is_implies(), expr::is_ite(), expr::is_not(), expr::is_or(), expr::is_true(), and expr::is_xor().

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

Z3_get_decl_kind

Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d)

Return declaration kind corresponding to declaration.

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

sort domain ( unsigned i ) const

inline

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

Referenced by func_decl::operator()().

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

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::func_decl::arity

unsigned arity() const

Definition: z3++.h:720

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

Z3_get_domain

Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i)

Return the sort of the i-th parameter of the given function declaration.

unsigned id ( ) const

inline

retrieve unique identifier for func_decl.

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

718 { unsigned r = Z3_get_func_decl_id(ctx(), *this); check_error(); return r; }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

Z3_get_func_decl_id

unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f)

Return a unique identifier for f.

bool is_const ( ) const

inline

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

730 { return arity() == 0; }

z3::func_decl::arity

unsigned arity() const

Definition: z3++.h:720

symbol name ( ) const

inline

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

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

Z3_get_decl_name

Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d)

Return the constant declaration name as a symbol.

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

operator Z3_func_decl ( ) const

inline

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

713 { return reinterpret_cast<Z3_func_decl>(m_ast); }

z3::ast::m_ast

Z3_ast m_ast

Definition: z3++.h:506

expr operator() ( ) const

inline

Definition at line 3515 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 3494 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 3505 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 3520 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 3527 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 3533 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 3540 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 3547 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 3554 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 3561 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 3568 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);
     }

sort range ( ) const

inline

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

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

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

Z3_get_range

Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)

Return the range of the given declaration.

func_decl transitive_closure ( func_decl const & )

inline

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

                                                        {
             Z3_func_decl tc = Z3_mk_transitive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc); 
         }

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation