13 #define Z3_sort_opt Z3_sort 16 #define Z3_ast_opt Z3_ast 33 #define Z3_func_interp_opt Z3_func_interp 40 #define __int64 long long 44 #define __uint64 unsigned long long 1361 #endif // __cplusplus 1538 void Z3_API
Z3_inc_ref(Z3_context c, Z3_ast a);
1546 void Z3_API
Z3_dec_ref(Z3_context c, Z3_ast a);
1785 Z3_sort Z3_API
Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range);
1803 Z3_symbol mk_tuple_name,
1804 unsigned num_fields,
1805 Z3_symbol
const field_names[],
1806 Z3_sort
const field_sorts[],
1807 Z3_func_decl * mk_tuple_decl,
1808 Z3_func_decl proj_decl[]);
1833 Z3_symbol
const enum_names[],
1834 Z3_func_decl enum_consts[],
1835 Z3_func_decl enum_testers[]);
1857 Z3_func_decl* nil_decl,
1858 Z3_func_decl* is_nil_decl,
1859 Z3_func_decl* cons_decl,
1860 Z3_func_decl* is_cons_decl,
1861 Z3_func_decl* head_decl,
1862 Z3_func_decl* tail_decl
1881 Z3_symbol recognizer,
1882 unsigned num_fields,
1883 Z3_symbol
const field_names[],
1885 unsigned sort_refs[]
1909 unsigned num_constructors,
1910 Z3_constructor constructors[]);
1921 unsigned num_constructors,
1922 Z3_constructor
const constructors[]);
1947 Z3_symbol
const sort_names[],
1949 Z3_constructor_list constructor_lists[]);
1963 Z3_constructor constr,
1964 unsigned num_fields,
1965 Z3_func_decl* constructor,
1966 Z3_func_decl* tester,
1967 Z3_func_decl accessors[]);
1991 unsigned domain_size, Z3_sort
const domain[],
2005 Z3_ast
const args[]);
2020 Z3_ast Z3_API
Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty);
2034 unsigned domain_size, Z3_sort
const domain[],
2072 Z3_ast Z3_API
Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r);
2085 Z3_ast Z3_API
Z3_mk_distinct(Z3_context c,
unsigned num_args, Z3_ast
const args[]);
2093 Z3_ast Z3_API
Z3_mk_not(Z3_context c, Z3_ast a);
2102 Z3_ast Z3_API
Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3);
2110 Z3_ast Z3_API
Z3_mk_iff(Z3_context c, Z3_ast t1, Z3_ast t2);
2118 Z3_ast Z3_API
Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2);
2126 Z3_ast Z3_API
Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2);
2137 Z3_ast Z3_API
Z3_mk_and(Z3_context c,
unsigned num_args, Z3_ast
const args[]);
2148 Z3_ast Z3_API
Z3_mk_or(Z3_context c,
unsigned num_args, Z3_ast
const args[]);
2162 Z3_ast Z3_API
Z3_mk_add(Z3_context c,
unsigned num_args, Z3_ast
const args[]);
2174 Z3_ast Z3_API
Z3_mk_mul(Z3_context c,
unsigned num_args, Z3_ast
const args[]);
2185 Z3_ast Z3_API
Z3_mk_sub(Z3_context c,
unsigned num_args, Z3_ast
const args[]);
2203 Z3_ast Z3_API
Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2211 Z3_ast Z3_API
Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2219 Z3_ast Z3_API
Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2227 Z3_ast Z3_API
Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2235 Z3_ast Z3_API
Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2);
2243 Z3_ast Z3_API
Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2);
2251 Z3_ast Z3_API
Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2);
2259 Z3_ast Z3_API
Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2);
2309 Z3_ast Z3_API
Z3_mk_bvnot(Z3_context c, Z3_ast t1);
2333 Z3_ast Z3_API
Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2);
2341 Z3_ast Z3_API
Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2);
2349 Z3_ast Z3_API
Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2);
2357 Z3_ast Z3_API
Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2);
2365 Z3_ast Z3_API
Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2);
2373 Z3_ast Z3_API
Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2);
2381 Z3_ast Z3_API
Z3_mk_bvneg(Z3_context c, Z3_ast t1);
2389 Z3_ast Z3_API
Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2);
2397 Z3_ast Z3_API
Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2);
2405 Z3_ast Z3_API
Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2);
2417 Z3_ast Z3_API
Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2);
2433 Z3_ast Z3_API
Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2);
2445 Z3_ast Z3_API
Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2);
2460 Z3_ast Z3_API
Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2);
2472 Z3_ast Z3_API
Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2);
2480 Z3_ast Z3_API
Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2);
2496 Z3_ast Z3_API
Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2);
2504 Z3_ast Z3_API
Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2);
2512 Z3_ast Z3_API
Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2);
2520 Z3_ast Z3_API
Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2);
2528 Z3_ast Z3_API
Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2);
2536 Z3_ast Z3_API
Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2);
2544 Z3_ast Z3_API
Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2);
2555 Z3_ast Z3_API
Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2);
2564 Z3_ast Z3_API
Z3_mk_extract(Z3_context c,
unsigned high,
unsigned low, Z3_ast t1);
2574 Z3_ast Z3_API
Z3_mk_sign_ext(Z3_context c,
unsigned i, Z3_ast t1);
2584 Z3_ast Z3_API
Z3_mk_zero_ext(Z3_context c,
unsigned i, Z3_ast t1);
2592 Z3_ast Z3_API
Z3_mk_repeat(Z3_context c,
unsigned i, Z3_ast t1);
2607 Z3_ast Z3_API
Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2);
2622 Z3_ast Z3_API
Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2);
2638 Z3_ast Z3_API
Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2);
2682 Z3_ast Z3_API
Z3_mk_int2bv(Z3_context c,
unsigned n, Z3_ast t1);
2787 Z3_ast Z3_API
Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i);
2804 Z3_ast Z3_API
Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v);
2831 Z3_ast Z3_API
Z3_mk_map(Z3_context c, Z3_func_decl f,
unsigned n, Z3_ast
const* args);
2871 Z3_ast Z3_API
Z3_mk_set_add(Z3_context c, Z3_ast
set, Z3_ast elem);
2879 Z3_ast Z3_API
Z3_mk_set_del(Z3_context c, Z3_ast
set, Z3_ast elem);
2885 Z3_ast Z3_API
Z3_mk_set_union(Z3_context c,
unsigned num_args, Z3_ast
const args[]);
2926 Z3_ast Z3_API
Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2);
2943 Z3_ast Z3_API Z3_mk_numeral(Z3_context c,
Z3_string numeral, Z3_sort ty);
2959 Z3_ast Z3_API Z3_mk_real(Z3_context c,
int num,
int den);
2970 Z3_ast Z3_API Z3_mk_int(Z3_context c,
int v, Z3_sort ty);
2981 Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c,
unsigned v, Z3_sort ty);
2992 Z3_ast Z3_API Z3_mk_int64(Z3_context c,
__int64 v, Z3_sort ty);
3003 Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c,
unsigned __int64 v, Z3_sort ty);
3014 Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s);
3020 Z3_bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s);
3026 Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq);
3032 Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s);
3041 Z3_sort Z3_API Z3_mk_string_sort(Z3_context c);
3047 Z3_bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s);
3052 Z3_ast Z3_API Z3_mk_string(Z3_context c,
Z3_string s);
3058 Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s);
3066 Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s);
3074 Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq);
3080 Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a);
3088 Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c,
unsigned n, Z3_ast
const args[]);
3096 Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s);
3104 Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s);
3112 Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee);
3118 Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length);
3124 Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst);
3130 Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index);
3136 Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s);
3145 Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);
3151 Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq);
3157 Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re);
3163 Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re);
3169 Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re);
3175 Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re);
3183 Z3_ast Z3_API Z3_mk_re_union(Z3_context c,
unsigned n, Z3_ast
const args[]);
3191 Z3_ast Z3_API Z3_mk_re_concat(Z3_context c,
unsigned n, Z3_ast
const args[]);
3217 Z3_pattern Z3_API Z3_mk_pattern(Z3_context c,
unsigned num_patterns, Z3_ast
const terms[]);
3247 Z3_ast Z3_API Z3_mk_bound(Z3_context c,
unsigned index, Z3_sort ty);
3271 Z3_ast Z3_API Z3_mk_forall(Z3_context c,
unsigned weight,
3272 unsigned num_patterns, Z3_pattern
const patterns[],
3273 unsigned num_decls, Z3_sort
const sorts[],
3274 Z3_symbol
const decl_names[],
3286 Z3_ast Z3_API Z3_mk_exists(Z3_context c,
unsigned weight,
3287 unsigned num_patterns, Z3_pattern
const patterns[],
3288 unsigned num_decls, Z3_sort
const sorts[],
3289 Z3_symbol
const decl_names[],
3312 Z3_ast Z3_API Z3_mk_quantifier(
3316 unsigned num_patterns, Z3_pattern
const patterns[],
3317 unsigned num_decls, Z3_sort
const sorts[],
3318 Z3_symbol
const decl_names[],
3345 Z3_ast Z3_API Z3_mk_quantifier_ex(
3349 Z3_symbol quantifier_id,
3350 Z3_symbol skolem_id,
3351 unsigned num_patterns, Z3_pattern
const patterns[],
3352 unsigned num_no_patterns, Z3_ast
const no_patterns[],
3353 unsigned num_decls, Z3_sort
const sorts[],
3354 Z3_symbol
const decl_names[],
3374 Z3_ast Z3_API Z3_mk_forall_const(
3378 Z3_app
const bound[],
3379 unsigned num_patterns,
3380 Z3_pattern
const patterns[],
3403 Z3_ast Z3_API Z3_mk_exists_const(
3407 Z3_app
const bound[],
3408 unsigned num_patterns,
3409 Z3_pattern
const patterns[],
3418 Z3_ast Z3_API Z3_mk_quantifier_const(
3422 unsigned num_bound, Z3_app
const bound[],
3423 unsigned num_patterns, Z3_pattern
const patterns[],
3432 Z3_ast Z3_API Z3_mk_quantifier_const_ex(
3436 Z3_symbol quantifier_id,
3437 Z3_symbol skolem_id,
3438 unsigned num_bound, Z3_app
const bound[],
3439 unsigned num_patterns, Z3_pattern
const patterns[],
3440 unsigned num_no_patterns, Z3_ast
const no_patterns[],
3454 Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s);
3464 int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s);
3478 Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s);
3484 Z3_symbol Z3_API Z3_get_sort_name(Z3_context c, Z3_sort d);
3490 unsigned Z3_API Z3_get_sort_id(Z3_context c, Z3_sort s);
3496 Z3_ast Z3_API Z3_sort_to_ast(Z3_context c, Z3_sort s);
3502 Z3_bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2);
3510 Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t);
3521 unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t);
3528 Z3_bool_opt Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s,
unsigned __int64* r);
3539 Z3_sort Z3_API Z3_get_array_sort_domain(Z3_context c, Z3_sort t);
3550 Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t);
3562 Z3_func_decl Z3_API Z3_get_tuple_sort_mk_decl(Z3_context c, Z3_sort t);
3573 unsigned Z3_API Z3_get_tuple_sort_num_fields(Z3_context c, Z3_sort t);
3586 Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t,
unsigned i);
3598 unsigned Z3_API Z3_get_datatype_sort_num_constructors(
3599 Z3_context c, Z3_sort t);
3612 Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(
3613 Z3_context c, Z3_sort t,
unsigned idx);
3626 Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(
3627 Z3_context c, Z3_sort t,
unsigned idx);
3641 Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c,
3664 Z3_ast Z3_API Z3_datatype_update_field(Z3_context c, Z3_func_decl field_access,
3665 Z3_ast t, Z3_ast value);
3675 unsigned Z3_API Z3_get_relation_arity(Z3_context c, Z3_sort s);
3686 Z3_sort Z3_API Z3_get_relation_column(Z3_context c, Z3_sort s,
unsigned col);
3695 Z3_ast Z3_API Z3_mk_atmost(Z3_context c,
unsigned num_args,
3696 Z3_ast
const args[],
unsigned k);
3705 Z3_ast Z3_API Z3_mk_pble(Z3_context c,
unsigned num_args,
3706 Z3_ast
const args[],
int coeffs[],
3716 Z3_ast Z3_API Z3_mk_pbeq(Z3_context c,
unsigned num_args,
3717 Z3_ast
const args[],
int coeffs[],
3724 Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f);
3730 Z3_bool Z3_API Z3_is_eq_func_decl(Z3_context c, Z3_func_decl f1, Z3_func_decl f2);
3736 unsigned Z3_API Z3_get_func_decl_id(Z3_context c, Z3_func_decl f);
3742 Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d);
3748 Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d);
3756 unsigned Z3_API Z3_get_domain_size(Z3_context c, Z3_func_decl d);
3764 unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d);
3774 Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d,
unsigned i);
3783 Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d);
3789 unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d);
3799 Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d,
unsigned idx);
3807 int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d,
unsigned idx);
3815 double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d,
unsigned idx);
3823 Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d,
unsigned idx);
3831 Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d,
unsigned idx);
3839 Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d,
unsigned idx);
3847 Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d,
unsigned idx);
3855 Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d,
unsigned idx);
3861 Z3_ast Z3_API Z3_app_to_ast(Z3_context c, Z3_app a);
3867 Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a);
3874 unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a);
3882 Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a,
unsigned i);
3888 Z3_bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2);
3900 unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t);
3908 unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a);
3916 Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a);
3922 Z3_bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t);
3928 Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a);
3934 Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a);
3938 Z3_bool Z3_API Z3_is_app(Z3_context c, Z3_ast a);
3942 Z3_bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a);
3948 Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a);
3956 Z3_app Z3_API
Z3_to_app(Z3_context c, Z3_ast a);
4105 Z3_ast Z3_API
Z3_get_pattern(Z3_context c, Z3_pattern p,
unsigned idx);
4204 Z3_ast Z3_API
Z3_simplify(Z3_context c, Z3_ast a);
4214 Z3_ast Z3_API
Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p);
4238 Z3_ast Z3_API
Z3_update_term(Z3_context c, Z3_ast a,
unsigned num_args, Z3_ast
const args[]);
4249 Z3_ast
const from[],
4268 Z3_ast Z3_API
Z3_translate(Z3_context source, Z3_ast a, Z3_context target);
4307 Z3_bool_opt Z3_API
Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t,
Z3_bool model_completion, Z3_ast * v);
4629 unsigned num_assumptions,
4630 Z3_ast
const assumptions[],
4647 Z3_symbol
const sort_names[],
4648 Z3_sort
const sorts[],
4650 Z3_symbol
const decl_names[],
4651 Z3_func_decl
const decls[]);
4660 Z3_symbol
const sort_names[],
4661 Z3_sort
const sorts[],
4663 Z3_symbol
const decl_names[],
4664 Z3_func_decl
const decls[]);
4682 Z3_symbol
const sort_names[],
4683 Z3_sort
const sorts[],
4685 Z3_symbol
const decl_names[],
4686 Z3_func_decl
const decls[]
4696 Z3_symbol
const sort_names[],
4697 Z3_sort
const sorts[],
4699 Z3_symbol
const decl_names[],
4700 Z3_func_decl
const decls[]
4822 void Z3_API
Z3_get_version(
unsigned * major,
unsigned * minor,
unsigned * build_number,
unsigned * revision_number);
4965 Z3_goal Z3_API
Z3_goal_translate(Z3_context source, Z3_goal g, Z3_context target);
5040 Z3_tactic Z3_API
Z3_tactic_par_or(Z3_context c,
unsigned num, Z3_tactic
const ts[]);
5061 Z3_tactic Z3_API
Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t);
5068 Z3_tactic Z3_API
Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2);
5075 Z3_tactic Z3_API
Z3_tactic_repeat(Z3_context c, Z3_tactic t,
unsigned max);
5120 Z3_probe Z3_API
Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2);
5128 Z3_probe Z3_API
Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2);
5136 Z3_probe Z3_API
Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2);
5144 Z3_probe Z3_API
Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2);
5152 Z3_probe Z3_API
Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2);
5160 Z3_probe Z3_API
Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2);
5168 Z3_probe Z3_API
Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2);
5176 Z3_probe Z3_API
Z3_probe_not(Z3_context x, Z3_probe p);
5235 double Z3_API
Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g);
5241 Z3_apply_result Z3_API
Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g);
5247 Z3_apply_result Z3_API
Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p);
5394 void Z3_API
Z3_solver_pop(Z3_context c, Z3_solver s,
unsigned n);
5469 unsigned num_assumptions, Z3_ast
const assumptions[]);
5491 Z3_ast
const terms[],
5492 unsigned class_ids[]);
5501 Z3_ast_vector assumptions,
5502 Z3_ast_vector variables,
5503 Z3_ast_vector consequences);
5630 #endif // __cplusplus Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences)
retrieve consequences from solver that determine values of the supplied function symbols.
Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...
Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i)
Return the name of the i probe.
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Z3_ast Z3_API Z3_mk_real2int(Z3_context c, Z3_ast t1)
Coerce a real to an integer.
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
Z3_bool Z3_API Z3_open_log(Z3_string filename)
Log interaction to a file.
Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a fresh constant or function.
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
Z3_sort Z3_API Z3_model_get_sort(Z3_context c, Z3_model m, unsigned i)
Return a uninterpreted sort that m assigns an interpretation.
Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f)
Return the arity (number of arguments) of the given function interpretation.
void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr)
Reclaim memory allocated to constructor.
Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c, Z3_symbol mk_tuple_name, unsigned num_fields, Z3_symbol const field_names[], Z3_sort const field_sorts[], Z3_func_decl *mk_tuple_decl, Z3_func_decl proj_decl[])
Create a tuple type.
Z3_tactic Z3_API Z3_tactic_fail_if_not_decided(Z3_context c)
Return a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsati...
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err)
Return a string describing the given error code.
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
Z3_ast Z3_API Z3_pattern_to_ast(Z3_context c, Z3_pattern p)
Convert a Z3_pattern into Z3_ast. This is just type casting.
Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s)
Retrieve documentation string corresponding to parameter name s.
void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.
unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g)
Return the number of formulas, subformulas and terms in the given goal.
__uint64 Z3_API Z3_get_estimated_alloc_size(void)
Return the estimated allocated memory in bytes.
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)
Erase all formulas from the given goal.
Z3_params Z3_API Z3_mk_params(Z3_context c)
Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many comp...
Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1...
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s)
Return the finite set of distinct values that represent the interpretation for sort s...
void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v)
Add a unsigned parameter k with value v to the parameter set p.
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i)
Return the declaration of the i-th function in the given model.
Z3_sort Z3_API Z3_get_smtlib_sort(Z3_context c, unsigned i)
Return the i-th sort parsed by the last call to Z3_parse_smtlib_string or Z3_parse_smtlib_file.
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g)
Return the depth of the given goal. It tracks how many transformations were applied to it...
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx)
Return a formula from the given goal.
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
void Z3_API Z3_set_error(Z3_context c, Z3_error_code e)
Set an error.
Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t)
Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
Z3_bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx)
Return Z3_TRUE if the given statistical data is a double.
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
void Z3_API Z3_del_context(Z3_context c)
Delete the given logical context.
unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)
Return the number of formulas in the given goal.
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
Z3_sort Z3_API Z3_mk_datatype(Z3_context c, Z3_symbol name, unsigned num_constructors, Z3_constructor constructors[])
Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.
Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)
Remove an element to a set.
Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the union of a list of sets.
Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i)
Return the i-th constant in the given model.
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i)
Return the number of parameters in the given parameter description set.
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create array extensionality index given two arrays with the same sort. The meaning is given by the ax...
Z3_error_code
Z3 error codes (See Z3_get_error_code).
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].
Z3_ast Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.
Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
Z3_bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g)
Return true if the goal contains false, and it is precise or the product of an over approximation...
Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i)
Return an argument of a Z3_func_entry object.
int Z3_bool
Z3 Boolean type. It is just an alias for int.
double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx)
Return the double value of the given statistical data.
Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a)
Return the function declaration f associated with a (_ as_array f) node.
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m)
Return the number of uninterpreted sorts that m assigs an interpretation to.
Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s)
Check whether the assertions in a given solver are consistent or not.
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
void Z3_API Z3_close_log(void)
Close interaction log.
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r)
Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
Z3_bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g)
Return true if the goal is empty, and it is precise or the product of a under approximation.
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
Z3_ast Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Parse the given string using the SMT-LIB2 parser.
Z3_context Z3_API Z3_mk_context_rc(Z3_config c)
Create a context using the given configuration. This function is similar to Z3_mk_context. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.
void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value)
Set a value of a context parameter.
Z3_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s)
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
Z3_ast Z3_API Z3_mk_ext_rotate_right(Z3_context c, Z3_ast t1, Z3_ast t2)
Rotate bits of t1 to the right t2 times.
void Z3_API Z3_reset_memory(void)
Reset all allocated resources.
Z3_sort Z3_API Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, unsigned i)
Return sort of the i'th bound variable.
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
unsigned Z3_API Z3_get_smtlib_num_decls(Z3_context c)
Return the number of declarations parsed by Z3_parse_smtlib_string or Z3_parse_smtlib_file.
Z3_string Z3_API Z3_get_smtlib_error(Z3_context c)
Retrieve that last error message information generated from parsing.
Z3_sort Z3_API Z3_mk_list_sort(Z3_context c, Z3_symbol name, Z3_sort elem_sort, Z3_func_decl *nil_decl, Z3_func_decl *is_nil_decl, Z3_func_decl *cons_decl, Z3_func_decl *is_cons_decl, Z3_func_decl *head_decl, Z3_func_decl *tail_decl)
Create a list sort.
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)
Return the parameter description set for the given solver object.
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not...
void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c, Z3_solver s, unsigned num_terms, Z3_ast const terms[], unsigned class_ids[])
Retrieve congruence class representatives for terms.
Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 and p2 evaluates to true.
Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i)
Return the name of the idx tactic.
Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the intersection of a list of sets.
Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array)
Access the array default value. Produces the default range value, for arrays that can be represented ...
Z3_string Z3_API Z3_pattern_to_string(Z3_context c, Z3_pattern p)
Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, Z3_bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...
unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx)
Return the unsigned value of the given statistical data.
Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p)
Convert a parameter description set into a string. This function is mainly used for printing the cont...
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
Z3_string * Z3_string_ptr
void Z3_API Z3_append_log(Z3_string string)
Append user-defined string to interaction log.
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a)
Return index of de-Brujin bound variable.
unsigned Z3_API Z3_get_pattern_num_terms(Z3_context c, Z3_pattern p)
Return number of terms in pattern.
Z3_error_code Z3_API Z3_get_error_code(Z3_context c)
Return the error code for the last API call.
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow...
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s)
Return the number of backtracking points.
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g)
Return the "precision" of the given goal. Goals can be transformed using over and under approximation...
void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist)
Reclaim memory allocated for constructor list.
Z3_constructor Z3_API Z3_mk_constructor(Z3_context c, Z3_symbol name, Z3_symbol recognizer, unsigned num_fields, Z3_symbol const field_names[], Z3_sort_opt const sorts[], unsigned sort_refs[])
Create a constructor.
Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, unsigned __int64 *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned __int6...
Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Take the set difference between two sets.
void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode)
Select mode for the format used for pretty-printing AST nodes.
Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, unsigned __int64 size)
Create a named finite domain sort.
Z3_context Z3_API Z3_mk_context(Z3_config c)
Create a context using the given configuration.
Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows dividend).
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a)
Convert an AST into a FUNC_DECL_AST. This is just type casting.
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
#define Z3_func_interp_opt
Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...
void Z3_API Z3_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p)
Increment the reference counter of the given parameter description set.
Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f)
Return the 'else' value of the given function interpretation.
Z3_ast Z3_API Z3_mk_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2)
Rotate bits of t1 to the left t2 times.
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
Z3_ast Z3_API Z3_update_term(Z3_context c, Z3_ast a, unsigned num_args, Z3_ast const args[])
Update the arguments of term a using the arguments args. The number of arguments num_args should coin...
unsigned Z3_API Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a)
Return number of bound variables of quantifier.
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry object.
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
void Z3_API Z3_del_config(Z3_config c)
Delete the given configuration object.
Z3_bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int...
Z3_string Z3_API Z3_probe_get_descr(Z3_context c, Z3_string name)
Return a string containing a description of the probe with the given name.
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs...
Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th no_pattern.
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
unsigned Z3_API Z3_get_smtlib_num_formulas(Z3_context c)
Return the number of SMTLIB formulas parsed by the last call to Z3_parse_smtlib_string or Z3_parse_sm...
Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than or equal to.
Z3_pattern Z3_API Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, unsigned i)
Return i'th pattern.
Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)
Add an element to a set.
Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p)
Return a tactic that applies t using the given set of parameters.
Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 or p2 evaluates to true.
Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.
Z3_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p)
Convert a parameter set into a string. This function is mainly used for printing the contents of a pa...
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than or equal to.
Z3_goal Z3_API Z3_mk_goal(Z3_context c, Z3_bool models, Z3_bool unsat_cores, Z3_bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
Z3_lbool
Lifted Boolean type: false, undefined, true.
void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a)
Add a new formula a to the given goal.
Z3_app Z3_API Z3_to_app(Z3_context c, Z3_ast a)
Create a numeral of a given sort.
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.
Z3_tactic Z3_API Z3_tactic_fail(Z3_context c)
Return a tactic that always fails.
void Z3_API Z3_finalize_memory(void)
Destroy all allocated resources.
void Z3_API Z3_disable_trace(Z3_string tag)
Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
unsigned Z3_API Z3_get_smtlib_num_assumptions(Z3_context c)
Return the number of SMTLIB assumptions parsed by Z3_parse_smtlib_string or Z3_parse_smtlib_file.
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h)
Register a Z3 error handler.
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.
Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1)
Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size m+i...
Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f)
Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...
Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p)
Apply tactic t to the goal g using the parameter set p.
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the right i times.
unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p)
Return the number of parameters in the given parameter description set.
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)
Decrement the reference counter of the given goal.
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.
Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL...
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
Z3_string Z3_API Z3_get_full_version(void)
Return a string that fully describes the version of Z3 in use.
Z3_func_decl Z3_API Z3_get_smtlib_decl(Z3_context c, unsigned i)
Return the i-th declaration parsed by the last call to Z3_parse_smtlib_string or Z3_parse_smtlib_file...
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)
Decrement the reference counter of the given parameter set.
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...
void Z3_API Z3_toggle_warning_messages(Z3_bool enabled)
Enable/disable printing warning messages to the console.
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
Z3_bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, __int64 *num, __int64 *den)
Return numeral value, as a pair of 64 bit numbers if the representation fits.
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
Z3_string Z3_API Z3_get_error_msg_ex(Z3_context c, Z3_error_code err)
Return a string describing the given error code. Retained function name for backwards compatibility w...
Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
Z3_param_kind
The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params)...
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a string of a numeric constant term.
Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
Z3_ast Z3_API Z3_get_smtlib_assumption(Z3_context c, unsigned i)
Return the i-th assumption parsed by the last call to Z3_parse_smtlib_string or Z3_parse_smtlib_file...
Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded, and store the result in v...
unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
void Z3_API Z3_parse_smtlib_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Parse the given string using the SMT-LIB parser.
Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...
Z3_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See #Z3...
Z3_bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Test if there exists an interpretation (i.e., assignment) for a in the model m.
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_ast Z3_API Z3_get_pattern(Z3_context c, Z3_pattern p, unsigned idx)
Return i'th ast in pattern.
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
unsigned Z3_API Z3_get_smtlib_num_sorts(Z3_context c)
Return the number of sorts parsed by Z3_parse_smtlib_string or Z3_parse_smtlib_file.
Z3_bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return Z3_TRUE if the given statistical data is a unsigned integer.
unsigned Z3_API Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a)
Return number of patterns used in quantifier.
void Z3_API Z3_interrupt(Z3_context c)
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers...
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow...
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new (incremental) solver.
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow...
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1)
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector...
Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t)
Return the parameter description set for the given tactic object.
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
Z3_goal Z3_API Z3_goal_translate(Z3_context source, Z3_goal g, Z3_context target)
Copy a goal g from the context source to a the context target.
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places...
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
unsigned Z3_API Z3_get_quantifier_weight(Z3_context c, Z3_ast a)
Obtain weight of quantifier.
Z3_symbol Z3_API Z3_get_quantifier_bound_name(Z3_context c, Z3_ast a, unsigned i)
Return symbol of the i'th bound variable.
Z3_tactic Z3_API Z3_tactic_skip(Z3_context c)
Return a tactic that just return the given goal.
unsigned Z3_API Z3_get_num_tactics(Z3_context c)
Return the number of builtin tactics available in Z3.
Z3_config Z3_API Z3_mk_config(void)
Create a configuration object for the Z3 context object.
Z3_string Z3_API Z3_tactic_get_descr(Z3_context c, Z3_string name)
Return a string containing a description of the tactic with the given name.
double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0...
Z3_bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if quantifier is universal.
Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target)
Copy a solver s from the context source to a the context target.
void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.
Z3_bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int...
void Z3_API Z3_params_validate(Z3_context c, Z3_params p, Z3_param_descrs d)
Validate the parameter set p against the parameter description set d.
void Z3_API Z3_mk_datatypes(Z3_context c, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort sorts[], Z3_constructor_list constructor_lists[])
Create mutually recursive datatypes.
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].
unsigned Z3_API Z3_get_num_probes(Z3_context c)
Return the number of builtin probes available in Z3.
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value)
Set a configuration parameter.
Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
void Z3_API Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v)
Add a double parameter k with value v to the parameter set p.
Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision)
Return a upper bound for the given real algebraic number. The interval isolating the number is smalle...
Z3_ast Z3_API Z3_get_smtlib_formula(Z3_context c, unsigned i)
Return the i-th formula parsed by the last call to Z3_parse_smtlib_string or Z3_parse_smtlib_file.
Z3_param_kind Z3_API Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n)
Return the kind associated with the given parameter name n.
Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
Z3_sort Z3_API Z3_mk_set_sort(Z3_context c, Z3_sort ty)
Create Set type.
Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a)
Return number of no_patterns used in quantifier.
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target)
Translate/Copy the AST a from context source to context target. AST a must have been created using co...
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow...
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p...
void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v)
Add a symbol parameter k with value v to the parameter set p.
void Z3_API Z3_global_param_reset_all(void)
Restore the value of all global (and module) parameters. This command will not affect already created...
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
Z3_string Z3_API Z3_simplify_get_help(Z3_context c)
Return a string describing all available parameters.
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i)
Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
void Z3_error_handler(Z3_context c, Z3_error_code e)
Z3 custom error handler (See Z3_set_error_handler).
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
Z3_bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a)
The (_ as-array f) AST node is a construct for assigning interpretations for arrays in Z3...
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_solver Z3_API Z3_mk_solver(Z3_context c)
Create a new (incremental) solver. This solver also uses a set of builtin tactics for handling the fi...
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)
Return the number of entries in the given function interpretation.
Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1)
Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n...
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
void Z3_API Z3_enable_trace(Z3_string tag)
Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise...
Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx)
Return the key (a string) for a particular statistical data.
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision)
Return a lower bound for the given real algebraic number. The interval isolating the number is smalle...
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...
Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i)
Return a "point" of the given function intepretation. It represents the value of f in a particular po...
Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, unsigned num_assumptions, Z3_ast const assumptions[], Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the left i times.
Z3_string Z3_API Z3_func_decl_to_string(Z3_context c, Z3_func_decl d)
void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, Z3_bool v)
Add a Boolean parameter k with value v to the parameter set p.
void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)
Return Z3 version number information.
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t)
Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...
Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, unsigned num_constructors, Z3_constructor const constructors[])
Create list of constructors.
void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...
Z3_bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, __int64 *num, __int64 *den)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit as a rational number as mach...
void Z3_API Z3_query_constructor(Z3_context c, Z3_constructor constr, unsigned num_fields, Z3_func_decl *constructor, Z3_func_decl *tester, Z3_func_decl accessors[])
Query constructor for declared functions.
Z3_bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.
Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const *args)
Map f on the argument arrays.
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value)
Get a global (or module) parameter.
void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...
Z3_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, __int64 *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine __int64 int...
void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e)
Decrement the reference counter of the given Z3_func_entry object.
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
Z3_decl_kind
The different kinds of interpreted function kinds.
Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read...
Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.
void Z3_API Z3_parse_smtlib_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Similar to Z3_parse_smtlib_string, but reads the benchmark from a file.
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow...
Z3_ast Z3_API Z3_mk_iff(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 iff t2.
Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.
Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])
Create a enumeration sort.
void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p)
Decrement the reference counter of the given parameter description set.
Z3_model Z3_API Z3_apply_result_convert_model(Z3_context c, Z3_apply_result r, unsigned i, Z3_model m)
Convert a model for the subgoal Z3_apply_result_get_subgoal(c, r, i) into a model for the original go...
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.
Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1...
Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1)
Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i...
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.