See https://lipsum.dev/2024-01-1-automates-regex-presburger/

presburger-dfa.py

from automathon import DFA
from collections import defaultdict
from itertools import zip_longest
from math import floor
from random import randint

# See https://www21.in.tum.de/teaching/sar/SS20/9.pdf

def ineq_to_dfa(A: list[int], b: int) -> DFA:
    n = len(A)
    Q = set()
    sigma = {bin(i)[2:].zfill(n) for i in range(2**n)}
    delta = defaultdict(dict)
    F = set()
    W = {b}
    while W:
        k = W.pop()
        Q.add(k)
        if k >= 0:
            F.add(str(k))
        for s in sigma:
            j = floor((k - sum(a * int(d) for a, d in zip(A, s))) / 2)
            if j not in Q:
                W.add(j)
            delta[str(k)][s] = str(j)
    # authomaton.DFA requires states to be strings
    return DFA({str(q) for q in Q}, sigma, delta, str(b), F)

### Build a DFA for 2x + 3y <= 100

A = [2, 3]
b = 100

automata = ineq_to_dfa(A, b)

def encode(*args):
    return ["".join(digits) for digits in zip_longest(*(bin(x)[-1:1:-1] for x in args), fillvalue="0")]

for _ in range(10):
    X = tuple(randint(0, 2 * b / sum(A)) for _ in range(len(A)))
    print((X, sum(a * x for a, x in zip(A, X)), automata.accept(encode(*X))))