autstr.utils package

autstr.utils package#

Submodules#

autstr.utils.automata_tools module#

autstr.utils.automata_tools.pad(dfa, padding_symbol=-1)[source]#

Accept the language followed by any number of padding symbols.

An accepting state may already have a transition on the padding symbol, so adding the padding loop makes the automaton nondeterministic: the padding symbol now leads both to the original target and into the padding loop. Only that one symbol changes, which on the diagrams is a single path rewrite; the subset construction then restores determinism.

Return type:

SparseDFA

Parameters:
autstr.utils.automata_tools.unpad(dfa, padding_symbol=-1)[source]#

Remove trailing padding symbols from accepted words: a state becomes accepting iff reading padding from it can reach an accepting state. The padding successor is a function, so its orbit is closed by iterative doubling; the transition diagrams are untouched.

Return type:

SparseDFA

Parameters:
autstr.utils.automata_tools.product(dfa, n)[source]#

Create the n-fold Cartesian product of the automaton’s language.

Return type:

SparseDFA

Parameters:
autstr.utils.automata_tools.stack(dfa1, dfa2)[source]#

Creates a stacked automaton that recognizes the concatenation of two relations without explicitly generating all possible symbols.

The new automaton accepts tuples (x1,…,xk,y1,…,yl) where:

(x1,…,xk) is accepted by dfa1 and (y1,…,yl) is accepted by dfa2

Parameters:

  • dfa1 (SparseDFA) – First automaton of arity k

  • dfa2 (SparseDFA) – Second automaton of arity l

Return type:

SparseDFA

Returns:

SparseDFA of arity k+l recognizing the stacked relation

autstr.utils.automata_tools.projection(dfa, i)[source]#

Existentially quantify tape i.

The projected transition of a state is the union of the m cofactors of its diagram on tape i’s variable block — a diagram over sets of states — and the subset construction then folds those over the members of each subset. Neither the source nor the projected alphabet is ever enumerated.

Quantifying a tape coarsens the dynamics, so the resulting NFA is pruned and quotiented by forward bisimulation (reduce_set_nfa) before it is determinized: even a minimal source DFA usually has bisimilar states once a tape is existentially quantified, and every merged pair halves a dimension of the subset space.

Return type:

SparseDFA

Parameters:
autstr.utils.automata_tools.expand(dfa, new_arity, pos)[source]#

Expand a DFA of arity k to new_arity by placing original tape t at new position pos[t]; the remaining positions accept any symbol.

This is a variable renaming on the transition diagrams: the new tapes’ variables simply do not occur. Repeated entries in pos identify tapes, which restricts the relation to their diagonal.

Return type:

SparseDFA

Parameters:
class autstr.utils.automata_tools.LengthLexHeap[source]#

Bases: object

push(item)[source]#
pop()[source]#
autstr.utils.automata_tools.iterate_language(dfa, decoder=None, backward=False, padding_symbol=-1)[source]#

Generator over the language of a SparseDFA. Yields words in length-lexicographic order. Note: The algorithm assumes minimality and optimal sparsity of the automaton.

Parameters:

  • dfa (SparseDFA) – Sparse automaton

  • decoder (Callable) – Function to decode words to Python objects

  • backward (bool) – If True, generate words in reverse order

  • padding_symbol (int) – Integer representing padding symbol

Return type:

Generator

Returns:

Generator of words (or decoded objects)

autstr.utils.automata_tools.permute_tapes(dfa, perm)[source]#

Reorder the tapes of a multi-tape automaton: tape t of the result is tape perm[t] of the input — a permutation of the variable blocks.

Return type:

SparseDFA

Parameters:
autstr.utils.automata_tools.word_automaton(word, base_alphabet, padding_symbol=None)[source]#

Automaton accepting exactly the given word, optionally followed by trailing padding symbols.

Parameters:

  • word (List) – sequence of symbols from base_alphabet

  • base_alphabet (Set) – the base alphabet

  • padding_symbol – if given, accept word followed by any number of padding symbols

Return type:

SparseDFA

Returns:

SparseDFA of arity 1 recognizing {word}·{pad}*

autstr.utils.automata_tools.lsbf_Z_automaton(z)[source]#

Creates a SparseDFA for LSB-first representation of integer z with sign bit and padding. Alphabet encoding:

"*" = 0
"0" = 1
"1" = 2
Return type:

SparseDFA

Parameters:

z (int)

autstr.utils.logic module#

autstr.utils.logic.get_free_elementary_vars(phi)[source]#

Get an ordered list of all free elementary variables of phi.

Parameters:

phi (Expression) – The formula

Return type:

List[str]

Returns:

Ordered list with all elementary variable names

autstr.utils.logic.optimize_query(query)[source]#

Optimize a query for optimized automata construction.

Parameters:

query (Expression) – The query expression

Return type:

Expression

Returns:

Optimized query expression

autstr.utils.misc module#

autstr.utils.misc.cmp_llex(v, w)[source]#

Length-lexicographic ordering of a tuple of strings ignoring the padding symbol.

Parameters:
Return type:

int

Returns:

autstr.utils.misc.heapify_llex(arr)[source]#

heaplyfy a list under the llex order.

Parameters:

arr (List[object])

Return type:

List[object]

Returns:

autstr.utils.misc.heappop_llex(heap)[source]#

heapop wrapper for llex order.

Parameters:

heap (List[object]) – The heap list

Return type:

object

Returns:

autstr.utils.misc.heappush_llex(heap, x)[source]#

Heappop wrapper for lllex order.

Parameters:
Return type:

None

Returns:

autstr.utils.misc.get_unique_id(current_id, n=1)[source]#
Return type:

Union[str, List[str]]

Parameters:
autstr.utils.misc.encode_symbol(tuple_symbol, base_alphabet)[source]#

Encode a symbol tuple into a single integer.

Return type:

int

Parameters:
autstr.utils.misc.decode_symbol(enc, arity, base_alphabet)[source]#

Decode an integer into a symbol tuple.

Return type:

Tuple[int]

Parameters:
autstr.utils.misc.complement(values, min_val, max_val)[source]#

Find the complement of a set of values within a specified range.

Parameters:

  • values (np.ndarray) – The input array of values.

  • min_val (int) – The minimum value of the range.

  • max_val (int) – The maximum value of the range.

Returns:

The sorted values of the range missing from the input.

Return type:

ndarray

autstr.utils.tree_automata_tools module#

The first-order pipeline for sparse tree automata: cylindrification (expand), existential projection, padding closure, and minimization.

Design notes.

Symbols are variable assignments. Every transition is a multi-terminal BDD over the binary digits of the convolution symbol, tape-major (see autstr.mtbdd), which is what makes the pipeline affordable:

  • expand renames variable blocks. The tapes it adds are simply never tested, so a k-tape transition widened to k+j tapes costs nothing — no row is duplicated once per letter of each new tape. Sending two source tapes to the same target block substitutes one variable block for the other, which is how a relation R(x, x) is formed.

  • project quantifies one tape’s variable block: the m cofactors of a transition are combined by set union, giving the nondeterministic transition as a diagram over sets of states, and the subset construction then folds those diagrams over the members of each child subset. No symbol is ever enumerated, and no “does this pair except all m preimages?” counting is needed — invalid binary codes carry the reserved NONE terminal.

  • minimize refines over diagram identity: hash-consing means two states have the same behavior on a child pair exactly when the class-relabelled diagrams of that pair are the same integer.

Padding has two directions.

  • project handles the absent direction: projecting away tape i turns the automaton nondeterministic and changes the domain semantics: the ∃-witness tree may extend below the remaining tapes’ domains, leaving regions labelled all-padding that are trimmed from the projected convolution. In a bottom-up run of the trimmed tree an absent child may therefore correspond to any state reachable by some pure-padding tree (the padding closure P0), so the subset determinization runs with the absent-child subset S⊥ = {BOT} ∪ P0.

  • attach_padding handles the present direction: it accepts every tree of the language with arbitrary all-padding regions attached below, by making such regions behave exactly like absent children (a single fresh PAD state, no subset construction — the source is deterministic). It must be applied before expand widens a relation to more tapes, because the wider convolution’s domain is the union of all tapes’ domains.

Sparsity. A child pair absent from the transition table sends every symbol to the global default. Products, projections and minimization all drop a pair again as soon as its diagram is the default constant, so the pair tables stay driven by genuine deviations.

autstr.utils.tree_automata_tools.expand(sta, new_arity, pos)[source]#

Expand a k-tape automaton to new_arity tapes, placing original tape t at position pos[t]; the remaining positions range over all letters.

This is a variable renaming on the transition diagrams: the new tapes’ variables do not occur, so the automaton ignores them. Repeated entries in pos identify tapes (the diagonal of the relation).

Note: like the string expand, this widens only the alphabet; apply attach_padding first so regions contributed solely by the new tapes (all-padding on the original tapes) are accepted.

Return type:

SparseTreeAutomaton

Parameters:
autstr.utils.tree_automata_tools.permute_tapes(sta, perm)[source]#

Reorder the tapes of a convolution automaton: new tape i carries what was tape perm[i].

Return type:

SparseTreeAutomaton

Parameters:
autstr.utils.tree_automata_tools.project(sta, tape, padding_symbol, max_states=None)[source]#

Existentially quantify one tape: accept the convolution of the remaining tapes iff some witness tree exists on the projected tape (including witnesses whose domain extends below the remaining tapes, which is what the padding closure of the absent-child set captures).

Subset construction is worst-case exponential; max_states aborts with a clear error instead of exhausting memory.

Return type:

SparseTreeAutomaton

Parameters:
autstr.utils.tree_automata_tools.attach_padding(sta, padding_symbol, max_states=None)[source]#

Accept exactly the trees whose maximal all-padding subtrees, once trimmed away, the source accepts — the tree analog of the string pipeline’s pad, required before expand widens the convolution (the wider convolution’s domain is the union of all tapes’ domains, so the original tapes see attached regions as padding).

The source is deterministic, so no subset construction is needed: one fresh PAD state absorbs pure-padding regions, and every child pair with an absent child gains a copy with PAD in that position, making a padding region behave exactly like an absent child. Any native transitions the source had on all-padding leaves are overridden — canonical convolutions contain no all-padding node, so those transitions carry no meaning.

Return type:

SparseTreeAutomaton

Parameters:
autstr.utils.tree_automata_tools.tree_automaton(tree, base_alphabet, symbol_arity=1)[source]#

Automaton accepting exactly the given tree. Subtrees are hash-consed (one state per distinct subtree), so equal keys always share a target and the exception table stays deterministic; state 0 is the dead default.

Return type:

SparseTreeAutomaton

Parameters:

symbol_arity (int)

autstr.utils.tree_automata_tools.string_chain(word)[source]#

Embed a word as a unary left-spine tree: the first letter labels the root, each next letter its left child. Chain convolution then aligns positions from the root and pads at the bottom — exactly the string convolution convention.

autstr.utils.tree_automata_tools.from_string_dfa(dfa)[source]#

Embed a string DFA’s language as chain trees (see string_chain).

A bottom-up run reads the chain from the last letter to the first, so this is the reversal-determinization of the DFA: the tree state after a suffix v is the set {p : reading v from p reaches acceptance}, computed with pre-images over a dense next-state table (validation-scale sizes). The root accepts iff the DFA’s start state lies in the set.

Return type:

SparseTreeAutomaton

autstr.utils.tree_automata_tools.minimize(sta)[source]#

Minimize by Moore refinement over class-relabelled transition diagrams.

A state q is characterized by, for each side and each partner class c, the function symbol -> target class it induces together with any partner in c. Relabelling a pair’s diagram by the current classes turns that function into a hash-consed node, so a state’s signature is the set of triples (side, partner class, node) — one apply1 per listed pair per round. Child pairs absent from the table contribute the default’s class on every symbol, and are folded in by counting how much of each class a state has listed. Unreachable states are pruned first.

Return type:

SparseTreeAutomaton

Parameters:

sta (SparseTreeAutomaton)

autstr.utils.tree_automata_tools.equivalent(a, b)[source]#
Return type:

bool

Parameters:

Module contents#