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.
- 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.
- autstr.utils.automata_tools.shortlex_order(base_alphabet, padding_symbol)[source]#
The binary automaton for
x <= yin shortlex order: shorter words first, ties broken by the alphabet’s own order, trailing padding ignored.Shortlex is a well-order, so every non-empty set of elements has a unique least member – which is exactly what picks the canonical representative of an equivalence class for a quotient interpretation.
- Return type:
- autstr.utils.automata_tools.fold_tapes(dfa, k)[source]#
Group every k consecutive tapes of a convolution into one tape over the product alphabet Sigma^k.
An automaton reading
k * rtapes over Sigma becomes one readingrtapes whose letters are k-tuples – the fold that turns the many-tape output of a k-dimensional interpretation into a structure whose elements are k-tuples. The diagram is unchanged in spirit (no state is added); only the alphabet is regrouped, and lexicographic tuple order matches encode_symbol, so membership lines up.
- autstr.utils.automata_tools.canonical(dfa, padding_symbol=-1)[source]#
Keep only the canonical convolution of each tuple: words in which no position is padding on every tape.
pad and unpad deliberately leave the all-padding self-loops in place, so a relation automaton accepts every tuple in infinitely many spellings – the convolution followed by any number of all-padding columns. That is invisible to membership and to enumeration (iterate_language skips the all-padding symbol), but it makes every non-empty relation look infinite to a word-level cycle test. Restricting to canonical words first is what makes finiteness and counting questions about tuples rather than about words.
- autstr.utils.automata_tools.product(dfa, n)[source]#
Create the n-fold Cartesian product of the automaton’s language.
- 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
- 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.
- 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.
- 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:
- Return type:
- 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.
- 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.
- 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
- autstr.utils.automata_tools.partial_dfa(base_alphabet, arity, transitions, initial, final)[source]#
A DFA over arity tapes from a partial transition table.
Every symbol tuple a state does not list goes to a rejecting sink, which is what an automaton authored by hand almost always wants: the interesting transitions are few and the alphabet — a product of k copies of the base — is large, so spelling the table out in full costs
|Σ|^kentries per state to say “reject” over and over.- Parameters:
base_alphabet (
Set) – the base alphabet, padding symbol included.arity (
int) – number of tapes; the automaton reads arity-tuples.transitions (
Dict[str,Dict[tuple,str]]) –{state: {symbol tuple: target state}}. Its keys are the states, in the order they are numbered.initial (
str) – the start state.
- Return type:
- Returns:
a minimized SparseDFA.
- autstr.utils.automata_tools.length_automaton(n, base_alphabet)[source]#
Creates an automaton that recognizes all words over base_alphabet with length exactly n.
- autstr.utils.automata_tools.k_longer_automaton(k, r, base_alphabet, padding_symbol)[source]#
Creates an automaton recognizing (r+1)-tuples where the last word is at least k letters longer than the other r words.
- autstr.utils.automata_tools.zero(symbol_arity=1, base_alphabet=None)[source]#
Automaton that rejects all inputs.
- autstr.utils.automata_tools.one(symbol_arity=1, base_alphabet=None)[source]#
Automaton that accepts all inputs.
autstr.utils.logic module#
autstr.utils.misc module#
- autstr.utils.misc.cmp_llex(v, w)[source]#
Length-lexicographic ordering of a tuple of strings ignoring the padding symbol.
- autstr.utils.misc.encode_symbol(tuple_symbol, base_alphabet)[source]#
Encode a symbol tuple into a single integer.
- autstr.utils.misc.decode_symbol(enc, arity, base_alphabet)[source]#
Decode an integer into a symbol tuple.
- autstr.utils.misc.complement(values, min_val, max_val)[source]#
Find the complement of a set of values within a specified range.
- autstr.utils.misc.alphabet_from_json(raw)[source]#
The base alphabet as stored in a serialized payload.
JSON has no tuples, so a product alphabet’s letters – which is what an interpreted structure of dimension > 1 has – come back as lists. Restore them, or the set() built from them raises on the first unhashable letter.
- Return type:
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:
- Parameters:
sta (SparseTreeAutomaton)
new_arity (int)
- 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:
- Parameters:
sta (SparseTreeAutomaton)
- autstr.utils.tree_automata_tools.fold_tapes(sta, k)[source]#
Group every k consecutive tapes of a convolution into one tape over the product alphabet Sigma^k.
An automaton reading
k * rtapes over Sigma becomes one readingrtapes whose letters are k-tuples — the fold that turns the many-tape output of a k-dimensional interpretation into a structure whose elements are k-tuples of trees. Since the convolution of k trees is one tree over k-tuples, an element of the interpreted structure is such a tree, and nothing about the shapes changes: the fold only regroups the alphabet.The regrouping is the same diagram surgery as in the string engine — the symbol diagrams are ordinary MTBDDs either way, so NodeStore.fold_tapes does the work here too, applied to each child pair’s diagram. No state is added, and lexicographic tuple order matches encode_symbol, so encodings line up.
- Return type:
- Parameters:
sta (SparseTreeAutomaton)
k (int)
- 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:
- Parameters:
sta (SparseTreeAutomaton)
tape (int)
max_states (int | None)
- autstr.utils.tree_automata_tools.tree_order(base_alphabet, padding_symbol, strict=False)[source]#
The binary automaton for
x <= y: compare the two trees at the lexicographically least position where they differ, an absent position counting as larger than any letter.Positions are ordered as the traversal visits them — a node, then its left subtree, then its right — so the verdict of a node is its own letters’, or, where those agree, its left subtree’s, or, where that is equal too, its right subtree’s.
This is a linear order on trees, and it is not well-founded: growing a tree at the position where two differ makes it smaller, so an infinite descending chain is easy to write down and a set of trees need have no least member. That is the whole reason a quotient over trees cannot pick the least element of a class the way the string engine’s shortlex order does; see autstr.interpretations.
- Parameters:
strict (
bool) – acceptx < yrather thanx <= y.- Return type:
- autstr.utils.tree_automata_tools.domain_within(base_alphabet, padding_symbol, depth=0)[source]#
The binary automaton for
dom(x) ⊆ dom(y)·{1,2}^{≤depth}: every position of x lies at most depth levels below a position of y.At
depth = 0this is plain domain containment. Deeper, it is the “fringe” relation the tree quotient construction needs: a description of an equivalence class is a member that reaches only so far past the class’s shadow.A tree’s domain is prefix-closed, so y’s positions form a region hanging from the root, and every position of x outside it is a fixed number of levels below where that region stops. The automaton therefore carries, up from the leaves, how far the deepest still-uncovered position of x is.
- Return type:
- Parameters:
depth (int)
- 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:
- Parameters:
sta (SparseTreeAutomaton)
max_states (int | None)
- autstr.utils.tree_automata_tools.canonical(sta, padding_symbol)[source]#
Keep only the canonical convolution of each tuple: trees in which no node is padding on every tape.
attach_padding deliberately accepts each tuple with arbitrary all-padding regions hanging below it, so the tree language of a saturated relation automaton is infinite as soon as the relation is non-empty. Restricting to canonical trees first is what makes finiteness and counting questions be about tuples rather than about trees – the tree analog of automata_tools.canonical.
- Return type:
- Parameters:
sta (SparseTreeAutomaton)
- autstr.utils.tree_automata_tools.k_deeper_automaton(k, references, base_alphabet, padding_symbol)[source]#
Convolutions whose last tape runs at least k nodes below every reference tape: some root-to-leaf path carries k nodes at which all references reference tapes are padding and the last tape is not.
The tree counterpart of automata_tools.k_longer_automaton, and it supports exists-infinity for the same pumping reason. A tree’s domain is closed under parents, so the nodes outside every reference’s domain form a suffix of each root-to-leaf path; k of them make a body automaton with fewer than k states repeat along that path, and the context between the two occurrences pumps without ever touching the references.
Requiring the last tape to be present is what keeps this sound under attach_padding, which hangs all-padding regions below a tree: those nodes have every reference padded too, so counting them would manufacture depth that carries no witness.
- Return type:
- Parameters:
- autstr.utils.tree_automata_tools.iterate_trees(sta, max_entries=10000000)[source]#
Generate the accepted trees in shortlex order: by node count, then by _shortlex_key.
Size is the tree’s own node count, which is the faithful analogue of the string engine’s length-lexicographic order – and, like it, says nothing about what the encoded values are. For Büchi arithmetic word length is ceil(log2|n|), so shortlex happens to enumerate integers by increasing absolute value; for Skolem arithmetic the tree size is instead the prime index plus the exponents’ bit lengths, so 128 arrives before 7. Any value-ordering belongs to the codec, not here: for Skolem the magnitude order is not even recognizable, since (N, *, <) is undecidable while every tree-automatic structure has a decidable theory.
Trees of every size below the one being yielded are retained, since they are the subtrees of the larger ones – enumeration of an infinite language grows without bound by nature.
- Parameters:
sta (SparseTreeAutomaton)
max_entries (int)
- autstr.utils.tree_automata_tools.restrict_alphabet(sta, base_alphabet)[source]#
The same automaton, read over a smaller alphabet.
Every letter of base_alphabet must be one the automaton already has, and the automaton keeps its behaviour on exactly those; what it did on the letters being dropped simply goes away. That is what a construction wants once a scaffolding letter has served its purpose — an annotation the automaton was built to read and a projection has since quantified away leaves the alphabet wider than the structure it belongs to.
The rewrite is one memoized pass over the diagrams: dropping letters narrows the digit blocks rather than rebuilding any transition table.
- Return type:
- Parameters:
sta (SparseTreeAutomaton)
- autstr.utils.tree_automata_tools.partial_tree_automaton(base_alphabet, symbol_arity, transitions, final)[source]#
A bottom-up tree automaton from a partial transition table — the tree counterpart of autstr.utils.automata_tools.partial_dfa.
Everything the table does not list goes to a rejecting sink, which is what an automaton authored by hand almost always wants: a convolution alphabet is a product, so spelling out “reject” for every combination of child states and symbols would swamp the few transitions that carry the meaning.
- Parameters:
- Return type:
- Returns:
a minimized SparseTreeAutomaton.
- 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:
- 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:
- 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:
- Parameters:
sta (SparseTreeAutomaton)