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 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
 
astoperator= (ast const &s)
 
Z3_ast_kind kind () const
 
unsigned hash () const
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void 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 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.

529 :ast(c) {}
ast(context &c)
Definition: z3++.h:413

§ func_decl() [2/3]

func_decl ( context c,
Z3_func_decl  n 
)
inline

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

530 :ast(c, reinterpret_cast<Z3_ast>(n)) {}
ast(context &c)
Definition: z3++.h:413

§ func_decl() [3/3]

func_decl ( func_decl const &  s)
inline

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

531 :ast(s) {}
ast(context &c)
Definition: z3++.h:413

Member Function Documentation

§ arity()

unsigned arity ( ) const
inline

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

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

535 { return Z3_get_arity(ctx(), *this); }
context & ctx() const
Definition: z3++.h:332

§ decl_kind()

Z3_decl_kind decl_kind ( ) const
inline

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

539 { return Z3_get_decl_kind(ctx(), *this); }
context & ctx() const
Definition: z3++.h:332

§ domain()

sort domain ( unsigned  i) const
inline

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

Referenced by FuncDeclRef::__call__().

536 { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
context & ctx() const
Definition: z3++.h:332
unsigned arity() const
Definition: z3++.h:535
void check_error() const
Definition: z3++.h:333

§ is_const()

bool is_const ( ) const
inline

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

541 { return arity() == 0; }
unsigned arity() const
Definition: z3++.h:535

§ name()

symbol name ( ) const
inline

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

538 { Z3_symbol s = Z3_get_decl_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ operator Z3_func_decl()

operator Z3_func_decl ( ) const
inline

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

532 { return reinterpret_cast<Z3_func_decl>(m_ast); }
Z3_ast m_ast
Definition: z3++.h:411

§ operator()() [1/11]

expr operator() ( ) const
inline

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

2244  {
2245  Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
2246  ctx().check_error();
2247  return expr(ctx(), r);
2248  }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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.
context & ctx() const
Definition: z3++.h:332

§ operator()() [2/11]

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

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

2223  {
2224  array<Z3_ast> _args(n);
2225  for (unsigned i = 0; i < n; i++) {
2226  check_context(*this, args[i]);
2227  _args[i] = args[i];
2228  }
2229  Z3_ast r = Z3_mk_app(ctx(), *this, n, _args.ptr());
2230  check_error();
2231  return expr(ctx(), r);
2232 
2233  }
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.
context & ctx() const
Definition: z3++.h:332
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
void check_error() const
Definition: z3++.h:333

§ operator()() [3/11]

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

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

2234  {
2235  array<Z3_ast> _args(args.size());
2236  for (unsigned i = 0; i < args.size(); i++) {
2237  check_context(*this, args[i]);
2238  _args[i] = args[i];
2239  }
2240  Z3_ast r = Z3_mk_app(ctx(), *this, args.size(), _args.ptr());
2241  check_error();
2242  return expr(ctx(), r);
2243  }
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.
context & ctx() const
Definition: z3++.h:332
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
void check_error() const
Definition: z3++.h:333

§ operator()() [4/11]

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

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

2249  {
2250  check_context(*this, a);
2251  Z3_ast args[1] = { a };
2252  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
2253  ctx().check_error();
2254  return expr(ctx(), r);
2255  }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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.
context & ctx() const
Definition: z3++.h:332
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator()() [5/11]

expr operator() ( int  a) const
inline

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

2256  {
2257  Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
2258  Z3_ast r = Z3_mk_app(ctx(), *this, 1, args);
2259  ctx().check_error();
2260  return expr(ctx(), r);
2261  }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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.
sort domain(unsigned i) const
Definition: z3++.h:536
context & ctx() const
Definition: z3++.h:332
expr num_val(int n, sort const &s)
Definition: z3++.h:2221

§ operator()() [6/11]

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

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

2262  {
2263  check_context(*this, a1); check_context(*this, a2);
2264  Z3_ast args[2] = { a1, a2 };
2265  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2266  ctx().check_error();
2267  return expr(ctx(), r);
2268  }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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.
context & ctx() const
Definition: z3++.h:332
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator()() [7/11]

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

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

2269  {
2270  check_context(*this, a1);
2271  Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
2272  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2273  ctx().check_error();
2274  return expr(ctx(), r);
2275  }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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.
sort domain(unsigned i) const
Definition: z3++.h:536
context & ctx() const
Definition: z3++.h:332
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
expr num_val(int n, sort const &s)
Definition: z3++.h:2221

§ operator()() [8/11]

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

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

2276  {
2277  check_context(*this, a2);
2278  Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
2279  Z3_ast r = Z3_mk_app(ctx(), *this, 2, args);
2280  ctx().check_error();
2281  return expr(ctx(), r);
2282  }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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.
sort domain(unsigned i) const
Definition: z3++.h:536
context & ctx() const
Definition: z3++.h:332
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
expr num_val(int n, sort const &s)
Definition: z3++.h:2221

§ operator()() [9/11]

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

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

2283  {
2284  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3);
2285  Z3_ast args[3] = { a1, a2, a3 };
2286  Z3_ast r = Z3_mk_app(ctx(), *this, 3, args);
2287  ctx().check_error();
2288  return expr(ctx(), r);
2289  }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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.
context & ctx() const
Definition: z3++.h:332
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336

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

2290  {
2291  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4);
2292  Z3_ast args[4] = { a1, a2, a3, a4 };
2293  Z3_ast r = Z3_mk_app(ctx(), *this, 4, args);
2294  ctx().check_error();
2295  return expr(ctx(), r);
2296  }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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.
context & ctx() const
Definition: z3++.h:332
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336

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

2297  {
2298  check_context(*this, a1); check_context(*this, a2); check_context(*this, a3); check_context(*this, a4); check_context(*this, a5);
2299  Z3_ast args[5] = { a1, a2, a3, a4, a5 };
2300  Z3_ast r = Z3_mk_app(ctx(), *this, 5, args);
2301  ctx().check_error();
2302  return expr(ctx(), r);
2303  }
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
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.
context & ctx() const
Definition: z3++.h:332
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator=()

func_decl& operator= ( func_decl const &  s)
inline

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

533 { return static_cast<func_decl&>(ast::operator=(s)); }
func_decl(context &c)
Definition: z3++.h:529
ast & operator=(ast const &s)
Definition: z3++.h:419

§ range()

sort range ( ) const
inline

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

537 { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333