module

Z3::API

Constants

Context = begin context = LibZ3.mk_context(LibZ3.mk_config) LibZ3.set_error_handler(context, ->(_context : LibZ3::Context, _code : LibZ3::ErrorCode) do end) context end

Z3's own error handler prints the message to stderr and lets the failed call hand back a null pointer, so the program carries on with a null AST inside an expression. This one does nothing at all, leaving the error code set for checked to raise on - a Crystal exception can't be thrown out of a C callback and back through Z3's own frames.

Instance methods

add_rec_def(decl, args, body)

app_args(ast)

The arguments of an application, so a term like a == 2 can be taken apart. Anything which isn't an application has no arguments. TODO: this becomes much less ad hoc once we have a real printer

ast_to_string(*args)

const_decl(expr)

The decl of a variable - a in a + 1 - which is what Z3 wants wherever it talks about one. Anything else is a term rather than a variable, and the two calls which take one (set_initial_value, model_has_interp) both mean this.

fpa_get_ebits(*args)

fpa_get_numeral_exponent_bv(*args)

fpa_get_numeral_exponent_string(*args)

fpa_get_numeral_sign_bv(*args)

fpa_get_numeral_significand_bv(*args)

fpa_get_numeral_significand_string(*args)

fpa_get_sbits(*args)

fpa_is_numeral(*args)

fpa_is_numeral_inf(*args)

fpa_is_numeral_nan(*args)

fpa_is_numeral_negative(*args)

fpa_is_numeral_zero(*args)

func_entry_dec_ref(*args)

func_entry_get_arg(*args)

func_entry_get_num_args(*args)

func_entry_get_value(*args)

func_entry_inc_ref(*args)

func_interp_dec_ref(*args)

func_interp_get_arity(*args)

func_interp_get_else(*args)

func_interp_get_entry(*args)

func_interp_get_num_entries(*args)

func_interp_inc_ref(*args)

get_algebraic_number_lower(*args)

get_algebraic_number_upper(*args)

get_app_decl(*args)

get_arity(*args)

get_ast_kind(*args)

get_bool_value(*args)

get_decl_kind(*args)

get_decl_name(decl)

get_domain(*args)

get_numeral_string(*args)

get_range(*args)

get_string(ast)

is_algebraic_number(*args)

is_eq_ast(*args)

is_string(*args)

mk_abs(*args)

mk_add(asts)

mk_and(asts)

mk_app(decl, args)

mk_atleast(asts, k : UInt32)

mk_atmost(asts, k : UInt32)

mk_bit2bool(*args)

mk_bv2int(*args)

mk_bvadd(*args)

mk_bvadd_no_overflow(*args)

mk_bvadd_no_underflow(*args)

mk_bvand(*args)

mk_bvashr(*args)

mk_bvlshr(*args)

mk_bvmul(*args)

mk_bvmul_no_overflow(*args)

mk_bvmul_no_underflow(*args)

mk_bvnand(*args)

mk_bvneg(*args)

mk_bvneg_no_overflow(*args)

mk_bvnor(*args)

mk_bvnot(*args)

mk_bvor(*args)

mk_bvredand(*args)

mk_bvredor(*args)

mk_bvsdiv(*args)

mk_bvsdiv_no_overflow(*args)

mk_bvsge(*args)

mk_bvsgt(*args)

mk_bvshl(*args)

mk_bvsle(*args)

mk_bvslt(*args)

mk_bvsmod(*args)

mk_bvsrem(*args)

mk_bvsub(*args)

mk_bvsub_no_overflow(*args)

mk_bvsub_no_underflow(*args)

mk_bvudiv(*args)

mk_bvuge(*args)

mk_bvugt(*args)

mk_bvule(*args)

mk_bvult(*args)

mk_bvurem(*args)

mk_bvxnor(*args)

mk_bvxor(*args)

mk_char(*args)

mk_char_from_bv(*args)

mk_char_is_digit(*args)

mk_char_le(*args)

mk_char_to_bv(*args)

mk_char_to_int(*args)

mk_concat(*args)

mk_const(name, sort)

mk_distinct(asts)

mk_div(*args)

mk_divides(*args)

mk_eq(*args)

mk_ext_rotate_left(*args)

mk_ext_rotate_right(*args)

mk_extract(*args)

mk_false(*args)

mk_fpa_abs(*args)

mk_fpa_add(*args)

mk_fpa_div(*args)

mk_fpa_eq(*args)

mk_fpa_fma(*args)

mk_fpa_fp(*args)

mk_fpa_geq(*args)

mk_fpa_gt(*args)

mk_fpa_inf(*args)

mk_fpa_is_infinite(*args)

mk_fpa_is_nan(*args)

mk_fpa_is_negative(*args)

mk_fpa_is_normal(*args)

mk_fpa_is_positive(*args)

mk_fpa_is_subnormal(*args)

mk_fpa_is_zero(*args)

mk_fpa_leq(*args)

mk_fpa_lt(*args)

mk_fpa_max(*args)

mk_fpa_min(*args)

mk_fpa_mul(*args)

mk_fpa_nan(*args)

mk_fpa_neg(*args)

mk_fpa_numeral_double(*args)

mk_fpa_rem(*args)

mk_fpa_round_nearest_ties_to_away(*args)

mk_fpa_round_nearest_ties_to_even(*args)

mk_fpa_round_to_integral(*args)

mk_fpa_round_toward_negative(*args)

mk_fpa_round_toward_positive(*args)

mk_fpa_round_toward_zero(*args)

mk_fpa_sort(*args)

mk_fpa_sqrt(*args)

mk_fpa_sub(*args)

mk_fpa_to_fp_bv(*args)

mk_fpa_to_fp_float(*args)

mk_fpa_to_fp_int_real(*args)

mk_fpa_to_fp_real(*args)

mk_fpa_to_fp_signed(*args)

mk_fpa_to_fp_unsigned(*args)

mk_fpa_to_ieee_bv(*args)

mk_fpa_to_real(*args)

mk_fpa_to_sbv(*args)

mk_fpa_to_ubv(*args)

mk_fpa_zero(*args)

mk_fresh_const(prefix : String, sort)

mk_fresh_func_decl(prefix : String, domain : Array(LibZ3::Sort), range : LibZ3::Sort)

mk_func_decl(name : String, domain : Array(LibZ3::Sort), range : LibZ3::Sort)

mk_ge(*args)

mk_gt(*args)

mk_iff(*args)

mk_implies(*args)

mk_int2bv(*args)

mk_int2real(*args)

mk_int_to_str(*args)

mk_is_int(*args)

mk_ite(*args)

mk_le(*args)

mk_lt(*args)

mk_mod(*args)

mk_mul(asts)

mk_ne(a, b)

Not a real Z3 function

mk_not(*args)

mk_numeral(num : Int | BigRational | Float, sort)

mk_optimize(*args)

mk_or(asts)

mk_pbeq(asts, coeffs : Array(Int32), k : Int32)

mk_pbge(asts, coeffs : Array(Int32), k : Int32)

mk_pble(asts, coeffs : Array(Int32), k : Int32)

mk_power(*args)

mk_real2int(*args)

mk_rec_func_decl(name : String, domain : Array(LibZ3::Sort), range : LibZ3::Sort)

mk_rem(*args)

mk_repeat(*args)

mk_rotate_left(*args)

mk_rotate_right(*args)

mk_sbv_to_str(*args)

mk_seq_at(*args)

mk_seq_concat(asts)

mk_seq_contains(*args)

mk_seq_empty(*args)

mk_seq_extract(*args)

mk_seq_index(*args)

mk_seq_last_index(*args)

mk_seq_length(*args)

mk_seq_nth(*args)

mk_seq_prefix(*args)

mk_seq_replace(*args)

mk_seq_replace_all(*args)

mk_seq_suffix(*args)

mk_seq_unit(*args)

mk_sign_ext(*args)

mk_simple_solver(*args)

mk_solver(*args)

mk_solver_for_logic(logic : String)

mk_str_le(*args)

mk_str_lt(*args)

mk_str_to_int(*args)

mk_string_from_code(*args)

mk_string_to_code(*args)

mk_sub(asts)

mk_symbol(name : String)

mk_true(*args)

mk_u32string(code_points : Array(UInt32))

A Z3 string is a sequence of code points, and these two are the only calls which pass one either way without escaping it into ASCII first

mk_ubv_to_str(*args)

mk_unary_minus(*args)

mk_xor(*args)

mk_zero_ext(*args)

model_eval(model, ast, complete)

model_get_const_decl(*args)

model_get_const_interp(model, decl)

model_get_func_decl(*args)

model_get_func_interp(model, decl)

What a model says a function does: the argument lists it had to pin down, and the else branch which answers for every other one.

model_get_num_consts(*args)

model_get_num_funcs(*args)

model_has_interp(*args)

model_inc_ref(*args)

model_to_string(*args)

new_ast_vector(exprs)

A vector we build ourselves, for the calls which take one. It comes back at refcount 1 and the caller has to release_ast_vector it.

new_from_ast_pointer(_ast) : AnyExpr

optimize_assert(*args)

optimize_assert_and_track(*args)

optimize_assert_soft(optimize, expr, weight : String)

optimize_check(target, assumptions)

optimize_from_file(*args)

optimize_from_string(*args)

optimize_get_assertions(*args)

optimize_get_help(*args)

optimize_get_model(*args)

optimize_get_reason_unknown(*args)

optimize_get_statistics(*args)

optimize_get_unsat_core(*args)

optimize_inc_ref(*args)

optimize_maximize(*args)

optimize_minimize(*args)

optimize_pop(*args)

optimize_push(*args)

optimize_set_initial_value(*args)

optimize_to_string(*args)

read_ast_vector(vec)

release_ast_vector(vec)

simplify(*args)

solver_assert(*args)

solver_assert_and_track(*args)

solver_check(*args)

solver_check_assumptions(target, assumptions)

solver_cube(solver, variables, backtrack_level : UInt32)

solver_from_file(*args)

solver_from_string(*args)

solver_get_assertions(*args)

solver_get_consequences(solver, assumptions, variables)

Answers the check result along with the consequences it found, since an :unsat or :unknown means there are none to speak of

solver_get_help(*args)

solver_get_model(*args)

solver_get_non_units(*args)

solver_get_num_scopes(*args)

solver_get_reason_unknown(*args)

solver_get_statistics(*args)

solver_get_trail(*args)

solver_get_units(*args)

solver_get_unsat_core(*args)

solver_inc_ref(*args)

solver_interrupt(*args)

solver_pop(*args)

solver_push(*args)

solver_reset(*args)

solver_set_initial_value(*args)

solver_to_dimacs_string(*args)

solver_to_string(*args)

sort_from_pointer(_sort) : AnySort