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
10
12
14
46
50typedef const char * Z3_string;
51typedef char const* Z3_char_ptr;
52typedef Z3_string * Z3_string_ptr;
53
57typedef enum
58{
59 Z3_L_FALSE = -1,
60 Z3_L_UNDEF,
61 Z3_L_TRUE
62} Z3_lbool;
63
76
77
105
129
152
989typedef enum {
990 // Basic
991 Z3_OP_TRUE = 0x100,
992 Z3_OP_FALSE,
993 Z3_OP_EQ,
994 Z3_OP_DISTINCT,
995 Z3_OP_ITE,
996 Z3_OP_AND,
997 Z3_OP_OR,
998 Z3_OP_IFF,
999 Z3_OP_XOR,
1000 Z3_OP_NOT,
1001 Z3_OP_IMPLIES,
1002 Z3_OP_OEQ,
1003
1004 // Arithmetic
1005 Z3_OP_ANUM = 0x200,
1006 Z3_OP_AGNUM,
1007 Z3_OP_LE,
1008 Z3_OP_GE,
1009 Z3_OP_LT,
1010 Z3_OP_GT,
1011 Z3_OP_ADD,
1012 Z3_OP_SUB,
1013 Z3_OP_UMINUS,
1014 Z3_OP_MUL,
1015 Z3_OP_DIV,
1016 Z3_OP_IDIV,
1017 Z3_OP_REM,
1018 Z3_OP_MOD,
1019 Z3_OP_TO_REAL,
1020 Z3_OP_TO_INT,
1021 Z3_OP_IS_INT,
1022 Z3_OP_POWER,
1023 Z3_OP_ABS,
1024
1025 // Arrays & Sets
1026 Z3_OP_STORE = 0x300,
1027 Z3_OP_SELECT,
1028 Z3_OP_CONST_ARRAY,
1029 Z3_OP_ARRAY_MAP,
1030 Z3_OP_ARRAY_DEFAULT,
1031 Z3_OP_SET_UNION,
1032 Z3_OP_SET_INTERSECT,
1033 Z3_OP_SET_DIFFERENCE,
1034 Z3_OP_SET_COMPLEMENT,
1035 Z3_OP_SET_SUBSET,
1036 Z3_OP_AS_ARRAY,
1037 Z3_OP_ARRAY_EXT,
1038
1039 // Bit-vectors
1040 Z3_OP_BNUM = 0x400,
1041 Z3_OP_BIT1,
1042 Z3_OP_BIT0,
1043 Z3_OP_BNEG,
1044 Z3_OP_BADD,
1045 Z3_OP_BSUB,
1046 Z3_OP_BMUL,
1047
1048 Z3_OP_BSDIV,
1049 Z3_OP_BUDIV,
1050 Z3_OP_BSREM,
1051 Z3_OP_BUREM,
1052 Z3_OP_BSMOD,
1053
1054 // special functions to record the division by 0 cases
1055 // these are internal functions
1056 Z3_OP_BSDIV0,
1057 Z3_OP_BUDIV0,
1058 Z3_OP_BSREM0,
1059 Z3_OP_BUREM0,
1060 Z3_OP_BSMOD0,
1061
1062 Z3_OP_ULEQ,
1063 Z3_OP_SLEQ,
1064 Z3_OP_UGEQ,
1065 Z3_OP_SGEQ,
1066 Z3_OP_ULT,
1067 Z3_OP_SLT,
1068 Z3_OP_UGT,
1069 Z3_OP_SGT,
1070
1071 Z3_OP_BAND,
1072 Z3_OP_BOR,
1073 Z3_OP_BNOT,
1074 Z3_OP_BXOR,
1075 Z3_OP_BNAND,
1076 Z3_OP_BNOR,
1077 Z3_OP_BXNOR,
1078
1079 Z3_OP_CONCAT,
1080 Z3_OP_SIGN_EXT,
1081 Z3_OP_ZERO_EXT,
1082 Z3_OP_EXTRACT,
1083 Z3_OP_REPEAT,
1084
1085 Z3_OP_BREDOR,
1086 Z3_OP_BREDAND,
1087 Z3_OP_BCOMP,
1088
1089 Z3_OP_BSHL,
1090 Z3_OP_BLSHR,
1091 Z3_OP_BASHR,
1092 Z3_OP_ROTATE_LEFT,
1093 Z3_OP_ROTATE_RIGHT,
1094 Z3_OP_EXT_ROTATE_LEFT,
1095 Z3_OP_EXT_ROTATE_RIGHT,
1096
1097 Z3_OP_BIT2BOOL,
1098 Z3_OP_INT2BV,
1099 Z3_OP_BV2INT,
1100 Z3_OP_SBV2INT,
1101 Z3_OP_CARRY,
1102 Z3_OP_XOR3,
1103
1104 Z3_OP_BSMUL_NO_OVFL,
1105 Z3_OP_BUMUL_NO_OVFL,
1106 Z3_OP_BSMUL_NO_UDFL,
1107 Z3_OP_BSDIV_I,
1108 Z3_OP_BUDIV_I,
1109 Z3_OP_BSREM_I,
1110 Z3_OP_BUREM_I,
1111 Z3_OP_BSMOD_I,
1112
1113 // Proofs
1114 Z3_OP_PR_UNDEF = 0x500,
1115 Z3_OP_PR_TRUE,
1116 Z3_OP_PR_ASSERTED,
1117 Z3_OP_PR_GOAL,
1118 Z3_OP_PR_MODUS_PONENS,
1119 Z3_OP_PR_REFLEXIVITY,
1120 Z3_OP_PR_SYMMETRY,
1121 Z3_OP_PR_TRANSITIVITY,
1122 Z3_OP_PR_TRANSITIVITY_STAR,
1123 Z3_OP_PR_MONOTONICITY,
1124 Z3_OP_PR_QUANT_INTRO,
1125 Z3_OP_PR_BIND,
1126 Z3_OP_PR_DISTRIBUTIVITY,
1127 Z3_OP_PR_AND_ELIM,
1128 Z3_OP_PR_NOT_OR_ELIM,
1129 Z3_OP_PR_REWRITE,
1130 Z3_OP_PR_REWRITE_STAR,
1131 Z3_OP_PR_PULL_QUANT,
1132 Z3_OP_PR_PUSH_QUANT,
1133 Z3_OP_PR_ELIM_UNUSED_VARS,
1134 Z3_OP_PR_DER,
1135 Z3_OP_PR_QUANT_INST,
1136 Z3_OP_PR_HYPOTHESIS,
1137 Z3_OP_PR_LEMMA,
1138 Z3_OP_PR_UNIT_RESOLUTION,
1139 Z3_OP_PR_IFF_TRUE,
1140 Z3_OP_PR_IFF_FALSE,
1141 Z3_OP_PR_COMMUTATIVITY,
1142 Z3_OP_PR_DEF_AXIOM,
1143 Z3_OP_PR_ASSUMPTION_ADD,
1144 Z3_OP_PR_LEMMA_ADD,
1145 Z3_OP_PR_REDUNDANT_DEL,
1146 Z3_OP_PR_CLAUSE_TRAIL,
1147 Z3_OP_PR_DEF_INTRO,
1148 Z3_OP_PR_APPLY_DEF,
1149 Z3_OP_PR_IFF_OEQ,
1150 Z3_OP_PR_NNF_POS,
1151 Z3_OP_PR_NNF_NEG,
1152 Z3_OP_PR_SKOLEMIZE,
1153 Z3_OP_PR_MODUS_PONENS_OEQ,
1154 Z3_OP_PR_TH_LEMMA,
1155 Z3_OP_PR_HYPER_RESOLVE,
1156
1157 // Relational algebra
1158 Z3_OP_RA_STORE = 0x600,
1159 Z3_OP_RA_EMPTY,
1160 Z3_OP_RA_IS_EMPTY,
1161 Z3_OP_RA_JOIN,
1162 Z3_OP_RA_UNION,
1163 Z3_OP_RA_WIDEN,
1164 Z3_OP_RA_PROJECT,
1165 Z3_OP_RA_FILTER,
1166 Z3_OP_RA_NEGATION_FILTER,
1167 Z3_OP_RA_RENAME,
1168 Z3_OP_RA_COMPLEMENT,
1169 Z3_OP_RA_SELECT,
1170 Z3_OP_RA_CLONE,
1171 Z3_OP_FD_CONSTANT,
1172 Z3_OP_FD_LT,
1173
1174 // Sequences
1175 Z3_OP_SEQ_UNIT,
1176 Z3_OP_SEQ_EMPTY,
1177 Z3_OP_SEQ_CONCAT,
1178 Z3_OP_SEQ_PREFIX,
1179 Z3_OP_SEQ_SUFFIX,
1180 Z3_OP_SEQ_CONTAINS,
1181 Z3_OP_SEQ_EXTRACT,
1182 Z3_OP_SEQ_REPLACE,
1183 Z3_OP_SEQ_REPLACE_RE,
1184 Z3_OP_SEQ_REPLACE_RE_ALL,
1185 Z3_OP_SEQ_REPLACE_ALL,
1186 Z3_OP_SEQ_AT,
1187 Z3_OP_SEQ_NTH,
1188 Z3_OP_SEQ_LENGTH,
1189 Z3_OP_SEQ_INDEX,
1190 Z3_OP_SEQ_LAST_INDEX,
1191 Z3_OP_SEQ_TO_RE,
1192 Z3_OP_SEQ_IN_RE,
1193 Z3_OP_SEQ_MAP,
1194 Z3_OP_SEQ_MAPI,
1195 Z3_OP_SEQ_FOLDL,
1196 Z3_OP_SEQ_FOLDLI,
1197 Z3_OP_SEQ_POWER,
1198
1199 // strings
1200 Z3_OP_STR_TO_INT,
1201 Z3_OP_INT_TO_STR,
1202 Z3_OP_UBV_TO_STR,
1203 Z3_OP_SBV_TO_STR,
1204 Z3_OP_STR_TO_CODE,
1205 Z3_OP_STR_FROM_CODE,
1206 Z3_OP_STRING_LT,
1207 Z3_OP_STRING_LE,
1208
1209 // regular expressions
1210 Z3_OP_RE_PLUS,
1211 Z3_OP_RE_STAR,
1212 Z3_OP_RE_OPTION,
1213 Z3_OP_RE_CONCAT,
1214 Z3_OP_RE_UNION,
1215 Z3_OP_RE_RANGE,
1216 Z3_OP_RE_DIFF,
1217 Z3_OP_RE_INTERSECT,
1218 Z3_OP_RE_LOOP,
1219 Z3_OP_RE_POWER,
1220 Z3_OP_RE_COMPLEMENT,
1221 Z3_OP_RE_EMPTY_SET,
1222 Z3_OP_RE_FULL_SET,
1223 Z3_OP_RE_FULL_CHAR_SET,
1224 Z3_OP_RE_OF_PRED,
1225 Z3_OP_RE_REVERSE,
1226 Z3_OP_RE_DERIVATIVE,
1227
1228 // char
1229 Z3_OP_CHAR_CONST,
1230 Z3_OP_CHAR_LE,
1231 Z3_OP_CHAR_TO_INT,
1232 Z3_OP_CHAR_TO_BV,
1233 Z3_OP_CHAR_FROM_BV,
1234 Z3_OP_CHAR_IS_DIGIT,
1235
1236 // Auxiliary
1237 Z3_OP_LABEL = 0x700,
1238 Z3_OP_LABEL_LIT,
1239
1240 // Datatypes
1241 Z3_OP_DT_CONSTRUCTOR=0x800,
1242 Z3_OP_DT_RECOGNISER,
1243 Z3_OP_DT_IS,
1244 Z3_OP_DT_ACCESSOR,
1245 Z3_OP_DT_UPDATE_FIELD,
1246
1247 // Pseudo Booleans
1248 Z3_OP_PB_AT_MOST=0x900,
1249 Z3_OP_PB_AT_LEAST,
1250 Z3_OP_PB_LE,
1251 Z3_OP_PB_GE,
1252 Z3_OP_PB_EQ,
1253
1254 // Special relations
1255 Z3_OP_SPECIAL_RELATION_LO = 0xa000,
1256 Z3_OP_SPECIAL_RELATION_PO,
1257 Z3_OP_SPECIAL_RELATION_PLO,
1258 Z3_OP_SPECIAL_RELATION_TO,
1259 Z3_OP_SPECIAL_RELATION_TC,
1260 Z3_OP_SPECIAL_RELATION_TRC,
1261
1262
1263 // Floating-Point Arithmetic
1264 Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN = 0xb000,
1265 Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY,
1266 Z3_OP_FPA_RM_TOWARD_POSITIVE,
1267 Z3_OP_FPA_RM_TOWARD_NEGATIVE,
1268 Z3_OP_FPA_RM_TOWARD_ZERO,
1269
1270 Z3_OP_FPA_NUM,
1271 Z3_OP_FPA_PLUS_INF,
1272 Z3_OP_FPA_MINUS_INF,
1273 Z3_OP_FPA_NAN,
1274 Z3_OP_FPA_PLUS_ZERO,
1275 Z3_OP_FPA_MINUS_ZERO,
1276
1277 Z3_OP_FPA_ADD,
1278 Z3_OP_FPA_SUB,
1279 Z3_OP_FPA_NEG,
1280 Z3_OP_FPA_MUL,
1281 Z3_OP_FPA_DIV,
1282 Z3_OP_FPA_REM,
1283 Z3_OP_FPA_ABS,
1284 Z3_OP_FPA_MIN,
1285 Z3_OP_FPA_MAX,
1286 Z3_OP_FPA_FMA,
1287 Z3_OP_FPA_SQRT,
1288 Z3_OP_FPA_ROUND_TO_INTEGRAL,
1289
1290 Z3_OP_FPA_EQ,
1291 Z3_OP_FPA_LT,
1292 Z3_OP_FPA_GT,
1293 Z3_OP_FPA_LE,
1294 Z3_OP_FPA_GE,
1295 Z3_OP_FPA_IS_NAN,
1296 Z3_OP_FPA_IS_INF,
1297 Z3_OP_FPA_IS_ZERO,
1298 Z3_OP_FPA_IS_NORMAL,
1299 Z3_OP_FPA_IS_SUBNORMAL,
1300 Z3_OP_FPA_IS_NEGATIVE,
1301 Z3_OP_FPA_IS_POSITIVE,
1302
1303 Z3_OP_FPA_FP,
1304 Z3_OP_FPA_TO_FP,
1305 Z3_OP_FPA_TO_FP_UNSIGNED,
1306 Z3_OP_FPA_TO_UBV,
1307 Z3_OP_FPA_TO_SBV,
1308 Z3_OP_FPA_TO_REAL,
1309
1310 Z3_OP_FPA_TO_IEEE_BV,
1311
1312 Z3_OP_FPA_BVWRAP,
1313 Z3_OP_FPA_BV2RM,
1314
1315 // Finite Sets
1316 Z3_OP_FINITE_SET_EMPTY = 0xc000,
1317 Z3_OP_FINITE_SET_SINGLETON,
1318 Z3_OP_FINITE_SET_UNION,
1319 Z3_OP_FINITE_SET_INTERSECT,
1320 Z3_OP_FINITE_SET_DIFFERENCE,
1321 Z3_OP_FINITE_SET_IN,
1322 Z3_OP_FINITE_SET_SIZE,
1323 Z3_OP_FINITE_SET_SUBSET,
1324 Z3_OP_FINITE_SET_MAP,
1325 Z3_OP_FINITE_SET_FILTER,
1326 Z3_OP_FINITE_SET_RANGE,
1327 Z3_OP_FINITE_SET_EXT,
1328 Z3_OP_FINITE_SET_MAP_INVERSE,
1329
1330 Z3_OP_INTERNAL,
1331 Z3_OP_RECURSIVE,
1332
1333 Z3_OP_UNINTERPRETED,
1334
1335 Z3_OP_FF_NUM = 0xd000,
1336 Z3_OP_FF_ADD,
1337 Z3_OP_FF_MUL,
1338 Z3_OP_FF_NEG,
1339 Z3_OP_FF_BITSUM
1340} Z3_decl_kind;
1341
1363
1376
1377
1411
1416
1420
1424
1425
1443
1445
1446#ifdef __cplusplus
1447extern "C" {
1448#endif // __cplusplus
1449
1451
1476 void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value);
1477
1478
1487 void Z3_API Z3_global_param_reset_all(void);
1488
1501 bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value);
1502
1504
1507
1538 Z3_config Z3_API Z3_mk_config(void);
1539
1546 void Z3_API Z3_del_config(Z3_config c);
1547
1556 void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value);
1557
1559
1562
1593 Z3_context Z3_API Z3_mk_context(Z3_config c);
1594
1619 Z3_context Z3_API Z3_mk_context_rc(Z3_config c);
1620
1627 void Z3_API Z3_del_context(Z3_context c);
1628
1635 void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a);
1636
1643 void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a);
1644
1651 void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value);
1652
1653
1658 Z3_param_descrs Z3_API Z3_get_global_param_descrs(Z3_context c);
1659
1665 void Z3_API Z3_interrupt(Z3_context c);
1666
1667
1674 void Z3_API Z3_enable_concurrent_dec_ref(Z3_context c);
1675
1676
1678
1681
1691 Z3_params Z3_API Z3_mk_params(Z3_context c);
1692
1697 void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p);
1698
1703 void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p);
1704
1709 void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, bool v);
1710
1715 void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v);
1716
1721 void Z3_API Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v);
1722
1727 void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v);
1728
1734 Z3_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p);
1735
1742 void Z3_API Z3_params_validate(Z3_context c, Z3_params p, Z3_param_descrs d);
1743
1745
1748
1753 void Z3_API Z3_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p);
1754
1759 void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p);
1760
1765 Z3_param_kind Z3_API Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n);
1766
1771 unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p);
1772
1779 Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i);
1780
1785 Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s);
1786
1792 Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p);
1793
1795
1798
1811 Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i);
1812
1822 Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s);
1823
1825
1828
1835 Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s);
1836
1845 Z3_sort Z3_API Z3_mk_type_variable(Z3_context c, Z3_symbol s);
1846
1853 Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c);
1854
1865 Z3_sort Z3_API Z3_mk_int_sort(Z3_context c);
1866
1873 Z3_sort Z3_API Z3_mk_real_sort(Z3_context c);
1874
1883 Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz);
1884
1897 Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size);
1898
1901 Z3_sort Z3_API Z3_mk_finite_field_sort(Z3_context c, Z3_string prime);
1904 Z3_string Z3_API Z3_get_finite_field_sort_size(Z3_context c, Z3_sort s);
1907 Z3_ast Z3_API Z3_mk_ff_add(Z3_context c, unsigned n, Z3_ast const args[]);
1910 Z3_ast Z3_API Z3_mk_ff_mul(Z3_context c, unsigned n, Z3_ast const args[]);
1913 Z3_ast Z3_API Z3_mk_ff_neg(Z3_context c, Z3_ast a);
1916 Z3_ast Z3_API Z3_mk_ff_bitsum(Z3_context c, unsigned n, Z3_ast const args[]);
1917
1918
1929 Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range);
1930
1938 Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const * domain, Z3_sort range);
1939
1955 Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c,
1956 Z3_symbol mk_tuple_name,
1957 unsigned num_fields,
1958 Z3_symbol const field_names[],
1959 Z3_sort const field_sorts[],
1960 Z3_func_decl * mk_tuple_decl,
1961 Z3_func_decl proj_decl[]);
1962
1983 Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c,
1984 Z3_symbol name,
1985 unsigned n,
1986 Z3_symbol const enum_names[],
1987 Z3_func_decl enum_consts[],
1988 Z3_func_decl enum_testers[]);
1989
2007 Z3_sort Z3_API Z3_mk_list_sort(Z3_context c,
2008 Z3_symbol name,
2009 Z3_sort elem_sort,
2010 Z3_func_decl* nil_decl,
2011 Z3_func_decl* is_nil_decl,
2012 Z3_func_decl* cons_decl,
2013 Z3_func_decl* is_cons_decl,
2014 Z3_func_decl* head_decl,
2015 Z3_func_decl* tail_decl
2016 );
2017
2036 Z3_constructor Z3_API Z3_mk_constructor(Z3_context c,
2037 Z3_symbol name,
2038 Z3_symbol recognizer,
2039 unsigned num_fields,
2040 Z3_symbol const field_names[],
2041 Z3_sort const sorts[],
2042 unsigned sort_refs[]
2043 );
2044
2052 unsigned Z3_API Z3_constructor_num_fields(Z3_context c, Z3_constructor constr);
2053
2063 void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr);
2064
2079 Z3_sort Z3_API Z3_mk_datatype(Z3_context c,
2080 Z3_symbol name,
2081 unsigned num_constructors,
2082 Z3_constructor constructors[]);
2083
2103 Z3_sort Z3_API Z3_mk_polymorphic_datatype(Z3_context c,
2104 Z3_symbol name,
2105 unsigned num_parameters,
2106 Z3_sort parameters[],
2107 unsigned num_constructors,
2108 Z3_constructor constructors[]);
2109
2125 Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name, unsigned num_params, Z3_sort const params[]);
2126
2138 Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c,
2139 unsigned num_constructors,
2140 Z3_constructor const constructors[]);
2141
2153 void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist);
2154
2169 void Z3_API Z3_mk_datatypes(Z3_context c,
2170 unsigned num_sorts,
2171 Z3_symbol const sort_names[],
2172 Z3_sort sorts[],
2173 Z3_constructor_list constructor_lists[]);
2174
2188 void Z3_API Z3_query_constructor(Z3_context c,
2189 Z3_constructor constr,
2190 unsigned num_fields,
2191 Z3_func_decl* constructor,
2192 Z3_func_decl* tester,
2193 Z3_func_decl accessors[]);
2194
2196
2199
2218 Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s,
2219 unsigned domain_size, Z3_sort const domain[],
2220 Z3_sort range);
2221
2222
2223
2232 Z3_ast Z3_API Z3_mk_app(
2233 Z3_context c,
2234 Z3_func_decl d,
2235 unsigned num_args,
2236 Z3_ast const args[]);
2237
2252 Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty);
2253
2265 Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix,
2266 unsigned domain_size, Z3_sort const domain[],
2267 Z3_sort range);
2268
2283 Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty);
2284
2285
2304 Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s,
2305 unsigned domain_size, Z3_sort const domain[],
2306 Z3_sort range);
2307
2323 void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body);
2324
2326
2333 Z3_ast Z3_API Z3_mk_true(Z3_context c);
2334
2339 Z3_ast Z3_API Z3_mk_false(Z3_context c);
2340
2347 Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r);
2348
2360 Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[]);
2361
2368 Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a);
2369
2377 Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3);
2378
2385 Z3_ast Z3_API Z3_mk_iff(Z3_context c, Z3_ast t1, Z3_ast t2);
2386
2393 Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2);
2394
2401 Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2);
2402
2412 Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[]);
2413
2423 Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[]);
2425
2437 Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[]);
2438
2449 Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[]);
2450
2460 Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[]);
2461
2468 Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg);
2469
2478 Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2479
2486 Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2487
2494 Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2495
2502 Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2503
2508 Z3_ast Z3_API Z3_mk_abs(Z3_context c, Z3_ast arg);
2509
2516 Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2);
2517
2524 Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2);
2525
2532 Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2);
2533
2540 Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2);
2541
2550 Z3_ast Z3_API Z3_mk_divides(Z3_context c, Z3_ast t1, Z3_ast t2);
2551
2568 Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1);
2569
2580 Z3_ast Z3_API Z3_mk_real2int(Z3_context c, Z3_ast t1);
2581
2589 Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1);
2591
2600 Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1);
2601
2608 Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1);
2609
2616 Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1);
2617
2624 Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2);
2625
2632 Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2);
2633
2640 Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2);
2641
2648 Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2);
2649
2656 Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2);
2657
2664 Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2);
2665
2672 Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1);
2673
2680 Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2);
2681
2688 Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2);
2689
2696 Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2);
2697
2708 Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2);
2709
2724 Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2);
2725
2736 Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2);
2737
2751 Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2);
2752
2763 Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2);
2764
2771 Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2);
2772
2787 Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2);
2788
2795 Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2);
2796
2803 Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2);
2804
2811 Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2);
2812
2819 Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2);
2820
2827 Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2);
2828
2835 Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2);
2836
2846 Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2);
2847
2855 Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1);
2856
2865 Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1);
2866
2875 Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1);
2876
2883 Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1);
2884
2892 Z3_ast Z3_API Z3_mk_bit2bool(Z3_context c, unsigned i, Z3_ast t1);
2893
2907 Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2);
2908
2922 Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2);
2923
2938 Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2);
2939
2946 Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1);
2947
2954 Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1);
2955
2962 Z3_ast Z3_API Z3_mk_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2);
2963
2970 Z3_ast Z3_API Z3_mk_ext_rotate_right(Z3_context c, Z3_ast t1, Z3_ast t2);
2971
2981 Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1);
2982
2994 Z3_ast Z3_API Z3_mk_bv2int(Z3_context c,Z3_ast t1, bool is_signed);
2995
3004 Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);
3005
3014 Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2);
3015
3024 Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2);
3025
3034 Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);
3035
3044 Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2);
3045
3054 Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1);
3055
3064 Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);
3065
3074 Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2);
3076
3091 Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i);
3092
3093
3094
3101 Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs);
3102
3103
3119 Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v);
3120
3121
3127 Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs, Z3_ast v);
3128
3140 Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v);
3141
3154 Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const* args);
3155
3165 Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array);
3166
3173 Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f);
3174
3175
3177
3184 Z3_sort Z3_API Z3_mk_set_sort(Z3_context c, Z3_sort ty);
3185
3190 Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain);
3191
3196 Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain);
3197
3204 Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem);
3205
3212 Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem);
3213
3218 Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[]);
3219
3224 Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[]);
3225
3230 Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2);
3231
3236 Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg);
3237
3244 Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set);
3245
3250 Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2);
3251
3258
3259 Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2);
3261
3268 Z3_sort Z3_API Z3_mk_finite_set_sort(Z3_context c, Z3_sort elem_sort);
3269
3274 bool Z3_API Z3_is_finite_set_sort(Z3_context c, Z3_sort s);
3275
3280 Z3_sort Z3_API Z3_get_finite_set_sort_basis(Z3_context c, Z3_sort s);
3281
3286 Z3_ast Z3_API Z3_mk_finite_set_empty(Z3_context c, Z3_sort set_sort);
3287
3292 Z3_ast Z3_API Z3_mk_finite_set_singleton(Z3_context c, Z3_ast elem);
3293
3298 Z3_ast Z3_API Z3_mk_finite_set_union(Z3_context c, Z3_ast s1, Z3_ast s2);
3299
3304 Z3_ast Z3_API Z3_mk_finite_set_intersect(Z3_context c, Z3_ast s1, Z3_ast s2);
3305
3310 Z3_ast Z3_API Z3_mk_finite_set_difference(Z3_context c, Z3_ast s1, Z3_ast s2);
3311
3316 Z3_ast Z3_API Z3_mk_finite_set_member(Z3_context c, Z3_ast elem, Z3_ast set);
3317
3322 Z3_ast Z3_API Z3_mk_finite_set_size(Z3_context c, Z3_ast set);
3323
3328 Z3_ast Z3_API Z3_mk_finite_set_subset(Z3_context c, Z3_ast s1, Z3_ast s2);
3329
3334 Z3_ast Z3_API Z3_mk_finite_set_map(Z3_context c, Z3_ast f, Z3_ast set);
3335
3340 Z3_ast Z3_API Z3_mk_finite_set_filter(Z3_context c, Z3_ast f, Z3_ast set);
3341
3346 Z3_ast Z3_API Z3_mk_finite_set_range(Z3_context c, Z3_ast low, Z3_ast high);
3348
3363 Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty);
3364
3365#if 0
3377
3378 Z3_ast Z3_mk_mpz_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], Z3_sort s);
3379
3394
3395 Z3_ast Z3_mk_mpq_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], unsigned d, unsigned const dens[]);
3396#endif
3397
3413 Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den);
3414
3420
3421 Z3_ast Z3_API Z3_mk_real_int64(Z3_context c, int64_t num, int64_t den);
3422
3432 Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty);
3433
3443 Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty);
3444
3454 Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty);
3455
3465 Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty);
3466
3472 Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, bool const* bits);
3473
3475
3478
3483 Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s);
3484
3489 bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s);
3490
3495 Z3_sort Z3_API Z3_get_seq_sort_basis(Z3_context c, Z3_sort s);
3496
3501 Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq);
3502
3507 bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s);
3508
3513 Z3_sort Z3_API Z3_get_re_sort_basis(Z3_context c, Z3_sort s);
3514
3523 Z3_sort Z3_API Z3_mk_string_sort(Z3_context c);
3524
3533 Z3_sort Z3_API Z3_mk_char_sort(Z3_context c);
3534
3539 bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s);
3540
3545 bool Z3_API Z3_is_char_sort(Z3_context c, Z3_sort s);
3546
3555 Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s);
3556
3564 Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned len, Z3_string s);
3565
3572 Z3_ast Z3_API Z3_mk_u32string(Z3_context c, unsigned len, unsigned const chars[]);
3573
3578 bool Z3_API Z3_is_string(Z3_context c, Z3_ast s);
3579
3587 Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s);
3588
3597 Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length);
3598
3605 unsigned Z3_API Z3_get_string_length(Z3_context c, Z3_ast s);
3606
3615 void Z3_API Z3_get_string_contents(Z3_context c, Z3_ast s, unsigned length, unsigned contents[]);
3616
3623 Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq);
3624
3629 Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a);
3630
3637 Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[]);
3638
3645 Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s);
3646
3653 Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s);
3654
3661 Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee);
3662
3663
3670 Z3_ast Z3_API Z3_mk_str_lt(Z3_context c, Z3_ast prefix, Z3_ast s);
3671
3678 Z3_ast Z3_API Z3_mk_str_le(Z3_context c, Z3_ast prefix, Z3_ast s);
3679
3684 Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length);
3685
3690 Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst);
3691
3696 Z3_ast Z3_API Z3_mk_seq_replace_all(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst);
3697
3702 Z3_ast Z3_API Z3_mk_seq_replace_re(Z3_context c, Z3_ast s, Z3_ast re, Z3_ast dst);
3703
3708 Z3_ast Z3_API Z3_mk_seq_replace_re_all(Z3_context c, Z3_ast s, Z3_ast re, Z3_ast dst);
3709
3715 Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index);
3716
3722 Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index);
3723
3729 Z3_ast Z3_API Z3_mk_seq_power(Z3_context c, Z3_ast s, Z3_ast n);
3730
3735 Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s);
3736
3737
3744 Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);
3745
3750 Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast s, Z3_ast substr);
3751
3755 Z3_ast Z3_API Z3_mk_seq_map(Z3_context c, Z3_ast f, Z3_ast s);
3756
3760 Z3_ast Z3_API Z3_mk_seq_mapi(Z3_context c, Z3_ast f, Z3_ast i, Z3_ast s);
3761
3765 Z3_ast Z3_API Z3_mk_seq_foldl(Z3_context c, Z3_ast f, Z3_ast a, Z3_ast s);
3766
3770 Z3_ast Z3_API Z3_mk_seq_foldli(Z3_context c, Z3_ast f, Z3_ast i, Z3_ast a, Z3_ast s);
3771
3776 Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s);
3777
3778
3783 Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s);
3784
3785
3790 Z3_ast Z3_API Z3_mk_string_to_code(Z3_context c, Z3_ast a);
3791
3796 Z3_ast Z3_API Z3_mk_string_from_code(Z3_context c, Z3_ast a);
3797
3802 Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s);
3803
3808 Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s);
3809
3814 Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq);
3815
3820 Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re);
3821
3826 Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re);
3827
3832 Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re);
3833
3838 Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re);
3839
3846 Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[]);
3847
3854 Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[]);
3855
3856
3861 Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi);
3862
3863
3868 Z3_ast Z3_API Z3_mk_re_allchar(Z3_context c, Z3_sort regex_sort);
3869
3877 Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi);
3878
3883 Z3_ast Z3_API Z3_mk_re_power(Z3_context c, Z3_ast re, unsigned n);
3884
3891 Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[]);
3892
3897 Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re);
3898
3903 Z3_ast Z3_API Z3_mk_re_diff(Z3_context c, Z3_ast re1, Z3_ast re2);
3904
3911 Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re);
3912
3913
3920 Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re);
3921
3922
3926 Z3_ast Z3_API Z3_mk_char(Z3_context c, unsigned ch);
3927
3932 Z3_ast Z3_API Z3_mk_char_le(Z3_context c, Z3_ast ch1, Z3_ast ch2);
3933
3938 Z3_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch);
3939
3944 Z3_ast Z3_API Z3_mk_char_to_bv(Z3_context c, Z3_ast ch);
3945
3950 Z3_ast Z3_API Z3_mk_char_from_bv(Z3_context c, Z3_ast bv);
3951
3956 Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch);
3957
3959
3960
3968 Z3_func_decl Z3_API Z3_mk_linear_order(Z3_context c, Z3_sort a, unsigned id);
3969
3974 Z3_func_decl Z3_API Z3_mk_partial_order(Z3_context c, Z3_sort a, unsigned id);
3975
3980 Z3_func_decl Z3_API Z3_mk_piecewise_linear_order(Z3_context c, Z3_sort a, unsigned id);
3981
3986 Z3_func_decl Z3_API Z3_mk_tree_order(Z3_context c, Z3_sort a, unsigned id);
3987
3996 Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f);
3997
3999
4021 Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[]);
4022
4054 Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty);
4055
4078 Z3_ast Z3_API Z3_mk_forall(Z3_context c, unsigned weight,
4079 unsigned num_patterns, Z3_pattern const patterns[],
4080 unsigned num_decls, Z3_sort const sorts[],
4081 Z3_symbol const decl_names[],
4082 Z3_ast body);
4083
4093 Z3_ast Z3_API Z3_mk_exists(Z3_context c, unsigned weight,
4094 unsigned num_patterns, Z3_pattern const patterns[],
4095 unsigned num_decls, Z3_sort const sorts[],
4096 Z3_symbol const decl_names[],
4097 Z3_ast body);
4098
4119 Z3_ast Z3_API Z3_mk_quantifier(
4120 Z3_context c,
4121 bool is_forall,
4122 unsigned weight,
4123 unsigned num_patterns, Z3_pattern const patterns[],
4124 unsigned num_decls, Z3_sort const sorts[],
4125 Z3_symbol const decl_names[],
4126 Z3_ast body);
4127
4128
4152 Z3_ast Z3_API Z3_mk_quantifier_ex(
4153 Z3_context c,
4154 bool is_forall,
4155 unsigned weight,
4156 Z3_symbol quantifier_id,
4157 Z3_symbol skolem_id,
4158 unsigned num_patterns, Z3_pattern const patterns[],
4159 unsigned num_no_patterns, Z3_ast const no_patterns[],
4160 unsigned num_decls, Z3_sort const sorts[],
4161 Z3_symbol const decl_names[],
4162 Z3_ast body);
4163
4181 Z3_ast Z3_API Z3_mk_forall_const(
4182 Z3_context c,
4183 unsigned weight,
4184 unsigned num_bound,
4185 Z3_app const bound[],
4186 unsigned num_patterns,
4187 Z3_pattern const patterns[],
4188 Z3_ast body
4189 );
4190
4210 Z3_ast Z3_API Z3_mk_exists_const(
4211 Z3_context c,
4212 unsigned weight,
4213 unsigned num_bound,
4214 Z3_app const bound[],
4215 unsigned num_patterns,
4216 Z3_pattern const patterns[],
4217 Z3_ast body
4218 );
4219
4225 Z3_ast Z3_API Z3_mk_quantifier_const(
4226 Z3_context c,
4227 bool is_forall,
4228 unsigned weight,
4229 unsigned num_bound, Z3_app const bound[],
4230 unsigned num_patterns, Z3_pattern const patterns[],
4231 Z3_ast body
4232 );
4233
4239 Z3_ast Z3_API Z3_mk_quantifier_const_ex(
4240 Z3_context c,
4241 bool is_forall,
4242 unsigned weight,
4243 Z3_symbol quantifier_id,
4244 Z3_symbol skolem_id,
4245 unsigned num_bound, Z3_app const bound[],
4246 unsigned num_patterns, Z3_pattern const patterns[],
4247 unsigned num_no_patterns, Z3_ast const no_patterns[],
4248 Z3_ast body
4249 );
4250
4273 Z3_ast Z3_API Z3_mk_lambda(Z3_context c,
4274 unsigned num_decls, Z3_sort const sorts[],
4275 Z3_symbol const decl_names[],
4276 Z3_ast body);
4277
4292 Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c,
4293 unsigned num_bound, Z3_app const bound[],
4294 Z3_ast body);
4295
4296
4298
4307 Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s);
4308
4317 int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s);
4318
4331 Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s);
4332
4337 Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d);
4338
4343 unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s);
4344
4349 Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s);
4350
4355 bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2);
4356
4363 Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t);
4364
4374 unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t);
4375
4381 bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r);
4382
4391 unsigned Z3_API Z3_get_array_arity(Z3_context c, Z3_sort s);
4392
4404 Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t);
4405
4406
4418 Z3_sort Z3_API Z3_get_array_sort_domain_n(Z3_context c, Z3_sort t, unsigned idx);
4419
4429 Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t);
4430
4441 Z3_func_decl Z3_API Z3_get_tuple_sort_mk_decl(Z3_context c, Z3_sort t);
4442
4452 unsigned Z3_API Z3_get_tuple_sort_num_fields(Z3_context c, Z3_sort t);
4453
4465 Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t, unsigned i);
4466
4471 bool Z3_API Z3_is_recursive_datatype_sort(Z3_context c, Z3_sort s);
4472
4483 unsigned Z3_API Z3_get_datatype_sort_num_constructors(
4484 Z3_context c, Z3_sort t);
4485
4497 Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(
4498 Z3_context c, Z3_sort t, unsigned idx);
4499
4511 Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(
4512 Z3_context c, Z3_sort t, unsigned idx);
4513
4526 Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c,
4527 Z3_sort t,
4528 unsigned idx_c,
4529 unsigned idx_a);
4530
4549 Z3_ast Z3_API Z3_datatype_update_field(Z3_context c, Z3_func_decl field_access,
4550 Z3_ast t, Z3_ast value);
4551
4560 unsigned Z3_API Z3_get_relation_arity(Z3_context c, Z3_sort s);
4561
4571 Z3_sort Z3_API Z3_get_relation_column(Z3_context c, Z3_sort s, unsigned col);
4572
4579 Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args,
4580 Z3_ast const args[], unsigned k);
4581
4588 Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args,
4589 Z3_ast const args[], unsigned k);
4590
4597 Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args,
4598 Z3_ast const args[], int const coeffs[],
4599 int k);
4600
4607 Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args,
4608 Z3_ast const args[], int const coeffs[],
4609 int k);
4610
4617 Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args,
4618 Z3_ast const args[], int const coeffs[],
4619 int k);
4620
4625 Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f);
4626
4631 bool Z3_API Z3_is_eq_func_decl(Z3_context c, Z3_func_decl f1, Z3_func_decl f2);
4632
4637 unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f);
4638
4643 Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d);
4644
4649 Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d);
4650
4657 unsigned Z3_API Z3_get_domain_size(Z3_context c, Z3_func_decl d);
4658
4665 unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d);
4666
4675 Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i);
4676
4684 Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d);
4685
4690 unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d);
4691
4700 Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx);
4701
4708 int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4709
4716 double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4717
4724 Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4725
4732 Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4733
4740 Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4741
4748 Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4749
4756 Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx);
4757
4762 Z3_ast Z3_API Z3_app_to_ast(Z3_context c, Z3_app a);
4763
4768 Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a);
4769
4777 unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a);
4778
4787 Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i);
4788
4793 bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2);
4794
4805 unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t);
4806
4814 unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a);
4815
4822 Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a);
4823
4828 bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t);
4829
4834 Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a);
4835
4840 Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a);
4841
4844 bool Z3_API Z3_is_app(Z3_context c, Z3_ast a);
4845
4848 bool Z3_API Z3_is_ground(Z3_context c, Z3_ast a);
4849
4852 unsigned Z3_API Z3_get_depth(Z3_context c, Z3_ast a);
4853
4856 bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a);
4857
4862 bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a);
4863
4870 Z3_app Z3_API Z3_to_app(Z3_context c, Z3_ast a);
4871
4878 Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a);
4879
4886 Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a);
4887
4895 Z3_string Z3_API Z3_get_numeral_binary_string(Z3_context c, Z3_ast a);
4896
4904 Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision);
4905
4912 double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a);
4913
4920 Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a);
4921
4928 Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a);
4929
4945 bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, int64_t* num, int64_t* den);
4946
4956 bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int* i);
4957
4967 bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned* u);
4968
4978 bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t* u);
4979
4989 bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t* i);
4990
5000 bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, int64_t* num, int64_t* den);
5001
5010 Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision);
5011
5020 Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision);
5021
5026 Z3_ast Z3_API Z3_pattern_to_ast(Z3_context c, Z3_pattern p);
5027
5032 unsigned Z3_API Z3_get_pattern_num_terms(Z3_context c, Z3_pattern p);
5033
5038 Z3_ast Z3_API Z3_get_pattern(Z3_context c, Z3_pattern p, unsigned idx);
5039
5046 unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a);
5047
5052 bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a);
5053
5059 bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a);
5060
5067 bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a);
5068
5075 unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a);
5076
5083 Z3_symbol Z3_API Z3_get_quantifier_skolem_id(Z3_context c, Z3_ast a);
5084
5091 Z3_symbol Z3_API Z3_get_quantifier_id(Z3_context c, Z3_ast a);
5092
5099 unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a);
5100
5107 Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i);
5108
5115 unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a);
5116
5123 Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i);
5124
5131 unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a);
5132
5139 Z3_symbol Z3_API Z3_get_quantifier_bound_name(Z3_context c, Z3_ast a, unsigned i);
5140
5147 Z3_sort Z3_API Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, unsigned i);
5148
5155 Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a);
5156
5168 Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a);
5169
5182 Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p);
5183
5191 Z3_string Z3_API Z3_simplify_get_help(Z3_context c);
5192
5200 Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c);
5202
5212 Z3_ast Z3_API Z3_update_term(Z3_context c, Z3_ast a, unsigned num_args, Z3_ast const args[]);
5213
5220 Z3_ast Z3_API Z3_substitute(Z3_context c,
5221 Z3_ast a,
5222 unsigned num_exprs,
5223 Z3_ast const from[],
5224 Z3_ast const to[]);
5225
5232 Z3_ast Z3_API Z3_substitute_vars(Z3_context c,
5233 Z3_ast a,
5234 unsigned num_exprs,
5235 Z3_ast const to[]);
5236
5244 Z3_ast Z3_API Z3_substitute_funs(Z3_context c,
5245 Z3_ast a,
5246 unsigned num_funs,
5247 Z3_func_decl const from[],
5248 Z3_ast const to[]);
5249
5256 Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target);
5258
5261
5266 Z3_model Z3_API Z3_mk_model(Z3_context c);
5267
5272 void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m);
5273
5278 void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m);
5279
5302 bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v);
5303
5312 Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a);
5313
5318 bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a);
5319
5331 Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f);
5332
5339 unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m);
5340
5350 Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i);
5351
5361 unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m);
5362
5371 Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i);
5372
5384 unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m);
5385
5395 Z3_sort Z3_API Z3_model_get_sort(Z3_context c, Z3_model m, unsigned i);
5396
5404 Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s);
5405
5414 Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst);
5415
5426 bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a);
5427
5434 Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a);
5435
5446 Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value);
5447
5452 void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a);
5453
5458 void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f);
5459
5464 void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f);
5465
5476 unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f);
5477
5487 Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i);
5488
5496 Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f);
5497
5505 void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value);
5506
5511 unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f);
5512
5526 void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value);
5527
5532 void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e);
5533
5538 void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e);
5539
5549 Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e);
5550
5558 unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e);
5559
5569 Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i);
5571
5581 bool Z3_API Z3_open_log(Z3_string filename);
5582
5594 void Z3_API Z3_append_log(Z3_string string);
5595
5603 void Z3_API Z3_close_log(void);
5604
5612 void Z3_API Z3_toggle_warning_messages(bool enabled);
5614
5633 void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode);
5634
5646 Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a);
5647
5650 Z3_string Z3_API Z3_pattern_to_string(Z3_context c, Z3_pattern p);
5651
5654 Z3_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s);
5655
5658 Z3_string Z3_API Z3_func_decl_to_string(Z3_context c, Z3_func_decl d);
5659
5668 Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m);
5669
5687 Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c,
5688 Z3_string name,
5689 Z3_string logic,
5690 Z3_string status,
5691 Z3_string attributes,
5692 unsigned num_assumptions,
5693 Z3_ast const assumptions[],
5694 Z3_ast formula);
5695
5697
5707 Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c,
5708 Z3_string str,
5709 unsigned num_sorts,
5710 Z3_symbol const sort_names[],
5711 Z3_sort const sorts[],
5712 unsigned num_decls,
5713 Z3_symbol const decl_names[],
5714 Z3_func_decl const decls[]);
5715
5720 Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c,
5721 Z3_string file_name,
5722 unsigned num_sorts,
5723 Z3_symbol const sort_names[],
5724 Z3_sort const sorts[],
5725 unsigned num_decls,
5726 Z3_symbol const decl_names[],
5727 Z3_func_decl const decls[]);
5728
5729
5737
5738 Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context c, Z3_string str);
5739
5740
5750 Z3_parser_context Z3_API Z3_mk_parser_context(Z3_context c);
5751
5756 void Z3_API Z3_parser_context_inc_ref(Z3_context c, Z3_parser_context pc);
5757
5762 void Z3_API Z3_parser_context_dec_ref(Z3_context c, Z3_parser_context pc);
5763
5768 void Z3_API Z3_parser_context_add_sort(Z3_context c, Z3_parser_context pc, Z3_sort s);
5769
5774 void Z3_API Z3_parser_context_add_decl(Z3_context c, Z3_parser_context pc, Z3_func_decl f);
5775
5780 Z3_ast_vector Z3_API Z3_parser_context_from_string(Z3_context c, Z3_parser_context pc, Z3_string s);
5781
5782
5784
5796 Z3_error_code Z3_API Z3_get_error_code(Z3_context c);
5797
5823 void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h);
5824
5829 void Z3_API Z3_set_error(Z3_context c, Z3_error_code e);
5830
5835 Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err);
5836
5838
5841
5848 void Z3_API Z3_get_version(unsigned * major, unsigned * minor, unsigned * build_number, unsigned * revision_number);
5849
5856 Z3_string Z3_API Z3_get_full_version(void);
5857
5865 void Z3_API Z3_enable_trace(Z3_string tag);
5866
5874 void Z3_API Z3_disable_trace(Z3_string tag);
5875
5885 void Z3_API Z3_reset_memory(void);
5886
5894 void Z3_API Z3_finalize_memory(void);
5896
5915 Z3_goal Z3_API Z3_mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs);
5916
5921 void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g);
5922
5927 void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g);
5928
5935 Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g);
5936
5948 void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a);
5949
5954 bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g);
5955
5960 unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g);
5961
5966 void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g);
5967
5972 unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g);
5973
5980 Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx);
5981
5986 unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g);
5987
5992 bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g);
5993
5998 bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g);
5999
6004 Z3_goal Z3_API Z3_goal_translate(Z3_context source, Z3_goal g, Z3_context target);
6005
6017 Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m);
6018
6023 Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g);
6024
6034 Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names);
6035
6037
6048 Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name);
6049
6054 void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t);
6055
6060 void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g);
6061
6071 Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name);
6072
6077 void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p);
6078
6083 void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p);
6084
6090 Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2);
6091
6097 Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2);
6098
6103 Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[]);
6104
6110 Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2);
6111
6117 Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms);
6118
6124 Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t);
6125
6131 Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2);
6132
6138 Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max);
6139
6144 Z3_tactic Z3_API Z3_tactic_skip(Z3_context c);
6145
6150 Z3_tactic Z3_API Z3_tactic_fail(Z3_context c);
6151
6156 Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p);
6157
6163 Z3_tactic Z3_API Z3_tactic_fail_if_not_decided(Z3_context c);
6164
6169 Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p);
6170
6171
6180 Z3_simplifier Z3_API Z3_mk_simplifier(Z3_context c, Z3_string name);
6181
6186 void Z3_API Z3_simplifier_inc_ref(Z3_context c, Z3_simplifier t);
6187
6192 void Z3_API Z3_simplifier_dec_ref(Z3_context c, Z3_simplifier g);
6193
6198 Z3_solver Z3_API Z3_solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier);
6199
6205 Z3_simplifier Z3_API Z3_simplifier_and_then(Z3_context c, Z3_simplifier t1, Z3_simplifier t2);
6206
6211 Z3_simplifier Z3_API Z3_simplifier_using_params(Z3_context c, Z3_simplifier t, Z3_params p);
6212
6213
6220 unsigned Z3_API Z3_get_num_simplifiers(Z3_context c);
6221
6230 Z3_string Z3_API Z3_get_simplifier_name(Z3_context c, unsigned i);
6231
6236 Z3_string Z3_API Z3_simplifier_get_help(Z3_context c, Z3_simplifier t);
6237
6242 Z3_param_descrs Z3_API Z3_simplifier_get_param_descrs(Z3_context c, Z3_simplifier t);
6243
6248 Z3_string Z3_API Z3_simplifier_get_descr(Z3_context c, Z3_string name);
6249
6250
6255 Z3_probe Z3_API Z3_probe_const(Z3_context x, double val);
6256
6263 Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2);
6264
6271 Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2);
6272
6279 Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2);
6280
6287 Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2);
6288
6295 Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2);
6296
6303 Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2);
6304
6311 Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2);
6312
6319 Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p);
6320
6327 unsigned Z3_API Z3_get_num_tactics(Z3_context c);
6328
6337 Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i);
6338
6345 unsigned Z3_API Z3_get_num_probes(Z3_context c);
6346
6355 Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i);
6356
6361 Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t);
6362
6367 Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t);
6368
6373 Z3_string Z3_API Z3_tactic_get_descr(Z3_context c, Z3_string name);
6374
6379 Z3_string Z3_API Z3_probe_get_descr(Z3_context c, Z3_string name);
6380
6386 double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g);
6387
6394 Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g);
6395
6402 Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p);
6403
6408 void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r);
6409
6414 void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r);
6415
6420 Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r);
6421
6428 unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r);
6429
6438 Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i);
6439
6441
6483 Z3_solver Z3_API Z3_mk_solver(Z3_context c);
6484
6513 Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c);
6514
6527 Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic);
6528
6542 Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t);
6543
6548 Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target);
6549
6562 void Z3_API Z3_solver_import_model_converter(Z3_context ctx, Z3_solver src, Z3_solver dst);
6563
6571 Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s);
6572
6580 Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s);
6581
6589 void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p);
6590
6595 void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s);
6596
6601 void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s);
6602
6612 void Z3_API Z3_solver_interrupt(Z3_context c, Z3_solver s);
6613
6623 void Z3_API Z3_solver_push(Z3_context c, Z3_solver s);
6624
6634 void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n);
6635
6643 void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s);
6644
6652 unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s);
6653
6664 void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a);
6665
6682 void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p);
6683
6691 void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name);
6692
6700 void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string str);
6701
6706 Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s);
6707
6712 Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s);
6713
6719 Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s);
6720
6725 Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s);
6726
6732 void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[]);
6733
6741 Z3_ast Z3_API Z3_solver_congruence_root(Z3_context c, Z3_solver s, Z3_ast a);
6742
6743
6749 Z3_ast Z3_API Z3_solver_congruence_next(Z3_context c, Z3_solver s, Z3_ast a);
6750
6756 Z3_ast Z3_API Z3_solver_congruence_explain(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast b);
6757
6765 void Z3_API Z3_solver_solve_for(Z3_context c, Z3_solver s, Z3_ast_vector variables, Z3_ast_vector terms, Z3_ast_vector guards);
6766
6779 void Z3_API Z3_solver_register_on_clause(
6780 Z3_context c,
6781 Z3_solver s,
6782 void* user_context,
6783 Z3_on_clause_eh on_clause_eh);
6784
6796
6797 void Z3_API Z3_solver_propagate_init(
6798 Z3_context c,
6799 Z3_solver s,
6800 void* user_context,
6801 Z3_push_eh push_eh,
6802 Z3_pop_eh pop_eh,
6803 Z3_fresh_eh fresh_eh);
6804
6812
6813 void Z3_API Z3_solver_propagate_fixed(Z3_context c, Z3_solver s, Z3_fixed_eh fixed_eh);
6814
6829 void Z3_API Z3_solver_propagate_final(Z3_context c, Z3_solver s, Z3_final_eh final_eh);
6830
6835 void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh);
6836
6841 void Z3_API Z3_solver_propagate_diseq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh);
6842
6848 void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh);
6849
6855 void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh);
6856
6857
6865
6866 void Z3_API Z3_solver_propagate_on_binding(Z3_context c, Z3_solver s, Z3_on_binding_eh on_binding_eh);
6874 bool Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase);
6875
6885 Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range);
6886
6892
6893 void Z3_API Z3_solver_propagate_register(Z3_context c, Z3_solver s, Z3_ast e);
6894
6902 void Z3_API Z3_solver_propagate_register_cb(Z3_context c, Z3_solver_callback cb, Z3_ast e);
6903
6925
6926 bool 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);
6927
6928
6935
6936 void Z3_API Z3_solver_set_initial_value(Z3_context c, Z3_solver s, Z3_ast v, Z3_ast val);
6937
6938
6956 Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s);
6957
6968 Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s,
6969 unsigned num_assumptions, Z3_ast const assumptions[]);
6970
6988 Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c,
6989 Z3_solver s,
6990 unsigned num_terms,
6991 Z3_ast const terms[],
6992 unsigned class_ids[]);
6993
6998
6999 Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c,
7000 Z3_solver s,
7001 Z3_ast_vector assumptions,
7002 Z3_ast_vector variables,
7003 Z3_ast_vector consequences);
7004
7005
7022
7023 Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level);
7024
7032 Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s);
7033
7042 Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s);
7043
7054 Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s);
7055
7061 Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s);
7062
7069 Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s);
7070
7078 Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s);
7079
7085 Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names);
7086
7088
7091
7096 Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s);
7097
7102 void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s);
7103
7108 void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s);
7109
7114 unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s);
7115
7122 Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx);
7123
7130 bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx);
7131
7138 bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx);
7139
7146 unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx);
7147
7154 double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx);
7155
7160 uint64_t Z3_API Z3_get_estimated_alloc_size(void);
7161
7163
7164#ifdef __cplusplus
7165}
7166#endif // __cplusplus
7167
Z3_mk_exists_const
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_solver_propagate_on_binding
void Z3_API Z3_solver_propagate_on_binding(Z3_context c, Z3_solver s, Z3_on_binding_eh on_binding_eh)
register a callback when the solver instantiates a quantifier. If the callback returns false,...
Z3_mk_pbeq
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_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
Definition z3_api.h:1371
Z3_ast_kind
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition z3_api.h:143
Z3_model_get_const_interp
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_mk_int_sort
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
Z3_simplifier_and_then
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_lt
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_mk_array_sort_n
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_mk_bvxnor
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
Z3_mk_quantifier
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_get_error_msg
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)
Return a string describing the given error code.
Z3_open_log
bool Z3_API Z3_open_log(Z3_string filename)
Log interaction to a file.
Z3_mk_seq_replace_all
Z3_ast Z3_API Z3_mk_seq_replace_all(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst)
Replace all occurrences of src with dst in s.
Z3_get_decl_parameter_kind
Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx)
Return the parameter type associated with a declaration.
Z3_is_seq_sort
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
Z3_mk_bvnor
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
Z3_get_denominator
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_not
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_get_decl_kind
Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d)
Return declaration kind corresponding to declaration.
Z3_solver_assert_and_track
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_func_interp_get_else
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_mk_char_to_bv
Z3_ast Z3_API Z3_mk_char_to_bv(Z3_context c, Z3_ast ch)
Create a bit-vector (code point) from character.
Z3_solver_propagate_diseq
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_mk_bvsge
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_using_params
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_mk_const_array
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
Z3_simplifier_inc_ref
void Z3_API Z3_simplifier_inc_ref(Z3_context c, Z3_simplifier t)
Increment the reference counter of the given simplifier.
Z3_probe_eq
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_mk_char_sort
Z3_sort Z3_API Z3_mk_char_sort(Z3_context c)
Create a sort for unicode characters.
Z3_mk_unsigned_int
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_mk_re_option
Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re)
Create the regular language [re].
Z3_mk_bvsle
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than or equal to.
Z3_query_constructor
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_get_app_decl
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_mk_context
Z3_context Z3_API Z3_mk_context(Z3_config c)
Create a context using the given configuration.
Z3_del_context
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
Z3_substitute
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_mk_mul
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_get_decl_func_decl_parameter
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_goal_prec
Z3 custom error handler (See Z3_set_error_handler).
Definition z3_api.h:1437
Z3_mk_seq_replace
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_param_descrs_to_string
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_mk_zero_ext
Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1)
Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i,...
Z3_solver_set_params
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_mk_set_intersect
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_mk_str_le
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_mk_params
Z3_params Z3_API Z3_mk_params(Z3_context c)
Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many comp...
Z3_get_decl_num_parameters
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_mk_set_subset
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
Z3_simplify
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_mk_int
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_solver_get_consequences
Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences)
retrieve consequences from solver that determine values of the supplied function symbols.
Z3_get_string_contents
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_mk_bvule
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
Z3_mk_full_set
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
Z3_param_descrs_get_kind
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_mk_ff_neg
Z3_ast Z3_API Z3_mk_ff_neg(Z3_context c, Z3_ast a)
Additive inverse in a prime field.
Z3_mk_char_le
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.
Z3_get_numeral_int64
bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int64_t int....
Z3_add_rec_def
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_solver_get_param_descrs
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)
Return the parameter description set for the given solver object.
Z3_eval_smtlib2_string
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...
Z3_toggle_warning_messages
void Z3_API Z3_toggle_warning_messages(bool enabled)
Enable/disable printing warning messages to the console.
Z3_mk_true
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
Z3_mk_set_union
Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the union of a list of sets.
Z3_mk_finite_set_empty
Z3_ast Z3_API Z3_mk_finite_set_empty(Z3_context c, Z3_sort set_sort)
Create an empty finite set of the given sort.
Z3_apply_result_inc_ref
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_add_func_interp
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_mk_bvsdiv_no_overflow
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
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition z3_api.h:989
Z3_parser_context_add_decl
void Z3_API Z3_parser_context_add_decl(Z3_context c, Z3_parser_context pc, Z3_func_decl f)
Add a function declaration.
Z3_get_arity
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.
Z3_mk_bvxor
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_stats_to_string
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
Z3_mk_real_sort
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
Z3_mk_string_from_code
Z3_ast Z3_API Z3_mk_string_from_code(Z3_context c, Z3_ast a)
Code to string conversion.
Z3_mk_le
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_get_tuple_sort_num_fields
unsigned Z3_API Z3_get_tuple_sort_num_fields(Z3_context c, Z3_sort t)
Return the number of fields of the given tuple sort.
Z3_global_param_get
bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value)
Get a global (or module) parameter.
Z3_mk_ff_bitsum
Z3_ast Z3_API Z3_mk_ff_bitsum(Z3_context c, unsigned n, Z3_ast const args[])
Weighted sum a0 + 2*a1 + 4*a2 + ... (does not constrain arguments to bits).
Z3_is_finite_set_sort
bool Z3_API Z3_is_finite_set_sort(Z3_context c, Z3_sort s)
Check if a sort is a finite set sort.
Z3_simplifier_get_help
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.
Z3_goal_inconsistent
bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.
Z3_mk_lambda_const
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_par_and_then
Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1....
Z3_solver_dec_ref
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
Z3_mk_bvslt
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
Z3_model_get_func_decl
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_mk_seq_length
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.
Z3_mk_numeral
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
Z3_mk_finite_set_difference
Z3_ast Z3_API Z3_mk_finite_set_difference(Z3_context c, Z3_ast s1, Z3_ast s2)
Create the set difference of two finite sets.
Z3_func_entry_get_num_args
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_simplify_ex
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
Z3_get_decl_symbol_parameter
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_get_quantifier_skolem_id
Z3_symbol Z3_API Z3_get_quantifier_skolem_id(Z3_context c, Z3_ast a)
Obtain skolem id of quantifier.
Z3_get_seq_sort_basis
Z3_sort Z3_API Z3_get_seq_sort_basis(Z3_context c, Z3_sort s)
Retrieve basis sort for sequence sort.
Z3_solver_from_string
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string str)
load solver assertions from a string.
Z3_get_numerator
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_mk_unary_minus
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
Z3_is_char_sort
bool Z3_API Z3_is_char_sort(Z3_context c, Z3_sort s)
Check if s is a character sort.
Z3_probe_ge
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_mk_and
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
Z3_mk_finite_set_subset
Z3_ast Z3_API Z3_mk_finite_set_subset(Z3_context c, Z3_ast s1, Z3_ast s2)
Check if one finite set is a subset of another.
Z3_simplifier_dec_ref
void Z3_API Z3_simplifier_dec_ref(Z3_context c, Z3_simplifier g)
Decrement the reference counter of the given simplifier.
Z3_interrupt
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers,...
Z3_mk_str_to_int
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.
Z3_goal_assert
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_param_descrs_get_name
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_func_decl_to_string
Z3_string Z3_API Z3_func_decl_to_string(Z3_context c, Z3_func_decl d)
Z3_mk_re_allchar
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_mk_polymorphic_datatype
Z3_sort Z3_API Z3_mk_polymorphic_datatype(Z3_context c, Z3_symbol name, unsigned num_parameters, Z3_sort parameters[], unsigned num_constructors, Z3_constructor constructors[])
Create a parametric datatype with explicit type parameters.
Z3_func_entry_get_value
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
Z3_is_quantifier_exists
bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.
Z3_mk_uninterpreted_sort
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
Z3_get_numeral_small
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_mk_false
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
Z3_mk_datatype
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_solver_check
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_mk_rotate_right
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_get_pattern
Z3_ast Z3_API Z3_get_pattern(Z3_context c, Z3_pattern p, unsigned idx)
Return i'th ast in pattern.
Z3_mk_bvmul
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_mk_seq_at
Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the unit sequence positioned at position index. The sequence is empty if the index is...
Z3_finalize_memory
void Z3_API Z3_finalize_memory(void)
Destroy all allocated resources.
Z3_goal_convert_model
Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m)
Convert a model of the formulas of a goal to a model of an original goal. The model may be null,...
Z3_del_constructor
void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr)
Reclaim memory allocated to constructor.
Z3_mk_bvsgt
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_ast_to_string
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
Z3_mk_re_complement
Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re)
Create the complement of the regular language re.
Z3_mk_context_rc
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_solver_get_assertions
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_get_full_version
Z3_string Z3_API Z3_get_full_version(void)
Return a string that fully describes the version of Z3 in use.
Z3_enable_trace
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_mk_solver_from_tactic
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_mk_lambda
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_mk_set_complement
Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.
Z3_get_quantifier_num_patterns
unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a)
Return number of patterns used in quantifier.
Z3_get_quantifier_bound_name
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_simplify_get_help
Z3_string Z3_API Z3_simplify_get_help(Z3_context c)
Return a string describing all available parameters.
Z3_get_num_probes
unsigned Z3_API Z3_get_num_probes(Z3_context c)
Return the number of builtin probes available in Z3.
Z3_stats_is_uint
bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return true if the given statistical data is a unsigned integer.
Z3_stats_is_double
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.
Z3_model_get_num_consts
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_get_algebraic_number_lower
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_get_lstring
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_mk_extract
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_mk_iff
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_mk_mod
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_solver_interrupt
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_mk_bvredand
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_mk_set_add
Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)
Add an element to a set.
Z3_mk_ge
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_mk_bvadd_no_underflow
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.
Z3_get_array_arity
unsigned Z3_API Z3_get_array_arity(Z3_context c, Z3_sort s)
Return the arity (number of dimensions) of the given array sort.
Z3_update_param_value
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_mk_bvadd_no_overflow
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
Z3_set_ast_print_mode
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_solver_propagate_consequence
bool 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 and equalities. A client may invoke it during the pro...
Z3_mk_array_default
Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array)
Access the array default value. Produces the default range value, for arrays that can be represented ...
Z3_enable_concurrent_dec_ref
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_datatype_update_field
Z3_ast Z3_API Z3_datatype_update_field(Z3_context c, Z3_func_decl field_access, Z3_ast t, Z3_ast value)
Update record field with a value.
Z3_char_ptr
char const * Z3_char_ptr
Definition z3_api.h:51
Z3_mk_quantifier_const
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_mk_forall_const
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables.
Z3_model_get_num_sorts
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
Z3_param_kind
The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params).
Definition z3_api.h:1354
Z3_get_pattern_num_terms
unsigned Z3_API Z3_get_pattern_num_terms(Z3_context c, Z3_pattern p)
Return number of terms in pattern.
Z3_string
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition z3_api.h:50
Z3_parser_context_dec_ref
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_tactic_get_param_descrs
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_mk_tuple_sort
Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c, Z3_symbol mk_tuple_name, unsigned num_fields, Z3_symbol const field_names[], Z3_sort const field_sorts[], Z3_func_decl *mk_tuple_decl, Z3_func_decl proj_decl[])
Create a tuple type.
Z3_func_entry_inc_ref
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_mk_fresh_const
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.
Z3_mk_bvsub_no_overflow
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
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition z3_api.h:110
Z3_solver_push
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
Z3_mk_bvsub_no_underflow
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_translate
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_fail_if_not_decided
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_to_app
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_mk_bvudiv
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
Z3_get_finite_set_sort_basis
Z3_sort Z3_API Z3_get_finite_set_sort_basis(Z3_context c, Z3_sort s)
Get the element sort of a finite set sort.
Z3_solver_get_trail
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_mk_quantifier_ex
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_mk_bvshl
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
Z3_set_error
void Z3_API Z3_set_error(Z3_context c, Z3_error_code e)
Set an error.
Z3_mk_tree_order
Z3_func_decl Z3_API Z3_mk_tree_order(Z3_context c, Z3_sort a, unsigned id)
create a tree ordering relation over signature a identified using index id.
Z3_is_numeral_ast
bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a)
Z3_mk_finite_set_filter
Z3_ast Z3_API Z3_mk_finite_set_filter(Z3_context c, Z3_ast f, Z3_ast set)
Filter a finite set using a predicate.
Z3_mk_bvsrem
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_solver_congruence_next
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...
Z3_is_as_array
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_mk_func_decl
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.
Z3_goal_num_exprs
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_mk_solver_for_logic
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_mk_is_int
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
Z3_params_set_bool
void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, bool v)
Add a Boolean parameter k with value v to the parameter set p.
Z3_apply_result_get_num_subgoals
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_mk_ite
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_mk_select
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_mk_sign_ext
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_mk_seq_unit
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.
Z3_mk_re_intersect
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_mk_finite_set_member
Z3_ast Z3_API Z3_mk_finite_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check if an element is a member of a finite set.
Z3_solver_cube
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_mk_u32string
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...
Z3_goal_size
unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)
Return the number of formulas in the given goal.
Z3_solver_propagate_declare
Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort *domain, Z3_sort range)
Z3_stats_inc_ref
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
Z3_mk_select_n
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.
Z3_is_string_sort
bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s)
Check if s is a string sort.
Z3_mk_div
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_fail
Z3_tactic Z3_API Z3_tactic_fail(Z3_context c)
Return a tactic that always fails.
Z3_app_to_ast
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_mk_pbge
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_mk_re_sort
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_mk_pble
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_model_dec_ref
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
Z3_mk_datatype_sort
Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name, unsigned num_params, Z3_sort const params[])
create a forward reference to a recursive datatype being declared. The forward reference can be used ...
Z3_mk_exists
Z3_ast Z3_API Z3_mk_exists(Z3_context c, unsigned weight, unsigned num_patterns, Z3_pattern const patterns[], unsigned num_decls, Z3_sort const sorts[], Z3_symbol const decl_names[], Z3_ast body)
Create an exists formula. Similar to Z3_mk_forall.
Z3_func_interp_inc_ref
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_mk_piecewise_linear_order
Z3_func_decl Z3_API Z3_mk_piecewise_linear_order(Z3_context c, Z3_sort a, unsigned id)
create a piecewise linear ordering relation over signature a and index id.
Z3_params_set_double
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_pattern_to_string
Z3_string Z3_API Z3_pattern_to_string(Z3_context c, Z3_pattern p)
Z3_param_descrs_get_documentation
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_mk_finite_set_union
Z3_ast Z3_API Z3_mk_finite_set_union(Z3_context c, Z3_ast s1, Z3_ast s2)
Create the union of two finite sets.
Z3_mk_solver
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_solver_get_model
Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_get_symbol_int
int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s)
Return the symbol int value.
Z3_get_as_array_func_decl
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_mk_ext_rotate_left
Z3_ast Z3_API Z3_mk_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2)
Rotate bits of t1 to the left t2 times.
Z3_goal_inc_ref
void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.
Z3_simplifier_get_descr
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_par_or
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_mk_implies
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
Z3_constructor_num_fields
unsigned Z3_API Z3_constructor_num_fields(Z3_context c, Z3_constructor constr)
Retrieve the number of fields of a constructor.
Z3_get_datatype_sort_num_constructors
unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)
Return number of constructors for datatype.
Z3_params_set_uint
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_solver_check_assumptions
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not.
Z3_model_get_sort
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_mk_bvashr
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
Z3_simplifier_using_params
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_mk_bv2int
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_mk_sbv_to_str
Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s)
Signed bit-vector to string conversion.
Z3_get_array_sort_domain_n
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.
Z3_solver_import_model_converter
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_mk_set_del
Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)
Remove an element to a set.
Z3_mk_bvmul_no_overflow
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_mk_re_union
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_simplifier_get_param_descrs
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_mk_finite_set_intersect
Z3_ast Z3_API Z3_mk_finite_set_intersect(Z3_context c, Z3_ast s1, Z3_ast s2)
Create the intersection of two finite sets.
Z3_mk_bvor
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
Z3_get_decl_int_parameter
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.
Z3_get_quantifier_num_no_patterns
unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a)
Return number of no_patterns used in quantifier.
Z3_get_num_simplifiers
unsigned Z3_API Z3_get_num_simplifiers(Z3_context c)
Return the number of builtin simplifiers available in Z3.
Z3_get_datatype_sort_constructor
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th constructor.
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition z3_api.h:58
Z3_mk_seq_empty
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
Z3_mk_probe
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_mk_quantifier_const_ex
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_when
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_mk_seq_suffix
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_mk_pattern
Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[])
Create a pattern for quantifier instantiation.
Z3_get_symbol_kind
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_get_re_sort_basis
Z3_sort Z3_API Z3_get_re_sort_basis(Z3_context c, Z3_sort s)
Retrieve basis sort for regex sort.
Z3_solver_set_initial_value
void Z3_API Z3_solver_set_initial_value(Z3_context c, Z3_solver s, Z3_ast v, Z3_ast val)
provide an initialization hint to the solver. The initialization hint is used to calibrate an initial...
Z3_is_recursive_datatype_sort
bool Z3_API Z3_is_recursive_datatype_sort(Z3_context c, Z3_sort s)
Check if s is a recursive datatype sort.
Z3_mk_set_sort
Z3_sort Z3_API Z3_mk_set_sort(Z3_context c, Z3_sort ty)
Create Set type.
Z3_is_lambda
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.
Z3_solver_translate
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_solver_get_help
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.
Z3_stats_get_uint_value
unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx)
Return the unsigned value of the given statistical data.
Z3_probe_inc_ref
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
Z3_get_array_sort_domain
Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t)
Return the domain of the given array sort. In the case of a multi-dimensional array,...
Z3_solver_propagate_register_cb
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_mk_bvmul_no_underflow
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_get_probe_name
Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i)
Return the name of the i probe.
Z3_func_decl_to_ast
Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f)
Convert a Z3_func_decl into Z3_ast. This is just type casting.
Z3_get_numeral_uint64
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....
Z3_add_const_interp
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_sort_to_string
Z3_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s)
Z3_mk_bvadd
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
Z3_params_dec_ref
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)
Decrement the reference counter of the given parameter set.
Z3_get_app_arg
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_mk_str_lt
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_solver_congruence_root
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_model_to_string
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
Z3_get_string_length
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_tactic_get_help
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_mk_fresh_func_decl
Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a fresh constant or function.
Z3_solver_propagate_final
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...
Z3_param_descrs_size
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
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition z3_api.h:94
Z3_parse_smtlib2_string
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_get_tuple_sort_mk_decl
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_mk_bit2bool
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.
Z3_solver_register_on_clause
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_goal_to_dimacs_string
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_mk_lt
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
Z3_get_quantifier_no_pattern_ast
Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th no_pattern.
Z3_stats_get_double_value
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_mk_bvugt
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
Z3_get_num_tactics
unsigned Z3_API Z3_get_num_tactics(Z3_context c)
Return the number of builtin tactics available in Z3.
Z3_goal_depth
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_update_term
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_get_symbol_string
Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)
Return the symbol name.
Z3_get_bool_value
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_mk_simplifier
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_pattern_to_ast
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_mk_bvnot
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
Z3_mk_bvurem
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
Z3_mk_seq_foldli
Z3_ast Z3_API Z3_mk_seq_foldli(Z3_context c, Z3_ast f, Z3_ast i, Z3_ast a, Z3_ast s)
Create a fold with index tracking of the function f over the sequence s with accumulator a starting a...
Z3_mk_datatypes
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.
Z3_func_interp_get_arity
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_solver_get_non_units
Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s)
Return the set of non units in the solver state.
Z3_is_eq_func_decl
bool Z3_API Z3_is_eq_func_decl(Z3_context c, Z3_func_decl f1, Z3_func_decl f2)
Compare terms.
Z3_mk_seq_to_re
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_mk_bvsub
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_get_relation_arity
unsigned Z3_API Z3_get_relation_arity(Z3_context c, Z3_sort s)
Return arity of relation.
Z3_get_finite_domain_sort_size
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_mk_seq_index
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_get_algebraic_number_upper
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_mk_power
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
Z3_mk_seq_concat
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_mk_enumeration_sort
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_mk_re_range
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.
Z3_get_bv_sort_size
unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t)
Return the size of the given bit-vector sort.
Z3_mk_ff_add
Z3_ast Z3_API Z3_mk_ff_add(Z3_context c, unsigned n, Z3_ast const args[])
Sum at least two elements of the same prime field.
Z3_mk_set_member
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
Z3_tactic_fail_if
Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
Z3_goal_reset
void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)
Erase all formulas from the given goal.
Z3_func_interp_dec_ref
void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.
Z3_probe_dec_ref
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
Z3_params_inc_ref
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.
Z3_set_error_handler
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
Z3_mk_distinct
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_mk_seq_prefix
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_mk_config
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
Z3_set_param_value
void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)
Set a configuration parameter.
Z3_solver_congruence_explain
Z3_ast Z3_API Z3_solver_congruence_explain(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast b)
retrieve explanation for congruence.
Z3_get_depth
unsigned Z3_API Z3_get_depth(Z3_context c, Z3_ast a)
Z3_mk_bv_sort
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
Z3_mk_bvult
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
Z3_probe_or
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_params_to_string
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_get_global_param_descrs
Z3_param_descrs Z3_API Z3_get_global_param_descrs(Z3_context c)
Retrieve description of global parameters.
Z3_mk_re_power
Z3_ast Z3_API Z3_mk_re_power(Z3_context c, Z3_ast re, unsigned n)
Create a power regular expression.
Z3_solver_propagate_init
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-propagator with the solver.
Z3_model_get_const_decl
Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i)
Return the i-th constant in the given model.
Z3_tactic_dec_ref
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
Z3_mk_bvnand
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
Z3_translate
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_mk_simple_solver
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new incremental solver.
Z3_get_range
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
Z3_global_param_set
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_model_get_sort_universe
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_benchmark_to_smtlib_string
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_mk_re_star
Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)
Create the regular language re*.
Z3_mk_bv_numeral
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_mk_char
Z3_ast Z3_API Z3_mk_char(Z3_context c, unsigned ch)
Create a character literal.
Z3_func_entry_dec_ref
void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e)
Decrement the reference counter of the given Z3_func_entry object.
Z3_stats_size
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
Z3_append_log
void Z3_API Z3_append_log(Z3_string string)
Append user-defined string to interaction log.
Z3_get_quantifier_body
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
Z3_param_descrs_dec_ref
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_mk_re_full
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.
Z3_mk_model
Z3_model Z3_API Z3_mk_model(Z3_context c)
Create a fresh model object. It has reference count 0.
Z3_get_decl_name
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d)
Return the constant declaration name as a symbol.
Z3_mk_seq_mapi
Z3_ast Z3_API Z3_mk_seq_mapi(Z3_context c, Z3_ast f, Z3_ast i, Z3_ast s)
Create a map of the function f over the sequence s starting at index i.
Z3_mk_bvneg_no_overflow
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_stats_get_key
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_mk_re_diff
Z3_ast Z3_API Z3_mk_re_diff(Z3_context c, Z3_ast re1, Z3_ast re2)
Create the difference of regular expressions.
Z3_mk_int64
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
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:72
Z3_mk_re_empty
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
Z3_mk_bvand
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
Z3_simplify_get_param_descrs
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
Z3_goal_is_decided_unsat
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_mk_finite_domain_sort
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_mk_add
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_get_ast_kind
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
Z3_parse_smtlib2_file
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_get_implied_equalities
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_mk_abs
Z3_ast Z3_API Z3_mk_abs(Z3_context c, Z3_ast arg)
Take the absolute value of an integer.
Z3_mk_bvsmod
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_cond
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_translate
Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst)
translate model from context c to context dst.
Z3_solver_get_levels
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...
Z3_get_version
void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)
Return Z3 version number information.
Z3_tactic_apply_ex
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_mk_int2bv
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
Z3_solver_assert
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
Z3_mk_tactic
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...
Z3_parser_context_add_sort
void Z3_API Z3_parser_context_add_sort(Z3_context c, Z3_parser_context pc, Z3_sort s)
Add a sort declaration.
Z3_get_quantifier_weight
unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a)
Obtain weight of quantifier.
Z3_model_eval
bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return true if succeeded, and store the result in v.
Z3_solver_get_num_scopes
unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s)
Return the number of backtracking points.
Z3_get_array_sort_range
Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t)
Return the range of the given array sort.
Z3_del_constructor_list
void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist)
Reclaim memory allocated for constructor list.
Z3_mk_bound
Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty)
Create a variable.
Z3_get_app_num_args
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_mk_real
Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den)
Create a real from a fraction.
Z3_substitute_funs
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 functions in from with new expressions in to.
Z3_func_entry_get_arg
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_code
Z3 error codes (See Z3_get_error_code).
Definition z3_api.h:1396
Z3_mk_eq
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
Z3_mk_atleast
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_get_estimated_alloc_size
uint64_t Z3_API Z3_get_estimated_alloc_size(void)
Return the estimated allocated memory in bytes.
Z3_model_get_num_funcs
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.
Z3_parser_context_inc_ref
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.
Z3_dec_ref
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_solver_get_unsat_core
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_get_tuple_sort_field_decl
Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t, unsigned i)
Return the i-th field declaration (i.e., projection function declaration) of the given tuple sort.
Z3_get_simplifier_name
Z3_string Z3_API Z3_get_simplifier_name(Z3_context c, unsigned i)
Return the name of the idx simplifier.
Z3_get_string
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s. Characters outside the basic printable ASCII range are esca...
Z3_get_numeral_int
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_get_error_code
Z3_error_code Z3_API Z3_get_error_code(Z3_context c)
Return the error code for the last API call.
Z3_mk_partial_order
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_mk_empty_set
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
Z3_get_relation_column
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_solver_solve_for
void Z3_API Z3_solver_solve_for(Z3_context c, Z3_solver s, Z3_ast_vector variables, Z3_ast_vector terms, Z3_ast_vector guards)
retrieve a 'solution' for variables as defined by equalities in maintained by solvers....
Z3_get_tactic_name
Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i)
Return the name of the idx tactic.
Z3_is_string
bool Z3_API Z3_is_string(Z3_context c, Z3_ast s)
Determine if s is a string constant.
Z3_mk_re_loop
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_mk_char_to_int
Z3_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch)
Create an integer (code point) from character.
Z3_mk_ff_mul
Z3_ast Z3_API Z3_mk_ff_mul(Z3_context c, unsigned n, Z3_ast const args[])
Multiply at least two elements of the same prime field.
Z3_mk_repeat
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.
Z3_tactic_get_descr
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_mk_re_plus
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.
Z3_mk_finite_field_sort
Z3_sort Z3_API Z3_mk_finite_field_sort(Z3_context c, Z3_string prime)
Create a prime-field sort. Large moduli undergo probable-prime screening.
Z3_goal_precision
Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g)
Return the "precision" of the given goal. Goals can be transformed using over and under approximation...
Z3_solver_pop
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
Z3_mk_int2real
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
Z3_get_index_value
unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a)
Return index of de-Bruijn bound variable.
Z3_mk_goal
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...
Z3_get_decl_double_parameter
double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
Z3_get_ast_hash
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_mk_unsigned_int64
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_get_sort_name
Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d)
Return the sort name as a symbol.
Z3_params_validate
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_get_datatype_sort_recognizer
Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th recognizer.
Z3_global_param_reset_all
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_mk_gt
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
Z3_mk_store
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.
Z3_probe_gt
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_skip
Z3_tactic Z3_API Z3_tactic_skip(Z3_context c)
Return a tactic that just return the given goal.
Z3_solver_get_proof
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_get_decl_rational_parameter
Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the rational value, as a string, associated with a rational parameter.
Z3_model_has_interp
bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Test if there exists an interpretation (i.e., assignment) for a in the model m.
Z3_is_eq_ast
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
Z3_is_quantifier_forall
bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.
Z3_tactic_inc_ref
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
Z3_mk_parser_context
Z3_parser_context Z3_API Z3_mk_parser_context(Z3_context c)
Create a parser context.
Z3_is_ground
bool Z3_API Z3_is_ground(Z3_context c, Z3_ast a)
Z3_mk_real_int64
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.
Z3_solver_from_file
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a file.
Z3_mk_seq_last_index
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_mk_xor
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
Z3_solver_propagate_eq
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_mk_string
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_mk_transitive_closure
Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f)
create transitive closure of binary relation.
Z3_tactic_try_for
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_mk_rotate_left
Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the left i times.
Z3_apply_result_dec_ref
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_mk_map
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_mk_finite_set_singleton
Z3_ast Z3_API Z3_mk_finite_set_singleton(Z3_context c, Z3_ast elem)
Create a singleton finite set.
Z3_mk_seq_sort
Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s)
Create a sequence sort out of the sort for the elements.
Z3_solver_get_units
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.
Z3_mk_const
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
Z3_mk_string_symbol
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
Z3_probe_get_descr
Z3_string Z3_API Z3_probe_get_descr(Z3_context c, Z3_string name)
Return a string containing a description of the probe with the given name.
Z3_param_descrs_inc_ref
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_apply_result_get_subgoal
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_le
Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
Z3_stats_dec_ref
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
Z3_mk_array_ext
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_mk_seq_replace_re_all
Z3_ast Z3_API Z3_mk_seq_replace_re_all(Z3_context c, Z3_ast s, Z3_ast re, Z3_ast dst)
Replace all occurrences of regular expression re with dst in s.
Z3_mk_re_concat
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_sort_to_ast
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_interp_get_entry
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_mk_rec_func_decl
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.
Z3_get_ast_id
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_mk_seq_power
Z3_ast Z3_API Z3_mk_seq_power(Z3_context c, Z3_ast s, Z3_ast n)
Create the sequence s concatenated n times with itself. The result is the empty sequence when n is no...
Z3_mk_concat
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_get_quantifier_num_bound
unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a)
Return number of bound variables of quantifier.
Z3_get_decl_sort_parameter
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_mk_constructor_list
Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, unsigned num_constructors, Z3_constructor const constructors[])
Create list of constructors.
Z3_tactic_apply
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
Z3_mk_finite_set_map
Z3_ast Z3_API Z3_mk_finite_set_map(Z3_context c, Z3_ast f, Z3_ast set)
Apply a function to all elements of a finite set.
Z3_solver_propagate_created
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...
Z3_get_sort_id
unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s)
Return a unique identifier for s.
Z3_parser_context_from_string
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_mk_app
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_get_sort_kind
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_solver_get_statistics
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
Z3_mk_bvneg
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
Z3_mk_store_n
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_mk_linear_order
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_get_domain
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_mk_seq_in_re
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_mk_bool_sort
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
Z3_mk_sub
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].
Z3_mk_finite_set_sort
Z3_sort Z3_API Z3_mk_finite_set_sort(Z3_context c, Z3_sort elem_sort)
Create a finite set sort.
Z3_params_set_symbol
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_solver_to_dimacs_string
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_mk_finite_set_size
Z3_ast Z3_API Z3_mk_finite_set_size(Z3_context c, Z3_ast set)
Get the size (cardinality) of a finite set.
Z3_to_func_decl
Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a)
Convert an AST into a FUNC_DECL_AST. This is just type casting.
Z3_get_func_decl_id
unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f)
Return a unique identifier for f.
Z3_mk_set_difference
Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Take the set difference between two sets.
Z3_solver_propagate_decide
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 cha...
Z3_mk_lstring
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_mk_bvsdiv
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
Z3_mk_bvlshr
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
Z3_get_decl_ast_parameter
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_mk_finite_set_range
Z3_ast Z3_API Z3_mk_finite_set_range(Z3_context c, Z3_ast low, Z3_ast high)
Create a finite set of integers in the range [low, high].
Z3_get_quantifier_pattern_ast
Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th pattern.
Z3_probe_apply
double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0....
Z3_func_interp_set_else
void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value)
Return the 'else' value of the given function interpretation.
Z3_goal_dec_ref
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)
Decrement the reference counter of the given goal.
Z3_mk_not
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
Z3_solver_propagate_register
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_substitute_vars
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_mk_or
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_mk_array_sort
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
Z3_tactic_or_else
Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...
Z3_model_inc_ref
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
Z3_mk_seq_extract
Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length)
Extract subsequence starting at offset of length.
Z3_mk_type_variable
Z3_sort Z3_API Z3_mk_type_variable(Z3_context c, Z3_symbol s)
Create a type variable.
Z3_goal_is_decided_sat
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_add_simplifier
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_mk_list_sort
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_mk_rem
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_mk_int_to_str
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.
Z3_get_numeral_uint
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_get_numeral_string
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.
Z3_solver_propagate_fixed
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 ...
Z3_mk_seq_map
Z3_ast Z3_API Z3_mk_seq_map(Z3_context c, Z3_ast f, Z3_ast s)
Create a map of the function f over the sequence s.
Z3_close_log
void Z3_API Z3_close_log(void)
Close interaction log.
Z3_mk_char_is_digit
Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch)
Create a check if the character is a digit.
Z3_func_interp_add_entry
void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value)
add a function entry to a function interpretation.
Z3_is_well_sorted
bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.
Z3_mk_bvuge
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_mk_as_array
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_apply_result_to_string
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_solver_to_string
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
Z3_mk_seq_foldl
Z3_ast Z3_API Z3_mk_seq_foldl(Z3_context c, Z3_ast f, Z3_ast a, Z3_ast s)
Create a fold of the function f over the sequence s with accumulator a.
Z3_solver_get_reason_unknown
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_get_numeral_binary_string
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_get_quantifier_bound_sort
Z3_sort Z3_API Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, unsigned i)
Return sort of the i'th bound variable.
Z3_disable_trace
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_repeat
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_ptr
Z3_string * Z3_string_ptr
Definition z3_api.h:52
Z3_goal_formula
Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx)
Return a formula from the given goal.
Z3_mk_divides
Z3_ast Z3_API Z3_mk_divides(Z3_context c, Z3_ast t1, Z3_ast t2)
Create division predicate.
Z3_mk_int_symbol
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
Z3_mk_char_from_bv
Z3_ast Z3_API Z3_mk_char_from_bv(Z3_context c, Z3_ast bv)
Create a character from a bit-vector (code point).
Z3_func_interp_get_num_entries
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)
Return the number of entries in the given function interpretation.
Z3_get_numeral_rational_int64
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_const
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
Z3_mk_constructor
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 const sorts[], unsigned sort_refs[])
Create a constructor.
Z3_goal_to_string
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.
Z3_mk_atmost
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_is_eq_sort
bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2)
compare sorts.
Z3_del_config
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
Z3_get_numeral_double
double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)
Return numeral as a double.
Z3_inc_ref
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_and_then
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_mk_real2int
Z3_ast Z3_API Z3_mk_real2int(Z3_context c, Z3_ast t1)
Coerce a real to an integer.
Z3_model_get_func_interp
Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f)
Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...
Z3_reset_memory
void Z3_API Z3_reset_memory(void)
Reset all allocated resources.
Z3_solver_inc_ref
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
Z3_is_app
bool Z3_API Z3_is_app(Z3_context c, Z3_ast a)
Z3_solver_next_split
bool Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase)
Z3_mk_forall
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_and
Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 and p2 evaluates to true.
Z3_get_quantifier_id
Z3_symbol Z3_API Z3_get_quantifier_id(Z3_context c, Z3_ast a)
Obtain id of quantifier.
Z3_is_re_sort
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
Z3_get_finite_field_sort_size
Z3_string Z3_API Z3_get_finite_field_sort_size(Z3_context c, Z3_sort s)
Return the decimal modulus of a finite-field sort.
Z3_mk_string_to_code
Z3_ast Z3_API Z3_mk_string_to_code(Z3_context c, Z3_ast a)
String to code conversion.
Z3_mk_seq_replace_re
Z3_ast Z3_API Z3_mk_seq_replace_re(Z3_context c, Z3_ast s, Z3_ast re, Z3_ast dst)
Replace the first occurrence of regular expression re with dst in s.
Z3_get_domain_size
unsigned Z3_API Z3_get_domain_size(Z3_context c, Z3_func_decl d)
Return the number of parameters of the given declaration.
Z3_mk_ubv_to_str
Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s)
Unsigned bit-vector to string conversion.
Z3_mk_string_sort
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for unicode strings.
Z3_mk_ext_rotate_right
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_get_numeral_decimal_string
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_get_sort
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
Z3_get_datatype_sort_constructor_accessor
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_mk_bvredor
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_mk_seq_nth
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_mk_seq_contains
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.
Z3_solver_reset
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
Z3_is_algebraic_number
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
@ Z3_PRINT_SMTLIB2_COMPLIANT
Definition z3_api.h:1374
Z3_PRINT_SMTLIB_FULL
@ Z3_PRINT_SMTLIB_FULL
Definition z3_api.h:1372
Z3_PRINT_LOW_LEVEL
@ Z3_PRINT_LOW_LEVEL
Definition z3_api.h:1373
Z3_APP_AST
@ Z3_APP_AST
Definition z3_api.h:145
Z3_VAR_AST
@ Z3_VAR_AST
Definition z3_api.h:146
Z3_SORT_AST
@ Z3_SORT_AST
Definition z3_api.h:148
Z3_NUMERAL_AST
@ Z3_NUMERAL_AST
Definition z3_api.h:144
Z3_FUNC_DECL_AST
@ Z3_FUNC_DECL_AST
Definition z3_api.h:149
Z3_QUANTIFIER_AST
@ Z3_QUANTIFIER_AST
Definition z3_api.h:147
Z3_UNKNOWN_AST
@ Z3_UNKNOWN_AST
Definition z3_api.h:150
Z3_GOAL_UNDER
@ Z3_GOAL_UNDER
Definition z3_api.h:1439
Z3_GOAL_UNDER_OVER
@ Z3_GOAL_UNDER_OVER
Definition z3_api.h:1441
Z3_GOAL_OVER
@ Z3_GOAL_OVER
Definition z3_api.h:1440
Z3_GOAL_PRECISE
@ Z3_GOAL_PRECISE
Definition z3_api.h:1438
Z3_OP_BSMOD
@ Z3_OP_BSMOD
Definition z3_api.h:1052
Z3_OP_SUB
@ Z3_OP_SUB
Definition z3_api.h:1012
Z3_OP_STRING_LE
@ Z3_OP_STRING_LE
Definition z3_api.h:1207
Z3_OP_SIGN_EXT
@ Z3_OP_SIGN_EXT
Definition z3_api.h:1080
Z3_OP_FPA_MUL
@ Z3_OP_FPA_MUL
Definition z3_api.h:1280
Z3_OP_RE_OF_PRED
@ Z3_OP_RE_OF_PRED
Definition z3_api.h:1224
Z3_OP_FPA_IS_NEGATIVE
@ Z3_OP_FPA_IS_NEGATIVE
Definition z3_api.h:1300
Z3_OP_FINITE_SET_SIZE
@ Z3_OP_FINITE_SET_SIZE
Definition z3_api.h:1322
Z3_OP_FPA_ROUND_TO_INTEGRAL
@ Z3_OP_FPA_ROUND_TO_INTEGRAL
Definition z3_api.h:1288
Z3_OP_FD_CONSTANT
@ Z3_OP_FD_CONSTANT
Definition z3_api.h:1171
Z3_OP_BADD
@ Z3_OP_BADD
Definition z3_api.h:1044
Z3_OP_BIT1
@ Z3_OP_BIT1
Definition z3_api.h:1041
Z3_OP_BREDAND
@ Z3_OP_BREDAND
Definition z3_api.h:1086
Z3_OP_MUL
@ Z3_OP_MUL
Definition z3_api.h:1014
Z3_OP_SEQ_POWER
@ Z3_OP_SEQ_POWER
Definition z3_api.h:1197
Z3_OP_XOR3
@ Z3_OP_XOR3
Definition z3_api.h:1102
Z3_OP_FINITE_SET_MAP
@ Z3_OP_FINITE_SET_MAP
Definition z3_api.h:1324
Z3_OP_FPA_SUB
@ Z3_OP_FPA_SUB
Definition z3_api.h:1278
Z3_OP_UGEQ
@ Z3_OP_UGEQ
Definition z3_api.h:1064
Z3_OP_RE_POWER
@ Z3_OP_RE_POWER
Definition z3_api.h:1219
Z3_OP_SBV_TO_STR
@ Z3_OP_SBV_TO_STR
Definition z3_api.h:1203
Z3_OP_BUDIV
@ Z3_OP_BUDIV
Definition z3_api.h:1049
Z3_OP_FPA_ABS
@ Z3_OP_FPA_ABS
Definition z3_api.h:1283
Z3_OP_SLT
@ Z3_OP_SLT
Definition z3_api.h:1067
Z3_OP_BASHR
@ Z3_OP_BASHR
Definition z3_api.h:1091
Z3_OP_PR_LEMMA
@ Z3_OP_PR_LEMMA
Definition z3_api.h:1137
Z3_OP_PR_BIND
@ Z3_OP_PR_BIND
Definition z3_api.h:1125
Z3_OP_SEQ_LENGTH
@ Z3_OP_SEQ_LENGTH
Definition z3_api.h:1188
Z3_OP_SEQ_FOLDLI
@ Z3_OP_SEQ_FOLDLI
Definition z3_api.h:1196
Z3_OP_FPA_PLUS_ZERO
@ Z3_OP_FPA_PLUS_ZERO
Definition z3_api.h:1274
Z3_OP_PR_IFF_FALSE
@ Z3_OP_PR_IFF_FALSE
Definition z3_api.h:1140
Z3_OP_SEQ_AT
@ Z3_OP_SEQ_AT
Definition z3_api.h:1186
Z3_OP_INTERNAL
@ Z3_OP_INTERNAL
Definition z3_api.h:1330
Z3_OP_PR_MONOTONICITY
@ Z3_OP_PR_MONOTONICITY
Definition z3_api.h:1123
Z3_OP_PR_UNIT_RESOLUTION
@ Z3_OP_PR_UNIT_RESOLUTION
Definition z3_api.h:1138
Z3_OP_FINITE_SET_EXT
@ Z3_OP_FINITE_SET_EXT
Definition z3_api.h:1327
Z3_OP_RE_PLUS
@ Z3_OP_RE_PLUS
Definition z3_api.h:1210
Z3_OP_FPA_NUM
@ Z3_OP_FPA_NUM
Definition z3_api.h:1270
Z3_OP_FINITE_SET_FILTER
@ Z3_OP_FINITE_SET_FILTER
Definition z3_api.h:1325
Z3_OP_LABEL
@ Z3_OP_LABEL
Definition z3_api.h:1237
Z3_OP_ARRAY_EXT
@ Z3_OP_ARRAY_EXT
Definition z3_api.h:1037
Z3_OP_SEQ_CONCAT
@ Z3_OP_SEQ_CONCAT
Definition z3_api.h:1177
Z3_OP_RE_EMPTY_SET
@ Z3_OP_RE_EMPTY_SET
Definition z3_api.h:1221
Z3_OP_FF_NEG
@ Z3_OP_FF_NEG
Definition z3_api.h:1338
Z3_OP_SEQ_INDEX
@ Z3_OP_SEQ_INDEX
Definition z3_api.h:1189
Z3_OP_SET_DIFFERENCE
@ Z3_OP_SET_DIFFERENCE
Definition z3_api.h:1033
Z3_OP_PR_IFF_TRUE
@ Z3_OP_PR_IFF_TRUE
Definition z3_api.h:1139
Z3_OP_RE_RANGE
@ Z3_OP_RE_RANGE
Definition z3_api.h:1215
Z3_OP_BUDIV_I
@ Z3_OP_BUDIV_I
Definition z3_api.h:1108
Z3_OP_DISTINCT
@ Z3_OP_DISTINCT
Definition z3_api.h:994
Z3_OP_RE_REVERSE
@ Z3_OP_RE_REVERSE
Definition z3_api.h:1225
Z3_OP_FINITE_SET_RANGE
@ Z3_OP_FINITE_SET_RANGE
Definition z3_api.h:1326
Z3_OP_SEQ_REPLACE_RE
@ Z3_OP_SEQ_REPLACE_RE
Definition z3_api.h:1183
Z3_OP_EXTRACT
@ Z3_OP_EXTRACT
Definition z3_api.h:1082
Z3_OP_RA_STORE
@ Z3_OP_RA_STORE
Definition z3_api.h:1158
Z3_OP_FPA_FMA
@ Z3_OP_FPA_FMA
Definition z3_api.h:1286
Z3_OP_BOR
@ Z3_OP_BOR
Definition z3_api.h:1072
Z3_OP_FPA_GT
@ Z3_OP_FPA_GT
Definition z3_api.h:1292
Z3_OP_DT_UPDATE_FIELD
@ Z3_OP_DT_UPDATE_FIELD
Definition z3_api.h:1245
Z3_OP_BUREM_I
@ Z3_OP_BUREM_I
Definition z3_api.h:1110
Z3_OP_SET_COMPLEMENT
@ Z3_OP_SET_COMPLEMENT
Definition z3_api.h:1034
Z3_OP_PR_QUANT_INST
@ Z3_OP_PR_QUANT_INST
Definition z3_api.h:1135
Z3_OP_RA_WIDEN
@ Z3_OP_RA_WIDEN
Definition z3_api.h:1163
Z3_OP_RE_COMPLEMENT
@ Z3_OP_RE_COMPLEMENT
Definition z3_api.h:1220
Z3_OP_AND
@ Z3_OP_AND
Definition z3_api.h:996
Z3_OP_FINITE_SET_UNION
@ Z3_OP_FINITE_SET_UNION
Definition z3_api.h:1318
Z3_OP_STRING_LT
@ Z3_OP_STRING_LT
Definition z3_api.h:1206
Z3_OP_SEQ_MAP
@ Z3_OP_SEQ_MAP
Definition z3_api.h:1193
Z3_OP_ARRAY_MAP
@ Z3_OP_ARRAY_MAP
Definition z3_api.h:1029
Z3_OP_PR_REFLEXIVITY
@ Z3_OP_PR_REFLEXIVITY
Definition z3_api.h:1119
Z3_OP_FALSE
@ Z3_OP_FALSE
Definition z3_api.h:992
Z3_OP_PR_DEF_AXIOM
@ Z3_OP_PR_DEF_AXIOM
Definition z3_api.h:1142
Z3_OP_SPECIAL_RELATION_TRC
@ Z3_OP_SPECIAL_RELATION_TRC
Definition z3_api.h:1260
Z3_OP_XOR
@ Z3_OP_XOR
Definition z3_api.h:999
Z3_OP_BIT2BOOL
@ Z3_OP_BIT2BOOL
Definition z3_api.h:1097
Z3_OP_FPA_GE
@ Z3_OP_FPA_GE
Definition z3_api.h:1294
Z3_OP_RA_IS_EMPTY
@ Z3_OP_RA_IS_EMPTY
Definition z3_api.h:1160
Z3_OP_PR_MODUS_PONENS
@ Z3_OP_PR_MODUS_PONENS
Definition z3_api.h:1118
Z3_OP_RA_EMPTY
@ Z3_OP_RA_EMPTY
Definition z3_api.h:1159
Z3_OP_PR_MODUS_PONENS_OEQ
@ Z3_OP_PR_MODUS_PONENS_OEQ
Definition z3_api.h:1153
Z3_OP_SEQ_REPLACE
@ Z3_OP_SEQ_REPLACE
Definition z3_api.h:1182
Z3_OP_DT_IS
@ Z3_OP_DT_IS
Definition z3_api.h:1243
Z3_OP_CONST_ARRAY
@ Z3_OP_CONST_ARRAY
Definition z3_api.h:1028
Z3_OP_FINITE_SET_SINGLETON
@ Z3_OP_FINITE_SET_SINGLETON
Definition z3_api.h:1317
Z3_OP_IMPLIES
@ Z3_OP_IMPLIES
Definition z3_api.h:1001
Z3_OP_SELECT
@ Z3_OP_SELECT
Definition z3_api.h:1027
Z3_OP_FPA_TO_FP
@ Z3_OP_FPA_TO_FP
Definition z3_api.h:1304
Z3_OP_FPA_NEG
@ Z3_OP_FPA_NEG
Definition z3_api.h:1279
Z3_OP_FPA_NAN
@ Z3_OP_FPA_NAN
Definition z3_api.h:1273
Z3_OP_RA_CLONE
@ Z3_OP_RA_CLONE
Definition z3_api.h:1170
Z3_OP_ADD
@ Z3_OP_ADD
Definition z3_api.h:1011
Z3_OP_GT
@ Z3_OP_GT
Definition z3_api.h:1010
Z3_OP_PR_NOT_OR_ELIM
@ Z3_OP_PR_NOT_OR_ELIM
Definition z3_api.h:1128
Z3_OP_FPA_TO_REAL
@ Z3_OP_FPA_TO_REAL
Definition z3_api.h:1308
Z3_OP_ULEQ
@ Z3_OP_ULEQ
Definition z3_api.h:1062
Z3_OP_FPA_EQ
@ Z3_OP_FPA_EQ
Definition z3_api.h:1290
Z3_OP_INT2BV
@ Z3_OP_INT2BV
Definition z3_api.h:1098
Z3_OP_TO_INT
@ Z3_OP_TO_INT
Definition z3_api.h:1020
Z3_OP_PB_EQ
@ Z3_OP_PB_EQ
Definition z3_api.h:1252
Z3_OP_PR_TRANSITIVITY
@ Z3_OP_PR_TRANSITIVITY
Definition z3_api.h:1121
Z3_OP_BNUM
@ Z3_OP_BNUM
Definition z3_api.h:1040
Z3_OP_REM
@ Z3_OP_REM
Definition z3_api.h:1017
Z3_OP_POWER
@ Z3_OP_POWER
Definition z3_api.h:1022
Z3_OP_RE_DERIVATIVE
@ Z3_OP_RE_DERIVATIVE
Definition z3_api.h:1226
Z3_OP_SET_UNION
@ Z3_OP_SET_UNION
Definition z3_api.h:1031
Z3_OP_FPA_LE
@ Z3_OP_FPA_LE
Definition z3_api.h:1293
Z3_OP_FPA_MAX
@ Z3_OP_FPA_MAX
Definition z3_api.h:1285
Z3_OP_MOD
@ Z3_OP_MOD
Definition z3_api.h:1018
Z3_OP_RE_UNION
@ Z3_OP_RE_UNION
Definition z3_api.h:1214
Z3_OP_OEQ
@ Z3_OP_OEQ
Definition z3_api.h:1002
Z3_OP_BCOMP
@ Z3_OP_BCOMP
Definition z3_api.h:1087
Z3_OP_CHAR_LE
@ Z3_OP_CHAR_LE
Definition z3_api.h:1230
Z3_OP_FPA_RM_TOWARD_NEGATIVE
@ Z3_OP_FPA_RM_TOWARD_NEGATIVE
Definition z3_api.h:1267
Z3_OP_BSMOD_I
@ Z3_OP_BSMOD_I
Definition z3_api.h:1111
Z3_OP_PR_IFF_OEQ
@ Z3_OP_PR_IFF_OEQ
Definition z3_api.h:1149
Z3_OP_BNOR
@ Z3_OP_BNOR
Definition z3_api.h:1076
Z3_OP_UMINUS
@ Z3_OP_UMINUS
Definition z3_api.h:1013
Z3_OP_SEQ_UNIT
@ Z3_OP_SEQ_UNIT
Definition z3_api.h:1175
Z3_OP_DT_RECOGNISER
@ Z3_OP_DT_RECOGNISER
Definition z3_api.h:1242
Z3_OP_ITE
@ Z3_OP_ITE
Definition z3_api.h:995
Z3_OP_FPA_IS_ZERO
@ Z3_OP_FPA_IS_ZERO
Definition z3_api.h:1297
Z3_OP_FPA_IS_SUBNORMAL
@ Z3_OP_FPA_IS_SUBNORMAL
Definition z3_api.h:1299
Z3_OP_EQ
@ Z3_OP_EQ
Definition z3_api.h:993
Z3_OP_INT_TO_STR
@ Z3_OP_INT_TO_STR
Definition z3_api.h:1201
Z3_OP_ROTATE_RIGHT
@ Z3_OP_ROTATE_RIGHT
Definition z3_api.h:1093
Z3_OP_RA_COMPLEMENT
@ Z3_OP_RA_COMPLEMENT
Definition z3_api.h:1168
Z3_OP_GE
@ Z3_OP_GE
Definition z3_api.h:1008
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
@ Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
Definition z3_api.h:1264
Z3_OP_PR_ASSERTED
@ Z3_OP_PR_ASSERTED
Definition z3_api.h:1116
Z3_OP_DT_ACCESSOR
@ Z3_OP_DT_ACCESSOR
Definition z3_api.h:1244
Z3_OP_BLSHR
@ Z3_OP_BLSHR
Definition z3_api.h:1090
Z3_OP_IFF
@ Z3_OP_IFF
Definition z3_api.h:998
Z3_OP_FPA_BVWRAP
@ Z3_OP_FPA_BVWRAP
Definition z3_api.h:1312
Z3_OP_UNINTERPRETED
@ Z3_OP_UNINTERPRETED
Definition z3_api.h:1333
Z3_OP_AS_ARRAY
@ Z3_OP_AS_ARRAY
Definition z3_api.h:1036
Z3_OP_FPA_BV2RM
@ Z3_OP_FPA_BV2RM
Definition z3_api.h:1313
Z3_OP_RE_CONCAT
@ Z3_OP_RE_CONCAT
Definition z3_api.h:1213
Z3_OP_FPA_PLUS_INF
@ Z3_OP_FPA_PLUS_INF
Definition z3_api.h:1271
Z3_OP_PR_REWRITE_STAR
@ Z3_OP_PR_REWRITE_STAR
Definition z3_api.h:1130
Z3_OP_PR_HYPOTHESIS
@ Z3_OP_PR_HYPOTHESIS
Definition z3_api.h:1136
Z3_OP_BNAND
@ Z3_OP_BNAND
Definition z3_api.h:1075
Z3_OP_PB_AT_LEAST
@ Z3_OP_PB_AT_LEAST
Definition z3_api.h:1249
Z3_OP_PR_NNF_NEG
@ Z3_OP_PR_NNF_NEG
Definition z3_api.h:1151
Z3_OP_FPA_DIV
@ Z3_OP_FPA_DIV
Definition z3_api.h:1281
Z3_OP_PR_ELIM_UNUSED_VARS
@ Z3_OP_PR_ELIM_UNUSED_VARS
Definition z3_api.h:1133
Z3_OP_RA_UNION
@ Z3_OP_RA_UNION
Definition z3_api.h:1162
Z3_OP_PR_CLAUSE_TRAIL
@ Z3_OP_PR_CLAUSE_TRAIL
Definition z3_api.h:1146
Z3_OP_PR_TH_LEMMA
@ Z3_OP_PR_TH_LEMMA
Definition z3_api.h:1154
Z3_OP_UGT
@ Z3_OP_UGT
Definition z3_api.h:1068
Z3_OP_BXOR
@ Z3_OP_BXOR
Definition z3_api.h:1074
Z3_OP_SEQ_SUFFIX
@ Z3_OP_SEQ_SUFFIX
Definition z3_api.h:1179
Z3_OP_BSMUL_NO_OVFL
@ Z3_OP_BSMUL_NO_OVFL
Definition z3_api.h:1104
Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
@ Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
Definition z3_api.h:1265
Z3_OP_FINITE_SET_IN
@ Z3_OP_FINITE_SET_IN
Definition z3_api.h:1321
Z3_OP_RA_SELECT
@ Z3_OP_RA_SELECT
Definition z3_api.h:1169
Z3_OP_IS_INT
@ Z3_OP_IS_INT
Definition z3_api.h:1021
Z3_OP_REPEAT
@ Z3_OP_REPEAT
Definition z3_api.h:1083
Z3_OP_RA_JOIN
@ Z3_OP_RA_JOIN
Definition z3_api.h:1161
Z3_OP_PR_PULL_QUANT
@ Z3_OP_PR_PULL_QUANT
Definition z3_api.h:1131
Z3_OP_FPA_SQRT
@ Z3_OP_FPA_SQRT
Definition z3_api.h:1287
Z3_OP_CHAR_CONST
@ Z3_OP_CHAR_CONST
Definition z3_api.h:1229
Z3_OP_FPA_RM_TOWARD_ZERO
@ Z3_OP_FPA_RM_TOWARD_ZERO
Definition z3_api.h:1268
Z3_OP_SEQ_IN_RE
@ Z3_OP_SEQ_IN_RE
Definition z3_api.h:1192
Z3_OP_BSHL
@ Z3_OP_BSHL
Definition z3_api.h:1089
Z3_OP_BSDIV
@ Z3_OP_BSDIV
Definition z3_api.h:1048
Z3_OP_OR
@ Z3_OP_OR
Definition z3_api.h:997
Z3_OP_EXT_ROTATE_LEFT
@ Z3_OP_EXT_ROTATE_LEFT
Definition z3_api.h:1094
Z3_OP_FPA_TO_SBV
@ Z3_OP_FPA_TO_SBV
Definition z3_api.h:1307
Z3_OP_PB_GE
@ Z3_OP_PB_GE
Definition z3_api.h:1251
Z3_OP_BXNOR
@ Z3_OP_BXNOR
Definition z3_api.h:1077
Z3_OP_STR_TO_INT
@ Z3_OP_STR_TO_INT
Definition z3_api.h:1200
Z3_OP_LABEL_LIT
@ Z3_OP_LABEL_LIT
Definition z3_api.h:1238
Z3_OP_FINITE_SET_MAP_INVERSE
@ Z3_OP_FINITE_SET_MAP_INVERSE
Definition z3_api.h:1328
Z3_OP_FINITE_SET_SUBSET
@ Z3_OP_FINITE_SET_SUBSET
Definition z3_api.h:1323
Z3_OP_RECURSIVE
@ Z3_OP_RECURSIVE
Definition z3_api.h:1331
Z3_OP_FD_LT
@ Z3_OP_FD_LT
Definition z3_api.h:1172
Z3_OP_UBV_TO_STR
@ Z3_OP_UBV_TO_STR
Definition z3_api.h:1202
Z3_OP_ABS
@ Z3_OP_ABS
Definition z3_api.h:1023
Z3_OP_SET_INTERSECT
@ Z3_OP_SET_INTERSECT
Definition z3_api.h:1032
Z3_OP_FPA_MIN
@ Z3_OP_FPA_MIN
Definition z3_api.h:1284
Z3_OP_BSMUL_NO_UDFL
@ Z3_OP_BSMUL_NO_UDFL
Definition z3_api.h:1106
Z3_OP_FF_BITSUM
@ Z3_OP_FF_BITSUM
Definition z3_api.h:1339
Z3_OP_TO_REAL
@ Z3_OP_TO_REAL
Definition z3_api.h:1019
Z3_OP_EXT_ROTATE_RIGHT
@ Z3_OP_EXT_ROTATE_RIGHT
Definition z3_api.h:1095
Z3_OP_PR_APPLY_DEF
@ Z3_OP_PR_APPLY_DEF
Definition z3_api.h:1148
Z3_OP_RE_DIFF
@ Z3_OP_RE_DIFF
Definition z3_api.h:1216
Z3_OP_DIV
@ Z3_OP_DIV
Definition z3_api.h:1015
Z3_OP_BSUB
@ Z3_OP_BSUB
Definition z3_api.h:1045
Z3_OP_BNEG
@ Z3_OP_BNEG
Definition z3_api.h:1043
Z3_OP_SEQ_CONTAINS
@ Z3_OP_SEQ_CONTAINS
Definition z3_api.h:1180
Z3_OP_PR_SKOLEMIZE
@ Z3_OP_PR_SKOLEMIZE
Definition z3_api.h:1152
Z3_OP_STR_TO_CODE
@ Z3_OP_STR_TO_CODE
Definition z3_api.h:1204
Z3_OP_FINITE_SET_INTERSECT
@ Z3_OP_FINITE_SET_INTERSECT
Definition z3_api.h:1319
Z3_OP_FPA_RM_TOWARD_POSITIVE
@ Z3_OP_FPA_RM_TOWARD_POSITIVE
Definition z3_api.h:1266
Z3_OP_FPA_ADD
@ Z3_OP_FPA_ADD
Definition z3_api.h:1277
Z3_OP_PR_COMMUTATIVITY
@ Z3_OP_PR_COMMUTATIVITY
Definition z3_api.h:1141
Z3_OP_RE_FULL_SET
@ Z3_OP_RE_FULL_SET
Definition z3_api.h:1222
Z3_OP_SET_SUBSET
@ Z3_OP_SET_SUBSET
Definition z3_api.h:1035
Z3_OP_BSREM
@ Z3_OP_BSREM
Definition z3_api.h:1050
Z3_OP_NOT
@ Z3_OP_NOT
Definition z3_api.h:1000
Z3_OP_BSREM_I
@ Z3_OP_BSREM_I
Definition z3_api.h:1109
Z3_OP_FINITE_SET_DIFFERENCE
@ Z3_OP_FINITE_SET_DIFFERENCE
Definition z3_api.h:1320
Z3_OP_SEQ_NTH
@ Z3_OP_SEQ_NTH
Definition z3_api.h:1187
Z3_OP_SEQ_LAST_INDEX
@ Z3_OP_SEQ_LAST_INDEX
Definition z3_api.h:1190
Z3_OP_PR_PUSH_QUANT
@ Z3_OP_PR_PUSH_QUANT
Definition z3_api.h:1132
Z3_OP_PR_SYMMETRY
@ Z3_OP_PR_SYMMETRY
Definition z3_api.h:1120
Z3_OP_SPECIAL_RELATION_PO
@ Z3_OP_SPECIAL_RELATION_PO
Definition z3_api.h:1256
Z3_OP_RE_LOOP
@ Z3_OP_RE_LOOP
Definition z3_api.h:1218
Z3_OP_ZERO_EXT
@ Z3_OP_ZERO_EXT
Definition z3_api.h:1081
Z3_OP_SBV2INT
@ Z3_OP_SBV2INT
Definition z3_api.h:1100
Z3_OP_SLEQ
@ Z3_OP_SLEQ
Definition z3_api.h:1063
Z3_OP_RA_FILTER
@ Z3_OP_RA_FILTER
Definition z3_api.h:1165
Z3_OP_FPA_MINUS_INF
@ Z3_OP_FPA_MINUS_INF
Definition z3_api.h:1272
Z3_OP_PR_QUANT_INTRO
@ Z3_OP_PR_QUANT_INTRO
Definition z3_api.h:1124
Z3_OP_SEQ_MAPI
@ Z3_OP_SEQ_MAPI
Definition z3_api.h:1194
Z3_OP_PR_DER
@ Z3_OP_PR_DER
Definition z3_api.h:1134
Z3_OP_BUREM0
@ Z3_OP_BUREM0
Definition z3_api.h:1059
Z3_OP_SEQ_EMPTY
@ Z3_OP_SEQ_EMPTY
Definition z3_api.h:1176
Z3_OP_PR_HYPER_RESOLVE
@ Z3_OP_PR_HYPER_RESOLVE
Definition z3_api.h:1155
Z3_OP_FPA_IS_POSITIVE
@ Z3_OP_FPA_IS_POSITIVE
Definition z3_api.h:1301
Z3_OP_LT
@ Z3_OP_LT
Definition z3_api.h:1009
Z3_OP_BSDIV0
@ Z3_OP_BSDIV0
Definition z3_api.h:1056
Z3_OP_CHAR_TO_BV
@ Z3_OP_CHAR_TO_BV
Definition z3_api.h:1232
Z3_OP_PR_GOAL
@ Z3_OP_PR_GOAL
Definition z3_api.h:1117
Z3_OP_SPECIAL_RELATION_TC
@ Z3_OP_SPECIAL_RELATION_TC
Definition z3_api.h:1259
Z3_OP_RA_PROJECT
@ Z3_OP_RA_PROJECT
Definition z3_api.h:1164
Z3_OP_FPA_IS_NAN
@ Z3_OP_FPA_IS_NAN
Definition z3_api.h:1295
Z3_OP_SPECIAL_RELATION_TO
@ Z3_OP_SPECIAL_RELATION_TO
Definition z3_api.h:1258
Z3_OP_PR_TRUE
@ Z3_OP_PR_TRUE
Definition z3_api.h:1115
Z3_OP_RA_RENAME
@ Z3_OP_RA_RENAME
Definition z3_api.h:1167
Z3_OP_AGNUM
@ Z3_OP_AGNUM
Definition z3_api.h:1006
Z3_OP_BNOT
@ Z3_OP_BNOT
Definition z3_api.h:1073
Z3_OP_FPA_IS_INF
@ Z3_OP_FPA_IS_INF
Definition z3_api.h:1296
Z3_OP_BSMOD0
@ Z3_OP_BSMOD0
Definition z3_api.h:1060
Z3_OP_CONCAT
@ Z3_OP_CONCAT
Definition z3_api.h:1079
Z3_OP_FPA_TO_FP_UNSIGNED
@ Z3_OP_FPA_TO_FP_UNSIGNED
Definition z3_api.h:1305
Z3_OP_PR_REDUNDANT_DEL
@ Z3_OP_PR_REDUNDANT_DEL
Definition z3_api.h:1145
Z3_OP_PR_NNF_POS
@ Z3_OP_PR_NNF_POS
Definition z3_api.h:1150
Z3_OP_SEQ_REPLACE_ALL
@ Z3_OP_SEQ_REPLACE_ALL
Definition z3_api.h:1185
Z3_OP_FPA_REM
@ Z3_OP_FPA_REM
Definition z3_api.h:1282
Z3_OP_SEQ_EXTRACT
@ Z3_OP_SEQ_EXTRACT
Definition z3_api.h:1181
Z3_OP_RA_NEGATION_FILTER
@ Z3_OP_RA_NEGATION_FILTER
Definition z3_api.h:1166
Z3_OP_PR_LEMMA_ADD
@ Z3_OP_PR_LEMMA_ADD
Definition z3_api.h:1144
Z3_OP_RE_OPTION
@ Z3_OP_RE_OPTION
Definition z3_api.h:1212
Z3_OP_BUDIV0
@ Z3_OP_BUDIV0
Definition z3_api.h:1057
Z3_OP_PR_REWRITE
@ Z3_OP_PR_REWRITE
Definition z3_api.h:1129
Z3_OP_BV2INT
@ Z3_OP_BV2INT
Definition z3_api.h:1099
Z3_OP_RE_INTERSECT
@ Z3_OP_RE_INTERSECT
Definition z3_api.h:1217
Z3_OP_PR_DEF_INTRO
@ Z3_OP_PR_DEF_INTRO
Definition z3_api.h:1147
Z3_OP_FPA_MINUS_ZERO
@ Z3_OP_FPA_MINUS_ZERO
Definition z3_api.h:1275
Z3_OP_SPECIAL_RELATION_PLO
@ Z3_OP_SPECIAL_RELATION_PLO
Definition z3_api.h:1257
Z3_OP_BUMUL_NO_OVFL
@ Z3_OP_BUMUL_NO_OVFL
Definition z3_api.h:1105
Z3_OP_SGEQ
@ Z3_OP_SGEQ
Definition z3_api.h:1065
Z3_OP_ROTATE_LEFT
@ Z3_OP_ROTATE_LEFT
Definition z3_api.h:1092
Z3_OP_PR_UNDEF
@ Z3_OP_PR_UNDEF
Definition z3_api.h:1114
Z3_OP_PR_AND_ELIM
@ Z3_OP_PR_AND_ELIM
Definition z3_api.h:1127
Z3_OP_PR_ASSUMPTION_ADD
@ Z3_OP_PR_ASSUMPTION_ADD
Definition z3_api.h:1143
Z3_OP_FPA_TO_UBV
@ Z3_OP_FPA_TO_UBV
Definition z3_api.h:1306
Z3_OP_FPA_LT
@ Z3_OP_FPA_LT
Definition z3_api.h:1291
Z3_OP_BMUL
@ Z3_OP_BMUL
Definition z3_api.h:1046
Z3_OP_PR_TRANSITIVITY_STAR
@ Z3_OP_PR_TRANSITIVITY_STAR
Definition z3_api.h:1122
Z3_OP_PB_LE
@ Z3_OP_PB_LE
Definition z3_api.h:1250
Z3_OP_FF_ADD
@ Z3_OP_FF_ADD
Definition z3_api.h:1336
Z3_OP_PB_AT_MOST
@ Z3_OP_PB_AT_MOST
Definition z3_api.h:1248
Z3_OP_CHAR_TO_INT
@ Z3_OP_CHAR_TO_INT
Definition z3_api.h:1231
Z3_OP_FPA_IS_NORMAL
@ Z3_OP_FPA_IS_NORMAL
Definition z3_api.h:1298
Z3_OP_ULT
@ Z3_OP_ULT
Definition z3_api.h:1066
Z3_OP_STORE
@ Z3_OP_STORE
Definition z3_api.h:1026
Z3_OP_SGT
@ Z3_OP_SGT
Definition z3_api.h:1069
Z3_OP_STR_FROM_CODE
@ Z3_OP_STR_FROM_CODE
Definition z3_api.h:1205
Z3_OP_CARRY
@ Z3_OP_CARRY
Definition z3_api.h:1101
Z3_OP_DT_CONSTRUCTOR
@ Z3_OP_DT_CONSTRUCTOR
Definition z3_api.h:1241
Z3_OP_BIT0
@ Z3_OP_BIT0
Definition z3_api.h:1042
Z3_OP_CHAR_FROM_BV
@ Z3_OP_CHAR_FROM_BV
Definition z3_api.h:1233
Z3_OP_CHAR_IS_DIGIT
@ Z3_OP_CHAR_IS_DIGIT
Definition z3_api.h:1234
Z3_OP_RE_FULL_CHAR_SET
@ Z3_OP_RE_FULL_CHAR_SET
Definition z3_api.h:1223
Z3_OP_FF_MUL
@ Z3_OP_FF_MUL
Definition z3_api.h:1337
Z3_OP_FINITE_SET_EMPTY
@ Z3_OP_FINITE_SET_EMPTY
Definition z3_api.h:1316
Z3_OP_BUREM
@ Z3_OP_BUREM
Definition z3_api.h:1051
Z3_OP_SEQ_PREFIX
@ Z3_OP_SEQ_PREFIX
Definition z3_api.h:1178
Z3_OP_SEQ_FOLDL
@ Z3_OP_SEQ_FOLDL
Definition z3_api.h:1195
Z3_OP_FPA_FP
@ Z3_OP_FPA_FP
Definition z3_api.h:1303
Z3_OP_SEQ_REPLACE_RE_ALL
@ Z3_OP_SEQ_REPLACE_RE_ALL
Definition z3_api.h:1184
Z3_OP_BREDOR
@ Z3_OP_BREDOR
Definition z3_api.h:1085
Z3_OP_BSREM0
@ Z3_OP_BSREM0
Definition z3_api.h:1058
Z3_OP_LE
@ Z3_OP_LE
Definition z3_api.h:1007
Z3_OP_SPECIAL_RELATION_LO
@ Z3_OP_SPECIAL_RELATION_LO
Definition z3_api.h:1255
Z3_OP_BSDIV_I
@ Z3_OP_BSDIV_I
Definition z3_api.h:1107
Z3_OP_PR_DISTRIBUTIVITY
@ Z3_OP_PR_DISTRIBUTIVITY
Definition z3_api.h:1126
Z3_OP_FPA_TO_IEEE_BV
@ Z3_OP_FPA_TO_IEEE_BV
Definition z3_api.h:1310
Z3_OP_IDIV
@ Z3_OP_IDIV
Definition z3_api.h:1016
Z3_OP_SEQ_TO_RE
@ Z3_OP_SEQ_TO_RE
Definition z3_api.h:1191
Z3_OP_ANUM
@ Z3_OP_ANUM
Definition z3_api.h:1005
Z3_OP_FF_NUM
@ Z3_OP_FF_NUM
Definition z3_api.h:1335
Z3_OP_RE_STAR
@ Z3_OP_RE_STAR
Definition z3_api.h:1211
Z3_OP_BAND
@ Z3_OP_BAND
Definition z3_api.h:1071
Z3_OP_ARRAY_DEFAULT
@ Z3_OP_ARRAY_DEFAULT
Definition z3_api.h:1030
Z3_OP_TRUE
@ Z3_OP_TRUE
Definition z3_api.h:991
Z3_PK_DOUBLE
@ Z3_PK_DOUBLE
Definition z3_api.h:1357
Z3_PK_SYMBOL
@ Z3_PK_SYMBOL
Definition z3_api.h:1358
Z3_PK_BOOL
@ Z3_PK_BOOL
Definition z3_api.h:1356
Z3_PK_OTHER
@ Z3_PK_OTHER
Definition z3_api.h:1360
Z3_PK_UINT
@ Z3_PK_UINT
Definition z3_api.h:1355
Z3_PK_INVALID
@ Z3_PK_INVALID
Definition z3_api.h:1361
Z3_PK_STRING
@ Z3_PK_STRING
Definition z3_api.h:1359
Z3_RELATION_SORT
@ Z3_RELATION_SORT
Definition z3_api.h:118
Z3_BOOL_SORT
@ Z3_BOOL_SORT
Definition z3_api.h:112
Z3_TYPE_VAR
@ Z3_TYPE_VAR
Definition z3_api.h:125
Z3_ROUNDING_MODE_SORT
@ Z3_ROUNDING_MODE_SORT
Definition z3_api.h:121
Z3_UNKNOWN_SORT
@ Z3_UNKNOWN_SORT
Definition z3_api.h:127
Z3_BV_SORT
@ Z3_BV_SORT
Definition z3_api.h:115
Z3_DATATYPE_SORT
@ Z3_DATATYPE_SORT
Definition z3_api.h:117
Z3_INT_SORT
@ Z3_INT_SORT
Definition z3_api.h:113
Z3_FINITE_DOMAIN_SORT
@ Z3_FINITE_DOMAIN_SORT
Definition z3_api.h:119
Z3_RE_SORT
@ Z3_RE_SORT
Definition z3_api.h:123
Z3_UNINTERPRETED_SORT
@ Z3_UNINTERPRETED_SORT
Definition z3_api.h:111
Z3_FINITE_FIELD_SORT
@ Z3_FINITE_FIELD_SORT
Definition z3_api.h:126
Z3_FLOATING_POINT_SORT
@ Z3_FLOATING_POINT_SORT
Definition z3_api.h:120
Z3_ARRAY_SORT
@ Z3_ARRAY_SORT
Definition z3_api.h:116
Z3_CHAR_SORT
@ Z3_CHAR_SORT
Definition z3_api.h:124
Z3_REAL_SORT
@ Z3_REAL_SORT
Definition z3_api.h:114
Z3_SEQ_SORT
@ Z3_SEQ_SORT
Definition z3_api.h:122
Z3_L_TRUE
@ Z3_L_TRUE
Definition z3_api.h:61
Z3_L_FALSE
@ Z3_L_FALSE
Definition z3_api.h:59
Z3_L_UNDEF
@ Z3_L_UNDEF
Definition z3_api.h:60
Z3_PARAMETER_INT
@ Z3_PARAMETER_INT
Definition z3_api.h:95
Z3_PARAMETER_FUNC_DECL
@ Z3_PARAMETER_FUNC_DECL
Definition z3_api.h:101
Z3_PARAMETER_INTERNAL
@ Z3_PARAMETER_INTERNAL
Definition z3_api.h:102
Z3_PARAMETER_ZSTRING
@ Z3_PARAMETER_ZSTRING
Definition z3_api.h:103
Z3_PARAMETER_SORT
@ Z3_PARAMETER_SORT
Definition z3_api.h:99
Z3_PARAMETER_RATIONAL
@ Z3_PARAMETER_RATIONAL
Definition z3_api.h:97
Z3_PARAMETER_AST
@ Z3_PARAMETER_AST
Definition z3_api.h:100
Z3_PARAMETER_DOUBLE
@ Z3_PARAMETER_DOUBLE
Definition z3_api.h:96
Z3_PARAMETER_SYMBOL
@ Z3_PARAMETER_SYMBOL
Definition z3_api.h:98
Z3_STRING_SYMBOL
@ Z3_STRING_SYMBOL
Definition z3_api.h:74
Z3_INT_SYMBOL
@ Z3_INT_SYMBOL
Definition z3_api.h:73
Z3_INTERNAL_FATAL
@ Z3_INTERNAL_FATAL
Definition z3_api.h:1406
Z3_DEC_REF_ERROR
@ Z3_DEC_REF_ERROR
Definition z3_api.h:1408
Z3_INVALID_USAGE
@ Z3_INVALID_USAGE
Definition z3_api.h:1407
Z3_INVALID_PATTERN
@ Z3_INVALID_PATTERN
Definition z3_api.h:1403
Z3_INVALID_ARG
@ Z3_INVALID_ARG
Definition z3_api.h:1400
Z3_OK
@ Z3_OK
Definition z3_api.h:1397
Z3_IOB
@ Z3_IOB
Definition z3_api.h:1399
Z3_FILE_ACCESS_ERROR
@ Z3_FILE_ACCESS_ERROR
Definition z3_api.h:1405
Z3_PARSER_ERROR
@ Z3_PARSER_ERROR
Definition z3_api.h:1401
Z3_EXCEPTION
@ Z3_EXCEPTION
Definition z3_api.h:1409
Z3_SORT_ERROR
@ Z3_SORT_ERROR
Definition z3_api.h:1398
Z3_MEMOUT_FAIL
@ Z3_MEMOUT_FAIL
Definition z3_api.h:1404
Z3_NO_PARSER
@ Z3_NO_PARSER
Definition z3_api.h:1402
Generated by doxygen 1.18.0