问题描述
我正在使用 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既不高效,也不可靠,也不维护,因此我建议您不要广泛使用它,而仅用于理解目的