[][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.