原始表达式与围裙中的结果不一致

如何解决原始表达式与围裙中的结果不一致

我正在使用 Apron 库的 OCaml 接口。

当我想减少表达式[| x + y -2 >= 0; x + y > - 3=0|]时，tab的结果是[|-3 + 1 * x + 1 * y >= 0|]，我怎样才能得到原表达式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'

解决方法

在我看来没有不一致，因为表达式 -3 + 1 * x + 1 * y >= 0 和 x + y - 3 >= 0 在语义上是等效的。

为什么这个表达式是这样打印的？

您正在构建一个多面体（我猜 manpk 指的是 polka 管理器），即使它是使用树约束构建的，它也使用线性约束在内部表示。因此，当您将其转换回树约束时，您实际上是将 Lincons1.earray 转换为 Tcons1.earray，因此表示为单体的总和。

如果您的意思是“获取原点表达式”，请让 Apron 以人性化的方式打印它，我建议您将多面体转换为线性约束数组（使用 to_lincons_array），然后定义自己的漂亮-超过线性约束的打印实用程序。

或者，您可以使用 Apronext 库，这是我围绕 Apron 库编写的一个小包装器，它提供了 pp_print 函数。在您的具体示例中，使用 Linconsext.pp_print，您会得到：x+y>=3。 免责声明，Apronext既不高效，也不可靠，也不维护，因此我建议您不要广泛使用它，而仅用于理解目的