1

我们正在尝试使用 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
4

1 回答 1

0

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

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

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

  start0!3
  (not start0!3)

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

于 2013-07-09T01:27:21.850 回答