[ondrik]

Fixes #40.

Problem

The inclusion searches start with one vertex per root state of A, built from the root states of B. If B has no root states, so its language is empty, that vertex is empty and *(vertex.begin()) is undefined behaviour:

• a <= b crashed with a segfault.
• autoq ver zero.lsta nop.qasm empty.lsta crashed with a segfault, even though the answer should be [failed].
• The symbolic ver grew its memory use until the process was killed.

ver reached this through a second bug. operator<<= unions B with the zero vector (zero_amplitude(n)), which normally gives B a root state. Here, reduce() merged that root state into an equivalent state that is not a root. It then dropped the root, because merged states were never mapped through for finalStates.

Changes

• src/reduce.cc, bottom_up_reduce(): records which state each merged-away state was merged into. Root states are mapped to that representative, with duplicates removed. A root state can no longer disappear in a merge. When a root is merged into another root, the result is the same as before.
• include/autoq/inclusion_bfs.hh (concrete and symbolic <<=) and src/inclusion/inclusion_index.cc (<=, == and the other comparisons): when B has no root states, they return autA.empty() straight away, since A ⊆ ∅ exactly when A is empty. The index version keeps the include-time bookkeeping.

Results

	Before	After
zero <= empty	segfault	false
ver zero.lsta nop.qasm empty.lsta	segfault (exit status 139)	[failed]
the same with a symbolic amplitude	memory grows until killed	[failed]
empty <= zero, ver zero.lsta nop.qasm zero.lsta, empty_c1.lsta control	unchanged	unchanged

Testing

• New unit test, inclusion_into_empty_automaton, using the issue's automata:

  • zero <= empty is false;
  • empty <= zero and empty <= empty are true;
  • zero <<= empty is false for concrete and symbolic amplitudes;
  • empty || zero_amplitude(1) keeps a root state and contains the zero vector.

  Without the fix, the test stops with a memory access violation. With it, the test passes. ctest passes (2/2).

• Unchanged behaviour on the benchmarks: reduce() runs on every automaton, so I compared this build against the saved outputs of the cleanup PR (Repository cleanup: stray files, dead code and duplicated logic #63). That covers 645 ver/ex runs from every benchmark family that finished within 20 s. 644 are identical. The remaining one, H2/500 ver, only hit the 60 s limit because 4 runs were going in parallel. Run on its own it gives the same [OK] in 23 s, against 22 s before.

• This branch merges cleanly with Playground: add the one-Grover-iteration demo #67, Report malformed input as an error instead of aborting (#56) #68 and Ignore trailing comments in OpenQASM input (#42, #47) #69.

🤖 Generated with Claude Code

https://claude.ai/code/session_013gtFQRPe1eSSpmA7EJ2KNY

[ondrik]

Checking that the reduce() change preserves the language

Why the change is correct. bottom_up_reduce() merges two states on a level only when they have exactly the same transitions: the same symbols, children (after earlier merges) and colours. Two such states accept exactly the same trees. Merging one into the other is therefore only correct if every reference to the merged-away state moves to its representative. The existing code did that for child references, but not for finalStates. A root state merged into an equivalent state that is not a root was then dropped by state_renumbering(), together with the trees it accepted. This PR moves finalStates the same way and removes duplicates. When a root is merged into another root, the result is the same as before.

Test. I wrote a standalone checker (source below) that computes the language of an automaton by brute force, without using AutoQ's code. A tree is accepted from a root state if there is one colour per level shared by every transition used on that level, the same rule print_language() implements. For each automaton, the checker compares the language before and after reduce(). I linked it once against the library built from main (3d92eb3) and once against this branch.

Automata	main	this PR
15,000 random automata (1–3 qubits, 1–4 states per level, colours from {1, 2, 3}, some states without transitions); each level copies the transitions of one or two templates, so equivalent states are common on every level	language changed by reduce() in 1,214	0
20,000 random cases: 10,000 automata, each also unioned with zero_amplitude(n), as operator<<= does	changed in 1,495	0
197 automata from benchmarks (pre.hsl/post.hsl from 52 small directories, the state after running each circuit, and each `post		zero_amplitude(n)), built with RED=0` and then reduced

• Every change on main that the checker printed lost trees. In each one, a root state was merged into a non-root. This means the bug is broader than the empty-automaton case in Inclusion check crashes when the right-hand automaton has no root states #40: whenever a root state is equivalent to a non-root state, reduce() could drop part of the language.
• Why the benchmarks never hit it: bottom_up_reduce() only keeps merging upward while every lower level had a merge, so roots are merged only when there are equivalent states on every level. My first random generator, without templates, rarely produced that and showed no differences even on main.
• An assumption the fix inherits: a state number appears on only one level. bottom_up_reduce() already relies on that, and every automaton AutoQ builds satisfies it.

reduce_check.cc

Build from the repository root after make:

c++ -std=c++20 -DCOMPLEX_FiveTuple -O2 -DNDEBUG -Iinclude -Iinclude/z3 -Iinclude/antlr4-runtime \
    reduce_check.cc build/src/liblsta.a libz3.so.4.12 -lantlr4-runtime -Wl,-rpath,$PWD -o reduce_check
./reduce_check random 5000 1
./reduce_check files benchmarks/all/BV/01

// Checks that Automata::reduce() preserves the language of an automaton.
//
// The language is computed by brute force, independently of AutoQ: a tree is
// accepted from a root state if there is one color per level such that every
// transition used at that level carries that color (the level-synchronized
// semantics that print_language() also implements).
//
// Usage: reduce_check random <count> <seed>
//        reduce_check files <dir>...   (each dir has pre.hsl, circuit.qasm, post.hsl)
#include "autoq/aut_description.hh"
#include "autoq/parsing/parser/timbuk_parser.hh"
#include <cstdlib>
#include <iostream>
#include <random>
#include <set>
#include <sstream>
#include <string>
#include <vector>

using Tree = std::vector<std::string>;
using Language = std::set<Tree>;
struct TooBig {};
constexpr size_t kMaxTrees = 200000;

template <typename Symbol>
std::set<Tree> trees(const AUTOQ::Automata<Symbol>& aut, typename AUTOQ::Automata<Symbol>::State q,
                     int level, const std::vector<int>& color) {
    std::set<Tree> out;
    for (const auto& [st, outs] : aut.transitions) {
        if (!(st.tag() & (1ULL << color[level]))) continue;
        bool leaf_level = level == aut.qubitNum + 1;
        if (leaf_level != st.symbol().is_leaf()) continue;
        if (!leaf_level && st.symbol().qubit() != level) continue;
        auto it = outs.find(q);
        if (it == outs.end()) continue;
        for (const auto& in : it->second) {
            if (leaf_level) {
                std::ostringstream ss;
                ss << st.symbol();
                out.insert({ss.str()});
                continue;
            }
            auto L = trees(aut, in.at(0), level + 1, color);
            auto R = trees(aut, in.at(1), level + 1, color);
            if (L.size() * R.size() > kMaxTrees) throw TooBig{};
            for (const auto& l : L)
                for (const auto& r : R) {
                    Tree t = l;
                    t.insert(t.end(), r.begin(), r.end());
                    out.insert(t);
                }
        }
    }
    if (out.size() > kMaxTrees) throw TooBig{};
    return out;
}

template <typename Symbol>
Language language(const AUTOQ::Automata<Symbol>& aut) {
    typename AUTOQ::Automata<Symbol>::Tag all = 0;
    for (const auto& [st, outs] : aut.transitions) all |= st.tag();
    std::vector<int> bits;
    for (int b = 0; b < 64; b++) if (all & (1ULL << b)) bits.push_back(b);
    Language lang;
    if (bits.empty()) return lang;
    int levels = aut.qubitNum + 1;
    std::vector<size_t> idx(levels + 1, 0); // one color index per level 1..levels
    while (true) {
        std::vector<int> color(levels + 1);
        for (int l = 1; l <= levels; l++) color[l] = bits[idx[l]];
        for (auto r : aut.finalStates)
            for (auto& t : trees(aut, r, 1, color)) lang.insert(t);
        if (lang.size() > kMaxTrees) throw TooBig{};
        int l = 1;
        while (l <= levels && ++idx[l] == bits.size()) idx[l++] = 0;
        if (l > levels) break;
    }
    return lang;
}

// Random level-structured automaton with few distinct shapes, so that many
// states are equivalent and some root states are equivalent to non-roots.
AUTOQ::ConcreteAutomata random_automaton(std::mt19937& rng) {
    using Aut = AUTOQ::ConcreteAutomata;
    auto pick = [&](int lo, int hi) { return std::uniform_int_distribution<int>(lo, hi)(rng); };
    Aut aut;
    aut.qubitNum = pick(1, 3);
    aut.hasLoop = false;
    std::vector<std::vector<Aut::State>> layer(aut.qubitNum + 2);
    Aut::State next = 0;
    for (int l = 1; l <= aut.qubitNum + 1; l++)
        for (int k = pick(1, 4); k > 0; k--) layer[l].push_back(next++);
    aut.stateNum = next;
    const AUTOQ::Complex::Complex values[] = {AUTOQ::Complex::Complex::Zero(), AUTOQ::Complex::Complex::One(),
                                             AUTOQ::Complex::Complex::One() + AUTOQ::Complex::Complex::One()};
    // Each state copies the transitions of one of a few templates per level, so
    // that equivalent states are common on every level.
    for (int l = 1; l <= aut.qubitNum + 1; l++) {
        int templates = pick(1, 2);
        std::vector<std::vector<std::pair<Aut::SymbolTag, Aut::StateVector>>> tpl(templates);
        for (auto& t : tpl) {
            int count = pick(0, 9) == 0 ? 0 : pick(1, 2); // sometimes no transitions at all
            for (int k = 0; k < count; k++) {
                Aut::Tag tag = pick(1, 3);
                if (l == aut.qubitNum + 1) {
                    t.push_back({{AUTOQ::Symbol::Concrete(values[pick(0, 2)]), tag}, {}});
                } else {
                    auto& below = layer[l + 1];
                    t.push_back({{AUTOQ::Symbol::Concrete(l), tag},
                                 {below[pick(0, below.size() - 1)], below[pick(0, below.size() - 1)]}});
                }
            }
        }
        for (auto q : layer[l])
            for (const auto& [st, in] : tpl[pick(0, templates - 1)])
                aut.transitions[st][q].insert(in);
    }
    for (auto q : layer[1])
        if (pick(0, 1)) aut.finalStates.push_back(q);
    return aut;
}

struct Counts { int checked = 0, mismatched = 0, skipped = 0, roots_changed = 0; };

template <typename Symbol>
void check(const AUTOQ::Automata<Symbol>& aut, const std::string& name, Counts& c) {
    try {
        auto before = language(aut);
        auto reduced = aut;
        unsetenv("RED");
        reduced.reduce();
        auto after = language(reduced);
        c.checked++;
        if (reduced.finalStates.size() != aut.finalStates.size()) c.roots_changed++;
        if (before != after) {
            c.mismatched++;
            if (c.mismatched <= 5)
                std::cout << "MISMATCH " << name << ": " << before.size() << " trees before reduce, "
                          << after.size() << " after; roots " << aut.finalStates.size() << " -> "
                          << reduced.finalStates.size() << "\n";
        }
    } catch (const TooBig&) {
        c.skipped++;
    }
}

int main(int argc, char** argv) {
    Counts c;
    std::string mode = argc > 1 ? argv[1] : "";
    if (mode == "random") {
        int n = std::atoi(argv[2]);
        std::mt19937 rng(std::atoi(argv[3]));
        for (int i = 0; i < n; i++) {
            auto aut = random_automaton(rng);
            check(aut, "random#" + std::to_string(i), c);
            // The union that operator<<= builds: B || zero vector.
            setenv("RED", "0", 1);
            auto with_zero = aut || AUTOQ::ConcreteAutomata::zero_amplitude(aut.qubitNum);
            check(with_zero, "random#" + std::to_string(i) + " || zero", c);
        }
    } else if (mode == "files") {
        for (int i = 2; i < argc; i++) {
            std::string d = argv[i];
            for (std::string f : {"pre.hsl", "post.hsl"}) {
                setenv("RED", "0", 1); // build the automata without reducing them
                try {
                    auto aut = AUTOQ::Parsing::TimbukParser<AUTOQ::Symbol::Concrete>::ReadAutomaton(d + "/" + f);
                    check(aut, d + "/" + f, c);
                    setenv("RED", "0", 1);
                    check(aut || AUTOQ::ConcreteAutomata::zero_amplitude(aut.qubitNum), d + "/" + f + " || zero", c);
                    if (f == "pre.hsl") {
                        setenv("RED", "0", 1);
                        aut.execute(d + "/circuit.qasm", {}, {}, {});
                        check(aut, d + "/circuit.qasm", c);
                    }
                } catch (const std::exception&) {
                    setenv("RED", "0", 1);
                    try {
                        auto aut = AUTOQ::Parsing::TimbukParser<AUTOQ::Symbol::Symbolic>::ReadAutomaton(d + "/" + f);
                        check(aut, d + "/" + f + " (symbolic)", c);
                    } catch (const std::exception& e) {
                        c.skipped++;
                    }
                }
            }
        }
    }
    std::cout << "checked " << c.checked << ", language changed by reduce: " << c.mismatched
              << ", root count changed: " << c.roots_changed << ", skipped (too large or unparsable): "
              << c.skipped << "\n";
    return c.mismatched ? 1 : 0;
}

🤖 Generated with Claude Code

https://claude.ai/code/session_013gtFQRPe1eSSpmA7EJ2KNY