klara.klara_z3.z3_nodes.Z3Proxy

class documentation

class Z3Proxy(infer_proxy.InferProxy): (source)

Undocumented

Class Method	`init_expr`	Undocumented
Method	`__init__`	Initialize proxy with Z3 variable :param z3_expr: the z3 variable wrapped within the proxy :param default: default value if z3_var is not in the model
Method	`__k_bool__`	Undocumented
Method	`__k_float__`	Undocumented
Method	`__k_int__`	Undocumented
Method	`__k_not_bool__`	Undocumented
Method	`__k_str__`	Undocumented
Instance Variable	`defaults`	Undocumented
Method	`_binop_dunder_operation`	Undocumented
Method	`_compop_dunder_operation`	Undocumented
Method	`_default_op`	Undocumented
Method	`_infer`	Undocumented
Method	`_setup_dunder`	setup all dunder method to do operation on proxy obj, and return an InferenceResult :return: None
Method	`_unary_dunder_operation`	Undocumented

Inherited from InferProxy:

Method	`__hash__`	Undocumented
Method	`__iter__`	Undocumented
Method	`__next__`	Undocumented
Method	`dunder_lookup`	try to resolve the dunder method
Method	`get_return_type`	Undocumented
Method	`hash`	Undocumented
Method	`infer`	Undocumented
Method	`to_ast`	Specify how to convert this node to ast expression, to be used as test case comparison :return: ast node
Static Method	`_convert_dunder`	convert dunder method string to klara's specification :param dunder: dunder method in string, e.g. __str__ :return: converted dunder
Method	`_infer_bool`	Undocumented
Method	`_infer_builtins`	Undocumented
Method	`_infer_unaryop`	Undocumented
Class Variable	`_fields`	Undocumented
Instance Variable	`_hash`	Undocumented
Instance Variable	`_infer_binop`	Undocumented
Instance Variable	`_infer_comp_op`	Undocumented

Inherited from Const (via InferProxy):

Method	`__repr__`	Undocumented
Method	`get_type`	get the type of the constant holding
Instance Variable	`value`	Undocumented

Inherited from BaseNode (via InferProxy, Const):

Static Method	`get_inferred`	Undocumented
Method	`__contains__`	Undocumented
Method	`accept`	Undocumented
Method	`generic_visit`	Undocumented
Method	`get_bound_conditions`	Undocumented
Method	`get_children`	Undocumented
Method	`get_from_outer`	find the definition of `var` from outer scope recursively. Skip param will determine how many parent scope to skip :param var: variable of interest :param skip: how many layer of parent scope to skip :return:...
Method	`get_parent_of_type`	Undocumented
Method	`get_statements`	Undocumented
Method	`get_stmt_target`	Undocumented
Method	`get_target_instance`	get the assigning target instance rather than scope(). See #mr68u a.b.c = node calling node.get_target_instance() will return `a.b.c.instance()`
Method	`is_children`	check if the given node is part of 'self' or children
Method	`iter_fields`	Yield a tuple of ``(fieldname, value)`` for each field in ``node._fields`` that is present on node.
Method	`prepare_inferred_value`	Undocumented
Method	`scope`	return the first containing scope
Method	`statement`	Undocumented
Instance Variable	`col_offset`	Undocumented
Instance Variable	`explicit_inference`	Undocumented
Instance Variable	`lineno`	Undocumented
Instance Variable	`parent`	Undocumented
Instance Variable	`refer_to_block`	Undocumented

Inherited from Proxy (via InferProxy, Const, BaseNode, BaseInstance):

Method	`__getattr__`	Undocumented
Instance Variable	`obj`	Undocumented

Inherited from InvertCondMixin (via InferProxy, Const, BaseNode, BaseInstance, Proxy):

Method	`invert_condition`	Invert the condition of this node. wrap the node in `not()`
Method	`wrap_bool`	Undocumented

@classmethod
def init_expr(cls, z3_expr, defaults=None): (source)

Undocumented

def __init__(self, z3_var, default=None): (source)

overrides klara.core.tree.infer_proxy.InferProxy.__init__

Initialize proxy with Z3 variable :param z3_expr: the z3 variable wrapped within the proxy :param default: default value if z3_var is not in the model

def __k_bool__(self): (source)

Undocumented

def __k_float__(self): (source)

Undocumented

def __k_int__(self): (source)

Undocumented

def __k_not_bool__(self): (source)

Undocumented

def __k_str__(self): (source)

Undocumented

defaults = (source)

Undocumented

def _binop_dunder_operation(self, op, op_callback, reflected=False, other=None): (source)

Undocumented

Parameters
op:`str`	Undocumented
op_callback	Undocumented
reflected	Undocumented
other:`nodes.Const`	Undocumented

def _compop_dunder_operation(self, op_callback, other=None): (source)

Undocumented

Parameters
op_callback	Undocumented
other:`nodes.Const`	Undocumented

def _default_op(self, op, other, method_name, context=None, self_result=inference.InferenceResult): (source)

overrides klara.core.tree.infer_proxy.InferProxy._default_op

Undocumented

Parameters
op:`str`	Undocumented
other:`inference.InferenceResult`	Undocumented
method_name:`str`	Undocumented
context	Undocumented
self_result	Undocumented

def _infer(self, context=None, inferred_attr=None): (source)

overrides klara.core.tree.infer_proxy.InferProxy._infer

Undocumented

def _setup_dunder(self): (source)

setup all dunder method to do operation on proxy obj, and return an InferenceResult :return: None

def _unary_dunder_operation(self, op_callback): (source)

Undocumented