class documentation

class Balancer: (source)

View In Hierarchy

The Balancer is an equation redistributor. The idea is to take an AST and rebalance it to, for example, isolate unknown terms on one side of an inequality.

Method __init__ Undocumented
Class Variable comparison_info Undocumented
Instance Variable sat Undocumented
Property compat_ret Undocumented
Property replacements Undocumented
Static Method _adjust_truism Swap the operands of the truism if the unknown variable is on the right side and the concrete value is on the left side.
Static Method _balance___add__ Undocumented
Static Method _balance___and__ Undocumented
Static Method _balance___sub__ Undocumented
Static Method _balance_Concat Undocumented
Static Method _balance_Extract Undocumented
Static Method _balance_Reverse Undocumented
Static Method _balance_SignExt Undocumented
Static Method _balance_ZeroExt Undocumented
Static Method _cardinality Undocumented
Static Method _get_assumptions Given a constraint, _get_assumptions() returns a set of constraints that are implicitly assumed to be true. For example, `x <= 10` would return `x >= 0`.
Static Method _handleable_truism Checks whether we can handle this truism. The truism should already be aligned.
Static Method _invert_comparison Undocumented
Static Method _max Undocumented
Static Method _min Undocumented
Static Method _reverse_comparison Undocumented
Method _add_lower_bound Undocumented
Method _add_upper_bound Undocumented
Method _align___sub__ Undocumented
Method _align_ast Aligns the AST so that the argument with the highest cardinality is on the left.
Method _align_bv Undocumented
Method _align_truism Undocumented
Method _balance Undocumented
Method _balance___lshift__ Undocumented
Method _balance_If Undocumented
Method _doit This function processes the list of truisms and finds bounds for ASTs.
Method _handle Undocumented
Method _handle___eq__ Undocumented
Method _handle___ne__ Undocumented
Method _handle_comparison Handles all comparisons.
Method _handle_If Undocumented
Method _queue_truism Undocumented
Method _queue_truisms Undocumented
Method _range Undocumented
Method _replacements_iter Undocumented
Method _same_bound_bv Undocumented
Method _unpack_truisms Given a constraint, _unpack_truisms() returns a set of constraints that must be True for this constraint to be True.
Method _unpack_truisms_And Undocumented
Method _unpack_truisms_Not Undocumented
Method _unpack_truisms_Or Undocumented
Instance Variable _helper Undocumented
Instance Variable _identified_assumptions Undocumented
Instance Variable _lower_bounds Undocumented
Instance Variable _processed_truisms Undocumented
Instance Variable _truisms Undocumented
Instance Variable _upper_bounds Undocumented
Instance Variable _validation_frontend Undocumented
def __init__(self, helper, c, validation_frontend=None): (source)

Undocumented

comparison_info: dict = (source)

Undocumented

Undocumented

Undocumented

@property
replacements = (source)

Undocumented

@staticmethod
def _adjust_truism(t): (source)

Swap the operands of the truism if the unknown variable is on the right side and the concrete value is on the left side.

@staticmethod
def _balance___add__(truism): (source)

Undocumented

@staticmethod
def _balance___and__(truism): (source)

Undocumented

@staticmethod
def _balance___sub__(truism): (source)

Undocumented

@staticmethod
def _balance_Concat(truism): (source)

Undocumented

@staticmethod
def _balance_Extract(truism): (source)

Undocumented

@staticmethod
def _balance_Reverse(truism): (source)

Undocumented

@staticmethod
def _balance_SignExt(truism): (source)

Undocumented

@staticmethod
def _balance_ZeroExt(truism): (source)

Undocumented

@staticmethod
def _cardinality(a): (source)

Undocumented

@staticmethod
def _get_assumptions(t): (source)

Given a constraint, _get_assumptions() returns a set of constraints that are implicitly assumed to be true. For example, `x <= 10` would return `x >= 0`.

@staticmethod
def _handleable_truism(t): (source)

Checks whether we can handle this truism. The truism should already be aligned.

@staticmethod
def _invert_comparison(a): (source)

Undocumented

@staticmethod
def _max(a, signed=False): (source)

Undocumented

@staticmethod
def _min(a, signed=False): (source)

Undocumented

@staticmethod
def _reverse_comparison(a): (source)

Undocumented

def _add_lower_bound(self, o, b): (source)

Undocumented

def _add_upper_bound(self, o, b): (source)

Undocumented

def _align___sub__(self, a): (source)

Undocumented

def _align_ast(self, a): (source)

Aligns the AST so that the argument with the highest cardinality is on the left. :return: a new AST.

def _align_bv(self, a): (source)

Undocumented

def _align_truism(self, truism): (source)

Undocumented

def _balance(self, truism): (source)

Undocumented

def _balance___lshift__(self, truism): (source)

Undocumented

def _balance_If(self, truism): (source)

Undocumented

def _doit(self): (source)

This function processes the list of truisms and finds bounds for ASTs.

def _handle(self, truism): (source)

Undocumented

def _handle___eq__(self, truism): (source)

Undocumented

def _handle___ne__(self, truism): (source)

Undocumented

def _handle_comparison(self, truism): (source)

Handles all comparisons.

def _handle_If(self, truism): (source)

Undocumented

def _queue_truism(self, t, check_true=False): (source)

Undocumented

def _queue_truisms(self, ts, check_true=False): (source)

Undocumented

def _range(self, a, signed=False): (source)

Undocumented

def _replacements_iter(self): (source)

Undocumented

def _same_bound_bv(self, a): (source)

Undocumented

def _unpack_truisms(self, c) -> Set: (source)

Given a constraint, _unpack_truisms() returns a set of constraints that must be True for this constraint to be True.

def _unpack_truisms_And(self, c): (source)

Undocumented

def _unpack_truisms_Not(self, c): (source)

Undocumented

def _unpack_truisms_Or(self, c): (source)

Undocumented

Undocumented

_identified_assumptions = (source)

Undocumented

_lower_bounds: dict = (source)

Undocumented

_processed_truisms = (source)

Undocumented

_truisms: list = (source)

Undocumented

_upper_bounds: dict = (source)

Undocumented

_validation_frontend = (source)

Undocumented