Z3
z3_api.h
Go to the documentation of this file.
1 /*++
2  Copyright (c) 2015 Microsoft Corporation
3 --*/
4 
5 #ifndef Z3_API_H_
6 #define Z3_API_H_
7 
8 DEFINE_TYPE(Z3_symbol);
9 DEFINE_TYPE(Z3_literals);
10 DEFINE_TYPE(Z3_config);
11 DEFINE_TYPE(Z3_context);
12 DEFINE_TYPE(Z3_sort);
13 #define Z3_sort_opt Z3_sort
14 DEFINE_TYPE(Z3_func_decl);
15 DEFINE_TYPE(Z3_ast);
16 #define Z3_ast_opt Z3_ast
17 DEFINE_TYPE(Z3_app);
18 DEFINE_TYPE(Z3_pattern);
19 DEFINE_TYPE(Z3_model);
20 DEFINE_TYPE(Z3_constructor);
21 DEFINE_TYPE(Z3_constructor_list);
22 DEFINE_TYPE(Z3_params);
23 DEFINE_TYPE(Z3_param_descrs);
24 DEFINE_TYPE(Z3_goal);
25 DEFINE_TYPE(Z3_tactic);
26 DEFINE_TYPE(Z3_probe);
27 DEFINE_TYPE(Z3_stats);
28 DEFINE_TYPE(Z3_solver);
29 DEFINE_TYPE(Z3_ast_vector);
30 DEFINE_TYPE(Z3_ast_map);
31 DEFINE_TYPE(Z3_apply_result);
32 DEFINE_TYPE(Z3_func_interp);
33 #define Z3_func_interp_opt Z3_func_interp
34 DEFINE_TYPE(Z3_func_entry);
35 DEFINE_TYPE(Z3_fixedpoint);
36 DEFINE_TYPE(Z3_optimize);
37 DEFINE_TYPE(Z3_rcf_num);
38 
41 
77 typedef bool Z3_bool;
78 
82 typedef const char * Z3_string;
84 
88 #define Z3_TRUE true
89 
93 #define Z3_FALSE false
94 
98 typedef enum
99 {
103 } Z3_lbool;
104 
112 typedef enum
113 {
117 
118 
132 typedef enum
133 {
142 
146 typedef enum
147 {
162 } Z3_sort_kind;
163 
176 typedef enum
177 {
185 } Z3_ast_kind;
186 
982 typedef enum {
983  // Basic
984  Z3_OP_TRUE = 0x100,
996 
997  // Arithmetic
998  Z3_OP_ANUM = 0x200,
1016 
1017  // Arrays & Sets
1018  Z3_OP_STORE = 0x300,
1030 
1031  // Bit-vectors
1032  Z3_OP_BNUM = 0x400,
1039 
1045 
1046  // special functions to record the division by 0 cases
1047  // these are internal functions
1053 
1062 
1070 
1076 
1080 
1088 
1094 
1103 
1104  // Proofs
1143 
1144  // Relational algebra
1160 
1161  // Sequences
1175 
1176  // strings
1179 
1180  // regular expressions
1192 
1193  // Auxiliary
1194  Z3_OP_LABEL = 0x700,
1196 
1197  // Datatypes
1203 
1204  // Pseudo Booleans
1210 
1211  // Floating-Point Arithmetic
1217 
1224 
1237 
1250 
1257 
1259 
1262 
1264 
1266 } Z3_decl_kind;
1267 
1280 typedef enum {
1288 } Z3_param_kind;
1289 
1297 typedef enum {
1302 
1303 
1321 typedef enum
1322 {
1336 } Z3_error_code;
1337 
1346 typedef void Z3_error_handler(Z3_context c, Z3_error_code e);
1347 
1358 typedef enum
1359 {
1364 } Z3_goal_prec;
1365 
1368 #ifdef __cplusplus
1369 extern "C" {
1370 #endif // __cplusplus
1371 
1395  void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value);
1396 
1397 
1405  void Z3_API Z3_global_param_reset_all(void);
1406 
1418  Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value);
1419 
1424 
1454  Z3_config Z3_API Z3_mk_config(void);
1455 
1462  void Z3_API Z3_del_config(Z3_config c);
1463 
1472  void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value);
1473 
1478 
1504  Z3_context Z3_API Z3_mk_context(Z3_config c);
1505 
1527  Z3_context Z3_API Z3_mk_context_rc(Z3_config c);
1528 
1535  void Z3_API Z3_del_context(Z3_context c);
1536 
1543  void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a);
1544 
1551  void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a);
1552 
1559  void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value);
1560 
1566  void Z3_API Z3_interrupt(Z3_context c);
1567 
1568 
1573 
1583  Z3_params Z3_API Z3_mk_params(Z3_context c);
1584 
1589  void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p);
1590 
1595  void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p);
1596 
1601  void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, bool v);
1602 
1607  void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v);
1608 
1613  void Z3_API Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v);
1614 
1619  void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v);
1620 
1626  Z3_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p);
1627 
1634  void Z3_API Z3_params_validate(Z3_context c, Z3_params p, Z3_param_descrs d);
1635 
1640 
1645  void Z3_API Z3_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p);
1646 
1651  void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p);
1652 
1657  Z3_param_kind Z3_API Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n);
1658 
1663  unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p);
1664 
1671  Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i);
1672 
1677  Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s);
1678 
1684  Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p);
1685 
1690 
1703  Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i);
1704 
1714  Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s);
1715 
1720 
1727  Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s);
1728 
1735  Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c);
1736 
1747  Z3_sort Z3_API Z3_mk_int_sort(Z3_context c);
1748 
1755  Z3_sort Z3_API Z3_mk_real_sort(Z3_context c);
1756 
1765  Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz);
1766 
1779  Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size);
1780 
1791  Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range);
1792 
1800  Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const * domain, Z3_sort range);
1801 
1817  Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c,
1818  Z3_symbol mk_tuple_name,
1819  unsigned num_fields,
1820  Z3_symbol const field_names[],
1821  Z3_sort const field_sorts[],
1822  Z3_func_decl * mk_tuple_decl,
1823  Z3_func_decl proj_decl[]);
1824 
1845  Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c,
1846  Z3_symbol name,
1847  unsigned n,
1848  Z3_symbol const enum_names[],
1849  Z3_func_decl enum_consts[],
1850  Z3_func_decl enum_testers[]);
1851 
1869  Z3_sort Z3_API Z3_mk_list_sort(Z3_context c,
1870  Z3_symbol name,
1871  Z3_sort elem_sort,
1872  Z3_func_decl* nil_decl,
1873  Z3_func_decl* is_nil_decl,
1874  Z3_func_decl* cons_decl,
1875  Z3_func_decl* is_cons_decl,
1876  Z3_func_decl* head_decl,
1877  Z3_func_decl* tail_decl
1878  );
1879 
1894  Z3_constructor Z3_API Z3_mk_constructor(Z3_context c,
1895  Z3_symbol name,
1896  Z3_symbol recognizer,
1897  unsigned num_fields,
1898  Z3_symbol const field_names[],
1899  Z3_sort_opt const sorts[],
1900  unsigned sort_refs[]
1901  );
1902 
1910  void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr);
1911 
1922  Z3_sort Z3_API Z3_mk_datatype(Z3_context c,
1923  Z3_symbol name,
1924  unsigned num_constructors,
1925  Z3_constructor constructors[]);
1926 
1935  Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c,
1936  unsigned num_constructors,
1937  Z3_constructor const constructors[]);
1938 
1948  void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist);
1949 
1960  void Z3_API Z3_mk_datatypes(Z3_context c,
1961  unsigned num_sorts,
1962  Z3_symbol const sort_names[],
1963  Z3_sort sorts[],
1964  Z3_constructor_list constructor_lists[]);
1965 
1977  void Z3_API Z3_query_constructor(Z3_context c,
1978  Z3_constructor constr,
1979  unsigned num_fields,
1980  Z3_func_decl* constructor,
1981  Z3_func_decl* tester,
1982  Z3_func_decl accessors[]);
1983 
1988 
2005  Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s,
2006  unsigned domain_size, Z3_sort const domain[],
2007  Z3_sort range);
2008 
2009 
2010 
2017  Z3_ast Z3_API Z3_mk_app(
2018  Z3_context c,
2019  Z3_func_decl d,
2020  unsigned num_args,
2021  Z3_ast const args[]);
2022 
2036  Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty);
2037 
2049  Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix,
2050  unsigned domain_size, Z3_sort const domain[],
2051  Z3_sort range);
2052 
2065  Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty);
2066 
2067 
2085  Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s,
2086  unsigned domain_size, Z3_sort const domain[],
2087  Z3_sort range);
2088 
2104  void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body);
2105 
2114  Z3_ast Z3_API Z3_mk_true(Z3_context c);
2115 
2120  Z3_ast Z3_API Z3_mk_false(Z3_context c);
2121 
2128  Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r);
2129 
2141  Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[]);
2142 
2149  Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a);
2150 
2158  Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3);
2159 
2166  Z3_ast Z3_API Z3_mk_iff(Z3_context c, Z3_ast t1, Z3_ast t2);
2167 
2174  Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2);
2175 
2182  Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2);
2183 
2193  Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[]);
2194 
2204  Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[]);
2218  Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[]);
2219 
2230  Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[]);
2231 
2241  Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[]);
2242 
2249  Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg);
2250 
2259  Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2260 
2267  Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2268 
2275  Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2276 
2283  Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2284 
2291  Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2);
2292 
2299  Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2);
2300 
2307  Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2);
2308 
2315  Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2);
2316 
2333  Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1);
2334 
2345  Z3_ast Z3_API Z3_mk_real2int(Z3_context c, Z3_ast t1);
2346 
2354  Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1);
2365  Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1);
2366 
2373  Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1);
2374 
2381  Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1);
2382 
2389  Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2);
2390 
2397  Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2);
2398 
2405  Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2);
2406 
2413  Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2);
2414 
2421  Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2);
2422 
2429  Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2);
2430 
2437  Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1);
2438 
2445  Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2);
2446 
2453  Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2);
2454 
2461  Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2);
2462 
2473  Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2);
2474 
2489  Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2);
2490 
2501  Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2);
2502 
2516  Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2);
2517 
2528  Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2);
2529 
2536  Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2);
2537 
2552  Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2);
2553 
2560  Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2);
2561 
2568  Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2);
2569 
2576  Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2);
2577 
2584  Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2);
2585 
2592  Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2);
2593 
2600  Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2);
2601 
2611  Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2);
2612 
2620  Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1);
2621 
2630  Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1);
2631 
2640  Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1);
2641 
2648  Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1);
2649 
2663  Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2);
2664 
2678  Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2);
2679 
2694  Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2);
2695 
2702  Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1);
2703 
2710  Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1);
2711 
2718  Z3_ast Z3_API Z3_mk_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2);
2719 
2726  Z3_ast Z3_API Z3_mk_ext_rotate_right(Z3_context c, Z3_ast t1, Z3_ast t2);
2727 
2737  Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1);
2738 
2750  Z3_ast Z3_API Z3_mk_bv2int(Z3_context c,Z3_ast t1, bool is_signed);
2751 
2759  Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);
2760 
2768  Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2);
2769 
2777  Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2);
2778 
2786  Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);
2787 
2795  Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2);
2796 
2804  Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1);
2805 
2813  Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);
2814 
2822  Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2);
2839  Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i);
2840 
2841 
2842 
2849  Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs);
2850 
2851 
2867  Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v);
2868 
2869 
2875  Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs, Z3_ast v);
2876 
2888  Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v);
2889 
2902  Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const* args);
2903 
2913  Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array);
2914 
2921  Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f);
2930  Z3_sort Z3_API Z3_mk_set_sort(Z3_context c, Z3_sort ty);
2931 
2936  Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain);
2937 
2942  Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain);
2943 
2950  Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem);
2951 
2958  Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem);
2959 
2964  Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[]);
2965 
2970  Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[]);
2971 
2976  Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2977 
2982  Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg);
2983 
2990  Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set);
2991 
2996  Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2997 
3005  Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2);
3022  Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty);
3023 
3038  Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den);
3039 
3049  Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty);
3050 
3060  Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty);
3061 
3071  Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty);
3072 
3082  Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty);
3083 
3089  Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, bool const* bits);
3090 
3095 
3100  Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s);
3101 
3106  bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s);
3107 
3112  Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq);
3113 
3118  bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s);
3119 
3127  Z3_sort Z3_API Z3_mk_string_sort(Z3_context c);
3128 
3133  bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s);
3134 
3138  Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s);
3139 
3144  bool Z3_API Z3_is_string(Z3_context c, Z3_ast s);
3145 
3152  Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s);
3153 
3160  Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq);
3161 
3166  Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a);
3167 
3174  Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[]);
3175 
3182  Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s);
3183 
3190  Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s);
3191 
3198  Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee);
3199 
3204  Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length);
3205 
3210  Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst);
3211 
3216  Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index);
3217 
3222  Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s);
3223 
3224 
3231  Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);
3232 
3237  Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s);
3238 
3239 
3244  Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s);
3245 
3250  Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq);
3251 
3256  Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re);
3257 
3262  Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re);
3263 
3268  Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re);
3269 
3274  Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re);
3275 
3282  Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[]);
3283 
3290  Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[]);
3291 
3292 
3297  Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi);
3298 
3306  Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi);
3307 
3314  Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[]);
3315 
3320  Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re);
3321 
3328  Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re);
3329 
3330 
3337  Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re);
3338 
3339 
3364  Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[]);
3365 
3394  Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty);
3395 
3418  Z3_ast Z3_API Z3_mk_forall(Z3_context c, unsigned weight,
3419  unsigned num_patterns, Z3_pattern const patterns[],
3420  unsigned num_decls, Z3_sort const sorts[],
3421  Z3_symbol const decl_names[],
3422  Z3_ast body);
3423 
3433  Z3_ast Z3_API Z3_mk_exists(Z3_context c, unsigned weight,
3434  unsigned num_patterns, Z3_pattern const patterns[],
3435  unsigned num_decls, Z3_sort const sorts[],
3436  Z3_symbol const decl_names[],
3437  Z3_ast body);
3438 
3459  Z3_ast Z3_API Z3_mk_quantifier(
3460  Z3_context c,
3461  bool is_forall,
3462  unsigned weight,
3463  unsigned num_patterns, Z3_pattern const patterns[],
3464  unsigned num_decls, Z3_sort const sorts[],
3465  Z3_symbol const decl_names[],
3466  Z3_ast body);
3467 
3468 
3492  Z3_ast Z3_API Z3_mk_quantifier_ex(
3493  Z3_context c,
3494  bool is_forall,
3495  unsigned weight,
3496  Z3_symbol quantifier_id,
3497  Z3_symbol skolem_id,
3498  unsigned num_patterns, Z3_pattern const patterns[],
3499  unsigned num_no_patterns, Z3_ast const no_patterns[],
3500  unsigned num_decls, Z3_sort const sorts[],
3501  Z3_symbol const decl_names[],
3502  Z3_ast body);
3503 
3521  Z3_ast Z3_API Z3_mk_forall_const(
3522  Z3_context c,
3523  unsigned weight,
3524  unsigned num_bound,
3525  Z3_app const bound[],
3526  unsigned num_patterns,
3527  Z3_pattern const patterns[],
3528  Z3_ast body
3529  );
3530 
3550  Z3_ast Z3_API Z3_mk_exists_const(
3551  Z3_context c,
3552  unsigned weight,
3553  unsigned num_bound,
3554  Z3_app const bound[],
3555  unsigned num_patterns,
3556  Z3_pattern const patterns[],
3557  Z3_ast body
3558  );
3559 
3565  Z3_ast Z3_API Z3_mk_quantifier_const(
3566  Z3_context c,
3567  bool is_forall,
3568  unsigned weight,
3569  unsigned num_bound, Z3_app const bound[],
3570  unsigned num_patterns, Z3_pattern const patterns[],
3571  Z3_ast body
3572  );
3573 
3579  Z3_ast Z3_API Z3_mk_quantifier_const_ex(
3580  Z3_context c,
3581  bool is_forall,
3582  unsigned weight,
3583  Z3_symbol quantifier_id,
3584  Z3_symbol skolem_id,
3585  unsigned num_bound, Z3_app const bound[],
3586  unsigned num_patterns, Z3_pattern const patterns[],
3587  unsigned num_no_patterns, Z3_ast const no_patterns[],
3588  Z3_ast body
3589  );
3590 
3613  Z3_ast Z3_API Z3_mk_lambda(Z3_context c,
3614  unsigned num_decls, Z3_sort const sorts[],
3615  Z3_symbol const decl_names[],
3616  Z3_ast body);
3617 
3632  Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c,
3633  unsigned num_bound, Z3_app const bound[],
3634  Z3_ast body);
3635 
3636 
3647  Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s);
3648 
3657  int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s);
3658 
3671  Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s);
3672 
3677  Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d);
3678 
3683  unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s);
3684 
3689  Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s);
3690 
3695  bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2);
3696 
3703  Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t);
3704 
3714  unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t);
3715 
3721  Z3_bool_opt Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r);
3722 
3733  Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t);
3734 
3744  Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t);
3745 
3756  Z3_func_decl Z3_API Z3_get_tuple_sort_mk_decl(Z3_context c, Z3_sort t);
3757 
3767  unsigned Z3_API Z3_get_tuple_sort_num_fields(Z3_context c, Z3_sort t);
3768 
3780  Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t, unsigned i);
3781 
3792  unsigned Z3_API Z3_get_datatype_sort_num_constructors(
3793  Z3_context c, Z3_sort t);
3794 
3806  Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(
3807  Z3_context c, Z3_sort t, unsigned idx);
3808 
3820  Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(
3821  Z3_context c, Z3_sort t, unsigned idx);
3822 
3835  Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c,
3836  Z3_sort t,
3837  unsigned idx_c,
3838  unsigned idx_a);
3839 
3858  Z3_ast Z3_API Z3_datatype_update_field(Z3_context c, Z3_func_decl field_access,
3859  Z3_ast t, Z3_ast value);
3860 
3869  unsigned Z3_API Z3_get_relation_arity(Z3_context c, Z3_sort s);
3870 
3880  Z3_sort Z3_API Z3_get_relation_column(Z3_context c, Z3_sort s, unsigned col);
3881 
3888  Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args,
3889  Z3_ast const args[], unsigned k);
3890 
3897  Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args,
3898  Z3_ast const args[], unsigned k);
3899 
3906  Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args,
3907  Z3_ast const args[], int const coeffs[],
3908  int k);
3909 
3916  Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args,
3917  Z3_ast const args[], int const coeffs[],
3918  int k);
3919 
3926  Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args,
3927  Z3_ast const args[], int const coeffs[],
3928  int k);
3929 
3934  Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f);
3935 
3940  bool Z3_API Z3_is_eq_func_decl(Z3_context c, Z3_func_decl f1, Z3_func_decl f2);
3941 
3946  unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f);
3947 
3952  Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d);
3953 
3958  Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d);
3959 
3966  unsigned Z3_API Z3_get_domain_size(Z3_context c, Z3_func_decl d);
3967 
3974  unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d);
3975 
3984  Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i);
3985 
3993  Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d);
3994 
3999  unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d);
4000 
4009  Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx);
4010 
4017  int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4018 
4025  double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4026 
4033  Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4034 
4041  Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4042 
4049  Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4050 
4057  Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4058 
4065  Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4066 
4071  Z3_ast Z3_API Z3_app_to_ast(Z3_context c, Z3_app a);
4072 
4077  Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a);
4078 
4084  unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a);
4085 
4092  Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i);
4093 
4098  bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2);
4099 
4110  unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t);
4111 
4118  unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a);
4119 
4126  Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a);
4127 
4132  bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t);
4133 
4138  Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a);
4139 
4144  Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a);
4145 
4148  bool Z3_API Z3_is_app(Z3_context c, Z3_ast a);
4149 
4152  bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a);
4153 
4158  bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a);
4159 
4166  Z3_app Z3_API Z3_to_app(Z3_context c, Z3_ast a);
4167 
4174  Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a);
4175 
4182  Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a);
4183 
4191  Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision);
4192 
4199  double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a);
4200 
4207  Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a);
4208 
4215  Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a);
4216 
4230  bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, int64_t* num, int64_t* den);
4231 
4241  bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int* i);
4242 
4252  bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned* u);
4253 
4263  bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t* u);
4264 
4274  bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t* i);
4275 
4285  bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, int64_t* num, int64_t* den);
4286 
4295  Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision);
4296 
4305  Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision);
4306 
4311  Z3_ast Z3_API Z3_pattern_to_ast(Z3_context c, Z3_pattern p);
4312 
4317  unsigned Z3_API Z3_get_pattern_num_terms(Z3_context c, Z3_pattern p);
4318 
4323  Z3_ast Z3_API Z3_get_pattern(Z3_context c, Z3_pattern p, unsigned idx);
4324 
4331  unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a);
4332 
4337  bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a);
4338 
4344  bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a);
4345 
4352  bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a);
4353 
4360  unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a);
4361 
4368  unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a);
4369 
4376  Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i);
4377 
4384  unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a);
4385 
4392  Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i);
4393 
4400  unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a);
4401 
4408  Z3_symbol Z3_API Z3_get_quantifier_bound_name(Z3_context c, Z3_ast a, unsigned i);
4409 
4416  Z3_sort Z3_API Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, unsigned i);
4417 
4424  Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a);
4425 
4437  Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a);
4438 
4451  Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p);
4452 
4460  Z3_string Z3_API Z3_simplify_get_help(Z3_context c);
4461 
4469  Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c);
4481  Z3_ast Z3_API Z3_update_term(Z3_context c, Z3_ast a, unsigned num_args, Z3_ast const args[]);
4482 
4489  Z3_ast Z3_API Z3_substitute(Z3_context c,
4490  Z3_ast a,
4491  unsigned num_exprs,
4492  Z3_ast const from[],
4493  Z3_ast const to[]);
4494 
4500  Z3_ast Z3_API Z3_substitute_vars(Z3_context c,
4501  Z3_ast a,
4502  unsigned num_exprs,
4503  Z3_ast const to[]);
4504 
4511  Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target);
4516 
4521  Z3_model Z3_API Z3_mk_model(Z3_context c);
4522 
4527  void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m);
4528 
4533  void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m);
4534 
4557  Z3_bool_opt Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v);
4558 
4567  Z3_ast_opt Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a);
4568 
4573  bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a);
4574 
4586  Z3_func_interp_opt Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f);
4587 
4594  unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m);
4595 
4604  Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i);
4605 
4613  unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m);
4614 
4623  Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i);
4624 
4636  unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m);
4637 
4647  Z3_sort Z3_API Z3_model_get_sort(Z3_context c, Z3_model m, unsigned i);
4648 
4656  Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s);
4657 
4662  Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst);
4663 
4674  bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a);
4675 
4682  Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a);
4683 
4694  Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value);
4695 
4700  void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a);
4701 
4706  void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f);
4707 
4712  void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f);
4713 
4722  unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f);
4723 
4733  Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i);
4734 
4742  Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f);
4743 
4751  void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value);
4752 
4757  unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f);
4758 
4772  void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value);
4773 
4778  void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e);
4779 
4784  void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e);
4785 
4795  Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e);
4796 
4803  unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e);
4804 
4813  Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i);
4822  bool Z3_API Z3_open_log(Z3_string filename);
4823 
4832  void Z3_API Z3_append_log(Z3_string string);
4833 
4838  void Z3_API Z3_close_log(void);
4839 
4847  void Z3_API Z3_toggle_warning_messages(bool enabled);
4868  void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode);
4869 
4881  Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a);
4882 
4885  Z3_string Z3_API Z3_pattern_to_string(Z3_context c, Z3_pattern p);
4886 
4889  Z3_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s);
4890 
4893  Z3_string Z3_API Z3_func_decl_to_string(Z3_context c, Z3_func_decl d);
4894 
4903  Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m);
4904 
4922  Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c,
4923  Z3_string name,
4924  Z3_string logic,
4925  Z3_string status,
4926  Z3_string attributes,
4927  unsigned num_assumptions,
4928  Z3_ast const assumptions[],
4929  Z3_ast formula);
4930 
4942  Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c,
4943  Z3_string str,
4944  unsigned num_sorts,
4945  Z3_symbol const sort_names[],
4946  Z3_sort const sorts[],
4947  unsigned num_decls,
4948  Z3_symbol const decl_names[],
4949  Z3_func_decl const decls[]);
4950 
4955  Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c,
4956  Z3_string file_name,
4957  unsigned num_sorts,
4958  Z3_symbol const sort_names[],
4959  Z3_sort const sorts[],
4960  unsigned num_decls,
4961  Z3_symbol const decl_names[],
4962  Z3_func_decl const decls[]);
4963 
4964 
4973  Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context, Z3_string str);
4974 
4979 #ifndef SAFE_ERRORS
4980 
4989  Z3_error_code Z3_API Z3_get_error_code(Z3_context c);
4990 
5003  void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h);
5004 #endif
5005 
5010  void Z3_API Z3_set_error(Z3_context c, Z3_error_code e);
5011 
5016  Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err);
5017 
5022 
5027  void Z3_API Z3_get_version(unsigned * major, unsigned * minor, unsigned * build_number, unsigned * revision_number);
5028 
5033  Z3_string Z3_API Z3_get_full_version(void);
5034 
5040  void Z3_API Z3_enable_trace(Z3_string tag);
5041 
5047  void Z3_API Z3_disable_trace(Z3_string tag);
5048 
5058  void Z3_API Z3_reset_memory(void);
5059 
5067  void Z3_API Z3_finalize_memory(void);
5088  Z3_goal Z3_API Z3_mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs);
5089 
5094  void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g);
5095 
5100  void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g);
5101 
5108  Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g);
5109 
5121  void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a);
5122 
5127  bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g);
5128 
5133  unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g);
5134 
5139  void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g);
5140 
5145  unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g);
5146 
5153  Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx);
5154 
5159  unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g);
5160 
5165  bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g);
5166 
5171  bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g);
5172 
5177  Z3_goal Z3_API Z3_goal_translate(Z3_context source, Z3_goal g, Z3_context target);
5178 
5185  Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m);
5186 
5191  Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g);
5192 
5202  Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g);
5203 
5216  Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name);
5217 
5222  void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t);
5223 
5228  void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g);
5229 
5239  Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name);
5240 
5245  void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p);
5246 
5251  void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p);
5252 
5258  Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2);
5259 
5265  Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2);
5266 
5271  Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[]);
5272 
5278  Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2);
5279 
5285  Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms);
5286 
5292  Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t);
5293 
5299  Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2);
5300 
5306  Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max);
5307 
5312  Z3_tactic Z3_API Z3_tactic_skip(Z3_context c);
5313 
5318  Z3_tactic Z3_API Z3_tactic_fail(Z3_context c);
5319 
5324  Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p);
5325 
5331  Z3_tactic Z3_API Z3_tactic_fail_if_not_decided(Z3_context c);
5332 
5337  Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p);
5338 
5343  Z3_probe Z3_API Z3_probe_const(Z3_context x, double val);
5344 
5351  Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2);
5352 
5359  Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2);
5360 
5367  Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2);
5368 
5375  Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2);
5376 
5383  Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2);
5384 
5391  Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2);
5392 
5399  Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2);
5400 
5407  Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p);
5408 
5413  unsigned Z3_API Z3_get_num_tactics(Z3_context c);
5414 
5421  Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i);
5422 
5427  unsigned Z3_API Z3_get_num_probes(Z3_context c);
5428 
5435  Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i);
5436 
5441  Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t);
5442 
5447  Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t);
5448 
5453  Z3_string Z3_API Z3_tactic_get_descr(Z3_context c, Z3_string name);
5454 
5459  Z3_string Z3_API Z3_probe_get_descr(Z3_context c, Z3_string name);
5460 
5466  double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g);
5467 
5472  Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g);
5473 
5478  Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p);
5479 
5484  void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r);
5485 
5490  void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r);
5491 
5496  Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r);
5497 
5502  unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r);
5503 
5510  Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i);
5511 
5551  Z3_solver Z3_API Z3_mk_solver(Z3_context c);
5552 
5577  Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c);
5578 
5587  Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic);
5588 
5598  Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t);
5599 
5604  Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target);
5605 
5610  void Z3_API Z3_solver_import_model_converter(Z3_context ctx, Z3_solver src, Z3_solver dst);
5611 
5619  Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s);
5620 
5628  Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s);
5629 
5637  void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p);
5638 
5643  void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s);
5644 
5649  void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s);
5650 
5660  void Z3_API Z3_solver_push(Z3_context c, Z3_solver s);
5661 
5671  void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n);
5672 
5680  void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s);
5681 
5689  unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s);
5690 
5701  void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a);
5702 
5719  void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p);
5720 
5728  void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name);
5729 
5737  void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name);
5738 
5743  Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s);
5744 
5749  Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s);
5750 
5751 
5756  Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s);
5757 
5775  Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s);
5776 
5787  Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s,
5788  unsigned num_assumptions, Z3_ast const assumptions[]);
5789 
5807  Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c,
5808  Z3_solver s,
5809  unsigned num_terms,
5810  Z3_ast const terms[],
5811  unsigned class_ids[]);
5812 
5818  Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c,
5819  Z3_solver s,
5820  Z3_ast_vector assumptions,
5821  Z3_ast_vector variables,
5822  Z3_ast_vector consequences);
5823 
5824 
5842  Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level);
5843 
5851  Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s);
5852 
5861  Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s);
5862 
5868  Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s);
5869 
5875  Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s);
5876 
5883  Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s);
5884 
5892  Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s);
5893 
5898 
5903  Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s);
5904 
5909  void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s);
5910 
5915  void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s);
5916 
5921  unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s);
5922 
5929  Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx);
5930 
5937  bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx);
5938 
5945  bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx);
5946 
5953  unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx);
5954 
5961  double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx);
5962 
5967  uint64_t Z3_API Z3_get_estimated_alloc_size(void);
5968 
5971 #ifdef __cplusplus
5972 }
5973 #endif // __cplusplus
5974 
5977 #endif
Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 and p2 evaluates to true.
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i)
Return the name of the i probe.
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)
Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...
Z3_goal Z3_API Z3_mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:146
Z3_ast Z3_API Z3_mk_real2int(Z3_context c, Z3_ast t1)
Coerce a real to an integer.
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a fresh constant or function.
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.
Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the rational value, as a string, associated with a rational parameter.
Z3_sort Z3_API Z3_model_get_sort(Z3_context c, Z3_model m, unsigned i)
Return a uninterpreted sort that m assigns an interpretation.
bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int....
Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f)
Return the arity (number of arguments) of the given function interpretation.
void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr)
Reclaim memory allocated to constructor.
Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t)
Return the parameter description set for the given tactic object.
void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)
Erase all formulas from the given goal.
Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c, Z3_symbol mk_tuple_name, unsigned num_fields, Z3_symbol const field_names[], Z3_sort const field_sorts[], Z3_func_decl *mk_tuple_decl, Z3_func_decl proj_decl[])
Create a tuple type.
bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return true if the given statistical data is a unsigned integer.
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.
Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t)
Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...
Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty)
Create a bound variable.
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)
Return a string describing the given error code.
bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a)
Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c, Z3_solver s, unsigned num_terms, Z3_ast const terms[], unsigned class_ids[])
Retrieve congruence class representatives for terms.
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
Z3_ast Z3_API Z3_pattern_to_ast(Z3_context c, Z3_pattern p)
Convert a Z3_pattern into Z3_ast. This is just type casting.
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d)
Return the constant declaration name as a symbol.
Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s)
Retrieve documentation string corresponding to parameter name s.
Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g)
Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF...
void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.
DEFINE_TYPE(Z3_symbol)
void Z3_API Z3_disable_trace(Z3_string tag)
Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
void Z3_API Z3_toggle_warning_messages(bool enabled)
Enable/disable printing warning messages to the console.
Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the unit sequence positioned at position index.
Z3_params Z3_API Z3_mk_params(Z3_context c)
Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many comp...
Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1.
Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s)
Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if th...
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s)
Return the finite set of distinct values that represent the interpretation for sort s.
void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v)
Add a unsigned parameter k with value v to the parameter set p.
void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a)
Add a constant interpretation.
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i)
Return the declaration of the i-th function in the given model.
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
Definition: z3_api.h:1323
bool Z3_API Z3_is_app(Z3_context c, Z3_ast a)
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...
bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a)
Return true if the given AST is a real algebraic number.
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...
unsigned Z3_API Z3_get_tuple_sort_num_fields(Z3_context c, Z3_sort t)
Return the number of fields of the given tuple sort.
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t)
Return the range of the given array sort.
void Z3_API Z3_set_error(Z3_context c, Z3_error_code e)
Set an error.
Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
bool Z3_bool
Z3 Boolean type. It is just an alias for bool.
Definition: z3_api.h:77
Z3_solver Z3_API Z3_mk_solver(Z3_context c)
Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally ...
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs....
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
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.
Z3_sort Z3_API Z3_mk_datatype(Z3_context c, Z3_symbol name, unsigned num_constructors, Z3_constructor constructors[])
Create datatype, such as lists, trees, records, enumerations or unions of records....
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.
Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)
Remove an element to a set.
Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the union of a list of sets.
Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i)
Return the i-th constant in the given model.
Z3_sort Z3_API Z3_get_relation_column(Z3_context c, Z3_sort s, unsigned col)
Return sort at i'th column of relation sort.
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2)
compare sorts.
Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i)
Return the name of the parameter at given index i.
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1358
Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create array extensionality index given two arrays with the same sort. The meaning is given by the ax...
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1321
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].
Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i)
Return an argument of a Z3_func_entry object.
Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a)
Return the function declaration f associated with a (_ as_array f) node.
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
Z3_tactic Z3_API Z3_tactic_skip(Z3_context c)
Return a tactic that just return the given goal.
Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m)
Return the number of uninterpreted sorts that m assigns an interpretation to.
Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m)
Convert a model of the formulas of a goal to a model of an original goal. The model may be null,...
Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d)
Return declaration kind corresponding to declaration.
bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.
Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i)
Return the name of the idx tactic.
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.
uint64_t Z3_API Z3_get_estimated_alloc_size(void)
Return the estimated allocated memory in bytes.
Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not.
Z3_goal Z3_API Z3_goal_translate(Z3_context source, Z3_goal g, Z3_context target)
Copy a goal g from the context source to the context target.
void Z3_API Z3_close_log(void)
Close interaction log.
Z3_ast Z3_API Z3_mk_quantifier(Z3_context c, bool is_forall, unsigned weight, unsigned num_patterns, Z3_pattern const patterns[], unsigned num_decls, Z3_sort const sorts[], Z3_symbol const decl_names[], Z3_ast body)
Create a quantifier - universal or existential, with pattern hints. See the documentation for Z3_mk_f...
Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f)
Convert a Z3_func_decl into Z3_ast. This is just type casting.
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
Z3_ast Z3_API Z3_mk_quantifier_const(Z3_context c, bool is_forall, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal or existential quantifier using a list of constants that will form the set of boun...
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s)
Return a unique identifier for s.
Z3_context Z3_API Z3_mk_context_rc(Z3_config c)
Create a context using the given configuration. This function is similar to Z3_mk_context....
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine uint64_t int....
void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value)
Set a value of a context parameter.
Z3_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s)
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
Z3_ast Z3_API Z3_mk_ext_rotate_right(Z3_context c, Z3_ast t1, Z3_ast t2)
Rotate bits of t1 to the right t2 times.
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.
Z3_sort Z3_API Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, unsigned i)
Return sort of the i'th bound variable.
Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size)
Create a named finite domain sort.
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.
Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx)
Return the parameter type associated with a declaration.
Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s)
Check if prefix is a prefix of s.
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.
Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx)
Return the key (a string) for a particular statistical data.
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i)
Return the i-th argument of the given application.
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.
Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th recognizer.
Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re)
Create the complement of the regular language re.
Z3_sort Z3_API Z3_mk_list_sort(Z3_context c, Z3_symbol name, Z3_sort elem_sort, Z3_func_decl *nil_decl, Z3_func_decl *is_nil_decl, Z3_func_decl *cons_decl, Z3_func_decl *is_cons_decl, Z3_func_decl *head_decl, Z3_func_decl *tail_decl)
Create a list sort.
bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g)
Return true if the goal contains false, and it is precise or the product of an over approximation.
void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.
Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t, unsigned i)
Return the i-th field declaration (i.e., projection function declaration) of the given tuple sort.
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the intersection of a list of sets.
Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array)
Access the array default value. Produces the default range value, for arrays that can be represented ...
Z3_string Z3_API Z3_pattern_to_string(Z3_context c, Z3_pattern p)
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p)
Convert a parameter description set into a string. This function is mainly used for printing the cont...
Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value)
Create a fresh func_interp object, add it to a model for a specified function. It has reference count...
Z3_string * Z3_string_ptr
Definition: z3_api.h:83
Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, unsigned num_bound, Z3_app const bound[], Z3_ast body)
Create a lambda expression using a list of constants that form the set of bound variables.
Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p)
Apply tactic t to the goal g using the parameter set p.
void Z3_API Z3_append_log(Z3_string string)
Append user-defined string to interaction log.
unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a)
Return index of de-Bruijn bound variable.
unsigned Z3_API Z3_get_pattern_num_terms(Z3_context c, Z3_pattern p)
Return number of terms in pattern.
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.
Z3_error_code Z3_API Z3_get_error_code(Z3_context c)
Return the error code for the last API call.
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for 8 bit strings.
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...
Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist)
Reclaim memory allocated for constructor list.
Z3_constructor Z3_API Z3_mk_constructor(Z3_context c, Z3_symbol name, Z3_symbol recognizer, unsigned num_fields, Z3_symbol const field_names[], Z3_sort_opt const sorts[], unsigned sort_refs[])
Create a constructor.
Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Take the set difference between two sets.
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
bool Z3_API Z3_open_log(Z3_string filename)
Log interaction to a file.
void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
Z3_context Z3_API Z3_mk_context(Z3_config c)
Create a context using the given configuration.
Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows dividend).
bool Z3_API Z3_is_eq_func_decl(Z3_context c, Z3_func_decl f1, Z3_func_decl f2)
Compare terms.
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a)
Convert an AST into a FUNC_DECL_AST. This is just type casting.
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
unsigned Z3_API Z3_get_relation_arity(Z3_context c, Z3_sort s)
Return arity of relation.
Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Parse the given string using the SMT-LIB2 parser.
Z3_ast Z3_API Z3_mk_forall(Z3_context c, unsigned weight, unsigned num_patterns, Z3_pattern const patterns[], unsigned num_decls, Z3_sort const sorts[], Z3_symbol const decl_names[], Z3_ast body)
Create a forall formula. It takes an expression body that contains bound variables of the same sorts ...
#define Z3_func_interp_opt
Definition: z3_api.h:33
void Z3_API Z3_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p)
Increment the reference counter of the given parameter description set.
Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f)
Return the 'else' value of the given function interpretation.
Z3_ast Z3_API Z3_mk_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2)
Rotate bits of t1 to the left t2 times.
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
Z3_ast Z3_API Z3_update_term(Z3_context c, Z3_ast a, unsigned num_args, Z3_ast const args[])
Update the arguments of term a using the arguments args. The number of arguments num_args should coin...
unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a)
Return number of bound variables of quantifier.
Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s)
Check if suffix is a suffix of s.
Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return true if succeeded, and store the result in v.
Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level)
extract a next cube for a solver. The last cube is the constant true or false. The number of (non-con...
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst)
Replace the first occurrence of src with dst in s.
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:176
unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g)
Return the depth of the given goal. It tracks how many transformations were applied to it.
void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry object.
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re)
Create the regular language [re].
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs,...
Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th no_pattern.
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t)
Return the size of the given bit-vector sort.
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g)
Return the "precision" of the given goal. Goals can be transformed using over and under approximation...
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than or equal to.
Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th pattern.
Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)
Add an element to a set.
double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs, Z3_ast v)
n-ary Array update.
Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den)
Create a real from a fraction.
Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.
unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a)
Return a hash code for the given AST. The hash code is structural. You can use Z3_get_ast_id intercha...
Z3_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p)
Convert a parameter set into a string. This function is mainly used for printing the contents of a pa...
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than or equal to.
Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Similar to Z3_mk_forall_const.
Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f)
Create array with the same interpretation as a function. The array satisfies the property (f x) = (se...
Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const *domain, Z3_sort range)
Create an array type with N arguments.
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:98
Z3_string Z3_API Z3_get_full_version(void)
Return a string that fully describes the version of Z3 in use.
Z3_app Z3_API Z3_to_app(Z3_context c, Z3_ast a)
Convert an ast into an APP_AST. This is just type casting.
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...
Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1....
Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context, Z3_string str)
Parse and evaluate and SMT-LIB2 command sequence. The state from a previous call is saved so the next...
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)
Decrement the reference counter of the given goal.
unsigned Z3_API Z3_get_domain_size(Z3_context c, Z3_func_decl d)
Return the number of parameters of the given declaration.
Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s)
Convert a Z3_sort into Z3_ast. This is just type casting.
Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s)
Create a string constant out of the string that is passed in.
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a file.
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
void Z3_API Z3_enable_trace(Z3_string tag)
Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.
Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1)
Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size m+i,...
bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, int64_t *num, int64_t *den)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit as a rational number as mach...
Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f)
Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s.
Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the right i times.
unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p)
Return the number of parameters in the given parameter description set.
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.
Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL,...
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
Definition: z3_api.h:1297
unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)
Return the number of formulas in the given goal.
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
Z3_func_decl Z3_API Z3_get_tuple_sort_mk_decl(Z3_context c, Z3_sort t)
Return the constructor declaration of the given tuple sort.
Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t)
Return the domain of the given array sort. In the case of a multi-dimensional array,...
Z3_model Z3_API Z3_mk_model(Z3_context c)
Create a fresh model object. It has reference count 0.
void Z3_API Z3_solver_import_model_converter(Z3_context ctx, Z3_solver src, Z3_solver dst)
Ad-hoc method for importing model conversion from solver.
Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target)
Copy a solver s from the context source to the context target.
int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s)
Return the symbol int value.
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)
Decrement the reference counter of the given parameter set.
double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0....
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
Z3_ast Z3_API Z3_mk_exists(Z3_context c, unsigned weight, unsigned num_patterns, Z3_pattern const patterns[], unsigned num_decls, Z3_sort const sorts[], Z3_symbol const decl_names[], Z3_ast body)
Create an exists formula. Similar to Z3_mk_forall.
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx)
Return the unsigned value of the given statistical data.
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
unsigned Z3_API Z3_get_num_tactics(Z3_context c)
Return the number of builtin tactics available in Z3.
Z3_param_kind
The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params).
Definition: z3_api.h:1280
bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int....
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a string of a numeric constant term.
bool Z3_API Z3_is_string(Z3_context c, Z3_ast s)
Determine if s is a string constant.
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.
unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int64_t int....
Z3_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See Z3_...
Definition: z3_api.h:112
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_ast Z3_API Z3_get_pattern(Z3_context c, Z3_pattern p, unsigned idx)
Return i'th ast in pattern.
bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx)
Return true if the given statistical data is a double.
unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a)
Return number of patterns used in quantifier.
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers,...
bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Test if there exists an interpretation (i.e., assignment) for a in the model m.
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s)
Create a sequence sort out of the sort for the elements.
bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s)
Check if s is a string sort.
Z3_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t *r)
Store the size of the sort in r. Return false if the call failed. That is, Z3_get_sort_kind(s) == Z3_...
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.
Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p)
Return a tactic that applies t using the given set of parameters.
double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)
Return numeral as a double.
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1)
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)
Create the regular language re*.
Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s)
Check whether the assertions in a given solver are consistent or not.
Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst)
translate model from context c to context dst.
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.
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)
Return a unique identifier for t. The identifier is unique up to structural equality....
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places.
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a)
Obtain weight of quantifier.
Z3_symbol Z3_API Z3_get_quantifier_bound_name(Z3_context c, Z3_ast a, unsigned i)
Return symbol of the i'th bound variable.
Z3_ast Z3_API Z3_app_to_ast(Z3_context c, Z3_app a)
Convert a Z3_app into Z3_ast. This is just type casting.
Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length)
Extract subsequence starting at offset of length.
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)
Return index of first occurrence of substr in s starting from offset offset. If s does not contain su...
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)
Create the range regular expression over two sequences of length 1.
unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g)
Return the number of formulas, subformulas and terms in the given goal.
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
void Z3_API Z3_params_validate(Z3_context c, Z3_params p, Z3_param_descrs d)
Validate the parameter set p against the parameter description set d.
void Z3_API Z3_mk_datatypes(Z3_context c, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort sorts[], Z3_constructor_list constructor_lists[])
Create mutually recursive datatypes.
#define Z3_sort_opt
Definition: z3_api.h:13
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
Z3_ast Z3_API Z3_mk_lambda(Z3_context c, unsigned num_decls, Z3_sort const sorts[], Z3_symbol const decl_names[], Z3_ast body)
Create a lambda expression. It takes an expression body that contains bound variables of the same sor...
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:132
Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].
Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new incremental solver.
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
void Z3_API Z3_reset_memory(void)
Reset all allocated resources.
void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)
Set a configuration parameter.
Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_quantifier_const_ex(Z3_context c, bool is_forall, unsigned weight, Z3_symbol quantifier_id, Z3_symbol skolem_id, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], unsigned num_no_patterns, Z3_ast const no_patterns[], Z3_ast body)
Create a universal or existential quantifier using a list of constants that will form the set of boun...
Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
void Z3_API Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v)
Add a double parameter k with value v to the parameter set p.
void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a)
Add a new formula a to the given goal. The formula is split according to the following procedure that...
Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)
Return the symbol name.
unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)
Return number of constructors for datatype.
Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision)
Return a upper bound for the given real algebraic number. The interval isolating the number is smalle...
Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[])
Create a pattern for quantifier instantiation.
Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences)
retrieve consequences from solver that determine values of the supplied function symbols.
Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i)
Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t)
Return the sort kind (e.g., array, tuple, int, bool, etc).
Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a)
Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.
Z3_param_kind Z3_API Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n)
Return the kind associated with the given parameter name n.
Z3_ast Z3_API Z3_mk_quantifier_ex(Z3_context c, bool is_forall, unsigned weight, Z3_symbol quantifier_id, Z3_symbol skolem_id, unsigned num_patterns, Z3_pattern const patterns[], unsigned num_no_patterns, Z3_ast const no_patterns[], unsigned num_decls, Z3_sort const sorts[], Z3_symbol const decl_names[], Z3_ast body)
Create a quantifier - universal or existential, with pattern hints, no patterns, and attributes.
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
Z3_sort Z3_API Z3_mk_set_sort(Z3_context c, Z3_sort ty)
Create Set type.
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a)
Return number of no_patterns used in quantifier.
unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f)
Return a unique identifier for f.
void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.
void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value)
add a function entry to a function interpretation.
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty)
Create a numeral of an int, bit-vector, or finite-domain sort.
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
unsigned Z3_API Z3_get_num_probes(Z3_context c)
Return the number of builtin probes available in Z3.
Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target)
Translate/Copy the AST a from context source to context target. AST a must have been created using co...
void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)
Return Z3 version number information.
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.
Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s)
Return the set of non units in the solver state.
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables.
Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.
void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v)
Add a symbol parameter k with value v to the parameter set p.
void Z3_API Z3_global_param_reset_all(void)
Restore the value of all global (and module) parameters. This command will not affect already created...
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
Z3_string Z3_API Z3_simplify_get_help(Z3_context c)
Return a string describing all available parameters.
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re)
Check if seq is in the language generated by the regular expression re.
void Z3_error_handler(Z3_context c, Z3_error_code e)
Z3 custom error handler (See Z3_set_error_handler).
Definition: z3_api.h:1346
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
void Z3_API Z3_finalize_memory(void)
Destroy all allocated resources.
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body)
Define the body of a recursive function.
void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value)
Return the 'else' value of the given function interpretation.
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)
Return the parameter description set for the given solver object.
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)
Return the number of entries in the given function interpretation.
bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g)
Return true if the goal is empty, and it is precise or the product of a under approximation.
Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1)
Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n,...
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq)
Create a regular expression that accepts the sequence seq.
double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx)
Return the double value of the given statistical data.
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, bool v)
Add a Boolean parameter k with value v to the parameter set p.
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision)
Return a lower bound for the given real algebraic number. The interval isolating the number is smalle...
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, bool const *bits)
create a bit-vector numeral from a vector of Booleans.
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t)
Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...
Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i)
Return a "point" of the given function interpretation. It represents the value of f in a particular p...
Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, unsigned num_assumptions, Z3_ast const assumptions[], Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the left i times.
expr max(expr const &a, expr const &b)
Definition: z3++.h:1499
Z3_string Z3_API Z3_func_decl_to_string(Z3_context c, Z3_func_decl d)
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, unsigned num_constructors, Z3_constructor const constructors[])
Create list of constructors.
Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx)
Return a formula from the given goal.
Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d)
Return the sort name as a symbol.
void Z3_API Z3_query_constructor(Z3_context c, Z3_constructor constr, unsigned num_fields, Z3_func_decl *constructor, Z3_func_decl *tester, Z3_func_decl accessors[])
Query constructor for declared functions.
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
Z3_string Z3_API Z3_probe_get_descr(Z3_context c, Z3_string name)
Return a string containing a description of the probe with the given name.
Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const *args)
Map f on the argument arrays.
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value)
Get a global (or module) parameter.
bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, int64_t *num, int64_t *den)
Return numeral value, as a pair of 64 bit numbers if the representation fits.
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...
Z3_ast Z3_API Z3_datatype_update_field(Z3_context c, Z3_func_decl field_access, Z3_ast t, Z3_ast value)
Update record field with a value.
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e)
Decrement the reference counter of the given Z3_func_entry object.
Z3_string Z3_API Z3_tactic_get_descr(Z3_context c, Z3_string name)
Return a string containing a description of the tactic with the given name.
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:982
Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read.
bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a)
The (_ as-array f) AST node is a construct for assigning interpretations for arrays in Z3....
unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r)
Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq)
Create a regular expression sort out of a sequence sort.
Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.
Z3_tactic Z3_API Z3_tactic_fail_if_not_decided(Z3_context c)
Return a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsati...
bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.
Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 or p2 evaluates to true.
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.
Z3_tactic Z3_API Z3_tactic_fail(Z3_context c)
Return a tactic that always fails.
Z3_ast Z3_API Z3_mk_iff(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 iff t2.
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th constructor.
unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s)
Return the number of backtracking points.
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
#define Z3_ast_opt
Definition: z3_api.h:16
Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])
Create a enumeration sort.
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.
Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a recursive function.
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.
void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p)
Decrement the reference counter of the given parameter description set.
Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the sort value associated with a sort parameter.
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.
Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1)
Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i,...
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:82
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.
Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs)
n-ary Array read. The argument a is the array and idxs are the indices of the array that gets read.