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 
39 #ifndef __int64
40 #define __int64 long long
41 #endif
42 
43 #ifndef __uint64
44 #define __uint64 unsigned long long
45 #endif
46 
49 
84 typedef int Z3_bool;
85 
89 typedef const char * Z3_string;
91 
95 #define Z3_TRUE 1
96 
100 #define Z3_FALSE 0
101 
105 typedef enum
106 {
110 } Z3_lbool;
111 
119 typedef enum
120 {
124 
125 
139 typedef enum
140 {
149 
153 typedef enum
154 {
169 } Z3_sort_kind;
170 
183 typedef enum
184 {
192 } Z3_ast_kind;
193 
955 typedef enum {
956  // Basic
957  Z3_OP_TRUE = 0x100,
970 
971  // Arithmetic
972  Z3_OP_ANUM = 0x200,
990 
991  // Arrays & Sets
992  Z3_OP_STORE = 0x300,
1004 
1005  // Bit-vectors
1006  Z3_OP_BNUM = 0x400,
1013 
1019 
1020  // special functions to record the division by 0 cases
1021  // these are internal functions
1027 
1036 
1044 
1050 
1054 
1062 
1067 
1076 
1077  // Proofs
1118 
1119  // Relational algebra
1135 
1136  // Sequences
1150 
1151  // regular expressions
1157 
1158  // Auxiliary
1159  Z3_OP_LABEL = 0x700,
1161 
1162  // Datatypes
1167 
1168  // Pseudo Booleans
1173 
1174  // Floating-Point Arithmetic
1180 
1187 
1200 
1213 
1220 
1222 
1225 
1227 
1229 } Z3_decl_kind;
1230 
1243 typedef enum {
1251 } Z3_param_kind;
1252 
1261 typedef enum {
1267 
1268 
1286 typedef enum
1287 {
1301 } Z3_error_code;
1302 
1337 typedef void Z3_error_handler(Z3_context c, Z3_error_code e);
1338 
1349 typedef enum
1350 {
1355 } Z3_goal_prec;
1356 
1359 #ifdef __cplusplus
1360 extern "C" {
1361 #endif // __cplusplus
1362 
1386  void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value);
1387 
1388 
1396  void Z3_API Z3_global_param_reset_all(void);
1397 
1409  Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value);
1410 
1415 
1446  Z3_config Z3_API Z3_mk_config(void);
1447 
1455  void Z3_API Z3_del_config(Z3_config c);
1456 
1466  void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value);
1467 
1472 
1499  Z3_context Z3_API Z3_mk_context(Z3_config c);
1500 
1522  Z3_context Z3_API Z3_mk_context_rc(Z3_config c);
1523 
1530  void Z3_API Z3_del_context(Z3_context c);
1531 
1538  void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a);
1539 
1546  void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a);
1547 
1555  void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value);
1556 
1562  void Z3_API Z3_interrupt(Z3_context c);
1563 
1564 
1569 
1579  Z3_params Z3_API Z3_mk_params(Z3_context c);
1580 
1585  void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p);
1586 
1591  void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p);
1592 
1597  void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, Z3_bool v);
1598 
1603  void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v);
1604 
1609  void Z3_API Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v);
1610 
1615  void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v);
1616 
1622  Z3_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p);
1623 
1630  void Z3_API Z3_params_validate(Z3_context c, Z3_params p, Z3_param_descrs d);
1631 
1636 
1641  void Z3_API Z3_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p);
1642 
1647  void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p);
1648 
1653  Z3_param_kind Z3_API Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n);
1654 
1659  unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p);
1660 
1667  Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i);
1668 
1673  Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s);
1674 
1680  Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p);
1681 
1686 
1698  Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i);
1699 
1708  Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s);
1709 
1714 
1721  Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s);
1722 
1729  Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c);
1730 
1741  Z3_sort Z3_API Z3_mk_int_sort(Z3_context c);
1742 
1749  Z3_sort Z3_API Z3_mk_real_sort(Z3_context c);
1750 
1759  Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz);
1760 
1773  Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, unsigned __int64 size);
1774 
1785  Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range);
1786 
1802  Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c,
1803  Z3_symbol mk_tuple_name,
1804  unsigned num_fields,
1805  Z3_symbol const field_names[],
1806  Z3_sort const field_sorts[],
1807  Z3_func_decl * mk_tuple_decl,
1808  Z3_func_decl proj_decl[]);
1809 
1830  Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c,
1831  Z3_symbol name,
1832  unsigned n,
1833  Z3_symbol const enum_names[],
1834  Z3_func_decl enum_consts[],
1835  Z3_func_decl enum_testers[]);
1836 
1854  Z3_sort Z3_API Z3_mk_list_sort(Z3_context c,
1855  Z3_symbol name,
1856  Z3_sort elem_sort,
1857  Z3_func_decl* nil_decl,
1858  Z3_func_decl* is_nil_decl,
1859  Z3_func_decl* cons_decl,
1860  Z3_func_decl* is_cons_decl,
1861  Z3_func_decl* head_decl,
1862  Z3_func_decl* tail_decl
1863  );
1864 
1879  Z3_constructor Z3_API Z3_mk_constructor(Z3_context c,
1880  Z3_symbol name,
1881  Z3_symbol recognizer,
1882  unsigned num_fields,
1883  Z3_symbol const field_names[],
1884  Z3_sort_opt const sorts[],
1885  unsigned sort_refs[]
1886  );
1887 
1895  void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr);
1896 
1907  Z3_sort Z3_API Z3_mk_datatype(Z3_context c,
1908  Z3_symbol name,
1909  unsigned num_constructors,
1910  Z3_constructor constructors[]);
1911 
1920  Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c,
1921  unsigned num_constructors,
1922  Z3_constructor const constructors[]);
1923 
1933  void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist);
1934 
1945  void Z3_API Z3_mk_datatypes(Z3_context c,
1946  unsigned num_sorts,
1947  Z3_symbol const sort_names[],
1948  Z3_sort sorts[],
1949  Z3_constructor_list constructor_lists[]);
1950 
1962  void Z3_API Z3_query_constructor(Z3_context c,
1963  Z3_constructor constr,
1964  unsigned num_fields,
1965  Z3_func_decl* constructor,
1966  Z3_func_decl* tester,
1967  Z3_func_decl accessors[]);
1968 
1973 
1990  Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s,
1991  unsigned domain_size, Z3_sort const domain[],
1992  Z3_sort range);
1993 
1994 
2001  Z3_ast Z3_API Z3_mk_app(
2002  Z3_context c,
2003  Z3_func_decl d,
2004  unsigned num_args,
2005  Z3_ast const args[]);
2006 
2020  Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty);
2021 
2033  Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix,
2034  unsigned domain_size, Z3_sort const domain[],
2035  Z3_sort range);
2036 
2049  Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty);
2058  Z3_ast Z3_API Z3_mk_true(Z3_context c);
2059 
2064  Z3_ast Z3_API Z3_mk_false(Z3_context c);
2065 
2072  Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r);
2073 
2085  Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[]);
2086 
2093  Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a);
2094 
2102  Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3);
2103 
2110  Z3_ast Z3_API Z3_mk_iff(Z3_context c, Z3_ast t1, Z3_ast t2);
2111 
2118  Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2);
2119 
2126  Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2);
2127 
2137  Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[]);
2138 
2148  Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[]);
2162  Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[]);
2163 
2174  Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[]);
2175 
2185  Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[]);
2186 
2193  Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg);
2194 
2203  Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2204 
2211  Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2212 
2219  Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2220 
2227  Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2228 
2235  Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2);
2236 
2243  Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2);
2244 
2251  Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2);
2252 
2259  Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2);
2260 
2277  Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1);
2278 
2289  Z3_ast Z3_API Z3_mk_real2int(Z3_context c, Z3_ast t1);
2290 
2298  Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1);
2309  Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1);
2310 
2317  Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1);
2318 
2325  Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1);
2326 
2333  Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2);
2334 
2341  Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2);
2342 
2349  Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2);
2350 
2357  Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2);
2358 
2365  Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2);
2366 
2373  Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2);
2374 
2381  Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1);
2382 
2389  Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2);
2390 
2397  Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2);
2398 
2405  Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2);
2406 
2417  Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2);
2418 
2433  Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2);
2434 
2445  Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2);
2446 
2460  Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2);
2461 
2472  Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2);
2473 
2480  Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2);
2481 
2496  Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2);
2497 
2504  Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2);
2505 
2512  Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2);
2513 
2520  Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2);
2521 
2528  Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2);
2529 
2536  Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2);
2537 
2544  Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2);
2545 
2555  Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2);
2556 
2564  Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1);
2565 
2574  Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1);
2575 
2584  Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1);
2585 
2592  Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1);
2593 
2607  Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2);
2608 
2622  Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2);
2623 
2638  Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2);
2639 
2646  Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1);
2647 
2654  Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1);
2655 
2662  Z3_ast Z3_API Z3_mk_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2);
2663 
2670  Z3_ast Z3_API Z3_mk_ext_rotate_right(Z3_context c, Z3_ast t1, Z3_ast t2);
2671 
2682  Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1);
2683 
2698  Z3_ast Z3_API Z3_mk_bv2int(Z3_context c,Z3_ast t1, Z3_bool is_signed);
2699 
2707  Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed);
2708 
2716  Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2);
2717 
2725  Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2);
2726 
2734  Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed);
2735 
2743  Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2);
2744 
2752  Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1);
2753 
2761  Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed);
2762 
2770  Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2);
2787  Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i);
2788 
2804  Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v);
2805 
2817  Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v);
2818 
2831  Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const* args);
2832 
2842  Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array);
2851  Z3_sort Z3_API Z3_mk_set_sort(Z3_context c, Z3_sort ty);
2852 
2857  Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain);
2858 
2863  Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain);
2864 
2871  Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem);
2872 
2879  Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem);
2880 
2885  Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[]);
2886 
2891  Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[]);
2892 
2897  Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2898 
2903  Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg);
2904 
2911  Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set);
2912 
2917  Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2918 
2926  Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2943  Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty);
2944 
2959  Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den);
2960 
2970  Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty);
2971 
2981  Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty);
2982 
2992  Z3_ast Z3_API Z3_mk_int64(Z3_context c, __int64 v, Z3_sort ty);
2993 
3003  Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, unsigned __int64 v, Z3_sort ty);
3004 
3009 
3014  Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s);
3015 
3020  Z3_bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s);
3021 
3026  Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq);
3027 
3032  Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s);
3033 
3041  Z3_sort Z3_API Z3_mk_string_sort(Z3_context c);
3042 
3047  Z3_bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s);
3048 
3052  Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s);
3053 
3058  Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s);
3059 
3066  Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s);
3067 
3074  Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq);
3075 
3080  Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a);
3081 
3088  Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[]);
3089 
3096  Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s);
3097 
3104  Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s);
3105 
3112  Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee);
3113 
3118  Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length);
3119 
3124  Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst);
3125 
3130  Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index);
3131 
3136  Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s);
3137 
3138 
3145  Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);
3146 
3151  Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq);
3152 
3157  Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re);
3158 
3163  Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re);
3164 
3169  Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re);
3170 
3175  Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re);
3176 
3183  Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[]);
3184 
3191  Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[]);
3192 
3217  Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[]);
3218 
3247  Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty);
3248 
3271  Z3_ast Z3_API Z3_mk_forall(Z3_context c, unsigned weight,
3272  unsigned num_patterns, Z3_pattern const patterns[],
3273  unsigned num_decls, Z3_sort const sorts[],
3274  Z3_symbol const decl_names[],
3275  Z3_ast body);
3276 
3286  Z3_ast Z3_API Z3_mk_exists(Z3_context c, unsigned weight,
3287  unsigned num_patterns, Z3_pattern const patterns[],
3288  unsigned num_decls, Z3_sort const sorts[],
3289  Z3_symbol const decl_names[],
3290  Z3_ast body);
3291 
3312  Z3_ast Z3_API Z3_mk_quantifier(
3313  Z3_context c,
3314  Z3_bool is_forall,
3315  unsigned weight,
3316  unsigned num_patterns, Z3_pattern const patterns[],
3317  unsigned num_decls, Z3_sort const sorts[],
3318  Z3_symbol const decl_names[],
3319  Z3_ast body);
3320 
3321 
3345  Z3_ast Z3_API Z3_mk_quantifier_ex(
3346  Z3_context c,
3347  Z3_bool is_forall,
3348  unsigned weight,
3349  Z3_symbol quantifier_id,
3350  Z3_symbol skolem_id,
3351  unsigned num_patterns, Z3_pattern const patterns[],
3352  unsigned num_no_patterns, Z3_ast const no_patterns[],
3353  unsigned num_decls, Z3_sort const sorts[],
3354  Z3_symbol const decl_names[],
3355  Z3_ast body);
3356 
3374  Z3_ast Z3_API Z3_mk_forall_const(
3375  Z3_context c,
3376  unsigned weight,
3377  unsigned num_bound,
3378  Z3_app const bound[],
3379  unsigned num_patterns,
3380  Z3_pattern const patterns[],
3381  Z3_ast body
3382  );
3383 
3403  Z3_ast Z3_API Z3_mk_exists_const(
3404  Z3_context c,
3405  unsigned weight,
3406  unsigned num_bound,
3407  Z3_app const bound[],
3408  unsigned num_patterns,
3409  Z3_pattern const patterns[],
3410  Z3_ast body
3411  );
3412 
3418  Z3_ast Z3_API Z3_mk_quantifier_const(
3419  Z3_context c,
3420  Z3_bool is_forall,
3421  unsigned weight,
3422  unsigned num_bound, Z3_app const bound[],
3423  unsigned num_patterns, Z3_pattern const patterns[],
3424  Z3_ast body
3425  );
3426 
3432  Z3_ast Z3_API Z3_mk_quantifier_const_ex(
3433  Z3_context c,
3434  Z3_bool is_forall,
3435  unsigned weight,
3436  Z3_symbol quantifier_id,
3437  Z3_symbol skolem_id,
3438  unsigned num_bound, Z3_app const bound[],
3439  unsigned num_patterns, Z3_pattern const patterns[],
3440  unsigned num_no_patterns, Z3_ast const no_patterns[],
3441  Z3_ast body
3442  );
3443 
3454  Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s);
3455 
3464  int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s);
3465 
3478  Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s);
3479 
3484  Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d);
3485 
3490  unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s);
3491 
3496  Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s);
3497 
3502  Z3_bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2);
3503 
3510  Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t);
3511 
3521  unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t);
3522 
3528  Z3_bool_opt Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, unsigned __int64* r);
3529 
3539  Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t);
3540 
3550  Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t);
3551 
3562  Z3_func_decl Z3_API Z3_get_tuple_sort_mk_decl(Z3_context c, Z3_sort t);
3563 
3573  unsigned Z3_API Z3_get_tuple_sort_num_fields(Z3_context c, Z3_sort t);
3574 
3586  Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t, unsigned i);
3587 
3598  unsigned Z3_API Z3_get_datatype_sort_num_constructors(
3599  Z3_context c, Z3_sort t);
3600 
3612  Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(
3613  Z3_context c, Z3_sort t, unsigned idx);
3614 
3626  Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(
3627  Z3_context c, Z3_sort t, unsigned idx);
3628 
3641  Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c,
3642  Z3_sort t,
3643  unsigned idx_c,
3644  unsigned idx_a);
3645 
3664  Z3_ast Z3_API Z3_datatype_update_field(Z3_context c, Z3_func_decl field_access,
3665  Z3_ast t, Z3_ast value);
3666 
3675  unsigned Z3_API Z3_get_relation_arity(Z3_context c, Z3_sort s);
3676 
3686  Z3_sort Z3_API Z3_get_relation_column(Z3_context c, Z3_sort s, unsigned col);
3687 
3695  Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args,
3696  Z3_ast const args[], unsigned k);
3697 
3705  Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args,
3706  Z3_ast const args[], int coeffs[],
3707  int k);
3708 
3716  Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args,
3717  Z3_ast const args[], int coeffs[],
3718  int k);
3719 
3724  Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f);
3725 
3730  Z3_bool Z3_API Z3_is_eq_func_decl(Z3_context c, Z3_func_decl f1, Z3_func_decl f2);
3731 
3736  unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f);
3737 
3742  Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d);
3743 
3748  Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d);
3749 
3756  unsigned Z3_API Z3_get_domain_size(Z3_context c, Z3_func_decl d);
3757 
3764  unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d);
3765 
3774  Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i);
3775 
3783  Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d);
3784 
3789  unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d);
3790 
3799  Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx);
3800 
3807  int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
3808 
3815  double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
3816 
3823  Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
3824 
3831  Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
3832 
3839  Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
3840 
3847  Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
3848 
3855  Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
3856 
3861  Z3_ast Z3_API Z3_app_to_ast(Z3_context c, Z3_app a);
3862 
3867  Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a);
3868 
3874  unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a);
3875 
3882  Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i);
3883 
3888  Z3_bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2);
3889 
3900  unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t);
3901 
3908  unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a);
3909 
3916  Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a);
3917 
3922  Z3_bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t);
3923 
3928  Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a);
3929 
3934  Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a);
3935 
3938  Z3_bool Z3_API Z3_is_app(Z3_context c, Z3_ast a);
3939 
3942  Z3_bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a);
3943 
3948  Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a);
3949 
3956  Z3_app Z3_API Z3_to_app(Z3_context c, Z3_ast a);
3957 
3964  Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a);
3965 
3972  Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a);
3973 
3981  Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision);
3982 
3989  Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a);
3990 
3997  Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a);
3998 
4012  Z3_bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, __int64* num, __int64* den);
4013 
4023  Z3_bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int* i);
4024 
4034  Z3_bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned* u);
4035 
4045  Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, unsigned __int64* u);
4046 
4056  Z3_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, __int64* i);
4057 
4067  Z3_bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, __int64* num, __int64* den);
4068 
4077  Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision);
4078 
4087  Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision);
4088 
4093  Z3_ast Z3_API Z3_pattern_to_ast(Z3_context c, Z3_pattern p);
4094 
4099  unsigned Z3_API Z3_get_pattern_num_terms(Z3_context c, Z3_pattern p);
4100 
4105  Z3_ast Z3_API Z3_get_pattern(Z3_context c, Z3_pattern p, unsigned idx);
4106 
4113  unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a);
4114 
4121  Z3_bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a);
4122 
4129  unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a);
4130 
4137  unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a);
4138 
4145  Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i);
4146 
4153  unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a);
4154 
4161  Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i);
4162 
4169  unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a);
4170 
4177  Z3_symbol Z3_API Z3_get_quantifier_bound_name(Z3_context c, Z3_ast a, unsigned i);
4178 
4185  Z3_sort Z3_API Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, unsigned i);
4186 
4193  Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a);
4194 
4204  Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a);
4205 
4214  Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p);
4215 
4220  Z3_string Z3_API Z3_simplify_get_help(Z3_context c);
4221 
4226  Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c);
4238  Z3_ast Z3_API Z3_update_term(Z3_context c, Z3_ast a, unsigned num_args, Z3_ast const args[]);
4239 
4246  Z3_ast Z3_API Z3_substitute(Z3_context c,
4247  Z3_ast a,
4248  unsigned num_exprs,
4249  Z3_ast const from[],
4250  Z3_ast const to[]);
4251 
4257  Z3_ast Z3_API Z3_substitute_vars(Z3_context c,
4258  Z3_ast a,
4259  unsigned num_exprs,
4260  Z3_ast const to[]);
4261 
4268  Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target);
4277  void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m);
4278 
4283  void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m);
4284 
4307  Z3_bool_opt Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast * v);
4308 
4317  Z3_ast_opt Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a);
4318 
4323  Z3_bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a);
4324 
4336  Z3_func_interp_opt Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f);
4337 
4344  unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m);
4345 
4354  Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i);
4355 
4363  unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m);
4364 
4373  Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i);
4374 
4386  unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m);
4387 
4397  Z3_sort Z3_API Z3_model_get_sort(Z3_context c, Z3_model m, unsigned i);
4398 
4406  Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s);
4407 
4418  Z3_bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a);
4419 
4426  Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a);
4427 
4432  void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f);
4433 
4438  void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f);
4439 
4448  unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f);
4449 
4459  Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i);
4460 
4468  Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f);
4469 
4474  unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f);
4475 
4480  void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e);
4481 
4486  void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e);
4487 
4497  Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e);
4498 
4505  unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e);
4506 
4515  Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i);
4524  Z3_bool Z3_API Z3_open_log(Z3_string filename);
4525 
4534  void Z3_API Z3_append_log(Z3_string string);
4535 
4540  void Z3_API Z3_close_log(void);
4541 
4549  void Z3_API Z3_toggle_warning_messages(Z3_bool enabled);
4570  void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode);
4571 
4583  Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a);
4584 
4587  Z3_string Z3_API Z3_pattern_to_string(Z3_context c, Z3_pattern p);
4588 
4591  Z3_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s);
4592 
4595  Z3_string Z3_API Z3_func_decl_to_string(Z3_context c, Z3_func_decl d);
4596 
4605  Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m);
4606 
4624  Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c,
4625  Z3_string name,
4626  Z3_string logic,
4627  Z3_string status,
4628  Z3_string attributes,
4629  unsigned num_assumptions,
4630  Z3_ast const assumptions[],
4631  Z3_ast formula);
4632 
4644  Z3_ast Z3_API Z3_parse_smtlib2_string(Z3_context c,
4645  Z3_string str,
4646  unsigned num_sorts,
4647  Z3_symbol const sort_names[],
4648  Z3_sort const sorts[],
4649  unsigned num_decls,
4650  Z3_symbol const decl_names[],
4651  Z3_func_decl const decls[]);
4652 
4657  Z3_ast Z3_API Z3_parse_smtlib2_file(Z3_context c,
4658  Z3_string file_name,
4659  unsigned num_sorts,
4660  Z3_symbol const sort_names[],
4661  Z3_sort const sorts[],
4662  unsigned num_decls,
4663  Z3_symbol const decl_names[],
4664  Z3_func_decl const decls[]);
4665 
4679  void Z3_API Z3_parse_smtlib_string(Z3_context c,
4680  Z3_string str,
4681  unsigned num_sorts,
4682  Z3_symbol const sort_names[],
4683  Z3_sort const sorts[],
4684  unsigned num_decls,
4685  Z3_symbol const decl_names[],
4686  Z3_func_decl const decls[]
4687  );
4688 
4693  void Z3_API Z3_parse_smtlib_file(Z3_context c,
4694  Z3_string file_name,
4695  unsigned num_sorts,
4696  Z3_symbol const sort_names[],
4697  Z3_sort const sorts[],
4698  unsigned num_decls,
4699  Z3_symbol const decl_names[],
4700  Z3_func_decl const decls[]
4701  );
4702 
4707  unsigned Z3_API Z3_get_smtlib_num_formulas(Z3_context c);
4708 
4715  Z3_ast Z3_API Z3_get_smtlib_formula(Z3_context c, unsigned i);
4716 
4721  unsigned Z3_API Z3_get_smtlib_num_assumptions(Z3_context c);
4722 
4729  Z3_ast Z3_API Z3_get_smtlib_assumption(Z3_context c, unsigned i);
4730 
4735  unsigned Z3_API Z3_get_smtlib_num_decls(Z3_context c);
4736 
4743  Z3_func_decl Z3_API Z3_get_smtlib_decl(Z3_context c, unsigned i);
4744 
4749  unsigned Z3_API Z3_get_smtlib_num_sorts(Z3_context c);
4750 
4757  Z3_sort Z3_API Z3_get_smtlib_sort(Z3_context c, unsigned i);
4758 
4763  Z3_string Z3_API Z3_get_smtlib_error(Z3_context c);
4768 #ifndef SAFE_ERRORS
4769 
4778  Z3_error_code Z3_API Z3_get_error_code(Z3_context c);
4779 
4792  void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h);
4793 #endif
4794 
4799  void Z3_API Z3_set_error(Z3_context c, Z3_error_code e);
4800 
4805  Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err);
4812  Z3_string Z3_API Z3_get_error_msg_ex(Z3_context c, Z3_error_code err);
4817 
4822  void Z3_API Z3_get_version(unsigned * major, unsigned * minor, unsigned * build_number, unsigned * revision_number);
4823 
4828  Z3_string Z3_API Z3_get_full_version(void);
4829 
4835  void Z3_API Z3_enable_trace(Z3_string tag);
4836 
4842  void Z3_API Z3_disable_trace(Z3_string tag);
4843 
4853  void Z3_API Z3_reset_memory(void);
4854 
4862  void Z3_API Z3_finalize_memory(void);
4883  Z3_goal Z3_API Z3_mk_goal(Z3_context c, Z3_bool models, Z3_bool unsat_cores, Z3_bool proofs);
4884 
4889  void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g);
4890 
4895  void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g);
4896 
4903  Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g);
4904 
4909  void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a);
4910 
4915  Z3_bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g);
4916 
4921  unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g);
4922 
4927  void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g);
4928 
4933  unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g);
4934 
4941  Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx);
4942 
4947  unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g);
4948 
4953  Z3_bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g);
4954 
4959  Z3_bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g);
4960 
4965  Z3_goal Z3_API Z3_goal_translate(Z3_context source, Z3_goal g, Z3_context target);
4966 
4971  Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g);
4972 
4985  Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name);
4986 
4991  void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t);
4992 
4997  void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g);
4998 
5008  Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name);
5009 
5014  void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p);
5015 
5020  void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p);
5021 
5027  Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2);
5028 
5034  Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2);
5035 
5040  Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[]);
5041 
5047  Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2);
5048 
5054  Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms);
5055 
5061  Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t);
5062 
5068  Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2);
5069 
5075  Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max);
5076 
5081  Z3_tactic Z3_API Z3_tactic_skip(Z3_context c);
5082 
5087  Z3_tactic Z3_API Z3_tactic_fail(Z3_context c);
5088 
5093  Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p);
5094 
5100  Z3_tactic Z3_API Z3_tactic_fail_if_not_decided(Z3_context c);
5101 
5106  Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p);
5107 
5112  Z3_probe Z3_API Z3_probe_const(Z3_context x, double val);
5113 
5120  Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2);
5121 
5128  Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2);
5129 
5136  Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2);
5137 
5144  Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2);
5145 
5152  Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2);
5153 
5160  Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2);
5161 
5168  Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2);
5169 
5176  Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p);
5177 
5182  unsigned Z3_API Z3_get_num_tactics(Z3_context c);
5183 
5190  Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i);
5191 
5196  unsigned Z3_API Z3_get_num_probes(Z3_context c);
5197 
5204  Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i);
5205 
5210  Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t);
5211 
5216  Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t);
5217 
5222  Z3_string Z3_API Z3_tactic_get_descr(Z3_context c, Z3_string name);
5223 
5228  Z3_string Z3_API Z3_probe_get_descr(Z3_context c, Z3_string name);
5229 
5235  double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g);
5236 
5241  Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g);
5242 
5247  Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p);
5248 
5253  void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r);
5254 
5259  void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r);
5260 
5265  Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r);
5266 
5271  unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r);
5272 
5279  Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i);
5280 
5286  Z3_model Z3_API Z3_apply_result_convert_model(Z3_context c, Z3_apply_result r, unsigned i, Z3_model m);
5287 
5301  Z3_solver Z3_API Z3_mk_solver(Z3_context c);
5302 
5317  Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c);
5318 
5327  Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic);
5328 
5338  Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t);
5339 
5344  Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target);
5345 
5350  Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s);
5351 
5356  Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s);
5357 
5362  void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p);
5363 
5368  void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s);
5369 
5374  void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s);
5375 
5384  void Z3_API Z3_solver_push(Z3_context c, Z3_solver s);
5385 
5394  void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n);
5395 
5400  void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s);
5401 
5409  unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s);
5410 
5418  void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a);
5419 
5433  void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p);
5434 
5439  Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s);
5440 
5456  Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s);
5457 
5468  Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s,
5469  unsigned num_assumptions, Z3_ast const assumptions[]);
5470 
5488  Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c,
5489  Z3_solver s,
5490  unsigned num_terms,
5491  Z3_ast const terms[],
5492  unsigned class_ids[]);
5493 
5499  Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c,
5500  Z3_solver s,
5501  Z3_ast_vector assumptions,
5502  Z3_ast_vector variables,
5503  Z3_ast_vector consequences);
5511  Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s);
5512 
5521  Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s);
5522 
5528  Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s);
5529 
5535  Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s);
5536 
5543  Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s);
5544 
5549  Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s);
5550 
5555 
5560  Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s);
5561 
5566  void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s);
5567 
5572  void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s);
5573 
5578  unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s);
5579 
5586  Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx);
5587 
5594  Z3_bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx);
5595 
5602  Z3_bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx);
5603 
5610  unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx);
5611 
5618  double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx);
5619 
5625 
5628 #ifdef __cplusplus
5629 }
5630 #endif // __cplusplus
5631 
5634 #endif
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_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_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_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_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.
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Definition: z3_api.h:153
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_bool Z3_API Z3_open_log(Z3_string filename)
Log interaction to a file.
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_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
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.
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 Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
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_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.
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...
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)
Return a string describing the given error code.
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_pattern_to_ast(Z3_context c, Z3_pattern p)
Convert a Z3_pattern into Z3_ast. This is just type casting.
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.
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)
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.
__uint64 Z3_API Z3_get_estimated_alloc_size(void)
Return the estimated allocated memory in bytes.
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_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)
Erase all formulas from the given goal.
Z3_params Z3_API Z3_mk_params(Z3_context c)
Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many comp...
Z3_tactic Z3_API Z3_tactic_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_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_solver_get_proof(Z3_context c, Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
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.
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_get_smtlib_sort(Z3_context c, unsigned i)
Return the i-th sort parsed by the last call to Z3_parse_smtlib_string or Z3_parse_smtlib_file.
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
Definition: z3_api.h:1288
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.
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...
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_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx)
Return a formula from the given goal.
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
void Z3_API Z3_set_error(Z3_context c, Z3_error_code e)
Set an error.
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_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
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. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
Z3_bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx)
Return Z3_TRUE if the given statistical data is a double.
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_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...
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
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_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. The datatype may be recursive. Return the datatype sort.
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_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_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i)
Return the number of parameters in the given parameter description set.
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:1349
Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create array extensionality index given two arrays with the same sort. The meaning is given by the ax...
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1286
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_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.
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_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_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i)
Return an argument of a Z3_func_entry object.
int Z3_bool
Z3 Boolean type. It is just an alias for int.
Definition: z3_api.h:84
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_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.
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m)
Return the number of uninterpreted sorts that m assigs an interpretation to.
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_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
void Z3_API Z3_close_log(void)
Close interaction log.
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
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_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_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_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
Z3_ast 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_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. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.
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_reset_memory(void)
Reset all allocated resources.
#define __uint64
Definition: z3_api.h:44
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.
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
unsigned Z3_API Z3_get_smtlib_num_decls(Z3_context c)
Return the number of declarations parsed by Z3_parse_smtlib_string or Z3_parse_smtlib_file.
Z3_string Z3_API Z3_get_smtlib_error(Z3_context c)
Retrieve that last error message information generated from parsing.
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.
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.
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...
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_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
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_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.
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_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_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...
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, Z3_bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...
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_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_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
Z3_string * Z3_string_ptr
Definition: z3_api.h:90
void Z3_API Z3_append_log(Z3_string string)
Append user-defined string to interaction log.
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a)
Return index of de-Brujin bound variable.
unsigned Z3_API Z3_get_pattern_num_terms(Z3_context c, Z3_pattern p)
Return number of terms in pattern.
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_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow...
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s)
Return the number of backtracking points.
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
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...
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_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, unsigned __int64 *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned __int6...
Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Take the set difference between two sets.
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.
Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, unsigned __int64 size)
Create a named finite domain sort.
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).
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
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.
#define Z3_func_interp_opt
Definition: z3_api.h:33
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...
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.
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_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
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_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...
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_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
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_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:183
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_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_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_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
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.
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
unsigned Z3_API Z3_get_smtlib_num_formulas(Z3_context c)
Return the number of SMTLIB formulas parsed by the last call to Z3_parse_smtlib_string or Z3_parse_sm...
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...
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.
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.
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_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.
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_goal Z3_API Z3_mk_goal(Z3_context c, Z3_bool models, Z3_bool unsat_cores, Z3_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_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:105
void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a)
Add a new formula a to the given goal.
Z3_app Z3_API Z3_to_app(Z3_context c, Z3_ast a)
Create a numeral of a given sort.
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.
Z3_tactic Z3_API Z3_tactic_fail(Z3_context c)
Return a tactic that always fails.
#define __int64
Definition: z3_api.h:40
void Z3_API Z3_finalize_memory(void)
Destroy all allocated resources.
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...
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
unsigned Z3_API Z3_get_smtlib_num_assumptions(Z3_context c)
Return the number of SMTLIB assumptions parsed by Z3_parse_smtlib_string or Z3_parse_smtlib_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.
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_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...
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...
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_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
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.
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_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...
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
Definition: z3_api.h:1261
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
Z3_string Z3_API Z3_get_full_version(void)
Return a string that fully describes the version of Z3 in use.
Z3_func_decl Z3_API Z3_get_smtlib_decl(Z3_context c, unsigned i)
Return the i-th declaration parsed by the last call to Z3_parse_smtlib_string or Z3_parse_smtlib_file...
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
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.
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)
Decrement the reference counter of the given parameter set.
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...
void Z3_API Z3_toggle_warning_messages(Z3_bool enabled)
Enable/disable printing warning messages to the console.
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_bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, __int64 *num, __int64 *den)
Return numeral value, as a pair of 64 bit numbers if the representation fits.
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
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.
Z3_string Z3_API Z3_get_error_msg_ex(Z3_context c, Z3_error_code err)
Return a string describing the given error code. Retained function name for backwards compatibility w...
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 ...
Z3_param_kind
The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params)...
Definition: z3_api.h:1243
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.
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.
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 Z3_API Z3_get_smtlib_assumption(Z3_context c, unsigned i)
Return the i-th assumption parsed by the last call to Z3_parse_smtlib_string or Z3_parse_smtlib_file...
Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded, and store the result in v...
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.
void Z3_API Z3_parse_smtlib_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-LIB parser.
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_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See #Z3...
Definition: z3_api.h:119
Z3_bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Test if there exists an interpretation (i.e., assignment) for a in the model m.
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_ast Z3_API Z3_get_pattern(Z3_context c, Z3_pattern p, unsigned idx)
Return i'th ast in pattern.
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
unsigned Z3_API Z3_get_smtlib_num_sorts(Z3_context c)
Return the number of sorts parsed by Z3_parse_smtlib_string or Z3_parse_smtlib_file.
Z3_bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return Z3_TRUE if the given statistical data is a unsigned integer.
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...
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow...
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new (incremental) solver.
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
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...
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_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_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.
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.
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 a the context target.
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_tactic Z3_API Z3_tactic_skip(Z3_context c)
Return a tactic that just return the given goal.
unsigned Z3_API Z3_get_num_tactics(Z3_context c)
Return the number of builtin tactics available in Z3.
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context 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.
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_bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if quantifier is universal.
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 a the context target.
void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.
Z3_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...
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_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:139
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].
unsigned Z3_API Z3_get_num_probes(Z3_context c)
Return the number of builtin probes available in Z3.
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.
void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)
Set a configuration parameter.
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...
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
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.
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_ast Z3_API Z3_get_smtlib_formula(Z3_context c, unsigned i)
Return the i-th formula parsed by the last call to Z3_parse_smtlib_string or Z3_parse_smtlib_file.
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_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_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_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 ...
unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a)
Return number of no_patterns used in quantifier.
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
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...
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 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.
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...
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_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_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.
void Z3_error_handler(Z3_context c, Z3_error_code e)
Z3 custom error handler (See Z3_set_error_handler).
Definition: z3_api.h:1337
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
Z3_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...
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_solver Z3_API Z3_mk_solver(Z3_context c)
Create a new (incremental) solver. This solver also uses a set of builtin tactics for handling the fi...
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.
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.
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_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_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
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_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_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 intepretation. It represents the value of f in a particular po...
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.
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_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_rotate_left(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the left i times.
Z3_string Z3_API Z3_func_decl_to_string(Z3_context c, Z3_func_decl d)
void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, Z3_bool v)
Add a Boolean parameter k with value v to the parameter set p.
void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)
Return Z3 version number information.
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_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, unsigned num_constructors, Z3_constructor const constructors[])
Create list of constructors.
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.
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...
Z3_bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, __int64 *num, __int64 *den)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit as a rational number as mach...
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.
Z3_bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.
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.
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_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, __int64 *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine __int64 int...
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.
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955
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...
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.
void Z3_API Z3_parse_smtlib_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_smtlib_string, but reads the benchmark from a file.
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_ast Z3_API Z3_mk_iff(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 iff t2.
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.
#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.
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_model Z3_API Z3_apply_result_convert_model(Z3_context c, Z3_apply_result r, unsigned i, Z3_model m)
Convert a model for the subgoal Z3_apply_result_get_subgoal(c, r, i) into a model for the original go...
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.
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_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:89
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.