时间戳

首页 > 解决方案 > 原始表达式与围裙中的结果不一致

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

问题描述

我正在使用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'

标签： ocamlpolyhedra

解决方案

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

为什么要这样打印表达式？

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

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

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

推荐阅读