1

C API (ScalaZ3 経由) を介して、z3 を使用して証明を生成しようとしています。したがって、PROOF=true を設定することで証明の生成を有効にします。ただし、これは他のチェックの結果に影響します。戦術/目標を使用しないことに注意してください。新しいソルバーを作成し、制約とチェックをアサートするだけです。

たとえば、次の制約 (x は Integer 型) の場合:

(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

ソルバー オブジェクトに送信される式は、2 つの異なるログで異なります。最初のログでは、次の式がアサートされます。

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

Z3 は正しく報告しますsat。2 番目のログでは、次の式がアサートされます。

  start0!3
  (not start0!3)

ログが正しく生成されたかどうかを確認していただけますか? 各「assert」呼び出しの前にそれらを印刷することにより、独自の assert を追跡することもできます。また、Valgrind を使用してログを実行しましたが、メモリの破損は検出されませんでした。

于 2013-07-09T01:27:21.850 に答える