'best' and 'exact' flags not set correctly for octagons?

[SantiagoBautista]

Hello,
I am new to using Apron, and I have the impression that the flags 'best' and 'exact' are not accurately modified when using the octagon domain.

The example that makes me think so is the following:

open Apron

let manoct = Oct.manager_alloc ()

let var_x = Var.of_string "x"
let var_y = Var.of_string "y"

let env_xy = Environment.make [||] [|var_x; var_y|]

let ex() =
  (*** Creating an abstract value for the point [x=1; y=3] ***)
  let cons1 = Lincons1.array_make env_xy 2 in
  (* Constraint x - 1 = 0  *)
  let eq1_expr1 = Linexpr1.make env_xy in
  Linexpr1.set_array eq1_expr1
    [|
      (Coeff.Scalar (Scalar.of_frac   1  1), var_x);
    |]
    (Some (Coeff.Scalar (Scalar.of_frac (-1) 1)));
  Lincons1.array_set cons1 0 (Lincons1.make eq1_expr1 Lincons1.EQ);

  (* Constraint y - 3 = 0 *)
  let eq2_expr1 = Linexpr1.make env_xy in
  Linexpr1.set_array eq2_expr1
    [|
      (Coeff.Scalar (Scalar.of_frac   1  1), var_y);
    |]
    (Some (Coeff.Scalar (Scalar.of_frac (-3) 1)));
  Lincons1.array_set cons1 1 (Lincons1.make eq2_expr1 Lincons1.EQ);

  (*** Creating an abstract value for the point [x=1; y=4] ***)
  let cons2 = Lincons1.array_make env_xy 2 in
  (* Constraint x - 1 = 0 *)
  let eq1_expr2 = Linexpr1.make env_xy in
  Linexpr1.set_array eq1_expr2
    [|
      (Coeff.Scalar (Scalar.of_frac   1  1), var_x);
    |]
    (Some (Coeff.Scalar (Scalar.of_frac (-1) 1)));
  Lincons1.array_set cons2 0 (Lincons1.make eq1_expr2 Lincons1.EQ);
  (* Constraint y - 4 = 0 *)
  let eq2_expr2 = Linexpr1.make env_xy in
  Linexpr1.set_array eq2_expr2
    [|
      (Coeff.Scalar (Scalar.of_frac   1  1), var_y);
    |]
    (Some (Coeff.Scalar (Scalar.of_frac (-4) 1)));
  Lincons1.array_set cons2 1 (Lincons1.make eq2_expr2 Lincons1.EQ);

  (*** Set the 'flags wanted' flags ***)
  let opt = Manager.get_funopt manoct Funid_join in
  Manager.set_funopt manoct Funid_join {opt with flag_exact_wanted = true; flag_best_wanted = true};
  
  (* The corresponding abstract values *)
  let u = Abstract1.of_lincons_array manoct env_xy cons1 in
  let v = Abstract1.of_lincons_array manoct env_xy cons2 in
  (* The join of the two points *)
  let res = Abstract1.join manoct u v in
  
  (* Printing of the different values and the flags *)
  let best = Manager.get_flag_best manoct in
  let exact = Manager.get_flag_exact manoct in
  Format.printf "u=%a@." Abstract1.print u;
  Format.printf "v=%a@." Abstract1.print v;
  Format.printf "result=%a@." Abstract1.print res;

  print_endline ("exact flag is " ^ Bool.to_string exact);
  print_endline ("best flag is " ^ Bool.to_string best)  
;;

ex();;

In this example, the union of two points cannot be exactly represented as an octagon, and hence the result of the join is a segment. The result is a best abstraction but not an exact abstraction. Nevertheless executing the above code results in the exact flag being true.

Did I misunderstand or misuse something?

In advance, thank you very much for your answers.

[antoinemine]

There was indeed a problem.
The flag was correctly set in the join function, but got overwritten by oct_size, called internally in the OCaml/C binding glue.
This should be fixed by 711aabe.
Closing for now.

Note that exact and best flags have not been much used and tested. They are also overly conservative. For instance, flag_exact will be false unless one element is empty. We don't implement the (complex and costly) algorithm to detect whether the union of two octagons can be exactly represented as an octagon.

[SantiagoBautista]

Thank you very much!