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 
1006 typedef enum {
1007  // Basic
1008  Z3_OP_TRUE = 0x100,
1020 
1021  // Arithmetic
1022  Z3_OP_ANUM = 0x200,
1040 
1041  // Arrays & Sets
1042  Z3_OP_STORE = 0x300,
1054 
1055  // Bit-vectors
1056  Z3_OP_BNUM = 0x400,
1063 
1069 
1070  // special functions to record the division by 0 cases
1071  // these are internal functions
1077 
1086 
1094 
1100 
1104 
1112 
1118 
1127 
1128  // Proofs
1171 
1172  // Relational algebra
1188 
1189  // Sequences
1205 
1206  // strings
1209 
1210  // regular expressions
1222 
1223  // Auxiliary
1224  Z3_OP_LABEL = 0x700,
1226 
1227  // Datatypes
1233 
1234  // Pseudo Booleans
1240 
1241  // Special relations
1248 
1249 
1250  // Floating-Point Arithmetic
1256 
1263 
1276 
1289 
1296 
1298 
1301 
1303 
1305 } Z3_decl_kind;
1306 
1319 typedef enum {
1327 } Z3_param_kind;
1328 
1336 typedef enum {
1341 
1342 
1360 typedef enum
1361 {
1375 } Z3_error_code;
1376 
1385 typedef void Z3_error_handler(Z3_context c, Z3_error_code e);
1386 
1397 typedef enum
1398 {
1403 } Z3_goal_prec;
1404 
1407 #ifdef __cplusplus
1408 extern "C" {
1409 #endif // __cplusplus
1410 
1437  void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value);
1438 
1439 
1448  void Z3_API Z3_global_param_reset_all(void);
1449 
1462  Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value);
1463 
1468 
1498  Z3_config Z3_API Z3_mk_config(void);
1499 
1506  void Z3_API Z3_del_config(Z3_config c);
1507 
1516  void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value);
1517 
1522 
1548  Z3_context Z3_API Z3_mk_context(Z3_config c);
1549 
1571  Z3_context Z3_API Z3_mk_context_rc(Z3_config c);
1572 
1579  void Z3_API Z3_del_context(Z3_context c);
1580 
1587  void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a);
1588 
1595  void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a);
1596 
1603  void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value);
1604 
1610  void Z3_API Z3_interrupt(Z3_context c);
1611 
1612 
1617 
1627  Z3_params Z3_API Z3_mk_params(Z3_context c);
1628 
1633  void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p);
1634 
1639  void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p);
1640 
1645  void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, bool v);
1646 
1651  void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v);
1652 
1657  void Z3_API Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v);
1658 
1663  void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v);
1664 
1670  Z3_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p);
1671 
1678  void Z3_API Z3_params_validate(Z3_context c, Z3_params p, Z3_param_descrs d);
1679 
1684 
1689  void Z3_API Z3_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p);
1690 
1695  void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p);
1696 
1701  Z3_param_kind Z3_API Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n);
1702 
1707  unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p);
1708 
1715  Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i);
1716 
1721  Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s);
1722 
1728  Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p);
1729 
1734 
1747  Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i);
1748 
1758  Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s);
1759 
1764 
1771  Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s);
1772 
1779  Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c);
1780 
1791  Z3_sort Z3_API Z3_mk_int_sort(Z3_context c);
1792 
1799  Z3_sort Z3_API Z3_mk_real_sort(Z3_context c);
1800 
1809  Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz);
1810 
1823  Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size);
1824 
1835  Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range);
1836 
1844  Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const * domain, Z3_sort range);
1845 
1861  Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c,
1862  Z3_symbol mk_tuple_name,
1863  unsigned num_fields,
1864  Z3_symbol const field_names[],
1865  Z3_sort const field_sorts[],
1866  Z3_func_decl * mk_tuple_decl,
1867  Z3_func_decl proj_decl[]);
1868 
1889  Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c,
1890  Z3_symbol name,
1891  unsigned n,
1892  Z3_symbol const enum_names[],
1893  Z3_func_decl enum_consts[],
1894  Z3_func_decl enum_testers[]);
1895 
1913  Z3_sort Z3_API Z3_mk_list_sort(Z3_context c,
1914  Z3_symbol name,
1915  Z3_sort elem_sort,
1916  Z3_func_decl* nil_decl,
1917  Z3_func_decl* is_nil_decl,
1918  Z3_func_decl* cons_decl,
1919  Z3_func_decl* is_cons_decl,
1920  Z3_func_decl* head_decl,
1921  Z3_func_decl* tail_decl
1922  );
1923 
1942  Z3_constructor Z3_API Z3_mk_constructor(Z3_context c,
1943  Z3_symbol name,
1944  Z3_symbol recognizer,
1945  unsigned num_fields,
1946  Z3_symbol const field_names[],
1947  Z3_sort_opt const sorts[],
1948  unsigned sort_refs[]
1949  );
1950 
1960  void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr);
1961 
1976  Z3_sort Z3_API Z3_mk_datatype(Z3_context c,
1977  Z3_symbol name,
1978  unsigned num_constructors,
1979  Z3_constructor constructors[]);
1980 
1992  Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c,
1993  unsigned num_constructors,
1994  Z3_constructor const constructors[]);
1995 
2007  void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist);
2008 
2023  void Z3_API Z3_mk_datatypes(Z3_context c,
2024  unsigned num_sorts,
2025  Z3_symbol const sort_names[],
2026  Z3_sort sorts[],
2027  Z3_constructor_list constructor_lists[]);
2028 
2042  void Z3_API Z3_query_constructor(Z3_context c,
2043  Z3_constructor constr,
2044  unsigned num_fields,
2045  Z3_func_decl* constructor,
2046  Z3_func_decl* tester,
2047  Z3_func_decl accessors[]);
2048 
2053 
2072  Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s,
2073  unsigned domain_size, Z3_sort const domain[],
2074  Z3_sort range);
2075 
2076 
2077 
2086  Z3_ast Z3_API Z3_mk_app(
2087  Z3_context c,
2088  Z3_func_decl d,
2089  unsigned num_args,
2090  Z3_ast const args[]);
2091 
2106  Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty);
2107 
2119  Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix,
2120  unsigned domain_size, Z3_sort const domain[],
2121  Z3_sort range);
2122 
2137  Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty);
2138 
2139 
2158  Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s,
2159  unsigned domain_size, Z3_sort const domain[],
2160  Z3_sort range);
2161 
2177  void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body);
2178 
2187  Z3_ast Z3_API Z3_mk_true(Z3_context c);
2188 
2193  Z3_ast Z3_API Z3_mk_false(Z3_context c);
2194 
2201  Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r);
2202 
2214  Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[]);
2215 
2222  Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a);
2223 
2231  Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3);
2232 
2239  Z3_ast Z3_API Z3_mk_iff(Z3_context c, Z3_ast t1, Z3_ast t2);
2240 
2247  Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2);
2248 
2255  Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2);
2256 
2266  Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[]);
2267 
2277  Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[]);
2291  Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[]);
2292 
2303  Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[]);
2304 
2314  Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[]);
2315 
2322  Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg);
2323 
2332  Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2333 
2340  Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2341 
2348  Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2349 
2356  Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2357 
2364  Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2);
2365 
2372  Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2);
2373 
2380  Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2);
2381 
2388  Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2);
2389 
2406  Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1);
2407 
2418  Z3_ast Z3_API Z3_mk_real2int(Z3_context c, Z3_ast t1);
2419 
2427  Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1);
2438  Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1);
2439 
2446  Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1);
2447 
2454  Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1);
2455 
2462  Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2);
2463 
2470  Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2);
2471 
2478  Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2);
2479 
2486  Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2);
2487 
2494  Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2);
2495 
2502  Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2);
2503 
2510  Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1);
2511 
2518  Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2);
2519 
2526  Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2);
2527 
2534  Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2);
2535 
2546  Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2);
2547 
2562  Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2);
2563 
2574  Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2);
2575 
2589  Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2);
2590 
2601  Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2);
2602 
2609  Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2);
2610 
2625  Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2);
2626 
2633  Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2);
2634 
2641  Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2);
2642 
2649  Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2);
2650 
2657  Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2);
2658 
2665  Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2);
2666 
2673  Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2);
2674 
2684  Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2);
2685 
2693  Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1);
2694 
2703  Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1);
2704 
2713  Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1);
2714 
2721  Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1);
2722 
2736  Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2);
2737 
2751  Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2);
2752 
2767  Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2);
2768 
2775  Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1);
2776 
2783  Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1);
2784 
2791  Z3_ast Z3_API Z3_mk_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2);
2792 
2799  Z3_ast Z3_API Z3_mk_ext_rotate_right(Z3_context c, Z3_ast t1, Z3_ast t2);
2800 
2810  Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1);
2811 
2823  Z3_ast Z3_API Z3_mk_bv2int(Z3_context c,Z3_ast t1, bool is_signed);
2824 
2832  Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);
2833 
2841  Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2);
2842 
2850  Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2);
2851 
2859  Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);
2860 
2868  Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2);
2869 
2877  Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1);
2878 
2886  Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);
2887 
2895  Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2);
2912  Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i);
2913 
2914 
2915 
2922  Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs);
2923 
2924 
2940  Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v);
2941 
2942 
2948  Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs, Z3_ast v);
2949 
2961  Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v);
2962 
2975  Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const* args);
2976 
2986  Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array);
2987 
2994  Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f);
2995 
3000  Z3_ast Z3_API Z3_mk_set_has_size(Z3_context c, Z3_ast set, Z3_ast k);
3001 
3010  Z3_sort Z3_API Z3_mk_set_sort(Z3_context c, Z3_sort ty);
3011 
3016  Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain);
3017 
3022  Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain);
3023 
3030  Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem);
3031 
3038  Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem);
3039 
3044  Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[]);
3045 
3050  Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[]);
3051 
3056  Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2);
3057 
3062  Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg);
3063 
3070  Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set);
3071 
3076  Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2);
3077 
3085  Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2);
3102  Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty);
3103 
3118  Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den);
3119 
3129  Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty);
3130 
3140  Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty);
3141 
3151  Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty);
3152 
3162  Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty);
3163 
3169  Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, bool const* bits);
3170 
3175 
3180  Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s);
3181 
3186  bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s);
3187 
3192  Z3_sort Z3_API Z3_get_seq_sort_basis(Z3_context c, Z3_sort s);
3193 
3198  Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq);
3199 
3204  bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s);
3205 
3210  Z3_sort Z3_API Z3_get_re_sort_basis(Z3_context c, Z3_sort s);
3211 
3219  Z3_sort Z3_API Z3_mk_string_sort(Z3_context c);
3220 
3225  bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s);
3226 
3230  Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s);
3231 
3238  Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned len, Z3_string s);
3239 
3244  bool Z3_API Z3_is_string(Z3_context c, Z3_ast s);
3245 
3252  Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s);
3253 
3260  Z3_string Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length);
3261 
3268  Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq);
3269 
3274  Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a);
3275 
3282  Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[]);
3283 
3290  Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s);
3291 
3298  Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s);
3299 
3306  Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee);
3307 
3308 
3315  Z3_ast Z3_API Z3_mk_str_lt(Z3_context c, Z3_ast prefix, Z3_ast s);
3316 
3323  Z3_ast Z3_API Z3_mk_str_le(Z3_context c, Z3_ast prefix, Z3_ast s);
3324 
3329  Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length);
3330 
3335  Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst);
3336 
3342  Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index);
3343 
3349  Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index);
3350 
3355  Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s);
3356 
3357 
3364  Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);
3365 
3370  Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast, Z3_ast substr);
3371 
3376  Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s);
3377 
3378 
3383  Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s);
3384 
3389  Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq);
3390 
3395  Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re);
3396 
3401  Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re);
3402 
3407  Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re);
3408 
3413  Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re);
3414 
3421  Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[]);
3422 
3429  Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[]);
3430 
3431 
3436  Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi);
3437 
3445  Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi);
3446 
3453  Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[]);
3454 
3459  Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re);
3460 
3467  Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re);
3468 
3469 
3476  Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re);
3477 
3488  Z3_func_decl Z3_API Z3_mk_linear_order(Z3_context c, Z3_sort a, unsigned id);
3489 
3494  Z3_func_decl Z3_API Z3_mk_partial_order(Z3_context c, Z3_sort a, unsigned id);
3495 
3500  Z3_func_decl Z3_API Z3_mk_piecewise_linear_order(Z3_context c, Z3_sort a, unsigned id);
3501 
3506  Z3_func_decl Z3_API Z3_mk_tree_order(Z3_context c, Z3_sort a, unsigned id);
3507 
3516  Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f);
3517 
3541  Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[]);
3542 
3571  Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty);
3572 
3595  Z3_ast Z3_API Z3_mk_forall(Z3_context c, unsigned weight,
3596  unsigned num_patterns, Z3_pattern const patterns[],
3597  unsigned num_decls, Z3_sort const sorts[],
3598  Z3_symbol const decl_names[],
3599  Z3_ast body);
3600 
3610  Z3_ast Z3_API Z3_mk_exists(Z3_context c, unsigned weight,
3611  unsigned num_patterns, Z3_pattern const patterns[],
3612  unsigned num_decls, Z3_sort const sorts[],
3613  Z3_symbol const decl_names[],
3614  Z3_ast body);
3615 
3636  Z3_ast Z3_API Z3_mk_quantifier(
3637  Z3_context c,
3638  bool is_forall,
3639  unsigned weight,
3640  unsigned num_patterns, Z3_pattern const patterns[],
3641  unsigned num_decls, Z3_sort const sorts[],
3642  Z3_symbol const decl_names[],
3643  Z3_ast body);
3644 
3645 
3669  Z3_ast Z3_API Z3_mk_quantifier_ex(
3670  Z3_context c,
3671  bool is_forall,
3672  unsigned weight,
3673  Z3_symbol quantifier_id,
3674  Z3_symbol skolem_id,
3675  unsigned num_patterns, Z3_pattern const patterns[],
3676  unsigned num_no_patterns, Z3_ast const no_patterns[],
3677  unsigned num_decls, Z3_sort const sorts[],
3678  Z3_symbol const decl_names[],
3679  Z3_ast body);
3680 
3698  Z3_ast Z3_API Z3_mk_forall_const(
3699  Z3_context c,
3700  unsigned weight,
3701  unsigned num_bound,
3702  Z3_app const bound[],
3703  unsigned num_patterns,
3704  Z3_pattern const patterns[],
3705  Z3_ast body
3706  );
3707 
3727  Z3_ast Z3_API Z3_mk_exists_const(
3728  Z3_context c,
3729  unsigned weight,
3730  unsigned num_bound,
3731  Z3_app const bound[],
3732  unsigned num_patterns,
3733  Z3_pattern const patterns[],
3734  Z3_ast body
3735  );
3736 
3742  Z3_ast Z3_API Z3_mk_quantifier_const(
3743  Z3_context c,
3744  bool is_forall,
3745  unsigned weight,
3746  unsigned num_bound, Z3_app const bound[],
3747  unsigned num_patterns, Z3_pattern const patterns[],
3748  Z3_ast body
3749  );
3750 
3756  Z3_ast Z3_API Z3_mk_quantifier_const_ex(
3757  Z3_context c,
3758  bool is_forall,
3759  unsigned weight,
3760  Z3_symbol quantifier_id,
3761  Z3_symbol skolem_id,
3762  unsigned num_bound, Z3_app const bound[],
3763  unsigned num_patterns, Z3_pattern const patterns[],
3764  unsigned num_no_patterns, Z3_ast const no_patterns[],
3765  Z3_ast body
3766  );
3767 
3790  Z3_ast Z3_API Z3_mk_lambda(Z3_context c,
3791  unsigned num_decls, Z3_sort const sorts[],
3792  Z3_symbol const decl_names[],
3793  Z3_ast body);
3794 
3809  Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c,
3810  unsigned num_bound, Z3_app const bound[],
3811  Z3_ast body);
3812 
3813 
3824  Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s);
3825 
3834  int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s);
3835 
3848  Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s);
3849 
3854  Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d);
3855 
3860  unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s);
3861 
3866  Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s);
3867 
3872  bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2);
3873 
3880  Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t);
3881 
3891  unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t);
3892 
3898  Z3_bool_opt Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r);
3899 
3910  Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t);
3911 
3921  Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t);
3922 
3933  Z3_func_decl Z3_API Z3_get_tuple_sort_mk_decl(Z3_context c, Z3_sort t);
3934 
3944  unsigned Z3_API Z3_get_tuple_sort_num_fields(Z3_context c, Z3_sort t);
3945 
3957  Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t, unsigned i);
3958 
3969  unsigned Z3_API Z3_get_datatype_sort_num_constructors(
3970  Z3_context c, Z3_sort t);
3971 
3983  Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(
3984  Z3_context c, Z3_sort t, unsigned idx);
3985 
3997  Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(
3998  Z3_context c, Z3_sort t, unsigned idx);
3999 
4012  Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c,
4013  Z3_sort t,
4014  unsigned idx_c,
4015  unsigned idx_a);
4016 
4035  Z3_ast Z3_API Z3_datatype_update_field(Z3_context c, Z3_func_decl field_access,
4036  Z3_ast t, Z3_ast value);
4037 
4046  unsigned Z3_API Z3_get_relation_arity(Z3_context c, Z3_sort s);
4047 
4057  Z3_sort Z3_API Z3_get_relation_column(Z3_context c, Z3_sort s, unsigned col);
4058 
4065  Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args,
4066  Z3_ast const args[], unsigned k);
4067 
4074  Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args,
4075  Z3_ast const args[], unsigned k);
4076 
4083  Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args,
4084  Z3_ast const args[], int const coeffs[],
4085  int k);
4086 
4093  Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args,
4094  Z3_ast const args[], int const coeffs[],
4095  int k);
4096 
4103  Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args,
4104  Z3_ast const args[], int const coeffs[],
4105  int k);
4106 
4111  Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f);
4112 
4117  bool Z3_API Z3_is_eq_func_decl(Z3_context c, Z3_func_decl f1, Z3_func_decl f2);
4118 
4123  unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f);
4124 
4129  Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d);
4130 
4135  Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d);
4136 
4143  unsigned Z3_API Z3_get_domain_size(Z3_context c, Z3_func_decl d);
4144 
4151  unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d);
4152 
4161  Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i);
4162 
4170  Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d);
4171 
4176  unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d);
4177 
4186  Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx);
4187 
4194  int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4195 
4202  double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4203 
4210  Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4211 
4218  Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4219 
4226  Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4227 
4234  Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4235 
4242  Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4243 
4248  Z3_ast Z3_API Z3_app_to_ast(Z3_context c, Z3_app a);
4249 
4254  Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a);
4255 
4261  unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a);
4262 
4269  Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i);
4270 
4275  bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2);
4276 
4287  unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t);
4288 
4295  unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a);
4296 
4303  Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a);
4304 
4309  bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t);
4310 
4315  Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a);
4316 
4321  Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a);
4322 
4325  bool Z3_API Z3_is_app(Z3_context c, Z3_ast a);
4326 
4329  bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a);
4330 
4335  bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a);
4336 
4343  Z3_app Z3_API Z3_to_app(Z3_context c, Z3_ast a);
4344 
4351  Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a);
4352 
4359  Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a);
4360 
4368  Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision);
4369 
4376  double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a);
4377 
4384  Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a);
4385 
4392  Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a);
4393 
4407  bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, int64_t* num, int64_t* den);
4408 
4418  bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int* i);
4419 
4429  bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned* u);
4430 
4440  bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t* u);
4441 
4451  bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t* i);
4452 
4462  bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, int64_t* num, int64_t* den);
4463 
4472  Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision);
4473 
4482  Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision);
4483 
4488  Z3_ast Z3_API Z3_pattern_to_ast(Z3_context c, Z3_pattern p);
4489 
4494  unsigned Z3_API Z3_get_pattern_num_terms(Z3_context c, Z3_pattern p);
4495 
4500  Z3_ast Z3_API Z3_get_pattern(Z3_context c, Z3_pattern p, unsigned idx);
4501 
4508  unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a);
4509 
4514  bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a);
4515 
4521  bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a);
4522 
4529  bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a);
4530 
4537  unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a);
4538 
4545  unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a);
4546 
4553  Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i);
4554 
4561  unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a);
4562 
4569  Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i);
4570 
4577  unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a);
4578 
4585  Z3_symbol Z3_API Z3_get_quantifier_bound_name(Z3_context c, Z3_ast a, unsigned i);
4586 
4593  Z3_sort Z3_API Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, unsigned i);
4594 
4601  Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a);
4602 
4614  Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a);
4615 
4628  Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p);
4629 
4637  Z3_string Z3_API Z3_simplify_get_help(Z3_context c);
4638 
4646  Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c);
4658  Z3_ast Z3_API Z3_update_term(Z3_context c, Z3_ast a, unsigned num_args, Z3_ast const args[]);
4659 
4666  Z3_ast Z3_API Z3_substitute(Z3_context c,
4667  Z3_ast a,
4668  unsigned num_exprs,
4669  Z3_ast const from[],
4670  Z3_ast const to[]);
4671 
4677  Z3_ast Z3_API Z3_substitute_vars(Z3_context c,
4678  Z3_ast a,
4679  unsigned num_exprs,
4680  Z3_ast const to[]);
4681 
4688  Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target);
4693 
4698  Z3_model Z3_API Z3_mk_model(Z3_context c);
4699 
4704  void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m);
4705 
4710  void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m);
4711 
4734  Z3_bool_opt Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v);
4735 
4744  Z3_ast_opt Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a);
4745 
4750  bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a);
4751 
4763  Z3_func_interp_opt Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f);
4764 
4771  unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m);
4772 
4781  Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i);
4782 
4790  unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m);
4791 
4800  Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i);
4801 
4813  unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m);
4814 
4824  Z3_sort Z3_API Z3_model_get_sort(Z3_context c, Z3_model m, unsigned i);
4825 
4833  Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s);
4834 
4839  Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst);
4840 
4851  bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a);
4852 
4859  Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a);
4860 
4871  Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value);
4872 
4877  void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a);
4878 
4883  void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f);
4884 
4889  void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f);
4890 
4899  unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f);
4900 
4910  Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i);
4911 
4919  Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f);
4920 
4928  void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value);
4929 
4934  unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f);
4935 
4949  void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value);
4950 
4955  void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e);
4956 
4961  void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e);
4962 
4972  Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e);
4973 
4980  unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e);
4981 
4990  Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i);
4999  bool Z3_API Z3_open_log(Z3_string filename);
5000 
5009  void Z3_API Z3_append_log(Z3_string string);
5010 
5015  void Z3_API Z3_close_log(void);
5016 
5024  void Z3_API Z3_toggle_warning_messages(bool enabled);
5045  void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode);
5046 
5058  Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a);
5059 
5062  Z3_string Z3_API Z3_pattern_to_string(Z3_context c, Z3_pattern p);
5063 
5066  Z3_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s);
5067 
5070  Z3_string Z3_API Z3_func_decl_to_string(Z3_context c, Z3_func_decl d);
5071 
5080  Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m);
5081 
5099  Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c,
5100  Z3_string name,
5101  Z3_string logic,
5102  Z3_string status,
5103  Z3_string attributes,
5104  unsigned num_assumptions,
5105  Z3_ast const assumptions[],
5106  Z3_ast formula);
5107 
5119  Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c,
5120  Z3_string str,
5121  unsigned num_sorts,
5122  Z3_symbol const sort_names[],
5123  Z3_sort const sorts[],
5124  unsigned num_decls,
5125  Z3_symbol const decl_names[],
5126  Z3_func_decl const decls[]);
5127 
5132  Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c,
5133  Z3_string file_name,
5134  unsigned num_sorts,
5135  Z3_symbol const sort_names[],
5136  Z3_sort const sorts[],
5137  unsigned num_decls,
5138  Z3_symbol const decl_names[],
5139  Z3_func_decl const decls[]);
5140 
5141 
5150  Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context, Z3_string str);
5151 
5156 #ifndef SAFE_ERRORS
5157 
5166  Z3_error_code Z3_API Z3_get_error_code(Z3_context c);
5167 
5180  void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h);
5181 #endif
5182 
5187  void Z3_API Z3_set_error(Z3_context c, Z3_error_code e);
5188 
5193  Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err);
5194 
5199 
5206  void Z3_API Z3_get_version(unsigned * major, unsigned * minor, unsigned * build_number, unsigned * revision_number);
5207 
5214  Z3_string Z3_API Z3_get_full_version(void);
5215 
5223  void Z3_API Z3_enable_trace(Z3_string tag);
5224 
5232  void Z3_API Z3_disable_trace(Z3_string tag);
5233 
5243  void Z3_API Z3_reset_memory(void);
5244 
5252  void Z3_API Z3_finalize_memory(void);
5273  Z3_goal Z3_API Z3_mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs);
5274 
5279  void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g);
5280 
5285  void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g);
5286 
5293  Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g);
5294 
5306  void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a);
5307 
5312  bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g);
5313 
5318  unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g);
5319 
5324  void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g);
5325 
5330  unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g);
5331 
5338  Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx);
5339 
5344  unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g);
5345 
5350  bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g);
5351 
5356  bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g);
5357 
5362  Z3_goal Z3_API Z3_goal_translate(Z3_context source, Z3_goal g, Z3_context target);
5363 
5370  Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m);
5371 
5376  Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g);
5377 
5387  Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g);
5388 
5401  Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name);
5402 
5407  void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t);
5408 
5413  void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g);
5414 
5424  Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name);
5425 
5430  void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p);
5431 
5436  void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p);
5437 
5443  Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2);
5444 
5450  Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2);
5451 
5456  Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[]);
5457 
5463  Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2);
5464 
5470  Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms);
5471 
5477  Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t);
5478 
5484  Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2);
5485 
5491  Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max);
5492 
5497  Z3_tactic Z3_API Z3_tactic_skip(Z3_context c);
5498 
5503  Z3_tactic Z3_API Z3_tactic_fail(Z3_context c);
5504 
5509  Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p);
5510 
5516  Z3_tactic Z3_API Z3_tactic_fail_if_not_decided(Z3_context c);
5517 
5522  Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p);
5523 
5528  Z3_probe Z3_API Z3_probe_const(Z3_context x, double val);
5529 
5536  Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2);
5537 
5544  Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2);
5545 
5552  Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2);
5553 
5560  Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2);
5561 
5568  Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2);
5569 
5576  Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2);
5577 
5584  Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2);
5585 
5592  Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p);
5593 
5598  unsigned Z3_API Z3_get_num_tactics(Z3_context c);
5599 
5606  Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i);
5607 
5612  unsigned Z3_API Z3_get_num_probes(Z3_context c);
5613 
5620  Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i);
5621 
5626  Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t);
5627 
5632  Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t);
5633 
5638  Z3_string Z3_API Z3_tactic_get_descr(Z3_context c, Z3_string name);
5639 
5644  Z3_string Z3_API Z3_probe_get_descr(Z3_context c, Z3_string name);
5645 
5651  double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g);
5652 
5657  Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g);
5658 
5663  Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p);
5664 
5669  void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r);
5670 
5675  void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r);
5676 
5681  Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r);
5682 
5687  unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r);
5688 
5695  Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i);
5696 
5736  Z3_solver Z3_API Z3_mk_solver(Z3_context c);
5737 
5762  Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c);
5763 
5772  Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic);
5773 
5783  Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t);
5784 
5789  Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target);
5790 
5803  void Z3_API Z3_solver_import_model_converter(Z3_context ctx, Z3_solver src, Z3_solver dst);
5804 
5812  Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s);
5813 
5821  Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s);
5822 
5830  void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p);
5831 
5836  void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s);
5837 
5842  void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s);
5843 
5853  void Z3_API Z3_solver_push(Z3_context c, Z3_solver s);
5854 
5864  void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n);
5865 
5873  void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s);
5874 
5882  unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s);
5883 
5894  void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a);
5895 
5912  void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p);
5913 
5921  void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name);
5922 
5930  void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name);
5931 
5936  Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s);
5937 
5942  Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s);
5943 
5949  Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s);
5950 
5955  Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s);
5956 
5962  void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[]);
5963 
5981  Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s);
5982 
5993  Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s,
5994  unsigned num_assumptions, Z3_ast const assumptions[]);
5995 
6013  Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c,
6014  Z3_solver s,
6015  unsigned num_terms,
6016  Z3_ast const terms[],
6017  unsigned class_ids[]);
6018 
6024  Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c,
6025  Z3_solver s,
6026  Z3_ast_vector assumptions,
6027  Z3_ast_vector variables,
6028  Z3_ast_vector consequences);
6029 
6030 
6048  Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level);
6049 
6057  Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s);
6058 
6067  Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s);
6068 
6079  Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s);
6080 
6086  Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s);
6087 
6094  Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s);
6095 
6103  Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s);
6104 
6110  Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s);
6111 
6116 
6121  Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s);
6122 
6127  void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s);
6128 
6133  void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s);
6134 
6139  unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s);
6140 
6147  Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx);
6148 
6155  bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx);
6156 
6163  bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx);
6164 
6171  unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx);
6172 
6179  double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx);
6180 
6185  uint64_t Z3_API Z3_get_estimated_alloc_size(void);
6186 
6189 #ifdef __cplusplus
6190 }
6191 #endif // __cplusplus
6192 
6195 #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.
Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f)
create transitive closure of binary relation.
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. The sequence is empty if the index is...
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_sort Z3_API Z3_get_seq_sort_basis(Z3_context c, Z3_sort s)
Retrieve basis sort for sequence sort.
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:3370
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:1362
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:1397
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_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s)
Convert a solver into a DIMACS formatted string.
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1360
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.
Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the element positioned at position index. The function is under-specified if the inde...
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_ast Z3_API Z3_mk_str_le(Z3_context c, Z3_ast prefix, Z3_ast s)
Check if s1 is equal or lexicographically strictly less than s2.
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.
Z3_sort Z3_API Z3_get_re_sort_basis(Z3_context c, Z3_sort s)
Retrieve basis sort for regex sort.
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_func_decl Z3_API Z3_mk_piecewise_linear_order(Z3_context c, Z3_sort a, unsigned id)
create a piecewise linear ordering relation over signature a and index id.
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:1336
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:1319
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_string Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned *length)
Retrieve the unescaped string constant stored in s.
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_func_decl Z3_API Z3_mk_tree_order(Z3_context c, Z3_sort a, unsigned id)
create a tree ordering relation over signature a identified using index id.
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.
Z3_func_decl Z3_API Z3_mk_partial_order(Z3_context c, Z3_sort a, unsigned id)
create a partial ordering relation over signature a and index id.
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_lstring(Z3_context c, unsigned len, Z3_string s)
Create a string constant out of the string that is passed in It takes the length of the string as wel...
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.
Z3_func_decl Z3_API Z3_mk_linear_order(Z3_context c, Z3_sort a, unsigned id)
create a linear ordering relation over signature a. The relation is identified by the index id.
void Z3_error_handler(Z3_context c, Z3_error_code e)
Z3 custom error handler (See Z3_set_error_handler).
Definition: z3_api.h:1385
Z3_ast Z3_API Z3_mk_str_lt(Z3_context c, Z3_ast prefix, Z3_ast s)
Check if s1 is lexicographically strictly less than s2.
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.
void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[])
retrieve the decision depth of Boolean literals (variables or their negations). Assumes a check-sat c...
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:1580
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:1006
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_mk_set_has_size(Z3_context c, Z3_ast set, Z3_ast k)
Create predicate that holds if Boolean array set has k elements set to true.
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_last_index(Z3_context c, Z3_ast, Z3_ast substr)
Return the last occurrence of substr in s. If s does not contain substr, then the value is -1,...
Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s)
Return the trail modulo model conversion, in order of decision level The decision level can be retrie...
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.