class Z3::Context

• Z3::Context
• Reference
• Object

Overview

A Context manages all other Z3 objects, global configuration options, etc. Z3Py uses a default global context. For most applications this is sufficient. An application may use multiple Z3 contexts. Objects created in one context cannot be used in another one. However, several objects may be "translated" from one context to another. It is not safe to access Z3 objects from multiple threads. The only exception is the method #interrupt that can be used to interrupt a long computation. The initialization method receives global configuration options for the new context.

Defined in:

z3/context.cr
z3/context/arithmetic_operators.cr
z3/context/compare_operators.cr
z3/context/logic_operators.cr
z3/context/sorts.cr
z3/context/values.cr
z3/context/vars.cr

Constructors

• .new(config = Config.new)

  https://github.com/angr/angr-z3/blob/6fa85ad65404c0dbc8adf3e120fa076bd5c6d003/src/api/python/z3/z3.py#L163

Instance Method Summary

• #bit_vector_sort(size : Int32) : Sort
• #bool_sort
• #finalize
• #int_sort
• #mk(v : Int32, ty : Sort) : Ast
• #mk(v : UInt32, ty : Sort) : Ast
• #mk(v : Int64, ty : Sort) : Ast
• #mk(v : UInt64, ty : Sort) : Ast
• #mk_add(a : Ast, b : Ast)
• #mk_and(a : Ast, b : Ast)
• #mk_bitvector_var(name : String, size : Int32)
• #mk_bool_var(name : String)
• #mk_distinct(a : Ast, b : Ast)
• #mk_eq(a : Ast, b : Ast)
• #mk_ge(a : Ast, b : Ast)
• #mk_gt(a : Ast, b : Ast)
• #mk_implies(a : Ast, b : Ast)
• #mk_int_var(name : String)
• #mk_le(a : Ast, b : Ast)
• #mk_lt(a : Ast, b : Ast)
• #mk_mul(a : Ast, b : Ast)
• #mk_numeral(numeral : String, ty : Sort) : Ast
• #mk_or(a : Ast, b : Ast)
• #mk_real(num : Int32, den : Int32) : Ast
• #mk_real_var(name : String)
• #mk_sub(a : Ast, b : Ast)
• #mk_xor(a : Ast, b : Ast)
• #real_sort
• #to_unsafe : LibZ3::Context

Constructor Detail

Instance Method Detail