158         void init(config & c) {  in init()
170         context() { config c; init(c); }  in context()  local
171         context(config & c) { init(c); }  in context()
396         T const * ptr() const { return m_array; }  in ptr()  function
397         T * ptr() { return m_array; }  in ptr()  function
404         object(context & c):m_ctx(&c) {}  in object()
415         symbol(context & c, Z3_symbol s):object(c), m_sym(s) {}  in symbol()
437 …param_descrs(context& c, Z3_param_descrs d): object(c), m_descrs(d) { Z3_param_descrs_inc_ref(c, d…  in param_descrs()
447 …static param_descrs simplify_param_descrs(context& c) { return param_descrs(c, Z3_simplify_get_par…  in simplify_param_descrs()
461 …  params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); }  in params()
488         ast(context & c):object(c), m_ast(0) {}  in ast()
489         ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }  in ast()
510     inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b); }  in eq()  function
518         sort(context & c):ast(c) {}  in sort()
519         sort(context & c, Z3_sort s):ast(c, reinterpret_cast<Z3_ast>(s)) {}  in sort()
520         sort(context & c, Z3_ast a):ast(c, a) {}  in sort()
620         func_decl(context & c):ast(c) {}  in func_decl()
621         func_decl(context & c, Z3_func_decl n):ast(c, reinterpret_cast<Z3_ast>(n)) {}  in func_decl()
669         expr(context & c):ast(c) {}  in expr()
670         expr(context & c, Z3_ast n):ast(c, reinterpret_cast<Z3_ast>(n)) {}  in expr()
1608     inline expr fma(expr const& a, expr const& b, expr const& c, expr const& rm) {  in fma()
1621     inline expr ite(expr const & c, expr const & t, expr const & e) {  in ite()
1634     inline expr to_expr(context & c, Z3_ast a) {  in to_expr()
1643     inline sort to_sort(context & c, Z3_sort s) {  in to_sort()
1648     inline func_decl to_func_decl(context & c, Z3_func_decl f) {  in to_func_decl()
1788         ast_vector_tpl(context & c):object(c) { init(Z3_mk_ast_vector(c)); }  in ast_vector_tpl()
1789         ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }  in ast_vector_tpl()
2058         func_entry(context & c, Z3_func_entry e):object(c) { init(e); }  in func_entry()
2081         func_interp(context & c, Z3_func_interp e):object(c) { init(e); }  in func_interp()
2113         model(context & c):object(c) { init(Z3_mk_model(c)); }  in model()
2114         model(context & c, Z3_model m):object(c) { init(m); }  in model()
2150         expr get_const_interp(func_decl c) const {  in get_const_interp()
2192         stats(context & c):object(c), m_stats(0) {}  in stats()
2193         stats(context & c, Z3_stats e):object(c) { init(e); }  in stats()
2232         solver(context & c):object(c) { init(Z3_mk_solver(c)); }  in solver()
2233         solver(context & c, simple):object(c) { init(Z3_mk_simple_solver(c)); }  in solver()
2234         solver(context & c, Z3_solver s):object(c) { init(s); }  in solver()
2235 …solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(lo…  in solver()
2236 …solver(context & c, solver const& src, translate): object(c) { init(Z3_solver_translate(src.ctx(),…  in solver()
2270 …check_result check() { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_che…  in check()  function
2271         check_result check(unsigned n, expr * const assumptions) {  in check()  function
2281         check_result check(expr_vector assumptions) {  in check()  function
2427             void set_cutoff(unsigned c) { m_cutoff = c; }  in set_cutoff()
2443 …goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3…  in object()  argument
2444         goal(context & c, Z3_goal s):object(c) { init(s); }  in goal()
2502         apply_result(context & c, Z3_apply_result s):object(c) { init(s); }  in apply_result()
2526 …tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_erro…  in tactic()
2527         tactic(context & c, Z3_tactic s):object(c) { init(s); }  in tactic()
2612 …probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error()…  in probe()
2613 …probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); ini…  in probe()
2614         probe(context & c, Z3_probe s):object(c) { init(s); }  in probe()
2692         optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }  in optimize()
2737 …check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt, 0, 0); check_error(); return t…  in check()  function
2738         check_result check(expr_vector const& asms) {  in check()  function
2775 …   fixedpoint(context& c):object(c) { m_fp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); }  in fixedpoint()