Z3 C++ namespace. More...
Data Structures | |
class | apply_result |
class | array |
class | ast |
class | ast_vector_tpl |
class | cast_ast |
class | cast_ast< ast > |
class | cast_ast< expr > |
class | cast_ast< func_decl > |
class | cast_ast< sort > |
class | config |
Z3 global configuration object. More... | |
class | context |
A Context manages all other Z3 objects, global configuration options, etc. More... | |
class | exception |
Exception used to sign API usage errors. More... | |
class | expr |
A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort. More... | |
class | func_decl |
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... | |
class | func_entry |
class | func_interp |
class | goal |
class | model |
class | object |
class | optimize |
class | params |
class | probe |
class | solver |
class | sort |
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. More... | |
class | stats |
class | symbol |
class | tactic |
Typedefs | |
typedef ast_vector_tpl< ast > | ast_vector |
typedef ast_vector_tpl< expr > | expr_vector |
typedef ast_vector_tpl< sort > | sort_vector |
typedef ast_vector_tpl< func_decl > | func_decl_vector |
Enumerations | |
enum | check_result { unsat, sat, unknown } |
Functions | |
void | set_param (char const *param, char const *value) |
void | set_param (char const *param, bool value) |
void | set_param (char const *param, int value) |
void | reset_params () |
void | check_context (object const &a, object const &b) |
bool | eq (ast const &a, ast const &b) |
expr | implies (expr const &a, bool b) |
expr | implies (bool a, expr const &b) |
expr | pw (expr const &a, expr const &b) |
expr | pw (expr const &a, int b) |
expr | pw (int a, expr const &b) |
expr | ite (expr const &c, expr const &t, expr const &e) |
Create the if-then-else expression ite(c, t, e) More... | |
expr | to_expr (context &c, Z3_ast a) |
Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the whole C API with the C++ layer defined in this file. More... | |
sort | to_sort (context &c, Z3_sort s) |
func_decl | to_func_decl (context &c, Z3_func_decl f) |
expr | ule (expr const &a, expr const &b) |
unsigned less than or equal to operator for bitvectors. More... | |
expr | ule (expr const &a, int b) |
expr | ule (int a, expr const &b) |
expr | ult (expr const &a, expr const &b) |
unsigned less than operator for bitvectors. More... | |
expr | ult (expr const &a, int b) |
expr | ult (int a, expr const &b) |
expr | uge (expr const &a, expr const &b) |
unsigned greater than or equal to operator for bitvectors. More... | |
expr | uge (expr const &a, int b) |
expr | uge (int a, expr const &b) |
expr | ugt (expr const &a, expr const &b) |
unsigned greater than operator for bitvectors. More... | |
expr | ugt (expr const &a, int b) |
expr | ugt (int a, expr const &b) |
expr | udiv (expr const &a, expr const &b) |
unsigned division operator for bitvectors. More... | |
expr | udiv (expr const &a, int b) |
expr | udiv (int a, expr const &b) |
expr | forall (expr const &x, expr const &b) |
expr | forall (expr const &x1, expr const &x2, expr const &b) |
expr | forall (expr const &x1, expr const &x2, expr const &x3, expr const &b) |
expr | forall (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b) |
expr | forall (expr_vector const &xs, expr const &b) |
expr | exists (expr const &x, expr const &b) |
expr | exists (expr const &x1, expr const &x2, expr const &b) |
expr | exists (expr const &x1, expr const &x2, expr const &x3, expr const &b) |
expr | exists (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b) |
expr | exists (expr_vector const &xs, expr const &b) |
expr | distinct (expr_vector const &args) |
expr | concat (expr const &a, expr const &b) |
std::ostream & | operator<< (std::ostream &out, check_result r) |
check_result | to_check_result (Z3_lbool l) |
tactic | repeat (tactic const &t, unsigned max=UINT_MAX) |
tactic | with (tactic const &t, params const &p) |
tactic | try_for (tactic const &t, unsigned ms) |
tactic | fail_if (probe const &p) |
tactic | when (probe const &p, tactic const &t) |
tactic | cond (probe const &p, tactic const &t1, tactic const &t2) |
expr | to_real (expr const &a) |
func_decl | function (symbol const &name, unsigned arity, sort const *domain, sort const &range) |
func_decl | function (char const *name, unsigned arity, sort const *domain, sort const &range) |
func_decl | function (char const *name, sort const &domain, sort const &range) |
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &range) |
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &range) |
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &range) |
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &d5, sort const &range) |
expr | select (expr const &a, expr const &i) |
expr | select (expr const &a, int i) |
expr | store (expr const &a, expr const &i, expr const &v) |
expr | store (expr const &a, int i, expr const &v) |
expr | store (expr const &a, expr i, int v) |
expr | store (expr const &a, int i, int v) |
expr | const_array (sort const &d, expr const &v) |
Z3 C++ namespace.
typedef ast_vector_tpl<ast> ast_vector |
typedef ast_vector_tpl<expr> expr_vector |
typedef ast_vector_tpl<func_decl> func_decl_vector |
typedef ast_vector_tpl<sort> sort_vector |
enum check_result |
Enumerator | |
---|---|
unsat | |
sat | |
unknown |
Definition at line 281 of file z3++.h.
Referenced by goal::add(), tactic::apply(), solver::check(), object::check_error(), concat(), cond(), const_array(), apply_result::convert_model(), model::eval(), exists(), forall(), context::function(), model::get_const_interp(), model::get_func_interp(), ite(), func_decl::operator()(), pw(), select(), store(), and when().
|
inline |
Definition at line 1083 of file z3++.h.
Definition at line 1088 of file z3++.h.
Definition at line 1093 of file z3++.h.
|
inline |
Definition at line 1098 of file z3++.h.
|
inline |
Definition at line 1103 of file z3++.h.
Definition at line 1059 of file z3++.h.
Definition at line 1064 of file z3++.h.
Definition at line 1069 of file z3++.h.
|
inline |
Definition at line 1074 of file z3++.h.
|
inline |
Definition at line 1079 of file z3++.h.
Create the if-then-else expression ite(c, t, e)
Definition at line 923 of file z3++.h.
|
inline |
Definition at line 1258 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 1265 of file z3++.h.
Referenced by solver::check(), and optimize::check().
Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the whole C API with the C++ layer defined in this file.
Definition at line 936 of file z3++.h.
Referenced by udiv(), uge(), ugt(), ule(), and ult().
Definition at line 945 of file z3++.h.
Referenced by context::enumeration_sort(), and context::uninterpreted_sort().
unsigned division operator for bitvectors.
Definition at line 982 of file z3++.h.
Referenced by udiv().
unsigned greater than or equal to operator for bitvectors.
Definition at line 970 of file z3++.h.
Referenced by uge().
unsigned greater than operator for bitvectors.
Definition at line 976 of file z3++.h.
Referenced by ugt().
unsigned less than or equal to operator for bitvectors.
Definition at line 958 of file z3++.h.
Referenced by ule().
unsigned less than operator for bitvectors.
Definition at line 964 of file z3++.h.
Referenced by ult().