Bit manipulation constraints are a class of constraints over fixed-size variables that operate directly on their bit-level structure rather than only on numeric ranges. In the cited work, the examples given are bit extraction and bit concatenation: X = Y[5:3] denotes that X is the slice made of bits 3 to 5 of Y, and X = (Y:Z) denotes that X is the concatenation of Y and Z. These constraints arise from hardware-description-style operations and therefore require dedicated support in the solver.^[1]

The source explains that handling such constraints as separate independent constraints on individual bits is not sufficient when the same variables also participate in arithmetic constraints. A purely bit-vector decomposition, as described in prior work cited by the source, "cannot be combined with arithmetic constraints on the same variable" and therefore prevents some possible domain reductions.^[2]

The same discussion places bit manipulation constraints alongside other fixed-width typing issues, including casts between variables of different bit sizes. Because casting can lose information—for example by truncating a higher-order bit—domain reasoning must account for both arithmetic intervals and bit-level structure.^[3]

In response to these issues, the STCS solver introduces dedicated support for several bit-oriented constraints, including logical AND, logical shift, bit concatenation, and bit extraction. To support both arithmetic and bit-based reasoning, STCS maintains two internal representations for each variable domain: an interval representation for arithmetic constraints and a bit representation that records known bits in the bit-vector. Propagation is split into interval propagation and bit propagation, with consistency maintained between the two representations.^[4]

^[1]: Citation 1 ^[2]: Citation 2 ^[3]: Citation 3 ^[4]: Citation 4