使用 Z3_solver_get_unsat_core 获取未饱和核心答案

【问题标题】：getting unsat core using Z3_solver_get_unsat_core使用 Z3_solver_get_unsat_core 获取未饱和核心
【发布时间】：2012-11-15 10:07:46
【问题描述】：

假设这里是非线性实数算术的一组约束，例如

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 将不满足。我想获得未饱和的核心（因为这个例子很简单）。因此，对于这些谓词中的每一个，我都定义了一个谓词变量。假设他们是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);

谢谢，

【问题讨论】：

标签： z3

【解决方案1】：

Z3 包含许多求解器。对于非线性算术问题，它使用nlsat。这个求解器的实现位于目录src/nlsat，算法解释here。但是，当前的nlsat 实现不支持 unsat 核心提取和证明生成。当用户要求提取 unsat core 时，Z3 切换到通用求解器，该求解器对于非线性算术是不完整的。也就是说，对于非线性算术问题，它可能会返回unknown。通用求解器支持许多理论、量词、未饱和核心提取和证明生成。 linear 算术是完整的，但正如我所说，它对于非线性片段来说并不完整。在计划中，Z3会有一个新版本的nlsat，它与其他理论相结合，支持unsat核心提取，但这是未来的工作。

【讨论】：