module Z3::API
Extended Modules
Defined in:
z3/api.crConstant Summary
-
Context =
LibZ3.mk_context(LibZ3.mk_config)
Instance Method Summary
- #ast_to_string(ast)
- #get_ast_kind(*args)
- #get_numeral_string(ast)
- #mk_add(asts)
- #mk_and(asts)
- #mk_bvadd(*args)
- #mk_bvand(*args)
- #mk_bvashr(*args)
- #mk_bvlshr(*args)
- #mk_bvmul(*args)
- #mk_bvnand(*args)
- #mk_bvneg(*args)
- #mk_bvnor(*args)
- #mk_bvnot(*args)
- #mk_bvor(*args)
- #mk_bvsdiv(*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_bvudiv(*args)
- #mk_bvuge(*args)
- #mk_bvugt(*args)
- #mk_bvule(*args)
- #mk_bvult(*args)
- #mk_bvurem(*args)
- #mk_bvxnor(*args)
- #mk_bvxor(*args)
- #mk_concat(*args)
- #mk_const(name, sort)
- #mk_distinct(asts)
- #mk_div(*args)
- #mk_eq(*args)
- #mk_extract(*args)
- #mk_false(*args)
- #mk_ge(*args)
- #mk_gt(*args)
- #mk_iff(*args)
- #mk_implies(*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_power(*args)
- #mk_rem(*args)
- #mk_rotate_left(*args)
- #mk_rotate_right(*args)
- #mk_sign_ext(*args)
- #mk_solver(*args)
- #mk_sub(asts)
- #mk_true(*args)
- #mk_unary_minus(*args)
- #mk_xor(*args)
- #mk_zero_ext(*args)
- #model_eval(model, ast, complete)
- #model_to_string(model)
- #new_from_ast_pointer(_ast)
- #simplify(*args)
- #solver_assert(*args)
- #solver_check(*args)
- #solver_get_model(*args)