Z3
Public Member Functions
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_decloperator= (func_decl const &s)
 
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
 
astoperator= (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)
 
 object (object const &s)
 
contextctx () const
 
Z3_error_code check_error () const
 

Additional Inherited Members

- Protected Attributes inherited from ast
Z3_ast m_ast
 
- Protected Attributes inherited from object
contextm_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 698 of file z3++.h.

Constructor & Destructor Documentation

◆ func_decl() [1/3]

func_decl ( context c)
inline

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

700 :ast(c) {}

Referenced by func_decl::transitive_closure().

◆ func_decl() [2/3]

func_decl ( context c,
Z3_func_decl  n 
)
inline

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

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

◆ func_decl() [3/3]

func_decl ( func_decl const &  s)
inline

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

702 :ast(s) {}

Member Function Documentation

◆ arity()

unsigned arity ( ) const
inline

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

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

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

◆ decl_kind()

Z3_decl_kind decl_kind ( ) const
inline

◆ domain()

sort domain ( unsigned  i) const
inline

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

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

Referenced by func_decl::operator()().

◆ id()

unsigned id ( ) const
inline

retrieve unique identifier for func_decl.

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

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

◆ is_const()

bool is_const ( ) const
inline

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

721 { return arity() == 0; }

◆ name()

symbol name ( ) const
inline

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

714 { 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 703 of file z3++.h.

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

◆ operator()() [1/11]

expr operator() ( ) const
inline

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

3236  {
3237  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
3238  ctx().check_error();
3239  return expr(ctx(), r);
3240  }

◆ operator()() [2/11]

expr operator() ( expr const &  a) const
inline

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

3241  {
3242  check_context(*this, a);
3243  Z3_ast args[1] = { a };
3244  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
3245  ctx().check_error();
3246  return expr(ctx(), r);
3247  }

◆ operator()() [3/11]

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

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

3254  {
3255  check_context(*this, a1); check_context(*this, a2);
3256  Z3_ast args[2] = { a1, a2 };
3257  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3258  ctx().check_error();
3259  return expr(ctx(), r);
3260  }

◆ operator()() [4/11]

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

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

3275  {
3276  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
3277  Z3_ast args[3] = { a1, a2, a3 };
3278  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
3279  ctx().check_error();
3280  return expr(ctx(), r);
3281  }

◆ operator()() [5/11]

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

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

3282  {
3283  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
3284  Z3_ast args[4] = { a1, a2, a3, a4 };
3285  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
3286  ctx().check_error();
3287  return expr(ctx(), r);
3288  }

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

3289  {
3290  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
3291  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3292  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
3293  ctx().check_error();
3294  return expr(ctx(), r);
3295  }

◆ operator()() [7/11]

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

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

3261  {
3262  check_context(*this, a1);
3263  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3264  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3265  ctx().check_error();
3266  return expr(ctx(), r);
3267  }

◆ operator()() [8/11]

expr operator() ( expr_vector const &  v) const
inline

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

3226  {
3227  array<Z3_ast> _args(args.size());
3228  for (unsigned i = 0; i < args.size(); i++) {
3229  check_context(*this, args[i]);
3230  _args[i] = args[i];
3231  }
3232  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
3233  check_error();
3234  return expr(ctx(), r);
3235  }

◆ operator()() [9/11]

expr operator() ( int  a) const
inline

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

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

◆ operator()() [10/11]

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

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

3268  {
3269  check_context(*this, a2);
3270  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3271  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
3272  ctx().check_error();
3273  return expr(ctx(), r);
3274  }

◆ operator()() [11/11]

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

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

3215  {
3216  array<Z3_ast> _args(n);
3217  for (unsigned i = 0; i < n; i++) {
3218  check_context(*this, args[i]);
3219  _args[i] = args[i];
3220  }
3221  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
3222  check_error();
3223  return expr(ctx(), r);
3224 
3225  }

◆ operator=()

func_decl& operator= ( func_decl const &  s)
inline

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

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

◆ range()

sort range ( ) const
inline

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

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

◆ transitive_closure()

func_decl transitive_closure ( func_decl const &  )
inline

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

717  {
718  Z3_func_decl tc = Z3_mk_transitive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc);
719  }
z3::func_decl::func_decl
func_decl(context &c)
Definition: z3++.h:700
z3::func_decl::domain
sort domain(unsigned i) const
Definition: z3++.h:712
Z3_mk_app
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
z3::ast::m_ast
Z3_ast m_ast
Definition: z3++.h:498
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.
Z3_get_arity
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.
Z3_get_range
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:422
z3::ast::ast
ast(context &c)
Definition: z3++.h:500
z3::func_decl::arity
unsigned arity() const
Definition: z3++.h:711
z3::context::num_val
expr num_val(int n, sort const &s)
Definition: z3++.h:3213
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_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_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.
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:419
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:187
z3::object::ctx
context & ctx() const
Definition: z3++.h:418
Z3_mk_transitive_closure
Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f)
create transitive closure of binary relation.