From c7556364b710107618f845278f6444acd4847b97 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 9 Jul 2020 07:43:09 -0700 Subject: [PATCH] [sledge] Change: Strengthen Term invariant that exponents are integers Summary: Exponents in polynomials are represented by rationals for code reuse purposes, but only integral exponents are supported. Strengthen the invariant check to clarify this. Reviewed By: ngorogiannis Differential Revision: D22170517 fbshipit-source-id: 81ae38f4e --- sledge/src/term.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sledge/src/term.ml b/sledge/src/term.ml index 87beec20f..66ad524a8 100644 --- a/sledge/src/term.ml +++ b/sledge/src/term.ml @@ -253,7 +253,7 @@ let assert_monomial mono = match mono with | Mul args -> Qset.iter args ~f:(fun factor exponent -> - assert (Q.is_real exponent) ; + assert (Z.equal (Q.den exponent) Z.one) ; assert (Q.sign exponent > 0) ; assert_indeterminate factor |> Fn.id ) | _ -> assert_indeterminate mono |> Fn.id