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...

#include <z3++.h>

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.
unsigned	arity () const
sort	domain (unsigned i) const
sort	range () const
symbol	name () const
Z3_decl_kind	decl_kind () const
unsigned	num_parameters () 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
func_decl_vector	accessors ()
Public Member Functions inherited from ast
	ast (context &c)
	ast (context &c, Z3_ast n)
	ast (ast const &s)
	~ast () override
	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)
virtual	~object ()=default
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 904 of file z3++.h.

Constructor & Destructor Documentation

func_decl() [1/2]

func_decl ( context & c )

inline

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

:ast(c) {}

Referenced by accessors(), and transitive_closure().

func_decl() [2/2]

func_decl ( context & c, Z3_func_decl n )

inline

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

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

Member Function Documentation

accessors()

func_decl_vector accessors ( )

inline

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

                                                 {
        sort s = range();
        assert(s.is_datatype());
        unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), s);
        unsigned idx = 0;
        for (; idx < n; ++idx) {
            func_decl f(ctx(), Z3_get_datatype_sort_constructor(ctx(), s, idx));
            if (id() == f.id())
                break;
        }
        assert(idx < n);
        n = arity();
        func_decl_vector as(ctx());
        for (unsigned i = 0; i < n; ++i) 
            as.push_back(func_decl(ctx(), Z3_get_datatype_sort_constructor_accessor(ctx(), s, idx, i)));
        return as;
    }

arity()

unsigned arity ( ) const

inline

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

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

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

decl_kind()

Z3_decl_kind decl_kind ( ) const

inline

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

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

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().

domain()

sort domain ( unsigned i ) const

inline

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

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

Referenced by operator()(), operator()(), and operator()().

id()

unsigned id ( ) const

inline

retrieve unique identifier for func_decl.

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

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

Referenced by accessors().

is_const()

bool is_const ( ) const

inline

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

{ return arity() == 0; }

name()

symbol name ( ) const

inline

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

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

num_parameters()

unsigned num_parameters ( ) const

inline

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

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

Referenced by parameter::parameter().

operator Z3_func_decl()

operator Z3_func_decl ( ) const

inline

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

{ return reinterpret_cast<Z3_func_decl>(m_ast); }

operator()() [1/11]

expr operator() ( ) const

inline

Definition at line 4220 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() ( expr const & a ) const

inline

Definition at line 4225 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()() [3/11]

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

inline

Definition at line 4238 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()() [4/11]

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

inline

Definition at line 4259 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()() [5/11]

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

inline

Definition at line 4266 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()() [6/11]

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

inline

Definition at line 4273 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()() [7/11]

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

inline

Definition at line 4245 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() ( expr_vector const & v ) const

inline

Definition at line 4210 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()() [9/11]

expr operator() ( int a ) const

inline

Definition at line 4232 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()() [10/11]

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

inline

Definition at line 4252 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()() [11/11]

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

inline

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

range()

sort range ( ) const

inline

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

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

Referenced by accessors().

transitive_closure()

func_decl transitive_closure ( func_decl const & )

inline

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

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