Efficient ASCII parsing#4
Merged
Merged
Conversation
Just an additional CLI flag for running the parser only, which I'll use to benchmark stuff while I'm focusing on that piece. I also slightly refactored the usage string. I'm considering all this somewhat temporary; eventually, this `main` will move to a more proper CLI parsing situation.
Because we know how many latches and outputs we will need, using `Vec::with_capacity` instead of `Vec::new` avoids reallocations when we eventually `push` that many elements into the vector.
This is a standalone utility (not yet integrated into the parsers) for handling text-file lines consisting of lists of integers. It has two main advantages over what the ASCII AIGER parser currently does: * It parses each line in a single pass, from left to right, without allocating anything. So we save the time creating and destroying the `Vec`s required for `String::split_whitespace`. * It operates on bytes instead of Rust's UTF-8-encoded `String`s. Because we're only looking for ASCII numerals and whitespace, the full generality of Unicode string handling isn't helping us much.
We replace `read_one_number_line`, `read_latch_line`, and `read_and_line` with calls to our new `LineParser`. To make this convenient, I added a wrapper that also takes care of advancing through the text-file lines emitted from a `BufRead`.
Oddly enough, the binary AIGER format still has some text lines in it! So we reuse our new efficient parser for ASCII-encoded integers in text files for that part of the binary parser too.
The AIGER header (used for both binary and text formats) is *also* a whitespace-separated list, consisting mostly of ASCII integers, so let's use our new one-pass processing approach for that as well.
`Literals` maps AIGER literals integers to our internal node IDs. We expect the space of AIGER literals to be dense: i.e., there are not many gaps in the "number line" of these integers. For dense data like that, a hash table doesn't buy us much space, and it costs time. So we can instead try a dense mapping based on a `Vec`. This doesn't yet try to guess the right maximum literal, so we just resize on demand.
Because our table only stores (and looks up) the "positive" literals, we were actually only using half the allotted space: every other "slot" in our array was unused. Now, we more carefully allocate one slot per *variable*, rather than one slot per literal. This also calculates the amount of space we need up front. The header tells us the maximum number of variables, so we need a vector contains that many slots. This way, we never need to resize.
We already have a way to signal "not a valid node," so maybe we can use that in our literals table. This means that our literals table is half as big, because each entry is 32 bits instead of 64 bits (the 1-bit discriminator + 32-bit value = 64 bits, unfortunately). This is my most dubious suggestion of this optimization effort! It required me making the reserved node ID value public where it was previously an internal implementation detail. We should consider whether this is a bad idea!
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is TRULY not the most important thing to be doing right now, but I have a kind of special interest in writing efficient parsers for super-duper simple text formats in the vein of ASCII AIGER. So I couldn't resist trying out a few standard tricks. I again don't think our ASCII parsing speed is all that important for this project, but perhaps some of these approaches will be interesting/educational for @Modertool999 nonetheless.
This PR is best reviewed commit by commit; I tried to make each change standalone and digestible. Please see the commit messages associated with each one for more detail, but the main techniques here are:
HashMapin the relevant data structure with a dense array.The final commit (e329fb8) contains one possibly questionable change. Please let me know if you think this is an acceptable detail to expose!
Here are some benchmarking results, all from gorgonzola. I used this Hyperfine command to run on a 1.2 MB ASCII AIGER file, converted from a binary file that @ekiwi shared:
Here are the results for various checkpoints:
(Let's call that no significant change from the previous point. But it was fun anyway?)