solver_get_unsat_core() 返回空核心

Question

我正在尝试使用 OCaml API 编写一个简单的 Z3 问题来提取未饱和的核心。问题是返回的 unsat 核心不应该是空的。你有什么想法或者你能指出我可能做错了什么吗？

我仅使用 OCaml API 按照 Rise4fun 中的示例进行操作：

let _ =
  (* make a new context:
    * - enable model construction
    * - enable quantifier instantiation
  *)
  let ctx = Z3.mk_context [("MODEL","true"); ("PROOF_MODE", "2"); ("MBQI","true")] in

  (* make a new "default" solver *)
  let solver = Z3.mk_solver ctx in

  (* assert some stupid constraints: exists x: int, y: int.  x < y *)
  let x_symb = Z3.mk_string_symbol ctx "x" in
  let x = Z3.mk_const ctx x_symb (Z3.mk_bool_sort ctx) in

  let y_symb = Z3.mk_string_symbol ctx "y" in
  let y = Z3.mk_const ctx y_symb (Z3.mk_bool_sort ctx) in

  let z_symb = Z3.mk_string_symbol ctx "z" in
  let z = Z3.mk_const ctx z_symb (Z3.mk_bool_sort ctx) in

  let p1_symb = Z3.mk_string_symbol ctx "p1" in
  let p1 = Z3.mk_const ctx p1_symb (Z3.mk_bool_sort ctx) in

  let p2_symb = Z3.mk_string_symbol ctx "p2" in
  let p2 = Z3.mk_const ctx p2_symb (Z3.mk_bool_sort ctx) in

  let p3_symb = Z3.mk_string_symbol ctx "p3" in
  let p3 = Z3.mk_const ctx p3_symb (Z3.mk_bool_sort ctx) in

  let p4_symb = Z3.mk_string_symbol ctx "p4" in
  let p4 = Z3.mk_const ctx p4_symb (Z3.mk_bool_sort ctx) in

  let p5_symb = Z3.mk_string_symbol ctx "p5" in
  let p5 = Z3.mk_const ctx p5_symb (Z3.mk_bool_sort ctx) in

  let p6_symb = Z3.mk_string_symbol ctx "p6" in
  let p6 = Z3.mk_const ctx p6_symb (Z3.mk_bool_sort ctx) in

  (* assert implications *)
  let notx = Z3.mk_not ctx x in
  let noty = Z3.mk_not ctx y in
  let notz = Z3.mk_not ctx z in
  let implies1 = Z3.mk_implies ctx p1 (Z3.mk_or ctx [| x; y|]) in
  Z3.solver_assert ctx solver implies1;

  let implies2 = Z3.mk_implies ctx p2 (Z3.mk_or ctx [| notx; y|]) in
  Z3.solver_assert ctx solver implies2;

  let implies3 = Z3.mk_implies ctx p3 (Z3.mk_or ctx [| x; noty|]) in
  Z3.solver_assert ctx solver implies3;

  let implies4 = Z3.mk_implies ctx p4 (Z3.mk_or ctx [| notx; noty|]) in
  Z3.solver_assert ctx solver implies4;

  let implies5 = Z3.mk_implies ctx p5 (Z3.mk_or ctx [| y; z|]) in
  Z3.solver_assert ctx solver implies5;

  let implies6 = Z3.mk_implies ctx p6 (Z3.mk_or ctx [| y; notz|]) in
  Z3.solver_assert ctx solver implies6;

  (* assert some constraints over p1, ..., p6 *)
  Z3.solver_assert ctx solver p1;
  Z3.solver_assert ctx solver p2;
  Z3.solver_assert ctx solver p3;
  Z3.solver_assert ctx solver p4;
  Z3.solver_assert ctx solver p5;
  Z3.solver_assert ctx solver p6;

  (* check satisfiability *)
  match Z3.solver_check ctx solver with
  | Z3.L_TRUE -> (* SAT *)
      (* get model *)
      let mdl = Z3.solver_get_model ctx solver in
      print_endline "Sat";
      print_endline (Z3.model_to_string ctx mdl)

  | Z3.L_FALSE -> (* UNSAT *)
    let unsat_core = Z3.solver_get_unsat_core ctx solver in
    print_endline "Unsat";
    print_endline "Solver";
    print_endline (Z3.solver_to_string ctx solver);
    print_endline "Unsat Core";
    print_endline (Z3.ast_vector_to_string ctx unsat_core)

  | Z3.L_UNDEF -> (* shrug *)
      print_endline "Unknown"

生成的输出是：

Unsat
Solver
(solver
  (=> p1 (or x y))
  (=> p2 (or (not x) y))
  (=> p3 (or x (not y)))
  (=> p4 (or (not x) (not y)))
  (=> p5 (or y z))
  (=> p6 (or y (not z)))
  p1
  p2
  p3
  p4
  p5
  p6)
Unsat Core
(ast-vector)

显式检查 unsat_core ast_vector 的大小返回 0。有什么想法吗？

Answer 1

如果我使用

Z3.solver_check_assumptions

而不仅仅是

Z3.solver_check

，它对我有用。要使用它，请为每个断言引入新的布尔变量，然后添加这些布尔变量作为假设。例如，我添加了变量

as1

和

as2

作为我的假设。运行这个例子，我得到的结果是：

Unsat
as1
as2

这是示例代码：

let _ =
  (* make a new context:
    * - enable model construction
  *)
  let ctx = Z3.mk_context [("MODEL","true")] in

  (* make a new "default" solver *)
  let solver = Z3.mk_solver ctx in

  (* assert some stupid constraints: exists x: int, y: int.  x < y *)
  let x_symb = Z3.mk_string_symbol ctx "x" in
  let x = Z3.mk_const ctx x_symb (Z3.mk_int_sort ctx) in

  let y_symb = Z3.mk_string_symbol ctx "y" in
  let y = Z3.mk_const ctx y_symb (Z3.mk_int_sort ctx) in

  let as1_symb = Z3.mk_string_symbol ctx "as1" in
  let as1 = Z3.mk_const ctx as1_symb (Z3.mk_bool_sort ctx) in
  let as2_symb = Z3.mk_string_symbol ctx "as2" in
  let as2 = Z3.mk_const ctx as2_symb (Z3.mk_bool_sort ctx) in

  Z3.solver_assert ctx solver (Z3.mk_iff ctx as1 (Z3.mk_lt ctx x y));
  Z3.solver_assert ctx solver (Z3.mk_iff ctx as2 (Z3.mk_lt ctx y x));

  (* check satisfiability *)
  match Z3.solver_check_assumptions ctx solver [| as1; as2 |] with
  | Z3.L_TRUE -> (* SAT *)
      (* get model *)
      let mdl = Z3.solver_get_model ctx solver in
      print_endline "Sat";
      print_endline (Z3.model_to_string ctx mdl)

  | Z3.L_FALSE -> (* UNSAT *)
      print_endline "Unsat";
      let core = Z3.solver_get_unsat_core ctx solver in
      for i = 0 to (Z3.ast_vector_size ctx core) - 1 do
        print_endline (Z3.ast_to_string ctx (Z3.ast_vector_get ctx core i))
      done

  | Z3.L_UNDEF -> (* shrug *)
      print_endline "Unknown"

Answer 2

您需要像设置

("UNSAT_CORE","true");

一样设置

("MODEL","true");

。