pytype.pytd.booleq.Solver

class documentation

class Solver: (source)

View In Hierarchy

Solver for boolean equations. This solver computes the union of all solutions. I.e. rather than assigning exactly one value to each variable, it will create a list of values for each variable: All the values this variable has in any of the solutions. To accomplish this, we use the following rewriting rules: [1] (t in X && ...) || (t in Y && ...) --> t in (X | Y) [2] t in X && t in Y --> t in (X & Y) Applying these iteratively for each variable in turn ("extracting pivots") reduces the system to one where we can "read off" the possible values for each variable. Attributes: ANY_VALUE: A special value assigned to variables with no constraints. variables: A list of all variables. implications: A nested dictionary mapping variable names to values to BooleanTerm instances. This is used to specify rules like "if x is 1, then ..." ground_truth: An equation that needs to always be TRUE. If this is FALSE, or can be reduced to FALSE, the system is unsolvable. assignments: The solutions, a mapping of variables to values.

Method __init__ Undocumented
Method __repr__ Undocumented
Method __str__ Undocumented
Method always_true Register a ground truth. Call before calling solve().
Method implies Register an implication. Call before calling solve().
Method register_variable Register a variable. Call before calling solve().
Method solve Solve the system of equations.
Constant ANY_VALUE Undocumented
Instance Variable assignments Undocumented
Instance Variable ground_truth Undocumented
Instance Variable implications Undocumented
Instance Variable variables Undocumented
Method _complete Insert missing implications.
Method _get_first_approximation Get all (variable, value) combinations to consider.
Method _get_nonfalse_values Undocumented
Method _iter_implications Undocumented
def __init__(self): (source)

Undocumented

def __repr__(self): (source)

Undocumented

def __str__(self): (source)

Undocumented

def always_true(self, formula): (source)

Register a ground truth. Call before calling solve().

def implies(self, e: BooleanTerm, implication: BooleanTerm): (source)

Register an implication. Call before calling solve().

def register_variable(self, variable): (source)

Register a variable. Call before calling solve().

def solve(self): (source)

Solve the system of equations. Returns: An assignment, mapping strings (variables) to sets of strings (values).

ANY_VALUE: str = (source)

Undocumented

Value
'?'
assignments = (source)

Undocumented

ground_truth = (source)

Undocumented

implications = (source)

Undocumented

variables = (source)

Undocumented

def _complete(self): (source)

Insert missing implications. Insert all implications needed to have one implication for every (variable, value) combination returned by _get_first_approximation().

def _get_first_approximation(self): (source)

Get all (variable, value) combinations to consider. This gets the (variable, value) combinations that the solver needs to consider based on the equalities that appear in the implications. E.g., with the following implication: t1 = v1 => t1 = t2 | t3 = v2 the combinations to consider are (t1, v1) because t1 = v1 appears, (t2, v1) because t1 = t2 and t1 = v1 appear, and (t3, v2) because t3 = v2 appears. Returns: A dictionary D mapping strings (variables) to sets of strings (values). For two variables t1 and t2, if t1 = t2 is a possible assignment (by first approximation), then D[t1] and D[t2] point to the same memory location.

def _get_nonfalse_values(self, var): (source)

Undocumented

def _iter_implications(self): (source)

Undocumented