This PR adds support for #packing annotations, including support for concatenation and packing applications, but no support for #solve annotations.
The idea is that packing expressions are flattened into a FlattenedExpr form, containing a bit pattern and assignments. These FlattenedExpr's can be concatenated or applied to obtain scalar assignments, interval assignments and bit patterns for each variant. These pre-existing constraints are fed into the original solver.
Issues:
[ ] No way of reporting errors at this stage of compilation (the verifier can't catch everything, some things should fail)
This PR adds support for
#packing
annotations, including support for concatenation and packing applications, but no support for#solve
annotations.The idea is that packing expressions are flattened into a
FlattenedExpr
form, containing a bit pattern and assignments. TheseFlattenedExpr
's can be concatenated or applied to obtain scalar assignments, interval assignments and bit patterns for each variant. These pre-existing constraints are fed into the original solver.Issues: