Z3_solver_check返回Z3_L_UNDEF咨询：约束矛盾未返回Z3_L_FALSE

问题代码 #

Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_del_config(cfg);
Z3_solver theSolver = mk_solver(ctx);

Z3_sort domainSort = Z3_mk_bv_sort(ctx, 32);
Z3_sort rangeSort = Z3_mk_bv_sort(ctx, 8);
Z3_sort arr_sort = Z3_mk_array_sort(ctx, domainSort, rangeSort);

Z3_symbol arr_name = Z3_mk_string_symbol(ctx, "fqv");
Z3_ast fqv_arr = Z3_mk_const(ctx, arr_name, arr_sort);

Z3_ast idx = Z3_mk_concat(
        ctx, 
        Z3_mk_select(ctx, fqv_arr, Z3_mk_int(ctx, 1, domainSort)),
        Z3_mk_select(ctx, fqv_arr, Z3_mk_int(ctx, 0, domainSort))
    );
idx = Z3_mk_concat(ctx, Z3_mk_select(ctx, fqv_arr, Z3_mk_int(ctx, 2, domainSort)), idx);
idx = Z3_mk_concat(ctx, Z3_mk_select(ctx, fqv_arr, Z3_mk_int(ctx, 3, domainSort)), idx);

arr_name = Z3_mk_string_symbol(ctx, "a");
Z3_ast a_arr = Z3_mk_const(ctx, arr_name, arr_sort);

arr_name = Z3_mk_string_symbol(ctx, "b");
Z3_ast b_arr = Z3_mk_const(ctx, arr_name, arr_sort);

Z3_ast body = Z3_mk_eq(ctx, Z3_mk_select(ctx, a_arr, idx), Z3_mk_select(ctx, b_arr, idx));

Z3_app bound_vars[] = {(Z3_app) fqv_arr};
int num_bound_vars = 1;
int weight = 0;
Z3_ast forall = Z3_mk_forall_const(ctx, weight, num_bound_vars, bound_vars, 0, 0, body);

Z3_ast a0 = Z3_mk_select(ctx, a_arr, Z3_mk_int(ctx, 0, domainSort));
Z3_ast b0 = Z3_mk_select(ctx, b_arr, Z3_mk_int(ctx, 0, domainSort));

Z3_solver_assert(ctx, theSolver, forall);
Z3_solver_assert(ctx, theSolver, Z3_mk_eq(ctx, Z3_mk_false(ctx), Z3_mk_eq(ctx, a0, b0)));

约束说明 #

• 量词约束：∀fqv: a[concat(fqv[3], fqv[2], fqv[1], fqv[0])] = b[concat(fqv[3], fqv[2], fqv[1], fqv[0])]
• 直接约束：a[0] ≠ b[0]

对应的SMT-LIB表达式：

量词约束 #

(forall ((fqv (Array (_ BitVec 32) (_ BitVec 8))))
  (! (= (select a
                (concat (select fqv #x00000003)
                        (concat (select fqv #x00000002)
                                (concat (select fqv #x00000001)
                                        (select fqv #x00000000)))))
        (select b
                (concat (select fqv #x00000003)
                        (concat (select fqv #x00000002)
                                (concat (select fqv #x00000001)
                                        (select fqv #x00000000)))))
     :weight 0))

直接约束 #

(= false (= (select a #x00000000) (select b #x00000000)))

问题现象 #

调用Z3_solver_check(ctx, theSolver)返回Z3_L_UNDEF，但预期应返回Z3_L_FALSE（因为若a、b对所有通过上述方式生成的索引都相等，那么索引0必然满足a[0]=b[0]，与第二个约束矛盾）。注释第二个约束时，返回结果为预期的Z3_L_TRUE。调用Z3_solver_get_reason_unknown得到：

reason for last failure: smt tactic failed to show goal to be sat/unsat (incomplete (theory array))

原因分析 #

你想要表达的实际约束是“对所有32位索引idx，a[idx] = b[idx]”，但当前代码错误地将量词变量设为数组类型的fqv，而非32位位向量类型的idx。虽然从语义上看，遍历所有fqv数组时，concat(fqv[3], fqv[2], fqv[1], fqv[0])可以覆盖所有32位索引值，但Z3的量词实例化策略对这种嵌套数组访问的模式支持不足：

1. 数组理论的量词推理本身存在不完备性，尤其是当量词变量是数组，且约束中包含数组元素拼接成新索引的复杂结构时；
2. Z3默认的求解策略无法自动生成足够的实例来触发矛盾（比如无法自动推导出存在某个fqv使得拼接后的idx等于0，从而将量词约束实例化为a[0]=b[0]，与第二个约束冲突）。

解决方法 #

修改量词约束，直接对32位索引变量进行量化，而非数组变量。修改后的核心代码如下：

// 定义32位索引的排序
Z3_sort idx_sort = Z3_mk_bv_sort(ctx, 32);
// 创建量词变量idx（32位BV）
Z3_symbol idx_name = Z3_mk_string_symbol(ctx, "idx");
Z3_ast idx = Z3_mk_const(ctx, idx_name, idx_sort);
// 量词约束的body：a[idx] = b[idx]
Z3_ast body = Z3_mk_eq(ctx, Z3_mk_select(ctx, a_arr, idx), Z3_mk_select(ctx, b_arr, idx));
// 构造forall约束，绑定变量为idx
Z3_app bound_vars[] = {(Z3_app) idx};
int num_bound_vars = 1;
int weight = 0;
Z3_ast forall = Z3_mk_forall_const(ctx, weight, num_bound_vars, bound_vars, 0, 0, body);

修改后，Z3可以直接识别这是对所有索引的全称约束，会自动实例化idx=0的情况，从而推导出矛盾，返回Z3_L_FALSE，符合预期。

内容的提问来源于stack exchange，提问作者Daneshvar Amrollahi