The new core sum() builtin works in the explicit-state (BFS) backend. The symbolic (Z3) encoder returns a clear error and auto-routing falls back to BFS. Implement symbolic encoding by unrolling sum over a known-finite element domain into a chained Add (the frontend DSL already does this for its own sum); relates to the indexed-map sum encoding in #67.
The new core
sum()builtin works in the explicit-state (BFS) backend. The symbolic (Z3) encoder returns a clear error and auto-routing falls back to BFS. Implement symbolic encoding by unrolling sum over a known-finite element domain into a chained Add (the frontend DSL already does this for its own sum); relates to the indexed-map sum encoding in #67.