claripy.backends.backend_z3

module documentation
(source)

Undocumented

Class BackendZ3 No class docstring; 0/7 property, 0/2 instance variable, 0/1 class variable, 2/62 methods, 1/39 static method documented
Class SmartLRUCache Undocumented
Function claripy_solver_to_smt2 Undocumented
Function condom Undocumented
Function handle_sigint Undocumented
Function z3_expr_to_smt2 Undocumented
Function z3_solver_sat Undocumented
Constant ALL_Z3_CONTEXTS Undocumented
Variable l Undocumented
Variable old_handler Undocumented
Variable op_map Undocumented
Variable op_type_map Undocumented
Variable solve_count Undocumented
Variable z3_op_names Undocumented
Variable z3_op_nums Undocumented
Function _add_memory_pressure PyPy's garbage collector is not aware of memory uses happening inside native code. When performing memory-intensive tasks in native code, the memory pressure that PyPy observes can greatly deviate from the actual memory pressure...
Function _z3_decl_name_str Undocumented
Variable _is_pypy Undocumented
def claripy_solver_to_smt2(s): (source)

Undocumented

def condom(f): (source)

Undocumented

def handle_sigint(signals, frametype): (source)

Undocumented

def z3_expr_to_smt2(f, status='unknown', name='benchmark', logic=''): (source)

Undocumented

def z3_solver_sat(solver, extra_constraints, occasion): (source)

Undocumented

ALL_Z3_CONTEXTS = (source)

Undocumented

Value
weakref.WeakSet()
l = (source)

Undocumented

old_handler: bool = (source)

Undocumented

op_map: dict[str, str] = (source)

Undocumented

op_type_map = (source)

Undocumented

solve_count: int = (source)

Undocumented

z3_op_names = (source)

Undocumented

z3_op_nums = (source)

Undocumented

def _add_memory_pressure(p): (source)

PyPy's garbage collector is not aware of memory uses happening inside native code. When performing memory-intensive tasks in native code, the memory pressure that PyPy observes can greatly deviate from the actual memory pressure. We must manually add sufficient memory pressure to account for the "missing" portion. This is not a problem for CPython since its GC is based on reference counting.

def _z3_decl_name_str(ctx, decl): (source)

Undocumented

_is_pypy: bool = (source)

Undocumented