Skip to content

Choice.py

from pymwp import Choices

Choice module generates a compact representation of analysis derivation result.

The Choice module allows determining valid derivation choices and analyzing available choices. By default, the term valid means derivations that do not fail, i.e., give \(\infty\) in matrix; but other interpretations of valid choice can be defined also.

Determining valid derivation choices

Inputs:

  • index: int degree of choice; total number of derivation choices in an analyzed program.
  • domain: List[int] possible inference choices at a program point, e.g. [0,1,2].
  • delta_sequences: Set[SEQ] sequences of choices to negate.

For example, to obtain derivation choices excluding failing derivations (\(\infty\) in matrix), the delta_sequences should be all sequences of deltas with scalar i.

The choice module converts the delta sequences to their negated choices, in a compact regular expression-like format:

# Input:
index = 3
domain = [0, 1, 2]
delta_sequences = {((0, 0), (2, 1)), ((1, 1),)}

# Output:
[[[1, 2], [0, 2], [0, 1, 2]], 
 [[0, 1, 2], [0], [0, 1, 2]]]

A regular expression matching the output is ([1|2][0|2][0-2])|([0-2]0[0-2]).

Steps

  1. Simplify. Using \(\delta\)-sequences set, simplify it:

    1. Replace combinations that can be represented by a single shorter sequence.
    2. Remove supersets.
    3. Preemptively remove deltas that would lead to invalid choice vectors.

    Apply simplifications iteratively until convergence.

    Simplifications

    This example assumes domain = [0,1,2].

    (A) All possible choices occur at index 0: any choice followed by sequence (2,1)(1,2) results in infinity. Therefore, remove \(a, b, c\) and insert [(2,1)(1,2)] in their place. Choices are reduced similarly from both ends.

    BEFORE                           AFTER
[(0,0)(2,1)(1,2)]     # a        [(2,1)(1,2)]
[(1,0)(2,1)(1,2)]     # b
[(2,0)(2,1)(1,2)]     # c

    (B) Sequence \(a\) is subset of \(b\). Since \(b\) cannot be selected without selecting \(a\), discard \(b\).

    BEFORE                           AFTER
[(0,0)]               # a        [(0,0)]
[(0,0)(0,1)(2,2)]     # b

    (C) Constructing a choice vector requires selecting deltas from each remaining sequence \(a, b, c\). Therefore, deltas (0,0) and (1,0) must always be selected, and one of \(c\), [(2,0)(2,1)(1,2)]. However, selecting (0,0), (1,0), and (2,0) eliminates all choices at index 0. This allows to reduce sequences \(c\) to (2,1)(1,2).

    BEFORE                           AFTER
[(0,0)]               # a        [(0,0)]
[(1,0)]               # b        [(1,0)] 
[(2,0)(2,1)(1,2)]     # c        [(2,1)(1,2)]

  2. Build choice vectors. Initially consider all choices as valid. Then eliminate unwanted sequences, for all possible combinations.

    Compute cross product of remaining \(\delta\)-sequences. Iterate the product, for each:

    • Create a vector whose length is index.
    • Each vector element is a set of choices defined by domain.
    • Eliminate choices that lead to an unwanted outcome.

    Discard invalid and redundant vectors. Add remaining vectors to result.

    Choice vector generation

    # remaining after simplification
sequences = [[(0,0)], [(1,0)], [(2,1)(1,2)], [(2,0)(1,1)(1,2)]]

# compute a cross product of sequences (6 total)
choice_paths = [[(0,0) (1,0) (2,1) (2,0)],
                [(0,0) (1,0) (2,1) (1,1)],
                [(0,0) (1,0) (2,1) (1,2)],…]

for each path:

    # initialize a vector with all choices at each index
    vector_init = [{0,1,2}, {0,1,2}, {0,1,2}]

    # eliminate path choices, and add to result:
    vector_final = [[2], [0], [0,1,2]]

  3. Result. The result is a disjunction of choice vectors. Choose one vector, then select one value at each vector index. This yields a valid derivation result. For example, for a choice vector,

    [[[2], [0],   [0,1,2]],
 [[1], [1,2], [0,1,2]]]

    selecting \((1, 2, 2)\) is valid choice, so is \((2, 0, 2)\) and \((1, 1, 0)\), …etc.

    • If all choices are valid, the Choice vector has a single vector permitting all choices.
    • If no valid derivation exists, the result is empty choice: [ ].
    • If index=0, i.e., no choice needs to be made, also result is empty [ ].

Choices 

Choices(valid: CHOICES = None, index: int = -1)

A compact representation of derivation choices.

Attributes:

Name Type Description
valid CHOICES

list of choice vectors.
index int

degree of choice.

Initialize representation from a precomputed vector.

This is primarily useful for restoring a result from file. To create a choice representation, call generate() instead.

first property 

first: Optional[tuple[int]]

Gets the first valid derivation choice, if at least one exists.

infinite property 

infinite

True if no valid choice exists.

n_bounds property 

n_bounds: int

Number of bounds that can be generated from a choice vector. This is calculated directly from the vector form. It is the product of number of choices at each index: \(\prod_{c \in v} |c|\).

Example

  1. Vector [[0, 1, 2], [0, 1, 2], [0]] allows making [3, 3, 1] choices/index. It has \(3 * 3 * 1 = 9\) total bounds.

  2. A vector with choices/index: [3, 1, 2, 1, 3, 3] has \(3^3 * 2^1 * 1^2 = 54\) possible bounds.

Returns:

Type Description
int

Number of possible choices (non-distinct).

all 

all() -> Generator[Tuple[int, ...]]

Generator for all valid derivation choices.

Note

Calling this method is very inefficient. Generally, we do not want to generate all choices. The method yields the next value in series, so it is possible to step through the choices one at a time. Use with caution/only call if necessary.

Yields:

Type Description
Generator[Tuple[int, ...]]

The next valid choice.

build_choices staticmethod 

build_choices(domain: List[int], index: int, infinities: Set[SEQ]) -> CHOICES

Build a list of distinct choice vectors excluding unwanted choices.

This method works by taking a list of delta paths that give unwanted scalars (e.g., \(\infty\)) and then negates those choices; the result is a list of choice vectors such that any remaining choice will give a valid derivation.

Example
  • Assume paths leading to \(\infty\) are: [(0,0)], [(1,0)], [(1,1)(0,3)].
  • The choices that do not lead to \(\infty\) are: [[[2], [0,2], [0,1,2]] or [[2], [0,1,2], [1,2]]].

Parameters:

Name Type Description Default
domain List[int]

list of valid choices for one index, e.g. [0, 1, 2].

 required
index int

the length of the vector, e.g. 10.

 required
infinities Set[SEQ]

set of deltas that lead to unwanted choices.

 required

Returns:

Type Description
CHOICES

Choice vector that excludes all paths leading to unwanted choices.

except_one staticmethod 

except_one(domain: List[int], sequences: Set[SEQ]) -> Set[SEQ]

Look for deltas of length=1 where all-but-one choices are made at same index. The remaining one choice can be eliminated from paths that contain it, because it would yield an invalid choice vector.

Example

Given sequence ((0,0),), ((1,0),), ((2,0),(2,1),(1,4),) and the goal to build a choice vector. Deltas (0,0) and (1,0) must be chosen. For ((2,0),(2,1),(1,4),) one of the deltas must be chosen. But choosing (0,0), (1,0), (2,0) eliminates all choices at index 0. It suffices to keep sequence ((0,0),), ((1,0),), ((2,1),(1,4),).

Parameters:

Name Type Description Default
domain List[int]

list of valid per index choices, e.g. [0, 1, 2].

 required
sequences Set[SEQ]

set of delta sequences.

 required

Returns:

Type Description
Set[SEQ]

A set of sequences after applying simplification.

generate staticmethod 

generate(domain: List[int], index: int, inf: Set[SEQ]) -> Choices

Generate the choice representation.

This works in two steps: (1) simplify delta sequences, (2) build choice vectors.

Parameters:

Name Type Description Default
domain List[int]

valid choices at index, e.g. [0, 1, 2].

 required
index int

the length of the vector, e.g. 10. This is the same as number of assignments in the analyzed function.

 required
inf Set[SEQ]

set of deltas that lead to infinity.

 required

Returns:

Type Description
Choices

Generated choice object.

intersection staticmethod 

intersection(c1: Choices, c2: Choices) -> Choices

Intersection of two choice vectors.

Intersection is a cross-product of non-empty vector intersections. If the none of the vectors intersect, the resulting Choice is empty.

Parameters:

Name Type Description Default
c1 Choices

First Choice vector.

 required
c2 Choices

Second Choice vector.

 required

Returns:

Type Description
Choices

New Choices representing the intersection of the two arguments.

is_valid 

is_valid(*choices: int) -> bool

Checks if sequence of choices can be made without infinity.

Example 
choice_obj.is_valid(0, 1, 2, 1, 1, 0)

Parameters:

Name Type Description Default
choices int

sequences of delta values to check.

 ()

Returns:

Type Description
bool

True if the given choices can be made without infinity.

prod staticmethod 

prod(values: list) -> int

Compute the product of numeric list.

Parameters:

Name Type Description Default
values list

1d list of numbers.

 required

Returns:

Type Description
int

Product of values.

reduce staticmethod 

reduce(domain: List[int], sequences: Set[SEQ]) -> bool

Look for first reducible sequence, if exists, then replace it.

Example

We can reduce a sequences where deltas differ only on first value, never on index, and all possible choice values are represented in the first delta. Below, it does not matter which choice is made at index 0. The 3 paths can be collapsed into a single, shorter path: (2,1)(1,4).

(0,0) (2,1) (1,4)
(1,0) (2,1) (1,4)
(2,0) (2,1) (1,4)

Parameters:

Name Type Description Default
domain List[int]

list of valid per index choices, e.g. [0, 1, 2].

 required
sequences Set[SEQ]

set of delta sequences.

 required

Returns:

Type Description
bool

True if a reduction occurred and False otherwise. The meaning of False is to say the operation is done and should not be repeated any further.

reduce_end staticmethod 

reduce_end(domain: List[int], sequences: Set[SEQ]) -> bool

Like reduce, but from end of sequence.

Example

When deltas only differ at last index, and all choices occur at last index, reduce choices to a shorter path. E.g., Below, choice at index 5 is irrelevant; keep (2,1) (1,4).

(2,1) (1,4) (0,5)
(2,1) (1,4) (1,5)
(2,1) (1,4) (2,5)

Parameters:

Name Type Description Default
domain List[int]

list of valid per index choices, e.g. [0, 1, 2].

 required
sequences Set[SEQ]

set of delta sequences.

 required

Returns:

Type Description
bool

True if a reduction occurred and False otherwise.

remove_subset staticmethod 

remove_subset(match: SEQ, items: Union[Set, List])

If match is a subset of any item in items, removes the superset from items, in place.

Parameters:

Name Type Description Default
match SEQ

single delta sequence.

 required
items Union[Set, List]

list of delta sequences to check against match.

 required

simplify staticmethod 

simplify(domain: List[int], sequences: Set[SEQ]) -> Set[SEQ]

Generate the most simplified, equivalent representation of the set of choices that cause unwanted derivation results.

Reduce sequences of deltas, until set of sequences cannot be reduced any further. Then remove all superset contained by some shorter sequence. Lastly, remove deltas that would generate an invalid choice vector. This process repeats until no more simplification can be applied.

Parameters:

Name Type Description Default
domain List[int]

list of valid per index choices, e.g. [0, 1, 2].

 required
sequences Set[SEQ]

set of delta sequences.

 required

Returns:

Type Description
Set[SEQ]

Simplified list of infinity paths.

sub_equal staticmethod 

sub_equal(first: SEQ, second: SEQ) -> bool

Compare two delta sequences for equality, except their 0th value.

Parameters:

Name Type Description Default
first SEQ

first delta sequence.

 required
second SEQ

second delta sequence.

 required

Returns:

Type Description
bool

True if two delta sequences are equal excluding the 0th value, and False otherwise.

sub_equal_end staticmethod 

sub_equal_end(first: SEQ, second: SEQ) -> bool

Compare two delta sequences for equality, except their N-th value. This is like sub_equal, but comparison is done at the end of sequences.

Parameters:

Name Type Description Default
first SEQ

first delta sequence.

 required
second SEQ

second delta sequence.

 required

Returns:

Type Description
bool

True if two delta sequences are equal excluding the N-th value, and False otherwise.

to_choices staticmethod 

to_choices(vectors: List[VECT]) -> CHOICES

Convert a list of vectors to CHOICES type. This is a simple type conversion over the inner collection-types.

unique_sequences staticmethod 

unique_sequences(infinities: Set[SEQ]) -> Set[SEQ]

Remove superset delta sequences.

Parameters:

Name Type Description Default
infinities Set[SEQ]

set of delta sequences causing infinity.

 required

Returns:

Type Description
Set[SEQ]

A list where all longer sequences, whose pattern is covered by some shorter sequence, are removed.

vect_contains staticmethod 

vect_contains(a: VECT, b: VECT) -> bool

Check if A allows making all choices of B.

Parameters:

Name Type Description Default
a VECT

first vector.

 required
b VECT

second vector.

 required

Returns:

Type Description
bool

True if A contains B, and False otherwise.

vect_intersection staticmethod 

vect_intersection(a: VECT, b: VECT) -> Optional[VECT]

Intersection of two vectors.

The intersection is the maximal choice at each index, permitted by both vectors A and B. The intersection is empty if, at some index, no choice exists.

Example

Let a=((0,1),(0,2)), b=((1,),(1,2)), and c=((1,),(1,)).

  • The intersection of a&b is ((1,),(2,)).
  • The intersection of a&c is None.
  • The intersection of b&c is ((1,),(1,)).

Parameters:

Name Type Description Default
a VECT

first vector.

 required
b VECT

second vector.

 required

Returns:

Type Description
Optional[VECT]

A new vector that is the intersection of A and B; None when the intersection is empty.

vect_new staticmethod 

vect_new(vectors: Set[VECT], vector: VECT) -> bool

Determines if a vector is distinct from all existing vectors.

Parameters:

Name Type Description Default
vectors Set[VECT]

a set of known vectors.

 required
vector VECT

vector to check.

 required

Returns:

Type Description
bool

True if vector does not occur in vectors.

vect_rm staticmethod 

vect_rm(vectors: Set[VECT], vector: VECT) -> None

Remove from vectors those that are contained by vector.

Parameters:

Name Type Description Default
vectors Set[VECT]

a set of vectors.

 required
vector VECT

vector compare against.

 required