2

ここに次のような非線形実数演算に対する一連の制約があるとします。

pred1 = (> (- (* (- v2_x v0_x) (- v1_y v0_y)) (* (- v2_y v0_y) (- v1_x v0_x))) 0)
pred2 = (> (- (* (- v1_x v0_x) (- v2_y v0_y)) (* (- v1_y v0_y) (- v2_x v0_x))) 0)

実際、そうするなら 

Z3_solver_assert(ctx,solver,pred1);
Z3_solver_assert(ctx,solver,pred2);
b = Z3_solver_check(ctx, solver);

b不満だろう。unsat コアを取得したい (この例は簡単なので)。したがって、これらの述語のそれぞれに対して、述語変数を定義しました。それらがp1であるとしましょうp2。

Z3_ast p1 = mk_bool_var(ctx, "P1");
assumptions[i] = Z3_mk_not(ctx, p1);
Z3_ast g[2] = { pred1, p1 };
Z3_solver_assert(ctx,solver,Z3_mk_or(ctx, 2, g));
Z3_ast p2 = mk_bool_var(ctx, "P2");
assumptions[i] = Z3_mk_not(ctx, p2);
Z3_ast g[2] = { pred2, p2 };
Z3_solver_assert(ctx,solver,Z3_mk_or(ctx, 2, g));

そして、私は電話しますZ3_solver_check_assumptions(ctx, solver, 2 , assumptions);

しかし、これは返さZ3_L_UNDEFれ、その理由は(incomplete (theory arithmetic))

どこで間違いを犯しているのか、この問題をどのように解決できるのか疑問に思っています。

物事がどのように初期化されるかは次のとおりです。

  ctx = Z3_mk_context(cfg);
  Z3_symbol logic_symbol = Z3_mk_string_symbol(ctx, "QF_UFNRA");
  solver = Z3_mk_solver_for_logic((Z3_context)ctx, logic_symbol);
  Z3_solver_inc_ref(ctx, solver);
  Z3_params params = Z3_mk_params(ctx);
  Z3_symbol param_symbol = Z3_mk_string_symbol(ctx, "unsat_core");
  Z3_params_set_bool(ctx , params, param_symbol, Z3_L_TRUE);
  Z3_solver_set_params(ctx, solver, params);

ありがとう、

4

1 に答える 1

2

Z3 には多くのソルバーが含まれています。非線形算術問題の場合、 を使用しますnlsat。このソルバーの実装はディレクトリsrc/nlsatにあり、アルゴリズムはここで説明されています。ただし、現在のnlsat実装では、unsat コアの抽出も証明の生成もサポートされていません。ユーザーが unsat コアの抽出を要求すると、Z3 は非線形演算が不完全な汎用ソルバーに切り替えます。つまり、unknown非線形算術問題で返される場合があります。汎用ソルバーは、多くの理論、量化子、unsat コア抽出、証明生成をサポートしています。線形演算については完全ですが、前述したように、非線形フラグメントについては完全ではありません。計画では、Z3 には新しいバージョンのnlsatこれは他の理論と統合され、unsat コアの抽出をサポートしますが、これは将来の作業です。

于 2012-11-29T07:45:47.063 に答える