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