Module monotonic_product 

Functions

collect_order_facts 🔒

Collects simple unsigned ordering facts from normalized constraints.

mul_operands 🔒

Returns the operands for an unsigned multiplication expression.

product_less_than_known 🔒

Returns whether known facts imply left_a * left_b < right_a * right_b.

product_less_than_known_ordered 🔒

Checks the ordered monotonicity case 0 < a < c && 0 < b < d.

product_less_than_negation 🔒

Extracts !(a * b < c * d) as product operands.

product_monotonic_unsat_normalized 🔒

Returns whether normalized monotonic product facts make constraints unsatisfiable.