--loopsum never finishes when the precondition has more than one state #66

Summary

With --loopsum, a for loop never finishes when the precondition contains more than one state. Without --loopsum the same input finishes instantly. This affects both ex and ver, and it already happens with one qubit, one x gate and one iteration.

Minimal example

pre.hsl

Extended Dirac
{|0>, |1>}

circuit.qasm

OPENQASM 3;
include "stdgates.inc";
qubit[1] q;

for int i in [1:1] {
    x q[0];
}

post.hsl

Extended Dirac
{|0>, |1>}

autoq ex  pre.hsl circuit.qasm
autoq ex  pre.hsl circuit.qasm --loopsum
autoq ver pre.hsl circuit.qasm post.hsl --loopsum

Observed

• ex without --loopsum prints {(1/1)|0>, (1/1)|1>} immediately.
• ex --loopsum and ver --loopsum use 100% of one CPU and were stopped after 20 s.
• ver without --loopsum prints [OK].

Other inputs I tried

Every multi-state precondition I tried hangs, independent of the gate and of the number of qubits:

Single-state preconditions such as {|00>} or {1/sqrt2 |00> + ei2pi(1/8)/sqrt2 |11>} finish at once.

What happens

I added temporary debug output after each refinement round in symbolic_loop. It printed the number of final states of Tref and the number of summarization variables:

round 1: finals=4   states=8   vars=4   changed=1
round 2: finals=16  states=32  vars=8   changed=1
round 3: finals=256 states=512 vars=16  changed=1
(round 4 did not finish)

The number of root states squares every round: 2 → 4 → 16 → 256 → 65,536. changes_behavior is set every round, so the fix point is never reached.

Possible cause (not verified)

refinement starts the product from every pair of a final state of T and a final state of Tref, and each pair becomes a new final state. With k roots the product has k² roots, and it becomes the next round's Tref. Pairs of unrelated roots (for example the tree for |0> before the body with the tree for |1> after it) then give the same "before" variable two different "after" values. eval_mapping therefore splits a variable and sets changes_behavior again:

With a single root, k² = 1, which would explain why single-state preconditions are unaffected.

A secondary slowdown: a stack sample taken during the hang was inside std::hash<AUTOQ::Symbol::Symbolic>. Hashing goes through Symbolic::str(), which creates a Z3 context (Z3_mk_context_rc) on every call, so each lookup in the unordered_maps used by eval_mapping is costly.

Expected

--loopsum should finish and give the same states as unrolling: {(1/1)|0>, (1/1)|1>} for the example above.

Found at 000801e28 (native Release build, Ubuntu 24.04). src/ is unchanged on current main (849709f6c), and the branch of #65 (the fix for #22) behaves the same.