module
Z3::API
Extended Modules
Defined in:
z3/api.crConstant Summary
-
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
checkedto raise on - a Crystal exception can't be thrown out of a C callback and back through Z3's own frames.
Instance Method Summary
- #add_rec_def(decl, args, body)
-
#app_args(ast)
The arguments of an application, so a term like
a == 2can be taken apart. - #ast_to_string(*args)
-
#const_decl(expr)
The decl of a variable -
aina + 1- which is what Z3 wants wherever it talks about one. - #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
elsebranch 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.
- #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
Instance Method Detail
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
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.
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
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.
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.
Answers the check result along with the consequences it found, since an :unsat or :unknown means there are none to speak of