From 0d70f57c6ff13b0885dcb6a34d983ce63788cd6a Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 26 Apr 2019 12:03:06 -0700 Subject: [PATCH] [sledge] Relax overly strong polynomial invariants Reviewed By: mbouaziz Differential Revision: D15098814 fbshipit-source-id: 4e4dac320 --- sledge/src/llair/exp.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index cae4c05e9..303ab665d 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -387,7 +387,7 @@ let assert_monomial add_typ mono = match mono with | Mul {typ; args} -> assert (Typ.castable add_typ typ) ; - assert (Option.exists ~f:(fun n -> 1 < n) (Typ.prim_bit_size_of typ)) ; + assert (Option.is_some (Typ.prim_bit_size_of typ)) ; Qset.iter args ~f:(fun factor exponent -> assert (Q.sign exponent > 0) ; assert_indeterminate factor |> Fn.id ) @@ -401,8 +401,10 @@ let assert_poly_term add_typ mono coeff = match mono with | Integer {data} -> assert (Z.equal Z.one data) | Mul {args} -> - if Q.equal Q.one coeff then assert (Qset.length args > 1) - else assert (Qset.length args > 0) ; + ( match Qset.min_elt args with + | None | Some (Integer _, _) -> assert false + | Some (_, n) -> assert (Qset.length args > 1 || not (Q.equal Q.one n)) + ) ; assert_monomial add_typ mono |> Fn.id | _ -> assert_monomial add_typ mono |> Fn.id