fix(arith): Do not overly tighten bounds over infinite domains (#1025)

Model generation for arithmetic constraints proceeds in two stages:

 - In the first stage, we only choose a value for variables that are
   within a finite domain (i.e. integer variables bounded from both
   above and below). This is the behavior of regular case splits, and
   happens in function `default_case_split`.

 - In the second stage, which we only reach if model generation is
   enabled, we must select a value for all variables. In this case, we
   select one interval for variables that can have multiple intervals
   (recall that we model arithmetic domains using unions of intervals).
   This happens in function `case_split_union_of_intervals`. If the
   selected interval is finite, we go back to the first stage in the
   next case split.

 - In the final stage, all remaining variables have infinite intervals
   as domains, and we must now pick a value for these. This happens in
   `model_from_unbounded_domains` -- even though for rational variables,
   the domain can still be bounded. For integers however, infinite
   intervals mean that they lack either a finite lower or upper bound
   (or both). For integers, we create a new simplex environment in
   `fm_simplex_unbounded_integers_encoding` where we adjust the bounds
   by a factor of half the sum of the absolute values of the
   coefficients. This means that an inequality `0 < 3x + 4y` becomes
   `0 + (3 + 4) / 2 < 3x + 4y`, i.e. `3.5 < 3x + 4y`. This removes
   `x = 1, y = 0` from the domain. On its own, this would be correct
   (albeit strange) because after removing a finite number of
   elements from an infinite domain there is still an infinite number of
   elements to choose from. But within a larger system this can (and is)
   problematic.

This patch removes the "adjustment" of the bounds which is not justified
and actually causes unsoundness.

Fixes #1022

Co-authored-by: Guillaume Bury <[email protected]>

src/lib/reasoners/intervalCalculus.ml

@@ -1921,37 +1921,19 @@ let fm_simplex_unbounded_integers_encoding env uf =
            "case-split over unions of intervals is needed !!!";
          assert false
 
-       | [(mn, ex_mn), (mx, ex_mx)] ->
+       | [(lb, ex_lb), (ub, ex_ub)] ->
          let l, c = P.to_list p in
-         let l = List.rev_map (fun (c, x) -> x, c) (List.rev l) in
-         assert (Q.sign c = 0);
-         let cst0 =
-           List.fold_left (fun z (_, c) -> Q.add z (Q.abs c))Q.zero l
-         in
-         let cst = Q.div cst0 (Q.from_int 2) in
-         assert (mn == None || mx == None);
-         let min =
-           let mn =
-             match mn with
-             | None -> None
-             | Some (q, q') -> Some (Q.add q cst, q')
-           in
-           bnd_to_simplex_bound (mn, ex_mn)
-         in
-         let max =
-           let mx =
-             match mx with
-             | None -> None
-             | Some (q, q') -> Some (Q.sub q cst, q')
-           in
-           bnd_to_simplex_bound (mx, ex_mx)
-         in
+         assert (Q.is_zero c);
+         assert (lb == None || ub == None);
+         let min = bnd_to_simplex_bound (lb, ex_lb) in
+         let max = bnd_to_simplex_bound (ub, ex_ub) in
          match l with
          | [] -> assert false
-         | [x, c] ->
+         | [c, x] ->
            assert (Q.is_one c);
            Sim.Assert.var simplex x ?min ?max |> fst
          | _ ->
+           let l = List.rev_map (fun (c, x) -> x, c) (List.rev l) in
            let xp = alien_of p in
            let sim_p =
              match Sim.Core.poly_of_slake simplex xp with
@@ -2009,7 +1991,7 @@ let model_from_simplex sim is_int env uf =
       )[] (List.rev main_vars)
 
 
-let model_from_unbounded_domains =
+let model_from_infinite_domains =
   let mk_cs acc (x, v, _ex) =
     ((LR.view (LR.mk_eq x v)), true,
      Th_util.CS (Th_util.Th_arith, Q.from_int 2)) :: acc
@@ -2040,7 +2022,7 @@ let case_split env uf ~for_model =
     else
       begin
         match case_split_union_of_intervals env uf with
-        | [] -> model_from_unbounded_domains env uf
+        | [] -> model_from_infinite_domains env uf
         | l -> l
       end
   | _ -> res

tests/issues/777.models.expected

@@ -1,5 +1,5 @@
 
 unknown
 (
-  (define-fun i () Int 2)
+  (define-fun i () Int 1)
 )

tests/models/uf/uf2.models.expected

@@ -1,7 +1,7 @@
 
 unknown
 (
-  (define-fun f ((arg_0 Int)) Int (ite (= arg_0 (- 2)) 0 2))
+  (define-fun f ((arg_0 Int)) Int (ite (= arg_0 (- 1)) 0 1))
   (define-fun a () Int 0)
-  (define-fun b () Int (- 2))
+  (define-fun b () Int (- 1))
 )