Implement faster parsing.

[adwait]

Parsing is super-linear (likely quadratic). Results from an application:

Parse Time (s)	Program length
1	5465
4	9029
14	16142
52	30376
190	58915
742	116186

Likely due to p argument in parse_inst:

btor2-opt/src/btoropt/parser.py

Line 145 in 3485976

def parse_inst(line: str, p: list[Instruction]) -> Instruction:

How can we improve this?

[dobios]

I didn't originally make this to be high-performance tbh, it was just a hacky research compiler to try out some new btor2 instructions and automate some post-processing tasks.

If you want to use this is production, it should probably be optimized.

Here are a few ideas of how this could be optimized:

• One idea would be to use the multiprocessing.Pool.map to process the list in parallel, however this would require exploring the text in a DFS manner and not linearly which is a bit trickier to do.

• Another idea would be to parse in two stages:
  .. group all dependent instructions together by naively looking at usage
  .. process each batch in parallel
  Not sure if this will be faster, but it's easier to implement than an actual DFS-order parsing (which is what we do in CIRCT but that's a bit easier to do on an AST than on raw text).

• Create a Parser object that maintains the program as a field rather than passing it around as an argument. Additionally, we should split up the program into smaller logical groupings, e.g. a list of sorts, one of constants, one of states ... Then growing then won't be as slow in massive files but emitting it at the end might be a bit more tricky ( you could probably decide IDs at emission time and then just use some logical ordering of the various groupings but that won't preserve the original program order just a loose dataflow ordering).

I can give it a shot if I find the time, but it probably won't be for another couple of weeks so if you need this to be fast, I would recommend not waiting on me ^^"

[adwait]

Thanks, good points; I was thinking of 3 as well, unclear whether overheads in 1,2 will pay off.

Created an issue to just keep in my cache :D - I'll take a shot at this sometime soonish.

[dobios]

Also awesome that you're benchmarking this !! Let me know when you need a new packaged release for the stuff you've made PRs for.

[dobios]

Made this a good bit faster with the most recent release. I've only benchmarked it on small designs though. If you end up rerunning your benchmarks on this @adwait let me know what you get! I'd be curious to see if deferred parsing scales better than the slightly better implementation of the sequential parsing.