Showing content from https://z3prover.github.io/api/html/namespacez3.html below:
Z3: z3 Namespace Reference
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, double b) expr operator== (double 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, double b) expr operator!= (double 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 bvredor (expr const &a) expr bvredand (expr const &a) expr abs (expr const &a) expr sqrt (expr const &a, expr const &rm) expr fp_eq (expr const &a, expr const &b) expr operator~ (expr const &a) expr fma (expr const &a, expr const &b, expr const &c, expr const &rm) expr fpa_fp (expr const &sgn, expr const &exp, expr const &sig) expr fpa_to_sbv (expr const &t, unsigned sz) expr fpa_to_ubv (expr const &t, unsigned sz) expr sbv_to_fpa (expr const &t, sort s) expr ubv_to_fpa (expr const &t, sort s) expr fpa_to_fpa (expr const &t, sort s) expr round_fpa_to_closest_integer (expr const &t) 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 sge (expr const &a, expr const &b) signed greater than or equal to operator for bitvectors. More...
expr sge (expr const &a, int b) expr sge (int a, expr const &b) expr sgt (expr const &a, expr const &b) signed greater than operator for bitvectors. More...
expr sgt (expr const &a, int b) expr sgt (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 map (expr const &f, expr const &list) expr mapi (expr const &f, expr const &i, expr const &list) expr foldl (expr const &f, expr const &a, expr const &list) expr foldli (expr const &f, expr const &i, expr const &a, expr const &list) expr mk_or (expr_vector const &args) expr mk_and (expr_vector const &args) expr mk_xor (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) simplifier operator& (simplifier const &t1, simplifier const &t2) simplifier with (simplifier const &t, params const &p) 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_diff (expr const &a, expr const &b) expr re_complement (expr const &a) expr range (expr const &lo, expr const &hi)
Z3 C++ namespace.
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