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
-
#app_args(ast)
The arguments of an application, so a term like
a == 2can be taken apart. - #ast_to_string(ast)
- #get_algebraic_number_lower(*args)
- #get_algebraic_number_upper(*args)
- #get_ast_kind(*args)
- #get_bool_value(*args)
- #get_decl_name(decl)
- #get_numeral_string(ast)
- #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_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_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_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_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_solver(*args)
- #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_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_num_consts(*args)
- #model_inc_ref(*args)
- #model_to_string(model)
- #new_from_ast_pointer(_ast) : AnyExpr
- #read_ast_vector(vec)
- #simplify(*args)
- #solver_assert(*args)
- #solver_assert_and_track(*args)
- #solver_check(*args)
- #solver_get_assertions(solver)
- #solver_get_model(*args)
- #solver_get_num_scopes(*args)
- #solver_get_reason_unknown(solver)
- #solver_get_statistics(solver)
- #solver_get_unsat_core(solver)
- #solver_inc_ref(*args)
- #solver_pop(*args)
- #solver_push(*args)
- #solver_reset(*args)
- #solver_to_string(solver)
- #sort_from_pointer(_sort) : AnySort
Instance Method Detail
def 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
def 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