RetroSearch Browse

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/classz3_1_1func__decl.html below:

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

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 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 () 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 object (context &c) virtual ~object ()=default context & ctx () const Z3_error_code check_error () const

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

◆ func_decl() [1/2] ◆ func_decl() [2/2] ◆ accessors()

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

4212

assert(s.is_datatype());

4215 for

(; idx < n; ++idx) {

4217 if

(

id

() == f.id())

4223 for

(

unsigned

i = 0; i < n; ++i)

unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)

Return number of constructors for datatype.

Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)

Return idx'th constructor.

Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c, Z3_sort t, unsigned idx_c, unsigned idx_a)

Return idx_a'th accessor for the idx_c'th constructor.

ast_vector_tpl< func_decl > func_decl_vector

◆ arity() ◆ decl_kind()

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

Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d)

Return declaration kind corresponding to declaration.

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

Z3_error_code check_error() const

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.

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

◆ id()

retrieve unique identifier for func_decl.

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

unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f)

Return a unique identifier for f.

Referenced by func_decl::accessors().

◆ is_const() ◆ name() ◆ num_parameters() unsigned num_parameters ( ) const inline

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

unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)

Return the number of parameters associated with a declaration.

Referenced by parameter::parameter().

◆ operator Z3_func_decl() operator Z3_func_decl ( ) const inline

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

System.IntPtr Z3_func_decl

◆ operator()() [1/11] expr operator() ( ) const inline

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

3853 return

expr(

ctx

(), r);

Z3_error_code check_error() const

Auxiliary method used to check for API usage errors.

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.

◆ operator()() [2/11] expr operator() ( expr const & a ) const inline

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

3860 return

expr(

ctx

(), r);

friend void check_context(object const &a, object const &b)

◆ operator()() [3/11]

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

3870 Z3_ast

args[2] = { a1, a2 };

3873 return

expr(

ctx

(), r);

◆ operator()() [4/11]

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

3891 Z3_ast

args[3] = { a1, a2, a3 };

3894 return

expr(

ctx

(), r);

◆ operator()() [5/11]

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

3898 Z3_ast

args[4] = { a1, a2, a3, a4 };

3901 return

expr(

ctx

(), r);

◆ operator()() [6/11]

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

3905 Z3_ast

args[5] = { a1, a2, a3, a4, a5 };

3908 return

expr(

ctx

(), r);

◆ operator()() [7/11] expr operator() ( expr const & a1, int a2 ) const inline

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

3880 return

expr(

ctx

(), r);

expr num_val(int n, sort const &s)

sort domain(unsigned i) const

◆ operator()() [8/11]

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

3841

array<Z3_ast> _args(args.size());

3842 for

(

unsigned

i = 0; i < args.size(); i++) {

3848 return

expr(

ctx

(), r);

◆ operator()() [9/11] expr operator() ( int a ) const inline

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

3866 return

expr(

ctx

(), r);

◆ operator()() [10/11] expr operator() ( int a1, expr const & a2 ) const inline

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

3887 return

expr(

ctx

(), r);

◆ operator()() [11/11] expr operator() ( unsigned n, expr const * args ) const inline

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

3830

array<Z3_ast> _args(n);

3831 for

(

unsigned

i = 0; i < n; i++) {

3837 return

expr(

ctx

(), r);

◆ range()

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

Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)

Return the range of the given declaration.

Referenced by func_decl::accessors().

◆ transitive_closure()

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

Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f)

create transitive closure of binary relation.

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4