如何通过Z3 OCaml API检测优化问题的目标是否无界？

Z3原生提供了针对优化问题的状态查询能力，不用反复添加约束试探。在OCaml API里，你可以通过以下步骤直接判断目标函数是否无界：

• 调用优化器的Optimize.check方法执行求解
• 通过Optimize.get_status获取求解状态，Z3的状态枚举包含UNBOUNDED选项——如果目标函数可以无限增大（或减小，取决于优化方向），该状态会直接返回

举个简单的OCaml代码示例：

open Z3

let () =
  let ctx = mk_context [] in
  let opt = Optimize.mk_opt ctx in
  let x = Arithmetic.Integer.mk_const ctx (Symbol.mk_string ctx "x") in
  (* 添加约束：x > 0 *)
  Optimize.add_goal opt (Arithmetic.mk_gt ctx x (Arithmetic.Integer.mk_numeral_i ctx 0)) None;
  (* 目标：最大化x *)
  Optimize.maximize opt x None;
  let status = Optimize.check opt [] in
  match status with
  | Solver.UNSATISFIABLE -> print_endline "无解"
  | Solver.SATISFIABLE -> print_endline "有界，存在最优解"
  | Solver.UNBOUNDED -> print_endline "目标函数无界"

这个状态判断仅需在调用Optimize.check后执行，Z3会自动分析约束空间，判断是否存在无限优化的可能，完全无需手动添加额外约束验证。你之前想到的试探方法虽然可行，但确实冗余，原生状态查询是更高效的方案。

内容的提问来源于stack exchange，提问作者David Monniaux