From ebe31e61533dfbcca4d6832dc98b885c24079c4b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Thu, 12 Oct 2023 18:41:44 +0200 Subject: [PATCH 1/2] Do not use existential variables for integer division This patch implements integer remainder in terms of integer division rather than the opposite. This avoids the introduction of fresh existential variables. Fixes #875 --- src/lib/reasoners/arith.ml | 94 ++++++++++++++++++++------------------ 1 file changed, 49 insertions(+), 45 deletions(-) diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index 87ec2bbf5..26d4d2aad 100644 --- a/src/lib/reasoners/arith.ml +++ b/src/lib/reasoners/arith.ml @@ -134,39 +134,47 @@ module Shostak | Some p -> p | _ -> P.create [Q.one, r] Q.zero (X.type_info r) - (* t1 % t2 = md <-> - c1. 0 <= md ; - c2. md < t2 ; - c3. exists k. t1 = t2 * k + t ; - c4. t2 <> 0 (already checked) *) - let mk_modulo md t1 t2 p2 ctx = - let zero = E.int "0" in - let c1 = E.mk_builtin ~is_pos:true Symbols.LE [zero; md] in - let c2 = - match P.is_const p2 with - | Some n2 -> - let an2 = Q.abs n2 in - assert (Q.is_int an2); - let t2 = E.int (Q.to_string an2) in - E.mk_builtin ~is_pos:true Symbols.LT [md; t2] - | None -> - E.mk_builtin ~is_pos:true Symbols.LT [md; t2] - in - let k = E.fresh_name Ty.Tint in - let t3 = E.mk_term (Sy.Op Sy.Mult) [t2;k] Ty.Tint in - let t3 = E.mk_term (Sy.Op Sy.Plus) [t3;md] Ty.Tint in - let c3 = E.mk_eq ~iff:false t1 t3 in - c3 :: c2 :: c1 :: ctx - - let mk_euc_division p p2 t1 t2 ctx = - match P.to_list p2 with - | [], coef_p2 -> - let md = E.mk_term (Sy.Op Sy.Modulo) [t1;t2] Ty.Tint in - let r, ctx' = X.make md in - let rp = - P.mult_const (Q.div Q.one coef_p2) (embed r) in - P.sub p rp, ctx' @ ctx - | _ -> assert false + (* Compute [t1 % t2] as [t1 - |t2| * (t1 / |t2|)]. + + Requires: [t1], [t2] have type [Tint] + Requires: [p1] is the representative for [t1] + Requires: [p2] is the representative for [t2] + Requires: [p2] is a non-zero constant *) + let mk_modulo t1 p1 p2 ctx = + match P.is_const p2 with + | Some n2 -> + let a2 = Q.to_z n2 |> Z.abs in + assert (Z.sign a2 > 0); + + (* NB: [t1 % t2] = [t1 % |t2|] *) + let div, ctx' = X.make (E.Ints.(t1 / ~$$a2)) in + P.sub p1 (P.mult_const (Q.from_z a2) (embed div)), ctx' @ ctx + | None -> assert false + + (* Add range information for [t = t1 / t2]. + + Requires: [t], [t1], [t2] have type [Tint] + Requires: [p2] is the term representative for [t2] + Requires: [p2] is a non-zero constant *) + let mk_euc_division t t1 p2 ctx = + assert (E.type_info t == Tint); + + match P.is_const p2 with + | Some n2 -> + let a2 = Q.to_z n2 |> Z.abs in + assert (Z.sign a2 > 0); + + if Q.sign n2 < 0 then + (* t1 / (-|t2|) = -(t1 / |t2|)*) + let r, ctx' = X.make E.Ints.(t1 / ~$$a2) in + P.mult_const Q.m_one (embed r), ctx' @ ctx + else + (* 0 <= t1 % t2 = t1 - t2 * (t1 / t2) < |t2| *) + let t1_mod_t2 = E.Ints.(t1 - ~$$a2 * t) in + let c1 = E.Ints.(~$0 <= t1_mod_t2) in + let c2 = E.Ints.(t1_mod_t2 < ~$$a2) in + P.create [Q.one, X.term_embed t] Q.zero Tint, c2 :: c1 :: ctx + | None -> assert false let exact_sqrt_or_Exit q = @@ -258,11 +266,10 @@ module Shostak P.add p (P.create [coef, xtau] Q.zero ty), List.rev_append ctx' ctx else let p3, ctx = - try - let p, approx = P.div p1 p2 in - if approx then mk_euc_division p p2 t1 t2 ctx - else p, ctx - with Division_by_zero | Polynome.Maybe_zero -> + match P.div p1 p2 with + | p, approx -> + if approx then mk_euc_division t t1 p2 ctx else p, ctx + | exception Division_by_zero | exception Polynome.Maybe_zero -> P.create [Q.one, X.term_embed t] Q.zero ty, ctx in P.add p (P.mult_const coef p3), ctx @@ -287,13 +294,10 @@ module Shostak else let p3, ctx = try P.modulo p1 p2, ctx - with e -> - let t = E.mk_term mod_symb [t1; t2] Ty.Tint in - let ctx = match e with - | Division_by_zero | Polynome.Maybe_zero -> ctx - | Polynome.Not_a_num -> mk_modulo t t1 t2 p2 ctx - | _ -> assert false - in + with + | Polynome.Not_a_num -> mk_modulo t1 p1 p2 ctx + | Division_by_zero | Polynome.Maybe_zero -> + let t = E.mk_term mod_symb [t1; t2] Tint in P.create [Q.one, X.term_embed t] Q.zero ty, ctx in P.add p (P.mult_const coef p3), ctx From 4d686a5d153ca18ee1caa8484cafa05f59d90aa1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Thu, 19 Oct 2023 10:24:25 +0200 Subject: [PATCH 2/2] Review comments and simplifications --- src/lib/reasoners/arith.ml | 57 +++++++++++++++++--------------------- 1 file changed, 26 insertions(+), 31 deletions(-) diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index 26d4d2aad..2e958ed1d 100644 --- a/src/lib/reasoners/arith.ml +++ b/src/lib/reasoners/arith.ml @@ -134,24 +134,7 @@ module Shostak | Some p -> p | _ -> P.create [Q.one, r] Q.zero (X.type_info r) - (* Compute [t1 % t2] as [t1 - |t2| * (t1 / |t2|)]. - - Requires: [t1], [t2] have type [Tint] - Requires: [p1] is the representative for [t1] - Requires: [p2] is the representative for [t2] - Requires: [p2] is a non-zero constant *) - let mk_modulo t1 p1 p2 ctx = - match P.is_const p2 with - | Some n2 -> - let a2 = Q.to_z n2 |> Z.abs in - assert (Z.sign a2 > 0); - - (* NB: [t1 % t2] = [t1 % |t2|] *) - let div, ctx' = X.make (E.Ints.(t1 / ~$$a2)) in - P.sub p1 (P.mult_const (Q.from_z a2) (embed div)), ctx' @ ctx - | None -> assert false - - (* Add range information for [t = t1 / t2]. + (* Add range information for [t = t1 / t2], where `/` is euclidean division. Requires: [t], [t1], [t2] have type [Tint] Requires: [p2] is the term representative for [t2] @@ -161,19 +144,31 @@ module Shostak match P.is_const p2 with | Some n2 -> - let a2 = Q.to_z n2 |> Z.abs in - assert (Z.sign a2 > 0); + let n2 = Q.to_z n2 in + assert (Z.sign n2 <> 0); + let a2 = Z.abs n2 in + + (* 0 <= t1 % t2 = t1 - t2 * (t1 / t2) < |t2| *) + let t1_mod_t2 = E.Ints.(t1 - ~$$n2 * t) in + let c1 = E.Ints.(~$0 <= t1_mod_t2) in + let c2 = E.Ints.(t1_mod_t2 < ~$$a2) in + P.create [Q.one, X.term_embed t] Q.zero Tint, c2 :: c1 :: ctx + | None -> assert false - if Q.sign n2 < 0 then - (* t1 / (-|t2|) = -(t1 / |t2|)*) - let r, ctx' = X.make E.Ints.(t1 / ~$$a2) in - P.mult_const Q.m_one (embed r), ctx' @ ctx - else - (* 0 <= t1 % t2 = t1 - t2 * (t1 / t2) < |t2| *) - let t1_mod_t2 = E.Ints.(t1 - ~$$a2 * t) in - let c1 = E.Ints.(~$0 <= t1_mod_t2) in - let c2 = E.Ints.(t1_mod_t2 < ~$$a2) in - P.create [Q.one, X.term_embed t] Q.zero Tint, c2 :: c1 :: ctx + + (* Compute the remainder of euclidean division [t1 % t2] as + [t1 - t2 * (t1 / t2)], where `a / b` is euclidean division. + + Requires: [t1], [t2] have type [Tint] + Requires: [p1] is the representative for [t1] + Requires: [p2] is the representative for [t2] + Requires: [p2] is a non-zero constant *) + let mk_euc_modulo t1 t2 p1 p2 ctx = + match P.is_const p2 with + | Some n2 -> + assert (Q.sign n2 <> 0); + let div, ctx = mk_euc_division E.Ints.(t1 / t2) t1 p2 ctx in + P.sub p1 (P.mult_const n2 div), ctx | None -> assert false @@ -295,7 +290,7 @@ module Shostak let p3, ctx = try P.modulo p1 p2, ctx with - | Polynome.Not_a_num -> mk_modulo t1 p1 p2 ctx + | Polynome.Not_a_num -> mk_euc_modulo t1 t2 p1 p2 ctx | Division_by_zero | Polynome.Maybe_zero -> let t = E.mk_term mod_symb [t1; t2] Tint in P.create [Q.one, X.term_embed t] Q.zero ty, ctx