Module gf::smt::simplifier

⚪ Expression simplification.

The simplify function performs the known transformations in a loop until no further simplification is possible. The remaining functions are the actual transformations performed.

Functions

absorb_concat	⚪ Transform two nested concatenations with constant consecutive parts into one.
absorb_ext	⚪ Transform two nested signed or unsigned extensions into one.
absorb_slice	⚪ Transform two nested slices into one.
concat_of_slices	⚪ Transform concatenation of two adjacent slices into one slice.
concat_to_extu	⚪ Transform concatenation of an all-zero bit vectors with a value into unsigned extension of the value.
equivalences	⚪ Reduce arithmetic and bitwise expressions to simpler equivalent ones.
fold_constants	⚪ Perform shallow constant folding.
normalize_commutative	⚪ Normalize commutative operators so that if there is a constant operand, it is the second one.
remove_trivial_slice	⚪ Remove a slice that encompasses the entire operand.
simplify	⚪ Simplify an expression.
slice_of_concat	⚪ Transform slice of concatenation that references just one part into slice of the part.