PROOF_MODE 影响检查结果

【问题标题】：PROOF_MODE affects outcome of checkPROOF_MODE 影响检查结果
【发布时间】：2023-03-29 13:40:01
【问题描述】：

我们正在尝试使用 z3 通过 C API（通过 ScalaZ3）生成证明。 因此，我们通过设置 PROOF=true 来启用证明生成。然而，这会影响其他检查的结果。请注意，我们不使用策略/目标，我们只是创建一个新的求解器并断言约束并进行检查。

例如，基于以下约束（其中 x 是整数）：

(x + x) != (2 * x)

check() 按预期返回带有 PROOF=false 的 UNSAT。然而，如果 PROOF=true，它会返回带有模型 (x -> 1) 的 SAT。

我们没有特别指定任何逻辑。我们尝试通过 QF_AUFLIA 明确请求求解器，但不清楚该逻辑是否被静默忽略/未知，或者它是否对此问题没有影响。当请求证明生成时，似乎 + 变得无法解释。

这种 proof_generation 模式是否遗漏了一些明显的东西？

编辑 2：

我们正在调试模式下使用来自 git (5b5a474b5443) 的最新不稳定版本。

这是我们使用 PROOF=true 得到的跟踪：

R
C 3
= 0x7f04a0091a08
R
P 0x7f04a0091a08
S "MODEL"
S "true"
C 5
R
P 0x7f04a0091a08
S "TYPE_CHECK"
S "true"
C 5
R
P 0x7f04a0091a08
S "PROOF"
S "true"
C 5
R
P 0x7f04a0091a08
S "WELL_SORTED_CHECK"
S "true"
C 5
R
I 1
C 273
R
P 0x7f04a0091a08
C 7
= 0x7f04a00abda8
R
P 0x7f04a00abda8
C 33
= 0x7f04a00915e8
R
P 0x7f04a00abda8
P 0x7f04a00915e8
C 9
R
P 0x7f04a00abda8
C 32
= 0x7f04a007a2c8
R
P 0x7f04a00abda8
P 0x7f04a007a2c8
C 9
R
P 0x7f04a00abda8
S "Unit"
C 30
R
P 0x7f04a00abda8
S "Unit"
C 30
R
P 0x7f04a00abda8
S "isUnit"
C 30
R
P 0x7f04a00abda8
$ |Unit|
$ |isUnit|
U 0
s 0
p 0
u 0
C 41
= 0x7f04a00ab4c8
R
P 0x7f04a00abda8
U 1
P 0x7f04a00ab4c8
p 1
C 44
= 0x7f04a006c218
R
P 0x7f04a00abda8
U 1
$ |Unit|
s 1
P 0
p 1
P 0x7f04a006c218
p 1
C 46
@ 0x7f04a00ab1c8 3 0
@ 0x7f04a006c218 4 0
R
P 0x7f04a00abda8
P 0x7f04a006c218
C 45
R
P 0x7f04a00abda8
P 0x7f04a00ab4c8
U 0
P 0
P 0
p 0
C 47
* 0x7f04a00ab2f8 3
* 0x7f04a00ab0f8 4
R
P 0x7f04a00abda8
P 0x7f04a00ab2f8
C 9
R
P 0x7f04a00abda8
P 0x7f04a00ab0f8
C 9
R
P 0x7f04a00abda8
P 0x7f04a00ab1c8
C 9
R
P 0x7f04a00abda8
P 0x7f04a00ab2f8
U 0
p 0
C 49
= 0x7f04a006ab98
R
P 0x7f04a00abda8
P 0x7f04a006ab98
C 9
R
P 0x7f04a00abda8
C 32
= 0x7f04a007a2c8
R
P 0x7f04a00abda8
P 0x7f04a00915e8
P 0x7f04a007a2c8
C 37
= 0x7f04a00ab538
R
P 0x7f04a00abda8
P 0x7f04a00ab538
C 9
R
P 0x7f04a00abda8
S "card"
U 1
P 0x7f04a00ab538
p 1
P 0x7f04a00915e8
C 51
= 0x7f04a007a588
R
P 0x7f04a00abda8
P 0x7f04a007a588
C 9
R
P 0x7f04a00abda8
S "setMin"
U 1
P 0x7f04a00ab538
p 1
P 0x7f04a00915e8
C 51
= 0x7f04a00ab3e8
R
P 0x7f04a00abda8
P 0x7f04a00ab3e8
C 9
R
P 0x7f04a00abda8
S "setMax"
U 1
P 0x7f04a00ab538
p 1
P 0x7f04a00915e8
C 51
= 0x7f04a00ab068
R
P 0x7f04a00abda8
P 0x7f04a00ab068
C 9
R
P 0x7f04a00abda8
U 0
s 0
p 0
p 0
C 46
R
P 0x7f04a00abda8
S "QF_AUFLIA"
C 30
R
P 0x7f04a00abda8
$ |QF_AUFLIA|
C 412
= 0x7f04a00bfb38
R
P 0x7f04a00abda8
P 0x7f04a00bfb38
C 417
R
P 0x7f04a00abda8
S "start0"
P 0x7f04a007a2c8
C 52
= 0x7f04a00bfc38
R
P 0x7f04a00abda8
P 0x7f04a00bfc38
C 9
R
P 0x7f04a00abda8
S "x0"
P 0x7f04a00915e8
C 52
= 0x7f04a00a55a8
R
P 0x7f04a00abda8
P 0x7f04a00a55a8
C 9
R
P 0x7f04a00abda8
U 2
P 0x7f04a00a55a8
P 0x7f04a00a55a8
p 2
C 64
= 0x7f04a00a51a8
R
P 0x7f04a00abda8
P 0x7f04a00a51a8
C 9
R
P 0x7f04a00abda8
I 2
P 0x7f04a00915e8
C 145
= 0x7f04a00a5528
R
P 0x7f04a00abda8
P 0x7f04a00a5528
C 9
R
P 0x7f04a00abda8
U 2
P 0x7f04a00a5528
P 0x7f04a00a55a8
p 2
C 65
= 0x7f04a00bf478
R
P 0x7f04a00abda8
P 0x7f04a00bf478
C 9
R
P 0x7f04a00abda8
U 2
P 0x7f04a00a51a8
P 0x7f04a00bf478
p 2
C 56
= 0x7f04a00bfd48
R
P 0x7f04a00abda8
P 0x7f04a00bfd48
C 9
R
P 0x7f04a00abda8
P 0x7f04a00bfc38
P 0x7f04a00bfd48
C 60
= 0x7f04a00bfda8
R
P 0x7f04a00abda8
P 0x7f04a00bfda8
C 9
R
P 0x7f04a00abda8
S "x0"
P 0x7f04a00915e8
C 52
= 0x7f04a00a50d8
R
P 0x7f04a00abda8
P 0x7f04a00a50d8
C 9
R
P 0x7f04a00abda8
P 0x7f04a00bfda8
U 2
P 0x7f04a00a55a8
P 0x7f04a00bfc38
p 2
P 0x7f04a00a50d8
P 0x7f04a00bfc38
p 2
C 245
= 0x7f04a00018d8
R
P 0x7f04a00abda8
P 0x7f04a00018d8
C 9
R
P 0x7f04a00abda8
P 0x7f04a00bfb38
P 0x7f04a00bfc38
C 423
R
P 0x7f04a00abda8
P 0x7f04a00bfb38
P 0x7f04a00018d8
C 423
R
P 0x7f04a00abda8
P 0x7f04a00bfb38
C 419
R
P 0x7f04a00abda8
P 0x7f04a00bfb38
U 0
p 0
C 427
R
P 0x7f04a00abda8
P 0x7f04a00bfb38
U 1
C 420
R
P 0x7f04a00abda8
P 0x7f04a00bfb38
C 428
= 0x7f04a011a9e8
R
P 0x7f04a00abda8
P 0x7f04a011a9e8
C 248
R
P 0x7f04a00abda8
P 0x7f04a011a9e8
P 0x7f04a00a50d8
I 0
P 0
C 250
* 0x7f04a00ff678 4
R
P 0x7f04a00abda8
P 0x7f04a00ff678
C 9
R
P 0x7f04a00abda8
P 0x7f04a00ff678
I 0
C 219

这是我们使用 PROOF=false 得到的跟踪：

R
C 3
= 0x7f489c03aef8
R
P 0x7f489c03aef8
S "MODEL"
S "true"
C 5
R
P 0x7f489c03aef8
S "TYPE_CHECK"
S "true"
C 5
R
P 0x7f489c03aef8
S "PROOF"
S "false"
C 5
R
P 0x7f489c03aef8
S "WELL_SORTED_CHECK"
S "true"
C 5
R
I 1
C 273
R
P 0x7f489c03aef8
C 7
= 0x7f489c06fe48
R
P 0x7f489c06fe48
C 33
= 0x7f489c0acba8
R
P 0x7f489c06fe48
P 0x7f489c0acba8
C 9
R
P 0x7f489c06fe48
C 32
= 0x7f489c0112a8
R
P 0x7f489c06fe48
P 0x7f489c0112a8
C 9
R
P 0x7f489c06fe48
S "Unit"
C 30
R
P 0x7f489c06fe48
S "Unit"
C 30
R
P 0x7f489c06fe48
S "isUnit"
C 30
R
P 0x7f489c06fe48
$ |Unit|
$ |isUnit|
U 0
s 0
p 0
u 0
C 41
= 0x7f489c0ccff8
R
P 0x7f489c06fe48
U 1
P 0x7f489c0ccff8
p 1
C 44
= 0x7f489c010c38
R
P 0x7f489c06fe48
U 1
$ |Unit|
s 1
P 0
p 1
P 0x7f489c010c38
p 1
C 46
@ 0x7f489c0ae2f8 3 0
@ 0x7f489c010c38 4 0
R
P 0x7f489c06fe48
P 0x7f489c010c38
C 45
R
P 0x7f489c06fe48
P 0x7f489c0ccff8
U 0
P 0
P 0
p 0
C 47
* 0x7f489c0c3ae8 3
* 0x7f489c0736e8 4
R
P 0x7f489c06fe48
P 0x7f489c0c3ae8
C 9
R
P 0x7f489c06fe48
P 0x7f489c0736e8
C 9
R
P 0x7f489c06fe48
P 0x7f489c0ae2f8
C 9
R
P 0x7f489c06fe48
P 0x7f489c0c3ae8
U 0
p 0
C 49
= 0x7f489c0be318
R
P 0x7f489c06fe48
P 0x7f489c0be318
C 9
R
P 0x7f489c06fe48
C 32
= 0x7f489c0112a8
R
P 0x7f489c06fe48
P 0x7f489c0acba8
P 0x7f489c0112a8
C 37
= 0x7f489c0b5c18
R
P 0x7f489c06fe48
P 0x7f489c0b5c18
C 9
R
P 0x7f489c06fe48
S "card"
U 1
P 0x7f489c0b5c18
p 1
P 0x7f489c0acba8
C 51
= 0x7f489c0739f8
R
P 0x7f489c06fe48
P 0x7f489c0739f8
C 9
R
P 0x7f489c06fe48
S "setMin"
U 1
P 0x7f489c0b5c18
p 1
P 0x7f489c0acba8
C 51
= 0x7f489c0cc1a8
R
P 0x7f489c06fe48
P 0x7f489c0cc1a8
C 9
R
P 0x7f489c06fe48
S "setMax"
U 1
P 0x7f489c0b5c18
p 1
P 0x7f489c0acba8
C 51
= 0x7f489c073768
R
P 0x7f489c06fe48
P 0x7f489c073768
C 9
R
P 0x7f489c06fe48
U 0
s 0
p 0
p 0
C 46
R
P 0x7f489c06fe48
S "QF_AUFLIA"
C 30
R
P 0x7f489c06fe48
$ |QF_AUFLIA|
C 412
= 0x7f489c0714f8
R
P 0x7f489c06fe48
P 0x7f489c0714f8
C 417
R
P 0x7f489c06fe48
S "start0"
P 0x7f489c0112a8
C 52
= 0x7f489c0d5488
R
P 0x7f489c06fe48
P 0x7f489c0d5488
C 9
R
P 0x7f489c06fe48
S "x0"
P 0x7f489c0acba8
C 52
= 0x7f489c0c37d8
R
P 0x7f489c06fe48
P 0x7f489c0c37d8
C 9
R
P 0x7f489c06fe48
U 2
P 0x7f489c0c37d8
P 0x7f489c0c37d8
p 2
C 64
= 0x7f489c0d07b8
R
P 0x7f489c06fe48
P 0x7f489c0d07b8
C 9
R
P 0x7f489c06fe48
I 2
P 0x7f489c0acba8
C 145
= 0x7f489c0cca98
R
P 0x7f489c06fe48
P 0x7f489c0cca98
C 9
R
P 0x7f489c06fe48
U 2
P 0x7f489c0cca98
P 0x7f489c0c37d8
p 2
C 65
= 0x7f489c0b0c08
R
P 0x7f489c06fe48
P 0x7f489c0b0c08
C 9
R
P 0x7f489c06fe48
U 2
P 0x7f489c0d07b8
P 0x7f489c0b0c08
p 2
C 56
= 0x7f489c0cbb78
R
P 0x7f489c06fe48
P 0x7f489c0cbb78
C 9
R
P 0x7f489c06fe48
P 0x7f489c0d5488
P 0x7f489c0cbb78
C 60
= 0x7f489c0cbbd8
R
P 0x7f489c06fe48
P 0x7f489c0cbbd8
C 9
R
P 0x7f489c06fe48
S "x0"
P 0x7f489c0acba8
C 52
= 0x7f489c181a78
R
P 0x7f489c06fe48
P 0x7f489c181a78
C 9
R
P 0x7f489c06fe48
P 0x7f489c0cbbd8
U 2
P 0x7f489c0c37d8
P 0x7f489c0d5488
p 2
P 0x7f489c181a78
P 0x7f489c0d5488
p 2
C 245
= 0x7f489c181a28
R
P 0x7f489c06fe48
P 0x7f489c181a28
C 9
R
P 0x7f489c06fe48
P 0x7f489c0714f8
P 0x7f489c0d5488
C 423
R
P 0x7f489c06fe48
P 0x7f489c0714f8
P 0x7f489c181a28
C 423
R
P 0x7f489c06fe48
P 0x7f489c0714f8
C 419
R
P 0x7f489c06fe48
P 0x7f489c0714f8
U 0
p 0
C 427
R
P 0x7f489c06fe48
P 0x7f489c0714f8
U 1
C 420
R
P 0x7f489c06fe48
P 0x7f489c0714f8
C 430
= 0x7f489c0cc9f8
R
P 0x7f489c06fe48
P 0x7f489c0cc9f8
C 330
R
P 0x7f489c06fe48
P 0x7f489c0cc9f8
C 332

编辑 3：

我创建了一个重现该问题的小型 C 程序：

#include <stdlib.h>
#include <stdio.h>
#include <z3.h>

int main(int argc, char **args) {
    Z3_open_log("z3.log");

    int proofMode = (argc > 1);

    Z3_config conf = Z3_mk_config();

    Z3_set_param_value(conf, "MODEL", "true");
    Z3_set_param_value(conf, "TYPE_CHECK", "true");
    Z3_set_param_value(conf, "WELL_SORTED_CHECK", "true");

    if (proofMode) {
        Z3_set_param_value(conf, "PROOF", "true");
    } else {
        Z3_set_param_value(conf, "PROOF", "false");
    }

    Z3_context ctx   = Z3_mk_context_rc(conf);

    Z3_solver solver = Z3_mk_solver(ctx);

    Z3_sort boolSort = Z3_mk_bool_sort(ctx);
    Z3_sort intSort  = Z3_mk_int_sort(ctx);

    Z3_ast x     = Z3_mk_fresh_const(ctx, "x", intSort);
    Z3_inc_ref(ctx, x);

    Z3_ast newX  = Z3_mk_fresh_const(ctx, "x", intSort);
    Z3_inc_ref(ctx, newX);

    Z3_ast c2    = Z3_mk_int(ctx, 2, intSort);
    Z3_inc_ref(ctx, c2);

    Z3_ast start = Z3_mk_fresh_const(ctx, "start", boolSort);
    Z3_inc_ref(ctx, start);

    Z3_ast xpx_args[2] = {x, x};
    Z3_ast xpx         = Z3_mk_add(ctx, 2, xpx_args);
    Z3_inc_ref(ctx, xpx);

    Z3_ast xt2_args[2] = {c2, x};
    Z3_ast xt2         = Z3_mk_mul(ctx, 2, xt2_args);
    Z3_inc_ref(ctx, xt2);

    Z3_ast dis_args[2] = {xpx, xt2};
    Z3_ast dis         = Z3_mk_distinct(ctx, 2, dis_args);
    Z3_inc_ref(ctx, dis);

    Z3_ast res = Z3_mk_implies(ctx, start, dis);
    Z3_inc_ref(ctx, res);

    printf("AST Before: %s\n", Z3_ast_to_string(ctx, res));

    // Substituting
    Z3_ast substRes = Z3_substitute(ctx, res, 1, &x, &newX);
    Z3_inc_ref(ctx, substRes);

    printf("AST After: %s\n", Z3_ast_to_string(ctx, substRes));

    // Solving
    Z3_solver_assert(ctx, solver, start);
    Z3_solver_assert(ctx, solver, substRes);

    Z3_lbool solverRes = Z3_solver_check(ctx, solver);

    printf("Solver (proofMode=%s) returned %s\n", proofMode ? "true" : "false", (solverRes == Z3_L_FALSE ? "UNSAT" : (solverRes == Z3_L_TRUE ? "SAT" : "UNKNOWN")));

    return 0;
}

使用以下 Makefile：

all: compile runproof runnoproof

compile:
    gcc -o test -I../z3/src/api/ -L ../z3/build/ -lz3 -g -fPIC -O2 -fopenmp test.c

runproof: compile
    LD_LIBRARY_PATH="../z3/build/" ./test proof

runnoproof: compile
    LD_LIBRARY_PATH="../z3/build/" ./test

针对最新的 z3 不稳定，我得到以下结果：

$ make
gcc -o test -I../z3/src/api/ -L ../z3/build/ -lz3 -g -fPIC -O2 -fopenmp test.c

LD_LIBRARY_PATH="../z3/build/" ./test proof
AST Before: (=> start!2 (distinct (+ x!0 x!0) (* 2 x!0)))
AST After: (or (not start!2) (not (= (* 2 x!1) (* 2 x!0))))
Solver (proofMode=true) returned SAT

LD_LIBRARY_PATH="../z3/build/" ./test
AST Before: (=> start!2 (distinct (+ x!0 x!0) (* 2 x!0)))
AST After: (not start!2)
Solver (proofMode=false) returned UNSAT

【问题讨论】：

  • 您使用的是哪个版本？你能创建一个执行跟踪的日志吗？这个链接解释了如何做到这一点：stackoverflow.com/questions/14821687/encoding-returns-unknown/…
  • @leonardo 我已经相应地更新了问题！
  • 上面的跟踪不是用“不稳定”分支（哈希ecceb0accc）生成的。这是来自旧版 Z3 的痕迹。你能检查一下你链接的版本是否正确吗？
  • 确实，对不起。 PROOF_MODE 甚至不再可用作配置参数：现在启用证明生成的唯一方法是使用目标吗？
  • 我们有一个新的参数设置框架。参数按模块组织。 PROOF_MODE 现在称为 PROOF，它是一个布尔参数。我们可以执行z3 -p 列出所有参数。我们也可以使用z3 -pd获得更详细的描述。

标签： z3


【解决方案1】：

发送到求解器对象的公式在两个不同的日志中是不同的。 在第一个日志中，断言了以下公式：

  start0!3
  (or (not start0!3) (not (= (* 2 x0!5) (* 2 x0!4))))

Z3 正确报告sat。 在第二个日志中，断言了以下公式：

  start0!3
  (not start0!3)

您能否检查日志是否正确生成？ 您还可以通过在每次“断言”调用之前打印它们来跟踪您自己的断言。 我还使用 Valgrind 执行了日志，没有检测到内存损坏。

【讨论】：

  • 我想我找到了问题，我们生成了相同的树： (=> start0!4 (distinct (+ x1!5 x1!5) (* 2 x1!5)))用新的 X 替换，当 PROOF_MODE 被禁用时，它会替换所有 X，并且 yield (or (not start0!4) (not (= (* 2 x1!6) (* 2 x1!6)))) 被简化为（不是start0！4）。当启用 PROOF_MODE 时，它只替换它们的子集，产生 (or (not start0!4) (not (= (* 2 x1!6) (* 2 x1!5)))) 是 SAT，因为 x1! 5 和 x1!6 是不同的。启用 PROOF_MODE 时替换有什么特别之处吗？ （我们使用 Z3_substitute）
  • 您使用哪个 API 来应用替换？
  • 我们通过ScalaZ3使用C API
  • 我只使用 C API 创建了一个可重现的小型 C 程序。请参阅编辑 3。
猜你喜欢
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
  • 2019-09-14
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
相关资源
最近更新 更多
热门标签
Java Python linux javascript Mysql C# Docker 算法 前端 SpringBoot Redis Vue spring 设计模式 .net core .net kubernetes c++ 数据库 数据结构 大数据 js 机器学习 微服务 Android Go 程序员 面试 JVM ASP.net core 云原生 人工智能 后端 PHP git CSS golang k8s Nginx Django mybatis 深度学习 多线程 React 架构 devops 爬虫 云计算 Spring Boot LeetCode