Module monotonic_product

Structs§

collect_order_facts 🔒
expr_less_or_equal 🔒: Returns whether the known unsigned order and no-overflow bounds imply left <= right.
less_or_equal_comparison 🔒: Returns the unsigned weak ordering asserted by this constraint.
mul_operands 🔒
nonzero_expr 🔒
order_facts 🔒
product_less_or_equal_known 🔒
product_less_or_equal_known_ordered 🔒
product_less_than_known 🔒
product_less_than_known_ordered 🔒
product_less_than_negation 🔒
product_monotonic_unsat_normalized 🔒: Returns whether normalized monotonic product facts make constraints unsatisfiable.
remove_implied_monotonic_constraints 🔒: Removes hard-arithmetic comparisons implied by the remaining path constraints.
reversed_strict_comparison 🔒: Returns a strict comparison that contradicts right <= left.