Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Do not use existential variables for integer division #881

Merged
merged 2 commits into from
Oct 19, 2023
Merged

Do not use existential variables for integer division #881

Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
ebe31e6
Do not use existential variables for integer division
bclement-ocp Oct 12, 2023
4d686a5
Review comments and simplifications
bclement-ocp Oct 19, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
94 changes: 49 additions & 45 deletions src/lib/reasoners/arith.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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|)].
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I know the division symbol / here means the integer division but at the first sight, it was a bit confusing as the fact t1 and t2 are integer is mentioned later. We may precise that / is the integer division?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure, added a note that / is Euclidean division here, and that % is the remainder of Euclidean division. Also renamed the function mk_euc_modulo.


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 *)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The previous comment gave a precise definition of the modulo used by Arith.

  (* t1 % t2 = md  <->
     c1. 0 <= md ;
     c2. md < t2 ;
     c3. exists k. t1 = t2 * k + t ;
     c4. t2 <> 0 (already checked) *)

It's meaningful to know that we choose an integer between 0and t2 as the representative element of the equivalence classes of Z/t2Z.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

t1 % t2 here is not an equivalence class, it is defined as the remainder of euclidean division, which is an integer between 0 and |t2| by definition (note that the condition c2 in the pre-existing comment was incorrect because t2 can be negative). Should be clear with the added definition of % as remainder of Euclidean division.

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|] *)
Copy link
Collaborator

@Halbaroth Halbaroth Oct 18, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here the equality = denotes the usual equality relation between integers and this equation is consequence of our choice of representative term for the equivalence classes. I think we should clarify this point.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This follows from the definition of t1 % t2 as the remainder of euclidean division. Anyways, I have removed this to avoid recomputing X.make t1 and call mk_euc_division directly instead.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This follows from the definition of t1 % t2 as the remainder of euclidean division.

It's exactly what I said ;)

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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If I understand well, we don't need to produce here an interval for the case n2 < 0 as the recursive call X.make will produce the appropriate interval for -n2?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, here we just rewrite t1 / (-|t2|) into -(t1 / |t2|) and then we let the recursive call take care of things. Although I am now realizing this means we will compute X.make t1 twice; I will inline the code.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually I have removed the distinction; we will create t1 / n and t1 / (-n) and rely on reasoning to prove they are identical, it is less error-prone.

else
(* 0 <= t1 % t2 = t1 - t2 * (t1 / t2) < |t2| *)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
(* 0 <= t1 % t2 = t1 - t2 * (t1 / t2) < |t2| *)
(* 0 <= t1 % t2 = t1 - |t2| * (t1 / t2) < |t2| *)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think I prefer the version that is always true, even if in this case t2 is positive so t2 = |t2|, I will clarify.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have no strong opinion about it. For me it was clearer that the formula agrees syntactically with the code below.

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 =
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down