Replace automata backend

.github/workflows/run_tests.yaml

@@ -10,11 +10,11 @@
     run_all_tests:
       runs-on: 'ubuntu-latest'
       steps:
-        - uses: actions/checkout@v2
+        - uses: actions/checkout@v4
         - name: Install Python 3
-          uses: actions/setup-python@v1
+          uses: actions/setup-python@v5
           with:
-            python-version: 3.9
+            python-version: 3.11
         - name: Install dependencies
           run: |
             python -m pip install --upgrade pip

README.md

@@ -2,7 +2,13 @@
 Working with infinite data structures in Python.
 
 ## Introduction
-Have you ever wondered what would happen if you could input an infinite structure (e.g., an infinite graph) into your algorithm instead of a finite one? With AutStr, you can do exactly that for certain infinite structures. AutStr provides an easy-to-use interface for defining relational structures over predefined infinite base structures. Currently, AutStr offers built-in support for a robust extension of linear integer arithmetic, while additional base structures over arbitrary countable domains can be defined via the low-level API.
+What if your algorithms could process infinite structures — like complete infinite graphs or the entire set of natural numbers — with the same ease as manipulating a data frame? AutStr provides an intuitive interface for defining and manipulating exact representations of infinite relational structures. With AutStr, infinite structures become first-class citizens in Python.
+
+Targeted at researchers in algorithmic model theory and curious practitioners alike, AutStr offers:
+- **Symbolic representation** of infinite sets and relations
+- **Automata-based computation** for efficient manipulation
+- **First-order logic interface** for formal queries
+- **Visualization tools** for insight into infinite structures
 
 ### Installation with `uv` 
 Here's how to install AutStr using `uv`, the high-performance Python package installer:
@@ -222,31 +228,14 @@ VisualDFA(remaining.evaluate()).show_diagram()
    # width=2 (easier):
    narrow = "∃x.∃y.E(x,y) ∧ (∃z.E(y,z))"
    ```
-   - Depth scales often better due to incremental minimization
-   - Width causes exponential alphabet growth: $|\Sigma|^k$
+   - Depth can cause non-elementary(!) statespace explosion but scales often much better due to incremental minimization
+   - Width causes exponential alphabet growth: $|\Sigma|^k$ but SparseDFAs can avoid explicit enumeration of entire alphabet in many cases.
 
 2. **Complexity Boundaries**
    | Parameter        | Best Case       | Worst Case          |
    |------------------|-----------------|---------------------|
    | **Quantifier Depth** | Constant state space   | Non-elementary state space |
-   | **Free Variables**  | Exponential alphabet size  | Exponential alphabet size |
-
-4. **Optimization Strategies**
-   - **Minimize aggressively**:
-     ```python
-     candidates = (candidates - multiples).minify()  # Force state reduction
-     ```
-   - **Avoid high-arity**:
-     ```python
-     # Decompose wide relations:
-     R1 = project(relation, ['x','y'])
-     R2 = project(relation, ['z'])
-     ```
-   - **Use bounded quantification**:
-     ```python
-     # Instead of ∀x.φ(x), use:
-     bounded = ∀(x, x<1000).φ(x)  # Finite domain restriction
-     ```
+   | **Free Variables**  | constant number of exceptions  | Exponential alphabet size |
 
 #### Theoretical Insight
 While this infinite sieve beautifully demonstrates symbolic algorithm design, state complexity grows rapidly for sieved primes
@@ -268,17 +257,53 @@ This implementation provides a complete toolkit for working with automatic struc
 ### Final Note
 AutStr began as a summer passion project in 2022—a practical exploration of the automatic structures I'd studied theoretically during my PhD. This library represents the intersection of academic curiosity and hands-on implementation, born from a desire to make abstract model theory concepts tangible.
 
-Released in June 2025 as-is, the library remains fundamentally unchanged from its original vision except for:
+Released in July 2025 following a major update, the library now includes significant new features beyond its original vision. This update was developed through a vibe coding session using DeepSeek, with extensive human testing and supervision throughout the process.
+
+Highlights of the update:
+- Newly implemented `sparse_dfa` backend for efficient automata operations
+- Serialization support for automata and structures
+- MSO0 as finite powerset structure over natural numbers (e.g. index sets)
 - Modernized packaging (`pyproject.toml`)
 - Dependency version updates
 - Expanded documentation
 
-While not actively maintained, AutStr stands as:
-1. A functional implementation of basic automatic structure theory
-2. A testament to the elegance of infinite-state computation
-3. An invitation to explore algorithmic model theory hands-on
+#### Performance and Maintenance
+Recent updates have removed obvious performance bottlenecks through:
+
+- JAX-accelerated automata operations
+- Sparse DFA representations
+- Efficient serialization, which allows storing precompiled results
+
+However, significant optimization opportunities remain:
+- Vectorization: Many sequential operations could still be parallelized
+- Query Optimization: Advanced planning for first-order queries
+
+As this is a passion project developed outside my primary research, active maintenance will be limited. That said:
+
+- Bug reports are welcome and will be prioritized
+- Performance contributions are especially appreciated
+- Research collaborations involving AutStr are encouraged
+
+
+## References on Automatic Structures
+1. **Abu Zaid, F.**  
+   *Algorithmic Solutions via Model Theoretic Interpretations.*  
+   Dissertation, RWTH Aachen University, 2016.  
+   DOI: [10.18154/RWTH-2017-07663](https://doi.org/10.18154/RWTH-2017-07663)  
+
+2. **Blumensath, A., & Grädel, E.**  
+   *Automatic Structures.*  
+   Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS 2000).  
+   Pages: 51–62.  
+   URL: [LICS 2000 Proceedings](https://lics.siglog.org/2000/Grdel-AutomaticStructures.html)  
 
-> "Some things are worth building not because they scale, but because they reveal."  
-> — Faried Abu Zaid, June 2025
+3. **Khoussainov, B., & Nerode, A.**  
+   *Automatic presentations of structures.*  
+   In D. Leivant (Ed.), Logic and Computational Complexity (LCC 1994). Lecture Notes in Computer Science, vol 960.  
+   Springer. DOI: [10.1007/3-540-60178-3_93](https://doi.org/10.1007/3-540-60178-3_93)  
 
-For researchers and enthusiasts: May this implementation spark new insights into the beautiful complexity of infinite structures. For practical applications, consider pairing with finite approximations or domain-specific abstractions.
+4. **Khoussainov, B., Rubin, S., & Stephan, F.**  
+   *Automatic Structures: Richness and Limitations.*  
+   Logical Methods in Computer Science, Volume 3, Issue 2 (2007).  
+   arXiv: [cs/0703064](https://arxiv.org/abs/cs/0703064)  
+   DOI: [10.2168/LMCS-3(2:2)2007](https://doi.org/10.2168/LMCS-3%282%3A2%292007)  

autstr/arithmetic.py

@@ -2,22 +2,22 @@
 
 from abc import ABC, abstractmethod
 from copy import deepcopy, copy
-from typing import List, Union, Tuple, Dict, Set
+from typing import List, Union, Tuple, Dict
 import math
 
-from automata.fa.dfa import DFA
-
 from autstr.buildin.automata import k_longer_automaton
+from autstr.sparse_automata import SparseDFA
 from autstr.utils.automata_tools import iterate_language, lsbf_Z_automaton
-from autstr.buildin.presentations import buechi_arithmetic_Z
+from autstr.buildin.presentations import BuechiArithmeticZ
 from autstr.utils.misc import get_unique_id
+from autstr.utils.misc import encode_symbol, decode_symbol
 
 
 class Term(ABC):
     """
     Abstract class representing a term over the (base 2) Büchi arithmetic over the integers :math:`\\mathbb{Z}`
     """
-    arithmetic = buechi_arithmetic_Z()
+    arithmetic = BuechiArithmeticZ()
 
     def __init__(self):
         self.presentation = None
@@ -32,7 +32,7 @@ def update_presentation(self, recursive=True) -> None:
         """
         raise NotImplementedError
 
-    def evaluate(self) -> DFA:
+    def evaluate(self) -> SparseDFA:
         """
         Returns automatic presentation of the relation.
 
@@ -119,7 +119,7 @@ def __contains__(self, item):
                 words[i] = w + ('*' * difference)
 
         input_word = [tuple(w[i] for w in words) for i in range(l_max)]
-        return self.evaluate().accepts_input(input_word)
+        return self.evaluate().accepts(input_word)
 
     def drop(self, variables: List[Union[str, VariableETerm]]) -> DropRATerm:
         """
@@ -157,7 +157,7 @@ def isempty(self) -> bool:
         if self.presentation is None:
             self.update_presentation()
 
-        return self.presentation.isempty()
+        return self.presentation.is_empty()
 
     def isfinite(self) -> bool:
         """
@@ -168,7 +168,7 @@ def isfinite(self) -> bool:
         if self.presentation is None:
             self.update_presentation()
 
-        return self.presentation.isfinite()
+        return self.presentation.is_finite()
 
     def __iter__(self):
         """
@@ -180,7 +180,7 @@ def __iter__(self):
         if self.presentation is None:
             self.update_presentation()
 
-        for t in iterate_language(self.presentation, backward=True):
+        for t in iterate_language(self.presentation, backward=True, padding_symbol='*'):
             yield tuple(
                 int(
                     n.replace('*', '')[:-1], base=2
@@ -201,8 +201,8 @@ def update_presentation(self, recursive=True) -> None:
             self.subterm.update_presentation(recursive)
 
         sub_presentation = self.subterm.evaluate()
-        k_distance = len(sub_presentation.states) + 1
-        inf_witness = k_longer_automaton(k_distance, len(self.subterm.get_variables()) - 1, self.arithmetic.sigma)
+        k_distance = sub_presentation.num_states + 1
+        inf_witness = k_longer_automaton(k_distance, len(self.subterm.get_variables()) - 1, self.arithmetic.sigma, self.arithmetic.padding_symbol)
         arithmetic = deepcopy(self.arithmetic)
         T, L = get_unique_id(arithmetic.get_relation_symbols(), 2)
         arithmetic.update(**{T: self.subterm.evaluate(), L: inf_witness})
@@ -504,9 +504,9 @@ def gt(self, other) -> BaseRATerm:
         :param other: The term on the lhs
         :return:
         """
-        return BaseRATerm('Lt', [other, self])
+        return BaseRATerm('Gt', [self, other])
 
-    def evaluate(self) -> DFA:
+    def evaluate(self) -> SparseDFA:
         if self.presentation is None:
             self.update_presentation()