issues
search
GaloisInc
/
daedalus
The Daedalus data description language
BSD 3-Clause "New" or "Revised" License
63
stars
11
forks
source link
Enhancements related to loops
#321
Open
simonjwinwood
opened
1 year ago
simonjwinwood
commented
1 year ago
[ ] See #317
[ ] Static analysis to give loop bounds would let us figure out reasonable unfolding counts.
[ ] Handle concat in MuxValue.hs (or remove Concat from DDL/replace by a prelude fun)
[ ] Investigate uses of explodeSequence in MuxValue.hs for perf. improvements
[ ] Investigate fan-out for loops (i.e., { xs = Many P; map (x in xs) ... } the map relies only on the value, we could get multiple bodies)
[ ] Create a SMT function for loop bodies which are unfolded.
[ ] Search for satisfying lengths for unrolled loops (requires linking unrolled loops and their use to extend list)
[ ] Split out nested loops where the inner loop body doesn't effect the outer loop body
[ ] Only get the minimum solver model needed when pooling loops (annotate pathbuilder loop nodes with the symbolicmodel)