From 98bd939436f7b8473ded86bd45796f13dea9d533 Mon Sep 17 00:00:00 2001
From: Mikael Zayenz Lagerkvist <research@zayenz.se>
Date: Tue, 28 Jul 2026 09:50:28 +0200
Subject: [PATCH 1/3] Reduce regular layered graph allocation

---
 gecode/int/extensional/layered-graph.hpp | 299 ++++++++++++----------
 test/int/extensional.cpp                 | 302 +++++++++++++++++++++++
 2 files changed, 471 insertions(+), 130 deletions(-)

diff --git a/gecode/int/extensional/layered-graph.hpp b/gecode/int/extensional/layered-graph.hpp
index 3ceb91fa35..3b069a4988 100755
--- a/gecode/int/extensional/layered-graph.hpp
+++ b/gecode/int/extensional/layered-graph.hpp
@@ -33,6 +33,7 @@
 
 #include <climits>
 #include <algorithm>
+#include <limits>
 
 namespace Gecode { namespace Int { namespace Extensional {
 
@@ -266,163 +267,202 @@ namespace Gecode { namespace Int { namespace Extensional {
                                                      const VarArgArray<Var>& x,
                                                      const DFA& dfa) {
 
-    Region r;
-
     // Allocate memory for layers
     layers = home.alloc<Layer>(n+1);
 
-    // Allocate temporary memory for all possible states
-    State* states = r.alloc<State>(max_states*(n+1));
-    for (int i=0; i<static_cast<int>(max_states)*(n+1); i++)
-      states[i].init();
-    for (int i=0; i<n+1; i++)
-      layers[i].states = states + i*max_states;
+    const int n_dfa_states = dfa.n_states();
+
+    {
+      Region r;
 
-    // Allocate temporary memory for edges
-    Edge* edges = r.alloc<Edge>(dfa.max_degree());
+      // Allocate temporary memory for edges
+      Edge* edges = r.alloc<Edge>(dfa.max_degree());
+
+      // Reachability sets and touched states
+      unsigned char* i_reachable = r.alloc<unsigned char>(n_dfa_states);
+      unsigned char* o_reachable = r.alloc<unsigned char>(n_dfa_states);
+      StateIdx* i_reached = r.alloc<StateIdx>(n_dfa_states);
+      StateIdx* o_reached = r.alloc<StateIdx>(n_dfa_states);
+      for (int i=0; i<n_dfa_states; i++)
+        i_reachable[i] = o_reachable[i] = 0;
+      unsigned int n_i_reached = 1;
+      unsigned int n_o_reached = 0;
+      i_reachable[0] = 1;
+      i_reached[0] = 0;
+
+      // Forward pass: add transitions
+      for (int i=0; i<n; i++) {
+        layers[i].x = x[i];
+        layers[i].support = home.alloc<Support>(layers[i].x.size());
+        ValSize j=0;
+        // Clear the next frontier
+        for (unsigned int k=0; k<n_o_reached; k++)
+          o_reachable[o_reached[k]] = 0;
+        n_o_reached = 0;
+        // Enter links leaving reachable states
+        for (ViewValues<View> nx(layers[i].x); nx(); ++nx) {
+          unsigned int n_support_edges=0;
+          for (DFA::Transitions t(dfa,nx.val()); t(); ++t)
+            if (i_reachable[t.i_state()] != 0) {
+              edges[n_support_edges].i_state =
+                static_cast<StateIdx>(t.i_state());
+              edges[n_support_edges].o_state =
+                static_cast<StateIdx>(t.o_state());
+              n_support_edges++;
+              if (o_reachable[t.o_state()] == 0) {
+                o_reachable[t.o_state()] = 1;
+                o_reached[n_o_reached++] =
+                  static_cast<StateIdx>(t.o_state());
+              }
+            }
+          assert(n_support_edges <= dfa.max_degree());
+          // Found support for value
+          if (n_support_edges > 0) {
+            Support& s = layers[i].support[j];
+            s.val = static_cast<Val>(nx.val());
+            s.n_edges = static_cast<Degree>(n_support_edges);
+            s.edges = Heap::copy(home.alloc<Edge>(n_support_edges),edges,
+                                 n_support_edges);
+            j++;
+          }
+        }
+        if ((layers[i].size = j) == 0)
+          return ES_FAILED;
+        std::swap(i_reachable,o_reachable);
+        std::swap(i_reached,o_reached);
+        std::swap(n_i_reached,n_o_reached);
+      }
+    }
 
-    // Mark initial state as being reachable
-    i_state(0,0).i_deg = 1;
+    Region r;
 
-    // Forward pass: add transitions
-    for (int i=0; i<n; i++) {
-      layers[i].x = x[i];
-      layers[i].support = home.alloc<Support>(layers[i].x.size());
-      ValSize j=0;
-      // Enter links leaving reachable states (indegree != 0)
-      for (ViewValues<View> nx(layers[i].x); nx(); ++nx) {
-        Degree n_edges=0;
-        for (DFA::Transitions t(dfa,nx.val()); t(); ++t)
-          if (i_state(i,static_cast<StateIdx>(t.i_state())).i_deg != 0) {
-            i_state(i,static_cast<StateIdx>(t.i_state())).o_deg++;
-            o_state(i,static_cast<StateIdx>(t.o_state())).i_deg++;
-            edges[n_edges].i_state = static_cast<StateIdx>(t.i_state());
-            edges[n_edges].o_state = static_cast<StateIdx>(t.o_state());
-            n_edges++;
+    // Maps from DFA state IDs to layer-local state indices
+    StateIdx* i_map = r.alloc<StateIdx>(n_dfa_states);
+    StateIdx* o_map = r.alloc<StateIdx>(n_dfa_states);
+    unsigned char* i_mapped = r.alloc<unsigned char>(n_dfa_states);
+    unsigned char* o_mapped = r.alloc<unsigned char>(n_dfa_states);
+    StateIdx* i_touched = r.alloc<StateIdx>(n_dfa_states);
+    StateIdx* o_touched = r.alloc<StateIdx>(n_dfa_states);
+    for (int i=0; i<n_dfa_states; i++)
+      i_mapped[i] = o_mapped[i] = 0;
+    unsigned int n_i_mapped = 0;
+    unsigned int n_o_mapped = 0;
+
+    // Count and map reachable edges entering final states
+    unsigned long long int final_degree = 0;
+    for (ValSize j=0; j<layers[n-1].size; j++) {
+      Support& s = layers[n-1].support[j];
+      for (unsigned int d=0; d<static_cast<unsigned int>(s.n_edges); d++) {
+        const int os = static_cast<int>(s.edges[d].o_state);
+        if ((os >= dfa.final_fst()) && (os < dfa.final_lst())) {
+          final_degree++;
+          if (o_mapped[os] == 0) {
+            o_mapped[os] = 1;
+            o_map[os] = static_cast<StateIdx>(n_o_mapped);
+            o_touched[n_o_mapped++] = static_cast<StateIdx>(os);
           }
-        assert(n_edges <= dfa.max_degree());
-        // Found support for value
-        if (n_edges > 0) {
-          Support& s = layers[i].support[j];
-          s.val = static_cast<Val>(nx.val());
-          s.n_edges = n_edges;
-          s.edges = Heap::copy(home.alloc<Edge>(n_edges),edges,n_edges);
-          j++;
         }
       }
-      if ((layers[i].size = j) == 0)
-        return ES_FAILED;
     }
+    if (final_degree == 0)
+      return ES_FAILED;
 
-    // Mark final states as reachable
-    for (int s=dfa.final_fst(); s<dfa.final_lst(); s++)
-      if (o_state(n-1,static_cast<StateIdx>(s)).i_deg != 0)
-        o_state(n-1,static_cast<StateIdx>(s)).o_deg = 1;
+    // Initialize the map for the terminal layer
+    if (final_degree <= static_cast<unsigned long long int>
+        (Gecode::Support::IntTypeTraits<Degree>::max)) {
+      // Merge all terminal states
+      for (unsigned int i=0; i<n_o_mapped; i++)
+        o_map[o_touched[i]] = 0;
+      layers[n].n_states = 1;
+    } else {
+      // Keep terminal states separate
+      layers[n].n_states = static_cast<StateIdx>(n_o_mapped);
+    }
 
-    // Backward pass: prune all transitions that do not lead to final state
+    unsigned long long int total_states = layers[n].n_states;
+    unsigned long long int total_edges = 0;
+    unsigned int max_s = layers[n].n_states;
+
+    // Backward pass: prune and translate endpoints to layer-local indices
     for (int i=n; i--; ) {
-      ValSize k=0;
+      for (unsigned int j=0; j<n_i_mapped; j++)
+        i_mapped[i_touched[j]] = 0;
+      n_i_mapped = 0;
+      ValSize n_supports=0;
       for (ValSize j=0; j<layers[i].size; j++) {
         Support& s = layers[i].support[j];
-        for (Degree d=s.n_edges; d--; )
-          if (o_state(i,s.edges[d]).o_deg == 0) {
-            // Adapt states
-            i_dec(i,s.edges[d]); o_dec(i,s.edges[d]);
-            // Prune edge
-            s.edges[d] = s.edges[--s.n_edges];
+        unsigned int n_support_edges=0;
+        for (unsigned int d=0; d<static_cast<unsigned int>(s.n_edges); d++) {
+          Edge e = s.edges[d];
+          const int is = static_cast<int>(e.i_state);
+          const int os = static_cast<int>(e.o_state);
+          if (o_mapped[os] != 0) {
+            e.o_state = o_map[os];
+            if (i_mapped[is] == 0) {
+              i_mapped[is] = 1;
+              i_map[is] = static_cast<StateIdx>(n_i_mapped);
+              i_touched[n_i_mapped++] = static_cast<StateIdx>(is);
+            }
+            e.i_state = i_map[is];
+            s.edges[n_support_edges++] = e;
           }
-        // Value has support, copy the support information
-        if (s.n_edges > 0)
-          layers[i].support[k++]=s;
+        }
+        s.n_edges = static_cast<Degree>(n_support_edges);
+        if (n_support_edges > 0) {
+          layers[i].support[n_supports++] = s;
+          total_edges += n_support_edges;
+        }
       }
-      if ((layers[i].size = k) == 0)
+      if ((layers[i].size = n_supports) == 0)
         return ES_FAILED;
+      layers[i].n_states = static_cast<StateIdx>(n_i_mapped);
+      total_states += n_i_mapped;
+      max_s = std::max(max_s,n_i_mapped);
       LayerValues lv(layers[i]);
       GECODE_ME_CHECK(layers[i].x.narrow_v(home,lv,false));
       if (!layers[i].x.assigned())
         layers[i].x.subscribe(home, *new (home) Index(home,*this,c,i));
-    }
 
-    // Copy and compress states, setup other information
-    {
-      // State map for in-states
-      StateIdx* i_map = r.alloc<StateIdx>(max_states);
-      // State map for out-states
-      StateIdx* o_map = r.alloc<StateIdx>(max_states);
-      // Number of in-states
-      StateIdx i_n = 0;
-
-      // Initialize map for in-states (special for last layer)
-      // Degree for single final state
-      unsigned int d = 0;
-      for (StateIdx j=0; j<max_states; j++)
-        d += static_cast<unsigned int>(layers[n].states[j].i_deg);
-      // Check whether all final states can be joined to a single state
-      if (d >
-          static_cast<unsigned int>
-          (Gecode::Support::IntTypeTraits<Degree>::max)) {
-        // Initialize map for in-states
-        for (StateIdx j=max_states; j--; )
-          if ((layers[n].states[j].o_deg != 0) ||
-              (layers[n].states[j].i_deg != 0))
-            i_map[j]=i_n++;
-      } else {
-        i_n = 1;
-        for (StateIdx j=max_states; j--; ) {
-          layers[n].states[j].init();
-          i_map[j] = 0;
-        }
-        layers[n].states[0].i_deg = static_cast<Degree>(d);
-        layers[n].states[0].o_deg = 1;
-      }
-      layers[n].n_states = i_n;
-
-      // Total number of states
-      n_states = i_n;
-      // Total number of edges
-      n_edges = 0;
-      // New maximal number of states
-      StateIdx max_s = i_n;
+      std::swap(i_map,o_map);
+      std::swap(i_mapped,o_mapped);
+      std::swap(i_touched,o_touched);
+      std::swap(n_i_mapped,n_o_mapped);
+    }
 
-      for (int i=n; i--; ) {
-        // In-states become out-states
-        std::swap(o_map,i_map); i_n=0;
-        // Initialize map for in-states
-        for (StateIdx j=max_states; j--; )
-          if ((layers[i].states[j].o_deg != 0) ||
-              (layers[i].states[j].i_deg != 0))
-            i_map[j]=i_n++;
-        layers[i].n_states = i_n;
-        n_states += i_n;
-        max_s = std::max(max_s,i_n);
+    if ((total_states >
+         static_cast<unsigned long long int>
+         ((std::numeric_limits<unsigned int>::max)())) ||
+        (total_edges >
+         static_cast<unsigned long long int>
+         ((std::numeric_limits<unsigned int>::max)())))
+      throw OutOfLimits("Int::regular");
+    n_states = static_cast<unsigned int>(total_states);
+    n_edges = static_cast<unsigned int>(total_edges);
+    max_states = static_cast<StateIdx>(max_s);
+
+    // Allocate persistent states in terminal-first, descending-layer order
+    State* states = home.alloc<State>(n_states);
+    for (unsigned int i=0; i<n_states; i++)
+      states[i].init();
+    for (int i=n+1; i--; ) {
+      layers[i].states = states;
+      states += layers[i].n_states;
+    }
 
-        // Update states in edges
-        for (ValSize j=layers[i].size; j--; ) {
-          Support& ls = layers[i].support[j];
-          n_edges += ls.n_edges;
-          for (Degree deg=ls.n_edges; deg--; ) {
-            ls.edges[deg].i_state = i_map[ls.edges[deg].i_state];
-            ls.edges[deg].o_state = o_map[ls.edges[deg].o_state];
-          }
+    // Reconstruct state degrees from the surviving edges
+    for (int i=0; i<n; i++)
+      for (ValSize j=0; j<layers[i].size; j++) {
+        Support& s = layers[i].support[j];
+        for (Degree d=s.n_edges; d--; ) {
+          i_state(i,s.edges[d]).o_deg++;
+          o_state(i,s.edges[d]).i_deg++;
         }
       }
 
-      // Allocate and copy states
-      State* a_states = home.alloc<State>(n_states);
-      for (int i=n+1; i--; ) {
-        StateIdx k=0;
-        for (StateIdx j=max_states; j--; )
-          if ((layers[i].states[j].o_deg != 0) ||
-              (layers[i].states[j].i_deg != 0))
-            a_states[k++] = layers[i].states[j];
-        assert(k == layers[i].n_states);
-        layers[i].states = a_states;
-        a_states += layers[i].n_states;
-      }
-
-      // Update maximal number of states
-      max_states = max_s;
-    }
+    // Restore artificial boundary degrees
+    layers[0].states[0].i_deg = 1;
+    for (StateIdx i=0; i<layers[n].n_states; i++)
+      layers[n].states[i].o_deg = 1;
 
     // Schedule if subsumption is needed
     if (c.empty())
@@ -980,4 +1020,3 @@ namespace Gecode { namespace Int { namespace Extensional {
 }}}
 
 // STATISTICS: int-prop
-
diff --git a/test/int/extensional.cpp b/test/int/extensional.cpp
index e1d41d0603..97a2dd3881 100755
--- a/test/int/extensional.cpp
+++ b/test/int/extensional.cpp
@@ -392,6 +392,296 @@ namespace Test { namespace Int {
 
      };
 
+     /// %Test an acyclic DFA whose states can occur at different depths
+     class RegAcyclicReconvergence : public Test {
+     public:
+       /// Create and register test
+       RegAcyclicReconvergence(void)
+         : Test("Extensional::Reg::Sparse::AcyclicReconvergence",
+                4,0,3,false,Gecode::IPL_DOM) {}
+       /// %Test whether \a x is solution
+       virtual bool solution(const Assignment& x) const {
+         return
+           ((x[0] == 0) && (x[1] == 2) &&
+            (x[2] == 2) && (x[3] == 2)) ||
+           ((x[0] == 1) && (x[1] == 0) &&
+            (x[2] == 3) && (x[3] == 3));
+       }
+       /// Post constraint on \a x
+       virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
+         using namespace Gecode;
+         // State 1 is reached at depth one by 0 and at depth two by 1,0.
+         // Its two acyclic suffixes have the corresponding lengths.
+         DFA d(0,
+               {
+                 {0,0,1}, {0,1,2}, {2,0,1},
+                 {1,2,3}, {3,2,4}, {4,2,7},
+                 {1,3,5}, {5,3,7}
+               },
+               {7},false);
+         extensional(home,x,d);
+       }
+     };
+
+     /// %Test a cyclic DFA whose frontier states recur across many layers
+     class RegCyclicFrontier : public Test {
+     public:
+       /// Create and register test
+       RegCyclicFrontier(void)
+         : Test("Extensional::Reg::Sparse::CyclicFrontier",
+                7,0,1,false,Gecode::IPL_DOM) {}
+       /// %Test whether \a x is solution
+       virtual bool solution(const Assignment& x) const {
+         int parity = 0;
+         for (int i=0; i<x.size(); i++)
+           parity ^= x[i];
+         return parity == 0;
+       }
+       /// Post constraint on \a x
+       virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
+         using namespace Gecode;
+         DFA d(0,
+               {
+                 {0,0,0}, {0,1,1},
+                 {1,0,1}, {1,1,0}
+               },
+               {0},false);
+         extensional(home,x,d);
+       }
+     };
+
+     /// %Test the Boolean-view regular posting route
+     class RegBoolCyclicFrontier : public Test {
+     public:
+       /// Create and register test
+       RegBoolCyclicFrontier(void)
+         : Test("Extensional::Reg::Sparse::BoolCyclicFrontier",
+                7,0,1,false,Gecode::IPL_DOM) {}
+       /// %Test whether \a x is solution
+       virtual bool solution(const Assignment& x) const {
+         int parity = 0;
+         for (int i=0; i<x.size(); i++)
+           parity ^= x[i];
+         return parity == 0;
+       }
+       /// Post constraint on \a x
+       virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
+         using namespace Gecode;
+         BoolVarArgs b(x.size());
+         for (int i=0; i<x.size(); i++)
+           b[i] = channel(home,x[i]);
+         DFA d(0,
+               {
+                 {0,0,0}, {0,1,1},
+                 {1,0,1}, {1,1,0}
+               },
+               {0},false);
+         extensional(home,b,d);
+       }
+     };
+
+     /// %Test deterministic generated DFAs against a reference runner
+     class RegRandomDifferential : public Test {
+     protected:
+       /// Number of DFA states
+       static const int n_dfa_states = 4;
+       /// Number of symbols
+       static const int n_symbols = 3;
+       /// Transition table, with -1 denoting no transition
+       int next[n_dfa_states][n_symbols];
+       /// Allowed-symbol bit masks for each position
+       unsigned int allowed[5];
+       /// Final-state bit mask
+       unsigned int finals;
+     public:
+       /// Create and register test
+       RegRandomDifferential(unsigned int seed)
+         : Test("Extensional::Reg::Sparse::RandomDifferential::" +
+                Test::str(static_cast<int>(seed)),
+                5,0,n_symbols-1,false,Gecode::IPL_DOM),
+           finals(0) {
+         unsigned int random = seed;
+         for (int state=0; state<n_dfa_states; state++)
+           for (int symbol=0; symbol<n_symbols; symbol++) {
+             random = 1664525U * random + 1013904223U;
+             next[state][symbol] =
+               ((random & 7U) == 0U) ? -1 :
+               static_cast<int>((random >> 8) % n_dfa_states);
+           }
+         for (int i=0; i<5; i++) {
+           random = 1664525U * random + 1013904223U;
+           allowed[i] = 1U + ((random >> 12) % 7U);
+         }
+         random = 1664525U * random + 1013904223U;
+         finals = 1U + ((random >> 16) % 15U);
+       }
+       /// %Test whether \a x is solution
+       virtual bool solution(const Assignment& x) const {
+         int state = 0;
+         for (int i=0; i<x.size(); i++) {
+           const int symbol = x[i];
+           if (((allowed[i] & (1U << symbol)) == 0U) ||
+               (next[state][symbol] < 0))
+             return false;
+           state = next[state][symbol];
+         }
+         return (finals & (1U << state)) != 0U;
+       }
+       /// Post constraint on \a x
+       virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
+         using namespace Gecode;
+         DFA::Transition transitions[n_dfa_states*n_symbols+1];
+         int n_transitions = 0;
+         for (int state=0; state<n_dfa_states; state++)
+           for (int symbol=0; symbol<n_symbols; symbol++)
+             if (next[state][symbol] >= 0)
+               transitions[n_transitions++] =
+                 DFA::Transition(state,symbol,next[state][symbol]);
+         transitions[n_transitions].i_state = -1;
+         int final_states[n_dfa_states+1];
+         int n_final_states = 0;
+         for (int state=0; state<n_dfa_states; state++)
+           if ((finals & (1U << state)) != 0U)
+             final_states[n_final_states++] = state;
+         final_states[n_final_states] = -1;
+         DFA d(0,transitions,final_states,false);
+         for (int i=0; i<x.size(); i++)
+           for (int symbol=0; symbol<n_symbols; symbol++)
+             if ((allowed[i] & (1U << symbol)) == 0U)
+               rel(home,x[i],IRT_NQ,symbol);
+         extensional(home,x,d);
+       }
+     };
+
+     /// %Test backward pruning caused by a position-specific domain
+     class RegPositionDomainPruning : public Test {
+     public:
+       /// Create and register test
+       RegPositionDomainPruning(void)
+         : Test("Extensional::Reg::Sparse::PositionDomainPruning",
+                3,0,1,false,Gecode::IPL_DOM) {}
+       /// %Test whether \a x is solution
+       virtual bool solution(const Assignment& x) const {
+         return (x[0] == 0) && (x[1] == 0) && (x[2] == 0);
+       }
+       /// Post constraint on \a x
+       virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
+         using namespace Gecode;
+         DFA d(0,
+               {
+                 {0,0,1}, {0,1,2},
+                 {1,0,3}, {2,1,4},
+                 {3,0,5}, {4,1,6}
+               },
+               {5,6},false);
+         rel(home,x[2],IRT_EQ,0);
+         extensional(home,x,d);
+       }
+     };
+
+     /// %Test failure when the forward frontier misses the terminal boundary
+     class RegNoAcceptingPath : public Test {
+     public:
+       /// Create and register test
+       RegNoAcceptingPath(void)
+         : Test("Extensional::Reg::Sparse::NoAcceptingPath",
+                3,0,0,false,Gecode::IPL_DOM) {
+         testsearch = false;
+       }
+       /// %Test whether \a x is solution
+       virtual bool solution(const Assignment& x) const {
+         (void)x;
+         return false;
+       }
+       /// Post constraint on \a x
+       virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
+         using namespace Gecode;
+         // Every position has a forward transition, but the sole final state
+         // is only reached after four symbols.
+         DFA d(0,
+               {
+                 {0,0,1}, {1,0,2}, {2,0,3}, {3,0,4}
+               },
+               {4},false);
+         extensional(home,x,d);
+       }
+     };
+
+     /// %Test merging several reached DFA final states
+     class RegTerminalMerged : public Test {
+     public:
+       /// Create and register test
+       RegTerminalMerged(void)
+         : Test("Extensional::Reg::Sparse::TerminalMerged",
+                1,0,2,false,Gecode::IPL_DOM) {}
+       /// %Test whether \a x is solution
+       virtual bool solution(const Assignment& x) const {
+         (void)x;
+         return true;
+       }
+       /// Post constraint on \a x
+       virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
+         using namespace Gecode;
+         DFA d(0,
+               {
+                 {0,0,1}, {0,1,2}, {0,2,3}
+               },
+               {1,2,3},false);
+         extensional(home,x,d);
+       }
+     };
+
+     /// %Test retaining separate terminal states when merging would overflow
+     class RegTerminalUnmerged : public Test {
+     public:
+       /// Create and register test
+       RegTerminalUnmerged(void)
+         : Test("Extensional::Reg::Sparse::TerminalUnmerged",
+                8,0,15,false,Gecode::IPL_DOM) {
+         testsearch = false;
+       }
+       /// Create a bounded random selection from the large uniform test domain
+       virtual Assignment* assignment(void) const {
+         return new RandomAssignment(arity,dom,1000,_rand);
+       }
+       /// %Test whether \a x is solution
+       virtual bool solution(const Assignment& x) const {
+         for (int i=0; i<x.size(); i++)
+           if ((x[i] != 2*i) && (x[i] != 2*i+1))
+             return false;
+         return true;
+       }
+       /// Post constraint on \a x
+       virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
+         using namespace Gecode;
+         // Symbols are unique per level. No symbol labels more than 128
+         // transitions, selecting the smallest Degree type, but 256 edges
+         // enter final states.
+         const int n_states = 511;
+         const int n_transitions = n_states - 1;
+         DFA::Transition* t = new DFA::Transition[n_transitions+1];
+         int ti = 0;
+         for (int depth=0; depth<8; depth++) {
+           const int first = (1 << depth) - 1;
+           const int width = 1 << depth;
+           for (int j=0; j<width; j++) {
+             const int i = first+j;
+             t[ti++] = DFA::Transition(i,2*depth,2*i+1);
+             t[ti++] = DFA::Transition(i,2*depth+1,2*i+2);
+           }
+         }
+         t[ti].i_state = -1;
+         int* f = new int[257];
+         for (int i=0; i<256; i++)
+           f[i] = 255+i;
+         f[256] = -1;
+         DFA d(0,t,f,false);
+         delete [] t;
+         delete [] f;
+         extensional(home,x,d);
+       }
+     };
+
      ///% Transform a TupleSet into a DFA
      Gecode::DFA tupleset2dfa(Gecode::TupleSet ts) {
        using namespace Gecode;
@@ -2155,6 +2445,18 @@ namespace Test { namespace Int {
      RegOpt ro6(static_cast<int>(USHRT_MAX-1));
      RegOpt ro7(static_cast<int>(USHRT_MAX));
 
+     RegAcyclicReconvergence reg_sparse_acyclic_reconvergence;
+     RegCyclicFrontier reg_sparse_cyclic_frontier;
+     RegBoolCyclicFrontier reg_sparse_bool_cyclic_frontier;
+     RegRandomDifferential reg_sparse_random_differential_1(1);
+     RegRandomDifferential reg_sparse_random_differential_2(2);
+     RegRandomDifferential reg_sparse_random_differential_3(3);
+     RegRandomDifferential reg_sparse_random_differential_4(4);
+     RegPositionDomainPruning reg_sparse_position_domain_pruning;
+     RegNoAcceptingPath reg_sparse_no_accepting_path;
+     RegTerminalMerged reg_sparse_terminal_merged;
+     RegTerminalUnmerged reg_sparse_terminal_unmerged;
+
      SparseTupleSetUnary sparse_tuple_set_unary;
      SparseTupleSetTernary sparse_tuple_set_ternary;
      SparseTupleSetHighArity sparse_tuple_set_high_arity;

From 44bddbebe10f182e8f2ce6d7e52e100dc125a05e Mon Sep 17 00:00:00 2001
From: Mikael Zayenz Lagerkvist <research@zayenz.se>
Date: Tue, 28 Jul 2026 11:01:39 +0200
Subject: [PATCH 2/3] Test regular propagation with NFAs

---
 test/int/extensional.cpp | 83 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 83 insertions(+)

diff --git a/test/int/extensional.cpp b/test/int/extensional.cpp
index 97a2dd3881..0e6a024a7a 100755
--- a/test/int/extensional.cpp
+++ b/test/int/extensional.cpp
@@ -553,6 +553,85 @@ namespace Test { namespace Int {
        }
      };
 
+     /// %Test nondeterministic generated automata against a reference runner
+     class RegRandomNFADifferential : public Test {
+     protected:
+       /// Number of automaton states
+       static const int n_fa_states = 4;
+       /// Number of symbols
+       static const int n_symbols = 3;
+       /// Transition relation
+       bool next[n_fa_states][n_symbols][n_fa_states];
+       /// Allowed-symbol bit masks for each position
+       unsigned int allowed[5];
+     public:
+       /// Create and register test
+       RegRandomNFADifferential(unsigned int seed)
+         : Test("Extensional::Reg::Sparse::RandomNFADifferential::" +
+                Test::str(static_cast<int>(seed)),
+                5,0,n_symbols-1,false,Gecode::IPL_DOM) {
+         unsigned int random = seed;
+         for (int state=0; state<n_fa_states; state++)
+           for (int symbol=0; symbol<n_symbols; symbol++)
+             for (int output=0; output<n_fa_states; output++) {
+               random = 1664525U * random + 1013904223U;
+               next[state][symbol][output] = ((random >> 29) == 0U);
+             }
+         // Keep a nondeterministic fork and both of its branches relevant.
+         next[0][0][1] = true;
+         next[0][0][2] = true;
+         next[1][1][3] = true;
+         next[2][2][3] = true;
+         for (int symbol=0; symbol<n_symbols; symbol++)
+           next[3][symbol][3] = true;
+         for (int i=0; i<5; i++) {
+           random = 1664525U * random + 1013904223U;
+           allowed[i] = 1U + ((random >> 12) % 7U);
+         }
+         // Ensure both branches of the fixed fork can occur.
+         allowed[0] |= 1U;
+         allowed[1] |= 6U;
+       }
+       /// %Test whether \a x is solution
+       virtual bool solution(const Assignment& x) const {
+         unsigned int states = 1U;
+         for (int i=0; i<x.size(); i++) {
+           const int symbol = x[i];
+           if ((allowed[i] & (1U << symbol)) == 0U)
+             return false;
+           unsigned int outputs = 0U;
+           for (int state=0; state<n_fa_states; state++)
+             if ((states & (1U << state)) != 0U)
+               for (int output=0; output<n_fa_states; output++)
+                 if (next[state][symbol][output])
+                   outputs |= 1U << output;
+           states = outputs;
+         }
+         return (states & (1U << 3)) != 0U;
+       }
+       /// Post constraint on \a x
+       virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) {
+         using namespace Gecode;
+         DFA::Transition
+           transitions[n_fa_states*n_symbols*n_fa_states+1];
+         int n_transitions = 0;
+         for (int state=0; state<n_fa_states; state++)
+           for (int symbol=0; symbol<n_symbols; symbol++)
+             for (int output=0; output<n_fa_states; output++)
+               if (next[state][symbol][output])
+                 transitions[n_transitions++] =
+                   DFA::Transition(state,symbol,output);
+         transitions[n_transitions].i_state = -1;
+         int final_states[] = {3,-1};
+         DFA d(0,transitions,final_states,false);
+         for (int i=0; i<x.size(); i++)
+           for (int symbol=0; symbol<n_symbols; symbol++)
+             if ((allowed[i] & (1U << symbol)) == 0U)
+               rel(home,x[i],IRT_NQ,symbol);
+         extensional(home,x,d);
+       }
+     };
+
      /// %Test backward pruning caused by a position-specific domain
      class RegPositionDomainPruning : public Test {
      public:
@@ -2452,6 +2531,10 @@ namespace Test { namespace Int {
      RegRandomDifferential reg_sparse_random_differential_2(2);
      RegRandomDifferential reg_sparse_random_differential_3(3);
      RegRandomDifferential reg_sparse_random_differential_4(4);
+     RegRandomNFADifferential reg_sparse_random_nfa_differential_1(1);
+     RegRandomNFADifferential reg_sparse_random_nfa_differential_2(2);
+     RegRandomNFADifferential reg_sparse_random_nfa_differential_3(3);
+     RegRandomNFADifferential reg_sparse_random_nfa_differential_4(4);
      RegPositionDomainPruning reg_sparse_position_domain_pruning;
      RegNoAcceptingPath reg_sparse_no_accepting_path;
      RegTerminalMerged reg_sparse_terminal_merged;

From 53903bfb9edb5b69dfbf88d85f89131501bb7cb7 Mon Sep 17 00:00:00 2001
From: Mikael Zayenz Lagerkvist <research@zayenz.se>
Date: Tue, 28 Jul 2026 16:00:30 +0200
Subject: [PATCH 3/3] Add regular construction changelog entry

---
 changelog.in | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/changelog.in b/changelog.in
index 4f8129b317..5b3d2b277f 100755
--- a/changelog.in
+++ b/changelog.in
@@ -67,6 +67,22 @@
 #    optional section in the html page.
 #
 
+[RELEASE]
+Version: 6.5.0
+Date: unreleased
+[DESCRIPTION]
+This is the development changelog for the next Gecode release.
+
+[ENTRY]
+Module: int
+What:   performance
+Rank:   major
+[DESCRIPTION]
+Reduce construction memory for regular constraints by building the layered
+graph from sparse forward frontiers and retaining only backward co-reachable
+states. This avoids allocating one temporary state for every automaton state
+at every sequence position while preserving the persistent graph.
+
 [RELEASE]
 Version: 6.4.0
 Date: 2026-07-15