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 | fixedpoint |
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 | param_descrs |
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 } |
enum | rounding_mode { RNA , RNE , RTP , RTN , RTZ } |
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 () |
std::ostream & | operator<< (std::ostream &out, exception const &e) |
check_result | to_check_result (Z3_lbool l) |
void | check_context (object const &a, object const &b) |
std::ostream & | operator<< (std::ostream &out, symbol const &s) |
std::ostream & | operator<< (std::ostream &out, param_descrs const &d) |
std::ostream & | operator<< (std::ostream &out, params const &p) |
std::ostream & | operator<< (std::ostream &out, ast const &n) |
bool | eq (ast const &a, ast const &b) |
expr | select (expr const &a, expr const &i) |
forward declarations More... | |
expr | select (expr const &a, expr_vector const &i) |
expr | implies (expr const &a, expr 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 | mod (expr const &a, expr const &b) |
expr | mod (expr const &a, int b) |
expr | mod (int a, expr const &b) |
expr | operator% (expr const &a, expr const &b) |
expr | operator% (expr const &a, int b) |
expr | operator% (int a, expr const &b) |
expr | rem (expr const &a, expr const &b) |
expr | rem (expr const &a, int b) |
expr | rem (int a, expr const &b) |
expr | operator! (expr const &a) |
expr | is_int (expr const &e) |
expr | operator&& (expr const &a, expr const &b) |
expr | operator&& (expr const &a, bool b) |
expr | operator&& (bool a, expr const &b) |
expr | operator|| (expr const &a, expr const &b) |
expr | operator|| (expr const &a, bool b) |
expr | operator|| (bool a, expr const &b) |
expr | operator== (expr const &a, expr const &b) |
expr | operator== (expr const &a, int b) |
expr | operator== (int a, expr const &b) |
expr | operator!= (expr const &a, expr const &b) |
expr | operator!= (expr const &a, int b) |
expr | operator!= (int a, expr const &b) |
expr | operator+ (expr const &a, expr const &b) |
expr | operator+ (expr const &a, int b) |
expr | operator+ (int a, expr const &b) |
expr | operator* (expr const &a, expr const &b) |
expr | operator* (expr const &a, int b) |
expr | operator* (int a, expr const &b) |
expr | operator>= (expr const &a, expr const &b) |
expr | operator/ (expr const &a, expr const &b) |
expr | operator/ (expr const &a, int b) |
expr | operator/ (int a, expr const &b) |
expr | operator- (expr const &a) |
expr | operator- (expr const &a, expr const &b) |
expr | operator- (expr const &a, int b) |
expr | operator- (int a, expr const &b) |
expr | operator<= (expr const &a, expr const &b) |
expr | operator<= (expr const &a, int b) |
expr | operator<= (int a, expr const &b) |
expr | operator>= (expr const &a, int b) |
expr | operator>= (int a, expr const &b) |
expr | operator< (expr const &a, expr const &b) |
expr | operator< (expr const &a, int b) |
expr | operator< (int a, expr const &b) |
expr | operator> (expr const &a, expr const &b) |
expr | operator> (expr const &a, int b) |
expr | operator> (int a, expr const &b) |
expr | operator& (expr const &a, expr const &b) |
expr | operator& (expr const &a, int b) |
expr | operator& (int a, expr const &b) |
expr | operator^ (expr const &a, expr const &b) |
expr | operator^ (expr const &a, int b) |
expr | operator^ (int a, expr const &b) |
expr | operator| (expr const &a, expr const &b) |
expr | operator| (expr const &a, int b) |
expr | operator| (int a, expr const &b) |
expr | nand (expr const &a, expr const &b) |
expr | nor (expr const &a, expr const &b) |
expr | xnor (expr const &a, expr const &b) |
expr | min (expr const &a, expr const &b) |
expr | max (expr const &a, expr const &b) |
expr | abs (expr const &a) |
expr | sqrt (expr const &a, expr const &rm) |
expr | operator~ (expr const &a) |
expr | fma (expr const &a, expr const &b, expr const &c, expr const &rm) |
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 | sle (expr const &a, expr const &b) |
signed less than or equal to operator for bitvectors. More... | |
expr | sle (expr const &a, int b) |
expr | sle (int a, expr const &b) |
expr | slt (expr const &a, expr const &b) |
signed less than operator for bitvectors. More... | |
expr | slt (expr const &a, int b) |
expr | slt (int a, expr const &b) |
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 | srem (expr const &a, expr const &b) |
signed remainder operator for bitvectors More... | |
expr | srem (expr const &a, int b) |
expr | srem (int a, expr const &b) |
expr | smod (expr const &a, expr const &b) |
signed modulus operator for bitvectors More... | |
expr | smod (expr const &a, int b) |
expr | smod (int a, expr const &b) |
expr | urem (expr const &a, expr const &b) |
unsigned reminder operator for bitvectors More... | |
expr | urem (expr const &a, int b) |
expr | urem (int a, expr const &b) |
expr | shl (expr const &a, expr const &b) |
shift left operator for bitvectors More... | |
expr | shl (expr const &a, int b) |
expr | shl (int a, expr const &b) |
expr | lshr (expr const &a, expr const &b) |
logic shift right operator for bitvectors More... | |
expr | lshr (expr const &a, int b) |
expr | lshr (int a, expr const &b) |
expr | ashr (expr const &a, expr const &b) |
arithmetic shift right operator for bitvectors More... | |
expr | ashr (expr const &a, int b) |
expr | ashr (int a, expr const &b) |
expr | zext (expr const &a, unsigned i) |
Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector. More... | |
expr | bv2int (expr const &a, bool is_signed) |
bit-vector and integer conversions. More... | |
expr | int2bv (unsigned n, expr const &a) |
expr | bvadd_no_overflow (expr const &a, expr const &b, bool is_signed) |
bit-vector overflow/underflow checks More... | |
expr | bvadd_no_underflow (expr const &a, expr const &b) |
expr | bvsub_no_overflow (expr const &a, expr const &b) |
expr | bvsub_no_underflow (expr const &a, expr const &b, bool is_signed) |
expr | bvsdiv_no_overflow (expr const &a, expr const &b) |
expr | bvneg_no_overflow (expr const &a) |
expr | bvmul_no_overflow (expr const &a, expr const &b, bool is_signed) |
expr | bvmul_no_underflow (expr const &a, expr const &b) |
expr | sext (expr const &a, unsigned i) |
Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector. More... | |
func_decl | linear_order (sort const &a, unsigned index) |
func_decl | partial_order (sort const &a, unsigned index) |
func_decl | piecewise_linear_order (sort const &a, unsigned index) |
func_decl | tree_order (sort const &a, unsigned index) |
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 | lambda (expr const &x, expr const &b) |
expr | lambda (expr const &x1, expr const &x2, expr const &b) |
expr | lambda (expr const &x1, expr const &x2, expr const &x3, expr const &b) |
expr | lambda (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b) |
expr | lambda (expr_vector const &xs, expr const &b) |
expr | pble (expr_vector const &es, int const *coeffs, int bound) |
expr | pbge (expr_vector const &es, int const *coeffs, int bound) |
expr | pbeq (expr_vector const &es, int const *coeffs, int bound) |
expr | atmost (expr_vector const &es, unsigned bound) |
expr | atleast (expr_vector const &es, unsigned bound) |
expr | sum (expr_vector const &args) |
expr | distinct (expr_vector const &args) |
expr | concat (expr const &a, expr const &b) |
expr | concat (expr_vector const &args) |
expr | mk_or (expr_vector const &args) |
expr | mk_and (expr_vector const &args) |
std::ostream & | operator<< (std::ostream &out, model const &m) |
std::ostream & | operator<< (std::ostream &out, stats const &s) |
std::ostream & | operator<< (std::ostream &out, check_result r) |
std::ostream & | operator<< (std::ostream &out, solver const &s) |
std::ostream & | operator<< (std::ostream &out, goal const &g) |
std::ostream & | operator<< (std::ostream &out, apply_result const &r) |
tactic | operator& (tactic const &t1, tactic const &t2) |
tactic | operator| (tactic const &t1, tactic const &t2) |
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 | par_or (unsigned n, tactic const *tactics) |
tactic | par_and_then (tactic const &t1, tactic const &t2) |
probe | operator<= (probe const &p1, probe const &p2) |
probe | operator<= (probe const &p1, double p2) |
probe | operator<= (double p1, probe const &p2) |
probe | operator>= (probe const &p1, probe const &p2) |
probe | operator>= (probe const &p1, double p2) |
probe | operator>= (double p1, probe const &p2) |
probe | operator< (probe const &p1, probe const &p2) |
probe | operator< (probe const &p1, double p2) |
probe | operator< (double p1, probe const &p2) |
probe | operator> (probe const &p1, probe const &p2) |
probe | operator> (probe const &p1, double p2) |
probe | operator> (double p1, probe const &p2) |
probe | operator== (probe const &p1, probe const &p2) |
probe | operator== (probe const &p1, double p2) |
probe | operator== (double p1, probe const &p2) |
probe | operator&& (probe const &p1, probe const &p2) |
probe | operator|| (probe const &p1, probe const &p2) |
probe | operator! (probe const &p) |
std::ostream & | operator<< (std::ostream &out, optimize const &s) |
std::ostream & | operator<< (std::ostream &out, fixedpoint const &f) |
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) |
func_decl | function (char const *name, sort_vector const &domain, sort const &range) |
func_decl | function (std::string const &name, sort_vector const &domain, sort const &range) |
func_decl | recfun (symbol const &name, unsigned arity, sort const *domain, sort const &range) |
func_decl | recfun (char const *name, unsigned arity, sort const *domain, sort const &range) |
func_decl | recfun (char const *name, sort const &d1, sort const &range) |
func_decl | recfun (char const *name, sort const &d1, sort const &d2, sort const &range) |
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 | store (expr const &a, expr_vector const &i, expr const &v) |
expr | as_array (func_decl &f) |
expr | const_array (sort const &d, expr const &v) |
expr | empty_set (sort const &s) |
expr | full_set (sort const &s) |
expr | set_add (expr const &s, expr const &e) |
expr | set_del (expr const &s, expr const &e) |
expr | set_union (expr const &a, expr const &b) |
expr | set_intersect (expr const &a, expr const &b) |
expr | set_difference (expr const &a, expr const &b) |
expr | set_complement (expr const &a) |
expr | set_member (expr const &s, expr const &e) |
expr | set_subset (expr const &a, expr const &b) |
expr | empty (sort const &s) |
expr | suffixof (expr const &a, expr const &b) |
expr | prefixof (expr const &a, expr const &b) |
expr | indexof (expr const &s, expr const &substr, expr const &offset) |
expr | last_indexof (expr const &s, expr const &substr) |
expr | to_re (expr const &s) |
expr | in_re (expr const &s, expr const &re) |
expr | plus (expr const &re) |
expr | option (expr const &re) |
expr | star (expr const &re) |
expr | re_empty (sort const &s) |
expr | re_full (sort const &s) |
expr | re_intersect (expr_vector const &args) |
expr | re_complement (expr const &a) |
expr | range (expr const &lo, expr const &hi) |
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 |
enum rounding_mode |
Definition at line 1606 of file z3++.h.
Definition at line 3293 of file z3++.h.
arithmetic shift right operator for bitvectors
Definition at line 1760 of file z3++.h.
Referenced by ashr().
|
inline |
Definition at line 2040 of file z3++.h.
|
inline |
Definition at line 2032 of file z3++.h.
bit-vector overflow/underflow checks
Definition at line 1778 of file z3++.h.
Definition at line 1781 of file z3++.h.
Definition at line 1796 of file z3++.h.
Definition at line 1799 of file z3++.h.
Definition at line 1790 of file z3++.h.
Definition at line 1784 of file z3++.h.
Definition at line 1787 of file z3++.h.
Definition at line 410 of file z3++.h.
Referenced by cond(), exists(), fma(), forall(), context::function(), indexof(), lambda(), last_indexof(), prefixof(), context::recdef(), context::recfun(), select(), set_intersect(), set_union(), store(), suffixof(), and when().
Definition at line 2066 of file z3++.h.
|
inline |
Definition at line 2084 of file z3++.h.
Definition at line 2898 of file z3++.h.
|
inline |
Definition at line 2057 of file z3++.h.
Definition at line 3366 of file z3++.h.
Definition at line 1959 of file z3++.h.
Definition at line 1964 of file z3++.h.
Definition at line 1969 of file z3++.h.
|
inline |
Definition at line 1974 of file z3++.h.
|
inline |
Definition at line 1979 of file z3++.h.
Definition at line 2887 of file z3++.h.
Definition at line 1631 of file z3++.h.
Definition at line 1935 of file z3++.h.
Definition at line 1940 of file z3++.h.
Definition at line 1945 of file z3++.h.
|
inline |
Definition at line 1950 of file z3++.h.
|
inline |
Definition at line 1955 of file z3++.h.
|
inline |
Definition at line 3233 of file z3++.h.
|
inline |
|
inline |
Definition at line 3383 of file z3++.h.
Create the if-then-else expression ite(c, t, e)
Definition at line 1645 of file z3++.h.
Definition at line 1983 of file z3++.h.
|
inline |
|
inline |
Definition at line 2003 of file z3++.h.
Definition at line 3389 of file z3++.h.
Definition at line 1591 of file z3++.h.
Referenced by Context::repeat().
Definition at line 1576 of file z3++.h.
|
inline |
Definition at line 2116 of file z3++.h.
|
inline |
Definition at line 2110 of file z3++.h.
Definition at line 1273 of file z3++.h.
Referenced by operator%().
Definition at line 2751 of file z3++.h.
|
inline |
Definition at line 1347 of file z3++.h.
|
inline |
|
inline |
Definition at line 2632 of file z3++.h.
Definition at line 1323 of file z3++.h.
Definition at line 1322 of file z3++.h.
Definition at line 1313 of file z3++.h.
Definition at line 2745 of file z3++.h.
Definition at line 1387 of file z3++.h.
Definition at line 1357 of file z3++.h.
Definition at line 1450 of file z3++.h.
Definition at line 1469 of file z3++.h.
Definition at line 1428 of file z3++.h.
Definition at line 1517 of file z3++.h.
Definition at line 2730 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 1492 of file z3++.h.
Definition at line 2720 of file z3++.h.
Definition at line 2740 of file z3++.h.
Definition at line 1539 of file z3++.h.
Definition at line 2735 of file z3++.h.
Definition at line 1411 of file z3++.h.
Definition at line 2725 of file z3++.h.
Definition at line 2639 of file z3++.h.
Definition at line 1336 of file z3++.h.
Definition at line 1334 of file z3++.h.
Definition at line 1325 of file z3++.h.
Definition at line 2748 of file z3++.h.
Definition at line 2671 of file z3++.h.
|
inline |
Definition at line 2024 of file z3++.h.
|
inline |
Definition at line 2016 of file z3++.h.
|
inline |
Definition at line 2008 of file z3++.h.
Definition at line 3377 of file z3++.h.
Definition at line 3431 of file z3++.h.
Referenced by AstVector::__getitem__(), z3py::AndThen(), z3py::ArraySort(), Goal::as_expr(), ApplyResult::as_expr(), FuncEntry::as_list(), FuncInterp::as_list(), z3py::AtLeast(), z3py::BoolVector(), Solver::check(), Optimize::check(), ExprRef::children(), z3py::Concat(), Solver::consequences(), z3py::CreateDatatypes(), ModelRef::decls(), z3py::describe_probes(), z3py::DisjointSum(), z3py::EnumSort(), z3py::eq(), z3py::Function(), context::function(), function(), Statistics::get_key_value(), z3py::Intersect(), z3py::IntVector(), z3py::is_quantifier(), Statistics::keys(), z3py::Lambda(), Context::mkArrayConst(), Context::mkArraySort(), Context::mkConst(), Context::mkConstDecl(), Context::mkFreshConst(), Context::mkFreshConstDecl(), Context::mkFreshFuncDecl(), Context::mkFuncDecl(), z3py::OrElse(), z3py::ParOr(), z3py::probes(), z3py::RealVarVector(), z3py::RealVector(), z3py::RecAddDefinition(), context::recfun(), recfun(), z3py::RecFunction(), AstVector::resize(), z3py::set_default_fp_sort(), Fixedpoint::set_predicate_representation(), ModelRef::sorts(), z3py::substitute(), z3py::substitute_vars(), z3py::tactics(), Solver::to_smt2(), z3py::TupleSort(), and z3py::Union().
Definition at line 3410 of file z3++.h.
Definition at line 3415 of file z3++.h.
|
inline |
Definition at line 3420 of file z3++.h.
|
inline |
Definition at line 3252 of file z3++.h.
Definition at line 1289 of file z3++.h.
|
inline |
Definition at line 78 of file z3++.h.
forward declarations
Definition at line 3256 of file z3++.h.
Referenced by expr::operator[](), and select().
|
inline |
Definition at line 3265 of file z3++.h.
Definition at line 3338 of file z3++.h.
|
inline |
|
inline |
Definition at line 75 of file z3++.h.
|
inline |
Definition at line 77 of file z3++.h.
Definition at line 3330 of file z3++.h.
Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
Definition at line 1807 of file z3++.h.
Definition at line 1622 of file z3++.h.
Definition at line 3273 of file z3++.h.
Referenced by store().
|
inline |
Definition at line 3285 of file z3++.h.
Definition at line 3371 of file z3++.h.
|
inline |
Definition at line 2048 of file z3++.h.
|
inline |
Definition at line 141 of file z3++.h.
Referenced by solver::check(), optimize::check(), solver::consequences(), and fixedpoint::query().
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 1658 of file z3++.h.
Referenced by ashr(), lshr(), sext(), shl(), sle(), slt(), smod(), srem(), udiv(), uge(), ugt(), ule(), ult(), urem(), and zext().
Definition at line 1672 of file z3++.h.
Referenced by linear_order(), partial_order(), piecewise_linear_order(), and tree_order().
Definition at line 1667 of file z3++.h.
Referenced by context::enumeration_sort(), context::tuple_sort(), and context::uninterpreted_sort().
Definition at line 2657 of file z3++.h.
Definition at line 2892 of file z3++.h.
Definition at line 2652 of file z3++.h.
Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
Definition at line 1767 of file z3++.h.