使用 Z3_solver_get_unsat_core 获取 unsat 核心

问题描述

假设这里是非线性实数算法的约束集，如

suppose that here is the set of constraints on nonlinear real arithmetic like

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)

事实上，如果我们这样做

In fact, if we do

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

b 会不满足.我想获得 unsat 核心(对于这个例子是微不足道的).因此，对于这些谓词中的每一个，我都定义了一个谓词变量.假设它们是 p1 和 p2.

b would be unsat. I want to obtain the unsat core (for this example is trivial). So, for each of these predicates I defined a predicate variable. Lets say they are p1 and 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 ,假设);

但这会返回Z3_L_UNDEF，原因是(不完整(理论算术))

我想知道我在哪里犯了错误以及如何解决这个问题.

I am wondering where I am making a mistake and how this issue can be solved.

以下是初始化的方式:

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

Z3 contains many solvers. For nonlinear arithmetic problems it uses nlsat. The implementation of this solver is located in the directory src/nlsat, and the algorithm is explained here. However, the current nlsat implementation does not support unsat core extraction nor proof generation. When unsat core extraction is requested by the user, Z3 switches to a general purpose solver which is incomplete for nonlinear arithmetic. That is, it may return unknown for nonlinear arithmetic problems. The general purpose solver has support for many theories, quantifier, unsat core extraction, and proof generation. It is complete for linear arithmetic, but as I said it is not complete for the nonlinear fragment. In the plan, Z3 will have a new version of nlsat that is integrated with other theories and support unsat core extraction, but this is future work.

这篇关于使用 Z3_solver_get_unsat_core 获取 unsat 核心的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！