1

OCaml API を使用して unsat コアを抽出する単純な 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 が返されます。

4

2 に答える 2

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"
于 2013-02-07T16:25:27.670 に答える
1

("UNSAT_CORE","true");と同じように設定する必要があります("MODEL","true");。

于 2013-02-07T09:09:53.957 に答える