Bit-lists provide a domain on bit-vectors that represent the known bits sets to 1 and 0, respectively.
This module provides an implementation of bitlists and related operators. The bitlists provided by this module do not have a fixed width, and can represent arbitrary-precision integers.
The type of bitlists.
Bitlists are indexed from the right: the least-significant bit has index 0.
Bitlists include an explanation (that can be recovered through the explanation function). The explanation indicates why the bitlist applies to a value, which must be maintained separately.
The explanation associated with the result of any bitlist operation is the union of the explanations associated with its arguments.
exception Inconsistent of Explanation.tException raised when an inconsistency is detected.
val unknown : tunknown is a bitlist that repersents all integers.
val explanation : t -> Explanation.tReturns the explanation associated with the bitlist. See the type-level documentation for details.
val exact : Z.t -> Explanation.t -> texact v ex returns a bitlist that represents the constant v.
equal b1 b2 returns true if the bitlists b1 and b2 are equal, albeit with possibly different explanations.
zeroes b returns a bitlist where the one bits in b are replaced with unknown bits.
val add_explanation : ex:Explanation.t -> t -> tadd_explanation ~ex b adds the explanation ex to the bitlist b. The returned bitlist has both the explanation of b and ex as explanation.
val unknown_bits : t -> Z.tunknown_bits b returns the set of unknown (or undetermined) bits in b.
The value of Z.logand (Z.lognot (unknown_bits b)) n is the same for any n in the set represented by the bitlist b.
val is_fully_known : t -> boolis_fully_known b determines if there are unknown bits in b or not. is_fully_known b is true iff unknown_bits b is Z.zero.
val value : t -> Z.tvalue b returns the value associated with the bitlist b. If the bitlist b is not fully known, then only the known bits (those that are set in bits_known b) are meaningful; unknown bits are set to 0.
intersect b1 b2 returns a new bitlist b that subsumes both b1 and b2. Any explanation justifying that b1 and b2 apply to the same value must have been added to b1 and b2.
Raises Inconsistent if b1 and b2 are not compatible (i.e. there are bits set in one bitlist and cleared in the other).
Logical left shift, truncated to the size least significant bits.
Logical right shift, truncated to the size least significant bits.
Shifts to the left. Equivalent to a multiplication by a power of 2. The second argument must be nonnegative.
Shifts to the right. This is an arithmetic shift, equivalent to a division by a power of 2 with rounding towards -oo. The second argument must be nonnegative.
extract b off len returns a nonnegative bitlist corresponding to bits off to off + len - 1 of b.
Note: This uses the same arguments as Z.extract, not the arguments from the SMT-LIB's extract primitive.
val increase_lower_bound : t -> Z.t -> Z.tincrease_lower_bound b lb returns the smallest integer lb' >= lb that matches the bit-pattern in b.
val decrease_upper_bound : t -> Z.t -> Z.tdecrease_upper_bound b ub returns the largest integer ub' >= ub that matches the bit-pattern in b.