Z3::Context
Inherits Reference < Object
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.
Constructors
new(config = Config.new)
https://github.com/angr/angr-z3/blob/6fa85ad65404c0dbc8adf3e120fa076bd5c6d003/src/api/python/z3/z3.py#L163
Instance methods
bit_vector_sort(size : Int32) : Sort
Sourcebool_sort
Sourcefinalize
Sourceint_sort
Sourcemk(v : Int32, ty : Sort) : Ast
Sourcemk(v : UInt32, ty : Sort) : Ast
Sourcemk(v : Int64, ty : Sort) : Ast
Sourcemk(v : UInt64, ty : Sort) : Ast
Sourcemk_add(a : Ast, b : Ast)
Sourcemk_and(a : Ast, b : Ast)
Sourcemk_bitvector_var(name : String, size : Int32)
Sourcemk_bool_var(name : String)
Sourcemk_distinct(a : Ast, b : Ast)
Sourcemk_eq(a : Ast, b : Ast)
Sourcemk_ge(a : Ast, b : Ast)
Sourcemk_gt(a : Ast, b : Ast)
Sourcemk_implies(a : Ast, b : Ast)
Sourcemk_int_var(name : String)
Sourcemk_le(a : Ast, b : Ast)
Sourcemk_lt(a : Ast, b : Ast)
Sourcemk_mul(a : Ast, b : Ast)
Sourcemk_numeral(numeral : String, ty : Sort) : Ast
Sourcemk_or(a : Ast, b : Ast)
Sourcemk_real(num : Int32, den : Int32) : Ast
Sourcemk_real_var(name : String)
Sourcemk_sub(a : Ast, b : Ast)
Sourcemk_xor(a : Ast, b : Ast)
Sourcereal_sort
Sourceto_unsafe
Source