Z3
 
Loading...
Searching...
No Matches
z3_api.h
Go to the documentation of this file.
1/*++
2 Copyright (c) 2015 Microsoft Corporation
3--*/
4
5#pragma once
6
7#define Z3_sort_opt Z3_sort
8#define Z3_ast_opt Z3_ast
9#define Z3_func_interp_opt Z3_func_interp
10
53typedef const char * Z3_string;
54typedef char const* Z3_char_ptr;
56
60typedef enum
61{
66
74typedef enum
75{
79
80
94typedef enum
95{
104
108typedef enum
109{
124 Z3_UNKNOWN_SORT = 1000
126
139typedef enum
140{
147 Z3_UNKNOWN_AST = 1000
149
962typedef enum {
963 // Basic
964 Z3_OP_TRUE = 0x100,
976
977 // Arithmetic
978 Z3_OP_ANUM = 0x200,
996
997 // Arrays & Sets
998 Z3_OP_STORE = 0x300,
1012
1013 // Bit-vectors
1014 Z3_OP_BNUM = 0x400,
1021
1027
1028 // special functions to record the division by 0 cases
1029 // these are internal functions
1035
1044
1052
1058
1062
1070
1076
1085
1086 // Proofs
1129
1130 // Relational algebra
1146
1147 // Sequences
1166
1167 // strings
1176
1177 // regular expressions
1195
1196 // char
1203
1204 // Auxiliary
1207
1208 // Datatypes
1214
1215 // Pseudo Booleans
1221
1222 // Special relations
1229
1230
1231 // Floating-Point Arithmetic
1237
1244
1257
1270
1277
1279
1282
1285
1288
1301typedef enum {
1310
1318typedef enum {
1323
1324
1342typedef enum
1343{
1358
1383typedef enum
1384{
1390
1393#ifdef __cplusplus
1394extern "C" {
1395#endif // __cplusplus
1396
1423 void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value);
1424
1425
1434 void Z3_API Z3_global_param_reset_all(void);
1435
1448 bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value);
1449
1485 Z3_config Z3_API Z3_mk_config(void);
1486
1493 void Z3_API Z3_del_config(Z3_config c);
1494
1503 void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value);
1504
1542 Z3_context Z3_API Z3_mk_context(Z3_config c);
1543
1565 Z3_context Z3_API Z3_mk_context_rc(Z3_config c);
1566
1573 void Z3_API Z3_del_context(Z3_context c);
1574
1581 void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a);
1582
1589 void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a);
1590
1597 void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value);
1598
1599
1604 Z3_param_descrs Z3_API Z3_get_global_param_descrs(Z3_context c);
1605
1611 void Z3_API Z3_interrupt(Z3_context c);
1612
1613
1620 void Z3_API Z3_enable_concurrent_dec_ref(Z3_context c);
1621
1622
1637 Z3_params Z3_API Z3_mk_params(Z3_context c);
1638
1643 void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p);
1644
1649 void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p);
1650
1655 void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, bool v);
1656
1661 void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v);
1662
1667 void Z3_API Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v);
1668
1673 void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v);
1674
1680 Z3_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p);
1681
1688 void Z3_API Z3_params_validate(Z3_context c, Z3_params p, Z3_param_descrs d);
1689
1699 void Z3_API Z3_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p);
1700
1705 void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p);
1706
1711 Z3_param_kind Z3_API Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n);
1712
1717 unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p);
1718
1725 Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i);
1726
1731 Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s);
1732
1738 Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p);
1739
1757 Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i);
1758
1768 Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s);
1769
1781 Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s);
1782
1789 Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c);
1790
1801 Z3_sort Z3_API Z3_mk_int_sort(Z3_context c);
1802
1809 Z3_sort Z3_API Z3_mk_real_sort(Z3_context c);
1810
1819 Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz);
1820
1833 Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size);
1834
1845 Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range);
1846
1854 Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const * domain, Z3_sort range);
1855
1871 Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c,
1872 Z3_symbol mk_tuple_name,
1873 unsigned num_fields,
1874 Z3_symbol const field_names[],
1875 Z3_sort const field_sorts[],
1876 Z3_func_decl * mk_tuple_decl,
1877 Z3_func_decl proj_decl[]);
1878
1899 Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c,
1900 Z3_symbol name,
1901 unsigned n,
1902 Z3_symbol const enum_names[],
1903 Z3_func_decl enum_consts[],
1904 Z3_func_decl enum_testers[]);
1905
1923 Z3_sort Z3_API Z3_mk_list_sort(Z3_context c,
1924 Z3_symbol name,
1925 Z3_sort elem_sort,
1926 Z3_func_decl* nil_decl,
1927 Z3_func_decl* is_nil_decl,
1928 Z3_func_decl* cons_decl,
1929 Z3_func_decl* is_cons_decl,
1930 Z3_func_decl* head_decl,
1931 Z3_func_decl* tail_decl
1932 );
1933
1952 Z3_constructor Z3_API Z3_mk_constructor(Z3_context c,
1953 Z3_symbol name,
1954 Z3_symbol recognizer,
1955 unsigned num_fields,
1956 Z3_symbol const field_names[],
1957 Z3_sort_opt const sorts[],
1958 unsigned sort_refs[]
1959 );
1960
1970 void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr);
1971
1986 Z3_sort Z3_API Z3_mk_datatype(Z3_context c,
1987 Z3_symbol name,
1988 unsigned num_constructors,
1989 Z3_constructor constructors[]);
1990
2001 Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name);
2002
2014 Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c,
2015 unsigned num_constructors,
2016 Z3_constructor const constructors[]);
2017
2029 void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist);
2030
2045 void Z3_API Z3_mk_datatypes(Z3_context c,
2046 unsigned num_sorts,
2047 Z3_symbol const sort_names[],
2048 Z3_sort sorts[],
2049 Z3_constructor_list constructor_lists[]);
2050
2064 void Z3_API Z3_query_constructor(Z3_context c,
2065 Z3_constructor constr,
2066 unsigned num_fields,
2067 Z3_func_decl* constructor,
2068 Z3_func_decl* tester,
2069 Z3_func_decl accessors[]);
2070
2094 Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s,
2095 unsigned domain_size, Z3_sort const domain[],
2096 Z3_sort range);
2097
2098
2099
2108 Z3_ast Z3_API Z3_mk_app(
2109 Z3_context c,
2110 Z3_func_decl d,
2111 unsigned num_args,
2112 Z3_ast const args[]);
2113
2128 Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty);
2129
2141 Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix,
2142 unsigned domain_size, Z3_sort const domain[],
2143 Z3_sort range);
2144
2159 Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty);
2160
2161
2180 Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s,
2181 unsigned domain_size, Z3_sort const domain[],
2182 Z3_sort range);
2183
2199 void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body);
2200
2209 Z3_ast Z3_API Z3_mk_true(Z3_context c);
2210
2215 Z3_ast Z3_API Z3_mk_false(Z3_context c);
2216
2223 Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r);
2224
2236 Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[]);
2237
2244 Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a);
2245
2253 Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3);
2254
2261 Z3_ast Z3_API Z3_mk_iff(Z3_context c, Z3_ast t1, Z3_ast t2);
2262
2269 Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2);
2270
2277 Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2);
2278
2288 Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[]);
2289
2299 Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[]);
2313 Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[]);
2314
2325 Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[]);
2326
2336 Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[]);
2337
2344 Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg);
2345
2354 Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2355
2362 Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2363
2370 Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2371
2378 Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2379
2386 Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2);
2387
2394 Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2);
2395
2402 Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2);
2403
2410 Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2);
2411
2420 Z3_ast Z3_API Z3_mk_divides(Z3_context c, Z3_ast t1, Z3_ast t2);
2421
2438 Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1);
2439
2450 Z3_ast Z3_API Z3_mk_real2int(Z3_context c, Z3_ast t1);
2451
2459 Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1);
2470 Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1);
2471
2478 Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1);
2479
2486 Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1);
2487
2494 Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2);
2495
2502 Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2);
2503
2510 Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2);
2511
2518 Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2);
2519
2526 Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2);
2527
2534 Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2);
2535
2542 Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1);
2543
2550 Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2);
2551
2558 Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2);
2559
2566 Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2);
2567
2578 Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2);
2579
2594 Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2);
2595
2606 Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2);
2607
2621 Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2);
2622
2633 Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2);
2634
2641 Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2);
2642
2657 Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2);
2658
2665 Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2);
2666
2673 Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2);
2674
2681 Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2);
2682
2689 Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2);
2690
2697 Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2);
2698
2705 Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2);
2706
2716 Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2);
2717
2725 Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1);
2726
2735 Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1);
2736
2745 Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1);
2746
2753 Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1);
2754
2762 Z3_ast Z3_API Z3_mk_bit2bool(Z3_context c, unsigned i, Z3_ast t1);
2763
2777 Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2);
2778
2792 Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2);
2793
2808 Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2);
2809
2816 Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1);
2817
2824 Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1);
2825
2832 Z3_ast Z3_API Z3_mk_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2);
2833
2840 Z3_ast Z3_API Z3_mk_ext_rotate_right(Z3_context c, Z3_ast t1, Z3_ast t2);
2841
2851 Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1);
2852
2864 Z3_ast Z3_API Z3_mk_bv2int(Z3_context c,Z3_ast t1, bool is_signed);
2865
2874 Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);
2875
2884 Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2);
2885
2894 Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2);
2895
2904 Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);
2905
2914 Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2);
2915
2924 Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1);
2925
2934 Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);
2935
2944 Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2);
2961 Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i);
2962
2963
2964
2971 Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs);
2972
2973
2989 Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v);
2990
2991
2997 Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs, Z3_ast v);
2998
3010 Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v);
3011
3024 Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const* args);
3025
3035 Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array);
3036
3043 Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f);
3044
3049 Z3_ast Z3_API Z3_mk_set_has_size(Z3_context c, Z3_ast set, Z3_ast k);
3050
3059 Z3_sort Z3_API Z3_mk_set_sort(Z3_context c, Z3_sort ty);
3060
3065 Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain);
3066
3071 Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain);
3072
3079 Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem);
3080
3087 Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem);
3088
3093 Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[]);
3094
3099 Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[]);
3100
3105 Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2);
3106
3111 Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg);
3112
3119 Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set);
3120
3125 Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2);
3126
3134 Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2);
3151 Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty);
3152
3153#if 0
3166 Z3_ast Z3_mk_mpz_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], Z3_sort s);
3167
3183 Z3_ast Z3_mk_mpq_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], unsigned d, unsigned const dens[]);
3184#endif
3185
3201 Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den);
3202
3209 Z3_ast Z3_API Z3_mk_real_int64(Z3_context c, int64_t num, int64_t den);
3210
3220 Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty);
3221
3231 Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty);
3232
3242 Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty);
3243
3253 Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty);
3254
3260 Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, bool const* bits);
3261
3271 Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s);
3272
3277 bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s);
3278
3283 Z3_sort Z3_API Z3_get_seq_sort_basis(Z3_context c, Z3_sort s);
3284
3289 Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq);
3290
3295 bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s);
3296
3301 Z3_sort Z3_API Z3_get_re_sort_basis(Z3_context c, Z3_sort s);
3302
3311 Z3_sort Z3_API Z3_mk_string_sort(Z3_context c);
3312
3321 Z3_sort Z3_API Z3_mk_char_sort(Z3_context c);
3322
3327 bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s);
3328
3333 bool Z3_API Z3_is_char_sort(Z3_context c, Z3_sort s);
3334
3343 Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s);
3344
3352 Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned len, Z3_string s);
3353
3360 Z3_ast Z3_API Z3_mk_u32string(Z3_context c, unsigned len, unsigned const chars[]);
3361
3366 bool Z3_API Z3_is_string(Z3_context c, Z3_ast s);
3367
3375 Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s);
3376
3385 Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length);
3386
3393 unsigned Z3_API Z3_get_string_length(Z3_context c, Z3_ast s);
3394
3403 void Z3_API Z3_get_string_contents(Z3_context c, Z3_ast s, unsigned length, unsigned contents[]);
3404
3411 Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq);
3412
3417 Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a);
3418
3425 Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[]);
3426
3433 Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s);
3434
3441 Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s);
3442
3449 Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee);
3450
3451
3458 Z3_ast Z3_API Z3_mk_str_lt(Z3_context c, Z3_ast prefix, Z3_ast s);
3459
3466 Z3_ast Z3_API Z3_mk_str_le(Z3_context c, Z3_ast prefix, Z3_ast s);
3467
3472 Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length);
3473
3478 Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst);
3479
3485 Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index);
3486
3492 Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index);
3493
3498 Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s);
3499
3500
3507 Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);
3508
3513 Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast s, Z3_ast substr);
3514
3519 Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s);
3520
3521
3526 Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s);
3527
3528
3533 Z3_ast Z3_API Z3_mk_string_to_code(Z3_context c, Z3_ast a);
3534
3539 Z3_ast Z3_API Z3_mk_string_from_code(Z3_context c, Z3_ast a);
3540
3545 Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s);
3546
3551 Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s);
3552
3557 Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq);
3558
3563 Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re);
3564
3569 Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re);
3570
3575 Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re);
3576
3581 Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re);
3582
3589 Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[]);
3590
3597 Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[]);
3598
3599
3604 Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi);
3605
3606
3611 Z3_ast Z3_API Z3_mk_re_allchar(Z3_context c, Z3_sort regex_sort);
3612
3620 Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi);
3621
3626 Z3_ast Z3_API Z3_mk_re_power(Z3_context c, Z3_ast re, unsigned n);
3627
3634 Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[]);
3635
3640 Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re);
3641
3646 Z3_ast Z3_API Z3_mk_re_diff(Z3_context c, Z3_ast re1, Z3_ast re2);
3647
3654 Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re);
3655
3656
3663 Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re);
3664
3665
3669 Z3_ast Z3_API Z3_mk_char(Z3_context c, unsigned ch);
3670
3675 Z3_ast Z3_API Z3_mk_char_le(Z3_context c, Z3_ast ch1, Z3_ast ch2);
3676
3681 Z3_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch);
3682
3687 Z3_ast Z3_API Z3_mk_char_to_bv(Z3_context c, Z3_ast ch);
3688
3693 Z3_ast Z3_API Z3_mk_char_from_bv(Z3_context c, Z3_ast bv);
3694
3699 Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch);
3700
3711 Z3_func_decl Z3_API Z3_mk_linear_order(Z3_context c, Z3_sort a, unsigned id);
3712
3717 Z3_func_decl Z3_API Z3_mk_partial_order(Z3_context c, Z3_sort a, unsigned id);
3718
3723 Z3_func_decl Z3_API Z3_mk_piecewise_linear_order(Z3_context c, Z3_sort a, unsigned id);
3724
3729 Z3_func_decl Z3_API Z3_mk_tree_order(Z3_context c, Z3_sort a, unsigned id);
3730
3739 Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f);
3740
3764 Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[]);
3765
3797 Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty);
3798
3821 Z3_ast Z3_API Z3_mk_forall(Z3_context c, unsigned weight,
3822 unsigned num_patterns, Z3_pattern const patterns[],
3823 unsigned num_decls, Z3_sort const sorts[],
3824 Z3_symbol const decl_names[],
3825 Z3_ast body);
3826
3836 Z3_ast Z3_API Z3_mk_exists(Z3_context c, unsigned weight,
3837 unsigned num_patterns, Z3_pattern const patterns[],
3838 unsigned num_decls, Z3_sort const sorts[],
3839 Z3_symbol const decl_names[],
3840 Z3_ast body);
3841
3862 Z3_ast Z3_API Z3_mk_quantifier(
3863 Z3_context c,
3864 bool is_forall,
3865 unsigned weight,
3866 unsigned num_patterns, Z3_pattern const patterns[],
3867 unsigned num_decls, Z3_sort const sorts[],
3868 Z3_symbol const decl_names[],
3869 Z3_ast body);
3870
3871
3895 Z3_ast Z3_API Z3_mk_quantifier_ex(
3896 Z3_context c,
3897 bool is_forall,
3898 unsigned weight,
3899 Z3_symbol quantifier_id,
3900 Z3_symbol skolem_id,
3901 unsigned num_patterns, Z3_pattern const patterns[],
3902 unsigned num_no_patterns, Z3_ast const no_patterns[],
3903 unsigned num_decls, Z3_sort const sorts[],
3904 Z3_symbol const decl_names[],
3905 Z3_ast body);
3906
3924 Z3_ast Z3_API Z3_mk_forall_const(
3925 Z3_context c,
3926 unsigned weight,
3927 unsigned num_bound,
3928 Z3_app const bound[],
3929 unsigned num_patterns,
3930 Z3_pattern const patterns[],
3931 Z3_ast body
3932 );
3933
3953 Z3_ast Z3_API Z3_mk_exists_const(
3954 Z3_context c,
3955 unsigned weight,
3956 unsigned num_bound,
3957 Z3_app const bound[],
3958 unsigned num_patterns,
3959 Z3_pattern const patterns[],
3960 Z3_ast body
3961 );
3962
3969 Z3_context c,
3970 bool is_forall,
3971 unsigned weight,
3972 unsigned num_bound, Z3_app const bound[],
3973 unsigned num_patterns, Z3_pattern const patterns[],
3974 Z3_ast body
3975 );
3976
3983 Z3_context c,
3984 bool is_forall,
3985 unsigned weight,
3986 Z3_symbol quantifier_id,
3987 Z3_symbol skolem_id,
3988 unsigned num_bound, Z3_app const bound[],
3989 unsigned num_patterns, Z3_pattern const patterns[],
3990 unsigned num_no_patterns, Z3_ast const no_patterns[],
3991 Z3_ast body
3992 );
3993
4016 Z3_ast Z3_API Z3_mk_lambda(Z3_context c,
4017 unsigned num_decls, Z3_sort const sorts[],
4018 Z3_symbol const decl_names[],
4019 Z3_ast body);
4020
4035 Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c,
4036 unsigned num_bound, Z3_app const bound[],
4037 Z3_ast body);
4038
4039
4050 Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s);
4051
4060 int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s);
4061
4074 Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s);
4075
4080 Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d);
4081
4086 unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s);
4087
4092 Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s);
4093
4098 bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2);
4099
4106 Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t);
4107
4117 unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t);
4118
4124 bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r);
4125
4137 Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t);
4138
4139
4151 Z3_sort Z3_API Z3_get_array_sort_domain_n(Z3_context c, Z3_sort t, unsigned idx);
4152
4162 Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t);
4163
4174 Z3_func_decl Z3_API Z3_get_tuple_sort_mk_decl(Z3_context c, Z3_sort t);
4175
4185 unsigned Z3_API Z3_get_tuple_sort_num_fields(Z3_context c, Z3_sort t);
4186
4198 Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t, unsigned i);
4199
4211 Z3_context c, Z3_sort t);
4212
4225 Z3_context c, Z3_sort t, unsigned idx);
4226
4239 Z3_context c, Z3_sort t, unsigned idx);
4240
4253 Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c,
4254 Z3_sort t,
4255 unsigned idx_c,
4256 unsigned idx_a);
4257
4276 Z3_ast Z3_API Z3_datatype_update_field(Z3_context c, Z3_func_decl field_access,
4277 Z3_ast t, Z3_ast value);
4278
4287 unsigned Z3_API Z3_get_relation_arity(Z3_context c, Z3_sort s);
4288
4298 Z3_sort Z3_API Z3_get_relation_column(Z3_context c, Z3_sort s, unsigned col);
4299
4306 Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args,
4307 Z3_ast const args[], unsigned k);
4308
4315 Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args,
4316 Z3_ast const args[], unsigned k);
4317
4324 Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args,
4325 Z3_ast const args[], int const coeffs[],
4326 int k);
4327
4334 Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args,
4335 Z3_ast const args[], int const coeffs[],
4336 int k);
4337
4344 Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args,
4345 Z3_ast const args[], int const coeffs[],
4346 int k);
4347
4352 Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f);
4353
4358 bool Z3_API Z3_is_eq_func_decl(Z3_context c, Z3_func_decl f1, Z3_func_decl f2);
4359
4364 unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f);
4365
4370 Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d);
4371
4376 Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d);
4377
4384 unsigned Z3_API Z3_get_domain_size(Z3_context c, Z3_func_decl d);
4385
4392 unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d);
4393
4402 Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i);
4403
4411 Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d);
4412
4417 unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d);
4418
4427 Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx);
4428
4435 int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4436
4443 double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4444
4451 Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4452
4459 Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4460
4467 Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4468
4475 Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4476
4483 Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4484
4489 Z3_ast Z3_API Z3_app_to_ast(Z3_context c, Z3_app a);
4490
4495 Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a);
4496
4504 unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a);
4505
4514 Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i);
4515
4520 bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2);
4521
4532 unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t);
4533
4541 unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a);
4542
4549 Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a);
4550
4555 bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t);
4556
4561 Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a);
4562
4567 Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a);
4568
4571 bool Z3_API Z3_is_app(Z3_context c, Z3_ast a);
4572
4575 bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a);
4576
4581 bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a);
4582
4589 Z3_app Z3_API Z3_to_app(Z3_context c, Z3_ast a);
4590
4597 Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a);
4598
4605 Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a);
4606
4614 Z3_string Z3_API Z3_get_numeral_binary_string(Z3_context c, Z3_ast a);
4615
4623 Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision);
4624
4631 double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a);
4632
4639 Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a);
4640
4647 Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a);
4648
4662 bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, int64_t* num, int64_t* den);
4663
4673 bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int* i);
4674
4684 bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned* u);
4685
4695 bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t* u);
4696
4706 bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t* i);
4707
4717 bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, int64_t* num, int64_t* den);
4718
4727 Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision);
4728
4737 Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision);
4738
4743 Z3_ast Z3_API Z3_pattern_to_ast(Z3_context c, Z3_pattern p);
4744
4749 unsigned Z3_API Z3_get_pattern_num_terms(Z3_context c, Z3_pattern p);
4750
4755 Z3_ast Z3_API Z3_get_pattern(Z3_context c, Z3_pattern p, unsigned idx);
4756
4763 unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a);
4764
4769 bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a);
4770
4776 bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a);
4777
4784 bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a);
4785
4792 unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a);
4793
4800 unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a);
4801
4808 Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i);
4809
4816 unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a);
4817
4824 Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i);
4825
4832 unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a);
4833
4840 Z3_symbol Z3_API Z3_get_quantifier_bound_name(Z3_context c, Z3_ast a, unsigned i);
4841
4848 Z3_sort Z3_API Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, unsigned i);
4849
4856 Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a);
4857
4869 Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a);
4870
4883 Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p);
4884
4892 Z3_string Z3_API Z3_simplify_get_help(Z3_context c);
4893
4901 Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c);
4913 Z3_ast Z3_API Z3_update_term(Z3_context c, Z3_ast a, unsigned num_args, Z3_ast const args[]);
4914
4921 Z3_ast Z3_API Z3_substitute(Z3_context c,
4922 Z3_ast a,
4923 unsigned num_exprs,
4924 Z3_ast const from[],
4925 Z3_ast const to[]);
4926
4933 Z3_ast Z3_API Z3_substitute_vars(Z3_context c,
4934 Z3_ast a,
4935 unsigned num_exprs,
4936 Z3_ast const to[]);
4937
4945 Z3_ast Z3_API Z3_substitute_funs(Z3_context c,
4946 Z3_ast a,
4947 unsigned num_funs,
4948 Z3_func_decl const from[],
4949 Z3_ast const to[]);
4950
4957 Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target);
4967 Z3_model Z3_API Z3_mk_model(Z3_context c);
4968
4973 void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m);
4974
4979 void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m);
4980
5003 bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v);
5004
5013 Z3_ast_opt Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a);
5014
5019 bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a);
5020
5032 Z3_func_interp_opt Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f);
5033
5040 unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m);
5041
5051 Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i);
5052
5062 unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m);
5063
5072 Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i);
5073
5085 unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m);
5086
5096 Z3_sort Z3_API Z3_model_get_sort(Z3_context c, Z3_model m, unsigned i);
5097
5105 Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s);
5106
5115 Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst);
5116
5127 bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a);
5128
5135 Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a);
5136
5147 Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value);
5148
5153 void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a);
5154
5159 void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f);
5160
5165 void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f);
5166
5177 unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f);
5178
5188 Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i);
5189
5197 Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f);
5198
5206 void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value);
5207
5212 unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f);
5213
5227 void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value);
5228
5233 void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e);
5234
5239 void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e);
5240
5250 Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e);
5251
5259 unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e);
5260
5270 Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i);
5282 bool Z3_API Z3_open_log(Z3_string filename);
5283
5295 void Z3_API Z3_append_log(Z3_string string);
5296
5304 void Z3_API Z3_close_log(void);
5305
5313 void Z3_API Z3_toggle_warning_messages(bool enabled);
5334 void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode);
5335
5347 Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a);
5348
5351 Z3_string Z3_API Z3_pattern_to_string(Z3_context c, Z3_pattern p);
5352
5355 Z3_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s);
5356
5359 Z3_string Z3_API Z3_func_decl_to_string(Z3_context c, Z3_func_decl d);
5360
5369 Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m);
5370
5389 Z3_string name,
5390 Z3_string logic,
5391 Z3_string status,
5392 Z3_string attributes,
5393 unsigned num_assumptions,
5394 Z3_ast const assumptions[],
5395 Z3_ast formula);
5396
5408 Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c,
5409 Z3_string str,
5410 unsigned num_sorts,
5411 Z3_symbol const sort_names[],
5412 Z3_sort const sorts[],
5413 unsigned num_decls,
5414 Z3_symbol const decl_names[],
5415 Z3_func_decl const decls[]);
5416
5421 Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c,
5422 Z3_string file_name,
5423 unsigned num_sorts,
5424 Z3_symbol const sort_names[],
5425 Z3_sort const sorts[],
5426 unsigned num_decls,
5427 Z3_symbol const decl_names[],
5428 Z3_func_decl const decls[]);
5429
5430
5439 Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context c, Z3_string str);
5440
5441
5451 Z3_parser_context Z3_API Z3_mk_parser_context(Z3_context c);
5452
5457 void Z3_API Z3_parser_context_inc_ref(Z3_context c, Z3_parser_context pc);
5458
5463 void Z3_API Z3_parser_context_dec_ref(Z3_context c, Z3_parser_context pc);
5464
5469 void Z3_API Z3_parser_context_add_sort(Z3_context c, Z3_parser_context pc, Z3_sort s);
5470
5475 void Z3_API Z3_parser_context_add_decl(Z3_context c, Z3_parser_context pc, Z3_func_decl f);
5476
5481 Z3_ast_vector Z3_API Z3_parser_context_from_string(Z3_context c, Z3_parser_context pc, Z3_string s);
5482
5483
5488#ifndef SAFE_ERRORS
5498 Z3_error_code Z3_API Z3_get_error_code(Z3_context c);
5499
5512 void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h);
5513#endif
5514
5519 void Z3_API Z3_set_error(Z3_context c, Z3_error_code e);
5520
5525 Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err);
5526
5538 void Z3_API Z3_get_version(unsigned * major, unsigned * minor, unsigned * build_number, unsigned * revision_number);
5539
5547
5555 void Z3_API Z3_enable_trace(Z3_string tag);
5556
5564 void Z3_API Z3_disable_trace(Z3_string tag);
5565
5575 void Z3_API Z3_reset_memory(void);
5576
5584 void Z3_API Z3_finalize_memory(void);
5605 Z3_goal Z3_API Z3_mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs);
5606
5611 void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g);
5612
5617 void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g);
5618
5625 Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g);
5626
5638 void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a);
5639
5644 bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g);
5645
5650 unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g);
5651
5656 void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g);
5657
5662 unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g);
5663
5670 Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx);
5671
5676 unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g);
5677
5682 bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g);
5683
5688 bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g);
5689
5694 Z3_goal Z3_API Z3_goal_translate(Z3_context source, Z3_goal g, Z3_context target);
5695
5702 Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m);
5703
5708 Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g);
5709
5719 Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names);
5720
5733 Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name);
5734
5739 void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t);
5740
5745 void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g);
5746
5756 Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name);
5757
5762 void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p);
5763
5768 void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p);
5769
5775 Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2);
5776
5782 Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2);
5783
5788 Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[]);
5789
5795 Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2);
5796
5802 Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms);
5803
5809 Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t);
5810
5816 Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2);
5817
5823 Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max);
5824
5829 Z3_tactic Z3_API Z3_tactic_skip(Z3_context c);
5830
5835 Z3_tactic Z3_API Z3_tactic_fail(Z3_context c);
5836
5841 Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p);
5842
5848 Z3_tactic Z3_API Z3_tactic_fail_if_not_decided(Z3_context c);
5849
5854 Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p);
5855
5856
5865 Z3_simplifier Z3_API Z3_mk_simplifier(Z3_context c, Z3_string name);
5866
5871 void Z3_API Z3_simplifier_inc_ref(Z3_context c, Z3_simplifier t);
5872
5877 void Z3_API Z3_simplifier_dec_ref(Z3_context c, Z3_simplifier g);
5878
5883 Z3_solver Z3_API Z3_solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier);
5884
5890 Z3_simplifier Z3_API Z3_simplifier_and_then(Z3_context c, Z3_simplifier t1, Z3_simplifier t2);
5891
5896 Z3_simplifier Z3_API Z3_simplifier_using_params(Z3_context c, Z3_simplifier t, Z3_params p);
5897
5898
5905 unsigned Z3_API Z3_get_num_simplifiers(Z3_context c);
5906
5915 Z3_string Z3_API Z3_get_simplifier_name(Z3_context c, unsigned i);
5916
5921 Z3_string Z3_API Z3_simplifier_get_help(Z3_context c, Z3_simplifier t);
5922
5927 Z3_param_descrs Z3_API Z3_simplifier_get_param_descrs(Z3_context c, Z3_simplifier t);
5928
5933 Z3_string Z3_API Z3_simplifier_get_descr(Z3_context c, Z3_string name);
5934
5935
5940 Z3_probe Z3_API Z3_probe_const(Z3_context x, double val);
5941
5948 Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2);
5949
5956 Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2);
5957
5964 Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2);
5965
5972 Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2);
5973
5980 Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2);
5981
5988 Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2);
5989
5996 Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2);
5997
6004 Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p);
6005
6012 unsigned Z3_API Z3_get_num_tactics(Z3_context c);
6013
6022 Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i);
6023
6030 unsigned Z3_API Z3_get_num_probes(Z3_context c);
6031
6040 Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i);
6041
6046 Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t);
6047
6052 Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t);
6053
6058 Z3_string Z3_API Z3_tactic_get_descr(Z3_context c, Z3_string name);
6059
6064 Z3_string Z3_API Z3_probe_get_descr(Z3_context c, Z3_string name);
6065
6071 double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g);
6072
6079 Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g);
6080
6087 Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p);
6088
6093 void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r);
6094
6099 void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r);
6100
6105 Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r);
6106
6113 unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r);
6114
6123 Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i);
6124
6168 Z3_solver Z3_API Z3_mk_solver(Z3_context c);
6169
6198 Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c);
6199
6212 Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic);
6213
6227 Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t);
6228
6233 Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target);
6234
6247 void Z3_API Z3_solver_import_model_converter(Z3_context ctx, Z3_solver src, Z3_solver dst);
6248
6256 Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s);
6257
6265 Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s);
6266
6274 void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p);
6275
6280 void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s);
6281
6286 void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s);
6287
6297 void Z3_API Z3_solver_interrupt(Z3_context c, Z3_solver s);
6298
6308 void Z3_API Z3_solver_push(Z3_context c, Z3_solver s);
6309
6319 void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n);
6320
6328 void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s);
6329
6337 unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s);
6338
6349 void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a);
6350
6367 void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p);
6368
6376 void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name);
6377
6385 void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name);
6386
6391 Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s);
6392
6397 Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s);
6398
6404 Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s);
6405
6410 Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s);
6411
6417 void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[]);
6418
6426 Z3_ast Z3_API Z3_solver_congruence_root(Z3_context c, Z3_solver s, Z3_ast a);
6427
6428
6434 Z3_ast Z3_API Z3_solver_congruence_next(Z3_context c, Z3_solver s, Z3_ast a);
6435
6436
6450 Z3_context c,
6451 Z3_solver s,
6452 void* user_context,
6453 Z3_on_clause_eh on_clause_eh);
6454
6468 Z3_context c,
6469 Z3_solver s,
6470 void* user_context,
6471 Z3_push_eh push_eh,
6472 Z3_pop_eh pop_eh,
6473 Z3_fresh_eh fresh_eh);
6474
6483 void Z3_API Z3_solver_propagate_fixed(Z3_context c, Z3_solver s, Z3_fixed_eh fixed_eh);
6484
6499 void Z3_API Z3_solver_propagate_final(Z3_context c, Z3_solver s, Z3_final_eh final_eh);
6500
6505 void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh);
6506
6511 void Z3_API Z3_solver_propagate_diseq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh);
6512
6518 void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh);
6519
6527 void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh);
6528
6533 void Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase);
6534
6544 Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range);
6545
6552 void Z3_API Z3_solver_propagate_register(Z3_context c, Z3_solver s, Z3_ast e);
6553
6561 void Z3_API Z3_solver_propagate_register_cb(Z3_context c, Z3_solver_callback cb, Z3_ast e);
6562
6571 void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback cb, unsigned num_fixed, Z3_ast const* fixed, unsigned num_eqs, Z3_ast const* eq_lhs, Z3_ast const* eq_rhs, Z3_ast conseq);
6572
6590 Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s);
6591
6602 Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s,
6603 unsigned num_assumptions, Z3_ast const assumptions[]);
6604
6623 Z3_solver s,
6624 unsigned num_terms,
6625 Z3_ast const terms[],
6626 unsigned class_ids[]);
6627
6634 Z3_solver s,
6635 Z3_ast_vector assumptions,
6636 Z3_ast_vector variables,
6637 Z3_ast_vector consequences);
6638
6639
6657 Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level);
6658
6666 Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s);
6667
6676 Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s);
6677
6688 Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s);
6689
6695 Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s);
6696
6703 Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s);
6704
6712 Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s);
6713
6719 Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names);
6720
6730 Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s);
6731
6736 void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s);
6737
6742 void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s);
6743
6748 unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s);
6749
6756 Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx);
6757
6764 bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx);
6765
6772 bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx);
6773
6780 unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx);
6781
6788 double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx);
6789
6794 uint64_t Z3_API Z3_get_estimated_alloc_size(void);
6795
6798#ifdef __cplusplus
6799}
6800#endif // __cplusplus
6801
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_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
Definition: z3_api.h:1318
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:140
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_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
Z3_simplifier Z3_API Z3_simplifier_and_then(Z3_context c, Z3_simplifier t1, Z3_simplifier t2)
Return a simplifier that applies t1 to a given goal and t2 to every subgoal produced by t1.
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_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_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
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_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_open_log(Z3_string filename)
Log interaction to a file.
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.
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
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_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_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d)
Return declaration kind corresponding to declaration.
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_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_char_to_bv(Z3_context c, Z3_ast ch)
Create a bit-vector (code point) from character.
void Z3_API Z3_solver_propagate_diseq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)
register a callback on expression dis-equalities.
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_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_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
void Z3_API Z3_simplifier_inc_ref(Z3_context c, Z3_simplifier t)
Increment the reference counter of the given simplifier.
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_sort Z3_API Z3_mk_char_sort(Z3_context c)
Create a sort for unicode characters.
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_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re)
Create the regular language [re].
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.
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_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
Z3_context Z3_API Z3_mk_context(Z3_config c)
Create a context using the given configuration.
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
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_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
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_goal_prec
Z3 custom error handler (See Z3_set_error_handler).
Definition: z3_api.h:1384
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_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_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,...
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_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_str_le(Z3_context c, Z3_ast prefix, Z3_ast s)
Check if s1 is equal or lexicographically strictly less than s2.
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...
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
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_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.
void Z3_API Z3_get_string_contents(Z3_context c, Z3_ast s, unsigned length, unsigned contents[])
Retrieve the unescaped string constant stored in s.
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
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_char_le(Z3_context c, Z3_ast ch1, Z3_ast ch2)
Create less than or equal to between two characters.
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....
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.
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.
void Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase)
Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context c, 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_toggle_warning_messages(bool enabled)
Enable/disable printing warning messages to the console.
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
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.
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_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_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_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:962
void Z3_API Z3_parser_context_add_decl(Z3_context c, Z3_parser_context pc, Z3_func_decl f)
Add a function declaration.
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
Z3_ast Z3_API Z3_mk_string_from_code(Z3_context c, Z3_ast a)
Code to string conversion.
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
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.
bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value)
Get a global (or module) parameter.
Z3_string Z3_API Z3_simplifier_get_help(Z3_context c, Z3_simplifier t)
Return a string containing a description of parameters accepted by the given simplifier.
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_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_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....
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_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
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_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
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.
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
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_sort Z3_API Z3_get_seq_sort_basis(Z3_context c, Z3_sort s)
Retrieve basis sort for sequence sort.
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.
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
bool Z3_API Z3_is_char_sort(Z3_context c, Z3_sort s)
Check if s is a character sort.
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...
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].
void Z3_API Z3_simplifier_dec_ref(Z3_context c, Z3_simplifier g)
Decrement the reference counter of the given simplifier.
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_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.
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_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_string Z3_API Z3_func_decl_to_string(Z3_context c, Z3_func_decl d)
Z3_ast Z3_API Z3_mk_re_allchar(Z3_context c, Z3_sort regex_sort)
Create a regular expression that accepts all singleton sequences of the regular expression sort.
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
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_false(Z3_context c)
Create an AST node representing false.
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_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_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the right i times.
Z3_ast Z3_API Z3_get_pattern(Z3_context c, Z3_pattern p, unsigned idx)
Return i'th ast in pattern.
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
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...
void Z3_API Z3_finalize_memory(void)
Destroy all allocated resources.
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,...
void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr)
Reclaim memory allocated to constructor.
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re)
Create the complement of the regular language re.
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_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.
Z3_string Z3_API Z3_get_full_version(void)
Return a string that fully describes the version of Z3 in use.
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_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_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...
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_quantifier_num_patterns(Z3_context c, Z3_ast a)
Return number of patterns used in 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_string Z3_API Z3_simplify_get_help(Z3_context c)
Return a string describing all available parameters.
unsigned Z3_API Z3_get_num_probes(Z3_context c)
Return the number of builtin probes available in Z3.
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.
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_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_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_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned *length)
Retrieve the string constant stored in s. The string can contain escape sequences....
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_iff(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 iff t2.
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
void Z3_API Z3_solver_interrupt(Z3_context c, Z3_solver s)
Solver local interrupt. Normally you should use Z3_interrupt to cancel solvers because only one solve...
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_set_add(Z3_context c, Z3_ast set, Z3_ast elem)
Add an element to a set.
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
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.
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_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.
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_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 ...
void Z3_API Z3_enable_concurrent_dec_ref(Z3_context c)
use concurrency control for dec-ref. Reference counting decrements are allowed in separate threads fr...
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.
char const * Z3_char_ptr
Definition: z3_api.h:54
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_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.
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_param_kind
The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params).
Definition: z3_api.h:1301
unsigned Z3_API Z3_get_pattern_num_terms(Z3_context c, Z3_pattern p)
Return number of terms in pattern.
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:53
void Z3_API Z3_parser_context_dec_ref(Z3_context c, Z3_parser_context pc)
Decrement the reference counter of the given Z3_parser_context object.
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_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_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.
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.
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_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_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:109
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
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_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.
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_app Z3_API Z3_to_app(Z3_context c, Z3_ast a)
Convert an ast into an APP_AST. This is just type casting.
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
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_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_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
void Z3_API Z3_set_error(Z3_context c, Z3_error_code e)
Set an error.
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.
bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a)
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_solver_congruence_next(Z3_context c, Z3_solver s, Z3_ast a)
retrieve the next expression in the congruence class. The set of congruent siblings form a cyclic lis...
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_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_goal_num_exprs(Z3_context c, Z3_goal g)
Return the number of formulas, subformulas and terms in the given goal.
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 Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
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.
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_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_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_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_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.
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_u32string(Z3_context c, unsigned len, unsigned const chars[])
Create a string constant out of the string that is passed in It takes the length of the string as wel...
unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)
Return the number of formulas in the given goal.
Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort *domain, Z3_sort range)
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_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.
bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s)
Check if s is a string sort.
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_tactic Z3_API Z3_tactic_fail(Z3_context c)
Return a tactic that always fails.
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_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
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_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
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_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.
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.
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.
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_string Z3_API Z3_pattern_to_string(Z3_context c, Z3_pattern p)
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_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name)
create a forward reference to a recursive datatype being declared. The forward reference can be used ...
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_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.
int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s)
Return the symbol int value.
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_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2)
Rotate bits of t1 to the left t2 times.
void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.
Z3_string Z3_API Z3_simplifier_get_descr(Z3_context c, Z3_string name)
Return a string containing a description of the simplifier with the given name.
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_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)
Return number of constructors for datatype.
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_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_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_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
Z3_simplifier Z3_API Z3_simplifier_using_params(Z3_context c, Z3_simplifier t, Z3_params p)
Return a simplifier that applies t using the given set of parameters.
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_sbv_to_str(Z3_context c, Z3_ast s)
Signed bit-vector to string conversion.
Z3_sort Z3_API Z3_get_array_sort_domain_n(Z3_context c, Z3_sort t, unsigned idx)
Return the i'th domain sort of an n-dimensional array.
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_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_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_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
Z3_param_descrs Z3_API Z3_simplifier_get_param_descrs(Z3_context c, Z3_simplifier t)
Return the parameter description set for the given simplifier object.
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
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_quantifier_num_no_patterns(Z3_context c, Z3_ast a)
Return number of no_patterns used in quantifier.
unsigned Z3_API Z3_get_num_simplifiers(Z3_context c)
Return the number of builtin simplifiers available in Z3.
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th constructor.
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:61
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
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_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_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_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s)
Check if suffix is a suffix of s.
Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[])
Create a pattern for quantifier instantiation.
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_sort Z3_API Z3_get_re_sort_basis(Z3_context c, Z3_sort s)
Retrieve basis sort for regex sort.
Z3_sort Z3_API Z3_mk_set_sort(Z3_context c, Z3_sort ty)
Create Set type.
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.
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.
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.
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.
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
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,...
void Z3_API Z3_solver_propagate_register_cb(Z3_context c, Z3_solver_callback cb, Z3_ast e)
register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Ve...
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_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i)
Return the name of the i probe.
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.
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_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a)
Add a constant interpretation.
Z3_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s)
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)
Decrement the reference counter of the given parameter set.
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_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_solver_congruence_root(Z3_context c, Z3_solver s, Z3_ast a)
retrieve the congruence closure root of an expression. The root is retrieved relative to the state wh...
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
unsigned Z3_API Z3_get_string_length(Z3_context c, Z3_ast s)
Retrieve the length of the unescaped string constant stored in s.
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_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.
void Z3_API Z3_solver_propagate_final(Z3_context c, Z3_solver s, Z3_final_eh final_eh)
register a callback on final check. This provides freedom to the propagator to delay actions or imple...
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.
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:95
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_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_ast Z3_API Z3_mk_bit2bool(Z3_context c, unsigned i, Z3_ast t1)
Extracts the bit at position i of a bit-vector and yields a boolean.
void Z3_API Z3_solver_register_on_clause(Z3_context c, Z3_solver s, void *user_context, Z3_on_clause_eh on_clause_eh)
register a callback to that retrieves assumed, inferred and deleted clauses during search.
Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names)
Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF...
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th no_pattern.
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_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
unsigned Z3_API Z3_get_num_tactics(Z3_context c)
Return the number of builtin tactics available in Z3.
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_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...
Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)
Return the symbol name.
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_simplifier Z3_API Z3_mk_simplifier(Z3_context c, Z3_string name)
Return a simplifier associated with the given name. The complete list of simplifiers may be obtained ...
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_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
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.
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.
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.
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_seq_to_re(Z3_context c, Z3_ast seq)
Create a regular expression that accepts the sequence seq.
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
unsigned Z3_API Z3_get_relation_arity(Z3_context c, Z3_sort s)
Return arity of relation.
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_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)
Return index of the first occurrence of substr in s starting from offset offset. If s does not contai...
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_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
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_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_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_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
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.
void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)
Erase all formulas from the given goal.
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.
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
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_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
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_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_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)
Set a configuration parameter.
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
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_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_param_descrs Z3_API Z3_get_global_param_descrs(Z3_context c)
Retrieve description of global parameters.
Z3_ast Z3_API Z3_mk_re_power(Z3_context c, Z3_ast re, unsigned n)
Create a power regular expression.
void Z3_API Z3_solver_propagate_init(Z3_context c, Z3_solver s, void *user_context, Z3_push_eh push_eh, Z3_pop_eh pop_eh, Z3_fresh_eh fresh_eh)
register a user-properator with the solver.
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.
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
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_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new incremental solver.
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
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.
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.
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_re_star(Z3_context c, Z3_ast re)
Create the regular language re*.
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_ast Z3_API Z3_mk_char(Z3_context c, unsigned ch)
Create a character literal.
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.
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
void Z3_API Z3_append_log(Z3_string string)
Append user-defined string to interaction log.
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
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_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.
Z3_model Z3_API Z3_mk_model(Z3_context c)
Create a fresh model object. It has reference count 0.
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d)
Return the constant declaration name as a symbol.
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_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_re_diff(Z3_context c, Z3_ast re1, Z3_ast re2)
Create the difference of regular expressions.
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_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See Z3_...
Definition: z3_api.h:75
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
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_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_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
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.
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_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
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_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst)
translate model from context c to context dst.
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...
void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)
Return Z3 version number information.
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.
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.
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_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_parser_context_add_sort(Z3_context c, Z3_parser_context pc, Z3_sort s)
Add a sort declaration.
unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a)
Obtain weight of quantifier.
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.
unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s)
Return the number of backtracking points.
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_del_constructor_list(Z3_context c, Z3_constructor_list clist)
Reclaim memory allocated for constructor list.
Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty)
Create a variable.
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_ast Z3_API Z3_mk_real(Z3_context c, int num, int den)
Create a real from a fraction.
Z3_ast Z3_API Z3_substitute_funs(Z3_context c, Z3_ast a, unsigned num_funs, Z3_func_decl const from[], Z3_ast const to[])
Substitute funcions in from with new expressions in to.
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_error_code
Z3 error codes (See Z3_get_error_code).
Definition: z3_api.h:1343
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_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
uint64_t Z3_API Z3_get_estimated_alloc_size(void)
Return the estimated allocated memory in bytes.
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.
void Z3_API Z3_parser_context_inc_ref(Z3_context c, Z3_parser_context pc)
Increment the reference counter of the given Z3_parser_context 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_...
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_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.
void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback cb, unsigned num_fixed, Z3_ast const *fixed, unsigned num_eqs, Z3_ast const *eq_lhs, Z3_ast const *eq_rhs, Z3_ast conseq)
propagate a consequence based on fixed values. This is a callback a client may invoke during the fixe...
Z3_string Z3_API Z3_get_simplifier_name(Z3_context c, unsigned i)
Return the name of the idx simplifier.
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s. Characters outside the basic printiable ASCII range are esc...
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_error_code Z3_API Z3_get_error_code(Z3_context c)
Return the error code for the last API call.
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.
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
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_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_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i)
Return the name of the idx tactic.
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_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_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch)
Create an integer (code point) from character.
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.
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_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.
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_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a)
Return index of de-Bruijn bound variable.
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...
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.
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 but two different AST objects can m...
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_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d)
Return the sort name as a symbol.
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.
Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th recognizer.
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...
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_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.
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_tactic Z3_API Z3_tactic_skip(Z3_context c)
Return a tactic that just return the given goal.
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_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.
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.
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
Z3_parser_context Z3_API Z3_mk_parser_context(Z3_context c)
Create a parser context.
Z3_ast Z3_API Z3_mk_real_int64(Z3_context c, int64_t num, int64_t den)
Create a real from a fraction of int64.
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_mk_seq_last_index(Z3_context c, Z3_ast s, Z3_ast substr)
Return index of the last occurrence of substr in s. If s does not contain substr, then the value is -...
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)
register a callback on expression equalities.
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 The string may contain escape encoding f...
Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f)
create transitive closure of binary relation.
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_rotate_left(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the left i times.
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_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const *args)
Map f on the argument arrays.
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_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
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.
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_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_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_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
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_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
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_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_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.
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_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a)
Return number of bound variables of quantifier.
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_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, unsigned num_constructors, Z3_constructor const constructors[])
Create list of constructors.
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh)
register a callback when a new expression with a registered function is used by the solver The regist...
unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s)
Return a unique identifier for s.
Z3_ast_vector Z3_API Z3_parser_context_from_string(Z3_context c, Z3_parser_context pc, Z3_string s)
Parse a string of SMTLIB2 commands. Return assertions.
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_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_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
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_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs, Z3_ast v)
n-ary Array update.
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.
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_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_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
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].
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.
Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names)
Convert a solver into a DIMACS formatted string.
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.
unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f)
Return a unique identifier for f.
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_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh)
register a callback when the solver decides to split on a registered expression. The callback may set...
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_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
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_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th pattern.
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....
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.
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)
Decrement the reference counter of the given goal.
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
void Z3_API Z3_solver_propagate_register(Z3_context c, Z3_solver s, Z3_ast e)
register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Ve...
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the variables in a with the expressions in to. For every i smaller than num_exprs,...
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_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
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...
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
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.
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_solver Z3_API Z3_solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier)
Attach simplifier to a solver. The solver will use the simplifier for incremental pre-processing.
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_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_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.
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_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a decimal string of a numeric constant term.
void Z3_API Z3_solver_propagate_fixed(Z3_context c, Z3_solver s, Z3_fixed_eh fixed_eh)
register a callback for when an expression is bound to a fixed value. The supported expression types ...
void Z3_API Z3_close_log(void)
Close interaction log.
Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch)
Create a check if the character is a digit.
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.
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_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
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_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_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
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_numeral_binary_string(Z3_context c, Z3_ast a)
Return numeral value, as a binary string of a numeric constant term.
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_disable_trace(Z3_string tag)
Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.
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_string * Z3_string_ptr
Definition: z3_api.h:55
Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx)
Return a formula from the given goal.
Z3_ast Z3_API Z3_mk_divides(Z3_context c, Z3_ast t1, Z3_ast t2)
Create division predicate.
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
Z3_ast Z3_API Z3_mk_char_from_bv(Z3_context c, Z3_ast bv)
Create a character from a bit-vector (code point).
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)
Return the number of entries in the given function interpretation.
bool Z3_API Z3_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_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2)
compare sorts.
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)
Return numeral as a double.
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_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_real2int(Z3_context c, Z3_ast t1)
Coerce a real to an integer.
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_reset_memory(void)
Reset all allocated resources.
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
bool Z3_API Z3_is_app(Z3_context c, Z3_ast a)
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 ...
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.
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
Z3_ast Z3_API Z3_mk_string_to_code(Z3_context c, Z3_ast a)
String to code conversion.
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_mk_ubv_to_str(Z3_context c, Z3_ast s)
Unsigned bit-vector to string conversion.
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for unicode strings.
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.
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_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
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_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
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...
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
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_PRINT_SMTLIB2_COMPLIANT
Definition: z3_api.h:1321
@ Z3_PRINT_SMTLIB_FULL
Definition: z3_api.h:1319
@ Z3_PRINT_LOW_LEVEL
Definition: z3_api.h:1320
@ Z3_APP_AST
Definition: z3_api.h:142
@ Z3_VAR_AST
Definition: z3_api.h:143
@ Z3_SORT_AST
Definition: z3_api.h:145
@ Z3_NUMERAL_AST
Definition: z3_api.h:141
@ Z3_FUNC_DECL_AST
Definition: z3_api.h:146
@ Z3_QUANTIFIER_AST
Definition: z3_api.h:144
@ Z3_UNKNOWN_AST
Definition: z3_api.h:147
@ Z3_GOAL_UNDER
Definition: z3_api.h:1386
@ Z3_GOAL_UNDER_OVER
Definition: z3_api.h:1388
@ Z3_GOAL_OVER
Definition: z3_api.h:1387
@ Z3_GOAL_PRECISE
Definition: z3_api.h:1385
@ Z3_OP_BSMOD
Definition: z3_api.h:1026
@ Z3_OP_SUB
Definition: z3_api.h:985
@ Z3_OP_STRING_LE
Definition: z3_api.h:1175
@ Z3_OP_SIGN_EXT
Definition: z3_api.h:1054
@ Z3_OP_FPA_MUL
Definition: z3_api.h:1248
@ Z3_OP_RE_OF_PRED
Definition: z3_api.h:1192
@ Z3_OP_FPA_IS_NEGATIVE
Definition: z3_api.h:1268
@ Z3_OP_FPA_ROUND_TO_INTEGRAL
Definition: z3_api.h:1256
@ Z3_OP_FD_CONSTANT
Definition: z3_api.h:1144
@ Z3_OP_BADD
Definition: z3_api.h:1018
@ Z3_OP_BIT1
Definition: z3_api.h:1015
@ Z3_OP_BREDAND
Definition: z3_api.h:1060
@ Z3_OP_MUL
Definition: z3_api.h:987
@ Z3_OP_XOR3
Definition: z3_api.h:1075
@ Z3_OP_FPA_SUB
Definition: z3_api.h:1246
@ Z3_OP_UGEQ
Definition: z3_api.h:1038
@ Z3_OP_RE_POWER
Definition: z3_api.h:1187
@ Z3_OP_SBV_TO_STR
Definition: z3_api.h:1171
@ Z3_OP_BUDIV
Definition: z3_api.h:1023
@ Z3_OP_FPA_ABS
Definition: z3_api.h:1251
@ Z3_OP_SLT
Definition: z3_api.h:1041
@ Z3_OP_BASHR
Definition: z3_api.h:1065
@ Z3_OP_PR_LEMMA
Definition: z3_api.h:1110
@ Z3_OP_PR_BIND
Definition: z3_api.h:1098
@ Z3_OP_SEQ_LENGTH
Definition: z3_api.h:1161
@ Z3_OP_FPA_PLUS_ZERO
Definition: z3_api.h:1242
@ Z3_OP_PR_IFF_FALSE
Definition: z3_api.h:1113
@ Z3_OP_SEQ_AT
Definition: z3_api.h:1159
@ Z3_OP_INTERNAL
Definition: z3_api.h:1283
@ Z3_OP_PR_MONOTONICITY
Definition: z3_api.h:1096
@ Z3_OP_PR_UNIT_RESOLUTION
Definition: z3_api.h:1111
@ Z3_OP_RE_PLUS
Definition: z3_api.h:1178
@ Z3_OP_FPA_NUM
Definition: z3_api.h:1238
@ Z3_OP_LABEL
Definition: z3_api.h:1205
@ Z3_OP_ARRAY_EXT
Definition: z3_api.h:1009
@ Z3_OP_SEQ_CONCAT
Definition: z3_api.h:1150
@ Z3_OP_RE_EMPTY_SET
Definition: z3_api.h:1189
@ Z3_OP_SEQ_INDEX
Definition: z3_api.h:1162
@ Z3_OP_SET_DIFFERENCE
Definition: z3_api.h:1005
@ Z3_OP_PR_IFF_TRUE
Definition: z3_api.h:1112
@ Z3_OP_RE_RANGE
Definition: z3_api.h:1183
@ Z3_OP_BUDIV_I
Definition: z3_api.h:1081
@ Z3_OP_DISTINCT
Definition: z3_api.h:967
@ Z3_OP_RE_REVERSE
Definition: z3_api.h:1193
@ Z3_OP_SEQ_REPLACE_RE
Definition: z3_api.h:1156
@ Z3_OP_EXTRACT
Definition: z3_api.h:1056
@ Z3_OP_RA_STORE
Definition: z3_api.h:1131
@ Z3_OP_FPA_FMA
Definition: z3_api.h:1254
@ Z3_OP_BOR
Definition: z3_api.h:1046
@ Z3_OP_FPA_GT
Definition: z3_api.h:1260
@ Z3_OP_DT_UPDATE_FIELD
Definition: z3_api.h:1213
@ Z3_OP_BUREM_I
Definition: z3_api.h:1083
@ Z3_OP_SET_COMPLEMENT
Definition: z3_api.h:1006
@ Z3_OP_PR_QUANT_INST
Definition: z3_api.h:1108
@ Z3_OP_RA_WIDEN
Definition: z3_api.h:1136
@ Z3_OP_RE_COMPLEMENT
Definition: z3_api.h:1188
@ Z3_OP_AND
Definition: z3_api.h:969
@ Z3_OP_STRING_LT
Definition: z3_api.h:1174
@ Z3_OP_ARRAY_MAP
Definition: z3_api.h:1001
@ Z3_OP_PR_REFLEXIVITY
Definition: z3_api.h:1092
@ Z3_OP_FALSE
Definition: z3_api.h:965
@ Z3_OP_PR_DEF_AXIOM
Definition: z3_api.h:1115
@ Z3_OP_SPECIAL_RELATION_TRC
Definition: z3_api.h:1228
@ Z3_OP_XOR
Definition: z3_api.h:972
@ Z3_OP_BIT2BOOL
Definition: z3_api.h:1071
@ Z3_OP_FPA_GE
Definition: z3_api.h:1262
@ Z3_OP_RA_IS_EMPTY
Definition: z3_api.h:1133
@ Z3_OP_PR_MODUS_PONENS
Definition: z3_api.h:1091
@ Z3_OP_RA_EMPTY
Definition: z3_api.h:1132
@ Z3_OP_PR_MODUS_PONENS_OEQ
Definition: z3_api.h:1126
@ Z3_OP_SEQ_REPLACE
Definition: z3_api.h:1155
@ Z3_OP_DT_IS
Definition: z3_api.h:1211
@ Z3_OP_CONST_ARRAY
Definition: z3_api.h:1000
@ Z3_OP_IMPLIES
Definition: z3_api.h:974
@ Z3_OP_SELECT
Definition: z3_api.h:999
@ Z3_OP_FPA_TO_FP
Definition: z3_api.h:1272
@ Z3_OP_FPA_NEG
Definition: z3_api.h:1247
@ Z3_OP_FPA_NAN
Definition: z3_api.h:1241
@ Z3_OP_RA_CLONE
Definition: z3_api.h:1143
@ Z3_OP_ADD
Definition: z3_api.h:984
@ Z3_OP_GT
Definition: z3_api.h:983
@ Z3_OP_PR_NOT_OR_ELIM
Definition: z3_api.h:1101
@ Z3_OP_FPA_TO_REAL
Definition: z3_api.h:1276
@ Z3_OP_ULEQ
Definition: z3_api.h:1036
@ Z3_OP_FPA_EQ
Definition: z3_api.h:1258
@ Z3_OP_INT2BV
Definition: z3_api.h:1072
@ Z3_OP_TO_INT
Definition: z3_api.h:993
@ Z3_OP_PB_EQ
Definition: z3_api.h:1220
@ Z3_OP_PR_TRANSITIVITY
Definition: z3_api.h:1094
@ Z3_OP_BNUM
Definition: z3_api.h:1014
@ Z3_OP_REM
Definition: z3_api.h:990
@ Z3_OP_POWER
Definition: z3_api.h:995
@ Z3_OP_RE_DERIVATIVE
Definition: z3_api.h:1194
@ Z3_OP_SET_UNION
Definition: z3_api.h:1003
@ Z3_OP_FPA_LE
Definition: z3_api.h:1261
@ Z3_OP_FPA_MAX
Definition: z3_api.h:1253
@ Z3_OP_MOD
Definition: z3_api.h:991
@ Z3_OP_SET_HAS_SIZE
Definition: z3_api.h:1010
@ Z3_OP_RE_UNION
Definition: z3_api.h:1182
@ Z3_OP_OEQ
Definition: z3_api.h:975
@ Z3_OP_BCOMP
Definition: z3_api.h:1061
@ Z3_OP_CHAR_LE
Definition: z3_api.h:1198
@ Z3_OP_FPA_RM_TOWARD_NEGATIVE
Definition: z3_api.h:1235
@ Z3_OP_BSMOD_I
Definition: z3_api.h:1084
@ Z3_OP_PR_IFF_OEQ
Definition: z3_api.h:1122
@ Z3_OP_BNOR
Definition: z3_api.h:1050
@ Z3_OP_UMINUS
Definition: z3_api.h:986
@ Z3_OP_SEQ_UNIT
Definition: z3_api.h:1148
@ Z3_OP_DT_RECOGNISER
Definition: z3_api.h:1210
@ Z3_OP_ITE
Definition: z3_api.h:968
@ Z3_OP_FPA_IS_ZERO
Definition: z3_api.h:1265
@ Z3_OP_FPA_IS_SUBNORMAL
Definition: z3_api.h:1267
@ Z3_OP_EQ
Definition: z3_api.h:966
@ Z3_OP_INT_TO_STR
Definition: z3_api.h:1169
@ Z3_OP_ROTATE_RIGHT
Definition: z3_api.h:1067
@ Z3_OP_RA_COMPLEMENT
Definition: z3_api.h:1141
@ Z3_OP_GE
Definition: z3_api.h:981
@ Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
Definition: z3_api.h:1232
@ Z3_OP_PR_ASSERTED
Definition: z3_api.h:1089
@ Z3_OP_DT_ACCESSOR
Definition: z3_api.h:1212
@ Z3_OP_BLSHR
Definition: z3_api.h:1064
@ Z3_OP_IFF
Definition: z3_api.h:971
@ Z3_OP_FPA_BVWRAP
Definition: z3_api.h:1280
@ Z3_OP_UNINTERPRETED
Definition: z3_api.h:1286
@ Z3_OP_AS_ARRAY
Definition: z3_api.h:1008
@ Z3_OP_FPA_BV2RM
Definition: z3_api.h:1281
@ Z3_OP_RE_CONCAT
Definition: z3_api.h:1181
@ Z3_OP_FPA_PLUS_INF
Definition: z3_api.h:1239
@ Z3_OP_PR_REWRITE_STAR
Definition: z3_api.h:1103
@ Z3_OP_PR_HYPOTHESIS
Definition: z3_api.h:1109
@ Z3_OP_BNAND
Definition: z3_api.h:1049
@ Z3_OP_PB_AT_LEAST
Definition: z3_api.h:1217
@ Z3_OP_PR_NNF_NEG
Definition: z3_api.h:1124
@ Z3_OP_FPA_DIV
Definition: z3_api.h:1249
@ Z3_OP_PR_ELIM_UNUSED_VARS
Definition: z3_api.h:1106
@ Z3_OP_RA_UNION
Definition: z3_api.h:1135
@ Z3_OP_PR_CLAUSE_TRAIL
Definition: z3_api.h:1119
@ Z3_OP_PR_TH_LEMMA
Definition: z3_api.h:1127
@ Z3_OP_UGT
Definition: z3_api.h:1042
@ Z3_OP_BXOR
Definition: z3_api.h:1048
@ Z3_OP_SEQ_SUFFIX
Definition: z3_api.h:1152
@ Z3_OP_BSMUL_NO_OVFL
Definition: z3_api.h:1077
@ Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
Definition: z3_api.h:1233
@ Z3_OP_RA_SELECT
Definition: z3_api.h:1142
@ Z3_OP_IS_INT
Definition: z3_api.h:994
@ Z3_OP_REPEAT
Definition: z3_api.h:1057
@ Z3_OP_RA_JOIN
Definition: z3_api.h:1134
@ Z3_OP_PR_PULL_QUANT
Definition: z3_api.h:1104
@ Z3_OP_FPA_SQRT
Definition: z3_api.h:1255
@ Z3_OP_CHAR_CONST
Definition: z3_api.h:1197
@ Z3_OP_FPA_RM_TOWARD_ZERO
Definition: z3_api.h:1236
@ Z3_OP_SEQ_IN_RE
Definition: z3_api.h:1165
@ Z3_OP_BSHL
Definition: z3_api.h:1063
@ Z3_OP_BSDIV
Definition: z3_api.h:1022
@ Z3_OP_OR
Definition: z3_api.h:970
@ Z3_OP_EXT_ROTATE_LEFT
Definition: z3_api.h:1068
@ Z3_OP_FPA_TO_SBV
Definition: z3_api.h:1275
@ Z3_OP_PB_GE
Definition: z3_api.h:1219
@ Z3_OP_BXNOR
Definition: z3_api.h:1051
@ Z3_OP_STR_TO_INT
Definition: z3_api.h:1168
@ Z3_OP_LABEL_LIT
Definition: z3_api.h:1206
@ Z3_OP_RECURSIVE
Definition: z3_api.h:1284
@ Z3_OP_FD_LT
Definition: z3_api.h:1145
@ Z3_OP_UBV_TO_STR
Definition: z3_api.h:1170
@ Z3_OP_SET_INTERSECT
Definition: z3_api.h:1004
@ Z3_OP_FPA_MIN
Definition: z3_api.h:1252
@ Z3_OP_BSMUL_NO_UDFL
Definition: z3_api.h:1079
@ Z3_OP_TO_REAL
Definition: z3_api.h:992
@ Z3_OP_EXT_ROTATE_RIGHT
Definition: z3_api.h:1069
@ Z3_OP_PR_APPLY_DEF
Definition: z3_api.h:1121
@ Z3_OP_RE_DIFF
Definition: z3_api.h:1184
@ Z3_OP_DIV
Definition: z3_api.h:988
@ Z3_OP_BSUB
Definition: z3_api.h:1019
@ Z3_OP_BNEG
Definition: z3_api.h:1017
@ Z3_OP_SEQ_CONTAINS
Definition: z3_api.h:1153
@ Z3_OP_PR_SKOLEMIZE
Definition: z3_api.h:1125
@ Z3_OP_STR_TO_CODE
Definition: z3_api.h:1172
@ Z3_OP_FPA_RM_TOWARD_POSITIVE
Definition: z3_api.h:1234
@ Z3_OP_FPA_ADD
Definition: z3_api.h:1245
@ Z3_OP_PR_COMMUTATIVITY
Definition: z3_api.h:1114
@ Z3_OP_RE_FULL_SET
Definition: z3_api.h:1190
@ Z3_OP_SET_SUBSET
Definition: z3_api.h:1007
@ Z3_OP_BSREM
Definition: z3_api.h:1024
@ Z3_OP_NOT
Definition: z3_api.h:973
@ Z3_OP_BSREM_I
Definition: z3_api.h:1082
@ Z3_OP_SEQ_NTH
Definition: z3_api.h:1160
@ Z3_OP_SEQ_LAST_INDEX
Definition: z3_api.h:1163
@ Z3_OP_PR_PUSH_QUANT
Definition: z3_api.h:1105
@ Z3_OP_PR_SYMMETRY
Definition: z3_api.h:1093
@ Z3_OP_SPECIAL_RELATION_PO
Definition: z3_api.h:1224
@ Z3_OP_RE_LOOP
Definition: z3_api.h:1186
@ Z3_OP_ZERO_EXT
Definition: z3_api.h:1055
@ Z3_OP_SLEQ
Definition: z3_api.h:1037
@ Z3_OP_RA_FILTER
Definition: z3_api.h:1138
@ Z3_OP_FPA_MINUS_INF
Definition: z3_api.h:1240
@ Z3_OP_PR_QUANT_INTRO
Definition: z3_api.h:1097
@ Z3_OP_PR_DER
Definition: z3_api.h:1107
@ Z3_OP_BUREM0
Definition: z3_api.h:1033
@ Z3_OP_SEQ_EMPTY
Definition: z3_api.h:1149
@ Z3_OP_PR_HYPER_RESOLVE
Definition: z3_api.h:1128
@ Z3_OP_FPA_IS_POSITIVE
Definition: z3_api.h:1269
@ Z3_OP_LT
Definition: z3_api.h:982
@ Z3_OP_BSDIV0
Definition: z3_api.h:1030
@ Z3_OP_CHAR_TO_BV
Definition: z3_api.h:1200
@ Z3_OP_PR_GOAL
Definition: z3_api.h:1090
@ Z3_OP_SPECIAL_RELATION_TC
Definition: z3_api.h:1227
@ Z3_OP_RA_PROJECT
Definition: z3_api.h:1137
@ Z3_OP_FPA_IS_NAN
Definition: z3_api.h:1263
@ Z3_OP_SPECIAL_RELATION_TO
Definition: z3_api.h:1226
@ Z3_OP_PR_TRUE
Definition: z3_api.h:1088
@ Z3_OP_RA_RENAME
Definition: z3_api.h:1140
@ Z3_OP_AGNUM
Definition: z3_api.h:979
@ Z3_OP_BNOT
Definition: z3_api.h:1047
@ Z3_OP_FPA_IS_INF
Definition: z3_api.h:1264
@ Z3_OP_BSMOD0
Definition: z3_api.h:1034
@ Z3_OP_CONCAT
Definition: z3_api.h:1053
@ Z3_OP_FPA_TO_FP_UNSIGNED
Definition: z3_api.h:1273
@ Z3_OP_PR_REDUNDANT_DEL
Definition: z3_api.h:1118
@ Z3_OP_PR_NNF_POS
Definition: z3_api.h:1123
@ Z3_OP_SEQ_REPLACE_ALL
Definition: z3_api.h:1158
@ Z3_OP_FPA_REM
Definition: z3_api.h:1250
@ Z3_OP_SEQ_EXTRACT
Definition: z3_api.h:1154
@ Z3_OP_RA_NEGATION_FILTER
Definition: z3_api.h:1139
@ Z3_OP_PR_LEMMA_ADD
Definition: z3_api.h:1117
@ Z3_OP_RE_OPTION
Definition: z3_api.h:1180
@ Z3_OP_BUDIV0
Definition: z3_api.h:1031
@ Z3_OP_PR_REWRITE
Definition: z3_api.h:1102
@ Z3_OP_BV2INT
Definition: z3_api.h:1073
@ Z3_OP_RE_INTERSECT
Definition: z3_api.h:1185
@ Z3_OP_SET_CARD
Definition: z3_api.h:1011
@ Z3_OP_PR_DEF_INTRO
Definition: z3_api.h:1120
@ Z3_OP_FPA_MINUS_ZERO
Definition: z3_api.h:1243
@ Z3_OP_SPECIAL_RELATION_PLO
Definition: z3_api.h:1225
@ Z3_OP_BUMUL_NO_OVFL
Definition: z3_api.h:1078
@ Z3_OP_SGEQ
Definition: z3_api.h:1039
@ Z3_OP_ROTATE_LEFT
Definition: z3_api.h:1066
@ Z3_OP_PR_UNDEF
Definition: z3_api.h:1087
@ Z3_OP_PR_AND_ELIM
Definition: z3_api.h:1100
@ Z3_OP_PR_ASSUMPTION_ADD
Definition: z3_api.h:1116
@ Z3_OP_FPA_TO_UBV
Definition: z3_api.h:1274
@ Z3_OP_FPA_LT
Definition: z3_api.h:1259
@ Z3_OP_BMUL
Definition: z3_api.h:1020
@ Z3_OP_PR_TRANSITIVITY_STAR
Definition: z3_api.h:1095
@ Z3_OP_PB_LE
Definition: z3_api.h:1218
@ Z3_OP_PB_AT_MOST
Definition: z3_api.h:1216
@ Z3_OP_CHAR_TO_INT
Definition: z3_api.h:1199
@ Z3_OP_FPA_IS_NORMAL
Definition: z3_api.h:1266
@ Z3_OP_ULT
Definition: z3_api.h:1040
@ Z3_OP_STORE
Definition: z3_api.h:998
@ Z3_OP_SGT
Definition: z3_api.h:1043
@ Z3_OP_STR_FROM_CODE
Definition: z3_api.h:1173
@ Z3_OP_CARRY
Definition: z3_api.h:1074
@ Z3_OP_DT_CONSTRUCTOR
Definition: z3_api.h:1209
@ Z3_OP_BIT0
Definition: z3_api.h:1016
@ Z3_OP_CHAR_FROM_BV
Definition: z3_api.h:1201
@ Z3_OP_CHAR_IS_DIGIT
Definition: z3_api.h:1202
@ Z3_OP_RE_FULL_CHAR_SET
Definition: z3_api.h:1191
@ Z3_OP_BUREM
Definition: z3_api.h:1025
@ Z3_OP_SEQ_PREFIX
Definition: z3_api.h:1151
@ Z3_OP_FPA_FP
Definition: z3_api.h:1271
@ Z3_OP_SEQ_REPLACE_RE_ALL
Definition: z3_api.h:1157
@ Z3_OP_BREDOR
Definition: z3_api.h:1059
@ Z3_OP_BSREM0
Definition: z3_api.h:1032
@ Z3_OP_LE
Definition: z3_api.h:980
@ Z3_OP_SPECIAL_RELATION_LO
Definition: z3_api.h:1223
@ Z3_OP_BSDIV_I
Definition: z3_api.h:1080
@ Z3_OP_PR_DISTRIBUTIVITY
Definition: z3_api.h:1099
@ Z3_OP_FPA_TO_IEEE_BV
Definition: z3_api.h:1278
@ Z3_OP_IDIV
Definition: z3_api.h:989
@ Z3_OP_SEQ_TO_RE
Definition: z3_api.h:1164
@ Z3_OP_ANUM
Definition: z3_api.h:978
@ Z3_OP_RE_STAR
Definition: z3_api.h:1179
@ Z3_OP_BAND
Definition: z3_api.h:1045
@ Z3_OP_ARRAY_DEFAULT
Definition: z3_api.h:1002
@ Z3_OP_TRUE
Definition: z3_api.h:964
@ Z3_PK_DOUBLE
Definition: z3_api.h:1304
@ Z3_PK_SYMBOL
Definition: z3_api.h:1305
@ Z3_PK_BOOL
Definition: z3_api.h:1303
@ Z3_PK_OTHER
Definition: z3_api.h:1307
@ Z3_PK_UINT
Definition: z3_api.h:1302
@ Z3_PK_INVALID
Definition: z3_api.h:1308
@ Z3_PK_STRING
Definition: z3_api.h:1306
@ Z3_RELATION_SORT
Definition: z3_api.h:117
@ Z3_BOOL_SORT
Definition: z3_api.h:111
@ Z3_ROUNDING_MODE_SORT
Definition: z3_api.h:120
@ Z3_UNKNOWN_SORT
Definition: z3_api.h:124
@ Z3_BV_SORT
Definition: z3_api.h:114
@ Z3_DATATYPE_SORT
Definition: z3_api.h:116
@ Z3_INT_SORT
Definition: z3_api.h:112
@ Z3_FINITE_DOMAIN_SORT
Definition: z3_api.h:118
@ Z3_RE_SORT
Definition: z3_api.h:122
@ Z3_UNINTERPRETED_SORT
Definition: z3_api.h:110
@ Z3_FLOATING_POINT_SORT
Definition: z3_api.h:119
@ Z3_ARRAY_SORT
Definition: z3_api.h:115
@ Z3_CHAR_SORT
Definition: z3_api.h:123
@ Z3_REAL_SORT
Definition: z3_api.h:113
@ Z3_SEQ_SORT
Definition: z3_api.h:121
@ Z3_L_TRUE
Definition: z3_api.h:64
@ Z3_L_FALSE
Definition: z3_api.h:62
@ Z3_L_UNDEF
Definition: z3_api.h:63
@ Z3_PARAMETER_INT
Definition: z3_api.h:96
@ Z3_PARAMETER_FUNC_DECL
Definition: z3_api.h:102
@ Z3_PARAMETER_SORT
Definition: z3_api.h:100
@ Z3_PARAMETER_RATIONAL
Definition: z3_api.h:98
@ Z3_PARAMETER_AST
Definition: z3_api.h:101
@ Z3_PARAMETER_DOUBLE
Definition: z3_api.h:97
@ Z3_PARAMETER_SYMBOL
Definition: z3_api.h:99
@ Z3_STRING_SYMBOL
Definition: z3_api.h:77
@ Z3_INT_SYMBOL
Definition: z3_api.h:76
@ Z3_INTERNAL_FATAL
Definition: z3_api.h:1353
@ Z3_DEC_REF_ERROR
Definition: z3_api.h:1355
@ Z3_INVALID_USAGE
Definition: z3_api.h:1354
@ Z3_INVALID_PATTERN
Definition: z3_api.h:1350
@ Z3_INVALID_ARG
Definition: z3_api.h:1347
@ Z3_OK
Definition: z3_api.h:1344
@ Z3_IOB
Definition: z3_api.h:1346
@ Z3_FILE_ACCESS_ERROR
Definition: z3_api.h:1352
@ Z3_PARSER_ERROR
Definition: z3_api.h:1348
@ Z3_EXCEPTION
Definition: z3_api.h:1356
@ Z3_SORT_ERROR
Definition: z3_api.h:1345
@ Z3_MEMOUT_FAIL
Definition: z3_api.h:1351
@ Z3_NO_PARSER
Definition: z3_api.h:1349
#define Z3_ast_opt
Definition: z3_api.h:8
#define Z3_sort_opt
Definition: z3_api.h:7
#define Z3_func_interp_opt
Definition: z3_api.h:9