inconsistencies between the original expression and the result one in apron

Question

I'm using the OCaml interface of the Apron library.

When I want to reduce the expression [| x + y -2 >= 0; x + y > - 3=0|], the result of tab is [|-3 + 1 * x + 1 * y >= 0|], How can I get the origin expression x + y - 3 >= 0?

let _ =
  let vx = Var.of_string "x" in
  let vy = Var.of_string "y" in
  let env = Environment.make [||] [|vx;vy|] in
  let c = Texpr1.cst env (Coeff.s_of_int 2) in
  let c' = Texpr1.cst env (Coeff.s_of_int 3) in
  let vx' =  Texpr1.var env vx in
  let vy' = Texpr1.var env vy in
  let texpr = Texpr1.binop Add vx' vy' Real Near in
  let texpr1 = Texpr1.binop Sub texpr c Real Near in
  let texpr2 = Texpr1.binop Sub texpr c' Real Near in
  (* let sum' = Texpr1.(Binop(Sub,x2,Cst c,Int,Near)) in *)
  Format.printf "env = %a@." (fun x -> Environment.print x) env;
  Format.printf "expr = %a@." (fun x -> Texpr1.print x) texpr;
  let cons1 = Tcons1.make texpr1 Lincons0.SUPEQ in
  let cons2 = Tcons1.make texpr2 Lincons0.SUPEQ in

  let tab = Tcons1.array_make env 2 in
  Tcons1.array_set tab 0 cons1;
  Tcons1.array_set tab 1 cons2;
  let abs = Abstract1.of_tcons_array manpk env tab in
  let tab' = Abstract1.to_tcons_array manpk abs in
  Format.printf "tab = %a@." (fun x -> Tcons1.array_print x) tab;
  Format.printf "tab1 = %a@." (fun x -> Tcons1.array_print x) tab'

Answer 1

It seems to me that there is no inconsistency as the expressions -3 + 1 * x + 1 * y >= 0 and x + y - 3 >= 0 are semantically equivalent.

Why is the expression printed this way?

You are building a polyhedron (i'm guessing manpk refers to the polka manager) and even if it is built using tree-constraints, it is represented internally using linear-constraints. So when you convert it back to tree-constraints, you actually are converting a Lincons1.earray to a Tcons1.earray, hence the representation as a sum of monoms.

If by "get the origin expression" you mean, make Apron print it in a human friendly way, i suggest you convert your polyhedron to a linear-constraint array (using to_lincons_array) and then define your own pretty-printing utility over linear constraints.

Alternatively, you can use the Apronext library, which is a small wrapper I wrote around the Apron library which provides pp_print functions. On your specific example, using Linconsext.pp_print, you get: x+y>=3. Disclaimer, Apronext is neither efficient, nor reliable, nor maintained, so i suggest you dont use it extensively, but only for understanding purposes