[−][src]Module varisat_internal_proof::vli_enc
Variable length integer encoding.
This uses a different encoding from the leb128 encoding used for binary DRAT and CLRAT. It uses the same amount of bytes for each input, but is faster to encode and decode.
Numbers are encoded like this:
1xxxxxxx for up to 7 bits
01xxxxxx xxxxxxxx for up to 14 bits
001xxxxx xxxxxxxx xxxxxxxx for up to 21 bits
...
The x-bits store the number from LSB to MSB. This scheme allows faster encoding and decoding, as the bits are kept consecutive and the length can be determined from the first or first two bytes.
The current implementations are not optimal but fast enough to not be the bottleneck when checking proofs.
Functions
read_u64_fast | Read an encoded 64 bit number, if at least 16 bytes lookahead are available. |
read_u64 | Read an encoded 64 bit number from a buffered reader. |
write_u64 | Write an encoded 64 bit number. |